added support for division by zero for bit-vector division operators

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6079f146eeeb033cc052b522d6e7ad118d417347..1fc32917e207bd0ebba70275feabc35c3fb3036d 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -41,6 +41,7 @@
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/theory_engine.h"
+#include "theory/bv/theory_bv_rewrite_rules.h"
 #include "proof/proof_manager.h"
 #include "util/proof.h"
 #include "util/boolean_simplification.h"
@@ -226,6 +227,14 @@ class SmtEnginePrivate : public NodeManagerListener {
    */
   Node d_divByZero;
 
+  /** 
+   * Maps from bit-vector width to divison-by-zero uninterpreted
+   * function symbols.  
+   */
+  hash_map<unsigned, Node> d_BVDivByZero;
+  hash_map<unsigned, Node> d_BVRemByZero;
+  
+
   /**
    * Function symbol used to implement uninterpreted
    * int-division-by-zero semantics.  Needed to deal with partial
@@ -400,6 +409,23 @@ public:
   void addFormula(TNode n)
     throw(TypeCheckingException, LogicException);
 
+  /** 
+   * Return the uinterpreted function symbol corresponding to division-by-zero
+   * for this particular bit-wdith 
+   * @param k should be UREM or UDIV
+   * @param width 
+   * 
+   * @return 
+   */
+  Node getBVDivByZero(Kind k, unsigned width);
+  /** 
+   * Returns the node modeling the division-by-zero semantics of node n. 
+   * 
+   * @param n 
+   * 
+   * @return 
+   */
+  Node expandBVDivByZero(TNode n);
   /**
    * Expand definitions in n.
    */
@@ -691,8 +717,8 @@ void SmtEngine::setLogicInternal() throw() {
   d_logic.lock();
 
   // may need to force uninterpreted functions to be on for non-linear
-  if(d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
-     !d_logic.isLinear() &&
+  if(((d_logic.isTheoryEnabled(theory::THEORY_ARITH) && !d_logic.isLinear()) ||
+       d_logic.isTheoryEnabled(theory::THEORY_BV)) &&
      !d_logic.isTheoryEnabled(theory::THEORY_UF)){
     d_logic = d_logic.getUnlockedCopy();
     d_logic.enableTheory(theory::THEORY_UF);
@@ -1101,6 +1127,53 @@ void SmtEngine::defineFunction(Expr func,
   d_definedFunctions->insert(funcNode, def);
 }
 
+
+Node SmtEnginePrivate::getBVDivByZero(Kind k, unsigned width) {
+  NodeManager* nm = d_smt.d_nodeManager; 
+  if (k == kind::BITVECTOR_UDIV) {
+    if (d_BVDivByZero.find(width) == d_BVDivByZero.end()) {
+      // lazily create the function symbols
+      std::ostringstream os;
+      os << "BVUDivByZero_" << width; 
+      Node divByZero = nm->mkSkolem(os.str(),
+                                    nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
+                                    "partial bvudiv", NodeManager::SKOLEM_EXACT_NAME);
+      d_BVDivByZero[width] = divByZero; 
+    }
+    return d_BVDivByZero[width]; 
+  }
+  else if (k == kind::BITVECTOR_UREM) {
+    if (d_BVRemByZero.find(width) == d_BVRemByZero.end()) {
+      std::ostringstream os;
+      os << "BVURemByZero_" << width; 
+      Node divByZero = nm->mkSkolem(os.str(),
+                                    nm->mkFunctionType(nm->mkBitVectorType(width), nm->mkBitVectorType(width)),
+                                    "partial bvurem", NodeManager::SKOLEM_EXACT_NAME);
+      d_BVRemByZero[width] = divByZero;
+    }
+    return d_BVRemByZero[width]; 
+  } 
+
+  Unreachable(); 
+}
+
+
+Node SmtEnginePrivate::expandBVDivByZero(TNode n) {
+  // we only deal wioth the unsigned division operators as the signed ones should have been
+  // expanded in terms of the unsigned operators
+  NodeManager* nm = d_smt.d_nodeManager;
+  unsigned width = n.getType().getBitVectorSize(); 
+  Node divByZero = getBVDivByZero(n.getKind(), width);
+  TNode num = n[0], den = n[1];
+  Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(BitVector(width, Integer(0)))); 
+  Node divByZeroNum = nm->mkNode(kind::APPLY_UF, divByZero, num);
+  Node divTotalNumDen = nm->mkNode(n.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL :
+                                   kind::BITVECTOR_UREM_TOTAL, num, den);
+  Node node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen); 
+  return node; 
+}
+
+
 Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache)
   throw(TypeCheckingException, LogicException) {
 
@@ -1120,10 +1193,26 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
 
   // otherwise expand it
 
-  Node node;
+  Node node = n;
   NodeManager* nm = d_smt.d_nodeManager;
 
   switch(k) {
+  case kind::BITVECTOR_SDIV:
+  case kind::BITVECTOR_SREM:
+  case kind::BITVECTOR_SMOD: {
+    node = bv::LinearRewriteStrategy <
+      bv::RewriteRule<bv::SremEliminate>,
+      bv::RewriteRule<bv::SdivEliminate>,
+      bv::RewriteRule<bv::SmodEliminate>
+      >::apply(node);
+    break;
+  }
+    
+ case kind::BITVECTOR_UDIV:
+ case kind::BITVECTOR_UREM: {
+   node = expandBVDivByZero(node); 
+    break; 
+  }    
   case kind::DIVISION: {
     // partial function: division
     if(d_smt.d_logic.isLinear()) {

diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index d2fbb432b1f038c6450c8f32b74aa8a94f868a39..fbf9a45ee8de6d027f2d2c002aff6c2929f8daf1 100644 (file)
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -640,7 +640,7 @@ void uDivModRec(const Bits& a, const Bits& b, Bits& q, Bits& r, unsigned rec_wid
 
 void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) {
   BVDebug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node << "\n";
-  Assert(node.getKind() == kind::BITVECTOR_UDIV &&  q.size() == 0);
+  Assert(node.getKind() == kind::BITVECTOR_UDIV_TOTAL &&  q.size() == 0);
 
   Bits a, b;
   bb->bbTerm(node[0], a);
@@ -650,13 +650,13 @@ void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) {
   uDivModRec(a, b, q, r, getSize(node)); 
 
   // cache the remainder in case we need it later
-  Node remainder = mkNode(kind::BITVECTOR_UREM, node[0], node[1]);
+  Node remainder = mkNode(kind::BITVECTOR_UREM_TOTAL, node[0], node[1]);
   bb->cacheTermDef(remainder, r);
 }
 
 void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) {
   BVDebug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node << "\n";
-  Assert(node.getKind() == kind::BITVECTOR_UREM &&  rem.size() == 0);
+  Assert(node.getKind() == kind::BITVECTOR_UREM_TOTAL &&  rem.size() == 0);
 
   Bits a, b;
   bb->bbTerm(node[0], a);
@@ -666,7 +666,7 @@ void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) {
   uDivModRec(a, b, q, rem, getSize(node)); 
 
   // cache the quotient in case we need it later
-  Node quotient = mkNode(kind::BITVECTOR_UDIV, node[0], node[1]);
+  Node quotient = mkNode(kind::BITVECTOR_UDIV_TOTAL, node[0], node[1]);
   bb->cacheTermDef(quotient, q);
 }
 

diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index 41d98326e631b22f0a89e1da91b0bafbd8de6214..aca81e1763eeb7fd7d3fa46f680bf2ec9b1cd722 100644 (file)
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -214,6 +214,13 @@ bool Bitblaster::assertToSat(TNode lit, bool propagate) {
  */
  
 bool Bitblaster::solve(bool quick_solve) {
+  if (Trace.isOn("bitvector")) {
+    Trace("bitvector") << "Bitblaster::solve() asserted atoms ";
+    context::CDList<prop::SatLiteral>::const_iterator it = d_assertedAtoms.begin();
+    for (; it != d_assertedAtoms.end(); ++it) {
+      Trace("bitvector") << "     " << d_cnfStream->getNode(*it) << "\n";
+    }
+  }
   BVDebug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; 
   return SAT_VALUE_TRUE == d_satSolver->solve(); 
 }
@@ -280,11 +287,13 @@ void Bitblaster::initTermBBStrategies() {
   d_termBBStrategies [ kind::BITVECTOR_PLUS ]         = DefaultPlusBB;
   d_termBBStrategies [ kind::BITVECTOR_SUB ]          = DefaultSubBB;
   d_termBBStrategies [ kind::BITVECTOR_NEG ]          = DefaultNegBB;
-  d_termBBStrategies [ kind::BITVECTOR_UDIV ]         = DefaultUdivBB;
-  d_termBBStrategies [ kind::BITVECTOR_UREM ]         = DefaultUremBB;
-  d_termBBStrategies [ kind::BITVECTOR_SDIV ]         = DefaultSdivBB;
-  d_termBBStrategies [ kind::BITVECTOR_SREM ]         = DefaultSremBB;
-  d_termBBStrategies [ kind::BITVECTOR_SMOD ]         = DefaultSmodBB;
+  d_termBBStrategies [ kind::BITVECTOR_UDIV ]         = UndefinedTermBBStrategy; 
+  d_termBBStrategies [ kind::BITVECTOR_UREM ]         = UndefinedTermBBStrategy; 
+  d_termBBStrategies [ kind::BITVECTOR_UDIV_TOTAL ]   = DefaultUdivBB;
+  d_termBBStrategies [ kind::BITVECTOR_UREM_TOTAL ]   = DefaultUremBB;
+  d_termBBStrategies [ kind::BITVECTOR_SDIV ]         = UndefinedTermBBStrategy; 
+  d_termBBStrategies [ kind::BITVECTOR_SREM ]         = UndefinedTermBBStrategy; 
+  d_termBBStrategies [ kind::BITVECTOR_SMOD ]         = UndefinedTermBBStrategy; 
   d_termBBStrategies [ kind::BITVECTOR_SHL ]          = DefaultShlBB;
   d_termBBStrategies [ kind::BITVECTOR_LSHR ]         = DefaultLshrBB;
   d_termBBStrategies [ kind::BITVECTOR_ASHR ]         = DefaultAshrBB;
@@ -429,6 +438,9 @@ void Bitblaster::collectModelInfo(TheoryModel* m) {
     TNode var = *it;
     if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) {
       Node const_value = getVarValue(var);
+      Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= "
+                                << var << " "
+                                << const_value << "))\n";
       m->assertEquality(var, const_value, true); 
     }
   }

diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp
index 17f3acdd1bc007edd7d4300e5a8b662f132888df..e809a256643a70ae152745cf44925fe6af72cc81 100644 (file)
--- a/src/theory/bv/bv_subtheory_eq.cpp
+++ b/src/theory/bv/bv_subtheory_eq.cpp
@@ -28,7 +28,8 @@ using namespace CVC4::theory::bv::utils;
 EqualitySolver::EqualitySolver(context::Context* c, TheoryBV* bv)
   : SubtheorySolver(c, bv),
     d_notify(*this),
-    d_equalityEngine(d_notify, c, "theory::bv::TheoryBV")
+    d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"),
+    d_assertions(c)
 {
   if (d_useEqualityEngine) {
 
@@ -87,14 +88,16 @@ void EqualitySolver::explain(TNode literal, std::vector<TNode>& assumptions) {
 }
 
 bool EqualitySolver::addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) {
-  BVDebug("bitvector::equality") << "EqualitySolver::addAssertions \n";
+  Trace("bitvector::equality") << "EqualitySolver::addAssertions \n";
   Assert (!d_bv->inConflict());
 
   for (unsigned i = 0; i < assertions.size(); ++i) {
     TNode fact = assertions[i];
-
+    
     // Notify the equality engine
     if (d_useEqualityEngine && !d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_EQUALITY) ) {
+      Trace("bitvector::equality") << "     (assert " << fact << ")\n";  
+      d_assertions.push_back(fact); 
       bool negated = fact.getKind() == kind::NOT;
       TNode predicate = negated ? fact[0] : fact;
       if (predicate.getKind() == kind::EQUAL) {
@@ -164,5 +167,12 @@ void EqualitySolver::conflict(TNode a, TNode b) {
 }
 
 void EqualitySolver::collectModelInfo(TheoryModel* m) {
+  if (Debug.isOn("bitvector-model")) {
+    context::CDList<TNode>::const_iterator it = d_assertions.begin();
+    for (; it!= d_assertions.end(); ++it) {
+      Debug("bitvector-model") << "EqualitySolver::collectModelInfo (assert "
+                               << *it << ")\n";
+    }
+  }
   m->assertEqualityEngine(&d_equalityEngine);
 }

diff --git a/src/theory/bv/bv_subtheory_eq.h b/src/theory/bv/bv_subtheory_eq.h
index 91ad1599bea86ac272410068875933eb76a36971..64fe12706825eba26d04f844f1a20be12d6d7eef 100644 (file)
--- a/src/theory/bv/bv_subtheory_eq.h
+++ b/src/theory/bv/bv_subtheory_eq.h
@@ -58,6 +58,8 @@ class EqualitySolver : public SubtheorySolver {
   /** Store a conflict from merging two constants */
   void conflict(TNode a, TNode b);
 
+  /** FIXME: for debugging purposes only */
+  context::CDList<TNode> d_assertions; 
 public:
 
   EqualitySolver(context::Context* c, TheoryBV* bv);

diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 9dc2e66bbacf81833b8342df28b0686f7a83a0ab..2faa124378418abd9f3358bd6b2cbb7e5242d0cd 100644 (file)
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -54,6 +54,10 @@ operator BITVECTOR_UREM 2 "bit-vector unsigned remainder from truncating divisio
 operator BITVECTOR_SDIV 2 "bit-vector 2's complement signed division"
 operator BITVECTOR_SREM 2 "bit-vector 2's complement signed remainder (sign follows dividend)"
 operator BITVECTOR_SMOD 2 "bit-vector 2's complement signed remainder (sign follows divisor)"
+# total division kinds 
+operator BITVECTOR_UDIV_TOTAL 2 "bit-vector total unsigned division, truncating towards 0 (undefined if divisor is 0)"
+operator BITVECTOR_UREM_TOTAL 2 "bit-vector total unsigned remainder from truncating division (undefined if divisor is 0)"
+
 operator BITVECTOR_SHL 2 "bit-vector left shift"
 operator BITVECTOR_LSHR 2 "bit-vector logical shift right"
 operator BITVECTOR_ASHR 2 "bit-vector arithmetic shift right"
@@ -135,6 +139,8 @@ typerule BITVECTOR_NEG ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
 
 typerule BITVECTOR_UDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
 typerule BITVECTOR_UREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_UDIV_TOTAL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
+typerule BITVECTOR_UREM_TOTAL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
 typerule BITVECTOR_SDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
 typerule BITVECTOR_SREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule
 typerule BITVECTOR_SMOD ::CVC4::theory::bv::BitVectorFixedWidthTypeRule

diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
index d7d7c96703270effeb64482ed75fc9f47e2779bd..8b080d104bfcd6d0079fa3a9000f0b3b7627be86 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -198,7 +198,7 @@ Node RewriteRule<EvalNeg>::apply(TNode node) {
 }
 template<> inline
 bool RewriteRule<EvalUdiv>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_UDIV &&
+  return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL &&
           utils::isBVGroundTerm(node));
 }
 
@@ -213,7 +213,7 @@ Node RewriteRule<EvalUdiv>::apply(TNode node) {
 }
 template<> inline
 bool RewriteRule<EvalUrem>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_UREM &&
+  return (node.getKind() == kind::BITVECTOR_UREM_TOTAL &&
           utils::isBVGroundTerm(node));
 }
 

diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index a2fd9ee19fa204953ba20c61c2e83736edc91bd6..23cd8381dd2d5a237816f241083d5cf9f499166e 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -752,7 +752,7 @@ Node RewriteRule<NegIdemp>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<UdivPow2>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_UDIV &&
+  return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL &&
           utils::isPow2Const(node[1]));
 }
 
@@ -776,7 +776,7 @@ Node RewriteRule<UdivPow2>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<UdivOne>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_UDIV &&
+  return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL &&
           node[1] == utils::mkConst(utils::getSize(node), 1));
 }
 
@@ -794,7 +794,7 @@ Node RewriteRule<UdivOne>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<UdivSelf>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_UDIV &&
+  return (node.getKind() == kind::BITVECTOR_UDIV_TOTAL &&
           node[0] == node[1]);
 }
 
@@ -812,7 +812,7 @@ Node RewriteRule<UdivSelf>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<UremPow2>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_UREM &&
+  return (node.getKind() == kind::BITVECTOR_UREM_TOTAL &&
           utils::isPow2Const(node[1]));
 }
 
@@ -837,7 +837,7 @@ Node RewriteRule<UremPow2>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<UremOne>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_UREM &&
+  return (node.getKind() == kind::BITVECTOR_UREM_TOTAL &&
           node[1] == utils::mkConst(utils::getSize(node), 1));
 }
 
@@ -855,7 +855,7 @@ Node RewriteRule<UremOne>::apply(TNode node) {
 
 template<> inline
 bool RewriteRule<UremSelf>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_UREM &&
+  return (node.getKind() == kind::BITVECTOR_UREM_TOTAL &&
           node[0] == node[1]);
 }
 

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index a8941aac2e767c007b2fd0b51331c6b1c914faf3..1335f8f4a0f3fa6e674c42fd399c7a7bc57beb50 100644 (file)
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -365,7 +365,8 @@ RewriteResponse TheoryBVRewriter::RewriteNeg(TNode node, bool preregister) {
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteUdiv(TNode node, bool preregister){
+
+RewriteResponse TheoryBVRewriter::RewriteUdivTotal(TNode node, bool preregister){
   Node resultNode = node;
 
   if(RewriteRule<UdivPow2>::applies(node)) {
@@ -382,7 +383,7 @@ RewriteResponse TheoryBVRewriter::RewriteUdiv(TNode node, bool preregister){
   return RewriteResponse(REWRITE_DONE, resultNode); 
 }
 
-RewriteResponse TheoryBVRewriter::RewriteUrem(TNode node, bool preregister) {
+RewriteResponse TheoryBVRewriter::RewriteUremTotal(TNode node, bool preregister) {
   Node resultNode = node;
 
   if(RewriteRule<UremPow2>::applies(node)) {
@@ -575,8 +576,10 @@ void TheoryBVRewriter::initializeRewrites() {
   d_rewriteTable [ kind::BITVECTOR_PLUS ] = RewritePlus;
   d_rewriteTable [ kind::BITVECTOR_SUB ] = RewriteSub;
   d_rewriteTable [ kind::BITVECTOR_NEG ] = RewriteNeg;
-  d_rewriteTable [ kind::BITVECTOR_UDIV ] = RewriteUdiv;
-  d_rewriteTable [ kind::BITVECTOR_UREM ] = RewriteUrem;
+  // d_rewriteTable [ kind::BITVECTOR_UDIV ] = RewriteUdiv;
+  // d_rewriteTable [ kind::BITVECTOR_UREM ] = RewriteUrem;
+  d_rewriteTable [ kind::BITVECTOR_UDIV_TOTAL ] = RewriteUdivTotal;
+  d_rewriteTable [ kind::BITVECTOR_UREM_TOTAL ] = RewriteUremTotal;
   d_rewriteTable [ kind::BITVECTOR_SMOD ] = RewriteSmod;
   d_rewriteTable [ kind::BITVECTOR_SDIV ] = RewriteSdiv;
   d_rewriteTable [ kind::BITVECTOR_SREM ] = RewriteSrem;

diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index c50a3bbe0f52d250f9924a900d67852fb0def08f..59a2f90f6716d056f162415cdd2678c6eecbfa91 100644 (file)
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -39,7 +39,7 @@ class TheoryBVRewriter {
 
   static void initializeRewrites();
   
- static RewriteResponse RewriteEqual(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteEqual(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteUlt(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteSlt(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteUle(TNode node, bool prerewrite = false);
@@ -63,6 +63,8 @@ class TheoryBVRewriter {
   static RewriteResponse RewriteNeg(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteUdiv(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteUrem(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteUdivTotal(TNode node, bool prerewrite = false);
+  static RewriteResponse RewriteUremTotal(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteSmod(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteSdiv(TNode node, bool prerewrite = false);
   static RewriteResponse RewriteSrem(TNode node, bool prerewrite = false);

diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am
index 05c66d60c106992abc061210a3ca33e948107969..7e5bcba8c6ceb1ae2638c31c1f3de805c699db14 100644 (file)
--- a/test/regress/regress0/unconstrained/Makefile.am
+++ b/test/regress/regress0/unconstrained/Makefile.am
@@ -16,6 +16,8 @@ export CVC4_REGRESSION_ARGS
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
 # dejan: disable arith2.smt2, arith7.smt2 it's mixed arithmetic and it doesn't go well when changing theoryof 
+# lianah: disabled bvdiv.smt2, bvconcat.smt2 as the unconstrained terms are no longer recognized after implementing
+# the divide-by-zero semantics for bv division. 
 TESTS =        \
        arith3.smt2 \
        arith4.smt2 \
@@ -28,9 +30,7 @@ TESTS =       \
        bvbool.smt2 \
        bvcmp.smt2 \
        bvconcat2.smt2 \
-       bvconcat.smt2 \
        bvdiv2.smt2 \
-       bvdiv.smt2 \
        bvext.smt2 \
        bvite.smt2 \
        bvmul2.smt2 \

diff --git a/test/regress/regress0/unconstrained/bvdiv2.smt2 b/test/regress/regress0/unconstrained/bvdiv2.smt2
index 6314701b334da29888874a618d0a83e6d8c0620a..7a8fc3753a9c3336981f48aaca60dcaeabc2d939 100644 (file)
--- a/test/regress/regress0/unconstrained/bvdiv2.smt2
+++ b/test/regress/regress0/unconstrained/bvdiv2.smt2
@@ -18,9 +18,9 @@
 (declare-fun v4 () (_ BitVec 1024))
 (declare-fun v5 () (_ BitVec 1024))
 (assert
- (not
-  (= (bvudiv x0 x0) (_ bv1 10))
- )
-)
+ (and
+ (not (= x0 (_ bv0 10)))
+ (not (= (bvudiv x0 x0) (_ bv1 10)))
+))
 (check-sat)
 (exit)