From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 18 Jul 2022 18:09:43 +0000 (-0500)
Subject: Fix global-declarations with abduction (#8961)
X-Git-Tag: cvc5-1.0.1~3
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=32a4d1cc8ba9b51be4c2af4aa5ba5025c645a2e0;p=cvc5.git

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 90e98e21f..c8d4acf42 100644
--- 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 63076c61f..c042780ed 100644
--- 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 e6a804653..fdebee42a 100644
--- 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 485ccb5d0..45cfe0f23 100644
--- 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 3d926c8e7..0545664b3 100644
--- 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
index 000000000..d6860e29d
--- /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)