summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/expr/proof_node.h3
-rw-r--r--src/theory/arith/theory_arith.cpp14
-rw-r--r--src/theory/arith/theory_arith.h4
-rw-r--r--src/theory/arith/theory_arith_private.cpp121
-rw-r--r--src/theory/arith/theory_arith_private.h8
-rw-r--r--src/theory/eager_proof_generator.cpp12
-rw-r--r--src/theory/eager_proof_generator.h11
-rw-r--r--src/theory/theory.cpp5
-rw-r--r--src/theory/theory.h7
9 files changed, 154 insertions, 31 deletions
diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h
index 0c36deada..a505b1bc0 100644
--- a/src/expr/proof_node.h
+++ b/src/expr/proof_node.h
@@ -27,6 +27,9 @@ namespace CVC4 {
class ProofNodeManager;
class ProofNode;
+// Alias for shared pointer to a proof node
+using Pf = std::shared_ptr<ProofNode>;
+
struct ProofNodeHashFunction
{
inline size_t operator()(std::shared_ptr<ProofNode> pfn) const;
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 7437ce223..6de5c7221 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -17,6 +17,7 @@
#include "theory/arith/theory_arith.h"
+#include "expr/proof_rule.h"
#include "options/smt_options.h"
#include "smt/smt_statistics_registry.h"
#include "theory/arith/arith_rewriter.h"
@@ -42,6 +43,7 @@ TheoryArith::TheoryArith(context::Context* c,
d_internal(
new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo, pnm)),
d_ppRewriteTimer("theory::arith::ppRewriteTimer"),
+ d_ppPfGen(pnm, c, "Arith::ppRewrite"),
d_astate(*d_internal, c, u, valuation),
d_inferenceManager(*this, d_astate, pnm),
d_nonlinearExtension(nullptr),
@@ -131,7 +133,17 @@ TrustNode TheoryArith::ppRewrite(TNode atom)
Debug("arith::preprocess")
<< "arith::preprocess() : returning " << rewritten << endl;
// don't need to rewrite terms since rewritten is not a non-standard op
- return TrustNode::mkTrustRewrite(atom, rewritten, nullptr);
+ if (proofsEnabled())
+ {
+ return d_ppPfGen.mkTrustedRewrite(
+ atom,
+ rewritten,
+ d_pnm->mkNode(PfRule::INT_TRUST, {}, {atom.eqNode(rewritten)}));
+ }
+ else
+ {
+ return TrustNode::mkTrustRewrite(atom, rewritten, nullptr);
+ }
}
}
return ppRewriteTerms(atom);
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index e26ff51ef..eba84e339 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -45,6 +45,9 @@ class TheoryArith : public Theory {
TimerStat d_ppRewriteTimer;
+ /** Used to prove pp-rewrites */
+ EagerProofGenerator d_ppPfGen;
+
public:
TheoryArith(context::Context* c,
context::UserContext* u,
@@ -152,6 +155,7 @@ class TheoryArith : public Theory {
ArithPreprocess d_arithPreproc;
/** The theory rewriter for this theory. */
ArithRewriter d_rewriter;
+
};/* class TheoryArith */
}/* CVC4::theory::arith namespace */
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 7b0096f30..58e874158 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -34,6 +34,7 @@
#include "expr/node_builder.h"
#include "expr/proof_generator.h"
#include "expr/proof_node_manager.h"
+#include "expr/proof_rule.h"
#include "expr/skolem_manager.h"
#include "options/arith_options.h"
#include "options/smt_options.h" // for incrementalSolving()
@@ -3033,11 +3034,11 @@ bool TheoryArithPrivate::solveRelaxationOrPanic(Theory::Effort effortLevel){
ArithVar canBranch = nextIntegerViolatation(false);
if(canBranch != ARITHVAR_SENTINEL){
++d_statistics.d_panicBranches;
- Node branch = branchIntegerVariable(canBranch);
- Assert(branch.getKind() == kind::OR);
- Node rwbranch = Rewriter::rewrite(branch[0]);
+ TrustNode branch = branchIntegerVariable(canBranch);
+ Assert(branch.getNode().getKind() == kind::OR);
+ Node rwbranch = Rewriter::rewrite(branch.getNode()[0]);
if(!isSatLiteral(rwbranch)){
- d_approxCuts.push_back(branch);
+ d_approxCuts.push_back(branch.getNode());
return true;
}
}
@@ -3619,15 +3620,15 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
}
if(!emmittedConflictOrSplit) {
- Node possibleLemma = roundRobinBranch();
- if(!possibleLemma.isNull()){
+ TrustNode possibleLemma = roundRobinBranch();
+ if (!possibleLemma.getNode().isNull())
+ {
++(d_statistics.d_externalBranchAndBounds);
d_cutCount = d_cutCount + 1;
emmittedConflictOrSplit = true;
Debug("arith::lemma") << "rrbranch lemma"
<< possibleLemma << endl;
- outputLemma(possibleLemma);
-
+ outputTrustedLemma(possibleLemma);
}
}
@@ -3662,7 +3663,8 @@ bool TheoryArithPrivate::postCheck(Theory::Effort effortLevel)
bool TheoryArithPrivate::foundNonlinear() const { return d_foundNl; }
-Node TheoryArithPrivate::branchIntegerVariable(ArithVar x) const {
+TrustNode TheoryArithPrivate::branchIntegerVariable(ArithVar x) const
+{
const DeltaRational& d = d_partialModel.getAssignment(x);
Assert(!d.isIntegral());
const Rational& r = d.getNoninfinitesimalPart();
@@ -3674,7 +3676,7 @@ Node TheoryArithPrivate::branchIntegerVariable(ArithVar x) const {
TNode var = d_partialModel.asNode(x);
Integer floor_d = d.floor();
- Node lem;
+ TrustNode lem = TrustNode::null();
NodeManager* nm = NodeManager::currentNM();
if (options::brabTest())
{
@@ -3691,38 +3693,102 @@ Node TheoryArithPrivate::branchIntegerVariable(ArithVar x) const {
nm->mkNode(kind::LEQ, var, mkRationalNode(nearest - 1)));
Node lb = Rewriter::rewrite(
nm->mkNode(kind::GEQ, var, mkRationalNode(nearest + 1)));
- lem = nm->mkNode(kind::OR, ub, lb);
- Node eq = Rewriter::rewrite(
- nm->mkNode(kind::EQUAL, var, mkRationalNode(nearest)));
+ Node right = nm->mkNode(kind::OR, ub, lb);
+ Node rawEq = nm->mkNode(kind::EQUAL, var, mkRationalNode(nearest));
+ Node eq = Rewriter::rewrite(rawEq);
// Also preprocess it before we send it out. This is important since
// arithmetic may prefer eliminating equalities.
+ TrustNode teq;
if (Theory::theoryOf(eq) == THEORY_ARITH)
{
- TrustNode teq = d_containing.ppRewrite(eq);
+ teq = d_containing.ppRewrite(eq);
eq = teq.isNull() ? eq : teq.getNode();
}
Node literal = d_containing.getValuation().ensureLiteral(eq);
+ Trace("integers") << "eq: " << eq << "\nto: " << literal << endl;
d_containing.getOutputChannel().requirePhase(literal, true);
- lem = nm->mkNode(kind::OR, literal, lem);
+ Node l = nm->mkNode(kind::OR, literal, right);
+ Trace("integers") << "l: " << l << endl;
+ if (proofsEnabled())
+ {
+ Node less = nm->mkNode(kind::LT, var, mkRationalNode(nearest));
+ Node greater = nm->mkNode(kind::GT, var, mkRationalNode(nearest));
+ // TODO (project #37): justify. Thread proofs through *ensureLiteral*.
+ Debug("integers::pf") << "less: " << less << endl;
+ Debug("integers::pf") << "greater: " << greater << endl;
+ Debug("integers::pf") << "literal: " << literal << endl;
+ Debug("integers::pf") << "eq: " << eq << endl;
+ Debug("integers::pf") << "rawEq: " << rawEq << endl;
+ Pf pfNotLit = d_pnm->mkAssume(literal.negate());
+ // rewrite notLiteral to notRawEq, using teq.
+ Pf pfNotRawEq =
+ literal == rawEq
+ ? pfNotLit
+ : d_pnm->mkNode(
+ PfRule::MACRO_SR_PRED_TRANSFORM,
+ {pfNotLit, teq.getGenerator()->getProofFor(teq.getProven())},
+ {rawEq.negate()});
+ Pf pfBot =
+ d_pnm->mkNode(PfRule::CONTRA,
+ {d_pnm->mkNode(PfRule::ARITH_TRICHOTOMY,
+ {d_pnm->mkAssume(less.negate()), pfNotRawEq},
+ {greater}),
+ d_pnm->mkAssume(greater.negate())},
+ {});
+ std::vector<Node> assumptions = {
+ literal.negate(), less.negate(), greater.negate()};
+ // Proof of (not (and (not (= v i)) (not (< v i)) (not (> v i))))
+ Pf pfNotAnd = d_pnm->mkScope(pfBot, assumptions);
+ Pf pfL = d_pnm->mkNode(PfRule::MACRO_SR_PRED_TRANSFORM,
+ {d_pnm->mkNode(PfRule::NOT_AND, {pfNotAnd}, {})},
+ {l});
+ lem = d_pfGen->mkTrustNode(l, pfL);
+ }
+ else
+ {
+ lem = TrustNode::mkTrustLemma(l, nullptr);
+ }
}
else
{
Node ub =
Rewriter::rewrite(nm->mkNode(kind::LEQ, var, mkRationalNode(floor_d)));
Node lb = ub.notNode();
- lem = nm->mkNode(kind::OR, ub, lb);
+ if (proofsEnabled())
+ {
+ lem = d_pfGen->mkTrustNode(
+ nm->mkNode(kind::OR, ub, lb), PfRule::SPLIT, {}, {ub});
+ }
+ else
+ {
+ lem = TrustNode::mkTrustLemma(nm->mkNode(kind::OR, ub, lb), nullptr);
+ }
}
Trace("integers") << "integers: branch & bound: " << lem << endl;
- if(isSatLiteral(lem[0])) {
- Debug("integers") << " " << lem[0] << " == " << getSatValue(lem[0]) << endl;
- } else {
- Debug("integers") << " " << lem[0] << " is not assigned a SAT literal" << endl;
- }
- if(isSatLiteral(lem[1])) {
- Debug("integers") << " " << lem[1] << " == " << getSatValue(lem[1]) << endl;
- } else {
- Debug("integers") << " " << lem[1] << " is not assigned a SAT literal" << endl;
+ if (Debug.isOn("integers"))
+ {
+ Node l = lem.getNode();
+ if (isSatLiteral(l[0]))
+ {
+ Debug("integers") << " " << l[0] << " == " << getSatValue(l[0])
+ << endl;
+ }
+ else
+ {
+ Debug("integers") << " " << l[0] << " is not assigned a SAT literal"
+ << endl;
+ }
+ if (isSatLiteral(l[1]))
+ {
+ Debug("integers") << " " << l[1] << " == " << getSatValue(l[1])
+ << endl;
+ }
+ else
+ {
+ Debug("integers") << " " << l[1] << " is not assigned a SAT literal"
+ << endl;
+ }
}
return lem;
}
@@ -3748,9 +3814,10 @@ std::vector<ArithVar> TheoryArithPrivate::cutAllBounded() const{
}
/** Returns true if the roundRobinBranching() issues a lemma. */
-Node TheoryArithPrivate::roundRobinBranch(){
+TrustNode TheoryArithPrivate::roundRobinBranch()
+{
if(hasIntegerModel()){
- return Node::null();
+ return TrustNode::null();
}else{
ArithVar v = d_nextIntegerCheckVar;
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 31435221f..e7f5d82b2 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -552,9 +552,11 @@ private:
* Returns a cut for a lemma.
* If there is an integer model, this returns Node::null().
*/
- Node roundRobinBranch();
+ TrustNode roundRobinBranch();
-public:
+ bool proofsEnabled() const { return d_pnm; }
+
+ public:
/**
* This requests a new unique ArithVar value for x.
* This also does initial (not context dependent) set up for a variable,
@@ -709,7 +711,7 @@ private:
/** Counts the number of fullCheck calls to arithmetic. */
uint32_t d_fullCheckCounter;
std::vector<ArithVar> cutAllBounded() const;
- Node branchIntegerVariable(ArithVar x) const;
+ TrustNode branchIntegerVariable(ArithVar x) const;
void branchVector(const std::vector<ArithVar>& lemmas);
context::CDO<unsigned> d_cutCount;
diff --git a/src/theory/eager_proof_generator.cpp b/src/theory/eager_proof_generator.cpp
index c49c33790..a1c78fc7d 100644
--- a/src/theory/eager_proof_generator.cpp
+++ b/src/theory/eager_proof_generator.cpp
@@ -120,6 +120,18 @@ TrustNode EagerProofGenerator::mkTrustNode(Node conc,
return mkTrustNode(pfs->getResult(), pfs, isConflict);
}
+TrustNode EagerProofGenerator::mkTrustedRewrite(
+ Node a, Node b, std::shared_ptr<ProofNode> pf)
+{
+ if (pf == nullptr)
+ {
+ return TrustNode::null();
+ }
+ Node eq = a.eqNode(b);
+ setProofFor(eq, pf);
+ return TrustNode::mkTrustRewrite(a, b, this);
+}
+
TrustNode EagerProofGenerator::mkTrustedPropagation(
Node n, Node exp, std::shared_ptr<ProofNode> pf)
{
diff --git a/src/theory/eager_proof_generator.h b/src/theory/eager_proof_generator.h
index 29f916e00..4b94228c5 100644
--- a/src/theory/eager_proof_generator.h
+++ b/src/theory/eager_proof_generator.h
@@ -146,6 +146,17 @@ class EagerProofGenerator : public ProofGenerator
TrustNode mkTrustedPropagation(Node n,
Node exp,
std::shared_ptr<ProofNode> pf);
+ /**
+ * Make trust node: `a = b` as a Rewrite trust node
+ *
+ * @param a the original
+ * @param b what is rewrites to
+ * @param pf The proof of a = b,
+ * @return The trust node corresponding to the fact that this generator has
+ * a proof of a = b
+ */
+ TrustNode mkTrustedRewrite(
+ Node a, Node b, std::shared_ptr<ProofNode> pf);
//--------------------------------------- common proofs
/**
* This returns the trust node corresponding to the splitting lemma
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 9ab20e6cb..5bea454e8 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -424,6 +424,11 @@ void Theory::getCareGraph(CareGraph* careGraph) {
d_careGraph = NULL;
}
+bool Theory::proofsEnabled() const
+{
+ return d_pnm != nullptr;
+}
+
EqualityStatus Theory::getEqualityStatus(TNode a, TNode b)
{
// if not using an equality engine, then by default we don't know the status
diff --git a/src/theory/theory.h b/src/theory/theory.h
index a9783c19c..0eb3d9a33 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -238,6 +238,13 @@ class Theory {
ProofNodeManager* d_pnm;
/**
+ * Are proofs enabled?
+ *
+ * They are considered enabled if the ProofNodeManager is non-null.
+ */
+ bool proofsEnabled() const;
+
+ /**
* Returns the next assertion in the assertFact() queue.
*
* @return the next assertion in the assertFact() queue
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback