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

diff --git a/src/theory/theoryof_table_middle.h b/src/theory/theoryof_table_middle.h
index f3ad433a3af96101d5c9ec6bdb7b5aece3aa0dc9..a0586d0ce93aa3fa5ac6801ef364e91c06d476fc 100644 (file)
--- 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 3753bd78a83cd2e0def172140626178c8c4536d0..128e28ca2059278b9394ebef140adf555bbfdc74 100644 (file)
--- 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 a4e08ff994639c2a7c274797b4aebdd6874c79ba..b456f2809f33f7eac2a8ee92d397e65f78362e96 100644 (file)
--- 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 (file)
index 0000000..c121ae8
--- /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 (file)
index 0000000..9c7b03f
--- /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 (file)
index 0000000..e0d6cc8
--- /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 (file)
index 0000000..7b15ad3
--- /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 (file)
index 0000000..85089a9
--- /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 (file)
index 0000000..020bafd
--- /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 (file)
index 0000000..0a89fe9
--- /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 (file)
index 0000000..69ec0ff
--- /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 (file)
index 0000000..1b4b058
--- /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 (file)
index 0000000..164bd47
--- /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 (file)
index 0000000..aff94ff
--- /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 (file)
index 0000000..7e7abb8
--- /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))))))))))
+)