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.
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()
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;
}
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);
}
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<Node, Node>& solMap)
void SmtEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
{
SmtScope smts(this);
- TheoryEngine* te = getTheoryEngine();
- Assert(te != nullptr);
- QuantifiersEngine* qe = te->getQuantifiersEngine();
+ QuantifiersEngine* qe =
+ getAvailableQuantifiersEngine("getInstantiatedQuantifiedFormulas");
qe->getInstantiatedQuantifiedFormulas(qs);
}
Node q, std::vector<std::vector<Node>>& tvecs)
{
SmtScope smts(this);
- TheoryEngine* te = getTheoryEngine();
- Assert(te != nullptr);
- QuantifiersEngine* qe = te->getQuantifiersEngine();
+ QuantifiersEngine* qe =
+ getAvailableQuantifiersEngine("getInstantiationTermVectors");
qe->getInstantiationTermVectors(q, tvecs);
}
namespace theory {
class TheoryModel;
class Rewriter;
+ class QuantifiersEngine;
}/* CVC4::theory namespace */
* 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
/**
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
class PropEngine;
}
+namespace theory {
+class QuantifiersEngine;
+}
+
namespace smt {
class Assertions;
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
#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;
Trace("smt") << "SygusSolver::getSynthSolutions" << std::endl;
std::map<Node, std::map<Node, Node>> 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;
}
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();
<< std::endl;
std::map<Node, std::map<Node, Node>> 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!";
* is a valid formula.
*/
bool getSynthSolutions(std::map<Node, Node>& sol_map);
+ /**
+ * Print solution for synthesis conjectures found by counter-example guided
+ * instantiation module.
+ */
+ void printSynthSolution(std::ostream& out);
private:
/**
return d_tc->buildModel();
}
-bool TheoryEngine::getSynthSolutions(
- std::map<Node, std::map<Node, Node>>& 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;
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
*/
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<Node, std::map<Node, Node> >& sol_map);
-
/**
* Get the theory associated to a given Node.
*
* 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.
projects / cvc5.git / commitdiff