diff options
| -rw-r--r-- | src/theory/booleans/theory_bool_rewriter.cpp | 75 | ||||
| -rw-r--r-- | src/util/cardinality.cpp | 4 | ||||
| -rw-r--r-- | src/util/cardinality.h | 5 | ||||
| -rw-r--r-- | test/regress/regress0/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/constant-rewrite.smt | 12 |
5 files changed, 76 insertions, 23 deletions
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index 967126da1..7a4e91035 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -118,29 +118,60 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) { } else if(n[1].getKind() == kind::NOT && n[1][0] == n[0]) { // IFF x (NOT x) return RewriteResponse(REWRITE_DONE, ff); + } else if(n[0].getKind() == kind::EQUAL && n[1].getKind() == kind::EQUAL) { + // a : (= i x) + // i : (= j k) + // x : (= y z) + + // assume wlog k, z are constants and j is the same symbol as y + // (iff (= j k) (= j z)) + // if k = z + // then (iff (= j k) (= j k)) => true + // else + // (iff (= j k) (= j z)) <=> b + // b : (and (not (= j k)) (not (= j z))) + // (= j k) (= j z) | a b + // f f | t t + // f t | f f + // t f | f f + // t t | * f + // * j cannot equal both k and z in a theory model + TNode t,c; + if (n[0][0].isConst()) { + c = n[0][0]; + t = n[0][1]; + } + else if (n[0][1].isConst()) { + c = n[0][1]; + t = n[0][0]; + } + bool matchesForm = false; + bool constantsEqual = false; + if (!c.isNull()) { + if (n[1][0] == t && n[1][1].isConst()) { + matchesForm = true; + constantsEqual = (n[1][1] == c); + } + else if (n[1][1] == t && n[1][0].isConst()) { + matchesForm = true; + constantsEqual = (n[1][1] == c); + } + } + if(matchesForm){ + if(constantsEqual){ + return RewriteResponse(REWRITE_DONE, tt); + }else{ + Cardinality kappa = t.getType().getCardinality(); + Cardinality two(2l); + if(kappa.knownLessThanOrEqual(two)){ + return RewriteResponse(REWRITE_DONE, ff); + }else{ + Node neitherEquality = (n[0].notNode()).andNode(n[1].notNode()); + return RewriteResponse(REWRITE_AGAIN, neitherEquality); + } + } + } } - // This is wrong: it would rewrite c1 == x <=> c2 == x to false - // when this is sat for x = c3 where c3 is different from c1, and c2 - - // else if(n[0].getKind() == kind::EQUAL && n[1].getKind() == kind::EQUAL) { - // TNode t,c; - // if (n[0][0].isConst()) { - // c = n[0][0]; - // t = n[0][1]; - // } - // else if (n[0][1].isConst()) { - // c = n[0][1]; - // t = n[0][0]; - // } - // if (!c.isNull()) { - // if (n[1][0] == t && n[1][1].isConst()) { - // return RewriteResponse(REWRITE_DONE, n[1][1] == c ? tt : ff); - // } - // else if (n[1][1] == t && n[1][0].isConst()) { - // return RewriteResponse(REWRITE_DONE, n[1][0] == c ? tt : ff); - // } - // } - // } break; } case kind::XOR: { diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp index 8abaa5611..36f09f137 100644 --- a/src/util/cardinality.cpp +++ b/src/util/cardinality.cpp @@ -193,6 +193,10 @@ Cardinality::CardinalityComparison Cardinality::compare(const Cardinality& c) co Unreachable(); } +bool Cardinality::knownLessThanOrEqual(const Cardinality& c) const throw() { + CardinalityComparison cmp = this->compare(c); + return cmp == LESS || cmp == EQUAL; +} std::string Cardinality::toString() const throw() { std::stringstream ss; diff --git a/src/util/cardinality.h b/src/util/cardinality.h index c536ea065..c9d051c9e 100644 --- a/src/util/cardinality.h +++ b/src/util/cardinality.h @@ -245,6 +245,11 @@ public: */ std::string toString() const throw(); + /** + * Compare two cardinalities and if it is known that the current + * cardinality is smaller or equal to c, it returns true. + */ + bool knownLessThanOrEqual(const Cardinality& c) const throw(); };/* class Cardinality */ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 48ac97294..b1e2f6491 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -37,7 +37,8 @@ SMT_TESTS = \ simple2.smt \ simple-lra.smt \ simple-rdl.smt \ - simple-uf.smt + simple-uf.smt \ + constant-rewrite.smt # Regression tests for SMT2 inputs SMT2_TESTS = \ diff --git a/test/regress/regress0/constant-rewrite.smt b/test/regress/regress0/constant-rewrite.smt new file mode 100644 index 000000000..b70b53bec --- /dev/null +++ b/test/regress/regress0/constant-rewrite.smt @@ -0,0 +1,12 @@ +(benchmark ConstantRewrite +:logic QF_LRA +:status sat +:extrafuns ((v0 Real)) +:formula +(and + (not (<= v0 0)) + (not (iff (= v0 0) + (= v0 (/ 1 2)))) + ) +) + |