level0_rewrites.eo

;;;;;;;;;;;;;;;;;
;; Arith
;;;;;;;;;;;;;;;;;

(declare-rule arith-int-div-total ((t1 Int) (s1 Int))
  :premises ((= (= s1 0) false))
  :args (t1 s1)
  :conclusion (= (div t1 s1) (div_total t1 s1))
)
(declare-rule arith-int-div-total-one ((t1 Int))
  :args (t1)
  :conclusion (= (div_total t1 1) t1)
)
(declare-rule arith-int-div-total-zero ((t1 Int))
  :args (t1)
  :conclusion (= (div_total t1 0) 0)
)
(declare-rule arith-int-div-total-neg ((t1 Int) (s1 Int))
  :premises ((= (< s1 0) true))
  :args (t1 s1)
  :conclusion (= (div_total t1 s1) (- (div_total t1 (- s1))))
)
(declare-rule arith-int-mod-total ((t1 Int) (s1 Int))
  :premises ((= (= s1 0) false))
  :args (t1 s1)
  :conclusion (= (mod t1 s1) (mod_total t1 s1))
)
(declare-rule arith-int-mod-total-one ((t1 Int))
  :args (t1)
  :conclusion (= (mod_total t1 1) 0)
)
(declare-rule arith-int-mod-total-zero ((t1 Int))
  :args (t1)
  :conclusion (= (mod_total t1 0) t1)
)
(declare-rule arith-int-mod-total-neg ((t1 Int) (s1 Int))
  :premises ((= (< s1 0) true))
  :args (t1 s1)
  :conclusion (= (mod_total t1 s1) (mod_total t1 (- s1)))
)
(declare-rule arith-elim-int-gt ((t1 Int) (s1 Int))
  :args (t1 s1)
  :conclusion (= (> 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)
)