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/smt_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/smt_solver.cpp')
| -rw-r--r-- | src/smt/smt_solver.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
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 |