From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 21 Apr 2015 14:34:56 +0000 (+0200)
Subject: Fix bug in fmf mbqi=fmc with arrays. Add two datatypes regressions.
X-Git-Tag: cvc5-1.0.0~6349
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=82f4d5bd67f70a561b0f6357f6d6b80c2fcd7b64;p=cvc5.git

Fix bug in fmf mbqi=fmc with arrays. Add two datatypes regressions.
---

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 3148901da..5be263254 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -903,6 +903,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
       Trace("fmc-debug") << "Do uninterpreted compose " << n << std::endl;
       //uninterpreted compose
       doUninterpretedCompose( fm, f, d, n.getOperator(), children );
+      /*
     } else if( n.getKind()==SELECT ){
       Trace("fmc-debug") << "Do select compose " << n << std::endl;
       std::vector< Def > children2;
@@ -911,6 +912,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
       mkCondDefaultVec(fm, f, cond);
       std::vector< Node > val;
       doUninterpretedCompose(fm, f, d, children[0], children2, 0, cond, val );
+      */
     } else {
       if( !var_ch.empty() ){
         if( n.getKind()==EQUAL ){
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index b323a2732..45060dbd3 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -63,7 +63,9 @@ TESTS =	\
 	tenum-bug.smt2 \
 	cdt-non-canon-stream.smt2 \
 	stream-singleton.smt2 \
-	is_test.smt2
+	is_test.smt2 \
+	manos-model.smt2 \
+	bug625.smt2
 
 FAILING_TESTS = \
 	datatype-dump.cvc
diff --git a/test/regress/regress0/datatypes/bug625.smt2 b/test/regress/regress0/datatypes/bug625.smt2
new file mode 100644
index 000000000..3f4312ad4
--- /dev/null
+++ b/test/regress/regress0/datatypes/bug625.smt2
@@ -0,0 +1,13 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-fun x1 () Int)
+(declare-fun x2 () Int)
+(declare-fun y1 () Int)
+(declare-fun y2 () Int)
+(declare-datatypes () ( (type
+    (constructor1 (f1 Int))
+    (constructor2 (f2 Int))
+)))
+(define-fun mktest ((constructor Int) (p1 Int) (p2 Int)) type (ite (= constructor 1) (constructor1 p1) (constructor2 p2)))
+(assert (distinct (mktest x1 x2 x2) (mktest y1 y2 y2)))
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/datatypes/manos-model.smt2 b/test/regress/regress0/datatypes/manos-model.smt2
new file mode 100644
index 000000000..4ade71151
--- /dev/null
+++ b/test/regress/regress0/datatypes/manos-model.smt2
@@ -0,0 +1,67 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-datatypes () ( (tuple2!879 (tuple2!879!880 (_1!881 Int) (_2!882 Int))) ))
+
+(declare-fun p1!207 () tuple2!879)
+
+(declare-fun p2!208 () tuple2!879)
+
+(declare-fun p3!209 () tuple2!879)
+
+(declare-fun reduce!206 (tuple2!879 tuple2!879) tuple2!879)
+
+(assert (not (= 
+    (reduce!206 p1!207 (reduce!206 p2!208 p3!209)) 
+    (reduce!206 (reduce!206 p1!207 p2!208) p3!209)
+)))
+
+(assert (= 
+    (reduce!206 p1!207 (reduce!206 p2!208 p3!209)) 
+    (ite 
+        (>= (_1!881 p1!207) (_2!882 (reduce!206 p2!208 p3!209))) 
+        (tuple2!879!880 
+            (+ (- (_1!881 p1!207) (_2!882 (reduce!206 p2!208 p3!209))) (_1!881 (reduce!206 p2!208 p3!209))) 
+            (_2!882 p1!207)
+        )
+        (tuple2!879!880 
+            (_1!881 (reduce!206 p2!208 p3!209)) 
+            (+ (- (_2!882 (reduce!206 p2!208 p3!209)) (_1!881 p1!207)) (_2!882 p1!207))
+        )
+    )
+))
+
+(assert (= 
+    (reduce!206 p2!208 p3!209) 
+    (ite 
+        (>= (_1!881 p2!208) (_2!882 p3!209))
+        (tuple2!879!880 (+ (- (_1!881 p2!208) (_2!882 p3!209)) (_1!881 p3!209)) (_2!882 p2!208))
+        (tuple2!879!880 (_1!881 p3!209) (+ (- (_2!882 p3!209) (_1!881 p2!208)) (_2!882 p2!208)))
+    )
+))
+
+(assert (= 
+    (reduce!206 (reduce!206 p1!207 p2!208) p3!209) 
+    (ite 
+        (>= (_1!881 (reduce!206 p1!207 p2!208)) (_2!882 p3!209)) 
+        (tuple2!879!880 
+            (+ (- (_1!881 (reduce!206 p1!207 p2!208)) (_2!882 p3!209)) (_1!881 p3!209)) 
+            (_2!882 (reduce!206 p1!207 p2!208))
+        ) 
+        (tuple2!879!880 
+            (_1!881 p3!209) 
+            (+ (- (_2!882 p3!209) (_1!881 (reduce!206 p1!207 p2!208))) (_2!882 (reduce!206 p1!207 p2!208)))
+        )
+    )
+))
+
+(assert (= 
+    (reduce!206 p1!207 p2!208) 
+    (ite 
+        (>= (_1!881 p1!207) (_2!882 p2!208)) 
+        (tuple2!879!880 (+ (- (_1!881 p1!207) (_2!882 p2!208)) (_1!881 p2!208)) (_2!882 p1!207)) 
+        (tuple2!879!880 (_1!881 p2!208) (+ (- (_2!882 p2!208) (_1!881 p1!207)) (_2!882 p1!207)))
+    )
+))
+
+(check-sat)
+