diff --git a/src/org/sosy_lab/java_smt/AxiomProof.java b/src/org/sosy_lab/java_smt/AxiomProof.java new file mode 100644 index 0000000000..78e66ff906 --- /dev/null +++ b/src/org/sosy_lab/java_smt/AxiomProof.java @@ -0,0 +1,31 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt; + +import java.util.Objects; +import org.sosy_lab.java_smt.ResProofRule.ResAxiom; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.proofs.Proof; +import org.sosy_lab.java_smt.basicimpl.AbstractProof; + +public class AxiomProof extends AbstractProof { + + public AxiomProof(ResAxiom rule, Formula formula) { + super( + Objects.requireNonNull(rule, "Rule must not be null"), + Objects.requireNonNull(formula, "Formula must not be null")); + } + + @Override + protected void addChild(Proof pProof) { + super.addChild(pProof); + } +} diff --git a/src/org/sosy_lab/java_smt/ResProofRule.java b/src/org/sosy_lab/java_smt/ResProofRule.java new file mode 100644 index 0000000000..5c5256c11d --- /dev/null +++ b/src/org/sosy_lab/java_smt/ResProofRule.java @@ -0,0 +1,161 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt; + +import java.util.HashMap; +import java.util.Locale; +import java.util.Map; +import org.sosy_lab.java_smt.api.proofs.ProofRule; + +/** + * A proof rule in the proof DAG of the proof format RESOLUTE used by SMTInterpol. See: ... + * + *

The conversion from other formats to RESOLUTE appears to be simple and as such, it is a good + * candidate for a common proof format. + * + * @author Gabriel Carpio + */ +public final class ResProofRule { + + private static final Map RULE_MAP = new HashMap<>(); + + private ResProofRule() { + // prevent instantiation + } + + static { + for (ResAxiom rule : ResAxiom.values()) { + RULE_MAP.put(rule.getName().toLowerCase(Locale.ENGLISH), rule); + } + } + + /** Any operation that proves a term. */ + public enum ResAxiom implements ProofRule { + // Resolution Rule + RESOLUTION("res", "(res t proof1 proof2)"), + ASSUME("assume", "(assume t)"), + // Logical operators + TRUE_POSITIVE("true+", "(+ true)"), + FALSE_NEGATIVE("false-", "(- false)"), + NOT_POSITIVE("not+", "(+ (not p0) + p0)"), + NOT_NEGATIVE("not-", "(- (not p0) - p0)"), + AND_POSITIVE("and+", "(+ (and p0 … pn) - p0 … - pn)"), + AND_NEGATIVE("and-", "(- (and p0 … pn) + pi)"), + OR_POSITIVE("or+", "(+ (or p0 … pn) - pi)"), + OR_NEGATIVE("or-", "(- (or p0 … pn) + p0 … + pn)"), + IMPLIES_POSITIVE("=>+", "(+ (=> p0 … pn) +/- pi)"), + IMPLIES_NEGATIVE("=>-", "(- (=> p0 … pn) - p0 … + pn)"), + EQUAL_POSITIVE1("=+1", "(+ (= p0 p1) + p0 + p1)"), + EQUAL_NEGATIVE1("=-1", "(- (= p0 p1) + p0 - p1)"), + EQUAL_POSITIVE2("=+2", "(+ (= p0 p1) - p0 - p1)"), + EQUAL_NEGATIVE2("=-2", "(- (= p0 p1) - p0 + p1)"), + XOR_POSITIVE("xor+", "(+(xor l1) +(xor l2) -(xor l3))"), + XOR_NEGATIVE("xor-", "(-(xor l1) -(xor l2) -(xor l3))"), + + // Quantifiers + FORALL_POSITIVE("forall+", "(+ (forall x (F x)) - (F (choose x (F x))))"), + FORALL_NEGATIVE("forall-", "(- (forall x (F x)) + (F t))"), + EXISTS_POSITIVE("exists+", "(+ (exists x (F x)) - (F t))"), + EXISTS_NEGATIVE("exists-", "(- (exists x (F x)) + (F (choose x (F x))))"), + + // Equality axioms + REFLEXIVITY("refl", "(+ (= t t))"), + SYMMETRY("symm", "(+(= t0 t1) -(= t1 t0))"), + TRANSITIVITY("trans", "(+(= t0 tn) -(= t0 t1) … -(= tn-1 tn))"), + CONGRUENCE("cong", "(+(= (f t0 … tn) (f t0' … tn')) -(= t0 t0') … -(= tn tn'))"), + EQUALITY_POSITIVE("=+", "(+ (= t0 … tn) -(= t0 t1) … -(= tn-1 tn))"), + EQUALITY_NEGATIVE("=-", "(- (= t0 … tn) +(= ti tj))"), + DISTINCT_POSITIVE("distinct+", "(+ (distinct t0 … tn) +(= t0 t1) … +(= t0 tn) … +(= tn-1 tn))"), + DISTINCT_NEGATIVE("distinct-", "(- (distinct t0 … tn) -(= ti tj))"), + + // ITE, define-fun, annotations + ITE1("ite1", "(+(= (ite t0 t1 t2) t1) - t0)"), + ITE2("ite2", "(+(= (ite t0 t1 t2) t2) + t0)"), + DEL("del!", "(+(= (! t :annotation…) t))"), + EXPAND("expand", "(+(= (f t0 … tn) (let ((x0 t0)…(xn tn)) d)))"), + + // Array Theory + SELECTSTORE1("selectstore1", "(+ (= (select (store a i v) i) v))"), + SELECTSTORE2("selectstore2", "(+ (= (select (store a i v) j) (select a j)) (= i j))"), + EXTDIFF("extdiff", "(+ (= a b) (- (= (select a (@diff a b)) (select b (@diff a b)))))"), + CONST("const", "(+ (= (select (@const v) i) v))"), + + // Linear Arithmetic + POLY_ADD("poly+", "(+ (= (+ a1 ... an) a))"), + POLY_MUL("poly*", "(+ (= (* a1 ... an) a))"), + TO_REAL("to_real", "(+ (= (to_real a) a'))"), + FARKAS("farkas", "(- (<=? a1 b1) ... - (<=? an bn))"), + TRICHOTOMY("trichotomy", "(+ (< a b) (= a b) (< b a))"), + TOTAL("total", "(+ (<= a b) (< b a))"), + GT_DEF("gt_def", "(+ (= (> a b) (< b a)))"), + GE_DEF("ge_def", "(+ (= (>= a b) (<= b a)))"), + DIV_DEF("div_def", "(+ (= a (* b1 ... bn (/ a b1 ... bn))) (= b1 0) ... (= bn 0))"), + NEG_DEF("neg_def", "(+ (= (- a) (* (- 1) a)))"), + NEG_DEF2("neg_def2", "(+ (= (- a b1 ... bn) (+ a (* (- 1) b1)) ... (* (- 1) bn)))"), + ABS_DEF("abs_def", "(+ (= (abs x) (ite (< x 0) (- x) x)))"), + TOTAL_INT("total-int", "(+ (<= a c) (<= (c+1) a))"), + TO_INT_LOW("to_int_low", "(+ (<= (to_real (to_int x)) x))"), + TO_INT_HIGH("to_int_high", "(+ (< x (+ (to_real (to_int x)) 1.0)))"), + DIV_LOW("div_low", "(+ (<= (* d (div x d)) x) (= d 0))"), + DIV_HIGH("div_high", "(+ (< x (+ (* d (div x d)) (abs d))) (= d 0))"), + MOD_DEF("mod_def", "(+ (= (mod x d) (- x (* d (div x d)))) (= d 0))"), + DIVISIBLE_DEF("divisible_def", "(+ (= ((_ divisible c) x) (= x (* c (div x c)))))"), + EXPAND_IS_INT("expand_is_int", "(+ (= (is_int x) (= x (to_real (to_int x)))))"), + + // Data Types + DT_PROJECT("dt_project", "(= (seli (cons a1 ... an)) ai)"), + DT_CONS("dt_cons", "(~ ((_ is cons) x), (= (cons (sel1 x) ... (seln x)) x))"), + DT_TEST_CONS("dt_test_cons", "((_ is cons) (cons a1 ... an))"), + DT_TEST_CONS_PRIME("dt_test_cons_prime", "(~ ((_ is cons') (cons a1 ... an)))"), + DT_EXHAUST("dt_exhaust", "((_ is cons1) x), ..., ((_ is consn) x)"), + DT_ACYCLIC("dt_acyclic", "(~ (= (cons ... x ...) x))"), + DT_MATCH( + "dt_match", + "(= (match t ((p1 x1) c1) ...) (ite ((_ is p1) t) (let (x1 (sel1 t)) c1) ...))"), + ORACLE( + "oracle", + "'The oracle rule can be used to introduce clauses that cannot be easily explained." + + " It should be used as a last resort, if a full low-level proof is too tedious, " + + "or if the axioms for the theory are missing'"); + + private final String name; + private final String formula; + + ResAxiom(String pName, String pFormula) { + name = pName; + formula = pFormula; + } + + @Override + public String getName() { + return name; + } + + @Override + public String getFormula() { + return formula; + } + } + + /** + * Retrieves a ProofRule by its name. + * + * @param name The name of the proof rule. + * @return The matching ProofRule. + * @throws NullPointerException if the name is null. + * @throws IllegalArgumentException if the name does not match any rule. + */ + public static ResAxiom getFromName(String name) { + ResAxiom rule = RULE_MAP.get(name.toLowerCase(Locale.ENGLISH)); + return rule; + } +} diff --git a/src/org/sosy_lab/java_smt/ResolutionProof.java b/src/org/sosy_lab/java_smt/ResolutionProof.java new file mode 100644 index 0000000000..8a0c86dde1 --- /dev/null +++ b/src/org/sosy_lab/java_smt/ResolutionProof.java @@ -0,0 +1,51 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt; + +import java.util.Objects; +import org.sosy_lab.java_smt.ResProofRule.ResAxiom; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.proofs.Proof; +import org.sosy_lab.java_smt.api.proofs.ProofRule; +import org.sosy_lab.java_smt.basicimpl.AbstractProof; + +/** + * This class represents a resolution proof DAG. Its nodes might be of the type {@link AxiomProof} + * or {@link ResolutionProof}. It is used to represent proofs based on the RESOLUTE proof format + * from SMTInterpol. + * + * @see ResProofRule + */ +public class ResolutionProof extends AbstractProof { + // Work in progress. The functionality of producing just nodes should be provided first. + // The idea is to provide extended functionality (by providng a set of edges for example). + + private final Formula pivot; + + @Override + public void addChild(Proof pProof) { + super.addChild(pProof); + } + + public ResolutionProof(Formula formula, Formula pivot) { + super(ResAxiom.RESOLUTION, Objects.requireNonNull(formula, "Formula must not be null")); + this.pivot = Objects.requireNonNull(pivot, "Pivot must not be null"); + } + + public Formula getPivot() { + return pivot; + } + + @Override + public ProofRule getRule() { + return super.getRule(); + } +} diff --git a/src/org/sosy_lab/java_smt/SolverContextFactory.java b/src/org/sosy_lab/java_smt/SolverContextFactory.java index 576285424d..b0f9604700 100644 --- a/src/org/sosy_lab/java_smt/SolverContextFactory.java +++ b/src/org/sosy_lab/java_smt/SolverContextFactory.java @@ -282,7 +282,7 @@ private SolverContext generateContext0(Solvers solverToCreate) case Z3: return Z3SolverContext.create( logger, - config, + Configuration.builder().copyFrom(config).setOption("requireProofs", "true").build(), shutdownNotifier, logfile, randomSeed, diff --git a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java index b5ac3b1455..e908f5ae66 100644 --- a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java @@ -16,6 +16,7 @@ import java.util.Optional; import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; +import org.sosy_lab.java_smt.api.proofs.Proof; /** * Super interface for {@link ProverEnvironment} and {@link InterpolatingProverEnvironment} that @@ -149,6 +150,12 @@ default ImmutableMap getStatistics() { return ImmutableMap.of(); } + /** + * Get proof of unsatisfiability of the conjuction of the current satck of all formulas. Should + * only be called after {@link #isUnsat()} returned true. + */ + Proof getProof() throws SolverException, InterruptedException; + /** * Closes the prover environment. The object should be discarded, and should not be used after * closing. The first call of this method will close the prover instance, further calls are diff --git a/src/org/sosy_lab/java_smt/api/SolverContext.java b/src/org/sosy_lab/java_smt/api/SolverContext.java index 3fbd476c77..100eb55494 100644 --- a/src/org/sosy_lab/java_smt/api/SolverContext.java +++ b/src/org/sosy_lab/java_smt/api/SolverContext.java @@ -52,6 +52,14 @@ enum ProverOptions { */ GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS, + /** + * Whether the solver should generate proofs for unsatisfiable formulas. For Z3, this parameter + * is context(not solver)-based, so for setting it, the extra option in the {@link + * org.sosy_lab.common.configuration.Configuration} instance: "requireProofs" should be set to + * "true". + */ + GENERATE_PROOFS, + /** Whether the solver should enable support for formulae build in SL theory. */ ENABLE_SEPARATION_LOGIC } diff --git a/src/org/sosy_lab/java_smt/api/proofs/Proof.java b/src/org/sosy_lab/java_smt/api/proofs/Proof.java new file mode 100644 index 0000000000..43842b7303 --- /dev/null +++ b/src/org/sosy_lab/java_smt/api/proofs/Proof.java @@ -0,0 +1,36 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.api.proofs; + +import java.util.Set; +import org.sosy_lab.java_smt.api.Formula; + +/** + * A proof node in the proof DAG of a proof. + * + * @author Gabriel Carpio + */ +public interface Proof { + + /** Get the children of the proof node. */ + Set getChildren(); + + boolean isLeaf(); + + /** + * Get the formula of the proof node. + * + * @return The formula of the proof node. + */ + Formula getFormula(); + + ProofRule getRule(); +} diff --git a/src/org/sosy_lab/java_smt/api/proofs/ProofFrame.java b/src/org/sosy_lab/java_smt/api/proofs/ProofFrame.java new file mode 100644 index 0000000000..71677e7ef4 --- /dev/null +++ b/src/org/sosy_lab/java_smt/api/proofs/ProofFrame.java @@ -0,0 +1,53 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.api.proofs; + +/** + * Stores proof related information and gets stored in a stack when processing proofs. Each frame + * contains a proof object and the number of arguments it has. + * + * @param The type of the proof object. + */ +public abstract class ProofFrame { + final T proof; + int numArgs = 0; + boolean visited; + + protected ProofFrame(T proof) { + this.proof = proof; + this.visited = false; + } + + /** Get the proof object. */ + public T getProof() { + return proof; + } + + /** Get the number of arguments the proof object has. */ + public int getNumArgs() { + return numArgs; + } + + /** Check if the frame has been visited. */ + public boolean isVisited() { + return visited; + } + + /** Set the frame as visited. */ + public void setAsVisited(boolean isVisited) { + this.visited = isVisited; + } + + /** Set the number of arguments the proof object has. */ + public void setNumArgs(int numArgs) { + this.numArgs = numArgs; + } +} diff --git a/src/org/sosy_lab/java_smt/api/proofs/ProofRule.java b/src/org/sosy_lab/java_smt/api/proofs/ProofRule.java new file mode 100644 index 0000000000..0199864eb5 --- /dev/null +++ b/src/org/sosy_lab/java_smt/api/proofs/ProofRule.java @@ -0,0 +1,23 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.api.proofs; + +/** A proof rule from a given proof format. */ +public interface ProofRule { + + /** Get the name of the proof rule. */ + String getName(); + + /** Get the formula of the proof rule. */ + default String getFormula() { + return "no formula available"; + } +} diff --git a/src/org/sosy_lab/java_smt/api/proofs/package-info.java b/src/org/sosy_lab/java_smt/api/proofs/package-info.java new file mode 100644 index 0000000000..1d2d7f8a4b --- /dev/null +++ b/src/org/sosy_lab/java_smt/api/proofs/package-info.java @@ -0,0 +1,14 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ +/** + * This package is meant to provide abstract classes and interfaces that are inherited and used all + * over to process proofs from the solvers. + */ +package org.sosy_lab.java_smt.api.proofs; diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java new file mode 100644 index 0000000000..154f6c9e1b --- /dev/null +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProof.java @@ -0,0 +1,116 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.basicimpl; + +import java.util.LinkedHashSet; +import java.util.Set; +import org.checkerframework.checker.nullness.qual.Nullable; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.proofs.Proof; +import org.sosy_lab.java_smt.api.proofs.ProofRule; + +/** + * A proof DAG of a proof. + * + * @author Gabriel Carpio + */ +public abstract class AbstractProof implements Proof { + + // protected abstract class Transformation { + // protected Transformation( + // FormulaCreator formulaCreator, T proof) {} + + // protected abstract Proof generateProof(); + // } + + private final Set children = new LinkedHashSet<>(); + private ProofRule rule; + @Nullable protected Formula formula; + + protected AbstractProof(ProofRule rule, Formula formula) { + this.rule = rule; + this.formula = formula; + } + + // TODO: Use Optional instead of nullable + @Nullable + @Override + public Formula getFormula() { + return this.formula; + } + + @Override + public Set getChildren() { + return this.children; + } + + protected void addChild(Proof child) { + this.children.add(child); + } + + @Override + public ProofRule getRule() { + return rule; + } + + @Override + public boolean isLeaf() { + return getChildren().isEmpty(); + } + + // void setRule(ProofRule rule) { + // this.rule = rule; + // } + + public void setFormula(Formula pFormula) { + formula = pFormula; + } + + public void setRule(ProofRule pRule) { + rule = pRule; + } + + // use this for debugging + public String proofAsString() { + return proofAsString(0); + } + + protected String proofAsString(int indentLevel) { + StringBuilder sb = new StringBuilder(); + String indent = " ".repeat(indentLevel); + + Formula f = getFormula(); + String sFormula; + if (f != null) { + sFormula = f.toString(); + } else { + sFormula = "null"; + } + + sb.append(indent).append("Formula: ").append(sFormula).append("\n"); + sb.append(indent).append("Rule: ").append(getRule().getName()).append("\n"); + sb.append(indent) + .append("No. Children: ") + .append(this.isLeaf() ? 0 : getChildren().size()) + .append("\n"); + sb.append(indent).append("leaf: ").append(isLeaf()).append("\n"); + + int i = 0; + if (!isLeaf()) { + for (Proof child : getChildren()) { + sb.append(indent).append("Child ").append(++i).append(":\n"); + sb.append(((AbstractProof) child).proofAsString(indentLevel + 1)); + } + } + + return sb.toString(); + } +} diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java index 07dbbbb5d6..58cf564605 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractProver.java @@ -26,6 +26,8 @@ import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Evaluator; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; +import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.proofs.Proof; public abstract class AbstractProver implements BasicProverEnvironment { @@ -33,6 +35,7 @@ public abstract class AbstractProver implements BasicProverEnvironment { private final boolean generateAllSat; protected final boolean generateUnsatCores; private final boolean generateUnsatCoresOverAssumptions; + private final boolean generateProofs; protected final boolean enableSL; protected boolean closed = false; @@ -53,6 +56,7 @@ protected AbstractProver(Set pOptions) { generateUnsatCores = pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE); generateUnsatCoresOverAssumptions = pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS); + generateProofs = pOptions.contains(ProverOptions.GENERATE_PROOFS); enableSL = pOptions.contains(ProverOptions.ENABLE_SEPARATION_LOGIC); assertedFormulas.add(LinkedHashMultimap.create()); @@ -77,6 +81,10 @@ protected final void checkGenerateUnsatCoresOverAssumptions() { ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS); } + protected final void checkGenerateProofs() { + Preconditions.checkState(generateProofs, TEMPLATE, ProverOptions.GENERATE_PROOFS); + } + protected final void checkEnableSeparationLogic() { Preconditions.checkState(enableSL, TEMPLATE, ProverOptions.ENABLE_SEPARATION_LOGIC); } @@ -158,4 +166,10 @@ public void close() { closeAllEvaluators(); closed = true; } + + @Override + public Proof getProof() throws InterruptedException, SolverException { + throw new UnsupportedOperationException( + "Proof generation is not available for the current solver."); + } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java index f2bf7435fe..f53b74d506 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java +++ b/src/org/sosy_lab/java_smt/basicimpl/withAssumptionsWrapper/BasicProverWithAssumptionsWrapper.java @@ -18,6 +18,7 @@ import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.proofs.Proof; public class BasicProverWithAssumptionsWrapper> implements BasicProverEnvironment { @@ -128,4 +129,9 @@ public R allSat(AllSatCallback pCallback, List pImportant clearAssumptions(); return delegate.allSat(pCallback, pImportant); } + + @Override + public Proof getProof() throws SolverException, InterruptedException { + return delegate.getProof(); + } } diff --git a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java index c548d30384..d8ad071624 100644 --- a/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/delegate/debugging/DebuggingBasicProverEnvironment.java @@ -18,6 +18,7 @@ import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.proofs.Proof; class DebuggingBasicProverEnvironment implements BasicProverEnvironment { private final BasicProverEnvironment delegate; @@ -93,6 +94,11 @@ public Optional> unsatCoreOverAssumptions( return delegate.unsatCoreOverAssumptions(assumptions); } + @Override + public Proof getProof() throws SolverException, InterruptedException { + return delegate.getProof(); + } + @Override public void close() { debugging.assertThreadLocal(); diff --git a/src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java index 2f194c6125..c20916c683 100644 --- a/src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/delegate/logging/LoggingBasicProverEnvironment.java @@ -24,6 +24,7 @@ import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.Model.ValueAssignment; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.proofs.Proof; /** Wraps a basic prover environment with a logging object. */ class LoggingBasicProverEnvironment implements BasicProverEnvironment { @@ -120,6 +121,12 @@ public ImmutableMap getStatistics() { return wrapped.getStatistics(); } + @Override + public Proof getProof() throws SolverException, InterruptedException { + Proof p = wrapped.getProof(); + return p; + } + @Override public void close() { wrapped.close(); diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java index 49106d6324..d0c6bef146 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBasicProverEnvironment.java @@ -18,6 +18,7 @@ import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.proofs.Proof; import org.sosy_lab.java_smt.delegate.statistics.TimerPool.TimerWrapper; class StatisticsBasicProverEnvironment implements BasicProverEnvironment { @@ -99,6 +100,11 @@ public Optional> unsatCoreOverAssumptions( return delegate.unsatCoreOverAssumptions(pAssumptions); } + @Override + public Proof getProof() throws SolverException, InterruptedException { + return delegate.getProof(); + } + @Override public void close() { delegate.close(); diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java index f0401c6db2..09d5894c60 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironment.java @@ -20,6 +20,7 @@ import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.proofs.Proof; class SynchronizedBasicProverEnvironment implements BasicProverEnvironment { @@ -104,6 +105,11 @@ public ImmutableMap getStatistics() { } } + @Override + public Proof getProof() throws SolverException, InterruptedException { + return delegate.getProof(); + } + @Override public void close() { synchronized (sync) { diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java index 43922ccc25..353e6dbbf5 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBasicProverEnvironmentWithContext.java @@ -22,6 +22,7 @@ import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.SolverContext; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.proofs.Proof; class SynchronizedBasicProverEnvironmentWithContext implements BasicProverEnvironment { @@ -121,6 +122,11 @@ public ImmutableMap getStatistics() { } } + @Override + public Proof getProof() throws SolverException, InterruptedException { + return delegate.getProof(); + } + @Override public void close() { synchronized (sync) { diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java index 85cfb0a23c..816219931b 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5AbstractProver.java @@ -8,7 +8,9 @@ package org.sosy_lab.java_smt.solvers.cvc5; -import com.google.common.base.Preconditions; +import static com.google.common.base.Preconditions.checkState; +import static org.sosy_lab.java_smt.solvers.cvc5.CVC5Proof.generateProofImpl; + import com.google.common.collect.Collections2; import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableMap; @@ -37,6 +39,7 @@ import org.sosy_lab.java_smt.api.Model.ValueAssignment; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.proofs.Proof; import org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat; abstract class CVC5AbstractProver extends AbstractProverWithAllSat { @@ -93,6 +96,9 @@ protected void setSolverOptions( if (pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE)) { pSolver.setOption("produce-unsat-cores", "true"); } + if (pOptions.contains(ProverOptions.GENERATE_PROOFS)) { + pSolver.setOption("produce-proofs", "true"); + } pSolver.setOption("produce-assertions", "true"); pSolver.setOption("dump-models", "true"); @@ -137,7 +143,7 @@ protected void popImpl() { @CanIgnoreReturnValue protected String addConstraint0(BooleanFormula pF) { - Preconditions.checkState(!closed); + checkState(!closed); setChanged(); Term exp = creator.extractInfo(pF); if (incremental) { @@ -151,8 +157,8 @@ protected String addConstraint0(BooleanFormula pF) { @SuppressWarnings("resource") @Override public CVC5Model getModel() throws SolverException { - Preconditions.checkState(!closed); - Preconditions.checkState(!changedSinceLastSatQuery); + checkState(!closed); + checkState(!changedSinceLastSatQuery); checkGenerateModels(); // special case for CVC5: Models are not permanent and need to be closed // before any change is applied to the prover stack. So, we register the Model as Evaluator. @@ -166,7 +172,7 @@ public CVC5Model getModel() throws SolverException { @Override public Evaluator getEvaluator() { - Preconditions.checkState(!closed); + checkState(!closed); checkGenerateModels(); return getEvaluatorWithoutChecks(); } @@ -186,15 +192,15 @@ protected void setChanged() { @Override public ImmutableList getModelAssignments() throws SolverException { - Preconditions.checkState(!closed); - Preconditions.checkState(!changedSinceLastSatQuery); + checkState(!closed); + checkState(!changedSinceLastSatQuery); return super.getModelAssignments(); } @Override @SuppressWarnings("try") public boolean isUnsat() throws InterruptedException, SolverException { - Preconditions.checkState(!closed); + checkState(!closed); closeAllEvaluators(); changedSinceLastSatQuery = false; if (!incremental) { @@ -221,9 +227,9 @@ private boolean convertSatResult(Result result) throws InterruptedException, Sol @Override public List getUnsatCore() { - Preconditions.checkState(!closed); + checkState(!closed); checkGenerateUnsatCores(); - Preconditions.checkState(!changedSinceLastSatQuery); + checkState(!changedSinceLastSatQuery); List converted = new ArrayList<>(); for (Term aCore : solver.getUnsatCore()) { converted.add(creator.encapsulateBoolean(aCore)); @@ -243,6 +249,25 @@ public Optional> unsatCoreOverAssumptions( throw new UnsupportedOperationException(); } + @Override + public Proof getProof() throws SolverException, InterruptedException { + checkGenerateProofs(); + checkState(!closed); + checkState(isUnsat()); + + io.github.cvc5.Proof[] proofs = solver.getProof(); + if (proofs == null || proofs.length == 0) { + throw new IllegalStateException("No proof available"); + } + + // CVC5ProofProcessor pp = new CVC5ProofProcessor(creator); + try { + return generateProofImpl(proofs[0], creator); + } catch (CVC5ApiException e) { + throw new SolverException("There was a problem generating proof", e); + } + } + @Override public void close() { if (!closed) { diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java index 9a61f193fd..11ecd442f4 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java @@ -1411,12 +1411,12 @@ public void testProofMethods() throws CVC5ApiException { assertThat(proof.getRule()).isEqualTo(ProofRule.SCOPE); - // Test getChildren + // Test getArguments assertThat(proof.getChildren()).isNotNull(); assertThat(proof.getChildren()[0]).isNotNull(); - // The way the proof DAG is structured, the root has one child, which has also one child and + // The way this proof DAG is structured, the root has one child, which has also one child and // the child of the latter has more than one child. Proof[] childOfSecondProof = proof.getChildren()[0].getChildren(); diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java new file mode 100644 index 0000000000..5fd2f2e197 --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5Proof.java @@ -0,0 +1,109 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.solvers.cvc5; + +import io.github.cvc5.CVC5ApiException; +import io.github.cvc5.Term; +import java.util.ArrayDeque; +import java.util.Deque; +import java.util.HashMap; +import java.util.Map; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.proofs.Proof; +import org.sosy_lab.java_smt.api.proofs.ProofFrame; +import org.sosy_lab.java_smt.api.proofs.ProofRule; + +public class CVC5Proof extends org.sosy_lab.java_smt.basicimpl.AbstractProof { + + static CVC5Proof generateProofImpl(io.github.cvc5.Proof pProof, CVC5FormulaCreator formulaCreator) + throws CVC5ApiException { + + // boolean skippedScope = false; + + Deque stack = new ArrayDeque<>(); + + Map computed = new HashMap<>(); + + stack.push(new CVC5Frame(pProof)); + + while (!stack.isEmpty()) { + CVC5Frame frame = stack.peek(); + + if (!frame.isVisited()) { + + frame.setNumArgs(frame.getProof().getChildren().length); + frame.setAsVisited(true); + + for (int i = frame.getNumArgs() - 1; i >= 0; i--) { + io.github.cvc5.Proof child = frame.getProof().getChildren()[i]; + if (!computed.containsKey(child)) { + stack.push(new CVC5Frame(child)); + } + } + } else { + stack.pop(); + int numChildren = frame.getNumArgs(); + + // if (frame.getProof().getRule().getValue() == 1 && !skippedScope) { + // Skip processing the frame if its rule is "SCOPE" + // This rule seems to just help the processing by CVC5 + // pProof = changeRoot(frame.getProof()); + // skippedScope = true; + // continue; + // } + + CVC5ProofRule proofRule = + Enum.valueOf(CVC5ProofRule.class, frame.getProof().getRule().toString()); + // ProofRule.fromName( + // CVC5ProofRule.class, frame.getProof().getRule().toString().toLowerCase()); + + // Generate formula + Term term = frame.getProof().getResult(); + Formula pFormula = formulaCreator.encapsulate(formulaCreator.getFormulaType(term), term); + CVC5Proof pn = new CVC5Proof(proofRule, pFormula); + for (int i = 0; i < numChildren; i++) { + io.github.cvc5.Proof child = frame.getProof().getChildren()[i]; + + if (computed.containsKey(child)) { + pn.addChild(computed.get(child)); + } + } + computed.put(frame.getProof(), pn); + } + } + return computed.get(pProof); + } + + private static class CVC5Frame extends ProofFrame { + CVC5Frame(io.github.cvc5.Proof proof) { + super(proof); + } + } + + public CVC5Proof(ProofRule pProofRule, Formula formula) { + + super(pProofRule, formula); + } + + @Override + protected void addChild(Proof pProof) { + super.addChild(pProof); + } + + // private static Proof changeRoot(Proof root) { + // return root.getArguments()[0]; + // } + + @Override + public String proofAsString() { + return super.proofAsString(); + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofRule.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofRule.java new file mode 100644 index 0000000000..b73ded009d --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ProofRule.java @@ -0,0 +1,190 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.solvers.cvc5; + +import org.sosy_lab.java_smt.api.proofs.ProofRule; + +// TODO: Properly include the formulas for the proof rules. +enum CVC5ProofRule implements ProofRule { + ASSUME("assume", ""), + SCOPE("scope", ""), + SUBS("subs", ""), + MACRO_REWRITE("macro_rewrite", ""), + EVALUATE("evaluate", ""), + DISTINCT_VALUES("distinct_values", ""), + ACI_NORM("aci_norm", ""), + ABSORB("absorb", ""), + MACRO_SR_EQ_INTRO("macro_sr_eq_intro", ""), + MACRO_SR_PRED_INTRO("macro_sr_pred_intro", ""), + MACRO_SR_PRED_ELIM("macro_sr_pred_elim", ""), + MACRO_SR_PRED_TRANSFORM("macro_sr_pred_transform", ""), + ENCODE_EQ_INTRO("encode_eq_intro", ""), + DSL_REWRITE("dsl_rewrite", ""), + THEORY_REWRITE("theory_rewrite", ""), + ITE_EQ("ite_eq", ""), + TRUST("trust", ""), + TRUST_THEORY_REWRITE("trust_theory_rewrite", ""), + SAT_REFUTATION("sat_refutation", ""), + DRAT_REFUTATION("drat_refutation", ""), + SAT_EXTERNAL_PROVE("sat_external_prove", ""), + RESOLUTION("resolution", ""), + CHAIN_RESOLUTION("chain_resolution", ""), + FACTORING("factoring", ""), + REORDERING("reordering", ""), + MACRO_RESOLUTION("macro_resolution", ""), + MACRO_RESOLUTION_TRUST("macro_resolution_trust", ""), + SPLIT("split", ""), + EQ_RESOLVE("eq_resolve", ""), + MODUS_PONENS("modus_ponens", ""), + NOT_NOT_ELIM("not_not_elim", ""), + CONTRA("contra", ""), + AND_ELIM("and_elim", ""), + AND_INTRO("and_intro", ""), + NOT_OR_ELIM("not_or_elim", ""), + IMPLIES_ELIM("implies_elim", ""), + NOT_IMPLIES_ELIM1("not_implies_elim1", ""), + NOT_IMPLIES_ELIM2("not_implies_elim2", ""), + EQUIV_ELIM1("equiv_elim1", ""), + EQUIV_ELIM2("equiv_elim2", ""), + NOT_EQUIV_ELIM1("not_equiv_elim1", ""), + NOT_EQUIV_ELIM2("not_equiv_elim2", ""), + XOR_ELIM1("xor_elim1", ""), + XOR_ELIM2("xor_elim2", ""), + NOT_XOR_ELIM1("not_xor_elim1", ""), + NOT_XOR_ELIM2("not_xor_elim2", ""), + ITE_ELIM1("ite_elim1", ""), + ITE_ELIM2("ite_elim2", ""), + NOT_ITE_ELIM1("not_ite_elim1", ""), + NOT_ITE_ELIM2("not_ite_elim2", ""), + NOT_AND("not_and", ""), + CNF_AND_POS("cnf_and_pos", ""), + CNF_AND_NEG("cnf_and_neg", ""), + CNF_OR_POS("cnf_or_pos", ""), + CNF_OR_NEG("cnf_or_neg", ""), + CNF_IMPLIES_POS("cnf_implies_pos", ""), + CNF_IMPLIES_NEG1("cnf_implies_neg1", ""), + CNF_IMPLIES_NEG2("cnf_implies_neg2", ""), + CNF_EQUIV_POS1("cnf_equiv_pos1", ""), + CNF_EQUIV_POS2("cnf_equiv_pos2", ""), + CNF_EQUIV_NEG1("cnf_equiv_neg1", ""), + CNF_EQUIV_NEG2("cnf_equiv_neg2", ""), + CNF_XOR_POS1("cnf_xor_pos1", ""), + CNF_XOR_POS2("cnf_xor_pos2", ""), + CNF_XOR_NEG1("cnf_xor_neg1", ""), + CNF_XOR_NEG2("cnf_xor_neg2", ""), + CNF_ITE_POS1("cnf_ite_pos1", ""), + CNF_ITE_POS2("cnf_ite_pos2", ""), + CNF_ITE_POS3("cnf_ite_pos3", ""), + CNF_ITE_NEG1("cnf_ite_neg1", ""), + CNF_ITE_NEG2("cnf_ite_neg2", ""), + CNF_ITE_NEG3("cnf_ite_neg3", ""), + REFL("refl", ""), + SYMM("symm", ""), + TRANS("trans", ""), + CONG("cong", ""), + NARY_CONG("nary_cong", ""), + TRUE_INTRO("true_intro", ""), + TRUE_ELIM("true_elim", ""), + FALSE_INTRO("false_intro", ""), + FALSE_ELIM("false_elim", ""), + HO_APP_ENCODE("ho_app_encode", ""), + HO_CONG("ho_cong", ""), + ARRAYS_READ_OVER_WRITE("arrays_read_over_write", ""), + ARRAYS_READ_OVER_WRITE_CONTRA("arrays_read_over_write_contra", ""), + ARRAYS_READ_OVER_WRITE_1("arrays_read_over_write_1", ""), + ARRAYS_EXT("arrays_ext", ""), + MACRO_BV_BITBLAST("macro_bv_bitblast", ""), + BV_BITBLAST_STEP("bv_bitblast_step", ""), + BV_EAGER_ATOM("bv_eager_atom", ""), + BV_POLY_NORM("bv_poly_norm", ""), + BV_POLY_NORM_EQ("bv_poly_norm_eq", ""), + DT_SPLIT("dt_split", ""), + SKOLEM_INTRO("skolem_intro", ""), + SKOLEMIZE("skolemize", ""), + INSTANTIATE("instantiate", ""), + ALPHA_EQUIV("alpha_equiv", ""), + QUANT_VAR_REORDERING("quant_var_reordering", ""), + SETS_SINGLETON_INJ("sets_singleton_inj", ""), + SETS_EXT("sets_ext", ""), + SETS_FILTER_UP("sets_filter_up", ""), + SETS_FILTER_DOWN("sets_filter_down", ""), + CONCAT_EQ("concat_eq", ""), + CONCAT_UNIFY("concat_unify", ""), + CONCAT_SPLIT("concat_split", ""), + CONCAT_CSPLIT("concat_csplit", ""), + CONCAT_LPROP("concat_lprop", ""), + CONCAT_CPROP("concat_cprop", ""), + STRING_DECOMPOSE("string_decompose", ""), + STRING_LENGTH_POS("string_length_pos", ""), + STRING_LENGTH_NON_EMPTY("string_length_non_empty", ""), + STRING_REDUCTION("string_reduction", ""), + STRING_EAGER_REDUCTION("string_eager_reduction", ""), + RE_INTER("re_inter", ""), + RE_CONCAT("re_concat", ""), + RE_UNFOLD_POS("re_unfold_pos", ""), + RE_UNFOLD_NEG("re_unfold_neg", ""), + RE_UNFOLD_NEG_CONCAT_FIXED("re_unfold_neg_concat_fixed", ""), + STRING_CODE_INJ("string_code_inj", ""), + STRING_SEQ_UNIT_INJ("string_seq_unit_inj", ""), + STRING_EXT("string_ext", ""), + MACRO_STRING_INFERENCE("macro_string_inference", ""), + MACRO_ARITH_SCALE_SUM_UB("macro_arith_scale_sum_ub", ""), + ARITH_MULT_ABS_COMPARISON("arith_mult_abs_comparison", ""), + ARITH_SUM_UB("arith_sum_ub", ""), + INT_TIGHT_UB("int_tight_ub", ""), + INT_TIGHT_LB("int_tight_lb", ""), + ARITH_TRICHOTOMY("arith_trichotomy", ""), + ARITH_REDUCTION("arith_reduction", ""), + ARITH_POLY_NORM("arith_poly_norm", ""), + ARITH_POLY_NORM_REL("arith_poly_norm_rel", ""), + ARITH_MULT_SIGN("arith_mult_sign", ""), + ARITH_MULT_POS("arith_mult_pos", ""), + ARITH_MULT_NEG("arith_mult_neg", ""), + ARITH_MULT_TANGENT("arith_mult_tangent", ""), + ARITH_TRANS_PI("arith_trans_pi", ""), + ARITH_TRANS_EXP_NEG("arith_trans_exp_neg", ""), + ARITH_TRANS_EXP_POSITIVITY("arith_trans_exp_positivity", ""), + ARITH_TRANS_EXP_SUPER_LIN("arith_trans_exp_super_lin", ""), + ARITH_TRANS_EXP_ZERO("arith_trans_exp_zero", ""), + ARITH_TRANS_EXP_APPROX_ABOVE_NEG("arith_trans_exp_approx_above_neg", ""), + ARITH_TRANS_EXP_APPROX_ABOVE_POS("arith_trans_exp_approx_above_pos", ""), + ARITH_TRANS_EXP_APPROX_BELOW("arith_trans_exp_approx_below", ""), + ARITH_TRANS_SINE_BOUNDS("arith_trans_sine_bounds", ""), + ARITH_TRANS_SINE_SHIFT("arith_trans_sine_shift", ""), + ARITH_TRANS_SINE_SYMMETRY("arith_trans_sine_symmetry", ""), + ARITH_TRANS_SINE_TANGENT_ZERO("arith_trans_sine_tangent_zero", ""), + ARITH_TRANS_SINE_TANGENT_PI("arith_trans_sine_tangent_pi", ""), + ARITH_TRANS_SINE_APPROX_ABOVE_NEG("arith_trans_sine_approx_above_neg", ""), + ARITH_TRANS_SINE_APPROX_ABOVE_POS("arith_trans_sine_approx_above_pos", ""), + ARITH_TRANS_SINE_APPROX_BELOW_NEG("arith_trans_sine_approx_below_neg", ""), + ARITH_TRANS_SINE_APPROX_BELOW_POS("arith_trans_sine_approx_below_pos", ""), + LFSC_RULE("lfsc_rule", ""), + ALETHE_RULE("alethe_rule", ""), + UNKNOWN("unknown", ""); + + private final String name; + private final String formula; + + CVC5ProofRule(String pName, String pFormula) { + name = pName; + formula = pFormula; + } + + @Override + public String getName() { + return name; + } + + @Override + public String getFormula() { + return formula; + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java index 39ace99503..3fa39f08ca 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5AbstractProver.java @@ -78,9 +78,11 @@ private long buildConfig(Set opts) { Map config = new LinkedHashMap<>(); boolean generateUnsatCore = opts.contains(ProverOptions.GENERATE_UNSAT_CORE) - || opts.contains(ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS); + || opts.contains(ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS) + || opts.contains(ProverOptions.GENERATE_PROOFS); config.put("model_generation", opts.contains(ProverOptions.GENERATE_MODELS) ? "true" : "false"); config.put("unsat_core_generation", generateUnsatCore ? "1" : "0"); + config.put("proof_generation", opts.contains(ProverOptions.GENERATE_PROOFS) ? "true" : "false"); if (generateUnsatCore) { config.put("theory.bv.eager", "false"); } diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java index 261c2f305f..b6e0820301 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java @@ -9,13 +9,16 @@ package org.sosy_lab.java_smt.solvers.mathsat5; import static com.google.common.truth.Truth.assertThat; +import static org.junit.Assert.assertThrows; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_assert_formula; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_check_sat; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_create_config; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_create_env; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_create_shared_env; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_decl_get_arity; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_decl_get_name; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_destroy_config; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_destroy_env; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_destroy_model_iterator; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_destroy_proof_manager; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_from_smtlib2; @@ -33,6 +36,7 @@ import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_eq; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_equal; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_exp; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_false; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_log; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_not; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_number; @@ -107,20 +111,121 @@ public void proofTest() throws IllegalStateException, InterruptedException, Solv env = msat_create_env(cfg); msat_destroy_config(cfg); - const0 = msat_make_number(env, "0"); - const1 = msat_make_number(env, "1"); - long rationalType = msat_get_rational_type(env); - var = msat_make_variable(env, "rat", rationalType); + testProofManager(env); + } - msat_push_backtrack_point(env); + // Tests if it is possible to enable proof generation in a shared environment after it was not + // enabled in the original + @Test + public void proofSharedEnvironmentTest() + throws IllegalStateException, InterruptedException, SolverException { + long cfg = msat_create_config(); + env = msat_create_env(cfg); + msat_destroy_config(cfg); - msat_assert_formula(env, msat_make_equal(env, var, const0)); - msat_assert_formula(env, msat_make_equal(env, var, const1)); + cfg = msat_create_config(); + msat_set_option_checked(cfg, "proof_generation", "true"); + long sharedEnv = msat_create_shared_env(cfg, env); + msat_destroy_config(cfg); + + testProofManager(sharedEnv); + } + + // MathSAT5 can not produce a msat_manager because there is no proof in this case. See + // ProverEnvironmentTest class + @SuppressWarnings("CheckReturnValue") + @Test + public void testProofOfFalse() throws SolverException, InterruptedException { + assertThrows( + IllegalArgumentException.class, + () -> { + long cfg = msat_create_config(); + + msat_set_option_checked(cfg, "proof_generation", "true"); + + env = msat_create_env(cfg); + msat_destroy_config(cfg); + long bottom = msat_make_false(env); + + msat_assert_formula(env, bottom); + + boolean isSat = msat_check_sat(env); + + assertThat(isSat).isFalse(); + + long pm = msat_get_proof_manager(env); + + msat_get_proof(pm); + + msat_destroy_proof_manager(pm); + msat_destroy_env(env); + }); + } + + @SuppressWarnings("CheckReturnValue") + @Test + public void api_exampleProofTest() throws SolverException, InterruptedException { + + long cfg = msat_create_config(); + msat_set_option_checked(cfg, "proof_generation", "true"); + msat_set_option_checked(cfg, "preprocessor.toplevel_propagation", "false"); + msat_set_option_checked(cfg, "preprocessor.simplification", "0"); + msat_set_option_checked(cfg, "theory.bv.eager", "false"); // for BV, only the lazy solver is + + msat_set_option_checked(cfg, "theory.fp.mode", "2"); + + long env = msat_create_env(cfg); + msat_destroy_config(cfg); + + long f; + + String smtlib2 = + "(declare-fun x1 () Real)" + + "(declare-fun x2 () Real)" + + "(declare-fun x3 () Real)" + + "(declare-fun y1 () Real)" + + "(declare-fun y2 () Real)" + + "(declare-fun y3 () Real)" + + "(declare-fun b () Real)" + + "(declare-fun f (Real) Real)" + + "(declare-fun g (Real) Real)" + + "(declare-fun a () Bool)" + + "(declare-fun c () Bool)" + + "(assert (and a (= (+ (f y1) y2) y3) (<= y1 x1)))" + + "(assert (and (= x2 (g b)) (= y2 (g b)) (<= x1 y1) (< x3 y3)))" + + "(assert (= a (= (+ (f x1) x2) x3)))" + + "(assert (and (or a c) (not c)))"; + f = msat_from_smtlib2(env, smtlib2); + + msat_assert_formula(env, f); + + boolean isSat = msat_check_sat(env); + + assertThat(isSat).isFalse(); + + long pm = msat_get_proof_manager(env); + + msat_get_proof(pm); + + msat_destroy_proof_manager(pm); + msat_destroy_env(env); + } + + private void testProofManager(long testEnv) throws InterruptedException, SolverException { + const0 = msat_make_number(testEnv, "0"); + const1 = msat_make_number(testEnv, "1"); + long rationalType = msat_get_rational_type(testEnv); + var = msat_make_variable(testEnv, "rat", rationalType); + + msat_push_backtrack_point(testEnv); + + msat_assert_formula(testEnv, msat_make_equal(testEnv, var, const0)); + msat_assert_formula(testEnv, msat_make_equal(testEnv, var, const1)); // UNSAT - assertThat(msat_check_sat(env)).isFalse(); + assertThat(msat_check_sat(testEnv)).isFalse(); - long proofMgr = msat_get_proof_manager(env); + long proofMgr = msat_get_proof_manager(testEnv); long proof = msat_get_proof(proofMgr); assertThat(msat_proof_is_term(proof)).isFalse(); diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5Proof.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5Proof.java new file mode 100644 index 0000000000..6a005751b2 --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5Proof.java @@ -0,0 +1,191 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.solvers.mathsat5; + +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_and; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_or; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_proof_get_arity; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_proof_get_child; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_proof_get_name; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_proof_get_term; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_proof_is_term; + +import java.util.ArrayDeque; +import java.util.Deque; +import java.util.HashMap; +import java.util.Locale; +import java.util.Map; +import org.checkerframework.checker.nullness.qual.Nullable; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.ProverEnvironment; +import org.sosy_lab.java_smt.api.proofs.Proof; +import org.sosy_lab.java_smt.api.proofs.ProofFrame; +import org.sosy_lab.java_smt.api.proofs.ProofRule; +import org.sosy_lab.java_smt.basicimpl.AbstractProof; +import org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5ProofRule.Rule; + +class Mathsat5Proof extends AbstractProof { + + /** + * Creates a proof node from a MathSAT5 proof object. + * + *

Not all proof rules are known beforehand, so some are not in the enum. This means that + * (specifically) the sub-DAG of the theory-lemma rule may contain a sub-proof that does not have + * either a {@link ProofRule} or a {@link Formula} in a given node. + * + * @param pProver The prover environment. + * @param rootProof The root proof object. + * @return The proof node. + */ + protected static Mathsat5Proof fromMsatProof(ProverEnvironment pProver, long rootProof) { + + Deque stack = new ArrayDeque<>(); + Map computed = new HashMap<>(); + + stack.push(new MsatProofFrame(rootProof)); + + while (!stack.isEmpty()) { + MsatProofFrame frame = stack.peek(); + + if (!frame.isVisited()) { + frame.setAsVisited(true); + String rule = + msat_proof_get_name(frame.getProof()) == null + ? "null" + : msat_proof_get_name(frame.getProof()); + + // If rule is claus-hyp, all the children get added to the dag in generateFormula + if (!rule.equals("clause-hyp")) { + frame.setNumArgs(msat_proof_get_arity(frame.getProof())); + for (int i = frame.getNumArgs() - 1; i >= 0; i--) { + long child = msat_proof_get_child(frame.getProof(), i); + if (!computed.containsKey(child)) { + // If the rules is theory-lemma and the child is a term, it gets added to the dag + // in generateFormula otherwise we push it to the stack to be processed later. + switch (rule) { + case "theory-lemma": + if (msat_proof_is_term(child)) { + frame.setNumArgs(frame.getNumArgs() - 1); + } else { + stack.push(new MsatProofFrame(child)); + } + break; + default: + stack.push(new MsatProofFrame(child)); + break; + } + } + } + } + } else { + + stack.pop(); + + String rule = msat_proof_get_name(frame.getProof()); + ProofRule proofRule; + + // If the theory-lemma rule includes a last argument that is not a term, it means it has + // a proof attached to it. Not all rules are known beforehand so they are not in the enum. + try { + proofRule = + rule == null + ? Rule.EMPTY + : Rule.valueOf(rule.toUpperCase(Locale.ENGLISH).replace("-", "_")); + } catch (IllegalArgumentException e) { + proofRule = new Mathsat5ProofRule(rule); + } + + Mathsat5Proof node; + Mathsat5TheoremProver prover = (Mathsat5TheoremProver) pProver; + Formula formula = generateFormula(frame, prover, proofRule); + + node = new Mathsat5Proof(proofRule, formula); + + // Retrieve computed child nodes and attach them. In this case the subtraction is due to + // the processing of the theory-lemma rule. + + for (int i = (msat_proof_get_arity(frame.getProof()) - frame.getNumArgs()); + i < msat_proof_get_arity(frame.getProof()); + i++) { + + long child = msat_proof_get_child(frame.getProof(), i); + + Mathsat5Proof childNode = computed.get(child); + if (childNode != null) { + node.addChild(childNode); + } + } + computed.put(frame.getProof(), node); + } + } + return computed.get(rootProof); + } + + @Nullable + private static Formula generateFormula( + MsatProofFrame frame, Mathsat5TheoremProver prover, ProofRule rule) { + Mathsat5FormulaCreator formulaCreator = prover.creator; + Formula formula = null; + long proof = frame.getProof(); + int children = msat_proof_get_arity(proof); + // If rule is EMPTY the proof should be a term and we encapsulate directly + if (rule.equals(Rule.EMPTY)) { + formula = + formulaCreator.encapsulate( + formulaCreator.getFormulaType(msat_proof_get_term(proof)), + msat_proof_get_term(proof)); + // For clause-hype, we create the clause using the children + } else if (rule.equals(Rule.CLAUSE_HYP)) { + assert msat_proof_get_arity(proof) > 0; + long or = msat_proof_get_term(msat_proof_get_child(proof, 0)); + for (int i = 1; i < children; i++) { + long child = msat_proof_get_term(msat_proof_get_child(proof, i)); + or = msat_make_or(prover.curEnv, or, child); + } + formula = formulaCreator.encapsulate(formulaCreator.getFormulaType(or), or); + } else if (rule.equals(Rule.RES_CHAIN)) { + // Generating the formula for the resolution chain should be easier after the whole DAG is + // built + } else if (rule.equals(Rule.THEORY_LEMMA)) { + if (msat_proof_is_term(msat_proof_get_child(proof, 0))) { + long and = msat_proof_get_term(msat_proof_get_child(proof, 0)); + for (int i = 1; i < children; i++) { + if (msat_proof_is_term(msat_proof_get_child(proof, i))) { + long child = msat_proof_get_term(msat_proof_get_child(proof, i)); + and = msat_make_and(prover.curEnv, and, child); + } + } + formula = formulaCreator.encapsulate(formulaCreator.getFormulaType(and), and); + } + } + return formula; + } + + protected static class MsatProofFrame extends ProofFrame { + MsatProofFrame(Long proof) { + super(proof); + } + } + + protected Mathsat5Proof(@Nullable ProofRule rule, Formula formula) { + super(rule, formula); + } + + @Override + protected void addChild(Proof pProof) { + super.addChild(pProof); + } + + @Override + public String proofAsString() { + return super.proofAsString(); + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5ProofRule.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5ProofRule.java new file mode 100644 index 0000000000..6eb1cc1129 --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5ProofRule.java @@ -0,0 +1,55 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.solvers.mathsat5; + +import org.sosy_lab.java_smt.api.proofs.ProofRule; + +class Mathsat5ProofRule implements ProofRule { + // Most comments are taken from the API Reference: https://mathsat.fbk.eu/apireference.html + // + enum Rule implements ProofRule { + THEORY_LEMMA(), // " representing theory lemmas. They have as children a list of terms that + // consititute the lemma, plus an optional last element which is a more detailed + // proof produced by a theory solver." + RES_CHAIN(), // "representing Boolean resolution chains. The children are an interleaving of + // proofs and terms, where terms are the pivots for the resolution. For example: + // "res-chain p1 v p2" represents a resolution step between p1 and p2 on the pivot + // v" + CLAUSE_HYP(), // " which are the clauses of the (CNF conversion of the) input problem. They have + // a list of terms as children" + + EMPTY(); // We introduce this rule for term nodes that do not have a proof rule attached, even + + // if they are pivots. In the future it might be good to a PIVOT rule so that those can have + // that instead. + + @Override + public String getName() { + return name(); + } + } + + private String name; + + Mathsat5ProofRule(String pName) { + name = pName; + } + + @Override + public String getName() { + return name; + } + + @Override + public String toString() { + return getName(); + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5TheoremProver.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5TheoremProver.java index 4801c5904f..51c55aa907 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5TheoremProver.java @@ -10,15 +10,33 @@ import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5FormulaManager.getMsatTerm; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_assert_formula; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_destroy_proof_manager; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_get_proof; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_get_proof_manager; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5Proof.fromMsatProof; import com.google.common.base.Preconditions; +import java.util.ArrayDeque; +import java.util.ArrayList; +import java.util.Deque; +import java.util.HashMap; +import java.util.List; import java.util.Map; import java.util.Set; import org.checkerframework.checker.nullness.qual.Nullable; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.BooleanFormulaManager; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.FunctionDeclaration; import org.sosy_lab.java_smt.api.ProverEnvironment; +import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; +import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.proofs.Proof; +import org.sosy_lab.java_smt.api.visitors.BooleanFormulaVisitor; +import org.sosy_lab.java_smt.api.visitors.TraversalProcess; +import org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5ProofRule.Rule; class Mathsat5TheoremProver extends Mathsat5AbstractProver implements ProverEnvironment { @@ -43,4 +61,286 @@ protected Void addConstraintImpl(BooleanFormula constraint) throws InterruptedEx msat_assert_formula(curEnv, getMsatTerm(constraint)); return null; } + + @Override + public Proof getProof() throws SolverException, InterruptedException { + Preconditions.checkState(!closed); + Preconditions.checkState(this.isUnsat()); + checkGenerateProofs(); + + Mathsat5Proof root; + long pm; + try { + pm = msat_get_proof_manager(curEnv); + } catch (IllegalArgumentException e) { + throw new UnsupportedOperationException("No proof available.", e); + } + long msatProof = msat_get_proof(pm); + root = fromMsatProof(this, msatProof); + clausifyResChain(root, context.getFormulaManager().getBooleanFormulaManager()); + msat_destroy_proof_manager(pm); + + return root; + + // return getProof0(); + } + + // update all RES_CHAIN nodes in the proof DAG by computing resolution + // formulas and return the updated root node with formulas attached. + private void clausifyResChain(Proof root, BooleanFormulaManager bfmgr) { + Map visited = new HashMap<>(); // Track visited nodes + Deque stack = new ArrayDeque<>(); + + stack.push(root); // Start with the root node + visited.put(root, Boolean.FALSE); // Mark root as unvisited + + while (!stack.isEmpty()) { + Proof node = stack.peek(); // Look at the top node, but don't pop yet + + if (visited.get(node).equals(Boolean.FALSE)) { + // First time visiting this node + visited.put(node, Boolean.TRUE); // Mark node as visited + + // Push all children onto stack + if (!node.isLeaf()) { + Set childrenSet = node.getChildren(); + List children = new ArrayList<>(childrenSet); + for (int i = children.size() - 1; i >= 0; i--) { + Proof child = children.get(i); + if (!visited.containsKey(child)) { + stack.push(child); // Only push unvisited children + visited.put(child, Boolean.FALSE); // Mark child as unvisited + } + } + } + } else { + // All children have been visited, now process the node + stack.pop(); // Pop the current node as we are done processing its children + + // Check if this node is a RES_CHAIN, process if true + if (node.getRule().equals(Rule.RES_CHAIN)) { + processResChain(node, bfmgr); // Process RES_CHAIN node + } + } + } + } + + // process proof nodes and compute formulas for res-chain nodes + private void processResChain(Proof node, BooleanFormulaManager bfmgr) { + Set childrenSet = node.getChildren(); + List children = new ArrayList<>(childrenSet); + + // If the current node is a RES_CHAIN, compute the resolved formula + if (node.getRule().equals(Rule.RES_CHAIN)) { + // Sanity check: res-chain nodes must have an odd number of children (clause, pivot, clause, + // ..., clause) + if (children.size() < 3 || children.size() % 2 == 0) { + throw new IllegalArgumentException("Invalid res-chain structure: must be odd and >= 3"); + } + + // Begin resolution chain: start with the first clause + BooleanFormula current = (BooleanFormula) children.get(0).getFormula(); + + // Apply resolution iteratively using pivot, clause pairs + for (int i = 1; i < children.size() - 1; i += 2) { + BooleanFormula pivot = (BooleanFormula) children.get(i).getFormula(); + BooleanFormula nextClause = (BooleanFormula) children.get(i + 1).getFormula(); + current = resolve(current, nextClause, pivot, bfmgr); // Perform resolution step + } + + // Store the resolved formula in the current node + ((Mathsat5Proof) node).setFormula(current); + } + } + + // Perform resolution between two clauses using a given pivot + private BooleanFormula resolve( + BooleanFormula clause1, + BooleanFormula clause2, + BooleanFormula pivot, + BooleanFormulaManager bfmgr) { + List literals1 = flattenLiterals(clause1, bfmgr); + List literals2 = flattenLiterals(clause2, bfmgr); + List combined = new ArrayList<>(); + + for (BooleanFormula lit : literals1) { + if (!isComplement(lit, pivot, bfmgr)) { + combined.add(lit); + } + } + + List temp = new ArrayList<>(); + for (BooleanFormula lit : literals2) { + if (!isComplement(lit, pivot, bfmgr)) { + temp.add(lit); + } + } + + combined.addAll(temp); + + if (combined.isEmpty()) { + return bfmgr.makeFalse(); + } else if (combined.size() == 1) { + return combined.get(0); + } else { + return bfmgr.or(combined); + } + } + + // Helper method to flatten an OR/AND-formula into a list of disjunctive literals + private List flattenLiterals( + BooleanFormula formula, BooleanFormulaManager bfmgr) { + List result = new ArrayList<>(); + + bfmgr.visit( + formula, + new BooleanFormulaVisitor<>() { + @Override + public TraversalProcess visitOr(List operands) { + for (BooleanFormula op : operands) { + result.addAll(flattenLiterals(op, bfmgr)); + } + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitAnd(List operands) { + for (BooleanFormula op : operands) { + result.addAll(flattenLiterals(op, bfmgr)); + } + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitNot(BooleanFormula operand) { + result.add(formula); // add original NOT node + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitAtom( + BooleanFormula atom, FunctionDeclaration decl) { + result.add(formula); // add original atom + return TraversalProcess.SKIP; + } + + // others unchanged... + @Override + public TraversalProcess visitXor(BooleanFormula first, BooleanFormula second) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitEquivalence(BooleanFormula first, BooleanFormula second) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitImplication(BooleanFormula first, BooleanFormula second) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitIfThenElse( + BooleanFormula c, BooleanFormula t, BooleanFormula e) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitQuantifier( + Quantifier q, BooleanFormula qBody, List vars, BooleanFormula body) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitConstant(boolean value) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitBoundVar(BooleanFormula var, int index) { + return TraversalProcess.SKIP; + } + }); + + return result; + } + + // Check whether two formulas are logical complements + private boolean isComplement(BooleanFormula a, BooleanFormula b, BooleanFormulaManager bfmgr) { + // Define the visitor to check for complement relation + final boolean[] isComplement = {false}; + + bfmgr.visitRecursively( + a, + new BooleanFormulaVisitor<>() { + @Override + public TraversalProcess visitNot(BooleanFormula operand) { + // Check if the negation of 'operand' equals 'b' + if (operand.equals(b)) { + isComplement[0] = true; + } + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitAtom( + BooleanFormula atom, FunctionDeclaration decl) { + if (atom.equals(b)) { + isComplement[0] = true; + } + return TraversalProcess.SKIP; + } + + // Default implementation for other nodes, such as OR, AND, etc. + @Override + public TraversalProcess visitOr(List operands) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitAnd(List operands) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitXor(BooleanFormula first, BooleanFormula second) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitEquivalence(BooleanFormula first, BooleanFormula second) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitImplication(BooleanFormula first, BooleanFormula second) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitIfThenElse( + BooleanFormula c, BooleanFormula t, BooleanFormula e) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitQuantifier( + Quantifier q, BooleanFormula qBody, List vars, BooleanFormula body) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitConstant(boolean value) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitBoundVar(BooleanFormula var, int index) { + return TraversalProcess.SKIP; + } + }); + + return isComplement[0]; + } } diff --git a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSMTProof.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSMTProof.java new file mode 100644 index 0000000000..284c585742 --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSMTProof.java @@ -0,0 +1,292 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.solvers.opensmt; + +import java.util.ArrayDeque; +import java.util.ArrayList; +import java.util.Deque; +import java.util.HashMap; +import java.util.Iterator; +import java.util.List; +import java.util.Map; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.proofs.ProofRule; +import org.sosy_lab.java_smt.basicimpl.AbstractProof; + +@SuppressWarnings("unchecked") +class OpenSMTProof extends AbstractProof { + static class OpenSMTProofRule implements ProofRule { + private final String name; + + OpenSMTProofRule(String pName) { + name = pName; + } + + @Override + public String getName() { + return name; + } + } + + String sFormula; + + protected OpenSMTProof(ProofRule rule, Formula formula) { + super(rule, formula); + } + + protected OpenSMTProof(ProofRule rule, String sFormula) { + super(rule, null); + this.sFormula = sFormula; + } + + static OpenSMTProof generateProof(String proof, OpenSmtFormulaCreator creator) { + Deque resNodes = new ArrayDeque<>(); + Map nodes = new HashMap<>(); + Deque rootStack = ProofParser.parse(ProofParser.tokenize(proof)); + + Deque> iterStack = new ArrayDeque<>(); + iterStack.push(rootStack.iterator()); + + OpenSMTProof result = null; + String formulaStr = ""; + + while (!iterStack.isEmpty()) { + Iterator currentIter = iterStack.peek(); + + if (!currentIter.hasNext()) { + iterStack.pop(); + continue; + } + + Object exp = currentIter.next(); + + if (exp instanceof String) { + String token = (String) exp; + switch (token) { + case "let": + // next element is a Deque with clause name and formula + if (!currentIter.hasNext()) { + throw new IllegalStateException("Expected argument after 'let'"); + } + Object letArg = currentIter.next(); + handleLet(letArg, nodes, resNodes, creator, formulaStr); + break; + + case ";": + if (!currentIter.hasNext()) { + throw new IllegalStateException("Expected formula string after ';'"); + } + formulaStr = (String) currentIter.next(); + // formula = creator.encapsulate(creator.getEnv().parseFormula(formulaStr)); + break; + + default: + break; + } + } else if (exp instanceof Deque) { + iterStack.push(((Deque) exp).iterator()); + } + } + result = resNodes.pop(); + assert result != null; + return result; + } + + static void handleLet( + Object stack, + Map nodes, + Deque resNodes, + OpenSmtFormulaCreator creator, + String lastSeenFormula) { + assert stack instanceof Deque; // no unchecked cast + Object expression = ((Deque) stack).pop(); + if (expression instanceof String) { // first element should be the assigned name + Object v1 = ((Deque) stack).peek(); + if (v1 instanceof Deque) { // then a stack with the formula + Object v2 = ((Deque) v1).peek(); + if (v2 instanceof String) { + if (v2.equals("res")) { + OpenSMTProof res = processRes(v1, nodes, resNodes, creator, lastSeenFormula); + nodes.putIfAbsent((String) expression, res); + resNodes.push(res); + } else { + String s = serializeDeque((Deque) v1); + nodes.putIfAbsent( + (String) expression, new OpenSMTProof(new OpenSMTProofRule("leaf"), s)); + } + } else { + String s = serializeDeque((Deque) v1); + nodes.putIfAbsent((String) expression, new OpenSMTProof(new OpenSMTProofRule("leaf"), s)); + } + } else if (v1 instanceof String) { // or a formula + String f = (String) v1; + nodes.putIfAbsent((String) expression, new OpenSMTProof(new OpenSMTProofRule("leaf"), f)); + } else { // this should handle when no term was assigned to the clause, meaning an empty + // clause was declared + nodes.putIfAbsent((String) expression, new OpenSMTProof(new OpenSMTProofRule("leaf"), "-")); + } + } + } + + static OpenSMTProof processRes( + Object expr, + Map nodes, + Deque resNodes, + OpenSmtFormulaCreator creator, + String formulaStr) { + + Deque> stack = new ArrayDeque<>(); + Object current = expr; + OpenSMTProof result = null; + + while (true) { + if (!(current instanceof Deque)) { + throw new IllegalArgumentException("Expected Deque in res expression but got: " + current); + } + Deque deque = new ArrayDeque<>((Deque) current); + Object op = deque.pollFirst(); + if (!"res".equals(op)) { + throw new IllegalStateException("Expected 'res' at head, got: " + op); + } + + Object first = deque.pollFirst(); + if (first instanceof String) { + String cls1 = (String) first; + String cls2 = (String) deque.pollFirst(); + Object rawPivot = deque.pollFirst(); + String pivotStr = + rawPivot instanceof String ? (String) rawPivot : serializeDeque((Deque) rawPivot); + + OpenSMTProof left = nodes.get(cls1); + OpenSMTProof right = nodes.get(cls2); + OpenSMTProof pivotNode = new OpenSMTProof(new OpenSMTProofRule("pivot"), pivotStr); + + OpenSMTProof res = + new OpenSMTProof(new OpenSMTProofRule("res"), stack.isEmpty() ? formulaStr : null); + res.addChild(left); + res.addChild(right); + res.addChild(pivotNode); + result = res; + break; + + } else if (first instanceof Deque) { + stack.push(deque); + current = first; + } else { + throw new IllegalStateException("Unexpected operand type in res: " + first); + } + } + + while (!stack.isEmpty()) { + Deque tokens = stack.pop(); + String cls2 = (String) tokens.pollFirst(); + Object rawPivot = tokens.pollFirst(); + String pivotStr = + rawPivot instanceof String ? (String) rawPivot : serializeDeque((Deque) rawPivot); + + OpenSMTProof right = nodes.get(cls2); + OpenSMTProof pivotNode = new OpenSMTProof(new OpenSMTProofRule("pivot"), pivotStr); + + boolean isOuter = stack.isEmpty(); + OpenSMTProof parent = + new OpenSMTProof(new OpenSMTProofRule("res"), isOuter ? formulaStr : null); + + parent.addChild(result); + parent.addChild(right); + parent.addChild(pivotNode); + result = parent; + } + + return result; + } + + private static String serializeDeque(Deque deque) { + StringBuilder sb = new StringBuilder(); + serializeHelper(deque, sb); + return sb.toString(); + } + + private static void serializeHelper(Object obj, StringBuilder sb) { + if (obj instanceof Deque) { + sb.append("("); + Deque inner = (Deque) obj; + boolean first = true; + for (Object o : inner) { + if (!first) sb.append(" "); + serializeHelper(o, sb); + first = false; + } + sb.append(")"); + } else if (obj instanceof String) { + sb.append((String) obj); + } + } + + static class ProofParser { + static List tokenize(String input) { + List tokens = new ArrayList<>(); + StringBuilder sb = new StringBuilder(); + + for (int i = 0; i < input.length(); i++) { + char c = input.charAt(i); + + if (Character.isWhitespace(c)) { + if (sb.length() > 0) { + String token = sb.toString(); + if (":core".equals(token)) { + tokens.add(")"); + break; + } + tokens.add(token); + sb.setLength(0); + } + } else if (c == '(' || c == ')') { + if (sb.length() > 0) { + String token = sb.toString(); + if (":core".equals(token)) { + tokens.add(")"); + break; + } + tokens.add(token); + sb.setLength(0); + } + tokens.add(Character.toString(c)); + } else { + sb.append(c); + } + } + + return tokens; + } + + static Deque parse(List tokens) { + Deque> stack = new ArrayDeque<>(); + Deque current = new ArrayDeque<>(); + + for (int i = 0; i < tokens.size(); i++) { + String token = tokens.get(i); + + if ("(".equals(token)) { + stack.push(current); + current = new ArrayDeque<>(); + } else if (")".equals(token)) { + Deque completed = current; + current = stack.pop(); + current.addLast(completed); + } else { + current.addLast(token); + } + } + + return current; + } + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java index 6678fb9b1c..b5efc03ca8 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtAbstractProver.java @@ -8,12 +8,16 @@ package org.sosy_lab.java_smt.solvers.opensmt; +import static org.sosy_lab.java_smt.solvers.opensmt.OpenSMTProof.generateProof; + import com.google.common.base.Preconditions; import com.google.common.collect.Collections2; import com.google.common.collect.ImmutableList; import com.google.common.collect.Lists; +import java.util.ArrayDeque; import java.util.ArrayList; import java.util.Collection; +import java.util.Deque; import java.util.HashMap; import java.util.List; import java.util.Map; @@ -23,11 +27,13 @@ import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.Evaluator; +import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaManager; import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.Model.ValueAssignment; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.proofs.Proof; import org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat; import org.sosy_lab.java_smt.basicimpl.ShutdownHook; import org.sosy_lab.java_smt.solvers.opensmt.OpenSmtSolverContext.OpenSMTOptions; @@ -46,6 +52,7 @@ public abstract class OpenSmtAbstractProver extends AbstractProverWithAllSat< protected final OpenSmtFormulaCreator creator; protected final MainSolver osmtSolver; protected final SMTConfig osmtConfig; + private final FormulaManager formulaManager; private boolean changedSinceLastSatQuery = false; @@ -63,6 +70,7 @@ protected OpenSmtAbstractProver( // not get garbage collected osmtConfig = pConfig; osmtSolver = new MainSolver(creator.getEnv(), pConfig, "JavaSmt"); + formulaManager = pMgr; // needed for parsing formulas in proofs } protected static SMTConfig getConfigInstance( @@ -78,6 +86,8 @@ protected static SMTConfig getConfigInstance( config.setOption(":produce-unsat-cores", optUnsatCore); config.setOption(":print-cores-full", optUnsatCore); config.setOption(":produce-interpolants", new SMTOption(interpolation)); + config.setOption( + ":produce-proofs", new SMTOption(pOptions.contains(ProverOptions.GENERATE_PROOFS))); if (interpolation) { config.setOption(":interpolation-bool-algorithm", new SMTOption(pSolverOptions.algBool)); config.setOption(":interpolation-euf-algorithm", new SMTOption(pSolverOptions.algUf)); @@ -282,6 +292,58 @@ public Optional> unsatCoreOverAssumptions( throw new UnsupportedOperationException("OpenSMT does not support solving with assumptions."); } + // TODO perform resolution throughout the DAG to calculate formulas that might not be present. + @Override + public Proof getProof() { + // throw new UnsupportedOperationException( + // "Proof generation is not available for the current solver."); + + // System.out.println(osmtSolver.printResolutionProofSMT2()); + OpenSMTProof root = generateProof(osmtSolver.printResolutionProofSMT2(), creator); + parseFormulas(root); + return root; + } + + // TODO: the parse method is asigning true as the formula always. This should not be. + private void parseFormulas(Proof root) { + Deque stack = new ArrayDeque<>(); + stack.push(root); + + while (!stack.isEmpty()) { + Proof proof = stack.pop(); + Formula formula; + String formulaString = ((OpenSMTProof) proof).sFormula; + // System.out.println(formulaString); + + if (formulaString.startsWith("(")) { + formula = formulaManager.parse(formulaString); + // System.out.println(formula); + ((OpenSMTProof) proof).setFormula(formula); + } else if (formulaString.equals("-")) { + formula = formulaManager.getBooleanFormulaManager().makeFalse(); + ((OpenSMTProof) proof).setFormula(formula); + } else { + if (formulaManager.isValidName(formulaString)) { + formula = formulaManager.getBooleanFormulaManager().makeVariable(formulaString); + ((OpenSMTProof) proof).setFormula(formula); + } else { + formula = formulaManager.parse("(" + formulaString + ")"); + ((OpenSMTProof) proof).setFormula(formula); + } + } + + // ((OpenSMTSubproof) subproof).setFormula(formula); + // System.out.println("."); + // System.out.println(subproof.getFormula()); + if (!proof.isLeaf()) { + Proof[] children = proof.getChildren().toArray(new Proof[0]); + for (int i = children.length - 1; i >= 0; i--) { + stack.push(children[i]); + } + } + } + } + @Override public void close() { if (!closed) { diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java index a816ed5c7e..ab6feadd21 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java @@ -278,4 +278,14 @@ public String toString() { return String.format("{%s, %s, %s}", booleanSymbols, theorySymbols, functionSymbols); } } + + // @Override + // public ProofNode getProof() { + // api.getCertificate(); + // return null; + // } + + // protected Certificate getCertificate() { + // return api.getCertificate(); + // } } diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java index 97c185ba00..1a02b53e22 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java @@ -25,8 +25,10 @@ import de.uni_freiburg.informatik.ultimate.logic.Sort; import de.uni_freiburg.informatik.ultimate.logic.Term; import java.util.ArrayDeque; +import java.util.ArrayList; import java.util.Collection; import java.util.Deque; +import java.util.HashMap; import java.util.LinkedHashMap; import java.util.List; import java.util.Map; @@ -37,13 +39,22 @@ import org.sosy_lab.common.collect.Collections3; import org.sosy_lab.common.collect.PathCopyingPersistentTreeMap; import org.sosy_lab.common.collect.PersistentMap; +import org.sosy_lab.java_smt.ResProofRule.ResAxiom; import org.sosy_lab.java_smt.api.BasicProverEnvironment; import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.BooleanFormulaManager; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.FunctionDeclaration; +import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.proofs.Proof; +import org.sosy_lab.java_smt.api.visitors.BooleanFormulaVisitor; +import org.sosy_lab.java_smt.api.visitors.TraversalProcess; import org.sosy_lab.java_smt.basicimpl.AbstractProver; import org.sosy_lab.java_smt.basicimpl.CachingModel; import org.sosy_lab.java_smt.basicimpl.FormulaCreator; +import org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolProofNodeCreator.ProvitionalProofNode; @SuppressWarnings("ClassTypeParameterName") abstract class SmtInterpolAbstractProver extends AbstractProver { @@ -213,6 +224,48 @@ public ImmutableMap getStatistics() { return builder.buildOrThrow(); } + @Override + public Proof getProof() throws InterruptedException { + checkState(!closed); + checkGenerateProofs(); + checkState(isUnsat()); + + final Term tProof; + try { + tProof = env.getProof(); + } catch (SMTLIBException e) { + if (e.getMessage().contains("Context is inconsistent")) { + throw new IllegalStateException("Cannot get proof from satisfiable environment", e); + } else { + throw e; + } + } + + SmtInterpolProofNodeCreator pc = + new SmtInterpolProofNodeCreator((SmtInterpolFormulaCreator) this.creator); + ProvitionalProofNode ppn = pc.createPPNDag(tProof); + Proof proof = pc.createProof(ppn); + // Before being able to perfom resolution, we need to calculate the formulas resulting from + // applying the axioms, as it stands, just the input for the axiom is stored. + // clausifyResChain(proof, mgr.getBooleanFormulaManager()); + + return proof; + } + + public Term smtInterpolGetProof() { + Term tProof; + try { + tProof = env.getProof(); + } catch (SMTLIBException e) { + if (e.getMessage().contains("Context is inconsistent")) { + throw new IllegalStateException("Cannot get proof from satisfiable environment", e); + } else { + throw e; + } + } + return tProof; + } + @Override public void close() { if (!closed) { @@ -250,4 +303,263 @@ public R allSat(AllSatCallback callback, List important) } return callback.getResult(); } + + // update all RES_CHAIN nodes in the proof DAG by computing resolution + // formulas and return the updated root node with formulas attached. + @SuppressWarnings("unused") + private void clausifyResChain(Proof root, BooleanFormulaManager bfmgr) { + Map visited = new HashMap<>(); // Track visited nodes + ArrayDeque stack = new ArrayDeque<>(); + + stack.push(root); // Start with the root node + visited.put(root, Boolean.FALSE); // Mark root as unvisited + + while (!stack.isEmpty()) { + Proof node = stack.peek(); // Look at the top node, but don't pop yet + + if (visited.get(node).equals(Boolean.FALSE)) { + // First time visiting this node + visited.put(node, Boolean.TRUE); // Mark node as visited + + // Push all children onto stack + Set children = node.getChildren(); + List childrenList = new ArrayList<>(children); + for (int i = childrenList.size() - 1; i >= 0; i--) { + Proof child = childrenList.get(i); + if (!visited.containsKey(child)) { + stack.push(child); // Only push unvisited children + visited.put(child, Boolean.FALSE); // Mark child as unvisited + } + } + } else { + // All children have been visited, now process the node + stack.pop(); // Pop the current node as we are done processing its children + + // Check if this node is a RES_CHAIN, process if true + if (node.getRule().equals(ResAxiom.RESOLUTION)) { + processResChain(node, bfmgr); // Process RES_CHAIN node + } + } + } + } + + // process proof nodes and compute formulas for res-chain nodes + private void processResChain(Proof node, BooleanFormulaManager bfmgr) { + Set childrenSet = node.getChildren(); + List children = new ArrayList<>(childrenSet); + + // If the current node is a RES_CHAIN, compute the resolved formula + if (node.getRule().equals(ResAxiom.RESOLUTION)) { + // Sanity check: res-chain nodes must have an odd number of children (clause, pivot, clause, + // ..., clause) + if (children.size() < 3 || children.size() % 2 == 0) { + throw new IllegalArgumentException("Invalid res-chain structure: must be odd and >= 3"); + } + + // Begin resolution chain: start with the first clause + BooleanFormula current = (BooleanFormula) children.get(0).getFormula(); + + // Apply resolution iteratively using pivot, clause pairs + for (int i = 1; i < children.size() - 1; i += 2) { + BooleanFormula pivot = (BooleanFormula) children.get(i).getFormula(); + BooleanFormula nextClause = (BooleanFormula) children.get(i + 1).getFormula(); + current = resolve(current, nextClause, pivot, bfmgr); // Perform resolution step + } + + // Store the resolved formula in the current node + ((SmtInterpolProof) node).setFormula(current); + } + } + + // Perform resolution between two clauses using a given pivot + private BooleanFormula resolve( + BooleanFormula clause1, + BooleanFormula clause2, + BooleanFormula pivot, + BooleanFormulaManager bfmgr) { + List literals1 = flattenLiterals(clause1, bfmgr); + List literals2 = flattenLiterals(clause2, bfmgr); + List combined = new ArrayList<>(); + + for (BooleanFormula lit : literals1) { + if (!isComplement(lit, pivot, bfmgr)) { + combined.add(lit); + } + } + + List temp = new ArrayList<>(); + + for (BooleanFormula lit : literals2) { + if (!isComplement(lit, pivot, bfmgr)) { + temp.add(lit); + } + } + + combined.addAll(temp); + + if (combined.isEmpty()) { + return bfmgr.makeFalse(); + } else if (combined.size() == 1) { + return combined.get(0); + } else { + return bfmgr.or(combined); + } + } + + // Helper method to flatten an OR/AND-formula into a list of disjunctive literals + private List flattenLiterals( + BooleanFormula formula, BooleanFormulaManager bfmgr) { + List result = new ArrayList<>(); + + bfmgr.visit( + formula, + new BooleanFormulaVisitor<>() { + @Override + public TraversalProcess visitOr(List operands) { + for (BooleanFormula op : operands) { + result.addAll(flattenLiterals(op, bfmgr)); + } + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitAnd(List operands) { + for (BooleanFormula op : operands) { + result.addAll(flattenLiterals(op, bfmgr)); + } + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitNot(BooleanFormula operand) { + result.add(formula); // add original NOT node + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitAtom( + BooleanFormula atom, FunctionDeclaration decl) { + result.add(formula); // add original atom + return TraversalProcess.SKIP; + } + + // others unchanged... + @Override + public TraversalProcess visitXor(BooleanFormula one, BooleanFormula two) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitEquivalence(BooleanFormula one, BooleanFormula two) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitImplication(BooleanFormula one, BooleanFormula two) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitIfThenElse( + BooleanFormula c, BooleanFormula t, BooleanFormula e) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitQuantifier( + Quantifier q, BooleanFormula qBody, List vars, BooleanFormula body) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitConstant(boolean value) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitBoundVar(BooleanFormula var, int index) { + return TraversalProcess.SKIP; + } + }); + + return result; + } + + // Check whether two formulas are logical complements + private boolean isComplement(BooleanFormula a, BooleanFormula b, BooleanFormulaManager bfmgr) { + // Define the visitor to check for complement relation + final boolean[] isComplement = {false}; + + bfmgr.visitRecursively( + a, + new BooleanFormulaVisitor<>() { + @Override + public TraversalProcess visitNot(BooleanFormula operand) { + // Check if the negation of 'operand' equals 'b' + if (operand.equals(b)) { + isComplement[0] = true; + } + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitAtom( + BooleanFormula atom, FunctionDeclaration decl) { + if (atom.equals(b)) { + isComplement[0] = true; + } + return TraversalProcess.SKIP; + } + + // Default implementation for other nodes, such as OR, AND, etc. + @Override + public TraversalProcess visitOr(List operands) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitAnd(List operands) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitXor(BooleanFormula var1, BooleanFormula var2) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitEquivalence(BooleanFormula var1, BooleanFormula var2) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitImplication(BooleanFormula var1, BooleanFormula var2) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitIfThenElse( + BooleanFormula c, BooleanFormula t, BooleanFormula e) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitQuantifier( + Quantifier q, BooleanFormula qBody, List vars, BooleanFormula body) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitConstant(boolean value) { + return TraversalProcess.SKIP; + } + + @Override + public TraversalProcess visitBoundVar(BooleanFormula var, int index) { + return TraversalProcess.SKIP; + } + }); + + return isComplement[0]; + } } diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolProof.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolProof.java new file mode 100644 index 0000000000..3159d6a2a2 --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolProof.java @@ -0,0 +1,352 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.solvers.smtinterpol; + +import com.google.common.base.Preconditions; +import de.uni_freiburg.informatik.ultimate.logic.AnnotatedTerm; +import de.uni_freiburg.informatik.ultimate.logic.Annotation; +import de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm; +import de.uni_freiburg.informatik.ultimate.logic.Sort; +import de.uni_freiburg.informatik.ultimate.logic.Term; +import de.uni_freiburg.informatik.ultimate.logic.Util; +import java.util.ArrayDeque; +import java.util.ArrayList; +import java.util.Deque; +import java.util.HashMap; +import java.util.List; +import java.util.Locale; +import java.util.Map; +import org.sosy_lab.java_smt.ResProofRule; +import org.sosy_lab.java_smt.ResProofRule.ResAxiom; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.proofs.Proof; +import org.sosy_lab.java_smt.api.proofs.ProofRule; +import org.sosy_lab.java_smt.basicimpl.AbstractProof; +import org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolProof.Rules; + +/** + * This class represents a SMTInterpol proof DAG in the JavaSMT proof interface. Many formulas that + * are not in the leafs or are pivots for resolution are null, as SMTInterpol does not provide them. + * Every resolution node has 3 chilren: sub-proof, pivot, sub-proof. There exists the RUP sub-proof, + * these means that the stored formula was proven by applying RUP to the child of the node. The + * PIVOT and RUP proof rules have been added to the proof format from SMTInterpol for the sake of + * offering a proof rule at every step of the proof as well as allowing to display the pivots for + * resolution steps. + */ +class SmtInterpolProof extends AbstractProof { + protected enum Rules implements ProofRule { + COEFFS("coeffs"), + VALUES("values"), + DIVISOR("divisor"), + POS("pos"), + UNIT("unit"), + DEFINE_FUN("define-fun"), + DECLARE_FUN("declare-fun"), + RUP("rup"), + PIVOT("pivot"); + final String name; + + Rules(String pDefineFun) { + name = pDefineFun; + } + + static Rules getFromName(String pName) { + if (pName.equals("DEFINE-FUN")) { + return DEFINE_FUN; + } else if (pName.equals("DECLARE-FUN")) { + return DECLARE_FUN; + } + return Rules.valueOf(pName); + } + + @Override + public String getName() { + if (this.equals(DEFINE_FUN) || this.equals(DECLARE_FUN)) { + return name; + } else { + return name().toLowerCase(Locale.ENGLISH); + } + } + } + + SmtInterpolProof(ProofRule pRule, Formula pFormula) { + super(pRule, pFormula); + } + + @Override + protected void addChild(Proof pProof) { + super.addChild(pProof); + } + + @Override + public String proofAsString() { + return super.proofAsString(); + } +} + +class SmtInterpolProofNodeCreator { + private final SmtInterpolFormulaCreator creator; + + SmtInterpolProofNodeCreator(SmtInterpolFormulaCreator pCreator) { + creator = pCreator; + } + + SmtInterpolProof createProof(ProvitionalProofNode pProofNode) { + Deque stack = new ArrayDeque<>(); + Map computed = new HashMap<>(); + + stack.push(pProofNode); + + while (!stack.isEmpty()) { + ProvitionalProofNode proofNode = stack.peek(); + + if (!proofNode.isVisited) { + proofNode.isVisited = true; + + if (proofNode.proofRule.equals(ResAxiom.RESOLUTION)) { + ProvitionalProofNode pivot = new ProvitionalProofNode(); + pivot.proofRule = Rules.PIVOT; + pivot.formulas.add(proofNode.pivot); + proofNode.children.add(1, pivot); + for (ProvitionalProofNode child : proofNode.children) { + stack.push(child); + } + } else { + for (ProvitionalProofNode child : proofNode.children) { + stack.push(child); + } + } + } else { + stack.pop(); + Formula formula = null; + if (proofNode.formulas.size() > 1) { + // This can not stay like this, the algorithm calculating the formulas to be stored is + // needed, as what we retrieve here is simply arguments for generating a clause, + // meaning the arguments do not have to be boolean and therefore joining them with OR + // causes an exception. + // Term or = Util.or(creator.getEnv(), proofNode.formulas.toArray(new Term[0])); + // formula = creator.encapsulate(creator.getFormulaType(or), or); + } else if (!proofNode.formulas.isEmpty()) { + // We only know for sure what formulas are stored in the following cases. Otherwise, we + // only have an input for generating the clauses after applying the RESOLUTE axioms. + if (proofNode.proofRule.equals(ResAxiom.RESOLUTION) + || proofNode.proofRule.equals(ResAxiom.ASSUME) + || proofNode.proofRule.equals(Rules.RUP) + || proofNode.proofRule.equals(Rules.PIVOT)) { + Term t = proofNode.formulas.get(0); + formula = creator.encapsulate(creator.getFormulaType(t), t); + } + } + SmtInterpolProof pn = new SmtInterpolProof(proofNode.proofRule, formula); + for (int i = 0; i < proofNode.children.size(); i++) { + ProvitionalProofNode child = proofNode.children.get(i); + if (computed.containsKey(child)) { + pn.addChild(computed.get(child)); + } + } + computed.put(proofNode, pn); + } + } + return computed.get(pProofNode); + } + + ProvitionalProofNode createPPNDag(Term pTerm) { + return new ProvitionalProofNode(pTerm); + } + + class ProvitionalProofNode { + Term pivot; + ProofRule proofRule; + List formulas = new ArrayList<>(); + boolean axiom; + List children = new ArrayList<>(); + Term unprocessedTerm; + boolean isVisited = false; + + ProvitionalProofNode() {} + + protected ProvitionalProofNode(Term pParameter) { + this.unprocessedTerm = pParameter; + processTerm(pParameter); + } + + protected void processTerm(Term pParameter) { + if (pParameter instanceof ApplicationTerm) { + processApplication((ApplicationTerm) pParameter); + } else if (pParameter instanceof AnnotatedTerm) { + processAnnotated((AnnotatedTerm) pParameter); + } + } + + void processApplication(ApplicationTerm term) { + Term[] parameters = term.getParameters(); + if (parameters.length == 3) { + this.proofRule = ResAxiom.RESOLUTION; + // This should be a resolution rule + Term first = parameters[0]; + if (first instanceof AnnotatedTerm) { + pivot = ((AnnotatedTerm) first).getSubterm(); + } else if (first instanceof ApplicationTerm) { + pivot = first; + } + + for (int i = 1; i < parameters.length; i++) { + Sort sort = term.getSort(); + if (sort.toString().equals("..Proof")) { + children.add(new ProvitionalProofNode(parameters[i])); + } + } + } + + if (term.getFunction().toString().contains("..assume")) { + // This should be the assume axiom + this.axiom = true; + this.proofRule = ResAxiom.ASSUME; + if (parameters[0] instanceof AnnotatedTerm) { + this.formulas.add(((AnnotatedTerm) parameters[0]).getSubterm()); + } else { + this.formulas.add(parameters[0]); + } + } + } + + private void processAnnotated(AnnotatedTerm term) { + + boolean rup = false; + + if (term.getSort().toString().equals("Bool")) { + if (this.axiom) { + this.pivot = term.getSubterm(); + } else { + this.formulas.add(term.getSubterm()); + } + } + + for (Annotation annotation : term.getAnnotations()) { + ProofRule rule; + String key = annotation.getKey().substring(1); + + if (term.getSubterm().toString().equals("..axiom")) { + this.axiom = true; + // Annotation key should contain axiom name and value should contain an array with some + // of its objects being Terms and the index before each one of those contains the + // polarity. + key = key.startsWith(":") ? key.substring(1) : key; + + rule = ResProofRule.getFromName(key); + if (rule == null) rule = Rules.getFromName(key.toUpperCase(Locale.ENGLISH)); + Preconditions.checkNotNull(key); + + this.proofRule = rule; + // This Annotation's value should have an array with the polarities and Terms that are + // proven. This is the clause proven the ApplicationTerm. The array is empty for the + // very first Term. + // Now we need to go through the array and find the Term objects and their polarity. + // This is the same for proves. + if (annotation.getValue() instanceof Object[]) { + Object[] values = (Object[]) annotation.getValue(); + addTermsFromAnnotationValue(values, false); + } else if (annotation.getValue() instanceof AnnotatedTerm) { + processAnnotated((AnnotatedTerm) annotation.getValue()); + } else if (annotation.getValue() instanceof ApplicationTerm) { + formulas.add((Term) annotation.getValue()); + } + } + + if (key.equals("rup")) { + this.proofRule = Rules.RUP; + this.children.add(new ProvitionalProofNode(term.getSubterm())); + rup = true; + } + + if (key.equals("proves")) { + Object[] values = (Object[]) annotation.getValue(); + addTermsFromAnnotationValue(values, true); + } + } + if (!rup) { + processTerm(term.getSubterm()); + } + } + + void addTermsFromAnnotationValue(Object[] values, boolean isProves) { + for (int i = 0; values.length > i; i++) { + if (values[i] instanceof Term) { + // We found a Term and the index before it should contain the polarity, but only if + // this is the value of the proves Annotation. + if (isProves) { + assert values[i - 1].getClass() == String.class; + if (((String) values[i - 1]).contains("+")) { + this.formulas.add((Term) values[i]); + } else { + // We try to create the negative polarity Term + this.formulas.add(Util.not(creator.getEnv(), (Term) values[i])); + } + } else { + this.formulas.add((Term) values[i]); + } + } + } + } + + // Just for testing purposes + protected String proofAsString() { + return proofAsString(0); + } + + String proofAsString(int indentLevel) { + StringBuilder sb = new StringBuilder(); + String indent = " ".repeat(indentLevel); + + // Node header + sb.append(indent).append("ProofNode {\n"); + + // Node properties + sb.append(indent).append(" pivot: ").append(pivot != null ? pivot : "null").append("\n"); + sb.append(indent) + .append(" proofRule: ") + .append(proofRule != null ? proofRule.getName() : "null") + .append("\n"); + sb.append(indent).append(" axiom: ").append(axiom).append("\n"); + + // Formulas + sb.append(indent).append(" formulas: [\n"); + if (formulas.isEmpty()) { + sb.append(indent).append(" empty\n"); + } else { + for (Term formula : formulas) { + sb.append(indent).append(" ").append(formula != null ? formula : "null").append("\n"); + } + } + sb.append(indent).append(" ]\n"); + + // Children nodes + sb.append(indent).append(" children: [\n"); + if (children.isEmpty()) { + sb.append(indent).append(" empty\n"); + } else { + for (ProvitionalProofNode child : children) { + if (child != null) { + sb.append(child.proofAsString(indentLevel + 2)); + } else { + sb.append(indent).append(" null\n"); + } + } + } + sb.append(indent).append(" ]\n"); + + // Close node + sb.append(indent).append("}\n"); + + return sb.toString(); + } + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java index 80f6a0e9c6..f469173d67 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolSolverContext.java @@ -202,6 +202,7 @@ private Script createNewScript(Set pOptions) { pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE) || pOptions.contains(ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS)); newOptions.put(":produce-models", pOptions.contains(ProverOptions.GENERATE_MODELS)); + newOptions.put(":produce-proofs", pOptions.contains(ProverOptions.GENERATE_PROOFS)); SMTInterpol smtInterpol = new SMTInterpol(getSmtInterpol(), newOptions, CopyMode.RESET_TO_DEFAULT); diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java index 7da2fbdbf5..237f3a2bda 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3AbstractProver.java @@ -242,6 +242,11 @@ private String getUnusedKey(Set seenKeys, final String originalKey) { return key; } + @Nullable + protected Deque> getStoredConstraints() { + return storedConstraints; + } + @Override public void close() { if (!closed) { diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3Proof.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3Proof.java new file mode 100644 index 0000000000..b359fa96ee --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3Proof.java @@ -0,0 +1,192 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.solvers.z3; + +import com.microsoft.z3.Native; +import com.microsoft.z3.enumerations.Z3_decl_kind; +import com.microsoft.z3.enumerations.Z3_parameter_kind; +import com.microsoft.z3.enumerations.Z3_sort_kind; +import java.util.ArrayDeque; +import java.util.ArrayList; +import java.util.Deque; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.proofs.Proof; +import org.sosy_lab.java_smt.api.proofs.ProofFrame; +import org.sosy_lab.java_smt.api.proofs.ProofRule; +import org.sosy_lab.java_smt.basicimpl.AbstractProof; +import org.sosy_lab.java_smt.basicimpl.FormulaCreator; +import org.sosy_lab.java_smt.solvers.z3.Z3ProofRule.Parameter; +import org.sosy_lab.java_smt.solvers.z3.Z3ProofRule.Rule; + +public class Z3Proof extends AbstractProof { + private static class Frame extends ProofFrame { + protected Frame(Long proof) { + super(proof); + } + } + + Z3Proof(Formula pFormula, ProofRule pProofRule) { + super(pProofRule, pFormula); + } + + @Override + protected void addChild(Proof child) { + super.addChild(child); + } + + @Override + public String proofAsString() { + return super.proofAsString(); + } + + /** + * This transformation omits one level of the proofs from Z3, as the leaves in that case are the + * operands of the boolean formulas used as the very first proof steps in the whole proof .E.g., + * when asserting (or (not q2) q1), that produces a single {@link Z3Proof}, but the input for that + * is a whole subtree from Z3 composed of the assertion, the disjunction and the negation, which + * in turn has q2 as a child, as well as q1. + * + * @param rootProof The root of proof DAG to be converted + * @param formulaCreator The {@link FormulaCreator} to be able to produce the {@link Formula}s + * @return The root of converted proof DAG as {@link Z3Proof} + */ + static Z3Proof generateProofImpl(long rootProof, Z3FormulaCreator formulaCreator) { + long z3context = formulaCreator.getEnv(); + // proof ast to be processed wrapped inside a frame + Deque stack = new ArrayDeque<>(); + + // proof ast has been converted into Z3Proof + Map computed = new HashMap<>(); + + stack.push(new Frame(rootProof)); + + while (!stack.isEmpty()) { + Frame frame = stack.peek(); + + // prevent processing the same proof ast multiple times + if (!frame.isVisited()) { + + Native.incRef(z3context, frame.getProof()); + + // The number of children of the proof node + frame.setNumArgs(Native.getAppNumArgs(z3context, frame.getProof())); + frame.setAsVisited(true); + + for (int i = frame.getNumArgs() - 2; i >= 0; i--) { + long arg = Native.getAppArg(z3context, frame.getProof(), i); + + if (!computed.containsKey(arg)) { + stack.push(new Frame(arg)); + } + } + } else { + + stack.pop(); + int numArgs = frame.getNumArgs(); + Formula formula; + + // needed for the sortKind + long sort = Native.getSort(z3context, frame.getProof()); + long sortKind = Native.getSortKind(z3context, sort); + Z3_sort_kind sk = Z3_sort_kind.fromInt((int) sortKind); + if (sk != Z3_sort_kind.Z3_UNKNOWN_SORT) { + // This should be a proof sort, this is not included in the enum class provided by the + // API + formula = + formulaCreator.encapsulate( + formulaCreator.getFormulaType(frame.getProof()), frame.getProof()); + } else { + // Return the i-th argument of the given application. The formula resulting from + // applying the proof rule is the last argument of the proof node. + long z3expr = Native.getAppArg(z3context, frame.getProof(), numArgs - 1); + formula = formulaCreator.encapsulate(formulaCreator.getFormulaType(z3expr), z3expr); + } + + long decl = Native.getAppDecl(z3context, frame.getProof()); + int declKind = + Native.getDeclKind(z3context, Native.getAppDecl(z3context, frame.getProof())); + + ProofRule proofRule = generateProofRule(z3context, decl, declKind); + Z3Proof node = new Z3Proof(formula, proofRule); + + for (int i = 0; i < numArgs - 1; i++) { + long arg = Native.getAppArg(z3context, frame.getProof(), i); + if (computed.containsKey(arg)) { + node.addChild(computed.get(arg)); + } + } + computed.put(frame.getProof(), node); + Native.decRef(z3context, frame.getProof()); + } + } + return computed.get(rootProof); + } + + private static Rule getPRfromDK(int declKind) { + String rawName = Z3_decl_kind.fromInt(declKind).name(); + String prName = rawName.replaceFirst("Z3_OP_PR_", ""); + // return ProofRule.fromName(Z3ProofRule.class, prName); + return Enum.valueOf(Rule.class, prName); + } + + private static ProofRule generateProofRule(long z3context, long decl, int declKind) { + List> parameters = new ArrayList<>(); + int numParams = Native.getDeclNumParameters(z3context, decl); + for (int i = 0; i < numParams; i++) { + int pk = Native.getDeclParameterKind(z3context, decl, i); + Z3_parameter_kind kind = Z3_parameter_kind.fromInt(pk); + switch (kind) { + case Z3_PARAMETER_AST: + long astRef = Native.getDeclAstParameter(z3context, decl, i); + parameters.add(new Z3ProofRule.Parameter<>(Native.astToString(z3context, astRef))); + break; + + case Z3_PARAMETER_INT: + parameters.add( + new Z3ProofRule.Parameter<>(Native.getDeclIntParameter(z3context, decl, i))); + break; + + case Z3_PARAMETER_RATIONAL: + parameters.add( + new Z3ProofRule.Parameter<>(Native.getDeclRationalParameter(z3context, decl, i))); + break; + + case Z3_PARAMETER_SYMBOL: + long symRef = Native.getDeclSymbolParameter(z3context, decl, i); + parameters.add(new Z3ProofRule.Parameter<>(Native.getSymbolString(z3context, symRef))); + break; + + case Z3_PARAMETER_DOUBLE: + parameters.add( + new Z3ProofRule.Parameter<>(Native.getDeclDoubleParameter(z3context, decl, i))); + break; + + case Z3_PARAMETER_SORT: + long sortRef = Native.getDeclSortParameter(z3context, decl, i); + parameters.add(new Z3ProofRule.Parameter<>(Native.sortToString(z3context, sortRef))); + break; + + case Z3_PARAMETER_FUNC_DECL: + long funcRef = Native.getDeclFuncDeclParameter(z3context, decl, i); + parameters.add(new Z3ProofRule.Parameter<>(Native.funcDeclToString(z3context, funcRef))); + break; + + default: + throw new UnsupportedOperationException("Can not get parameter kind: " + kind); + } + } + Rule pr = getPRfromDK(declKind); + return new Z3ProofRule(pr, parameters); + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3ProofRule.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3ProofRule.java new file mode 100644 index 0000000000..371fcdc536 --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3ProofRule.java @@ -0,0 +1,174 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.solvers.z3; + +import java.util.List; +import org.sosy_lab.java_smt.api.proofs.ProofRule; + +// TODO correctly document the formula strings + +/** Proof rules for Z3. These can be found in the Z3 API source code in the file Z3_api.h */ +class Z3ProofRule implements ProofRule { + + enum Rule implements ProofRule { + // Undefined proof object + UNDEF("undef", "undefined proof object"), + + // Basic assertions + TRUE("true", "proof for the expression 'true'"), + + ASSERTED("asserted", "(asserted p)"), + + GOAL("goal", "(goal p)"), + + // Logical inference rules + MODUS_PONENS("modus_ponens", "(mp p (implies p q) q)"), + + REFLEXIVITY("reflexivity", "reflexivity (R t t), R is element of {=, ~, iff}"), // no antecendts + + SYMMETRY("symmetry", "symmetry (R t1 t2) (R t2 t1)"), + + TRANSITIVITY("transitivity", "trans (R t1 t2) (R t2 t3) (R t1 t3)"), + + TRANSITIVITY_STAR("transitivity*", "trans *(R t1 t2) ... (R t3 t4) (R t1 t4)"), + + MONOTONICITY( + "monotonicity", + "monotonicity (R t1 s1) ... (R tn sn) (R (f t1 ... tn) (f s1 ... " + "sn))"), + + QUANT_INTRO("quant-intro", "quant-intro (~ p q) (~ (forall (x) p) (forall (x) q))"), + + BIND("bind", "(proof-bind f (forall (x) f))"), + + // Boolean and CNF transformations + DISTRIBUTIVITY("distributivity", "(f g (= (f a (g b c)) (g (f a b) (f a c)))"), // + + // no antecedents + AND_ELIM("and-elim", "and-elim (and p1 ... pn) pi"), + + NOT_OR_ELIM("not-or-elim", "not-or-elim (not (or p1 ... pn)) (not pi)"), + + // Rewriting and simplifications + REWRITE("rewrite", "rewrite (R t s), R is element of {=, iff}"), // no antededents + + REWRITE_STAR("rewrite*", "rewrite* (= t1 t2) ... (= tn-1 tn) (= t1 tn)"), + + PULL_QUANT("pull_quant", "(= (f (forall x P(x)) R) (forall x (f P(x) R)))"), + + PUSH_QUANT( + "push_quant", + "(forall x (and P1(x) ... Pn(x))) (and (forall x P1(x)) ... (forall x Pn(x)))"), + + ELIM_UNUSED_VARS("elim_unused_vars", "(forall x y P(x)) (forall x P(x))"), + + DER("der", "(iff (forall x (or (not (= x t)) P(x))) P(t))"), + + QUANT_INST("quant_inst", "(or (not (forall x P(x))) P(a))"), + + // Natural deduction style + HYPOTHESIS("hypothesis", "(hypothesis p)"), + + LEMMA("lemma", "(or (not p1) ... (not pn))"), + + UNIT_RESOLUTION( + "unit_resolution", "(or p1 ... pn q1 ... qm) (not p1) ... (not pn) (or q1 ... qm)"), + + IFF_TRUE("iff_true", "(iff p true)"), + + IFF_FALSE("iff_false", "(iff p false)"), + + COMMUTATIVITY("commutativity", "(= (f a b) (f b a))"), + + // Tseitin-like axioms + DEF_AXIOM("def_axiom", "Propositional tautologies (CNF conversion)"), + + // Clause manipulation rules + ASSUMPTION_ADD("assumption_add", "(add_clause p)"), + + LEMMA_ADD("lemma_add", "(add_lemma p)"), + + REDUNDANT_DEL("redundant_del", "(delete_clause p)"), + + CLAUSE_TRAIL("clause_trail", "(clause_trail p)"), + + // Definitions and introduction rules + DEF_INTRO("def_intro", "(= n e)"), + + APPLY_DEF("apply_def", "(~ p q)"), + + IFF_OEQ("iff_oeq", "(iff p q) (~ p q)"), + + // Negation Normal Form (NNF) transformations + NNF_POS("nnf_pos", "(~ (iff p q) (and (or p (not q)) (or (not p) q)))"), + + NNF_NEG("nnf_neg", "(not (and p1 ... pn)) (or (not p1) ... (not pn))"), + + // Skolemization + SKOLEMIZE("skolemize", "(~ (exists x P(x)) P(sk))"), + + // Theory reasoning + MODUS_PONENS_OEQ("modus_ponens_oeq", "(mp~ p (~ p q) q)"), + + TH_LEMMA("th_lemma", "Theory-specific lemma"), + + HYPER_RESOLVE("hyper_resolve", "Hyper-resolution with multiple premises"), + + OPERATION("operation", ""); + + private final String name; + private final String formula; + + Rule(String name, String formula) { + this.name = name; + this.formula = formula; + } + + // @Override + public String getName() { + return name; + } + + // @Override + public String getFormula() { + return formula; + } + } + + static class Parameter { + private final T value; + + Parameter(T value) { + this.value = value; + } + } + + private final Rule rule; + private List> parameters; + + Z3ProofRule(Rule pRule, List> pParameters) { + this.rule = pRule; + this.parameters = pParameters; + } + + @Override + public String getName() { + return rule.getName(); + } + + @Override + public String getFormula() { + return rule.getFormula(); + } + + public List> getParameters() { + return List.copyOf(this.parameters); + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java index 7d408faf11..98a8b4cf32 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java @@ -50,12 +50,16 @@ public final class Z3SolverContext extends AbstractSolverContext { private static final String OPT_ENGINE_CONFIG_KEY = "optsmt_engine"; private static final String OPT_PRIORITY_CONFIG_KEY = "priority"; + private static boolean generateProofs = false; // for debugging @Options(prefix = "solver.z3") private static class ExtraOptions { - @Option(secure = true, description = "Require proofs from SMT solver") - boolean requireProofs = false; + @Option( + secure = true, + description = "Require proofs from SMT solver", + values = {"true", "false"}) + String requireProofs = "true"; @Option( secure = true, @@ -141,8 +145,9 @@ public static synchronized Z3SolverContext create( } long cfg = Native.mkConfig(); - if (extraOptions.requireProofs) { + if (extraOptions.requireProofs.equals("true")) { Native.setParamValue(cfg, "PROOF", "true"); + generateProofs = true; } Native.globalParamSet("smt.random_seed", String.valueOf(randomSeed)); Native.globalParamSet("model.compact", "false"); @@ -279,6 +284,11 @@ public void close() { } } + // Method exlcusively used for testing + boolean getGenerateProofs() { + return generateProofs; + } + @Override protected boolean supportsAssumptionSolving() { return true; diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java index 5ec0eae466..066c68ed7f 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3TheoremProver.java @@ -8,6 +8,8 @@ package org.sosy_lab.java_smt.solvers.z3; +import static org.sosy_lab.java_smt.solvers.z3.Z3Proof.generateProofImpl; + import com.google.common.base.Preconditions; import com.google.common.collect.ImmutableMap; import com.microsoft.z3.Native; @@ -25,6 +27,7 @@ import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import org.sosy_lab.java_smt.api.SolverException; import org.sosy_lab.java_smt.api.UserPropagator; +import org.sosy_lab.java_smt.api.proofs.Proof; class Z3TheoremProver extends Z3AbstractProver implements ProverEnvironment { @@ -146,6 +149,23 @@ protected long getZ3Model() { } } + @Override + public Proof getProof() throws SolverException, InterruptedException { + Preconditions.checkState(!closed); + Preconditions.checkState(this.isUnsat()); + long proofAst; + try { + proofAst = Native.solverGetProof(z3context, z3solver); + } catch (Z3Exception e) { + throw creator.handleZ3Exception(e); + } + return generateProofImpl(proofAst, creator); + } + + public long getZ3solver() { + return z3solver; + } + @Override public int size() { Preconditions.checkState(!closed); diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3ToResolutionProofConverter.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3ToResolutionProofConverter.java new file mode 100644 index 0000000000..d65de8153c --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3ToResolutionProofConverter.java @@ -0,0 +1,1069 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2024 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.solvers.z3; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import org.sosy_lab.java_smt.AxiomProof; +import org.sosy_lab.java_smt.ResProofRule.ResAxiom; +import org.sosy_lab.java_smt.ResolutionProof; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.BooleanFormulaManager; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.FunctionDeclaration; +import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier; +import org.sosy_lab.java_smt.api.proofs.Proof; +import org.sosy_lab.java_smt.api.visitors.BooleanFormulaVisitor; +import org.sosy_lab.java_smt.api.visitors.TraversalProcess; + +/** + * Converts a Z3 proof into a format based on the RESOLUTE proof format. + * + *

The RESOLUTE format is a low-level proof format used by SMTInterpol. It exclusively relies on + * the resolution rule, with multiple axioms defined to support various theories. These axioms serve + * as the leaf nodes in the proof DAG. The strategy used is to transform each result from a Z3 proof + * into corresponding resolution proof nodes, aiming to maintain the formulas used as arguments for + * the Z3 proof rule as well as the result. Depending on the rule, the number of nodes may remain + * the same (e.g., for modus ponens) or increase (e.g., for transitivity star). For the transitivity + * star rule, the sub-proof grows approximately 2n-1 times, where n is the + * number of nodes in the sub-proof. + * + * @see Z3ProofRule for the list of Z3 proof rules. + * @see org.sosy_lab.java_smt.ResProofRule for the list of RESOLUTE axioms. + */ +@SuppressWarnings({"unchecked", "rawtypes", "unused", "static-access", "ModifiedButNotUsed"}) +public class Z3ToResolutionProofConverter { // This class is inclompete and currently not used. The + // strategy for transforming proof rules should be proved first. + private final Z3FormulaManager formulaManager; + + private final BooleanFormulaManager bfm; + + Z3ToResolutionProofConverter(Z3FormulaManager creator) { + formulaManager = creator; + bfm = formulaManager.getBooleanFormulaManager(); + } + + private static final Map ruleMapping = new HashMap<>(); + + /** + * This method converts a set of Z3ProofNodes into a {@link + * org.sosy_lab.java_smt.ResolutionProof}. + * + * @param z3ProofNodes the nodes to be converted. + * @return {@link org.sosy_lab.java_smt.ResolutionProof} + */ + ResolutionProof convertToResolutionProofDag(Z3Proof z3ProofNodes) { + + throw new UnsupportedOperationException(); + } + + // This should help extract parts of a formula to better transform proof rules. + private static final class ExtractorVisitor implements BooleanFormulaVisitor { + private final List operands = new ArrayList<>(); + + public List getOperands() { + return operands; + } + + @Override + public TraversalProcess visitEquivalence(BooleanFormula left, BooleanFormula right) { + operands.add(left); + operands.add(right); + return TraversalProcess.ABORT; + } + + @Override + public TraversalProcess visitImplication(BooleanFormula operand1, BooleanFormula operand2) { + return TraversalProcess.ABORT; + } + + @Override + public TraversalProcess visitConstant(boolean value) { + return TraversalProcess.ABORT; + } + + @Override + public TraversalProcess visitBoundVar(BooleanFormula var, int deBruijnIdx) { + return TraversalProcess.ABORT; + } + + @Override + public TraversalProcess visitNot(BooleanFormula operand) { + operands.add(operand); + return TraversalProcess.ABORT; + } + + @Override + public TraversalProcess visitAnd(List operands) { + return TraversalProcess.ABORT; + } + + @Override + public TraversalProcess visitOr(List operands) { + this.operands.addAll(operands); + return TraversalProcess.ABORT; + } + + @Override + public TraversalProcess visitXor(BooleanFormula operand1, BooleanFormula operand2) { + return TraversalProcess.ABORT; + } + + @Override + public TraversalProcess visitIfThenElse( + BooleanFormula condition, BooleanFormula thenFormula, BooleanFormula elseFormula) { + return TraversalProcess.ABORT; + } + + @Override + public TraversalProcess visitQuantifier( + Quantifier quantifier, + BooleanFormula quantifiedAST, + List boundVars, + BooleanFormula body) { + return TraversalProcess.ABORT; + } + + @Override + public TraversalProcess visitAtom( + BooleanFormula atom, FunctionDeclaration funcDecl) { + return TraversalProcess.ABORT; + } + } + + public List extractOperands(BooleanFormula formula) { + ExtractorVisitor extractor = new ExtractorVisitor(); + bfm.visitRecursively(formula, extractor); + return extractor.getOperands(); + } + + /** + * Converts a {@link Z3Proof} into either a {@link ResolutionProof} or a {@link AxiomProof}, + * depending on its rule. + * + * @param node the {@link Z3Proof} to convert + * @return the resulting {@link Proof} + */ + Proof handleNode(Z3Proof node) { + Z3ProofRule.Rule rule = (Z3ProofRule.Rule) node.getRule(); + + switch (rule) { + case TRUE: + return handleTrue(node); + + case ASSERTED: + return handleAsserted(node); + + case GOAL: + return handleAsserted(node); + + case MODUS_PONENS: + return handleModusPonens(node); + + case REFLEXIVITY: + return handleReflexivity(node); + + case SYMMETRY: + return handleSymmetry(node); + + case TRANSITIVITY: + return handleTransitivity(node); + + case TRANSITIVITY_STAR: + return handleTransitivityStar(node); + + case MONOTONICITY: + return handleMonotonicity(node); + + case QUANT_INTRO: + return handleQuantIntro(node); + + case BIND: + return handleBind(node); + + case DISTRIBUTIVITY: + handleDistributivity(node); + + case AND_ELIM: + return handleAndElim(node); + + case NOT_OR_ELIM: + return handleNotOrElim(node); + + case REWRITE: + return handleRewrite(node); + + case REWRITE_STAR: + return handleRewriteStar(node); + + case PULL_QUANT: + return handlePullQuant(node); + + case PUSH_QUANT: + return handlePushQuant(node); + + case ELIM_UNUSED_VARS: + return handleElimUnusedVars(node); + + case DER: + return handleDer(node); + + case QUANT_INST: + return handleQuantInst(node); + + case HYPOTHESIS: + return handleHypothesis(node); + + case LEMMA: + return handleLemma(node); + + case UNIT_RESOLUTION: + return handleUnitResolution(node); + + case IFF_TRUE: + handleIffTrue(node); + + case IFF_FALSE: + handleIffFalse(node); + + case COMMUTATIVITY: + handleCommutativity(node); + + case DEF_AXIOM: + return handleDefAxiom(node); + + case ASSUMPTION_ADD: + return handleAssumptionAdd(node); + + case LEMMA_ADD: + return handleLemmaAdd(node); + + case REDUNDANT_DEL: + return handleRedundantDel(node); + + case CLAUSE_TRAIL: + handleClauseTrail(node); + + case DEF_INTRO: + return handleDefIntro(node); + + case APPLY_DEF: + return handleApplyDef(node); + + case IFF_OEQ: + return handleIffOeq(node); + + case NNF_POS: + return handleNnfPos(node); + + case NNF_NEG: + return handleNnfNeg(node); + + case SKOLEMIZE: + return handleSkolemize(node); + + case MODUS_PONENS_OEQ: + return handleModusPonensOeq(node); + + case TH_LEMMA: + return handleThLemma(node); + + case HYPER_RESOLVE: + return handleHyperResolve(node); + + case OPERATION: + return handleOperation(node); + + default: + return handleDefault(node); + } + } + + Proof handleTrue(Z3Proof node) { + BooleanFormula formula = (BooleanFormula) node.getFormula(); + AxiomProof pn = new AxiomProof(ResAxiom.TRUE_POSITIVE, formula); + return pn; + } + + Proof handleAsserted(Z3Proof node) { + BooleanFormula formula = (BooleanFormula) node.getFormula(); + AxiomProof pn = new AxiomProof(ResAxiom.ASSUME, formula); + return pn; + } + + Proof handleModusPonens(Z3Proof node) { + BooleanFormula formula = (BooleanFormula) node.getFormula(); + BooleanFormula pivot = + (BooleanFormula) node.getChildren().stream().findFirst().get().getFormula(); + ResolutionProof pn = new ResolutionProof(formula, pivot); + Proof c1 = handleNode((Z3Proof) node.getChildren().stream().findFirst().get()); + Proof c2 = handleNode((Z3Proof) new ArrayList<>(node.getChildren()).get(1)); + return pn; + } + + Proof handleReflexivity(Z3Proof node) { + BooleanFormula formula = (BooleanFormula) node.getFormula(); + AxiomProof pn = new AxiomProof(ResAxiom.REFLEXIVITY, formula); + return pn; + } + + Proof handleSymmetry(Z3Proof node) { + BooleanFormula formula = (BooleanFormula) node.getFormula(); + BooleanFormula pivot = + (BooleanFormula) node.getChildren().stream().findFirst().get().getFormula(); + BooleanFormula snFormula = bfm.or(bfm.not(pivot), formula); + + ResolutionProof pn = new ResolutionProof(formula, pivot); + AxiomProof sn = new AxiomProof(ResAxiom.SYMMETRY, snFormula); + pn.addChild(sn); + pn.addChild(handleNode((Z3Proof) node.getChildren().stream().findFirst().get())); + return pn; + } + + Proof handleTransitivity(Z3Proof node) { + + BooleanFormula t1 = (BooleanFormula) node.getChildren().stream().findFirst().get().getFormula(); + BooleanFormula t2 = (BooleanFormula) new ArrayList<>(node.getChildren()).get(1).getFormula(); + BooleanFormula formula = (BooleanFormula) node.getFormula(); + + List equivalenceOperands1 = extractOperands(t1); + List equivalenceOperands2 = extractOperands(t2); + + assert equivalenceOperands1.get(1).equals(equivalenceOperands2.get(0)); + + BooleanFormula transRes = formula; + BooleanFormula transClause = bfm.or(bfm.not(t1), bfm.not(t2), formula); + + AxiomProof pn = new AxiomProof(ResAxiom.TRANSITIVITY, transClause); + + ResolutionProof transResNode = new ResolutionProof(transRes, t2); + ResolutionProof trnAnte1 = new ResolutionProof(t2, t2); + BooleanFormula trn2Formula = bfm.or(bfm.not(t2), transRes); + ResolutionProof trnAnte2 = new ResolutionProof(trn2Formula, t1); + ResolutionProof trnAnte2Ante = new ResolutionProof(t1, t1); + + transResNode.addChild(trnAnte1); + transResNode.addChild(trnAnte2); + trnAnte2.addChild(trnAnte2Ante); + trnAnte2.addChild(pn); + + return transResNode; + } + + // RESOLUTE has the transitivity axiom which we are using to create the transitivity leaf and + // encode the transitivity star rule from Z3. The original proven formulas from the premises for + // the Z3 proof are then used to perform resolution iteratively on the transitivity clause for the + // resolution proof. The resulting node has the same formula as the initial node from Z3 but also + // includes the pivot used in the last resolution step. + Proof handleTransitivityStar(Z3Proof node) { + return iterativeResolutionWithAxiom(node, ResAxiom.TRANSITIVITY); + } + + // There seems to be no equivalent singular axiom in RESOLUTE for the encoding of the + // Z3_MONOTONICITY Proof Rule: + // " Z3_OP_PR_MONOTONICITY: Monotonicity proof object. + // + // T1: (R t_1 s_1) + // ... + // Tn: (R t_n s_n) + // [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n)) + // + // Remark: if t_i == s_i, then the antecedent Ti is suppressed. + // That is, reflexivity proofs are suppressed to save space." + // from: https://github.com/Z3Prover/z3/blob/master/src/api/z3_api.h + // Possible strategy: use the oracle proof rule from RESOLUTE. Possibility: introduce the + // oracle_(rule) proof rule, e.g.: oracle_Z3_monotonicity to be able to introduce the rule as a + // clause: from ((R t_1 s_1) AND ... AND (R t_n s_n)) => (R (f t_1 ... t_n) (f s_1 ... s_n)) + // into (not (R t_1 s_1)) OR ... OR (not (R t_n s_n)) OR (R (f t_1 ... t_n) (f s_1 ... s_n)) + Proof handleMonotonicity(Z3Proof node) { + return iterativeResolutionWithAxiom(node, ResAxiom.ORACLE); + } + + // From https://github.com/Z3Prover/z3/blob/master/src/api/z3_api.h: + // Z3_OP_PR_MONOTONICITY: Monotonicity proof object. + // + // T1: (R t_1 s_1) + // ... + // Tn: (R t_n s_n) + // [monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n)) + // + // Remark: if t_i == s_i, then the antecedent Ti is suppressed. + // That is, reflexivity proofs are suppressed to save space. + Proof handleQuantIntro(Z3Proof node) { + throw new UnsupportedOperationException(); + } + + // From https://github.com/Z3Prover/z3/blob/master/src/api/z3_api.h: + // Z3_OP_PR_BIND: Given a proof p, + // produces a proof of lambda x . p, where x are free variables in p. + // + // T1: f + // [proof-bind T1] forall (x) f + // Could not find a way to encode this with given axioms from RESOLUTE, so the default solution + // is to use oracle to prove "NOT f OR (forall (x) f)" and use f as pivot from the proof of f to + // resolve into "forall (x) f". + Proof handleBind(Z3Proof node) { + List children = new ArrayList<>(node.getChildren()); + Proof child = children.get(0); + BooleanFormula f = (BooleanFormula) child.getFormula(); + + BooleanFormula forallF = (BooleanFormula) node.getFormula(); + + BooleanFormula axiomFormula = bfm.or(bfm.not(f), forallF); + AxiomProof axiom = new AxiomProof(ResAxiom.ORACLE, axiomFormula); + + ResolutionProof resNode = new ResolutionProof(forallF, f); + resNode.addChild(axiom); + resNode.addChild(child); + + return resNode; + } + + // From https://github.com/Z3Prover/z3/blob/master/src/api/z3_api.h: + // - Z3_OP_PR_DISTRIBUTIVITY: Distributivity proof object. + // Given that f (= or) distributes over g (= and), produces a proof for + // \nicebox{ + // (= (f a (g c d)) + // (g (f a c) (f a d))) + // } + // If f and g are associative, this proof also justifies the following equality: + // \nicebox{ + // (= (f (g a b) (g c d)) + // (g (f a c) (f a d) (f b c) (f b d))) + // } + // where each f and g can have arbitrary number of arguments. + // + // This proof object has no antecedents. + // Remark. This rule is used by the CNF conversion pass and + // instantiated by f = or, and g = and. + // For now skip this node and take the next step in the proof, RESOLUTE uses a combination of + // axioms to do CNF conversion and does not need a proof of distributivity. If this proof rule + // from Z3 is used for CNF conversion the next step could be useful for the resolution based + // proof + void handleDistributivity(Z3Proof node) { + // do nothing + // the parent node should be a proof step for CNF conversion that is more relevant to RESOLUTE + } + + // Z3_OP_PR_AND_ELIM: Given a proof for (and l_1 ... l_n), produces a proof for l_i + // + // T1: (and l_1 ... l_n) + // [and-elim T1]: l_i + // This is exactly the RESOLUTE axiom "and-": (-(and l_1 ... l_n) +(l_i)) + // Introduce node with said axiom and use the proof T1 to resolve the conjunction and prove l_i + // through resolution + Proof handleAndElim(Z3Proof node) { + + List children = new ArrayList<>(node.getChildren()); + Proof child = children.get(0); + + BooleanFormula t1 = (BooleanFormula) child.getFormula(); + BooleanFormula li = (BooleanFormula) node.getFormula(); + + BooleanFormula axiomFormula = bfm.or(bfm.not(t1), li); + AxiomProof axiom = new AxiomProof(ResAxiom.AND_NEGATIVE, axiomFormula); + + ResolutionProof resNode = new ResolutionProof(li, t1); + resNode.addChild(axiom); + resNode.addChild(child); + + return resNode; + } + + // Z3_OP_PR_NOT_OR_ELIM: Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i). + // + // T1: (not (or l_1 ... l_n)) + // [not-or-elim T1]: (not l_i) + // This is exactly the RESOLUTE axiom "or+": (+(or l_1 ... l_n) -(l_i)) + // Introduce node with said axiom and use the proof T1 to resolve the conjunction and prove not + // l_i through resolution + Proof handleNotOrElim(Z3Proof node) { + + List children = new ArrayList<>(node.getChildren()); + Proof child = children.get(0); + BooleanFormula t1 = (BooleanFormula) child.getFormula(); + + BooleanFormula notLi = (BooleanFormula) node.getFormula(); + + BooleanFormula orFormula = bfm.not(t1); + + BooleanFormula axiomFormula = bfm.or(orFormula, notLi); + AxiomProof axiom = new AxiomProof(ResAxiom.OR_POSITIVE, axiomFormula); + + ResolutionProof resNode = new ResolutionProof(notLi, orFormula); + resNode.addChild(axiom); + resNode.addChild(child); + + return resNode; + } + + // Z3_OP_PR_REWRITE: A proof for a local rewriting step (= t s). + // The head function symbol of t is interpreted. + // + // This proof object has no antecedents. + // The conclusion of a rewrite rule is either an equality (= t s), + // an equivalence (iff t s), or equi-satisfiability (~ t s). + // Remark: if f is bool, then = is iff. + // Examples: + // \nicebox{ + // (= (+ x 0) x) + // (= (+ x 1 2) (+ 3 x)) + // (iff (or x false) x) + // } + // the assume axiom should produce a proof that is semantically equivalent + Proof handleRewrite(Z3Proof node) { + + BooleanFormula conclusion = (BooleanFormula) node.getFormula(); + + AxiomProof axiom = new AxiomProof(ResAxiom.ASSUME, conclusion); + + return axiom; + } + + // Z3_OP_PR_REWRITE_STAR: A proof for rewriting an expression t into an expression s. + // This proof object can have n antecedents. + // The antecedents are proofs for equalities used as substitution rules. + // The proof rule is used in a few cases. The cases are: + // - When applying contextual simplification (CONTEXT_SIMPLIFIER=true) + // - When converting bit-vectors to Booleans (BIT2BOOL=true) + // Since this is also a rewrite, use the assume axiom here for the clause NOT (AND p0 ... pn) + // OR (= t s) where pi is an antecedent. This lets us resolve all the antecedents with this + // clause and conclude (= t s) + Proof handleRewriteStar(Z3Proof node) { + return iterativeResolutionWithAxiom(node, ResAxiom.ASSUME); + } + + // Z3_OP_PR_PULL_QUANT: A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). + // This proof object has no antecedents. + Proof handlePullQuant(Z3Proof node) { + throw new UnsupportedOperationException(); + } + + // Z3_OP_PR_ELIM_UNUSED_VARS: + // A proof for (iff (forall (x_1 ... x_n y_1 ... y_m) p[x_1 ... x_n]) + // (forall (x_1 ... x_n) p[x_1 ... x_n])) + // + // It is used to justify the elimination of unused variables. + // This proof object has no antecedents. + // Assume the equivalency. If this is used to substitute all occurrences of (forall (x_1 ... + // x_n y_1 ... y_m) p[x_1 ... x_n]) with (forall (x_1 ... x_n) p[x_1 ... x_n]) then a more + // complex process is needed. + Proof handleElimUnusedVars(Z3Proof node) { + BooleanFormula conclusion = (BooleanFormula) node.getFormula(); + AxiomProof axiom = new AxiomProof(ResAxiom.ASSUME, conclusion); + return axiom; + } + + // Z3_OP_PR_PUSH_QUANT: A proof for: + // \nicebox{ + // (iff (forall (x_1 ... x_m) (and p_1[x_1 ... x_m] ... p_n[x_1 ... x_m])) + // (and (forall (x_1 ... x_m) p_1[x_1 ... x_m]) + // ... + // (forall (x_1 ... x_m) p_n[x_1 ... x_m]))) + // } + // This proof object has no antecedents. + Proof handlePushQuant(Z3Proof node) { + throw new UnsupportedOperationException(); + } + + // Z3_OP_PR_DER: A proof for destructive equality resolution: + // (iff (forall (x) (or (not (= x t)) P[x])) P[t]) + // if x does not occur in t. + // + // This proof object has no antecedents. + // + // Several variables can be eliminated simultaneously. + // Analogous to the UNUSED_VARS rule. + Proof handleDer(Z3Proof node) { + BooleanFormula conclusion = (BooleanFormula) node.getFormula(); + AxiomProof axiom = new AxiomProof(ResAxiom.ASSUME, conclusion); + return axiom; + } + + // Z3_OP_PR_QUANT_INST: A proof of (or (not (forall (x) (P x))) (P a)) + // This is equivalent to the forall- axiom + Proof handleQuantInst(Z3Proof node) { + BooleanFormula formula = (BooleanFormula) node.getFormula(); + AxiomProof axiomProof = new AxiomProof(ResAxiom.FORALL_NEGATIVE, formula); + return axiomProof; + } + + // Z3_OP_PR_HYPOTHESIS: Mark a hypothesis in a natural deduction style proof. + // Assume the hypothesis + Proof handleHypothesis(Z3Proof node) { + BooleanFormula conclusion = (BooleanFormula) node.getFormula(); + AxiomProof axiom = new AxiomProof(ResAxiom.ASSUME, conclusion); + return axiom; + } + + // Z3_OP_PR_LEMMA: + // + // T1: false + // [lemma T1]: (or (not l_1) ... (not l_n)) + // + // This proof object has one antecedent: a hypothetical proof for false. + // It converts the proof in a proof for (or (not l_1) ... (not l_n)), + // when T1 contains the open hypotheses: l_1, ..., l_n. + // The hypotheses are closed after an application of a lemma. + // Furthermore, there are no other open hypotheses in the subtree covered by + // the lemma. + Proof handleLemma(Z3Proof node) { + throw new UnsupportedOperationException(); + } + + // Z3_OP_PR_UNIT_RESOLUTION: + // \nicebox{ + // T1: (or l_1 ... l_n l_1' ... l_m') + // T2: (not l_1) + // ... + // T(n+1): (not l_n) + // [unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m') + // } + // Resolve one by one, creating a resolution step for every Ti in the proof. + Proof handleUnitResolution(Z3Proof node) { + List children = new ArrayList<>(node.getChildren()); + int n = children.size(); + + // First child is the large disjunction + Proof currentRes = children.get(0); + + // Resolve iteratively with each subsequent "not l_i" + for (int i = 1; i < n; i++) { + Proof negChild = children.get(i); + BooleanFormula pivot = extractOperands((BooleanFormula) negChild.getFormula()).get(0); + List operands = extractOperands((BooleanFormula) currentRes.getFormula()); + operands.remove(0); + BooleanFormula formula = bfm.or(operands); + ResolutionProof resNode = new ResolutionProof(formula, pivot); + resNode.addChild(currentRes); + resNode.addChild(negChild); + currentRes = resNode; + } + + return currentRes; + } + + // Z3_OP_PR_IFF_TRUE: + // \nicebox{ + // T1: p + // [iff-true T1]: (iff p true) + // } + // it proves the equivalence of p. Leaving as is will be tested otherwise using the + // BooleanFormulaManager.makeTrue() method should work. + void handleIffTrue(Z3Proof node) { + // do nothing + } + + // Z3_OP_PR_IFF_FALSE: + // \nicebox{ + // T1: (not p) + // [iff-false T1]: (iff p false) + // } + // it proves the equivalence of p. Leaving as is will be tested otherwise using the + // BooleanFormulaManager.makeFalse() method should work. + void handleIffFalse(Z3Proof node) { + // do nothing + } + + // Z3_OP_PR_COMMUTATIVITY: + // + // [comm]: (= (f a b) (f b a)) + // + // f is a commutative operator. + // + // This proof object has no antecedents. + // Remark: if f is bool, then = is iff. + // similar case to handleDistributivity + void handleCommutativity(Z3Proof node) { + // do nothing + } + + // Z3_OP_PR_DEF_AXIOM: Proof object used to justify Tseitin's like axioms: + // \nicebox{ + // (or (not (and p q)) p) + // (or (not (and p q)) q) + // (or (not (and p q r)) p) + // (or (not (and p q r)) q) + // (or (not (and p q r)) r) + // ... + // (or (and p q) (not p) (not q)) + // (or (not (or p q)) p q) + // (or (or p q) (not p)) + // (or (or p q) (not q)) + // (or (not (iff p q)) (not p) q) + // (or (not (iff p q)) p (not q)) + // (or (iff p q) (not p) (not q)) + // (or (iff p q) p q) + // (or (not (ite a b c)) (not a) b) + // (or (not (ite a b c)) a c) + // (or (ite a b c) (not a) (not b)) + // (or (ite a b c) a (not c)) + // (or (not (not a)) (not a)) + // (or (not a) a) + // } + // This proof object has no antecedents. + // Note: all axioms are propositional tautologies. + // Note also that 'and' and 'or' can take multiple arguments. + // You can recover the propositional tautologies by + // unfolding the Boolean connectives in the axioms a small + // bounded number of steps (=3). + // Assume formula proven by this rule. + Proof handleDefAxiom(Z3Proof node) { + BooleanFormula conclusion = (BooleanFormula) node.getFormula(); + AxiomProof axiom = new AxiomProof(ResAxiom.ASSUME, conclusion); + return axiom; + } + + // Z3_OP_PR_ASSUMPTION_ADD + // Clausal proof adding axiom + // assume formula + Proof handleAssumptionAdd(Z3Proof node) { + BooleanFormula conclusion = (BooleanFormula) node.getFormula(); + AxiomProof axiom = new AxiomProof(ResAxiom.ASSUME, conclusion); + return axiom; + } + + // Z3_OP_PR_LEMMA_ADD + // Clausal proof lemma addition + // assume formula + Proof handleLemmaAdd(Z3Proof node) { + BooleanFormula conclusion = (BooleanFormula) node.getFormula(); + AxiomProof axiom = new AxiomProof(ResAxiom.ASSUME, conclusion); + return axiom; + } + + // Z3_OP_PR_REDUNDANT_DEL + // Clausal proof lemma deletion + // Possibility: delete whole subtree that was derived from using the redundant lemma. otherwise + // resolve it from clauses that may contain it. + Proof handleRedundantDel(Z3Proof node) { + throw new UnsupportedOperationException(); + } + + // Z3_OP_PR_CLAUSE_TRAIL, + // Clausal proof trail of additions and deletions + // this tracks the applications of additions and deletions. + void handleClauseTrail(Z3Proof node) { + // do nothing + } + + // Z3_OP_PR_DEF_INTRO: Introduces a name for a formula/term. + // Suppose e is an expression with free variables x, and def-intro + // introduces the name n(x). The possible cases are: + // + // When e is of Boolean type: + // [def-intro]: (and (or n (not e)) (or (not n) e)) + // + // or: + // [def-intro]: (or (not n) e) + // when e only occurs positively. + // + // When e is of the form (ite cond th el): + // [def-intro]: (and (or (not cond) (= n th)) (or cond (= n el))) + // + // Otherwise: + // [def-intro]: (= n e) + // + // Check form of the formula proven. + // + // When e is of Boolean type - ((not e ) or n) and ((not n) or e)) -: + // ... + // + // When e only occurs positively - (or (not n) e) -: + // we use the axiom 'or+' which produces '(+ (or (not n) e) - e)' assuming e (the + // expression) we can resolve e and get the original. + // + // ... + // + // The way it is done in the second case could be expanded to the other cases. Otherwise, it is a + // possibility to implement the oracle rule with different inputs. + // It should be possible to introduce names with the 'let' operator, as well as the way it is + // done by Z3. So another option is to use said operator here. + Proof handleDefIntro(Z3Proof node) { + throw new UnsupportedOperationException(); + } + + // Z3_OP_PR_APPLY_DEF: + // + // [apply-def T1]: F ~ n + // + // F is 'equivalent' to n, given that T1 is a proof that + // n is a name for F. + // + // This rule depends on the implementation of the DEF_INTRO rule. if using 'let' this step + // might not be needed, otherwise should be kept. According to the paper found here: + // https://www21.in.tum.de/~boehmes/proof-reconstruction.html + // Most instance of equisatisfiability -'~'- can be represented by equivalency in Isabelle/HOL. + // Therefore, it should be possible to also use equivalency in a RESOLUTE based format. + Proof handleApplyDef(Z3Proof node) { + throw new UnsupportedOperationException(); + } + + // Z3_OP_PR_IFF_OEQ: + // + // T1: (iff p q) + // [iff~ T1]: (~ p q) + // + // This rule does the opposite of what we are trying to do with the ~ operator. Skipping this + // rule applicaiton should work. However, every instance of ~ later on should be replaced with + // iff. In fact, replacing all ~ instances with iff might be desired. + Proof handleIffOeq(Z3Proof node) { + Z3Proof child = (Z3Proof) node.getChildren().toArray()[0]; + ResolutionProof resolutionProof = (ResolutionProof) handleNode(child); + return resolutionProof; + } + + // Z3_OP_PR_NNF_POS: Proof for a (positive) NNF step. Example: + // + // T1: (not s_1) ~ r_1 + // T2: (not s_2) ~ r_2 + // T3: s_1 ~ r_1' + // T4: s_2 ~ r_2' r_2 => r_1 r_1 => r_2 + // [nnf-pos T1 T2 T3 T4]: (~ (iff s_1 s_2) (and (or r_1 r_2') (or r_1' r_2))) + // NOT r_2 not r_1 + // The negation normal form steps NNF_POS and NNF_NEG are used in the following cases: + // (a) When creating the NNF of a positive force quantifier. + // The quantifier is retained (unless the bound variables are eliminated). + // Example + // + // T1: q ~ q_new + // [nnf-pos T1]: (~ (forall (x T) q) (forall (x T) q_new)) + // + // (b) When recursively creating NNF over Boolean formulas, where the top-level + // connective is changed during NNF conversion. The relevant Boolean connectives + // for NNF_POS are 'implies', 'iff', 'xor', 'ite'. + // NNF_NEG furthermore handles the case where negation is pushed + // over Boolean connectives 'and' and 'or'. + // + // Possibly skip the rest of the tree and use oracle to introduce the equivalence this rule + // proves. + // Actually, this equivalence would require to have a system in place to record the + // susbtitution of the previous formula for the one in nnf so that it can then be used in place + // of the original one if this is indeed what happens during z3. + // use =+2: (+ (= p0 p1) - p0 - p1) to establish the required substitution. + Proof handleNnfPos(Z3Proof node) { + throw new UnsupportedOperationException(); + } + + // Z3_OP_PR_NNF_NEG: Proof for a (negative) NNF step. Examples: + // + // T1: (not s_1) ~ r_1 + // ... + // Tn: (not s_n) ~ r_n + // [nnf-neg T1 ... Tn]: (not (and s_1 ... s_n)) ~ (or r_1 ... r_n) + // + // and + // + // T1: (not s_1) ~ r_1 + // ... + // Tn: (not s_n) ~ r_n + // [nnf-neg T1 ... Tn]: (not (or s_1 ... s_n)) ~ (and r_1 ... r_n) + // + // and + // + // T1: (not s_1) ~ r_1 + // T2: (not s_2) ~ r_2 + // T3: s_1 ~ r_1' + // T4: s_2 ~ r_2' + // [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2)) + // (and (or r_1 r_2) (or r_1' r_2'))) + // Same strategy as with NnfPos + Proof handleNnfNeg(Z3Proof node) { + throw new UnsupportedOperationException(); + } + + // Z3_OP_PR_SKOLEMIZE: Proof for: + // + // [sk]: (~ (not (forall x (p x y))) (not (p (sk y) y))) + // [sk]: (~ (exists x (p x y)) (p (sk y) y)) + // + // This proof object has no antecedents. + // Strategies: + // - use the exists- axiom to prove the formula without the quantifier. + // - oracle axiom to prove the entire formula. + // - use the define-fun axiom to defin the sk function to be used. This would imply tracking + // the whole proof where the (p (sk y) y) formula is used. + // - use a let or other mechanism for recording the equisatisfiability of the original formula + // with the new one. + Proof handleSkolemize(Z3Proof node) { + throw new UnsupportedOperationException(); + } + + // Z3_OP_PR_MODUS_PONENS_OEQ: Modus ponens style rule for equi-satisfiability. + // + // T1: p + // T2: (~ p q) + // [mp~ T1 T2]: q + // Strategy: Introduce (not (T1 and T2)) or q as an axiom and proceed to resolve T1 and T2 to + // end up with q. + Proof handleModusPonensOeq(Z3Proof node) { + return iterativeResolutionWithAxiom(node, ResAxiom.ORACLE); + } + + // Z3_OP_PR_TH_LEMMA: Generic proof for theory lemmas. + // The theory lemma function comes with one or more parameters. + // The first parameter indicates the name of the theory. + // For the theory of arithmetic, additional parameters provide hints for + // checking the theory lemma. + // The hints for arithmetic are: + // + // - farkas - followed by rational coefficients. Multiply the coefficients to the + // inequalities in the lemma, add the (negated) inequalities and obtain a contradiction. + // + // - triangle-eq - Indicates a lemma related to the equivalence: + // + // (iff (= t1 t2) (and (<= t1 t2) (<= t2 t1))) + // + // - gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test. + // This is an example for the parameters included with a TH_LEMMA proof: + // Decl kind: Z3_OP_PR_TH_LEMMA (th-lemma) + // Num parameters: 4 + // Param[0] kind: Z3_PARAMETER_SYMBOL + // symbol: arith + // Param[1] kind: Z3_PARAMETER_SYMBOL + // symbol: farkas + // Param[2] kind: Z3_PARAMETER_RATIONAL + // value: 1 + // Param[3] kind: Z3_PARAMETER_RATIONAL + // value: 1 + // child 0 of ast 125199987906936 + // Kind: Z3_APP_AST + // Decl kind: Z3_OP_OR (or) + // String: (or (>= (+ x (* (- 1.0) y)) (- 2.0)) (<= (+ x (* (- 1.0) y)) 2.0)) + // This actually shows that some information is lost when transforming the proof form Z3 into + // the representation in the Proofs common API. + // Strategy: Use oracle. In the future this should be expanded to allow to include the hints of + // the theory, lemma and other parameters. + Proof handleThLemma(Z3Proof node) { + return new AxiomProof(ResAxiom.ORACLE, node.getFormula()); + } + + // Z3_OP_PR_HYPER_RESOLVE: Hyper-resolution rule. + // + // The premises of the rules is a sequence of clauses. + // The first clause argument is the main clause of the rule. + // with a literal from the first (main) clause. + // + // Premises of the rules are of the form + // \nicebox{ + // (or l0 l1 l2 .. ln) + // } + // or + // \nicebox{ + // (=> (and l1 l2 .. ln) l0) + // } + // or in the most general (ground) form: + // \nicebox{ + // (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln)) + // } + // In other words we use the following (Prolog style) convention for Horn + // implications: + // The head of a Horn implication is position 0, + // the first conjunct in the body of an implication is position 1 + // the second conjunct in the body of an implication is position 2 + // + // For general implications where the head is a disjunction, the + // first n positions correspond to the n disjuncts in the head. + // The next m positions correspond to the m conjuncts in the body. + // + // The premises can be universally quantified so that the most + // general non-ground form is: + // + // \nicebox{ + // (forall (vars) (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln))) + // } + // + // The hyper-resolution rule takes a sequence of parameters. + // The parameters are substitutions of bound variables separated by pairs + // of literal positions from the main clause and side clause. + // + Proof handleHyperResolve(Z3Proof node) { + throw new UnsupportedOperationException(); + } + + Proof handleOperation(Z3Proof node) { + throw new UnsupportedOperationException(); + } + + Proof handleDefault(Z3Proof node) { + throw new UnsupportedOperationException(); + } + + // Creates a subtree of resolution rule applications after creating the axiom needed to then + // resolve each pivot. + private ResolutionProof iterativeResolutionWithAxiom(Z3Proof node, ResAxiom axiom) { + List children = new ArrayList<>(node.getChildren()); + int n = children.size(); + List formulas = new ArrayList<>(); + + for (int i = 0; i < n; i++) { + assert (formulaManager.getFormulaType(children.get(i).getFormula()).isBooleanType()); + formulas.add(bfm.not((BooleanFormula) children.get(i).getFormula())); + } + + assert (formulaManager.getFormulaType(node.getFormula()).isBooleanType()); + formulas.add((BooleanFormula) node.getFormula()); + + BooleanFormula axiomFormula = bfm.or(formulas); + AxiomProof ax = new AxiomProof(axiom, axiomFormula); + + Formula resPivot = children.get(n - 1).getFormula(); + ResolutionProof resNode = new ResolutionProof(node.getFormula(), resPivot); + + Proof childNode = ax; + for (int i = 0; i < n - 1; i++) { + resPivot = children.get(i).getFormula(); + assert formulas.get(0).equals(bfm.not((BooleanFormula) resPivot)); + formulas.remove(0); + ResolutionProof rp = new ResolutionProof(bfm.or(formulas), resPivot); + rp.addChild(childNode); + rp.addChild(children.get(i)); + childNode = rp; + } + + resNode.addChild(childNode); + resNode.addChild(children.get(n - 1)); + + return resNode; + } + + // This is for debugging purposes. + void printProof(Proof node, int indentLevel) { + String indent = " ".repeat(indentLevel); + + if (node instanceof AxiomProof) { + AxiomProof sourceNode = (AxiomProof) node; + System.out.println(indent + "Formula: " + sourceNode.getFormula()); + System.out.println(indent + "Rule: " + sourceNode.getRule()); + System.out.println(indent + "No. Children: " + sourceNode.getChildren().size()); + int i = 0; + for (Proof child : sourceNode.getChildren()) { + System.out.println(indent + "Child " + ++i + ":"); + printProof(child, indentLevel + 1); + } + } else if (node instanceof ResolutionProof) { + ResolutionProof resolutionNode = (ResolutionProof) node; + System.out.println(indent + "Formula: " + resolutionNode.getFormula()); + System.out.println(indent + "Pivot: " + resolutionNode.getPivot()); + System.out.println(indent + "Rule: " + resolutionNode.getRule()); + System.out.println(indent + "No. Children: " + resolutionNode.getChildren().size()); + int i = 0; + for (Proof child : resolutionNode.getChildren()) { + System.out.println(indent + "Child " + ++i + ":"); + printProof(child, indentLevel + 1); + } + } else { + throw new AssertionError("Unknown proof node type"); + } + } +} diff --git a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java index 861d441372..546f2a7816 100644 --- a/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java +++ b/src/org/sosy_lab/java_smt/test/ProverEnvironmentTest.java @@ -10,12 +10,17 @@ import static com.google.common.truth.Truth.assertThat; import static com.google.common.truth.TruthJUnit.assume; +import static org.junit.Assert.assertNotEquals; import static org.junit.Assert.assertThrows; +import static org.junit.Assert.assertTrue; import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.CVC4; import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.CVC5; import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.MATHSAT5; import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.OPENSMT; import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.PRINCESS; +import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.SMTINTERPOL; +import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.Z3; +import static org.sosy_lab.java_smt.api.FormulaType.IntegerType; import static org.sosy_lab.java_smt.api.SolverContext.ProverOptions.GENERATE_UNSAT_CORE; import static org.sosy_lab.java_smt.api.SolverContext.ProverOptions.GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS; import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat; @@ -24,12 +29,28 @@ import java.util.List; import java.util.Optional; import org.junit.Test; +import org.sosy_lab.java_smt.api.ArrayFormula; import org.sosy_lab.java_smt.api.BasicProverEnvironment; +import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType; +import org.sosy_lab.java_smt.api.FunctionDeclaration; import org.sosy_lab.java_smt.api.Model; +import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; +import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; import org.sosy_lab.java_smt.api.ProverEnvironment; +import org.sosy_lab.java_smt.api.RationalFormulaManager; import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; import org.sosy_lab.java_smt.api.SolverException; +import org.sosy_lab.java_smt.api.proofs.Proof; +import org.sosy_lab.java_smt.api.proofs.ProofRule; +import org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaSolverContext; +import org.sosy_lab.java_smt.solvers.boolector.BoolectorSolverContext; +import org.sosy_lab.java_smt.solvers.cvc4.CVC4SolverContext; +import org.sosy_lab.java_smt.solvers.opensmt.OpenSmtSolverContext; +import org.sosy_lab.java_smt.solvers.princess.PrincessSolverContext; +import org.sosy_lab.java_smt.solvers.yices2.Yices2SolverContext; public class ProverEnvironmentTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { @@ -187,4 +208,616 @@ private void checkSimpleQuery(ProverEnvironment pProver) pProver.pop(); } } + + @Test + public void testGetSimpleBooleanProof() throws InterruptedException, SolverException { + requireProofGeneration(); // Ensures proofs are supported + BooleanFormula q1 = bmgr.makeVariable("q1"); + BooleanFormula q2 = bmgr.makeVariable("q2"); + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_PROOFS)) { + prover.addConstraint(bmgr.or(bmgr.not(q1), q2)); + prover.addConstraint(q1); + prover.addConstraint(bmgr.not(q2)); + + assertThat(prover.isUnsat()).isTrue(); + + // Test getProof() + Proof proof = prover.getProof(); + assertThat(proof).isNotNull(); + + // Test getRule() + assertThat(proof.getRule()).isNotNull(); + assertThat(proof.getRule()).isInstanceOf(ProofRule.class); + + // Test getFormula() + if (solverToUse().equals(SMTINTERPOL)) { + assertThat(proof.getFormula()).isNull(); + } else { + assertThat(proof.getFormula()).isNotNull(); + } + + // Test getArguments() + assertThat(proof.getChildren()).isNotNull(); + assertThat(proof.getChildren()).isNotEmpty(); + + // Test isLeaf() + assertThat(proof.isLeaf()).isFalse(); + Proof leaf = findanyProofLeaf(proof); + assertThat(leaf).isNotNull(); + assertThat(leaf.isLeaf()).isTrue(); + + } catch (UnsupportedOperationException e) { + assertThat(e) + .hasMessageThat() + .isEqualTo("Proof generation is not available for the current solver."); + Class contextClass = context.getClass(); + boolean isExpected = + contextClass.equals(CVC4SolverContext.class) + || contextClass.equals(PrincessSolverContext.class) + || contextClass.equals(OpenSmtSolverContext.class) + || contextClass.equals(BoolectorSolverContext.class) + || contextClass.equals(BitwuzlaSolverContext.class) + || contextClass.equals(Yices2SolverContext.class); + assertThat(isExpected).isTrue(); + } + } + + @Test + public void testGetComplexRationalNumeralAndUFProof() + throws InterruptedException, SolverException { + requireProofGeneration(); // Ensures proofs are supported + requireRationals(); + + // "(declare-fun x1 () Real)" + + // "(declare-fun x2 () Real)" + + // "(declare-fun x3 () Real)" + + // "(declare-fun y1 () Real)" + + // "(declare-fun y2 () Real)" + + // "(declare-fun y3 () Real)" + + // "(declare-fun b () Real)" + + // "(declare-fun f (Real) Real)" + + // "(declare-fun g (Real) Real)" + + // "(declare-fun a () Bool)" + + // "(declare-fun c () Bool)" + + // "(assert (and a (= (+ (f y1) y2) y3) (<= y1 x1)))" + + // "(assert (and (= x2 (g b)) (= y2 (g b)) (<= x1 y1) (< x3 y3)))" + + // "(assert (= a (= (+ (f x1) x2) x3)))" + + // "(assert (and (or a c) (not c)))"; + RationalFormula x1 = mgr.makeVariable(FormulaType.RationalType, "x1"); + RationalFormula x2 = mgr.makeVariable(FormulaType.RationalType, "x2"); + RationalFormula x3 = mgr.makeVariable(FormulaType.RationalType, "x3"); + RationalFormula y1 = mgr.makeVariable(FormulaType.RationalType, "y1"); + RationalFormula y2 = mgr.makeVariable(FormulaType.RationalType, "y2"); + RationalFormula y3 = mgr.makeVariable(FormulaType.RationalType, "y3"); + RationalFormula b = mgr.makeVariable(FormulaType.RationalType, "b"); + FunctionDeclaration f = + mgr.getUFManager().declareUF("f", FormulaType.RationalType, FormulaType.RationalType); + FunctionDeclaration g = + mgr.getUFManager().declareUF("g", FormulaType.RationalType, FormulaType.RationalType); + BooleanFormula a = bmgr.makeVariable("a"); + BooleanFormula c = bmgr.makeVariable("c"); + + RationalFormulaManager rfmgr = mgr.getRationalFormulaManager(); + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_PROOFS)) { + // "(assert (and a (= (+ (f y1) y2) y3) (<= y1 x1)))" + prover.addConstraint( + bmgr.and( + a, + rfmgr.equal(rfmgr.add(mgr.makeApplication(f, y1), y2), y3), + rfmgr.lessOrEquals(y1, x1))); + // "(assert (and (= x2 (g b)) (= y2 (g b)) (<= x1 y1) (< x3 y3)))" + prover.addConstraint( + bmgr.and( + rfmgr.equal(x2, mgr.makeApplication(g, b)), + rfmgr.equal(y2, mgr.makeApplication(g, b)), + rfmgr.lessOrEquals(x1, y1), + rfmgr.lessThan(x3, y3))); + // "(assert (= a (= (+ (f x1) x2) x3)))" + prover.addConstraint( + bmgr.equivalence(a, rfmgr.equal(rfmgr.add(mgr.makeApplication(f, x1), x2), x3))); + // "(assert (and (or a c) (not c)))" + prover.addConstraint(bmgr.and(bmgr.or(a, c), bmgr.not(c))); + assertTrue(prover.isUnsat()); + + // Retrieve and verify proof + Proof proof = prover.getProof(); + assertThat(proof).isNotNull(); + + // Root formula check + if (solverToUse().equals(SMTINTERPOL)) { + assertThat(proof.getFormula()).isNull(); + } else { + assertThat(proof.getFormula()).isEqualTo(bmgr.makeFalse()); + } + + // Rule check + assertThat(proof.getRule()).isNotNull(); + assertThat(proof.getRule()).isInstanceOf(ProofRule.class); + + // Arguments check + assertThat(proof.getChildren()).isNotNull(); + assertThat(proof.getChildren()).isNotEmpty(); + + // Leaf check + assertThat(proof.isLeaf()).isFalse(); + Proof leaf = findanyProofLeaf(proof); + assertThat(leaf).isNotNull(); + assertThat(leaf.isLeaf()).isTrue(); + + } catch (UnsupportedOperationException e) { + assertThat(e) + .hasMessageThat() + .isEqualTo("Proof generation is not available for the current solver."); + Class contextClass = context.getClass(); + boolean isExpected = + contextClass.equals(CVC4SolverContext.class) + || contextClass.equals(PrincessSolverContext.class) + || contextClass.equals(OpenSmtSolverContext.class) + || contextClass.equals(BoolectorSolverContext.class) + || contextClass.equals(BitwuzlaSolverContext.class) + || contextClass.equals(Yices2SolverContext.class); + assertThat(isExpected).isTrue(); + } + } + + @Test + public void proofOfTrueTest() throws InterruptedException, SolverException { + requireProofGeneration(); + + BooleanFormula tru = bmgr.makeTrue(); + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_PROOFS)) { + prover.addConstraint(tru); + assertThat(prover.isUnsat()).isFalse(); + + Proof proof = prover.getProof(); + assertThat(proof).isNotNull(); + + } catch (UnsupportedOperationException e) { + assertThat(e) + .hasMessageThat() + .isEqualTo("Proof generation is not available for the current solver."); + Class contextClass = context.getClass(); + boolean isExpected = + contextClass.equals(CVC4SolverContext.class) + || contextClass.equals(PrincessSolverContext.class) + || contextClass.equals(BoolectorSolverContext.class) + || contextClass.equals(BitwuzlaSolverContext.class) + || contextClass.equals(Yices2SolverContext.class); + assertThat(isExpected).isTrue(); + } catch (IllegalStateException ie) { + // this should be thrown as getProof was called when last evaluation was SAT + } + } + + // TODO: Mathsat5 does not produce a msat_manager. It adds null to de asserted formulas when + // adding the constraint for false. + @Test + public void proofOfFalseTest() throws InterruptedException, SolverException { + requireProofGeneration(); + assume().that(solverToUse()).isNotEqualTo(MATHSAT5); + + BooleanFormula bottom = bmgr.makeFalse(); + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_PROOFS)) { + prover.addConstraint(bottom); + assertThat(prover.isUnsat()).isTrue(); + + Proof proof = prover.getProof(); + assertThat(proof).isNotNull(); + + } catch (UnsupportedOperationException e) { + assertThat(e) + .hasMessageThat() + .isEqualTo("Proof generation is not available for the current solver."); + Class contextClass = context.getClass(); + boolean isExpected = + contextClass.equals(CVC4SolverContext.class) + || contextClass.equals(PrincessSolverContext.class) + || contextClass.equals(BoolectorSolverContext.class) + || contextClass.equals(BitwuzlaSolverContext.class) + || contextClass.equals(Yices2SolverContext.class); + assertThat(isExpected).isTrue(); + } catch (IllegalStateException ie) { + // this should be thrown as getProof was called when last evaluation was SAT + } + } + + @Test + public void testGetSimpleIntegerProof() throws InterruptedException, SolverException { + requireProofGeneration(); // Ensures proofs are supported + requireIntegers(); + + IntegerFormula x1 = imgr.makeVariable("x1"); + IntegerFormula two = imgr.makeNumber("2"); + IntegerFormula cero = imgr.makeNumber("0"); + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_PROOFS)) { + prover.addConstraint(imgr.equal(x1, two)); + prover.addConstraint(imgr.lessThan(x1, cero)); + assertThat(prover.isUnsat()).isTrue(); + + // Test getProof() + Proof proof = prover.getProof(); + assertThat(proof).isNotNull(); + + // Test getRule() + assertThat(proof.getRule()).isNotNull(); + assertThat(proof.getRule()).isInstanceOf(ProofRule.class); + + // Test getFormula(), the root should always be false + if (solverToUse().equals(SMTINTERPOL)) { + assertThat(proof.getFormula()).isNull(); + } else { + assertThat(proof.getFormula()).isEqualTo(bmgr.makeFalse()); + } + + // Test getArguments() + assertThat(proof.getChildren()).isNotNull(); + assertThat(proof.getChildren()).isNotEmpty(); + + // Test isLeaf() + assertThat(proof.isLeaf()).isFalse(); + Proof leaf = findanyProofLeaf(proof); + assertThat(leaf).isNotNull(); + assertThat(leaf.isLeaf()).isTrue(); + + // if (solverToUse().equals(OPENSMT)) { + // System.out.println(((AbstractSubproof) proof).proofAsString()); + // } + + } catch (UnsupportedOperationException e) { + assertThat(e) + .hasMessageThat() + .isEqualTo("Proof generation is not available for the current solver."); + Class contextClass = context.getClass(); + boolean isExpected = + contextClass.equals(CVC4SolverContext.class) + || contextClass.equals(PrincessSolverContext.class) + // || contextClass.equals(OpenSmtSolverContext.class) + || contextClass.equals(BoolectorSolverContext.class) + || contextClass.equals(BitwuzlaSolverContext.class) + || contextClass.equals(Yices2SolverContext.class); + assertThat(isExpected).isTrue(); + } + } + + @Test + public void getProofAfterGetProofAndAddingAssertionsTest() + throws InterruptedException, SolverException { + requireProofGeneration(); // Ensures proofs are supported + BooleanFormula q1 = bmgr.makeVariable("q1"); + BooleanFormula q2 = bmgr.makeVariable("q2"); + IntegerFormula x1 = imgr.makeVariable("x1"); + IntegerFormula two = imgr.makeNumber("2"); + IntegerFormula cero = imgr.makeNumber("0"); + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_PROOFS)) { + prover.addConstraint(bmgr.or(bmgr.not(q1), q2)); + prover.addConstraint(q1); + prover.addConstraint(bmgr.not(q2)); + + assertThat(prover.isUnsat()).isTrue(); + + // Test getProof() + Proof proof = prover.getProof(); + assertThat(proof).isNotNull(); + + // Test getRule() + assertThat(proof.getRule()).isNotNull(); + assertThat(proof.getRule()).isInstanceOf(ProofRule.class); + + // Test getFormula(), the root should always be false + if (solverToUse().equals(SMTINTERPOL)) { + assertThat(proof.getFormula()).isNull(); + } else { + assertThat(proof.getFormula()).isEqualTo(bmgr.makeFalse()); + } + + // Test getArguments() + assertThat(proof.getChildren()).isNotNull(); + assertThat(proof.getChildren()).isNotEmpty(); + + // Test isLeaf() + assertThat(proof.isLeaf()).isFalse(); + Proof leaf = findanyProofLeaf(proof); + assertThat(leaf).isNotNull(); + assertThat(leaf.isLeaf()).isTrue(); + + // assert integer formulas and test again + prover.addConstraint(imgr.equal(x1, two)); + prover.addConstraint(imgr.lessThan(x1, cero)); + + assertThat(prover.isUnsat()).isTrue(); + + // Test getProof() + Proof secondProof = prover.getProof(); + assertThat(secondProof).isNotNull(); + + // Test getRule() + assertThat(secondProof.getRule()).isNotNull(); + assertThat(secondProof.getRule()).isInstanceOf(ProofRule.class); + + // Test getFormula(), the root should always be false + if (solverToUse().equals(SMTINTERPOL)) { + assertThat(secondProof.getFormula()).isNull(); + } else { + assertThat(secondProof.getFormula()).isEqualTo(bmgr.makeFalse()); + } + + // Test getArguments() + assertThat(secondProof.getChildren()).isNotNull(); + assertThat(secondProof.getChildren()).isNotEmpty(); + + // Test isLeaf() + assertThat(secondProof.isLeaf()).isFalse(); + leaf = findanyProofLeaf(secondProof); + assertThat(leaf).isNotNull(); + assertThat(leaf.isLeaf()).isTrue(); + + assertNotEquals(proof, secondProof); + + } catch (UnsupportedOperationException e) { + assertThat(e) + .hasMessageThat() + .isEqualTo("Proof generation is not available for the current solver."); + Class contextClass = context.getClass(); + boolean isExpected = + contextClass.equals(CVC4SolverContext.class) + || contextClass.equals(PrincessSolverContext.class) + || contextClass.equals(OpenSmtSolverContext.class) + || contextClass.equals(BoolectorSolverContext.class) + || contextClass.equals(BitwuzlaSolverContext.class) + || contextClass.equals(Yices2SolverContext.class); + assertThat(isExpected).isTrue(); + } + } + + @Test + public void getProofAfterGetProofClearingStackAndAddingDifferentAssertionsTest() + throws InterruptedException, SolverException { + requireProofGeneration(); // Ensures proofs are supported + requireIntegers(); + + BooleanFormula q1 = bmgr.makeVariable("q1"); + BooleanFormula q2 = bmgr.makeVariable("q2"); + IntegerFormula x1 = imgr.makeVariable("x1"); + IntegerFormula two = imgr.makeNumber("2"); + IntegerFormula cero = imgr.makeNumber("0"); + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_PROOFS)) { + + prover.push(bmgr.or(bmgr.not(q1), q2)); + prover.push(q1); + prover.push(bmgr.not(q2)); + + assertThat(prover.isUnsat()).isTrue(); + + // Test getProof() + Proof proof = prover.getProof(); + assertThat(proof).isNotNull(); + + // Test getRule() + assertThat(proof.getRule()).isNotNull(); + assertThat(proof.getRule()).isInstanceOf(ProofRule.class); + + // Test getFormula(), the root should always be false + if (solverToUse().equals(SMTINTERPOL)) { + assertThat(proof.getFormula()).isNull(); + } else { + assertThat(proof.getFormula()).isEqualTo(bmgr.makeFalse()); + } + + // Test getArguments() + assertThat(proof.getChildren()).isNotNull(); + assertThat(proof.getChildren()).isNotEmpty(); + + // Test isLeaf() + assertThat(proof.isLeaf()).isFalse(); + Proof leaf = findanyProofLeaf(proof); + assertThat(leaf).isNotNull(); + assertThat(leaf.isLeaf()).isTrue(); + + // System.out.println(((AbstractSubproof) proof).proofAsString()); + + prover.pop(); + prover.pop(); + prover.pop(); + + // assert integer formulas and test again + prover.push(imgr.equal(x1, two)); + prover.push(imgr.lessThan(x1, cero)); + + assertThat(prover.isUnsat()).isTrue(); + + // Test getProof() + Proof secondProof = prover.getProof(); + assertThat(secondProof).isNotNull(); + + // Test getRule() + assertThat(secondProof.getRule()).isNotNull(); + assertThat(secondProof.getRule()).isInstanceOf(ProofRule.class); + + // Test getFormula(), the root should always be false + if (solverToUse().equals(SMTINTERPOL)) { + assertThat(secondProof.getFormula()).isNull(); + } else { + assertThat(secondProof.getFormula()).isEqualTo(bmgr.makeFalse()); + } + + // Test getArguments() + assertThat(secondProof.getChildren()).isNotNull(); + assertThat(secondProof.getChildren()).isNotEmpty(); + + // Test isLeaf() + assertThat(secondProof.isLeaf()).isFalse(); + leaf = findanyProofLeaf(proof); + assertThat(leaf).isNotNull(); + assertThat(leaf.isLeaf()).isTrue(); + + // System.out.println(((AbstractSubproof) proof).proofAsString()); + + assertNotEquals(proof, secondProof); + + } catch (UnsupportedOperationException e) { + assertThat(e) + .hasMessageThat() + .isEqualTo("Proof generation is not available for the current solver."); + Class contextClass = context.getClass(); + boolean isExpected = + contextClass.equals(CVC4SolverContext.class) + || contextClass.equals(PrincessSolverContext.class) + || contextClass.equals(OpenSmtSolverContext.class) + || contextClass.equals(BoolectorSolverContext.class) + || contextClass.equals(BitwuzlaSolverContext.class) + || contextClass.equals(Yices2SolverContext.class); + assertThat(isExpected).isTrue(); + } + } + + @Test + public void getProofWithoutProofProductionEnabledTest() + throws InterruptedException, SolverException { + requireProofGeneration(); + + BooleanFormula bottom = bmgr.makeFalse(); + + try (ProverEnvironment prover = context.newProverEnvironment()) { + prover.addConstraint(bottom); + assertThat(prover.isUnsat()).isTrue(); + + Proof proof = prover.getProof(); + + // Z3 always has proof generation on + if (solverToUse().equals(Z3)) { + assertThat(proof.getFormula()).isNotNull(); + } + + } catch (UnsupportedOperationException e) { + assertThat(e) + .hasMessageThat() + .isEqualTo("Proof generation is not available for the current solver."); + } catch (IllegalStateException e) { + assertThat(e).hasMessageThat().isEqualTo("Please set the prover option GENERATE_PROOFS."); + } + } + + // This test is based on the bvIsZeroAfterShiftLeft() test in BitvectorFormulaManagerTest + @Test + public void getBitVectorProofTest() throws InterruptedException, SolverException { + requireProofGeneration(); + requireBitvectors(); + + BitvectorFormula one = bvmgr.makeBitvector(32, 1); + + // unsigned char + BitvectorFormula a = bvmgr.makeVariable(8, "char_a"); + BitvectorFormula b = bvmgr.makeVariable(8, "char_b"); + BitvectorFormula rightOp = bvmgr.makeBitvector(32, 7); + + // 'cast' a to unsigned int + a = bvmgr.extend(a, 32 - 8, false); + b = bvmgr.extend(b, 32 - 8, false); + a = bvmgr.or(a, one); + b = bvmgr.or(b, one); + a = bvmgr.extract(a, 7, 0); + b = bvmgr.extract(b, 7, 0); + a = bvmgr.extend(a, 32 - 8, false); + b = bvmgr.extend(b, 32 - 8, false); + + a = bvmgr.shiftLeft(a, rightOp); + b = bvmgr.shiftLeft(b, rightOp); + a = bvmgr.extract(a, 7, 0); + b = bvmgr.extract(b, 7, 0); + BooleanFormula f = bmgr.not(bvmgr.equal(a, b)); + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_PROOFS)) { + prover.addConstraint(f); + assertThat(prover.isUnsat()).isTrue(); + + // Test getProof() + Proof proof = prover.getProof(); + assertThat(proof).isNotNull(); + + // Test getRule() + assertThat(proof.getRule()).isNotNull(); + assertThat(proof.getRule()).isInstanceOf(ProofRule.class); + + // Test getFormula(), the root should always be false + if (solverToUse().equals(SMTINTERPOL)) { + assertThat(proof.getFormula()).isNull(); + } else { + assertThat(proof.getFormula()).isEqualTo(bmgr.makeFalse()); + } + + // Test getArguments() + assertThat(proof.getChildren()).isNotNull(); + assertThat(proof.getChildren()).isNotEmpty(); + + // Test isLeaf() + assertThat(proof.isLeaf()).isFalse(); + Proof leaf = findanyProofLeaf(proof); + assertThat(leaf).isNotNull(); + assertThat(leaf.isLeaf()).isTrue(); + } + } + + // This test is based on the testIntIndexIntValue() test in ArrayFormulaManagerTest + @Test + public void getArrayProofTest() throws InterruptedException, SolverException { + requireProofGeneration(); + requireIntegers(); + requireArrays(); + + // (arr2 = store(arr1, 4, 2)) & !(select(arr2, 4) = 2) + ArrayFormulaType type = + FormulaType.getArrayType(IntegerType, IntegerType); + IntegerFormula num2 = imgr.makeNumber(2); + IntegerFormula num4 = imgr.makeNumber(4); + ArrayFormula arr1 = amgr.makeArray("arr1", type); + ArrayFormula arr2 = amgr.makeArray("arr2", type); + BooleanFormula query = + bmgr.and( + amgr.equivalence(arr2, amgr.store(arr1, num4, num2)), + bmgr.not(imgr.equal(num2, amgr.select(arr2, num4)))); + + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_PROOFS)) { + prover.addConstraint(query); + assertThat(prover.isUnsat()).isTrue(); + + // Test getProof() + Proof proof = prover.getProof(); + assertThat(proof).isNotNull(); + + // Test getRule() + assertThat(proof.getRule()).isNotNull(); + assertThat(proof.getRule()).isInstanceOf(ProofRule.class); + + // Test getFormula(), the root should always be false + if (solverToUse().equals(SMTINTERPOL)) { + assertThat(proof.getFormula()).isNull(); + } else { + assertThat(proof.getFormula()).isEqualTo(bmgr.makeFalse()); + } + + // Test getArguments() + assertThat(proof.getChildren()).isNotNull(); + assertThat(proof.getChildren()).isNotEmpty(); + + // Test isLeaf() + assertThat(proof.isLeaf()).isFalse(); + Proof leaf = findanyProofLeaf(proof); + assertThat(leaf).isNotNull(); + assertThat(leaf.isLeaf()).isTrue(); + } + } + + private Proof findanyProofLeaf(Proof pn) { + if (pn.isLeaf()) { + return pn; + } + return findanyProofLeaf(pn.getChildren().stream().findFirst().get()); + } } diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index e96c7b39f1..65d14d6eec 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -129,6 +129,9 @@ protected ConfigurationBuilder createTestConfigBuilder() { if (solverToUse() == Solvers.OPENSMT) { newConfig.setOption("solver.opensmt.logic", logicToUse().toString()); } + if (solverToUse() == Solvers.Z3) { + newConfig.setOption("solver.z3.requireProofs", "true"); + } return newConfig; } @@ -386,6 +389,14 @@ protected void requireUserPropagators() { .isEqualTo(Solvers.Z3); } + protected void requireProofGeneration() { + assume() + .withMessage( + "Current version of solver %s does not support proof generation", solverToUse()) + .that(solverToUse()) + .isNoneOf(Solvers.BOOLECTOR, Solvers.BITWUZLA, Solvers.YICES2, Solvers.CVC4); + } + /** * Use this for checking assertions about BooleanFormulas with Truth: * assertThatFormula(formula).is...(). diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java index a08232a24a..06cbcf3387 100644 --- a/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverThreadLocalityTest.java @@ -161,7 +161,8 @@ public void nonLocalProverTest() throws InterruptedException, ExecutionException // (Solver.java:1455) // at org.sosy_lab.java_smt.solvers.cvc5.CVC5AbstractProver.addConstraintImpl // (CVC5AbstractProver.java:114) - // at org.sosy_lab.java_smt.basicimpl.AbstractProver.addConstraint + // at + // org.sosy_lab.java_smt.basicimpl.AbstractProofDag.AbstractProver.addConstraint // (AbstractProver.java:108) // at .. prover.push(formula); @@ -284,7 +285,7 @@ public void nonLocalInterpolationTest() throws InterruptedException, Executi // You tried to use push() on an CVC5 assertion stack illegally. // at org.sosy_lab.java_smt.solvers.cvc5.CVC5AbstractProver.pushImpl // (CVC5AbstractProver.java:89) - // at org.sosy_lab.java_smt.basicimpl.AbstractProver.push + // at org.sosy_lab.java_smt.basicimpl.AbstractProofDag.AbstractProver.push // (AbstractProver.java:88) // at .. prover.push(f2);