Remove quantifiers rewrite rules infrastructure (#3754)

11 files changed, 0 insertions, 612 deletions

diff --git a/test/regress/regress0/rewriterules/datatypes.smt2 b/test/regress/regress0/rewriterules/datatypes.smt2
deleted file mode 100644
index 9a5f68100..000000000
--- a/test/regress/regress0/rewriterules/datatypes.smt2
+++ /dev/null
@@ -1,102 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; try to solve datatypes with rewriterules
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; lists 2 nil
-(declare-sort elt 0) ;; we suppose that elt is infinite
-(declare-sort list 0)
-
-(declare-fun nil1 () list)
-(declare-fun nil2 () list)
-(declare-fun cons (elt list) list)
-
-;;;;;;;;;;;;;;;;;;;;
-;; injective
-
-(declare-fun inj1 (list) elt)
-(assert (forall ((?e elt) (?l list))
-                (! (! (=> true (=> true (= (inj1 (cons ?e ?l)) ?e))) :pattern ((cons ?e ?l)) ) :rewrite-rule) ))
-
-(declare-fun inj2 (list) list)
-(assert (forall ((?e elt) (?l list))
-                (! (! (=> true (=> true (= (inj2 (cons ?e ?l)) ?l))) :pattern ((cons ?e ?l)) ) :rewrite-rule) ))
-
-;;;;;;;;;;;;;;;;;;;;
-;; projection
-
-(declare-fun proj1 (list) elt)
-(assert (forall ((?e elt) (?l list))
-                (! (= (proj1 (cons ?e ?l)) ?e) :rewrite-rule) ))
-
-(declare-fun proj2 (list) list)
-(assert (forall ((?e elt) (?l list))
-                (! (= (proj2 (cons ?e ?l)) ?l) :rewrite-rule) ))
-
-;;;;;;;;;;;;;;;;;;;
-;; test
-(declare-fun iscons (list) Bool)
-(assert (= (iscons nil1) false))
-(assert (= (iscons nil2) false))
-(assert (forall ((?e elt) (?l list))
-                (! (! (=> true (=> true (= (iscons (cons ?e ?l)) true))) :pattern ((cons ?e ?l)) ) :rewrite-rule) ))
-
-(assert (forall ((?l list))
-                (! (! (=> true (=> (iscons ?l) (= ?l (cons (proj1 ?l) (proj2 ?l))))) :pattern ((proj1 ?l)) ) :rewrite-rule) ))
-(assert (forall ((?l list))
-                (! (! (=> true (=> (iscons ?l) (= ?l (cons (proj1 ?l) (proj2 ?l))))) :pattern ((proj2 ?l)) ) :rewrite-rule) ))
-
-
-(declare-fun isnil1 (list) Bool)
-(assert (= (isnil1 nil1) true))
-(assert (= (isnil1 nil2) false))
-(assert (forall ((?e elt) (?l list))
-                (! (= (isnil1 (cons ?e ?l)) false) :rewrite-rule) ))
-(assert (forall ((?l list))
-                (! (=> true (=> (isnil1 ?l) (= ?l nil1))) :rewrite-rule) ))
-
-(declare-fun isnil2 (list) Bool)
-(assert (= (isnil2 nil1) false))
-(assert (= (isnil2 nil2) true))
-(assert (forall ((?e elt) (?l list))
-                (! (= (isnil2 (cons ?e ?l)) false) :rewrite-rule) ))
-(assert (forall ((?l list))
-                (! (=> true (=> (isnil2 ?l) (= ?l nil2))) :rewrite-rule) ))
-
-;; distinct
-(assert (forall ((?l list))
-                (! (=> (isnil1 ?l) (and (not (isnil2 ?l)) (not (iscons ?l))) ) :rewrite-rule) ))
-
-(assert (forall ((?l list))
-                (! (=> (isnil2 ?l) (and (not (isnil1 ?l)) (not (iscons ?l))) ) :rewrite-rule) ))
-
-(assert (forall ((?l list))
-                (! (=> (iscons ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l))) ) :rewrite-rule) ))
-
-
-;;;;;;;;;;;;;;;;;;;
-;; case-split
-(assert (forall ((?l list))
-                (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons ?l))) :pattern ((proj1 ?l)) ) :rewrite-rule) ))
-(assert (forall ((?l list))
-                (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons ?l))) :pattern ((proj2 ?l)) ) :rewrite-rule) ))
-
-;;;;;;;;;;;;;;;;;;;
-;; finite case-split
-(assert (forall ((?l list))
-                 (! (=> (not (iscons ?l)) (or (isnil1 ?l) (isnil2 ?l))) :rewrite-rule) ))
-
-
-
-;;;;; goal
-
-(declare-fun e () elt)
-(declare-fun l1 () list)
-(declare-fun l2 () list)
-
-
-(assert (not (=> (iscons l1) (=> (= (proj2 l1) (proj2 l2)) (= l1 (cons (proj1 l1) (proj2 l2)))))))
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress0/rewriterules/datatypes_clark.smt2 b/test/regress/regress0/rewriterules/datatypes_clark.smt2
deleted file mode 100644
index cc217fc79..000000000
--- a/test/regress/regress0/rewriterules/datatypes_clark.smt2
+++ /dev/null
@@ -1,205 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-(set-logic AUFLIRA)
-
-;; DATATYPE
-;;   nat = succ(pred : nat) | zero,
-;;   list = cons(car : tree, cdr : list) | null,
-;;   tree = node(children : list) | leaf(data : nat)
-;; END;
-
-;;;;;;;;;;;
-;; nat   ;;
-;;;;;;;;;;;
-(declare-sort nat 0)
-(declare-fun zero () nat)
-(declare-fun succ (nat) nat)
-
-;;;;;;;;;;;;;;;;
-;; injective
-
-(declare-fun inj1 (nat) nat)
-(assert-propagation((?x1 nat))
-                 (((succ ?x1))) () () (= (inj1 (succ ?x1)) ?x1) )
-
-;;;;;;;;;;;;;;;;;;;;
-;; projection
-
-(declare-fun pred (nat) nat)
-(assert-rewrite ((?x1 nat)) () () (pred (succ ?x1)) ?x1 )
-
-(assert (= (pred zero) zero))
-
-;;;;;;;;;;;;;;;;;;;
-;; test
-(declare-fun is_succ (nat) Bool)
-(assert (= (is_succ zero) false))
-(assert-propagation ((?x1 nat)) (((succ ?x1))) () () (= (is_succ (succ ?x1)) true) )
-
-(assert-propagation ((?x1 nat)) (((pred ?x1))) () ((is_succ ?x1)) (= ?x1 (succ (pred ?x1))))
-
-(declare-fun is_zero (nat) Bool)
-(assert (= (is_zero zero) true))
-(assert-propagation ((?x1 nat)) () () ((is_zero ?x1)) (= ?x1 zero))
-
-;;; directrr
-(assert-rewrite ((?x1 nat)) () () (is_succ (succ ?x1)) true )
-(assert-rewrite ((?x1 nat)) () () (is_zero (succ ?x1)) false )
-
-
-;;;;;;;;;;;;;;;;;;;;
-;; distinct
-(assert-propagation ((?x1 nat)) () () ((is_zero ?x1)) (not (is_succ ?x1)) )
-(assert-propagation ((?x1 nat)) () () ((is_succ ?x1)) (not (is_zero ?x1)) )
-(assert-propagation ((?x1 nat)) () () ((not (is_zero ?x1))) (is_succ ?x1) )
-(assert-propagation ((?x1 nat)) () () ((not (is_succ ?x1))) (is_zero ?x1) )
-
-;;;;;;;;;;;;;;;;;;;
-;; case-split
-(assert-propagation ((?x1 nat)) (((pred ?x1))) () () (or (is_zero ?x1) (is_succ ?x1)) )
-
-;;;;;;;;;;;;;;;;;;;
-;; non-cyclic
-(declare-fun size_nat (nat) Real)
-(assert-propagation ((?x1 nat)) (((succ ?x1))) () () (> (size_nat (succ ?x1)) (size_nat ?x1)) )
-
-
-
-;;;;;;;;;;;;;;;;;;;;;
-;; list and tree
-
-(declare-sort list 0)
-(declare-sort tree 0)
-
-;;;;;;;;;;;
-;; list  ;;
-;;;;;;;;;;;
-
-(declare-fun null () list)
-(declare-fun cons (tree list) list)
-
-(declare-fun node (list) tree)
-(declare-fun leaf (nat) tree)
-
-;;;;;;;;;;;;;;;;
-;; injective
-
-(declare-fun inj2 (list) tree)
-(assert-propagation ((?x1 tree) (?x2 list)) (((cons ?x1 ?x2))) () () (= (inj2 (cons ?x1 ?x2)) ?x1) )
-
-(declare-fun inj3 (list) list)
-(assert-propagation ((?x1 tree) (?x2 list)) (((cons ?x1 ?x2))) () () (= (inj3 (cons ?x1 ?x2)) ?x2) )
-
-
-;;;;;;;;;;;;;;;;;;;;
-;; projection
-
-(declare-fun car (list) tree)
-(assert-rewrite ((?x1 tree) (?x2 list)) () () (car (cons ?x1 ?x2)) ?x1)
-
-(assert (= (car null) (node null)))
-
-(declare-fun cdr (list) list)
-(assert-rewrite ((?x1 tree) (?x2 list)) () () (cdr (cons ?x1 ?x2)) ?x2)
-
-(assert (= (cdr null) null))
-
-;;;;;;;;;;;;;;;;;;;
-;; test
-(declare-fun is_cons (list) Bool)
-(assert (= (is_cons null) false))
-(assert-propagation ((?x1 tree) (?x2 list)) (((cons ?x1 ?x2))) () () (= (is_cons (cons ?x1 ?x2)) true) )
-
-(assert-propagation ((?x1 list)) (((car ?x1))) () ((is_cons ?x1)) (= ?x1 (cons (car ?x1) (cdr ?x1))) )
-(assert-propagation ((?x1 list)) (((cdr ?x1))) () ((is_cons ?x1)) (= ?x1 (cons (car ?x1) (cdr ?x1))) )
-
-(declare-fun is_null (list) Bool)
-(assert (= (is_null null) true))
-
-(assert-propagation ((?x1 list)) (((car ?x1))) () ((is_null ?x1)) (= (car ?x1) (node null)) )
-(assert-propagation ((?x1 list)) (((cdr ?x1))) () ((is_null ?x1)) (= (cdr ?x1) null) )
-
-(assert-propagation ((?x1 list)) () () ((is_null ?x1)) (= ?x1 null))
-
-;;; directrr
-(assert-rewrite ((?x1 tree) (?x2 list)) () () (is_cons (cons ?x1 ?x2)) true)
-(assert-rewrite ((?x1 tree) (?x2 list)) () () (is_null (cons ?x1 ?x2)) false)
-
-
-
-;;;;;;;;;;;;;;;;;;;;
-;; distinct
-(assert-propagation ((?x1 list)) () () ((is_null ?x1)) (not (is_cons ?x1)) )
-(assert-propagation ((?x1 list)) () () ((is_cons ?x1)) (not (is_null ?x1)) )
-(assert-propagation ((?x1 list)) () () ((not (is_null ?x1))) (is_cons ?x1) )
-(assert-propagation ((?x1 list)) () () ((not (is_cons ?x1))) (is_null ?x1) )
-
-;;;;;;;;;;;;;;;;;;;
-;; case-split
-(assert-propagation ((?x1 list)) (((car ?x1))) () () (or (is_null ?x1) (is_cons ?x1)) )
-(assert-propagation ((?x1 list)) (((cdr ?x1))) () () (or (is_null ?x1) (is_cons ?x1)) )
-
-;;;;;;;;;;;;;;;
-;; tree
-
-;;;;;;;;;;;;;;;;
-;; injective
-
-(declare-fun inj4 (tree) list)
-(assert-propagation ((?x1 list)) (((node ?x1))) () () (= (inj4 (node ?x1)) ?x1) )
-
-(declare-fun inj5 (tree) nat)
-(assert-propagation ((?x1 nat)) (((leaf ?x1))) () () (= (inj5 (leaf ?x1)) ?x1) )
-
-
-;;;;;;;;;;;;;;;;;;;;
-;; projection
-
-(declare-fun children (tree) list)
-(assert-rewrite ((?x1 list)) () () (children (node ?x1)) ?x1 )
-(assert-rewrite ((?x1 nat)) () () (children (leaf ?x1)) null )
-
-(declare-fun data (tree) nat)
-(assert-rewrite ((?x1 nat)) () () (data (leaf ?x1)) ?x1 )
-(assert-rewrite ((?x1 list)) () () (data (node ?x1)) zero )
-
-;;;;;;;;;;;;;;;;;;;
-;; test
-(declare-fun is_node (tree) Bool)
-(assert-propagation ((?x1 list)) (((node ?x1))) () () (= (is_node (node ?x1)) true) )
-
-(assert-propagation ((?x1 tree)) (((children ?x1))) () ((is_node ?x1)) (= ?x1 (node (children ?x1))) )
-(assert-propagation ((?x1 tree)) (((data ?x1))) () ((is_node ?x1)) (= (data ?x1) zero) )
-
-
-(declare-fun is_leaf (tree) Bool)
-(assert-propagation ((?x1 nat)) (((leaf ?x1))) () () (= (is_leaf (leaf ?x1)) true) )
-(assert-propagation ((?x1 tree)) (((data ?x1))) () ((is_leaf ?x1)) (= ?x1 (leaf (data ?x1))) )
-(assert-propagation ((?x1 tree)) (((children ?x1))) () ((is_leaf ?x1)) (= (children ?x1) null) )
-
-;;; directrr
-(assert-rewrite ((?x1 list)) () () (is_node (node ?x1)) true )
-(assert-rewrite ((?x1 list)) () () (is_leaf (node ?x1)) false )
-(assert-rewrite ((?x1 nat)) () () (is_leaf (leaf ?x1)) true )
-(assert-rewrite ((?x1 nat)) () () (is_node (leaf ?x1)) false )
-
-
-;;;;;;;;;;;;;;;;;;;;
-;; distinct
-(assert-propagation ((?x1 tree)) () () ((is_node ?x1)) (not (is_leaf ?x1)) )
-(assert-propagation ((?x1 tree)) () () ((is_leaf ?x1)) (not (is_node ?x1)) )
-(assert-propagation ((?x1 tree)) () () ((not (is_node ?x1))) (is_leaf ?x1) )
-(assert-propagation ((?x1 tree)) () () ((not (is_leaf ?x1))) (is_node ?x1) )
-
-;;;;;;;;;;;;;;;;;;;
-;; case-split
-(assert-propagation ((?x1 tree)) (((children ?x1))) () () (or (is_node ?x1) (is_leaf ?x1)) )
-(assert-propagation ((?x1 tree)) (((data ?x1))) () () (or (is_node ?x1) (is_leaf ?x1)) )
-
-
-;;;;;;;;;;;;;;;;;;
-;; non-cyclic
-(declare-fun size_list (list) Real)
-(declare-fun size_tree (tree) Real)
-(assert-propagation ((?x1 tree) (?x2 list)) (((cons ?x1 ?x2))) () () (and (> (size_list (cons ?x1 ?x2)) (size_tree ?x1)) (> (size_list (cons ?x1 ?x2)) (size_list ?x2))) )
-(assert-propagation ((?x1 list)) (((node ?x1))) () () (> (size_tree (node ?x1)) (size_list ?x1)) )
-(assert-propagation ((?x1 nat)) (((leaf ?x1))) () () (> (size_tree (leaf ?x1)) (size_nat ?x1)) )
diff --git a/test/regress/regress0/rewriterules/length.smt2 b/test/regress/regress0/rewriterules/length.smt2
deleted file mode 100644
index b144d7745..000000000
--- a/test/regress/regress0/rewriterules/length.smt2
+++ /dev/null
@@ -1,27 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort list 0)
-
-(declare-fun cons (Int list) list)
-(declare-fun nil  ()         list)
-
-
-;;define length
-(declare-fun length (list) Int)
-
-(assert (forall ((?l list)) (! (=> (= ?l nil) (= (length ?l) 0)) :rewrite-rule)))
-
-(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ (length ?l) 1)) :rewrite-rule)))
-
-;;(assert (forall ((?l list)) (=> (= ?l nil) (= (length ?l) 0))))
-
-;;(assert (forall ((?e Int) (?l list) (?l2 list)) (=> (= ?l2 (cons ?e ?l)) (= (length ?l2) (+ (length ?l) 1)))))
-
-
-(assert (not (= (length (cons 1 (cons  2 (cons 3 nil)))) 3)))
-
-(check-sat)
-(exit)
diff --git a/test/regress/regress0/rewriterules/length_gen_n.smt2 b/test/regress/regress0/rewriterules/length_gen_n.smt2
deleted file mode 100644
index 7da2f6777..000000000
--- a/test/regress/regress0/rewriterules/length_gen_n.smt2
+++ /dev/null
@@ -1,46 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; Same than length.smt2 but the nil case is not a rewrite rule
-;; So here the rewrite rules have no guards length
-
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort list 0)
-
-(declare-fun cons (Int list) list)
-(declare-fun nil  ()         list)
-
-
-;;define length
-(declare-fun length (list) Int)
-
-(assert (= (length nil) 0))
-
-(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ 1 (length ?l))) :rewrite-rule)))
-
-(declare-fun gen_cons (Int list) list)
-
-(assert (forall ((?n Int) (?l list)) (! (=> (= ?n 0) (= (gen_cons ?n ?l) ?l)) :rewrite-rule)))
-
-(assert (forall ((?n Int) (?l list)) (! (=> (> ?n 0) (= (gen_cons ?n ?l)
-        (gen_cons (- ?n 1) (cons 1 ?l)))) :rewrite-rule)))
-
-
-;;(assert (not (forall ((?n Int)) (=> (>= ?n 0) (=> (= (length (gen_cons ?n nil)) ?n) (= (length (gen_cons (+ ?n 1) nil)) (+ ?n 1))) ))))
-
-;;(assert (not (forall ((?n Int) (?l list)) (=> (>= ?n 0) (=> (= (length ?l) ?n) (= (length (cons 1 ?l)) (+ ?n 1))) ))))
-
-;; (assert (not (forall ((?n Int)) (=> (>= ?n 0) (=> (= (length (gen_cons ?n nil)) ?n) (= (length (cons 1 (gen_cons ?n nil))) (+ ?n 1))) ))))
-
-;;(assert (not (forall ((?n Int)) (=> (>= ?n 0) (= (gen_cons (+ ?n 1) nil) (cons 1 (gen_cons ?n nil))) ))))
-
-(assert (not (forall ((?n Int)) (=> (>= ?n 0) (=>
-        (forall ((?l list)) (= (gen_cons ?n (cons 1 ?l)) (cons 1 (gen_cons ?n ?l))))
-        (forall ((?l list)) (= (gen_cons (+ ?n 1) (cons 1 ?l)) (cons 1 (gen_cons (+ ?n 1) ?l))))
-     )))))
-
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress0/rewriterules/length_gen_n_lemma.smt2 b/test/regress/regress0/rewriterules/length_gen_n_lemma.smt2
deleted file mode 100644
index 7d65356ad..000000000
--- a/test/regress/regress0/rewriterules/length_gen_n_lemma.smt2
+++ /dev/null
@@ -1,44 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; Same than length.smt2 but the nil case is not a rewrite rule
-;; So here the rewrite rules have no guards length
-
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort list 0)
-
-(declare-fun cons (Int list) list)
-(declare-fun nil  ()         list)
-
-
-;;define length
-(declare-fun length (list) Int)
-
-(assert (= (length nil) 0))
-
-(assert (forall ((?e Int) (?l list)) (= (length (cons ?e ?l)) (+ 1 (length ?l)))))
-
-(declare-fun gen_cons (Int list) list)
-
-(assert (forall ((?n Int) (?l list)) (=> (= ?n 0) (= (gen_cons ?n ?l) ?l))))
-
-(assert (forall ((?n Int) (?l list)) (=> (> ?n 0) (= (gen_cons ?n ?l)
-        (gen_cons (- ?n 1) (cons 1 ?l))))))
-
-
-;;(assert (not (forall ((?n Int)) (=> (>= ?n 0) (=> (= (length (gen_cons ?n nil)) ?n) (= (length (gen_cons (+ ?n 1) nil)) (+ ?n 1))) ))))
-
-;;(assert (not (forall ((?n Int) (?l list)) (=> (>= ?n 0) (=> (= (length ?l) ?n) (= (length (cons 1 ?l)) (+ ?n 1))) ))))
-
-;;(assert (not (forall ((?n Int)) (=> (>= ?n 0) (=> (= (length (gen_cons ?n nil)) ?n) (= (length (cons 1 (gen_cons ?n nil))) (+ ?n 1))) ))))
-
-(assert (not (forall ((?n Int)) (=> (>= ?n 0) (=>
-        (forall ((?l list)) (= (gen_cons ?n (cons 1 ?l)) (cons 1 (gen_cons ?n ?l))))
-        (forall ((?l list)) (= (gen_cons (+ ?n 1) (cons 1 ?l)) (cons 1 (gen_cons (+ ?n 1) ?l))))
-     )))))
-
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress0/rewriterules/length_trick.smt2 b/test/regress/regress0/rewriterules/length_trick.smt2
deleted file mode 100644
index e01e97b84..000000000
--- a/test/regress/regress0/rewriterules/length_trick.smt2
+++ /dev/null
@@ -1,33 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; Same than length.smt2 but the nil case is not a rewrite rule
-;; So here the rewrite rules have no guards length
-
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort list 0)
-
-(declare-fun cons (Int list) list)
-(declare-fun nil  ()         list)
-
-
-;;define length
-(declare-fun length (list) Int)
-
-(assert (= (length nil) 0))
-
-
-
-
-(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ (length ?l) 1)) :rewrite-rule)))
-
-;;(assert (forall ((?l list)) (=> (= ?l nil) (= (length ?l) 0))))
-
-;;(assert (forall ((?e Int) (?l list) (?l2 list)) (=> (= ?l2 (cons ?e ?l)) (= (length ?l2) (+ (length ?l) 1)))))
-
-
-(assert (not (= (length (cons 1 (cons  2 (cons 3 nil)))) 3)))
-
-(check-sat)
-(exit)
diff --git a/test/regress/regress0/rewriterules/length_trick2.smt2 b/test/regress/regress0/rewriterules/length_trick2.smt2
deleted file mode 100644
index 8d47d9550..000000000
--- a/test/regress/regress0/rewriterules/length_trick2.smt2
+++ /dev/null
@@ -1,33 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; Same than length.smt2 but the nil case is not a rewrite rule
-;; So here the rewrite rules have no guards length
-
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort list 0)
-
-(declare-fun cons (Int list) list)
-(declare-fun nil  ()         list)
-
-
-;;define length
-(declare-fun length (list) Int)
-
-(assert (= (length nil) 0))
-
-
-
-
-(assert (forall ((?e Int) (?l list)) (! (= (length (cons ?e ?l)) (+ (length ?l) 1)) :rewrite-rule)))
-
-;;(assert (forall ((?l list)) (=> (= ?l nil) (= (length ?l) 0))))
-
-;;(assert (forall ((?e Int) (?l list) (?l2 list)) (=> (= ?l2 (cons ?e ?l)) (= (length ?l2) (+ (length ?l) 1)))))
-
-(assert (forall ((?a Int) (?b Int) (?l list))
-        (not (> (length (cons ?a (cons  ?b ?l))) (length ?l)))))
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress0/rewriterules/native_arrays.smt2 b/test/regress/regress0/rewriterules/native_arrays.smt2
deleted file mode 100644
index 83de7d8f4..000000000
--- a/test/regress/regress0/rewriterules/native_arrays.smt2
+++ /dev/null
@@ -1,35 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; This example can't be done if we don't access the EqualityEngine of
-;; the theory of arrays
-
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-(declare-sort Index 0)
-(declare-sort Element 0)
-
-;;A dumb predicate for a simple example
-(declare-fun P (Element) Bool)
-
-(assert-rewrite ((?i1 Index) (?i2 Index) (?e Element) (?a (Array Index Element))) () ()
-                (P (select (store ?a ?i1 ?e) ?i2)) true )
-
-(declare-fun a1 () (Array Index Element))
-(declare-fun a2 () (Array Index Element))
-(declare-fun a3 () (Array Index Element))
-(declare-fun i1 () Index)
-(declare-fun i2 () Index)
-(declare-fun e1 () Element)
-
-(assert (not (=>  (or (= a1 (store a2 i1 e1)) (= a1 (store a3 i1 e1))) (P (select a1 i2)) )))
-(check-sat)
-(exit)
-
-
-;; (declare-fun a1 () (Array Index Element))
-;; (declare-fun a2 () (Array Index Element))
-;; (declare-fun i1 () Index)
-;; (assert (= (store a1 i1 (select a2 i1)) (store a2 i1 (select a1 i1))))
-;; (assert (not (= a1 a2)))
-;; (check-sat)
-;; (exit)
diff --git a/test/regress/regress0/rewriterules/native_datatypes.smt2 b/test/regress/regress0/rewriterules/native_datatypes.smt2
deleted file mode 100644
index 365ec0624..000000000
--- a/test/regress/regress0/rewriterules/native_datatypes.smt2
+++ /dev/null
@@ -1,34 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; Same than length.smt2 but the nil case is not a rewrite rule
-;; So here the rewrite rules have no guards length
-
-(set-info :status unsat)
-
-(declare-datatypes ((nat 0) (list 0)) (
-((succ (pred nat)) (zero ) )
-((cons (car nat)(cdr list)) (nil ) )
-
-))
-
-
-;;define length
-(declare-fun length (list) nat)
-
-(assert (= (length nil) zero))
-
-(assert (forall ((?e nat) (?l list)) (! (= (length (cons ?e ?l)) (succ (length ?l))) :rewrite-rule)))
-
-(declare-fun gen_cons (nat list) list)
-
-(assert (forall ((?l list)) (! (= (gen_cons zero ?l) ?l) :rewrite-rule)))
-
-(assert (forall ((?n nat) (?l list)) (! (= (gen_cons (succ ?n) ?l)
-        (gen_cons ?n (cons zero ?l))) :rewrite-rule)))
-
-(declare-fun n () nat)
-
-(assert (not (= (length (gen_cons (succ (succ zero)) nil)) (succ (succ zero)))))
-
-(check-sat)
-
-(exit)
diff --git a/test/regress/regress0/rewriterules/relation.smt2 b/test/regress/regress0/rewriterules/relation.smt2
deleted file mode 100644
index 6b55a9677..000000000
--- a/test/regress/regress0/rewriterules/relation.smt2
+++ /dev/null
@@ -1,28 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-;; don't use a datatypes for currently focusing in uf
-(declare-sort elt 0)
-
-(declare-fun R (elt elt) Bool)
-
-;; reflexive
-(assert-rewrite ((x elt)) () () (R x x) true)
-
-;; transitive
-(assert-propagation ((x elt) (y elt) (z elt)) () () ((R x y) (R y z)) (R x z))
-
-;; anti-symmetric
-(assert-propagation ((x elt) (y elt)) () () ((R x y) (R y x)) (= x y))
-
-(declare-fun e1 () elt)
-(declare-fun e2 () elt)
-(declare-fun e3 () elt)
-(declare-fun e4 () elt)
-
-(assert (not (=> (and (R e1 e2) (R e2 e3) (R e3 e4) (R e4 e1)) (= e1 e4))))
-
-(check-sat)
-
-(exit)
\ No newline at end of file
diff --git a/test/regress/regress0/rewriterules/simulate_rewriting.smt2 b/test/regress/regress0/rewriterules/simulate_rewriting.smt2
deleted file mode 100644
index f67a0e6a2..000000000
--- a/test/regress/regress0/rewriterules/simulate_rewriting.smt2
+++ /dev/null
@@ -1,25 +0,0 @@
-; COMMAND-LINE: --rewrite-rules
-;; A new fast tableau-base ... Domenico Cantone et Calogero G.Zarba
-(set-logic AUFLIA)
-(set-info :status unsat)
-
-(declare-sort elt1 0)
-(declare-sort elt2 0)
-
-(declare-fun g (elt2) Bool)
-
-(declare-fun p (elt1 elt1) Bool)
-(declare-fun f (elt2) elt1)
-(declare-fun c1 () elt1)
-(declare-fun c2 () elt1)
-
-(assert (forall ((?e elt2)) (! (=> (g ?e) (= (f ?e) c2)) :rewrite-rule)))
-(assert (forall ((?e elt2)) (! (=> (g ?e) (= (f ?e) c1)) :rewrite-rule)))
-
-(declare-fun e () elt2)
-
-(assert (not (=> (g e) (=> (p c1 c2) (p (f e) (f e)))) ))
-
-(check-sat)
-
-(exit)