summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/interpolation_solver.cpp2
-rw-r--r--src/smt/smt_engine.cpp2
-rw-r--r--src/theory/quantifiers/sygus/sygus_interpol.cpp23
-rw-r--r--src/theory/quantifiers/sygus/sygus_interpol.h36
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<Node, Node> sols;
- d_subSolver->getSynthSolutions(sols);
+ subSolver->getSynthSolutions(sols);
Assert(sols.size() == 1);
std::map<Node, Node>::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<Node>& axioms,
const Node& conj,
const TypeNode& itpGType,
Node& interpol)
{
- initializeSubsolver(d_subSolver);
+ std::unique_ptr<SmtEngine> 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<Node> 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<Node>& 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<SmtEngine> d_subSolver;
+ bool findInterpol(SmtEngine* subsolver, Node& interpol, Node itp);
/**
* symbols from axioms and conjecture.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback