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/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/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/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/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/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/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/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/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/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/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/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/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/proof/alf/alf_printer.cpp b/src/proof/alf/alf_printer.cpp index 9c2207c1df4..151873738c4 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(); @@ -270,12 +264,16 @@ 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: 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: @@ -283,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/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/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 df7c4ebe96d..90fc478c348 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) { @@ -1086,7 +1179,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); @@ -1120,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/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/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/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/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/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/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/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/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/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/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..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); @@ -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/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/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/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/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/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/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/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/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; diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp index 450d8526163..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); @@ -1298,14 +1299,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 +1447,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))); 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, diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 0fc1707f39f..4fb25d98874 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 @@ -1334,6 +1335,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 @@ -1358,6 +1360,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 @@ -1457,6 +1460,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 +2922,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/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/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) 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) 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) 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) + 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) 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 == "":