From: Tim King <taking@cs.nyu.edu>
Date: Thu, 11 Mar 2010 18:23:31 +0000 (+0000)
Subject: Added some hand generated UF tests. Unfortunartely all of them work. Also fixed some... 
X-Git-Tag: cvc5-1.0.0~9184
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7cc72123f6b422a53c8840ca034cfdb353be59bf;p=cvc5.git

Added some hand generated UF tests. Unfortunartely all of them work. Also fixed some cleanup stuff.
---

diff --git a/src/theory/theoryof_table_middle.h b/src/theory/theoryof_table_middle.h
index f3ad433a3..a0586d0ce 100644
--- a/src/theory/theoryof_table_middle.h
+++ b/src/theory/theoryof_table_middle.h
@@ -28,6 +28,9 @@ public:
   TheoryOfTable() :
     d_table(new Theory*[::CVC4::kind::LAST_KIND]) {
   }
+  ~TheoryOfTable(){
+    delete[] d_table;
+  }
 
   Theory* operator[](TNode n) {
     Assert(n.getKind() >= 0 && n.getKind() < ::CVC4::kind::LAST_KIND,
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 3753bd78a..128e28ca2 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -194,7 +194,7 @@ struct EquivClass;
 /**
  * ECAttr is the attribute that maps a node to an equivalence class.
  */
-typedef expr::Attribute<EquivClass, ECData* /*, ECCleanupFcn*/> ECAttr;
+typedef expr::Attribute<EquivClass, ECData*, ECCleanupFcn > ECAttr;
 
 } /* CVC4::theory::uf namespace */
 } /* CVC4::theory namespace */
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index a4e08ff99..b456f2809 100644
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -3,6 +3,18 @@ TESTS =	simple.01.cvc \
 	simple.02.cvc \
 	simple.03.cvc \
 	simple.04.cvc \
+	euf_simp01.smt \
+	euf_simp02.smt \
+	euf_simp03.smt \
+	euf_simp04.smt \
+	euf_simp05.smt \
+	euf_simp06.smt \
+	euf_simp08.smt \
+	euf_simp09.smt \
+	euf_simp10.smt \
+	euf_simp11.smt \
+	euf_simp12.smt \
+	euf_simp13.smt \
 	dead_dnd002.smt \
 	iso_brn001.smt \
 	SEQ032_size2.smt
diff --git a/test/regress/regress0/uf/euf_simp01.smt b/test/regress/regress0/uf/euf_simp01.smt
new file mode 100644
index 000000000..c121ae82e
--- /dev/null
+++ b/test/regress/regress0/uf/euf_simp01.smt
@@ -0,0 +1,23 @@
+
+(benchmark euf_simp1.smt
+:status sat
+:logic QF_UF
+:category { crafted }
+
+:extrafuns ((x U))
+:extrafuns ((y U))
+:extrafuns ((z U))
+:extrafuns ((f U U))
+:extrafuns ((g U U))
+:extrafuns ((H U U U))
+:extrafuns ((J U U U))
+
+
+
+:formula
+(and
+ (= (f x) (f z))
+ (= (g y) (g z))
+ (or (not (= x z)) (not (= y z)))
+ )
+)
\ No newline at end of file
diff --git a/test/regress/regress0/uf/euf_simp02.smt b/test/regress/regress0/uf/euf_simp02.smt
new file mode 100644
index 000000000..9c7b03f6e
--- /dev/null
+++ b/test/regress/regress0/uf/euf_simp02.smt
@@ -0,0 +1,29 @@
+
+(benchmark euf_simp2.smt
+:status unsat
+:logic QF_UF
+:category { crafted }
+
+:extrafuns ((x U))
+:extrafuns ((y U))
+:extrafuns ((z U))
+:extrafuns ((f U U))
+:extrafuns ((g U U))
+:extrafuns ((H U U U))
+:extrafuns ((J U U U))
+
+
+
+:formula
+(and
+ (not (= x y))
+ (= (f x) (f z))
+ (= (g y) (g z))
+ (= (g y) (g z))
+ (= (g y) y)
+ (= (f x) x)
+ (= (f z) z)
+ (= (g z) z)
+ (or (not (= x z)) (not (= y z)))
+ )
+)
\ No newline at end of file
diff --git a/test/regress/regress0/uf/euf_simp03.smt b/test/regress/regress0/uf/euf_simp03.smt
new file mode 100644
index 000000000..e0d6cc849
--- /dev/null
+++ b/test/regress/regress0/uf/euf_simp03.smt
@@ -0,0 +1,26 @@
+
+(benchmark euf_simp3.smt
+:status unsat
+:logic QF_UF
+:category { crafted }
+
+:extrafuns ((x U))
+:extrafuns ((y U))
+:extrafuns ((z U))
+:extrafuns ((f U U))
+:extrafuns ((g U U))
+:extrafuns ((H U U U))
+:extrafuns ((J U U U))
+
+
+
+:formula
+(and
+ (not (= x y))
+ (= (f (f x)) (f (f (f x))))
+ (= (f (f x)) y)
+ (= (f (f (f (f x)))) z)
+ (= (f x) z)
+ (not (= (f x) y))
+ )
+)
\ No newline at end of file
diff --git a/test/regress/regress0/uf/euf_simp04.smt b/test/regress/regress0/uf/euf_simp04.smt
new file mode 100644
index 000000000..7b15ad309
--- /dev/null
+++ b/test/regress/regress0/uf/euf_simp04.smt
@@ -0,0 +1,25 @@
+
+(benchmark euf_simp4.smt
+:status unsat
+:logic QF_UF
+:category { crafted }
+
+:extrafuns ((x U))
+:extrafuns ((y U))
+:extrafuns ((z U))
+:extrafuns ((f U U))
+:extrafuns ((g U U))
+:extrafuns ((H U U U))
+:extrafuns ((J U U U))
+
+
+
+:formula
+(and
+ (= (H x y) (H y x))
+ (or (= x (J z y)) (= y (J z y)))
+ (= (J z y) (f x))
+ (or (= x (f x)) (not (= y (f x))) )
+ (or (not (= x (f x))) (not (= (H x (f x)) (H (f x) x) )) )
+ )
+)
\ No newline at end of file
diff --git a/test/regress/regress0/uf/euf_simp05.smt b/test/regress/regress0/uf/euf_simp05.smt
new file mode 100644
index 000000000..85089a92a
--- /dev/null
+++ b/test/regress/regress0/uf/euf_simp05.smt
@@ -0,0 +1,11 @@
+(benchmark euf_simp5.smt
+
+  :status unsat
+  :difficulty { unknown }
+  :category { crafted }
+  :logic QF_UF
+  :extrasorts (A)
+  :extrafuns ((x A))
+  :extrafuns ((f A A))
+  :formula (let (?cvc_1 (f x)) (let (?cvc_0 (f ?cvc_1)) (not (implies (and (= ?cvc_0 x) (= (f ?cvc_0) x)) (= ?cvc_1 x)))))
+)
diff --git a/test/regress/regress0/uf/euf_simp06.smt b/test/regress/regress0/uf/euf_simp06.smt
new file mode 100644
index 000000000..020bafdff
--- /dev/null
+++ b/test/regress/regress0/uf/euf_simp06.smt
@@ -0,0 +1,11 @@
+(benchmark euf_simp6.smt
+
+  :status unsat
+  :difficulty { unknown }
+  :category { crafted }
+  :logic QF_UF
+  :extrasorts (A)
+  :extrafuns ((x A))
+  :extrafuns ((f A A))
+  :formula (let (?cvc_1 (f x)) (let (?cvc_0 (f ?cvc_1)) (not (implies (and (= ?cvc_0 x) (= (f (f (f ?cvc_0))) x)) (= ?cvc_1 x)))))
+)
diff --git a/test/regress/regress0/uf/euf_simp08.smt b/test/regress/regress0/uf/euf_simp08.smt
new file mode 100644
index 000000000..0a89fe96a
--- /dev/null
+++ b/test/regress/regress0/uf/euf_simp08.smt
@@ -0,0 +1,13 @@
+(benchmark euf_simp8.smt
+
+  :status unsat
+  :difficulty { unknown }
+  :category { crafted }
+  :logic QF_UF
+  :extrasorts (A)
+  :extrafuns ((x A))
+  :extrafuns ((f A A))
+
+  :formula (let (?cvc_1 (f x)) (let (?cvc_0 (f (f ?cvc_1))) (not (implies (and (= ?cvc_0 x) (= (f (f ?cvc_0)) ?cvc_0)) (= ?cvc_1 x)))))
+
+)
diff --git a/test/regress/regress0/uf/euf_simp09.smt b/test/regress/regress0/uf/euf_simp09.smt
new file mode 100644
index 000000000..69ec0fff4
--- /dev/null
+++ b/test/regress/regress0/uf/euf_simp09.smt
@@ -0,0 +1,11 @@
+(benchmark euf_simp9.smt
+
+  :status unsat
+  :difficulty { unknown }
+  :category { crafted }
+  :logic QF_UF
+  :extrasorts (A)
+  :extrafuns ((x A))
+  :extrafuns ((f A A))
+  :formula (let (?cvc_1 (f (f x))) (let (?cvc_0 (f (f ?cvc_1))) (not (implies (and (= ?cvc_0 x) (= (f (f ?cvc_0)) x)) (= ?cvc_1 x)))))
+)
diff --git a/test/regress/regress0/uf/euf_simp10.smt b/test/regress/regress0/uf/euf_simp10.smt
new file mode 100644
index 000000000..1b4b05854
--- /dev/null
+++ b/test/regress/regress0/uf/euf_simp10.smt
@@ -0,0 +1,12 @@
+(benchmark euf_simp10.smt
+
+  :status unsat
+  :difficulty { unknown }
+  :category { crafted }
+  :logic QF_UF
+  :extrasorts (A)
+  :extrafuns ((x A))
+  :extrafuns ((f A A))
+
+  :formula (let (?cvc_0 (f x)) (let (?cvc_1 (f (f ?cvc_0))) (flet ($cvc_2 (= ?cvc_1 ?cvc_0)) (not (implies (and $cvc_2 (= (f (f ?cvc_1)) ?cvc_0)) $cvc_2)))))
+)
diff --git a/test/regress/regress0/uf/euf_simp11.smt b/test/regress/regress0/uf/euf_simp11.smt
new file mode 100644
index 000000000..164bd47e5
--- /dev/null
+++ b/test/regress/regress0/uf/euf_simp11.smt
@@ -0,0 +1,17 @@
+(benchmark euf_simp11.smt
+
+  :status unsat
+  :difficulty { unknown }
+  :category { crafted }
+  :logic QF_UF
+  :extrasorts (A)
+  :extrafuns ((x A))
+  :extrafuns ((f A A))
+
+
+
+
+
+
+  :formula (let (?cvc_0 (f x)) (let (?cvc_2 (f ?cvc_0)) (let (?cvc_1 (f (f ?cvc_2))) (not (implies (and (= ?cvc_1 ?cvc_0) (= (f (f ?cvc_1)) ?cvc_0)) (= ?cvc_2 ?cvc_0))))))
+)
diff --git a/test/regress/regress0/uf/euf_simp12.smt b/test/regress/regress0/uf/euf_simp12.smt
new file mode 100644
index 000000000..aff94fff3
--- /dev/null
+++ b/test/regress/regress0/uf/euf_simp12.smt
@@ -0,0 +1,12 @@
+(benchmark euf_simp12.smt
+
+  :status unsat
+  :category { crafted }
+  :logic QF_UF
+  :extrasorts (A)
+  :extrafuns ((x A))
+  :extrafuns ((f A A))
+
+  :formula (let (?cvc_0 (f (f x))) (let (?cvc_2 (f ?cvc_0)) (let (?cvc_3 (f ?cvc_2)) (let (?cvc_1 (f ?cvc_3)) (let (?cvc_4 (f ?cvc_1)) (not (implies (and (= ?cvc_4 ?cvc_0) (= ?cvc_1 ?cvc_2)) (and (= ?cvc_3 ?cvc_0) (= ?cvc_4 ?cvc_3)))))))))
+
+)
diff --git a/test/regress/regress0/uf/euf_simp13.smt b/test/regress/regress0/uf/euf_simp13.smt
new file mode 100644
index 000000000..7e7abb8f9
--- /dev/null
+++ b/test/regress/regress0/uf/euf_simp13.smt
@@ -0,0 +1,12 @@
+(benchmark euf_simp13.smt
+
+  :status unsat
+  :difficulty { unknown }
+  :category { crafted }
+  :logic QF_UF
+  :extrasorts (A)
+  :extrafuns ((x A))
+  :extrafuns ((f A A))
+  :formula
+  (let (?cvc_6 (f x)) (let (?cvc_0 (f ?cvc_6)) (flet ($cvc_1 (= ?cvc_0 x)) (let (?cvc_2 (f ?cvc_0)) (flet ($cvc_3 (= ?cvc_2 x)) (let (?cvc_4 (f ?cvc_2)) (let (?cvc_5 (f ?cvc_4)) (not (implies (or (or (or (and $cvc_1 $cvc_3) (and $cvc_1 (= ?cvc_5 x))) (and $cvc_3 (= ?cvc_4 ?cvc_2))) (and $cvc_3 (= ?cvc_5 ?cvc_2))) (= ?cvc_6 x))))))))))
+)