From 2e97dc2a19b4daa9fa996597ef08b678fcfbd2a3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 17 Dec 2024 08:13:03 -0600 Subject: [PATCH 1/9] Add Eunoia definitions of 3 datatype ad-hoc rewrites (#11443) Does some minor reorg of signature files. Also moves ARITH_POLY_NORM to fully supported, which was missed on a previous PR. --- proofs/eo/cpc/programs/Datatypes.eo | 75 ++++++++++++ proofs/eo/cpc/programs/Utils.eo | 15 ++- proofs/eo/cpc/rules/Datatypes.eo | 110 +++++++++--------- src/proof/alf/alf_printer.cpp | 11 +- .../quantifiers/stream-x2014-09-18-unsat.smt2 | 1 + 5 files changed, 151 insertions(+), 61 deletions(-) create mode 100644 proofs/eo/cpc/programs/Datatypes.eo diff --git a/proofs/eo/cpc/programs/Datatypes.eo b/proofs/eo/cpc/programs/Datatypes.eo new file mode 100644 index 00000000000..1f0c7f1f1fe --- /dev/null +++ b/proofs/eo/cpc/programs/Datatypes.eo @@ -0,0 +1,75 @@ +(include "../theories/Datatypes.eo") + +; program: $dt_get_constructors +; args: +; - T Type: The datatype to get the constructors for. +; return: The list of constructors of T, as a eo::List. +; note: > +; (Unit) tuples are treated as a special case of datatypes with a single +; constructor. Parametric datatypes must reference the type constructor to +; extract their constructors. +(program $dt_get_constructors ((D Type) (T Type) (c T) (T1 Type) (T2 Type :list) (DC (-> Type Type))) + (Type) eo::List + ( + (($dt_get_constructors (Tuple T1 T2)) (eo::cons eo::List::cons tuple eo::List::nil)) + (($dt_get_constructors UnitTuple) (eo::cons eo::List::cons tuple.unit eo::List::nil)) + (($dt_get_constructors (DC T)) ($dt_get_constructors DC)) ; user-defined parameteric datatypes, traverse + (($dt_get_constructors D) (eo::dt_constructors D)) ; ordinary user-defined datatypes + ) +) + +; program: $tuple_get_selectors_rec +; args: +; - T Type: The tuple type to get the selectors for. +; - n Int: The number of component types we have processed so far. +; return: The list of selectors of T, as a eo::List. +; note: > +; Tuples use a special selector tuple.select indexed by an integer, which is +; why they require a special method here. +(program $tuple_get_selectors_rec ((D Type) (T Type) (t T) (T1 Type) (T2 Type :list) (n Int)) + (Type Int) Bool + ( + (($tuple_get_selectors_rec UnitTuple n) eo::List::nil) + (($tuple_get_selectors_rec (Tuple T1 T2) n) (eo::cons eo::List::cons (tuple.select n) ($tuple_get_selectors_rec T2 (eo::add n 1)))) + ) +) + +; program: $dt_get_selectors +; args: +; - D Type: The type to get the selectors for. +; - c T: The constructor of D. +; return: The list of selectors of c, as a eo::List. +; note: > +; (Unit) tuples are treated as a special case of datatypes whose selectors are +; tuple.select indexed by an integer, which requires the above method. +(program $dt_get_selectors ((D Type) (T Type) (c Type) (T1 Type) (T2 Type :list)) + (Type T) eo::List + ( + (($dt_get_selectors (Tuple T1 T2) tuple) ($tuple_get_selectors_rec (Tuple T1 T2) 0)) + (($dt_get_selectors UnitTuple tuple.unit) eo::List::nil) + (($dt_get_selectors D c) (eo::dt_selectors c)) ; user-defined datatypes + ) +) + +; define: $dt_is_cons +; args: +; - t T: The term in question. +; return: true iff t is a constructor symbol. +(define $dt_is_cons ((T Type :implicit) (t T)) + (eo::is_z (eo::list_len eo::List::cons (eo::dt_selectors t)))) + +; define: $dt_arg_nth +; args: +; - t T: The term to inspect, expected to be a constructor application. +; - n Int: The index of the argument to get. +; return: > +; The nth argument of t. +(program $dt_arg_nth ((T Type) (U Type) (V Type) (W Type) (t T) (n Int) (t1 V) (t2 W :list)) + (T Int) U + ( + ; for tuples, use nth on tuple as an n-ary constructor + (($dt_arg_nth (tuple t1 t2) n) (eo::list_nth tuple (tuple t1 t2) n)) + ; otherwise we get the argument list + (($dt_arg_nth t n) (eo::list_nth @list ($get_arg_list t) n)) + ) +) diff --git a/proofs/eo/cpc/programs/Utils.eo b/proofs/eo/cpc/programs/Utils.eo index 3f96619a777..d4690bd3ee1 100644 --- a/proofs/eo/cpc/programs/Utils.eo +++ b/proofs/eo/cpc/programs/Utils.eo @@ -21,6 +21,19 @@ (declare-const @list.nil @List) (declare-const @list (-> (! Type :var T :implicit) T @List @List) :right-assoc-nil @list.nil) +; program: $get_fun +; args: +; - t S: The term to inspect. +; return: > +; The function at the head of the application of t, or t itself if it is not +; an application. +(program $get_fun ((T Type) (S Type) (U Type) (f (-> T S)) (x T) (y S)) + (S) U + ( + (($get_fun (f x)) ($get_fun f)) + (($get_fun y) y) + ) +) ; program: $get_arg_list_rec ; args: @@ -45,8 +58,6 @@ ; list if t is not a function application. (define $get_arg_list ((T Type :implicit) (t T)) ($get_arg_list_rec t @list.nil)) - - ; program: $is_app ; args: ; - f (-> T U): The function. diff --git a/proofs/eo/cpc/rules/Datatypes.eo b/proofs/eo/cpc/rules/Datatypes.eo index 7adaf46f2b0..8dd4ae47441 100644 --- a/proofs/eo/cpc/rules/Datatypes.eo +++ b/proofs/eo/cpc/rules/Datatypes.eo @@ -1,56 +1,5 @@ (include "../theories/Datatypes.eo") - - -; program: $dt_get_constructors -; args: -; - T Type: The datatype to get the constructors for. -; return: The list of constructors of T, as a eo::List. -; note: > -; (Unit) tuples are treated as a special case of datatypes with a single -; constructor. Parametric datatypes must reference the type constructor to -; extract their constructors. -(program $dt_get_constructors ((D Type) (T Type) (c T) (T1 Type) (T2 Type :list) (DC (-> Type Type))) - (Type) eo::List - ( - (($dt_get_constructors (Tuple T1 T2)) (eo::cons eo::List::cons tuple eo::List::nil)) - (($dt_get_constructors UnitTuple) (eo::cons eo::List::cons tuple.unit eo::List::nil)) - (($dt_get_constructors (DC T)) ($dt_get_constructors DC)) ; user-defined parameteric datatypes, traverse - (($dt_get_constructors D) (eo::dt_constructors D)) ; ordinary user-defined datatypes - ) -) - -; program: $tuple_get_selectors_rec -; args: -; - T Type: The tuple type to get the selectors for. -; - n Int: The number of component types we have processed so far. -; return: The list of selectors of T, as a eo::List. -; note: > -; Tuples use a special selector tuple.select indexed by an integer, which is -; why they require a special method here. -(program $tuple_get_selectors_rec ((D Type) (T Type) (t T) (T1 Type) (T2 Type :list) (n Int)) - (Type Int) Bool - ( - (($tuple_get_selectors_rec UnitTuple n) eo::List::nil) - (($tuple_get_selectors_rec (Tuple T1 T2) n) (eo::cons eo::List::cons (tuple.select n) ($tuple_get_selectors_rec T2 (eo::add n 1)))) - ) -) - -; program: $dt_get_selectors -; args: -; - D Type: The type to get the selectors for. -; - c T: The constructor of D. -; return: The list of selectors of c, as a eo::List. -; note: > -; (Unit) tuples are treated as a special case of datatypes whose selectors are -; tuple.select indexed by an integer, which requires the above method. -(program $dt_get_selectors ((D Type) (T Type) (c Type) (T1 Type) (T2 Type :list)) - (Type T) eo::List - ( - (($dt_get_selectors (Tuple T1 T2) tuple) ($tuple_get_selectors_rec (Tuple T1 T2) 0)) - (($dt_get_selectors UnitTuple tuple.unit) eo::List::nil) - (($dt_get_selectors D c) (eo::dt_selectors c)) ; user-defined datatypes - ) -) +(include "../programs/Datatypes.eo") ;;;;; ProofRule::DT_SPLIT @@ -144,3 +93,60 @@ :requires ((($mk_dt_inst (eo::typeof x) c x) t)) :conclusion (= (is c x) (= x t)) ) + +;;;;; ProofRewriteRule::DT_COLLAPSE_SELECTOR + +; rule: dt-collapse-selector +; implements: ProofRewriteRule::DT_COLLAPSE_SELECTOR. +; args: +; - eq Bool: The equality to prove. +; requires: > +; We require that the index^th argument of the term t we are selecting from +; is the right hand side of the equality, where index is the index of the +; selector in the constructor of t. +; conclusion: The given equality. +(declare-rule dt-collapse-selector ((D Type) (T Type) (s (-> D T)) (t D) (ti T)) + :args ((= (s t) ti)) + :requires (((eo::define ((c ($get_fun t))) + (eo::define ((ss ($dt_get_selectors (eo::typeof t) c))) + ; note that s must be a selector of the constructor of t, or else index will not evaluate + (eo::define ((index (eo::list_find eo::List::cons ss s))) + ($dt_arg_nth t index)))) ti)) + :conclusion (= (s t) ti) +) + +;;;;; ProofRewriteRule::DT_COLLAPSE_TESTER + +; rule: dt-collapse-tester +; implements: ProofRewriteRule::DT_COLLAPSE_TESTER. +; args: +; - eq Bool: The equality to prove. +; requires: > +; If the right hand side is true, then the function head of the term we are +; testing must be the constructor. If the right hand side is false, then the +; function head of the term we are testing must be the constructor that is +; not the constructor we are testing. +; conclusion: The given equality. +(declare-rule dt-collapse-tester ((D Type) (T Type) (c T) (t D) (b Bool)) + :args ((= (is c t) b)) + :requires (((eo::define ((f ($get_fun t))) + (eo::ite b + (eo::is_eq f c) + (eo::and ($dt_is_cons f) (eo::not (eo::is_eq f c))))) true)) + :conclusion (= (is c t) b) +) + +;;;;; ProofRewriteRule::DT_COLLAPSE_TESTER_SINGLETON + +; rule: dt-collapse-tester-singleton +; implements: ProofRewriteRule::DT_COLLAPSE_TESTER_SINGLETON. +; args: +; - eq Bool: The equality to prove. +; requires: > +; The number of constructors of the type of the term we are testing is one. +; conclusion: The given equality. +(declare-rule dt-collapse-tester-singleton ((D Type) (T Type) (c T) (t D)) + :args ((= (is c t) true)) + :requires (((eo::list_len eo::List::cons ($dt_get_constructors (eo::typeof t))) 1)) + :conclusion (= (is c t) true) +) diff --git a/src/proof/alf/alf_printer.cpp b/src/proof/alf/alf_printer.cpp index 9c2207c1df4..1aabb0d34e8 100644 --- a/src/proof/alf/alf_printer.cpp +++ b/src/proof/alf/alf_printer.cpp @@ -181,6 +181,7 @@ bool AlfPrinter::isHandled(const Options& opts, const ProofNode* pfn) case ProofRule::ENCODE_EQ_INTRO: case ProofRule::HO_APP_ENCODE: case ProofRule::ACI_NORM: + case ProofRule::ARITH_POLY_NORM: case ProofRule::ARITH_POLY_NORM_REL: case ProofRule::DSL_REWRITE: return true; case ProofRule::BV_BITBLAST_STEP: @@ -195,13 +196,6 @@ bool AlfPrinter::isHandled(const Options& opts, const ProofNode* pfn) return isHandledTheoryRewrite(id, pfn->getArguments()[1]); } break; - case ProofRule::ARITH_POLY_NORM: - { - // we don't support bitvectors yet - Assert(pargs[0].getKind() == Kind::EQUAL); - return pargs[0][0].getType().isRealOrInt(); - } - break; case ProofRule::ARITH_REDUCTION: { Kind k = pargs[0].getKind(); @@ -276,6 +270,9 @@ bool AlfPrinter::isHandledTheoryRewrite(ProofRewriteRule id, const Node& n) case ProofRewriteRule::QUANT_UNUSED_VARS: case ProofRewriteRule::ARRAYS_SELECT_CONST: case ProofRewriteRule::DT_INST: + case ProofRewriteRule::DT_COLLAPSE_SELECTOR: + case ProofRewriteRule::DT_COLLAPSE_TESTER: + case ProofRewriteRule::DT_COLLAPSE_TESTER_SINGLETON: case ProofRewriteRule::QUANT_MERGE_PRENEX: case ProofRewriteRule::QUANT_MINISCOPE_AND: case ProofRewriteRule::QUANT_MINISCOPE_OR: diff --git a/test/regress/cli/regress1/quantifiers/stream-x2014-09-18-unsat.smt2 b/test/regress/cli/regress1/quantifiers/stream-x2014-09-18-unsat.smt2 index 953589cc97b..615759ec05b 100644 --- a/test/regress/cli/regress1/quantifiers/stream-x2014-09-18-unsat.smt2 +++ b/test/regress/cli/regress1/quantifiers/stream-x2014-09-18-unsat.smt2 @@ -1,4 +1,5 @@ ; EXPECT: unsat +; DISABLE-TESTER: cpc (set-logic ALL) (set-info :status unsat) (declare-sort A$ 0) From fbbf9a7416842456bf30e6ce983e46cbdeda8058 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 17 Dec 2024 10:34:39 -0600 Subject: [PATCH 2/9] Add Eunoia definitions for 3 simple theory rewrites (#11449) Includes minor refactoring of the sets insert elimination rewrite to make the Eunoia definition simpler. --- proofs/eo/cpc/Cpc.eo | 6 ++-- proofs/eo/cpc/programs/Arith.eo | 26 ++++++++++++++++- proofs/eo/cpc/programs/BitVectors.eo | 22 +++++++------- proofs/eo/cpc/rules/Arith.eo | 15 ++++++++++ proofs/eo/cpc/rules/BitVectors.eo | 18 ++++++++++-- proofs/eo/cpc/rules/Sets.eo | 37 ++++++++++++++++++++++++ src/proof/alf/alf_printer.cpp | 3 ++ src/theory/sets/theory_sets_rewriter.cpp | 12 ++++---- 8 files changed, 116 insertions(+), 23 deletions(-) diff --git a/proofs/eo/cpc/Cpc.eo b/proofs/eo/cpc/Cpc.eo index e55143392c3..2fcbd9a804e 100644 --- a/proofs/eo/cpc/Cpc.eo +++ b/proofs/eo/cpc/Cpc.eo @@ -211,11 +211,11 @@ (($run_evaluate (bvsge xb yb)) (eo::define ((ex ($bv_to_signed_int ($run_evaluate xb)))) (eo::define ((ey ($bv_to_signed_int ($run_evaluate yb)))) (eo::or (eo::gt ex ey) (eo::is_eq ex ey))))) - (($run_evaluate (repeat n xb)) ($bv_eval_repeat ($run_evaluate n) ($run_evaluate xb))) + (($run_evaluate (repeat n xb)) ($run_evaluate ($bv_unfold_repeat ($run_evaluate n) ($run_evaluate xb)))) (($run_evaluate (sign_extend n xb)) (eo::define ((ex ($run_evaluate xb))) - (eo::concat ($bv_eval_repeat ($run_evaluate n) ($bv_sign_bit ex)) ex))) + (eo::concat ($run_evaluate ($bv_unfold_repeat ($run_evaluate n) ($bv_sign_bit ex))) ex))) (($run_evaluate (zero_extend n xb)) (eo::define ((ex ($run_evaluate xb))) - (eo::concat ($bv_eval_repeat ($run_evaluate n) #b0) ex))) + (eo::concat ($run_evaluate ($bv_unfold_repeat ($run_evaluate n) #b0)) ex))) (($run_evaluate (@bv n m)) (eo::to_bin ($run_evaluate m) ($run_evaluate n))) (($run_evaluate (@bvsize x)) ($bv_bitwidth (eo::typeof x))) diff --git a/proofs/eo/cpc/programs/Arith.eo b/proofs/eo/cpc/programs/Arith.eo index af636e8e801..79dec9aa8be 100644 --- a/proofs/eo/cpc/programs/Arith.eo +++ b/proofs/eo/cpc/programs/Arith.eo @@ -106,7 +106,7 @@ ; define: $arith_eval_int_pow_2 ; args: -; - x Int: The term to compute whether it is a power of two. +; - x Int: The term to compute take as the exponent of two. ; return: > ; two raised to the power of x. If x is not a numeral value, we return ; the term (int.pow2 x). @@ -140,3 +140,27 @@ (eo::ite (eo::is_z x) (eo::ite (eo::is_neg x) false ($arith_eval_int_is_pow_2_rec x)) (int.ispow2 x))) + + +; define: $arith_unfold_pow_rec +; args: +; - n Int: The number of times to multiply, expected to be a non-negative numeral. +; - a T: The term to muliply. +; return: The result of multiplying a, n times. +(program $arith_unfold_pow_rec ((T Type) (n Int) (a T)) + (Int T) T + ( + (($arith_unfold_pow_rec 0 a) 1) + (($arith_unfold_pow_rec n a) (eo::cons * a ($arith_unfold_pow_rec (eo::add n -1) a))) + ) +) + +; define: $arith_unfold_pow +; args: +; - n Int: The number of times to multiply. +; - a T: The term to muliply. +; return: The result of multiplying a, n times. If n is not a positive numeral, this returns (^ a n). +(define $arith_unfold_pow ((T Type :implicit) (n Int) (a T)) + (eo::ite (eo::and (eo::is_z n) (eo::not (eo::is_neg n))) + ($arith_unfold_pow_rec n a) + (^ a n))) diff --git a/proofs/eo/cpc/programs/BitVectors.eo b/proofs/eo/cpc/programs/BitVectors.eo index 2dd46304b97..5315db08bfb 100644 --- a/proofs/eo/cpc/programs/BitVectors.eo +++ b/proofs/eo/cpc/programs/BitVectors.eo @@ -23,29 +23,29 @@ (eo::add (eo::neg ($arith_eval_int_pow_2 wm1)) z) z)))))) -; define: $bv_eval_repeat_rec +; define: $bv_unfold_repeat_rec ; args: ; - n Int: The number of times to repeat, expected to be a non-negative numeral. -; - b (BitVec m): The bitvector term, expected to be a binary constant. -; return: The result of repeating b n times. -(program $bv_eval_repeat_rec ((m Int) (n Int) (b (BitVec m))) +; - b (BitVec m): The bitvector term. +; return: The result of concatenating b n times. +(program $bv_unfold_repeat_rec ((m Int) (n Int) (b (BitVec m))) (Int (BitVec m)) (BitVec (eo::mul n m)) ( - (($bv_eval_repeat_rec 0 b) (eo::to_bin 0 0)) - (($bv_eval_repeat_rec n b) (eo::concat b ($bv_eval_repeat_rec (eo::add n -1) b))) + (($bv_unfold_repeat_rec 0 b) (eo::to_bin 0 0)) + (($bv_unfold_repeat_rec n b) (eo::cons concat b ($bv_unfold_repeat_rec (eo::add n -1) b))) ) ) -; define: $bv_eval_repeat +; define: $bv_unfold_repeat ; args: ; - n Int: The number of times to repeat, expected to be a non-negative numeral. -; - b (BitVec m): The bitvector term, expected to be a binary constant. +; - b (BitVec m): The bitvector term. ; return: > -; The result of repeating b n times. If n is not a numeral or is negative, +; The result of concatenating b n times. If n is not a numeral or is negative, ; this returns the term (repeat n b). -(define $bv_eval_repeat ((m Int :implicit) (n Int) (b (BitVec m))) +(define $bv_unfold_repeat ((m Int :implicit) (n Int) (b (BitVec m))) (eo::ite (eo::and (eo::is_z n) (eo::not (eo::is_neg n))) - ($bv_eval_repeat_rec n b) + ($bv_unfold_repeat_rec n b) (repeat n b))) ; program: $bv_get_first_const_child diff --git a/proofs/eo/cpc/rules/Arith.eo b/proofs/eo/cpc/rules/Arith.eo index e6e44fdf524..4607d0f6990 100644 --- a/proofs/eo/cpc/rules/Arith.eo +++ b/proofs/eo/cpc/rules/Arith.eo @@ -348,3 +348,18 @@ :args (t) :conclusion ($arith_reduction_pred t) ) + +;;;;; ProofRewriteRule::ARITH_POW_ELIM + +; rule: arith-pow-elim +; implements: ProofRewriteRule::ARITH_POW_ELIM +; args: +; - eq Bool: The equality to prove with this rule. +; requires: n is integral, and b is the multiplication of a, n times. +; conclusion: the equality between a and b. +(declare-rule arith-pow-elim ((T Type) (a T) (n T) (b T)) + :args ((= (^ a n) b)) + :requires (((eo::to_q (eo::to_z n)) (eo::to_q n)) + (($singleton_elim ($arith_unfold_pow (eo::to_z n) a)) b)) + :conclusion (= (^ a n) b) +) diff --git a/proofs/eo/cpc/rules/BitVectors.eo b/proofs/eo/cpc/rules/BitVectors.eo index 1d6638ac180..96a9e64a840 100644 --- a/proofs/eo/cpc/rules/BitVectors.eo +++ b/proofs/eo/cpc/rules/BitVectors.eo @@ -1,6 +1,20 @@ (include "../programs/BitVectors.eo") -; ---------------- ProofRewriteRule::BV_BITWISE_SLICING +;;;;; ProofRewriteRule::BV_REPEAT_ELIM + +; rule: bv-repeat-elim +; implements: ProofRewriteRule::BV_REPEAT_ELIM +; args: +; - eq Bool: The equality to prove with this rule. +; requires: b is the concatenation of a, n times. +; conclusion: the equality between a and b. +(declare-rule bv-repeat-elim ((k1 Int) (k2 Int) (n Int) (a (BitVec k1)) (b (BitVec k2))) + :args ((= (repeat n a) b)) + :requires ((($singleton_elim ($bv_unfold_repeat n a)) b)) + :conclusion (= (repeat n a) b) +) + +;;;;; ProofRewriteRule::BV_BITWISE_SLICING ; program: $bv_mk_bitwise_slicing_rec ; args: @@ -84,7 +98,7 @@ :conclusion (= a b) ) -; ---------------- ProofRewriteRule::BV_BITBLAST_STEP +;;;;; ProofRule::BV_BITBLAST_STEP ; program: $bv_mk_bitblast_step_eq ; args: diff --git a/proofs/eo/cpc/rules/Sets.eo b/proofs/eo/cpc/rules/Sets.eo index 168ead31e8b..29e2468efb4 100644 --- a/proofs/eo/cpc/rules/Sets.eo +++ b/proofs/eo/cpc/rules/Sets.eo @@ -1,5 +1,7 @@ (include "../theories/Sets.eo") +;;;;; ProofRewriteRule::SETS_IS_EMPTY_EVAL + ; define: $set_is_empty_eval ; args: ; - t (Set T): The set to check. @@ -31,6 +33,8 @@ :conclusion (= (set.is_empty t) b) ) +;;;;; ProofRule::SETS_SINGLETON_INJ + ; rule: sets_singleton_inj ; implements: ProofRule::SETS_SINGLETON_INJ ; premises: @@ -41,6 +45,8 @@ :conclusion (= a b) ) +;;;;; ProofRule::SETS_EXT + ; rule: sets_ext ; implements: ProofRule::SETS_EXT ; premises: @@ -53,6 +59,35 @@ :conclusion (not (= (set.member (@sets_deq_diff a b) a) (set.member (@sets_deq_diff a b) b))) ) +;;;;; ProofRewriteRule::SETS_INSERT_ELIM + +; program: $set_eval_insert +; args: +; - es @List: The list of elements +; - t (Set T): The set to insert into. +; return: > +; The union of elements in es with t. +(program $set_eval_insert ((T Type) (x T) (xs @List :list) (t (Set T))) + (@List (Set T)) (Set T) + ( + (($set_eval_insert (@list x xs) t) (set.union (set.singleton x) ($set_eval_insert xs t))) + (($set_eval_insert @list.nil t) t) + ) +) + +; rule: sets-insert-elim +; implements: ProofRewriteRule::SETS_INSERT_ELIM +; args: +; - eq Bool: The equality to prove with this rule. +; requires: the union of the elements in the first argument with the last argument equal the right hand side. +; conclusion: the equality between a and b. +(declare-rule sets-insert-elim ((T Type) (s (Set T)) (es @List) (t (Set T))) + :args ((= (set.insert es s) t)) + :requires ((($set_eval_insert es s) t)) + :conclusion (= (set.insert es s) t) +) + +;;;;; ProofRewriteRule::SETS_FILTER_DOWN ; rule: sets_filter_down ; implements: ProofRewriteRule::SETS_FILTER_DOWN @@ -66,6 +101,8 @@ :conclusion (and (set.member x S) (P x)) ) +;;;;; ProofRewriteRule::SETS_FILTER_UP + ; rule: sets_filter_up ; implements: ProofRewriteRule::SETS_FILTER_UP ; args: diff --git a/src/proof/alf/alf_printer.cpp b/src/proof/alf/alf_printer.cpp index 1aabb0d34e8..151873738c4 100644 --- a/src/proof/alf/alf_printer.cpp +++ b/src/proof/alf/alf_printer.cpp @@ -264,6 +264,7 @@ bool AlfPrinter::isHandledTheoryRewrite(ProofRewriteRule id, const Node& n) case ProofRewriteRule::DISTINCT_ELIM: case ProofRewriteRule::BETA_REDUCE: case ProofRewriteRule::LAMBDA_ELIM: + case ProofRewriteRule::ARITH_POW_ELIM: case ProofRewriteRule::ARITH_STRING_PRED_ENTAIL: case ProofRewriteRule::ARITH_STRING_PRED_SAFE_APPROX: case ProofRewriteRule::EXISTS_ELIM: @@ -280,11 +281,13 @@ bool AlfPrinter::isHandledTheoryRewrite(ProofRewriteRule id, const Node& n) case ProofRewriteRule::QUANT_VAR_ELIM_EQ: case ProofRewriteRule::RE_LOOP_ELIM: case ProofRewriteRule::SETS_IS_EMPTY_EVAL: + case ProofRewriteRule::SETS_INSERT_ELIM: case ProofRewriteRule::STR_IN_RE_CONCAT_STAR_CHAR: case ProofRewriteRule::STR_IN_RE_SIGMA: case ProofRewriteRule::STR_IN_RE_SIGMA_STAR: case ProofRewriteRule::STR_IN_RE_CONSUME: case ProofRewriteRule::RE_INTER_UNION_INCLUSION: + case ProofRewriteRule::BV_REPEAT_ELIM: case ProofRewriteRule::BV_BITWISE_SLICING: return true; case ProofRewriteRule::STR_IN_RE_EVAL: Assert(n[0].getKind() == Kind::STRING_IN_REGEXP && n[0][0].isConst()); diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 3e1d5ce862c..78c09c55094 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -62,14 +62,14 @@ Node TheorySetsRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n) { NodeManager* nm = nodeManager(); size_t setNodeIndex = n.getNumChildren() - 1; - Node elems = nm->mkNode(Kind::SET_SINGLETON, n[0]); - - for (size_t i = 1; i < setNodeIndex; ++i) + Node elems = n[setNodeIndex]; + for (size_t i = 0; i < setNodeIndex; ++i) { - Node singleton = nm->mkNode(Kind::SET_SINGLETON, n[i]); - elems = nm->mkNode(Kind::SET_UNION, elems, singleton); + size_t ii = (setNodeIndex-i)-1; + Node singleton = nm->mkNode(Kind::SET_SINGLETON, n[ii]); + elems = nm->mkNode(Kind::SET_UNION, singleton, elems); } - return nm->mkNode(Kind::SET_UNION, elems, n[setNodeIndex]); + return elems; } } break; From 6c11825ddf1c43a2747e0d35d8468831fd997e63 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jos=C3=A9=20Neto?= Date: Tue, 17 Dec 2024 15:21:34 -0300 Subject: [PATCH 3/9] Add option to exclude tester (#11451) Added flag to allow removal of specific testers in the regression test setup. The idea is using this mechanism to disable the alethe tester for some machine at the buildbot. --- test/regress/cli/run_regression.py | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/test/regress/cli/run_regression.py b/test/regress/cli/run_regression.py index bf386f170a7..9bc6adf3f65 100755 --- a/test/regress/cli/run_regression.py +++ b/test/regress/cli/run_regression.py @@ -938,10 +938,13 @@ def main(): parser = argparse.ArgumentParser( description="Runs benchmark and checks for correct exit status and output." ) - tester_choices = ["all"] + list(g_testers.keys()) + + g_testers_keys = list(g_testers.keys()) + tester_choices = ["all"] + g_testers_keys parser.add_argument("--use-skip-return-code", action="store_true") parser.add_argument("--skip-timeout", action="store_true") parser.add_argument("--tester", choices=tester_choices, action="append") + parser.add_argument("--tester-exc", choices=g_testers_keys, action="append") parser.add_argument("--lfsc-binary", default="") parser.add_argument("--lfsc-sig-dir", default="") parser.add_argument("--carcara-binary", default="") @@ -973,7 +976,10 @@ def main(): if not testers: testers = g_default_testers elif "all" in testers: - testers = list(g_testers.keys()) + testers = g_testers_keys + + if g_args.tester_exc: + testers = [t for t in testers if t not in g_args.tester_exc] lfsc_sigs = [] if not g_args.lfsc_sig_dir == "": From 746e38e19f8bff331d606231e9d494ce0a80f854 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 17 Dec 2024 14:19:02 -0600 Subject: [PATCH 4/9] Fix Eunoia definition of ARRAYS_READ_OVER_WRITE_CONTRA (#11455) Was out of sync with the internal definition. --- proofs/eo/cpc/rules/Arrays.eo | 2 +- test/regress/cli/CMakeLists.txt | 1 + .../cli/regress0/proofs/ios_np_sf.smt2 | 44 +++++++++++++++++++ 3 files changed, 46 insertions(+), 1 deletion(-) create mode 100644 test/regress/cli/regress0/proofs/ios_np_sf.smt2 diff --git a/proofs/eo/cpc/rules/Arrays.eo b/proofs/eo/cpc/rules/Arrays.eo index 59b37c9e1b8..0a439288db6 100644 --- a/proofs/eo/cpc/rules/Arrays.eo +++ b/proofs/eo/cpc/rules/Arrays.eo @@ -21,7 +21,7 @@ ; conclusion: The index of the store is equal to the selected index. (declare-rule arrays_read_over_write_contra ((T Type) (U Type) (i T) (j T) (e U) (a (Array T U))) :premises ((not (= (select (store a i e) j) (select a j)))) - :conclusion (= i j) + :conclusion (= j i) ) ; rule: arrays_read_over_write_1 diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 6878c4af344..5ccfe96efd8 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -1333,6 +1333,7 @@ set(regress_0_tests regress0/proofs/fixed-point-rew.smt2 regress0/proofs/fixed-point-rew-conc.smt2 regress0/proofs/indexof-eval-rw_155.smt2 + regress0/proofs/ios_np_sf.smt2 regress0/proofs/issue277-circuit-propagator.smt2 regress0/proofs/issue10278-pf-clone.smt2 regress0/proofs/issue8983-trust-subs.smt2 diff --git a/test/regress/cli/regress0/proofs/ios_np_sf.smt2 b/test/regress/cli/regress0/proofs/ios_np_sf.smt2 new file mode 100644 index 00000000000..faa61e48f1c --- /dev/null +++ b/test/regress/cli/regress0/proofs/ios_np_sf.smt2 @@ -0,0 +1,44 @@ +; EXPECT: unsat +(set-info :smt-lib-version 2.6) +(set-logic QF_ALIA) +(set-info :status unsat) +(declare-fun earray_12 () (Array Int Int)) +(declare-fun earray_14 () (Array Int Int)) +(declare-fun earray_16 () (Array Int Int)) +(declare-fun earray_3 () (Array Int Int)) +(declare-fun earray_6 () (Array Int Int)) +(declare-fun earray_9 () (Array Int Int)) +(declare-fun elem_0 () Int) +(declare-fun elem_1 () Int) +(declare-fun elem_10 () Int) +(declare-fun elem_11 () Int) +(declare-fun elem_13 () Int) +(declare-fun elem_15 () Int) +(declare-fun elem_2 () Int) +(declare-fun elem_4 () Int) +(declare-fun elem_5 () Int) +(declare-fun elem_7 () Int) +(declare-fun elem_8 () Int) +(declare-fun a () (Array Int Int)) +(declare-fun i () Int) +(assert (= earray_12 (store a elem_4 elem_11))) +(assert (= earray_14 (store earray_12 elem_0 elem_13))) +(assert (= earray_16 (store earray_14 i elem_15))) +(assert (= earray_3 (store a elem_0 elem_2))) +(assert (= earray_6 (store earray_3 elem_4 elem_5))) +(assert (= earray_9 (store earray_6 elem_7 elem_8))) +(assert (= elem_0 (+ i 1))) +(assert (= elem_1 (select a i))) +(assert (= elem_10 (select a elem_7))) +(assert (= elem_11 (- elem_10 1))) +(assert (= elem_13 (- elem_11 1))) +(assert (= elem_15 (- elem_13 1))) +(assert (= elem_2 (+ elem_1 1))) +(assert (= elem_4 (+ elem_0 1))) +(assert (= elem_5 (+ elem_2 1))) +(assert (= elem_7 (+ elem_4 1))) +(assert (= elem_8 (+ elem_5 1))) +(assert (= earray_9 earray_16)) +(assert (not (= elem_8 elem_10))) +(check-sat) +(exit) From 13c3d2c45670b499ff674e9f32ed1c59738799b9 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Wed, 18 Dec 2024 08:45:27 -0600 Subject: [PATCH 5/9] Eliminate more calls to NodeManager::{currentNM,getSkolemManager} (#11457) --- src/expr/bound_var_manager.h | 2 +- src/expr/elim_shadow_converter.cpp | 2 +- src/expr/skolem_manager.cpp | 9 +++--- src/expr/skolem_manager.h | 4 +-- src/printer/let_binding.cpp | 3 +- src/proof/alethe/alethe_node_converter.cpp | 2 +- src/smt/proof_post_processor_dsl.cpp | 2 +- src/theory/arith/arith_utilities.cpp | 2 +- src/theory/arith/linear/normal_form.h | 4 +-- .../arith/nl/coverings/proof_generator.cpp | 20 ++++++------- .../arith/nl/transcendental/sine_solver.cpp | 6 ++-- .../nl/transcendental/taylor_generator.cpp | 2 +- .../arrays/theory_arrays_type_rules.cpp | 2 +- src/theory/bags/theory_bags_type_rules.cpp | 8 ++--- src/theory/conflict_processor.cpp | 6 ++-- src/theory/datatypes/sygus_datatype_utils.cpp | 2 +- src/theory/datatypes/theory_datatypes.cpp | 4 +-- src/theory/quantifiers/cegqi/nested_qe.cpp | 2 +- .../quantifiers/conjecture_generator.cpp | 10 +++---- .../quantifiers/ematching/ho_trigger.cpp | 4 +-- src/theory/quantifiers/ematching/trigger.cpp | 7 ++--- .../quantifiers/fmf/full_model_check.cpp | 14 ++++----- src/theory/quantifiers/ho_term_database.cpp | 3 +- .../inst_strategy_sub_conflict.cpp | 2 +- src/theory/quantifiers/instantiate.cpp | 2 +- src/theory/quantifiers/mbqi_fast_sygus.cpp | 2 +- src/theory/quantifiers/oracle_engine.cpp | 5 ++-- src/theory/quantifiers/skolemize.cpp | 2 +- .../quantifiers/sygus/sygus_enumerator.cpp | 2 +- .../sygus/transition_inference.cpp | 2 +- src/theory/sets/theory_sets_private.cpp | 2 +- src/theory/sets/theory_sets_rels.cpp | 4 +-- src/theory/strings/infer_proof_cons.cpp | 6 ++-- src/theory/strings/term_registry.cpp | 12 ++++---- .../strings/theory_strings_preprocess.cpp | 2 +- src/theory/strings/word.cpp | 2 +- src/theory/theory_engine.cpp | 29 +++---------------- src/theory/theory_model_builder.cpp | 4 +-- 38 files changed, 85 insertions(+), 113 deletions(-) diff --git a/src/expr/bound_var_manager.h b/src/expr/bound_var_manager.h index b43376042de..046729ca2ab 100644 --- a/src/expr/bound_var_manager.h +++ b/src/expr/bound_var_manager.h @@ -63,7 +63,7 @@ class BoundVarManager Assert(n.getAttribute(attr).getType() == tn); return n.getAttribute(attr); } - Node v = NodeManager::currentNM()->mkBoundVar(tn); + Node v = NodeManager::mkBoundVar(tn); n.setAttribute(attr, v); // if we are keeping cache values, insert it to the set if (d_keepCacheVals) diff --git a/src/expr/elim_shadow_converter.cpp b/src/expr/elim_shadow_converter.cpp index 68ef3b4c857..784fdb16d62 100644 --- a/src/expr/elim_shadow_converter.cpp +++ b/src/expr/elim_shadow_converter.cpp @@ -123,7 +123,7 @@ Node ElimShadowNodeConverter::eliminateShadow(const Node& q) { children.push_back(esnc.convert(q[i])); } - return NodeManager::currentNM()->mkNode(q.getKind(), children); + return nm->mkNode(q.getKind(), children); } } // namespace cvc5::internal diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index 140248e319f..9e379ca4a1a 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -161,22 +161,23 @@ Node SkolemManager::mkSkolemFunctionTyped(SkolemId id, return mkSkolemFunctionTyped(id, tn, cacheVal); } -bool SkolemManager::isSkolemFunction(TNode k) const +bool SkolemManager::isSkolemFunction(TNode k) { return k.getKind() == Kind::SKOLEM; } bool SkolemManager::isSkolemFunction(TNode k, SkolemId& id, - Node& cacheVal) const + Node& cacheVal) { + SkolemManager* skm = k.getNodeManager()->getSkolemManager(); if (k.getKind() != Kind::SKOLEM) { return false; } std::map>::const_iterator it = - d_skolemFunMap.find(k); - Assert(it != d_skolemFunMap.end()); + skm->d_skolemFunMap.find(k); + Assert(it != skm->d_skolemFunMap.end()); id = std::get<0>(it->second); cacheVal = std::get<2>(it->second); return true; diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index e0bc4ea6b8f..6d600785675 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -149,12 +149,12 @@ class SkolemManager * Is k a skolem function? Returns true if k was generated by the above * call. */ - bool isSkolemFunction(TNode k) const; + static bool isSkolemFunction(TNode k); /** * Is k a skolem function? Returns true if k was generated by the above * call. Updates the arguments to the values used when constructing it. */ - bool isSkolemFunction(TNode k, SkolemId& id, Node& cacheVal) const; + static bool isSkolemFunction(TNode k, SkolemId& id, Node& cacheVal); /** * @param k The skolem. * @return skolem function id for k. diff --git a/src/printer/let_binding.cpp b/src/printer/let_binding.cpp index eb307cceeec..f97fd3d0a6d 100644 --- a/src/printer/let_binding.cpp +++ b/src/printer/let_binding.cpp @@ -178,8 +178,7 @@ void LetBinding::updateCounts(Node n) { SkolemId skid; Node cacheVal; - SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); - if (sm->isSkolemFunction(cur, skid, cacheVal) && !cacheVal.isNull()) + if (SkolemManager::isSkolemFunction(cur, skid, cacheVal) && !cacheVal.isNull()) { if (cacheVal.getKind() == Kind::SEXPR) { diff --git a/src/proof/alethe/alethe_node_converter.cpp b/src/proof/alethe/alethe_node_converter.cpp index 32b59bd2ca3..a313e51e596 100644 --- a/src/proof/alethe/alethe_node_converter.cpp +++ b/src/proof/alethe/alethe_node_converter.cpp @@ -501,7 +501,7 @@ Node AletheNodeConverter::mkInternalSymbol(const std::string& name, Node AletheNodeConverter::mkInternalSymbol(const std::string& name) { - return mkInternalSymbol(name, NodeManager::currentNM()->sExprType()); + return mkInternalSymbol(name, d_nm->sExprType()); } const std::string& AletheNodeConverter::getError() { return d_error; } diff --git a/src/smt/proof_post_processor_dsl.cpp b/src/smt/proof_post_processor_dsl.cpp index ac1b16cb91d..cb811e1d3e8 100644 --- a/src/smt/proof_post_processor_dsl.cpp +++ b/src/smt/proof_post_processor_dsl.cpp @@ -27,7 +27,7 @@ namespace smt { ProofPostprocessDsl::ProofPostprocessDsl(Env& env, rewriter::RewriteDb* rdb) : EnvObj(env), d_rdbPc(env, rdb) { - d_true = NodeManager::currentNM()->mkConst(true); + d_true = nodeManager()->mkConst(true); d_tmode = (options().proof.proofGranularityMode == options::ProofGranularityMode::DSL_REWRITE_STRICT) ? rewriter::TheoryRewriteMode::RESORT diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp index 8a09c98cd88..9f5d0edb785 100644 --- a/src/theory/arith/arith_utilities.cpp +++ b/src/theory/arith/arith_utilities.cpp @@ -361,7 +361,7 @@ Node eliminateInt2Bv(TNode node) { return v[0]; } - NodeBuilder result(NodeManager::currentNM(), Kind::BITVECTOR_CONCAT); + NodeBuilder result(nm, Kind::BITVECTOR_CONCAT); result.append(v.rbegin(), v.rend()); return Node(result); } diff --git a/src/theory/arith/linear/normal_form.h b/src/theory/arith/linear/normal_form.h index 10cca5c794c..3836c703364 100644 --- a/src/theory/arith/linear/normal_form.h +++ b/src/theory/arith/linear/normal_form.h @@ -634,7 +634,7 @@ class Monomial : public NodeWrapper { Assert(!c.isZero()); Assert(!c.isOne()); Assert(!vl.empty()); - return NodeManager::currentNM()->mkNode( + return NodeManager::mkNode( Kind::MULT, c.getNode(), vl.getNode()); } @@ -1157,7 +1157,7 @@ class Polynomial : public NodeWrapper { class SumPair : public NodeWrapper { private: static Node toNode(const Polynomial& p, const Constant& c){ - return NodeManager::currentNM()->mkNode( + return NodeManager::mkNode( Kind::ADD, p.getNode(), c.getNode()); } diff --git a/src/theory/arith/nl/coverings/proof_generator.cpp b/src/theory/arith/nl/coverings/proof_generator.cpp index 0f714f1cc26..0fd3a77c221 100644 --- a/src/theory/arith/nl/coverings/proof_generator.cpp +++ b/src/theory/arith/nl/coverings/proof_generator.cpp @@ -75,14 +75,14 @@ std::pair getRootIDs( * @param poly The polynomial whose root shall be considered * @param vm A variable mapper from cvc5 to libpoly variables */ -Node mkIRP(const Node& var, +Node mkIRP(NodeManager* nm, + const Node& var, Kind rel, const Node& zero, std::size_t k, const poly::Polynomial& poly, VariableMapper& vm) { - auto* nm = NodeManager::currentNM(); auto op = nm->mkConst(IndexedRootPredicate(k)); return nm->mkNode(Kind::INDEXED_ROOT_PREDICATE, op, @@ -96,8 +96,8 @@ CoveringsProofGenerator::CoveringsProofGenerator(Env& env, context::Context* ctx) : EnvObj(env), d_proofs(env, ctx), d_current(nullptr) { - d_false = NodeManager::currentNM()->mkConst(false); - d_zero = NodeManager::currentNM()->mkConstReal(Rational(0)); + d_false = nodeManager()->mkConst(false); + d_zero = nodeManager()->mkConstReal(Rational(0)); } void CoveringsProofGenerator::startNewProof() @@ -157,7 +157,7 @@ void CoveringsProofGenerator::addDirect(Node var, auto ids = getRootIDs(roots, get_lower(interval)); Assert(ids.first == ids.second); res.emplace_back( - mkIRP(var, Kind::EQUAL, mkZero(var.getType()), ids.first, poly, vm)); + mkIRP(nodeManager(), var, Kind::EQUAL, mkZero(var.getType()), ids.first, poly, vm)); } else { @@ -168,7 +168,7 @@ void CoveringsProofGenerator::addDirect(Node var, auto ids = getRootIDs(roots, get_lower(interval)); Assert(ids.first == ids.second); Kind rel = poly::get_lower_open(interval) ? Kind::GT : Kind::GEQ; - res.emplace_back(mkIRP(var, rel, d_zero, ids.first, poly, vm)); + res.emplace_back(mkIRP(nodeManager(), var, rel, d_zero, ids.first, poly, vm)); } if (!is_plus_infinity(get_upper(interval))) { @@ -176,7 +176,7 @@ void CoveringsProofGenerator::addDirect(Node var, auto ids = getRootIDs(roots, get_upper(interval)); Assert(ids.first == ids.second); Kind rel = poly::get_upper_open(interval) ? Kind::LT : Kind::LEQ; - res.emplace_back(mkIRP(var, rel, d_zero, ids.first, poly, vm)); + res.emplace_back(mkIRP(nodeManager(), var, rel, d_zero, ids.first, poly, vm)); } } // Add to proof manager @@ -214,7 +214,7 @@ std::vector CoveringsProofGenerator::constructCell(Node var, if (ids.first == ids.second) { // Excludes a single point only - res.emplace_back(mkIRP(var, Kind::EQUAL, d_zero, ids.first, poly, vm)); + res.emplace_back(mkIRP(nodeManager(), var, Kind::EQUAL, d_zero, ids.first, poly, vm)); } else { @@ -222,12 +222,12 @@ std::vector CoveringsProofGenerator::constructCell(Node var, if (ids.first > 0) { // Interval has lower bound that is not -inf - res.emplace_back(mkIRP(var, Kind::GT, d_zero, ids.first, poly, vm)); + res.emplace_back(mkIRP(nodeManager(), var, Kind::GT, d_zero, ids.first, poly, vm)); } if (ids.second <= roots.size()) { // Interval has upper bound that is not inf - res.emplace_back(mkIRP(var, Kind::LT, d_zero, ids.second, poly, vm)); + res.emplace_back(mkIRP(nodeManager(), var, Kind::LT, d_zero, ids.second, poly, vm)); } } } diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index ac4f1a70e9a..f98ec529e78 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -41,7 +41,7 @@ namespace transcendental { SineSolver::SineSolver(Env& env, TranscendentalState* tstate) : EnvObj(env), d_data(tstate) { - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = nodeManager(); Node zero = nm->mkConstReal(Rational(0)); Node one = nm->mkConstReal(Rational(1)); Node negOne = nm->mkConstReal(Rational(-1)); @@ -66,7 +66,7 @@ SineSolver::~SineSolver() {} void SineSolver::doReductions() { - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = nodeManager(); std::map >::iterator it = d_data->d_funcMap.find(Kind::SINE); if (it == d_data->d_funcMap.end()) @@ -506,7 +506,7 @@ void SineSolver::checkMonotonic() void SineSolver::doTangentLemma( TNode e, TNode c, TNode poly_approx, int region, std::uint64_t d) { - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = nodeManager(); Assert(region != -1); Trace("nl-ext-sine") << c << " in region " << region << std::endl; diff --git a/src/theory/arith/nl/transcendental/taylor_generator.cpp b/src/theory/arith/nl/transcendental/taylor_generator.cpp index 8491566ba1f..8efce912185 100644 --- a/src/theory/arith/nl/transcendental/taylor_generator.cpp +++ b/src/theory/arith/nl/transcendental/taylor_generator.cpp @@ -29,7 +29,7 @@ namespace nl { namespace transcendental { TaylorGenerator::TaylorGenerator() - : d_taylor_real_fv(NodeManager::currentNM()->mkBoundVar( + : d_taylor_real_fv(NodeManager::mkBoundVar( "x", NodeManager::currentNM()->realType())) { } diff --git a/src/theory/arrays/theory_arrays_type_rules.cpp b/src/theory/arrays/theory_arrays_type_rules.cpp index 35d1fa3c9b4..7d92f3a6c9f 100644 --- a/src/theory/arrays/theory_arrays_type_rules.cpp +++ b/src/theory/arrays/theory_arrays_type_rules.cpp @@ -112,7 +112,7 @@ TypeNode ArrayStoreTypeRule::computeType(NodeManager* nodeManager, } return TypeNode::null(); } - return NodeManager::currentNM()->mkArrayType(indexjoin, valuejoin); + return nodeManager->mkArrayType(indexjoin, valuejoin); } else { diff --git a/src/theory/bags/theory_bags_type_rules.cpp b/src/theory/bags/theory_bags_type_rules.cpp index cbda69965ac..f6196891ee9 100644 --- a/src/theory/bags/theory_bags_type_rules.cpp +++ b/src/theory/bags/theory_bags_type_rules.cpp @@ -421,9 +421,8 @@ TypeNode BagFilterTypeRule::computeType(NodeManager* nodeManager, return TypeNode::null(); } std::vector argTypes = functionType.getArgTypes(); - NodeManager* nm = NodeManager::currentNM(); if (!(argTypes.size() == 1 && argTypes[0] == elementType - && functionType.getRangeType() == nm->booleanType())) + && functionType.getRangeType() == nodeManager->booleanType())) { if (errOut) { @@ -517,7 +516,6 @@ TypeNode BagPartitionTypeRule::computeType(NodeManager* nodeManager, Assert(n.getKind() == Kind::BAG_PARTITION); TypeNode functionType = n[0].getTypeOrNull(); TypeNode bagType = n[1].getTypeOrNull(); - NodeManager* nm = NodeManager::currentNM(); if (check) { if (!bagType.isBag()) @@ -546,7 +544,7 @@ TypeNode BagPartitionTypeRule::computeType(NodeManager* nodeManager, std::vector argTypes = functionType.getArgTypes(); TypeNode rangeType = functionType.getRangeType(); if (!(argTypes.size() == 2 && elementType == argTypes[0] - && elementType == argTypes[1] && rangeType == nm->booleanType())) + && elementType == argTypes[1] && rangeType == nodeManager->booleanType())) { if (errOut) { @@ -558,7 +556,7 @@ TypeNode BagPartitionTypeRule::computeType(NodeManager* nodeManager, return TypeNode::null(); } } - TypeNode retType = nm->mkBagType(bagType); + TypeNode retType = nodeManager->mkBagType(bagType); return retType; } diff --git a/src/theory/conflict_processor.cpp b/src/theory/conflict_processor.cpp index 5c53d2da7f6..ad33b93e90b 100644 --- a/src/theory/conflict_processor.cpp +++ b/src/theory/conflict_processor.cpp @@ -30,7 +30,7 @@ namespace theory { ConflictProcessor::ConflictProcessor(Env& env, bool useExtRewriter) : EnvObj(env), d_useExtRewriter(useExtRewriter), d_stats(statisticsRegistry()) { - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = env.getNodeManager(); d_true = nm->mkConst(true); d_false = nm->mkConst(false); } @@ -137,7 +137,7 @@ TrustNode ConflictProcessor::processLemma(const TrustNode& lem) return TrustNode::null(); } // just take the OR as target - tgtLit = NodeManager::currentNM()->mkOr(tgtLitsNc); + tgtLit = nodeManager()->mkOr(tgtLitsNc); } else { @@ -210,7 +210,7 @@ TrustNode ConflictProcessor::processLemma(const TrustNode& lem) if (minimized) { ++d_stats.d_minLemmas; - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = nodeManager(); std::vector clause; for (std::pair& e : varToExp) { diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp index 665db56076e..7eb1be0ecd5 100644 --- a/src/theory/datatypes/sygus_datatype_utils.cpp +++ b/src/theory/datatypes/sygus_datatype_utils.cpp @@ -209,7 +209,7 @@ Node mkSygusTerm(const Node& op, } else { - ret = NodeManager::currentNM()->mkNode(tok, schildren); + ret = nm->mkNode(tok, schildren); } Trace("dt-sygus-util") << "...return " << ret << std::endl; return ret; diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 176e5091e58..1b1f50e1147 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -761,7 +761,7 @@ void TheoryDatatypes::addTester( Assert(testerIndex != -1); //we must explain why each term in the set of testers for this equivalence class is equal std::vector< Node > eq_terms; - NodeBuilder nb(NodeManager::currentNM(), Kind::AND); + NodeBuilder nb(nodeManager(), Kind::AND); for (unsigned i = 0; i < n_lbl; i++) { Node ti = d_labels_data[n][i]; @@ -1696,7 +1696,7 @@ void TheoryDatatypes::checkSplit() Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl; test = rewrite(test); - NodeBuilder nb(NodeManager::currentNM(), Kind::OR); + NodeBuilder nb(nodeManager(), Kind::OR); nb << test << test.notNode(); Node lemma = nb; d_im.lemma(lemma, InferenceId::DATATYPES_BINARY_SPLIT); diff --git a/src/theory/quantifiers/cegqi/nested_qe.cpp b/src/theory/quantifiers/cegqi/nested_qe.cpp index fa1931f72be..0b5e559f6b6 100644 --- a/src/theory/quantifiers/cegqi/nested_qe.cpp +++ b/src/theory/quantifiers/cegqi/nested_qe.cpp @@ -72,7 +72,7 @@ bool NestedQe::hasNestedQuantification(Node q) Node NestedQe::doNestedQe(Env& env, Node q, bool keepTopLevel) { - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = env.getNodeManager(); Node qOrig = q; bool inputExists = false; if (q.getKind() == Kind::EXISTS) diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 3c0b2ada994..5914354955c 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -102,8 +102,8 @@ ConjectureGenerator::ConjectureGenerator(Env& env, d_fullEffortCount(0), d_hasAddedLemma(false) { - d_true = NodeManager::currentNM()->mkConst(true); - d_false = NodeManager::currentNM()->mkConst(false); + d_true = nodeManager()->mkConst(true); + d_false = nodeManager()->mkConst(false); d_uequalityEngine.addFunctionKind(Kind::APPLY_UF); d_uequalityEngine.addFunctionKind(Kind::APPLY_CONSTRUCTOR); } @@ -938,7 +938,7 @@ unsigned ConjectureGenerator::flushWaitingConjectures( unsigned& addedLemmas, in Node rsg; if( !bvs.empty() ){ Node bvl = - NodeManager::currentNM()->mkNode(Kind::BOUND_VAR_LIST, bvs); + nodeManager()->mkNode(Kind::BOUND_VAR_LIST, bvs); rsg = NodeManager::mkNode(Kind::FORALL, bvl, lhs.eqNode(rhs)); }else{ rsg = lhs.eqNode( rhs ); @@ -1115,7 +1115,7 @@ int ConjectureGenerator::calculateGeneralizationDepth( TNode n, std::vector< TNo Node ConjectureGenerator::getPredicateForType( TypeNode tn ) { std::map< TypeNode, Node >::iterator it = d_typ_pred.find( tn ); if( it==d_typ_pred.end() ){ - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = nodeManager(); TypeNode op_tn = nm->mkFunctionType(tn, nm->booleanType()); Node op = NodeManager::mkDummySkolem( "PE", op_tn, "was created by conjecture ground term enumerator."); @@ -1205,7 +1205,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector< } children.push_back( lc ); Node nenum = - NodeManager::currentNM()->mkNode(Kind::APPLY_UF, children); + nodeManager()->mkNode(Kind::APPLY_UF, children); Trace("sg-gt-enum") << "Ground term enumerate : " << nenum << std::endl; terms.push_back(nenum); diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index b225de6f242..88b50f169fc 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -46,7 +46,7 @@ HigherOrderTrigger::HigherOrderTrigger( bool isUser) : Trigger(env, qs, qim, qr, tr, q, nodes, isUser), d_ho_var_apps(ho_apps) { - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = nodeManager(); // process the higher-order variable applications for (std::pair >& as : d_ho_var_apps) { @@ -503,7 +503,7 @@ uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas() if (d_ho_var_types.find(stn) != d_ho_var_types.end()) { Node u = HoTermDb::getHoTypeMatchPredicate(tn); - Node au = nm->mkNode(Kind::APPLY_UF, u, f); + Node au = NodeManager::mkNode(Kind::APPLY_UF, u, f); if (d_qim.addPendingLemma(au, InferenceId::QUANTIFIERS_HO_MATCH_PRED)) { diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 846809e1caf..2014e30f53a 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -86,7 +86,7 @@ Trigger::Trigger(Env& env, Node ns = d_qreg.substituteInstConstantsToBoundVariables(nt, q); extNodes.push_back(ns); } - d_trNode = NodeManager::currentNM()->mkNode(Kind::SEXPR, extNodes); + d_trNode = nodeManager()->mkNode(Kind::SEXPR, extNodes); if (isOutputOn(OutputTag::TRIGGER)) { output(OutputTag::TRIGGER) << (isUser ? "(user-trigger " : "(trigger "); @@ -147,7 +147,7 @@ bool Trigger::isMultiTrigger() const { return d_nodes.size() > 1; } Node Trigger::getInstPattern() const { - return NodeManager::currentNM()->mkNode(Kind::INST_PATTERN, d_nodes); + return nodeManager()->mkNode(Kind::INST_PATTERN, d_nodes); } uint64_t Trigger::addInstantiations() @@ -162,8 +162,7 @@ uint64_t Trigger::addInstantiations() { if (!ee->hasTerm(gt)) { - SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); - Node k = sm->mkPurifySkolem(gt); + Node k = SkolemManager::mkPurifySkolem(gt); Node eq = k.eqNode(gt); Trace("trigger-gt-lemma") << "Trigger: ground term purify lemma: " << eq << std::endl; diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 5eb214ec64a..5bdb643945d 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -306,8 +306,8 @@ FullModelChecker::FullModelChecker(Env& env, : QModelBuilder(env, qs, qim, qr, tr), d_fm(new FirstOrderModelFmc(env, qs, qr, tr)) { - d_true = NodeManager::currentNM()->mkConst(true); - d_false = NodeManager::currentNM()->mkConst(false); + d_true = nodeManager()->mkConst(true); + d_false = nodeManager()->mkConst(false); } void FullModelChecker::finishInit() { d_model = d_fm.get(); } @@ -499,7 +499,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ } entry_children.push_back(ri); } - Node n = NodeManager::currentNM()->mkNode(Kind::APPLY_UF, children); + Node n = nodeManager()->mkNode(Kind::APPLY_UF, children); Node nv = fm->getRepresentative( v ); Trace("fmc-model-debug") << "Representative of " << v << " is " << nv << std::endl; @@ -507,7 +507,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl; } Node en = hasNonStar ? n - : NodeManager::currentNM()->mkNode(Kind::APPLY_UF, + : nodeManager()->mkNode(Kind::APPLY_UF, entry_children); if( std::find(conds.begin(), conds.end(), n )==conds.end() ){ Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl; @@ -1391,7 +1391,7 @@ bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & co Node FullModelChecker::mkCond(const std::vector& cond) { - return NodeManager::currentNM()->mkNode(Kind::APPLY_UF, cond); + return nodeManager()->mkNode(Kind::APPLY_UF, cond); } Node FullModelChecker::mkCondDefault( FirstOrderModelFmc * fm, Node f) { @@ -1466,7 +1466,7 @@ Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals ) children.push_back( vals[i] ); } } - Node nc = NodeManager::currentNM()->mkNode(n.getKind(), children); + Node nc = nodeManager()->mkNode(n.getKind(), children); Trace("fmc-eval") << "Evaluate " << nc << " to "; nc = rewrite(nc); Trace("fmc-eval") << nc << std::endl; @@ -1493,7 +1493,7 @@ void FullModelChecker::registerQuantifiedFormula(Node q) { return; } - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = nodeManager(); std::vector types; for (const Node& v : q[0]) { diff --git a/src/theory/quantifiers/ho_term_database.cpp b/src/theory/quantifiers/ho_term_database.cpp index de780997b0d..dfd81376a5c 100644 --- a/src/theory/quantifiers/ho_term_database.cpp +++ b/src/theory/quantifiers/ho_term_database.cpp @@ -43,7 +43,6 @@ void HoTermDb::addTermInternal(Node n) return; } NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); Node curr = n; std::vector args; while (curr.getKind() == Kind::HO_APPLY) @@ -59,7 +58,7 @@ void HoTermDb::addTermInternal(Node n) continue; } d_hoFunOpPurify.insert(curr); - Node psk = sm->mkPurifySkolem(curr); + Node psk = SkolemManager::mkPurifySkolem(curr); // we do not add it to d_ops since it is an internal operator Node eq = psk.eqNode(curr); std::vector children; diff --git a/src/theory/quantifiers/inst_strategy_sub_conflict.cpp b/src/theory/quantifiers/inst_strategy_sub_conflict.cpp index ab998f08e89..5151f4358e8 100644 --- a/src/theory/quantifiers/inst_strategy_sub_conflict.cpp +++ b/src/theory/quantifiers/inst_strategy_sub_conflict.cpp @@ -156,7 +156,7 @@ void InstStrategySubConflict::check(Theory::Effort e, QEffort quant_e) << addedLemmas << "/" << triedLemmas << " instantiated" << std::endl; // Add the computed unsat core as a conflict, which will cause a backtrack. UnsatCore uc = findConflict->getUnsatCore(); - Node ucc = NodeManager::currentNM()->mkAnd(uc.getCore()); + Node ucc = nodeManager()->mkAnd(uc.getCore()); Trace("qscf-engine-debug") << "Unsat core is " << ucc << std::endl; Trace("qscf-engine") << "Core size = " << uc.getCore().size() << std::endl; d_qim.lemma(ucc.notNode(), InferenceId::QUANTIFIERS_SUB_UC); diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index c7dbff78f55..2edbc2ddf4b 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -559,7 +559,7 @@ Node Instantiate::getInstantiation(Node q, { std::vector pfTerms; // Include the list of terms as an SEXPR. - pfTerms.push_back(NodeManager::currentNM()->mkNode(Kind::SEXPR, terms)); + pfTerms.push_back(nodeManager()->mkNode(Kind::SEXPR, terms)); // additional arguments: if the inference id is not unknown, include it, // followed by the proof argument if non-null. The latter is used e.g. // to track which trigger caused an instantiation. diff --git a/src/theory/quantifiers/mbqi_fast_sygus.cpp b/src/theory/quantifiers/mbqi_fast_sygus.cpp index 7f4c3e042aa..1ca3f953f9d 100644 --- a/src/theory/quantifiers/mbqi_fast_sygus.cpp +++ b/src/theory/quantifiers/mbqi_fast_sygus.cpp @@ -35,7 +35,7 @@ void MVarInfo::initialize(Env& env, const Node& v, const std::vector& etrules) { - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = env.getNodeManager(); TypeNode tn = v.getType(); Assert(MQuantInfo::shouldEnumerate(tn)); TypeNode retType = tn; diff --git a/src/theory/quantifiers/oracle_engine.cpp b/src/theory/quantifiers/oracle_engine.cpp index 061f45e384a..3af08d5955b 100644 --- a/src/theory/quantifiers/oracle_engine.cpp +++ b/src/theory/quantifiers/oracle_engine.cpp @@ -83,8 +83,7 @@ void OracleEngine::presolve() { visited.insert(cur); if (OracleCaller::isOracleFunctionApp(cur)) { - SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); - Node k = sm->mkPurifySkolem(cur); + Node k = SkolemManager::mkPurifySkolem(cur); Node eq = k.eqNode(cur); d_qim.lemma(eq, InferenceId::QUANTIFIERS_ORACLE_PURIFY_SUBS); } @@ -129,7 +128,7 @@ void OracleEngine::check(Theory::Effort e, QEffort quant_e) FirstOrderModel* fm = d_treg.getModel(); TermDb* termDatabase = d_treg.getTermDatabase(); - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = nodeManager(); unsigned nquant = fm->getNumAssertedQuantifiers(); std::vector currInterfaces; for (unsigned i = 0; i < nquant; i++) diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index b49e66c1ecf..f0a96160cd1 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -63,7 +63,7 @@ TrustNode Skolemize::process(Node q) ProofNodeManager * pnm = d_env.getProofNodeManager(); // if using proofs and not using induction, we use the justified // skolemization - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = d_env.getNodeManager(); // cache the skolems in d_skolem_constants[q] std::vector& skolems = d_skolem_constants[q]; skolems = getSkolemConstants(q); diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index 6b712ba8204..2e8285f20a9 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -77,7 +77,7 @@ void SygusEnumerator::initialize(Node e) } // Get the statically registered symmetry breaking clauses for e, see if they // can be used for speeding up the enumeration. - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = nodeManager(); std::vector sbl; d_tds->getSymBreakLemmas(e, sbl); Node ag = d_tds->getActiveGuardForEnumerator(e); diff --git a/src/theory/quantifiers/sygus/transition_inference.cpp b/src/theory/quantifiers/sygus/transition_inference.cpp index f5fc8d1fb73..f4f13ed491e 100644 --- a/src/theory/quantifiers/sygus/transition_inference.cpp +++ b/src/theory/quantifiers/sygus/transition_inference.cpp @@ -198,7 +198,7 @@ void TransitionInference::process(Node n, Node f) void TransitionInference::process(Node n) { - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = nodeManager(); d_complete = true; d_trivial = true; std::vector n_check; diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 79d48557cc4..f7fafe3c207 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1524,7 +1524,7 @@ bool TheorySetsPrivate::collectModelValues(TheoryModel* m, { Trace("sets-model") <debugPrintModelEqc(); } - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = nodeManager(); std::map mvals; // If cardinality is enabled, we need to use the ordered equivalence class // list computed by the cardinality solver, where sets equivalence classes diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index cc1f55d3cc9..ca8bd15ebc1 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -978,7 +978,7 @@ void TheorySetsRels::check(Theory::Effort level) computeMembersForBinOpRel(n); d_rel_nodes.insert(n); } - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = nodeManager(); Node A = n[0]; Node B = n[1]; Node e = exp[0]; @@ -1323,7 +1323,7 @@ void TheorySetsRels::check(Theory::Effort level) return; } - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = nodeManager(); std::vector aMemberships = d_rReps_memberReps_exp_cache[aRep]; std::vector bMemberships = d_rReps_memberReps_exp_cache[bRep]; diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index 450d8526163..3220b2be185 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -1298,14 +1298,13 @@ bool InferProofCons::purifyCoreSubstitution( } // To avoid rare issues where purification variables introduced by this method // already appear in the inference, we also purify them here. - SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); SkolemId id; Node cval; for (const Node& nc : children) { // if this is a purification skolem of a term that is being purified, // we purify this. - if (sm->isSkolemFunction(nc[0], id, cval) && id == SkolemId::PURIFY + if (SkolemManager::isSkolemFunction(nc[0], id, cval) && id == SkolemId::PURIFY && termsToPurify.find(cval) != termsToPurify.end()) { termsToPurify.insert(nc[0]); @@ -1447,8 +1446,7 @@ Node InferProofCons::maybePurifyTerm( // did not need to purify return n; } - SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); - Node k = sm->mkPurifySkolem(n); + Node k = SkolemManager::mkPurifySkolem(n); return k; } diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index 219ba9790d2..ca81659ce66 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -63,10 +63,10 @@ TermRegistry::TermRegistry(Env& env, : nullptr), d_inFullEffortCheck(false) { - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = nodeManager(); d_zero = nm->mkConstInt(Rational(0)); d_one = nm->mkConstInt(Rational(1)); - d_negOne = NodeManager::currentNM()->mkConstInt(Rational(-1)); + d_negOne = nm->mkConstInt(Rational(-1)); Assert(options().strings.stringsAlphaCard <= String::num_codes()); d_alphaCard = options().strings.stringsAlphaCard; } @@ -372,7 +372,7 @@ void TermRegistry::registerType(TypeNode tn) TrustNode TermRegistry::getRegisterTermLemma(Node n) { Assert(n.getType().isStringLike()); - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = nodeManager(); // register length information: // for variables, split on empty vs positive length // for concat/const/replace, introduce proxy var and state length relation @@ -487,7 +487,7 @@ bool TermRegistry::isHandledUpdateOrSubstr(Node n) { Assert(n.getKind() == Kind::STRING_UPDATE || n.getKind() == Kind::STRING_SUBSTR); - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = nodeManager(); Node lenN = n[2]; if (n.getKind() == Kind::STRING_UPDATE) { @@ -517,7 +517,7 @@ TrustNode TermRegistry::getRegisterTermAtomicLemma( return TrustNode::null(); } Assert(n.getType().isStringLike()); - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = nodeManager(); Node n_len = nm->mkNode(Kind::STRING_LENGTH, n); Node emp = Word::mkEmptyWord(n.getType()); if (s == LENGTH_GEQ_ONE) @@ -616,7 +616,7 @@ Node TermRegistry::getSymbolicDefinition(Node n, std::vector& exp) const } } } - return NodeManager::currentNM()->mkNode(n.getKind(), children); + return nodeManager()->mkNode(n.getKind(), children); } Node TermRegistry::getProxyVariableFor(Node n) const diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 4a3245c3ecf..3e625b2cb51 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -1112,7 +1112,7 @@ Node StringsPreprocess::simplifyRec(Node t, std::vector& asserts) } Node tmp = t; if( changed ){ - tmp = NodeManager::currentNM()->mkNode( t.getKind(), cc ); + tmp = nodeManager()->mkNode( t.getKind(), cc ); } // We cannot statically reduce seq.nth due to it being partial function. // Reducing it here would violate the functional property of seq.nth. diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp index 4123a4aa1f6..1fdcb838c33 100644 --- a/src/theory/strings/word.cpp +++ b/src/theory/strings/word.cpp @@ -69,7 +69,7 @@ Node Word::mkWordFlatten(const std::vector& xs) const std::vector& vecc = sx.getVec(); seq.insert(seq.end(), vecc.begin(), vecc.end()); } - return NodeManager::currentNM()->mkConst( + return nm->mkConst( Sequence(tn.getSequenceElementType(), seq)); } Unimplemented(); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 77b9fcd65ad..dbac310821a 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -89,27 +89,6 @@ namespace theory { /* -------------------------------------------------------------------------- */ -inline void flattenAnd(Node n, std::vector& out){ - Assert(n.getKind() == Kind::AND); - for(Node::iterator i=n.begin(), i_end=n.end(); i != i_end; ++i){ - Node curr = *i; - if (curr.getKind() == Kind::AND) - { - flattenAnd(curr, out); - } - else - { - out.push_back(curr); - } - } -} - -inline Node flattenAnd(Node n){ - std::vector out; - flattenAnd(n, out); - return NodeManager::currentNM()->mkNode(Kind::AND, out); -} - /** * Compute the string for a given theory id. In this module, we use * THEORY_SAT_SOLVER as an id, which is not a normal id but maps to @@ -286,8 +265,8 @@ TheoryEngine::TheoryEngine(Env& env) d_cp.reset(new ConflictProcessor(env, useExtRewriter)); } - d_true = NodeManager::currentNM()->mkConst(true); - d_false = NodeManager::currentNM()->mkConst(false); + d_true = nodeManager()->mkConst(true); + d_false = nodeManager()->mkConst(false); } TheoryEngine::~TheoryEngine() { @@ -1927,7 +1906,7 @@ TrustNode TheoryEngine::getExplanation( if (exp.size() == 0) { // Normalize to true - expNode = NodeManager::currentNM()->mkConst(true); + expNode = nodeManager()->mkConst(true); } else if (exp.size() == 1) { @@ -2175,7 +2154,7 @@ std::pair TheoryEngine::entailmentCheck(options::TheoryOfMode mode, } if( is_conjunction ){ return std::pair( - true, NodeManager::currentNM()->mkNode(Kind::AND, children)); + true, nodeManager()->mkNode(Kind::AND, children)); }else{ return std::pair(false, Node::null()); } diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 4ed40f91977..e890fdd9084 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -1337,7 +1337,7 @@ void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f) TypeNode rangeType = f.getType().getRangeType(); if (dfvm == options::DefaultFunctionValueMode::HOLE) { - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = nodeManager(); SkolemManager* sm = nm->getSkolemManager(); std::vector cacheVals; cacheVals.push_back(nm->mkConst(SortToTerm(rangeType))); @@ -1389,7 +1389,7 @@ void TheoryEngineModelBuilder::assignHoFunction(TheoryModel* m, Node f) Node curr, currPre; if (dfvm == options::DefaultFunctionValueMode::HOLE) { - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = nodeManager(); SkolemManager* sm = nm->getSkolemManager(); std::vector cacheVals; cacheVals.push_back(nm->mkConst(SortToTerm(rangeType))); From 6c1b9d26cad7cf5c75cefd16107e231916cdf6bf Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Wed, 18 Dec 2024 10:08:00 -0600 Subject: [PATCH 6/9] Disable unsat-core tester on t3_rw903 (#11458) This fixes a timeout in the nightlies. --- test/regress/cli/regress0/proofs/t3_rw903.smt2 | 1 + 1 file changed, 1 insertion(+) diff --git a/test/regress/cli/regress0/proofs/t3_rw903.smt2 b/test/regress/cli/regress0/proofs/t3_rw903.smt2 index 052e207ed5f..93cc7ebfb7d 100644 --- a/test/regress/cli/regress0/proofs/t3_rw903.smt2 +++ b/test/regress/cli/regress0/proofs/t3_rw903.smt2 @@ -1,4 +1,5 @@ ; EXPECT: unsat +; DISABLE-TESTER: unsat-core (set-logic UFNIA) (declare-fun pow2 (Int) Int) (declare-fun intor (Int Int Int) Int) From f102069ee7a7f629bc83aa886df67208c2843227 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 18 Dec 2024 10:09:32 -0600 Subject: [PATCH 7/9] Several fixes for quantifiers rewrite proofs (#11456) 1. We had an incorrect definition of quant_unused_vars in Eunoia. 2. We did not checking for shadowing in miniscope_or internally, which would lead to checking failures. A regression is added that triggers both issues 1 and 2. 3. The elaboration for macro quant rewrite body did not properly take instantiation pattern lists into account. A regression is added for this issue. --- proofs/eo/cpc/rules/Quantifiers.eo | 3 ++- src/rewriter/basic_rewrite_rcons.cpp | 10 +++++++- .../quantifiers/quantifiers_rewriter.cpp | 6 +++++ test/regress/cli/CMakeLists.txt | 2 ++ .../quantifiers/dd_spark2014-pat.smt2 | 15 ++++++++++++ .../quantifiers/quick-sort-q-rew.smt2 | 23 +++++++++++++++++++ 6 files changed, 57 insertions(+), 2 deletions(-) create mode 100644 test/regress/cli/regress0/quantifiers/dd_spark2014-pat.smt2 create mode 100644 test/regress/cli/regress1/quantifiers/quick-sort-q-rew.smt2 diff --git a/proofs/eo/cpc/rules/Quantifiers.eo b/proofs/eo/cpc/rules/Quantifiers.eo index 23f35f021a6..e9702c2ccdb 100644 --- a/proofs/eo/cpc/rules/Quantifiers.eo +++ b/proofs/eo/cpc/rules/Quantifiers.eo @@ -127,7 +127,8 @@ (($mk_quant_unused_vars_rec @list.nil F) @list.nil) (($mk_quant_unused_vars_rec (@list x xs) F) (eo::define ((r ($mk_quant_unused_vars_rec xs F))) (eo::ite ($contains_subterm F x) - (eo::ite ($contains_subterm r x) r (eo::cons @list x r)) + ; remove the duplicate of x in r if it exists + (eo::cons @list x ($nary_remove @list @list.nil x r)) r))) ) ) diff --git a/src/rewriter/basic_rewrite_rcons.cpp b/src/rewriter/basic_rewrite_rcons.cpp index df7c4ebe96d..ec63b44f2aa 100644 --- a/src/rewriter/basic_rewrite_rcons.cpp +++ b/src/rewriter/basic_rewrite_rcons.cpp @@ -1086,7 +1086,15 @@ bool BasicRewriteRCons::ensureProofMacroQuantRewriteBody(CDProof* cdp, << std::endl; // Call the utility again with proof tracking and construct the term // conversion proof. This proof itself may have trust steps in it. - TConvProofGenerator tcpg(d_env, nullptr); + // We ensure the proof generator does not rewrite in the pattern list using a + // term context. + WithinKindTermContext wktc(Kind::INST_PATTERN_LIST); + TConvProofGenerator tcpg(d_env, + nullptr, + TConvPolicy::FIXPOINT, + TConvCachePolicy::NEVER, + "EnsureProofMacroQuantRewrite", + &wktc); theory::quantifiers::QuantifiersRewriter qrew( nodeManager(), d_env.getRewriter(), options()); Node qr = qrew.computeRewriteBody(eq[0], &tcpg); diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 9770a1742d4..8a2e639f643 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -279,6 +279,12 @@ Node QuantifiersRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n) size_t prevVarIndex = varIndex; while (varIndex < nvars && fvs.find(n[0][varIndex]) != fvs.end()) { + // cannot have shadowing + if (varsUsed.find(n[0][varIndex]) != varsUsed.end()) + { + return Node::null(); + } + varsUsed.insert(n[0][varIndex]); varIndex++; } std::vector dvs(n[0].begin() + prevVarIndex, diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 5ccfe96efd8..2c51cb76988 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -1457,6 +1457,7 @@ set(regress_0_tests regress0/quantifiers/clock-3.smt2 regress0/quantifiers/cond-var-elim-binary.smt2 regress0/quantifiers/dd_german169_semi_eval.smt2 + regress0/quantifiers/dd_spark2014-pat.smt2 regress0/quantifiers/dd.german169-ieval.smt2 regress0/quantifiers/dd.german169-lemma-inp.smt2 regress0/quantifiers/dd.ho-matching-enum.smt2 @@ -2918,6 +2919,7 @@ set(regress_1_tests regress1/quantifiers/qid-debug-inst.smt2 regress1/quantifiers/quant-wf-int-ind.smt2 regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 + regress1/quantifiers/quick-sort-q-rew.smt2 regress1/quantifiers/qs-has-term.smt2 regress1/quantifiers/recfact.cvc.smt2 regress1/quantifiers/rel-trigger-unusable.smt2 diff --git a/test/regress/cli/regress0/quantifiers/dd_spark2014-pat.smt2 b/test/regress/cli/regress0/quantifiers/dd_spark2014-pat.smt2 new file mode 100644 index 00000000000..babf76bbbba --- /dev/null +++ b/test/regress/cli/regress0/quantifiers/dd_spark2014-pat.smt2 @@ -0,0 +1,15 @@ +; EXPECT: unsat +(set-logic ALL) +(declare-sort i 0) +(declare-fun ii (i) Int) +(define-fun t ((x i)) Int (ii x)) +(declare-fun o (Int) i) +(assert (forall ((x i)) (! (= x (o (t x))) :pattern ((t x))))) +(declare-sort t 0) +(declare-fun l (t) i) +(declare-fun m (Int Int) t) +(declare-datatypes ((u 0)) (((uc (e (Array Int i)) (r t))))) +(declare-fun s (i Int) (Array Int i)) +(assert (forall ((v i)) (forall ((i Int)) (= v (select (s v i) i))))) +(assert (exists ((n u)) (not (=> (exists ((o i)) (= 1 (ii o))) (= (- 1) (ii (l (r (uc (s (o 1) 0) (m 0 0)))))) (= 1 (ii (select (e (uc (s (o 1) (- 1)) (m 0 0))) (ii (l (r (uc (s (o 1) 0) (m 0 0)))))))))))) +(check-sat) diff --git a/test/regress/cli/regress1/quantifiers/quick-sort-q-rew.smt2 b/test/regress/cli/regress1/quantifiers/quick-sort-q-rew.smt2 new file mode 100644 index 00000000000..e37a4c3b1cb --- /dev/null +++ b/test/regress/cli/regress1/quantifiers/quick-sort-q-rew.smt2 @@ -0,0 +1,23 @@ +; EXPECT: unsat +(set-logic AUFBVDTLIA) +(declare-datatypes ((List!1123 0)) (((Cons!1124 (head!1125 (_ BitVec 32)) (tail!1126 List!1123)) (Nil!1127)) +)) +(declare-datatypes ((OptInt!1128 0)) (((None!1129) (Some!1130 (i!1131 (_ BitVec 32)))) +)) +(declare-fun error_value!1132 () OptInt!1128) +(declare-fun error_value!1133 () OptInt!1128) +(declare-fun max!216 (List!1123) OptInt!1128) +(declare-fun error_value!1134 () List!1123) +(declare-fun smaller!233 ((_ BitVec 32) List!1123) List!1123) +(declare-fun error_value!1135 () Bool) +(declare-sort I_max!216 0) +(declare-fun max!216_arg_0_1 (I_max!216) List!1123) +(declare-sort I_smaller!233 0) +(declare-fun smaller!233_arg_0_2 (I_smaller!233) (_ BitVec 32)) +(declare-fun smaller!233_arg_1_3 (I_smaller!233) List!1123) +(assert (forall ((?i I_max!216)) (and (= (max!216 (max!216_arg_0_1 ?i)) (ite ((_ is Nil!1127) (max!216_arg_0_1 ?i)) None!1129 (ite ((_ is Cons!1124) (max!216_arg_0_1 ?i)) (ite ((_ is Some!1130) (max!216 (tail!1126 (max!216_arg_0_1 ?i)))) (ite (not (bvslt (head!1125 (max!216_arg_0_1 ?i)) (i!1131 (max!216 (tail!1126 (max!216_arg_0_1 ?i)))))) (Some!1130 (head!1125 (max!216_arg_0_1 ?i))) (Some!1130 (i!1131 (max!216 (tail!1126 (max!216_arg_0_1 ?i)))))) (ite ((_ is None!1129) (max!216 (tail!1126 (max!216_arg_0_1 ?i)))) (Some!1130 (head!1125 (max!216_arg_0_1 ?i))) error_value!1132)) error_value!1133))) (ite ((_ is Nil!1127) (max!216_arg_0_1 ?i)) true (ite ((_ is Cons!1124) (max!216_arg_0_1 ?i)) (and (not (forall ((?z I_max!216)) (not (= (max!216_arg_0_1 ?z) (tail!1126 (max!216_arg_0_1 ?i)))) )) (ite ((_ is Some!1130) (max!216 (tail!1126 (max!216_arg_0_1 ?i)))) (and (not (forall ((?z I_max!216)) (not (= (max!216_arg_0_1 ?z) (tail!1126 (max!216_arg_0_1 ?i)))) )) (ite (not (bvslt (head!1125 (max!216_arg_0_1 ?i)) (i!1131 (max!216 (tail!1126 (max!216_arg_0_1 ?i)))))) true (not (forall ((?z I_max!216)) (not (= (max!216_arg_0_1 ?z) (tail!1126 (max!216_arg_0_1 ?i)))) )))) (not (forall ((?z I_max!216)) (not (= (max!216_arg_0_1 ?z) (tail!1126 (max!216_arg_0_1 ?i)))) )))) true))) )) +(assert (forall ((?i I_smaller!233)) (and (= (smaller!233 (smaller!233_arg_0_2 ?i) (smaller!233_arg_1_3 ?i)) (ite ((_ is Nil!1127) (smaller!233_arg_1_3 ?i)) Nil!1127 (ite ((_ is Cons!1124) (smaller!233_arg_1_3 ?i)) (ite (bvslt (head!1125 (smaller!233_arg_1_3 ?i)) (smaller!233_arg_0_2 ?i)) (Cons!1124 (head!1125 (smaller!233_arg_1_3 ?i)) (smaller!233 (smaller!233_arg_0_2 ?i) (tail!1126 (smaller!233_arg_1_3 ?i)))) (smaller!233 (smaller!233_arg_0_2 ?i) (tail!1126 (smaller!233_arg_1_3 ?i)))) error_value!1134))) (ite ((_ is Nil!1127) (smaller!233_arg_1_3 ?i)) true (ite ((_ is Cons!1124) (smaller!233_arg_1_3 ?i)) (ite (bvslt (head!1125 (smaller!233_arg_1_3 ?i)) (smaller!233_arg_0_2 ?i)) (not (forall ((?z I_smaller!233)) (not (and (= (smaller!233_arg_0_2 ?z) (smaller!233_arg_0_2 ?i)) (= (smaller!233_arg_1_3 ?z) (tail!1126 (smaller!233_arg_1_3 ?i))))) )) (not (forall ((?z I_smaller!233)) (not (and (= (smaller!233_arg_0_2 ?z) (smaller!233_arg_0_2 ?i)) (= (smaller!233_arg_1_3 ?z) (tail!1126 (smaller!233_arg_1_3 ?i))))) ))) true))) )) +(assert (not (forall ((n!234 (_ BitVec 32))) (or (ite ((_ is Some!1130) (max!216 (smaller!233 (i!1131 (max!216 (smaller!233 n!234 Nil!1127))) Nil!1127))) (bvslt n!234 n!234) (or (ite ((_ is None!1129) (max!216 (smaller!233 n!234 Nil!1127))) true error_value!1135) (forall ((?z I_max!216)) (not (= (max!216_arg_0_1 ?z) (smaller!233 n!234 Nil!1127))) ) (forall ((?z I_smaller!233)) (not (and (= (smaller!233_arg_0_2 ?z) n!234) (= (smaller!233_arg_1_3 ?z) Nil!1127))) ))) (forall ((?z I_max!216)) (not (= (max!216_arg_0_1 ?z) (smaller!233 (i!1131 (max!216 (smaller!233 n!234 Nil!1127))) Nil!1127))) ) (forall ((?z I_smaller!233)) (not (and (= (smaller!233_arg_0_2 ?z) (i!1131 (max!216 (smaller!233 n!234 Nil!1127)))) (= (smaller!233_arg_1_3 ?z) Nil!1127))) ) (forall ((?z I_max!216)) (not (= (max!216_arg_0_1 ?z) (smaller!233 n!234 Nil!1127))) ) (forall ((?z I_smaller!233)) (not (and (= (smaller!233_arg_0_2 ?z) n!234) (= (smaller!233_arg_1_3 ?z) Nil!1127))) )) ))) +(check-sat) +(exit) + From d9249b35a6b7a1387831deb09fd479ef26eaacce Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 18 Dec 2024 11:02:13 -0600 Subject: [PATCH 8/9] Make DT_CONS_EQ macro, elaborate to simpler version (#11420) This fixes proof failures in datatypes involving the rule DT_CONS_EQ. This rule currently involves a more complex implementation than what is documented and expected. This fixes the documentation, makes it a macro, and introduces 2 new rules for its elaboration. We then use the simpler version in the datatypes infer proof constructor. The proof elaboration for this macro is not yet complete, but this fixes the open proof errors involving this rule, included is an example regression. --- include/cvc5/cvc5_proof_rule.h | 39 +++++++- src/api/cpp/cvc5_proof_rule_template.cpp | 2 + src/proof/conv_proof_generator.cpp | 10 ++ src/proof/conv_proof_generator.h | 6 ++ src/rewriter/basic_rewrite_rcons.cpp | 93 +++++++++++++++++++ src/rewriter/basic_rewrite_rcons.h | 9 ++ src/theory/datatypes/datatypes_rewriter.cpp | 52 +++++++++-- src/theory/datatypes/theory_datatypes.cpp | 2 +- .../datatypes/theory_datatypes_utils.cpp | 7 +- src/theory/datatypes/theory_datatypes_utils.h | 11 ++- test/regress/cli/CMakeLists.txt | 2 + .../regress0/datatypes/dt-cons-eq-simple.smt2 | 11 +++ .../regress0/proofs/pfcheck-ufdt-distro.smt2 | 19 ++++ 13 files changed, 246 insertions(+), 17 deletions(-) create mode 100644 test/regress/cli/regress0/datatypes/dt-cons-eq-simple.smt2 create mode 100644 test/regress/cli/regress0/proofs/pfcheck-ufdt-distro.smt2 diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h index b4affb0b934..319ccff2acf 100644 --- a/include/cvc5/cvc5_proof_rule.h +++ b/include/cvc5/cvc5_proof_rule.h @@ -2786,6 +2786,26 @@ enum ENUM(ProofRewriteRule) * \endverbatim */ EVALUE(DT_COLLAPSE_TESTER_SINGLETON), + /** + * \verbatim embed:rst:leading-asterisk + * **Datatypes -- Macro constructor equality** + * + * .. math:: + * (t = s) = (t_1 = s_1 \wedge \ldots \wedge t_n = s_n) + * + * where :math:`t_1, \ldots, t_n` and :math:`s_1, \ldots, s_n` are subterms + * of :math:`t` and :math:`s` that occur at the same position respectively + * (beneath constructor applications), or alternatively + * + * .. math:: + * (t = s) = false + * + * where :math:`t` and :math:`s` have subterms that occur in the same + * position (beneath constructor applications) that are distinct. + * + * \endverbatim + */ + EVALUE(MACRO_DT_CONS_EQ), /** * \verbatim embed:rst:leading-asterisk * **Datatypes -- constructor equality** @@ -2793,17 +2813,26 @@ enum ENUM(ProofRewriteRule) * .. math:: * (c(t_1, \ldots, t_n) = c(s_1, \ldots, s_n)) = * (t_1 = s_1 \wedge \ldots \wedge t_n = s_n) + * + * where :math:`c` is a constructor. * - * or alternatively + * \endverbatim + */ + EVALUE(DT_CONS_EQ), + /** + * \verbatim embed:rst:leading-asterisk + * **Datatypes -- constructor equality clash** * * .. math:: - * (c(t_1, \ldots, t_n) = d(s_1, \ldots, s_m)) = false - * - * where :math:`c` and :math:`d` are distinct constructors. + * (t = s) = false + * + * where :math:`t` and :math:`s` have subterms that occur in the same + * position (beneath constructor applications) that are distinct constructor + * applications. * * \endverbatim */ - EVALUE(DT_CONS_EQ), + EVALUE(DT_CONS_EQ_CLASH), /** * \verbatim embed:rst:leading-asterisk * **Datatypes -- cycle** diff --git a/src/api/cpp/cvc5_proof_rule_template.cpp b/src/api/cpp/cvc5_proof_rule_template.cpp index f837d9e904d..943d97d788c 100644 --- a/src/api/cpp/cvc5_proof_rule_template.cpp +++ b/src/api/cpp/cvc5_proof_rule_template.cpp @@ -269,7 +269,9 @@ const char* toString(cvc5::ProofRewriteRule rule) case ProofRewriteRule::DT_COLLAPSE_TESTER: return "dt-collapse-tester"; case ProofRewriteRule::DT_COLLAPSE_TESTER_SINGLETON: return "dt-collapse-tester-singleton"; + case ProofRewriteRule::MACRO_DT_CONS_EQ: return "macro-dt-cons-eq"; case ProofRewriteRule::DT_CONS_EQ: return "dt-cons-eq"; + case ProofRewriteRule::DT_CONS_EQ_CLASH: return "dt-cons-eq-clash"; case ProofRewriteRule::DT_CYCLE: return "dt-cycle"; case ProofRewriteRule::DT_COLLAPSE_UPDATER: return "dt-collapse-updater"; case ProofRewriteRule::DT_UPDATER_ELIM: return "dt-updater-elim"; diff --git a/src/proof/conv_proof_generator.cpp b/src/proof/conv_proof_generator.cpp index 2db8a60d6b4..6c66381e93a 100644 --- a/src/proof/conv_proof_generator.cpp +++ b/src/proof/conv_proof_generator.cpp @@ -23,6 +23,7 @@ #include "proof/proof_checker.h" #include "proof/proof_node.h" #include "proof/proof_node_algorithm.h" +#include "rewriter/rewrites.h" using namespace cvc5::internal::kind; @@ -112,6 +113,15 @@ void TConvProofGenerator::addRewriteStep(Node t, } } +void TConvProofGenerator::addTheoryRewriteStep( + Node t, Node s, ProofRewriteRule id, bool isPre, uint32_t tctx) +{ + std::vector sargs; + sargs.push_back(rewriter::mkRewriteRuleNode(id)); + sargs.push_back(t.eqNode(s)); + addRewriteStep(t, s, ProofRule::THEORY_REWRITE, {}, sargs, isPre, tctx); +} + bool TConvProofGenerator::hasRewriteStep(Node t, uint32_t tctx, bool isPre) const diff --git a/src/proof/conv_proof_generator.h b/src/proof/conv_proof_generator.h index 1b7b428aa8d..942a8ff4eef 100644 --- a/src/proof/conv_proof_generator.h +++ b/src/proof/conv_proof_generator.h @@ -172,6 +172,12 @@ class TConvProofGenerator : protected EnvObj, public ProofGenerator const std::vector& args, bool isPre = false, uint32_t tctx = 0); + /** Same as above, with a theory rewrite step */ + void addTheoryRewriteStep(Node t, + Node s, + ProofRewriteRule id, + bool isPre = false, + uint32_t tctx = 0); /** Has rewrite step for term t */ bool hasRewriteStep(Node t, uint32_t tctx = 0, bool isPre = false) const; /** diff --git a/src/rewriter/basic_rewrite_rcons.cpp b/src/rewriter/basic_rewrite_rcons.cpp index ec63b44f2aa..23611a34219 100644 --- a/src/rewriter/basic_rewrite_rcons.cpp +++ b/src/rewriter/basic_rewrite_rcons.cpp @@ -182,6 +182,12 @@ void BasicRewriteRCons::ensureProofForTheoryRewrite( handledMacro = true; } break; + case ProofRewriteRule::MACRO_DT_CONS_EQ: + if (ensureProofMacroDtConsEq(cdp, eq)) + { + handledMacro = true; + } + break; case ProofRewriteRule::MACRO_ARITH_STRING_PRED_ENTAIL: if (ensureProofMacroArithStringPredEntail(cdp, eq)) { @@ -274,6 +280,93 @@ bool BasicRewriteRCons::ensureProofMacroBoolNnfNorm(CDProof* cdp, return true; } +bool BasicRewriteRCons::ensureProofMacroDtConsEq(CDProof* cdp, const Node& eq) +{ + Assert(eq.getKind() == Kind::EQUAL); + Trace("brc-macro") << "Expand dt cons eq for " << eq << std::endl; + TConvProofGenerator tcpg(d_env); + theory::Rewriter* rr = d_env.getRewriter(); + if (eq[1].isConst()) + { + // DT_CONS_EQ_CLASH may suffice if it is purely datatypes + Node curRew = rr->rewriteViaRule(ProofRewriteRule::DT_CONS_EQ_CLASH, eq[0]); + if (curRew == eq[1]) + { + cdp->addTheoryRewriteStep(eq, ProofRewriteRule::DT_CONS_EQ_CLASH); + return true; + } + // otherwise, we require proving the non-datatype constants are distinct + // this case is not yet handled. + return false; + } + std::unordered_set visited; + std::vector visit; + TNode cur; + visit.push_back(eq[0]); + do + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + visited.insert(cur); + if (cur.getKind() == Kind::EQUAL) + { + // if a reflexive component, it rewrites to true + if (cur[0] == cur[1]) + { + Node truen = nodeManager()->mkConst(true); + tcpg.addRewriteStep(cur, + truen, + nullptr, + true, + TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE); + continue; + } + Node curRew = rr->rewriteViaRule(ProofRewriteRule::DT_CONS_EQ, cur); + if (!curRew.isNull()) + { + tcpg.addTheoryRewriteStep( + cur, curRew, ProofRewriteRule::DT_CONS_EQ, true); + visit.push_back(curRew); + } + } + else + { + // traverse AND + Assert(cur.getKind() == Kind::AND); + visit.insert(visit.end(), cur.begin(), cur.end()); + } + } + } while (!visit.empty()); + // get proof for rewriting, which should expand equalities + std::shared_ptr pfn = tcpg.getProofForRewriting(eq[0]); + Node res = pfn->getResult(); + Assert(res.getKind() == Kind::EQUAL); + // the right hand side should rewrite to the other side + Node rhs = res[1]; + if (rhs == eq[1]) + { + // no rewrite needed, e.g. one step + cdp->addProof(pfn); + return true; + } + // should rewrite via ACI_NORM + if (!expr::isACINorm(rhs, eq[1])) + { + Trace("brc-macro") << "Failed to show " << rhs << " == " << eq[1] + << std::endl; + Assert(false) << "Failed to show " << rhs << " == " << eq[1] << std::endl; + return false; + } + // use ACI_NORM + cdp->addProof(pfn); + Node eqa = rhs.eqNode(eq[1]); + cdp->addStep(eqa, ProofRule::ACI_NORM, {}, {eqa}); + cdp->addStep(eq, ProofRule::TRANS, {res, eqa}, {}); + return true; +} + bool BasicRewriteRCons::ensureProofMacroArithStringPredEntail(CDProof* cdp, const Node& eq) { diff --git a/src/rewriter/basic_rewrite_rcons.h b/src/rewriter/basic_rewrite_rcons.h index 7ff561a0b37..67ab914dc12 100644 --- a/src/rewriter/basic_rewrite_rcons.h +++ b/src/rewriter/basic_rewrite_rcons.h @@ -140,6 +140,15 @@ class BasicRewriteRCons : protected EnvObj * @return true if added a closed proof of eq to cdp. */ bool ensureProofMacroBoolNnfNorm(CDProof* cdp, const Node& eq); + /** + * Elaborate a rewrite eq that was proven by + * ProofRewriteRule::MACRO_DT_CONS_EQ. + * + * @param cdp The proof to add to. + * @param eq The rewrite proven by ProofRewriteRule::MACRO_DT_CONS_EQ. + * @return true if added a closed proof of eq to cdp. + */ + bool ensureProofMacroDtConsEq(CDProof* cdp, const Node& eq); /** * Elaborate a rewrite eq that was proven by * ProofRewriteRule::MACRO_ARITH_STRING_PRED_ENTAIL. diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index d506b63773c..b57b00912e0 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -49,7 +49,9 @@ DatatypesRewriter::DatatypesRewriter(NodeManager* nm, TheoryRewriteCtx::PRE_DSL); registerProofRewriteRule(ProofRewriteRule::DT_COLLAPSE_TESTER_SINGLETON, TheoryRewriteCtx::PRE_DSL); - registerProofRewriteRule(ProofRewriteRule::DT_CONS_EQ, + // DT_CONS_EQ and DT_CONS_EQ_CLASH are part of the reconstruction of + // MACRO_DT_CONS_EQ. + registerProofRewriteRule(ProofRewriteRule::MACRO_DT_CONS_EQ, TheoryRewriteCtx::PRE_DSL); registerProofRewriteRule(ProofRewriteRule::DT_COLLAPSE_UPDATER, TheoryRewriteCtx::PRE_DSL); @@ -126,7 +128,7 @@ Node DatatypesRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n) } } break; - case ProofRewriteRule::DT_CONS_EQ: + case ProofRewriteRule::MACRO_DT_CONS_EQ: { if (n.getKind() == Kind::EQUAL) { @@ -136,10 +138,14 @@ Node DatatypesRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n) { nn = nodeManager()->mkConst(false); } - else + else if (!rew.empty()) { nn = nodeManager()->mkAnd(rew); } + else + { + return Node::null(); + } // In the "else" case above will n if this rewrite does not apply. We // do not return the reflexive equality in this case. if (nn != n) @@ -149,6 +155,42 @@ Node DatatypesRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n) } } break; + case ProofRewriteRule::DT_CONS_EQ: + { + if (n.getKind() != Kind::EQUAL + || n[0].getKind() != Kind::APPLY_CONSTRUCTOR + || n[1].getKind() != Kind::APPLY_CONSTRUCTOR) + { + return Node::null(); + } + if (n[0].getOperator() == n[1].getOperator()) + { + Assert(n[0].getNumChildren() == n[1].getNumChildren()); + std::vector children; + for (size_t i = 0, size = n[0].getNumChildren(); i < size; i++) + { + children.push_back(n[0][i].eqNode(n[1][i])); + } + return nodeManager()->mkAnd(children); + } + } + break; + case ProofRewriteRule::DT_CONS_EQ_CLASH: + { + if (n.getKind() != Kind::EQUAL + || n[0].getKind() != Kind::APPLY_CONSTRUCTOR + || n[1].getKind() != Kind::APPLY_CONSTRUCTOR) + { + return Node::null(); + } + // do not look for constant clashing equality between non-datatypes + std::vector rew; + if (utils::checkClash(n[0], n[1], rew, false)) + { + return nodeManager()->mkConst(false); + } + } + break; case ProofRewriteRule::DT_UPDATER_ELIM: { if (n.getKind() == Kind::APPLY_UPDATER) @@ -379,10 +421,6 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in) Trace("datatypes-rewrite") << "Rewrite clashing equality " << in << " to false" << std::endl; return RewriteResponse(REWRITE_DONE, nm->mkConst(false)); - //}else if( rew.size()==1 && rew[0]!=in ){ - // Trace("datatypes-rewrite") << "Rewrite equality " << in << " to " << - // rew[0] << std::endl; - // return RewriteResponse(REWRITE_AGAIN_FULL, rew[0] ); } else if (in[1] < in[0]) { diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 1b1f50e1147..edbab9eefba 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -392,7 +392,7 @@ TrustNode TheoryDatatypes::ppStaticRewrite(TNode in) << endl; if (in.getKind() == Kind::EQUAL) { - Node nn = d_rewriter.rewriteViaRule(ProofRewriteRule::DT_CONS_EQ, in); + Node nn = d_rewriter.rewriteViaRule(ProofRewriteRule::MACRO_DT_CONS_EQ, in); if (!nn.isNull() && in != nn) { return TrustNode::mkTrustRewrite(in, nn, nullptr); diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp index 9f953fc3800..be7b190947e 100644 --- a/src/theory/datatypes/theory_datatypes_utils.cpp +++ b/src/theory/datatypes/theory_datatypes_utils.cpp @@ -161,7 +161,7 @@ bool isNullaryConstructor(const DTypeConstructor& c) return true; } -bool checkClash(Node n1, Node n2, std::vector& rew) +bool checkClash(Node n1, Node n2, std::vector& rew, bool checkNdtConst) { Trace("datatypes-rewrite-debug") << "Check clash : " << n1 << " " << n2 << std::endl; @@ -178,7 +178,7 @@ bool checkClash(Node n1, Node n2, std::vector& rew) Assert(n1.getNumChildren() == n2.getNumChildren()); for (unsigned i = 0, size = n1.getNumChildren(); i < size; i++) { - if (checkClash(n1[i], n2[i], rew)) + if (checkClash(n1[i], n2[i], rew, checkNdtConst)) { return true; } @@ -186,7 +186,8 @@ bool checkClash(Node n1, Node n2, std::vector& rew) } else if (n1 != n2) { - if (n1.isConst() && n2.isConst()) + // if checking equality between non-datatypes + if (checkNdtConst && n1.isConst() && n2.isConst()) { Trace("datatypes-rewrite-debug") << "Clash constants : " << n1 << " " << n2 << std::endl; diff --git a/src/theory/datatypes/theory_datatypes_utils.h b/src/theory/datatypes/theory_datatypes_utils.h index b8450af4d79..94d7aa88d97 100644 --- a/src/theory/datatypes/theory_datatypes_utils.h +++ b/src/theory/datatypes/theory_datatypes_utils.h @@ -109,8 +109,17 @@ bool isNullaryConstructor(const DTypeConstructor& c); * C( x, y ) and C( D( x ), y ) * C( D( x ), y ) and C( x, E( z ) ) * C( x, y ) and z + * + * @param n1 The first term. + * @param n2 The second term. + * @param rew The set of entailed equalities. + * @param checkNdtConst If true, we consider constants (of non-datatype type) to + * be a conflict. */ -bool checkClash(Node n1, Node n2, std::vector& rew); +bool checkClash(Node n1, + Node n2, + std::vector& rew, + bool checkNdtConst = true); } // namespace utils } // namespace datatypes diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 2c51cb76988..71ae0c13d55 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -695,6 +695,7 @@ set(regress_0_tests regress0/datatypes/datatype4.cvc.smt2 regress0/datatypes/dd.pair-real-bool-const-conf.smt2 regress0/datatypes/dt-2.6.smt2 + regress0/datatypes/dt-cons-eq-simple.smt2 regress0/datatypes/dt-different-params.smt2 regress0/datatypes/dt-match-pat-param-2.6.smt2 regress0/datatypes/dt-param-2.6-print.smt2 @@ -1358,6 +1359,7 @@ set(regress_0_tests regress0/proofs/open-pf-if-unordered-iff.smt2 regress0/proofs/open-pf-rederivation.smt2 regress0/proofs/other-optResRecons-corner-case.smt2 + regress0/proofs/pfcheck-ufdt-distro.smt2 regress0/proofs/project-issue317-inc-sat-conflictlit.smt2 regress0/proofs/project-issue330-eqproof.smt2 regress0/proofs/proj-issue326-nl-bounds-check.smt2 diff --git a/test/regress/cli/regress0/datatypes/dt-cons-eq-simple.smt2 b/test/regress/cli/regress0/datatypes/dt-cons-eq-simple.smt2 new file mode 100644 index 00000000000..ef1f4e9ab9b --- /dev/null +++ b/test/regress/cli/regress0/datatypes/dt-cons-eq-simple.smt2 @@ -0,0 +1,11 @@ +; EXPECT: unsat +(set-logic ALL) + +(declare-datatype List ((cons (head Int) (tail List)) (nil))) + +(declare-fun x () Int) +(declare-fun y () Int) + +(assert (not (= x y))) +(assert (= (cons x nil) (cons y nil))) +(check-sat) diff --git a/test/regress/cli/regress0/proofs/pfcheck-ufdt-distro.smt2 b/test/regress/cli/regress0/proofs/pfcheck-ufdt-distro.smt2 new file mode 100644 index 00000000000..71f49b60238 --- /dev/null +++ b/test/regress/cli/regress0/proofs/pfcheck-ufdt-distro.smt2 @@ -0,0 +1,19 @@ +; EXPECT: unsat +(set-logic ALL) +(declare-sort N 0) +(declare-sort D 0) +(declare-sort N_ 0) +(declare-sort _l 0) +(declare-sort d 0) +(declare-datatypes ((T 0) (l 0) (T_ 0) (i 0) (_d 0) (N_l 0)) (((r (r D))) ((i) (o ($ N) (l2 l))) ((ni)) ((l3)) ((ni)) ((ni)))) +(declare-fun f () N_) +(declare-fun n () N) +(declare-fun c (D) d) +(declare-fun p (N_) _l) +(declare-fun m (T d) Bool) +(declare-fun u (_l l) Bool) +(declare-fun u (N_ N) D) +(assert (not (m (r (u f n)) (c (u f n))))) +(assert (u (p f) (o n (o n i)))) +(assert (forall ((?v l)) (= (u (p f) ?v) (or (exists ((? N) (v N)) (and (= ?v (o v (o ? i))) (m (r (u f ?)) (c (u f v))))))))) +(check-sat) From da255fd537f4e2735a25333759fc34a33e7f24f2 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Wed, 18 Dec 2024 11:58:21 -0600 Subject: [PATCH 9/9] preprocessing/proof: Refactor to not use NodeManager::currentNM() (#11459) This PR introduces some calls to `NodeManager::currentNM()`, which will be removed in subsequent PRs. --- src/preprocessing/passes/synth_rew_rules.cpp | 7 +++---- src/preprocessing/passes/synth_rew_rules.h | 4 ++-- src/proof/lazy_proof.cpp | 2 +- src/proof/lazy_tree_proof_generator.cpp | 2 +- src/proof/method_id.cpp | 14 +++++++------- src/proof/method_id.h | 5 +++-- src/proof/proof.cpp | 2 +- src/proof/proof_node_algorithm.cpp | 3 ++- src/proof/proof_node_manager.cpp | 2 +- src/proof/proof_rule_checker.cpp | 5 ++--- src/proof/proof_rule_checker.h | 2 +- src/proof/proof_step_buffer.cpp | 2 +- src/proof/resolution_proofs_util.cpp | 4 ++-- src/proof/resolution_proofs_util.h | 3 ++- src/proof/rewrite_proof_generator.cpp | 6 +++++- src/proof/subtype_elim_proof_converter.cpp | 4 ++-- src/proof/theory_proof_step_buffer.cpp | 10 +++++----- src/proof/trust_id.cpp | 5 ++--- src/proof/trust_id.h | 2 +- src/rewriter/basic_rewrite_rcons.cpp | 2 +- src/rewriter/rewrite_db_proof_cons.cpp | 2 +- src/smt/proof_post_processor.cpp | 5 +++-- src/smt/solver_engine.cpp | 5 +++-- src/theory/arrays/inference_manager.cpp | 2 +- src/theory/datatypes/infer_proof_cons.cpp | 2 +- src/theory/quantifiers/alpha_equivalence.cpp | 3 ++- src/theory/rewriter.cpp | 5 +++-- src/theory/sep/theory_sep.cpp | 2 +- src/theory/sets/inference_manager.cpp | 2 +- src/theory/strings/infer_proof_cons.cpp | 5 +++-- src/theory/theory_preprocessor.cpp | 2 +- src/theory/uf/eq_proof.cpp | 7 ++++--- 32 files changed, 69 insertions(+), 59 deletions(-) diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp index c2b093f1231..e8b373ef8c3 100644 --- a/src/preprocessing/passes/synth_rew_rules.cpp +++ b/src/preprocessing/passes/synth_rew_rules.cpp @@ -51,11 +51,11 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal( } std::vector SynthRewRulesPass::getGrammarsFrom( - const std::vector& assertions, uint64_t nvars) + NodeManager* nm, const std::vector& assertions, uint64_t nvars) { std::vector ret; std::map tlGrammarTypes = - constructTopLevelGrammar(assertions, nvars); + constructTopLevelGrammar(nm, assertions, nvars); for (std::pair ttp : tlGrammarTypes) { ret.push_back(ttp.second); @@ -64,14 +64,13 @@ std::vector SynthRewRulesPass::getGrammarsFrom( } std::map SynthRewRulesPass::constructTopLevelGrammar( - const std::vector& assertions, uint64_t nvars) + NodeManager* nm, const std::vector& assertions, uint64_t nvars) { std::map tlGrammarTypes; if (assertions.empty()) { return tlGrammarTypes; } - NodeManager* nm = NodeManager::currentNM(); // initialize the candidate rewrite std::unordered_map visited; std::unordered_map::iterator it; diff --git a/src/preprocessing/passes/synth_rew_rules.h b/src/preprocessing/passes/synth_rew_rules.h index 42ebd8da780..7c425f224da 100644 --- a/src/preprocessing/passes/synth_rew_rules.h +++ b/src/preprocessing/passes/synth_rew_rules.h @@ -66,11 +66,11 @@ class SynthRewRulesPass : public PreprocessingPass SynthRewRulesPass(PreprocessingPassContext* preprocContext); static std::vector getGrammarsFrom( - const std::vector& assertions, uint64_t nvars); + NodeManager* nm, const std::vector& assertions, uint64_t nvars); protected: static std::map constructTopLevelGrammar( - const std::vector& assertions, uint64_t nvars); + NodeManager* nm, const std::vector& assertions, uint64_t nvars); PreprocessingPassResult applyInternal( AssertionPipeline* assertionsToPreprocess) override; }; diff --git a/src/proof/lazy_proof.cpp b/src/proof/lazy_proof.cpp index bf82bf1134d..7c549998d56 100644 --- a/src/proof/lazy_proof.cpp +++ b/src/proof/lazy_proof.cpp @@ -181,7 +181,7 @@ void LazyCDProof::addLazyStep(Node expected, } Trace("lazy-cdproof") << "LazyCDProof::addLazyStep: " << expected << " set (trusted) step " << idNull << "\n"; - Node tid = mkTrustId(idNull); + Node tid = mkTrustId(nodeManager(), idNull); addStep(expected, ProofRule::TRUST, {}, {tid, expected}); return; } diff --git a/src/proof/lazy_tree_proof_generator.cpp b/src/proof/lazy_tree_proof_generator.cpp index ddd23abc628..1dfe9d4e934 100644 --- a/src/proof/lazy_tree_proof_generator.cpp +++ b/src/proof/lazy_tree_proof_generator.cpp @@ -74,7 +74,7 @@ void LazyTreeProofGenerator::setCurrentTrust(size_t objectId, Node proven) { std::vector newArgs; - newArgs.push_back(mkTrustId(tid)); + newArgs.push_back(mkTrustId(nodeManager(), tid)); newArgs.push_back(proven); newArgs.insert(newArgs.end(), args.begin(), args.end()); setCurrent(objectId, ProofRule::TRUST, premise, newArgs, proven); diff --git a/src/proof/method_id.cpp b/src/proof/method_id.cpp index 1d0ae845ca5..25de7b57bf8 100644 --- a/src/proof/method_id.cpp +++ b/src/proof/method_id.cpp @@ -50,10 +50,9 @@ std::ostream& operator<<(std::ostream& out, MethodId id) return out; } -Node mkMethodId(MethodId id) +Node mkMethodId(NodeManager* nm, MethodId id) { - return NodeManager::currentNM()->mkConstInt( - Rational(static_cast(id))); + return nm->mkConstInt(Rational(static_cast(id))); } bool getMethodId(TNode n, MethodId& i) @@ -98,7 +97,8 @@ bool getMethodIds(const std::vector& args, return true; } -void addMethodIds(std::vector& args, +void addMethodIds(NodeManager* nm, + std::vector& args, MethodId ids, MethodId ida, MethodId idr) @@ -107,15 +107,15 @@ void addMethodIds(std::vector& args, bool ndefApply = (ida != MethodId::SBA_SEQUENTIAL); if (ids != MethodId::SB_DEFAULT || ndefRewriter || ndefApply) { - args.push_back(mkMethodId(ids)); + args.push_back(mkMethodId(nm, ids)); } if (ndefApply || ndefRewriter) { - args.push_back(mkMethodId(ida)); + args.push_back(mkMethodId(nm, ida)); } if (ndefRewriter) { - args.push_back(mkMethodId(idr)); + args.push_back(mkMethodId(nm, idr)); } } diff --git a/src/proof/method_id.h b/src/proof/method_id.h index 2d321dd5f7f..c4c1982b030 100644 --- a/src/proof/method_id.h +++ b/src/proof/method_id.h @@ -84,7 +84,7 @@ const char* toString(MethodId id); /** Write a rewriter id to out */ std::ostream& operator<<(std::ostream& out, MethodId id); /** Make a method id node */ -Node mkMethodId(MethodId id); +Node mkMethodId(NodeManager* nm, MethodId id); /** get a method identifier from a node, return false if we fail */ bool getMethodId(TNode n, MethodId& i); @@ -102,7 +102,8 @@ bool getMethodIds(const std::vector& args, * Add method identifiers ids, ida and idr as nodes to args. This does not add * ids, ida or idr if their values are the default ones. */ -void addMethodIds(std::vector& args, +void addMethodIds(NodeManager* nm, + std::vector& args, MethodId ids, MethodId ida, MethodId idr); diff --git a/src/proof/proof.cpp b/src/proof/proof.cpp index 50bfff12b6f..dbc697890f5 100644 --- a/src/proof/proof.cpp +++ b/src/proof/proof.cpp @@ -267,7 +267,7 @@ bool CDProof::addTrustedStep(Node expected, CDPOverwrite opolicy) { std::vector sargs; - sargs.push_back(mkTrustId(id)); + sargs.push_back(mkTrustId(nodeManager(), id)); sargs.push_back(expected); sargs.insert(sargs.end(), args.begin(), args.end()); return addStep( diff --git a/src/proof/proof_node_algorithm.cpp b/src/proof/proof_node_algorithm.cpp index 7dbe8df0662..542fc9a0d1b 100644 --- a/src/proof/proof_node_algorithm.cpp +++ b/src/proof/proof_node_algorithm.cpp @@ -272,7 +272,8 @@ ProofRule getCongRule(const Node& n, std::vector& args) break; } // Add the arguments - args.push_back(ProofRuleChecker::mkKindNode(k)); + NodeManager* nm = NodeManager::currentNM(); + args.push_back(ProofRuleChecker::mkKindNode(nm, k)); if (kind::metaKindOf(k) == kind::metakind::PARAMETERIZED) { args.push_back(n.getOperator()); diff --git a/src/proof/proof_node_manager.cpp b/src/proof/proof_node_manager.cpp index 2e0a6583fbb..9730c0b4b4a 100644 --- a/src/proof/proof_node_manager.cpp +++ b/src/proof/proof_node_manager.cpp @@ -68,7 +68,7 @@ std::shared_ptr ProofNodeManager::mkTrustedNode( const Node& conc) { std::vector sargs; - sargs.push_back(mkTrustId(id)); + sargs.push_back(mkTrustId(NodeManager::currentNM(), id)); sargs.push_back(conc); sargs.insert(sargs.end(), args.begin(), args.end()); return mkNode(ProofRule::TRUST, children, sargs); diff --git a/src/proof/proof_rule_checker.cpp b/src/proof/proof_rule_checker.cpp index 4e8251b00a4..deca6ebfd7d 100644 --- a/src/proof/proof_rule_checker.cpp +++ b/src/proof/proof_rule_checker.cpp @@ -63,15 +63,14 @@ bool ProofRuleChecker::getKind(TNode n, Kind& k) return true; } -Node ProofRuleChecker::mkKindNode(Kind k) +Node ProofRuleChecker::mkKindNode(NodeManager* nm, Kind k) { if (k == Kind::UNDEFINED_KIND) { // UNDEFINED_KIND is negative, hence return null to avoid cast return Node::null(); } - return NodeManager::currentNM()->mkConstInt( - Rational(static_cast(k))); + return nm->mkConstInt(Rational(static_cast(k))); } NodeManager* ProofRuleChecker::nodeManager() const { return d_nm; } diff --git a/src/proof/proof_rule_checker.h b/src/proof/proof_rule_checker.h index 6a5dbf66b48..a309560af38 100644 --- a/src/proof/proof_rule_checker.h +++ b/src/proof/proof_rule_checker.h @@ -63,7 +63,7 @@ class ProofRuleChecker /** get a Kind from a node, return false if we fail */ static bool getKind(TNode n, Kind& k); /** Make a Kind into a node */ - static Node mkKindNode(Kind k); + static Node mkKindNode(NodeManager* nm, Kind k); /** Register all rules owned by this rule checker into pc. */ virtual void registerTo(ProofChecker* pc) {} diff --git a/src/proof/proof_step_buffer.cpp b/src/proof/proof_step_buffer.cpp index 4d48a6b42d8..5cb64ba89c8 100644 --- a/src/proof/proof_step_buffer.cpp +++ b/src/proof/proof_step_buffer.cpp @@ -126,7 +126,7 @@ bool ProofStepBuffer::addTrustedStep(TrustId id, Node conc) { std::vector sargs; - sargs.push_back(mkTrustId(id)); + sargs.push_back(mkTrustId(NodeManager::currentNM(), id)); sargs.push_back(conc); sargs.insert(sargs.end(), args.begin(), args.end()); return addStep(ProofRule::TRUST, children, sargs, conc); diff --git a/src/proof/resolution_proofs_util.cpp b/src/proof/resolution_proofs_util.cpp index 3dc79621db3..2b664fb9118 100644 --- a/src/proof/resolution_proofs_util.cpp +++ b/src/proof/resolution_proofs_util.cpp @@ -64,7 +64,8 @@ std::ostream& operator<<(std::ostream& out, CrowdingLitInfo info) return out; } -Node eliminateCrowdingLits(bool reorderPremises, +Node eliminateCrowdingLits(NodeManager* nm, + bool reorderPremises, const std::vector& clauseLits, const std::vector& targetClauseLits, const std::vector& children, @@ -76,7 +77,6 @@ Node eliminateCrowdingLits(bool reorderPremises, Trace("crowding-lits") << "Clause lits: " << clauseLits << "\n"; Trace("crowding-lits") << "Target lits: " << targetClauseLits << "\n\n"; std::vector newChildren{children}, newArgs{args}; - NodeManager* nm = NodeManager::currentNM(); Node trueNode = nm->mkConst(true); // get crowding lits and the position of the last clause that includes // them. The factoring step must be added after the last inclusion and before diff --git a/src/proof/resolution_proofs_util.h b/src/proof/resolution_proofs_util.h index ce239f780ca..42c2249d1c6 100644 --- a/src/proof/resolution_proofs_util.h +++ b/src/proof/resolution_proofs_util.h @@ -107,7 +107,8 @@ namespace proof { * @return The resulting node of transforming MACRO_RESOLUTION into * CHAIN_RESOLUTION according to the above idea. */ -Node eliminateCrowdingLits(bool reorderPremises, +Node eliminateCrowdingLits(NodeManager* nm, + bool reorderPremises, const std::vector& clauseLits, const std::vector& targetClauseLits, const std::vector& children, diff --git a/src/proof/rewrite_proof_generator.cpp b/src/proof/rewrite_proof_generator.cpp index 5b885edff43..069319d8c7a 100644 --- a/src/proof/rewrite_proof_generator.cpp +++ b/src/proof/rewrite_proof_generator.cpp @@ -24,7 +24,11 @@ RewriteProofGenerator::RewriteProofGenerator(Env& env, MethodId id) : EnvObj(env), ProofGenerator(), d_id(id) { // initialize the proof args - addMethodIds(d_pargs, MethodId::SB_DEFAULT, MethodId::SBA_SEQUENTIAL, d_id); + addMethodIds(nodeManager(), + d_pargs, + MethodId::SB_DEFAULT, + MethodId::SBA_SEQUENTIAL, + d_id); } RewriteProofGenerator::~RewriteProofGenerator() {} diff --git a/src/proof/subtype_elim_proof_converter.cpp b/src/proof/subtype_elim_proof_converter.cpp index 3f892ce485b..77f23637b85 100644 --- a/src/proof/subtype_elim_proof_converter.cpp +++ b/src/proof/subtype_elim_proof_converter.cpp @@ -254,7 +254,7 @@ bool SubtypeElimConverterCallback::prove(const Node& src, Node csrc = nm->mkNode(src.getKind(), conv[0], conv[1]); if (tgt.getKind() == Kind::EQUAL) { - Node nk = ProofRuleChecker::mkKindNode(Kind::TO_REAL); + Node nk = ProofRuleChecker::mkKindNode(nm, Kind::TO_REAL); cdp->addStep(csrc, ProofRule::CONG, {src}, {nk}); Trace("pf-subtype-elim") << "...via " << csrc << std::endl; if (csrc != tgt) @@ -295,7 +295,7 @@ bool SubtypeElimConverterCallback::prove(const Node& src, if (csrc != tgt) { Node congEq = csrc.eqNode(tgt); - Node nk = ProofRuleChecker::mkKindNode(csrc.getKind()); + Node nk = ProofRuleChecker::mkKindNode(nm, csrc.getKind()); cdp->addStep(congEq, ProofRule::CONG, {convEq[0], convEq[1]}, {nk}); cdp->addStep(fullEq, ProofRule::TRANS, {rewriteEq, congEq}, {}); } diff --git a/src/proof/theory_proof_step_buffer.cpp b/src/proof/theory_proof_step_buffer.cpp index 0a9f361d81a..c6a225034b9 100644 --- a/src/proof/theory_proof_step_buffer.cpp +++ b/src/proof/theory_proof_step_buffer.cpp @@ -38,7 +38,7 @@ bool TheoryProofStepBuffer::applyEqIntro(Node src, { std::vector args; args.push_back(src); - addMethodIds(args, ids, ida, idr); + addMethodIds(NodeManager::currentNM(), args, ids, ida, idr); bool added; Node expected = src.eqNode(tgt); Node res = tryStep(added, @@ -84,7 +84,7 @@ bool TheoryProofStepBuffer::applyPredTransform(Node src, // try to prove that tgt rewrites to src children.insert(children.end(), exp.begin(), exp.end()); args.push_back(tgt); - addMethodIds(args, ids, ida, idr); + addMethodIds(NodeManager::currentNM(), args, ids, ida, idr); Node res = tryStep(ProofRule::MACRO_SR_PRED_TRANSFORM, children, args, @@ -108,7 +108,7 @@ bool TheoryProofStepBuffer::applyPredIntro(Node tgt, { std::vector args; args.push_back(tgt); - addMethodIds(args, ids, ida, idr); + addMethodIds(NodeManager::currentNM(), args, ids, ida, idr); Node res = tryStep(ProofRule::MACRO_SR_PRED_INTRO, exp, args, @@ -131,7 +131,7 @@ Node TheoryProofStepBuffer::applyPredElim(Node src, children.push_back(src); children.insert(children.end(), exp.begin(), exp.end()); std::vector args; - addMethodIds(args, ids, ida, idr); + addMethodIds(NodeManager::currentNM(), args, ids, ida, idr); bool added; Node srcRew = tryStep(added, ProofRule::MACRO_SR_PRED_ELIM, children, args); if (d_autoSym && added && CDProof::isSame(src, srcRew)) @@ -198,7 +198,7 @@ Node TheoryProofStepBuffer::factorReorderElimDoubleNeg(Node n) Node congEq = oldn.eqNode(n); addStep(ProofRule::NARY_CONG, childrenEqs, - {ProofRuleChecker::mkKindNode(Kind::OR)}, + {ProofRuleChecker::mkKindNode(nm, Kind::OR)}, congEq); // add an equality resolution step to derive normalize clause addStep(ProofRule::EQ_RESOLVE, {oldn, congEq}, {}, n); diff --git a/src/proof/trust_id.cpp b/src/proof/trust_id.cpp index ddefef08d74..53212222fae 100644 --- a/src/proof/trust_id.cpp +++ b/src/proof/trust_id.cpp @@ -114,10 +114,9 @@ std::ostream& operator<<(std::ostream& out, TrustId id) return out; } -Node mkTrustId(TrustId id) +Node mkTrustId(NodeManager* nm, TrustId id) { - return NodeManager::currentNM()->mkConstInt( - Rational(static_cast(id))); + return nm->mkConstInt(Rational(static_cast(id))); } bool getTrustId(TNode n, TrustId& i) diff --git a/src/proof/trust_id.h b/src/proof/trust_id.h index 4763a85c4d4..fa82104a0ea 100644 --- a/src/proof/trust_id.h +++ b/src/proof/trust_id.h @@ -207,7 +207,7 @@ const char* toString(TrustId id); /** Write a trust id to out */ std::ostream& operator<<(std::ostream& out, TrustId id); /** Make a trust id node */ -Node mkTrustId(TrustId id); +Node mkTrustId(NodeManager* nm, TrustId id); /** get a trust identifier from a node, return false if we fail */ bool getTrustId(TNode n, TrustId& i); diff --git a/src/rewriter/basic_rewrite_rcons.cpp b/src/rewriter/basic_rewrite_rcons.cpp index 23611a34219..90fc478c348 100644 --- a/src/rewriter/basic_rewrite_rcons.cpp +++ b/src/rewriter/basic_rewrite_rcons.cpp @@ -1221,7 +1221,7 @@ bool BasicRewriteRCons::ensureProofArithPolyNormRel(CDProof* cdp, Trace("brc-macro") << "...fail premise" << std::endl; return false; } - Node kn = ProofRuleChecker::mkKindNode(eq[0].getKind()); + Node kn = ProofRuleChecker::mkKindNode(nodeManager(), eq[0].getKind()); if (!cdp->addStep(eq, ProofRule::ARITH_POLY_NORM_REL, {premise}, {kn})) { Trace("brc-macro") << "...fail application" << std::endl; diff --git a/src/rewriter/rewrite_db_proof_cons.cpp b/src/rewriter/rewrite_db_proof_cons.cpp index c70456290c3..726e6970884 100644 --- a/src/rewriter/rewrite_db_proof_cons.cpp +++ b/src/rewriter/rewrite_db_proof_cons.cpp @@ -1217,7 +1217,7 @@ bool RewriteDbProofCons::ensureProofInternal( cdp->addStep(cur, ProofRule::ARITH_POLY_NORM_REL, {pcur.d_vars[0]}, - {ProofRuleChecker::mkKindNode(cur[0].getKind())}); + {ProofRuleChecker::mkKindNode(nm, cur[0].getKind())}); } } else if (pcur.d_id == RewriteProofStatus::DSL diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 3b2d1f2291a..168abd5ceaa 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -580,7 +580,8 @@ Node ProofPostprocessCallback::expandMacros(ProofRule id, Trace("crowding-lits") << "..premises: " << children << "\n"; Trace("crowding-lits") << "..args: " << args << "\n"; chainConclusion = - proof::eliminateCrowdingLits(d_env.getOptions().proof.optResReconSize, + proof::eliminateCrowdingLits(nm, + d_env.getOptions().proof.optResReconSize, chainConclusionLits, conclusionLits, children, @@ -927,7 +928,7 @@ Node ProofPostprocessCallback::expandMacros(ProofRule id, { // will expand this as a default rewrite if needed Node eqd = retCurr.eqNode(retDef); - Node mid = mkMethodId(midi); + Node mid = mkMethodId(nodeManager(), midi); cdp->addStep(eqd, ProofRule::MACRO_REWRITE, {}, {retCurr, mid}); transEq.push_back(eqd); } diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 4c5a15ce8d9..0e78ce69eda 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -1022,8 +1022,9 @@ Node SolverEngine::findSynth(modes::FindSynthTarget fst, const TypeNode& gtn) } uint64_t nvars = options().quantifiers.sygusRewSynthInputNVars; std::vector asserts = getAssertionsInternal(); - gtnu = preprocessing::passes::SynthRewRulesPass::getGrammarsFrom(asserts, - nvars); + NodeManager* nm = d_env->getNodeManager(); + gtnu = preprocessing::passes::SynthRewRulesPass::getGrammarsFrom( + nm, asserts, nvars); if (gtnu.empty()) { Warning() << "Could not find grammar in find-synth :rewrite_input" diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp index 0298b36e3c4..8481ec76b5c 100644 --- a/src/theory/arrays/inference_manager.cpp +++ b/src/theory/arrays/inference_manager.cpp @@ -127,7 +127,7 @@ void InferenceManager::convert(ProofRule& id, Assert(false) << "Unknown rule " << id << "\n"; } children.push_back(exp); - args.push_back(mkTrustId(TrustId::THEORY_INFERENCE)); + args.push_back(mkTrustId(nodeManager(), TrustId::THEORY_INFERENCE)); args.push_back(conc); args.push_back( builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_ARRAYS)); diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp index 0bcd4ef6252..681ea13d341 100644 --- a/src/theory/datatypes/infer_proof_cons.cpp +++ b/src/theory/datatypes/infer_proof_cons.cpp @@ -188,7 +188,7 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof* // s(exp[0]) = s(exp[1]) s(exp[1]) = r // --------------------------------------------------- TRANS // s(exp[0]) = r - Node asn = ProofRuleChecker::mkKindNode(Kind::APPLY_SELECTOR); + Node asn = ProofRuleChecker::mkKindNode(nm, Kind::APPLY_SELECTOR); Node seq = sl.eqNode(sr); cdp->addStep(seq, ProofRule::CONG, {exp}, {asn, sop}); Node sceq = sr.eqNode(concEq[1]); diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index 23a16555461..2376c9965f2 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -310,7 +310,8 @@ TrustNode AlphaEquivalence::reduceQuantifier(Node q) // sret = q std::vector pfArgs2; pfArgs2.push_back(eq2); - addMethodIds(pfArgs2, + addMethodIds(nodeManager(), + pfArgs2, MethodId::SB_DEFAULT, MethodId::SBA_SEQUENTIAL, MethodId::RW_EXT_REWRITE); diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 78fb9b7ad74..82c64731150 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -402,7 +402,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node eq = rewriteStackTop.d_node.eqNode(cached); // we make this a post-rewrite, since we are processing a node that // has finished post-rewriting above - Node trrid = mkTrustId(TrustId::REWRITE_NO_ELABORATE); + Node trrid = mkTrustId(d_nm, TrustId::REWRITE_NO_ELABORATE); tcpg->addRewriteStep(rewriteStackTop.d_node, cached, ProofRule::TRUST, @@ -490,7 +490,8 @@ RewriteResponse Rewriter::processTrustRewriteResponse( { Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId); // add small step trusted rewrite - Node rid = mkMethodId(isPre ? MethodId::RW_REWRITE_THEORY_PRE + Node rid = mkMethodId(d_nm, + isPre ? MethodId::RW_REWRITE_THEORY_PRE : MethodId::RW_REWRITE_THEORY_POST); tcpg->addRewriteStep(proven[0], proven[1], diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index bbe42d6e1ee..7306f00623e 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -58,7 +58,7 @@ TheorySep::TheorySep(Env& env, OutputChannel& out, Valuation valuation) { d_true = nodeManager()->mkConst(true); d_false = nodeManager()->mkConst(false); - d_tiid = mkTrustId(TrustId::THEORY_INFERENCE); + d_tiid = mkTrustId(nodeManager(), TrustId::THEORY_INFERENCE); d_tsid = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_SEP); // indicate we are using the default theory state object diff --git a/src/theory/sets/inference_manager.cpp b/src/theory/sets/inference_manager.cpp index cbdbae13631..49cbdf41f59 100644 --- a/src/theory/sets/inference_manager.cpp +++ b/src/theory/sets/inference_manager.cpp @@ -37,7 +37,7 @@ InferenceManager::InferenceManager(Env& env, { d_true = nodeManager()->mkConst(true); d_false = nodeManager()->mkConst(false); - d_tid = mkTrustId(TrustId::THEORY_INFERENCE); + d_tid = mkTrustId(nodeManager(), TrustId::THEORY_INFERENCE); d_tsid = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_SETS); } diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index 3220b2be185..b3aa955c463 100644 --- a/src/theory/strings/infer_proof_cons.cpp +++ b/src/theory/strings/infer_proof_cons.cpp @@ -485,7 +485,8 @@ void InferProofCons::convert(InferenceId infer, // above. Notice we need both in sequence since ext equality rewriting // is not recursive. std::vector argsERew; - addMethodIds(argsERew, + addMethodIds(nm, + argsERew, MethodId::SB_DEFAULT, MethodId::SBA_SEQUENTIAL, MethodId::RW_REWRITE_EQ_EXT); @@ -1125,7 +1126,7 @@ void InferProofCons::convert(InferenceId infer, // untrustworthy conversion, the argument of THEORY_INFERENCE is its // conclusion ps.d_args.clear(); - ps.d_args.push_back(mkTrustId(TrustId::THEORY_INFERENCE)); + ps.d_args.push_back(mkTrustId(nm, TrustId::THEORY_INFERENCE)); ps.d_args.push_back(conc); Node t = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_STRINGS); ps.d_args.push_back(t); diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp index f25f219b871..5ebca4fe79d 100644 --- a/src/theory/theory_preprocessor.cpp +++ b/src/theory/theory_preprocessor.cpp @@ -67,7 +67,7 @@ TheoryPreprocessor::TheoryPreprocessor(Env& env, TheoryEngine& engine) ts.push_back(d_tpg.get()); d_tspg.reset(new TConvSeqProofGenerator( pnm, ts, userContext(), "TheoryPreprocessor::sequence")); - d_tpid = mkTrustId(TrustId::THEORY_PREPROCESS); + d_tpid = mkTrustId(nodeManager(), TrustId::THEORY_PREPROCESS); } } diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp index c7db8551d36..012bbfa5944 100644 --- a/src/theory/uf/eq_proof.cpp +++ b/src/theory/uf/eq_proof.cpp @@ -481,7 +481,7 @@ bool EqProof::expandTransitivityForDisequalities( p->addStep(congConclusion, ProofRule::CONG, substPremises, - {ProofRuleChecker::mkKindNode(Kind::EQUAL)}, + {ProofRuleChecker::mkKindNode(nm, Kind::EQUAL)}, true); Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: via " "congruence derived " @@ -609,10 +609,11 @@ bool EqProof::expandTransitivityForTheoryDisequalities( << "EqProof::expandTransitivityForTheoryDisequalities: adding " << ProofRule::CONG << " step for " << congConclusion << " from " << subChildren << "\n"; + NodeManager* nm = NodeManager::currentNM(); p->addStep(congConclusion, ProofRule::CONG, {subChildren}, - {ProofRuleChecker::mkKindNode(Kind::EQUAL)}, + {ProofRuleChecker::mkKindNode(nm, Kind::EQUAL)}, true); Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: via " "congruence derived " @@ -1465,7 +1466,7 @@ Node EqProof::addToProof(CDProof* p, p->addStep(conclusion, ProofRule::HO_CONG, children, - {ProofRuleChecker::mkKindNode(Kind::APPLY_UF)}, + {ProofRuleChecker::mkKindNode(nm, Kind::APPLY_UF)}, true); } // If the conclusion of the congruence step changed due to the n-ary handling,