From f4b57b49edd9a098f311811e460c3c5c8a344e87 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 3 Feb 2024 10:01:45 -0600 Subject: [PATCH 01/18] Simplify ProofRule::ARITH_TRICHOTOMY (#10338) Towards unifying the internal calculus to the cvc5 ALF proof signature. --- include/cvc5/cvc5_proof_rule.h | 2 +- src/proof/alf/alf_printer.cpp | 3 -- src/theory/arith/branch_and_bound.cpp | 3 +- .../arith/linear/congruence_manager.cpp | 6 ++-- src/theory/arith/linear/constraint.cpp | 6 ++-- .../arith/nl/ext/monomial_bounds_check.cpp | 6 ++-- src/theory/arith/proof_checker.cpp | 29 ++++++++++++------- 7 files changed, 28 insertions(+), 27 deletions(-) diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h index afc40a7d4a0..eba5f4c5ef7 100644 --- a/include/cvc5/cvc5_proof_rule.h +++ b/include/cvc5/cvc5_proof_rule.h @@ -1744,7 +1744,7 @@ enum ENUM(ProofRule) : uint32_t * **Arithmetic -- Trichotomy of the reals** * * .. math:: - * \inferrule{A, B \mid C}{C} + * \inferrule{A, B \mid -}{C} * * where :math:`\neg A, \neg B, C` are :math:`x < c, x = c, x > c` in some order. * Note that :math:`\neg` here denotes arithmetic negation, i.e., flipping :math:`\geq` to :math:`<` etc. diff --git a/src/proof/alf/alf_printer.cpp b/src/proof/alf/alf_printer.cpp index b30f8986420..ffb3ddf9f4a 100644 --- a/src/proof/alf/alf_printer.cpp +++ b/src/proof/alf/alf_printer.cpp @@ -439,9 +439,6 @@ void AlfPrinter::getArgsFromProofRule(const ProofNode* pn, return; } break; - case ProofRule::ARITH_TRICHOTOMY: - // argument is redundant - return; case ProofRule::INSTANTIATE: { // ignore arguments past the term vector, collect them into an sexpr diff --git a/src/theory/arith/branch_and_bound.cpp b/src/theory/arith/branch_and_bound.cpp index 09f2821abd8..c50a08c24d7 100644 --- a/src/theory/arith/branch_and_bound.cpp +++ b/src/theory/arith/branch_and_bound.cpp @@ -105,7 +105,8 @@ std::vector BranchAndBound::branchIntegerVariable(TNode var, pnm->mkNode(ProofRule::CONTRA, {pnm->mkNode(ProofRule::ARITH_TRICHOTOMY, {pnm->mkAssume(less.negate()), pfNotRawEq}, - {greater}), + {}, + greater), pnm->mkAssume(greater.negate())}, {}); std::vector assumptions = { diff --git a/src/theory/arith/linear/congruence_manager.cpp b/src/theory/arith/linear/congruence_manager.cpp index 5d584b3fe58..2f6ae20124e 100644 --- a/src/theory/arith/linear/congruence_manager.cpp +++ b/src/theory/arith/linear/congruence_manager.cpp @@ -188,8 +188,8 @@ void ArithCongruenceManager::watchedVariableIsZero(ConstraintCP lb, ConstraintCP if (isProofEnabled()) { pf = d_pnm->mkNode( - ProofRule::ARITH_TRICHOTOMY, {pfLb, pfUb}, {eqC->getProofLiteral()}); - pf = d_pnm->mkNode(ProofRule::MACRO_SR_PRED_TRANSFORM, {pf}, {eq}); + ProofRule::ARITH_TRICHOTOMY, {pfLb, pfUb}, {}, eqC->getProofLiteral()); + pf = d_pnm->mkNode(ProofRule::MACRO_SR_PRED_TRANSFORM, {pf}, {eq}, eq); } d_keepAlive.push_back(reason); @@ -601,7 +601,7 @@ void ArithCongruenceManager::equalsConstant(ConstraintCP lb, ConstraintCP ub){ std::shared_ptr pf; if (isProofEnabled()) { - pf = d_pnm->mkNode(ProofRule::ARITH_TRICHOTOMY, {pfLb, pfUb}, {eq}); + pf = d_pnm->mkNode(ProofRule::ARITH_TRICHOTOMY, {pfLb, pfUb}, {}, eq); } d_keepAlive.push_back(eq); d_keepAlive.push_back(reason); diff --git a/src/theory/arith/linear/constraint.cpp b/src/theory/arith/linear/constraint.cpp index edba04ada72..e50c158b965 100644 --- a/src/theory/arith/linear/constraint.cpp +++ b/src/theory/arith/linear/constraint.cpp @@ -1849,10 +1849,8 @@ std::shared_ptr Constraint::externalExplain( } case ArithProofType::TrichotomyAP: { - pf = pnm->mkNode(ProofRule::ARITH_TRICHOTOMY, - children, - {getProofLiteral()}, - getProofLiteral()); + pf = pnm->mkNode( + ProofRule::ARITH_TRICHOTOMY, children, {}, getProofLiteral()); break; } case ArithProofType::InternalAssumeAP: diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp index 37660c05096..8cbdca9eb9d 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp +++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp @@ -399,10 +399,8 @@ void MonomialBoundsCheck::checkBounds(const std::vector& asserts, {exp[1][0]}, {rb}); } - proof->addStep(simpleeq, - ProofRule::ARITH_TRICHOTOMY, - {lb, rb}, - {simpleeq}); + proof->addStep( + simpleeq, ProofRule::ARITH_TRICHOTOMY, {lb, rb}, {}); proof->addStep( tmplem[0], ProofRule::AND_INTRO, {exp[0], simpleeq}, {}); proof->addStep(tmplem[1], diff --git a/src/theory/arith/proof_checker.cpp b/src/theory/arith/proof_checker.cpp index a0d5205620a..7919de76202 100644 --- a/src/theory/arith/proof_checker.cpp +++ b/src/theory/arith/proof_checker.cpp @@ -310,29 +310,37 @@ Node ArithProofRuleChecker::checkInternal(ProofRule id, { Node a = negateProofLiteral(children[0]); Node b = negateProofLiteral(children[1]); - Node c = args[0]; - if (a[0] == b[0] && b[0] == c[0] && a[1] == b[1] && b[1] == c[1]) + if (a[0] == b[0] && a[1] == b[1]) { std::set cmps; cmps.insert(a.getKind()); cmps.insert(b.getKind()); - cmps.insert(c.getKind()); + Kind retk = Kind::UNDEFINED_KIND; if (cmps.count(Kind::EQUAL) == 0) { - Trace("arith::pf::check") << "Error: No = " << std::endl; - return Node::null(); + retk = Kind::EQUAL; } if (cmps.count(Kind::GT) == 0) { - Trace("arith::pf::check") << "Error: No > " << std::endl; - return Node::null(); + if (retk != Kind::UNDEFINED_KIND) + { + Trace("arith::pf::check") + << "Error: No GT and " << retk << std::endl; + return Node::null(); + } + retk = Kind::GT; } if (cmps.count(Kind::LT) == 0) { - Trace("arith::pf::check") << "Error: No < " << std::endl; - return Node::null(); + if (retk != Kind::UNDEFINED_KIND) + { + Trace("arith::pf::check") + << "Error: No LT and " << retk << std::endl; + return Node::null(); + } + retk = Kind::LT; } - return args[0]; + return nm->mkNode(retk, a[0], a[1]); } else { @@ -340,7 +348,6 @@ Node ArithProofRuleChecker::checkInternal(ProofRule id, << "Error: Different polynomials / values" << std::endl; Trace("arith::pf::check") << " a: " << a << std::endl; Trace("arith::pf::check") << " b: " << b << std::endl; - Trace("arith::pf::check") << " c: " << c << std::endl; return Node::null(); } // Check that all have the same constant: From c37ecd92c201db41bd6c30a0360e220442a835d4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 3 Feb 2024 10:54:35 -0600 Subject: [PATCH 02/18] Merge quantifier prenex during prerewrite. (#10305) Fixes #10303. --- .../quantifiers/quantifiers_rewriter.cpp | 124 +++++++++++------- src/theory/quantifiers/quantifiers_rewriter.h | 7 + test/regress/cli/CMakeLists.txt | 1 + ...ees.adb_1105_16_loop_invariant_init_1.smt2 | 19 +++ 4 files changed, 106 insertions(+), 45 deletions(-) create mode 100644 test/regress/cli/regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2 diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index f97d9cec8db..5df8f466c32 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -196,8 +196,29 @@ void QuantifiersRewriter::computeArgVec2(const std::vector& args, } } -RewriteResponse QuantifiersRewriter::preRewrite(TNode in) { - return RewriteResponse(REWRITE_DONE, in); +RewriteResponse QuantifiersRewriter::preRewrite(TNode q) +{ + Kind k = q.getKind(); + if (k == Kind::FORALL || k == Kind::EXISTS) + { + // Do prenex merging now, since this may impact trigger selection. + // In particular consider: + // (forall ((x Int)) (forall ((y Int)) (! (P x) :pattern ((f x))))) + // If we wait until post-rewrite, we would rewrite the inner quantified + // formula, dropping the pattern, so the entire formula becomes: + // (forall ((x Int)) (P x)) + // Instead, we merge to: + // (forall ((x Int) (y Int)) (! (P x) :pattern ((f x)))) + // eagerly here, where after we would drop y to obtain: + // (forall ((x Int)) (! (P x) :pattern ((f x)))) + // See issue #10303. + Node qm = mergePrenex(q); + if (q != qm) + { + return RewriteResponse(REWRITE_AGAIN_FULL, qm); + } + } + return RewriteResponse(REWRITE_DONE, q); } RewriteResponse QuantifiersRewriter::postRewrite(TNode in) @@ -222,50 +243,10 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) } else if (in.getKind() == Kind::FORALL) { - std::vector boundVars; - Node body = in; - bool combineQuantifiers = false; - bool continueCombine = false; - do - { - for (const Node& v : body[0]) - { - if (std::find(boundVars.begin(), boundVars.end(), v)==boundVars.end()) - { - boundVars.push_back(v); - } - } - continueCombine = false; - if (body.getNumChildren() == 2 && body[1].getKind() == Kind::FORALL) - { - QAttributes qa; - QuantAttributes::computeQuantAttributes(body[1], qa); - // should never combine a quantified formula with a pool or - // non-standard quantified formula here. - // note that we technically should check - // doOperation(body[1], COMPUTE_PRENEX, qa) here, although this - // is too restrictive, as sometimes nested patterns should just be - // applied to the top level. - if (qa.isStandard() && !qa.d_hasPool) - { - body = body[1]; - continueCombine = true; - combineQuantifiers = true; - } - } - } - while (continueCombine); - if (combineQuantifiers) + // do prenex merging + ret = mergePrenex(in); + if (ret != in) { - NodeManager* nm = NodeManager::currentNM(); - std::vector children; - children.push_back(nm->mkNode(Kind::BOUND_VAR_LIST, boundVars)); - children.push_back(body[1]); - if (body.getNumChildren() == 3) - { - children.push_back(body[2]); - } - ret = nm->mkNode(Kind::FORALL, children); status = REWRITE_AGAIN_FULL; } else if (in[1].isConst() && in.getNumChildren() == 2) @@ -300,6 +281,59 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) return RewriteResponse( status, ret ); } +Node QuantifiersRewriter::mergePrenex(const Node& q) +{ + Assert(q.getKind() == Kind::FORALL || q.getKind() == Kind::EXISTS); + Kind k = q.getKind(); + std::vector boundVars; + Node body = q; + bool combineQuantifiers = false; + bool continueCombine = false; + do + { + for (const Node& v : body[0]) + { + if (std::find(boundVars.begin(), boundVars.end(), v) == boundVars.end()) + { + boundVars.push_back(v); + } + } + continueCombine = false; + if (body.getNumChildren() == 2 && body[1].getKind() == k) + { + QAttributes qa; + QuantAttributes::computeQuantAttributes(body[1], qa); + // Should never combine a quantified formula with a pool or + // non-standard quantified formula here. + // Note that we technically should check + // doOperation(body[1], COMPUTE_PRENEX, qa) here, although this + // is too restrictive, as sometimes nested patterns should just be + // applied to the top level, for example: + // (forall ((x Int)) (forall ((y Int)) (! P :pattern ((f x y))))) + // should be a pattern for the top-level quantifier here. + if (qa.isStandard() && !qa.d_hasPool) + { + body = body[1]; + continueCombine = true; + combineQuantifiers = true; + } + } + } while (continueCombine); + if (combineQuantifiers) + { + NodeManager* nm = NodeManager::currentNM(); + std::vector children; + children.push_back(nm->mkNode(Kind::BOUND_VAR_LIST, boundVars)); + children.push_back(body[1]); + if (body.getNumChildren() == 3) + { + children.push_back(body[2]); + } + return nm->mkNode(k, children); + } + return q; +} + bool QuantifiersRewriter::addCheckElimChild(std::vector& children, Node c, Kind k, diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 3553f2cdc07..36f61219e33 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -217,6 +217,13 @@ class QuantifiersRewriter : public TheoryRewriter static bool isStandard(QAttributes& qa, const Options& opts); private: + /** + * Do trivial merging of the prenex of quantified formula q, e.g. + * (forall ((x Int)) (forall ((y Int)) (P x y))) ---> + * (forall ((x Int) (y Int)) (P x y)). + * This is done until fixed point. + */ + Node mergePrenex(const Node& q); /** * Helper method for getVarElim, called when n has polarity pol in body. */ diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index c0ec9198866..5a7b523c3c9 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -2510,6 +2510,7 @@ set(regress_1_tests regress1/quantifiers/choice-move-delta-relt.smt2 regress1/quantifiers/const.cvc.smt2 regress1/quantifiers/constfunc.cvc.smt2 + regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2 regress1/quantifiers/dd.bug812-ieval.smt2 regress1/quantifiers/ddatv-delta2.smt2 regress1/quantifiers/dt-tc-opt-small.smt2 diff --git a/test/regress/cli/regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2 b/test/regress/cli/regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2 new file mode 100644 index 00000000000..1cf2eff929b --- /dev/null +++ b/test/regress/cli/regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: -q +; EXPECT: unsat +(set-logic ALL) +(declare-sort e 0) +(declare-sort p 0) +(declare-fun t (p) Int) +(declare-fun o (Int) p) +(assert (forall ((x Int)) (! (= 0 x) :pattern ((o x))))) +(declare-datatypes ((s 0)) (((s_ (x e) (e e) (c e) (c_ p))))) +(declare-datatypes ((us 0)) (((re (_s s))))) +(declare-datatypes ((_s 0)) (((s_ (e (Array Int us)))))) +(declare-datatypes ((us_ 0)) (((us (us _s))))) +(declare-datatypes ((s_ 0)) (((us (re Bool))))) +(declare-datatypes ((u 0)) (((us (_s s_))))) +(declare-fun e (us_ Int) (Array Int u)) +(declare-const r e) +(assert (forall ((p us_)) (forall ((a Int)) (! (not (ite (forall ((i Int)) (= (t (c_ (_s (select (e (us p)) i)))) (t (c_ (_s (re (s_ r r r (o 0)))))))) true false)) :pattern ((e p 0)))))) +(assert (exists ((f _s)) (or (forall ((n Int)) (or (forall ((j Int)) (= true (re (_s (select (e (us f) 0) 0)))))))))) +(check-sat) From a40c4663b2fd5723b32e3c98a29d763e5dc90517 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 5 Feb 2024 09:22:03 -0600 Subject: [PATCH 03/18] Disambiguate symbol overloading in regression (#10347) Fixes nightlies. --- ..._trees.adb_1105_16_loop_invariant_init_1.smt2 | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/test/regress/cli/regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2 b/test/regress/cli/regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2 index 1cf2eff929b..2253b8cde8c 100644 --- a/test/regress/cli/regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2 +++ b/test/regress/cli/regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2 @@ -6,14 +6,14 @@ (declare-fun t (p) Int) (declare-fun o (Int) p) (assert (forall ((x Int)) (! (= 0 x) :pattern ((o x))))) -(declare-datatypes ((s 0)) (((s_ (x e) (e e) (c e) (c_ p))))) +(declare-datatypes ((s 0)) (((s_1 (x e) (e2 e) (c e) (c_ p))))) (declare-datatypes ((us 0)) (((re (_s s))))) -(declare-datatypes ((_s 0)) (((s_ (e (Array Int us)))))) -(declare-datatypes ((us_ 0)) (((us (us _s))))) -(declare-datatypes ((s_ 0)) (((us (re Bool))))) -(declare-datatypes ((u 0)) (((us (_s s_))))) -(declare-fun e (us_ Int) (Array Int u)) +(declare-datatypes ((_s2 0)) (((s_ (e3 (Array Int us)))))) +(declare-datatypes ((us_ 0)) (((us4 (us3 _s2))))) +(declare-datatypes ((s_2 0)) (((us2 (re2 Bool))))) +(declare-datatypes ((u 0)) (((us5 (_s3 s_2))))) +(declare-fun e1 (us_ Int) (Array Int u)) (declare-const r e) -(assert (forall ((p us_)) (forall ((a Int)) (! (not (ite (forall ((i Int)) (= (t (c_ (_s (select (e (us p)) i)))) (t (c_ (_s (re (s_ r r r (o 0)))))))) true false)) :pattern ((e p 0)))))) -(assert (exists ((f _s)) (or (forall ((n Int)) (or (forall ((j Int)) (= true (re (_s (select (e (us f) 0) 0)))))))))) +(assert (forall ((p1 us_)) (forall ((a Int)) (! (not (ite (forall ((i Int)) (= (t (c_ (_s (select (e3 (us3 p1)) i)))) (t (c_ (_s (re (s_1 r r r (o 0)))))))) true false)) :pattern ((e1 p1 0)))))) +(assert (exists ((f _s2)) (or (forall ((n Int)) (or (forall ((j Int)) (= true (re2 (_s3 (select (e1 (us4 f) 0) 0)))))))))) (check-sat) From 2ad7def076c3f9645ca371eb38cb753805d9f625 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Mon, 5 Feb 2024 11:09:56 -0600 Subject: [PATCH 04/18] Update COPYING and licenses directory (#10339) This PR removes antlr3-LICENSE since cvc5 doesn't use ANTLR anymore. It also adds a copy of minisat LICENSE to the licenses directory, updates the references to the minisat LICENSE in COPYING, and moves CaDiCaL from the optional list to the required one. --- COPYING | 16 +++++++++++----- licenses/antlr3-LICENSE | 28 ---------------------------- licenses/minisat-LICENSE | 21 +++++++++++++++++++++ 3 files changed, 32 insertions(+), 33 deletions(-) delete mode 100644 licenses/antlr3-LICENSE create mode 100644 licenses/minisat-LICENSE diff --git a/COPYING b/COPYING index 9a040ad24a4..f589966a6d4 100644 --- a/COPYING +++ b/COPYING @@ -52,16 +52,23 @@ The following file contains third-party software. The copyright and licensing information of this file is in its header. -cvc5 incorporates MiniSat code (see src/prop/minisat and src/prop/bvminisat), -excluded from the above copyright. See src/prop/minisat/LICENSE and -src/prop/bvminisat/LICENSE for copyright and licensing information. +cvc5 incorporates MiniSat code (see src/prop/minisat), +excluded from the above copyright. See licenses/minisat-LICENSE +for copyright and licensing information. cvc5 by default links against The GNU Multiple Precision (GMP) Arithmetic -Library, which is licensed under GNU LGPL v3. See the file +Library, which is licensed under GNU LGPL v3. See the file licenses/lgpl-3.0.txt for a copy of that license. Note that according to the terms of the LGPL, both cvc5's source, and the combined work (cvc5 linked with GMP) may (and do) remain under the more permissive modified BSD license. +cvc5 also links against the CaDiCaL library +(https://github.com/arminbiere/cadical), which is licensed under +the MIT license. +See https://raw.githubusercontent.com/arminbiere/cadical/master/LICENSE +for copyright and licensing information. Linking cvc5 against +this library does not affect the license terms of the cvc5 code. + The implementation of the floating point solver in cvc5 depends on symfpu (https://github.com/martin-cs/symfpu) written by Martin Brain. See https://raw.githubusercontent.com/martin-cs/symfpu/CVC4/LICENSE for @@ -70,7 +77,6 @@ copyright and licensing information. cvc5 optionally links against the following libraries: ABC (https://bitbucket.org/alanmi/abc) - CaDiCaL (https://github.com/arminbiere/cadical) CryptoMiniSat (https://github.com/msoos/cryptominisat) LibPoly (https://github.com/SRI-CSL/libpoly) libedit (https://thrysoee.dk/editline) diff --git a/licenses/antlr3-LICENSE b/licenses/antlr3-LICENSE deleted file mode 100644 index 6364129f5ab..00000000000 --- a/licenses/antlr3-LICENSE +++ /dev/null @@ -1,28 +0,0 @@ -[The "BSD licence"] -Copyright (c) 2005-2009 Jim Idle, Temporal Wave LLC -http://www.temporal-wave.com -http://www.linkedin.com/in/jimidle - -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions -are met: -1. Redistributions of source code must retain the above copyright - notice, this list of conditions and the following disclaimer. -2. Redistributions in binary form must reproduce the above copyright - notice, this list of conditions and the following disclaimer in the - documentation and/or other materials provided with the distribution. -3. The name of the author may not be used to endorse or promote products - derived from this software without specific prior written permission. - -THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR -IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES -OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. -IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, -INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT -NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, -DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY -THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT -(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF -THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/licenses/minisat-LICENSE b/licenses/minisat-LICENSE new file mode 100644 index 00000000000..22816ff39b1 --- /dev/null +++ b/licenses/minisat-LICENSE @@ -0,0 +1,21 @@ +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson + Copyright (c) 2007-2010 Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a +copy of this software and associated documentation files (the +"Software"), to deal in the Software without restriction, including +without limitation the rights to use, copy, modify, merge, publish, +distribute, sublicense, and/or sell copies of the Software, and to +permit persons to whom the Software is furnished to do so, subject to +the following conditions: + +The above copyright notice and this permission notice shall be included +in all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS +OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE +LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION +OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION +WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. From 624dc1a6914d6f25d150a038a1572a1fcc1d714a Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Mon, 5 Feb 2024 12:01:00 -0600 Subject: [PATCH 05/18] Fix Python package licensing (#10348) This PR updates the `License` field of the Python wheel metadata to reflect that the package includes artifacts under three different licenses: BSD-3-Clause, LGPL-3.0-or-later, and MIT. It also includes a COPYING file and associated license files in the `dist-info` directory of the Python wheel. It fixes #10327. It depends on #10339. --- contrib/packaging_python/mk_clean_wheel.sh | 2 ++ contrib/packaging_python/mk_wheel.py | 8 ++++-- src/api/python/CMakeLists.txt | 33 +++++++++++++++++++++- 3 files changed, 40 insertions(+), 3 deletions(-) diff --git a/contrib/packaging_python/mk_clean_wheel.sh b/contrib/packaging_python/mk_clean_wheel.sh index 782a64b5eb5..a69a7673a83 100755 --- a/contrib/packaging_python/mk_clean_wheel.sh +++ b/contrib/packaging_python/mk_clean_wheel.sh @@ -59,6 +59,8 @@ rm -rf build_wheel/ echo "Building pycvc5 wheel" pushd build_wheel +# Copy the license files to be included in the wheel +cmake --build . --target cvc5_python_licenses if [ -z "$PLATFORM" ] ; then python ../contrib/packaging_python/mk_wheel.py bdist_wheel -d dist else diff --git a/contrib/packaging_python/mk_wheel.py b/contrib/packaging_python/mk_wheel.py index 297cca98df4..e343194702f 100644 --- a/contrib/packaging_python/mk_wheel.py +++ b/contrib/packaging_python/mk_wheel.py @@ -113,9 +113,13 @@ def build_extension(self, ext): version=get_cvc5_version(), long_description='Python bindings for cvc5', url='https://github.com/cvc5/cvc5', - license='BSD-3-Clause', + license = "BSD-3-Clause AND LGPL-3.0-or-later AND MIT", + # BSD-3-Clause : cvc5 library and Python API + # LGPL-3.0-or-later : LibPoly and GMP + # MIT : Pythonic API zip_safe=False, ext_modules=[CMakeExtension('cvc5')], cmdclass=dict(build_ext=CMakeBuild), - tests_require=['pytest'] + tests_require=['pytest'], + license_files = ['COPYING', 'licenses/*'], ) diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt index 027d659859d..4e570a5e2a0 100644 --- a/src/api/python/CMakeLists.txt +++ b/src/api/python/CMakeLists.txt @@ -178,7 +178,6 @@ python_extension_module(cvc5_python_base) find_package(CVC5PythonicAPI) set(COPIED_PYTHONIC_FILES - "${CMAKE_CURRENT_BINARY_DIR}/cvc5/pythonic/LICENSE.txt" "${CMAKE_CURRENT_BINARY_DIR}/cvc5/pythonic/__init__.py" "${CMAKE_CURRENT_BINARY_DIR}/cvc5/pythonic/cvc5_pythonic.py" "${CMAKE_CURRENT_BINARY_DIR}/cvc5/pythonic/cvc5_pythonic_printer.py" @@ -191,11 +190,43 @@ add_custom_command( ${CMAKE_COMMAND} -E copy_directory "${CVC5PythonicAPI_BASEDIR}/cvc5_pythonic_api" "${CMAKE_CURRENT_BINARY_DIR}/cvc5/pythonic" + # Remove the license of the Pythonic API from the package's source files. + # The license file is included in the package's dist-info dir by setup() + COMMAND + ${CMAKE_COMMAND} -E remove + "${CMAKE_CURRENT_BINARY_DIR}/cvc5/pythonic/LICENSE.txt" DEPENDS cvc5_python_base CVC5PythonicAPI ) add_custom_target(cvc5_python_api ALL DEPENDS ${COPIED_PYTHONIC_FILES}) +set(LICENSE_FILES + "${CMAKE_BINARY_DIR}/COPYING" + "${CMAKE_BINARY_DIR}/licenses/lgpl-3.0.txt" + "${CMAKE_BINARY_DIR}/licenses/pythonic-LICENSE" +) + +add_custom_command( + OUTPUT + ${LICENSE_FILES} + COMMAND + ${CMAKE_COMMAND} -E copy + "${PROJECT_SOURCE_DIR}/COPYING" + "${CMAKE_BINARY_DIR}/COPYING" + COMMAND + ${CMAKE_COMMAND} -E copy_directory + "${PROJECT_SOURCE_DIR}/licenses" + "${CMAKE_BINARY_DIR}/licenses" + COMMAND + ${CMAKE_COMMAND} -E copy + "${CVC5PythonicAPI_BASEDIR}/cvc5_pythonic_api/LICENSE.txt" + "${CMAKE_BINARY_DIR}/licenses/pythonic-LICENSE" + DEPENDS CVC5PythonicAPI +) + +# Copy license files to build directory where setup() can find them +add_custom_target(cvc5_python_licenses DEPENDS ${LICENSE_FILES}) + # Installation based on https://bloerg.net/2012/11/10/cmake-and-distutils.html # Create a wrapper python directory and generate a distutils setup.py file configure_file(setup.py.in setup.py) From 91c3bc8c2b35f7ecd5ab824cab8d4fb3ad7e04c1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 5 Feb 2024 13:46:22 -0600 Subject: [PATCH 06/18] Cleanup nary cong rule in ALF (#10341) This is work towards unifying the internal calculus and the ALF signature. This cleans up the NARY_CONG rule in the ALF signature by using a new alf.emptylist operator in the ALF language. --- contrib/get-alf-checker | 2 +- proofs/alf/rules/Uf.smt3 | 23 +++++++++++++++-------- src/proof/alf/alf_post_processor.cpp | 9 ++------- 3 files changed, 18 insertions(+), 16 deletions(-) diff --git a/contrib/get-alf-checker b/contrib/get-alf-checker index c50dc4606d8..b452e3eb95c 100755 --- a/contrib/get-alf-checker +++ b/contrib/get-alf-checker @@ -24,7 +24,7 @@ ALFC_DIR="$BASE_DIR/alf-checker" mkdir -p $ALFC_DIR # download and unpack ALFC -ALF_VERSION="b51d495b4871dc0c4e4f68e579a504cec288b022" +ALF_VERSION="57b34b6b5c130eb44332149b110bed130b3281e3" download "https://github.com/cvc5/alfc/archive/$ALF_VERSION.tar.gz" $BASE_DIR/tmp/alfc.tgz tar --strip 1 -xzf $BASE_DIR/tmp/alfc.tgz -C $ALFC_DIR diff --git a/proofs/alf/rules/Uf.smt3 b/proofs/alf/rules/Uf.smt3 index 4374fbbe3ba..99f3f3a0bda 100644 --- a/proofs/alf/rules/Uf.smt3 +++ b/proofs/alf/rules/Uf.smt3 @@ -57,20 +57,27 @@ ) ; N-ary congruence -; note that arguments are provided in reverse order to avoid intermediate node construction -(program mk_nary_cong ((U Type) (f (-> U U)) (t1 U) (t2 U) (s1 U) (s2 U) (tail Bool :list)) - ((-> U U) U U Bool) Bool +; We use two side conditions for computing each side of the returned equality. +; This avoids intermediate node construction. +(program mk_nary_cong_lhs ((U Type) (f (-> U U)) (s1 U) (s2 U) (tail Bool :list)) + ((-> U U) Bool) Bool ( - ((mk_nary_cong f t1 t2 (and (= s1 s2) tail)) (mk_nary_cong f (f s1 t1) (f s2 t2) tail)) - ((mk_nary_cong f t1 t2 true) (= t1 t2)) - ((mk_nary_cong f t1 t2 (= s1 s2)) (= (f s1 t1) (f s2 t2))) + ((mk_nary_cong_lhs f (and (= s1 s2) tail)) (f s1 (mk_nary_cong_lhs f tail))) + ((mk_nary_cong_lhs f true) (alf.emptylist f)) + ) +) +(program mk_nary_cong_rhs ((U Type) (f (-> U U)) (s1 U) (s2 U) (tail Bool :list)) + ((-> U U) Bool) Bool + ( + ((mk_nary_cong_rhs f (and (= s1 s2) tail)) (f s2 (mk_nary_cong_rhs f tail))) + ((mk_nary_cong_rhs f true) (alf.emptylist f)) ) ) (declare-rule nary_cong ((U Type) (E Bool) (f (-> U U)) (nil U)) :premise-list E and - :args (f nil) - :conclusion (mk_nary_cong f nil nil E) + :args (f) + :conclusion (= (mk_nary_cong_lhs f E) (mk_nary_cong_rhs f E)) ) ; TRUE_INTRO diff --git a/src/proof/alf/alf_post_processor.cpp b/src/proof/alf/alf_post_processor.cpp index 4fdfc9d0e27..168f74241fe 100644 --- a/src/proof/alf/alf_post_processor.cpp +++ b/src/proof/alf/alf_post_processor.cpp @@ -208,13 +208,8 @@ bool AlfProofPostprocessCallback::update(Node res, } if (isNary) { - std::vector rchildren = children; - std::reverse(rchildren.begin(), rchildren.end()); - std::vector cargs; - cargs.push_back(op); - cargs.push_back(nullt); - // use n-ary rule, must reverse children - addAlfStep(AlfRule::NARY_CONG, res, rchildren, cargs, *cdp); + // use n-ary rule + addAlfStep(AlfRule::NARY_CONG, res, children, {op}, *cdp); } else { From afa08441f0ba8b27d3c6efe917814a4f5e3dbc92 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 5 Feb 2024 14:17:58 -0600 Subject: [PATCH 07/18] Print lambda and witness in SMT-LIB compliant way in ALF (#10337) --- proofs/alf/rules/Quantifiers.smt3 | 2 +- proofs/alf/theories/Builtin.smt3 | 9 ++++++++- proofs/alf/theories/Quantifiers.smt3 | 9 ++++++++- src/proof/alf/alf_node_converter.cpp | 18 ------------------ src/proof/alf/alf_post_processor.cpp | 25 +------------------------ 5 files changed, 18 insertions(+), 45 deletions(-) diff --git a/proofs/alf/rules/Quantifiers.smt3 b/proofs/alf/rules/Quantifiers.smt3 index eaeee1698c3..9dae962bcaf 100644 --- a/proofs/alf/rules/Quantifiers.smt3 +++ b/proofs/alf/rules/Quantifiers.smt3 @@ -34,7 +34,7 @@ t ( ; special case for witness - ((skolem (@k.QUANTIFIERS_SKOLEMIZE (exists (@list x) F) x)) (= t (witness x F))) + ((skolem (@k.QUANTIFIERS_SKOLEMIZE (exists (@list x) F) x)) (= t (witness (@list x) F))) ((skolem x) (= t x)) ) ) diff --git a/proofs/alf/theories/Builtin.smt3 b/proofs/alf/theories/Builtin.smt3 index 6b15589a1fc..0a5349916d6 100644 --- a/proofs/alf/theories/Builtin.smt3 +++ b/proofs/alf/theories/Builtin.smt3 @@ -22,7 +22,14 @@ :chainable and ) -(declare-const lambda (-> (! Type :var A :implicit) (! Type :var B :implicit) A B (-> A B))) +(program get_lambda_type ((x @List) (xs @List :list) (B Type)) + (@List Type) Type + ( + ((get_lambda_type (@list x xs) B) (-> (alf.typeof x) (get_lambda_type xs B))) + ((get_lambda_type @list.nil B) B) + ) +) +(declare-const lambda (-> (! Type :var B :implicit) (! @List :var L) B (get_lambda_type L B)) :binder @list) (declare-const distinct (-> (! Type :var A :implicit) A A Bool) :pairwise and) diff --git a/proofs/alf/theories/Quantifiers.smt3 b/proofs/alf/theories/Quantifiers.smt3 index b7577e89bd8..10bbeffef91 100644 --- a/proofs/alf/theories/Quantifiers.smt3 +++ b/proofs/alf/theories/Quantifiers.smt3 @@ -4,7 +4,14 @@ (declare-const exists (-> @List Bool Bool) :binder @list) -(declare-const witness (-> (! Type :var T :implicit) T Bool T)) +; returns the type of the element in the list, if the list is a singleton. +(program get_witness_type ((x @List)) + (@List) Type + ( + ((get_witness_type (@list x)) (alf.typeof x)) + ) +) +(declare-const witness (-> (! @List :var L) Bool (get_witness_type L)) :binder @list) ; skolems (declare-const @k.QUANTIFIERS_SKOLEMIZE (-> (! Type :var T :implicit) Bool T T)) diff --git a/src/proof/alf/alf_node_converter.cpp b/src/proof/alf/alf_node_converter.cpp index 7277199e76b..34f88bcac14 100644 --- a/src/proof/alf/alf_node_converter.cpp +++ b/src/proof/alf/alf_node_converter.cpp @@ -161,24 +161,6 @@ Node AlfNodeConverter::postConvert(Node n) ss << (r.sgn() == -1 ? "-" : "") << num << "/" << den; return mkInternalSymbol(ss.str(), tn); } - else if (k == Kind::LAMBDA || k == Kind::WITNESS) - { - // e.g. (lambda ((x1 T1) ... (xn Tk)) P) is - // (lambda x1 (lambda x2 ... (lambda xn P))) - Node ret = n[1]; - TypeNode tnr = ret.getType(); - std::stringstream opName; - opName << printer::smt2::Smt2Printer::smtKindString(k); - for (size_t i = 0, nchild = n[0].getNumChildren(); i < nchild; i++) - { - size_t ii = (nchild - 1) - i; - Node v = convert(n[0][ii]); - // use the body return type for all terms except the last one. - tnr = ii == 0 ? n.getType() : nm->mkFunctionType({v.getType()}, tnr); - ret = mkInternalApp(opName.str(), {v, ret}, tnr); - } - return ret; - } else if (n.isClosure()) { // e.g. (forall ((x1 T1) ... (xn Tk)) P) is diff --git a/src/proof/alf/alf_post_processor.cpp b/src/proof/alf/alf_post_processor.cpp index 168f74241fe..c7a2a3ac48f 100644 --- a/src/proof/alf/alf_post_processor.cpp +++ b/src/proof/alf/alf_post_processor.cpp @@ -148,30 +148,7 @@ bool AlfProofPostprocessCallback::update(Node res, Node op = d_tproc.getOperatorOfTerm(res[0]); Trace("alf-proof") << "Processing cong for op " << op << " " << op.getType() << std::endl; - if (k == Kind::LAMBDA || k == Kind::WITNESS) - { - Assert(res[1].getKind() == k && res[0][0] == res[1][0]); - Node lam1 = d_tproc.convert(res[0]); - Node lam2 = d_tproc.convert(res[1]); - for (size_t i = 0, nvars = res[0][0].getNumChildren(); i < nvars; i++) - { - Assert(lam1.getNumChildren() == 2 && lam2.getNumChildren() == 2); - Node varEq = lam1[0].eqNode(lam1[0]); - cdp->addStep(varEq, ProofRule::REFL, {}, {lam1[0]}); - Node bodyEq = i + 1 == nvars ? children[1] : lam1[1].eqNode(lam2[1]); - Node lamEq = lam1.eqNode(lam2); - Node conclusion = i == 0 ? res : lamEq; - addAlfStep(AlfRule::CONG, - conclusion, - {varEq, bodyEq}, - {lam1.getOperator()}, - *cdp); - lam1 = lam1[1]; - lam2 = lam2[1]; - } - return true; - } - else if (res[0].isClosure()) + if (res[0].isClosure()) { Assert(children.size() >= 2); // variable lists should be equal From df22f76e6b404048964aec1d8e7c7a43803fcbab Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 5 Feb 2024 15:17:03 -0600 Subject: [PATCH 08/18] Do not convert SCOPE in ALF post processor (#10345) This is work towards eliminating the postprocessing step for the ALF printer. This handles the printing of SCOPE in the ALF printer without converting the proof nodes. --- proofs/alf/rules/Booleans.smt3 | 38 ------------- proofs/alf/rules/Builtin.smt3 | 38 +++++++++++++ src/proof/alf/alf_post_processor.cpp | 27 --------- src/proof/alf/alf_printer.cpp | 83 ++++++++++++++++++---------- src/proof/alf/alf_printer.h | 4 +- src/proof/alf/alf_proof_rule.cpp | 2 - src/proof/alf/alf_proof_rule.h | 4 -- 7 files changed, 93 insertions(+), 103 deletions(-) diff --git a/proofs/alf/rules/Booleans.smt3 b/proofs/alf/rules/Booleans.smt3 index bfa77afff70..44eedb46827 100644 --- a/proofs/alf/rules/Booleans.smt3 +++ b/proofs/alf/rules/Booleans.smt3 @@ -3,44 +3,6 @@ (include "../programs/Nary.smt3") -; SCOPE -(declare-rule scope - ((F Bool) (G Bool)) - :assumption F - :premises (G) - :args () - :conclusion (=> F G) -) - -; `extract_antec F C` -; returns the antecedant of F up to C, -; e.g. returns (and G1 G2) when F is (=> G1 (=> G2 C)). -(program extract_antec - ((C Bool) (F1 Bool) (F2 Bool)) - (Bool Bool) Bool - ( - ((extract_antec C C) true) - ((extract_antec (=> F1 F2) C) (alf.cons and F1 (extract_antec F2 C))) - ) -) - -(program run_process_scope - ((C Bool) (F Bool)) - (Bool Bool) Bool - ( - ((run_process_scope F false) (not (alf.from_list and (extract_antec F false)))) - ((run_process_scope F C) (=> (alf.from_list and (extract_antec F C)) C)) - ) -) - -; this rule processes the result of n scopes into the conclusion expected by ProofRule::SCOPE -(declare-rule process_scope - ((C Bool) (F Bool)) - :premises (F) - :args (C) - :conclusion (run_process_scope F C) -) - ; SPLIT (declare-rule split ((F Bool)) :args (F) diff --git a/proofs/alf/rules/Builtin.smt3 b/proofs/alf/rules/Builtin.smt3 index 29e1006f828..d697958309d 100644 --- a/proofs/alf/rules/Builtin.smt3 +++ b/proofs/alf/rules/Builtin.smt3 @@ -1,5 +1,43 @@ (include "../theories/Builtin.smt3") +; SCOPE +(declare-rule scope + ((F Bool) (G Bool)) + :assumption F + :premises (G) + :args () + :conclusion (=> F G) +) + +; `extract_antec F C` +; returns the antecedant of F up to C, +; e.g. returns (and G1 G2) when F is (=> G1 (=> G2 C)). +(program extract_antec + ((C Bool) (F1 Bool) (F2 Bool)) + (Bool Bool) Bool + ( + ((extract_antec C C) true) + ((extract_antec (=> F1 F2) C) (alf.cons and F1 (extract_antec F2 C))) + ) +) + +(program run_process_scope + ((C Bool) (F Bool)) + (Bool Bool) Bool + ( + ((run_process_scope F false) (not (alf.from_list and (extract_antec F false)))) + ((run_process_scope F C) (=> (alf.from_list and (extract_antec F C)) C)) + ) +) + +; this rule processes the result of n scopes into the conclusion expected by ProofRule::SCOPE +(declare-rule process_scope + ((C Bool) (F Bool)) + :premises (F) + :args (C) + :conclusion (run_process_scope F C) +) + (declare-rule remove_term_formula_axiom ((T Type) (b Bool) (t1 T) (t2 T)) :args ((ite b t1 t2)) :conclusion diff --git a/src/proof/alf/alf_post_processor.cpp b/src/proof/alf/alf_post_processor.cpp index c7a2a3ac48f..a325723fadf 100644 --- a/src/proof/alf/alf_post_processor.cpp +++ b/src/proof/alf/alf_post_processor.cpp @@ -50,7 +50,6 @@ bool AlfProofPostprocessCallback::shouldUpdate(std::shared_ptr pn, { switch (pn->getRule()) { - case ProofRule::SCOPE: case ProofRule::CONG: case ProofRule::CONCAT_CONFLICT: case ProofRule::SKOLEM_INTRO: return true; @@ -98,35 +97,9 @@ bool AlfProofPostprocessCallback::update(Node res, { Trace("alf-proof") << "...Alf pre-update " << res << " " << id << " " << children << " / " << args << std::endl; - NodeManager* nm = NodeManager::currentNM(); switch (id) { - case ProofRule::SCOPE: - { - // On the first two calls to update, the proof nodes are the outermost - // scopes of the proof. These scopes should not be printed in the AletheLF - // proof. Instead, the AletheLF proof printer will print the proper scopes - // around the proof, which e.g. involves an AletheLF "check" command. - if (d_numIgnoredScopes < 2) - { - d_numIgnoredScopes++; - // Note that we do not want to modify the top-most SCOPEs. - return false; - } - Node curr = children[0]; - for (size_t i = 0, nargs = args.size(); i < nargs; i++) - { - size_t ii = (nargs - 1) - i; - Node next = nm->mkNode(Kind::IMPLIES, args[ii], curr); - addAlfStep(AlfRule::SCOPE, next, {curr}, {args[ii]}, *cdp); - curr = next; - } - // convert (=> F1 (=> ... (=> Fn C)...)) to (=> (and F1 ... Fn) C) or - // (not (and F1 ... Fn)) - addAlfStep(AlfRule::PROCESS_SCOPE, res, {curr}, {children[0]}, *cdp); - } - break; case ProofRule::CONG: { Assert(res.getKind() == Kind::EQUAL); diff --git a/src/proof/alf/alf_printer.cpp b/src/proof/alf/alf_printer.cpp index ffb3ddf9f4a..dee138e0797 100644 --- a/src/proof/alf/alf_printer.cpp +++ b/src/proof/alf/alf_printer.cpp @@ -48,6 +48,7 @@ bool AlfPrinter::isHandled(const ProofNode* pfn) const switch (pfn->getRule()) { // List of handled rules + case ProofRule::SCOPE: case ProofRule::REFL: case ProofRule::SYMM: case ProofRule::TRANS: @@ -405,18 +406,16 @@ void AlfPrinter::printStepPre(AlfPrintChannel* out, const ProofNode* pn) { // if we haven't yet allocated a proof id, do it now ProofRule r = pn->getRule(); - if (r == ProofRule::ALF_RULE) + if (r == ProofRule::SCOPE) { - Assert(!pn->getArguments().empty()); - Node rn = pn->getArguments()[0]; - AlfRule ar = getAlfRule(rn); - if (ar == AlfRule::SCOPE) + const std::vector& args = pn->getArguments(); + Assert(!args.empty()); + for (const Node& a : args) { - Assert(pn->getArguments().size() == 3); - size_t aid = allocateAssumePushId(pn); - Node a = d_tproc.convert(pn->getArguments()[2]); + size_t aid = allocateAssumePushId(pn, a); + Node aa = d_tproc.convert(a); // print a push - out->printAssume(a, aid, true); + out->printAssume(aa, aid, true); } } } @@ -472,7 +471,6 @@ void AlfPrinter::printStepPost(AlfPrintChannel* out, const ProofNode* pn) Assert(pn->getRule() != ProofRule::ASSUME); // if we have yet to allocate a proof id, do it now bool wasAlloc = false; - bool isPop = false; TNode conclusion = d_tproc.convert(pn->getResult()); TNode conclusionPrint; // print conclusion only if option is set, or this is false @@ -488,20 +486,10 @@ void AlfPrinter::printStepPost(AlfPrintChannel* out, const ProofNode* pn) { const std::vector aargs = pn->getArguments(); Node rn = aargs[0]; - AlfRule ar = getAlfRule(rn); - // if scope, do pop the assumption from passumeMap - if (ar == AlfRule::SCOPE) + // arguments are converted here + for (size_t i = 2, nargs = aargs.size(); i < nargs; i++) { - isPop = true; - // note that aargs[1] is not provided, it is consumed as an assumption - } - else - { - // arguments are converted here - for (size_t i = 2, nargs = aargs.size(); i < nargs; i++) - { - args.push_back(d_tproc.convert(aargs[i])); - } + args.push_back(d_tproc.convert(aargs[i])); } } else if (handled) @@ -538,19 +526,54 @@ void AlfPrinter::printStepPost(AlfPrintChannel* out, const ProofNode* pn) premises.push_back(pid); } std::string rname = getRuleName(pn); - out->printStep(rname, conclusionPrint, id, premises, args, isPop); + if (r == ProofRule::SCOPE) + { + if (args.empty()) + { + // If there are no premises, any reference to this proof can just refer to + // the body. + d_pletMap[pn] = premises[0]; + } + else + { + // Assuming the body of the scope has identifier id_0, the following prints: + // (step-pop id_1 :rule scope :premises (id_0)) + // ... + // (step-pop id_n :rule scope :premises (id_{n-1})) + // (step id :rule process_scope :premises (id_n) :args (C)) + size_t tmpId; + for (size_t i = 0, nargs = args.size(); i < nargs; i++) + { + // Manually increment proof id counter and premises. Note they will only be + // used locally here to chain together the pops mentioned above. + tmpId = d_pfIdCounter; + d_pfIdCounter++; + out->printStep(rname, Node::null(), tmpId, premises, {}, true); + // The current id is the premises of the next. + premises.clear(); + premises.push_back(tmpId); + } + // Finish with the process scope step. + std::vector pargs; + pargs.push_back(d_tproc.convert(children[0]->getResult())); + out->printStep("process_scope", conclusionPrint, id, premises, pargs); + } + } + else + { + out->printStep(rname, conclusionPrint, id, premises, args); + } } -size_t AlfPrinter::allocateAssumePushId(const ProofNode* pn) +size_t AlfPrinter::allocateAssumePushId(const ProofNode* pn, const Node& a) { - std::map::iterator it = d_ppushMap.find(pn); + std::pair key(pn, a); + std::map, size_t>::iterator it = + d_ppushMap.find(key); if (it != d_ppushMap.end()) { return it->second; } - Assert(pn->getRule() == ProofRule::ALF_RULE); - // pn is a Alf SCOPE - Node a = pn->getArguments()[2]; bool wasAlloc = false; size_t aid = allocateAssumeId(a, wasAlloc); // if we assigned an id to the assumption @@ -560,7 +583,7 @@ size_t AlfPrinter::allocateAssumePushId(const ProofNode* pn) d_pfIdCounter++; aid = d_pfIdCounter; } - d_ppushMap[pn] = aid; + d_ppushMap[key] = aid; return aid; } diff --git a/src/proof/alf/alf_printer.h b/src/proof/alf/alf_printer.h index 886d50121cf..d56b0faf566 100644 --- a/src/proof/alf/alf_printer.h +++ b/src/proof/alf/alf_printer.h @@ -84,7 +84,7 @@ class AlfPrinter : protected EnvObj * return the identifier. pn should be an application of ProofNode::ALF_RULE * with AlfRule::SCOPE. */ - size_t allocateAssumePushId(const ProofNode* pn); + size_t allocateAssumePushId(const ProofNode* pn, const Node& a); /** * Allocate (if necessary) the identifier for an assume step for the * assumption for formula n and return the identifier. Note this identifier is @@ -103,7 +103,7 @@ class AlfPrinter : protected EnvObj /** Assume id counter */ size_t d_pfIdCounter; /** Mapping scope proofs to identifiers */ - std::map d_ppushMap; + std::map, size_t> d_ppushMap; /** Mapping proofs to identifiers */ std::map d_pletMap; /** Mapping assumed formulas to identifiers */ diff --git a/src/proof/alf/alf_proof_rule.cpp b/src/proof/alf/alf_proof_rule.cpp index a9e45db2ff0..23dadeedaa0 100644 --- a/src/proof/alf/alf_proof_rule.cpp +++ b/src/proof/alf/alf_proof_rule.cpp @@ -28,8 +28,6 @@ const char* AlfRuleToString(AlfRule id) { case AlfRule::CONG: return "cong"; case AlfRule::NARY_CONG: return "nary_cong"; - case AlfRule::SCOPE: return "scope"; - case AlfRule::PROCESS_SCOPE: return "process_scope"; case AlfRule::CONCAT_CONFLICT_DEQ: return "concat_conflict_deq"; //================================================= Undefined rule case AlfRule::UNDEFINED: return "undefined"; diff --git a/src/proof/alf/alf_proof_rule.h b/src/proof/alf/alf_proof_rule.h index 7a46751db63..bbeb35dcfaa 100644 --- a/src/proof/alf/alf_proof_rule.h +++ b/src/proof/alf/alf_proof_rule.h @@ -36,10 +36,6 @@ enum class AlfRule : uint32_t CONG, // n-ary congruence NARY_CONG, - // scope - SCOPE, - // process_scope - PROCESS_SCOPE, // concat conflict disequality CONCAT_CONFLICT_DEQ, // Used in case that a step in the proof rule could not be translated. From 5bb855ce148c85703c50473d91d6d2cee533f1d3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 6 Feb 2024 08:24:38 -0600 Subject: [PATCH 09/18] Add ProofRule::CONCAT_CONFLICT_DEQ for sequences (#10342) This separates a special case of the rule CONCAT_CONFLICT to its own proof rule. This eliminates the need for special casing in the internal -> ALF conversion. --- include/cvc5/cvc5_proof_rule.h | 18 +++++++++++++----- src/api/cpp/cvc5_proof_rule.cpp | 1 + src/proof/alf/alf_post_processor.cpp | 14 -------------- src/proof/alf/alf_proof_rule.cpp | 1 - src/proof/alf/alf_proof_rule.h | 2 -- src/theory/strings/infer_proof_cons.cpp | 5 +++-- src/theory/strings/proof_checker.cpp | 10 ++++++---- 7 files changed, 23 insertions(+), 28 deletions(-) diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h index eba5f4c5ef7..e106cf5bd48 100644 --- a/include/cvc5/cvc5_proof_rule.h +++ b/include/cvc5/cvc5_proof_rule.h @@ -1371,21 +1371,29 @@ enum ENUM(ProofRule) : uint32_t * \mathit{index},b)` is null, in other words, neither is a prefix of the * other. Note it may be the case that one side of the equality denotes the * empty string. + * + * This rule is used exclusively for strings. * - * Alternatively, if the equality is between sequences, this rule has the - * form: + * \endverbatim + */ + EVALUE(CONCAT_CONFLICT), + /** + * \verbatim embed:rst:leading-asterisk + * **Strings -- Core rules -- Concatenation conflict for disequal characters** * * .. math:: * * \inferrule{(t_1\cdot t) = (s_1 \cdot s), t_1 \deq s_1 \mid b}{\bot} * - * where t_1 and s_1 are constants of length one, or otherwise one side - * of the equality is the empty sequence and t_1 or s_1 corresponding to + * where $t_1$ and $s_1$ are constants of length one, or otherwise one side + * of the equality is the empty sequence and $t_1$ or $s_1$ corresponding to * that side is the empty sequence. + * + * This rule is used exclusively for sequences. * * \endverbatim */ - EVALUE(CONCAT_CONFLICT), + EVALUE(CONCAT_CONFLICT_DEQ), /** * \verbatim embed:rst:leading-asterisk * **Strings -- Core rules -- Concatenation split** diff --git a/src/api/cpp/cvc5_proof_rule.cpp b/src/api/cpp/cvc5_proof_rule.cpp index 0918f1e1483..cfe0b8efe3b 100644 --- a/src/api/cpp/cvc5_proof_rule.cpp +++ b/src/api/cpp/cvc5_proof_rule.cpp @@ -132,6 +132,7 @@ const char* toString(ProofRule id) case ProofRule::CONCAT_EQ: return "CONCAT_EQ"; case ProofRule::CONCAT_UNIFY: return "CONCAT_UNIFY"; case ProofRule::CONCAT_CONFLICT: return "CONCAT_CONFLICT"; + case ProofRule::CONCAT_CONFLICT_DEQ: return "CONCAT_CONFLICT_DEQ"; case ProofRule::CONCAT_SPLIT: return "CONCAT_SPLIT"; case ProofRule::CONCAT_CSPLIT: return "CONCAT_CSPLIT"; case ProofRule::CONCAT_LPROP: return "CONCAT_LPROP"; diff --git a/src/proof/alf/alf_post_processor.cpp b/src/proof/alf/alf_post_processor.cpp index a325723fadf..307ad7a02b0 100644 --- a/src/proof/alf/alf_post_processor.cpp +++ b/src/proof/alf/alf_post_processor.cpp @@ -168,20 +168,6 @@ bool AlfProofPostprocessCallback::update(Node res, } } break; - case ProofRule::CONCAT_CONFLICT: - { - if (children.size() == 1) - { - // no need to change - return false; - } - Assert(children.size() == 2); - Assert(children[0].getKind() == Kind::EQUAL); - Assert(children[0][0].getType().isSequence()); - // must use the sequences version of the rule - addAlfStep(AlfRule::CONCAT_CONFLICT_DEQ, res, children, args, *cdp); - } - break; default: return false; } return true; diff --git a/src/proof/alf/alf_proof_rule.cpp b/src/proof/alf/alf_proof_rule.cpp index 23dadeedaa0..62f3407e000 100644 --- a/src/proof/alf/alf_proof_rule.cpp +++ b/src/proof/alf/alf_proof_rule.cpp @@ -28,7 +28,6 @@ const char* AlfRuleToString(AlfRule id) { case AlfRule::CONG: return "cong"; case AlfRule::NARY_CONG: return "nary_cong"; - case AlfRule::CONCAT_CONFLICT_DEQ: return "concat_conflict_deq"; //================================================= Undefined rule case AlfRule::UNDEFINED: return "undefined"; default: return "?"; diff --git a/src/proof/alf/alf_proof_rule.h b/src/proof/alf/alf_proof_rule.h index bbeb35dcfaa..c3022c52958 100644 --- a/src/proof/alf/alf_proof_rule.h +++ b/src/proof/alf/alf_proof_rule.h @@ -36,8 +36,6 @@ enum class AlfRule : uint32_t CONG, // n-ary congruence NARY_CONG, - // concat conflict disequality - CONCAT_CONFLICT_DEQ, // Used in case that a step in the proof rule could not be translated. UNDEFINED }; diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index 2d196fda030..00ac11f501d 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -434,6 +434,7 @@ void InferProofCons::convert(InferenceId infer, std::vector childrenC; childrenC.push_back(mainEqCeq); // if it is between sequences, we require the explicit disequality + ProofRule r = ProofRule::CONCAT_CONFLICT; if (mainEqCeq[0].getType().isSequence()) { Assert(t0.isConst() && s0.isConst()); @@ -442,11 +443,11 @@ void InferProofCons::convert(InferenceId infer, psb.addStep(ProofRule::MACRO_SR_PRED_INTRO, {}, {deq}, deq); Assert(!deq.isNull()); childrenC.push_back(deq); + r = ProofRule::CONCAT_CONFLICT_DEQ; } std::vector argsC; argsC.push_back(nodeIsRev); - Node conflict = - psb.tryStep(ProofRule::CONCAT_CONFLICT, childrenC, argsC); + Node conflict = psb.tryStep(r, childrenC, argsC); if (conflict == conc) { useBuffer = true; diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp index ccdf5b40ca8..c620170cc62 100644 --- a/src/theory/strings/proof_checker.cpp +++ b/src/theory/strings/proof_checker.cpp @@ -37,6 +37,7 @@ void StringProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(ProofRule::CONCAT_EQ, this); pc->registerChecker(ProofRule::CONCAT_UNIFY, this); pc->registerChecker(ProofRule::CONCAT_CONFLICT, this); + pc->registerChecker(ProofRule::CONCAT_CONFLICT_DEQ, this); pc->registerChecker(ProofRule::CONCAT_SPLIT, this); pc->registerChecker(ProofRule::CONCAT_CSPLIT, this); pc->registerChecker(ProofRule::CONCAT_LPROP, this); @@ -179,7 +180,8 @@ Node StringProofRuleChecker::checkInternal(ProofRule id, } return children[1][0][0].eqNode(children[1][1][0]); } - else if (id == ProofRule::CONCAT_CONFLICT) + else if (id == ProofRule::CONCAT_CONFLICT + || id == ProofRule::CONCAT_CONFLICT_DEQ) { Assert(children.size() >= 1 && children.size() <= 2); if (!t0.isConst() || !s0.isConst()) @@ -196,9 +198,9 @@ Node StringProofRuleChecker::checkInternal(ProofRule id, return Node::null(); } // if a disequality was provided, ensure that it is correct - if (children.size() == 2) + if (id == ProofRule::CONCAT_CONFLICT_DEQ) { - if (children[1].getKind() != Kind::NOT + if (children.size() != 2 || children[1].getKind() != Kind::NOT || children[1][0].getKind() != Kind::EQUAL || children[1][0][0] != t0 || children[1][0][1] != s0) { @@ -207,7 +209,7 @@ Node StringProofRuleChecker::checkInternal(ProofRule id, } else if (t0.getType().isSequence()) { - // we require the disequality for sequences + // we require the CONCAT_CONFLICT_DEQ for sequences return Node::null(); } return nm->mkConst(false); From 06806d63cfc8a7ec6af3b5f08bfaf705998e0b5d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 6 Feb 2024 09:19:30 -0600 Subject: [PATCH 10/18] Update ProofRule::ALPHA_EQUIV and add support in ALF (#10340) --- include/cvc5/cvc5_proof_rule.h | 2 +- proofs/alf/programs/Quantifiers.smt3 | 1 - proofs/alf/rules/Quantifiers.smt3 | 8 ++++++ src/proof/alf/alf_printer.cpp | 1 + src/theory/quantifiers/alpha_equivalence.cpp | 9 +++---- src/theory/quantifiers/proof_checker.cpp | 28 +++++++++----------- 6 files changed, 26 insertions(+), 23 deletions(-) diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h index e106cf5bd48..ae8cc05c88d 100644 --- a/include/cvc5/cvc5_proof_rule.h +++ b/include/cvc5/cvc5_proof_rule.h @@ -1310,7 +1310,7 @@ enum ENUM(ProofRule) : uint32_t * * .. math:: * - * \inferruleSC{-\mid F, y_1=z_1,\dots, y_n=z_n} + * \inferruleSC{-\mid F, (y_1 \ldots y_n), (z_1,\dots, z_n)} * {F = F\{y_1\mapsto z_1,\dots,y_n\mapsto z_n\}} * {if $y_1,\dots,y_n, z_1,\dots,z_n$ are unique bound variables} * diff --git a/proofs/alf/programs/Quantifiers.smt3 b/proofs/alf/programs/Quantifiers.smt3 index 415579e89fd..828f8b0855c 100644 --- a/proofs/alf/programs/Quantifiers.smt3 +++ b/proofs/alf/programs/Quantifiers.smt3 @@ -19,4 +19,3 @@ ((substitute_list @list.nil @list.nil F) F) ) ) - diff --git a/proofs/alf/rules/Quantifiers.smt3 b/proofs/alf/rules/Quantifiers.smt3 index 9dae962bcaf..89e5e99c1fb 100644 --- a/proofs/alf/rules/Quantifiers.smt3 +++ b/proofs/alf/rules/Quantifiers.smt3 @@ -39,3 +39,11 @@ ) ) ) + +; B is the formula to apply to +; vs is a list of variables to substitution for the variable list ts +; Note we don't currently check whether this is valid renaming. +(declare-rule alpha_equiv ((B Bool) (vs @List) (ts @List)) + :args (B vs ts) + :conclusion (= B (substitute_list vs ts B)) +) diff --git a/src/proof/alf/alf_printer.cpp b/src/proof/alf/alf_printer.cpp index dee138e0797..28c8bb11a62 100644 --- a/src/proof/alf/alf_printer.cpp +++ b/src/proof/alf/alf_printer.cpp @@ -129,6 +129,7 @@ bool AlfPrinter::isHandled(const ProofNode* pfn) const case ProofRule::REMOVE_TERM_FORMULA_AXIOM: case ProofRule::INSTANTIATE: case ProofRule::SKOLEMIZE: + case ProofRule::ALPHA_EQUIV: case ProofRule::ENCODE_PRED_TRANSFORM: case ProofRule::DSL_REWRITE: // alf rule is handled diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index 3b530f4bb4a..1b3e7af0923 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -209,12 +209,9 @@ TrustNode AlphaEquivalence::reduceQuantifier(Node q) { std::vector pfArgs; pfArgs.push_back(ret); - for (size_t i = 0, nvars = vars.size(); i < nvars; i++) - { - pfArgs.push_back(vars[i].eqNode(subs[i])); - Trace("alpha-eq") << "subs: " << vars[i] << " -> " << subs[i] - << std::endl; - } + NodeManager* nm = NodeManager::currentNM(); + pfArgs.push_back(nm->mkNode(Kind::SEXPR, vars)); + pfArgs.push_back(nm->mkNode(Kind::SEXPR, subs)); CDProof cdp(d_env); Node sret = ret.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); diff --git a/src/theory/quantifiers/proof_checker.cpp b/src/theory/quantifiers/proof_checker.cpp index 388388e8732..1b410405de9 100644 --- a/src/theory/quantifiers/proof_checker.cpp +++ b/src/theory/quantifiers/proof_checker.cpp @@ -100,33 +100,31 @@ Node QuantifiersProofRuleChecker::checkInternal( else if (id == ProofRule::ALPHA_EQUIV) { Assert(children.empty()); - if (args[0].getKind() != Kind::FORALL) + Assert(args.size() == 3); + // must be lists of the same length + if (args[1].getKind() != Kind::SEXPR || args[2].getKind() != Kind::SEXPR + || args[1].getNumChildren() != args[2].getNumChildren()) { return Node::null(); } - // arguments must be equalities that are bound variables that are - // pairwise unique + // arguments must be lists of bound variables that are pairwise unique std::unordered_set allVars[2]; std::vector vars; std::vector newVars; - for (size_t i = 1, nargs = args.size(); i < nargs; i++) + for (size_t i = 0, nargs = args[1].getNumChildren(); i < nargs; i++) { - if (args[i].getKind() != Kind::EQUAL) + for (size_t j = 1; j <= 2; j++) { - return Node::null(); - } - for (size_t j = 0; j < 2; j++) - { - Node v = args[i][j]; - if (v.getKind() != Kind::BOUND_VARIABLE - || allVars[j].find(v) != allVars[j].end()) + Node v = args[j][i]; + std::unordered_set& av = allVars[j - 1]; + if (v.getKind() != Kind::BOUND_VARIABLE || av.find(v) != av.end()) { return Node::null(); } - allVars[j].insert(v); + av.insert(v); } - vars.push_back(args[i][0]); - newVars.push_back(args[i][1]); + vars.push_back(args[1][i]); + newVars.push_back(args[2][i]); } Node renamedBody = args[0].substitute( vars.begin(), vars.end(), newVars.begin(), newVars.end()); From 2711528c64927ec1d42935c73b774c89b2bb7021 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 6 Feb 2024 10:49:48 -0600 Subject: [PATCH 11/18] Remove spurious assertion from ALF printer (#10351) Fixes the nightlies. --- src/proof/alf/alf_printer.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/proof/alf/alf_printer.cpp b/src/proof/alf/alf_printer.cpp index 28c8bb11a62..6b2372f12ac 100644 --- a/src/proof/alf/alf_printer.cpp +++ b/src/proof/alf/alf_printer.cpp @@ -410,7 +410,6 @@ void AlfPrinter::printStepPre(AlfPrintChannel* out, const ProofNode* pn) if (r == ProofRule::SCOPE) { const std::vector& args = pn->getArguments(); - Assert(!args.empty()); for (const Node& a : args) { size_t aid = allocateAssumePushId(pn, a); From d8f176be4eb484988d696764e00ac85f0f2389c9 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Tue, 6 Feb 2024 11:38:28 -0600 Subject: [PATCH 12/18] ci: Upgrade setup-python to v5 (#10322) --- .github/actions/package-python-wheel-macos/action.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/actions/package-python-wheel-macos/action.yml b/.github/actions/package-python-wheel-macos/action.yml index 6850d142d73..78edc63b10a 100644 --- a/.github/actions/package-python-wheel-macos/action.yml +++ b/.github/actions/package-python-wheel-macos/action.yml @@ -10,7 +10,7 @@ inputs: runs: using: composite steps: - - uses: actions/setup-python@v4 + - uses: actions/setup-python@v5 if: runner.os == 'macOS' with: python-version: ${{ inputs.python-version }} From bd7ffe86b024f9c338815f18eef1eb3b815d4a59 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Tue, 6 Feb 2024 10:27:47 -0800 Subject: [PATCH 13/18] [proofs] Using user names in proof assumptions (#10344) Extends the API with the functionality and the Alethe backend to use it. This functionality is important, in the same way as for unsat cores, for users to know which assumptions in the proof correspond to the assertions in the problem. --- include/cvc5/cvc5.h | 6 +++++- src/api/cpp/cvc5.cpp | 13 +++++++++++-- src/parser/commands.cpp | 5 ++++- src/proof/alethe/alethe_printer.cpp | 20 +++++++++++++++----- src/proof/alethe/alethe_printer.h | 6 +++++- src/smt/proof_manager.cpp | 5 +++-- src/smt/proof_manager.h | 4 +++- src/smt/solver_engine.cpp | 5 +++-- src/smt/solver_engine.h | 3 ++- 9 files changed, 51 insertions(+), 16 deletions(-) diff --git a/include/cvc5/cvc5.h b/include/cvc5/cvc5.h index 2f7bc28bc6c..4a01e20e7fb 100644 --- a/include/cvc5/cvc5.h +++ b/include/cvc5/cvc5.h @@ -4642,11 +4642,15 @@ class CVC5_EXPORT Solver * @param format The proof format used to print the proof. Must be * `modes::ProofFormat::NONE` if the proof is from a component other than * `modes::ProofComponent::FULL`. + * @param assertionNames Mapping between assertions and names, if they were + * given by the user. * @return The string representation of the proof in the given format. */ std::string proofToString( Proof proof, - modes::ProofFormat format = modes::ProofFormat::DEFAULT) const; + modes::ProofFormat format = modes::ProofFormat::DEFAULT, + const std::map& assertionNames = + std::map()) const; /** * Get a list of learned literals that are entailed by the current set of diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 49c1258357c..1b2217b185b 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -7385,12 +7385,21 @@ std::vector Solver::getProof(modes::ProofComponent c) const CVC5_API_TRY_CATCH_END; } -std::string Solver::proofToString(Proof proof, modes::ProofFormat format) const +std::string Solver::proofToString( + Proof proof, + modes::ProofFormat format, + const std::map& assertionNames) const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line std::ostringstream ss; - this->d_slv->printProof(ss, proof.getProofNode(), format); + // convert the map's domain to use nodes rather than terms + std::map nodeAssertionNames; + for (const auto& p : assertionNames) + { + nodeAssertionNames[p.first.getNode()] = p.second; + } + this->d_slv->printProof(ss, proof.getProofNode(), format, nodeAssertionNames); return ss.str(); //////// CVC5_API_TRY_CATCH_END; diff --git a/src/parser/commands.cpp b/src/parser/commands.cpp index 11b8edb521d..a423170587e 100644 --- a/src/parser/commands.cpp +++ b/src/parser/commands.cpp @@ -1586,7 +1586,10 @@ void GetProofCommand::invoke(cvc5::Solver* solver, SymManager* sm) { ss << "(!" << std::endl; } - ss << solver->proofToString(p, format); + // get assertions, and build a map between them and their names + std::map assertionNames = + sm->getExpressionNames(true); + ss << solver->proofToString(p, format, assertionNames); if (commentProves) { ss << ":proves " << p.getResult() << ")" << std::endl; diff --git a/src/proof/alethe/alethe_printer.cpp b/src/proof/alethe/alethe_printer.cpp index 657b0668519..335e11a810a 100644 --- a/src/proof/alethe/alethe_printer.cpp +++ b/src/proof/alethe/alethe_printer.cpp @@ -82,8 +82,10 @@ void AletheProofPrinter::printTerm(std::ostream& out, TNode n) out << ss.str(); } -void AletheProofPrinter::print(std::ostream& out, - std::shared_ptr pfn) +void AletheProofPrinter::print( + std::ostream& out, + std::shared_ptr pfn, + const std::map& assertionNames) { Trace("alethe-printer") << "- Print proof in Alethe format. " << std::endl; std::shared_ptr innerPf = pfn->getChildren()[0]; @@ -119,11 +121,19 @@ void AletheProofPrinter::print(std::ostream& out, // Print assumptions and add them to the list but do not print anchor. for (size_t i = 3, size = args.size(); i < size; i++) { - // assumptions are always being declared - out << "(assume a" << i - 3 << " "; + auto it = assertionNames.find(args[i]); + if (it != assertionNames.end()) + { + out << "(assume " << it->second << " "; + assumptions[args[i]] = it->second; + } + else + { // assumptions are always being declared + out << "(assume a" << i - 3 << " "; + assumptions[args[i]] = "a" + std::to_string(i - 3); + } printTerm(out, args[i]); out << ")\n"; - assumptions[args[i]] = "a" + std::to_string(i - 3); } // Then, print the rest of the proof node uint32_t start_t = 1; diff --git a/src/proof/alethe/alethe_printer.h b/src/proof/alethe/alethe_printer.h index f1cde85b852..791a9eff93f 100644 --- a/src/proof/alethe/alethe_printer.h +++ b/src/proof/alethe/alethe_printer.h @@ -69,8 +69,12 @@ class AletheProofPrinter : protected EnvObj * * @param out The stream to write to * @param pfn The proof node to be printed + * @param assertionNames Mapping between assertions and names, if they were + * given by the user. */ - void print(std::ostream& out, std::shared_ptr pfn); + void print(std::ostream& out, + std::shared_ptr pfn, + const std::map& assertionNames); private: /** Used for printing the proof node after the initial Alethe anchor has been diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 3eccb638904..146120e8bd8 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -229,7 +229,8 @@ std::shared_ptr PfManager::connectProofToAssertions( void PfManager::printProof(std::ostream& out, std::shared_ptr fp, - options::ProofFormatMode mode) + options::ProofFormatMode mode, + const std::map& assertionNames) { Trace("smt-proof") << "PfManager::printProof: start" << std::endl; // We don't want to invalidate the proof nodes in fp, since these may be @@ -262,7 +263,7 @@ void PfManager::printProof(std::ostream& out, d_env, anc, options().proof.proofAletheResPivots); vpfpp.process(fp); proof::AletheProofPrinter vpp(d_env); - vpp.print(out, fp); + vpp.print(out, fp, assertionNames); } else if (mode == options::ProofFormatMode::LFSC) { diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h index f678aee6632..94a58d76864 100644 --- a/src/smt/proof_manager.h +++ b/src/smt/proof_manager.h @@ -95,7 +95,9 @@ class PfManager : protected EnvObj */ void printProof(std::ostream& out, std::shared_ptr fp, - options::ProofFormatMode mode); + options::ProofFormatMode mode, + const std::map& assertionNames = + std::map()); /** * Translate difficulty map. This takes a mapping dmap from preprocessed diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index d127853e8a0..a2715d9a251 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -1388,7 +1388,8 @@ std::vector SolverEngine::convertPreprocessedToInput( void SolverEngine::printProof(std::ostream& out, std::shared_ptr fp, - modes::ProofFormat proofFormat) + modes::ProofFormat proofFormat, + const std::map& assertionNames) { // we print in the format based on the proof mode options::ProofFormatMode mode = options::ProofFormatMode::NONE; @@ -1405,7 +1406,7 @@ void SolverEngine::printProof(std::ostream& out, case modes::ProofFormat::LFSC: mode = options::ProofFormatMode::LFSC; break; } - d_pfManager->printProof(out, fp, mode); + d_pfManager->printProof(out, fp, mode, assertionNames); out << std::endl; } diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index 5b98abc9208..a3b77df4d56 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -1047,7 +1047,8 @@ class CVC5_EXPORT SolverEngine */ void printProof(std::ostream& out, std::shared_ptr fp, - modes::ProofFormat proofFormat); + modes::ProofFormat proofFormat, + const std::map& assertionNames); /* Members -------------------------------------------------------------- */ From bb14490bb7b82ffe3a5e9220c0d1cf199c27e69b Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Tue, 6 Feb 2024 13:15:02 -0600 Subject: [PATCH 14/18] ci: Include licenses directory in cvc5 packages (#10352) --- .github/actions/add-package/action.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/actions/add-package/action.yml b/.github/actions/add-package/action.yml index eeaaec3ee2e..0a82e3f4792 100644 --- a/.github/actions/add-package/action.yml +++ b/.github/actions/add-package/action.yml @@ -26,8 +26,9 @@ runs: # only work for the specific CI Python version. rm -rf ${{ inputs.build-dir }}/install/lib/python* - # Copy COPYING file to install directory + # Copy COPYING file and licenses directory to install directory cp COPYING ${{ inputs.build-dir }}/install/ + cp -r licenses ${{ inputs.build-dir }}/install/ # Create ZIP file pushd ${{ inputs.build-dir }} From 566104905f14a1ab71666c271acf41b14511a97b Mon Sep 17 00:00:00 2001 From: "Andrew V. Teylu" Date: Tue, 6 Feb 2024 21:23:11 +0000 Subject: [PATCH 15/18] Fix some `clang` warnings when compiling approx_simplex (#10314) This PR fixes some compilation warnings you get when compiling `cvc5` under "newer `clang`s" (warnings appear with `clang` 17 on openSUSE and Apple `clang` 15). Signed-off-by: Andrew V. Teylu --- src/theory/arith/linear/approx_simplex.cpp | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/theory/arith/linear/approx_simplex.cpp b/src/theory/arith/linear/approx_simplex.cpp index 15fb3ae96ed..336fa52db38 100644 --- a/src/theory/arith/linear/approx_simplex.cpp +++ b/src/theory/arith/linear/approx_simplex.cpp @@ -136,8 +136,8 @@ struct CutScratchPad { } }; -class GmiInfo; -class MirInfo; +struct GmiInfo; +struct MirInfo; class BranchCutInfo; class ApproxGLPK : public ApproximateSimplex @@ -257,10 +257,6 @@ class ApproxGLPK : public ApproximateSimplex bool replaceSlacksOnCuts(); bool loadVB(int nid, int M, int j, int ri, bool wantUb, VirtualBound& tmp); - double sumInfeasibilities(bool mip) const - { - return sumInfeasibilities(mip? d_mipProb : d_realProb); - } double sumInfeasibilities(glp_prob* prob, bool mip) const; /** UTILITIES FOR DEALING WITH ESTIMATES */ From da91f0d166011efb1b8893e3c5abe4428dc27fd6 Mon Sep 17 00:00:00 2001 From: "Andrew V. Teylu" Date: Tue, 6 Feb 2024 22:23:01 +0000 Subject: [PATCH 16/18] Setup Python 'requirement.txt' files for building and Python development (#10315) I always forget what packages I need to install inside of a venv to build cvc5. This PR adds two requirements.txt files: requirements_build.txt for the Python packages you need to install to build cvc5 requirements_python_dev.txt for the Python packages you need to build cvc5's Python bindings Signed-off-by: Andrew V. Teylu andrew@tey.lu --- INSTALL.rst | 7 +++++++ contrib/packaging_python/mk_clean_wheel.sh | 3 ++- contrib/requirements_build.txt | 2 ++ contrib/requirements_python_dev.txt | 3 +++ docs/api/python/python.rst | 2 +- 5 files changed, 15 insertions(+), 2 deletions(-) create mode 100644 contrib/requirements_build.txt create mode 100644 contrib/requirements_python_dev.txt diff --git a/INSTALL.rst b/INSTALL.rst index 46b8381bbdb..c14ae333f15 100644 --- a/INSTALL.rst +++ b/INSTALL.rst @@ -125,6 +125,9 @@ versions; more recent versions should be compatible. - `CaDiCaL (SAT solver) `_ - `SymFPU `_ +For Python, to install these dependencies automatically, please use: + + - `pip install -r contrib/requirements_build.txt` CaDiCaL (SAT solver) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ @@ -258,6 +261,10 @@ Dependencies for Language Bindings - `pytest `_ - The source for the `pythonic API <(https://github.com/cvc5/cvc5_pythonic_api)>`. +For Python, to install these depedencies automatically, please use: + + - `pip install -r contrib/requirements_python_dev.txt` + If configured with ``--pythonic-path=PATH``, the build system will expect the Pythonic API's source to be at ``PATH``. Otherwise, if configured with ``--auto-download``, the build system will download it. diff --git a/contrib/packaging_python/mk_clean_wheel.sh b/contrib/packaging_python/mk_clean_wheel.sh index a69a7673a83..27e13dcf4a0 100755 --- a/contrib/packaging_python/mk_clean_wheel.sh +++ b/contrib/packaging_python/mk_clean_wheel.sh @@ -40,7 +40,8 @@ source ./$ENVDIR/bin/activate # install packages pip install -q --upgrade pip setuptools auditwheel -pip install -q Cython pytest tomli scikit-build flex pyparsing +pip install -r contrib/requirements_build.txt +pip install -r contrib/requirements_python_dev.txt if [ "$(uname)" == "Darwin" ]; then # Mac version of auditwheel pip install -q delocate diff --git a/contrib/requirements_build.txt b/contrib/requirements_build.txt new file mode 100644 index 00000000000..b1d0a9aa1d1 --- /dev/null +++ b/contrib/requirements_build.txt @@ -0,0 +1,2 @@ +tomli +pyparsing diff --git a/contrib/requirements_python_dev.txt b/contrib/requirements_python_dev.txt new file mode 100644 index 00000000000..125abe538fd --- /dev/null +++ b/contrib/requirements_python_dev.txt @@ -0,0 +1,3 @@ +Cython +pytest +scikit-build diff --git a/docs/api/python/python.rst b/docs/api/python/python.rst index 0f020d03368..4efc645c387 100644 --- a/docs/api/python/python.rst +++ b/docs/api/python/python.rst @@ -47,7 +47,7 @@ Before building and installing, the following dependencies should be installed, .. code:: bash brew install cmake python gmp java - pip3 install cython tomli scikit-build pyparsing + pip3 install -r contrib/requirements_python_dev.txt Then `cvc5` can be installed from source as follows: From 119615647dd588e4b6ca09a0d82f4d7c3033bf8c Mon Sep 17 00:00:00 2001 From: "Andrew V. Teylu" Date: Tue, 6 Feb 2024 23:16:03 +0000 Subject: [PATCH 17/18] Add support for Python 3.12 (#10316) This PR adds support for Python 3.12 while building `cvc5` (there's no functional changes in this PR really, apart from changing the message in `INSTALL.rst` to say that Python 3.11 and 3.12 also work). Signed-off-by: Andrew V. Teylu --- INSTALL.rst | 2 +- src/api/python/cvc5.pxi | 8 ++++---- src/api/python/genenums.py.in | 18 +++++++++--------- src/base/collect_tags.py | 2 +- 4 files changed, 15 insertions(+), 15 deletions(-) diff --git a/INSTALL.rst b/INSTALL.rst index c14ae333f15..40ffa82dce3 100644 --- a/INSTALL.rst +++ b/INSTALL.rst @@ -118,7 +118,7 @@ versions; more recent versions should be compatible. - `GNU C and C++ (gcc and g++, >= 7) `_ or `Clang (>= 5) `_ - `CMake >= 3.9 `_ -- `Python >= 3.6 and <= 3.10 `_ +- `Python >= 3.6 `_ + module `tomli `_ + module `pyparsing `_ - `GMP v6.3 (GNU Multi-Precision arithmetic library) `_ diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index fcf57384a5c..6821430d94a 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -1559,7 +1559,7 @@ cdef class Solver: if a < 0 or a >= 2 ** 31: raise ValueError( "Argument {} must fit in a uint32_t".format(a)) - v.push_back(( a)) + v.push_back( a) op.cop = self.csolver.mkOp( k.value, v) return op @@ -1618,7 +1618,7 @@ cdef class Solver: str(val).encode()) else: assert(isinstance(val, int)) - term.cterm = self.csolver.mkInteger(( val)) + term.cterm = self.csolver.mkInteger( val) return term def mkReal(self, numerator, denominator=None): @@ -3103,7 +3103,7 @@ cdef class Solver: free variables in :math:`y_1...y_n` - If :math:`Q` is :math:`\\exists`, let :math:`(A \\wedge Q_n)` be the formula - :math:`(A \\wedge \\neg (\\phi \wedge Q_1) \\wedge ... \\wedge \\neg (\\phi \\wedge Q_n))` + :math:`(A \\wedge \\neg (\\phi \\wedge Q_1) \\wedge ... \\wedge \\neg (\\phi \\wedge Q_n))` where for each :math:`i = 1...n`, formula :math:`(\\phi \\wedge Q_i)` is the result of calling :py:meth:`getQuantifierEliminationDisjunct()` @@ -4553,7 +4553,7 @@ cdef class Term: return (get0(t), get1(t), term) def isSetValue(self): - """ + r""" A term is a set value if it is considered to be a (canonical) constant set value. A canonical set value is one whose AST is: diff --git a/src/api/python/genenums.py.in b/src/api/python/genenums.py.in index efca44d0324..238c5afa8bc 100644 --- a/src/api/python/genenums.py.in +++ b/src/api/python/genenums.py.in @@ -71,15 +71,15 @@ comment_repls = [ (':cpp:func:`(.*?)`', '\\1'), (':cpp:enumerator:`(.*?)`', ':py:obj:`\\1`'), # introduce proper python references - ('Term::([a-zA-Z]+)\(([^)]*)\)', ':py:meth:`Term.\\1()`'), - ('Solver::([a-zA-Z]+)\(([^)]*)\) const', ':py:meth:`Solver.\\1()`'), - ('Solver::([a-zA-Z]+)\(([^)]*)\)', ':py:meth:`Solver.\\1()`'), - ('DatatypeConstructor::([a-zA-Z]+)\(([^)]*)\) const', ':py:meth:`DatatypeConstructor.\\1()`'), - ('DatatypeConstructor::([a-zA-Z]+)\(([^)]*)\)', ':py:meth:`DatatypeConstructor.\\1()`'), - ('Datatype::([a-zA-Z]+)\(([^)]*)\) const', ':py:meth:`Datatype.\\1()`'), - ('Datatype::([a-zA-Z]+)\(([^)]*)\)', ':py:meth:`Datatype.\\1()`'), - ('DatatypeSelector::([a-zA-Z]+)\(([^)]*)\) const', ':py:meth:`DatatypeSelector.\\1()`'), - ('DatatypeSelector::([a-zA-Z]+)\(([^)]*)\)', ':py:meth:`DatatypeSelector.\\1()`'), + (r'Term::([a-zA-Z]+)\(([^)]*)\)', ':py:meth:`Term.\\1()`'), + (r'Solver::([a-zA-Z]+)\(([^)]*)\) const', ':py:meth:`Solver.\\1()`'), + (r'Solver::([a-zA-Z]+)\(([^)]*)\)', ':py:meth:`Solver.\\1()`'), + (r'DatatypeConstructor::([a-zA-Z]+)\(([^)]*)\) const', ':py:meth:`DatatypeConstructor.\\1()`'), + (r'DatatypeConstructor::([a-zA-Z]+)\(([^)]*)\)', ':py:meth:`DatatypeConstructor.\\1()`'), + (r'Datatype::([a-zA-Z]+)\(([^)]*)\) const', ':py:meth:`Datatype.\\1()`'), + (r'Datatype::([a-zA-Z]+)\(([^)]*)\)', ':py:meth:`Datatype.\\1()`'), + (r'DatatypeSelector::([a-zA-Z]+)\(([^)]*)\) const', ':py:meth:`DatatypeSelector.\\1()`'), + (r'DatatypeSelector::([a-zA-Z]+)\(([^)]*)\)', ':py:meth:`DatatypeSelector.\\1()`'), ('\\\\', '\\\\\\\\'), ] diff --git a/src/base/collect_tags.py b/src/base/collect_tags.py index 3534584ab13..ce0b27229ac 100644 --- a/src/base/collect_tags.py +++ b/src/base/collect_tags.py @@ -33,7 +33,7 @@ def parse_args(): { 'patterns' : ['assertions::pre-{}', 'assertions::post-{}'], 'collector' : lambda basedir: - re.findall('registerPassInfo\("([a-z-]+)"', + re.findall(r'registerPassInfo\("([a-z-]+)"', open(os.path.join(basedir, 'preprocessing', 'preprocessing_pass_registry.cpp')).read() ) } From e5195d69a1d73c34c80ed6274d546eac1017e2b4 Mon Sep 17 00:00:00 2001 From: "Andrew V. Teylu" Date: Wed, 7 Feb 2024 00:07:50 +0000 Subject: [PATCH 18/18] Bump CLN to 1.3.7 (#10318) This PR bumps CLN to 1.3.7. This is to resolve a build issue I have with Apple `clang` 15. Signed-off-by: Andrew V. Teylu --- cmake/FindCLN.cmake | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/cmake/FindCLN.cmake b/cmake/FindCLN.cmake index f74be293a14..6a02a403ac1 100644 --- a/cmake/FindCLN.cmake +++ b/cmake/FindCLN.cmake @@ -44,7 +44,7 @@ if(NOT CLN_FOUND_SYSTEM) fail_if_cross_compiling("Windows" "" "CLN" "autoconf fails") fail_if_cross_compiling("" "arm" "CLN" "syntax error in configure") - set(CLN_VERSION "1.3.6") + set(CLN_VERSION "1.3.7") string(REPLACE "." "-" CLN_TAG ${CLN_VERSION}) find_program(AUTORECONF autoreconf) @@ -56,7 +56,7 @@ if(NOT CLN_FOUND_SYSTEM) CLN-EP ${COMMON_EP_CONFIG} URL "https://www.ginac.de/CLN/cln.git/?p=cln.git\\\;a=snapshot\\\;h=cln_${CLN_TAG}\\\;sf=tgz" - URL_HASH SHA1=71d02b90ef0575f06b7bafb8690f73e8064d8228 + URL_HASH SHA1=bd6dec17cf1088bdd592794d9239d47c752cf3da DOWNLOAD_NAME cln.tgz CONFIGURE_COMMAND ${CMAKE_COMMAND} -E chdir ./autogen.sh