diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-09-03 11:33:27 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-03 09:33:27 -0700 |
commit | 39dd4cf7678da7bbce2a0aaf4d9b44d3f885ea49 (patch) | |
tree | 764de9c5b2d9ae292d6329cea925fef53f6548f6 /src/smt/smt_engine.cpp | |
parent | 8e2c02201d30b5715a095ffe0098dd74a636ac85 (diff) |
Eliminate backwards ref to SmtEngine from abduction and interpol solvers (#7133)
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 72268aa03..582ca0c2c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -255,12 +255,12 @@ void SmtEngine::finishInit() // subsolvers if (d_env->getOptions().smt.produceAbducts) { - d_abductSolver.reset(new AbductionSolver(*d_env.get(), this)); + d_abductSolver.reset(new AbductionSolver(*d_env.get())); } if (d_env->getOptions().smt.produceInterpols != options::ProduceInterpols::NONE) { - d_interpolSolver.reset(new InterpolationSolver(*d_env.get(), this)); + d_interpolSolver.reset(new InterpolationSolver(*d_env.get())); } d_pp->finishInit(); @@ -1754,7 +1754,9 @@ bool SmtEngine::getInterpol(const Node& conj, { SmtScope smts(this); finishInit(); - bool success = d_interpolSolver->getInterpol(conj, grammarType, interpol); + std::vector<Node> axioms = getExpandedAssertions(); + bool success = + d_interpolSolver->getInterpol(axioms, conj, grammarType, interpol); // notify the state of whether the get-interpol call was successfuly, which // impacts the SMT mode. d_state->notifyGetInterpol(success); @@ -1773,7 +1775,8 @@ bool SmtEngine::getAbduct(const Node& conj, { SmtScope smts(this); finishInit(); - bool success = d_abductSolver->getAbduct(conj, grammarType, abd); + std::vector<Node> axioms = getExpandedAssertions(); + bool success = d_abductSolver->getAbduct(axioms, conj, grammarType, abd); // notify the state of whether the get-abduct call was successfuly, which // impacts the SMT mode. d_state->notifyGetAbduct(success); |