summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/arith/congruence_manager.cpp22
-rw-r--r--src/theory/arith/congruence_manager.h55
-rw-r--r--src/theory/arith/constraint.cpp32
-rw-r--r--src/theory/arith/constraint.h20
-rw-r--r--src/theory/arith/theory_arith.cpp4
-rw-r--r--src/theory/arith/theory_arith.h2
-rw-r--r--src/theory/arith/theory_arith_private.cpp27
-rw-r--r--src/theory/arith/theory_arith_private.h15
8 files changed, 147 insertions, 30 deletions
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 361b47c65..520903562 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -29,10 +29,12 @@ namespace arith {
ArithCongruenceManager::ArithCongruenceManager(
context::Context* c,
+ context::UserContext* u,
ConstraintDatabase& cd,
SetupLiteralCallBack setup,
const ArithVariables& avars,
- RaiseEqualityEngineConflict raiseConflict)
+ RaiseEqualityEngineConflict raiseConflict,
+ ProofNodeManager* pnm)
: d_inConflict(c),
d_raiseConflict(raiseConflict),
d_notify(*this),
@@ -42,7 +44,15 @@ ArithCongruenceManager::ArithCongruenceManager(
d_constraintDatabase(cd),
d_setupLiteral(setup),
d_avariables(avars),
- d_ee(nullptr)
+ d_ee(nullptr),
+ d_satContext(c),
+ d_userContext(u),
+ d_pnm(pnm),
+ d_pfGenEe(
+ new EagerProofGenerator(pnm, c, "ArithCongruenceManager::pfGenEe")),
+ d_pfGenExplain(new EagerProofGenerator(
+ pnm, u, "ArithCongruenceManager::pfGenExplain")),
+ d_pfee(nullptr)
{
}
@@ -55,7 +65,8 @@ bool ArithCongruenceManager::needsEqualityEngine(EeSetupInfo& esi)
return true;
}
-void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee)
+void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee,
+ eq::ProofEqEngine* pfee)
{
Assert(ee != nullptr);
d_ee = ee;
@@ -63,6 +74,9 @@ void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee)
d_ee->addFunctionKind(kind::EXPONENTIAL);
d_ee->addFunctionKind(kind::SINE);
d_ee->addFunctionKind(kind::IAND);
+ // have proof equality engine only if proofs are enabled
+ Assert(isProofEnabled() == (pfee != nullptr));
+ d_pfee = pfee;
}
ArithCongruenceManager::Statistics::Statistics():
@@ -458,6 +472,8 @@ void ArithCongruenceManager::addSharedTerm(Node x){
d_ee->addTriggerTerm(x, THEORY_ARITH);
}
+bool ArithCongruenceManager::isProofEnabled() const { return d_pnm != nullptr; }
+
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 77d4455ca..3565d86b5 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -24,11 +24,15 @@
#include "context/cdo.h"
#include "context/cdtrail_queue.h"
#include "context/context.h"
+#include "expr/proof_node_manager.h"
#include "theory/arith/arithvar.h"
#include "theory/arith/constraint_forward.h"
#include "theory/arith/partial_model.h"
+#include "theory/eager_proof_generator.h"
#include "theory/ee_setup_info.h"
+#include "theory/trust_node.h"
#include "theory/uf/equality_engine.h"
+#include "theory/uf/proof_equality_engine.h"
#include "util/dense_map.h"
#include "util/statistics_registry.h"
@@ -96,10 +100,46 @@ private:
/** The equality engine being used by this class */
eq::EqualityEngine* d_ee;
+ /** The sat context */
+ context::Context* d_satContext;
+ /** The user context */
+ context::UserContext* d_userContext;
+
+ /** proof manager */
+ ProofNodeManager* d_pnm;
+ /** A proof generator for storing proofs of facts that are asserted to the EQ
+ * engine. Note that these proofs **are not closed**, and assume the
+ * explanation of these facts. This is why this generator is separate from the
+ * TheoryArithPrivate generator, which stores closed proofs.
+ */
+ std::unique_ptr<EagerProofGenerator> d_pfGenEe;
+ /** A proof generator for TrustNodes sent to TheoryArithPrivate.
+ *
+ * When TheoryArithPrivate requests an explanation from
+ * ArithCongruenceManager, it can request a TrustNode for that explanation.
+ * This proof generator is the one used in that TrustNode: it stores the
+ * (closed) proofs of implications proved by the
+ * ArithCongruenceManager/EqualityEngine.
+ *
+ * It is insufficient to just use the ProofGenerator from the ProofEqEngine,
+ * since sometimes the ArithCongruenceManager needs to add some
+ * arith-specific reasoning to extend the proof (e.g. rewriting the result
+ * into a normal form).
+ * */
+ std::unique_ptr<EagerProofGenerator> d_pfGenExplain;
+
+ /** Pointer to the proof equality engine of TheoryArith */
+ theory::eq::ProofEqEngine* d_pfee;
+
void raiseConflict(Node conflict);
-public:
+ /**
+ * Are proofs enabled? This is true if a non-null proof manager was provided
+ * to the constructor of this class.
+ */
+ bool isProofEnabled() const;
+ public:
bool inConflict() const;
bool hasMorePropagations() const;
@@ -133,7 +173,14 @@ private:
Node explainInternal(TNode internal);
public:
- ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, SetupLiteralCallBack, const ArithVariables&, RaiseEqualityEngineConflict raiseConflict);
+ public:
+ ArithCongruenceManager(context::Context* satContext,
+ context::UserContext* u,
+ ConstraintDatabase&,
+ SetupLiteralCallBack,
+ const ArithVariables&,
+ RaiseEqualityEngineConflict raiseConflict,
+ ProofNodeManager* pnm);
~ArithCongruenceManager();
//--------------------------------- initialization
@@ -144,9 +191,9 @@ public:
bool needsEqualityEngine(EeSetupInfo& esi);
/**
* Finish initialize. This class is instructed by TheoryArithPrivate to use
- * the equality engine ee.
+ * the equality engine ee and proof equality engine pfee.
*/
- void finishInit(eq::EqualityEngine* ee);
+ void finishInit(eq::EqualityEngine* ee, eq::ProofEqEngine* pfee);
//--------------------------------- end initialization
Node explain(TNode literal);
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 98427950b..06ecb9618 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -847,17 +847,25 @@ ConstraintP Constraint::makeNegation(ArithVar v, ConstraintType t, const DeltaRa
}
}
-ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Context* userContext, const ArithVariables& avars, ArithCongruenceManager& cm, RaiseConflict raiseConflict)
- : d_varDatabases()
- , d_toPropagate(satContext)
- , d_antecedents(satContext, false)
- , d_watches(new Watches(satContext, userContext))
- , d_avariables(avars)
- , d_congruenceManager(cm)
- , d_satContext(satContext)
- , d_raiseConflict(raiseConflict)
- , d_one(1)
- , d_negOne(-1)
+ConstraintDatabase::ConstraintDatabase(context::Context* satContext,
+ context::Context* userContext,
+ const ArithVariables& avars,
+ ArithCongruenceManager& cm,
+ RaiseConflict raiseConflict,
+ EagerProofGenerator* pfGen,
+ ProofNodeManager* pnm)
+ : d_varDatabases(),
+ d_toPropagate(satContext),
+ d_antecedents(satContext, false),
+ d_watches(new Watches(satContext, userContext)),
+ d_avariables(avars),
+ d_congruenceManager(cm),
+ d_satContext(satContext),
+ d_pfGen(pfGen),
+ d_pnm(pnm),
+ d_raiseConflict(raiseConflict),
+ d_one(1),
+ d_negOne(-1)
{
}
@@ -1722,6 +1730,8 @@ ConstraintDatabase::Watches::Watches(context::Context* satContext, context::Cont
void Constraint::setLiteral(Node n) {
+ Debug("arith::constraint") << "Mapping " << *this << " to " << n << std::endl;
+ Assert(Comparison::isNormalAtom(n));
Assert(!hasLiteral());
Assert(sanityChecking(n));
d_literal = n;
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index eb2d89de7..0afc0bc2f 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -85,6 +85,7 @@
#include "context/cdqueue.h"
#include "context/context.h"
#include "expr/node.h"
+#include "expr/proof_node_manager.h"
#include "theory/arith/arithvar.h"
#include "theory/arith/callbacks.h"
#include "theory/arith/congruence_manager.h"
@@ -1086,6 +1087,10 @@ private:
ArithCongruenceManager& d_congruenceManager;
const context::Context * const d_satContext;
+ /** Owned by the TheoryArithPrivate, used here. */
+ EagerProofGenerator* d_pfGen;
+ /** Owned by the TheoryArithPrivate, used here. */
+ ProofNodeManager* d_pnm;
RaiseConflict d_raiseConflict;
@@ -1095,13 +1100,14 @@ private:
friend class Constraint;
-public:
-
- ConstraintDatabase( context::Context* satContext,
- context::Context* userContext,
- const ArithVariables& variables,
- ArithCongruenceManager& dm,
- RaiseConflict conflictCallBack);
+ public:
+ ConstraintDatabase(context::Context* satContext,
+ context::Context* userContext,
+ const ArithVariables& variables,
+ ArithCongruenceManager& dm,
+ RaiseConflict conflictCallBack,
+ EagerProofGenerator* pfGen,
+ ProofNodeManager* pnm);
~ConstraintDatabase();
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 9324c94af..f16e0a297 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -205,6 +205,10 @@ std::pair<bool, Node> TheoryArith::entailmentCheck(TNode lit)
std::pair<bool, Node> res = d_internal->entailmentCheck(lit, def, ase);
return res;
}
+eq::ProofEqEngine* TheoryArith::getProofEqEngine()
+{
+ return d_inferenceManager.getProofEqEngine();
+}
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 25d3b1e45..e332646ff 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -112,6 +112,8 @@ class TheoryArith : public Theory {
}
private:
+ /** Get the proof equality engine */
+ eq::ProofEqEngine* getProofEqEngine();
/** The state object wrapping TheoryArithPrivate */
ArithState d_astate;
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 74c35ff13..dfc51a6da 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -34,6 +34,8 @@
#include "expr/node.h"
#include "expr/node_algorithm.h"
#include "expr/node_builder.h"
+#include "expr/proof_generator.h"
+#include "expr/proof_node_manager.h"
#include "expr/skolem_manager.h"
#include "options/arith_options.h"
#include "options/smt_options.h" // for incrementalSolving()
@@ -92,8 +94,16 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
: d_containing(containing),
d_nlIncomplete(false),
d_rowTracking(),
- d_constraintDatabase(
- c, u, d_partialModel, d_congruenceManager, RaiseConflict(*this)),
+ d_pnm(pnm),
+ d_checker(),
+ d_pfGen(new EagerProofGenerator(d_pnm, u)),
+ d_constraintDatabase(c,
+ u,
+ d_partialModel,
+ d_congruenceManager,
+ RaiseConflict(*this),
+ d_pfGen.get(),
+ d_pnm),
d_qflraStatus(Result::SAT_UNKNOWN),
d_unknownsInARow(0),
d_hasDoneWorkSinceCut(false),
@@ -119,11 +129,14 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
d_tableauResetPeriod(10),
d_conflicts(c),
d_blackBoxConflict(c, Node::null()),
+ d_blackBoxConflictPf(c, std::shared_ptr<ProofNode>(nullptr)),
d_congruenceManager(c,
+ u,
d_constraintDatabase,
SetupLiteralCallBack(*this),
d_partialModel,
- RaiseEqualityEngineConflict(*this)),
+ RaiseEqualityEngineConflict(*this),
+ d_pnm),
d_cmEnabled(c, true),
d_dualSimplex(
@@ -159,6 +172,11 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing,
d_statistics(),
d_opElim(pnm, logicInfo)
{
+ ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
+ if (pc != nullptr)
+ {
+ d_checker.registerTo(pc);
+ }
}
TheoryArithPrivate::~TheoryArithPrivate(){
@@ -174,8 +192,9 @@ bool TheoryArithPrivate::needsEqualityEngine(EeSetupInfo& esi)
void TheoryArithPrivate::finishInit()
{
eq::EqualityEngine* ee = d_containing.getEqualityEngine();
+ eq::ProofEqEngine* pfee = d_containing.getProofEqEngine();
Assert(ee != nullptr);
- d_congruenceManager.finishInit(ee);
+ d_congruenceManager.finishInit(ee, pfee);
d_nonlinearExtension = d_containing.d_nonlinearExtension.get();
}
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 298c989f4..6f6ca7fdf 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -31,6 +31,7 @@
#include "expr/metakind.h"
#include "expr/node.h"
#include "expr/node_builder.h"
+#include "expr/proof_generator.h"
#include "options/arith_options.h"
#include "smt/logic_exception.h"
#include "smt_util/boolean_simplification.h"
@@ -51,10 +52,12 @@
#include "theory/arith/normal_form.h"
#include "theory/arith/operator_elim.h"
#include "theory/arith/partial_model.h"
+#include "theory/arith/proof_checker.h"
#include "theory/arith/simplex.h"
#include "theory/arith/soi_simplex.h"
#include "theory/arith/theory_arith.h"
#include "theory/arith/theory_arith_private_forward.h"
+#include "theory/eager_proof_generator.h"
#include "theory/rewriter.h"
#include "theory/theory_model.h"
#include "theory/valuation.h"
@@ -101,6 +104,14 @@ private:
BoundInfoMap d_rowTracking;
+ // For proofs
+ /** Manages the proof nodes of this theory. */
+ ProofNodeManager* d_pnm;
+ /** Checks the proof rules of this theory. */
+ ArithProofRuleChecker d_checker;
+ /** Stores proposition(node)/proof pairs. */
+ std::unique_ptr<EagerProofGenerator> d_pfGen;
+
/**
* The constraint database associated with the theory.
* This must be declared before ArithPartialModel.
@@ -306,8 +317,10 @@ private:
/** This is only used by simplex at the moment. */
context::CDO<Node> d_blackBoxConflict;
-public:
+ /** For holding the proof of the above conflict node. */
+ context::CDO<std::shared_ptr<ProofNode>> d_blackBoxConflictPf;
+ public:
/**
* This adds the constraint a to the queue of conflicts in d_conflicts.
* Both a and ~a must have a proof.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback