diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-06 19:46:34 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-06 19:46:34 -0400 |
commit | 8d29fef7286ab07c630c65284bfb399e2f7f5326 (patch) | |
tree | 23d70ebf1ef248df304aa23ecb044cd84cbbebc8 | |
parent | ab83b7f8d4cc25580cf140d753e0bfe3c76cb36c (diff) | |
parent | 8227a1fac2ce875dfed79c4b6cc8499158e4d7d1 (diff) |
Merge branch 'master' of https://github.com/CVC4/CVC4
-rw-r--r-- | src/theory/unconstrained_simplifier.cpp | 35 | ||||
-rw-r--r-- | test/regress/regress0/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/ite5.smt2 | 8 | ||||
-rw-r--r-- | test/regress/regress0/unconstrained/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/unconstrained/ite.smt2 | 9 |
5 files changed, 38 insertions, 16 deletions
diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp index a6e885f97..115788639 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/theory/unconstrained_simplifier.cpp @@ -163,23 +163,26 @@ void UnconstrainedSimplifier::processUnconstrained() currentSub = Node(); } } - else if (uCond && parent.getType().getCardinality().isFinite() && parent.getType().getCardinality().getFiniteCardinality() == 2) { - // Special case: condition is unconstrained, then and else are different, and total cardinality of the type is 2, then the result - // is unconstrained - Node test; - if (parent.getType().isBoolean()) { - test = Rewriter::rewrite(parent[1].iffNode(parent[2])); - } - else { - test = Rewriter::rewrite(parent[1].eqNode(parent[2])); - } - if (test == NodeManager::currentNM()->mkConst<bool>(false)) { - ++d_numUnconstrainedElim; - if (currentSub.isNull()) { - currentSub = current; + else if (uCond) { + Cardinality card = parent.getType().getCardinality(); + if (card.isFinite() && !card.isLargeFinite() && card.getFiniteCardinality() == 2) { + // Special case: condition is unconstrained, then and else are different, and total cardinality of the type is 2, then the result + // is unconstrained + Node test; + if (parent.getType().isBoolean()) { + test = Rewriter::rewrite(parent[1].iffNode(parent[2])); + } + else { + test = Rewriter::rewrite(parent[1].eqNode(parent[2])); + } + if (test == NodeManager::currentNM()->mkConst<bool>(false)) { + ++d_numUnconstrainedElim; + if (currentSub.isNull()) { + currentSub = current; + } + currentSub = newUnconstrainedVar(parent.getType(), currentSub); + current = parent; } - currentSub = newUnconstrainedVar(parent.getType(), currentSub); - current = parent; } } break; diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 5df8577af..f16e18bdf 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -53,6 +53,7 @@ SMT2_TESTS = \ ite2.smt2 \ ite3.smt2 \ ite4.smt2 \ + ite5.smt2 \ simple-lra.smt2 \ simple-rdl.smt2 \ simple-uf.smt2 \ diff --git a/test/regress/regress0/ite5.smt2 b/test/regress/regress0/ite5.smt2 new file mode 100644 index 000000000..e3d2bc9b8 --- /dev/null +++ b/test/regress/regress0/ite5.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_AUFBV ) +(set-info :status sat) +(declare-fun arr0 () (Array (_ BitVec 32) (_ BitVec 8) ) ) +(declare-fun arr1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) +(declare-fun arr2 () (Array (_ BitVec 32) (_ BitVec 8) ) ) +(assert (bvult (ite (bvult (_ bv0 1) ((_ extract 0 0) (select arr1 (_ bv0 32)))) (concat (select arr0 (_ bv7 32)) (select arr0 (_ bv6 32)) (select arr0 (_ bv5 32)) (select arr0 (_ bv4 32)) (select arr0 (_ bv3 32)) (select arr0 (_ bv2 32)) (select arr0 (_ bv1 32)) (select arr0 (_ bv0 32))) (concat (_ bv0 57) ((_ extract 7 1) (select arr2 (_ bv0 32))))) (_ bv1 64) )) +(check-sat) +(exit) diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am index fcae3196a..dcc44d43a 100644 --- a/test/regress/regress0/unconstrained/Makefile.am +++ b/test/regress/regress0/unconstrained/Makefile.am @@ -65,6 +65,7 @@ TESTS = \ bvult.smt2 \ geq.smt2 \ gt.smt2 \ + ite.smt2 \ leq.smt2 \ lt.smt2 \ uf1.smt2 \ diff --git a/test/regress/regress0/unconstrained/ite.smt2 b/test/regress/regress0/unconstrained/ite.smt2 new file mode 100644 index 000000000..4dc1cc295 --- /dev/null +++ b/test/regress/regress0/unconstrained/ite.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_AUFBV ) +(set-info :status sat) +(declare-sort U 0) +(declare-fun a () (Array U (_ BitVec 64) ) ) +(declare-fun i () U) +(declare-fun p () Bool) +(assert (= (_ bv0 64) (ite p (select a i) (_ bv1 64)))) +(check-sat) +(exit) |