From 504fcaa57815943cf584ba6130facb3942b3ac96 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 21 Oct 2024 12:46:11 -0500 Subject: [PATCH 1/2] Fix proof checker for quant var reodering (#11295) Fixes errors in nightlies. This corrects the proof checker for QUANT_VAR_REORDERING, which currently throws spurious errors due to an incorrect check. --- src/theory/quantifiers/proof_checker.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/theory/quantifiers/proof_checker.cpp b/src/theory/quantifiers/proof_checker.cpp index f120dd49b6d..b4ac242be5a 100644 --- a/src/theory/quantifiers/proof_checker.cpp +++ b/src/theory/quantifiers/proof_checker.cpp @@ -137,8 +137,8 @@ Node QuantifiersProofRuleChecker::checkInternal( std::unordered_set varSet1(eq[0][0].begin(), eq[0][0].end()); std::unordered_set varSet2(eq[1][0].begin(), eq[1][0].end()); // cannot have repetition - if (varSet1.size() != eq[0].getNumChildren() - || varSet2.size() != eq[1].getNumChildren()) + if (varSet1.size() != eq[0][0].getNumChildren() + || varSet2.size() != eq[1][0].getNumChildren()) { return Node::null(); } From 63eb5e699c228a0bdad21b1df17e1551fbbc3db6 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 21 Oct 2024 13:26:49 -0500 Subject: [PATCH 2/2] Generalize more string RARE rules to sequences (#11291) Updates the RARE and Eunoia. Required for filling rewrites for sequences, with this change, we fill 3 more cases of the 886 unfilled rewrites in our regressions. --- proofs/eo/cpc/rules/Rewrites.eo | 94 ++++++++++++++++----------------- src/theory/strings/rewrites | 34 ++++++------ 2 files changed, 64 insertions(+), 64 deletions(-) diff --git a/proofs/eo/cpc/rules/Rewrites.eo b/proofs/eo/cpc/rules/Rewrites.eo index 80609d474b0..5acdbc5d654 100644 --- a/proofs/eo/cpc/rules/Rewrites.eo +++ b/proofs/eo/cpc/rules/Rewrites.eo @@ -1252,33 +1252,33 @@ :args (s1 n1 m1 k1) :conclusion (= (>= k1 (seq.len (seq.extract s1 n1 m1))) true) ) -(declare-rule str-concat-clash ((s1 String) (s2 String :list) (t1 String) (t2 String :list)) - :premises ((= (= s1 t1) false) (= (str.len s1) (str.len t1))) +(declare-rule str-concat-clash ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (s1 (Seq @T0)) (s2 (Seq @T1) :list) (t1 (Seq @T2)) (t2 (Seq @T3) :list)) + :premises ((= (= s1 t1) false) (= (seq.len s1) (seq.len t1))) :args (s1 s2 t1 t2) - :conclusion (= (= ($singleton_elim (str.++ s1 s2)) ($singleton_elim (str.++ t1 t2))) false) + :conclusion (= (= ($singleton_elim (seq.++ s1 s2)) ($singleton_elim (seq.++ t1 t2))) false) ) -(declare-rule str-concat-clash-rev ((s1 String) (s2 String :list) (t1 String) (t2 String :list)) - :premises ((= (= s1 t1) false) (= (str.len s1) (str.len t1))) +(declare-rule str-concat-clash-rev ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (s1 (Seq @T0)) (s2 (Seq @T1) :list) (t1 (Seq @T2)) (t2 (Seq @T3) :list)) + :premises ((= (= s1 t1) false) (= (seq.len s1) (seq.len t1))) :args (s1 s2 t1 t2) - :conclusion (= (= ($singleton_elim (str.++ s2 s1)) ($singleton_elim (str.++ t2 t1))) false) + :conclusion (= (= ($singleton_elim (seq.++ s2 s1)) ($singleton_elim (seq.++ t2 t1))) false) ) -(declare-rule str-concat-clash2 ((s1 String) (t1 String) (t2 String :list)) - :premises ((= (= s1 t1) false) (= (str.len s1) (str.len t1))) +(declare-rule str-concat-clash2 ((@T0 Type) (@T1 Type) (@T2 Type) (s1 (Seq @T0)) (t1 (Seq @T1)) (t2 (Seq @T2) :list)) + :premises ((= (= s1 t1) false) (= (seq.len s1) (seq.len t1))) :args (s1 t1 t2) - :conclusion (= (= s1 ($singleton_elim (str.++ t1 t2))) false) + :conclusion (= (= s1 ($singleton_elim (seq.++ t1 t2))) false) ) -(declare-rule str-concat-clash2-rev ((s1 String) (t1 String) (t2 String :list)) - :premises ((= (= s1 t1) false) (= (str.len s1) (str.len t1))) +(declare-rule str-concat-clash2-rev ((@T0 Type) (@T1 Type) (@T2 Type) (s1 (Seq @T0)) (t1 (Seq @T1)) (t2 (Seq @T2) :list)) + :premises ((= (= s1 t1) false) (= (seq.len s1) (seq.len t1))) :args (s1 t1 t2) - :conclusion (= (= s1 ($singleton_elim (str.++ t2 t1))) false) + :conclusion (= (= s1 ($singleton_elim (seq.++ t2 t1))) false) ) -(declare-rule str-concat-unify ((s1 String) (s2 String) (s3 String :list) (t1 String) (t2 String :list)) +(declare-rule str-concat-unify ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (@T4 Type) (s1 (Seq @T0)) (s2 (Seq @T1)) (s3 (Seq @T2) :list) (t1 (Seq @T3)) (t2 (Seq @T4) :list)) :args (s1 s2 s3 t1 t2) - :conclusion (= (= (str.++ s1 s2 s3) (str.++ s1 t1 t2)) (= ($singleton_elim (str.++ s2 s3)) ($singleton_elim (str.++ t1 t2)))) + :conclusion (= (= (seq.++ s1 s2 s3) (seq.++ s1 t1 t2)) (= ($singleton_elim (seq.++ s2 s3)) ($singleton_elim (seq.++ t1 t2)))) ) -(declare-rule str-concat-unify-rev ((s1 String) (s2 String) (s3 String :list) (t1 String) (t2 String :list)) +(declare-rule str-concat-unify-rev ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (@T4 Type) (s1 (Seq @T0)) (s2 (Seq @T1)) (s3 (Seq @T2) :list) (t1 (Seq @T3)) (t2 (Seq @T4) :list)) :args (s1 s2 s3 t1 t2) - :conclusion (= (= (str.++ s2 s3 s1) (str.++ t1 t2 s1)) (= ($singleton_elim (str.++ s2 s3)) ($singleton_elim (str.++ 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) @@ -1288,15 +1288,15 @@ :args (s1 t1 t2) :conclusion (= (= s1 (str.++ t1 t2 s1)) (= "" ($singleton_elim (str.++ t1 t2)))) ) -(declare-rule str-concat-clash-char ((s1 String) (s2 String :list) (s3 String :list) (t1 String) (t2 String :list) (t3 String :list)) - :premises ((= (= s1 t1) false) (= (str.len s1) (str.len t1))) +(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))) :args (s1 s2 s3 t1 t2 t3) - :conclusion (= (= ($singleton_elim (str.++ ($singleton_elim (str.++ s1 s2)) s3)) ($singleton_elim (str.++ ($singleton_elim (str.++ t1 t2)) t3))) false) + :conclusion (= (= ($singleton_elim (seq.++ ($singleton_elim (seq.++ s1 s2)) s3)) ($singleton_elim (seq.++ ($singleton_elim (seq.++ t1 t2)) t3))) false) ) -(declare-rule str-concat-clash-char-rev ((s1 String) (s2 String :list) (s3 String :list) (t1 String) (t2 String :list) (t3 String :list)) - :premises ((= (= s1 t1) false) (= (str.len s1) (str.len t1))) +(declare-rule str-concat-clash-char-rev ((@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))) :args (s1 s2 s3 t1 t2 t3) - :conclusion (= (= ($singleton_elim (str.++ s3 ($singleton_elim (str.++ s2 s1)))) ($singleton_elim (str.++ t3 ($singleton_elim (str.++ t2 t1))))) false) + :conclusion (= (= ($singleton_elim (seq.++ s3 ($singleton_elim (seq.++ s2 s1)))) ($singleton_elim (seq.++ t3 ($singleton_elim (seq.++ t2 t1))))) false) ) (declare-rule str-prefixof-elim ((@T0 Type) (@T1 Type) (s1 (Seq @T0)) (t1 (Seq @T1))) :args (s1 t1) @@ -1316,25 +1316,25 @@ :args (s1 t1) :conclusion (= (seq.suffixof s1 t1) (seq.contains t1 s1)) ) -(declare-rule str-substr-combine1 ((s1 String) (n1 Int) (m1 Int) (n2 Int) (m2 Int)) +(declare-rule str-substr-combine1 ((@T0 Type) (s1 (Seq @T0)) (n1 Int) (m1 Int) (n2 Int) (m2 Int)) :premises ((= (>= n1 0) true) (= (>= n2 0) true) (= (>= (- m2 (- m1 n2)) 0) true)) :args (s1 n1 m1 n2 m2) - :conclusion (= (str.substr (str.substr s1 n1 m1) n2 m2) (str.substr s1 (+ n1 n2) (- m1 n2))) + :conclusion (= (seq.extract (seq.extract s1 n1 m1) n2 m2) (seq.extract s1 (+ n1 n2) (- m1 n2))) ) -(declare-rule str-substr-combine2 ((s1 String) (n1 Int) (m1 Int) (n2 Int) (m2 Int)) +(declare-rule str-substr-combine2 ((@T0 Type) (s1 (Seq @T0)) (n1 Int) (m1 Int) (n2 Int) (m2 Int)) :premises ((= (>= n1 0) true) (= (>= n2 0) true) (= (>= (- (- m1 n2) m2) 0) true)) :args (s1 n1 m1 n2 m2) - :conclusion (= (str.substr (str.substr s1 n1 m1) n2 m2) (str.substr s1 (+ n1 n2) m2)) + :conclusion (= (seq.extract (seq.extract s1 n1 m1) n2 m2) (seq.extract s1 (+ n1 n2) m2)) ) -(declare-rule str-substr-combine3 ((s1 String) (n1 Int) (m1 Int) (n2 Int) (m2 Int)) - :premises ((= (>= n1 0) true) (= (>= n2 0) true) (= (>= (str.len (str.substr s1 n1 m1)) (+ n2 m2)) true)) +(declare-rule str-substr-combine3 ((@T0 Type) (s1 (Seq @T0)) (n1 Int) (m1 Int) (n2 Int) (m2 Int)) + :premises ((= (>= n1 0) true) (= (>= n2 0) true) (= (>= (seq.len (seq.extract s1 n1 m1)) (+ n2 m2)) true)) :args (s1 n1 m1 n2 m2) - :conclusion (= (str.substr (str.substr s1 n1 m1) n2 m2) (str.substr s1 (+ n1 n2) m2)) + :conclusion (= (seq.extract (seq.extract s1 n1 m1) n2 m2) (seq.extract s1 (+ n1 n2) m2)) ) -(declare-rule str-substr-combine4 ((s1 String) (n1 Int) (m1 Int) (n2 Int) (m2 Int)) - :premises ((= (>= n1 0) true) (= (>= n2 0) true) (= (>= (+ n2 m2) (str.len (str.substr s1 n1 m1))) true)) +(declare-rule str-substr-combine4 ((@T0 Type) (s1 (Seq @T0)) (n1 Int) (m1 Int) (n2 Int) (m2 Int)) + :premises ((= (>= n1 0) true) (= (>= n2 0) true) (= (>= (+ n2 m2) (seq.len (seq.extract s1 n1 m1))) true)) :args (s1 n1 m1 n2 m2) - :conclusion (= (str.substr (str.substr s1 n1 m1) n2 m2) (str.substr s1 (+ n1 n2) (- m1 n2))) + :conclusion (= (seq.extract (seq.extract s1 n1 m1) n2 m2) (seq.extract s1 (+ n1 n2) (- m1 n2))) ) (declare-rule str-substr-concat1 ((@T0 Type) (@T1 Type) (s1 (Seq @T0)) (s2 (Seq @T1) :list) (n1 Int) (m1 Int)) :premises ((= (>= n1 0) true) (= (>= (seq.len s1) (+ n1 m1)) true)) @@ -1370,25 +1370,25 @@ :args (x1 y1 z1 w1) :conclusion (= (seq.contains (seq.++ x1 y1 z1) w1) (or (seq.contains x1 w1) (seq.contains ($singleton_elim (seq.++ y1 z1)) w1))) ) -(declare-rule str-contains-lt-len ((x1 String) (y1 String)) - :premises ((= (> (str.len y1) (str.len x1)) true)) +(declare-rule str-contains-lt-len ((@T0 Type) (@T1 Type) (x1 (Seq @T0)) (y1 (Seq @T1))) + :premises ((= (> (seq.len y1) (seq.len x1)) true)) :args (x1 y1) - :conclusion (= (str.contains x1 y1) false) + :conclusion (= (seq.contains x1 y1) false) ) -(declare-rule str-contains-leq-len-eq ((x1 String) (y1 String)) - :premises ((= (>= (str.len y1) (str.len x1)) true)) +(declare-rule str-contains-leq-len-eq ((@T0 Type) (@T1 Type) (x1 (Seq @T0)) (y1 (Seq @T1))) + :premises ((= (>= (seq.len y1) (seq.len x1)) true)) :args (x1 y1) - :conclusion (= (str.contains x1 y1) (= x1 y1)) + :conclusion (= (seq.contains x1 y1) (= x1 y1)) ) -(declare-rule str-contains-emp ((x1 String) (y1 String)) - :premises ((= (str.len y1) 0)) +(declare-rule str-contains-emp ((@T0 Type) (@T1 Type) (x1 (Seq @T0)) (y1 (Seq @T1))) + :premises ((= (seq.len y1) 0)) :args (x1 y1) - :conclusion (= (str.contains x1 y1) true) + :conclusion (= (seq.contains x1 y1) true) ) -(declare-rule str-contains-is-emp ((x1 String) (y1 String)) - :premises ((= (str.len x1) 0)) +(declare-rule str-contains-is-emp ((@T0 Type) (@T1 Type) (x1 (Seq @T0)) (y1 (Seq @T1))) + :premises ((= (seq.len x1) 0)) :args (x1 y1) - :conclusion (= (str.contains x1 y1) (= x1 y1)) + :conclusion (= (seq.contains x1 y1) (= x1 y1)) ) (declare-rule str-concat-emp ((xs1 String :list) (ys1 String :list)) :args (xs1 ys1) @@ -1419,10 +1419,10 @@ :args (t1 n1) :conclusion (= (str.indexof t1 t1 n1) (str.indexof "" "" n1)) ) -(declare-rule str-indexof-no-contains ((t1 String) (s1 String) (n1 Int)) - :premises ((= (str.contains (str.substr t1 n1 (str.len t1)) s1) false)) +(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)) :args (t1 s1 n1) - :conclusion (= (str.indexof t1 s1 n1) -1) + :conclusion (= (seq.indexof t1 s1 n1) -1) ) (declare-rule str-to-lower-concat ((s1 String) (s2 String) (s3 String :list)) :args (s1 s2 s3) diff --git a/src/theory/strings/rewrites b/src/theory/strings/rewrites index e9de1a131be..94ede9b8588 100644 --- a/src/theory/strings/rewrites +++ b/src/theory/strings/rewrites @@ -72,28 +72,28 @@ (>= k (str.len (str.substr s n m))) true) -(define-cond-rule str-concat-clash ((s1 String) (s2 String :list) (t1 String) (t2 String :list)) +(define-cond-rule str-concat-clash ((s1 ?Seq) (s2 ?Seq :list) (t1 ?Seq) (t2 ?Seq :list)) (and (not (= s1 t1)) (= (str.len s1) (str.len t1))) (= (str.++ s1 s2) (str.++ t1 t2)) false) -(define-cond-rule str-concat-clash-rev ((s1 String) (s2 String :list) (t1 String) (t2 String :list)) +(define-cond-rule str-concat-clash-rev ((s1 ?Seq) (s2 ?Seq :list) (t1 ?Seq) (t2 ?Seq :list)) (and (not (= s1 t1)) (= (str.len s1) (str.len t1))) (= (str.++ s2 s1) (str.++ t2 t1)) false) -(define-cond-rule str-concat-clash2 ((s1 String) (t1 String) (t2 String :list)) +(define-cond-rule str-concat-clash2 ((s1 ?Seq) (t1 ?Seq) (t2 ?Seq :list)) (and (not (= s1 t1)) (= (str.len s1) (str.len t1))) (= s1 (str.++ t1 t2)) false) -(define-cond-rule str-concat-clash2-rev ((s1 String) (t1 String) (t2 String :list)) +(define-cond-rule str-concat-clash2-rev ((s1 ?Seq) (t1 ?Seq) (t2 ?Seq :list)) (and (not (= s1 t1)) (= (str.len s1) (str.len t1))) (= s1 (str.++ t2 t1)) false) -(define-rule* str-concat-unify ((s1 String) (s2 String) (s3 String :list) (t2 String) (t3 String :list)) +(define-rule* str-concat-unify ((s1 ?Seq) (s2 ?Seq) (s3 ?Seq :list) (t2 ?Seq) (t3 ?Seq :list)) (= (str.++ s1 s2 s3) (str.++ s1 t2 t3)) (= (str.++ s2 s3) (str.++ t2 t3)) _) -(define-rule* str-concat-unify-rev ((s1 String) (s2 String) (s3 String :list) (t2 String) (t3 String :list)) +(define-rule* str-concat-unify-rev ((s1 ?Seq) (s2 ?Seq) (s3 ?Seq :list) (t2 ?Seq) (t3 ?Seq :list)) (= (str.++ s2 s3 s1) (str.++ t2 t3 s1)) (= (str.++ s2 s3) (str.++ t2 t3)) _) @@ -105,11 +105,11 @@ (= s (str.++ t1 t2 s)) (= "" (str.++ t1 t2))) -(define-cond-rule str-concat-clash-char ((s1 String) (s2 String :list) (s3 String :list) (t1 String) (t2 String :list) (t3 String :list)) +(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))) (= (str.++ (str.++ s1 s2) s3) (str.++ (str.++ t1 t2) t3)) false) -(define-cond-rule str-concat-clash-char-rev ((s1 String) (s2 String :list) (s3 String :list) (t1 String) (t2 String :list) (t3 String :list)) +(define-cond-rule str-concat-clash-char-rev ((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))) (= (str.++ s3 (str.++ s2 s1)) (str.++ t3 (str.++ t2 t1))) false) @@ -130,22 +130,22 @@ (str.suffixof s t) (str.contains t s)) -(define-cond-rule str-substr-combine1 ((s String) (n1 Int) (m1 Int) (n2 Int) (m2 Int)) +(define-cond-rule str-substr-combine1 ((s ?Seq) (n1 Int) (m1 Int) (n2 Int) (m2 Int)) (and (>= n1 0) (>= n2 0) (>= (- m2 (- m1 n2)) 0)) (str.substr (str.substr s n1 m1) n2 m2) (str.substr s (+ n1 n2) (- m1 n2))) -(define-cond-rule str-substr-combine2 ((s String) (n1 Int) (m1 Int) (n2 Int) (m2 Int)) +(define-cond-rule str-substr-combine2 ((s ?Seq) (n1 Int) (m1 Int) (n2 Int) (m2 Int)) (and (>= n1 0) (>= n2 0) (>= (- (- m1 n2) m2) 0)) (str.substr (str.substr s n1 m1) n2 m2) (str.substr s (+ n1 n2) m2)) -(define-cond-rule str-substr-combine3 ((s String) (n1 Int) (m1 Int) (n2 Int) (m2 Int)) +(define-cond-rule str-substr-combine3 ((s ?Seq) (n1 Int) (m1 Int) (n2 Int) (m2 Int)) (and (>= n1 0) (>= n2 0) (>= (str.len (str.substr s n1 m1)) (+ n2 m2))) (str.substr (str.substr s n1 m1) n2 m2) (str.substr s (+ n1 n2) m2)) -(define-cond-rule str-substr-combine4 ((s String) (n1 Int) (m1 Int) (n2 Int) (m2 Int)) +(define-cond-rule str-substr-combine4 ((s ?Seq) (n1 Int) (m1 Int) (n2 Int) (m2 Int)) (and (>= n1 0) (>= n2 0) (>= (+ n2 m2) (str.len (str.substr s n1 m1)))) (str.substr (str.substr s n1 m1) n2 m2) (str.substr s (+ n1 n2) (- m1 n2))) @@ -183,22 +183,22 @@ (str.contains (str.++ x y z) w) (or (str.contains x w) (str.contains (str.++ y z) w))) -(define-cond-rule str-contains-lt-len ((x String) (y String)) +(define-cond-rule str-contains-lt-len ((x ?Seq) (y ?Seq)) (> (str.len y) (str.len x)) (str.contains x y) false) -(define-cond-rule str-contains-leq-len-eq ((x String) (y String)) +(define-cond-rule str-contains-leq-len-eq ((x ?Seq) (y ?Seq)) (>= (str.len y) (str.len x)) (str.contains x y) (= x y)) -(define-cond-rule str-contains-emp ((x String) (y String)) +(define-cond-rule str-contains-emp ((x ?Seq) (y ?Seq)) (= (str.len y) 0) (str.contains x y) true) -(define-cond-rule str-contains-is-emp ((x String) (y String)) +(define-cond-rule str-contains-is-emp ((x ?Seq) (y ?Seq)) (= (str.len x) 0) (str.contains x y) (= x y)) @@ -237,7 +237,7 @@ (str.indexof t t n) (str.indexof "" "" n)) -(define-cond-rule str-indexof-no-contains ((t String) (s String) (n Int)) +(define-cond-rule str-indexof-no-contains ((t ?Seq) (s ?Seq) (n Int)) (not (str.contains (str.substr t n (str.len t)) s)) (str.indexof t s n) (- 1))