Skip to content

Commit

Permalink
Merge branch 'main' of https://github.com/cvc5/cvc5 into pfTrustId
Browse files Browse the repository at this point in the history
  • Loading branch information
@ajreynol
ajreynol committed Oct 21, 2024
2 parents e9ef3b8 + 63eb5e6 commit df7b4a4
Show file tree
Hide file tree
Showing 3 changed files with 66 additions and 66 deletions.
94 changes: 47 additions & 47 deletions proofs/eo/cpc/rules/Rewrites.eo
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)
Expand All @@ -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))
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand Down
4 changes: 2 additions & 2 deletions src/theory/quantifiers/proof_checker.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -137,8 +137,8 @@ Node QuantifiersProofRuleChecker::checkInternal(
std::unordered_set<Node> varSet1(eq[0][0].begin(), eq[0][0].end());
std::unordered_set<Node> 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();
}
Expand Down
34 changes: 17 additions & 17 deletions src/theory/strings/rewrites
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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))
_)
Expand All @@ -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)
Expand All @@ -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)))
Expand Down Expand Up @@ -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))
Expand Down Expand Up @@ -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))
Expand Down

0 comments on commit df7b4a4

Please sign in to comment.