diff options
Diffstat (limited to 'src')
34 files changed, 714 insertions, 579 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index d03b8975e..d6c0a58ee 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -7381,6 +7381,36 @@ bool Solver::isModelCoreSymbol(const Term& v) const CVC5_API_TRY_CATCH_END; } +std::string Solver::getModel(const std::vector<Sort>& sorts, + const std::vector<Term>& vars) const +{ + CVC5_API_TRY_CATCH_BEGIN; + NodeManagerScope scope(getNodeManager()); + CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getOptions().smt.produceModels) + << "Cannot get model unless model generation is enabled " + "(try --produce-models)"; + CVC5_API_RECOVERABLE_CHECK(d_smtEngine->isSmtModeSat()) + << "Cannot get model unless after a SAT or unknown response."; + CVC5_API_SOLVER_CHECK_SORTS(sorts); + for (const Sort& s : sorts) + { + CVC5_API_RECOVERABLE_CHECK(s.isUninterpretedSort()) + << "Expecting an uninterpreted sort as argument to " + "getModel."; + } + CVC5_API_SOLVER_CHECK_TERMS(vars); + for (const Term& v : vars) + { + CVC5_API_RECOVERABLE_CHECK(v.getKind() == CONSTANT) + << "Expecting a free constant as argument to getModel."; + } + //////// all checks before this line + return d_smtEngine->getModel(Sort::sortVectorToTypeNodes(sorts), + Term::termVectorToNodes(vars)); + //////// + CVC5_API_TRY_CATCH_END; +} + Term Solver::getQuantifierElimination(const Term& q) const { NodeManagerScope scope(getNodeManager()); @@ -7900,12 +7930,6 @@ std::vector<Term> Solver::getSynthSolutions( CVC5_API_TRY_CATCH_END; } -/* - * !!! This is only temporarily available until the parser is fully migrated to - * the new API. !!! - */ -SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); } - Statistics Solver::getStatistics() const { return Statistics(d_smtEngine->getStatisticsRegistry()); diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 11b138a50..a221f3711 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -3951,6 +3951,22 @@ class CVC5_EXPORT Solver bool isModelCoreSymbol(const Term& v) const; /** + * Get the model + * SMT-LIB: + * \verbatim + * ( get-model ) + * \endverbatim + * Requires to enable option 'produce-models'. + * @param sorts The list of uninterpreted sorts that should be printed in the + * model. + * @param vars The list of free constants that should be printed in the + * model. A subset of these may be printed based on isModelCoreSymbol. + * @return a string representing the model. + */ + std::string getModel(const std::vector<Sort>& sorts, + const std::vector<Term>& vars) const; + + /** * Do quantifier elimination. * SMT-LIB: * \verbatim @@ -4329,10 +4345,6 @@ class CVC5_EXPORT Solver */ std::vector<Term> getSynthSolutions(const std::vector<Term>& terms) const; - // !!! This is only temporarily available until the parser is fully migrated - // to the new API. !!! - SmtEngine* getSmtEngine(void) const; - /** * Returns a snapshot of the current state of the statistic values of this * solver. The returned object is completely decoupled from the solver and diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 0a7a56e5b..1e8d848a4 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -27,10 +27,6 @@ namespace cvc5 { class Command; -namespace smt { -class SmtEngine; -} - namespace main { class CommandExecutor @@ -81,8 +77,6 @@ class CommandExecutor api::Result getResult() const { return d_result; } void reset(); - SmtEngine* getSmtEngine() const { return d_solver->getSmtEngine(); } - /** Store the current options as the original options */ void storeOptionsAsOriginal(); diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp index 3f6828a7b..7d1c5bf54 100644 --- a/src/preprocessing/passes/sort_infer.cpp +++ b/src/preprocessing/passes/sort_infer.cpp @@ -20,6 +20,7 @@ #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" #include "smt/dump_manager.h" +#include "smt/smt_engine.h" #include "theory/rewriter.h" #include "theory/sort_inference.h" #include "theory/theory_engine.h" diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp index e3cb13851..3b2a088a2 100644 --- a/src/preprocessing/preprocessing_pass.cpp +++ b/src/preprocessing/preprocessing_pass.cpp @@ -20,6 +20,7 @@ #include "printer/printer.h" #include "smt/dump.h" #include "smt/output_manager.h" +#include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "util/statistics_stats.h" diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index fe4c8784a..8a8bad20f 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -17,6 +17,7 @@ #include "expr/node_algorithm.h" #include "smt/env.h" +#include "smt/smt_engine.h" #include "theory/theory_engine.h" #include "theory/theory_model.h" @@ -36,31 +37,39 @@ PreprocessingPassContext::PreprocessingPassContext( d_symsInAssertions(env.getUserContext()) { } -const Options& PreprocessingPassContext::getOptions() +const Options& PreprocessingPassContext::getOptions() const { return d_env.getOptions(); } -const LogicInfo& PreprocessingPassContext::getLogicInfo() +const LogicInfo& PreprocessingPassContext::getLogicInfo() const { return d_env.getLogicInfo(); } -theory::Rewriter* PreprocessingPassContext::getRewriter() +theory::Rewriter* PreprocessingPassContext::getRewriter() const { return d_env.getRewriter(); } theory::TrustSubstitutionMap& -PreprocessingPassContext::getTopLevelSubstitutions() +PreprocessingPassContext::getTopLevelSubstitutions() const { return d_env.getTopLevelSubstitutions(); } -context::Context* PreprocessingPassContext::getUserContext() +TheoryEngine* PreprocessingPassContext::getTheoryEngine() const +{ + return d_smt->getTheoryEngine(); +} +prop::PropEngine* PreprocessingPassContext::getPropEngine() const +{ + return d_smt->getPropEngine(); +} +context::Context* PreprocessingPassContext::getUserContext() const { return d_env.getUserContext(); } -context::Context* PreprocessingPassContext::getDecisionContext() +context::Context* PreprocessingPassContext::getDecisionContext() const { return d_env.getContext(); } @@ -88,7 +97,7 @@ void PreprocessingPassContext::notifyLearnedLiteral(TNode lit) d_llm.notifyLearnedLiteral(lit); } -std::vector<Node> PreprocessingPassContext::getLearnedLiterals() +std::vector<Node> PreprocessingPassContext::getLearnedLiterals() const { return d_llm.getLearnedLiterals(); } @@ -108,7 +117,7 @@ void PreprocessingPassContext::addSubstitution(const Node& lhs, getTopLevelSubstitutions().addSubstitution(lhs, rhs, id, {}, args); } -ProofNodeManager* PreprocessingPassContext::getProofNodeManager() +ProofNodeManager* PreprocessingPassContext::getProofNodeManager() const { return d_env.getProofNodeManager(); } diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index 901322a10..a2407b953 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -24,53 +24,78 @@ #include "context/cdhashset.h" #include "preprocessing/learned_literal_manager.h" -#include "smt/smt_engine.h" +#include "theory/logic_info.h" #include "util/resource_manager.h" namespace cvc5 { + +class Env; class SmtEngine; class TheoryEngine; + +namespace theory { +class Rewriter; +} + namespace theory::booleans { class CircuitPropagator; } + namespace prop { class PropEngine; } + namespace preprocessing { class PreprocessingPassContext { public: + /** Constructor. */ PreprocessingPassContext( SmtEngine* smt, Env& env, theory::booleans::CircuitPropagator* circuitPropagator); - SmtEngine* getSmt() { return d_smt; } - TheoryEngine* getTheoryEngine() { return d_smt->getTheoryEngine(); } - prop::PropEngine* getPropEngine() { return d_smt->getPropEngine(); } - context::Context* getUserContext(); - context::Context* getDecisionContext(); + /** Get the associated SmtEngine. */ + SmtEngine* getSmt() const { return d_smt; } - theory::booleans::CircuitPropagator* getCircuitPropagator() + /** Get the associated TheoryEngine. */ + TheoryEngine* getTheoryEngine() const; + /** Get the associated Propengine. */ + prop::PropEngine* getPropEngine() const; + /** Get the current user context. */ + context::Context* getUserContext() const; + /** Get the current decision context. */ + context::Context* getDecisionContext() const; + + /** Get the associated circuit propagator. */ + theory::booleans::CircuitPropagator* getCircuitPropagator() const { return d_circuitPropagator; } - context::CDHashSet<Node>& getSymsInAssertions() { return d_symsInAssertions; } + /** + * Get the (user-context-dependent) set of symbols that occur in at least one + * assertion in the current user context. + */ + const context::CDHashSet<Node>& getSymsInAssertions() const + { + return d_symsInAssertions; + } + /** Spend resource in the resource manager of the associated Env. */ void spendResource(Resource r); /** Get the options of the environment */ - const Options& getOptions(); + const Options& getOptions() const; /** Get the current logic info of the environment */ - const LogicInfo& getLogicInfo(); + const LogicInfo& getLogicInfo() const; /** Get a pointer to the Rewriter owned by the associated Env. */ - theory::Rewriter* getRewriter(); + theory::Rewriter* getRewriter() const; /** Get a reference to the top-level substitution map */ - theory::TrustSubstitutionMap& getTopLevelSubstitutions(); + theory::TrustSubstitutionMap& getTopLevelSubstitutions() const; /** Record symbols in assertions * @@ -90,7 +115,7 @@ class PreprocessingPassContext /** * Get the learned literals */ - std::vector<Node> getLearnedLiterals(); + std::vector<Node> getLearnedLiterals() const; /** * Add substitution to the top-level substitutions, which also as a * consequence is used by the theory model. @@ -108,7 +133,7 @@ class PreprocessingPassContext const std::vector<Node>& args); /** The the proof node manager associated with this context, if it exists */ - ProofNodeManager* getProofNodeManager(); + ProofNodeManager* getProofNodeManager() const; private: /** Pointer to the SmtEngine that this context was created in. */ diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 7c1a0e887..75219840a 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -141,16 +141,16 @@ void AstPrinter::toStream(std::ostream& out, const smt::Model& m) const } void AstPrinter::toStreamModelSort(std::ostream& out, - const smt::Model& m, - TypeNode tn) const + TypeNode tn, + const std::vector<Node>& elements) const { // shouldn't be called; only the non-Command* version above should be Unreachable(); } void AstPrinter::toStreamModelTerm(std::ostream& out, - const smt::Model& m, - Node n) const + const Node& n, + const Node& value) const { // shouldn't be called; only the non-Command* version above should be Unreachable(); diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h index da5785f9f..fd4775da4 100644 --- a/src/printer/ast/ast_printer.h +++ b/src/printer/ast/ast_printer.h @@ -173,16 +173,16 @@ class AstPrinter : public cvc5::Printer * tn declared via declare-sort or declare-datatype. */ void toStreamModelSort(std::ostream& out, - const smt::Model& m, - TypeNode tn) const override; + TypeNode tn, + const std::vector<Node>& elements) const override; /** * To stream model term. This prints the appropriate output for term * n declared via declare-fun. */ void toStreamModelTerm(std::ostream& out, - const smt::Model& m, - Node n) const override; + const Node& n, + const Node& value) const override; /** * To stream with let binding. This prints n, possibly in the scope * of letification generated by this method based on lbind. diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 1f1296b7f..04274ddc3 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -1029,8 +1029,8 @@ void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const }/* CvcPrinter::toStream(CommandStatus*) */ void CvcPrinter::toStreamModelSort(std::ostream& out, - const smt::Model& m, - TypeNode tn) const + TypeNode tn, + const std::vector<Node>& elements) const { if (!tn.isSort()) { @@ -1038,36 +1038,25 @@ void CvcPrinter::toStreamModelSort(std::ostream& out, << tn << std::endl; return; } - const theory::TheoryModel* tm = m.getTheoryModel(); - const std::vector<Node>* type_reps = tm->getRepSet()->getTypeRepsOrNull(tn); - if (type_reps != nullptr) + out << "% cardinality of " << tn << " is " << elements.size() << std::endl; + toStreamCmdDeclareType(out, tn); + for (const Node& type_rep : elements) { - out << "% cardinality of " << tn << " is " << type_reps->size() - << std::endl; - toStreamCmdDeclareType(out, tn); - for (Node type_rep : *type_reps) + if (type_rep.isVar()) { - if (type_rep.isVar()) - { - out << type_rep << " : " << tn << ";" << std::endl; - } - else - { - out << "% rep: " << type_rep << std::endl; - } + out << type_rep << " : " << tn << ";" << std::endl; + } + else + { + out << "% rep: " << type_rep << std::endl; } - } - else - { - toStreamCmdDeclareType(out, tn); } } void CvcPrinter::toStreamModelTerm(std::ostream& out, - const smt::Model& m, - Node n) const + const Node& n, + const Node& value) const { - const theory::TheoryModel* tm = m.getTheoryModel(); TypeNode tn = n.getType(); out << n << " : "; if (tn.isFunction() || tn.isPredicate()) @@ -1087,10 +1076,7 @@ void CvcPrinter::toStreamModelTerm(std::ostream& out, { out << tn; } - // We get the value from the theory model directly, which notice - // does not have to go through the standard SmtEngine::getValue interface. - Node val = tm->getValue(n); - out << " = " << val << ";" << std::endl; + out << " = " << value << ";" << std::endl; } void CvcPrinter::toStream(std::ostream& out, const smt::Model& m) const diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h index 555237177..4851868d3 100644 --- a/src/printer/cvc/cvc_printer.h +++ b/src/printer/cvc/cvc_printer.h @@ -175,19 +175,19 @@ class CvcPrinter : public cvc5::Printer LetBinding* lbind) const; /** * To stream model sort. This prints the appropriate output for type - * tn declared via declare-sort or declare-datatype. + * tn declared via declare-sort. */ void toStreamModelSort(std::ostream& out, - const smt::Model& m, - TypeNode tn) const override; + TypeNode tn, + const std::vector<Node>& elements) const override; /** * To stream model term. This prints the appropriate output for term * n declared via declare-fun. */ void toStreamModelTerm(std::ostream& out, - const smt::Model& m, - Node n) const override; + const Node& n, + const Node& value) const override; /** * To stream with let binding. This prints n, possibly in the scope * of letification generated by this method based on lbind. diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 59122cf3d..e038952c4 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -66,22 +66,15 @@ void Printer::toStream(std::ostream& out, const smt::Model& m) const const std::vector<TypeNode>& dsorts = m.getDeclaredSorts(); for (const TypeNode& tn : dsorts) { - toStreamModelSort(out, m, tn); + toStreamModelSort(out, tn, m.getDomainElements(tn)); } - // print the declared terms const std::vector<Node>& dterms = m.getDeclaredTerms(); for (const Node& n : dterms) { - // take into account model core, independently of the format - if (!m.isModelCoreSymbol(n)) - { - continue; - } - toStreamModelTerm(out, m, n); + toStreamModelTerm(out, n, m.getValue(n)); } - -}/* Printer::toStream(Model) */ +} void Printer::toStreamUsing(Language lang, std::ostream& out, diff --git a/src/printer/printer.h b/src/printer/printer.h index 05ac8879b..5e141fe8f 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -271,19 +271,19 @@ class Printer /** * To stream model sort. This prints the appropriate output for type - * tn declared via declare-sort or declare-datatype. + * tn declared via declare-sort. */ virtual void toStreamModelSort(std::ostream& out, - const smt::Model& m, - TypeNode tn) const = 0; + TypeNode tn, + const std::vector<Node>& elements) const = 0; /** * To stream model term. This prints the appropriate output for term * n declared via declare-fun. */ virtual void toStreamModelTerm(std::ostream& out, - const smt::Model& m, - Node n) const = 0; + const Node& n, + const Node& value) const = 0; /** write model response to command using another language printer */ void toStreamUsing(Language lang, diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 8a23a59ea..0d556c1dc 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1262,7 +1262,6 @@ void Smt2Printer::toStream(std::ostream& out, const UnsatCore& core) const void Smt2Printer::toStream(std::ostream& out, const smt::Model& m) const { - const theory::TheoryModel* tm = m.getTheoryModel(); //print the model out << "(" << endl; // don't need to print approximations since they are built into choice @@ -1271,7 +1270,7 @@ void Smt2Printer::toStream(std::ostream& out, const smt::Model& m) const out << ")" << endl; //print the heap model, if it exists Node h, neq; - if (tm->getHeapModel(h, neq)) + if (m.getHeapModel(h, neq)) { // description of the heap+what nil is equal to fully describes model out << "(heap" << endl; @@ -1282,8 +1281,8 @@ void Smt2Printer::toStream(std::ostream& out, const smt::Model& m) const } void Smt2Printer::toStreamModelSort(std::ostream& out, - const smt::Model& m, - TypeNode tn) const + TypeNode tn, + const std::vector<Node>& elements) const { if (!tn.isSort()) { @@ -1291,8 +1290,6 @@ void Smt2Printer::toStreamModelSort(std::ostream& out, << tn << std::endl; return; } - const theory::TheoryModel* tm = m.getTheoryModel(); - std::vector<Node> elements = tm->getDomainElements(tn); // print the cardinality out << "; cardinality of " << tn << " is " << elements.size() << endl; if (options::modelUninterpPrint() @@ -1322,26 +1319,22 @@ void Smt2Printer::toStreamModelSort(std::ostream& out, } void Smt2Printer::toStreamModelTerm(std::ostream& out, - const smt::Model& m, - Node n) const + const Node& n, + const Node& value) const { - const theory::TheoryModel* tm = m.getTheoryModel(); - // We get the value from the theory model directly, which notice - // does not have to go through the standard SmtEngine::getValue interface. - Node val = tm->getValue(n); - if (val.getKind() == kind::LAMBDA) + if (value.getKind() == kind::LAMBDA) { TypeNode rangeType = n.getType().getRangeType(); - out << "(define-fun " << n << " " << val[0] << " " << rangeType << " "; + out << "(define-fun " << n << " " << value[0] << " " << rangeType << " "; // call toStream and force its type to be proper - toStreamCastToType(out, val[1], -1, rangeType); + toStreamCastToType(out, value[1], -1, rangeType); out << ")" << endl; } else { out << "(define-fun " << n << " () " << n.getType() << " "; // call toStream and force its type to be proper - toStreamCastToType(out, val, -1, n.getType()); + toStreamCastToType(out, value, -1, n.getType()); out << ")" << endl; } } diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 15f45a10e..729caebf4 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -252,16 +252,16 @@ class Smt2Printer : public cvc5::Printer * tn declared via declare-sort or declare-datatype. */ void toStreamModelSort(std::ostream& out, - const smt::Model& m, - TypeNode tn) const override; + TypeNode tn, + const std::vector<Node>& elements) const override; /** * To stream model term. This prints the appropriate output for term * n declared via declare-fun. */ void toStreamModelTerm(std::ostream& out, - const smt::Model& m, - Node n) const override; + const Node& n, + const Node& value) const override; /** * To stream with let binding. This prints n, possibly in the scope diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp index bb8df120e..6c8746706 100644 --- a/src/printer/tptp/tptp_printer.cpp +++ b/src/printer/tptp/tptp_printer.cpp @@ -58,16 +58,16 @@ void TptpPrinter::toStream(std::ostream& out, const smt::Model& m) const } void TptpPrinter::toStreamModelSort(std::ostream& out, - const smt::Model& m, - TypeNode tn) const + TypeNode tn, + const std::vector<Node>& elements) const { // shouldn't be called; only the non-Command* version above should be Unreachable(); } void TptpPrinter::toStreamModelTerm(std::ostream& out, - const smt::Model& m, - Node n) const + const Node& n, + const Node& value) const { // shouldn't be called; only the non-Command* version above should be Unreachable(); diff --git a/src/printer/tptp/tptp_printer.h b/src/printer/tptp/tptp_printer.h index db86de8cf..9d288b4ed 100644 --- a/src/printer/tptp/tptp_printer.h +++ b/src/printer/tptp/tptp_printer.h @@ -48,16 +48,16 @@ class TptpPrinter : public cvc5::Printer * tn declared via declare-sort or declare-datatype. */ void toStreamModelSort(std::ostream& out, - const smt::Model& m, - TypeNode tn) const override; + TypeNode tn, + const std::vector<Node>& elements) const override; /** * To stream model term. This prints the appropriate output for term * n declared via declare-fun. */ void toStreamModelTerm(std::ostream& out, - const smt::Model& m, - Node n) const override; + const Node& n, + const Node& value) const override; }; /* class TptpPrinter */ diff --git a/src/proof/lazy_proof.cpp b/src/proof/lazy_proof.cpp index b16a8d758..eab452d49 100644 --- a/src/proof/lazy_proof.cpp +++ b/src/proof/lazy_proof.cpp @@ -100,7 +100,14 @@ std::shared_ptr<ProofNode> LazyCDProof::getProofFor(Node fact) if (isSym) { - d_manager->updateNode(cur, PfRule::SYMM, {pgc}, {}); + if (pgc->getRule() == PfRule::SYMM) + { + d_manager->updateNode(cur, pgc->getChildren()[0].get()); + } + else + { + d_manager->updateNode(cur, PfRule::SYMM, {pgc}, {}); + } } else { diff --git a/src/proof/proof.cpp b/src/proof/proof.cpp index 79f84135d..dc370a04d 100644 --- a/src/proof/proof.cpp +++ b/src/proof/proof.cpp @@ -97,8 +97,7 @@ std::shared_ptr<ProofNode> CDProof::getProofSymm(Node fact) if (pf == nullptr) { Trace("cdproof") << "...fresh make symm" << std::endl; - std::shared_ptr<ProofNode> psym = - d_manager->mkNode(PfRule::SYMM, pschild, args, fact); + std::shared_ptr<ProofNode> psym = d_manager->mkSymm(pfs, fact); Assert(psym != nullptr); d_nodes.insert(fact, psym); return psym; @@ -411,13 +410,23 @@ bool CDProof::isAssumption(ProofNode* pn) { return true; } - else if (rule == PfRule::SYMM) + else if (rule != PfRule::SYMM) { - const std::vector<std::shared_ptr<ProofNode>>& pc = pn->getChildren(); - Assert(pc.size() == 1); - return pc[0]->getRule() == PfRule::ASSUME; + return false; } - return false; + pn = ProofNodeManager::cancelDoubleSymm(pn); + rule = pn->getRule(); + if (rule == PfRule::ASSUME) + { + return true; + } + else if (rule != PfRule::SYMM) + { + return false; + } + const std::vector<std::shared_ptr<ProofNode>>& pc = pn->getChildren(); + Assert(pc.size() == 1); + return pc[0]->getRule() == PfRule::ASSUME; } bool CDProof::isSame(TNode f, TNode g) diff --git a/src/proof/proof_node_manager.cpp b/src/proof/proof_node_manager.cpp index cf19eebdf..7e41a9057 100644 --- a/src/proof/proof_node_manager.cpp +++ b/src/proof/proof_node_manager.cpp @@ -61,6 +61,18 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkAssume(Node fact) return mkNode(PfRule::ASSUME, {}, {fact}, fact); } +std::shared_ptr<ProofNode> ProofNodeManager::mkSymm( + std::shared_ptr<ProofNode> child, Node expected) +{ + if (child->getRule() == PfRule::SYMM) + { + Assert(expected.isNull() + || child->getChildren()[0]->getResult() == expected); + return child->getChildren()[0]; + } + return mkNode(PfRule::SYMM, {child}, {}, expected); +} + std::shared_ptr<ProofNode> ProofNodeManager::mkTrans( const std::vector<std::shared_ptr<ProofNode>>& children, Node expected) { @@ -173,7 +185,14 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope( // use SYMM if possible if (aMatch == aeqSym) { - updateNode(pfs.get(), PfRule::SYMM, children, {}); + if (pfaa->getRule() == PfRule::SYMM) + { + updateNode(pfs.get(), pfaa->getChildren()[0].get()); + } + else + { + updateNode(pfs.get(), PfRule::SYMM, children, {}); + } } else { @@ -263,6 +282,11 @@ bool ProofNodeManager::updateNode(ProofNode* pn, ProofNode* pnr) { Assert(pn != nullptr); Assert(pnr != nullptr); + if (pn == pnr) + { + // same node, no update necessary + return true; + } if (pn->getResult() != pnr->getResult()) { return false; @@ -299,7 +323,7 @@ Node ProofNodeManager::checkInternal( ProofChecker* ProofNodeManager::getChecker() const { return d_checker; } std::shared_ptr<ProofNode> ProofNodeManager::clone( - std::shared_ptr<ProofNode> pn) + std::shared_ptr<ProofNode> pn) const { const ProofNode* orig = pn.get(); std::unordered_map<const ProofNode*, std::shared_ptr<ProofNode>> visited; @@ -333,7 +357,13 @@ std::shared_ptr<ProofNode> ProofNodeManager::clone( { it = visited.find(cp.get()); Assert(it != visited.end()); - Assert(it->second != nullptr); + // if we encounter nullptr here, then this child is currently being + // traversed at a higher level, hence this corresponds to a cyclic + // proof. + if (it->second == nullptr) + { + Unreachable() << "Cyclic proof encountered when cloning a proof node"; + } cchildren.push_back(it->second); } cloned = std::make_shared<ProofNode>( @@ -347,6 +377,23 @@ std::shared_ptr<ProofNode> ProofNodeManager::clone( return visited[orig]; } +ProofNode* ProofNodeManager::cancelDoubleSymm(ProofNode* pn) +{ + while (pn->getRule() == PfRule::SYMM) + { + std::shared_ptr<ProofNode> pnc = pn->getChildren()[0]; + if (pnc->getRule() == PfRule::SYMM) + { + pn = pnc->getChildren()[0].get(); + } + else + { + break; + } + } + return pn; +} + bool ProofNodeManager::updateNodeInternal( ProofNode* pn, PfRule id, diff --git a/src/proof/proof_node_manager.h b/src/proof/proof_node_manager.h index 2fa7ed3e9..541686a30 100644 --- a/src/proof/proof_node_manager.h +++ b/src/proof/proof_node_manager.h @@ -85,6 +85,12 @@ class ProofNodeManager */ std::shared_ptr<ProofNode> mkAssume(Node fact); /** + * Make symm, which accounts for whether the child is already a SYMM + * node, in which case we return its child. + */ + std::shared_ptr<ProofNode> mkSymm(std::shared_ptr<ProofNode> child, + Node expected = Node::null()); + /** * Make transitivity proof, where children contains one or more proofs of * equalities that form an ordered chain. In other words, the vector children * is a legal set of children for an application of TRANS. @@ -166,7 +172,12 @@ class ProofNodeManager * @param pn The proof node to clone * @return the cloned proof node. */ - std::shared_ptr<ProofNode> clone(std::shared_ptr<ProofNode> pn); + std::shared_ptr<ProofNode> clone(std::shared_ptr<ProofNode> pn) const; + /** + * Cancel double SYMM. Returns a proof node that is not a double application + * of SYMM, e.g. for (SYMM (SYMM (r P))), this returns (r P) where r != SYMM. + */ + static ProofNode* cancelDoubleSymm(ProofNode* pn); private: /** The (optional) proof checker */ diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index ad23bedc9..8891016a4 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -305,11 +305,19 @@ void SatProofManager::processRedundantLit( printClause(reason); Trace("sat-proof") << "\n"; } - // check if redundant literals in the reason. The first literal is the one we - // will be eliminating, so we check the others + // Since processRedundantLit calls can reallocate memory in the SAT solver due + // to explaining stuff, we directly get the literals and the clause node here + std::vector<SatLiteral> toProcess; for (unsigned i = 1, size = reason.size(); i < size; ++i) { - SatLiteral satLit = MinisatSatSolver::toSatLiteral(reason[i]); + toProcess.push_back(MinisatSatSolver::toSatLiteral(reason[i])); + } + Node clauseNode = getClauseNode(reason); + // check if redundant literals in the reason. The first literal is the one we + // will be eliminating, so we check the others + for (unsigned i = 0, size = toProcess.size(); i < size; ++i) + { + SatLiteral satLit = toProcess[i]; // if literal does not occur in the conclusion we process it as well if (!conclusionLits.count(satLit)) { @@ -325,7 +333,6 @@ void SatProofManager::processRedundantLit( // reason, not only with ~lit, since the learned clause is built under the // assumption that the redundant literal is removed via the resolution with // the explanation of its negation - Node clauseNode = getClauseNode(reason); Node litNode = d_cnfStream->getNodeCache()[lit]; bool negated = lit.isNegated(); Assert(!negated || litNode.getKind() == kind::NOT); diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index 0bc7ce99b..d3a2dfefa 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -18,13 +18,13 @@ #include "base/modal_exception.h" #include "options/smt_options.h" #include "smt/env.h" -#include "smt/model.h" #include "smt/node_command.h" #include "smt/preprocessor.h" #include "smt/smt_solver.h" #include "theory/rewriter.h" #include "theory/substitutions.h" #include "theory/theory_engine.h" +#include "theory/theory_model.h" using namespace cvc5::theory; @@ -34,7 +34,7 @@ namespace smt { CheckModels::CheckModels(Env& e) : d_env(e) {} CheckModels::~CheckModels() {} -void CheckModels::checkModel(Model* m, +void CheckModels::checkModel(TheoryModel* m, context::CDList<Node>* al, bool hardFailure) { diff --git a/src/smt/check_models.h b/src/smt/check_models.h index ce06bae07..fbfb1c2f5 100644 --- a/src/smt/check_models.h +++ b/src/smt/check_models.h @@ -25,9 +25,11 @@ namespace cvc5 { class Env; -namespace smt { +namespace theory { +class TheoryModel; +} -class Model; +namespace smt { /** * This utility is responsible for checking the current model. @@ -43,7 +45,9 @@ class CheckModels * This throws an exception if we fail to verify that m is a proper model * given assertion list al based on the model checking policy. */ - void checkModel(Model* m, context::CDList<Node>* al, bool hardFailure); + void checkModel(theory::TheoryModel* m, + context::CDList<Node>* al, + bool hardFailure); private: /** Reference to the environment */ diff --git a/src/smt/command.cpp b/src/smt/command.cpp index e6be0a646..008d7a6d8 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -38,8 +38,6 @@ #include "proof/unsat_core.h" #include "smt/dump.h" #include "smt/model.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" #include "util/unsafe_interrupt_exception.h" #include "util/utility.h" @@ -1748,27 +1746,17 @@ void GetAssignmentCommand::toStream(std::ostream& out, /* class GetModelCommand */ /* -------------------------------------------------------------------------- */ -GetModelCommand::GetModelCommand() : d_result(nullptr) {} +GetModelCommand::GetModelCommand() {} void GetModelCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { - d_result = solver->getSmtEngine()->getModel(); - // set the model declarations, which determines what is printed in the model - d_result->clearModelDeclarations(); std::vector<api::Sort> declareSorts = sm->getModelDeclareSorts(); - for (const api::Sort& s : declareSorts) - { - d_result->addDeclarationSort(sortToTypeNode(s)); - } std::vector<api::Term> declareTerms = sm->getModelDeclareTerms(); - for (const api::Term& t : declareTerms) - { - d_result->addDeclarationTerm(termToNode(t)); - } + d_result = solver->getModel(declareSorts, declareTerms); d_commandStatus = CommandSuccess::instance(); } - catch (RecoverableModalException& e) + catch (api::CVC5ApiRecoverableException& e) { d_commandStatus = new CommandRecoverableFailure(e.what()); } @@ -1782,12 +1770,6 @@ void GetModelCommand::invoke(api::Solver* solver, SymbolManager* sm) } } -/* Model is private to the library -- for now -Model* GetModelCommand::getResult() const { - return d_result; -} -*/ - void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const { if (!ok()) @@ -1796,13 +1778,13 @@ void GetModelCommand::printResult(std::ostream& out, uint32_t verbosity) const } else { - out << *d_result; + out << d_result; } } Command* GetModelCommand::clone() const { - GetModelCommand* c = new GetModelCommand(); + GetModelCommand* c = new GetModelCommand; c->d_result = d_result; return c; } diff --git a/src/smt/command.h b/src/smt/command.h index d3e3679d2..627cb13c9 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -950,7 +950,8 @@ class CVC5_EXPORT GetModelCommand : public Command Language language = Language::LANG_AUTO) const override; protected: - smt::Model* d_result; + /** Result of printing the model */ + std::string d_result; }; /* class GetModelCommand */ /** The command to block models. */ diff --git a/src/smt/model.cpp b/src/smt/model.cpp index cf6a90f12..9a195cb51 100644 --- a/src/smt/model.cpp +++ b/src/smt/model.cpp @@ -18,18 +18,13 @@ #include "expr/expr_iomanip.h" #include "options/base_options.h" #include "printer/printer.h" -#include "smt/dump_manager.h" -#include "smt/node_command.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" -#include "theory/theory_model.h" namespace cvc5 { namespace smt { -Model::Model(theory::TheoryModel* tm) : d_isKnownSat(false), d_tmodel(tm) +Model::Model(bool isKnownSat, const std::string& inputName) + : d_inputName(inputName), d_isKnownSat(isKnownSat) { - Assert(d_tmodel != nullptr); } std::ostream& operator<<(std::ostream& out, const Model& m) { @@ -38,31 +33,55 @@ std::ostream& operator<<(std::ostream& out, const Model& m) { return out; } -theory::TheoryModel* Model::getTheoryModel() { return d_tmodel; } +const std::vector<Node>& Model::getDomainElements(TypeNode tn) const +{ + std::map<TypeNode, std::vector<Node>>::const_iterator it = + d_domainElements.find(tn); + Assert(it != d_domainElements.end()); + return it->second; +} -const theory::TheoryModel* Model::getTheoryModel() const { return d_tmodel; } +Node Model::getValue(TNode n) const +{ + std::map<Node, Node>::const_iterator it = d_declareTermValues.find(n); + Assert(it != d_declareTermValues.end()); + return it->second; +} -bool Model::isModelCoreSymbol(TNode sym) const +bool Model::getHeapModel(Node& h, Node& nilEq) const { - return d_tmodel->isModelCoreSymbol(sym); + if (d_sepHeap.isNull() || d_sepNilEq.isNull()) + { + return false; + } + h = d_sepHeap; + nilEq = d_sepNilEq; + return true; } -Node Model::getValue(TNode n) const { return d_tmodel->getValue(n); } -bool Model::hasApproximations() const { return d_tmodel->hasApproximations(); } +void Model::addDeclarationSort(TypeNode tn, const std::vector<Node>& elements) +{ + d_declareSorts.push_back(tn); + d_domainElements[tn] = elements; +} -void Model::clearModelDeclarations() +void Model::addDeclarationTerm(Node n, Node value) { - d_declareTerms.clear(); - d_declareSorts.clear(); + d_declareTerms.push_back(n); + d_declareTermValues[n] = value; } -void Model::addDeclarationSort(TypeNode tn) { d_declareSorts.push_back(tn); } +void Model::setHeapModel(Node h, Node nilEq) +{ + d_sepHeap = h; + d_sepNilEq = nilEq; +} -void Model::addDeclarationTerm(Node n) { d_declareTerms.push_back(n); } const std::vector<TypeNode>& Model::getDeclaredSorts() const { return d_declareSorts; } + const std::vector<Node>& Model::getDeclaredTerms() const { return d_declareTerms; diff --git a/src/smt/model.h b/src/smt/model.h index 342a9f3b0..5275ea680 100644 --- a/src/smt/model.h +++ b/src/smt/model.h @@ -15,8 +15,8 @@ #include "cvc5_private.h" -#ifndef CVC5__MODEL_H -#define CVC5__MODEL_H +#ifndef CVC5__SMT__MODEL_H +#define CVC5__SMT__MODEL_H #include <iosfwd> #include <vector> @@ -24,13 +24,6 @@ #include "expr/node.h" namespace cvc5 { - -class SmtEngine; - -namespace theory { -class TheoryModel; -} - namespace smt { class Model; @@ -38,22 +31,15 @@ class Model; std::ostream& operator<<(std::ostream&, const Model&); /** - * This is the SMT-level model object, that is responsible for maintaining - * the necessary information for how to print the model, as well as - * holding a pointer to the underlying implementation of the theory model. - * - * The model declarations maintained by this class are context-independent - * and should be updated when this model is printed. + * A utility for representing a model for pretty printing. */ class Model { - friend std::ostream& operator<<(std::ostream&, const Model&); - friend class ::cvc5::SmtEngine; - public: - /** construct */ - Model(theory::TheoryModel* tm); - /** virtual destructor */ - ~Model() {} + /** Constructor + * @param isKnownSat True if this model is associated with a "sat" response, + * or false if it is associated with an "unknown" response. + */ + Model(bool isKnownSat, const std::string& inputName); /** get the input name (file name, etc.) this model is associated to */ std::string getInputName() const { return d_inputName; } /** @@ -63,31 +49,37 @@ class Model { * only a candidate solution. */ bool isKnownSat() const { return d_isKnownSat; } - /** Get the underlying theory model */ - theory::TheoryModel* getTheoryModel(); - /** Get the underlying theory model (const version) */ - const theory::TheoryModel* getTheoryModel() const; - //----------------------- helper methods in the underlying theory model - /** Is the node n a model core symbol? */ - bool isModelCoreSymbol(TNode sym) const; + /** Get domain elements */ + const std::vector<Node>& getDomainElements(TypeNode tn) const; /** Get value */ Node getValue(TNode n) const; - /** Does this model have approximations? */ - bool hasApproximations() const; - //----------------------- end helper methods + /** Get separation logic heap and nil, return true if they have been set */ + bool getHeapModel(Node& h, Node& nilEq) const; //----------------------- model declarations - /** Clear the current model declarations. */ - void clearModelDeclarations(); /** * Set that tn is a sort that should be printed in the model, when applicable, * based on the output language. + * + * @param tn The uninterpreted sort + * @param elements The domain elements of tn in the model */ - void addDeclarationSort(TypeNode tn); + void addDeclarationSort(TypeNode tn, const std::vector<Node>& elements); /** * Set that n is a variable that should be printed in the model, when * applicable, based on the output language. + * + * @param n The variable + * @param value The value of the variable in the model + */ + void addDeclarationTerm(Node n, Node value); + /** + * Set the separation logic model information where h is the heap and nilEq + * is the value of sep.nil. + * + * @param h The value of heap in the heap model + * @param nilEq The value of sep.nil in the heap model */ - void addDeclarationTerm(Node n); + void setHeapModel(Node h, Node nilEq); /** get declared sorts */ const std::vector<TypeNode>& getDeclaredSorts() const; /** get declared terms */ @@ -102,23 +94,25 @@ class Model { */ bool d_isKnownSat; /** - * Pointer to the underlying theory model, which maintains all data regarding - * the values of sorts and terms. - */ - theory::TheoryModel* d_tmodel; - /** * The list of types to print, generally corresponding to declare-sort * commands. */ std::vector<TypeNode> d_declareSorts; + /** The interpretation of the above sorts, as a list of domain elements. */ + std::map<TypeNode, std::vector<Node>> d_domainElements; /** * The list of terms to print, is typically one-to-one with declare-fun * commands. */ std::vector<Node> d_declareTerms; + /** Mapping terms to values */ + std::map<Node, Node> d_declareTermValues; + /** Separation logic heap and nil */ + Node d_sepHeap; + Node d_sepNilEq; }; } // namespace smt } // namespace cvc5 -#endif /* CVC5__MODEL_H */ +#endif /* CVC5__SMT__MODEL_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2276956b5..27e7b8530 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -92,7 +92,6 @@ SmtEngine::SmtEngine(NodeManager* nm, const Options* optr) d_routListener(new ResourceOutListener(*this)), d_snmListener(new SmtNodeManagerListener(*getDumpManager(), d_outMgr)), d_smtSolver(nullptr), - d_model(nullptr), d_checkModels(nullptr), d_pfManager(nullptr), d_ucManager(nullptr), @@ -224,7 +223,6 @@ void SmtEngine::finishInit() TheoryModel* tm = te->getModel(); if (tm != nullptr) { - d_model.reset(new Model(tm)); // make the check models utility d_checkModels.reset(new CheckModels(*d_env.get())); } @@ -305,7 +303,6 @@ SmtEngine::~SmtEngine() d_absValues.reset(nullptr); d_asserts.reset(nullptr); - d_model.reset(nullptr); d_abductSolver.reset(nullptr); d_interpolSolver.reset(nullptr); @@ -712,7 +709,7 @@ Result SmtEngine::quickCheck() { Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, filename); } -Model* SmtEngine::getAvailableModel(const char* c) const +TheoryModel* SmtEngine::getAvailableModel(const char* c) const { if (!d_env->getOptions().theory.assignFunctionValues) { @@ -751,7 +748,7 @@ Model* SmtEngine::getAvailableModel(const char* c) const throw RecoverableModalException(ss.str().c_str()); } - return d_model.get(); + return m; } QuantifiersEngine* SmtEngine::getAvailableQuantifiersEngine(const char* c) const @@ -1121,7 +1118,7 @@ Node SmtEngine::getValue(const Node& ex) const } Trace("smt") << "--- getting value of " << n << endl; - Model* m = getAvailableModel("get-value"); + TheoryModel* m = getAvailableModel("get-value"); Assert(m != nullptr); Node resultNode = m->getValue(n); Trace("smt") << "--- got value " << n << " = " << resultNode << endl; @@ -1163,8 +1160,8 @@ std::vector<Node> SmtEngine::getValues(const std::vector<Node>& exprs) const std::vector<Node> SmtEngine::getModelDomainElements(TypeNode tn) const { Assert(tn.isSort()); - Model* m = getAvailableModel("getModelDomainElements"); - return m->getTheoryModel()->getDomainElements(tn); + TheoryModel* m = getAvailableModel("getModelDomainElements"); + return m->getDomainElements(tn); } bool SmtEngine::isModelCoreSymbol(Node n) @@ -1177,8 +1174,7 @@ bool SmtEngine::isModelCoreSymbol(Node n) // if the model core mode is none, we are always a model core symbol return true; } - Model* m = getAvailableModel("isModelCoreSymbol"); - TheoryModel* tm = m->getTheoryModel(); + TheoryModel* tm = getAvailableModel("isModelCoreSymbol"); // compute the model core if not done so already if (!tm->isUsingModelCore()) { @@ -1193,41 +1189,54 @@ bool SmtEngine::isModelCoreSymbol(Node n) return tm->isModelCoreSymbol(n); } -// TODO(#1108): Simplify the error reporting of this method. -Model* SmtEngine::getModel() { - Trace("smt") << "SMT getModel()" << endl; +std::string SmtEngine::getModel(const std::vector<TypeNode>& declaredSorts, + const std::vector<Node>& declaredFuns) +{ SmtScope smts(this); - - finishInit(); - - if (Dump.isOn("benchmark")) + // !!! Note that all methods called here should have a version at the API + // level. This is to ensure that the information associated with a model is + // completely accessible by the user. This is currently not rigorously + // enforced. An alternative design would be to have this method implemented + // at the API level, but this makes exceptions in the text interface less + // intuitive and makes it impossible to implement raw-benchmark at the + // SmtEngine level. + if (Dump.isOn("raw-benchmark")) { getPrinter().toStreamCmdGetModel(d_env->getDumpOut()); } - - Model* m = getAvailableModel("get model"); - - // Notice that the returned model is (currently) accessed by the - // GetModelCommand only, and is not returned to the user. The information - // in that model may become stale after it is returned. This is safe - // since GetModelCommand always calls this command again when it prints - // a model. - - if (d_env->getOptions().smt.modelCoresMode - != options::ModelCoresMode::NONE) + TheoryModel* tm = getAvailableModel("get model"); + // use the smt::Model model utility for printing + const Options& opts = d_env->getOptions(); + bool isKnownSat = (d_state->getMode() == SmtMode::SAT); + Model m(isKnownSat, opts.driver.filename); + // set the model declarations, which determines what is printed in the model + for (const TypeNode& tn : declaredSorts) { - // If we enabled model cores, we compute a model core for m based on our - // (expanded) assertions using the model core builder utility - std::vector<Node> asserts = getAssertionsInternal(); - d_pp->expandDefinitions(asserts); - ModelCoreBuilder::setModelCore( - asserts, m->getTheoryModel(), d_env->getOptions().smt.modelCoresMode); + m.addDeclarationSort(tn, getModelDomainElements(tn)); } - // set the information on the SMT-level model - Assert(m != nullptr); - m->d_inputName = d_env->getOptions().driver.filename; - m->d_isKnownSat = (d_state->getMode() == SmtMode::SAT); - return m; + bool usingModelCores = + (opts.smt.modelCoresMode != options::ModelCoresMode::NONE); + for (const Node& n : declaredFuns) + { + if (usingModelCores && !tm->isModelCoreSymbol(n)) + { + // skip if not in model core + continue; + } + Node value = tm->getValue(n); + m.addDeclarationTerm(n, value); + } + // for separation logic + TypeNode locT, dataT; + if (getSepHeapTypes(locT, dataT)) + { + std::pair<Node, Node> sh = getSepHeapAndNilExpr(); + m.setHeapModel(sh.first, sh.second); + } + // print the model + std::stringstream ssm; + ssm << m; + return ssm.str(); } Result SmtEngine::blockModel() @@ -1242,7 +1251,7 @@ Result SmtEngine::blockModel() getPrinter().toStreamCmdBlockModel(d_env->getDumpOut()); } - Model* m = getAvailableModel("block model"); + TheoryModel* m = getAvailableModel("block model"); if (d_env->getOptions().smt.blockModelsMode == options::BlockModelsMode::NONE) @@ -1254,10 +1263,8 @@ Result SmtEngine::blockModel() // get expanded assertions std::vector<Node> eassertsProc = getExpandedAssertions(); - Node eblocker = - ModelBlocker::getModelBlocker(eassertsProc, - m->getTheoryModel(), - d_env->getOptions().smt.blockModelsMode); + Node eblocker = ModelBlocker::getModelBlocker( + eassertsProc, m, d_env->getOptions().smt.blockModelsMode); Trace("smt") << "Block formula: " << eblocker << std::endl; return assertFormula(eblocker); } @@ -1274,16 +1281,13 @@ Result SmtEngine::blockModelValues(const std::vector<Node>& exprs) getPrinter().toStreamCmdBlockModelValues(d_env->getDumpOut(), exprs); } - Model* m = getAvailableModel("block model values"); + TheoryModel* m = getAvailableModel("block model values"); // get expanded assertions std::vector<Node> eassertsProc = getExpandedAssertions(); // we always do block model values mode here - Node eblocker = - ModelBlocker::getModelBlocker(eassertsProc, - m->getTheoryModel(), - options::BlockModelsMode::VALUES, - exprs); + Node eblocker = ModelBlocker::getModelBlocker( + eassertsProc, m, options::BlockModelsMode::VALUES, exprs); return assertFormula(eblocker); } @@ -1299,8 +1303,7 @@ std::pair<Node, Node> SmtEngine::getSepHeapAndNilExpr(void) NodeManagerScope nms(getNodeManager()); Node heap; Node nil; - Model* m = getAvailableModel("get separation logic heap and nil"); - TheoryModel* tm = m->getTheoryModel(); + TheoryModel* tm = getAvailableModel("get separation logic heap and nil"); if (!tm->getHeapModel(heap, nil)) { const char* msg = @@ -1548,7 +1551,7 @@ void SmtEngine::checkModel(bool hardFailure) { TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime); Notice() << "SmtEngine::checkModel(): generating model" << endl; - Model* m = getAvailableModel("check model"); + TheoryModel* m = getAvailableModel("check model"); Assert(m != nullptr); // check the model with the theory engine for debugging diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 84501d35e..06a1c9ae4 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -42,7 +42,6 @@ class Env; class NodeManager; class TheoryEngine; class UnsatCore; -class LogicRequest; class StatisticsRegistry; class Printer; class ResourceManager; @@ -77,7 +76,6 @@ namespace prop { namespace smt { /** Utilities */ -class Model; class SmtEngineState; class AbstractValues; class Assertions; @@ -104,9 +102,10 @@ class UnsatCoreManager; /* -------------------------------------------------------------------------- */ namespace theory { - class Rewriter; - class QuantifiersEngine; - } // namespace theory +class TheoryModel; +class Rewriter; +class QuantifiersEngine; +} // namespace theory /* -------------------------------------------------------------------------- */ @@ -115,7 +114,6 @@ class CVC5_EXPORT SmtEngine friend class ::cvc5::api::Solver; friend class ::cvc5::smt::SmtEngineState; friend class ::cvc5::smt::SmtScope; - friend class ::cvc5::LogicRequest; /* ....................................................................... */ public: @@ -227,14 +225,6 @@ class CVC5_EXPORT SmtEngine bool isInternalSubsolver() const; /** - * Get the model (only if immediately preceded by a SAT or NOT_ENTAILED - * query). Only permitted if produce-models is on. - * - * TODO (issues#287): eliminate this method. - */ - smt::Model* getModel(); - - /** * Block the current model. Can be called only if immediately preceded by * a SAT or INVALID query. Only permitted if produce-models is on, and the * block-models option is set to a mode other than "none". @@ -523,6 +513,19 @@ class CVC5_EXPORT SmtEngine */ bool isModelCoreSymbol(Node v); + /** + * Get a model (only if immediately preceded by an SAT or unknown query). + * Only permitted if the model option is on. + * + * @param declaredSorts The sorts to print in the model + * @param declaredFuns The free constants to print in the model. A subset + * of these may be printed based on isModelCoreSymbol. + * @return the string corresponding to the model. If the output language is + * smt2, then this corresponds to a response to the get-model command. + */ + std::string getModel(const std::vector<TypeNode>& declaredSorts, + const std::vector<Node>& declaredFuns); + /** print instantiations * * Print all instantiations for all quantified formulas on out, @@ -936,7 +939,7 @@ class CVC5_EXPORT SmtEngine * @param c used for giving an error message to indicate the context * this method was called. */ - smt::Model* getAvailableModel(const char* c) const; + theory::TheoryModel* getAvailableModel(const char* c) const; /** * Get available quantifiers engine, which throws a modal exception if it * does not exist. This can happen if a quantifiers-specific call (e.g. @@ -1047,13 +1050,6 @@ class CVC5_EXPORT SmtEngine std::unique_ptr<smt::SmtSolver> d_smtSolver; /** - * The SMT-level model object, which contains information about how to - * print the model, as well as a pointer to the underlying TheoryModel - * implementation maintained by the SmtSolver. - */ - std::unique_ptr<smt::Model> d_model; - - /** * The utility used for checking models */ std::unique_ptr<smt::CheckModels> d_checkModels; diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index de8750d89..d02069fd8 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -148,7 +148,7 @@ Node Rewriter::rewriteEqualityExt(TNode node) void Rewriter::registerTheoryRewriter(theory::TheoryId tid, TheoryRewriter* trew) { - getInstance()->d_theoryRewriters[tid] = trew; + d_theoryRewriters[tid] = trew; } void Rewriter::registerPreRewrite( diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index 09f0123bf..9ee13d952 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -103,8 +103,7 @@ class Rewriter { * @param tid The theory that the theory rewriter should be associated with. * @param trew The theory rewriter to register. */ - static void registerTheoryRewriter(theory::TheoryId tid, - TheoryRewriter* trew); + void registerTheoryRewriter(theory::TheoryId tid, TheoryRewriter* trew); /** * Register a prerewrite for a given kind. diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 6bec3dc8f..db98b47fa 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1965,4 +1965,6 @@ void TheoryEngine::initializeProofChecker(ProofChecker* pc) } } +theory::Rewriter* TheoryEngine::getRewriter() { return d_env.getRewriter(); } + } // namespace cvc5 diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index e610adcf7..5c44f8968 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -78,11 +78,13 @@ struct NodeTheoryPairHashFunction { /* Forward declarations */ namespace theory { -class TheoryModel; + class CombinationEngine; -class SharedSolver; class DecisionManager; class RelevanceManager; +class Rewriter; +class SharedSolver; +class TheoryModel; } // namespace theory @@ -96,203 +98,14 @@ class PropEngine; * T-solvers look like a single unit to the propositional part of * cvc5. */ -class TheoryEngine { - +class TheoryEngine +{ /** Shared terms database can use the internals notify the theories */ friend class SharedTermsDatabase; friend class theory::EngineOutputChannel; friend class theory::CombinationEngine; friend class theory::SharedSolver; - /** Associated PropEngine engine */ - prop::PropEngine* d_propEngine; - - /** - * Reference to the environment. - */ - Env& d_env; - - /** - * A table of from theory IDs to theory pointers. Never use this table - * directly, use theoryOf() instead. - */ - theory::Theory* d_theoryTable[theory::THEORY_LAST]; - - /** - * A collection of theories that are "active" for the current run. - * This set is provided by the user (as a logic string, say, in SMT-LIBv2 - * format input), or else by default it's all-inclusive. This is important - * because we can optimize for single-theory runs (no sharing), can reduce - * the cost of walking the DAG on registration, etc. - */ - const LogicInfo& d_logicInfo; - - /** The separation logic location and data types */ - TypeNode d_sepLocType; - TypeNode d_sepDataType; - - //--------------------------------- new proofs - /** Proof node manager used by this theory engine, if proofs are enabled */ - ProofNodeManager* d_pnm; - /** The lazy proof object - * - * This stores instructions for how to construct proofs for all theory lemmas. - */ - std::shared_ptr<LazyCDProof> d_lazyProof; - /** The proof generator */ - std::shared_ptr<TheoryEngineProofGenerator> d_tepg; - //--------------------------------- end new proofs - /** The combination manager we are using */ - std::unique_ptr<theory::CombinationEngine> d_tc; - /** The shared solver of the above combination engine. */ - theory::SharedSolver* d_sharedSolver; - /** The quantifiers engine, which is owned by the quantifiers theory */ - theory::QuantifiersEngine* d_quantEngine; - /** - * The decision manager - */ - std::unique_ptr<theory::DecisionManager> d_decManager; - /** The relevance manager */ - std::unique_ptr<theory::RelevanceManager> d_relManager; - /** - * An empty set of relevant assertions, which is returned as a dummy value for - * getRelevantAssertions when relevance is disabled. - */ - std::unordered_set<TNode> d_emptyRelevantSet; - - /** are we in eager model building mode? (see setEagerModelBuilding). */ - bool d_eager_model_building; - - /** - * Output channels for individual theories. - */ - theory::EngineOutputChannel* d_theoryOut[theory::THEORY_LAST]; - - /** - * Are we in conflict. - */ - context::CDO<bool> d_inConflict; - - /** - * Are we in "SAT mode"? In this state, the user can query for the model. - * This corresponds to the state in Figure 4.1, page 52 of the SMT-LIB - * standard, version 2.6. - */ - bool d_inSatMode; - - /** - * Called by the theories to notify of a conflict. - * - * @param conflict The trust node containing the conflict and its proof - * generator (if it exists), - * @param theoryId The theory that sent the conflict - */ - void conflict(TrustNode conflict, theory::TheoryId theoryId); - - /** set in conflict */ - void markInConflict(); - - /** - * Debugging flag to ensure that shutdown() is called before the - * destructor. - */ - bool d_hasShutDown; - - /** - * True if a theory has notified us of incompleteness (at this - * context level or below). - */ - context::CDO<bool> d_incomplete; - /** The theory and identifier that (most recently) set incomplete */ - context::CDO<theory::TheoryId> d_incompleteTheory; - context::CDO<theory::IncompleteId> d_incompleteId; - - /** - * Called by the theories to notify that the current branch is incomplete. - */ - void setIncomplete(theory::TheoryId theory, theory::IncompleteId id); - - /** - * Mapping of propagations from recievers to senders. - */ - typedef context::CDHashMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> PropagationMap; - PropagationMap d_propagationMap; - - /** - * Timestamp of propagations - */ - context::CDO<size_t> d_propagationMapTimestamp; - - /** - * Literals that are propagated by the theory. Note that these are TNodes. - * The theory can only propagate nodes that have an assigned literal in the - * SAT solver and are hence referenced in the SAT solver. - */ - context::CDList<TNode> d_propagatedLiterals; - - /** - * The index of the next literal to be propagated by a theory. - */ - context::CDO<unsigned> d_propagatedLiteralsIndex; - - /** - * Called by the output channel to propagate literals and facts - * @return false if immediate conflict - */ - bool propagate(TNode literal, theory::TheoryId theory); - - /** - * Internal method to call the propagation routines and collect the - * propagated literals. - */ - void propagate(theory::Theory::Effort effort); - - /** - * A variable to mark if we added any lemmas. - */ - bool d_lemmasAdded; - - /** - * A variable to mark if the OutputChannel was "used" by any theory - * since the start of the last check. If it has been, we require - * a FULL_EFFORT check before exiting and reporting SAT. - * - * See the documentation for the needCheck() function, below. - */ - bool d_outputChannelUsed; - - /** Atom requests from lemmas */ - AtomRequests d_atomRequests; - - /** - * Adds a new lemma, returning its status. - * @param node the lemma - * @param p the properties of the lemma. - * @param atomsTo the theory that atoms of the lemma should be sent to - * @param from the theory that sent the lemma - */ - void lemma(TrustNode node, - theory::LemmaProperty p, - theory::TheoryId from = theory::THEORY_LAST); - - /** Ensure atoms from the given node are sent to the given theory */ - void ensureLemmaAtoms(TNode n, theory::TheoryId atomsTo); - /** Ensure that the given atoms are sent to the given theory */ - void ensureLemmaAtoms(const std::vector<TNode>& atoms, - theory::TheoryId atomsTo); - - /** sort inference module */ - std::unique_ptr<theory::SortInference> d_sortInfer; - - /** Time spent in theory combination */ - TimerStat d_combineTheoriesTime; - - Node d_true; - Node d_false; - - /** Whether we were just interrupted (or not) */ - bool d_interrupted; - public: /** Constructs a theory engine */ TheoryEngine(Env& env); @@ -310,13 +123,13 @@ class TheoryEngine { * there is another theory it will be deleted. */ template <class TheoryClass> - inline void addTheory(theory::TheoryId theoryId) + void addTheory(theory::TheoryId theoryId) { Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL); d_theoryOut[theoryId] = new theory::EngineOutputChannel(this, theoryId); d_theoryTable[theoryId] = new TheoryClass(d_env, *d_theoryOut[theoryId], theory::Valuation(this)); - theory::Rewriter::registerTheoryRewriter( + getRewriter()->registerTheoryRewriter( theoryId, d_theoryTable[theoryId]->getTheoryRewriter()); } @@ -340,9 +153,7 @@ class TheoryEngine { /** * Get a pointer to the underlying propositional engine. */ - inline prop::PropEngine* getPropEngine() const { - return d_propEngine; - } + prop::PropEngine* getPropEngine() const { return d_propEngine; } /** Get the proof node manager */ ProofNodeManager* getProofNodeManager() const; @@ -360,7 +171,8 @@ class TheoryEngine { /** * Get a pointer to the underlying quantifiers engine. */ - theory::QuantifiersEngine* getQuantifiersEngine() const { + theory::QuantifiersEngine* getQuantifiersEngine() const + { return d_quantEngine; } /** @@ -371,60 +183,6 @@ class TheoryEngine { return d_decManager.get(); } - private: - /** - * Queue of nodes for pre-registration. - */ - std::queue<TNode> d_preregisterQueue; - - /** - * Boolean flag denoting we are in pre-registration. - */ - bool d_inPreregister; - - /** - * Did the theories get any new facts since the last time we called - * check() - */ - context::CDO<bool> d_factsAsserted; - - /** - * Assert the formula to the given theory. - * @param assertion the assertion to send (not necesserily normalized) - * @param original the assertion as it was sent in from the propagating theory - * @param toTheoryId the theory to assert to - * @param fromTheoryId the theory that sent it - */ - void assertToTheory(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId); - - /** - * Marks a theory propagation from a theory to a theory where a - * theory could be the THEORY_SAT_SOLVER for literals coming from - * or being propagated to the SAT solver. If the receiving theory - * already recieved the literal, the method returns false, otherwise - * it returns true. - * - * @param assertion the normalized assertion being sent - * @param originalAssertion the actual assertion that was sent - * @param toTheoryId the theory that is on the receiving end - * @param fromTheoryId the theory that sent the assertion - * @return true if a new assertion, false if theory already got it - */ - bool markPropagation(TNode assertion, TNode originalAssertions, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId); - - /** - * Computes the explanation by traversing the propagation graph and - * asking relevant theories to explain the propagations. Initially - * the explanation vector should contain only the element (node, theory) - * where the node is the one to be explained, and the theory is the - * theory that sent the literal. - */ - TrustNode getExplanation(std::vector<NodeTheoryPair>& explanationVector); - - /** Are proofs enabled? */ - bool isProofEnabled() const; - - public: /** * Preprocess rewrite equality, called by the preprocessor to rewrite * equalities appearing in the input. @@ -434,7 +192,7 @@ class TheoryEngine { void notifyPreprocessedAssertions(const std::vector<Node>& assertions); /** Return whether or not we are incomplete (in the current context). */ - inline bool isIncomplete() const { return d_incomplete; } + bool isIncomplete() const { return d_incomplete; } /** * Returns true if we need another round of checking. If this @@ -451,9 +209,7 @@ class TheoryEngine { * as it might decide to further instantiate some lemmas, precluding * a SAT response. */ - inline bool needCheck() const { - return d_outputChannelUsed || d_lemmasAdded; - } + bool needCheck() const { return d_outputChannelUsed || d_lemmasAdded; } /** * Is the literal lit (possibly) critical for satisfying the input formula in * the current context? This call is applicable only during collectModelInfo @@ -505,7 +261,7 @@ class TheoryEngine { */ bool presolve(); - /** + /** * Calls postsolve() on all theories. */ void postsolve(); @@ -515,9 +271,14 @@ class TheoryEngine { */ void notifyRestart(); - void getPropagatedLiterals(std::vector<TNode>& literals) { - for (; d_propagatedLiteralsIndex < d_propagatedLiterals.size(); d_propagatedLiteralsIndex = d_propagatedLiteralsIndex + 1) { - Debug("getPropagatedLiterals") << "TheoryEngine::getPropagatedLiterals: propagating: " << d_propagatedLiterals[d_propagatedLiteralsIndex] << std::endl; + void getPropagatedLiterals(std::vector<TNode>& literals) + { + for (; d_propagatedLiteralsIndex < d_propagatedLiterals.size(); + d_propagatedLiteralsIndex = d_propagatedLiteralsIndex + 1) + { + Debug("getPropagatedLiterals") + << "TheoryEngine::getPropagatedLiterals: propagating: " + << d_propagatedLiterals[d_propagatedLiteralsIndex] << std::endl; literals.push_back(d_propagatedLiterals[d_propagatedLiteralsIndex]); } } @@ -569,7 +330,8 @@ class TheoryEngine { * @returns the theory, or NULL if the TNode is * of built-in type. */ - inline theory::Theory* theoryOf(TNode node) const { + theory::Theory* theoryOf(TNode node) const + { return d_theoryTable[theory::Theory::theoryOf(node)]; } @@ -578,12 +340,14 @@ class TheoryEngine { * * @returns the theory */ - inline theory::Theory* theoryOf(theory::TheoryId theoryId) const { + theory::Theory* theoryOf(theory::TheoryId theoryId) const + { Assert(theoryId < theory::THEORY_LAST); return d_theoryTable[theoryId]; } - inline bool isTheoryEnabled(theory::TheoryId theoryId) const { + bool isTheoryEnabled(theory::TheoryId theoryId) const + { return d_logicInfo.isTheoryEnabled(theoryId); } /** get the logic info used by this theory engine */ @@ -648,26 +412,278 @@ class TheoryEngine { */ bool isFiniteType(TypeNode tn) const; //---------------------- end information about cardinality of types + + theory::SortInference* getSortInference() { return d_sortInfer.get(); } + + /** Prints the assertions to the debug stream */ + void printAssertions(const char* tag); + + /** + * Check that the theory assertions are satisfied in the model. + * This function is called from the smt engine's checkModel routine. + */ + void checkTheoryAssertionsWithModel(bool hardFailure); + private: + typedef context:: + CDHashMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> + PropagationMap; + + /** + * Called by the theories to notify of a conflict. + * + * @param conflict The trust node containing the conflict and its proof + * generator (if it exists), + * @param theoryId The theory that sent the conflict + */ + void conflict(TrustNode conflict, theory::TheoryId theoryId); + + /** set in conflict */ + void markInConflict(); + + /** + * Called by the theories to notify that the current branch is incomplete. + */ + void setIncomplete(theory::TheoryId theory, theory::IncompleteId id); + + /** + * Called by the output channel to propagate literals and facts + * @return false if immediate conflict + */ + bool propagate(TNode literal, theory::TheoryId theory); + + /** + * Internal method to call the propagation routines and collect the + * propagated literals. + */ + void propagate(theory::Theory::Effort effort); + + /** + * Assert the formula to the given theory. + * @param assertion the assertion to send (not necesserily normalized) + * @param original the assertion as it was sent in from the propagating theory + * @param toTheoryId the theory to assert to + * @param fromTheoryId the theory that sent it + */ + void assertToTheory(TNode assertion, + TNode originalAssertion, + theory::TheoryId toTheoryId, + theory::TheoryId fromTheoryId); + + /** + * Marks a theory propagation from a theory to a theory where a + * theory could be the THEORY_SAT_SOLVER for literals coming from + * or being propagated to the SAT solver. If the receiving theory + * already recieved the literal, the method returns false, otherwise + * it returns true. + * + * @param assertion the normalized assertion being sent + * @param originalAssertion the actual assertion that was sent + * @param toTheoryId the theory that is on the receiving end + * @param fromTheoryId the theory that sent the assertion + * @return true if a new assertion, false if theory already got it + */ + bool markPropagation(TNode assertion, + TNode originalAssertions, + theory::TheoryId toTheoryId, + theory::TheoryId fromTheoryId); + + /** + * Computes the explanation by traversing the propagation graph and + * asking relevant theories to explain the propagations. Initially + * the explanation vector should contain only the element (node, theory) + * where the node is the one to be explained, and the theory is the + * theory that sent the literal. + */ + TrustNode getExplanation(std::vector<NodeTheoryPair>& explanationVector); + + /** Are proofs enabled? */ + bool isProofEnabled() const; + + /** + * Get a pointer to the rewriter owned by the associated Env. + */ + theory::Rewriter* getRewriter(); + + /** + * Adds a new lemma, returning its status. + * @param node the lemma + * @param p the properties of the lemma. + * @param atomsTo the theory that atoms of the lemma should be sent to + * @param from the theory that sent the lemma + */ + void lemma(TrustNode node, + theory::LemmaProperty p, + theory::TheoryId from = theory::THEORY_LAST); + + /** Ensure atoms from the given node are sent to the given theory */ + void ensureLemmaAtoms(TNode n, theory::TheoryId atomsTo); + /** Ensure that the given atoms are sent to the given theory */ + void ensureLemmaAtoms(const std::vector<TNode>& atoms, + theory::TheoryId atomsTo); /** Dump the assertions to the dump */ void dumpAssertions(const char* tag); - /** For preprocessing pass lifting bit-vectors of size 1 to booleans */ -public: - theory::SortInference* getSortInference() { return d_sortInfer.get(); } + /** Associated PropEngine engine */ + prop::PropEngine* d_propEngine; - /** Prints the assertions to the debug stream */ - void printAssertions(const char* tag); + /** + * Reference to the environment. + */ + Env& d_env; - public: + /** + * A table of from theory IDs to theory pointers. Never use this table + * directly, use theoryOf() instead. + */ + theory::Theory* d_theoryTable[theory::THEORY_LAST]; /** - * Check that the theory assertions are satisfied in the model. - * This function is called from the smt engine's checkModel routine. + * A collection of theories that are "active" for the current run. + * This set is provided by the user (as a logic string, say, in SMT-LIBv2 + * format input), or else by default it's all-inclusive. This is important + * because we can optimize for single-theory runs (no sharing), can reduce + * the cost of walking the DAG on registration, etc. */ - void checkTheoryAssertionsWithModel(bool hardFailure); -};/* class TheoryEngine */ + const LogicInfo& d_logicInfo; + + /** The separation logic location and data types */ + TypeNode d_sepLocType; + TypeNode d_sepDataType; + + //--------------------------------- new proofs + /** Proof node manager used by this theory engine, if proofs are enabled */ + ProofNodeManager* d_pnm; + /** The lazy proof object + * + * This stores instructions for how to construct proofs for all theory lemmas. + */ + std::shared_ptr<LazyCDProof> d_lazyProof; + /** The proof generator */ + std::shared_ptr<TheoryEngineProofGenerator> d_tepg; + //--------------------------------- end new proofs + /** The combination manager we are using */ + std::unique_ptr<theory::CombinationEngine> d_tc; + /** The shared solver of the above combination engine. */ + theory::SharedSolver* d_sharedSolver; + /** The quantifiers engine, which is owned by the quantifiers theory */ + theory::QuantifiersEngine* d_quantEngine; + /** + * The decision manager + */ + std::unique_ptr<theory::DecisionManager> d_decManager; + /** The relevance manager */ + std::unique_ptr<theory::RelevanceManager> d_relManager; + /** + * An empty set of relevant assertions, which is returned as a dummy value for + * getRelevantAssertions when relevance is disabled. + */ + std::unordered_set<TNode> d_emptyRelevantSet; + + /** are we in eager model building mode? (see setEagerModelBuilding). */ + bool d_eager_model_building; + + /** + * Output channels for individual theories. + */ + theory::EngineOutputChannel* d_theoryOut[theory::THEORY_LAST]; + + /** + * Are we in conflict. + */ + context::CDO<bool> d_inConflict; + + /** + * Are we in "SAT mode"? In this state, the user can query for the model. + * This corresponds to the state in Figure 4.1, page 52 of the SMT-LIB + * standard, version 2.6. + */ + bool d_inSatMode; + + /** + * Debugging flag to ensure that shutdown() is called before the + * destructor. + */ + bool d_hasShutDown; + + /** + * True if a theory has notified us of incompleteness (at this + * context level or below). + */ + context::CDO<bool> d_incomplete; + /** The theory and identifier that (most recently) set incomplete */ + context::CDO<theory::TheoryId> d_incompleteTheory; + context::CDO<theory::IncompleteId> d_incompleteId; + + /** + * Mapping of propagations from recievers to senders. + */ + PropagationMap d_propagationMap; + + /** + * Timestamp of propagations + */ + context::CDO<size_t> d_propagationMapTimestamp; + + /** + * Literals that are propagated by the theory. Note that these are TNodes. + * The theory can only propagate nodes that have an assigned literal in the + * SAT solver and are hence referenced in the SAT solver. + */ + context::CDList<TNode> d_propagatedLiterals; + + /** + * The index of the next literal to be propagated by a theory. + */ + context::CDO<unsigned> d_propagatedLiteralsIndex; + + /** + * A variable to mark if we added any lemmas. + */ + bool d_lemmasAdded; + + /** + * A variable to mark if the OutputChannel was "used" by any theory + * since the start of the last check. If it has been, we require + * a FULL_EFFORT check before exiting and reporting SAT. + * + * See the documentation for the needCheck() function, below. + */ + bool d_outputChannelUsed; + + /** Atom requests from lemmas */ + AtomRequests d_atomRequests; + + /** sort inference module */ + std::unique_ptr<theory::SortInference> d_sortInfer; + + /** Time spent in theory combination */ + TimerStat d_combineTheoriesTime; + + Node d_true; + Node d_false; + + /** Whether we were just interrupted (or not) */ + bool d_interrupted; + + /** + * Queue of nodes for pre-registration. + */ + std::queue<TNode> d_preregisterQueue; + + /** + * Boolean flag denoting we are in pre-registration. + */ + bool d_inPreregister; + + /** + * Did the theories get any new facts since the last time we called + * check() + */ + context::CDO<bool> d_factsAsserted; + +}; /* class TheoryEngine */ } // namespace cvc5 |