From 82f4d5bd67f70a561b0f6357f6d6b80c2fcd7b64 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 21 Apr 2015 16:34:56 +0200 Subject: [PATCH] Fix bug in fmf mbqi=fmc with arrays. Add two datatypes regressions. --- src/theory/quantifiers/full_model_check.cpp | 2 + test/regress/regress0/datatypes/Makefile.am | 4 +- test/regress/regress0/datatypes/bug625.smt2 | 13 ++++ .../regress0/datatypes/manos-model.smt2 | 67 +++++++++++++++++++ 4 files changed, 85 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/datatypes/bug625.smt2 create mode 100644 test/regress/regress0/datatypes/manos-model.smt2 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) + -- 2.30.2