diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-28 15:58:17 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-28 15:58:17 -0600 |
commit | 145b99d771e182fba70402398702ed12e3303682 (patch) | |
tree | 677cc444dd38af7354aa83eefad2b0ed695cf7f3 /src/smt/sygus_solver.cpp | |
parent | 2f4bae4b4ffe6e913925f3d8f2c857a01aeea3bd (diff) |
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.
Diffstat (limited to 'src/smt/sygus_solver.cpp')
-rw-r--r-- | src/smt/sygus_solver.cpp | 22 |
1 files changed, 17 insertions, 5 deletions
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!"; |