From a04226ef3519c4fdce7bd6c3ff92f18bf6bee83c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 23 Dec 2020 16:17:48 -0600 Subject: [PATCH] Add option to track and notify from CNF stream (#5708) This adds functionality to CNF stream to allow e.g. TheoryProxy to be notified when a formula is asserted (not just literals). This will be required for SAT relevancy. No behavior changes in this PR. --- src/prop/cnf_stream.cpp | 21 ++++++++++++-- src/prop/cnf_stream.h | 32 +++++++++++++++++++-- src/prop/minisat/core/Solver.cc | 4 +-- src/prop/minisat/core/Solver.h | 7 ++++- src/prop/prop_engine.cpp | 2 +- src/theory/bv/bitblast/eager_bitblaster.cpp | 3 +- src/theory/bv/bitblast/lazy_bitblaster.cpp | 2 +- src/theory/bv/bv_eager_solver.cpp | 1 + src/theory/bv/theory_bv.cpp | 2 +- 9 files changed, 61 insertions(+), 13 deletions(-) diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index e5b778365..6a4990c2b 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -46,14 +46,15 @@ CnfStream::CnfStream(SatSolver* satSolver, context::Context* context, OutputManager* outMgr, ResourceManager* rm, - bool fullLitToNodeMap, + FormulaLitPolicy flpol, std::string name) : d_satSolver(satSolver), d_outMgr(outMgr), d_booleanVariables(context), + d_notifyFormulas(context), d_nodeToLiteralMap(context), d_literalToNodeMap(context), - d_fullLitToNodeMap(fullLitToNodeMap), + d_flitPolicy(flpol), d_registrar(registrar), d_name(name), d_cnfProof(nullptr), @@ -203,6 +204,13 @@ SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister << push; Assert(node.getKind() != kind::NOT); + // if we are tracking formulas, everything is a theory atom + if (!isTheoryAtom && d_flitPolicy == FormulaLitPolicy::TRACK_AND_NOTIFY) + { + isTheoryAtom = true; + d_notifyFormulas.insert(node); + } + // Get the literal for this node SatLiteral lit; if (!hasLiteral(node)) { @@ -226,7 +234,9 @@ SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister } // If it's a theory literal, need to store it for back queries - if ( isTheoryAtom || d_fullLitToNodeMap || (Dump.isOn("clauses")) ) { + if (isTheoryAtom || d_flitPolicy == FormulaLitPolicy::TRACK + || (Dump.isOn("clauses"))) + { d_literalToNodeMap.insert_safe(lit, node); d_literalToNodeMap.insert_safe(~lit, node.notNode()); } @@ -268,6 +278,11 @@ void CnfStream::getBooleanVariables(std::vector& outputVariables) const { } } +bool CnfStream::isNotifyFormula(TNode node) const +{ + return d_notifyFormulas.find(node) != d_notifyFormulas.end(); +} + void CnfStream::setProof(CnfProof* proof) { Assert(d_cnfProof == NULL); d_cnfProof = proof; diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index e92532f08..90ed1b9cd 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -25,6 +25,7 @@ #ifndef CVC4__PROP__CNF_STREAM_H #define CVC4__PROP__CNF_STREAM_H +#include "context/cdhashset.h" #include "context/cdinsert_hashmap.h" #include "context/cdlist.h" #include "expr/node.h" @@ -41,6 +42,17 @@ namespace prop { class ProofCnfStream; +/** A policy for how literals for formulas are handled in cnf_stream */ +enum class FormulaLitPolicy : uint32_t +{ + // literals for formulas are notified + TRACK_AND_NOTIFY, + // literals for formulas are added to node map + TRACK, + // literals for formulas are kept internal (default) + INTERNAL, +}; + /** * Implements the following recursive algorithm * http://people.inf.ethz.ch/daniekro/classes/251-0247-00/f2007/readings/Tseitin70.pdf @@ -74,7 +86,8 @@ class CnfStream { * @param outMgr Reference to the output manager of the smt engine. Assertions * will not be dumped if outMgr == nullptr. * @param rm the resource manager of the CNF stream - * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping. + * @param flpol policy for literals corresponding to formulas (those that are + * not-theory literals). * @param name string identifier to distinguish between different instances * even for non-theory literals. */ @@ -83,7 +96,7 @@ class CnfStream { context::Context* context, OutputManager* outMgr, ResourceManager* rm, - bool fullLitToNodeMap = false, + FormulaLitPolicy flpol = FormulaLitPolicy::INTERNAL, std::string name = ""); /** * Convert a given formula to CNF and assert it to the SAT solver. @@ -133,6 +146,16 @@ class CnfStream { */ void getBooleanVariables(std::vector& outputVariables) const; + /** + * For SAT/theory relevancy. Returns true if node is a "notify formula". + * Returns true if node is formula that we are being notified about that + * is not a theory atom. + * + * Note this is only ever true when the policy passed to this class is + * FormulaLitPolicy::TRACK_AND_NOTIFY. + */ + bool isNotifyFormula(TNode node) const; + /** Retrieves map from nodes to literals. */ const CnfStream::NodeToLiteralMap& getTranslationCache() const; @@ -189,6 +212,9 @@ class CnfStream { /** Boolean variables that we translated */ context::CDList d_booleanVariables; + /** Formulas that we translated that we are notifying */ + context::CDHashSet d_notifyFormulas; + /** Map from nodes to literals */ NodeToLiteralMap d_nodeToLiteralMap; @@ -200,7 +226,7 @@ class CnfStream { * theory lits. This is true if e.g. replay logging is on, which * dumps the Nodes corresponding to decision literals. */ - const bool d_fullLitToNodeMap; + const FormulaLitPolicy d_flitPolicy; /** The "registrar" for pre-registration of terms */ Registrar* d_registrar; diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index ca29e604f..12246be41 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -274,7 +274,8 @@ Var Solver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister, bo polarity .push(sign); decision .push(); trail .capacity(v+1); - theory .push(isTheoryAtom); + // push whether it corresponds to a theory atom + theory.push(isTheoryAtom); setDecisionVar(v, dvar); @@ -306,7 +307,6 @@ void Solver::resizeVars(int newSize) { polarity.shrink(shrinkSize); decision.shrink(shrinkSize); theory.shrink(shrinkSize); - } if (Debug.isOn("minisat::pop")) { diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 00d68cf80..8fa489f65 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -390,7 +390,12 @@ protected: ClauseAllocator ca; // CVC4 Stuff - vec theory; // Is the variable representing a theory atom + /** + * A vector determining whether each variable represents a theory atom. + * More generally, this value is true for any literal that the theory proxy + * should be notified about when asserted. + */ + vec theory; enum TheoryCheckType { // Quick check, but don't perform theory reasoning diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 8352373c5..eeb879a2b 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -94,7 +94,7 @@ PropEngine::PropEngine(TheoryEngine* te, d_registrar = new theory::TheoryRegistrar(d_theoryEngine); d_cnfStream = new CVC4::prop::CnfStream( - d_satSolver, d_registrar, userContext, &d_outMgr, rm, true); + d_satSolver, d_registrar, userContext, &d_outMgr, rm, FormulaLitPolicy::TRACK); d_theoryProxy = new TheoryProxy(this, d_theoryEngine, diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp index 046ad4b1b..44db8a3cd 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.cpp +++ b/src/theory/bv/bitblast/eager_bitblaster.cpp @@ -18,6 +18,7 @@ #include "cvc4_private.h" #include "options/bv_options.h" +#include "options/smt_options.h" #include "prop/cnf_stream.h" #include "prop/sat_solver_factory.h" #include "smt/smt_engine.h" @@ -74,7 +75,7 @@ EagerBitblaster::EagerBitblaster(BVSolverLazy* theory_bv, context::Context* c) d_nullContext.get(), nullptr, rm, - false, + prop::FormulaLitPolicy::INTERNAL, "EagerBitblaster")); } diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp index 95d78c69b..7f38c61a2 100644 --- a/src/theory/bv/bitblast/lazy_bitblaster.cpp +++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp @@ -85,7 +85,7 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, d_nullContext.get(), nullptr, rm, - false, + prop::FormulaLitPolicy::INTERNAL, "LazyBitblaster")); d_satSolverNotify.reset( diff --git a/src/theory/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp index 44dc9555f..dbdb350b7 100644 --- a/src/theory/bv/bv_eager_solver.cpp +++ b/src/theory/bv/bv_eager_solver.cpp @@ -17,6 +17,7 @@ #include "theory/bv/bv_eager_solver.h" #include "options/bv_options.h" +#include "options/smt_options.h" #include "theory/bv/bitblast/aig_bitblaster.h" #include "theory/bv/bitblast/eager_bitblaster.h" diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 6f22d4520..227df458a 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -16,6 +16,7 @@ #include "theory/bv/theory_bv.h" #include "options/bv_options.h" +#include "options/smt_options.h" #include "theory/bv/bv_solver_lazy.h" #include "theory/bv/bv_solver_simple.h" #include "theory/bv/theory_bv_utils.h" @@ -129,7 +130,6 @@ TrustNode TheoryBV::expandDefinition(Node node) case kind::BITVECTOR_UREM: { NodeManager* nm = NodeManager::currentNM(); - unsigned width = node.getType().getBitVectorSize(); Kind kind = node.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL -- 2.30.2