Fixes for get-abduct (#3229)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1827d902cfcb6d7eff659fe5896bfa9830fd6f98..3c10516e45f83ff7b94cdd6d9f1aacd6e12e4926 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -5127,7 +5127,7 @@ bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd)
   }
   Trace("sygus-abduct") << "SmtEngine::getAbduct: conjecture " << conj
                         << std::endl;
-  std::vector<Expr> easserts = getAssertions();
+  std::vector<Expr> easserts = getExpandedAssertions();
   std::vector<Node> axioms;
   for (unsigned i = 0, size = easserts.size(); i < size; i++)
   {
@@ -5135,7 +5135,12 @@ bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd)
   }
   std::vector<Node> asserts(axioms.begin(), axioms.end());
   // negate the conjecture
-  Node conjn = Node::fromExpr(conj).negate();
+  Node conjn = Node::fromExpr(conj);
+  // must expand definitions
+  std::unordered_map<Node, Node, NodeHashFunction> cache;
+  conjn = d_private->expandDefinitions(conjn, cache);
+  // now negate
+  conjn = conjn.negate();
   d_abdConj = conjn.toExpr();
   asserts.push_back(conjn);
   std::string name("A");

diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp
index 4f621934311c063ba1da92368f1d06f07d62ab8f..7e72ecb4123cb55e10e7e201a47b842f8760901c 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_abduct.cpp
+++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp
@@ -278,24 +278,22 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name,
   Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusVar);
   std::vector<Node> iplc;
   iplc.push_back(instAttr);
-  if (!axioms.empty())
-  {
-    Node aconj = axioms.size() == 1 ? axioms[0] : nm->mkNode(AND, axioms);
-    aconj =
-        aconj.substitute(syms.begin(), syms.end(), vars.begin(), vars.end());
-    Trace("sygus-abduct") << "---> Assumptions: " << aconj << std::endl;
-    Node sc = nm->mkNode(AND, aconj, abdApp);
-    Node vbvl = nm->mkNode(BOUND_VAR_LIST, vars);
-    sc = nm->mkNode(EXISTS, vbvl, sc);
-    Node sygusScVar = nm->mkSkolem("sygus_sc", nm->booleanType());
-    sygusScVar.setAttribute(theory::SygusSideConditionAttribute(), sc);
-    instAttr = nm->mkNode(INST_ATTRIBUTE, sygusScVar);
-    // build in the side condition
-    //   exists x. A( x ) ^ input_axioms( x )
-    // as an additional annotation on the sygus conjecture. In other words,
-    // the abducts A we procedure must be consistent with our axioms.
-    iplc.push_back(instAttr);
-  }
+  Node aconj = axioms.size() == 0
+                   ? nm->mkConst(true)
+                   : (axioms.size() == 1 ? axioms[0] : nm->mkNode(AND, axioms));
+  aconj = aconj.substitute(syms.begin(), syms.end(), vars.begin(), vars.end());
+  Trace("sygus-abduct") << "---> Assumptions: " << aconj << std::endl;
+  Node sc = nm->mkNode(AND, aconj, abdApp);
+  Node vbvl = nm->mkNode(BOUND_VAR_LIST, vars);
+  sc = nm->mkNode(EXISTS, vbvl, sc);
+  Node sygusScVar = nm->mkSkolem("sygus_sc", nm->booleanType());
+  sygusScVar.setAttribute(theory::SygusSideConditionAttribute(), sc);
+  instAttr = nm->mkNode(INST_ATTRIBUTE, sygusScVar);
+  // build in the side condition
+  //   exists x. A( x ) ^ input_axioms( x )
+  // as an additional annotation on the sygus conjecture. In other words,
+  // the abducts A we procedure must be consistent with our axioms.
+  iplc.push_back(instAttr);
   Node instAttrList = nm->mkNode(INST_PATTERN_LIST, iplc);
 
   Node fbvl = nm->mkNode(BOUND_VAR_LIST, abd);