Fix global-declarations with abduction (#8961)

FYI @arjunvish

The same issue would lead to issues when using global-declarations with interpolation or block-models.

diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp
index 90e98e21f0cab9499baa92a1a330213924cc899d..c8d4acf4282aa4505ba964db66ead5326c9409ff 100644 (file)
--- a/src/smt/abduction_solver.cpp
+++ b/src/smt/abduction_solver.cpp
@@ -45,6 +45,7 @@ bool AbductionSolver::getAbduct(const std::vector<Node>& axioms,
     const char* msg = "Cannot get abduct when produce-abducts options is off.";
     throw ModalException(msg);
   }
+  Trace("sygus-abduct") << "Axioms: " << axioms << std::endl;
   Trace("sygus-abduct") << "SolverEngine::getAbduct: goal " << goal
                         << std::endl;
   std::vector<Node> asserts(axioms.begin(), axioms.end());

diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index 63076c61f124eaed817d39874b9ccfad825d5fe6..c042780ed9882571c68592f5cf60a401eb5ad3ff 100644 (file)
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -129,6 +129,7 @@ Node Preprocessor::expandDefinitions(const Node& node,
   }
   // apply substitutions here (without rewriting), before expanding definitions
   n = d_env.getTopLevelSubstitutions().apply(n);
+  Trace("smt-debug") << "...after top-level subs: " << n << std::endl;
   // now call expand definitions
   n = d_exDefs.expandDefinitions(n, cache);
   return n;

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index e6a8046530e61ca299980f49098326b84a67c9e5..fdebee42a62e4b121c3c23978472db87d2bea10b 100644 (file)
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -1221,6 +1221,8 @@ std::pair<Node, Node> SolverEngine::getSepHeapAndNilExpr(void)
 std::vector<Node> SolverEngine::getAssertionsInternal() const
 {
   Assert(d_state->isFullyInited());
+  // ensure that global declarations are processed
+  d_asserts->refresh();
   const CDList<Node>& al = d_asserts->getAssertionList();
   std::vector<Node> res;
   for (const Node& n : al)
@@ -1698,9 +1700,11 @@ Node SolverEngine::getInterpolant(const Node& conj, const TypeNode& grammarType)
   SolverEngineScope smts(this);
   finishInit();
   std::vector<Node> axioms = getExpandedAssertions();
+  // expand definitions in the conjecture as well
+  Node conje = d_smtSolver->getPreprocessor()->expandDefinitions(conj);
   Node interpol;
   bool success =
-      d_interpolSolver->getInterpolant(axioms, conj, grammarType, interpol);
+      d_interpolSolver->getInterpolant(axioms, conje, grammarType, interpol);
   // notify the state of whether the get-interpolant call was successfuly, which
   // impacts the SMT mode.
   d_state->notifyGetInterpol(success);
@@ -1732,8 +1736,10 @@ Node SolverEngine::getAbduct(const Node& conj, const TypeNode& grammarType)
   SolverEngineScope smts(this);
   finishInit();
   std::vector<Node> axioms = getExpandedAssertions();
+  // expand definitions in the conjecture as well
+  Node conje = d_smtSolver->getPreprocessor()->expandDefinitions(conj);
   Node abd;
-  bool success = d_abductSolver->getAbduct(axioms, conj, grammarType, abd);
+  bool success = d_abductSolver->getAbduct(axioms, conje, grammarType, abd);
   // notify the state of whether the get-abduct call was successful, which
   // impacts the SMT mode.
   d_state->notifyGetAbduct(success);

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 485ccb5d019fe0f7c854defe0d92604f527c8545..45cfe0f23b9d536a937b2923ceb4032819ac1406 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1722,8 +1722,6 @@ TrustNode TheorySetsPrivate::ppRewrite(Node node,
         NodeManager* nm = NodeManager::currentNM();
         SkolemManager* sm = nm->getSkolemManager();
         Node sk = sm->mkPurifySkolem(node[0], "univ");
-        Trace("ajr-temp") << "PURIFY " << node[0] << " returns " << sk
-                          << std::endl;
         Node eq = sk.eqNode(node[0]);
         lems.push_back(SkolemLemma(TrustNode::mkTrustLemma(eq), sk));
         Node ret = nm->mkNode(kind::SET_MINUS, sk, node[1]);

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 3d926c8e7e20ac1939039ffa543965de21ca52f9..0545664b3be1e521d25ecb73c368216e228f14b6 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -1725,6 +1725,7 @@ set(regress_1_tests
   regress1/abduction/abduct-dt.smt2
   regress1/abduction/abd-real-const.smt2
   regress1/abduction/abd-simple-conj-4.smt2
+  regress1/abduction/arjun-global-dec.smt2
   regress1/abduction/issue5848-2.smt2
   regress1/abduction/issue5848-3-trivial-no-abduct.smt2
   regress1/abduction/issue5848-4.smt2

diff --git a/test/regress/cli/regress1/abduction/arjun-global-dec.smt2 b/test/regress/cli/regress1/abduction/arjun-global-dec.smt2
new file mode 100644 (file)
index 0000000..d6860e2
--- /dev/null
+++ b/test/regress/cli/regress1/abduction/arjun-global-dec.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --produce-abducts
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+
+(set-option :produce-models true)
+(set-option :global-declarations true)
+(set-option :produce-abducts true)
+(set-option :incremental true)
+(set-logic QF_LIA)
+(declare-fun y () Int)
+(define-fun x!0 () Bool (<= 0 y))
+(declare-fun x () Int)
+(declare-fun z () Int)
+(define-fun x!1 () Int (+ z y x))
+(define-fun x!2 () Bool (<= 0 x!1))
+(assert x!0)
+(get-abduct abd x!2)
+(get-abduct-next)