summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/smt_engine.cpp35
-rw-r--r--src/smt/smt_engine.h12
-rw-r--r--src/smt/smt_solver.cpp6
-rw-r--r--src/smt/smt_solver.h6
-rw-r--r--src/smt/sygus_solver.cpp22
-rw-r--r--src/smt/sygus_solver.h5
-rw-r--r--src/theory/theory_engine.cpp20
-rw-r--r--src/theory/theory_engine.h20
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<Node, Node>& solMap)
@@ -1686,9 +1693,8 @@ bool SmtEngine::getAbduct(const Node& conj, Node& abd)
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);
}
@@ -1696,9 +1702,8 @@ void SmtEngine::getInstantiationTermVectors(
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);
}
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<Node, Node>& sol_map)
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;
}
@@ -244,6 +244,18 @@ bool SygusSolver::getSynthSolutions(std::map<Node, Node>& 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<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!";
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<Node, Node>& 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<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;
@@ -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<Node, std::map<Node, Node> >& 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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback