diff --git a/include/cvc5/cvc5_proof_rule.h b/include/cvc5/cvc5_proof_rule.h index 029ba64c68e..319ccff2acf 100644 --- a/include/cvc5/cvc5_proof_rule.h +++ b/include/cvc5/cvc5_proof_rule.h @@ -2498,6 +2498,33 @@ enum ENUM(ProofRewriteRule) * \endverbatim */ EVALUE(ARRAYS_SELECT_CONST), + /** + * \verbatim embed:rst:leading-asterisk + * **Arrays -- Macro distinct arrays** + * + * .. math:: + * (A = B) = \bot + * + * where :math:`A` and :math:`B` are distinct array values, that is, + * the Node::isConst method returns true for both. + * + * \endverbatim + */ + EVALUE(MACRO_ARRAYS_DISTINCT_ARRAYS), + /** + * \verbatim embed:rst:leading-asterisk + * **Arrays -- Macro normalize constant** + * + * .. math:: + * A = B + * + * where :math:`B` is the result of normalizing the array value :math:`A` + * into a canonical form, using the internal method + * TheoryArraysRewriter::normalizeConstant. + * + * \endverbatim + */ + EVALUE(MACRO_ARRAYS_NORMALIZE_CONSTANT), /** * \verbatim embed:rst:leading-asterisk * **Arrays -- Expansion of array range equality** @@ -2576,14 +2603,19 @@ enum ENUM(ProofRewriteRule) * G_1 \wedge \cdots \wedge G_n * * where each :math:`G_i` is semantically equivalent to - * :math:`\forall X.\> F_i`. + * :math:`\forall X.\> F_i`, or alternatively + * + * .. math:: + * \forall X.\> \ite{C}{F_1}{F_2} = \ite{C}{G_1}{G_2} + * + * where :math:`C` does not have any free variable in :math:`X`. * * \endverbatim */ EVALUE(MACRO_QUANT_MINISCOPE), /** * \verbatim embed:rst:leading-asterisk - * **Quantifiers -- Miniscoping** + * **Quantifiers -- Miniscoping and** * * .. math:: * \forall X.\> F_1 \wedge \ldots \wedge F_n = @@ -2591,10 +2623,10 @@ enum ENUM(ProofRewriteRule) * * \endverbatim */ - EVALUE(QUANT_MINISCOPE), + EVALUE(QUANT_MINISCOPE_AND), /** * \verbatim embed:rst:leading-asterisk - * **Quantifiers -- Miniscoping free variables** + * **Quantifiers -- Miniscoping or** * * .. math:: * \forall X.\> F_1 \vee \ldots \vee F_n = (\forall X_1.\> F_1) \vee \ldots \vee (\forall X_n.\> F_n) @@ -2604,7 +2636,19 @@ enum ENUM(ProofRewriteRule) * * \endverbatim */ - EVALUE(QUANT_MINISCOPE_FV), + EVALUE(QUANT_MINISCOPE_OR), + /** + * \verbatim embed:rst:leading-asterisk + * **Quantifiers -- Miniscoping ite** + * + * .. math:: + * \forall X.\> \ite{C}{F_1}{F_2} = \ite{C}{\forall X.\> F_1}{\forall X.\> F_2} + * + * where :math:`C` does not have any free variable in :math:`X`. + * + * \endverbatim + */ + EVALUE(QUANT_MINISCOPE_ITE), /** * \verbatim embed:rst:leading-asterisk * **Quantifiers -- Datatypes Split** @@ -3618,6 +3662,10 @@ enum ENUM(ProofRewriteRule) EVALUE(SETS_CARD_MINUS), /** Auto-generated from RARE rule sets-card-emp */ EVALUE(SETS_CARD_EMP), + /** Auto-generated from RARE rule sets-minus-self */ + EVALUE(SETS_MINUS_SELF), + /** Auto-generated from RARE rule sets-is-empty-elim */ + EVALUE(SETS_IS_EMPTY_ELIM), /** Auto-generated from RARE rule str-eq-ctn-false */ EVALUE(STR_EQ_CTN_FALSE), /** Auto-generated from RARE rule str-eq-ctn-full-false1 */ @@ -3708,8 +3756,6 @@ enum ENUM(ProofRewriteRule) EVALUE(STR_CONTAINS_EMP), /** Auto-generated from RARE rule str-contains-is-emp */ EVALUE(STR_CONTAINS_IS_EMP), - /** Auto-generated from RARE rule str-concat-emp */ - EVALUE(STR_CONCAT_EMP), /** Auto-generated from RARE rule str-at-elim */ EVALUE(STR_AT_ELIM), /** Auto-generated from RARE rule str-replace-self */ @@ -3826,6 +3872,8 @@ enum ENUM(ProofRewriteRule) EVALUE(SEQ_NTH_UNIT), /** Auto-generated from RARE rule seq-rev-unit */ EVALUE(SEQ_REV_UNIT), + /** Auto-generated from RARE rule seq-len-empty */ + EVALUE(SEQ_LEN_EMPTY), /** Auto-generated from RARE rule re-in-empty */ EVALUE(RE_IN_EMPTY), /** Auto-generated from RARE rule re-in-sigma */ diff --git a/proofs/eo/cpc/Cpc.eo b/proofs/eo/cpc/Cpc.eo index f2f6ba96f02..a132b43513f 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/Strings.eo b/proofs/eo/cpc/programs/Strings.eo index 4fb69684937..a9143e6aa50 100644 --- a/proofs/eo/cpc/programs/Strings.eo +++ b/proofs/eo/cpc/programs/Strings.eo @@ -16,7 +16,7 @@ (program $str_is_empty ((U Type) (x U)) (U) Bool ( - (($str_is_empty (seq.empty U)) true) + (($str_is_empty (@seq.empty U)) true) (($str_is_empty "") true) (($str_is_empty x) false) ) 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/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 004a69e55c6..23f35f021a6 100644 --- a/proofs/eo/cpc/rules/Quantifiers.eo +++ b/proofs/eo/cpc/rules/Quantifiers.eo @@ -192,74 +192,90 @@ :conclusion (= (Q x F) G) ) -;;;;; ProofRewriteRule::QUANT_MINISCOPE +;;;;; ProofRewriteRule::QUANT_MINISCOPE_AND -; program: $mk_quant_miniscope +; program: $mk_quant_miniscope_and ; args: ; - x @List: The list of variables of the formula. ; - F Bool: The body of the formula in question. ; return: The result of miniscoping (forall x F) based on conjunctions. -(program $mk_quant_miniscope ((x @List) (f Bool) (fs Bool :list)) +(program $mk_quant_miniscope_and ((x @List) (f Bool) (fs Bool :list)) (@List Bool) Bool ( - (($mk_quant_miniscope x (and f fs)) (eo::cons and (forall x f) ($mk_quant_miniscope x fs))) - (($mk_quant_miniscope x true) true) + (($mk_quant_miniscope_and x (and f fs)) (eo::cons and (forall x f) ($mk_quant_miniscope_and x fs))) + (($mk_quant_miniscope_and x true) true) ) ) -; rule: quant-miniscope -; implements: ProofRewriteRule::QUANT_MINISCOPE +; rule: quant-miniscope-and +; implements: ProofRewriteRule::QUANT_MINISCOPE_AND ; args: ; - eq Bool: The equality whose left hand side is a quantified formula. ; requires: > ; The right hand side of the equality is the result of miniscoping the ; left hand side. ; conclusion: The given equality. -(declare-rule quant-miniscope ((x @List) (F Bool) (G Bool)) +(declare-rule quant-miniscope-and ((x @List) (F Bool) (G Bool)) :args ((= (forall x F) G)) - :requires ((($mk_quant_miniscope x F) G)) + :requires ((($mk_quant_miniscope_and x F) G)) :conclusion (= (forall x F) G) ) -;;;;; ProofRewriteRule::QUANT_MINISCOPE_FV +;;;;; ProofRewriteRule::QUANT_MINISCOPE_OR -; program: $is_quant_miniscope_fv +; program: $is_quant_miniscope_or ; args: ; - x @List: The list of variables of the first formula we have yet to process ; - F Bool: The body of the first formula in question. ; - G Bool: The second formula in question. ; return: > ; True if (forall x F) is equivalent to G based on miniscope reasoning with -; free variables. -(program $is_quant_miniscope_fv ((x @List) (xs @List :list) (ys @List :list) (f Bool) (fs Bool :list) (g Bool) (gs Bool :list)) +; free variables over OR. +(program $is_quant_miniscope_or ((x @List) (xs @List :list) (ys @List :list) (f Bool) (fs Bool :list) (g Bool) (gs Bool :list)) (@List Bool Bool) Bool ( - (($is_quant_miniscope_fv x (or f fs) (or f gs)) (eo::requires ($contains_subterm_list f x) false - ($is_quant_miniscope_fv x fs gs))) - (($is_quant_miniscope_fv x (or f fs) (or (forall @list.nil f) gs)) (eo::requires ($contains_subterm_list f x) false - ($is_quant_miniscope_fv x fs gs))) - (($is_quant_miniscope_fv (@list x xs) (or f fs) (or (forall (@list x ys) f) gs)) + (($is_quant_miniscope_or x (or f fs) (or f gs)) (eo::requires ($contains_subterm_list f x) false + ($is_quant_miniscope_or x fs gs))) + (($is_quant_miniscope_or x (or f fs) (or (forall @list.nil f) gs)) (eo::requires ($contains_subterm_list f x) false + ($is_quant_miniscope_or x fs gs))) + (($is_quant_miniscope_or (@list x xs) (or f fs) (or (forall (@list x ys) f) gs)) (eo::requires ($contains_subterm gs x) false - ($is_quant_miniscope_fv xs (or f fs) (or (forall ys f) gs)))) - (($is_quant_miniscope_fv @list.nil false false) true) - (($is_quant_miniscope_fv x f g) false) + ($is_quant_miniscope_or xs (or f fs) (or (forall ys f) gs)))) + (($is_quant_miniscope_or @list.nil false false) true) + (($is_quant_miniscope_or x f g) false) ) ) -; rule: quant-miniscope-fv -; implements: ProofRewriteRule::QUANT_MINISCOPE_FV +; rule: quant-miniscope-or +; implements: ProofRewriteRule::QUANT_MINISCOPE_OR ; args: ; - eq Bool: The equality whose left hand side is a quantified formula. ; requires: > ; The right hand side of the equality can be shown equivalent to the right ; hand side based on reasoning about the disjuncts of F that contain x. ; conclusion: The given equality. -(declare-rule quant-miniscope-fv ((x @List) (F Bool) (G Bool)) +(declare-rule quant-miniscope-or ((x @List) (F Bool) (G Bool)) :args ((= (forall x F) G)) - :requires ((($is_quant_miniscope_fv x F G) true)) + :requires ((($is_quant_miniscope_or x F G) true)) :conclusion (= (forall x F) G) ) +;;;;; ProofRewriteRule::QUANT_MINISCOPE_ITE + +; rule: quant-miniscope-ite +; implements: ProofRewriteRule::QUANT_MINISCOPE_ITE +; args: +; - eq Bool: The equality whose left hand side is a quantified formula. +; requires: > +; The right hand side of the equality is the result of miniscoping the +; left hand side. +; conclusion: The given equality. +(declare-rule quant-miniscope-ite ((x @List) (A Bool) (F1 Bool) (F2 Bool) (G Bool)) + :args ((= (forall x (ite A F1 F2)) (ite A (forall x F1) (forall x F2)))) + :requires ((($contains_subterm_list A x) false)) + :conclusion (= (forall x (ite A F1 F2)) (ite A (forall x F1) (forall x F2))) +) + ;;;;; ProofRewriteRule::QUANT_VAR_ELIM_EQ ; define: $mk_quant_var_elim_eq_subs diff --git a/proofs/eo/cpc/rules/Rewrites.eo b/proofs/eo/cpc/rules/Rewrites.eo index 83179849e03..4c4c93f296d 100644 --- a/proofs/eo/cpc/rules/Rewrites.eo +++ b/proofs/eo/cpc/rules/Rewrites.eo @@ -1161,8 +1161,8 @@ :conclusion (= (bvult (@bv c1 nm1) (sign_extend m1 x1)) (= (extract nm2 nm2 x1) (@bv 1 1))) ) (declare-rule sets-eq-singleton-emp ((@T0 Type) (@T1 Type) (x1 (Set @T0)) (y1 @T1)) - :premises ((= (set.is_empty x1) true)) - :args (x1 y1) + :premises ((= x1 (set.empty (Set @T0)))) + :args (x1 y1 (Set @T0)) :conclusion (= (= x1 (set.singleton y1)) false) ) (declare-rule sets-member-singleton ((@T0 Type) (@T1 Type) (x1 @T0) (y1 @T1)) @@ -1170,8 +1170,8 @@ :conclusion (= (set.member x1 (set.singleton y1)) (= x1 y1)) ) (declare-rule sets-member-emp ((@T0 Type) (@T1 Type) (x1 @T0) (y1 (Set @T1))) - :premises ((= (set.is_empty y1) true)) - :args (x1 y1) + :premises ((= y1 (set.empty (Set @T1)))) + :args (x1 y1 (Set @T1)) :conclusion (= (set.member x1 y1) false) ) (declare-rule sets-subset-elim ((@T0 Type) (@T1 Type) (x1 (Set @T0)) (y1 (Set @T1))) @@ -1187,33 +1187,33 @@ :conclusion (= (set.inter x1 y1) (set.inter y1 x1)) ) (declare-rule sets-inter-emp1 ((@T0 Type) (@T1 Type) (x1 (Set @T0)) (y1 (Set @T1))) - :premises ((= (set.is_empty x1) true)) - :args (x1 y1) + :premises ((= x1 (set.empty (Set @T0)))) + :args (x1 y1 (Set @T0)) :conclusion (= (set.inter x1 y1) x1) ) (declare-rule sets-inter-emp2 ((@T0 Type) (@T1 Type) (x1 (Set @T0)) (y1 (Set @T1))) - :premises ((= (set.is_empty y1) true)) - :args (x1 y1) + :premises ((= y1 (set.empty (Set @T1)))) + :args (x1 y1 (Set @T1)) :conclusion (= (set.inter x1 y1) y1) ) (declare-rule sets-minus-emp1 ((@T0 Type) (@T1 Type) (x1 (Set @T0)) (y1 (Set @T1))) - :premises ((= (set.is_empty x1) true)) - :args (x1 y1) + :premises ((= x1 (set.empty (Set @T0)))) + :args (x1 y1 (Set @T0)) :conclusion (= (set.minus x1 y1) x1) ) (declare-rule sets-minus-emp2 ((@T0 Type) (@T1 Type) (x1 (Set @T0)) (y1 (Set @T1))) - :premises ((= (set.is_empty y1) true)) - :args (x1 y1) + :premises ((= y1 (set.empty (Set @T1)))) + :args (x1 y1 (Set @T1)) :conclusion (= (set.minus x1 y1) x1) ) (declare-rule sets-union-emp1 ((@T0 Type) (@T1 Type) (x1 (Set @T0)) (y1 (Set @T1))) - :premises ((= (set.is_empty x1) true)) - :args (x1 y1) + :premises ((= x1 (set.empty (Set @T0)))) + :args (x1 y1 (Set @T0)) :conclusion (= (set.union x1 y1) y1) ) (declare-rule sets-union-emp2 ((@T0 Type) (@T1 Type) (x1 (Set @T0)) (y1 (Set @T1))) - :premises ((= (set.is_empty y1) true)) - :args (x1 y1) + :premises ((= y1 (set.empty (Set @T1)))) + :args (x1 y1 (Set @T1)) :conclusion (= (set.union x1 y1) x1) ) (declare-rule sets-inter-member ((@T0 Type) (@T1 Type) (@T2 Type) (x1 @T0) (y1 (Set @T1)) (z1 (Set @T2))) @@ -1245,10 +1245,18 @@ :conclusion (= (set.card (set.minus s1 t1)) (- (set.card s1) (set.card (set.inter s1 t1)))) ) (declare-rule sets-card-emp ((@T0 Type) (x1 (Set @T0))) - :premises ((= (set.is_empty x1) true)) - :args (x1) + :premises ((= x1 (set.empty (Set @T0)))) + :args (x1 (Set @T0)) :conclusion (= (set.card x1) 0) ) +(declare-rule sets-minus-self ((@T0 Type) (x1 (Set @T0))) + :args (x1 (Set @T0)) + :conclusion (= (set.minus x1 x1) (set.empty (Set @T0))) +) +(declare-rule sets-is-empty-elim ((@T0 Type) (x1 (Set @T0))) + :args (x1 (Set @T0)) + :conclusion (= (set.is_empty x1) (= x1 (set.empty (Set @T0)))) +) (declare-rule str-eq-ctn-false ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (x1 (Seq @T0) :list) (x2 (Seq @T1)) (x3 (Seq @T2) :list) (y1 (Seq @T3))) :premises ((= (seq.contains y1 x2) false)) :args (x1 x2 x3 y1) @@ -1276,29 +1284,30 @@ :args (x1 x2 x3 y1) :conclusion (= (= ($singleton_elim (seq.++ x3 ($singleton_elim (seq.++ x2 x1)))) y1) (= y1 ($singleton_elim (seq.++ x3 x2 x1)))) ) -(declare-rule str-substr-empty-str ((n1 Int) (m1 Int)) - :args (n1 m1) - :conclusion (= (str.substr "" n1 m1) "") +(declare-rule str-substr-empty-str ((@T0 Type) (x1 (Seq @T0)) (n1 Int) (m1 Int)) + :premises ((= x1 (seq.empty (Seq @T0)))) + :args (x1 n1 m1 (Seq @T0)) + :conclusion (= (seq.extract x1 n1 m1) x1) ) -(declare-rule str-substr-empty-range ((x1 String) (n1 Int) (m1 Int)) +(declare-rule str-substr-empty-range ((@T0 Type) (x1 (Seq @T0)) (n1 Int) (m1 Int)) :premises ((= (>= 0 m1) true)) - :args (x1 n1 m1) - :conclusion (= (str.substr x1 n1 m1) "") + :args (x1 n1 m1 (Seq @T0)) + :conclusion (= (seq.extract x1 n1 m1) (seq.empty (Seq @T0))) ) -(declare-rule str-substr-empty-start ((x1 String) (n1 Int) (m1 Int)) - :premises ((= (>= n1 (str.len x1)) true)) - :args (x1 n1 m1) - :conclusion (= (str.substr x1 n1 m1) "") +(declare-rule str-substr-empty-start ((@T0 Type) (x1 (Seq @T0)) (n1 Int) (m1 Int)) + :premises ((= (>= n1 (seq.len x1)) true)) + :args (x1 n1 m1 (Seq @T0)) + :conclusion (= (seq.extract x1 n1 m1) (seq.empty (Seq @T0))) ) -(declare-rule str-substr-empty-start-neg ((x1 String) (n1 Int) (m1 Int)) +(declare-rule str-substr-empty-start-neg ((@T0 Type) (x1 (Seq @T0)) (n1 Int) (m1 Int)) :premises ((= (< n1 0) true)) - :args (x1 n1 m1) - :conclusion (= (str.substr x1 n1 m1) "") + :args (x1 n1 m1 (Seq @T0)) + :conclusion (= (seq.extract x1 n1 m1) (seq.empty (Seq @T0))) ) -(declare-rule str-substr-eq-empty ((s1 String) (n1 Int) (m1 Int)) - :premises ((= n1 0) (= (> m1 n1) true)) - :args (s1 n1 m1) - :conclusion (= (= (str.substr s1 n1 m1) "") (= s1 "")) +(declare-rule str-substr-eq-empty ((@T0 Type) (@T1 Type) (s1 (Seq @T0)) (r1 (Seq @T1)) (n1 Int) (m1 Int)) + :premises ((= n1 0) (= (> m1 n1) true) (= r1 (seq.empty (Seq @T1)))) + :args (s1 r1 n1 m1 (Seq @T1)) + :conclusion (= (= (seq.extract s1 n1 m1) r1) (= s1 r1)) ) (declare-rule str-len-replace-inv ((@T0 Type) (@T1 Type) (@T2 Type) (t1 (Seq @T0)) (s1 (Seq @T1)) (r1 (Seq @T2))) :premises ((= (seq.len s1) (seq.len r1))) @@ -1352,13 +1361,13 @@ :args (s1 s2 s3 t1 t2) :conclusion (= (= (seq.++ s2 s3 s1) (seq.++ t1 t2 s1)) (= ($singleton_elim (seq.++ s2 s3)) ($singleton_elim (seq.++ t1 t2)))) ) -(declare-rule str-concat-unify-base ((s1 String) (t1 String) (t2 String :list)) - :args (s1 t1 t2) - :conclusion (= (= s1 (str.++ s1 t1 t2)) (= "" ($singleton_elim (str.++ t1 t2)))) +(declare-rule str-concat-unify-base ((@T0 Type) (@T1 Type) (@T2 Type) (s1 (Seq @T0)) (t1 (Seq @T1)) (t2 (Seq @T2) :list)) + :args (s1 t1 t2 (Seq @T0)) + :conclusion (= (= s1 (seq.++ s1 t1 t2)) (= (seq.empty (Seq @T0)) ($singleton_elim (seq.++ t1 t2)))) ) -(declare-rule str-concat-unify-base-rev ((s1 String) (t1 String) (t2 String :list)) - :args (s1 t1 t2) - :conclusion (= (= s1 (str.++ t1 t2 s1)) (= "" ($singleton_elim (str.++ t1 t2)))) +(declare-rule str-concat-unify-base-rev ((@T0 Type) (@T1 Type) (@T2 Type) (s1 (Seq @T0)) (t1 (Seq @T1)) (t2 (Seq @T2) :list)) + :args (s1 t1 t2 (Seq @T0)) + :conclusion (= (= s1 (seq.++ t1 t2 s1)) (= (seq.empty (Seq @T0)) ($singleton_elim (seq.++ t1 t2)))) ) (declare-rule str-concat-clash-char ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (@T4 Type) (@T5 Type) (s1 (Seq @T0)) (s2 (Seq @T1) :list) (s3 (Seq @T2) :list) (t1 (Seq @T3)) (t2 (Seq @T4) :list) (t3 (Seq @T5) :list)) :premises ((= (= s1 t1) false) (= (seq.len s1) (seq.len t1))) @@ -1462,10 +1471,6 @@ :args (x1 y1) :conclusion (= (seq.contains x1 y1) (= x1 y1)) ) -(declare-rule str-concat-emp ((xs1 String :list) (ys1 String :list)) - :args (xs1 ys1) - :conclusion (= ($singleton_elim (str.++ xs1 "" ys1)) ($singleton_elim (str.++ xs1 ys1))) -) (declare-rule str-at-elim ((@T0 Type) (x1 (Seq @T0)) (n1 Int)) :args (x1 n1) :conclusion (= (seq.at x1 n1) (seq.extract x1 n1 1)) @@ -1483,9 +1488,10 @@ :args (t1 s1 r1) :conclusion (= (seq.replace t1 s1 r1) t1) ) -(declare-rule str-replace-empty ((@T0 Type) (@T1 Type) (t1 (Seq @T0)) (s1 (Seq @T1))) - :args (t1 s1) - :conclusion (= (seq.replace t1 "" s1) (seq.++ s1 t1)) +(declare-rule str-replace-empty ((@T0 Type) (@T1 Type) (@T2 Type) (t1 (Seq @T0)) (s1 (Seq @T1)) (r1 (Seq @T2))) + :premises ((= r1 (seq.empty (Seq @T2)))) + :args (t1 s1 r1 (Seq @T2)) + :conclusion (= (seq.replace t1 r1 s1) (seq.++ s1 t1)) ) (declare-rule str-replace-contains-pre ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (t1 (Seq @T0)) (t2 (Seq @T1) :list) (s1 (Seq @T2)) (r1 (Seq @T3))) :premises ((= (seq.contains t1 s1) true)) @@ -1509,9 +1515,9 @@ :args (s1 s2 s3) :conclusion (= (seq.len (seq.++ s1 s2 s3)) (+ (seq.len s1) (seq.len ($singleton_elim (seq.++ s2 s3))))) ) -(declare-rule str-indexof-self ((t1 String) (n1 Int)) - :args (t1 n1) - :conclusion (= (str.indexof t1 t1 n1) (str.indexof "" "" n1)) +(declare-rule str-indexof-self ((@T0 Type) (t1 (Seq @T0)) (n1 Int)) + :args (t1 n1 (Seq @T0)) + :conclusion (= (seq.indexof t1 t1 n1) (eo::define ((_let_1 (seq.empty (Seq @T0)))) (seq.indexof _let_1 _let_1 n1))) ) (declare-rule str-indexof-no-contains ((@T0 Type) (@T1 Type) (t1 (Seq @T0)) (s1 (Seq @T1)) (n1 Int)) :premises ((= (seq.contains (seq.extract t1 n1 (seq.len t1)) s1) false)) @@ -1712,6 +1718,11 @@ :args (x1) :conclusion (= (seq.rev (seq.unit x1)) (seq.unit x1)) ) +(declare-rule seq-len-empty ((@T0 Type) (x1 (Seq @T0))) + :premises ((= x1 (seq.empty (Seq @T0)))) + :args (x1 (Seq @T0)) + :conclusion (= (seq.len x1) 0) +) (declare-rule re-in-empty ((t1 String)) :args (t1) :conclusion (= (str.in_re t1 re.none) false) 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/proofs/eo/cpc/theories/Strings.eo b/proofs/eo/cpc/theories/Strings.eo index 444e5e6bb54..6a6bb8774b1 100644 --- a/proofs/eo/cpc/theories/Strings.eo +++ b/proofs/eo/cpc/theories/Strings.eo @@ -32,21 +32,38 @@ (declare-consts String) ; Empty sequence -; disclaimer: This function is not in SMT-LIB. -(declare-const seq.empty (-> (! Type :var T) T)) - -; program: $mk_emptystr +; note: > +; This symbol is used as the term denoting the empty sequence. +; This is not the same as seq.empty, which is defined as the +; (user-facing) constructor of the empty string or sequence, +; defined as seq.empty below. It is never used for strings. +(declare-const @seq.empty (-> (! Type :var T) T)) + +; program: seq.empty ; args: ; - T Type: The string-like type. ; return: The empty string of the given string-like type T. -(program $mk_emptystr ((U Type)) +; note: > +; We define seq.empty in this way since the same symbols in our theory +; are used for strings and sequences, yet for the purposes of +; e.g. evaluation, strings require using string literals as their +; values. In places where seq.empty can be used for a string or +; sequence (e.g., RARE), we use this program to ensure this is the case. +; disclaimer: This function is not in SMT-LIB. +(program seq.empty ((U Type)) (Type) (Seq U) ( - (($mk_emptystr String) "") - (($mk_emptystr (Seq U)) (seq.empty (Seq U))) + ((seq.empty String) "") + ((seq.empty (Seq U)) (@seq.empty (Seq U))) ) ) +; define: $mk_emptystr +; note: > +; This is used as a macro for constructing the empty string or sequence. +; It is equivalent to seq.empty above. +(define $mk_emptystr () seq.empty) + ; Core functions of strings. (declare-const str.len (-> (! Type :var T :implicit) @@ -57,7 +74,7 @@ ; declare it to be :right-assoc-nil to model cvc5's treatment of variadic ; functions. (declare-parameterized-const str.++ ((T Type)) - (-> (Seq T) (Seq T) (Seq T)) :right-assoc-nil ($mk_emptystr (Seq T))) + (-> (Seq T) (Seq T) (Seq T)) :right-assoc-nil (seq.empty (Seq T))) ; Extended functions for strings. (declare-const str.substr (-> (! Type :var T :implicit) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 9679a76d6b4..c56a74fa81e 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1263,6 +1263,8 @@ libcvc5_add_sources( theory/uf/cardinality_extension.h theory/uf/conversions_solver.cpp theory/uf/conversions_solver.h + theory/uf/diamonds_proof_generator.cpp + theory/uf/diamonds_proof_generator.h theory/uf/equality_engine.cpp theory/uf/equality_engine.h theory/uf/equality_engine_iterator.cpp diff --git a/src/api/cpp/cvc5_proof_rule_template.cpp b/src/api/cpp/cvc5_proof_rule_template.cpp index 3a5ec87a380..943d97d788c 100644 --- a/src/api/cpp/cvc5_proof_rule_template.cpp +++ b/src/api/cpp/cvc5_proof_rule_template.cpp @@ -237,6 +237,10 @@ const char* toString(cvc5::ProofRewriteRule rule) case ProofRewriteRule::BETA_REDUCE: return "beta-reduce"; case ProofRewriteRule::LAMBDA_ELIM: return "lambda-elim"; case ProofRewriteRule::ARRAYS_SELECT_CONST: return "arrays-select-const"; + case ProofRewriteRule::MACRO_ARRAYS_DISTINCT_ARRAYS: + return "macro-arrays-distinct-arrays"; + case ProofRewriteRule::MACRO_ARRAYS_NORMALIZE_CONSTANT: + return "macro-arrays-normalize-constant"; case ProofRewriteRule::ARRAYS_EQ_RANGE_EXPAND: return "arrays-eq-range-expand"; case ProofRewriteRule::EXISTS_ELIM: return "exists-elim"; @@ -247,8 +251,9 @@ const char* toString(cvc5::ProofRewriteRule rule) case ProofRewriteRule::MACRO_QUANT_PRENEX: return "macro-quant-prenex"; case ProofRewriteRule::MACRO_QUANT_MINISCOPE: return "macro-quant-miniscope"; - case ProofRewriteRule::QUANT_MINISCOPE: return "quant-miniscope"; - case ProofRewriteRule::QUANT_MINISCOPE_FV: return "quant-miniscope-fv"; + case ProofRewriteRule::QUANT_MINISCOPE_AND: return "quant-miniscope-and"; + case ProofRewriteRule::QUANT_MINISCOPE_OR: return "quant-miniscope-or"; + case ProofRewriteRule::QUANT_MINISCOPE_ITE: return "quant-miniscope-ite"; case ProofRewriteRule::QUANT_DT_SPLIT: return "quant-dt-split"; case ProofRewriteRule::MACRO_QUANT_PARTITION_CONNECTED_FV: return "macro-quant-partition-connected-fv"; diff --git a/src/expr/nary_term_util.cpp b/src/expr/nary_term_util.cpp index 102adc29df3..242726219d3 100644 --- a/src/expr/nary_term_util.cpp +++ b/src/expr/nary_term_util.cpp @@ -17,7 +17,9 @@ #include "expr/aci_norm.h" #include "expr/attribute.h" +#include "expr/emptyset.h" #include "expr/node_algorithm.h" +#include "expr/sort_to_term.h" #include "theory/bv/theory_bv_utils.h" #include "theory/strings/word.h" #include "util/bitvector.h" @@ -221,7 +223,40 @@ Node narySubstitute(Node src, { children.insert(children.begin(), cur.getOperator()); } - ret = nm->mkNode(cur.getKind(), children); + Kind k = cur.getKind(); + // We treat @set.empty_of_type, @seq.empty_of_type, @type_of as + // macros in this method, meaning they are immediately evaluated + // as soon as RARE rules are instantiated. + switch (k) + { + case Kind::SET_EMPTY_OF_TYPE: + case Kind::SEQ_EMPTY_OF_TYPE: + { + if (children[0].getKind() == Kind::SORT_TO_TERM) + { + const SortToTerm& st = children[0].getConst(); + TypeNode tn = st.getType(); + if (k == Kind::SET_EMPTY_OF_TYPE) + { + ret = nm->mkConst(EmptySet(tn)); + } + else + { + Assert(k == Kind::SEQ_EMPTY_OF_TYPE); + ret = theory::strings::Word::mkEmptyWord(tn); + } + } + else + { + ret = nm->mkNode(k, children); + } + } + break; + case Kind::TYPE_OF: + ret = nm->mkConst(SortToTerm(children[0].getType())); + break; + default: ret = nm->mkNode(k, children); break; + } } } visited[cur] = ret; diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp index 934d3992050..ed1f5cdcc98 100644 --- a/src/expr/node_manager_template.cpp +++ b/src/expr/node_manager_template.cpp @@ -1134,7 +1134,7 @@ Node NodeManager::getBoundVarListForFunctionType(TypeNode tn) { vars.push_back(mkBoundVar(tn[i])); } - bvl = mkNode(Kind::BOUND_VAR_LIST, vars); + bvl = tn.getNodeManager()->mkNode(Kind::BOUND_VAR_LIST, vars); Trace("functions") << "Make standard bound var list " << bvl << " for " << tn << std::endl; tn.setAttribute(LambdaBoundVarListAttr(), bvl); diff --git a/src/expr/node_manager_template.h b/src/expr/node_manager_template.h index af70a9f10bf..67b8285a618 100644 --- a/src/expr/node_manager_template.h +++ b/src/expr/node_manager_template.h @@ -140,7 +140,7 @@ class NodeManager const DType& getDTypeFor(Node n) const; /** get the canonical bound variable list for function type tn */ - Node getBoundVarListForFunctionType(TypeNode tn); + static Node getBoundVarListForFunctionType(TypeNode tn); /** * Get the (singleton) operator of an OPERATOR-kinded kind. The @@ -459,7 +459,7 @@ class NodeManager TypeNode mkFiniteFieldType(const Integer& modulus); /** Make the type of arrays with the given parameterization */ - TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType); + static TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType); /** Make the type of set with the given parameterization */ TypeNode mkSetType(TypeNode elementType); @@ -556,20 +556,21 @@ class NodeManager Node mkOr(const std::vector >& children); /** Create a node (with no children) by operator. */ - Node mkNode(TNode opNode); + static Node mkNode(TNode opNode); /** Create a node with one child by operator. */ - Node mkNode(TNode opNode, TNode child1); + static Node mkNode(TNode opNode, TNode child1); /** Create a node with two children by operator. */ - Node mkNode(TNode opNode, TNode child1, TNode child2); + static Node mkNode(TNode opNode, TNode child1, TNode child2); /** Create a node with three children by operator. */ - Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3); + static Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3); /** Create a node by applying an operator to the children. */ template - Node mkNode(TNode opNode, const std::vector >& children); + static Node mkNode(TNode opNode, + const std::vector>& children); /** * Create a node by applying an operator to an arbitrary number of children. @@ -1095,7 +1096,8 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType, Assert(!constituentType.isNull()) << "unexpected NULL constituent type"; Trace("arrays") << "making array type " << indexType << " " << constituentType << std::endl; - return mkTypeNode(Kind::ARRAY_TYPE, indexType, constituentType); + NodeManager* nm = indexType.getNodeManager(); + return nm->mkTypeNode(Kind::ARRAY_TYPE, indexType, constituentType); } inline TypeNode NodeManager::mkSetType(TypeNode elementType) diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index 1349b10c57f..140248e319f 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -43,8 +43,9 @@ SkolemManager::SkolemManager() : d_skolemCounter(0) {} Node SkolemManager::mkPurifySkolem(Node t) { + SkolemManager* skm = t.getNodeManager()->getSkolemManager(); // We do not recursively compute the original form of t here - Node k = mkSkolemFunction(SkolemId::PURIFY, {t}); + Node k = skm->mkSkolemFunction(SkolemId::PURIFY, {t}); Trace("sk-manager-skolem") << "skolem: " << k << " purify " << t << std::endl; return k; } diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index 20b67536362..e0bc4ea6b8f 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -96,7 +96,7 @@ class SkolemManager * @param t The term to purify * @return The purification skolem for t */ - Node mkPurifySkolem(Node t); + static Node mkPurifySkolem(Node t); /** * Make skolem function. This method should be used for creating fixed * skolem functions of the forms described in SkolemId. The user of this diff --git a/src/expr/subs.cpp b/src/expr/subs.cpp index 11935c65b4c..e370f445f35 100644 --- a/src/expr/subs.cpp +++ b/src/expr/subs.cpp @@ -55,9 +55,8 @@ std::optional Subs::find(TNode v) const void Subs::add(Node v) { - SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); // default, use a fresh skolem of the same type - Node s = sm->mkDummySkolem("sk", v.getType()); + Node s = NodeManager::mkDummySkolem("sk", v.getType()); add(v, s); } diff --git a/src/expr/subtype_elim_node_converter.cpp b/src/expr/subtype_elim_node_converter.cpp index e6d86571242..62a483599c5 100644 --- a/src/expr/subtype_elim_node_converter.cpp +++ b/src/expr/subtype_elim_node_converter.cpp @@ -54,7 +54,6 @@ Node SubtypeElimNodeConverter::postConvert(Node n) // note that EQUAL is strictly typed so we don't need to handle it here if (convertToRealChildren) { - NodeManager* nm = NodeManager::currentNM(); std::vector children; bool childChanged = false; for (const Node& nc : n) @@ -65,12 +64,12 @@ Node SubtypeElimNodeConverter::postConvert(Node n) if (nc.isConst()) { // we convert constant integers to constant reals - children.push_back(nm->mkConstReal(nc.getConst())); + children.push_back(d_nm->mkConstReal(nc.getConst())); } else { // otherwise, use TO_REAL - children.push_back(nm->mkNode(Kind::TO_REAL, nc)); + children.push_back(d_nm->mkNode(Kind::TO_REAL, nc)); } } else @@ -82,13 +81,13 @@ Node SubtypeElimNodeConverter::postConvert(Node n) { return n; } - return nm->mkNode(k, children); + return d_nm->mkNode(k, children); } // convert skolems as well, e.g. the purify skolem for (> 1 0.0) becomes the // purify skolem for (> 1.0 0.0). if (n.isVar()) { - SkolemManager* skm = NodeManager::currentNM()->getSkolemManager(); + SkolemManager* skm = d_nm->getSkolemManager(); SkolemId id; Node cacheVal; if (skm->isSkolemFunction(n, id, cacheVal)) diff --git a/src/expr/sygus_term_enumerator.cpp b/src/expr/sygus_term_enumerator.cpp index dc80b9e8a55..cedfecf486b 100644 --- a/src/expr/sygus_term_enumerator.cpp +++ b/src/expr/sygus_term_enumerator.cpp @@ -39,9 +39,7 @@ SygusTermEnumerator::SygusTermEnumerator(Env& env, // grammar, which is important if the grammar involves terms that have // user definitions in env. theory::datatypes::utils::computeExpandedDefinitionForms(env, tn); - NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); - d_enum = sm->mkDummySkolem("enum", tn); + d_enum = NodeManager::mkDummySkolem("enum", tn); d_internal->initialize(d_enum); // ensure current is non-null if (d_internal->getCurrent().isNull()) diff --git a/src/preprocessing/passes/ackermann.cpp b/src/preprocessing/passes/ackermann.cpp index c98f870be66..dda90e92062 100644 --- a/src/preprocessing/passes/ackermann.cpp +++ b/src/preprocessing/passes/ackermann.cpp @@ -209,13 +209,11 @@ void collectUSortsToBV(NodeManager* nm, const USortToBVSizeMap& usortCardinality, SubstitutionMap& usVarsToBVVars) { - SkolemManager* sm = nm->getSkolemManager(); - for (TNode var : vars) { TypeNode type = var.getType(); size_t size = getBVSkolemSize(usortCardinality.at(type)); - Node skolem = sm->mkDummySkolem( + Node skolem = NodeManager::mkDummySkolem( "ackermann.bv", nm->mkBitVectorType(size), "a variable created by the ackermannization " diff --git a/src/preprocessing/passes/fun_def_fmf.cpp b/src/preprocessing/passes/fun_def_fmf.cpp index d0fad4c16e2..c608b90d41b 100644 --- a/src/preprocessing/passes/fun_def_fmf.cpp +++ b/src/preprocessing/passes/fun_def_fmf.cpp @@ -93,7 +93,6 @@ void FunDefFmf::process(AssertionPipeline* assertionsToPreprocess) std::map subs_head; // first pass : find defined functions, transform quantifiers NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); for (size_t i = 0, asize = assertions.size(); i < asize; i++) { Node n = QuantAttributes::getFunDefHead(assertions[i]); @@ -139,7 +138,7 @@ void FunDefFmf::process(AssertionPipeline* assertionsToPreprocess) TypeNode typ = nm->mkFunctionType(iType, n[j].getType()); std::stringstream ssf; ssf << f << "_arg_" << j; - d_input_arg_inj[f].push_back(sm->mkDummySkolem( + d_input_arg_inj[f].push_back(NodeManager::mkDummySkolem( ssf.str(), typ, "op created during fun def fmf")); } diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp index a3b00c29d0f..d2c58ae5ac0 100644 --- a/src/preprocessing/passes/ho_elim.cpp +++ b/src/preprocessing/passes/ho_elim.cpp @@ -42,7 +42,6 @@ HoElim::HoElim(PreprocessingPassContext* preprocContext) Node HoElim::eliminateLambdaComplete(Node n, std::map& newLambda) { NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); std::unordered_map::iterator it; std::vector visit; TNode cur; @@ -99,7 +98,7 @@ Node HoElim::eliminateLambdaComplete(Node n, std::map& newLambda) } TypeNode rangeType = lam.getType().getRangeType(); TypeNode nft = nm->mkFunctionType(ftypes, rangeType); - Node nf = sm->mkDummySkolem("ll", nft); + Node nf = NodeManager::mkDummySkolem("ll", nft); Trace("ho-elim-ll") << "...introduce: " << nf << " of type " << nft << std::endl; newLambda[nf] = nlambda; @@ -160,7 +159,6 @@ Node HoElim::eliminateHo(Node n) { Trace("ho-elim-assert") << "Ho-elim assertion: " << n << std::endl; NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); std::unordered_map::iterator it; std::map preReplace; std::map::iterator itr; @@ -197,7 +195,7 @@ Node HoElim::eliminateHo(Node n) } else { - ret = sm->mkDummySkolem("k", ut); + ret = NodeManager::mkDummySkolem("k", ut); } // must get the ho apply to ensure extensionality is applied Node hoa = getHoApplyUf(tn); @@ -270,7 +268,7 @@ Node HoElim::eliminateHo(Node n) { Assert(!childrent.empty()); TypeNode newFType = nm->mkFunctionType(childrent, cur.getType()); - retOp = sm->mkDummySkolem("rf", newFType); + retOp = NodeManager::mkDummySkolem("rf", newFType); d_visited_op[op] = retOp; } else @@ -513,13 +511,12 @@ Node HoElim::getHoApplyUf(TypeNode tnf, TypeNode tna, TypeNode tnr) if (it == d_hoApplyUf.end()) { NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); std::vector hoTypeArgs; hoTypeArgs.push_back(tnf); hoTypeArgs.push_back(tna); TypeNode tnh = nm->mkFunctionType(hoTypeArgs, tnr); - Node k = sm->mkDummySkolem("ho", tnh); + Node k = NodeManager::mkDummySkolem("ho", tnh); d_hoApplyUf[tnf] = k; return k; } diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp index db3c7fb5d95..22b2c60abad 100644 --- a/src/preprocessing/passes/int_to_bv.cpp +++ b/src/preprocessing/passes/int_to_bv.cpp @@ -111,7 +111,6 @@ Node IntToBV::intToBV(TNode n, NodeMap& cache) AlwaysAssert(!options().base.incrementalSolving); NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); NodeMap binaryCache; Node n_binary = intToBVMakeBinary(nm, n, binaryCache); @@ -236,9 +235,10 @@ Node IntToBV::intToBV(TNode n, NodeMap& cache) { if (current.getType() == nm->integerType()) { - result = sm->mkDummySkolem("__intToBV_var", - nm->mkBitVectorType(size), - "Variable introduced in intToBV pass"); + result = + NodeManager::mkDummySkolem("__intToBV_var", + nm->mkBitVectorType(size), + "Variable introduced in intToBV pass"); /** * Correctly convert signed/unsigned BV values to Integers as follows * x < 0 ? -nat(-x) : nat(x) diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp index 66af5994bfd..47f78f8eebb 100644 --- a/src/preprocessing/passes/miplib_trick.cpp +++ b/src/preprocessing/passes/miplib_trick.cpp @@ -209,7 +209,6 @@ PreprocessingPassResult MipLibTrick::applyInternal( SubstitutionMap& top_level_substs = tlsm.get(); NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); Node zero = nm->mkConstInt(Rational(0)), one = nm->mkConstInt(Rational(1)); Node trueNode = nm->mkConst(true); @@ -523,7 +522,7 @@ PreprocessingPassResult MipLibTrick::applyInternal( { stringstream ss; ss << "mipvar_" << *ii; - Node newVar = sm->mkDummySkolem( + Node newVar = NodeManager::mkDummySkolem( ss.str(), nm->integerType(), "a variable introduced due to scrubbing a miplib encoding"); diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp index ad6b30372d8..228e7cd868b 100644 --- a/src/preprocessing/passes/nl_ext_purify.cpp +++ b/src/preprocessing/passes/nl_ext_purify.cpp @@ -35,7 +35,6 @@ Node NlExtPurify::purifyNlTerms(TNode n, bool beneathMult) { NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); if (beneathMult) { NodeMap::iterator find = bcache.find(n); @@ -72,9 +71,10 @@ Node NlExtPurify::purifyNlTerms(TNode n, else { // new variable - ret = sm->mkDummySkolem("__purifyNl_var", - n.getType(), - "Variable introduced in purifyNl pass"); + ret = + NodeManager::mkDummySkolem("__purifyNl_var", + n.getType(), + "Variable introduced in purifyNl pass"); Node np = purifyNlTerms(n, cache, bcache, var_eq, false); var_eq.push_back(np.eqNode(ret)); Trace("nl-ext-purify") << "Purify : " << ret << " -> " << np diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp index 20bbd60b1b9..ad040100ceb 100644 --- a/src/preprocessing/passes/sep_skolem_emp.cpp +++ b/src/preprocessing/passes/sep_skolem_emp.cpp @@ -47,7 +47,6 @@ Node preSkolemEmp(NodeManager* nm, std::map::iterator it = visited[pol].find(n); if (it == visited[pol].end()) { - SkolemManager* sm = nm->getSkolemManager(); Trace("sep-preprocess") << "Pre-skolem emp " << n << " with pol " << pol << std::endl; Node ret = n; @@ -55,10 +54,10 @@ Node preSkolemEmp(NodeManager* nm, { if (!pol) { - Node x = - sm->mkDummySkolem("ex", locType, "skolem location for negated emp"); - Node y = - sm->mkDummySkolem("ey", dataType, "skolem data for negated emp"); + Node x = NodeManager::mkDummySkolem( + "ex", locType, "skolem location for negated emp"); + Node y = NodeManager::mkDummySkolem( + "ey", dataType, "skolem data for negated emp"); return nm ->mkNode(Kind::SEP_STAR, nm->mkNode(Kind::SEP_PTO, x, y), diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp index 4dfc485a4f8..7935b559cf2 100644 --- a/src/preprocessing/passes/unconstrained_simplifier.cpp +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -126,8 +126,7 @@ void UnconstrainedSimplifier::visitAll(TNode assertion) Node UnconstrainedSimplifier::newUnconstrainedVar(TypeNode t, TNode var) { - SkolemManager* sm = nodeManager()->getSkolemManager(); - Node n = sm->mkDummySkolem( + Node n = NodeManager::mkDummySkolem( "unconstrained", t, "a new var introduced because of unconstrained variable " diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp index 6be35a3b062..e6e0c6842dc 100644 --- a/src/preprocessing/util/ite_utilities.cpp +++ b/src/preprocessing/util/ite_utilities.cpp @@ -346,8 +346,7 @@ Node ITECompressor::push_back_boolean(Node original, Node compressed) else { NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); - Node skolem = sm->mkDummySkolem("compress", nm->booleanType()); + Node skolem = NodeManager::mkDummySkolem("compress", nm->booleanType()); d_compressed[rewritten] = skolem; d_compressed[original] = skolem; d_compressed[compressed] = skolem; @@ -1362,8 +1361,7 @@ Node ITESimplifier::getSimpVar(TypeNode t) { return (*it).second; } - SkolemManager* sm = nodeManager()->getSkolemManager(); - Node var = sm->mkDummySkolem( + Node var = NodeManager::mkDummySkolem( "iteSimp", t, "is a variable resulting from ITE simplification"); d_simpVars[t] = var; return var; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 141f7fb54df..0bee9b74bad 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1147,6 +1147,8 @@ std::string Smt2Printer::smtKindString(Kind k) case Kind::DISTINCT: return "distinct"; case Kind::SEXPR: break; + case Kind::TYPE_OF: return "@type_of"; + // bool theory case Kind::NOT: return "not"; case Kind::AND: return "and"; @@ -1313,6 +1315,7 @@ std::string Smt2Printer::smtKindString(Kind k) case Kind::RELATION_GROUP: return "rel.group"; case Kind::RELATION_AGGREGATE: return "rel.aggr"; case Kind::RELATION_PROJECT: return "rel.project"; + case Kind::SET_EMPTY_OF_TYPE: return "@set.empty_of_type"; // bag theory case Kind::BAG_TYPE: return "Bag"; @@ -1436,6 +1439,7 @@ std::string Smt2Printer::smtKindString(Kind k) case Kind::SEQUENCE_TYPE: return "Seq"; case Kind::SEQ_UNIT: return "seq.unit"; case Kind::SEQ_NTH: return "seq.nth"; + case Kind::SEQ_EMPTY_OF_TYPE: return "@seq.empty_of_type"; // sep theory case Kind::SEP_STAR: return "sep"; diff --git a/src/proof/alf/alf_list_node_converter.cpp b/src/proof/alf/alf_list_node_converter.cpp index f5e33ab4b87..d45e5ce277b 100644 --- a/src/proof/alf/alf_list_node_converter.cpp +++ b/src/proof/alf/alf_list_node_converter.cpp @@ -15,19 +15,58 @@ #include "proof/alf/alf_list_node_converter.h" +#include "expr/emptyset.h" #include "expr/nary_term_util.h" +#include "expr/sequence.h" #include "printer/printer.h" #include "printer/smt2/smt2_printer.h" +#include "theory/strings/word.h" namespace cvc5::internal { namespace proof { AlfListNodeConverter::AlfListNodeConverter(NodeManager* nm, - BaseAlfNodeConverter& tproc) - : NodeConverter(nm), d_tproc(tproc) + BaseAlfNodeConverter& tproc, + const std::map& adtcMap) + : NodeConverter(nm), d_tproc(tproc), d_adtcMap(adtcMap) { } +Node AlfListNodeConverter::preConvert(Node n) +{ + Kind k = n.getKind(); + if (k == Kind::SET_EMPTY_OF_TYPE || k == Kind::SEQ_EMPTY_OF_TYPE) + { + if (n[0].getKind() == Kind::TYPE_OF) + { + Node t = n[0][0]; + std::map::const_iterator it = d_adtcMap.find(t); + if (it != d_adtcMap.end()) + { + std::stringstream ss; + ss << it->second[0]; + TypeNode tn = d_nm->mkSort(ss.str()); + if (k == Kind::SET_EMPTY_OF_TYPE) + { + tn = d_nm->mkSetType(tn); + return d_tproc.convert(d_nm->mkConst(EmptySet(tn))); + } + else + { + std::vector seq; + return d_tproc.convert(d_nm->mkConst(Sequence(tn, seq))); + } + } + } + Assert(false) << "AlfListNodeConverter: unhandled term " << n; + } + else + { + Assert(k != Kind::TYPE_OF) << "AlfListNodeConverter: unhandled term " << n; + } + return n; +} + Node AlfListNodeConverter::postConvert(Node n) { Kind k = n.getKind(); diff --git a/src/proof/alf/alf_list_node_converter.h b/src/proof/alf/alf_list_node_converter.h index 1a31fd0a98d..6b639186b2b 100644 --- a/src/proof/alf/alf_list_node_converter.h +++ b/src/proof/alf/alf_list_node_converter.h @@ -27,20 +27,20 @@ namespace proof { * This node converter adds applications of "singleton elimination" to * accurately reflect the difference in semantics between ALF and RARE. * - * This is used when printing RARE rules in ALF. For example, the RARE rule: + * This is used when printing RARE rules in Eunoia. For example, the RARE rule: * * (define-rule bool-or-false ((xs Bool :list) (ys Bool :list)) * (or xs false ys) * (or xs ys)) * - * becomes the ALF rule: + * becomes the Eunoia rule: * * (declare-rule bool-or-false ((xs Bool :list) (ys Bool :list)) * :args (xs ys) * :conclusion (= (or xs false ys)) ($singleton_elim (or xs ys))) * ) * - * Where note that $singleton_elim is defined in our ALF signature: + * Where note that $singleton_elim is defined in our CPC Eunoia signature: * * (program $singleton_elim * ((T Type) (S Type) (U Type) (f (-> T U S)) (x S) (x1 T) (x2 T :list)) @@ -57,23 +57,47 @@ namespace proof { * The reason is that (or xs ys) *may* become a singleton list when xs and ys * are instantiated. Say xs -> [A] and ys -> []. In RARE, the conclusion is * (= (or A false) A) - * In ALF, the conclusion is: + * In Eunoia, the conclusion is: * (= (or A false) (or A)) * * The above transformation takes into account the difference in semantics. * More generally, we apply $singleton_elim to any subterm of the input * term that has fewer than 2 children that are not marked with :list. + * + * We additionally convert terms that represent empty sets and sequences + * in their internal cvc5+RARE representation. In particular, + * (@set.empty_of_type (@type_of x1)) becomes (set.empty T1). + * (@seq.empty_of_type (@type_of x1)) becomes (seq.empty T1). + * where T1 is the type of x1, which was assigned by the dependent type + * converter (alf_dependent_type_converter.h). We take this mapping as + * an input to this class. */ class AlfListNodeConverter : public NodeConverter { public: - AlfListNodeConverter(NodeManager* nm, BaseAlfNodeConverter& tproc); + /** + * @param nm The node manager + * @param tproc The node converter, for converting terms to their final + * form to be printed + * @param adtcMap Mapping from variables to symbols whose names are the + * types of the variables assigned to them. For example, a variable of type + * ?Set may be mapped to `(Set T1)` where `T1` is a sort name allocated by + * the dependent type converter (alf_dependent_type_converter.h). + */ + AlfListNodeConverter(NodeManager* nm, + BaseAlfNodeConverter& tproc, + const std::map& adtcMap); + /** Convert node n based on the conversion described above. */ + Node preConvert(Node n) override; /** Convert node n based on the conversion described above. */ Node postConvert(Node n) override; private: /** The parent converter, used for getting internal symbols and utilities */ BaseAlfNodeConverter& d_tproc; + /** Mapping symbols to a node whose name is the type associated to that symbol + */ + const std::map& d_adtcMap; }; } // namespace proof diff --git a/src/proof/alf/alf_printer.cpp b/src/proof/alf/alf_printer.cpp index 93d3dcb221e..10659b62407 100644 --- a/src/proof/alf/alf_printer.cpp +++ b/src/proof/alf/alf_printer.cpp @@ -48,7 +48,6 @@ AlfPrinter::AlfPrinter(Env& env, d_alreadyPrinted(&d_passumeCtx), d_passumeMap(&d_passumeCtx), d_termLetPrefix("@t"), - d_ltproc(nodeManager(), atp), d_rdb(rdb), // Use a let binding if proofDagGlobal is true. We can traverse binders // due to the way we print global declare-var, since terms beneath @@ -61,6 +60,7 @@ AlfPrinter::AlfPrinter(Env& env, { d_pfType = nodeManager()->mkSort("proofType"); d_false = nodeManager()->mkConst(false); + d_absType = nodeManager()->mkAbstractType(Kind::ABSTRACT_TYPE); } bool AlfPrinter::isHandled(const Options& opts, const ProofNode* pfn) @@ -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,23 +264,30 @@ 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: - case ProofRewriteRule::QUANT_MINISCOPE_FV: + case ProofRewriteRule::QUANT_MINISCOPE_AND: + case ProofRewriteRule::QUANT_MINISCOPE_OR: + case ProofRewriteRule::QUANT_MINISCOPE_ITE: 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()); @@ -529,6 +530,7 @@ void AlfPrinter::printDslRule(std::ostream& out, ProofRewriteRule r) std::stringstream ssExplicit; std::map nameCount; std::vector uviList; + std::map adtcConvMap; for (size_t i = 0, nvars = uvarList.size(); i < nvars; i++) { if (i > 0) @@ -557,6 +559,7 @@ void AlfPrinter::printDslRule(std::ostream& out, ProofRewriteRule r) ssExplicit << "(" << sss.str() << " "; TypeNode uvt = uv.getType(); Node uvtp = adtc.process(uvt); + adtcConvMap[uvi] = uvtp; ssExplicit << uvtp; if (expr::isListVar(uv)) { @@ -572,6 +575,9 @@ void AlfPrinter::printDslRule(std::ostream& out, ProofRewriteRule r) { out << "(" << p << " " << p.getType() << ") "; } + // carry the mapping from symbols to their types, which is used when + // eliminating internal-only operators for representing empty set and sequence + AlfListNodeConverter ltproc(nodeManager(), d_tproc, adtcConvMap); // now print variables of the proof rule out << ssExplicit.str(); out << ")" << std::endl; @@ -591,23 +597,39 @@ void AlfPrinter::printDslRule(std::ostream& out, ProofRewriteRule r) } // note we apply list conversion to premises as well. Node cc = d_tproc.convert(su.apply(c)); - cc = d_ltproc.convert(cc); + cc = ltproc.convert(cc); out << cc; } out << ")" << std::endl; } out << " :args ("; - for (size_t i = 0, nvars = uviList.size(); i < nvars; i++) + bool printedArg = false; + for (const Node& v : uviList) { - if (i > 0) - { - out << " "; - } - out << uviList[i]; + out << (printedArg ? " " : ""); + printedArg = true; + out << v; + } + // Special case: must print explicit types. + // This is to handle rules where Kind::TYPE_OF appears in the conclusion + // or in the premises. Since RARE rules do not take types as arguments, + // we must add them here. The printer for proof steps will add them in + // a similar manner. + std::vector explictTypeOf = rpr.getExplicitTypeOfList(); + std::map::iterator itet; + for (const Node& et : explictTypeOf) + { + out << (printedArg ? " " : ""); + printedArg = true; + Assert(et.getKind() == Kind::TYPE_OF); + Node v = su.apply(et[0]); + itet = adtcConvMap.find(v); + Assert(itet != adtcConvMap.end()); + out << itet->second; } out << ")" << std::endl; Node sconc = d_tproc.convert(su.apply(conc)); - sconc = d_ltproc.convert(sconc); + sconc = ltproc.convert(sconc); Assert(sconc.getKind() == Kind::EQUAL); out << " :conclusion (= " << sconc[0] << " " << sconc[1] << ")" << std::endl; out << ")" << std::endl; @@ -907,7 +929,6 @@ void AlfPrinter::getArgsFromProofRule(const ProofNode* pn, std::vector ss(pargs.begin() + 1, pargs.end()); std::vector>> witnessTerms; rpr.getConclusionFor(ss, witnessTerms); - TypeNode absType = nodeManager()->mkAbstractType(Kind::ABSTRACT_TYPE); // the arguments are the computed witness terms for (const std::pair>& w : witnessTerms) { @@ -926,7 +947,28 @@ void AlfPrinter::getArgsFromProofRule(const ProofNode* pn, args.push_back(d_tproc.mkInternalApp( printer::smt2::Smt2Printer::smtKindString(w.first), wargs, - absType)); + d_absType)); + } + } + // special case: explicit type-of terms, which require explicit type + // arguments + std::map>::iterator it = + d_explicitTypeOf.find(dr); + if (it == d_explicitTypeOf.end()) + { + d_explicitTypeOf[dr] = rpr.getExplicitTypeOfList(); + it = d_explicitTypeOf.find(dr); + } + if (!it->second.empty()) + { + const std::vector& fvs = rpr.getVarList(); + AlwaysAssert(fvs.size() == ss.size()); + for (const Node& t : it->second) + { + Assert(t.getKind() == Kind::TYPE_OF); + Node tts = + t[0].substitute(fvs.begin(), fvs.end(), ss.begin(), ss.end()); + args.push_back(d_tproc.typeAsNode(tts.getType())); } } return; diff --git a/src/proof/alf/alf_printer.h b/src/proof/alf/alf_printer.h index 03421d605d1..fce09439a98 100644 --- a/src/proof/alf/alf_printer.h +++ b/src/proof/alf/alf_printer.h @@ -186,8 +186,8 @@ class AlfPrinter : protected EnvObj std::string d_termLetPrefix; /** The false node */ Node d_false; - /** List node converter */ - AlfListNodeConverter d_ltproc; + /** */ + TypeNode d_absType; /** Pointer to the rewrite database */ rewriter::RewriteDb* d_rdb; /** The empty vector */ @@ -198,6 +198,8 @@ class AlfPrinter : protected EnvObj LetBinding* d_lbindUse; /** The letification channel. */ AlfPrintChannelPre d_aletify; + /** A cache for explicit type-of variables, for printing DSL_REWRITE steps */ + std::map> d_explicitTypeOf; }; } // namespace proof diff --git a/src/proof/trust_id.cpp b/src/proof/trust_id.cpp index 01306f84c6a..ddefef08d74 100644 --- a/src/proof/trust_id.cpp +++ b/src/proof/trust_id.cpp @@ -84,6 +84,7 @@ const char* toString(TrustId id) case TrustId::ARITH_NL_COMPARE_LIT_TRANSFORM: return "ARITH_NL_COMPARE_LIT_TRANSFORM"; case TrustId::ARITH_DIO_LEMMA: return "ARITH_DIO_LEMMA"; + case TrustId::DIAMONDS: return "DIAMONDS"; case TrustId::EXT_THEORY_REWRITE: return "EXT_THEORY_REWRITE"; case TrustId::REWRITE_NO_ELABORATE: return "REWRITE_NO_ELABORATE"; case TrustId::FLATTENING_REWRITE: return "FLATTENING_REWRITE"; diff --git a/src/proof/trust_id.h b/src/proof/trust_id.h index 6f29b9bb976..4763a85c4d4 100644 --- a/src/proof/trust_id.h +++ b/src/proof/trust_id.h @@ -149,6 +149,8 @@ enum class TrustId : uint32_t ARITH_NL_COMPARE_LIT_TRANSFORM, /** A lemma from the DIO solver */ ARITH_DIO_LEMMA, + /** Diamonds preprocessing in TheoryUf::ppStaticLearn */ + DIAMONDS, /** An extended theory rewrite */ EXT_THEORY_REWRITE, /** A rewrite whose proof could not be elaborated */ diff --git a/src/rewriter/basic_rewrite_rcons.cpp b/src/rewriter/basic_rewrite_rcons.cpp index dff46203ad1..df7c4ebe96d 100644 --- a/src/rewriter/basic_rewrite_rcons.cpp +++ b/src/rewriter/basic_rewrite_rcons.cpp @@ -650,7 +650,7 @@ bool BasicRewriteRCons::ensureProofMacroQuantPrenex(CDProof* cdp, rr->rewriteViaRule(ProofRewriteRule::QUANT_MERGE_PRENEX, umergeq); if (mergeq != eq[1]) { - Trace("brc-macro") << "Failed merge step"; + Trace("brc-macro") << "Failed merge step" << std::endl; return false; } Node eqq2 = umergeq.eqNode(mergeq); @@ -658,56 +658,86 @@ bool BasicRewriteRCons::ensureProofMacroQuantPrenex(CDProof* cdp, cdp->addStep(eq, ProofRule::TRANS, {eqq, eqq2}, {}); Trace("brc-macro") << "Remains to prove: " << body1 << " == " << body2 << std::endl; - Node body2ms = - rr->rewriteViaRule(ProofRewriteRule::QUANT_MINISCOPE_FV, body2); - if (body2ms.isNull()) - { - // currently fails if we are doing - // forall x. ite(C, forall Y. t, s) = - // forall xy. ite(C, t, s) - // since we don't miniscope over ITE. - Trace("brc-macro") << "Failed miniscope"; - return false; - } - Node eqqm = body2.eqNode(body2ms); - cdp->addTheoryRewriteStep(eqqm, ProofRewriteRule::QUANT_MINISCOPE_FV); + // add the symmetry of the equality to the process vector, we will recursively + // prove it via miniscoping steps below. Node eqqrs = body2.eqNode(body1); - if (body2ms != body1) + std::vector toProcess; + std::unordered_set processed; + toProcess.push_back(eqqrs); + while (!toProcess.empty()) { - if (body2ms.getKind() != body1.getKind() - || body2ms.getNumChildren() != body1.getNumChildren()) + Node currEq = toProcess.back(); + toProcess.pop_back(); + if (processed.find(currEq) != processed.end()) + { + continue; + } + processed.insert(currEq); + if (currEq[0].getKind() != Kind::FORALL) { - Trace("brc-macro") << "Failed after miniscope"; + Trace("brc-macro") << "Unexpected subgoal" << std::endl; return false; } - // We may have used alpha equivalence to rename variables, thus we - // introduce a CONG step where children that are disequal are given as - // subgoals. - std::vector cpremises; - for (size_t i = 0, nchildren = body2ms.getNumChildren(); i < nchildren; i++) + Kind bk = currEq[0][1].getKind(); + ProofRewriteRule prr = + bk == Kind::ITE + ? ProofRewriteRule::QUANT_MINISCOPE_ITE + : (bk == Kind::OR ? ProofRewriteRule::QUANT_MINISCOPE_OR + : ProofRewriteRule::QUANT_MINISCOPE_AND); + Node body2ms = rr->rewriteViaRule(prr, currEq[0]); + if (body2ms.isNull()) { - Node eqc = body2ms[i].eqNode(body1[i]); - if (body2ms[i] == body1[i]) + Trace("brc-macro") << "Failed miniscope" << std::endl; + return false; + } + Node eqqm = currEq[0].eqNode(body2ms); + cdp->addTheoryRewriteStep(eqqm, prr); + if (body2ms != currEq[1]) + { + if (body2ms.getKind() != currEq[1].getKind() + || body2ms.getNumChildren() != currEq[1].getNumChildren()) { - cdp->addStep(eqc, ProofRule::REFL, {}, {body2ms[i]}); + Trace("brc-macro") << "Failed after miniscope" << std::endl; + return false; } - else + // We may have used alpha equivalence to rename variables, thus we + // introduce a CONG step where children that are disequal are given as + // subgoals. + std::vector cpremises; + for (size_t i = 0, nchildren = body2ms.getNumChildren(); i < nchildren; + i++) { - Trace("brc-macro") << "...subgoal " << eqc << std::endl; - // otherwise just add subgoal, likely alpha equivalence - // Some of these goals cannot be currently proven since they involve - // multiple nested steps of miniscoping, combined with alpha - // equivalence. - cdp->addTrustedStep( - eqc, TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE, {}, {}); + Node eqc = body2ms[i].eqNode(currEq[1][i]); + cpremises.push_back(eqc); + if (eqc[0] == eqc[1]) + { + cdp->addStep(eqc, ProofRule::REFL, {}, {eqc[0]}); + continue; + } + if (eqc[1].getKind() == Kind::FORALL) + { + // just add subgoal, likely alpha equivalence + cdp->addTrustedStep( + eqc, TrustId::MACRO_THEORY_REWRITE_RCONS_SIMPLE, {}, {}); + continue; + } + // maybe the result of QUANT_UNUSED_VARS? + Node buv = + rr->rewriteViaRule(ProofRewriteRule::QUANT_UNUSED_VARS, eqc[0]); + if (buv == eqc[1]) + { + cdp->addTheoryRewriteStep(eqc, ProofRewriteRule::QUANT_UNUSED_VARS); + continue; + } + // otherwise recursely prove + toProcess.push_back(eqc); } - cpremises.push_back(eqc); + cargs.clear(); + cr = expr::getCongRule(body2ms, cargs); + Node eqqb = body2ms.eqNode(currEq[1]); + cdp->addStep(eqqb, cr, cpremises, cargs); + cdp->addStep(currEq, ProofRule::TRANS, {eqqm, eqqb}, {}); } - cargs.clear(); - cr = expr::getCongRule(body2ms, cargs); - Node eqqb = body2ms.eqNode(body1); - cdp->addStep(eqqb, cr, cpremises, cargs); - cdp->addStep(eqqrs, ProofRule::TRANS, {eqqm, eqqb}, {}); } cdp->addStep(beq, ProofRule::SYMM, {eqqrs}, {}); return true; @@ -806,8 +836,8 @@ bool BasicRewriteRCons::ensureProofMacroQuantPartitionConnectedFv( Node eqq2 = newQuant.eqNode(eq[1]); // Then prove // (forall X F1 or ... or Fn) = (forall X1 F1) or ... or (forall Xn Fn) - // via ProofRewriteRule::QUANT_MINISCOPE_FV. - if (!cdp->addTheoryRewriteStep(eqq2, ProofRewriteRule::QUANT_MINISCOPE_FV)) + // via ProofRewriteRule::QUANT_MINISCOPE_OR. + if (!cdp->addTheoryRewriteStep(eqq2, ProofRewriteRule::QUANT_MINISCOPE_OR)) { Assert(false); return false; @@ -974,13 +1004,20 @@ bool BasicRewriteRCons::ensureProofMacroQuantVarElimEq(CDProof* cdp, bool BasicRewriteRCons::ensureProofMacroQuantMiniscope(CDProof* cdp, const Node& eq) { + Trace("brc-macro") << "Expand quant miniscope " << eq[0] << " == " << eq[1] + << std::endl; Node q = eq[0]; Assert(q.getKind() == Kind::FORALL); NodeManager* nm = nodeManager(); + Kind bk = q[1].getKind(); + Assert(bk == Kind::AND || bk == Kind::ITE); + ProofRewriteRule prr = bk == Kind::AND + ? ProofRewriteRule::QUANT_MINISCOPE_AND + : ProofRewriteRule::QUANT_MINISCOPE_ITE; theory::Rewriter* rr = d_env.getRewriter(); - Node mq = rr->rewriteViaRule(ProofRewriteRule::QUANT_MINISCOPE, q); + Node mq = rr->rewriteViaRule(prr, q); Node equiv = q.eqNode(mq); - cdp->addTheoryRewriteStep(equiv, ProofRewriteRule::QUANT_MINISCOPE); + cdp->addTheoryRewriteStep(equiv, prr); if (mq == eq[1]) { return true; @@ -1033,7 +1070,7 @@ bool BasicRewriteRCons::ensureProofMacroQuantMiniscope(CDProof* cdp, Assert(false) << "Failed ensureProofMacroQuantMiniscope " << eq; return false; } - // add the CONG step to conclude AND terms are equal + // add the CONG step to conclude AND or ITE terms are equal std::vector cargs; ProofRule cr = expr::getCongRule(mq, cargs); cdp->addStep(equiv2, cr, premises, cargs); diff --git a/src/rewriter/node.py b/src/rewriter/node.py index fc6e461f830..b7c1f7d1c80 100644 --- a/src/rewriter/node.py +++ b/src/rewriter/node.py @@ -156,6 +156,8 @@ def __new__(cls, symbol, kind): BV_TO_NAT = ('bv2nat', 'BITVECTOR_TO_NAT') INT_TO_BV = ('int2bv', 'INT_TO_BITVECTOR') + + TYPE_OF = ('@type_of', 'TYPE_OF') ########################################################################### # Strings @@ -190,6 +192,7 @@ def __new__(cls, symbol, kind): SEQ_UNIT = ('seq.unit', 'SEQ_UNIT') SEQ_NTH = ('seq.nth', 'SEQ_NTH') + SEQ_EMPTY_OF_TYPE = ('@seq.empty_of_type', 'SEQ_EMPTY_OF_TYPE') STRING_TO_REGEXP = ('str.to_re', 'STRING_TO_REGEXP') REGEXP_CONCAT = ('re.++', 'REGEXP_CONCAT') @@ -221,6 +224,7 @@ def __new__(cls, symbol, kind): SET_CARD = ('set.card', 'SET_CARD') SET_IS_EMPTY = ('set.is_empty', 'SET_IS_EMPTY') SET_IS_SINGLETON = ('set.is_singleton', 'SET_IS_SINGLETON') + SET_EMPTY_OF_TYPE = ('@set.empty_of_type', 'SET_EMPTY_OF_TYPE') class BaseSort(Enum): diff --git a/src/rewriter/rewrite_db_term_process.cpp b/src/rewriter/rewrite_db_term_process.cpp index f0016e70a71..03bf9d31926 100644 --- a/src/rewriter/rewrite_db_term_process.cpp +++ b/src/rewriter/rewrite_db_term_process.cpp @@ -47,7 +47,6 @@ Node RewriteDbNodeConverter::postConvert(Node n) Kind k = n.getKind(); if (k == Kind::CONST_STRING) { - NodeManager* nm = NodeManager::currentNM(); // "ABC" is (str.++ "A" "B" "C") const std::vector& vec = n.getConst().getVec(); if (vec.size() <= 1) @@ -59,9 +58,9 @@ Node RewriteDbNodeConverter::postConvert(Node n) { std::vector tmp; tmp.push_back(c); - children.push_back(nm->mkConst(String(tmp))); + children.push_back(d_nm->mkConst(String(tmp))); } - Node ret = nm->mkNode(Kind::STRING_CONCAT, children); + Node ret = d_nm->mkNode(Kind::STRING_CONCAT, children); recordProofStep(n, ret, ProofRule::EVALUATE); return ret; } @@ -74,12 +73,12 @@ Node RewriteDbNodeConverter::postConvert(Node n) else if (k == Kind::CONST_BITVECTOR) { // (_ bv N M) is (bv N M) - NodeManager* nm = NodeManager::currentNM(); std::vector children; children.push_back( - nm->mkConstInt(Rational(n.getConst().toInteger()))); - children.push_back(nm->mkConstInt(Rational(theory::bv::utils::getSize(n)))); - Node ret = nm->mkNode(Kind::CONST_BITVECTOR_SYMBOLIC, children); + d_nm->mkConstInt(Rational(n.getConst().toInteger()))); + children.push_back( + d_nm->mkConstInt(Rational(theory::bv::utils::getSize(n)))); + Node ret = d_nm->mkNode(Kind::CONST_BITVECTOR_SYMBOLIC, children); recordProofStep(n, ret, ProofRule::EVALUATE); return ret; } @@ -95,8 +94,7 @@ Node RewriteDbNodeConverter::postConvert(Node n) // ignore annotation if (n.getNumChildren() == 3) { - NodeManager* nm = NodeManager::currentNM(); - Node ret = nm->mkNode(Kind::FORALL, n[0], n[1]); + Node ret = d_nm->mkNode(Kind::FORALL, n[0], n[1]); recordProofStep(n, ret, ProofRule::ENCODE_EQ_INTRO); return ret; } @@ -136,12 +134,11 @@ Node RewriteDbNodeConverter::postConvert(Node n) // convert indexed operators to symbolic if (GenericOp::isNumeralIndexedOperatorKind(k)) { - NodeManager* nm = NodeManager::currentNM(); std::vector indices = GenericOp::getIndicesForOperator(k, n.getOperator()); - indices.insert(indices.begin(), nm->mkConst(GenericOp(k))); + indices.insert(indices.begin(), d_nm->mkConst(GenericOp(k))); indices.insert(indices.end(), n.begin(), n.end()); - Node ret = nm->mkNode(Kind::APPLY_INDEXED_SYMBOLIC, indices); + Node ret = d_nm->mkNode(Kind::APPLY_INDEXED_SYMBOLIC, indices); recordProofStep(n, ret, ProofRule::ENCODE_EQ_INTRO); return ret; } diff --git a/src/rewriter/rewrite_proof_rule.cpp b/src/rewriter/rewrite_proof_rule.cpp index b06c2996cab..b960e09a84f 100644 --- a/src/rewriter/rewrite_proof_rule.cpp +++ b/src/rewriter/rewrite_proof_rule.cpp @@ -37,7 +37,7 @@ void RewriteProofRule::init(ProofRewriteRule id, Node context) { // not initialized yet - Assert(d_cond.empty() && d_obGen.empty() && d_fvs.empty()); + Assert(d_cond.empty() && d_fvs.empty()); d_id = id; d_userFvs = userFvs; std::map condDef; @@ -49,7 +49,6 @@ void RewriteProofRule::init(ProofRewriteRule id, << "Ambiguous context for list variables in condition of rule " << id; } d_cond.push_back(c); - d_obGen.push_back(c); if (c.getKind() == Kind::EQUAL && c[0].getKind() == Kind::BOUND_VARIABLE) { condDef[c[0]] = c[1]; @@ -134,6 +133,24 @@ const std::vector& RewriteProofRule::getUserVarList() const return d_userFvs; } const std::vector& RewriteProofRule::getVarList() const { return d_fvs; } + +std::vector RewriteProofRule::getExplicitTypeOfList() const +{ + std::vector ret; + Node conc = getConclusion(true); + std::unordered_set ccts; + expr::getKindSubterms(conc, Kind::TYPE_OF, true, ccts); + for (const Node& c : d_cond) + { + expr::getKindSubterms(c, Kind::TYPE_OF, true, ccts); + } + for (const Node& t : ccts) + { + ret.emplace_back(t); + } + return ret; +} + bool RewriteProofRule::isExplicitVar(Node v) const { Assert(std::find(d_fvs.begin(), d_fvs.end(), v) != d_fvs.end()); @@ -160,7 +177,7 @@ bool RewriteProofRule::getObligations(const std::vector& vs, std::vector& vcs) const { // substitute into each condition - for (const Node& c : d_obGen) + for (const Node& c : d_cond) { Node sc = expr::narySubstitute(c, vs, ss); vcs.push_back(sc); diff --git a/src/rewriter/rewrite_proof_rule.h b/src/rewriter/rewrite_proof_rule.h index 5d06a5366a7..200ada4e026 100644 --- a/src/rewriter/rewrite_proof_rule.h +++ b/src/rewriter/rewrite_proof_rule.h @@ -128,7 +128,12 @@ class RewriteProofRule Node getConclusionFor( const std::vector& ss, std::vector>>& witnessTerms) const; - + /** + * @return the list of applications of Kind::TYPE_OF that appear in the + * conclusion or a premise. These require special handling by the + * printer. + */ + std::vector getExplicitTypeOfList() const; /** * Is variable explicit? An explicit variable is one that does not occur * in a condition and thus its value must be specified in a proof @@ -171,8 +176,6 @@ class RewriteProofRule ProofRewriteRule d_id; /** The conditions of the rule */ std::vector d_cond; - /** The obligation generator formulas of the rule */ - std::vector d_obGen; /** The conclusion of the rule (an equality) */ Node d_conc; /** Is the rule applied in some fixed point context? */ diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index be9abd6d6d4..4744e9b424b 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -130,7 +130,7 @@ TrustNode RemoveTermFormulas::runLemma( Node RemoveTermFormulas::runInternal(TNode assertion, std::vector& output) { - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = nodeManager(); TCtxStack ctx(&d_rtfc); std::vector processedChildren; ctx.pushInitial(assertion); @@ -271,8 +271,7 @@ Node RemoveTermFormulas::runCurrentInternal(TNode node, TConvProofGenerator* pg) { AlwaysAssert (node.getKind()!=Kind::WITNESS) << "WITNESS should never appear in asserted terms"; - NodeManager *nodeManager = NodeManager::currentNM(); - SkolemManager* sm = nodeManager->getSkolemManager(); + SkolemManager* sm = nodeManager()->getSkolemManager(); TypeNode nodeType = node.getType(); Node skolem; @@ -310,7 +309,7 @@ Node RemoveTermFormulas::runCurrentInternal(TNode node, // of the lemma is used. // The new assertion - newAssertion = nodeManager->mkNode( + newAssertion = nodeManager()->mkNode( Kind::ITE, node[0], skolem.eqNode(node[1]), skolem.eqNode(node[2])); // we justify it internally @@ -444,11 +443,10 @@ Node RemoveTermFormulas::getSkolemForNode(Node k) const Node RemoveTermFormulas::getAxiomFor(Node n) { - NodeManager* nm = NodeManager::currentNM(); Kind k = n.getKind(); if (k == Kind::ITE) { - return nm->mkNode(Kind::ITE, n[0], n.eqNode(n[1]), n.eqNode(n[2])); + return NodeManager::mkNode(Kind::ITE, n[0], n.eqNode(n[1]), n.eqNode(n[2])); } return Node::null(); } diff --git a/src/theory/arith/linear/callbacks.cpp b/src/theory/arith/linear/callbacks.cpp index f50a574270b..12615c1255b 100644 --- a/src/theory/arith/linear/callbacks.cpp +++ b/src/theory/arith/linear/callbacks.cpp @@ -48,8 +48,7 @@ TempVarMalloc::TempVarMalloc(TheoryArithPrivate& ta) {} ArithVar TempVarMalloc::request(){ NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); - Node skolem = sm->mkDummySkolem("tmpVar", nm->realType()); + Node skolem = NodeManager::mkDummySkolem("tmpVar", nm->realType()); return d_ta.requestArithVar(skolem, false, true); } void TempVarMalloc::release(ArithVar v){ diff --git a/src/theory/arith/linear/dio_solver.cpp b/src/theory/arith/linear/dio_solver.cpp index f1cf0308fe4..45281277cc3 100644 --- a/src/theory/arith/linear/dio_solver.cpp +++ b/src/theory/arith/linear/dio_solver.cpp @@ -32,10 +32,10 @@ namespace arith::linear { inline Node makeIntegerVariable(NodeManager* nm) { - SkolemManager* sm = nm->getSkolemManager(); - return sm->mkDummySkolem("intvar", - nm->integerType(), - "is an integer variable created by the dio solver"); + return NodeManager::mkDummySkolem( + "intvar", + nm->integerType(), + "is an integer variable created by the dio solver"); } DioSolver::DioSolver(Env& env) diff --git a/src/theory/arith/linear/theory_arith_private.cpp b/src/theory/arith/linear/theory_arith_private.cpp index 04de2797a11..dbe7c60430e 100644 --- a/src/theory/arith/linear/theory_arith_private.cpp +++ b/src/theory/arith/linear/theory_arith_private.cpp @@ -1823,8 +1823,7 @@ void TheoryArithPrivate::outputPropagate(TNode lit) { void TheoryArithPrivate::outputRestart() { Trace("arith::channel") << "Arith restart!" << std::endl; NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); - Node restartVar = sm->mkDummySkolem( + Node restartVar = NodeManager::mkDummySkolem( "restartVar", nm->booleanType(), "A boolean variable asserted to be true to force a restart"); diff --git a/src/theory/arith/nl/coverings_solver.cpp b/src/theory/arith/nl/coverings_solver.cpp index 0e237577179..b18e5bf86b2 100644 --- a/src/theory/arith/nl/coverings_solver.cpp +++ b/src/theory/arith/nl/coverings_solver.cpp @@ -43,8 +43,7 @@ CoveringsSolver::CoveringsSolver(Env& env, InferenceManager& im, NlModel& model) d_eqsubs(env) { NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); - d_ranVariable = sm->mkDummySkolem("__z", nm->realType(), ""); + d_ranVariable = NodeManager::mkDummySkolem("__z", nm->realType(), ""); } CoveringsSolver::~CoveringsSolver() {} diff --git a/src/theory/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp index 19256df3cf7..8aaa6c58fac 100644 --- a/src/theory/arrays/theory_arrays_rewriter.cpp +++ b/src/theory/arrays/theory_arrays_rewriter.cpp @@ -66,6 +66,10 @@ void setMostFrequentValueCount(TNode store, uint64_t count) TheoryArraysRewriter::TheoryArraysRewriter(NodeManager* nm, Rewriter* r) : TheoryRewriter(nm), d_rewriter(r) { + registerProofRewriteRule(ProofRewriteRule::MACRO_ARRAYS_DISTINCT_ARRAYS, + TheoryRewriteCtx::PRE_DSL); + registerProofRewriteRule(ProofRewriteRule::MACRO_ARRAYS_NORMALIZE_CONSTANT, + TheoryRewriteCtx::PRE_DSL); registerProofRewriteRule(ProofRewriteRule::ARRAYS_SELECT_CONST, TheoryRewriteCtx::PRE_DSL); registerProofRewriteRule(ProofRewriteRule::ARRAYS_EQ_RANGE_EXPAND, @@ -76,6 +80,29 @@ Node TheoryArraysRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n) { switch (id) { + case ProofRewriteRule::MACRO_ARRAYS_DISTINCT_ARRAYS: + { + if (n.getKind() == Kind::EQUAL && n[0].isConst() && n[1].isConst() + && n[0] != n[1]) + { + Assert(n[0].getType().isArray()); + return d_nm->mkConst(false); + } + } + break; + case ProofRewriteRule::MACRO_ARRAYS_NORMALIZE_CONSTANT: + { + if (n.getKind() == Kind::STORE && n[0].isConst() && n[1].isConst() + && n[2].isConst()) + { + Node nn = normalizeConstant(nodeManager(), n); + if (nn != n) + { + return nn; + } + } + } + break; case ProofRewriteRule::ARRAYS_SELECT_CONST: { if (n.getKind() == Kind::SELECT && n[0].getKind() == Kind::STORE_ALL) diff --git a/src/theory/bags/solver_state.cpp b/src/theory/bags/solver_state.cpp index a8c6d4147f8..c82d6886b8c 100644 --- a/src/theory/bags/solver_state.cpp +++ b/src/theory/bags/solver_state.cpp @@ -176,8 +176,8 @@ void SolverState::checkInjectivity(Node n) } TypeNode domainType = f.getType().getArgTypes()[0]; - Node x = sm->mkDummySkolem("x", domainType); - Node y = sm->mkDummySkolem("y", domainType); + Node x = NodeManager::mkDummySkolem("x", domainType); + Node y = NodeManager::mkDummySkolem("y", domainType); Node f_x = d_nm->mkNode(Kind::APPLY_UF, f, x); Node f_y = d_nm->mkNode(Kind::APPLY_UF, f, y); Node f_x_equals_f_y = f_x.eqNode(f_y); diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index aef4c6b5efd..d798b753790 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -320,6 +320,7 @@ typerule WITNESS ::cvc5::internal::theory::builtin::WitnessTypeRule variable RAW_SYMBOL "a variable that is not quoted in the smt2 printer (internal only)" +# The following operators and types are used primarily for RARE constant ABSTRACT_TYPE \ class \ @@ -340,8 +341,6 @@ parameterized APPLY_INDEXED_SYMBOLIC APPLY_INDEXED_SYMBOLIC_OP 1: "generic index typerule APPLY_INDEXED_SYMBOLIC_OP "SimpleTypeRule" typerule APPLY_INDEXED_SYMBOLIC ::cvc5::internal::theory::builtin::ApplyIndexedSymbolicTypeRule - -# constants constant SORT_TO_TERM \ class \ SortToTerm \ @@ -350,4 +349,7 @@ constant SORT_TO_TERM \ "term representing a sort; payload is an instance of the cvc5::internal::SortToTerm class" typerule SORT_TO_TERM "SimpleTypeRule" +operator TYPE_OF 1 "the type of an expression, used internally for RARE" +typerule TYPE_OF ::cvc5::internal::theory::builtin::TypeOfTypeRule + endtheory diff --git a/src/theory/builtin/theory_builtin_type_rules.cpp b/src/theory/builtin/theory_builtin_type_rules.cpp index be8518f9e46..29100f06fbd 100644 --- a/src/theory/builtin/theory_builtin_type_rules.cpp +++ b/src/theory/builtin/theory_builtin_type_rules.cpp @@ -185,6 +185,19 @@ TypeNode ApplyIndexedSymbolicTypeRule::computeType(NodeManager* nodeManager, return cn.getType(); } +TypeNode TypeOfTypeRule::preComputeType(NodeManager* nm, TNode n) +{ + return TypeNode::null(); +} + +TypeNode TypeOfTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check, + std::ostream* errOut) +{ + return nodeManager->builtinOperatorType(); +} + Node SortProperties::mkGroundTerm(TypeNode type) { // we typically use this method for sorts, although there are other types diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 63cdec37e1c..10d86fcbcf1 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -87,6 +87,20 @@ class ApplyIndexedSymbolicTypeRule std::ostream* errOut); }; +/** + * Type rule for the internally used typeof operator used by RARE proof + * reconstruction. + */ +class TypeOfTypeRule +{ + public: + static TypeNode preComputeType(NodeManager* nm, TNode n); + static TypeNode computeType(NodeManager* nodeManager, + TNode n, + bool check, + std::ostream* errOut); +}; + class SortProperties { public: diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp index b7dd12ff793..636225c6fa2 100644 --- a/src/theory/bv/theory_bv_utils.cpp +++ b/src/theory/bv/theory_bv_utils.cpp @@ -276,10 +276,10 @@ Node mkConst(const BitVector& value) Node mkVar(unsigned size) { NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); - return sm->mkDummySkolem("BVSKOLEM$$", - nm->mkBitVectorType(size), - "is a variable created by the theory of bitvectors"); + return NodeManager::mkDummySkolem( + "BVSKOLEM$$", + nm->mkBitVectorType(size), + "is a variable created by the theory of bitvectors"); } /* ------------------------------------------------------------------------- */ diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index 9bf20222c8c..c172de454d3 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -458,11 +458,10 @@ Node SygusExtension::getTraversalPredicate(TypeNode tn, Node n, bool isPre) return itt->second; } NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); std::vector types; types.push_back(tn); TypeNode ptn = nm->mkPredicateType(types); - Node pred = sm->mkDummySkolem(isPre ? "pre" : "post", ptn); + Node pred = NodeManager::mkDummySkolem(isPre ? "pre" : "post", ptn); d_traversal_pred[index][tn][n] = pred; return pred; } @@ -470,7 +469,6 @@ Node SygusExtension::getTraversalPredicate(TypeNode tn, Node n, bool isPre) Node SygusExtension::eliminateTraversalPredicates(Node n) { NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); std::unordered_map visited; std::unordered_map::iterator it; std::map::iterator ittb; @@ -496,7 +494,7 @@ Node SygusExtension::eliminateTraversalPredicates(Node n) { std::stringstream ss; ss << "v_" << cur; - ret = sm->mkDummySkolem(ss.str(), cur.getType()); + ret = NodeManager::mkDummySkolem(ss.str(), cur.getType()); d_traversal_bool[cur] = ret; } else @@ -1769,8 +1767,7 @@ Node SygusExtension::SygusSizeDecisionStrategy::getOrMkMeasureValue() if (d_measure_value.isNull()) { NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); - d_measure_value = sm->mkDummySkolem("mt", nm->integerType()); + d_measure_value = NodeManager::mkDummySkolem("mt", nm->integerType()); Node mtlem = nm->mkNode(Kind::GEQ, d_measure_value, nm->mkConstInt(Rational(0))); d_im.lemma(mtlem, InferenceId::DATATYPES_SYGUS_MT_POS); @@ -1784,8 +1781,7 @@ Node SygusExtension::SygusSizeDecisionStrategy::getOrMkActiveMeasureValue( if (mkNew) { NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); - Node new_mt = sm->mkDummySkolem("mt", nm->integerType()); + Node new_mt = NodeManager::mkDummySkolem("mt", nm->integerType()); Node mtlem = nm->mkNode(Kind::GEQ, new_mt, nm->mkConstInt(Rational(0))); d_measure_value_active = new_mt; d_im.lemma(mtlem, InferenceId::DATATYPES_SYGUS_MT_POS); diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 57806821e2d..176e5091e58 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1121,7 +1121,6 @@ Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_c Node TheoryDatatypes::getSingletonLemma( TypeNode tn, bool pol ) { NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); int index = pol ? 0 : 1; std::map< TypeNode, Node >::iterator it = d_singleton_lemma[index].find( tn ); if( it==d_singleton_lemma[index].end() ){ @@ -1133,8 +1132,8 @@ Node TheoryDatatypes::getSingletonLemma( TypeNode tn, bool pol ) { nm->mkNode(Kind::BOUND_VAR_LIST, v1, v2), v1.eqNode(v2)); }else{ - Node v1 = sm->mkDummySkolem("k1", tn); - Node v2 = sm->mkDummySkolem("k2", tn); + Node v1 = NodeManager::mkDummySkolem("k1", tn); + Node v2 = NodeManager::mkDummySkolem("k2", tn); a = v1.eqNode( v2 ).negate(); //send out immediately as lemma d_im.lemma(a, InferenceId::DATATYPES_REC_SINGLETON_FORCE_DEQ); diff --git a/src/theory/fp/fp_word_blaster.cpp b/src/theory/fp/fp_word_blaster.cpp index 3eb94618a06..2a51b8e20fb 100644 --- a/src/theory/fp/fp_word_blaster.cpp +++ b/src/theory/fp/fp_word_blaster.cpp @@ -260,7 +260,7 @@ symbolicRoundingMode::symbolicRoundingMode(const symbolicRoundingMode& old) symbolicProposition symbolicRoundingMode::valid(void) const { - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = getNodeManager(); Node zero(nm->mkConst(BitVector(SYMFPU_NUMBER_OF_ROUNDING_MODES, 0u))); // Is there a better encoding of this? @@ -290,7 +290,7 @@ template Node symbolicBitVector::boolNodeToBV(Node node) const { Assert(node.getType().isBoolean()); - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = getNodeManager(); return nm->mkNode(Kind::ITE, node, nm->mkConst(BitVector(1U, 1U)), @@ -302,7 +302,7 @@ Node symbolicBitVector::BVToBoolNode(Node node) const { Assert(node.getType().isBitVector()); Assert(node.getType().getBitVectorSize() == 1); - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = getNodeManager(); return nm->mkNode(Kind::EQUAL, node, nm->mkConst(BitVector(1U, 1U))); } @@ -630,8 +630,8 @@ symbolicBitVector symbolicBitVector::toUnsigned(void) const template <> symbolicBitVector symbolicBitVector::extend(bwt extension) const { - NodeBuilder construct(NodeManager::currentNM(), Kind::BITVECTOR_SIGN_EXTEND); - construct << NodeManager::currentNM()->mkConst( + NodeBuilder construct(getNodeManager(), Kind::BITVECTOR_SIGN_EXTEND); + construct << getNodeManager()->mkConst( BitVectorSignExtend(extension)) << *this; @@ -641,8 +641,8 @@ symbolicBitVector symbolicBitVector::extend(bwt extension) const template <> symbolicBitVector symbolicBitVector::extend(bwt extension) const { - NodeBuilder construct(NodeManager::currentNM(), Kind::BITVECTOR_ZERO_EXTEND); - construct << NodeManager::currentNM()->mkConst( + NodeBuilder construct(getNodeManager(), Kind::BITVECTOR_ZERO_EXTEND); + construct << getNodeManager()->mkConst( BitVectorZeroExtend(extension)) << *this; @@ -655,8 +655,8 @@ symbolicBitVector symbolicBitVector::contract( { Assert(this->getWidth() > reduction); - NodeBuilder construct(NodeManager::currentNM(), Kind::BITVECTOR_EXTRACT); - construct << NodeManager::currentNM()->mkConst( + NodeBuilder construct(getNodeManager(), Kind::BITVECTOR_EXTRACT); + construct << getNodeManager()->template mkConst( BitVectorExtract((this->getWidth() - 1) - reduction, 0)) << *this; @@ -706,8 +706,8 @@ symbolicBitVector symbolicBitVector::extract( { Assert(upper >= lower); - NodeBuilder construct(NodeManager::currentNM(), Kind::BITVECTOR_EXTRACT); - construct << NodeManager::currentNM()->mkConst( + NodeBuilder construct(getNodeManager(), Kind::BITVECTOR_EXTRACT); + construct << getNodeManager()->template mkConst( BitVectorExtract(upper, lower)) << *this; diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 4b2aa4d2390..b8eb5deacd7 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -43,8 +43,7 @@ Node BvInverter::getSolveVariable(TypeNode tn) std::map::iterator its = d_solve_var.find(tn); if (its == d_solve_var.end()) { - SkolemManager* sm = NodeManager::currentNM()->getSkolemManager(); - Node k = sm->mkDummySkolem("slv", tn); + Node k = NodeManager::mkDummySkolem("slv", tn); d_solve_var[tn] = k; return k; } diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index 4a577745b27..2e55809a920 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -645,7 +645,6 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma( if (d_opts.quantifiers.cegqiBvRmExtract) { NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); Trace("cegqi-bv-pp") << "-----remove extracts..." << std::endl; // map from terms to bitvector extracts applied to that term std::map > extract_map; @@ -694,10 +693,10 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma( Assert(boundaries[i - 1] > 0); Node ex = bv::utils::mkExtract( es.first, boundaries[i - 1] - 1, boundaries[i]); - Node var = - sm->mkDummySkolem("ek", - ex.getType(), - "variable to represent disjoint extract region"); + Node var = NodeManager::mkDummySkolem( + "ek", + ex.getType(), + "variable to represent disjoint extract region"); children.push_back(var); vars.push_back(var); } diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 0c222f064c4..4520b321710 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -491,8 +491,7 @@ Node InstStrategyCegqi::getCounterexampleLiteral(Node q) return it->second; } NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); - Node g = sm->mkDummySkolem("g", nm->booleanType()); + Node g = NodeManager::mkDummySkolem("g", nm->booleanType()); // ensure that it is a SAT literal Node ceLit = d_qstate.getValuation().ensureLiteral(g); d_ce_lit[q] = ceLit; diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 697412066da..3c0b2ada994 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -1116,9 +1116,8 @@ 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(); - SkolemManager* sm = nm->getSkolemManager(); TypeNode op_tn = nm->mkFunctionType(tn, nm->booleanType()); - Node op = sm->mkDummySkolem( + Node op = NodeManager::mkDummySkolem( "PE", op_tn, "was created by conjecture ground term enumerator."); d_typ_pred[tn] = op; return op; diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp index 639fd742182..004e590bd6d 100644 --- a/src/theory/quantifiers/dynamic_rewrite.cpp +++ b/src/theory/quantifiers/dynamic_rewrite.cpp @@ -149,7 +149,6 @@ Node DynamicRewriter::toExternal(Node ai) Node DynamicRewriter::OpInternalSymTrie::getSymbol(Node n) { NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); std::vector ctypes; for (const Node& cn : n) { @@ -181,7 +180,8 @@ Node DynamicRewriter::OpInternalSymTrie::getSymbol(Node n) { utype = nm->mkFunctionType(ctypes); } - Node f = sm->mkDummySkolem("ufd", utype, "internal op for dynamic_rewriter"); + Node f = NodeManager::mkDummySkolem( + "ufd", utype, "internal op for dynamic_rewriter"); curr->d_sym = f; return f; } diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 46dc994bed0..e8aa916ca3b 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -39,13 +39,11 @@ Node ExprMiner::convertToSkolem(Node n) { if (d_skolems.empty()) { - NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); for (const Node& v : d_vars) { std::stringstream ss; ss << "k_" << v; - Node sk = sm->mkDummySkolem(ss.str(), v.getType()); + Node sk = NodeManager::mkDummySkolem(ss.str(), v.getType()); d_skolems.push_back(sk); d_fv_to_skolem[v] = sk; } diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 0c29787e2f7..29a5e491f7c 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -50,8 +50,8 @@ BoundedIntegers::IntRangeDecisionHeuristic::IntRangeDecisionHeuristic( // we require a proxy if the term is set.card if (options().quantifiers.fmfBoundLazy || r.getKind() == Kind::SET_CARD) { - SkolemManager* sm = nodeManager()->getSkolemManager(); - d_proxy_range = isProxy ? r : sm->mkDummySkolem("pbir", r.getType()); + d_proxy_range = + isProxy ? r : NodeManager::mkDummySkolem("pbir", r.getType()); } else { @@ -397,7 +397,6 @@ void BoundedIntegers::checkOwnership(Node f) } NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); bool success; do{ @@ -565,7 +564,7 @@ void BoundedIntegers::checkOwnership(Node f) { // introduce a new bound Node new_range = - sm->mkDummySkolem("bir", r.getType(), "bound for term"); + NodeManager::mkDummySkolem("bir", r.getType(), "bound for term"); d_nground_range[f][v] = r; d_range[f][v] = new_range; r = new_range; @@ -978,8 +977,7 @@ Node BoundedIntegers::mkBoundedForall(NodeManager* nm, Node bvl, Node body) } else { - SkolemManager* sm = nm->getSkolemManager(); - qvar = sm->mkDummySkolem("qinternal", nm->booleanType()); + qvar = NodeManager::mkDummySkolem("qinternal", nm->booleanType()); // this dummy variable marks that the quantified formula is internal qvar.setAttribute(BoundedQuantAttribute(), true); // remember the dummy variable diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp index b4f004f0e94..9be1bf8a420 100644 --- a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp +++ b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp @@ -92,9 +92,8 @@ Node FirstOrderModelFmc::getStar(TypeNode tn) { return it->second; } - SkolemManager* sm = nodeManager()->getSkolemManager(); - Node st = - sm->mkDummySkolem("star", tn, "skolem created for full-model checking"); + Node st = NodeManager::mkDummySkolem( + "star", tn, "skolem created for full-model checking"); d_type_star[tn] = st; st.setAttribute(IsStarAttribute(), true); return st; diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 52a5a84f6d5..5eb214ec64a 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -1494,7 +1494,6 @@ void FullModelChecker::registerQuantifiedFormula(Node q) return; } NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); std::vector types; for (const Node& v : q[0]) { @@ -1509,7 +1508,8 @@ void FullModelChecker::registerQuantifiedFormula(Node q) types.push_back(tn); } TypeNode typ = nm->mkFunctionType(types, nm->booleanType()); - Node op = sm->mkDummySkolem("qfmc", typ, "op for full-model checking"); + Node op = + NodeManager::mkDummySkolem("qfmc", typ, "op for full-model checking"); d_quant_cond[q] = op; } diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 00551b5d177..9770a1742d4 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -112,7 +112,7 @@ QuantifiersRewriter::QuantifiersRewriter(NodeManager* nm, TheoryRewriteCtx::PRE_DSL); registerProofRewriteRule(ProofRewriteRule::MACRO_QUANT_MINISCOPE, TheoryRewriteCtx::PRE_DSL); - // QUANT_MINISCOPE is part of the reconstruction for MACRO_QUANT_MINISCOPE + // QUANT_MINISCOPE_OR is part of the reconstruction for MACRO_QUANT_MINISCOPE registerProofRewriteRule(ProofRewriteRule::MACRO_QUANT_PARTITION_CONNECTED_FV, TheoryRewriteCtx::PRE_DSL); // note ProofRewriteRule::QUANT_DT_SPLIT is done by a module dynamically with @@ -201,7 +201,12 @@ Node QuantifiersRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n) break; case ProofRewriteRule::MACRO_QUANT_MINISCOPE: { - if (n.getKind() != Kind::FORALL || n[1].getKind() != Kind::AND) + if (n.getKind() != Kind::FORALL) + { + return Node::null(); + } + Kind k = n[1].getKind(); + if (k != Kind::AND && k != Kind::ITE) { return Node::null(); } @@ -210,11 +215,13 @@ Node QuantifiersRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n) QAttributes qa; QuantAttributes::computeQuantAttributes(n, qa); Node nret = computeMiniscoping(n, qa, true, false); - Assert(nret != n); - return nret; + if (nret != n) + { + return nret; + } } break; - case ProofRewriteRule::QUANT_MINISCOPE: + case ProofRewriteRule::QUANT_MINISCOPE_AND: { if (n.getKind() != Kind::FORALL || n[1].getKind() != Kind::AND) { @@ -252,7 +259,7 @@ Node QuantifiersRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n) } } break; - case ProofRewriteRule::QUANT_MINISCOPE_FV: + case ProofRewriteRule::QUANT_MINISCOPE_OR: { if (n.getKind() != Kind::FORALL || n[1].getKind() != Kind::OR) { @@ -305,6 +312,23 @@ Node QuantifiersRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n) return ret; } break; + case ProofRewriteRule::QUANT_MINISCOPE_ITE: + { + if (n.getKind() != Kind::FORALL || n[1].getKind() != Kind::ITE) + { + return Node::null(); + } + std::vector args(n[0].begin(), n[0].end()); + Node body = n[1]; + if (!expr::hasSubterm(body[0], args)) + { + return d_nm->mkNode(Kind::ITE, + body[0], + d_nm->mkNode(Kind::FORALL, n[0], body[1]), + d_nm->mkNode(Kind::FORALL, n[0], body[2])); + } + } + break; case ProofRewriteRule::QUANT_DT_SPLIT: { // always runs split utility on the first variable @@ -1989,8 +2013,7 @@ Node QuantifiersRewriter::mkForall(const std::vector& args, children.push_back(body); if (marked) { - SkolemManager* sm = nm->getSkolemManager(); - Node avar = sm->mkDummySkolem("id", nm->booleanType()); + Node avar = NodeManager::mkDummySkolem("id", nm->booleanType()); QuantIdNumAttribute ida; avar.setAttribute(ida, 0); iplc.push_back(nm->mkNode(Kind::INST_ATTRIBUTE, avar)); @@ -2011,16 +2034,26 @@ Node QuantifiersRewriter::computeMiniscoping(Node q, NodeManager* nm = nodeManager(); std::vector args(q[0].begin(), q[0].end()); Node body = q[1]; - if (body.getKind() == Kind::AND) + Kind k = body.getKind(); + if (k == Kind::AND || k == Kind::ITE) { + bool doRewrite = miniscopeConj; + if (k == Kind::ITE) + { + // ITE miniscoping is only valid if condition contains no variables + if (expr::hasSubterm(body[0], args)) + { + doRewrite = false; + } + } // aggressive miniscoping implies that structural miniscoping should // be applied first - if (miniscopeConj) + if (doRewrite) { BoundVarManager* bvm = nm->getBoundVarManager(); // Break apart the quantifed formula // forall x. P1 ^ ... ^ Pn ---> forall x. P1 ^ ... ^ forall x. Pn - NodeBuilder t(nm, Kind::AND); + NodeBuilder t(nm, k); std::vector argsc; for (size_t i = 0, nchild = body.getNumChildren(); i < nchild; i++) { diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp index e0a451e97c3..96f648cd643 100644 --- a/src/theory/quantifiers/single_inv_partition.cpp +++ b/src/theory/quantifiers/single_inv_partition.cpp @@ -185,7 +185,6 @@ bool SingleInvocationPartition::init(std::vector& funcs, Assert(d_input_funcs.empty()); Assert(d_si_vars.empty()); NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); d_has_input_funcs = has_funcs; d_arg_types.insert(d_arg_types.end(), typs.begin(), typs.end()); d_input_funcs.insert(d_input_funcs.end(), funcs.begin(), funcs.end()); @@ -200,7 +199,7 @@ bool SingleInvocationPartition::init(std::vector& funcs, Assert(d_si_vars.size() == d_arg_types.size()); for (const Node& inf : d_input_funcs) { - Node sk = sm->mkDummySkolem("_sik", inf.getType()); + Node sk = NodeManager::mkDummySkolem("_sik", inf.getType()); d_input_func_sks.push_back(sk); } Trace("si-prt") << "SingleInvocationPartition::process " << n << std::endl; diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 661c14a70d5..b49e66c1ecf 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -197,7 +197,6 @@ Node Skolemize::mkSkolemizedBodyInduction(const Options& opts, { argTypes.push_back(v.getType()); } - SkolemManager* sm = nm->getSkolemManager(); Assert(sk.empty() || sk.size() == f[0].getNumChildren()); // calculate the variables and substitution std::vector ind_vars; @@ -228,7 +227,7 @@ Node Skolemize::mkSkolemizedBodyInduction(const Options& opts, else { TypeNode typ = nm->mkFunctionType(argTypes, f[0][i].getType()); - Node op = sm->mkDummySkolem( + Node op = NodeManager::mkDummySkolem( "skop", typ, "op created during pre-skolemization"); // DOTHIS: set attribute on op, marking that it should not be selected // as trigger diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index eca3a5def33..dab0d0cc7fd 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -143,7 +143,6 @@ void CegSingleInv::finishInit(bool syntaxRestricted) return; } NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); d_single_inv = d_sip->getSingleInvocation(); d_single_inv = TermUtil::simpleNegate(d_single_inv); std::vector func_vars; @@ -159,8 +158,8 @@ void CegSingleInv::finishInit(bool syntaxRestricted) d_sip->getSingleInvocationVariables(sivars); for (unsigned i = 0, size = sivars.size(); i < size; i++) { - Node v = - sm->mkDummySkolem("a", sivars[i].getType(), "single invocation arg"); + Node v = NodeManager::mkDummySkolem( + "a", sivars[i].getType(), "single invocation arg"); d_single_inv_arg_sk.push_back(v); } d_single_inv = d_single_inv.substitute(sivars.begin(), diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 4ea4b6b908b..f2fe2008b12 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -423,8 +423,7 @@ CegisUnifEnumDecisionStrategy::CegisUnifEnumDecisionStrategy( Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) { NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); - Node newLit = sm->mkDummySkolem("G_cost", nm->booleanType()); + Node newLit = NodeManager::mkDummySkolem("G_cost", nm->booleanType()); unsigned new_size = n + 1; // allocate an enumerator for each candidate @@ -432,13 +431,13 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) { Node c = ci.first; TypeNode ct = c.getType(); - Node eu = sm->mkDummySkolem("eu", ct); + Node eu = NodeManager::mkDummySkolem("eu", ct); Node ceu; if (!d_useCondPool && !ci.second.d_enums[0].empty()) { // make a new conditional enumerator as well, starting the // second type around - ceu = sm->mkDummySkolem("cu", ci.second.d_ce_type); + ceu = NodeManager::mkDummySkolem("cu", ci.second.d_ce_type); } // register the new enumerators for (unsigned index = 0; index < 2; index++) @@ -474,7 +473,7 @@ Node CegisUnifEnumDecisionStrategy::mkLiteral(unsigned n) NodeManager::mkBoundVar("_virtual_enum_grammar", nm->integerType()); SygusGrammar g({}, {a}); g.addRules(a, {nm->mkConstInt(Rational(1)), nm->mkNode(Kind::ADD, a, a)}); - d_virtual_enum = sm->mkDummySkolem("_ve", g.resolve()); + d_virtual_enum = NodeManager::mkDummySkolem("_ve", g.resolve()); d_tds->registerEnumerator( d_virtual_enum, Node::null(), d_parent, ROLE_ENUM_CONSTRAINED); } @@ -517,7 +516,6 @@ void CegisUnifEnumDecisionStrategy::initialize( } // initialize type information for candidates NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); for (const Node& e : es) { Trace("cegis-unif-enum-debug") << "...adding strategy point " << e << "\n"; @@ -563,7 +561,7 @@ void CegisUnifEnumDecisionStrategy::initialize( // allocate a condition enumerator for each candidate for (std::pair& ci : d_ce_info) { - Node ceu = sm->mkDummySkolem("cu", ci.second.d_ce_type); + Node ceu = NodeManager::mkDummySkolem("cu", ci.second.d_ce_type); setUpEnumerator(ceu, ci.second, 1); } } diff --git a/src/theory/quantifiers/sygus/rcons_type_info.cpp b/src/theory/quantifiers/sygus/rcons_type_info.cpp index ad80aafd6a0..b1497732da6 100644 --- a/src/theory/quantifiers/sygus/rcons_type_info.cpp +++ b/src/theory/quantifiers/sygus/rcons_type_info.cpp @@ -33,16 +33,14 @@ void RConsTypeInfo::initialize(Env& env, TypeNode stn, const std::vector& builtinVars) { - NodeManager* nm = env.getNodeManager(); - SkolemManager* sm = nm->getSkolemManager(); // create a terms enumerator d_enumerators.push_back( std::make_unique(env, tds, nullptr, &s, false)); - d_enumerators[0]->initialize(sm->mkDummySkolem("sygus_rcons", stn)); + d_enumerators[0]->initialize(NodeManager::mkDummySkolem("sygus_rcons", stn)); // create a patterns enumerator d_enumerators.push_back( std::make_unique(env, tds, nullptr, &s, true)); - d_enumerators[1]->initialize(sm->mkDummySkolem("sygus_rcons", stn)); + d_enumerators[1]->initialize(NodeManager::mkDummySkolem("sygus_rcons", stn)); d_crd.reset(new CandidateRewriteDatabase(env, true, false, false)); // since initial samples are not always useful for equivalence checks, set diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index fbb72ac7153..0ee24218e12 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -42,7 +42,6 @@ Node SygusAbduct::mkAbductionConjecture(NodeManager* nm, const std::vector& axioms, TypeNode abdGType) { - SkolemManager* sm = nm->getSkolemManager(); std::unordered_set symset; for (size_t i = 0, size = asserts.size(); i < size; i++) { @@ -170,7 +169,7 @@ Node SygusAbduct::mkAbductionConjecture(NodeManager* nm, Node vbvl = nm->mkNode(Kind::BOUND_VAR_LIST, vars); sc = nm->mkNode(Kind::EXISTS, vbvl, sc); } - Node sygusScVar = sm->mkDummySkolem("sygus_sc", nm->booleanType()); + Node sygusScVar = NodeManager::mkDummySkolem("sygus_sc", nm->booleanType()); sygusScVar.setAttribute(theory::SygusSideConditionAttribute(), sc); Node instAttr = nm->mkNode(Kind::INST_ATTRIBUTE, sygusScVar); // build in the side condition diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp index e5e64983fd3..39683020e2c 100644 --- a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp +++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp @@ -36,7 +36,6 @@ Node SygusQePreproc::preprocess(Node q) body = body[0][1]; } NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); Trace("cegqi-qep") << "Compute single invocation for " << q << "..." << std::endl; quantifiers::SingleInvocationPartition sip(d_env); @@ -86,7 +85,7 @@ Node SygusQePreproc::preprocess(Node q) // skolemize non-qe variables for (unsigned i = 0, size = nqe_vars.size(); i < size; i++) { - Node k = sm->mkDummySkolem( + Node k = NodeManager::mkDummySkolem( "k", nqe_vars[i].getType(), "qe for non-ground single invocation"); orig.push_back(nqe_vars[i]); subs.push_back(k); @@ -102,7 +101,7 @@ Node SygusQePreproc::preprocess(Node q) Node fv = sip.getFirstOrderVariableForFunction(f); Assert(!fi.isNull()); orig.push_back(fi); - Node k = sm->mkDummySkolem( + Node k = NodeManager::mkDummySkolem( "k", fv.getType(), "qe for function in non-ground single invocation"); subs.push_back(k); Trace("cegqi-qep") << " subs : " << fi << " -> " << k << std::endl; diff --git a/src/theory/quantifiers/sygus/sygus_random_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_random_enumerator.cpp index afa8b96b2e1..14fbdb8f755 100644 --- a/src/theory/quantifiers/sygus/sygus_random_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_random_enumerator.cpp @@ -73,11 +73,10 @@ bool SygusRandomEnumerator::increment() Node SygusRandomEnumerator::incrementH() { NodeManager* nm = nodeManager(); - SkolemManager* sm = nodeManager()->getSkolemManager(); Random& rnd = Random::getRandom(); double p = options().quantifiers.sygusEnumRandomP; - Node mainSkolem = sm->mkDummySkolem("sygus_rand", d_tn); + Node mainSkolem = NodeManager::mkDummySkolem("sygus_rand", d_tn); // List of skolems with no corresponding constructor. std::vector remainingSkolems; remainingSkolems.push_back(mainSkolem); @@ -125,7 +124,7 @@ Node SygusRandomEnumerator::incrementH() for (size_t i = 0, n = skolemCons[currSkolem]->getNumArgs(); i < n; ++i) { TypeNode subSkolemType = skolemCons[currSkolem]->getArgType(i); - Node subSkolem = sm->mkDummySkolem("sygus_rand", subSkolemType); + Node subSkolem = NodeManager::mkDummySkolem("sygus_rand", subSkolemType); remainingSkolems.push_back(subSkolem); subSkolems[currSkolem].push_back(subSkolem); } diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 8df3b6b8eb5..51656ae4b50 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -138,7 +138,6 @@ Node SygusUnifRl::purifyLemma(Node n, bool childChanged = false; std::vector children; NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); for (unsigned i = 0; i < size; ++i) { if (i == 0 && fapp) @@ -188,7 +187,7 @@ Node SygusUnifRl::purifyLemma(Node n, // Build purified head with fresh skolem and recreate node std::stringstream ss; ss << nb[0] << "_" << d_cand_to_hd_count[nb[0]]++; - Node new_f = sm->mkDummySkolem( + Node new_f = NodeManager::mkDummySkolem( ss.str(), nb[0].getType(), "head of unif evaluation point"); // Adds new enumerator to map from candidate Trace("sygus-unif-rl-purify") diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index 576865cb987..085edb68dcc 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -173,7 +173,6 @@ void SygusUnifStrategy::registerStrategyPoint(Node et, void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole) { NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); if (d_tinfo.find(tn) == d_tinfo.end()) { // register type @@ -196,7 +195,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole) std::map::iterator iten = eti.d_enum.find(erole); if (iten == eti.d_enum.end()) { - ee = sm->mkDummySkolem("ee", tn); + ee = NodeManager::mkDummySkolem("ee", tn); eti.d_enum[erole] = ee; Trace("sygus-unif-debug") << "...enumerator " << ee << " for " << tn.getDType().getName() @@ -247,7 +246,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole) for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++) { TypeNode ttn = dt[j][k].getRangeType(); - Node kv = sm->mkDummySkolem("ut", ttn); + Node kv = NodeManager::mkDummySkolem("ut", ttn); sks.push_back(kv); cop_to_sks[cop].push_back(kv); sktns.push_back(ttn); @@ -305,7 +304,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole) << std::endl; Node esk = nm->mkNode(Kind::DT_SYGUS_EVAL, echildren); vs.push_back(esk); - Node tvar = sm->mkDummySkolem("templ", esk.getType()); + Node tvar = NodeManager::mkDummySkolem("templ", esk.getType()); templ_var_index[tvar] = k; Trace("sygus-unif-debug2") << "* template inference : looking for " << tvar << " for arg " << k << std::endl; @@ -576,7 +575,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole) if (cop_to_child_templ[cop].find(j) != cop_to_child_templ[cop].end()) { // it is templated, allocate a fresh variable - et = sm->mkDummySkolem("et", ct); + et = NodeManager::mkDummySkolem("et", ct); Trace("sygus-unif-debug") << "...enumerate " << et << " of type " << ct.getDType().getName(); Trace("sygus-unif-debug") << " for arg " << j << " of " diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index d44daa00ad4..e21f50e429b 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -244,7 +244,7 @@ void SynthConjecture::assign(Node q) { for (const Node& v : d_checkBody[0][0]) { - Node sk = sm->mkDummySkolem("rsk", v.getType()); + Node sk = NodeManager::mkDummySkolem("rsk", v.getType()); bsubs.add(v, sk); d_innerVars.push_back(v); d_innerSks.push_back(sk); diff --git a/src/theory/quantifiers/sygus/template_infer.cpp b/src/theory/quantifiers/sygus/template_infer.cpp index 523958d8d34..e34d93d7d51 100644 --- a/src/theory/quantifiers/sygus/template_infer.cpp +++ b/src/theory/quantifiers/sygus/template_infer.cpp @@ -87,7 +87,6 @@ void SygusTemplateInfer::initialize(Node q) } Assert(prog == q[0][0]); NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); // map the program back via non-single invocation map std::vector prog_templ_vars; d_ti.getVariables(prog_templ_vars); @@ -102,7 +101,7 @@ void SygusTemplateInfer::initialize(Node q) { atn = atn.getRangeType(); } - d_templ_arg[prog] = sm->mkDummySkolem("I", atn); + d_templ_arg[prog] = NodeManager::mkDummySkolem("I", atn); // construct template Node templ; diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 5e997633d43..54b30c35769 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -102,8 +102,7 @@ Node TermDbSygus::getProxyVariable(TypeNode tn, Node c) Node k; if (anyC == -1) { - SkolemManager* sm = nm->getSkolemManager(); - k = sm->mkDummySkolem("sy", tn, "sygus proxy"); + k = NodeManager::mkDummySkolem("sy", tn, "sygus proxy"); SygusPrintProxyAttribute spa; k.setAttribute(spa, c); } @@ -517,9 +516,8 @@ void TermDbSygus::registerEnumerator(Node e, // populate a pool of terms, or (some cases) of when it is actively generated. if (isActiveGen || erole == ROLE_ENUM_POOL) { - SkolemManager* sm = nm->getSkolemManager(); // make the guard - Node ag = sm->mkDummySkolem("eG", nm->booleanType()); + Node ag = NodeManager::mkDummySkolem("eG", nm->booleanType()); // must ensure it is a literal immediately here ag = d_qstate.getValuation().ensureLiteral(ag); // must ensure that it is asserted as a literal before we begin solving diff --git a/src/theory/quantifiers/sygus/transition_inference.cpp b/src/theory/quantifiers/sygus/transition_inference.cpp index 7e70d3247fc..f5fc8d1fb73 100644 --- a/src/theory/quantifiers/sygus/transition_inference.cpp +++ b/src/theory/quantifiers/sygus/transition_inference.cpp @@ -199,7 +199,6 @@ void TransitionInference::process(Node n, Node f) void TransitionInference::process(Node n) { NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); d_complete = true; d_trivial = true; std::vector n_check; @@ -279,7 +278,7 @@ void TransitionInference::process(Node n) { for (unsigned j = 0, nchild = next.getNumChildren(); j < nchild; j++) { - Node v = sm->mkDummySkolem( + Node v = NodeManager::mkDummySkolem( "ir", next[j].getType(), "template inference rev argument"); d_prime_vars.push_back(v); } @@ -428,12 +427,10 @@ bool TransitionInference::processDisjunct( d_trivial = false; d_func = op; Trace("cegqi-inv-debug") << "Use " << op << " with args "; - NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); for (const Node& l : lit) { - Node v = - sm->mkDummySkolem("i", l.getType(), "template inference argument"); + Node v = NodeManager::mkDummySkolem( + "i", l.getType(), "template inference argument"); d_vars.push_back(v); Trace("cegqi-inv-debug") << v << " "; } diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index 24af5118d99..793a62b3160 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -503,8 +503,7 @@ Node SygusInst::getCeLiteral(Node q) } NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); - Node sk = sm->mkDummySkolem("CeLiteral", nm->booleanType()); + Node sk = NodeManager::mkDummySkolem("CeLiteral", nm->booleanType()); Node lit = d_qstate.getValuation().ensureLiteral(sk); d_ce_lits[q] = lit; return lit; diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index a3086b4d818..bbe42d6e1ee 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -340,7 +340,6 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) TNode satom = atom.getKind() == Kind::SEP_LABEL ? atom[0] : atom; TNode slbl = atom.getKind() == Kind::SEP_LABEL ? atom[1] : TNode::null(); NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); if (slbl.isNull()) { Trace("sep-lemma-debug") @@ -446,8 +445,8 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) else { Assert(!d_type_ref.isNull()); - Node kl = sm->mkDummySkolem("loc", d_type_ref); - Node kd = sm->mkDummySkolem("data", d_type_data); + Node kl = NodeManager::mkDummySkolem("loc", d_type_ref); + Node kd = NodeManager::mkDummySkolem("data", d_type_data); Node econc = nm->mkNode( Kind::SEP_LABEL, nm->mkNode( @@ -479,7 +478,7 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) Trace("sep-lemma-debug") << "Negated spatial constraint asserted to sep theory: " << fact << std::endl; - Node g = sm->mkDummySkolem("G", nm->booleanType()); + Node g = NodeManager::mkDummySkolem("G", nm->booleanType()); d_neg_guard_strategy[g].reset(new DecisionStrategySingleton( d_env, "sep_neg_guard", g, getValuation())); DecisionStrategySingleton* ds = d_neg_guard_strategy[g].get(); @@ -520,7 +519,6 @@ void TheorySep::postCheck(Effort level) return; } NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); Trace("sep-process") << "Checking heap at full effort..." << std::endl; d_label_model.clear(); d_tmodel.clear(); @@ -836,7 +834,7 @@ void TheorySep::postCheck(Effort level) { Trace("sep-process") << "Must witness label : " << ll << ", data type is " << d_type_data << std::endl; - Node dsk = sm->mkDummySkolem( + Node dsk = NodeManager::mkDummySkolem( "dsk", d_type_data, "pto-data for implicit location"); // if location is in the heap, then something must point to it Node lem = nm->mkNode( @@ -1122,8 +1120,6 @@ void TheorySep::initializeBounds() { { return; } - NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); Trace("sep-bound") << "Initialize bounds for " << d_type_ref << "..." << std::endl; size_t n_emp = 0; @@ -1144,7 +1140,7 @@ void TheorySep::initializeBounds() { << std::endl; for (size_t r = 0; r < n_emp; r++) { - Node e = sm->mkDummySkolem( + Node e = NodeManager::mkDummySkolem( "e", d_type_ref, "cardinality bound element for seplog"); d_type_references_card.push_back(e); d_type_ref_card_id[e] = r; @@ -1158,19 +1154,18 @@ Node TheorySep::getBaseLabel() return d_base_label; } NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); initializeBounds(); Trace("sep") << "Make base label for " << d_type_ref << std::endl; std::stringstream ss; ss << "__Lb"; TypeNode ltn = nm->mkSetType(d_type_ref); - Node n_lbl = sm->mkDummySkolem(ss.str(), ltn, "base label"); + Node n_lbl = NodeManager::mkDummySkolem(ss.str(), ltn, "base label"); d_base_label = n_lbl; // make reference bound Trace("sep") << "Make reference bound label for " << d_type_ref << std::endl; std::stringstream ss2; ss2 << "__Lu"; - d_reference_bound = sm->mkDummySkolem(ss2.str(), ltn, ""); + d_reference_bound = NodeManager::mkDummySkolem(ss2.str(), ltn, ""); // check whether monotonic (elements can be added to tn without effecting // satisfiability) @@ -1280,17 +1275,18 @@ Node TheorySep::mkUnion( TypeNode tn, std::vector< Node >& locs ) { Node TheorySep::getLabel( Node atom, int child, Node lbl ) { std::map< int, Node >::iterator it = d_label_map[atom][lbl].find( child ); - if( it==d_label_map[atom][lbl].end() ){ - NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); + if (it == d_label_map[atom][lbl].end()) + { Assert(!d_type_ref.isNull()); std::stringstream ss; ss << "__Lc" << child; TypeNode ltn = nodeManager()->mkSetType(d_type_ref); - Node n_lbl = sm->mkDummySkolem(ss.str(), ltn, "sep label"); + Node n_lbl = NodeManager::mkDummySkolem(ss.str(), ltn, "sep label"); d_label_map[atom][lbl][child] = n_lbl; return n_lbl; - }else{ + } + else + { return (*it).second; } } diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index 3a400b93912..486494b888f 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -1063,7 +1063,6 @@ void CardinalityExtension::mkModelValueElementsFor( std::uint32_t vu = v.getConst().getNumerator().toUnsignedInt(); Assert(els.size() <= vu); NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); if (elementTypeFinite) { // get all members of this finite type @@ -1083,7 +1082,7 @@ void CardinalityExtension::mkModelValueElementsFor( // slack elements for the leaves without worrying about conflicts with // the current members of this finite type. - Node slack = sm->mkDummySkolem("slack", elementType); + Node slack = NodeManager::mkDummySkolem("slack", elementType); Node singleton = nm->mkNode(Kind::SET_SINGLETON, slack); els.push_back(singleton); d_finite_type_slack_elements[elementType].push_back(slack); @@ -1092,8 +1091,9 @@ void CardinalityExtension::mkModelValueElementsFor( } else { - els.push_back(nm->mkNode(Kind::SET_SINGLETON, - sm->mkDummySkolem("msde", elementType))); + els.push_back( + nm->mkNode(Kind::SET_SINGLETON, + NodeManager::mkDummySkolem("msde", elementType))); } } } diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index c63ed0b2efc..961ab0e86ec 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -186,4 +186,9 @@ parameterized RELATION_TABLE_JOIN RELATION_TABLE_JOIN_OP 2 "relation table join" typerule RELATION_TABLE_JOIN_OP "SimpleTypeRule" typerule RELATION_TABLE_JOIN ::cvc5::internal::theory::sets::RelationTableJoinTypeRule +# for RARE + +operator SET_EMPTY_OF_TYPE 1 "the empty set whose argument represents its type" +typerule SET_EMPTY_OF_TYPE ::cvc5::internal::theory::sets::SetEmptyOfTypeTypeRule + endtheory diff --git a/src/theory/sets/rewrites b/src/theory/sets/rewrites index 415db21a690..be9f3baca72 100644 --- a/src/theory/sets/rewrites +++ b/src/theory/sets/rewrites @@ -1,7 +1,7 @@ ; Equality (define-cond-rule sets-eq-singleton-emp ((x ?Set) (y ?)) - (set.is_empty x) + (= x (@set.empty_of_type (@type_of x))) (= x (set.singleton y)) false) @@ -10,7 +10,7 @@ (= x y)) (define-cond-rule sets-member-emp ((x ?) (y ?Set)) - (set.is_empty y) + (= y (@set.empty_of_type (@type_of y))) (set.member x y) false) @@ -26,27 +26,27 @@ (set.inter y x)) (define-cond-rule sets-inter-emp1 ((x ?Set) (y ?Set)) - (set.is_empty x) + (= x (@set.empty_of_type (@type_of x))) (set.inter x y) x) (define-cond-rule sets-inter-emp2 ((x ?Set) (y ?Set)) - (set.is_empty y) + (= y (@set.empty_of_type (@type_of y))) (set.inter x y) y) (define-cond-rule sets-minus-emp1 ((x ?Set) (y ?Set)) - (set.is_empty x) + (= x (@set.empty_of_type (@type_of x))) (set.minus x y) x) (define-cond-rule sets-minus-emp2 ((x ?Set) (y ?Set)) - (set.is_empty y) + (= y (@set.empty_of_type (@type_of y))) (set.minus x y) x) (define-cond-rule sets-union-emp1 ((x ?Set) (y ?Set)) - (set.is_empty x) + (= x (@set.empty_of_type (@type_of x))) (set.union x y) y) (define-cond-rule sets-union-emp2 ((x ?Set) (y ?Set)) - (set.is_empty y) + (= y (@set.empty_of_type (@type_of y))) (set.union x y) x) @@ -77,8 +77,16 @@ (- (set.card s) (set.card (set.inter s t)))) (define-cond-rule sets-card-emp ((x ?Set)) - (set.is_empty x) + (= x (@set.empty_of_type (@type_of x))) (set.card x) 0) +(define-rule sets-minus-self ((x ?Set)) + (set.minus x x) + (@set.empty_of_type (@type_of x))) + ; (set.complement S) ---> (set.minus (as set.universe (Set Int)) S) + +(define-rule sets-is-empty-elim ((x ?Set)) + (set.is_empty x) + (= x (@set.empty_of_type (@type_of x)))) diff --git a/src/theory/sets/skolem_cache.cpp b/src/theory/sets/skolem_cache.cpp index d5e61f6723d..c5af14a274b 100644 --- a/src/theory/sets/skolem_cache.cpp +++ b/src/theory/sets/skolem_cache.cpp @@ -49,7 +49,7 @@ Node SkolemCache::mkTypedSkolemCached( } else { - sk = sm->mkDummySkolem(c, tn, "sets skolem"); + sk = NodeManager::mkDummySkolem(c, tn, "sets skolem"); } d_skolemCache[a][b][id] = sk; d_allSkolems.insert(sk); @@ -67,8 +67,7 @@ Node SkolemCache::mkTypedSkolemCached(TypeNode tn, Node SkolemCache::mkTypedSkolem(TypeNode tn, const char* c) { - SkolemManager* sm = d_nm->getSkolemManager(); - Node n = sm->mkDummySkolem(c, tn, "sets skolem"); + Node n = NodeManager::mkDummySkolem(c, tn, "sets skolem"); d_allSkolems.insert(n); return n; } diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index c66c4f63b60..cc1f55d3cc9 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -432,7 +432,6 @@ void TheorySetsRels::check(Theory::Effort level) } } NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); Node reason = exp; Node conclusion = d_trueNode; std::vector< Node > distinct_skolems; @@ -443,7 +442,7 @@ void TheorySetsRels::check(Theory::Effort level) Kind::AND, reason, nm->mkNode(Kind::EQUAL, exp[1], join_image_term)); } for( unsigned int i = 0; i < min_card; i++ ) { - Node skolem = sm->mkDummySkolem( + Node skolem = NodeManager::mkDummySkolem( "jig", join_image_rel.getType()[0].getTupleTypes()[0]); distinct_skolems.push_back( skolem ); conclusion = nm->mkNode( 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/sets/theory_sets_type_rules.cpp b/src/theory/sets/theory_sets_type_rules.cpp index 32a0bc83463..985a1f1bceb 100644 --- a/src/theory/sets/theory_sets_type_rules.cpp +++ b/src/theory/sets/theory_sets_type_rules.cpp @@ -1246,6 +1246,19 @@ TypeNode RelationProjectTypeRule::computeType(NodeManager* nm, return nm->mkSetType(retTupleType); } +TypeNode SetEmptyOfTypeTypeRule::preComputeType(NodeManager* nm, TNode n) +{ + return TypeNode::null(); +} + +TypeNode SetEmptyOfTypeTypeRule::computeType(NodeManager* nm, + TNode n, + bool check, + std::ostream* errOut) +{ + return nm->mkAbstractType(Kind::SET_TYPE); +} + Cardinality SetsProperties::computeCardinality(TypeNode type) { Assert(type.getKind() == Kind::SET_TYPE); diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 91b9f251a0e..b74b555acfa 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -396,6 +396,19 @@ struct RelationAggregateTypeRule std::ostream* errOut); }; /* struct RelationAggregateTypeRule */ +/** + * Type rule for set.empty_of_type + */ +struct SetEmptyOfTypeTypeRule +{ + static TypeNode preComputeType(NodeManager* nm, TNode n); + + static TypeNode computeType(NodeManager* nodeManager, + TNode n, + bool check, + std::ostream* errOut); +}; + struct SetsProperties { static Cardinality computeCardinality(TypeNode type); diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp index 82f3372a802..4dd8959562c 100644 --- a/src/theory/sort_inference.cpp +++ b/src/theory/sort_inference.cpp @@ -604,9 +604,8 @@ TypeNode SortInference::getTypeForId( int t ){ } } -Node SortInference::getNewSymbol( Node old, TypeNode tn ){ - NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); +Node SortInference::getNewSymbol(Node old, TypeNode tn) +{ // if no sort was inferred for this node, return original if (tn.isNull() || tn == old.getType()) { @@ -618,7 +617,7 @@ Node SortInference::getNewSymbol( Node old, TypeNode tn ){ if( d_const_map[tn].find( old )==d_const_map[tn].end() ){ std::stringstream ss; ss << "ic_" << tn << "_" << old; - d_const_map[tn][old] = sm->mkDummySkolem( + d_const_map[tn][old] = NodeManager::mkDummySkolem( ss.str(), tn, "constant created during sort inference"); // use mkConst??? @@ -633,7 +632,8 @@ Node SortInference::getNewSymbol( Node old, TypeNode tn ){ } std::stringstream ss; ss << "i_" << old; - return sm->mkDummySkolem(ss.str(), tn, "created during sort inference"); + return NodeManager::mkDummySkolem( + ss.str(), tn, "created during sort inference"); } Node SortInference::simplifyNode( @@ -648,7 +648,6 @@ Node SortInference::simplifyNode( return itv->second; }else{ NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); Trace("sort-inference-debug2") << "Simplify " << n << ", type context=" << tnn << std::endl; std::vector< Node > children; std::map< Node, std::map< TypeNode, Node > > new_visited; @@ -758,7 +757,7 @@ Node SortInference::simplifyNode( std::stringstream ss; ss << "io_" << op; TypeNode typ = nm->mkFunctionType(argTypes, retType); - d_symbol_map[op] = sm->mkDummySkolem( + d_symbol_map[op] = NodeManager::mkDummySkolem( ss.str(), typ, "op created during sort inference"); Trace("setp-model") << "Function " << op << " is replaced with " << d_symbol_map[op] << std::endl; model_replace_f[op] = d_symbol_map[op]; @@ -813,12 +812,11 @@ Node SortInference::simplifyNode( Node SortInference::mkInjection( TypeNode tn1, TypeNode tn2 ) { NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); std::vector< TypeNode > tns; tns.push_back( tn1 ); TypeNode typ = nm->mkFunctionType(tns, tn2); - Node f = - sm->mkDummySkolem("inj", typ, "injection for monotonicity constraint"); + Node f = NodeManager::mkDummySkolem( + "inj", typ, "injection for monotonicity constraint"); Trace("sort-inference") << "-> Make injection " << f << " from " << tn1 << " to " << tn2 << std::endl; Node v1 = NodeManager::mkBoundVar("?x", tn1); Node v2 = NodeManager::mkBoundVar("?y", tn1); diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index dafdd351c95..f5d96cdddc7 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -189,4 +189,9 @@ typerule CONST_SEQUENCE ::cvc5::internal::theory::strings::ConstSequenceTypeRule typerule SEQ_UNIT ::cvc5::internal::theory::strings::SeqUnitTypeRule typerule SEQ_NTH ::cvc5::internal::theory::strings::SeqNthTypeRule +# for RARE + +operator SEQ_EMPTY_OF_TYPE 1 "the empty sequence whose argument represents its type" +typerule SEQ_EMPTY_OF_TYPE ::cvc5::internal::theory::strings::SeqEmptyOfTypeTypeRule + endtheory diff --git a/src/theory/strings/regexp_entail.h b/src/theory/strings/regexp_entail.h index 4dd924c4d2f..37c04a231ce 100644 --- a/src/theory/strings/regexp_entail.h +++ b/src/theory/strings/regexp_entail.h @@ -47,24 +47,24 @@ class RegExpEntail * the vectors such that the resulting vectors are such that the membership * mchildren[n'...n''] in children[m'...m''] is equivalent to the input * membership. The argument dir indicates the direction to consider, where - * 0 means strip off the front, 1 off the back, and < 0 off of both. + * 1 means strip off the front, 0 off the back, and < 0 off of both. * * If this method returns the false node, then we have inferred that no - * string in the language of r1 ++ ... ++ rm is a prefix (when dir!=1) or - * suffix (when dir!=0) of s1 ++ ... ++ sn. Otherwise, it returns the null + * string in the language of r1 ++ ... ++ rm is a prefix (when dir!=0) or + * suffix (when dir!=1) of s1 ++ ... ++ sn. Otherwise, it returns the null * node. * * For example, given input - * mchildren = { "ab", x }, children = { [["a"]], ([["cd"]])* } and dir = 0, + * mchildren = { "ab", x }, children = { [["a"]], ([["cd"]])* } and dir = 1, * this method updates: - * mchildren = { "b", x }, children = { ("cd")* } + * mchildren = { "b", x }, children = { } * and returns null. * * For example, given input * { x, "abb", x }, { [[x]], ["a"..."b"], allchar, [[y]], [[x]]} and dir=-1, * this method updates: * { "b" }, { [[y]] } - * where [[.]] denotes str.to.re, and returns null. + * where [[.]] denotes str.to_re, and returns null. * * Notice that the above requirement for returning false is stronger than * determining that s1 ++ ... ++ sn in r1 ++ ... ++ rm is equivalent to false. @@ -78,12 +78,12 @@ class RegExpEntail * For example, given input * { "bb", x }, { "b", ("a")* } and dir=-1, * this method updates: - * { "b" }, { ("a")* } + * { "b", x }, { } * and returns null. * * For example, given input * { "cb", x }, { "b", ("a")* } and dir=-1, - * this method leaves children and mchildren unchanged and returns false. + * this method returns false. * * Notice that based on this, we can determine that: * "cb" ++ x in ( "b" ++ ("a")* )* diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index a4f7154ff1a..a8f50ad1751 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -275,7 +275,6 @@ int RegExpOpr::derivativeS(Node r, cvc5::internal::String c, Node& retNode) int ret = 1; retNode = d_emptyRegexp; NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); PairNodeStr dv = std::make_pair( r, c ); if( d_deriv_cache.find( dv ) != d_deriv_cache.end() ) { @@ -362,8 +361,8 @@ int RegExpOpr::derivativeS(Node r, cvc5::internal::String c, Node& retNode) } } if(ret == 0) { - Node sk = - sm->mkDummySkolem("rsp", nm->stringType(), "Split RegExp"); + Node sk = NodeManager::mkDummySkolem( + "rsp", nm->stringType(), "Split RegExp"); retNode = nm->mkNode(Kind::STRING_TO_REGEXP, sk); if(!rest.isNull()) { retNode = rewrite(nm->mkNode(Kind::REGEXP_CONCAT, retNode, rest)); diff --git a/src/theory/strings/rewrites b/src/theory/strings/rewrites index 78bfbaab505..d93449cb000 100644 --- a/src/theory/strings/rewrites +++ b/src/theory/strings/rewrites @@ -39,14 +39,30 @@ (= (str.++ x2 (str.++ x1 x)) y) (= y (str.++ x2 x1 x))) -(define-rule str-substr-empty-str ((n Int) (m Int)) (str.substr "" n m) "") -(define-cond-rule str-substr-empty-range ((x String) (n Int) (m Int)) (>= 0 m) (str.substr x n m) "") -(define-cond-rule str-substr-empty-start ((x String) (n Int) (m Int)) (>= n (str.len x)) (str.substr x n m) "") -(define-cond-rule str-substr-empty-start-neg ((x String) (n Int) (m Int)) (< n 0) (str.substr x n m) "") -(define-cond-rule str-substr-eq-empty ((s String) (n Int) (m Int)) - (and (= n 0) (> m n)) - (= (str.substr s n m) "") - (= s "")) +(define-cond-rule str-substr-empty-str ((x ?Seq) (n Int) (m Int)) + (= x (@seq.empty_of_type (@type_of x))) + (str.substr x n m) + x) + +(define-cond-rule str-substr-empty-range ((x ?Seq) (n Int) (m Int)) + (>= 0 m) + (str.substr x n m) + (@seq.empty_of_type (@type_of x))) + +(define-cond-rule str-substr-empty-start ((x ?Seq) (n Int) (m Int)) + (>= n (str.len x)) + (str.substr x n m) + (@seq.empty_of_type (@type_of x))) + +(define-cond-rule str-substr-empty-start-neg ((x ?Seq) (n Int) (m Int)) + (< n 0) + (str.substr x n m) + (@seq.empty_of_type (@type_of x))) + +(define-cond-rule str-substr-eq-empty ((s ?Seq) (r ?Seq) (n Int) (m Int)) + (and (= n 0) (> m n) (= r (@seq.empty_of_type (@type_of r)))) + (= (str.substr s n m) r) + (= s r)) (define-cond-rule str-len-replace-inv ((t ?Seq) (s ?Seq) (r ?Seq)) (= (str.len s) (str.len r)) @@ -98,12 +114,12 @@ (= (str.++ s2 s3) (str.++ t2 t3)) _) -(define-rule str-concat-unify-base ((s String) (t1 String) (t2 String :list)) +(define-rule str-concat-unify-base ((s ?Seq) (t1 ?Seq) (t2 ?Seq :list)) (= s (str.++ s t1 t2)) - (= "" (str.++ t1 t2))) -(define-rule str-concat-unify-base-rev ((s String) (t1 String) (t2 String :list)) + (= (@seq.empty_of_type (@type_of s)) (str.++ t1 t2))) +(define-rule str-concat-unify-base-rev ((s ?Seq) (t1 ?Seq) (t2 ?Seq :list)) (= s (str.++ t1 t2 s)) - (= "" (str.++ t1 t2))) + (= (@seq.empty_of_type (@type_of s)) (str.++ t1 t2))) (define-cond-rule str-concat-clash-char ((s1 ?Seq) (s2 ?Seq :list) (s3 ?Seq :list) (t1 ?Seq) (t2 ?Seq :list) (t3 ?Seq :list)) (and (not (= s1 t1)) (= (str.len s1) (str.len t1))) @@ -203,10 +219,6 @@ (str.contains x y) (= x y)) -(define-rule str-concat-emp ((xs String :list) (ys String :list)) - (str.++ xs "" ys) - (str.++ xs ys)) - (define-rule str-at-elim ((x ?Seq) (n Int)) (str.at x n) (str.substr x n 1)) ; not effective since due to not proving inequalities on length @@ -228,8 +240,9 @@ (str.replace t s r) t) -(define-rule str-replace-empty ((t ?Seq) (s ?Seq)) - (str.replace t "" s) +(define-cond-rule str-replace-empty ((t ?Seq) (s ?Seq) (r ?Seq)) + (= r (@seq.empty_of_type (@type_of r))) + (str.replace t r s) (str.++ s t)) (define-cond-rule str-replace-contains-pre ((t1 ?Seq) (t2 ?Seq :list) (s ?Seq) (r ?Seq)) @@ -255,9 +268,10 @@ (str.len (str.++ s2 s3)) (+ (str.len s1) _)) -(define-rule str-indexof-self ((t String) (n Int)) +(define-rule str-indexof-self ((t ?Seq) (n Int)) + (def (emp (@seq.empty_of_type (@type_of t)))) (str.indexof t t n) - (str.indexof "" "" n)) + (str.indexof emp emp n)) (define-cond-rule str-indexof-no-contains ((t ?Seq) (s ?Seq) (n Int)) (not (str.contains (str.substr t n (str.len t)) s)) @@ -419,3 +433,8 @@ (define-rule seq-len-unit ((x ?)) (str.len (seq.unit x)) 1) (define-rule seq-nth-unit ((x ?)) (seq.nth (seq.unit x) 0) x) (define-rule seq-rev-unit ((x ?)) (str.rev (seq.unit x)) (seq.unit x)) + +(define-cond-rule seq-len-empty ((x ?Seq)) + (= x (@seq.empty_of_type (@type_of x))) + (str.len x) + 0) diff --git a/src/theory/strings/skolem_cache.cpp b/src/theory/strings/skolem_cache.cpp index 835ea2ad821..b58320a7a5a 100644 --- a/src/theory/strings/skolem_cache.cpp +++ b/src/theory/strings/skolem_cache.cpp @@ -132,7 +132,7 @@ Node SkolemCache::mkTypedSkolemCached( { Trace("skolem-cache") << "Don't know how to handle Skolem ID " << id << std::endl; - sk = sm->mkDummySkolem(c, tn, "string skolem"); + sk = NodeManager::mkDummySkolem(c, tn, "string skolem"); } break; } @@ -152,8 +152,7 @@ Node SkolemCache::mkTypedSkolemCached(TypeNode tn, Node SkolemCache::mkSkolem(const char* c) { // TODO: eliminate this - SkolemManager* sm = d_nm->getSkolemManager(); - Node n = sm->mkDummySkolem(c, d_strType, "string skolem"); + Node n = NodeManager::mkDummySkolem(c, d_strType, "string skolem"); d_allSkolems.insert(n); return n; } diff --git a/src/theory/strings/theory_strings_type_rules.cpp b/src/theory/strings/theory_strings_type_rules.cpp index 251ff4db3ec..595d259a22f 100644 --- a/src/theory/strings/theory_strings_type_rules.cpp +++ b/src/theory/strings/theory_strings_type_rules.cpp @@ -548,6 +548,19 @@ TypeNode SeqNthTypeRule::computeType(NodeManager* nodeManager, return t.getSequenceElementType(); } +TypeNode SeqEmptyOfTypeTypeRule::preComputeType(NodeManager* nm, TNode n) +{ + return TypeNode::null(); +} + +TypeNode SeqEmptyOfTypeTypeRule::computeType(NodeManager* nm, + TNode n, + bool check, + std::ostream* errOut) +{ + return nm->mkAbstractType(Kind::SEQUENCE_TYPE); +} + Cardinality SequenceProperties::computeCardinality(TypeNode type) { Assert(type.getKind() == Kind::SEQUENCE_TYPE); diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h index d709a90951e..8d931826f82 100644 --- a/src/theory/strings/theory_strings_type_rules.h +++ b/src/theory/strings/theory_strings_type_rules.h @@ -204,6 +204,19 @@ class SeqNthTypeRule bool check, std::ostream* errOut); }; +/** + * Type rule for seq.empty_of_type + */ +class SeqEmptyOfTypeTypeRule +{ + public: + static TypeNode preComputeType(NodeManager* nm, TNode n); + + static TypeNode computeType(NodeManager* nodeManager, + TNode n, + bool check, + std::ostream* errOut); +}; /** Properties of the sequence type */ struct SequenceProperties diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index 96586e34c47..038d525516f 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -173,7 +173,7 @@ void Region::setDisequal( Node n1, Node n2, int type, bool valid ){ //if they are both a part of testClique, then remove split if( d_testClique.find( n1 )!=d_testClique.end() && d_testClique[n1] && d_testClique.find( n2 )!=d_testClique.end() && d_testClique[n2] ){ - Node eq = NodeManager::currentNM()->mkNode(Kind::EQUAL, n1, n2); + Node eq = NodeManager::mkNode(Kind::EQUAL, n1, n2); if( d_splits.find( eq )!=d_splits.end() && d_splits[ eq ] ){ Trace("uf-ss-debug") << "removing split for " << n1 << " " << n2 << std::endl; @@ -343,8 +343,7 @@ bool Region::check( Theory::Effort level, int cardinality, if( !isDisequal( newClique[j], newClique[k], 1 ) ){ Node at_j = newClique[j]; Node at_k = newClique[k]; - Node j_eq_k = - NodeManager::currentNM()->mkNode(Kind::EQUAL, at_j, at_k); + Node j_eq_k = NodeManager::mkNode(Kind::EQUAL, at_j, at_k); d_splits[ j_eq_k ] = true; d_splitsSize = d_splitsSize + 1; } @@ -457,7 +456,7 @@ SortModel::CardinalityDecisionStrategy::CardinalityDecisionStrategy( Node SortModel::CardinalityDecisionStrategy::mkLiteral(unsigned i) { - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = nodeManager(); Node cco = nm->mkConst(CardinalityConstraint(d_type, Integer(i + 1))); return nm->mkNode(Kind::CARDINALITY_CONSTRAINT, cco); } @@ -1017,8 +1016,8 @@ int SortModel::addSplit(Region* r) Node ss = rewrite(s); if (ss.getKind() != Kind::EQUAL) { - Node b_t = NodeManager::currentNM()->mkConst( true ); - Node b_f = NodeManager::currentNM()->mkConst( false ); + Node b_t = nodeManager()->mkConst(true); + Node b_f = nodeManager()->mkConst(false); if( ss==b_f ){ Trace("uf-ss-lemma") << "....Assert disequal directly : " << s[0] << " " << s[1] << std::endl; @@ -1049,7 +1048,7 @@ int SortModel::addSplit(Region* r) //Trace("uf-ss-lemma") << d_th->getEqualityEngine()->areDisequal( s[0], s[1] ) << std::endl; //Trace("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl; //split on the equality s - Node lem = NodeManager::currentNM()->mkNode(Kind::OR, ss, ss.negate()); + Node lem = NodeManager::mkNode(Kind::OR, ss, ss.negate()); // send lemma, with caching if (d_im.lemma(lem, InferenceId::UF_CARD_SPLIT)) { @@ -1082,7 +1081,7 @@ void SortModel::addCliqueLemma(std::vector& clique) } } eqs.push_back(d_cardinality_literal[d_cardinality].notNode()); - Node lem = NodeManager::currentNM()->mkNode(Kind::OR, eqs); + Node lem = nodeManager()->mkNode(Kind::OR, eqs); // send lemma, with caching if (d_im.lemma(lem, InferenceId::UF_CARD_CLIQUE)) { @@ -1093,10 +1092,10 @@ void SortModel::addCliqueLemma(std::vector& clique) void SortModel::simpleCheckCardinality() { if( d_maxNegCard.get()!=0 && d_hasCard.get() && d_cardinality.get()mkNode( - Kind::AND, - getCardinalityLiteral(d_cardinality.get()), - getCardinalityLiteral(d_maxNegCard.get()).negate()); + Node lem = + NodeManager::mkNode(Kind::AND, + getCardinalityLiteral(d_cardinality.get()), + getCardinalityLiteral(d_maxNegCard.get()).negate()); Trace("uf-ss-lemma") << "*** Simple cardinality conflict : " << lem << std::endl; d_im.conflict(lem, InferenceId::UF_CARD_SIMPLE_CONFLICT); } @@ -1134,8 +1133,6 @@ void SortModel::debugPrint( const char* c ){ bool SortModel::checkLastCall() { - NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); TheoryModel* m = d_state.getModel(); if( TraceIsOn("uf-ss-warn") ){ std::vector< Node > eqcs; @@ -1173,7 +1170,7 @@ bool SortModel::checkLastCall() { std::stringstream ss; ss << "r_" << d_type << "_"; - Node nn = sm->mkDummySkolem( + Node nn = NodeManager::mkDummySkolem( ss.str(), d_type, "enumeration to meet negative card constraint"); d_fresh_aloc_reps.push_back( nn ); } @@ -1194,7 +1191,8 @@ bool SortModel::checkLastCall() } } Node cl = getCardinalityLiteral( d_maxNegCard ); - Node lem = nm->mkNode(Kind::OR, cl, nm->mkAnd(force_cl)); + Node lem = + NodeManager::mkNode(Kind::OR, cl, nodeManager()->mkAnd(force_cl)); Trace("uf-ss-lemma") << "*** Enforce negative cardinality constraint lemma : " << lem << std::endl; d_im.lemma(lem, InferenceId::UF_CARD_ENFORCE_NEGATIVE); return false; @@ -1547,8 +1545,7 @@ void CardinalityExtension::check(Theory::Effort level) Node b = itel->second[j]; if( !d_th->getEqualityEngine()->areDisequal( a, b, false ) ){ Node eq = rewrite(a.eqNode(b)); - Node lem = NodeManager::currentNM()->mkNode( - Kind::OR, eq, eq.negate()); + Node lem = NodeManager::mkNode(Kind::OR, eq, eq.negate()); Trace("uf-ss-lemma") << "*** Split (no-minimal) : " << lem << std::endl; d_im.lemma(lem, InferenceId::UF_CARD_SPLIT); d_im.preferPhase(eq, true); @@ -1591,7 +1588,7 @@ CardinalityExtension::CombinedCardinalityDecisionStrategy:: Node CardinalityExtension::CombinedCardinalityDecisionStrategy::mkLiteral( unsigned i) { - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = nodeManager(); Node cco = nm->mkConst(CombinedCardinalityConstraint(Integer(i))); return nm->mkNode(Kind::COMBINED_CARDINALITY_CONSTRAINT, cco); } @@ -1750,7 +1747,7 @@ void CardinalityExtension::checkCombinedCardinality() std::vector< Node > conf; conf.push_back( d_rep_model[d_tn_mono_master]->getCardinalityLiteral( mc ) ); conf.push_back( d_rep_model[maxSlaveType]->getCardinalityLiteral( maxMonoSlave ).negate() ); - Node cf = NodeManager::currentNM()->mkNode(Kind::AND, conf); + Node cf = nodeManager()->mkNode(Kind::AND, conf); Trace("uf-ss-lemma") << "*** Combined monotone cardinality conflict" << " : " << cf << std::endl; Trace("uf-ss-com-card") << "*** Combined monotone cardinality conflict" @@ -1789,7 +1786,7 @@ void CardinalityExtension::checkCombinedCardinality() } } } - Node cf = NodeManager::currentNM()->mkNode(Kind::AND, conf); + Node cf = nodeManager()->mkNode(Kind::AND, conf); Trace("uf-ss-lemma") << "*** Combined cardinality conflict : " << cf << std::endl; Trace("uf-ss-com-card") << "*** Combined cardinality conflict : " << cf diff --git a/src/theory/uf/conversions_solver.cpp b/src/theory/uf/conversions_solver.cpp index 2ff09c9edc0..31b5a871e61 100644 --- a/src/theory/uf/conversions_solver.cpp +++ b/src/theory/uf/conversions_solver.cpp @@ -79,12 +79,12 @@ void ConversionsSolver::checkReduction(Node n) } if (options().uf.modelBasedArithBvConv) { - NodeManager* nm = NodeManager::currentNM(); Node argval = d_state.getModel()->getValue(n[0]); Trace("bv-convs-debug") << " arg value = " << argval << std::endl; - Node eval = rewrite(nm->mkNode(n.getOperator(), argval)); + Node eval = rewrite(NodeManager::mkNode(n.getOperator(), argval)); Trace("bv-convs-debug") << " evaluated = " << eval << std::endl; - Node lem = nm->mkNode(Kind::IMPLIES, n[0].eqNode(argval), n.eqNode(eval)); + Node lem = + NodeManager::mkNode(Kind::IMPLIES, n[0].eqNode(argval), n.eqNode(eval)); d_im.lemma(lem, InferenceId::UF_ARITH_BV_CONV_VALUE_REFINE); return; } diff --git a/src/theory/uf/diamonds_proof_generator.cpp b/src/theory/uf/diamonds_proof_generator.cpp new file mode 100644 index 00000000000..9eec970ba25 --- /dev/null +++ b/src/theory/uf/diamonds_proof_generator.cpp @@ -0,0 +1,182 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Diamonds proof generator utility. + */ + +#include "theory/uf/diamonds_proof_generator.h" + +#include "proof/proof.h" + +namespace cvc5::internal { + +DiamondsProofGenerator::DiamondsProofGenerator(Env& env) : EnvObj(env) {} + +DiamondsProofGenerator::~DiamondsProofGenerator() {} + +void DiamondsProofGenerator::ppStaticLearn(TNode n, + std::vector& learned) +{ + std::vector workList; + workList.push_back(n); + std::unordered_set processed; + + while (!workList.empty()) + { + n = workList.back(); + + if (n.isClosure()) + { + // unsafe to go under quantifiers; we might pull bound vars out of scope! + processed.insert(n); + workList.pop_back(); + continue; + } + + bool unprocessedChildren = false; + for (TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) + { + if (processed.find(*i) == processed.end()) + { + // unprocessed child + workList.push_back(*i); + unprocessedChildren = true; + } + } + + if (unprocessedChildren) + { + continue; + } + + workList.pop_back(); + // has node n been processed in the meantime ? + if (processed.find(n) != processed.end()) + { + continue; + } + processed.insert(n); + + // == DIAMONDS == + + Trace("diamonds") << "===================== looking at" << std::endl + << n << std::endl; + + // binary OR of binary ANDs of EQUALities + if (n.getKind() == Kind::OR && n.getNumChildren() == 2 + && n[0].getKind() == Kind::AND && n[0].getNumChildren() == 2 + && n[1].getKind() == Kind::AND && n[1].getNumChildren() == 2 + && (n[0][0].getKind() == Kind::EQUAL) + && (n[0][1].getKind() == Kind::EQUAL) + && (n[1][0].getKind() == Kind::EQUAL) + && (n[1][1].getKind() == Kind::EQUAL)) + { + // now we have (a = b && c = d) || (e = f && g = h) + + Trace("diamonds") << "has form of a diamond!" << std::endl; + + TNode a = n[0][0][0], b = n[0][0][1], c = n[0][1][0], d = n[0][1][1], + e = n[1][0][0], f = n[1][0][1], g = n[1][1][0], h = n[1][1][1]; + + // test that one of {a, b} = one of {c, d}, and make "b" the + // shared node (i.e. put in the form (a = b && b = d)) + // note we don't actually care about the shared ones, so the + // "swaps" below are one-sided, ignoring b and c + if (a == c) + { + a = b; + } + else if (a == d) + { + a = b; + d = c; + } + else if (b == c) + { + // nothing to do + } + else if (b == d) + { + d = c; + } + else + { + // condition not satisfied + Trace("diamonds") << "+ A fails" << std::endl; + continue; + } + + Trace("diamonds") << "+ A holds" << std::endl; + + // same: one of {e, f} = one of {g, h}, and make "f" the + // shared node (i.e. put in the form (e = f && f = h)) + if (e == g) + { + e = f; + } + else if (e == h) + { + e = f; + h = g; + } + else if (f == g) + { + // nothing to do + } + else if (f == h) + { + h = g; + } + else + { + // condition not satisfied + Trace("diamonds") << "+ B fails" << std::endl; + continue; + } + + Trace("diamonds") << "+ B holds" << std::endl; + + // now we have (a = b && b = d) || (e = f && f = h) + // test that {a, d} == {e, h} + if ((a == e && d == h) || (a == h && d == e)) + { + // learn: n implies a == d + Trace("diamonds") << "+ C holds" << std::endl; + Node newEquality = a.eqNode(d); + Trace("diamonds") << " ==> " << newEquality << std::endl; + Node lem = n.impNode(newEquality); + TrustNode trn = TrustNode::mkTrustLemma(lem, this); + learned.emplace_back(trn); + } + else + { + Trace("diamonds") << "+ C fails" << std::endl; + } + } + } +} + +std::shared_ptr DiamondsProofGenerator::getProofFor(Node fact) +{ + Trace("valid-witness") << "Prove " << fact << std::endl; + // proofs not yet supported + CDProof cdp(d_env); + cdp.addTrustedStep(fact, TrustId::DIAMONDS, {}, {}); + return cdp.getProofFor(fact); +} + +std::string DiamondsProofGenerator::identify() const +{ + return "DiamondsProofGenerator"; +} + +} // namespace cvc5::internal diff --git a/src/theory/uf/diamonds_proof_generator.h b/src/theory/uf/diamonds_proof_generator.h new file mode 100644 index 00000000000..b16bb355a83 --- /dev/null +++ b/src/theory/uf/diamonds_proof_generator.h @@ -0,0 +1,60 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Diamonds proof generator utility. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__UF__DIAMONDS_PROOF_GENERATOR_H +#define CVC5__THEORY__UF__DIAMONDS_PROOF_GENERATOR_H + +#include "proof/method_id.h" +#include "proof/proof_generator.h" +#include "proof/trust_node.h" +#include "smt/env_obj.h" + +namespace cvc5::internal { + +class ProofNode; +class ProofNodeManager; + +/** + * Proof generator implementing the "diamonds" preprocessing step, performed + * by TheoryUF. + */ +class DiamondsProofGenerator : protected EnvObj, public ProofGenerator +{ + public: + /** + * @param env Reference to the environment + */ + DiamondsProofGenerator(Env& env); + virtual ~DiamondsProofGenerator(); + /** + * Performs ppStaticLearn for theory UF. + * @param n The asserted formula. + * @param learned A list of lemmas to add to, if applicable. + */ + void ppStaticLearn(TNode n, std::vector& learned); + /** + * Get proof for fact. Called on fact that were added to learned by + * the above method. + */ + std::shared_ptr getProofFor(Node fact) override; + /** identify */ + std::string identify() const override; +}; + +} // namespace cvc5::internal + +#endif /* CVC5__PROOF__DIAMONDS_PROOF_GENERATOR_H */ diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp index ea0bc1394c5..c7db8551d36 100644 --- a/src/theory/uf/eq_proof.cpp +++ b/src/theory/uf/eq_proof.cpp @@ -144,7 +144,7 @@ bool EqProof::expandTransitivityForDisequalities( << "EqProof::expandTransitivityForDisequalities: no need.\n"; return false; } - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = conclusion.getNodeManager(); Assert(termPos == 0 || termPos == 1); Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: found " "offending equality at index " @@ -595,7 +595,7 @@ bool EqProof::expandTransitivityForTheoryDisequalities( // (= (= t1 t2) (= c1 c2)) (= (= c1 c2) false) // --------------------------------------------------------------------- TR // (= (= t1 t2) false) - Node constApp = NodeManager::currentNM()->mkNode(Kind::EQUAL, constChildren); + Node constApp = conclusion.getNodeManager()->mkNode(Kind::EQUAL, constChildren); Node constEquality = constApp.eqNode(conclusion[1 - termPos]); Trace("eqproof-conv") << "EqProof::expandTransitivityForTheoryDisequalities: adding " @@ -953,13 +953,13 @@ Node EqProof::addToProof(CDProof* p, { intro = ProofRule::FALSE_INTRO; conclusion = - d_node[0].eqNode(NodeManager::currentNM()->mkConst(false)); + d_node[0].eqNode(d_node.getNodeManager()->mkConst(false)); } else { intro = ProofRule::TRUE_INTRO; conclusion = - d_node.eqNode(NodeManager::currentNM()->mkConst(true)); + d_node.eqNode(d_node.getNodeManager()->mkConst(true)); } Trace("eqproof-conv") << "EqProof::addToProof: adding " << intro << " step for " << d_node << "\n"; @@ -1007,7 +1007,7 @@ Node EqProof::addToProof(CDProof* p, if (d_children.empty()) { Node conclusion = - d_node[0].eqNode(NodeManager::currentNM()->mkConst(false)); + d_node[0].eqNode(d_node.getNodeManager()->mkConst(false)); p->addStep(d_node, ProofRule::MACRO_SR_PRED_INTRO, {}, {d_node}); p->addStep(conclusion, ProofRule::FALSE_INTRO, {d_node}, {}); visited[d_node] = conclusion; @@ -1088,7 +1088,7 @@ Node EqProof::addToProof(CDProof* p, { constChildren.insert(constChildren.begin(), d_node[0].getOperator()); } - Node constApp = NodeManager::currentNM()->mkNode(k, constChildren); + Node constApp = d_node.getNodeManager()->mkNode(k, constChildren); Node constEquality = constApp.eqNode(d_node[1]); Trace("eqproof-conv") << "EqProof::addToProof: adding " << ProofRule::MACRO_SR_PRED_INTRO << " step for " @@ -1123,7 +1123,7 @@ Node EqProof::addToProof(CDProof* p, Node conclusion = d_node.getKind() != Kind::NOT ? d_node - : d_node[0].eqNode(NodeManager::currentNM()->mkConst(false)); + : d_node[0].eqNode(d_node.getNodeManager()->mkConst(false)); // If the conclusion is an assumption, its derivation was spurious, so it // can be discarded. Moreover, reconstructing the step may lead to cyclic // proofs, so we *must* cut here. @@ -1261,7 +1261,7 @@ Node EqProof::addToProof(CDProof* p, // whether the transitivity matrix computed by reduceNestedCongruence contains // empty rows Node conclusion = d_node; - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = conclusion.getNodeManager(); if (isNary) { unsigned emptyRows = 0; diff --git a/src/theory/uf/function_const.cpp b/src/theory/uf/function_const.cpp index 59d282fd76c..711fcdda918 100644 --- a/src/theory/uf/function_const.cpp +++ b/src/theory/uf/function_const.cpp @@ -64,7 +64,7 @@ Node FunctionConst::toLambda(TNode n) Assert(tn.isFunction()); std::vector argTypes = tn.getArgTypes(); std::vector bvs; - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = n.getNodeManager(); BoundVarManager* bvm = nm->getBoundVarManager(); // associate a unique bound variable list with the value for (size_t i = 0, nargs = argTypes.size(); i < nargs; i++) @@ -94,7 +94,7 @@ TypeNode FunctionConst::getFunctionTypeForArrayType(TypeNode atn, Node bvl) atn = atn.getArrayConstituentType(); } children.push_back(atn); - return NodeManager::currentNM()->mkFunctionType(children); + return bvl.getNodeManager()->mkFunctionType(children); } TypeNode FunctionConst::getArrayTypeForFunctionType(TypeNode ftn) @@ -106,7 +106,7 @@ TypeNode FunctionConst::getArrayTypeForFunctionType(TypeNode ftn) for (size_t i = 0; i < nchildren - 1; i++) { size_t ii = nchildren - i - 2; - ret = NodeManager::currentNM()->mkArrayType(ftn[ii], ret); + ret = NodeManager::mkArrayType(ftn[ii], ret); } return ret; } @@ -142,7 +142,7 @@ Node FunctionConst::getLambdaForArrayRepresentationRec( Assert(a[1].getType() == bvl[bvlIndex].getType()); Assert(val.getType() == body.getType()); Node cond = bvl[bvlIndex].eqNode(a[1]); - ret = NodeManager::currentNM()->mkNode(Kind::ITE, cond, val, body); + ret = NodeManager::mkNode(Kind::ITE, cond, val, body); } } } @@ -174,7 +174,7 @@ Node FunctionConst::getLambdaForArrayRepresentation(TNode a, TNode bvl) { Trace("builtin-rewrite-debug") << "...got lambda body " << body << std::endl; - return NodeManager::currentNM()->mkNode(Kind::LAMBDA, bvl, body); + return NodeManager::mkNode(Kind::LAMBDA, bvl, body); } Trace("builtin-rewrite-debug") << "...failed to get lambda body" << std::endl; return Node::null(); @@ -184,7 +184,7 @@ Node FunctionConst::getArrayRepresentationForLambdaRec(TNode n, TypeNode retType) { Assert(n.getKind() == Kind::LAMBDA); - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = n.getNodeManager(); Trace("builtin-rewrite-debug") << "Get array representation for : " << n << std::endl; diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index a3b67301723..0d648a76d9f 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -209,7 +209,6 @@ Node HoExtension::getApplyUfForHoApply(Node node) Node f = TheoryUfRewriter::decomposeHoApply(node, args, true); Node new_f = f; NodeManager* nm = nodeManager(); - SkolemManager* sm = nm->getSkolemManager(); if (!TheoryUfRewriter::canUseAsApplyUfOperator(f)) { NodeNodeMap::const_iterator itus = d_uf_std_skolem.find(f); @@ -237,7 +236,7 @@ Node HoExtension::getApplyUfForHoApply(Node node) newTypes.insert(newTypes.end(), argTypes.begin(), argTypes.end()); TypeNode nft = nm->mkFunctionType(newTypes, rangeType); - new_f = sm->mkDummySkolem("app_uf", nft); + new_f = NodeManager::mkDummySkolem("app_uf", nft); for (const Node& v : vs) { new_f = nm->mkNode(Kind::HO_APPLY, new_f, v); @@ -251,7 +250,7 @@ Node HoExtension::getApplyUfForHoApply(Node node) else { // introduce skolem to make a standard APPLY_UF - new_f = sm->mkDummySkolem("app_uf", f.getType()); + new_f = NodeManager::mkDummySkolem("app_uf", f.getType()); lem = new_f.eqNode(f); } Trace("uf-ho-lemma") diff --git a/src/theory/uf/lambda_lift.cpp b/src/theory/uf/lambda_lift.cpp index d21fa1d56d4..bc6b88c35cb 100644 --- a/src/theory/uf/lambda_lift.cpp +++ b/src/theory/uf/lambda_lift.cpp @@ -174,7 +174,7 @@ Node LambdaLift::getAssertionFor(TNode node) Node lambda = FunctionConst::toLambda(node); if (!lambda.isNull()) { - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = node.getNodeManager(); // The new assertion std::vector children; // bound variable list @@ -222,9 +222,7 @@ Node LambdaLift::getSkolemFor(TNode node) Trace("rtf-proof-debug") << "RemoveTermFormulas::run: make LAMBDA skolem" << std::endl; // Make the skolem to represent the lambda - NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); - skolem = sm->mkPurifySkolem(node); + skolem = SkolemManager::mkPurifySkolem(node); } } return skolem; @@ -258,11 +256,10 @@ TrustNode LambdaLift::betaReduce(TNode node) const Node LambdaLift::betaReduce(TNode lam, const std::vector& args) const { Assert(lam.getKind() == Kind::LAMBDA); - NodeManager* nm = NodeManager::currentNM(); std::vector betaRed; betaRed.push_back(lam); betaRed.insert(betaRed.end(), args.begin(), args.end()); - Node app = nm->mkNode(Kind::APPLY_UF, betaRed); + Node app = nodeManager()->mkNode(Kind::APPLY_UF, betaRed); app = rewrite(app); return app; } diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 09da10d767a..579d1c15733 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -50,6 +50,7 @@ TheoryUF::TheoryUF(Env& env, d_thss(nullptr), d_lambdaLift(new LambdaLift(env)), d_ho(nullptr), + d_dpfgen(env), d_functionsTerms(context()), d_symb(env, instanceName), d_rewriter(nodeManager(), env.getRewriter()), @@ -434,121 +435,8 @@ void TheoryUF::ppStaticLearn(TNode n, std::vector& learned) { //TimerStat::CodeTimer codeTimer(d_staticLearningTimer); - vector workList; - workList.push_back(n); - std::unordered_set processed; - - while(!workList.empty()) { - n = workList.back(); - - if (n.isClosure()) - { - // unsafe to go under quantifiers; we might pull bound vars out of scope! - processed.insert(n); - workList.pop_back(); - continue; - } - - bool unprocessedChildren = false; - for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) { - if(processed.find(*i) == processed.end()) { - // unprocessed child - workList.push_back(*i); - unprocessedChildren = true; - } - } - - if(unprocessedChildren) { - continue; - } - - workList.pop_back(); - // has node n been processed in the meantime ? - if(processed.find(n) != processed.end()) { - continue; - } - processed.insert(n); - - // == DIAMONDS == - - Trace("diamonds") << "===================== looking at" << endl - << n << endl; - - // binary OR of binary ANDs of EQUALities - if (n.getKind() == Kind::OR && n.getNumChildren() == 2 - && n[0].getKind() == Kind::AND && n[0].getNumChildren() == 2 - && n[1].getKind() == Kind::AND && n[1].getNumChildren() == 2 - && (n[0][0].getKind() == Kind::EQUAL) - && (n[0][1].getKind() == Kind::EQUAL) - && (n[1][0].getKind() == Kind::EQUAL) - && (n[1][1].getKind() == Kind::EQUAL)) - { - // now we have (a = b && c = d) || (e = f && g = h) - - Trace("diamonds") << "has form of a diamond!" << endl; - - TNode - a = n[0][0][0], b = n[0][0][1], - c = n[0][1][0], d = n[0][1][1], - e = n[1][0][0], f = n[1][0][1], - g = n[1][1][0], h = n[1][1][1]; - - // test that one of {a, b} = one of {c, d}, and make "b" the - // shared node (i.e. put in the form (a = b && b = d)) - // note we don't actually care about the shared ones, so the - // "swaps" below are one-sided, ignoring b and c - if(a == c) { - a = b; - } else if(a == d) { - a = b; - d = c; - } else if(b == c) { - // nothing to do - } else if(b == d) { - d = c; - } else { - // condition not satisfied - Trace("diamonds") << "+ A fails" << endl; - continue; - } - - Trace("diamonds") << "+ A holds" << endl; - - // same: one of {e, f} = one of {g, h}, and make "f" the - // shared node (i.e. put in the form (e = f && f = h)) - if(e == g) { - e = f; - } else if(e == h) { - e = f; - h = g; - } else if(f == g) { - // nothing to do - } else if(f == h) { - h = g; - } else { - // condition not satisfied - Trace("diamonds") << "+ B fails" << endl; - continue; - } - - Trace("diamonds") << "+ B holds" << endl; - - // now we have (a = b && b = d) || (e = f && f = h) - // test that {a, d} == {e, h} - if( (a == e && d == h) || - (a == h && d == e) ) { - // learn: n implies a == d - Trace("diamonds") << "+ C holds" << endl; - Node newEquality = a.eqNode(d); - Trace("diamonds") << " ==> " << newEquality << endl; - Node lem = n.impNode(newEquality); - TrustNode trn = TrustNode::mkTrustLemma(lem, nullptr); - learned.emplace_back(trn); - } else { - Trace("diamonds") << "+ C fails" << endl; - } - } - } + // Use the diamonds utility + d_dpfgen.ppStaticLearn(n, learned); if (options().uf.ufSymmetryBreaker) { diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 0bafcaa79c2..dbcc75957fc 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -23,6 +23,7 @@ #include "theory/theory.h" #include "theory/theory_eq_notify.h" #include "theory/theory_state.h" +#include "theory/uf/diamonds_proof_generator.h" #include "theory/uf/proof_checker.h" #include "theory/uf/symmetry_breaker.h" #include "theory/uf/theory_uf_rewriter.h" @@ -80,6 +81,8 @@ class TheoryUF : public Theory { std::unique_ptr d_ho; /** the conversions solver */ std::unique_ptr d_csolver; + /** Diamonds proof generator */ + DiamondsProofGenerator d_dpfgen; /** node for true */ Node d_true; diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index 962af4354da..f416d55abe6 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -81,16 +81,15 @@ Node UfModelTreeNode::getFunctionValue(const std::vector& args, } } - NodeManager* nm = NodeManager::currentNM(); Node retNode = defaultValue; // condense function values for (size_t i = 0, cargs = caseArgs.size(); i < cargs; i++) { size_t ii = cargs - i - 1; - retNode = nm->mkNode(Kind::ITE, - args[index].eqNode(caseArgs[ii]), - caseValues[caseArgs[ii]], - retNode); + retNode = NodeManager::mkNode(Kind::ITE, + args[index].eqNode(caseArgs[ii]), + caseValues[caseArgs[ii]], + retNode); } return retNode; } @@ -207,9 +206,8 @@ Node UfModelTree::getFunctionValue(const std::vector& args, Rewriter* r) { body = r->rewrite(body); } - Node boundVarList = - NodeManager::currentNM()->mkNode(Kind::BOUND_VAR_LIST, args); - return NodeManager::currentNM()->mkNode(Kind::LAMBDA, boundVarList, body); + Node boundVarList = body.getNodeManager()->mkNode(Kind::BOUND_VAR_LIST, args); + return NodeManager::mkNode(Kind::LAMBDA, boundVarList, body); } Node UfModelTree::getFunctionValue(const std::string& argPrefix, Rewriter* r) @@ -219,7 +217,7 @@ Node UfModelTree::getFunctionValue(const std::string& argPrefix, Rewriter* r) for( size_t i=0; imkBoundVar( ss.str(), type[i] ) ); + vars.push_back(NodeManager::mkBoundVar(ss.str(), type[i])); } return getFunctionValue(vars, r); } diff --git a/src/theory/uf/theory_uf_rewriter.cpp b/src/theory/uf/theory_uf_rewriter.cpp index 9c94c681b99..138d9a589a4 100644 --- a/src/theory/uf/theory_uf_rewriter.cpp +++ b/src/theory/uf/theory_uf_rewriter.cpp @@ -78,7 +78,7 @@ RewriteResponse TheoryUfRewriter::postRewrite(TNode node) std::vector args; args.push_back(lambdaRew); args.insert(args.end(), node.begin(), node.end()); - NodeManager* nm = NodeManager::currentNM(); + NodeManager* nm = nodeManager(); Node ret = nm->mkNode(Kind::APPLY_UF, args); Assert(ret != node); return RewriteResponse(REWRITE_AGAIN_FULL, ret); @@ -257,7 +257,7 @@ Node TheoryUfRewriter::getHoApplyForApplyUf(TNode n) Node curr = n.getOperator(); for (unsigned i = 0; i < n.getNumChildren(); i++) { - curr = NodeManager::currentNM()->mkNode(Kind::HO_APPLY, curr, n[i]); + curr = NodeManager::mkNode(Kind::HO_APPLY, curr, n[i]); } return curr; } @@ -268,7 +268,7 @@ Node TheoryUfRewriter::getApplyUfForHoApply(TNode n) // if operator is standard if (canUseAsApplyUfOperator(curr)) { - return NodeManager::currentNM()->mkNode(Kind::APPLY_UF, children); + return n.getNodeManager()->mkNode(Kind::APPLY_UF, children); } // cannot construct APPLY_UF if operator is partially applied or is not // standard diff --git a/src/theory/uf/theory_uf_type_rules.cpp b/src/theory/uf/theory_uf_type_rules.cpp index 267af22d142..e094902c765 100644 --- a/src/theory/uf/theory_uf_type_rules.cpp +++ b/src/theory/uf/theory_uf_type_rules.cpp @@ -278,10 +278,9 @@ bool FunctionProperties::isWellFounded(TypeNode type) Node FunctionProperties::mkGroundTerm(TypeNode type) { - NodeManager* nm = NodeManager::currentNM(); - Node bvl = nm->getBoundVarListForFunctionType(type); + Node bvl = NodeManager::getBoundVarListForFunctionType(type); Node ret = NodeManager::mkGroundTerm(type.getRangeType()); - return nm->mkNode(Kind::LAMBDA, bvl, ret); + return NodeManager::mkNode(Kind::LAMBDA, bvl, ret); } TypeNode IntToBitVectorOpTypeRule::preComputeType(NodeManager* nm, TNode n) diff --git a/src/theory/uf/type_enumerator.cpp b/src/theory/uf/type_enumerator.cpp index f0673068882..25077bb9f9d 100644 --- a/src/theory/uf/type_enumerator.cpp +++ b/src/theory/uf/type_enumerator.cpp @@ -37,7 +37,7 @@ Node FunctionEnumerator::operator*() throw NoMoreValuesException(getType()); } Node a = *d_arrayEnum; - return NodeManager::currentNM()->mkConst(FunctionArrayConst(getType(), a)); + return a.getNodeManager()->mkConst(FunctionArrayConst(getType(), a)); } FunctionEnumerator& FunctionEnumerator::operator++() diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 4c05243db10..6878c4af344 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -1505,6 +1505,7 @@ set(regress_0_tests regress0/quantifiers/matching-lia-1arg.smt2 regress0/quantifiers/mbqi-simple.smt2 regress0/quantifiers/merge-shadow.smt2 + regress0/quantifiers/miniscope-ite.smt2 regress0/quantifiers/mix-complete-strat.smt2 regress0/quantifiers/mix-match.smt2 regress0/quantifiers/mix-simp.smt2 diff --git a/test/regress/cli/regress0/quantifiers/miniscope-ite.smt2 b/test/regress/cli/regress0/quantifiers/miniscope-ite.smt2 new file mode 100644 index 00000000000..4331e813f11 --- /dev/null +++ b/test/regress/cli/regress0/quantifiers/miniscope-ite.smt2 @@ -0,0 +1,7 @@ +; EXPECT: unsat +(set-logic ALL) +(declare-fun a () Int) +(declare-fun c () Int) +(assert (forall ((x Int)) (ite (> c 0) (> x 0) (or (< x a) (> x (- a 3)))))) +(assert (> c 1)) +(check-sat) 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)