From 145b99d771e182fba70402398702ed12e3303682 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 28 Jan 2021 15:58:17 -0600 Subject: [PATCH] Reorganize calls to quantifiers engine from SmtEngine layer (#5828) This reorganizes calls to QuantifiersEngine from SmtEngine. Our policy has changed recently that the SmtEngine layer is allowed to make calls directly to QuantifiersEngine, which eliminates the need for TheoryEngine to have forwarding calls. This PR makes this policy more consistent. This also makes quantifier-specific calls more safe by throwing modal exceptions in the cases where quantifiers are present. Marking "major" since we currently segfault when e.g. dumping instantiations in non-quantified logics. This PR makes it so that we throw a modal exception. --- src/smt/smt_engine.cpp | 35 ++++++++++++++++++++--------------- src/smt/smt_engine.h | 12 +++++++++++- src/smt/smt_solver.cpp | 6 ++++++ src/smt/smt_solver.h | 6 ++++++ src/smt/sygus_solver.cpp | 22 +++++++++++++++++----- src/smt/sygus_solver.h | 5 +++++ src/theory/theory_engine.cpp | 20 -------------------- src/theory/theory_engine.h | 20 -------------------- 8 files changed, 65 insertions(+), 61 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 19fa8dc34..4d3665da6 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -844,6 +844,18 @@ Model* SmtEngine::getAvailableModel(const char* c) const return d_model.get(); } +QuantifiersEngine* SmtEngine::getAvailableQuantifiersEngine(const char* c) const +{ + QuantifiersEngine* qe = d_smtSolver->getQuantifiersEngine(); + if (qe == nullptr) + { + std::stringstream ss; + ss << "Cannot " << c << " when quantifiers are not present."; + throw ModalException(ss.str().c_str()); + } + return qe; +} + void SmtEngine::notifyPushPre() { d_smtSolver->processAssertions(*d_asserts); } void SmtEngine::notifyPushPost() @@ -1533,9 +1545,7 @@ void SmtEngine::printInstantiations( std::ostream& out ) { out << "% SZS output start Proof for " << d_state->getFilename() << std::endl; } - TheoryEngine* te = getTheoryEngine(); - Assert(te != nullptr); - QuantifiersEngine* qe = te->getQuantifiersEngine(); + QuantifiersEngine* qe = getAvailableQuantifiersEngine("printInstantiations"); // First, extract and print the skolemizations bool printed = false; @@ -1611,9 +1621,8 @@ void SmtEngine::getInstantiationTermVectors( } else { - TheoryEngine* te = getTheoryEngine(); - Assert(te != nullptr); - QuantifiersEngine* qe = te->getQuantifiersEngine(); + QuantifiersEngine* qe = + getAvailableQuantifiersEngine("getInstantiationTermVectors"); // otherwise, just get the list of all instantiations qe->getInstantiationTermVectors(insts); } @@ -1622,9 +1631,7 @@ void SmtEngine::getInstantiationTermVectors( void SmtEngine::printSynthSolution( std::ostream& out ) { SmtScope smts(this); finishInit(); - TheoryEngine* te = getTheoryEngine(); - Assert(te != nullptr); - te->printSynthSolution(out); + d_sygusSolver->printSynthSolution(out); } bool SmtEngine::getSynthSolutions(std::map& solMap) @@ -1686,9 +1693,8 @@ bool SmtEngine::getAbduct(const Node& conj, Node& abd) void SmtEngine::getInstantiatedQuantifiedFormulas(std::vector& qs) { SmtScope smts(this); - TheoryEngine* te = getTheoryEngine(); - Assert(te != nullptr); - QuantifiersEngine* qe = te->getQuantifiersEngine(); + QuantifiersEngine* qe = + getAvailableQuantifiersEngine("getInstantiatedQuantifiedFormulas"); qe->getInstantiatedQuantifiedFormulas(qs); } @@ -1696,9 +1702,8 @@ void SmtEngine::getInstantiationTermVectors( Node q, std::vector>& tvecs) { SmtScope smts(this); - TheoryEngine* te = getTheoryEngine(); - Assert(te != nullptr); - QuantifiersEngine* qe = te->getQuantifiersEngine(); + QuantifiersEngine* qe = + getAvailableQuantifiersEngine("getInstantiationTermVectors"); qe->getInstantiationTermVectors(q, tvecs); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index a392e8c42..a1fc809e4 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -127,6 +127,7 @@ ProofManager* currentProofManager(); namespace theory { class TheoryModel; class Rewriter; + class QuantifiersEngine; }/* CVC4::theory namespace */ @@ -972,10 +973,19 @@ class CVC4_PUBLIC SmtEngine * by this class is currently available, which means that CVC4 is producing * models, and is in "SAT mode", otherwise a recoverable exception is thrown. * - * The flag c is used for giving an error message to indicate the context + * @param c used for giving an error message to indicate the context * this method was called. */ smt::Model* 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. + * getInstantiatedQuantifiedFormulas) is called in a non-quantified logic. + * + * @param c used for giving an error message to indicate the context + * this method was called. + */ + theory::QuantifiersEngine* getAvailableQuantifiersEngine(const char* c) const; // --------------------------------------- callbacks from the state /** diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 3e8d0f147..433eb9cd0 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -258,6 +258,12 @@ TheoryEngine* SmtSolver::getTheoryEngine() { return d_theoryEngine.get(); } prop::PropEngine* SmtSolver::getPropEngine() { return d_propEngine.get(); } +theory::QuantifiersEngine* SmtSolver::getQuantifiersEngine() +{ + Assert(d_theoryEngine != nullptr); + return d_theoryEngine->getQuantifiersEngine(); +} + Preprocessor* SmtSolver::getPreprocessor() { return &d_pp; } } // namespace smt diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h index 8b6ca3021..97525224d 100644 --- a/src/smt/smt_solver.h +++ b/src/smt/smt_solver.h @@ -34,6 +34,10 @@ namespace prop { class PropEngine; } +namespace theory { +class QuantifiersEngine; +} + namespace smt { class Assertions; @@ -119,6 +123,8 @@ class SmtSolver TheoryEngine* getTheoryEngine(); /** Get a pointer to the PropEngine owned by this solver. */ prop::PropEngine* getPropEngine(); + /** Get a pointer to the QuantifiersEngine owned by this solver. */ + theory::QuantifiersEngine* getQuantifiersEngine(); /** Get a pointer to the preprocessor */ Preprocessor* getPreprocessor(); //------------------------------------------ end access methods diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index a3a976d4a..44941fc46 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -24,6 +24,7 @@ #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/sygus_utils.h" +#include "theory/quantifiers_engine.h" #include "theory/smt_engine_subsolver.h" using namespace CVC4::theory; @@ -228,9 +229,8 @@ bool SygusSolver::getSynthSolutions(std::map& sol_map) Trace("smt") << "SygusSolver::getSynthSolutions" << std::endl; std::map> sol_mapn; // fail if the theory engine does not have synthesis solutions - TheoryEngine* te = d_smtSolver.getTheoryEngine(); - Assert(te != nullptr); - if (!te->getSynthSolutions(sol_mapn)) + QuantifiersEngine* qe = d_smtSolver.getQuantifiersEngine(); + if (qe == nullptr || !qe->getSynthSolutions(sol_mapn)) { return false; } @@ -244,6 +244,18 @@ bool SygusSolver::getSynthSolutions(std::map& sol_map) return true; } +void SygusSolver::printSynthSolution(std::ostream& out) +{ + QuantifiersEngine* qe = d_smtSolver.getQuantifiersEngine(); + if (qe == nullptr) + { + InternalError() + << "SygusSolver::printSynthSolution(): Cannot print synth solution in " + "the current logic, which does not include quantifiers"; + } + qe->printSynthSolution(out); +} + void SygusSolver::checkSynthSolution(Assertions& as) { NodeManager* nm = NodeManager::currentNM(); @@ -251,8 +263,8 @@ void SygusSolver::checkSynthSolution(Assertions& as) << std::endl; std::map> sol_map; // Get solutions and build auxiliary vectors for substituting - TheoryEngine* te = d_smtSolver.getTheoryEngine(); - if (!te->getSynthSolutions(sol_map)) + QuantifiersEngine* qe = d_smtSolver.getQuantifiersEngine(); + if (qe == nullptr || !qe->getSynthSolutions(sol_map)) { InternalError() << "SygusSolver::checkSynthSolution(): No solution to check!"; diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h index b0670ea27..9e1be5de7 100644 --- a/src/smt/sygus_solver.h +++ b/src/smt/sygus_solver.h @@ -136,6 +136,11 @@ class SygusSolver * is a valid formula. */ bool getSynthSolutions(std::map& sol_map); + /** + * Print solution for synthesis conjectures found by counter-example guided + * instantiation module. + */ + void printSynthSolution(std::ostream& out); private: /** diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 3492f97a9..bd03a4d03 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -692,17 +692,6 @@ bool TheoryEngine::buildModel() return d_tc->buildModel(); } -bool TheoryEngine::getSynthSolutions( - std::map>& sol_map) -{ - if (d_quantEngine) - { - return d_quantEngine->getSynthSolutions(sol_map); - } - // we are not in a quantified logic, there is no synthesis solution - return false; -} - bool TheoryEngine::presolve() { // Reset the interrupt flag d_interrupted = false; @@ -1161,15 +1150,6 @@ Node TheoryEngine::getModelValue(TNode var) { return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var); } -void TheoryEngine::printSynthSolution( std::ostream& out ) { - if( d_quantEngine ){ - d_quantEngine->printSynthSolution( out ); - }else{ - out << "Internal error : synth solution not available when quantifiers are not present." << std::endl; - Assert(false); - } -} - TrustNode TheoryEngine::getExplanation(TNode node) { Debug("theory::explain") << "TheoryEngine::getExplanation(" << node diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 46498e71a..1a9447681 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -584,22 +584,6 @@ class TheoryEngine { */ void setEagerModelBuilding() { d_eager_model_building = true; } - /** get synth solutions - * - * This method returns true if there is a synthesis solution available. This - * is the case if the last call to check satisfiability originated in a - * check-synth call, and the synthesis solver successfully found a solution - * for all active synthesis conjectures. - * - * This method adds entries to sol_map that map functions-to-synthesize with - * their solutions, for all active conjectures. This should be called - * immediately after the solver answers unsat for sygus input. - * - * For details on what is added to sol_map, see - * SynthConjecture::getSynthSolutions. - */ - bool getSynthSolutions(std::map >& sol_map); - /** * Get the theory associated to a given Node. * @@ -646,10 +630,6 @@ class TheoryEngine { * has (or null if none); */ Node getModelValue(TNode var); - /** - * Print solution for synthesis conjectures found by ce_guided_instantiation module - */ - void printSynthSolution( std::ostream& out ); /** * Forwards an entailment check according to the given theoryOfMode. -- 2.30.2