diff --git a/IsaRARE.thy b/IsaRARE.thy index 8bd362f..7b4d42a 100644 --- a/IsaRARE.thy +++ b/IsaRARE.thy @@ -244,7 +244,6 @@ val _ = Outer_Syntax.local_theory \<^command_keyword>\parse_rare_file\ t1 s1) (>= t1 (+ s1 1))) +) +(declare-rule arith-elim-int-lt ((t1 Int) (s1 Int)) + :args (t1 s1) + :conclusion (= (< t1 s1) (>= s1 (+ t1 1))) +) +(declare-rule arith-leq-norm ((t1 Int) (s1 Int)) + :args (t1 s1) + :conclusion (= (<= t1 s1) (not (>= t1 (+ s1 1)))) +) +(declare-rule arith-geq-tighten ((t1 Int) (s1 Int)) + :args (t1 s1) + :conclusion (= (not (>= t1 s1)) (>= s1 (+ t1 1))) +) +(declare-rule arith-geq-norm1-int ((t1 Int) (s1 Int)) + :args (t1 s1) + :conclusion (= (>= t1 s1) (>= (- t1 s1) 0)) +) +(declare-rule arith-geq-norm1-real ((t1 Real) (s1 Real)) + :args (t1 s1) + :conclusion (= (>= t1 s1) (>= (- t1 s1) 0/1)) +) +(declare-rule arith-eq-elim-real ((t1 Real) (s1 Real)) + :args (t1 s1) + :conclusion (= (= t1 s1) (and (>= t1 s1) (<= t1 s1))) +) +(declare-rule arith-eq-elim-int ((t1 Int) (s1 Int)) + :args (t1 s1) + :conclusion (= (= t1 s1) (and (>= t1 s1) (<= t1 s1))) +) +(declare-rule arith-int-eq-conflict ((t1 Int) (c1 Real)) + :premises ((= (= (to_real (to_int c1)) c1) false)) + :args (t1 c1) + :conclusion (= (= (to_real t1) c1) false) +) +(declare-rule arith-int-geq-tighten ((t1 Int) (c1 Real) (cc1 Int)) + :premises ((= (= (to_real (to_int c1)) c1) false) (= cc1 (+ (to_int c1) 1))) + :args (t1 c1 cc1) + :conclusion (= (>= (to_real t1) c1) (>= t1 cc1)) +) +(declare-rule arith-divisible-elim ((n1 Int) (t1 Int)) + :premises ((= (= n1 0) false)) + :args (n1 t1) + :conclusion (= (divisible n1 t1) (= (mod_total t1 n1) 0)) +) + +;;;;;;;;;;;;;;;;; +;; Boolean +;;;;;;;;;;;;;;;;; + +(declare-rule bool-double-not-elim ((t1 Bool)) + :args (t1) + :conclusion (= (not (not t1)) t1) +) +(declare-rule bool-not-true ((t1 Bool)) + :premises ((= t1 false)) + :args (t1) + :conclusion (= (not t1) true) +) +(declare-rule bool-not-false ((t1 Bool)) + :premises ((= t1 true)) + :args (t1) + :conclusion (= (not t1) false) +) +(declare-rule bool-eq-true ((t1 Bool)) + :args (t1) + :conclusion (= (= t1 true) t1) +) +(declare-rule bool-eq-false ((t1 Bool)) + :args (t1) + :conclusion (= (= t1 false) (not t1)) +) +(declare-rule bool-eq-nrefl ((x1 Bool)) + :args (x1) + :conclusion (= (= x1 (not x1)) false) +) +(declare-rule bool-impl-false1 ((t1 Bool)) + :args (t1) + :conclusion (= (=> t1 false) (not t1)) +) +(declare-rule bool-impl-false2 ((t1 Bool)) + :args (t1) + :conclusion (= (=> false t1) true) +) +(declare-rule bool-impl-true1 ((t1 Bool)) + :args (t1) + :conclusion (= (=> t1 true) true) +) +(declare-rule bool-impl-true2 ((t1 Bool)) + :args (t1) + :conclusion (= (=> true t1) t1) +) +(declare-rule bool-impl-elim ((t1 Bool) (s1 Bool)) + :args (t1 s1) + :conclusion (= (=> t1 s1) (or (not t1) s1)) +) +(declare-rule bool-dual-impl-eq ((t1 Bool) (s1 Bool)) + :args (t1 s1) + :conclusion (= (and (=> t1 s1) (=> s1 t1)) (= t1 s1)) +) +(declare-rule bool-implies-de-morgan ((x1 Bool) (y1 Bool)) + :args (x1 y1) + :conclusion (= (not (=> x1 y1)) (and x1 (not y1))) +) +(declare-rule bool-xor-refl ((x1 Bool)) + :args (x1) + :conclusion (= (xor x1 x1) false) +) +(declare-rule bool-xor-nrefl ((x1 Bool)) + :args (x1) + :conclusion (= (xor x1 (not x1)) true) +) +(declare-rule bool-xor-false ((x1 Bool)) + :args (x1) + :conclusion (= (xor x1 false) x1) +) +(declare-rule bool-xor-true ((x1 Bool)) + :args (x1) + :conclusion (= (xor x1 true) (not x1)) +) +(declare-rule bool-xor-comm ((x1 Bool) (y1 Bool)) + :args (x1 y1) + :conclusion (= (xor x1 y1) (xor y1 x1)) +) +(declare-rule bool-xor-elim ((x1 Bool) (y1 Bool)) + :args (x1 y1) + :conclusion (= (xor x1 y1) (= (not x1) y1)) +) +(declare-rule bool-not-xor-elim ((x1 Bool) (y1 Bool)) + :args (x1 y1) + :conclusion (= (not (xor x1 y1)) (= x1 y1)) +) +(declare-rule bool-not-eq-elim1 ((x1 Bool) (y1 Bool)) + :args (x1 y1) + :conclusion (= (not (= x1 y1)) (= (not x1) y1)) +) +(declare-rule bool-not-eq-elim2 ((x1 Bool) (y1 Bool)) + :args (x1 y1) + :conclusion (= (not (= x1 y1)) (= x1 (not y1))) +) + +;;;;;;;;;;;;;;;;; +;; Ite +;;;;;;;;;;;;;;;;; + +(declare-rule ite-neg-branch ((c1 Bool) (x1 Bool) (y1 Bool)) + :premises ((= (not y1) x1)) + :args (c1 x1 y1) + :conclusion (= (ite c1 x1 y1) (= c1 x1)) +) +(declare-rule ite-then-true ((c1 Bool) (x1 Bool)) + :args (c1 x1) + :conclusion (= (ite c1 true x1) (or c1 x1)) +) +(declare-rule ite-else-false ((c1 Bool) (x1 Bool)) + :args (c1 x1) + :conclusion (= (ite c1 x1 false) (and c1 x1)) +) +(declare-rule ite-then-false ((c1 Bool) (x1 Bool)) + :args (c1 x1) + :conclusion (= (ite c1 false x1) (and (not c1) x1)) +) +(declare-rule ite-else-true ((c1 Bool) (x1 Bool)) + :args (c1 x1) + :conclusion (= (ite c1 x1 true) (or (not c1) x1)) +) +(declare-rule ite-then-lookahead-self ((c1 Bool) (x1 Bool)) + :args (c1 x1) + :conclusion (= (ite c1 c1 x1) (ite c1 true x1)) +) +(declare-rule ite-else-lookahead-self ((c1 Bool) (x1 Bool)) + :args (c1 x1) + :conclusion (= (ite c1 x1 c1) (ite c1 x1 false)) +) +(declare-rule ite-then-lookahead-not-self ((c1 Bool) (x1 Bool)) + :args (c1 x1) + :conclusion (= (ite c1 (not c1) x1) (ite c1 false x1)) +) +(declare-rule ite-else-lookahead-not-self ((c1 Bool) (x1 Bool)) + :args (c1 x1) + :conclusion (= (ite c1 x1 (not c1)) (ite c1 x1 true)) +) +(declare-rule ite-expand ((c1 Bool) (x1 Bool) (y1 Bool)) + :args (c1 x1 y1) + :conclusion (= (ite c1 x1 y1) (and (or (not c1) x1) (or c1 y1))) +) +(declare-rule bool-not-ite-elim ((c1 Bool) (x1 Bool) (y1 Bool)) + :args (c1 x1 y1) + :conclusion (= (not (ite c1 x1 y1)) (ite c1 (not x1) (not y1))) +) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Strings and regular expressions +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(declare-rule str-eq-len-false ((x1 String) (y1 String)) + :premises ((= (= (str.len x1) (str.len y1)) false)) + :args (x1 y1) + :conclusion (= (= x1 y1) false) +) +(declare-rule str-indexof-re-none ((t1 String) (n1 Int)) + :args (t1 n1) + :conclusion (= (str.indexof_re t1 re.none n1) -1) +) +(declare-rule str-indexof-re-emp-re ((t1 String) (r1 RegLan) (n1 Int)) + :premises ((= (str.in_re "" r1) true) (= (>= (str.len t1) n1) true)) + :args (t1 r1 n1) + :conclusion (= (str.indexof_re t1 r1 n1) n1) +) +(declare-rule str-to-lower-upper ((s1 String)) + :args (s1) + :conclusion (= (str.to_lower (str.to_upper s1)) (str.to_lower s1)) +) +(declare-rule str-to-upper-lower ((s1 String)) + :args (s1) + :conclusion (= (str.to_upper (str.to_lower s1)) (str.to_upper s1)) +) +(declare-rule str-to-lower-len ((s1 String)) + :args (s1) + :conclusion (= (str.len (str.to_lower s1)) (str.len s1)) +) +(declare-rule str-to-upper-len ((s1 String)) + :args (s1) + :conclusion (= (str.len (str.to_upper s1)) (str.len s1)) +) +(declare-rule str-to-lower-from-int ((n1 Int)) + :args (n1) + :conclusion (= (str.to_lower (str.from_int n1)) (str.from_int n1)) +) +(declare-rule str-to-upper-from-int ((n1 Int)) + :args (n1) + :conclusion (= (str.to_upper (str.from_int n1)) (str.from_int n1)) +) +(declare-rule str-leq-empty ((s1 String)) + :args (s1) + :conclusion (= (str.<= "" s1) true) +) +(declare-rule str-leq-empty-eq ((s1 String)) + :args (s1) + :conclusion (= (str.<= s1 "") (= s1 "")) +) +(declare-rule str-lt-elim ((s1 String) (t1 String)) + :args (s1 t1) + :conclusion (= (str.< s1 t1) (and (not (= s1 t1)) (str.<= s1 t1))) +) +(declare-rule str-from-int-no-ctn-nondigit ((n1 Int) (s1 String)) + :premises ((= (= s1 "") false) (= (str.to_int s1) -1)) + :args (n1 s1) + :conclusion (= (str.contains (str.from_int n1) s1) false) +) +(declare-rule re-all-elim () + :args () + :conclusion (= re.all (re.* re.allchar)) +) +(declare-rule re-opt-elim ((x1 RegLan)) + :args (x1) + :conclusion (= (re.opt x1) (re.union (str.to_re "") x1)) +) +(declare-rule re-diff-elim ((x1 RegLan) (y1 RegLan)) + :args (x1 y1) + :conclusion (= (re.diff x1 y1) (re.inter x1 (re.comp y1))) +) +(declare-rule re-plus-elim ((x1 RegLan)) + :args (x1) + :conclusion (= (re.+ x1) (re.++ x1 (re.* x1))) +) +(declare-rule re-repeat-elim ((n1 Int) (x1 RegLan)) + :args (n1 x1) + :conclusion (= (re.^ n1 x1) (re.loop n1 n1 x1)) +) +(declare-rule re-union-const-elim ((r1 RegLan) (s1 String)) + :premises ((= (str.in_re s1 r1) true)) + :args (r1 s1) + :conclusion (= (re.union (str.to_re s1) r1) r1) +) +(declare-rule re-star-none () + :args () + :conclusion (= (re.* re.none) (str.to_re "")) +) +(declare-rule re-star-emp () + :args () + :conclusion (= (re.* (str.to_re "")) (str.to_re "")) +) +(declare-rule re-star-star ((x1 RegLan)) + :args (x1) + :conclusion (= (re.* (re.* x1)) (re.* x1)) +) +(declare-rule re-loop-neg ((n1 Int) (m1 Int) (r1 RegLan)) + :premises ((= (> n1 m1) true)) + :args (n1 m1 r1) + :conclusion (= (re.loop n1 m1 r1) re.none) +) +(declare-rule re-in-empty ((t1 String)) + :args (t1) + :conclusion (= (str.in_re t1 re.none) false) +) +(declare-rule re-in-sigma ((t1 String)) + :args (t1) + :conclusion (= (str.in_re t1 re.allchar) (= (str.len t1) 1)) +) +(declare-rule re-in-sigma-star ((t1 String)) + :args (t1) + :conclusion (= (str.in_re t1 (re.* re.allchar)) true) +) +(declare-rule re-in-cstring ((t1 String) (s1 String)) + :args (t1 s1) + :conclusion (= (str.in_re t1 (str.to_re s1)) (= t1 s1)) +) +(declare-rule re-in-comp ((t1 String) (r1 RegLan)) + :args (t1 r1) + :conclusion (= (str.in_re t1 (re.comp r1)) (not (str.in_re t1 r1))) +) + +(declare-rule str-in-re-from-int-dig-range ((n1 Int)) + :args (n1) + :conclusion (= (str.in_re (str.from_int n1) (re.* (re.range "0" "9"))) true) +) diff --git a/Tests/RareAsEunoiaTests/level1_rewrites.eo b/Tests/RareAsEunoiaTests/level1_rewrites.eo new file mode 100644 index 0000000..be91353 --- /dev/null +++ b/Tests/RareAsEunoiaTests/level1_rewrites.eo @@ -0,0 +1,120 @@ +;;;;;;;;;;;;;;;;; +;; Arith +;;;;;;;;;;;;;;;;; + +(declare-rule arith-div-total-zero-real ((@T0 Type) (t1 @T0)) + :args (t1) + :conclusion (= (/_total t1 0/1) 0/1) +) +(declare-rule arith-div-total-zero-int ((@T0 Type) (t1 @T0)) + :args (t1) + :conclusion (= (/_total t1 0) 0/1) +) +(declare-rule arith-elim-gt ((@T0 Type) (@T1 Type) (t1 @T0) (s1 @T1)) + :args (t1 s1) + :conclusion (= (> t1 s1) (not (>= s1 t1))) +) +(declare-rule arith-elim-lt ((@T0 Type) (@T1 Type) (t1 @T0) (s1 @T1)) + :args (t1 s1) + :conclusion (= (< t1 s1) (not (>= t1 s1))) +) +(declare-rule arith-elim-leq ((@T0 Type) (@T1 Type) (t1 @T0) (s1 @T1)) + :args (t1 s1) + :conclusion (= (<= t1 s1) (>= s1 t1)) +) +(declare-rule arith-abs-eq ((@T0 Type) (@T1 Type) (x1 @T0) (y1 @T1)) + :args (x1 y1) + :conclusion (= (= (abs x1) (abs y1)) (or (= x1 y1) (= x1 (- y1)))) +) +(declare-rule arith-geq-ite-lift ((@T0 Type) (@T1 Type) (@T2 Type) (C1 Bool) (t1 @T0) (s1 @T1) (r1 @T2)) + :args (C1 t1 s1 r1) + :conclusion (= (>= (ite C1 t1 s1) r1) (ite C1 (>= t1 r1) (>= s1 r1))) +) +(declare-rule arith-leq-ite-lift ((@T0 Type) (@T1 Type) (@T2 Type) (C1 Bool) (t1 @T0) (s1 @T1) (r1 @T2)) + :args (C1 t1 s1 r1) + :conclusion (= (<= (ite C1 t1 s1) r1) (ite C1 (<= t1 r1) (<= s1 r1))) +) +(declare-rule arith-min-lt1 ((@T0 Type) (@T1 Type) (t1 @T0) (s1 @T1)) + :args (t1 s1) + :conclusion (= (<= (ite (< t1 s1) t1 s1) t1) true) +) +(declare-rule arith-min-lt2 ((@T0 Type) (@T1 Type) (t1 @T0) (s1 @T1)) + :args (t1 s1) + :conclusion (= (<= (ite (< t1 s1) t1 s1) s1) true) +) +(declare-rule arith-max-geq1 ((@T0 Type) (@T1 Type) (t1 @T0) (s1 @T1)) + :args (t1 s1) + :conclusion (= (>= (ite (>= t1 s1) t1 s1) t1) true) +) +(declare-rule arith-max-geq2 ((@T0 Type) (@T1 Type) (t1 @T0) (s1 @T1)) + :args (t1 s1) + :conclusion (= (>= (ite (>= t1 s1) t1 s1) s1) true) +) + +;;;;;;;;;;;;;;;;; +;; Ite +;;;;;;;;;;;;;;;;; + +(declare-rule ite-true-cond ((@T0 Type) (@T1 Type) (x1 @T0) (y1 @T1)) + :args (x1 y1) + :conclusion (= (ite true x1 y1) x1) +) +(declare-rule ite-false-cond ((@T0 Type) (@T1 Type) (x1 @T0) (y1 @T1)) + :args (x1 y1) + :conclusion (= (ite false x1 y1) y1) +) +(declare-rule ite-not-cond ((@T0 Type) (@T1 Type) (c1 Bool) (x1 @T0) (y1 @T1)) + :args (c1 x1 y1) + :conclusion (= (ite (not c1) x1 y1) (ite c1 y1 x1)) +) +(declare-rule ite-eq-branch ((@T0 Type) (c1 Bool) (x1 @T0)) + :args (c1 x1) + :conclusion (= (ite c1 x1 x1) x1) +) +(declare-rule ite-then-lookahead ((@T0 Type) (@T1 Type) (@T2 Type) (c1 Bool) (x1 @T0) (y1 @T1) (z1 @T2)) + :args (c1 x1 y1 z1) + :conclusion (= (ite c1 (ite c1 x1 y1) z1) (ite c1 x1 z1)) +) +(declare-rule ite-else-lookahead ((@T0 Type) (@T1 Type) (@T2 Type) (c1 Bool) (x1 @T0) (y1 @T1) (z1 @T2)) + :args (c1 x1 y1 z1) + :conclusion (= (ite c1 x1 (ite c1 y1 z1)) (ite c1 x1 z1)) +) +(declare-rule ite-then-neg-lookahead ((@T0 Type) (@T1 Type) (@T2 Type) (c1 Bool) (x1 @T0) (y1 @T1) (z1 @T2)) + :args (c1 x1 y1 z1) + :conclusion (= (ite c1 (ite (not c1) x1 y1) z1) (ite c1 y1 z1)) +) +(declare-rule ite-else-neg-lookahead ((@T0 Type) (@T1 Type) (@T2 Type) (c1 Bool) (x1 @T0) (y1 @T1) (z1 @T2)) + :args (c1 x1 y1 z1) + :conclusion (= (ite c1 x1 (ite (not c1) y1 z1)) (ite c1 x1 y1)) +) + +;;;;;;;;;;;;;;;;; +;; Equality +;;;;;;;;;;;;;;;;; + +(declare-rule eq-refl ((@T0 Type) (t1 @T0)) + :args (t1) + :conclusion (= (= t1 t1) true) +) +(declare-rule eq-symm ((@T0 Type) (@T1 Type) (t1 @T0) (s1 @T1)) + :args (t1 s1) + :conclusion (= (= t1 s1) (= s1 t1)) +) +(declare-rule eq-cond-deq ((@T0 Type) (@T1 Type) (@T2 Type) (t1 @T0) (s1 @T1) (r1 @T2)) + :premises ((= (= s1 r1) false)) + :args (t1 s1 r1) + :conclusion (= (= (= t1 s1) (= t1 r1)) (and (not (= t1 s1)) (not (= t1 r1)))) +) +(declare-rule eq-ite-lift ((@T0 Type) (@T1 Type) (@T2 Type) (C1 Bool) (t1 @T0) (s1 @T1) (r1 @T2)) + :args (C1 t1 s1 r1) + :conclusion (= (= (ite C1 t1 s1) r1) (ite C1 (= t1 r1) (= s1 r1))) +) + +;;;;;;;;;;;;;;;;; +;; Distinct +;;;;;;;;;;;;;;;;; + +(declare-rule distinct-binary-elim ((@T0 Type) (@T1 Type) (t1 @T0) (s1 @T1)) + :args (t1 s1) + :conclusion (= (distinct t1 s1) (not (= t1 s1))) +) diff --git a/Tests/RareAsEunoiaTests/level2_rewrites.eo b/Tests/RareAsEunoiaTests/level2_rewrites.eo new file mode 100644 index 0000000..fa97dff --- /dev/null +++ b/Tests/RareAsEunoiaTests/level2_rewrites.eo @@ -0,0 +1,136 @@ +;;;;;;;;;;;;;;;;; +;; Arith +;;;;;;;;;;;;;;;;; + +(declare-rule arith-mod-over-mod ((c1 Int) (ts1 Int :list) (r1 Int) (ss1 Int :list)) + :premises ((= (= c1 0) false)) + :args (c1 ts1 r1 ss1) + :conclusion (= (mod_total (+ ts1 (mod_total r1 c1) ss1) c1) (mod_total (+ ts1 r1 ss1) c1)) +) + +;;;;;;;;;;;;;;;;; +;; Boolean +;;;;;;;;;;;;;;;;; + +(declare-rule bool-and-conf ((xs1 Bool :list) (w1 Bool) (ys1 Bool :list) (zs1 Bool :list)) + :args (xs1 w1 ys1 zs1) + :conclusion (= (and xs1 w1 ys1 (not w1) zs1) false) +) +(declare-rule bool-and-conf2 ((xs1 Bool :list) (w1 Bool) (ys1 Bool :list) (zs1 Bool :list)) + :args (xs1 w1 ys1 zs1) + :conclusion (= (and xs1 (not w1) ys1 w1 zs1) false) +) +(declare-rule bool-or-taut ((xs1 Bool :list) (w1 Bool) (ys1 Bool :list) (zs1 Bool :list)) + :args (xs1 w1 ys1 zs1) + :conclusion (= (or xs1 w1 ys1 (not w1) zs1) true) +) +(declare-rule bool-or-taut2 ((xs1 Bool :list) (w1 Bool) (ys1 Bool :list) (zs1 Bool :list)) + :args (xs1 w1 ys1 zs1) + :conclusion (= (or xs1 (not w1) ys1 w1 zs1) true) +) +(declare-rule bool-or-de-morgan ((x1 Bool) (y1 Bool) (zs1 Bool :list)) + :args (x1 y1 zs1) + :conclusion (= (not (or x1 y1 zs1)) (and (not x1) (not (or y1 zs1)))) +) + +(declare-rule bool-and-de-morgan ((x1 Bool) (y1 Bool) (zs1 Bool :list)) + :args (x1 y1 zs1) + :conclusion (= (not (and x1 y1 zs1)) (or (not x1) (not (and y1 zs1)))) +) +(declare-rule bool-or-and-distrib ((y1 Bool) (y2 Bool) (ys1 Bool :list) (z1 Bool) (zs1 Bool :list)) + :args (y1 y2 ys1 z1 zs1) + :conclusion (= (or (and y1 y2 ys1) z1 zs1) (and (or y1 z1 zs1) (or (and y2 ys1) z1 zs1))) +) +(declare-rule bool-implies-or-distrib ((y1 Bool) (y2 Bool) (ys1 Bool :list) (z1 Bool)) + :args (y1 y2 ys1 z1) + :conclusion (= (=> (or y1 y2 ys1) z1) (and (=> y1 z1) (=> (or y2 ys1) z1))) +) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Strings and regular expressions +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(declare-rule str-to-lower-concat ((s1 String) (s2 String) (s3 String :list)) + :args (s1 s2 s3) + :conclusion (= (str.to_lower (str.++ s1 s2 s3)) (str.++ (str.to_lower s1) (str.to_lower (str.++ s2 s3)))) +) +(declare-rule str-to-upper-concat ((s1 String) (s2 String) (s3 String :list)) + :args (s1 s2 s3) + :conclusion (= (str.to_upper (str.++ s1 s2 s3)) (str.++ (str.to_upper s1) (str.to_upper (str.++ s2 s3)))) +) + +(declare-rule str-to-int-concat-neg-one ((s1 String :list) (s2 String) (s3 String :list)) + :premises ((= (str.to_int s2) -1)) + :args (s1 s2 s3) + :conclusion (= (str.to_int (str.++ s1 s2 s3)) -1) +) +(declare-rule str-leq-concat-false ((s1 String :list) (t1 String) (s2 String) (t2 String :list) (s3 String :list)) + :premises ((= (str.len t1) (str.len s2)) (= (str.<= t1 s2) false)) + :args (s1 t1 s2 t2 s3) + :conclusion (= (str.<= (str.++ s1 t1 t2) (str.++ s1 s2 s3)) false) +) +(declare-rule str-leq-concat-true ((s1 String :list) (t1 String) (s2 String) (t2 String :list) (s3 String :list)) + :premises ((= (str.len t1) (str.len s2)) (= (= t1 s2) false) (= (str.<= t1 s2) true)) + :args (s1 t1 s2 t2 s3) + :conclusion (= (str.<= (str.++ s1 t1 t2) (str.++ s1 s2 s3)) true) +) +(declare-rule str-leq-concat-base-1 ((t1 String) (t2 String :list) (s1 String)) + :premises ((= (str.len t1) (str.len s1)) (= (= t1 s1) false)) + :args (t1 t2 s1) + :conclusion (= (str.<= (str.++ t1 t2) s1) (str.<= t1 s1)) +) +(declare-rule str-leq-concat-base-2 ((t1 String) (s1 String) (s2 String :list)) + :premises ((= (str.len t1) (str.len s1)) (= (= t1 s1) false)) + :args (t1 s1 s2) + :conclusion (= (str.<= t1 (str.++ s1 s2)) (str.<= t1 s1)) +) + +(declare-rule re-concat-star-swap ((xs1 RegLan :list) (r1 RegLan) (ys1 RegLan :list)) + :args (xs1 r1 ys1) + :conclusion (= (re.++ xs1 (re.* r1) r1 ys1) (re.++ xs1 r1 (re.* r1) ys1)) +) + +(declare-rule re-concat-star-subsume1 ((xs1 RegLan :list) (r1 RegLan) (ys1 RegLan :list)) + :args (xs1 r1 ys1) + :conclusion (= (re.++ xs1 (re.* r1) (re.* re.allchar) ys1) (re.++ xs1 (re.* re.allchar) ys1)) +) +(declare-rule re-concat-star-subsume2 ((xs1 RegLan :list) (r1 RegLan) (ys1 RegLan :list)) + :args (xs1 r1 ys1) + :conclusion (= (re.++ xs1 (re.* re.allchar) (re.* r1) ys1) (re.++ xs1 (re.* re.allchar) ys1))) +(declare-rule re-concat-merge ((xs1 RegLan :list) (s1 String) (t1 String) (ys1 RegLan :list)) + :args (xs1 s1 t1 ys1) + :conclusion (= (re.++ xs1 (str.to_re s1) (str.to_re t1) ys1) (re.++ xs1 (str.to_re (str.++ s1 t1) ys1))) +) +(declare-rule re-union-all ((xs1 RegLan :list) (ys1 RegLan :list)) + :args (xs1 ys1) + :conclusion (= (re.union xs1 (re.* re.allchar) ys1) (re.* re.allchar)) +) + +(declare-rule re-inter-all ((xs1 RegLan :list) (ys1 RegLan :list)) + :args (xs1 ys1) + :conclusion (= (re.inter xs1 (re.* re.allchar) ys1) (re.inter xs1 ys1)) +) + +(declare-rule re-star-union-drop-emp ((x1 RegLan :list) (y1 RegLan :list)) + :args (x1 y1) + :conclusion (= (re.* (re.union x1 (str.to_re "") y1)) (re.* (re.union x1 y1))) +) + +(declare-rule re-inter-cstring ((xs1 RegLan :list) (ys1 RegLan :list) (s1 String)) + :premises ((= (str.in_re s1 (re.inter xs1 ys1)) true)) + :args (xs1 ys1 s1) + :conclusion (= (re.inter xs1 (str.to_re s1) ys1) (str.to_re s1)) +) +(declare-rule re-inter-cstring-neg ((xs1 RegLan :list) (ys1 RegLan :list) (s1 String)) + :premises ((= (str.in_re s1 (re.inter xs1 ys1)) false)) + :args (xs1 ys1 s1) + :conclusion (= (re.inter xs1 (str.to_re s1) ys1) re.none) +) +(declare-rule str-in-re-union-elim ((s1 String) (r1 RegLan) (r2 RegLan) (rs1 RegLan :list)) + :args (s1 r1 r2 rs1) + :conclusion (= (str.in_re s1 (re.union r1 r2 rs1)) (or (str.in_re s1 r1) (str.in_re s1 (re.union r2 rs1)))) +) +(declare-rule str-in-re-inter-elim ((s1 String) (r1 RegLan) (r2 RegLan) (rs1 RegLan :list)) + :args (s1 r1 r2 rs1) + :conclusion (= (str.in_re s1 (re.inter r1 r2 rs1)) (and (str.in_re s1 r1) (str.in_re s1 (re.inter r2 rs1)))) +) diff --git a/Tests/RareAsEunoiaTests/level3_rewrites.eo b/Tests/RareAsEunoiaTests/level3_rewrites.eo new file mode 100644 index 0000000..fd8594a --- /dev/null +++ b/Tests/RareAsEunoiaTests/level3_rewrites.eo @@ -0,0 +1,1133 @@ +;;;;;;;;;;;;;;;;; +;; Bitvectors +;;;;;;;;;;;;;;;;; + +(declare-rule bv-extract-extract ((@n0 Int) (x1 (BitVec @n0)) (i1 Int) (j1 Int) (k1 Int) (l1 Int) (ll1 Int) (kk1 Int)) + :premises ((= ll1 (+ i1 l1)) (= kk1 (+ i1 k1))) + :args (x1 i1 j1 k1 l1 ll1 kk1) + :conclusion (= (extract l1 k1 (extract j1 i1 x1)) (extract ll1 kk1 x1)) +) +(declare-rule bv-extract-whole ((@n0 Int) (x1 (BitVec @n0)) (n1 Int)) + :premises ((= (>= n1 (- (@bvsize x1) 1)) true)) + :args (x1 n1) + :conclusion (= (extract n1 0 x1) x1) +) +(declare-rule bv-extract-concat-1 ((@n0 Int) (@n1 Int) (@n2 Int) (x1 (BitVec @n0)) (xs1 (BitVec @n1) :list) (y1 (BitVec @n2)) (i1 Int) (j1 Int)) + :premises ((= (<= j1 (@bvsize x1)) true)) + :args (x1 xs1 y1 i1 j1) + :conclusion (= (extract j1 i1 (concat xs1 y1 x1)) (extract j1 i1 x1)) +) +(declare-rule bv-eq-extract-elim1 ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (i1 Int) (j1 Int) (wm1 Int) (jp1 Int) (im1 Int)) + :premises ((= wm1 (- (@bvsize x1) 1)) (= jp1 (+ j1 1)) (= im1 (- i1 1)) (= (> wm1 j1) true) (= (> i1 0) true)) + :args (x1 y1 i1 j1 wm1 jp1 im1) + :conclusion (= (= (extract j1 i1 x1) y1) (= x1 (concat (extract wm1 jp1 x1) y1 (extract im1 0 x1)))) +) +(declare-rule bv-eq-extract-elim2 ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (j1 Int) (wm1 Int) (jp1 Int)) + :premises ((= wm1 (- (@bvsize x1) 1)) (= jp1 (+ j1 1)) (= (> wm1 j1) true)) + :args (x1 y1 j1 wm1 jp1) + :conclusion (= (= (extract j1 0 x1) y1) (= x1 (concat (extract wm1 jp1 x1) y1))) +) +(declare-rule bv-eq-extract-elim3 ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (i1 Int) (j1 Int) (im1 Int)) + :premises ((= j1 (- (@bvsize x1) 1)) (= im1 (- i1 1)) (= (> i1 0) true)) + :args (x1 y1 i1 j1 im1) + :conclusion (= (= (extract j1 i1 x1) y1) (= x1 (concat y1 (extract im1 0 x1)))) +) +(declare-rule bv-extract-not ((@n0 Int) (x1 (BitVec @n0)) (i1 Int) (j1 Int)) + :args (x1 i1 j1) + :conclusion (= (extract j1 i1 (bvnot x1)) (bvnot (extract j1 i1 x1))) +) +(declare-rule bv-extract-sign-extend-1 ((@n0 Int) (x1 (BitVec @n0)) (low1 Int) (high1 Int) (k1 Int)) + :premises ((= (< high1 (@bvsize x1)) true)) + :args (x1 low1 high1 k1) + :conclusion (= (extract high1 low1 (sign_extend k1 x1)) (extract high1 low1 x1)) +) +(declare-rule bv-extract-sign-extend-2 ((@n0 Int) (x1 (BitVec @n0)) (low1 Int) (high1 Int) (k1 Int) (nm1 Int) (sn1 Int)) + :premises ((= (< low1 (@bvsize x1)) true) (= (>= high1 (@bvsize x1)) true) (= nm1 (- (@bvsize x1) 1)) (= sn1 (+ 1 (- high1 (@bvsize x1))))) + :args (x1 low1 high1 k1 nm1 sn1) + :conclusion (= (extract high1 low1 (sign_extend k1 x1)) (sign_extend sn1 (extract nm1 low1 x1))) +) +(declare-rule bv-extract-sign-extend-3 ((@n0 Int) (x1 (BitVec @n0)) (low1 Int) (high1 Int) (k1 Int) (rn1 Int) (nm1 Int)) + :premises ((= (>= low1 (@bvsize x1)) true) (= rn1 (+ 1 (- high1 low1))) (= nm1 (- (@bvsize x1) 1))) + :args (x1 low1 high1 k1 rn1 nm1) + :conclusion (= (extract high1 low1 (sign_extend k1 x1)) (repeat rn1 (extract nm1 nm1 x1))) +) +(declare-rule bv-commutative-xor ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1))) + :args (x1 y1) + :conclusion (= (bvxor x1 y1) (bvxor y1 x1)) +) +(declare-rule bv-commutative-comp ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1))) + :args (x1 y1) + :conclusion (= (bvcomp x1 y1) (bvcomp y1 x1)) +) +(declare-rule bv-zero-extend-eliminate-0 ((@n0 Int) (x1 (BitVec @n0))) + :args (x1) + :conclusion (= (zero_extend 0 x1) x1) +) +(declare-rule bv-sign-extend-eliminate-0 ((@n0 Int) (x1 (BitVec @n0))) + :args (x1) + :conclusion (= (sign_extend 0 x1) x1) +) +(declare-rule bv-not-neq ((@n0 Int) (x1 (BitVec @n0))) + :premises ((= (> (@bvsize x1) 0) true)) + :args (x1) + :conclusion (= (= x1 (bvnot x1)) false) +) +(declare-rule bv-ult-ones ((@n0 Int) (x1 (BitVec @n0)) (n1 Int) (w1 Int)) + :premises ((= n1 (- (int.pow2 w1) 1))) + :args (x1 n1 w1) + :conclusion (= (bvult x1 (@bv n1 w1)) (distinct x1 (@bv n1 w1))) +) +(declare-rule bv-commutative-add ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1))) + :args (x1 y1) + :conclusion (= (bvadd x1 y1) (bvadd y1 x1)) +) +(declare-rule bv-sub-eliminate ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1))) + :args (x1 y1) + :conclusion (= (bvsub x1 y1) (bvadd x1 (bvneg y1))) +) +(declare-rule bv-eq-xor-solve ((@n0 Int) (@n1 Int) (@n2 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (z1 (BitVec @n2))) + :args (x1 y1 z1) + :conclusion (= (= (= (bvxor x1 y1) z1) (= x1 (bvxor z1 y1))) true) +) +(declare-rule bv-eq-not-solve ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1))) + :args (x1 y1) + :conclusion (= (= (= (bvnot x1) y1) (= x1 (bvnot y1))) true) +) +(declare-rule bv-ugt-eliminate ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1))) + :args (x1 y1) + :conclusion (= (bvugt x1 y1) (bvult y1 x1)) +) +(declare-rule bv-uge-eliminate ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1))) + :args (x1 y1) + :conclusion (= (bvuge x1 y1) (bvule y1 x1)) +) +(declare-rule bv-sgt-eliminate ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1))) + :args (x1 y1) + :conclusion (= (bvsgt x1 y1) (bvslt y1 x1)) +) +(declare-rule bv-sge-eliminate ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1))) + :args (x1 y1) + :conclusion (= (bvsge x1 y1) (bvsle y1 x1)) +) +(declare-rule bv-sle-eliminate ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1))) + :args (x1 y1) + :conclusion (= (bvsle x1 y1) (not (bvslt y1 x1))) +) +(declare-rule bv-redor-eliminate ((@n0 Int) (x1 (BitVec @n0)) (w1 Int)) + :premises ((= w1 (@bvsize x1))) + :args (x1 w1) + :conclusion (= (bvredor x1) (bvnot (bvcomp x1 (@bv 0 w1)))) +) +(declare-rule bv-redand-eliminate ((@n0 Int) (x1 (BitVec @n0)) (w1 Int)) + :premises ((= w1 (@bvsize x1))) + :args (x1 w1) + :conclusion (= (bvredand x1) (bvcomp x1 (bvnot (@bv 0 w1)))) +) +(declare-rule bv-ule-eliminate ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1))) + :args (x1 y1) + :conclusion (= (bvule x1 y1) (not (bvult y1 x1))) +) +(declare-rule bv-comp-eliminate ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1))) + :args (x1 y1) + :conclusion (= (bvcomp x1 y1) (ite (= x1 y1) (@bv 1 1) (@bv 0 1))) +) +(declare-rule bv-rotate-left-eliminate-2 ((@n0 Int) (x1 (BitVec @n0)) (amount1 Int)) + :premises ((= (mod amount1 (@bvsize x1)) 0)) + :args (x1 amount1) + :conclusion (= (rotate_left amount1 x1) x1) +) +(declare-rule bv-rotate-right-eliminate-1 ((@n0 Int) (x1 (BitVec @n0)) (amount1 Int) (u1 Int) (u2 Int) (l1 Int)) + :premises ((= (= (mod amount1 (@bvsize x1)) 0) false) (= u1 (- (mod amount1 (@bvsize x1)) 1)) (= u2 (- (@bvsize x1) 1)) (= l1 (mod amount1 (@bvsize x1)))) + :args (x1 amount1 u1 u2 l1) + :conclusion (= (rotate_right amount1 x1) (concat (extract u1 0 x1) (extract u2 l1 x1))) +) +(declare-rule bv-rotate-right-eliminate-2 ((@n0 Int) (x1 (BitVec @n0)) (amount1 Int)) + :premises ((= (mod amount1 (@bvsize x1)) 0)) + :args (x1 amount1) + :conclusion (= (rotate_right amount1 x1) x1) +) +(declare-rule bv-nand-eliminate ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1))) + :args (x1 y1) + :conclusion (= (bvnand x1 y1) (bvnot (bvand x1 y1))) +) +(declare-rule bv-nor-eliminate ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1))) + :args (x1 y1) + :conclusion (= (bvnor x1 y1) (bvnot (bvor x1 y1))) +) +(declare-rule bv-xnor-eliminate ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1))) + :args (x1 y1) + :conclusion (= (bvxnor x1 y1) (bvnot (bvxor x1 y1))) +) +(declare-rule bv-zero-extend-eliminate ((@n0 Int) (x1 (BitVec @n0)) (n1 Int)) + :args (x1 n1) + :conclusion (= (zero_extend n1 x1) (concat (@bv 0 n1) x1)) +) +(declare-rule bv-sdivo-eliminate ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (w1 Int) (wm1 Int)) + :premises ((= wm1 (- (@bvsize x1) 1)) (= w1 (@bvsize y1))) + :args (x1 y1 w1 wm1) + :conclusion (= (bvsdivo x1 y1) (and (= x1 (concat (@bv 1 1) (@bv 0 wm1))) (= y1 (bvnot (@bv 0 w1))))) +) +(declare-rule bv-usubo-eliminate ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (n1 Int)) + :premises ((= n1 (@bvsize x1))) + :args (x1 y1 n1) + :conclusion (= (bvusubo x1 y1) (= (extract n1 n1 (bvsub (zero_extend 1 x1) (zero_extend 1 y1))) (@bv 1 1))) +) +(declare-rule bv-nego-eliminate ((@n0 Int) (x1 (BitVec @n0)) (n1 Int)) + :premises ((= n1 (- (@bvsize x1) 1))) + :args (x1 n1) + :conclusion (= (bvnego x1) (= x1 (concat (@bv 1 1) (@bv 0 n1)))) +) +(declare-rule bv-ite-equal-children ((@n0 Int) (c1 (_ BitVec 1)) (x1 (BitVec @n0))) + :args (c1 x1) + :conclusion (= (bvite c1 x1 x1) x1) +) +(declare-rule bv-ite-const-children-1 ((c1 (_ BitVec 1))) + :args (c1) + :conclusion (= (bvite c1 (@bv 0 1) (@bv 1 1)) (bvnot c1)) +) +(declare-rule bv-ite-const-children-2 ((c1 (_ BitVec 1))) + :args (c1) + :conclusion (= (bvite c1 (@bv 1 1) (@bv 0 1)) c1) +) +(declare-rule bv-ite-equal-cond-1 ((@n0 Int) (@n1 Int) (@n2 Int) (c1 (_ BitVec 1)) (t1 (BitVec @n0)) (e1 (BitVec @n1)) (e2 (BitVec @n2))) + :args (c1 t1 e1 e2) + :conclusion (= (bvite c1 (bvite c1 t1 e1) e2) (bvite c1 t1 e2)) +) +(declare-rule bv-ite-equal-cond-2 ((@n0 Int) (@n1 Int) (@n2 Int) (c1 (_ BitVec 1)) (t1 (BitVec @n0)) (t2 (BitVec @n1)) (e1 (BitVec @n2))) + :args (c1 t1 t2 e1) + :conclusion (= (bvite c1 t1 (bvite c1 t2 e1)) (bvite c1 t1 e1)) +) +(declare-rule bv-ite-equal-cond-3 ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (c1 (_ BitVec 1)) (t1 (BitVec @n0)) (e1 (BitVec @n1)) (t2 (BitVec @n2)) (e2 (BitVec @n3))) + :args (c1 t1 e1 t2 e2) + :conclusion (= (bvite c1 (bvite c1 t1 e1) (bvite c1 t2 e2)) (bvite c1 t1 e2)) +) +(declare-rule bv-ite-merge-then-if ((@n0 Int) (@n1 Int) (c1 (_ BitVec 1)) (c2 (_ BitVec 1)) (t1 (BitVec @n0)) (e1 (BitVec @n1))) + :args (c1 c2 t1 e1) + :conclusion (= (bvite c1 (bvite c2 t1 e1) t1) (bvite (bvand c1 (bvnot c2)) e1 t1)) +) +(declare-rule bv-ite-merge-else-if ((@n0 Int) (@n1 Int) (c1 (_ BitVec 1)) (c2 (_ BitVec 1)) (t1 (BitVec @n0)) (e1 (BitVec @n1))) + :args (c1 c2 t1 e1) + :conclusion (= (bvite c1 (bvite c2 t1 e1) e1) (bvite (bvand c1 c2) t1 e1)) +) +(declare-rule bv-ite-merge-then-else ((@n0 Int) (@n1 Int) (c1 (_ BitVec 1)) (c2 (_ BitVec 1)) (t1 (BitVec @n0)) (e1 (BitVec @n1))) + :args (c1 c2 t1 e1) + :conclusion (= (bvite c1 t1 (bvite c2 t1 e1)) (bvite (bvand (bvnot c1) (bvnot c2)) e1 t1)) +) +(declare-rule bv-ite-merge-else-else ((@n0 Int) (@n1 Int) (c1 (_ BitVec 1)) (c2 (_ BitVec 1)) (t1 (BitVec @n0)) (t2 (BitVec @n1))) + :args (c1 c2 t1 t2) + :conclusion (= (bvite c1 t2 (bvite c2 t1 t2)) (bvite (bvand (bvnot c1) c2) t1 t2)) +) +(declare-rule bv-shl-by-const-0 ((@n0 Int) (x1 (BitVec @n0)) (sz1 Int)) + :args (x1 sz1) + :conclusion (= (bvshl x1 (@bv 0 sz1)) x1) +) +(declare-rule bv-shl-by-const-1 ((@n0 Int) (x1 (BitVec @n0)) (amount1 Int) (sz1 Int) (en1 Int)) + :premises ((= (< amount1 (@bvsize x1)) true) (= en1 (- (@bvsize x1) (+ 1 amount1)))) + :args (x1 amount1 sz1 en1) + :conclusion (= (bvshl x1 (@bv amount1 sz1)) (concat (extract en1 0 x1) (@bv 0 amount1))) +) +(declare-rule bv-shl-by-const-2 ((@n0 Int) (x1 (BitVec @n0)) (amount1 Int) (sz1 Int) (w1 Int)) + :premises ((= (>= amount1 (@bvsize x1)) true) (= w1 (@bvsize x1))) + :args (x1 amount1 sz1 w1) + :conclusion (= (bvshl x1 (@bv amount1 sz1)) (@bv 0 w1)) +) +(declare-rule bv-lshr-by-const-0 ((@n0 Int) (x1 (BitVec @n0)) (sz1 Int)) + :args (x1 sz1) + :conclusion (= (bvlshr x1 (@bv 0 sz1)) x1) +) +(declare-rule bv-lshr-by-const-1 ((@n0 Int) (x1 (BitVec @n0)) (amount1 Int) (sz1 Int) (nm1 Int)) + :premises ((= (< amount1 (@bvsize x1)) true) (= nm1 (- (@bvsize x1) 1))) + :args (x1 amount1 sz1 nm1) + :conclusion (= (bvlshr x1 (@bv amount1 sz1)) (concat (@bv 0 amount1) (extract nm1 amount1 x1))) +) +(declare-rule bv-lshr-by-const-2 ((@n0 Int) (x1 (BitVec @n0)) (amount1 Int) (sz1 Int)) + :premises ((= (>= amount1 (@bvsize x1)) true)) + :args (x1 amount1 sz1) + :conclusion (= (bvlshr x1 (@bv amount1 sz1)) (@bv 0 sz1)) +) +(declare-rule bv-ashr-by-const-0 ((@n0 Int) (x1 (BitVec @n0)) (sz1 Int)) + :args (x1 sz1) + :conclusion (= (bvashr x1 (@bv 0 sz1)) x1) +) +(declare-rule bv-ashr-by-const-1 ((@n0 Int) (x1 (BitVec @n0)) (amount1 Int) (sz1 Int) (nm1 Int)) + :premises ((= (< amount1 (@bvsize x1)) true) (= nm1 (- (@bvsize x1) 1))) + :args (x1 amount1 sz1 nm1) + :conclusion (= (bvashr x1 (@bv amount1 sz1)) (concat (repeat amount1 (extract nm1 nm1 x1)) (extract nm1 amount1 x1))) +) +(declare-rule bv-ashr-by-const-2 ((@n0 Int) (x1 (BitVec @n0)) (amount1 Int) (sz1 Int) (nm1 Int) (rn1 Int)) + :premises ((= (>= amount1 (@bvsize x1)) true) (= nm1 (- (@bvsize x1) 1)) (= rn1 (@bvsize x1))) + :args (x1 amount1 sz1 nm1 rn1) + :conclusion (= (bvashr x1 (@bv amount1 sz1)) (repeat rn1 (extract nm1 nm1 x1))) +) +(declare-rule bv-xor-duplicate ((@n0 Int) (x1 (BitVec @n0)) (w1 Int)) + :premises ((= w1 (@bvsize x1))) + :args (x1 w1) + :conclusion (= (bvxor x1 x1) (@bv 0 w1)) +) +(declare-rule bv-xor-not ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1))) + :args (x1 y1) + :conclusion (= (bvxor (bvnot x1) (bvnot y1)) (bvxor x1 y1)) +) +(declare-rule bv-not-idemp ((@n0 Int) (x1 (BitVec @n0))) + :args (x1) + :conclusion (= (bvnot (bvnot x1)) x1) +) +(declare-rule bv-ult-zero-1 ((@n0 Int) (x1 (BitVec @n0)) (n1 Int)) + :args (x1 n1) + :conclusion (= (bvult (@bv 0 n1) x1) (not (= x1 (@bv 0 n1)))) +) +(declare-rule bv-ult-zero-2 ((@n0 Int) (x1 (BitVec @n0)) (n1 Int)) + :args (x1 n1) + :conclusion (= (bvult x1 (@bv 0 n1)) false) +) +(declare-rule bv-ult-self ((@n0 Int) (x1 (BitVec @n0))) + :args (x1) + :conclusion (= (bvult x1 x1) false) +) +(declare-rule bv-lt-self ((@n0 Int) (x1 (BitVec @n0))) + :args (x1) + :conclusion (= (bvslt x1 x1) false) +) +(declare-rule bv-ule-self ((@n0 Int) (x1 (BitVec @n0))) + :args (x1) + :conclusion (= (bvule x1 x1) true) +) +(declare-rule bv-ule-zero ((@n0 Int) (x1 (BitVec @n0)) (n1 Int)) + :args (x1 n1) + :conclusion (= (bvule x1 (@bv 0 n1)) (= x1 (@bv 0 n1))) +) +(declare-rule bv-zero-ule ((@n0 Int) (x1 (BitVec @n0)) (n1 Int)) + :args (x1 n1) + :conclusion (= (bvule (@bv 0 n1) x1) true) +) +(declare-rule bv-sle-self ((@n0 Int) (x1 (BitVec @n0))) + :args (x1) + :conclusion (= (bvsle x1 x1) true) +) +(declare-rule bv-ule-max ((@n0 Int) (x1 (BitVec @n0)) (n1 Int) (w1 Int)) + :premises ((= w1 (@bvsize x1)) (= n1 (- (int.pow2 (@bvsize x1)) 1))) + :args (x1 n1 w1) + :conclusion (= (bvule x1 (@bv n1 w1)) true) +) +(declare-rule bv-not-ult ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1))) + :args (x1 y1) + :conclusion (= (not (bvult x1 y1)) (bvule y1 x1)) +) +(declare-rule bv-mult-pow2-2b ((@n0 Int) (z1 (BitVec @n0)) (size1 Int) (n1 Int) (exponent1 Int) (u1 Int)) + :premises ((= (int.ispow2 (- (int.pow2 size1) n1)) true) (= exponent1 (int.log2 (- (int.pow2 size1) n1))) (= u1 (- (- size1 (int.log2 (- (int.pow2 size1) n1))) 1))) + :args (z1 size1 n1 exponent1 u1) + :conclusion (= (bvmul z1 (@bv n1 size1)) (concat (extract u1 0 (bvneg z1)) (@bv 0 exponent1))) +) +(declare-rule bv-extract-mult-leading-bit ((@n0 Int) (@n1 Int) (high1 Int) (low1 Int) (x1i1 Int) (x1in1 Int) (x1 (BitVec @n0)) (y1i1 Int) (y1in1 Int) (y1 (BitVec @n1)) (w1 Int)) + :premises ((= (> (+ x1in1 (@bvsize x1)) 64) true) (= (<= (- (* 2 (+ x1in1 (@bvsize x1))) (+ (ite (= x1i1 0) x1in1 (- x1in1 (+ 1 (int.log2 x1i1)))) (ite (= y1i1 0) y1in1 (- y1in1 (+ 1 (int.log2 y1i1)))))) low1) true) (= w1 (+ 1 (- high1 low1)))) + :args (high1 low1 x1i1 x1in1 x1 y1i1 y1in1 y1 w1) + :conclusion (= (extract high1 low1 (bvmul (concat (@bv x1i1 x1in1) x1) (concat (@bv y1i1 y1in1) y1))) (@bv 0 w1)) +) +(declare-rule bv-udiv-pow2-not-one ((@n0 Int) (x1 (BitVec @n0)) (v1 Int) (n1 Int) (power1 Int) (nm1 Int)) + :premises ((= (int.ispow2 v1) true) (= (> v1 1) true) (= power1 (int.log2 v1)) (= nm1 (- n1 1))) + :args (x1 v1 n1 power1 nm1) + :conclusion (= (bvudiv x1 (@bv v1 n1)) (concat (@bv 0 power1) (extract nm1 power1 x1))) +) +(declare-rule bv-udiv-zero ((@n0 Int) (x1 (BitVec @n0)) (n1 Int)) + :args (x1 n1) + :conclusion (= (bvudiv x1 (@bv 0 n1)) (bvnot (@bv 0 n1))) +) +(declare-rule bv-udiv-one ((@n0 Int) (x1 (BitVec @n0)) (n1 Int)) + :args (x1 n1) + :conclusion (= (bvudiv x1 (@bv 1 n1)) x1) +) +(declare-rule bv-urem-pow2-not-one ((@n0 Int) (x1 (BitVec @n0)) (v1 Int) (n1 Int) (nmp1 Int) (pm1 Int)) + :premises ((= (int.ispow2 v1) true) (= (> v1 1) true) (= nmp1 (- n1 (int.log2 v1))) (= pm1 (- (int.log2 v1) 1))) + :args (x1 v1 n1 nmp1 pm1) + :conclusion (= (bvurem x1 (@bv v1 n1)) (concat (@bv 0 nmp1) (extract pm1 0 x1))) +) +(declare-rule bv-urem-one ((@n0 Int) (x1 (BitVec @n0)) (n1 Int)) + :args (x1 n1) + :conclusion (= (bvurem x1 (@bv 1 n1)) (@bv 0 n1)) +) +(declare-rule bv-urem-self ((@n0 Int) (x1 (BitVec @n0)) (w1 Int)) + :premises ((= w1 (@bvsize x1))) + :args (x1 w1) + :conclusion (= (bvurem x1 x1) (@bv 0 w1)) +) +(declare-rule bv-shl-zero ((@n0 Int) (a1 (BitVec @n0)) (n1 Int)) + :args (a1 n1) + :conclusion (= (bvshl (@bv 0 n1) a1) (@bv 0 n1)) +) +(declare-rule bv-lshr-zero ((@n0 Int) (a1 (BitVec @n0)) (n1 Int)) + :args (a1 n1) + :conclusion (= (bvlshr (@bv 0 n1) a1) (@bv 0 n1)) +) +(declare-rule bv-ashr-zero ((@n0 Int) (a1 (BitVec @n0)) (n1 Int)) + :args (a1 n1) + :conclusion (= (bvashr (@bv 0 n1) a1) (@bv 0 n1)) +) +(declare-rule bv-ult-one ((@n0 Int) (x1 (BitVec @n0)) (n1 Int)) + :args (x1 n1) + :conclusion (= (bvult x1 (@bv 1 n1)) (= x1 (@bv 0 n1))) +) +(declare-rule bv-merge-sign-extend-1 ((@n0 Int) (x1 (BitVec @n0)) (i1 Int) (j1 Int) (k1 Int)) + :premises ((= k1 (+ i1 j1))) + :args (x1 i1 j1 k1) + :conclusion (= (sign_extend i1 (sign_extend j1 x1)) (sign_extend k1 x1)) +) +(declare-rule bv-merge-sign-extend-2 ((@n0 Int) (x1 (BitVec @n0)) (i1 Int) (j1 Int) (k1 Int)) + :premises ((= (> j1 0) true) (= k1 (+ i1 j1))) + :args (x1 i1 j1 k1) + :conclusion (= (sign_extend i1 (zero_extend j1 x1)) (zero_extend k1 x1)) +) + +(declare-rule bv-sign-extend-ult-const-2 ((@n0 Int) (x1 (BitVec @n0)) (m1 Int) (c1 Int) (nm1 Int) (nm2 Int)) + :premises ((= (bvult (bvshl (@bv 1 nm1) (@bv (- (@bvsize x1) 1) nm1)) (@bv c1 nm1)) true) (= (bvule (@bv c1 nm1) (bvshl (bvnot (@bv 0 nm1)) (@bv (- (@bvsize x1) 1) nm1))) true) (= nm2 (- (@bvsize x1) 1))) + :args (x1 m1 c1 nm1 nm2) + :conclusion (= (bvult (sign_extend m1 x1) (@bv c1 nm1)) (= (extract nm2 nm2 x1) (@bv 0 1))) +) +(declare-rule bv-sign-extend-ult-const-4 ((@n0 Int) (x1 (BitVec @n0)) (m1 Int) (c1 Int) (nm1 Int) (nm2 Int)) + :premises ((= (bvule (bvnot (bvshl (bvnot (@bv 0 nm1)) (@bv (- (@bvsize x1) 1) nm1))) (@bv c1 nm1)) true) (= (bvule (@bv c1 nm1) (bvnot (bvshl (@bv 1 nm1) (@bv (- (@bvsize x1) 1) nm1)))) true) (= nm2 (- (@bvsize x1) 1))) + :args (x1 m1 c1 nm1 nm2) + :conclusion (= (bvult (@bv c1 nm1) (sign_extend m1 x1)) (= (extract nm2 nm2 x1) (@bv 1 1))) +) +(declare-rule uf-bv2nat-int2bv ((@n0 Int) (w1 Int) (t1 (BitVec @n0))) + :premises ((= (@bvsize t1) w1)) + :args (w1 t1) + :conclusion (= (int_to_bv w1 (ubv_to_int t1)) t1) +) +(declare-rule uf-bv2nat-int2bv-extend ((@n0 Int) (w1 Int) (t1 (BitVec @n0)) (n1 Int)) + :premises ((= (> w1 (@bvsize t1)) true) (= n1 (- w1 (@bvsize t1)))) + :args (w1 t1 n1) + :conclusion (= (int_to_bv w1 (ubv_to_int t1)) (concat (@bv 0 n1) t1)) +) +(declare-rule uf-bv2nat-int2bv-extract ((@n0 Int) (w1 Int) (t1 (BitVec @n0)) (wm1 Int)) + :premises ((= (< w1 (@bvsize t1)) true) (= wm1 (- w1 1))) + :args (w1 t1 wm1) + :conclusion (= (int_to_bv w1 (ubv_to_int t1)) (extract wm1 0 t1)) +) +(declare-rule uf-bv2nat-geq-elim ((@n0 Int) (x1 (BitVec @n0)) (n1 Int) (w1 Int)) + :premises ((= w1 (@bvsize x1))) + :args (x1 n1 w1) + :conclusion (= (>= (ubv_to_int x1) n1) (ite (>= n1 w1) false (ite (< n1 0) true (bvuge x1 (int_to_bv w1 n1))))) +) +(declare-rule uf-int2bv-bvult-equiv ((@n0 Int) (@n1 Int) (t1 (BitVec @n0)) (s1 (BitVec @n1))) + :args (t1 s1) + :conclusion (= (bvult t1 s1) (< (ubv_to_int t1) (ubv_to_int s1))) +) +(declare-rule uf-int2bv-bvule-equiv ((@n0 Int) (@n1 Int) (t1 (BitVec @n0)) (s1 (BitVec @n1))) + :args (t1 s1) + :conclusion (= (bvule t1 s1) (<= (ubv_to_int t1) (ubv_to_int s1))) +) +(declare-rule bv-concat-extract-merge ((@n0 Int) (@n1 Int) (@n2 Int) (xs1 (BitVec @n0) :list) (s1 (BitVec @n1)) (ys1 (BitVec @n2) :list) (i1 Int) (j1 Int) (j2 Int) (k1 Int)) + :premises ((= j2 (+ j1 1))) + :args (xs1 s1 ys1 i1 j1 j2 k1) + :conclusion (= (concat xs1 (extract k1 j2 s1) (extract j1 i1 s1) ys1) (concat xs1 (extract k1 i1 s1) ys1)) +) + +(declare-rule bv-extract-concat-2 ((@n0 Int) (@n1 Int) (@n2 Int) (x1 (BitVec @n0)) (xs1 (BitVec @n1) :list) (y1 (BitVec @n2)) (i1 Int) (j1 Int) (u1 Int) (u2 Int)) + :premises ((= (< i1 (@bvsize x1)) true) (= (>= j1 (@bvsize x1)) true) (= u1 (- j1 (@bvsize x1))) (= u2 (- (@bvsize x1) 1))) + :args (x1 xs1 y1 i1 j1 u1 u2) + :conclusion (= (extract j1 i1 (concat xs1 y1 x1)) (concat (extract u1 0 (concat xs1 y1)) (extract u2 i1 x1))) +) +(declare-rule bv-extract-concat-3 ((@n0 Int) (@n1 Int) (@n2 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (xs1 (BitVec @n2) :list) (i1 Int) (j1 Int) (u1 Int) (l1 Int)) + :premises ((= (>= i1 (@bvsize x1)) true) (= u1 (- j1 (@bvsize x1))) (= l1 (- i1 (@bvsize x1)))) + :args (x1 y1 xs1 i1 j1 u1 l1) + :conclusion (= (extract j1 i1 (concat xs1 y1 x1)) (extract u1 l1 (concat xs1 y1))) +) +(declare-rule bv-extract-concat-4 ((@n0 Int) (@n1 Int) (@n2 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (xs1 (BitVec @n2) :list) (i1 Int) (j1 Int)) + :premises ((= (< j1 (- (@bvsize (concat x1 xs1 y1)) (@bvsize x1))) true)) + :args (x1 y1 xs1 i1 j1) + :conclusion (= (extract j1 i1 (concat x1 xs1 y1)) (extract j1 i1 (concat xs1 y1))) +) + +(declare-rule bv-not-xor ((@n0 Int) (@n1 Int) (@n2 Int) (x1 (BitVec @n0)) (x2 (BitVec @n1)) (xs1 (BitVec @n2) :list)) + :args (x1 x2 xs1) + :conclusion (= (bvnot (bvxor x1 x2 xs1)) (bvxor (bvnot x1) x2 xs1)) +) +(declare-rule bv-and-simplify-1 ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (xs1 (BitVec @n0) :list) (ys1 (BitVec @n1) :list) (zs1 (BitVec @n2) :list) (x1 (BitVec @n3)) (w1 Int)) + :premises ((= w1 (@bvsize x1))) + :args (xs1 ys1 zs1 x1 w1) + :conclusion (= (bvand xs1 (bvnot x1) ys1 x1 zs1) (@bv 0 w1)) +) +(declare-rule bv-and-simplify-2 ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (xs1 (BitVec @n0) :list) (ys1 (BitVec @n1) :list) (zs1 (BitVec @n2) :list) (x1 (BitVec @n3)) (w1 Int)) + :premises ((= w1 (@bvsize x1))) + :args (xs1 ys1 zs1 x1 w1) + :conclusion (= (bvand xs1 x1 ys1 (bvnot x1) zs1) (@bv 0 w1)) +) +(declare-rule bv-or-simplify-1 ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (xs1 (BitVec @n0) :list) (ys1 (BitVec @n1) :list) (zs1 (BitVec @n2) :list) (x1 (BitVec @n3)) (w1 Int)) + :premises ((= w1 (@bvsize x1))) + :args (xs1 ys1 zs1 x1 w1) + :conclusion (= (bvor xs1 (bvnot x1) ys1 x1 zs1) (bvnot (@bv 0 w1))) +) +(declare-rule bv-or-simplify-2 ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (xs1 (BitVec @n0) :list) (ys1 (BitVec @n1) :list) (zs1 (BitVec @n2) :list) (x1 (BitVec @n3)) (w1 Int)) + :premises ((= w1 (@bvsize x1))) + :args (xs1 ys1 zs1 x1 w1) + :conclusion (= (bvor xs1 x1 ys1 (bvnot x1) zs1) (bvnot (@bv 0 w1))) +) +(declare-rule bv-xor-simplify-1 ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (xs1 (BitVec @n0) :list) (ys1 (BitVec @n1) :list) (zs1 (BitVec @n2) :list) (x1 (BitVec @n3))) + :args (xs1 ys1 zs1 x1) + :conclusion (= (bvxor xs1 x1 ys1 x1 zs1) (bvxor xs1 ys1 zs1)) +) +(declare-rule bv-xor-simplify-2 ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (xs1 (BitVec @n0) :list) (ys1 (BitVec @n1) :list) (zs1 (BitVec @n2) :list) (x1 (BitVec @n3))) + :args (xs1 ys1 zs1 x1) + :conclusion (= (bvxor xs1 x1 ys1 (bvnot x1) zs1) (bvnot (bvxor xs1 ys1 zs1))) +) +(declare-rule bv-xor-simplify-3 ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (xs1 (BitVec @n0) :list) (ys1 (BitVec @n1) :list) (zs1 (BitVec @n2) :list) (x1 (BitVec @n3))) + :args (xs1 ys1 zs1 x1) + :conclusion (= (bvxor xs1 (bvnot x1) ys1 x1 zs1) (bvnot (bvxor xs1 ys1 zs1))) +) + + +(declare-rule bv-concat-merge-const ((@n0 Int) (@n1 Int) (xs1 (BitVec @n0) :list) (n1 Int) (w1 Int) (n2 Int) (w2 Int) (ww1 Int) (zs1 (BitVec @n1) :list)) + :premises ((= ww1 (+ w1 w2))) + :args (xs1 n1 w1 n2 w2 ww1 zs1) + :conclusion (= (concat xs1 (@bv n1 w1) (@bv n2 w2) zs1) (concat xs1 (@bv (+ (* n1 (int.pow2 w2) n2) ww1) zs1))) +) + +(declare-rule bv-xor-ones ((@n0 Int) (@n1 Int) (xs1 (BitVec @n0) :list) (zs1 (BitVec @n1) :list) (n1 Int) (w1 Int)) + :premises ((= n1 (- (int.pow2 w1) 1))) + :args (xs1 zs1 n1 w1) + :conclusion (= (bvxor xs1 (@bv n1 w1) zs1) (bvnot (bvxor xs1 zs1))) +) +(declare-rule bv-mult-pow2-1 ((@n0 Int) (@n1 Int) (@n2 Int) (xs1 (BitVec @n0) :list) (ys1 (BitVec @n1) :list) (z1 (BitVec @n2)) (size1 Int) (n1 Int) (exponent1 Int) (u1 Int)) + :premises ((= (int.ispow2 n1) true) (= exponent1 (int.log2 n1)) (= u1 (- (- size1 (int.log2 n1)) 1))) + :args (xs1 ys1 z1 size1 n1 exponent1 u1) + :conclusion (= (bvmul xs1 z1 (@bv n1 size1) ys1) (concat (extract u1 0 (bvmul xs1 z1 ys1)) (@bv 0 exponent1))) +) +(declare-rule bv-mult-pow2-2 ((@n0 Int) (@n1 Int) (@n2 Int) (xs1 (BitVec @n0) :list) (ys1 (BitVec @n1) :list) (z1 (BitVec @n2)) (size1 Int) (n1 Int) (exponent1 Int) (u1 Int)) + :premises ((= (int.ispow2 (- (int.pow2 size1) n1)) true) (= exponent1 (int.log2 (- (int.pow2 size1) n1))) (= u1 (- (- size1 (int.log2 (- (int.pow2 size1) n1))) 1))) + :args (xs1 ys1 z1 size1 n1 exponent1 u1) + :conclusion (= (bvmul xs1 z1 (@bv n1 size1) ys1) (concat (extract u1 0 (bvneg (bvmul xs1 z1 ys1))) (@bv 0 exponent1))) +) +(declare-rule uf-int2bv-bv2nat ((w1 Int) (t1 Int)) + :args (w1 t1) + :conclusion (= (ubv_to_int (int_to_bv w1 t1)) (mod_total t1 (int.pow2 w1))) +) + +;;;;;;;;;;;;;;;;; +;; Arrays +;;;;;;;;;;;;;;;;; + +(declare-rule array-read-over-write ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (t1 (Array @T0 @T1)) (i1 @T2) (e1 @T3)) + :args (t1 i1 e1) + :conclusion (= (select (store t1 i1 e1) i1) e1) +) +(declare-rule array-read-over-write2 ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (@T4 Type) (t1 (Array @T0 @T1)) (i1 @T2) (j1 @T3) (e1 @T4)) + :premises ((= (= i1 j1) false)) + :args (t1 i1 j1 e1) + :conclusion (= (select (store t1 i1 e1) j1) (select t1 j1)) +) +(declare-rule array-store-overwrite ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (@T4 Type) (t1 (Array @T0 @T1)) (i1 @T2) (e1 @T3) (f1 @T4)) + :args (t1 i1 e1 f1) + :conclusion (= (store (store t1 i1 e1) i1 f1) (store t1 i1 f1)) +) +(declare-rule array-store-self ((@T0 Type) (@T1 Type) (@T2 Type) (t1 (Array @T0 @T1)) (i1 @T2)) + :args (t1 i1) + :conclusion (= (store t1 i1 (select t1 i1)) t1) +) +(declare-rule array-read-over-write-split ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (@T4 Type) (t1 (Array @T0 @T1)) (i1 @T2) (e1 @T3) (j1 @T4)) + :args (t1 i1 e1 j1) + :conclusion (= (select (store t1 j1 e1) i1) (ite (= i1 j1) e1 (select t1 i1))) +) +(declare-rule array-store-swap ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (@T4 Type) (@T5 Type) (t1 (Array @T0 @T1)) (i1 @T2) (j1 @T3) (e1 @T4) (f1 @T5)) + :premises ((= (= i1 j1) false)) + :args (t1 i1 j1 e1 f1) + :conclusion (= (store (store t1 i1 e1) j1 f1) (store (store t1 j1 f1) i1 e1)) +) + +;;;;;;;;;;;;;;;;; +;; Sets +;;;;;;;;;;;;;;;;; + + +(declare-rule sets-eq-singleton-emp ((@T0 Type) (@T1 Type) (x1 (Set @T0)) (y1 @T1)) + :premises ((= x1 (as set.empty (Set @T0)))) + :args (x1 y1 (Set @T0)) + :conclusion (= (= x1 (set.singleton y1)) false) +) + +(declare-rule sets-member-emp ((@T0 Type) (@T1 Type) (x1 @T0) (y1 (Set @T1))) + :premises ((= y1 (as 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))) + :args (x1 y1) + :conclusion (= (set.subset x1 y1) (= (set.union x1 y1) y1)) +) +(declare-rule sets-union-comm ((@T0 Type) (@T1 Type) (x1 (Set @T0)) (y1 (Set @T1))) + :args (x1 y1) + :conclusion (= (set.union x1 y1) (set.union y1 x1)) +) +(declare-rule sets-inter-comm ((@T0 Type) (@T1 Type) (x1 (Set @T0)) (y1 (Set @T1))) + :args (x1 y1) + :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 ((= x1 (as 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 ((= y1 (as 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 ((= x1 (as 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 ((= y1 (as 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 ((= x1 (as 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 ((= y1 (as 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))) + :args (x1 y1 z1) + :conclusion (= (set.member x1 (set.inter y1 z1)) (and (set.member x1 y1) (set.member x1 z1))) +) +(declare-rule sets-minus-member ((@T0 Type) (@T1 Type) (@T2 Type) (x1 @T0) (y1 (Set @T1)) (z1 (Set @T2))) + :args (x1 y1 z1) + :conclusion (= (set.member x1 (set.minus y1 z1)) (and (set.member x1 y1) (not (set.member x1 z1)))) +) +(declare-rule sets-union-member ((@T0 Type) (@T1 Type) (@T2 Type) (x1 @T0) (y1 (Set @T1)) (z1 (Set @T2))) + :args (x1 y1 z1) + :conclusion (= (set.member x1 (set.union y1 z1)) (or (set.member x1 y1) (set.member x1 z1))) +) + +(declare-rule sets-minus-self ((@T0 Type) (x1 (Set @T0))) + :args (x1 (Set @T0)) + :conclusion (= (set.minus x1 x1) (as 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 (as set.empty (Set @T0)))) +) +(declare-rule sets-is-singleton-elim ((@T0 Type) (x1 (Set @T0))) + :args (x1) + :conclusion (= (set.is_singleton x1) (= x1 (set.singleton (set.choose x1)))) +) +(declare-rule sets-member-singleton ((@T0 Type) (@T1 Type) (x1 @T0) (y1 @T1)) + :args (x1 y1) + :conclusion (= (set.member x1 (set.singleton y1)) (= x1 y1)) +) +(declare-rule sets-choose-singleton ((@T0 Type) (x1 @T0)) + :args (x1) + :conclusion (= (set.choose (set.singleton x1)) x1) +) + +;;;;;;;;;;;;;;;;; +;; Sequences +;;;;;;;;;;;;;;;;; + +(declare-rule seq-len-unit ((@T0 Type) (x1 @T0)) + :args (x1) + :conclusion (= (seq.len (seq.unit x1)) 1) +) +(declare-rule seq-nth-unit ((@T0 Type) (x1 @T0)) + :args (x1) + :conclusion (= (seq.nth (seq.unit x1) 0) x1) +) +(declare-rule seq-rev-unit ((@T0 Type) (x1 @T0)) + :args (x1) + :conclusion (= (seq.rev (seq.unit x1)) (seq.unit x1)) +) +(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) + :conclusion (= (= (seq.++ x1 x2 x3) y1) false) +) +(declare-rule str-eq-ctn-full-false1 ((@T0 Type) (@T1 Type) (x1 (Seq @T0)) (y1 (Seq @T1))) + :premises ((= (seq.contains y1 x1) false)) + :args (x1 y1) + :conclusion (= (= x1 y1) false) +) +(declare-rule str-eq-ctn-full-false2 ((@T0 Type) (@T1 Type) (x1 (Seq @T0)) (y1 (Seq @T1))) + :premises ((= (seq.contains x1 y1) false)) + :args (x1 y1) + :conclusion (= (= x1 y1) false) +) + +(declare-rule str-substr-empty-str ((@T0 Type) (x1 (Seq @T0)) (n1 Int) (m1 Int)) + :premises ((= (seq.len x1) 0)) + :args (x1 n1 m1) + :conclusion (= (seq.extract x1 n1 m1) x1) +) +(declare-rule str-substr-empty-range ((@T0 Type) (x1 (Seq @T0)) (n1 Int) (m1 Int)) + :premises ((= (>= 0 m1) true)) + :args (x1 n1 m1 (Seq @T0)) + :conclusion (= (seq.extract x1 n1 m1) ($seq_empty (Seq @T0))) +) +(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 ((@T0 Type) (x1 (Seq @T0)) (n1 Int) (m1 Int)) + :premises ((= (< n1 0) true)) + :args (x1 n1 m1 (Seq @T0)) + :conclusion (= (seq.extract x1 n1 m1) ($seq_empty (Seq @T0))) +) +(declare-rule str-substr-substr-start-geq-len ((@T0 Type) (x1 (Seq @T0)) (n1 Int) (m1 Int) (n2 Int) (m2 Int)) + :premises ((= (>= n2 m1) true)) + :args (x1 n1 m1 n2 m2 (Seq @T0)) + :conclusion (= (seq.extract (seq.extract x1 n1 m1) n2 m2) ($seq_empty (Seq @T0))) +) +(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) (= (seq.len r1) 0)) + :args (s1 r1 n1 m1) + :conclusion (= (= (seq.extract s1 n1 m1) r1) (= s1 r1)) +) +(declare-rule str-substr-z-eq-empty-leq ((@T0 Type) (@T1 Type) (s1 (Seq @T0)) (r1 (Seq @T1)) (m1 Int)) + :premises ((= (= (seq.len s1) 0) false) (= (seq.len r1) 0)) + :args (s1 r1 m1) + :conclusion (= (= (seq.extract s1 0 m1) r1) (<= m1 0)) +) +(declare-rule str-substr-eq-empty-leq-len ((@T0 Type) (@T1 Type) (s1 (Seq @T0)) (emp1 (Seq @T1)) (n1 Int) (m1 Int)) + :premises ((= (>= n1 0) true) (= (> m1 0) true) (= (seq.len emp1) 0)) + :args (s1 emp1 n1 m1) + :conclusion (= (= (seq.extract s1 n1 m1) emp1) (<= (seq.len s1) n1)) +) +(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))) + :args (t1 s1 r1) + :conclusion (= (seq.len (seq.replace t1 s1 r1)) (seq.len t1)) +) +(declare-rule str-len-replace-all-inv ((@T0 Type) (@T1 Type) (@T2 Type) (t1 (Seq @T0)) (s1 (Seq @T1)) (r1 (Seq @T2))) + :premises ((= (seq.len s1) (seq.len r1))) + :args (t1 s1 r1) + :conclusion (= (seq.len (seq.replace_all t1 s1 r1)) (seq.len t1)) +) +(declare-rule str-len-update-inv ((@T0 Type) (@T1 Type) (t1 (Seq @T0)) (n1 Int) (r1 (Seq @T1))) + :args (t1 n1 r1) + :conclusion (= (seq.len (seq.update t1 n1 r1)) (seq.len t1)) +) +(declare-rule str-update-in-first-concat ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (@T4 Type) (t1 (Seq @T0)) (ts1 (Seq @T1) :list) (s1 (Seq @T2)) (n1 Int) (tpre1 (Seq @T3)) (tpost1 (Seq @T4))) + :premises ((= (>= n1 0) true) (= (< (+ n1 (seq.len s1)) (seq.len t1)) true) (= tpre1 (seq.extract t1 0 n1)) (= tpost1 (seq.extract t1 (+ n1 (seq.len s1)) (seq.len t1)))) + :args (t1 ts1 s1 n1 tpre1 tpost1) + :conclusion (= (seq.update (seq.++ t1 ts1) n1 s1) (seq.++ tpre1 s1 tpost1 ts1)) +) +(declare-rule str-len-substr-in-range ((@T0 Type) (s1 (Seq @T0)) (n1 Int) (m1 Int)) + :premises ((= (>= n1 0) true) (= (>= m1 0) true) (= (>= (seq.len s1) (+ n1 m1)) true)) + :args (s1 n1 m1) + :conclusion (= (seq.len (seq.extract s1 n1 m1)) m1) +) +(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 (= (= (seq.++ s1 s2) (seq.++ t1 t2)) false) +) +(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 (= (= (seq.++ s2 s1) (seq.++ t2 t1)) false) +) +(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 (seq.++ t1 t2)) false) +) +(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 (seq.++ t2 t1)) false) +) +(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 (= (= (seq.++ s1 s2 s3) (seq.++ s1 t1 t2)) (= (seq.++ s2 s3) (seq.++ t1 t2))) +) +(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 (= (= (seq.++ s2 s3 s1) (seq.++ t1 t2 s1)) (= (seq.++ s2 s3) (seq.++ 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)) (seq.++ 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)) (seq.++ t1 t2))) +) +(declare-rule str-prefixof-elim ((@T0 Type) (@T1 Type) (s1 (Seq @T0)) (t1 (Seq @T1))) + :args (s1 t1) + :conclusion (= (seq.prefixof s1 t1) (= s1 (seq.extract t1 0 (seq.len s1)))) +) + +(declare-rule str-prefixof-eq ((@T0 Type) (@T1 Type) (s1 (Seq @T0)) (t1 (Seq @T1))) + :premises ((= (>= (seq.len s1) (seq.len t1)) true)) + :args (s1 t1) + :conclusion (= (seq.prefixof s1 t1) (= s1 t1)) +) +(declare-rule str-suffixof-eq ((@T0 Type) (@T1 Type) (s1 (Seq @T0)) (t1 (Seq @T1))) + :premises ((= (>= (seq.len s1) (seq.len t1)) true)) + :args (s1 t1) + :conclusion (= (seq.suffixof s1 t1) (= s1 t1)) +) +(declare-rule str-prefixof-one ((@T0 Type) (@T1 Type) (s1 (Seq @T0)) (t1 (Seq @T1))) + :premises ((= (seq.len t1) 1)) + :args (s1 t1) + :conclusion (= (seq.prefixof s1 t1) (seq.contains t1 s1)) +) +(declare-rule str-suffixof-one ((@T0 Type) (@T1 Type) (s1 (Seq @T0)) (t1 (Seq @T1))) + :premises ((= (seq.len t1) 1)) + :args (s1 t1) + :conclusion (= (seq.suffixof s1 t1) (seq.contains t1 s1)) +) +(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 (= (seq.extract (seq.extract s1 n1 m1) n2 m2) (seq.extract s1 (+ n1 n2) (- m1 n2))) +) +(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 (= (seq.extract (seq.extract s1 n1 m1) n2 m2) (seq.extract s1 (+ n1 n2) m2)) +) +(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 (= (seq.extract (seq.extract s1 n1 m1) n2 m2) (seq.extract s1 (+ n1 n2) m2)) +) +(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 (= (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)) + :args (s1 s2 n1 m1) + :conclusion (= (seq.extract (seq.++ s1 s2) n1 m1) (seq.extract s1 n1 m1)) +) +(declare-rule str-substr-concat2 ((@T0 Type) (@T1 Type) (@T2 Type) (s1 (Seq @T0)) (s2 (Seq @T1)) (s3 (Seq @T2) :list) (n1 Int) (m1 Int)) + :premises ((= (>= n1 (seq.len s1)) true)) + :args (s1 s2 s3 n1 m1) + :conclusion (= (seq.extract (seq.++ s1 s2 s3) n1 m1) (seq.extract (seq.++ s2 s3) (- n1 (seq.len s1)) m1)) +) +(declare-rule str-substr-replace ((@T0 Type) (@T1 Type) (@T2 Type) (s1 (Seq @T0)) (t1 (Seq @T1)) (r1 (Seq @T2)) (n1 Int)) + :premises ((= (seq.len t1) (seq.len r1)) (= (seq.len t1) 1)) + :args (s1 t1 r1 n1) + :conclusion (= (seq.extract (seq.replace s1 t1 r1) 0 n1) (seq.replace (seq.extract s1 0 n1) t1 r1)) +) +(declare-rule str-substr-full ((@T0 Type) (s1 (Seq @T0)) (n1 Int)) + :premises ((= (>= n1 (seq.len s1)) true)) + :args (s1 n1) + :conclusion (= (seq.extract s1 0 n1) s1) +) +(declare-rule str-substr-full-eq ((@T0 Type) (s1 (Seq @T0)) (n1 Int)) + :premises ((= (seq.len s1) n1)) + :args (s1 n1) + :conclusion (= (seq.extract s1 0 n1) s1) +) +(declare-rule str-contains-refl ((@T0 Type) (x1 (Seq @T0))) + :args (x1) + :conclusion (= (seq.contains x1 x1) true) +) +(declare-rule str-contains-concat-find ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (xs1 (Seq @T0) :list) (z1 (Seq @T1)) (y1 (Seq @T2)) (zs1 (Seq @T3) :list)) + :premises ((= (seq.contains z1 y1) true)) + :args (xs1 z1 y1 zs1) + :conclusion (= (seq.contains (seq.++ xs1 z1 zs1) y1) true) +) +(declare-rule str-contains-concat-find-contra ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (xs1 (Seq @T0) :list) (z1 (Seq @T1)) (y1 (Seq @T2)) (zs1 (Seq @T3) :list)) + :premises ((= (seq.contains y1 z1) false)) + :args (xs1 z1 y1 zs1) + :conclusion (= (seq.contains y1 (seq.++ xs1 z1 zs1)) false) +) +(declare-rule str-contains-split-char ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (x1 (Seq @T0)) (y1 (Seq @T1)) (z1 (Seq @T2) :list) (w1 (Seq @T3))) + :premises ((= (seq.len w1) 1)) + :args (x1 y1 z1 w1) + :conclusion (= (seq.contains (seq.++ x1 y1 z1) w1) (or (seq.contains x1 w1) (seq.contains (seq.++ y1 z1) w1))) +) +(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 (= (seq.contains x1 y1) (= x1 y1)) +) +(declare-rule str-contains-emp ((@T0 Type) (@T1 Type) (x1 (Seq @T0)) (y1 (Seq @T1))) + :premises ((= (seq.len y1) 0)) + :args (x1 y1) + :conclusion (= (seq.contains x1 y1) true) +) +(declare-rule str-contains-char ((@T0 Type) (@T1 Type) (x1 (Seq @T0)) (y1 (Seq @T1))) + :premises ((= (seq.len x1) 1)) + :args (x1 y1 (Seq @T0)) + :conclusion (= (seq.contains x1 y1) (or (= ($seq_empty (Seq @T0)) y1) (= x1 y1))) +) +(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)) +) +(declare-rule str-replace-self ((@T0 Type) (@T1 Type) (t1 (Seq @T0)) (s1 (Seq @T1))) + :args (t1 s1) + :conclusion (= (seq.replace t1 t1 s1) s1) +) +(declare-rule str-replace-id ((@T0 Type) (@T1 Type) (t1 (Seq @T0)) (s1 (Seq @T1))) + :args (t1 s1) + :conclusion (= (seq.replace t1 s1 s1) t1) +) +(declare-rule str-replace-prefix ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (t1 (Seq @T0)) (t2 (Seq @T1)) (r1 (Seq @T2) :list) (s1 (Seq @T3))) + :args (t1 t2 r1 s1) + :conclusion (= (seq.replace (seq.++ t1 t2 r1) t1 s1) (seq.++ s1 t2 r1)) +) +(declare-rule str-replace-no-contains ((@T0 Type) (@T1 Type) (@T2 Type) (t1 (Seq @T0)) (s1 (Seq @T1)) (r1 (Seq @T2))) + :premises ((= (seq.contains t1 s1) false)) + :args (t1 s1 r1) + :conclusion (= (seq.replace t1 s1 r1) t1) +) +(declare-rule str-replace-find-base ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (@T4 Type) (t1 (Seq @T0)) (s1 (Seq @T1)) (r1 (Seq @T2)) (tpre1 (Seq @T3)) (tpost1 (Seq @T4))) + :premises ((= (>= (seq.indexof t1 s1 0) 0) true) (= tpre1 (seq.extract t1 0 (seq.indexof t1 s1 0))) (= tpost1 (seq.extract t1 (+ (seq.indexof t1 s1 0) (seq.len s1)) (seq.len t1)))) + :args (t1 s1 r1 tpre1 tpost1) + :conclusion (= (seq.replace t1 s1 r1) (seq.++ tpre1 r1 tpost1)) +) +(declare-rule str-replace-find-first-concat ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (@T4 Type) (@T5 Type) (t1 (Seq @T0)) (ts1 (Seq @T1) :list) (s1 (Seq @T2)) (r1 (Seq @T3)) (tpre1 (Seq @T4)) (tpost1 (Seq @T5))) + :premises ((= (>= (seq.indexof t1 s1 0) 0) true) (= tpre1 (seq.extract t1 0 (seq.indexof t1 s1 0))) (= tpost1 (seq.extract t1 (+ (seq.indexof t1 s1 0) (seq.len s1)) (seq.len t1)))) + :args (t1 ts1 s1 r1 tpre1 tpost1) + :conclusion (= (seq.replace (seq.++ t1 ts1) s1 r1) (seq.++ tpre1 r1 tpost1 ts1)) +) +(declare-rule str-replace-empty ((@T0 Type) (@T1 Type) (@T2 Type) (t1 (Seq @T0)) (s1 (Seq @T1)) (r1 (Seq @T2))) + :premises ((= (seq.len r1) 0)) + :args (t1 s1 r1) + :conclusion (= (seq.replace t1 r1 s1) (seq.++ s1 t1)) +) +(declare-rule str-replace-one-pre ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (@T4 Type) (t1 (Seq @T0)) (s1 (Seq @T1)) (r1 (Seq @T2)) (ts1 (Seq @T3) :list) (ss1 (Seq @T4) :list)) + :premises ((= (seq.len s1) 1)) + :args (t1 s1 r1 ts1 ss1) + :conclusion (= (seq.replace (seq.++ ts1 t1 ss1 t1) s1 r1) (seq.++ (seq.replace (seq.++ ts1 t1 ss1) s1 r1) t1)) +) +(declare-rule str-replace-find-pre ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (t1 (Seq @T0)) (r1 (Seq @T1)) (ts1 (Seq @T2) :list) (ss1 (Seq @T3) :list)) + :args (t1 r1 ts1 ss1) + :conclusion (= (seq.replace (seq.++ ts1 t1 ss1) t1 r1) (seq.++ (seq.replace (seq.++ ts1 t1) t1 r1) ss1)) +) +(declare-rule str-replace-all-no-contains ((@T0 Type) (@T1 Type) (@T2 Type) (t1 (Seq @T0)) (s1 (Seq @T1)) (r1 (Seq @T2))) + :premises ((= (seq.contains t1 s1) false)) + :args (t1 s1 r1) + :conclusion (= (seq.replace_all t1 s1 r1) t1) +) +(declare-rule str-replace-re-none ((@T0 Type) (@T1 Type) (t1 (Seq @T0)) (r1 (Seq @T1))) + :args (t1 r1) + :conclusion (= (str.replace_re t1 re.none r1) t1) +) +(declare-rule str-replace-re-all-none ((@T0 Type) (@T1 Type) (t1 (Seq @T0)) (r1 (Seq @T1))) + :args (t1 r1) + :conclusion (= (str.replace_re_all t1 re.none r1) t1) +) +(declare-rule str-len-concat-rec ((@T0 Type) (@T1 Type) (@T2 Type) (s1 (Seq @T0)) (s2 (Seq @T1)) (s3 (Seq @T2) :list)) + :args (s1 s2 s3) + :conclusion (= (seq.len (seq.++ s1 s2 s3)) (+ (seq.len s1) (seq.len (seq.++ s2 s3)))) +) +(declare-rule str-len-eq-zero-concat-rec ((@T0 Type) (@T1 Type) (@T2 Type) (s1 (Seq @T0)) (s2 (Seq @T1)) (s3 (Seq @T2) :list)) + :args (s1 s2 s3 (Seq @T0)) + :conclusion (= (= (seq.len (seq.++ s1 s2 s3)) 0) (and (= s1 ($seq_empty (Seq @T0))) (= (seq.len (seq.++ s2 s3)) 0))) +) +(declare-rule str-len-eq-zero-base ((@T0 Type) (s1 (Seq @T0))) + :args (s1 (Seq @T0)) + :conclusion (= (= (seq.len s1) 0) (= s1 ($seq_empty (Seq @T0)))) +) + +(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 (= (seq.indexof t1 s1 n1) -1) +) +(declare-rule str-indexof-oob ((@T0 Type) (@T1 Type) (t1 (Seq @T0)) (s1 (Seq @T1)) (n1 Int)) + :premises ((= (> n1 (seq.len t1)) true)) + :args (t1 s1 n1) + :conclusion (= (seq.indexof t1 s1 n1) -1) +) +(declare-rule str-indexof-oob2 ((@T0 Type) (@T1 Type) (t1 (Seq @T0)) (s1 (Seq @T1)) (n1 Int)) + :premises ((= (> 0 n1) true)) + :args (t1 s1 n1) + :conclusion (= (seq.indexof t1 s1 n1) -1) +) +(declare-rule str-indexof-contains-pre ((@T0 Type) (@T1 Type) (@T2 Type) (t1 (Seq @T0)) (t2 (Seq @T1) :list) (s1 (Seq @T2)) (n1 Int)) + :premises ((= (seq.contains (seq.extract t1 n1 (seq.len t1)) s1) true)) + :args (t1 t2 s1 n1) + :conclusion (= (seq.indexof (seq.++ t1 t2) s1 n1) (seq.indexof t1 s1 n1)) +) +(declare-rule str-indexof-find-emp ((@T0 Type) (@T1 Type) (t1 (Seq @T0)) (emp1 (Seq @T1)) (n1 Int)) + :premises ((= (seq.len emp1) 0) (= (>= (seq.len t1) n1) true) (= (>= n1 0) true)) + :args (t1 emp1 n1) + :conclusion (= (seq.indexof t1 emp1 n1) n1) +) +(declare-rule str-indexof-eq-irr ((@T0 Type) (@T1 Type) (@T2 Type) (t1 (Seq @T0)) (s1 (Seq @T1)) (r1 (Seq @T2)) (n1 Int)) + :premises ((= (<= n1 (seq.len t1)) true) (= (<= n1 (seq.len r1)) true) (= (seq.extract t1 n1 (seq.len t1)) (seq.extract r1 n1 (seq.len r1)))) + :args (t1 s1 r1 n1) + :conclusion (= (= (seq.indexof t1 s1 n1) (seq.indexof r1 s1 n1)) true) +) +(declare-rule str-substr-ctn-contra ((@T0 Type) (@T1 Type) (t1 (Seq @T0)) (s1 (Seq @T1)) (n1 Int) (m1 Int)) + :premises ((= (seq.contains t1 s1) false)) + :args (t1 s1 n1 m1) + :conclusion (= (seq.contains (seq.extract t1 n1 m1) s1) false) +) +(declare-rule str-substr-ctn ((@T0 Type) (s1 (Seq @T0)) (n1 Int) (m1 Int)) + :args (s1 n1 m1) + :conclusion (= (seq.contains s1 (seq.extract s1 n1 m1)) true) +) +(declare-rule str-replace-dual-ctn ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (s1 (Seq @T0)) (t1 (Seq @T1)) (r1 (Seq @T2)) (u1 (Seq @T3))) + :premises ((= (seq.contains s1 u1) true) (= (seq.contains r1 u1) true)) + :args (s1 t1 r1 u1) + :conclusion (= (seq.contains (seq.replace s1 t1 r1) u1) true) +) +(declare-rule str-replace-dual-ctn-false ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (s1 (Seq @T0)) (t1 (Seq @T1)) (r1 (Seq @T2)) (u1 (Seq @T3))) + :premises ((= (seq.contains s1 t1) false) (= (seq.contains s1 u1) false)) + :args (s1 t1 r1 u1) + :conclusion (= (seq.contains s1 (seq.replace t1 r1 u1)) false) +) +(declare-rule str-replace-self-ctn-simp ((@T0 Type) (@T1 Type) (s1 (Seq @T0)) (t1 (Seq @T1))) + :args (s1 t1) + :conclusion (= (seq.contains s1 (seq.replace t1 s1 t1)) (seq.contains s1 t1)) +) +(declare-rule str-replace-emp-ctn-src ((@T0 Type) (@T1 Type) (@T2 Type) (s1 (Seq @T0)) (t1 (Seq @T1)) (emp1 (Seq @T2))) + :premises ((= (seq.len emp1) 0)) + :args (s1 t1 emp1) + :conclusion (= (seq.contains s1 (seq.replace emp1 s1 t1)) (= emp1 (seq.replace emp1 s1 t1))) +) +(declare-rule str-substr-char-start-eq-len ((@T0 Type) (x1 (Seq @T0)) (n1 Int)) + :premises ((= (>= 1 (seq.len x1)) true)) + :args (x1 n1 (Seq @T0)) + :conclusion (= (seq.extract x1 n1 n1) ($seq_empty (Seq @T0))) +) +(declare-rule str-contains-repl-char ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (x1 (Seq @T0)) (y1 (Seq @T1)) (z1 (Seq @T2)) (w1 (Seq @T3))) + :premises ((= (seq.len w1) 1) (= (seq.contains y1 w1) false)) + :args (x1 y1 z1 w1) + :conclusion (= (seq.contains (seq.replace x1 y1 z1) w1) (or (seq.contains x1 w1) (and (seq.contains x1 y1) (seq.contains z1 w1)))) +) +(declare-rule str-contains-repl-self-tgt-char ((@T0 Type) (@T1 Type) (@T2 Type) (x1 (Seq @T0)) (y1 (Seq @T1)) (w1 (Seq @T2))) + :premises ((= (seq.len w1) 1)) + :args (x1 y1 w1) + :conclusion (= (seq.contains (seq.replace x1 y1 x1) w1) (seq.contains x1 w1)) +) +(declare-rule str-contains-repl-self ((@T0 Type) (@T1 Type) (x1 (Seq @T0)) (y1 (Seq @T1))) + :args (x1 y1) + :conclusion (= (seq.contains (seq.replace x1 y1 x1) y1) (seq.contains x1 y1)) +) +(declare-rule str-contains-repl-tgt ((@T0 Type) (@T1 Type) (@T2 Type) (x1 (Seq @T0)) (y1 (Seq @T1)) (z1 (Seq @T2))) + :args (x1 y1 z1) + :conclusion (= (seq.contains (seq.replace x1 y1 z1) z1) (or (seq.contains x1 y1) (seq.contains x1 z1))) +) +(declare-rule str-repl-repl-len-id ((@T0 Type) (@T1 Type) (x1 (Seq @T0)) (y1 (Seq @T1))) + :premises ((= (>= (seq.len y1) (seq.len x1)) true)) + :args (x1 y1) + :conclusion (= (seq.replace x1 y1 x1) x1) +) +(declare-rule str-repl-repl-src-tgt-no-ctn ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (x1 (Seq @T0)) (y1 (Seq @T1)) (z1 (Seq @T2)) (w1 (Seq @T3))) + :premises ((= (seq.contains z1 w1) false)) + :args (x1 y1 z1 w1) + :conclusion (= (seq.replace x1 w1 (seq.replace z1 x1 y1)) (seq.replace x1 w1 z1)) +) +(declare-rule str-repl-repl-tgt-self ((@T0 Type) (@T1 Type) (x1 (Seq @T0)) (y1 (Seq @T1))) + :args (x1 y1) + :conclusion (= (seq.replace x1 y1 (seq.replace y1 x1 y1)) x1) +) +(declare-rule str-repl-repl-tgt-no-ctn ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (x1 (Seq @T0)) (y1 (Seq @T1)) (z1 (Seq @T2)) (w1 (Seq @T3))) + :premises ((= (seq.contains x1 z1) false)) + :args (x1 y1 z1 w1) + :conclusion (= (seq.replace x1 y1 (seq.replace y1 z1 w1)) x1) +) +(declare-rule str-repl-repl-src-self ((@T0 Type) (@T1 Type) (@T2 Type) (x1 (Seq @T0)) (y1 (Seq @T1)) (z1 (Seq @T2))) + :args (x1 y1 z1) + :conclusion (= (seq.replace x1 (seq.replace y1 x1 y1) z1) (seq.replace x1 y1 z1)) +) +(declare-rule str-repl-repl-src-inv-no-ctn1 ((@T0 Type) (@T1 Type) (@T2 Type) (x1 (Seq @T0)) (y1 (Seq @T1)) (z1 (Seq @T2))) + :premises ((= (seq.contains y1 z1) false)) + :args (x1 y1 z1) + :conclusion (= (seq.replace x1 (seq.replace y1 x1 z1) y1) (seq.replace x1 y1 y1)) +) +(declare-rule str-repl-repl-src-inv-no-ctn2 ((@T0 Type) (@T1 Type) (@T2 Type) (x1 (Seq @T0)) (y1 (Seq @T1)) (z1 (Seq @T2))) + :premises ((= (seq.contains y1 z1) false)) + :args (x1 y1 z1) + :conclusion (= (seq.replace x1 (seq.replace y1 x1 z1) x1) (seq.replace x1 y1 x1)) +) +(declare-rule str-repl-repl-src-inv-no-ctn3 ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (@T4 Type) (x1 (Seq @T0)) (y1 (Seq @T1)) (z1 (Seq @T2)) (w1 (Seq @T3)) (u1 (Seq @T4))) + :premises ((= (seq.contains x1 z1) false) (= (seq.contains x1 w1) false)) + :args (x1 y1 z1 w1 u1) + :conclusion (= (seq.replace x1 (seq.replace y1 z1 w1) u1) (seq.replace x1 y1 u1)) +) +(declare-rule str-repl-repl-dual-self ((@T0 Type) (@T1 Type) (x1 (Seq @T0)) (y1 (Seq @T1))) + :args (x1 y1) + :conclusion (= (seq.replace x1 (seq.replace x1 y1 x1) x1) x1) +) +(declare-rule str-repl-repl-dual-ite1 ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (x1 (Seq @T0)) (y1 (Seq @T1)) (z1 (Seq @T2)) (w1 (Seq @T3))) + :premises ((= (seq.contains x1 z1) false)) + :args (x1 y1 z1 w1) + :conclusion (= (seq.replace x1 (seq.replace x1 y1 z1) w1) (ite (seq.contains x1 y1) x1 w1)) +) +(declare-rule str-repl-repl-dual-ite2 ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (x1 (Seq @T0)) (y1 (Seq @T1)) (z1 (Seq @T2)) (w1 (Seq @T3))) + :premises ((= (seq.contains y1 z1) false) (= (seq.contains z1 y1) false)) + :args (x1 y1 z1 w1) + :conclusion (= (seq.replace x1 (seq.replace x1 y1 z1) w1) (ite (seq.contains x1 y1) x1 w1)) +) +(declare-rule str-repl-repl-lookahead-id-simp ((@T0 Type) (@T1 Type) (@T2 Type) (y1 (Seq @T0)) (z1 (Seq @T1)) (w1 (Seq @T2))) + :premises ((= (= w1 z1) false) (= (>= (seq.len w1) (seq.len z1)) true)) + :args (y1 z1 w1) + :conclusion (= (seq.replace (seq.replace y1 w1 y1) y1 z1) (seq.replace (seq.replace y1 w1 z1) y1 z1)) +) + +(declare-rule str-substr-len-include ((@T0 Type) (@T1 Type) (s1 (Seq @T0)) (s2 (Seq @T1) :list) (n1 Int) (m1 Int)) + :premises ((= (>= (seq.len s1) (+ n1 m1)) true)) + :args (s1 s2 n1 m1) + :conclusion (= (seq.extract (seq.++ s1 s2) n1 m1) (seq.extract s1 n1 m1)) +) +(declare-rule str-substr-len-include-pre ((@T0 Type) (@T1 Type) (@T2 Type) (s1 (Seq @T0)) (s2 (Seq @T1)) (s3 (Seq @T2) :list) (n1 Int)) + :premises ((= (>= n1 (seq.len s1)) true)) + :args (s1 s2 s3 n1) + :conclusion (= (seq.extract (seq.++ s1 s2 s3) 0 n1) (seq.++ s1 (seq.extract (seq.++ s2 s3) 0 (- n1 (seq.len s1))))) +) +(declare-rule str-substr-len-norm ((@T0 Type) (s1 (Seq @T0)) (n1 Int) (m1 Int)) + :premises ((= (>= m1 (seq.len s1)) true)) + :args (s1 n1 m1) + :conclusion (= (seq.extract s1 n1 m1) (seq.extract s1 n1 (seq.len s1))) +) +(declare-rule seq-len-rev ((@T0 Type) (x1 (Seq @T0))) + :args (x1) + :conclusion (= (seq.len (seq.rev x1)) (seq.len x1)) +) +(declare-rule seq-rev-rev ((@T0 Type) (x1 (Seq @T0))) + :args (x1) + :conclusion (= (seq.rev (seq.rev x1)) x1) +) +(declare-rule seq-rev-concat ((@T0 Type) (@T1 Type) (@T2 Type) (x1 (Seq @T0)) (y1 (Seq @T1) :list) (z1 (Seq @T2))) + :args (x1 y1 z1) + :conclusion (= (seq.rev (seq.++ x1 y1 z1)) (seq.++ (seq.rev z1) (seq.rev (seq.++ x1 y1)))) +) +(declare-rule str-eq-repl-self-emp ((@T0 Type) (@T1 Type) (@T2 Type) (x1 (Seq @T0)) (y1 (Seq @T1)) (emp1 (Seq @T2))) + :premises ((= (seq.len emp1) 0)) + :args (x1 y1 emp1) + :conclusion (= (= (seq.replace x1 y1 x1) emp1) (= x1 emp1)) +) +(declare-rule str-eq-repl-no-change ((@T0 Type) (@T1 Type) (@T2 Type) (x1 (Seq @T0)) (y1 (Seq @T1)) (z1 (Seq @T2))) + :premises ((= (= y1 z1) false)) + :args (x1 y1 z1) + :conclusion (= (= (seq.replace x1 y1 z1) x1) (not (seq.contains x1 y1))) +) +(declare-rule str-eq-repl-tgt-eq-len ((@T0 Type) (@T1 Type) (@T2 Type) (x1 (Seq @T0)) (y1 (Seq @T1)) (z1 (Seq @T2))) + :premises ((= (seq.len y1) (seq.len z1))) + :args (x1 y1 z1) + :conclusion (= (= (seq.replace x1 y1 z1) z1) (or (= x1 y1) (= x1 z1))) +) +(declare-rule str-eq-repl-len-one-emp-prefix ((@T0 Type) (@T1 Type) (@T2 Type) (x1 (Seq @T0)) (y1 (Seq @T1)) (emp1 (Seq @T2))) + :premises ((= (seq.len emp1) 0) (= (seq.len y1) 1)) + :args (x1 y1 emp1) + :conclusion (= (= (seq.replace x1 y1 emp1) emp1) (seq.prefixof x1 y1)) +) +(declare-rule str-eq-repl-emp-tgt-nemp ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (x1 (Seq @T0)) (y1 (Seq @T1)) (z1 (Seq @T2)) (emp1 (Seq @T3))) + :premises ((= (seq.len emp1) 0) (= (= z1 emp1) false)) + :args (x1 y1 z1 emp1) + :conclusion (= (= (seq.replace x1 y1 z1) emp1) (and (= x1 emp1) (not (= y1 emp1)))) +) +(declare-rule str-eq-repl-nemp-src-emp ((@T0 Type) (@T1 Type) (@T2 Type) (@T3 Type) (x1 (Seq @T0)) (y1 (Seq @T1)) (z1 (Seq @T2)) (emp1 (Seq @T3))) + :premises ((= (seq.len emp1) 0) (= (= z1 emp1) false)) + :args (x1 y1 z1 emp1) + :conclusion (= (= (seq.replace emp1 x1 y1) z1) (and (= x1 emp1) (= y1 z1))) +) +(declare-rule str-eq-repl-self-src ((@T0 Type) (@T1 Type) (x1 (Seq @T0)) (y1 (Seq @T1))) + :args (x1 y1) + :conclusion (= (= (seq.replace x1 y1 x1) y1) (= x1 y1)) +) diff --git a/Tests/RareAsEunoiaTests/level4_rewrites.eo b/Tests/RareAsEunoiaTests/level4_rewrites.eo new file mode 100644 index 0000000..e7fa129 --- /dev/null +++ b/Tests/RareAsEunoiaTests/level4_rewrites.eo @@ -0,0 +1,202 @@ +;;;;;;;;;;;;;;;;; +;; Arrays +;;;;;;;;;;;;;;;;; + +(declare-rule arith-abs-int-gt ((x1 Int) (y1 Int)) + :args (x1 y1) + :conclusion (= (> (abs x1) (abs y1)) (eo::define ((_let_1 (- y1))) (eo::define ((_let_2 (- x1))) (eo::define ((_let_3 (>= y1 0))) (ite (>= x1 0) (ite _let_3 (> x1 y1) (> x1 _let_1)) (ite _let_3 (> _let_2 y1) (> _let_2 _let_1))))))) +) +(declare-rule arith-abs-real-gt ((x1 Real) (y1 Real)) + :args (x1 y1) + :conclusion (= (> (abs x1) (abs y1)) (eo::define ((_let_1 (- y1))) (eo::define ((_let_2 (- x1))) (eo::define ((_let_3 (>= y1 0/1))) (ite (>= x1 0/1) (ite _let_3 (> x1 y1) (> x1 _let_1)) (ite _let_3 (> _let_2 y1) (> _let_2 _let_1))))))) +) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Strings and regular expressions +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(declare-rule str-in-re-range-elim ((s1 String) (c1 String) (c2 String)) + :premises ((= (str.len c1) 1) (= (str.len c2) 1)) + :args (s1 c1 c2) + :conclusion (= (str.in_re s1 (re.range c1 c2)) (eo::define ((_let_1 (str.to_code s1))) (and (<= (str.to_code c1) _let_1) (<= _let_1 (str.to_code c2))))) +) +(declare-rule str-in-re-contains ((t1 String) (s1 String)) + :args (t1 s1) + :conclusion (= (eo::define ((_let_1 (re.* re.allchar))) (str.in_re t1 (re.++ _let_1 (str.to_re s1) _let_1))) (str.contains t1 s1)) +) +(declare-rule str-in-re-from-int-nemp-dig-range ((n1 Int)) + :premises ((= (>= n1 0) true)) + :args (n1) + :conclusion (= (eo::define ((_let_1 (re.range "0" "9"))) (str.in_re (str.from_int n1) (re.++ _let_1 (re.* _let_1)))) true) +) +(declare-rule str-suffixof-elim ((@T0 Type) (@T1 Type) (s1 (Seq @T0)) (t1 (Seq @T1))) + :args (s1 t1) + :conclusion (= (seq.suffixof s1 t1) (eo::define ((_let_1 (seq.len s1))) (= s1 (seq.extract t1 (- (seq.len t1) _let_1) _let_1)))) +) +(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 re-concat-star-repeat ((xs1 RegLan :list) (r1 RegLan) (ys1 RegLan :list)) + :args (xs1 r1 ys1) + :conclusion (= (eo::define ((_let_1 (re.* r1))) (re.++ xs1 _let_1 _let_1 ys1)) (re.++ xs1 (re.* r1) ys1)) +) + +;;;;;;;;;;;;;;;;; +;; BitVectors +;;;;;;;;;;;;;;;;; + +(declare-rule uf-sbv-to-int-elim ((@n0 Int) (t1 (BitVec @n0)) (wm1 Int) (n1 Int)) + :premises ((= wm1 (- (@bvsize t1) 1)) (= n1 (int.pow2 (@bvsize t1)))) + :args (t1 wm1 n1) + :conclusion (= (sbv_to_int t1) (eo::define ((_let_1 (ubv_to_int t1))) (ite (= (extract wm1 wm1 t1) (@bv 0 1)) _let_1 (- _let_1 n1)))) +) +(declare-rule bv-ult-add-one ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (x1 (BitVec @n0)) (ys1 (BitVec @n1) :list) (zs1 (BitVec @n2) :list) (c1 (BitVec @n3)) (w1 Int)) + :premises ((= c1 (@bv 1 w1)) (= w1 (@bvsize x1))) + :args (x1 ys1 zs1 c1 w1) + :conclusion (= (bvult x1 (bvadd ys1 c1 zs1)) (eo::define ((_let_1 (bvadd ys1 zs1))) (and (not (= _let_1 (bvnot (@bv 0 w1)))) (not (bvult _let_1 x1))))) +) +(declare-rule bv-and-concat-pullup ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (@n4 Int) (xs1 (BitVec @n0) :list) (ws1 (BitVec @n1) :list) (y1 (BitVec @n2)) (z1 (BitVec @n3)) (ys1 (BitVec @n4) :list) (nxm1 Int) (ny1 Int) (nym1 Int)) + :premises ((= ny1 (@bvsize y1)) (= nxm1 (- (@bvsize (bvand xs1 ws1)) 1)) (= nym1 (- (@bvsize y1) 1))) + :args (xs1 ws1 y1 z1 ys1 nxm1 ny1 nym1) + :conclusion (= (bvand xs1 (concat ys1 z1 y1) ws1) (eo::define ((_let_1 (bvand xs1 ws1))) (concat (bvand (extract nxm1 ny1 _let_1) (concat ys1 z1)) (bvand (extract nym1 0 _let_1) y1)))) +) +(declare-rule bv-or-concat-pullup ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (@n4 Int) (xs1 (BitVec @n0) :list) (ws1 (BitVec @n1) :list) (y1 (BitVec @n2)) (z1 (BitVec @n3)) (ys1 (BitVec @n4) :list) (nxm1 Int) (ny1 Int) (nym1 Int)) + :premises ((= ny1 (@bvsize y1)) (= nxm1 (- (@bvsize (bvor xs1 ws1)) 1)) (= nym1 (- (@bvsize y1) 1))) + :args (xs1 ws1 y1 z1 ys1 nxm1 ny1 nym1) + :conclusion (= (bvor xs1 (concat ys1 z1 y1) ws1) (eo::define ((_let_1 (bvor xs1 ws1))) (concat (bvor (extract nxm1 ny1 _let_1) (concat ys1 z1)) (bvor (extract nym1 0 _let_1) y1)))) +) +(declare-rule bv-xor-concat-pullup ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (@n4 Int) (xs1 (BitVec @n0) :list) (ws1 (BitVec @n1) :list) (y1 (BitVec @n2)) (z1 (BitVec @n3)) (ys1 (BitVec @n4) :list) (nxm1 Int) (ny1 Int) (nym1 Int)) + :premises ((= ny1 (@bvsize y1)) (= nxm1 (- (@bvsize (bvxor xs1 ws1)) 1)) (= nym1 (- (@bvsize y1) 1))) + :args (xs1 ws1 y1 z1 ys1 nxm1 ny1 nym1) + :conclusion (= (bvxor xs1 (concat ys1 z1 y1) ws1) (eo::define ((_let_1 (bvxor xs1 ws1))) (concat (bvxor (extract nxm1 ny1 _let_1) (concat ys1 z1)) (bvxor (extract nym1 0 _let_1) y1)))) +) +(declare-rule bv-and-concat-pullup2 ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (@n4 Int) (xs1 (BitVec @n0) :list) (ws1 (BitVec @n1) :list) (y1 (BitVec @n2)) (z1 (BitVec @n3)) (ys1 (BitVec @n4) :list) (nxm1 Int) (ny1 Int) (nym1 Int)) + :premises ((= ny1 (@bvsize (concat y1 ys1))) (= nxm1 (- (@bvsize (bvand xs1 ws1)) 1)) (= nym1 (- (@bvsize (concat y1 ys1)) 1))) + :args (xs1 ws1 y1 z1 ys1 nxm1 ny1 nym1) + :conclusion (= (bvand xs1 (concat z1 y1 ys1) ws1) (eo::define ((_let_1 (bvand xs1 ws1))) (concat (bvand (extract nxm1 ny1 _let_1) z1) (bvand (extract nym1 0 _let_1) (concat y1 ys1))))) +) +(declare-rule bv-or-concat-pullup2 ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (@n4 Int) (xs1 (BitVec @n0) :list) (ws1 (BitVec @n1) :list) (y1 (BitVec @n2)) (z1 (BitVec @n3)) (ys1 (BitVec @n4) :list) (nxm1 Int) (ny1 Int) (nym1 Int)) + :premises ((= ny1 (@bvsize (concat y1 ys1))) (= nxm1 (- (@bvsize (bvor xs1 ws1)) 1)) (= nym1 (- (@bvsize (concat y1 ys1)) 1))) + :args (xs1 ws1 y1 z1 ys1 nxm1 ny1 nym1) + :conclusion (= (bvor xs1 (concat z1 y1 ys1) ws1) (eo::define ((_let_1 (bvor xs1 ws1))) (concat (bvor (extract nxm1 ny1 _let_1) z1) (bvor (extract nym1 0 _let_1) (concat y1 ys1))))) +) +(declare-rule bv-xor-concat-pullup2 ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (@n4 Int) (xs1 (BitVec @n0) :list) (ws1 (BitVec @n1) :list) (y1 (BitVec @n2)) (z1 (BitVec @n3)) (ys1 (BitVec @n4) :list) (nxm1 Int) (ny1 Int) (nym1 Int)) + :premises ((= ny1 (@bvsize (concat y1 ys1))) (= nxm1 (- (@bvsize (bvxor xs1 ws1)) 1)) (= nym1 (- (@bvsize (concat y1 ys1)) 1))) + :args (xs1 ws1 y1 z1 ys1 nxm1 ny1 nym1) + :conclusion (= (bvxor xs1 (concat z1 y1 ys1) ws1) (eo::define ((_let_1 (bvxor xs1 ws1))) (concat (bvxor (extract nxm1 ny1 _let_1) z1) (bvxor (extract nym1 0 _let_1) (concat y1 ys1))))) +) +(declare-rule bv-and-concat-pullup3 ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (@n4 Int) (xs1 (BitVec @n0) :list) (ws1 (BitVec @n1) :list) (y1 (BitVec @n2)) (z1 (BitVec @n3)) (u1 (BitVec @n4)) (nxm1 Int) (nyu1 Int) (nyum1 Int) (nu1 Int) (num1 Int)) + :premises ((= nxm1 (- (@bvsize (bvand xs1 ws1)) 1)) (= nyu1 (+ (@bvsize y1) (@bvsize u1))) (= nyum1 (- (+ (@bvsize y1) (@bvsize u1)) 1)) (= nu1 (@bvsize u1)) (= num1 (- (@bvsize u1) 1))) + :args (xs1 ws1 y1 z1 u1 nxm1 nyu1 nyum1 nu1 num1) + :conclusion (= (bvand xs1 (concat z1 y1 u1) ws1) (eo::define ((_let_1 (bvand xs1 ws1))) (concat (bvand (extract nxm1 nyu1 _let_1) z1) (bvand (extract nyum1 nu1 _let_1) y1) (bvand (extract num1 0 _let_1) u1)))) +) +(declare-rule bv-or-concat-pullup3 ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (@n4 Int) (xs1 (BitVec @n0) :list) (ws1 (BitVec @n1) :list) (y1 (BitVec @n2)) (z1 (BitVec @n3)) (u1 (BitVec @n4)) (nxm1 Int) (nyu1 Int) (nyum1 Int) (nu1 Int) (num1 Int)) + :premises ((= nxm1 (- (@bvsize (bvor xs1 ws1)) 1)) (= nyu1 (+ (@bvsize y1) (@bvsize u1))) (= nyum1 (- (+ (@bvsize y1) (@bvsize u1)) 1)) (= nu1 (@bvsize u1)) (= num1 (- (@bvsize u1) 1))) + :args (xs1 ws1 y1 z1 u1 nxm1 nyu1 nyum1 nu1 num1) + :conclusion (= (bvor xs1 (concat z1 y1 u1) ws1) (eo::define ((_let_1 (bvor xs1 ws1))) (concat (bvor (extract nxm1 nyu1 _let_1) z1) (bvor (extract nyum1 nu1 _let_1) y1) (bvor (extract num1 0 _let_1) u1)))) +) +(declare-rule bv-xor-concat-pullup3 ((@n0 Int) (@n1 Int) (@n2 Int) (@n3 Int) (@n4 Int) (xs1 (BitVec @n0) :list) (ws1 (BitVec @n1) :list) (y1 (BitVec @n2)) (z1 (BitVec @n3)) (u1 (BitVec @n4)) (nxm1 Int) (nyu1 Int) (nyum1 Int) (nu1 Int) (num1 Int)) + :premises ((= nxm1 (- (@bvsize (bvxor xs1 ws1)) 1)) (= nyu1 (+ (@bvsize y1) (@bvsize u1))) (= nyum1 (- (+ (@bvsize y1) (@bvsize u1)) 1)) (= nu1 (@bvsize u1)) (= num1 (- (@bvsize u1) 1))) + :args (xs1 ws1 y1 z1 u1 nxm1 nyu1 nyum1 nu1 num1) + :conclusion (= (bvxor xs1 (concat z1 y1 u1) ws1) (eo::define ((_let_1 (bvxor xs1 ws1))) (concat (bvxor (extract nxm1 nyu1 _let_1) z1) (bvxor (extract nyum1 nu1 _let_1) y1) (bvxor (extract num1 0 _let_1) u1)))) +) +(declare-rule bv-mult-slt-mult-1 ((@n0 Int) (@n1 Int) (@n2 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (a1 (BitVec @n2)) (n1 Int) (m1 Int) (tn1 Int) (an1 Int)) + :premises ((= tn1 (@bvsize x1)) (= an1 (@bvsize a1))) + :args (x1 y1 a1 n1 m1 tn1 an1) + :conclusion (= (eo::define ((_let_1 (sign_extend m1 a1))) (bvslt (bvmul (sign_extend n1 y1) _let_1) (bvmul (sign_extend n1 x1) _let_1))) (eo::define ((_let_1 (@bv 0 an1))) (and (not (= (bvsub y1 x1) (@bv 0 tn1))) (not (= a1 _let_1)) (= (bvslt y1 x1) (bvsgt a1 _let_1))))) +) +(declare-rule bv-mult-slt-mult-2 ((@n0 Int) (@n1 Int) (@n2 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (a1 (BitVec @n2)) (n1 Int) (m1 Int) (tn1 Int) (an1 Int)) + :premises ((= tn1 (@bvsize x1)) (= an1 (@bvsize a1))) + :args (x1 y1 a1 n1 m1 tn1 an1) + :conclusion (= (eo::define ((_let_1 (sign_extend m1 a1))) (bvslt (bvmul (zero_extend n1 y1) _let_1) (bvmul (zero_extend n1 x1) _let_1))) (eo::define ((_let_1 (@bv 0 an1))) (and (not (= (bvsub y1 x1) (@bv 0 tn1))) (not (= a1 _let_1)) (= (bvult y1 x1) (bvsgt a1 _let_1))))) +) +(declare-rule bv-ite-width-one ((@n0 Int) (x1 (BitVec @n0))) + :args (x1) + :conclusion (= (eo::define ((_let_1 (@bv 1 1))) (ite (= x1 _let_1) _let_1 (@bv 0 1))) x1) +) +(declare-rule bv-ite-width-one-not ((@n0 Int) (x1 (BitVec @n0))) + :args (x1) + :conclusion (= (eo::define ((_let_1 (@bv 0 1))) (ite (= x1 _let_1) (@bv 1 1) _let_1)) (bvnot x1)) +) +(declare-rule bv-rotate-left-eliminate-1 ((@n0 Int) (x1 (BitVec @n0)) (amount1 Int) (u1 Int) (u2 Int) (l1 Int)) + :premises ((= (= (mod amount1 (@bvsize x1)) 0) false) (eo::define ((_let_1 (@bvsize x1))) (= u1 (- _let_1 (+ 1 (mod amount1 _let_1))))) (= u2 (- (@bvsize x1) 1)) (eo::define ((_let_1 (@bvsize x1))) (= l1 (- _let_1 (mod amount1 _let_1))))) + :args (x1 amount1 u1 u2 l1) + :conclusion (= (rotate_left amount1 x1) (concat (extract u1 0 x1) (extract u2 l1 x1))) +) +(declare-rule bv-sdiv-eliminate ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (nm1 Int)) + :premises ((= nm1 (- (@bvsize x1) 1))) + :args (x1 y1 nm1) + :conclusion (= (bvsdiv x1 y1) (eo::define ((_let_1 (@bv 1 1))) (eo::define ((_let_2 (= (extract nm1 nm1 y1) _let_1))) (eo::define ((_let_3 (= (extract nm1 nm1 x1) _let_1))) (eo::define ((_let_4 (bvudiv (ite _let_3 (bvneg x1) x1) (ite _let_2 (bvneg y1) y1)))) (ite (xor _let_3 _let_2) (bvneg _let_4) _let_4)))))) +) +(declare-rule bv-uaddo-eliminate ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (w1 Int)) + :premises ((= w1 (@bvsize x1))) + :args (x1 y1 w1) + :conclusion (= (bvuaddo x1 y1) (eo::define ((_let_1 (@bv 0 1))) (= (extract w1 w1 (bvadd (concat _let_1 x1) (concat _let_1 y1))) (@bv 1 1)))) +) +(declare-rule bv-saddo-eliminate ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (wm1 Int)) + :premises ((= wm1 (- (@bvsize x1) 1))) + :args (x1 y1 wm1) + :conclusion (= (bvsaddo x1 y1) (eo::define ((_let_1 (@bv 1 1))) (eo::define ((_let_2 (extract wm1 wm1 (bvadd x1 y1)))) (eo::define ((_let_3 (@bv 0 1))) (eo::define ((_let_4 (extract wm1 wm1 y1))) (eo::define ((_let_5 (extract wm1 wm1 x1))) (or (and (and (= _let_5 _let_1) (= _let_4 _let_1)) (= _let_2 _let_3)) (and (and (= _let_5 _let_3) (= _let_4 _let_3)) (= _let_2 _let_1))))))))) +) +(declare-rule bv-smod-eliminate ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (w1 Int) (wm1 Int)) + :premises ((= w1 (@bvsize x1)) (= wm1 (- (@bvsize x1) 1))) + :args (x1 y1 w1 wm1) + :conclusion (= (bvsmod x1 y1) (eo::define ((_let_1 (@bv 0 1))) (eo::define ((_let_2 (extract wm1 wm1 y1))) (eo::define ((_let_3 (= _let_2 _let_1))) (eo::define ((_let_4 (extract wm1 wm1 x1))) (eo::define ((_let_5 (= _let_4 _let_1))) (eo::define ((_let_6 (bvurem (ite _let_5 x1 (bvneg x1)) (ite _let_3 y1 (bvneg y1))))) (eo::define ((_let_7 (bvneg _let_6))) (eo::define ((_let_8 (@bv 1 1))) (ite (= _let_6 (@bv 0 w1)) _let_6 (ite (and _let_5 _let_3) _let_6 (ite (and (= _let_4 _let_8) _let_3) (bvadd _let_7 y1) (ite (and _let_5 (= _let_2 _let_8)) (bvadd _let_6 y1) _let_7))))))))))))) +) +(declare-rule bv-srem-eliminate ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (nm1 Int)) + :premises ((= nm1 (- (@bvsize x1) 1))) + :args (x1 y1 nm1) + :conclusion (= (bvsrem x1 y1) (eo::define ((_let_1 (@bv 1 1))) (eo::define ((_let_2 (= (extract nm1 nm1 x1) _let_1))) (eo::define ((_let_3 (bvurem (ite _let_2 (bvneg x1) x1) (ite (= (extract nm1 nm1 y1) _let_1) (bvneg y1) y1)))) (ite _let_2 (bvneg _let_3) _let_3))))) +) +(declare-rule bv-ssubo-eliminate ((@n0 Int) (@n1 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (nm1 Int)) + :premises ((= nm1 (- (@bvsize x1) 1))) + :args (x1 y1 nm1) + :conclusion (= (bvssubo x1 y1) (eo::define ((_let_1 (@bv 1 1))) (eo::define ((_let_2 (extract nm1 nm1 (bvsub x1 y1)))) (eo::define ((_let_3 (extract nm1 nm1 y1))) (eo::define ((_let_4 (@bv 0 1))) (eo::define ((_let_5 (extract nm1 nm1 x1))) (or (and (and (= _let_5 _let_1) (= _let_3 _let_4)) (= _let_2 _let_4)) (and (and (= _let_5 _let_4) (= _let_3 _let_1)) (= _let_2 _let_1))))))))) +) +(declare-rule bv-ugt-urem ((@n0 Int) (@n1 Int) (y1 (BitVec @n0)) (x1 (BitVec @n1)) (w1 Int)) + :premises ((= w1 (@bvsize y1))) + :args (y1 x1 w1) + :conclusion (= (bvugt (bvurem y1 x1) x1) (eodefine ((_let_1 (@bv 0 w1))) (and (= x1 _let_1) (bvugt y1 _let_1)))) +) +(declare-rule bv-sign-extend-eq-const-1 ((@n0 Int) (x1 (BitVec @n0)) (m1 Int) (c1 Int) (nm1 Int) (mp1 Int) (nm2 Int) (nmm1 Int)) + :premises ((= mp1 (+ m1 1)) (= nm2 (- (@bvsize x1) 1)) (= nmm1 (- nm1 1))) + :args (x1 m1 c1 nm1 mp1 nm2 nmm1) + :conclusion (= (= (sign_extend m1 x1) (@bv c1 nm1)) (eo::define ((_let_1 (@bv c1 nm1))) (eo::define ((_let_2 (@bv 0 mp1))) (eo::define ((_let_3 (extract nmm1 nm2 _let_1))) (and (or (= _let_3 _let_2) (= _let_3 (bvnot _let_2))) (= x1 (extract nm2 0 _let_1))))))) +) +(declare-rule bv-sign-extend-eq-const-2 ((@n0 Int) (x1 (BitVec @n0)) (m1 Int) (c1 Int) (nm1 Int) (mp1 Int) (nm2 Int) (nmm1 Int)) + :premises ((= mp1 (+ m1 1)) (= nm2 (- (@bvsize x1) 1)) (= nmm1 (- nm1 1))) + :args (x1 m1 c1 nm1 mp1 nm2 nmm1) + :conclusion (= (= (@bv c1 nm1) (sign_extend m1 x1)) (eo::define ((_let_1 (@bv c1 nm1))) (eo::define ((_let_2 (@bv 0 mp1))) (eo::define ((_let_3 (extract nmm1 nm2 _let_1))) (and (or (= _let_3 _let_2) (= _let_3 (bvnot _let_2))) (= x1 (extract nm2 0 _let_1))))))) +) +(declare-rule bv-zero-extend-eq-const-1 ((@n0 Int) (x1 (BitVec @n0)) (m1 Int) (c1 Int) (nm1 Int) (nm2 Int) (nmm1 Int)) + :premises ((= nm2 (- (@bvsize x1) 1)) (= nmm1 (- nm1 1))) + :args (x1 m1 c1 nm1 nm2 nmm1) + :conclusion (= (= (zero_extend m1 x1) (@bv c1 nm1)) (eo::define ((_let_1 (@bv c1 nm1))) (and (= (extract nmm1 nm2 _let_1) (@bv 0 m1)) (= x1 (extract nm2 0 _let_1))))) +) +(declare-rule bv-zero-extend-eq-const-2 ((@n0 Int) (x1 (BitVec @n0)) (m1 Int) (c1 Int) (nm1 Int) (nm2 Int) (nmm1 Int)) + :premises ((= nm2 (- (@bvsize x1) 1)) (= nmm1 (- nm1 1))) + :args (x1 m1 c1 nm1 nm2 nmm1) + :conclusion (= (= (@bv c1 nm1) (zero_extend m1 x1)) (eo::define ((_let_1 (@bv c1 nm1))) (and (= (extract nmm1 nm2 _let_1) (@bv 0 m1)) (= x1 (extract nm2 0 _let_1))))) +) +(declare-rule bv-zero-extend-ult-const-1 ((@n0 Int) (x1 (BitVec @n0)) (m1 Int) (c1 Int) (nm1 Int) (nm2 Int)) + :premises ((= nm2 (- (@bvsize x1) 1)) (eo::define ((_let_1 (@bv c1 nm1))) (= _let_1 (zero_extend m1 (extract nm2 0 _let_1))))) + :args (x1 m1 c1 nm1 nm2) + :conclusion (= (bvult (zero_extend m1 x1) (@bv c1 nm1)) (bvult x1 (extract nm2 0 (@bv c1 nm1)))) +) +(declare-rule bv-zero-extend-ult-const-2 ((@n0 Int) (x1 (BitVec @n0)) (m1 Int) (c1 Int) (nm1 Int) (nm2 Int)) + :premises ((= nm2 (- (@bvsize x1) 1)) (eo::define ((_let_1 (@bv c1 nm1))) (= _let_1 (zero_extend m1 (extract nm2 0 _let_1))))) + :args (x1 m1 c1 nm1 nm2) + :conclusion (= (bvult (@bv c1 nm1) (zero_extend m1 x1)) (bvult (extract nm2 0 (@bv c1 nm1)) x1)) +) +(declare-rule bv-sign-extend-ult-const-1 ((@n0 Int) (x1 (BitVec @n0)) (m1 Int) (c1 Int) (nm1 Int) (nm2 Int)) + :premises ((eo::define ((_let_1 (@bv (- (@bvsize x1) 1) nm1))) (eo::define ((_let_2 (@bv c1 nm1))) (= (or (bvule _let_2 (bvshl (@bv 1 nm1) _let_1)) (bvuge _let_2 (bvshl (bvnot (@bv 0 nm1)) _let_1))) true))) (= nm2 (- (@bvsize x1) 1))) + :args (x1 m1 c1 nm1 nm2) + :conclusion (= (bvult (sign_extend m1 x1) (@bv c1 nm1)) (bvult x1 (extract nm2 0 (@bv c1 nm1)))) +) +(declare-rule bv-sign-extend-ult-const-3 ((@n0 Int) (x1 (BitVec @n0)) (m1 Int) (c1 Int) (nm1 Int) (nm2 Int)) + :premises ((eo::define ((_let_1 (bvshl (@bv 1 nm1) (@bv (- (@bvsize x1) 1) nm1)))) (eo::define ((_let_2 (@bv c1 nm1))) (= (or (bvult _let_2 _let_1) (bvuge _let_2 (bvnot _let_1))) true))) (= nm2 (- (@bvsize x1) 1))) + :args (x1 m1 c1 nm1 nm2) + :conclusion (= (bvult (@bv c1 nm1) (sign_extend m1 x1)) (bvult (extract nm2 0 (@bv c1 nm1)) x1)) +) + diff --git a/src/abstract_type_parser.ML b/src/abstract_type_parser.ML index 5fe52ea..1d78011 100644 --- a/src/abstract_type_parser.ML +++ b/src/abstract_type_parser.ML @@ -4,15 +4,33 @@ Additional type and term parser for RARE for its features that extend SMT-LIB *) - fun rare_type_parser (SMTLIB.Sym "?Array", []) = SOME (Type(\<^type_name>\fun\,[dummyT,Type(\<^type_name>\option\,[dummyT])])) | rare_type_parser (SMTLIB.Sym "?Set", []) = SOME (Type(\<^type_name>\Set.set\,[dummyT])) | rare_type_parser (SMTLIB.Sym "?", []) = SOME (dummyT) + (* Check if it is an Eunoia's Type variable. *) + | rare_type_parser (SMTLIB.Sym variable, []) = if String.isPrefix "TYPE" variable + then (* Eunoia's Type variables are represented + as an schematic type variable, whose index + is 0: when a Type variable is present in + an Eunoia rule, the corresponding Isabelle + lemma begins with a quantification of + the corresponding schematic type variable.*) + SOME (TVar (("?" ^ variable, 0), [])) + else NONE | rare_type_parser _ = NONE +(* Embedding of arithmetic symbols. *) +fun rare_term_parser (SMTLIB.Sym "div_total", [t1, t2]) = SOME ( \<^term>\Rings.divide::int => int => int\ $ t1 $ t2) + | rare_term_parser (SMTLIB.Sym "mod_total", [t1, t2]) = SOME ( \<^term>\Rings.modulo::int => int => int\ $ t1 $ t2) + | rare_term_parser (SMTLIB.Sym "divisible", [t1, t2]) = SOME ( \<^term>\Rings.dvd::int => int => bool\ $ t1 $ t2) + | rare_term_parser (SMTLIB.Sym "abs", [t]) = SOME ( \<^term>\Groups.abs::int => int\ $ t) + | rare_term_parser _ = NONE + +(* Registering parsers for specific constructions. *) val _ = Theory.setup (Context.theory_map ( - SMTLIB_Proof.add_type_parser rare_type_parser)) + SMTLIB_Proof.add_type_parser rare_type_parser #> + SMTLIB_Proof.add_term_parser rare_term_parser)) (* fun mk_test (t1, t2) = (Const (\<^const_name>\Word.word_cat\, dummyT --> dummyT --> dummyT)) $ t1 $ t2 @@ -41,4 +59,4 @@ fun mk_concat (t, u) = val t2' = if T2 = \<^typ>\Int.int\ then Const ( \<^const_name>\nat\, T2 --> \<^typ>\Nat.nat\) $ t2 else t2 in SOME (Const (\<^const_name>\SMT_Word.smt_extract\, @{typ nat} --> @{typ nat} --> dummyT --> dummyT) $ t1' $ t2' $ t3) end -*) \ No newline at end of file +*) diff --git a/src/parse_rare.ML b/src/parse_rare.ML index b2581de..96c8e01 100644 --- a/src/parse_rare.ML +++ b/src/parse_rare.ML @@ -147,6 +147,10 @@ fun parse_token s [] = s | parse_token _ _ = raise TOKEN("error parsing token") +(* Common smaller parsing routines *) + +fun equal_to c = (curry (op =) c) + (* Lexer Util *) fun debug_msg_lexer ctxt l msg = @@ -163,7 +167,7 @@ fun raise_lexer_error l msg = raise PARSE(lexer_debug_prefix l ^ msg) fun lexer_add_line ctxt l line uf = let val _ = verbose_msg_lexer ctxt ("reading line nr. " ^ Int.toString(l) ^ ": " ^ line) - val trimmed_lines = raw_explode line |> Library.trim (curry (op =) " ") + val trimmed_lines = raw_explode line |> Library.trim (equal_to " ") in case trimmed_lines of [] => (debug_msg_lexer ctxt l ("found empty line , skip"); uf) | @@ -173,7 +177,7 @@ in val _ = debug_msg_lexer ctxt l ("found non empty line, start parsing rule"); (* If line has a comment in it cut it *) val sanitized_lines = - Library.take (Library.find_index (curry (op =) ";") trimmed_lines) trimmed_lines |> Library.trim (curry (op =) " ") + Library.take (Library.find_index (equal_to ";") trimmed_lines) trimmed_lines |> Library.trim (equal_to " ") val token = parse_token uf sanitized_lines handle @@ -227,15 +231,15 @@ in end fun expect_char l err_msg c cs = - Scan.catch (Scan.one (curry (op =) c)) cs + Scan.catch (Scan.one (equal_to c)) cs handle (Fail _) => raise_parser_error l ("Expected '" ^ c ^ "' but could not find it." ^ err_msg) fun least_one_char l err_msg c cs = - Scan.catch (Scan.many1 (curry (op =) c)) cs + Scan.catch (Scan.many1 (equal_to c)) cs handle (Fail _) => raise_parser_error l ("Expected at least one '" ^ c ^ "' but could not find any." ^ err_msg) fun ignore_chars l c cs = - Scan.catch (Scan.many (curry (op =) c)) cs + Scan.catch (Scan.many (equal_to c)) cs handle (Fail _) => raise_parser_error l ("Was expecting more input but rule might have ended prematurely. ") @@ -251,18 +255,15 @@ fun type_parser _ (("d"::"e"::"f"::"i"::"n"::"e"::"-"::"r"::"u"::"l"::"e"::"*":: ::"r"::"u"::"l"::"e"::cs)) = (DEFINE_COND_RULE,cs) | type_parser l _ = raise_parser_error l "Could not read type!" -(* In alf the rule type is determined by annotations and not by a keyword. However, there is some -syntax sugar that allows to write declare-axiom for rules without any conditions. Since the type -depends on whether a :rare-fixed-point or a :premises ((= F false)) term is found later in the -rule we cannot determine it here yet. *) +(* Eunoia declare-rule token *) -datatype alf_rule_type = ALF_AXIOM | ALF_RULE +datatype eunoia_declare_rule = EUNOIA_RULE -fun alf_type_parser _ (("d"::"e"::"c"::"l"::"a"::"r"::"e"::"-"::"a"::"x"::"i"::"o"::"m":: cs)) = - (ALF_AXIOM,cs) | - alf_type_parser _ (("d"::"e"::"c"::"l"::"a"::"r"::"e"::"-"::"r"::"u"::"l"::"e":: cs)) = - (ALF_RULE,cs) | - alf_type_parser l _ = raise_parser_error l "Could not read type of alf rule!" +fun eunoia_declare_rule_lexer + _ (("d"::"e"::"c"::"l"::"a"::"r"::"e"::"-"::"r"::"u"::"l"::"e":: cs)) = + (EUNOIA_RULE,cs) | + eunoia_declare_rule_lexer + l _ = raise_parser_error l "Could not read Eunoia's declare-rule keyword!" (* Rule name *) @@ -297,8 +298,8 @@ fun par_parser l = (parse_next_term l >> implode) :|-- (fn s => fn cs => if s<>" fun param_parser l = expect_char l "Could not find first opening parentheses in parameter list" "(" - --| (Scan.many (curry (op =) " ")) - |-- (Scan.repeat (par_parser l --| (Scan.many1 (curry (op =) " "))) + --| (Scan.many (equal_to " ")) + |-- (Scan.repeat (par_parser l --| (Scan.many1 (equal_to " "))) @@@ (Scan.option (par_parser l) >> (fn NONE => [] | SOME xs => [xs]))) --| expect_char l "Could not find final closing parentheses in parameter list" ")" @@ -307,26 +308,26 @@ fun param_parser l = fun let_parser l (cs : string list) = (@{print}("let",cs); cs |> Scan.catch( - (Scan.many1 (curry (op =) " ")) - --| (Scan.one (curry (op =) "(")) - -- Scan.many (curry (op =) " ") - --| Scan.one (curry (op =) "d") - --| Scan.one (curry (op =) "e") - --| Scan.one (curry (op =) "f") - --| Scan.many1 (curry (op =) " ") + (Scan.many1 (equal_to " ")) + --| (Scan.one (equal_to "(")) + -- Scan.many (equal_to " ") + --| Scan.one (equal_to "d") + --| Scan.one (equal_to "e") + --| Scan.one (equal_to "d") + --| Scan.many1 (equal_to " ") |-- (Scan.repeat (( - (Scan.one (curry (op =) "(")) + (Scan.one (equal_to "(")) |-- parse_next_term l - --| (Scan.many1 (curry (op =) " ")) + --| (Scan.many1 (equal_to " ")) -- parse_next_term l - --| (Scan.many (curry (op =) " ")) - --| (Scan.one (curry (op =) ")")) - --| (Scan.many (curry (op =) " ")) + --| (Scan.many (equal_to " ")) + --| (Scan.one (equal_to ")")) + --| (Scan.many (equal_to " ")) ) >> (fn (v,t) => (get_smtlib_term l v,get_smtlib_term l t)) )) - --| Scan.many (curry (op =) " ") - --| Scan.one (curry (op =) ")")) + --| Scan.many (equal_to " ") + --| Scan.one (equal_to ")")) >> Option.SOME handle (Fail _) => (NONE,cs) @@ -361,22 +362,22 @@ let -- let_parser l :|-- debug_msg ctxt "possible let defs" (fn (SOME xs) => str_of_lets xs | NONE => "") -- Scan.repeat - ((Scan.many1 (curry (op =) " ")) + ((Scan.many1 (equal_to " ")) |-- (expression_parser l)) :|-- debug_msg ctxt "expressions" (fn xs => String.concat (map SMTLIB.str_of xs)) --| ignore_chars l " " --| (Scan.one (fn c => c = ")")) --| (fn cs => if cs = [] then Scan.succeed [] cs else raise_parser_error l "Text found after end of rule") - fun seperate_expr DEFINE_RULE [m,t] = (NONE,m,t,NONE) | - seperate_expr DEFINE_COND_RULE [p,m,t] = (SOME p,m,t,NONE) | - seperate_expr DEFINE_RULE_STAR [m,t] = (NONE,m,t,NONE) | - seperate_expr DEFINE_RULE_STAR [m,t,c] = (NONE,m,t,SOME c) | - seperate_expr r xs = + fun separate_expr DEFINE_RULE [m,t] = (NONE,m,t,NONE) | + separate_expr DEFINE_COND_RULE [p,m,t] = (SOME p,m,t,NONE) | + separate_expr DEFINE_RULE_STAR [m,t] = (NONE,m,t,NONE) | + separate_expr DEFINE_RULE_STAR [m,t,c] = (NONE,m,t,SOME c) | + separate_expr r xs = raise_parser_error l ("Rule type is " ^ str_of_type r ^ " but found " ^ Int.toString(length xs) ^ "expressions") - val (rprecondition,rmatch,rtarget,rcontext_expr) = seperate_expr rtyp rexpressions + val (rprecondition,rmatch,rtarget,rcontext_expr) = separate_expr rtyp rexpressions in ({ @@ -393,50 +394,103 @@ in end +(* EUNOIA *) + +(* Traverses a given list of Eunoia declare-rule parameters, removing + occurrences of the Type universe, and collecting information about variables + of type Type, for later processing. + TODO: current approach renames Type variables x to "_TYPE_" ^ x. *) +fun remove_type_universe accum [] = [] | + +remove_type_universe accum ((Par (SMTLIB.S [SMTLIB.Sym t_name, + SMTLIB.Sym "Type"])) :: xs) += +remove_type_universe ((SMTLIB.Sym t_name) :: accum) xs | + +remove_type_universe accum ((Par (SMTLIB.S [SMTLIB.Sym var, + SMTLIB.Sym t_name])) :: xs) += +if List.exists (fn x => x = (SMTLIB.Sym t_name)) accum +then +(Par (SMTLIB.S [SMTLIB.Sym var, + SMTLIB.Sym ("TYPE" ^ t_name)])) :: remove_type_universe accum xs +else +(Par (SMTLIB.S [SMTLIB.Sym var, + SMTLIB.Sym t_name])) :: remove_type_universe accum xs | + +remove_type_universe accum (x :: xs) = x :: remove_type_universe accum xs + + +fun convert_bit_vectors_to_approx [] = [] | + + convert_bit_vectors_to_approx + ((Par (SMTLIB.S [SMTLIB.Sym t_name, + SMTLIB.S [SMTLIB.Sym "BitVec", + SMTLIB.Sym width] + ]))::xs) + = + ((Par (SMTLIB.S [SMTLIB.Sym t_name, + SMTLIB.Sym "?BitVec"]))::convert_bit_vectors_to_approx xs) | + + convert_bit_vectors_to_approx (x::xs) = x::convert_bit_vectors_to_approx xs -fun parse_single_alf_rule ctxt (l,cs) = +fun eunoia_param_parser l = + expect_char l "Could not find first opening parentheses in parameter list" "(" + --| (Scan.many (equal_to " ")) + |-- (((Scan.repeat ((par_parser l) --| (Scan.many1 (equal_to " "))) ) + @@@ (Scan.option (par_parser l) + >> (fn NONE => [] | SOME xs => [xs]))) + >> remove_type_universe [] + >> convert_bit_vectors_to_approx) + + --| expect_char l "Could not find final closing parentheses in parameter list" ")" + + +fun parse_single_eunoia_rule ctxt (l,cs) = let fun debug_msg ctxt msg f (x,t) cs = ((debug_msg_parser ctxt ("Parsed " ^ msg ^ ". Token parsed in is: " ^ f t );((x,t),cs))) - val (((((_,alfT),rname),rparams),rexpressions),cs') + val (((((_,eunoiaT),rname),rparams),rexpressions),cs') = cs |> - Scan.succeed (debug_msg_parser ctxt ("Start parsing alf rule in line " ^ Int.toString(l) )) + Scan.succeed (debug_msg_parser ctxt ("Start parsing eunoia rule in line " ^ Int.toString(l) )) --| (Scan.one (fn c => c = "(")) --| ignore_chars l " " - -- alf_type_parser l + -- eunoia_declare_rule_lexer l --| least_one_char l "No whitespace after type found." " " -- name_parser l :|-- debug_msg ctxt "name" I --| least_one_char l "No whitespace after name found." " " - -- param_parser l - :|-- debug_msg ctxt "parameter" (fn xs => String.concat (map str_of_par xs)) + -- eunoia_param_parser l + :|-- debug_msg ctxt "Eunoia parameter" (fn xs => String.concat (map str_of_par xs)) -- Scan.repeat - ((Scan.many1 (curry (op =) " ")) + ((Scan.many1 (equal_to " ")) |-- (expression_parser l)) - :|-- debug_msg ctxt "expressions" (fn xs => String.concat (map SMTLIB.str_of xs)) + :|-- debug_msg ctxt "Eunoia expressions" (fn xs => String.concat (map SMTLIB.str_of xs)) --| ignore_chars l " " --| (Scan.one (fn c => c = ")")) --| (fn cs => if cs = [] then Scan.succeed [] cs else raise_parser_error l "Text found after end of rule") - fun seperate_expr_rule ((SMTLIB.Key "premises")::p::(SMTLIB.Key "conclusion")::[c]) = (DEFINE_COND_RULE,SOME p,c) | - seperate_expr_rule ((SMTLIB.Key "conclusion")::[c,SMTLIB.Key "rare-fixed-point"]) = (DEFINE_RULE_STAR,NONE,c) | (*TODO: Ask Andy does this has the context expr as argument? Or do thy not exist anymore?*) - seperate_expr_rule ((SMTLIB.Key "conclusion")::[c]) = (DEFINE_RULE,NONE,c) | - seperate_expr_rule xs =(@{print}("xs",xs); - raise_parser_error l ("Found " - ^ Int.toString(length xs) ^ " expressions in rule but expected less or more than that.")) + fun separate_expr_rule ((SMTLIB.Key "args")::args::(SMTLIB.Key "conclusion")::[c]) + = (* We ignore occurrences of Eunoia's :args *) + (DEFINE_RULE,NONE,c) | - fun seperate_expr_axiom (c::[SMTLIB.Key "rare-fixed-point"]) = (DEFINE_RULE_STAR,NONE,c) | - seperate_expr_axiom [c] = (DEFINE_RULE,NONE,c) | - seperate_expr_axiom xs = (@{print}("xs",xs); - raise_parser_error l ("Found " - ^ Int.toString(length xs) ^ " expressions in axiom but expected less or more than that.")) + separate_expr_rule ((SMTLIB.Key "premises")::p::(SMTLIB.Key "args")::args::(SMTLIB.Key "conclusion")::[c]) + = + (DEFINE_COND_RULE,SOME (@{print}("Eunoia premises parsed:", p); p |> + (fn SMTLIB.S xs => (if length xs = 1 then hd xs else SMTLIB.S ([SMTLIB.Sym "and"] @ xs)))) , c) | + separate_expr_rule xs + = + (@{print}("xs",xs); raise_parser_error l + ("Found " + ^ Int.toString(length xs) + ^ " expressions in rule but expected less or more than that.")) - val (rtyp,rprecondition,conclusion) = rexpressions |> (if alfT = ALF_RULE then seperate_expr_rule else seperate_expr_axiom) + val (rtyp,rprecondition,conclusion) = rexpressions |> separate_expr_rule val (rmatch,rtarget) = (fn (SMTLIB.S [SMTLIB.Sym "=", x,y]) => (x,y) | _ => raise_parser_error l "" ) conclusion in @@ -458,9 +512,9 @@ end fun parse_rewrites ctxt xs = map ((if Config.get ctxt IsaRARE_Config.ruleFormat = "RARE" then parse_single_rule - else if Config.get ctxt IsaRARE_Config.ruleFormat = "ALF" - then parse_single_alf_rule + else if Config.get ctxt IsaRARE_Config.ruleFormat = "EUNOIA" + then parse_single_eunoia_rule else raise_parser_error 0 "Unkown proof format set") ctxt) (map (fn (i,x) => (i,raw_explode x)) xs) -end; \ No newline at end of file +end; diff --git a/src/process_rare.ML b/src/process_rare.ML index 679dbaf..93bedb6 100644 --- a/src/process_rare.ML +++ b/src/process_rare.ML @@ -148,7 +148,7 @@ fun process_rule ctxt (rule as ({rule_name, params, let_defs, ...} : rewrite_rul (*Add implicit assumptions*) val (implAss,body') = RARE_Impl_Assms.process ctxt body params val body_with_implAss = SMTLIB.S [SMTLIB.Sym "implies", SMTLIB.S ([SMTLIB.Sym "and"]@implAss), body'] - val _ = IsaRARE_Config.debug_msg ctxt (fn _ => "Added impl ass " ^ SMTLIB.str_of body_with_implAss) [] + val _ = IsaRARE_Config.debug_msg ctxt (fn _ => "Added impl ass " ^ (if (Config.get ctxt IsaRARE_Config.implAssump) then SMTLIB.str_of body_with_implAss else "None")) [] val body_with_implAss = body (*Add lets*) diff --git a/src/string_parser.ML b/src/string_parser.ML index fba9e60..78ce749 100644 --- a/src/string_parser.ML +++ b/src/string_parser.ML @@ -76,7 +76,7 @@ fun string_term_parser (SMTLIB.Sym "str.++", t::ts) = SOME (mk_lassoc' \<^const | string_term_parser (SMTLIB.Sym "re.range", [t1,t2]) = SOME (mk_binary \<^const_name>\re_range\ \<^typ>\uc_regex\ t1 t2) | string_term_parser (SMTLIB.Sym "re.^", [t1]) = SOME (mk_unary \<^const_abbrev>\re_pow\ \<^typ>\uc_regex\ t1) (*TODO*) | string_term_parser (SMTLIB.Sym "re.loop", [t1]) = SOME (mk_unary \<^const_abbrev>\re_loop\ \<^typ>\uc_regex\ t1) (*TODO*) - | string_term_parser (SMTLIB.Sym "str.is_digit", [t1]) = SOME (mk_unary \<^const_name>\is_digit\ \<^typ>\HOL.bool\ t1) + | string_term_parser (SMTLIB.Sym "str.is_digit", [t1]) = SOME (mk_unary \<^const_name>\is_digit\ \<^typ>\HOL.bool\ t1) | string_term_parser (SMTLIB.Sym "str.to_code", [t1]) = SOME (mk_unary \<^const_name>\to_code\ \<^typ>\Int.int\ t1) | string_term_parser (SMTLIB.Sym "str.from_code", [t1]) = SOME (mk_unary \<^const_name>\from_code\ \<^typ>\uc_word\ t1) | string_term_parser (SMTLIB.Sym "str.to_int", [t1]) = SOME (mk_unary \<^const_name>\to_int\ \<^typ>\Int.int\ t1) diff --git a/src/write_theory.ML b/src/write_theory.ML index 9072682..5b509d4 100644 --- a/src/write_theory.ML +++ b/src/write_theory.ML @@ -48,7 +48,7 @@ We could find closest anchestor but who guarantees us that we can prove the lemm fun write_file_header ctxt theory_name theory_imports = Library.cat_lines ["theory " ^ theory_name, - " imports \"HOL-CVC.Dsl_Nary_Ops\" " ^ theory_imports, + " imports \"HOL.Dsl_Nary_Ops\" " ^ theory_imports, "begin\n", "(* Thank you for using IsaRARE. This is a theory automatically created from a RARE file!", "All that remains to do is to prove any lemma whose provided proof fails.", @@ -186,8 +186,13 @@ fun write_lemma ctxt i (lemma as {rule_name,rule_body} : rewrite_rule_lemma) = -fun write_thy ctxt theory_name theory_imports cs = (@{print}("cs",cs); - write_file_header ctxt theory_name theory_imports ^ String.concat (map (write_lemma ctxt 0) cs) ^ write_file_footer) +fun write_thy ctxt theory_name theory_imports cs = +let + val ctxt = (Config.put show_types false ctxt) + val ctxt = (Config.put show_sorts false ctxt) +in + write_file_header ctxt theory_name theory_imports ^ String.concat (map (write_lemma ctxt 0) cs) ^ write_file_footer +end end; \ No newline at end of file