Sygus abduction feature (#2744)

4 files changed, 6 insertions, 0 deletions

diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index b65d1c522..65678f674 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -87,9 +87,11 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
     try
     {
       checker.reset(new SmtEngine(&em));
+      checker->setIsInternalSubsolver();
       checker->setTimeLimit(options::sygusExprMinerCheckTimeout(), true);
       checker->setLogic(smt::currentSmtEngine()->getLogicInfo());
       checker->setOption("sygus-rr-synth-input", false);
+      checker->setOption("sygus-abduct", false);
       checker->setOption("input-language", "smt2");
       Expr equery = squery.toExpr().exportTo(&em, varMap);
       checker->assertFormula(equery);
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 09525712f..18722a192 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -115,6 +115,7 @@ void SygusRepairConst::initializeChecker(std::unique_ptr<SmtEngine>& checker,
     try
     {
       checker.reset(new SmtEngine(&em));
+      checker->setIsInternalSubsolver();
       checker->setTimeLimit(options::sygusRepairConstTimeout(), true);
       checker->setLogic(smt::currentSmtEngine()->getLogicInfo());
       // renable options disabled by sygus
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index e25e8a225..2e0fa75fe 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -540,6 +540,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
     Trace("cegqi-engine") << "Check side condition..." << std::endl;
     Trace("cegqi-debug") << "Check side condition : " << sc << std::endl;
     SmtEngine scSmt(nm->toExprManager());
+    scSmt.setIsInternalSubsolver();
     scSmt.setLogic(smt::currentSmtEngine()->getLogicInfo());
     scSmt.assertFormula(sc.toExpr());
     Result r = scSmt.checkSat();
@@ -572,6 +573,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
     {
       Trace("cegqi-engine") << "  *** Verify with subcall..." << std::endl;
       SmtEngine verifySmt(nm->toExprManager());
+      verifySmt.setIsInternalSubsolver();
       verifySmt.setLogic(smt::currentSmtEngine()->getLogicInfo());
       verifySmt.assertFormula(query.toExpr());
       Result r = verifySmt.checkSat();
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index d3eff1750..0623c257a 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -159,6 +159,7 @@ void SynthEngine::assignConjecture(Node q)
     {
       // create new smt engine to do quantifier elimination
       SmtEngine smt_qe(nm->toExprManager());
+      smt_qe.setIsInternalSubsolver();
       smt_qe.setLogic(smt::currentSmtEngine()->getLogicInfo());
       Trace("cegqi-qep") << "Property is non-ground single invocation, run "
                             "QE to obtain single invocation."