From 32a4d1cc8ba9b51be4c2af4aa5ba5025c645a2e0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 18 Jul 2022 13:09:43 -0500 Subject: [PATCH] Fix global-declarations with abduction (#8961) FYI @arjunvish The same issue would lead to issues when using global-declarations with interpolation or block-models. --- src/smt/abduction_solver.cpp | 1 + src/smt/preprocessor.cpp | 1 + src/smt/solver_engine.cpp | 10 ++++++++-- src/theory/sets/theory_sets_private.cpp | 2 -- test/regress/cli/CMakeLists.txt | 1 + .../regress1/abduction/arjun-global-dec.smt2 | 18 ++++++++++++++++++ 6 files changed, 29 insertions(+), 4 deletions(-) create mode 100644 test/regress/cli/regress1/abduction/arjun-global-dec.smt2 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& 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 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 SolverEngine::getSepHeapAndNilExpr(void) std::vector SolverEngine::getAssertionsInternal() const { Assert(d_state->isFullyInited()); + // ensure that global declarations are processed + d_asserts->refresh(); const CDList& al = d_asserts->getAssertionList(); std::vector 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 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 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) -- 2.30.2