diff options
author | Ying Sheng <sqy1415@gmail.com> | 2020-09-15 09:47:15 +0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-14 20:47:15 -0500 |
commit | 51be2e14c632d45e63a40659dea2177133251dfa (patch) | |
tree | d47380a72d05dc3ede4d61f4c04f9e4034b791fc /src/smt/smt_engine.cpp | |
parent | 9e2a36f53007b932412a98c8e7ff1556a53f37c5 (diff) |
Interpolation: Add implementation for SyGuS interpolation module (final) (#5063)
Add interface for SyGuS Interpolation module. Adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack.
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7f824bff3..d271ca05d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -75,6 +75,7 @@ #include "smt/defined_function.h" #include "smt/dump_manager.h" #include "smt/expr_names.h" +#include "smt/interpolation_solver.h" #include "smt/listeners.h" #include "smt/logic_request.h" #include "smt/model_blocker.h" @@ -134,6 +135,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr) d_definedFunctions(nullptr), d_sygusSolver(nullptr), d_abductSolver(nullptr), + d_interpolSolver(nullptr), d_quantElimSolver(nullptr), d_assignments(nullptr), d_logic(), @@ -299,6 +301,10 @@ void SmtEngine::finishInit() { d_abductSolver.reset(new AbductionSolver(this)); } + if (options::produceInterpols() != options::ProduceInterpols::NONE) + { + d_interpolSolver.reset(new InterpolationSolver(this)); + } d_pp->finishInit(); @@ -1755,12 +1761,6 @@ void SmtEngine::checkModel(bool hardFailure) { Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl; } -void SmtEngine::checkInterpol(Expr interpol, - const std::vector<Expr>& easserts, - const Node& conj) -{ -} - // TODO(#1108): Simplify the error reporting of this method. UnsatCore SmtEngine::getUnsatCore() { Trace("smt") << "SMT getUnsatCore()" << endl; @@ -1818,7 +1818,11 @@ bool SmtEngine::getInterpol(const Node& conj, const TypeNode& grammarType, Node& interpol) { - return false; + bool success = d_interpolSolver->getInterpol(conj, grammarType, interpol); + // notify the state of whether the get-interpol call was successfuly, which + // impacts the SMT mode. + d_state->notifyGetInterpol(success); + return success; } bool SmtEngine::getInterpol(const Node& conj, Node& interpol) |