From e91077d81183c6c54ff0fdad5c6eb160f16c4205 Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Tue, 20 Oct 2020 20:28:35 -0500 Subject: [PATCH] Add finishInit for getInterpol and getAbduct. (#5316) This PR removes d_subSolver from SygusInterpol class. findInterpol function now receives the sub-solver as input (possibly through solveInterpolation function). In addition, finishInit is now called for getAbduct and getInterpol functions in smt_engine.cpp. --- src/smt/interpolation_solver.cpp | 2 +- src/smt/smt_engine.cpp | 2 ++ .../quantifiers/sygus/sygus_interpol.cpp | 23 ++++++------ src/theory/quantifiers/sygus/sygus_interpol.h | 36 +++++++++---------- 4 files changed, 31 insertions(+), 32 deletions(-) diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp index ffcb09a23..c47d99951 100644 --- a/src/smt/interpolation_solver.cpp +++ b/src/smt/interpolation_solver.cpp @@ -50,7 +50,7 @@ bool InterpolationSolver::getInterpol(const Node& conj, std::string name("A"); quantifiers::SygusInterpol interpolSolver; - if (interpolSolver.SolveInterpolation( + if (interpolSolver.solveInterpolation( name, axioms, conjn, grammarType, interpol)) { if (options::checkInterpols()) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 343b79966..f345bee2e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1593,6 +1593,7 @@ bool SmtEngine::getInterpol(const Node& conj, Node& interpol) { SmtScope smts(this); + finishInit(); bool success = d_interpolSolver->getInterpol(conj, grammarType, interpol); // notify the state of whether the get-interpol call was successfuly, which // impacts the SMT mode. @@ -1611,6 +1612,7 @@ bool SmtEngine::getAbduct(const Node& conj, Node& abd) { SmtScope smts(this); + finishInit(); bool success = d_abductSolver->getAbduct(conj, grammarType, abd); // notify the state of whether the get-abduct call was successfuly, which // impacts the SMT mode. diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index c58d77a9b..e4e7a02c7 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -268,11 +268,11 @@ void SygusInterpol::mkSygusConjecture(Node itp, Trace("sygus-interpol") << "Generate: " << d_sygusConj << std::endl; } -bool SygusInterpol::findInterpol(Node& interpol, Node itp) +bool SygusInterpol::findInterpol(SmtEngine* subSolver, Node& interpol, Node itp) { // get the synthesis solution std::map sols; - d_subSolver->getSynthSolutions(sols); + subSolver->getSynthSolutions(sols); Assert(sols.size() == 1); std::map::iterator its = sols.find(itp); if (its == sols.end()) @@ -313,43 +313,44 @@ bool SygusInterpol::findInterpol(Node& interpol, Node itp) return true; } -bool SygusInterpol::SolveInterpolation(const std::string& name, +bool SygusInterpol::solveInterpolation(const std::string& name, const std::vector& axioms, const Node& conj, const TypeNode& itpGType, Node& interpol) { - initializeSubsolver(d_subSolver); + std::unique_ptr subSolver; + initializeSubsolver(subSolver); // get the logic - LogicInfo l = d_subSolver->getLogicInfo().getUnlockedCopy(); + LogicInfo l = subSolver->getLogicInfo().getUnlockedCopy(); // enable everything needed for sygus l.enableSygus(); - d_subSolver->setLogic(l); + subSolver->setLogic(l); collectSymbols(axioms, conj); createVariables(itpGType.isNull()); for (Node var : d_vars) { - d_subSolver->declareSygusVar(name, var, var.getType()); + subSolver->declareSygusVar(name, var, var.getType()); } std::vector vars_empty; TypeNode grammarType = setSynthGrammar(itpGType, axioms, conj); Node itp = mkPredicate(name); - d_subSolver->declareSynthFun(name, itp, grammarType, false, vars_empty); + subSolver->declareSynthFun(name, itp, grammarType, false, vars_empty); mkSygusConjecture(itp, axioms, conj); Trace("sygus-interpol") << "SmtEngine::getInterpol: made conjecture : " << d_sygusConj << ", solving for " << d_sygusConj[0][0] << std::endl; - d_subSolver->assertSygusConstraint(d_sygusConj); + subSolver->assertSygusConstraint(d_sygusConj); Trace("sygus-interpol") << " SmtEngine::getInterpol check sat..." << std::endl; - Result r = d_subSolver->checkSynth(); + Result r = subSolver->checkSynth(); Trace("sygus-interpol") << " SmtEngine::getInterpol result: " << r << std::endl; if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) { - return findInterpol(interpol, itp); + return findInterpol(subSolver.get(), interpol, itp); } return false; } diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h index 4e126032b..916f2d9b5 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.h +++ b/src/theory/quantifiers/sygus/sygus_interpol.h @@ -40,6 +40,20 @@ namespace quantifiers { * shared between Fa and Fc. In other words, A( x ) must be implied by our * axioms Fa( x ) and implies Fc( x ). Then, to solve the interpolation problem, * we just need to synthesis A( x ). + * + * This class uses a fresh copy of the SMT engine which is used for solving the + * interpolation problem. In particular, consider the input: (assert A) + * (get-interpol s B) + * In the copy of the SMT engine where these commands are issued, we maintain + * A in the assertion stack. In solving the interpolation problem, we will + * need to call a SMT engine solver with a different assertion stack, which is + * a sygus conjecture build from A and B. Then to solve the interpolation + * problem, instead of modifying the assertion stack to remove A and add the + * sygus conjecture (exists I. ...), we invoke a fresh copy of the SMT engine + * and leave the original assertion stack unchanged. This copy of the SMT + * engine will have the assertion stack with the sygus conjecture. This copy + * of the SMT engine can be further queried for information regarding further + * solutions. */ class SygusInterpol { @@ -59,7 +73,7 @@ class SygusInterpol * grammar that should be used for solutions of the interpolation conjecture. * @interpol the solution to the sygus conjecture. */ - bool SolveInterpolation(const std::string& name, + bool solveInterpolation(const std::string& name, const std::vector& axioms, const Node& conj, const TypeNode& itpGType, @@ -156,25 +170,7 @@ class SygusInterpol * @param interpol the solution to the sygus conjecture. * @param itp the interpolation predicate. */ - bool findInterpol(Node& interpol, Node itp); - - /** The SMT engine subSolver - * - * This is a fresh copy of the SMT engine which is used for solving the - * interpolation problem. In particular, consider the input: (assert A) - * (get-interpol s B) - * In the copy of the SMT engine where these commands are issued, we maintain - * A in the assertion stack. In solving the interpolation problem, we will - * need to call a SMT engine solver with a different assertion stack, which is - * a sygus conjecture build from A and B. Then to solve the interpolation - * problem, instead of modifying the assertion stack to remove A and add the - * sygus conjecture (exists I. ...), we invoke a fresh copy of the SMT engine - * and leave the original assertion stack unchanged. This copy of the SMT - * engine will have the assertion stack with the sygus conjecture. This copy - * of the SMT engine can be further queried for information regarding further - * solutions. - */ - std::unique_ptr d_subSolver; + bool findInterpol(SmtEngine* subsolver, Node& interpol, Node itp); /** * symbols from axioms and conjecture. -- 2.30.2