From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Thu, 14 Jun 2012 01:08:11 +0000 (+0000)
Subject: * removing rewriteEquality from the rewriter
X-Git-Tag: cvc5-1.0.0~8028
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dd713fdbc16b07adc8011dea09b53fb3bc168662;p=cvc5.git

* removing rewriteEquality from the rewriter
* theories now get either an assertion from the SAT solver (normalized) or an (dis-)equality between two shared terms that is non-normalized
---

diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 748ed8686..c32cc0e56 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -34,10 +34,6 @@ public:
 
   static RewriteResponse preRewrite(TNode n);
   static RewriteResponse postRewrite(TNode n);
-  static Node rewriteEquality(TNode equality) {
-    // Arithmetic owns the domain, so this is totally ok
-    return Rewriter::rewrite(equality);
-  }
 
   static void init() { }
 
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 1bf42a105..25797dda3 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -271,16 +271,14 @@ class TheoryArrays : public Theory {
           }
         }
         // Propagate equality between shared terms
-        Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2));
-        return d_arrays.propagate(equality);
+        return d_arrays.propagate(t1.eqNode(t2));
       } else {
         if (t1.getType().isArray()) {
           if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) {
             return true;
           }
         }
-        Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2));
-        return d_arrays.propagate(equality.notNode());
+        return d_arrays.propagate(t1.eqNode(t2).notNode());
       }
       return true;
     }
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index 627f34a30..c6ef5cd25 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -109,10 +109,6 @@ public:
     return RewriteResponse(REWRITE_DONE, node);
   }
 
-  static Node rewriteEquality(TNode node) {
-    return postRewrite(node).node;
-  }
-
   static inline void init() {}
   static inline void shutdown() {}
 
diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h
index d26a4d478..6771f775c 100644
--- a/src/theory/booleans/theory_bool_rewriter.h
+++ b/src/theory/booleans/theory_bool_rewriter.h
@@ -37,11 +37,6 @@ public:
     return preRewrite(node);
   }
 
-  static Node rewriteEquality(TNode node) {
-    Unreachable();
-    return node;
-  }
-
   static void init() {}
   static void shutdown() {}
 
diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h
index e299f84e7..acf535388 100644
--- a/src/theory/builtin/theory_builtin_rewriter.h
+++ b/src/theory/builtin/theory_builtin_rewriter.h
@@ -48,11 +48,6 @@ public:
     }
   }
 
-  static inline Node rewriteEquality(TNode equality) {
-    Unreachable();
-    return equality;
-  }
-
   static inline void init() {}
   static inline void shutdown() {}
 
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index 5bb906841..a9c6d2676 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -94,17 +94,15 @@ void Bitblaster::bbAtom(TNode node) {
   BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; 
   ++d_statistics.d_numAtoms;
   // the bitblasted definition of the atom
-  Node atom_bb = d_atomBBStrategies[node.getKind()](node, this);
+  Node atom_bb = Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this));
   // asserting that the atom is true iff the definition holds
   Node atom_definition = mkNode(kind::IFF, node, atom_bb);
-  // do boolean simplifications if possible
-  Node rewritten = Rewriter::rewrite(atom_definition);
 
   if (!Options::current()->bitvectorEagerBitblast) {
-    d_cnfStream->convertAndAssert(rewritten, true, false);
+    d_cnfStream->convertAndAssert(atom_definition, true, false);
     d_bitblastedAtoms.insert(node);
   } else {
-    d_bvOutput->lemma(rewritten, false);
+    d_bvOutput->lemma(atom_definition, false);
   }
 }
 
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index bfd8a2897..6b885f1ed 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -84,11 +84,6 @@ public:
 
   static RewriteResponse preRewrite(TNode node);
 
-  static Node rewriteEquality(TNode node) {
-    Debug("bitvector") << "TheoryBV::rewriteEquality(" << node << ")" << std::endl;
-    return postRewrite(node).node;
-  }
-
   static void init();
   static void shutdown();
   
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 124e6870d..ea1409108 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -108,10 +108,6 @@ public:
     return RewriteResponse(REWRITE_DONE, in);
   }
 
-  static Node rewriteEquality(TNode equality) {
-    return postRewrite(equality).node;
-  }
-
   static inline void init() {}
   static inline void shutdown() {}
 
diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter
index 780409d52..71a8ea097 100755
--- a/src/theory/mkrewriter
+++ b/src/theory/mkrewriter
@@ -47,8 +47,6 @@ post_rewrite_calls=
 post_rewrite_get_cache=
 post_rewrite_set_cache=
 
-rewrite_equality_calls=
-
 seen_theory=false
 seen_theory_builtin=false
 
@@ -140,9 +138,6 @@ function rewriter {
   post_rewrite_set_cache="${post_rewrite_set_cache}    case ${theory_id}: return RewriteAttibute<${theory_id}>::setPostRewriteCache(node, cache);
 "
 
-  rewrite_equality_calls="${rewrite_equality_calls}    case ${theory_id}: return ${class}::rewriteEquality(node);
-"
-
   lineno=${BASH_LINENO[0]}
   check_theory_seen
 }
@@ -235,7 +230,6 @@ for var in \
     rewriter_includes \
     pre_rewrite_calls \
     post_rewrite_calls \
-    rewrite_equality_calls \
     pre_rewrite_get_cache \
     post_rewrite_get_cache \
     pre_rewrite_set_cache \
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 8c037d30b..4f51edab8 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -65,9 +65,6 @@ private:
 public:
   static RewriteResponse preRewrite(TNode in);
   static RewriteResponse postRewrite(TNode in);
-  static Node rewriteEquality(TNode equality) {
-    return postRewrite(equality).node;
-  }
   static inline void init() {}
   static inline void shutdown() {}
 private:
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index e0b1458fb..8c20c84c1 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -64,15 +64,6 @@ Node Rewriter::rewrite(TNode node) {
   return rewriteTo(theory::Theory::theoryOf(node), node);
 }
 
-Node Rewriter::rewriteEquality(theory::TheoryId theoryId, TNode node) {
-  Assert(node.getKind() == kind::EQUAL);
-  Trace("rewriter") << "Rewriter::rewriteEquality(" << theoryId << "," << node << ")"<< std::endl;
-  Node result = Rewriter::callRewriteEquality(theoryId, node);
-  Trace("rewriter") << "Rewriter::rewriteEquality(" << theoryId << "," << node << ") => " << result << std::endl;
-  Assert(result.getKind() == kind::EQUAL || result.isConst());
-  return result;
-}
-
 Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
 
 #ifdef CVC4_ASSERTIONS
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index e80606c95..4169cb9fe 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -98,12 +98,6 @@ public:
    */
   static Node rewrite(TNode node);
 
-  /**
-   * Rewrite an equality between two terms that are already in normal form, so
-   * that the equality is in theory-normal form.
-   */
-  static Node rewriteEquality(theory::TheoryId theoryId, TNode node);
-
   /**
    * Should be called before the rewriter gets used for the first time.
    */
@@ -113,6 +107,8 @@ public:
    * Should be called to clean up any state.
    */
   static void shutdown();
+
+
 };/* class Rewriter */
 
 }/* CVC4::theory namespace */
diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h
index cd79dcd9f..9ab98168e 100644
--- a/src/theory/rewriter_tables_template.h
+++ b/src/theory/rewriter_tables_template.h
@@ -45,14 +45,6 @@ ${post_rewrite_calls}
   }
 }
 
-Node Rewriter::callRewriteEquality(theory::TheoryId theoryId, TNode node) {
-  switch(theoryId) {
-${rewrite_equality_calls}
-  default:
-    Unreachable();
-  }
-}
-
 Node Rewriter::getPreRewriteCache(theory::TheoryId theoryId, TNode node) {
   switch(theoryId) {
 ${pre_rewrite_get_cache}
diff --git a/src/theory/rewriterules/theory_rewriterules_rewriter.h b/src/theory/rewriterules/theory_rewriterules_rewriter.h
index d9da095f7..3d01dc2a5 100644
--- a/src/theory/rewriterules/theory_rewriterules_rewriter.h
+++ b/src/theory/rewriterules/theory_rewriterules_rewriter.h
@@ -56,14 +56,6 @@ public:
     return RewriteResponse(REWRITE_DONE, node);
   }
 
-  /**
-   * Rewrite an equality, in case special handling is required.
-   */
-  static Node rewriteEquality(TNode equality) {
-    // often this will suffice
-    return postRewrite(equality).node;
-  }
-
   /**
    * Initialize the rewriter.
    */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 8abc7a0e3..060d48230 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -394,7 +394,9 @@ void TheoryEngine::combineTheories() {
     Assert(!d_sharedTerms.areDisequal(carePair.a, carePair.b), "Please don't care about stuff you were notified about");
 
     // The equality in question
-    Node equality = Rewriter::rewriteEquality(carePair.theory, carePair.a.eqNode(carePair.b));
+    Node equality = carePair.a < carePair.b ?
+        carePair.a.eqNode(carePair.b) :
+        carePair.b.eqNode(carePair.a);
 
     // Normalize the equality
     Node normalizedEquality = Rewriter::rewrite(equality);
@@ -862,33 +864,41 @@ void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId,
     }
     return;
   }
-  
-  // We are left with internal distribution of shared literals
-  Assert(atom.getKind() == kind::EQUAL);
-  Node normalizedAtom = Rewriter::rewriteEquality(toTheoryId, atom);
-  Node normalizedAssertion = polarity ? normalizedAtom : normalizedAtom.notNode();
-  
-  // If we normalize to true or false, it's a special case
-  if (normalizedAtom.isConst()) {
-    if (polarity == normalizedAtom.getConst<bool>()) {
-      // Trivially true, just ignore
-      return;
+
+  // See if it rewrites to true or false directly
+  Node normalizedLiteral = Rewriter::rewrite(assertion);
+  if (normalizedLiteral.isConst()) {
+    if (normalizedLiteral.getConst<bool>()) {
+      // trivially true, but theories need to share even trivially true facts
+      // unless of course it is the theory that normalized it
+      if (Theory::theoryOf(atom) == toTheoryId) {
+      	return;
+      }
     } else {
       // Mark the propagation for explanations
-      if (markPropagation(normalizedAssertion, assertion, toTheoryId, fromTheoryId)) {
+      if (markPropagation(normalizedLiteral, assertion, toTheoryId, fromTheoryId)) {
         // Get the explanation (conflict will figure out where it came from)
-        conflict(normalizedAssertion, toTheoryId);
+        conflict(normalizedLiteral, toTheoryId);
       } else {
         Unreachable();
       }
       return;
     }
   }
-  
-  // Try and assert
+
+  // Normalize to lhs < rhs
+  Assert(atom.getKind() == kind::EQUAL);
+  Assert(atom[0] != atom[1]);
+  Node normalizedAtom = atom;
+  if (atom[0] > atom[1]) {
+    normalizedAtom = atom[1].eqNode(atom[0]);
+  }
+  Node normalizedAssertion = polarity ? normalizedAtom : normalizedAtom.notNode();
+
+  // Try and assert (note that we assert the non-normalized one)
   if (markPropagation(normalizedAssertion, assertion, toTheoryId, fromTheoryId)) {
     // Check if has been pre-registered with the theory
-    bool preregistered = d_propEngine->isSatLiteral(normalizedAssertion) && Theory::theoryOf(normalizedAtom) == toTheoryId;
+    bool preregistered = d_propEngine->isSatLiteral(normalizedAssertion) && Theory::theoryOf(normalizedAssertion) == toTheoryId;
     // Assert away
     theoryOf(toTheoryId)->assertFact(normalizedAssertion, preregistered);
     d_factsAsserted = true;
@@ -1139,9 +1149,8 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
     Assert(properConflict(fullConflict));
     lemma(fullConflict, true, true);
   } else {
-    Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "):" << std::endl;
-
     // When only one theory, the conflict should need no processing
+    Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << ")" << std::endl;
     Assert(properConflict(conflict));
     lemma(conflict, true, true);
   }
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index be4906ab6..8ba39f372 100644
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -54,10 +54,6 @@ public:
     return RewriteResponse(REWRITE_DONE, node);
   }
 
-  static Node rewriteEquality(TNode equality) {
-    return postRewrite(equality).node;
-  }
-
   static inline void init() {}
   static inline void shutdown() {}
 
diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am
index 263795814..efffc7afd 100644
--- a/test/regress/regress0/aufbv/Makefile.am
+++ b/test/regress/regress0/aufbv/Makefile.am
@@ -14,6 +14,7 @@ TESTS =	\
 	bug00.smt \
 	bug338.smt2 \
 	bug347.smt \
+	bug348.smt \
 	try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt \
 	diseqprop.01.smt \
 	wchains010ue.delta01.smt \
diff --git a/test/regress/regress0/aufbv/bug348.smt b/test/regress/regress0/aufbv/bug348.smt
new file mode 100644
index 000000000..46172eba9
--- /dev/null
+++ b/test/regress/regress0/aufbv/bug348.smt
@@ -0,0 +1,133 @@
+(benchmark B_
+:logic QF_AUFBV
+:extrafuns ((start2 BitVec[32]))
+:extrafuns ((start1 BitVec[32]))
+:extrafuns ((a1 Array[32:8]))
+:status unsat
+:formula
+(let (?n1 bv0[1])
+(let (?n2 bv0[8])
+(let (?n3 (store a1 start1 ?n2))
+(let (?n4 bv3[32])
+(let (?n5 (bvadd ?n4 start1))
+(let (?n6 (store ?n3 ?n5 ?n2))
+(let (?n7 bv0[32])
+(let (?n8 (select ?n6 ?n7))
+(let (?n9 (bvnot ?n8))
+(let (?n10 (select ?n6 ?n7))
+(let (?n11 (bvnot ?n10))
+(let (?n12 (bvand ?n9 ?n11))
+(let (?n13 (bvnot ?n12))
+(let (?n14 (bvand ?n8 ?n10))
+(let (?n15 (bvnot ?n14))
+(let (?n16 (bvand ?n13 ?n15))
+(let (?n17 (bvnot ?n16))
+(let (?n18 (bvand ?n9 ?n17))
+(let (?n19 (bvnot ?n18))
+(let (?n20 (bvand ?n8 ?n16))
+(let (?n21 (bvnot ?n20))
+(let (?n22 (bvand ?n19 ?n21))
+(let (?n23 (store ?n6 ?n7 ?n22))
+(let (?n24 (bvnot ?n22))
+(let (?n25 (bvand ?n17 ?n24))
+(let (?n26 (bvnot ?n25))
+(let (?n27 (bvand ?n16 ?n22))
+(let (?n28 (bvnot ?n27))
+(let (?n29 (bvand ?n26 ?n28))
+(let (?n30 (store ?n23 ?n7 ?n29))
+(let (?n31 (bvadd ?n4 start2))
+(let (?n32 (select ?n30 ?n31))
+(let (?n33 (bvnot ?n32))
+(let (?n34 (select ?n30 start2))
+(let (?n35 (bvnot ?n34))
+(let (?n36 (bvand ?n33 ?n35))
+(let (?n37 (bvnot ?n36))
+(let (?n38 (bvand ?n32 ?n34))
+(let (?n39 (bvnot ?n38))
+(let (?n40 (bvand ?n37 ?n39))
+(let (?n41 (bvnot ?n40))
+(let (?n42 (bvand ?n33 ?n41))
+(let (?n43 (bvnot ?n42))
+(let (?n44 (bvand ?n32 ?n40))
+(let (?n45 (bvnot ?n44))
+(let (?n46 (bvand ?n43 ?n45))
+(let (?n47 (store ?n30 ?n31 ?n46))
+(let (?n48 (bvnot ?n46))
+(let (?n49 (bvand ?n41 ?n48))
+(let (?n50 (bvnot ?n49))
+(let (?n51 (bvand ?n40 ?n46))
+(let (?n52 (bvnot ?n51))
+(let (?n53 (bvand ?n50 ?n52))
+(let (?n54 (store ?n47 start2 ?n53))
+(let (?n55 (select ?n54 ?n7))
+(let (?n56 (bvnot ?n55))
+(let (?n57 (select ?n54 start2))
+(let (?n58 (bvnot ?n57))
+(let (?n59 (bvand ?n56 ?n58))
+(let (?n60 (bvnot ?n59))
+(let (?n61 (bvand ?n55 ?n57))
+(let (?n62 (bvnot ?n61))
+(let (?n63 (bvand ?n60 ?n62))
+(let (?n64 (bvnot ?n63))
+(let (?n65 (bvand ?n56 ?n64))
+(let (?n66 (bvnot ?n65))
+(let (?n67 (bvand ?n55 ?n63))
+(let (?n68 (bvnot ?n67))
+(let (?n69 (bvand ?n66 ?n68))
+(let (?n70 (store ?n54 ?n7 ?n69))
+(let (?n71 (bvnot ?n69))
+(let (?n72 (bvand ?n64 ?n71))
+(let (?n73 (bvnot ?n72))
+(let (?n74 (bvand ?n63 ?n69))
+(let (?n75 (bvnot ?n74))
+(let (?n76 (bvand ?n73 ?n75))
+(let (?n77 (store ?n70 start2 ?n76))
+(let (?n78 (select ?n77 ?n7))
+(let (?n79 (bvnot ?n78))
+(let (?n80 (select ?n77 ?n7))
+(let (?n81 (bvnot ?n80))
+(let (?n82 (bvand ?n79 ?n81))
+(let (?n83 (bvnot ?n82))
+(let (?n84 (bvand ?n78 ?n80))
+(let (?n85 (bvnot ?n84))
+(let (?n86 (bvand ?n83 ?n85))
+(let (?n87 (bvnot ?n86))
+(let (?n88 (bvand ?n79 ?n87))
+(let (?n89 (bvnot ?n88))
+(let (?n90 (bvand ?n78 ?n86))
+(let (?n91 (bvnot ?n90))
+(let (?n92 (bvand ?n89 ?n91))
+(let (?n93 (store ?n77 ?n7 ?n92))
+(let (?n94 (bvnot ?n92))
+(let (?n95 (bvand ?n87 ?n94))
+(let (?n96 (bvnot ?n95))
+(let (?n97 (bvand ?n86 ?n92))
+(let (?n98 (bvnot ?n97))
+(let (?n99 (bvand ?n96 ?n98))
+(let (?n100 (store ?n93 ?n7 ?n99))
+(let (?n101 (store a1 ?n5 ?n2))
+(let (?n102 (store ?n101 start1 ?n2))
+(let (?n103 (select ?n102 ?n7))
+(let (?n104 (store ?n102 ?n7 ?n103))
+(let (?n105 (select ?n102 ?n7))
+(let (?n106 (store ?n104 ?n7 ?n105))
+(let (?n107 (select ?n106 start2))
+(let (?n108 (store ?n106 ?n31 ?n107))
+(let (?n109 (select ?n106 ?n31))
+(let (?n110 (store ?n108 start2 ?n109))
+(let (?n111 (select ?n110 start2))
+(let (?n112 (store ?n110 ?n7 ?n111))
+(let (?n113 (select ?n110 ?n7))
+(let (?n114 (store ?n112 start2 ?n113))
+(let (?n115 (select ?n114 ?n7))
+(let (?n116 (store ?n114 ?n7 ?n115))
+(let (?n117 (select ?n114 ?n7))
+(let (?n118 (store ?n116 ?n7 ?n117))
+(flet ($n119 (= ?n100 ?n118))
+(let (?n120 bv1[1])
+(let (?n121 (ite $n119 ?n120 ?n1))
+(let (?n122 (bvnot ?n121))
+(flet ($n123 (= ?n1 ?n122))
+(flet ($n124 (not $n123))
+$n124
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))