Merging bv parts of ajr/bvExt branch, minor additions to ExtTheory.

diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp
index 37e9f4476ff4f2f6f34af6cec46c2586f798d481..bb2c403aaa4b39461c512e6866107b4acceb5f6d 100644 (file)
--- a/src/theory/bv/aig_bitblaster.cpp
+++ b/src/theory/bv/aig_bitblaster.cpp
@@ -276,6 +276,7 @@ void AigBitblaster::bbTerm(TNode node, Bits& bits) {
     getBBTerm(node, bits);
     return;
   }
+  Assert( node.getType().isBitVector() );
 
   Debug("bitvector-bitblast") << "Bitblasting term " << node <<"\n";
   d_termBBStrategies[node.getKind()] (node, bits, this);

diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 6c6c13ee831c3cd74a247ff5f99d96094085f52c..7b7d38307750b743138f59e5107d2d1599cd7deb 100644 (file)
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -107,6 +107,9 @@ void BitblastSolver::bitblastQueue() {
       // don't bit-blast lemma atoms
       continue;
     }
+    if( !utils::isBitblastAtom(atom) ){
+      continue;
+    }
     Debug("bitblast-queue") << "Bitblasting atom " << atom <<"\n";
     {
       TimerStat::CodeTimer codeTimer(d_bitblaster->d_statistics.d_bitblastTimer);
@@ -121,6 +124,7 @@ bool BitblastSolver::check(Theory::Effort e) {
 
   ++(d_statistics.d_numCallstoCheck);
 
+  Debug("bv-bitblast-debug") << "...process queue" << std::endl;
   //// Lazy bit-blasting
   // bit-blast enqueued nodes
   bitblastQueue();
@@ -138,6 +142,10 @@ bool BitblastSolver::check(Theory::Effort e) {
         continue;
       }
     }
+    //skip facts involving integer equalities (from bv2nat)
+    if( !utils::isBitblastAtom( fact ) ){
+      continue;
+    }
 
     if (!d_bv->inConflict() &&
         (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) {
@@ -154,6 +162,7 @@ bool BitblastSolver::check(Theory::Effort e) {
     }
   }
 
+  Debug("bv-bitblast-debug") << "...do propagation" << std::endl;
   // We need to ensure we are fully propagated, so propagate now
   if (d_useSatPropagation) {
     d_bv->spendResource(1);
@@ -167,6 +176,7 @@ bool BitblastSolver::check(Theory::Effort e) {
   }
 
   // Solving
+  Debug("bv-bitblast-debug") << "...do solving" << std::endl;
   if (e == Theory::EFFORT_FULL) {
     Assert(!d_bv->inConflict());
     Debug("bitvector::bitblaster") << "BitblastSolver::addAssertions solving. \n";
@@ -180,6 +190,7 @@ bool BitblastSolver::check(Theory::Effort e) {
     }
   }
 
+  Debug("bv-bitblast-debug") << "...do abs bb" << std::endl;
   if (options::bvAbstraction() &&
       e == Theory::EFFORT_FULL &&
       d_lemmaAtomsQueue.size()) {
@@ -187,9 +198,11 @@ bool BitblastSolver::check(Theory::Effort e) {
     // bit-blast lemma atoms
     while(!d_lemmaAtomsQueue.empty()) {
       TNode lemma_atom = d_lemmaAtomsQueue.front();
-      d_bitblaster->bbAtom(lemma_atom);
       d_lemmaAtomsQueue.pop();
-
+      if( !utils::isBitblastAtom( lemma_atom ) ){
+        continue;
+      }
+      d_bitblaster->bbAtom(lemma_atom);
       // Assert to sat and check for conflicts
       bool ok = d_bitblaster->assertToSat(lemma_atom, d_useSatPropagation);
       if (!ok) {

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 97cbdb215943bfa79e317a48044fcb4992113979..c59da27f46009d0466a7a0ee57c00d2fdd451eae 100644 (file)
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -74,6 +74,8 @@ CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
   //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE);
   //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT);
   //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE);
+  d_equalityEngine.addFunctionKind(kind::BITVECTOR_TO_NAT);
+  d_equalityEngine.addFunctionKind(kind::INT_TO_BITVECTOR);
 }
 
 CoreSolver::~CoreSolver() {
@@ -368,6 +370,10 @@ void CoreSolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
   d_solver.conflict(t1, t2);
 }
 
+void CoreSolver::NotifyClass::eqNotifyNewClass(TNode t) {
+  d_solver.eqNotifyNewClass( t );
+}
+
 bool CoreSolver::storePropagation(TNode literal) {
   return d_bv->storePropagation(literal, SUB_CORE);
 }
@@ -379,6 +385,11 @@ void CoreSolver::conflict(TNode a, TNode b) {
   d_bv->setConflict(conflict);
 }
 
+void CoreSolver::eqNotifyNewClass(TNode t) {
+  Assert( d_bv->getExtTheory()!=NULL );
+  d_bv->getExtTheory()->registerTerm( t );
+}
+
 bool CoreSolver::isCompleteForTerm(TNode term, TNodeBoolMap& seen) {
   if (d_useSlicer)
     return utils::isCoreTerm(term, seen);

diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 93a938cc043649dd3eb4d3c29aa3bccbb2149465..22219b5d0b5cafc061641d4debc6a35b470a3c9e 100644 (file)
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -53,7 +53,7 @@ class CoreSolver : public SubtheorySolver {
     bool eqNotifyTriggerPredicate(TNode predicate, bool value);
     bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value);
     void eqNotifyConstantTermMerge(TNode t1, TNode t2);
-    void eqNotifyNewClass(TNode t) { }
+    void eqNotifyNewClass(TNode t);
     void eqNotifyPreMerge(TNode t1, TNode t2) { }
     void eqNotifyPostMerge(TNode t1, TNode t2) { }
     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
@@ -72,6 +72,9 @@ class CoreSolver : public SubtheorySolver {
   /** Store a conflict from merging two constants */
   void conflict(TNode a, TNode b);
 
+  /** new equivalence class */
+  void eqNotifyNewClass(TNode t);
+
   Slicer* d_slicer;
   context::CDO<bool> d_isComplete;
   unsigned d_lemmaThreshold;

diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 7d68f19b2659e7eaa1308b591fe3f9987a879e32..1fe096214df1557993b0ef26c81cf00c34284c9b 100644 (file)
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -40,14 +40,18 @@ bool InequalitySolver::check(Theory::Effort e) {
     Debug("bv-subtheory-inequality") << "  "<< fact <<"\n";
     if (fact.getKind() == kind::EQUAL) {
       TNode a = fact[0];
-      TNode b = fact[1];
-      ok = addInequality(a, b, false, fact);
-      if (ok)
-        ok = addInequality(b, a, false, fact);
+      if( a.getType().isBitVector() ){
+        TNode b = fact[1];
+        ok = addInequality(a, b, false, fact);
+        if (ok)
+          ok = addInequality(b, a, false, fact);
+      }
     } else if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL) {
       TNode a = fact[0][0];
-      TNode b = fact[0][1];
-      ok = d_inequalityGraph.addDisequality(a, b, fact);
+      if( a.getType().isBitVector() ){
+        TNode b = fact[0][1];
+        ok = d_inequalityGraph.addDisequality(a, b, fact);
+      }
     }
     if (fact.getKind() == kind::NOT && fact[0].getKind() == kind::BITVECTOR_ULE) {
       TNode a = fact[0][1];

diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index 53fb4f94b0371b8c7aaf1d8b2139bf2bb53d4d7b..e66b7f62147249f5ea319852ac65faa93a6845a4 100644 (file)
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -137,6 +137,8 @@ bool EagerBitblaster::hasBBAtom(TNode atom) const {
 }
 
 void EagerBitblaster::bbTerm(TNode node, Bits& bits) {
+  Assert( node.getType().isBitVector() );
+  
   if (hasBBTerm(node)) {
     getBBTerm(node, bits);
     return;

diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 3cbc45cd124ecc512f0eb5dffb1b4c7488867931..0ab33379f941d731b89285d8b0661322d1ed8d4e 100644 (file)
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -191,6 +191,7 @@ typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
 typerule BITVECTOR_SIGN_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule
 
 typerule BITVECTOR_TO_NAT ::CVC4::theory::bv::BitVectorConversionTypeRule
+typerule INT_TO_BITVECTOR_OP ::CVC4::theory::bv::IntToBitVectorOpTypeRule
 typerule INT_TO_BITVECTOR ::CVC4::theory::bv::BitVectorConversionTypeRule
 
 endtheory

diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index b549c329a9af8d08dfcefc434fb15f2b4946af82..fd21456eefc3c33489ecdeff4236109f06540629 100644 (file)
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -94,12 +94,13 @@ void TLazyBitblaster::bbAtom(TNode node) {
   if (hasBBAtom(node)) {
     return;
   }
-
+  
   // make sure it is marked as an atom
   addAtom(node);
 
   Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
   ++d_statistics.d_numAtoms;
+  
 
   /// if we are using bit-vector abstraction bit-blast the original interpretation
   if (options::bvAbstraction() &&
@@ -174,7 +175,9 @@ void TLazyBitblaster::makeVariable(TNode var, Bits& bits) {
 
 uint64_t TLazyBitblaster::computeAtomWeight(TNode node, NodeSet& seen) {
   node = node.getKind() == kind::NOT?  node[0] : node;
-
+  if( !utils::isBitblastAtom( node ) ){
+    return 0;
+  }
   Node atom_bb = Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this));
   uint64_t size = utils::numNodes(atom_bb, seen);
   return size;
@@ -191,9 +194,10 @@ void TLazyBitblaster::bbTerm(TNode node, Bits& bits) {
     getBBTerm(node, bits);
     return;
   }
+  Assert( node.getType().isBitVector() );
 
   d_bv->spendResource(options::bitblastStep());
-  Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n";
+  Debug("bitvector-bitblast") << "Bitblasting term " << node <<"\n";
   ++d_statistics.d_numTerms;
 
   d_termBBStrategies[node.getKind()] (node, bits,this);
@@ -250,6 +254,7 @@ bool TLazyBitblaster::assertToSat(TNode lit, bool propagate) {
   } else {
     atom = lit;
   }
+  Assert( utils::isBitblastAtom( atom ) );
 
   Assert (hasBBAtom(atom));
 

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index de596e3d5bdbbfa2dfb220a42fdf0e7ce3876c5c..7bcd23344b28f7ca14f102992638c893e181233d 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -68,6 +68,9 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u,
     d_isCoreTheory(false),
     d_calledPreregister(false)
 {
+  d_extt = new ExtTheory( this );
+  d_extt->addFunctionKind( kind::BITVECTOR_TO_NAT );
+  d_extt->addFunctionKind( kind::INT_TO_BITVECTOR );
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
     d_eagerSolver = new EagerBitblastSolver(this);
@@ -108,6 +111,7 @@ TheoryBV::~TheoryBV() {
     delete d_subtheories[i];
   }
   delete d_abstractionModule;
+  delete d_extt;
 }
 
 void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
@@ -324,6 +328,9 @@ void TheoryBV::preRegisterTerm(TNode node) {
   for (unsigned i = 0; i < d_subtheories.size(); ++i) {
     d_subtheories[i]->preRegister(node);
   }
+  
+  // AJR : equality solver currently registers all terms, if we want a lazy reduction without the bv equality solver, need to call this
+  //getExtTheory()->registerTermRec( node );
 }
 
 void TheoryBV::sendConflict() {
@@ -442,8 +449,22 @@ void TheoryBV::check(Effort e)
     }
     if (complete) {
       // if the last subtheory was complete we stop
+      break;
+    }
+  }
+  
+  //check extended functions
+  if (Theory::fullEffort(e)) {
+    //do inferences (adds external lemmas)  TODO: this can be improved to add internal inferences
+    std::vector< Node > nred;
+    if( getExtTheory()->doInferences( 0, nred ) ){
+      return;
+    }
+    std::vector< Node > nredr;
+    if( getExtTheory()->doReductions( 0, nred, nredr ) ){
       return;
     }
+    Assert( nredr.empty() );
   }
 }
 
@@ -497,12 +518,12 @@ void TheoryBV::propagate(Effort e) {
   }
 }
 
+
 eq::EqualityEngine * TheoryBV::getEqualityEngine() {
   return NULL;
 }
 
 bool TheoryBV::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) {
-#if 0
   CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
   if( core ){
     //get the constant equivalence classes
@@ -510,7 +531,7 @@ bool TheoryBV::getCurrentSubstitution( int effort, std::vector< Node >& vars, st
     for( unsigned i=0; i<vars.size(); i++ ){
       Node n = vars[i];
       if( core->getEqualityEngine()->hasTerm( n ) ){
-        Node nr = core->getEqualityEngine()->getRepresenative( n );
+        Node nr = core->getEqualityEngine()->getRepresentative( n );
         if( nr.isConst() ){
           subs.push_back( nr );
           exp[n].push_back( n.eqNode( nr ) );
@@ -518,14 +539,53 @@ bool TheoryBV::getCurrentSubstitution( int effort, std::vector< Node >& vars, st
         }else{
           subs.push_back( n );
         }
+      }else{
+        subs.push_back( n );
       }
     }
     //return true if the substitution is non-trivial
     return retVal;
   }
-#endif
   return false;
 }
+
+int TheoryBV::getReduction( int effort, Node n, Node& nr ) {
+  Trace("bv-ext") << "TheoryBV::checkExt : non-reduced : " << n << std::endl;
+  if( n.getKind()==kind::BITVECTOR_TO_NAT ){
+    //taken from rewrite code
+    const unsigned size = utils::getSize(n[0]);
+    NodeManager* const nm = NodeManager::currentNM();
+    const Node z = nm->mkConst(Rational(0));
+    const Node bvone = nm->mkConst(BitVector(1u, 1u));
+    NodeBuilder<> result(kind::PLUS);
+    Integer i = 1;
+    for(unsigned bit = 0; bit < size; ++bit, i *= 2) {
+      Node cond = nm->mkNode(kind::EQUAL, nm->mkNode(nm->mkConst(BitVectorExtract(bit, bit)), n[0]), bvone);
+      result << nm->mkNode(kind::ITE, cond, nm->mkConst(Rational(i)), z);
+    }
+    nr = Node(result);
+    return -1;
+  }else if( n.getKind()==kind::INT_TO_BITVECTOR ){
+    //taken from rewrite code
+    const unsigned size = n.getOperator().getConst<IntToBitVector>().size;
+    NodeManager* const nm = NodeManager::currentNM();
+    const Node bvzero = nm->mkConst(BitVector(1u, 0u));
+    const Node bvone = nm->mkConst(BitVector(1u, 1u));
+    std::vector<Node> v;
+    Integer i = 2;
+    while(v.size() < size) {
+      Node cond = nm->mkNode(kind::GEQ, nm->mkNode(kind::INTS_MODULUS_TOTAL, n[0], nm->mkConst(Rational(i))), nm->mkConst(Rational(i, 2)));
+      cond = Rewriter::rewrite( cond );
+      v.push_back(nm->mkNode(kind::ITE, cond, bvone, bvzero));
+      i *= 2;
+    }
+    NodeBuilder<> result(kind::BITVECTOR_CONCAT);
+    result.append(v.rbegin(), v.rend());
+    nr = Node(result);
+    return -1;
+  }
+  return 0;
+}
   
 Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
   switch(in.getKind()) {

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 0709ca4279310f654336ac63094c4e4ffbb0c10b..3cf47135631f213c89db1c91568b1bf4af7232f1 100644 (file)
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -82,6 +82,7 @@ public:
   /** equality engine */
   eq::EqualityEngine * getEqualityEngine();
   bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp );
+  int getReduction( int effort, Node n, Node& nr );
   
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
 

diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index 2bcb6ca1b43ea2e17be517ab3657fb6852124e10..052bc8c1a8b0d78f0438332cd5a94b7c1cc2f754 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -239,6 +239,10 @@ template<>
 Node RewriteRule<BVToNatEliminate>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<BVToNatEliminate>(" << node << ")" << std::endl;
 
+  //if( node[0].isConst() ){
+    //TODO? direct computation instead of term construction+rewriting
+  //}
+
   const unsigned size = utils::getSize(node[0]);
   NodeManager* const nm = NodeManager::currentNM();
   const Node z = nm->mkConst(Rational(0));
@@ -263,6 +267,10 @@ template<>
 Node RewriteRule<IntToBVEliminate>::apply(TNode node) {
   Debug("bv-rewrite") << "RewriteRule<IntToBVEliminate>(" << node << ")" << std::endl;
 
+  //if( node[0].isConst() ){
+    //TODO? direct computation instead of term construction+rewriting
+  //}
+
   const unsigned size = node.getOperator().getConst<IntToBitVector>().size;
   NodeManager* const nm = NodeManager::currentNM();
   const Node bvzero = nm->mkConst(BitVector(1u, 0u));

diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index acb12d649bb022041e0b1d3718016c0720d13915..7b9bdf14fe89d2f11ce741ce0dfef7c3133a89e1 100644 (file)
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -570,19 +570,28 @@ RewriteResponse TheoryBVRewriter::RewriteRedand(TNode node, bool prerewrite){
 }
 
 RewriteResponse TheoryBVRewriter::RewriteBVToNat(TNode node, bool prerewrite) {
-  Node resultNode = LinearRewriteStrategy
-    < RewriteRule<BVToNatEliminate>
-    >::apply(node);
-
-  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+  //do not use lazy rewrite strategy if equality solver is disabled
+  if( node[0].isConst() || !options::bitvectorEqualitySolver() ){
+    Node resultNode = LinearRewriteStrategy
+      < RewriteRule<BVToNatEliminate>
+      >::apply(node);
+    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+  }else{
+    return RewriteResponse(REWRITE_DONE, node); 
+  }
 }
 
 RewriteResponse TheoryBVRewriter::RewriteIntToBV(TNode node, bool prerewrite) {
-  Node resultNode = LinearRewriteStrategy
-    < RewriteRule<IntToBVEliminate>
-    >::apply(node);
+  //do not use lazy rewrite strategy if equality solver is disabled
+  if( node[0].isConst() || !options::bitvectorEqualitySolver() ){
+    Node resultNode = LinearRewriteStrategy
+      < RewriteRule<IntToBVEliminate>
+      >::apply(node);
 
-  return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+    return RewriteResponse(REWRITE_AGAIN_FULL, resultNode);
+  }else{
+    return RewriteResponse(REWRITE_DONE, node); 
+  }
 }
 
 RewriteResponse TheoryBVRewriter::RewriteEqual(TNode node, bool prerewrite) {

diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index cafa7044a43a6a7e8bd1e8a1ea4c4aa72783444b..3995aa74fbe28201c38a43979649349b766ace32 100644 (file)
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -287,6 +287,19 @@ class BitVectorConversionTypeRule {
   }
 }; /* class BitVectorConversionTypeRule */
 
+class IntToBitVectorOpTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+
+    if(n.getKind() == kind::INT_TO_BITVECTOR_OP) {
+      size_t bvSize = n.getConst<IntToBitVector>();
+      return nodeManager->mkFunctionType( nodeManager->integerType(), nodeManager->mkBitVectorType(bvSize) );
+    }
+
+    InternalError("bv-conversion typerule invoked for non-bv-conversion kind");
+  }
+}; /* class IntToBitVectorOpTypeRule */
+
 class CardinalityComputer {
  public:
   inline static Cardinality computeCardinality(TypeNode type) {

diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index dc3463c84d520cc8f33c5e99e5b5742a7364ac81..1210e8495201a19a1c5a54624d73ddb746626f2f 100644 (file)
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -515,6 +515,12 @@ uint64_t numNodes(TNode node, NodeSet& seen);
 
 void collectVariables(TNode node, NodeSet& vars);
 
+// is bitblast atom
+inline bool isBitblastAtom( Node lit ) {
+  TNode atom = lit.getKind()==kind::NOT ? lit[0] : lit;
+  return atom.getKind()!=kind::EQUAL || atom[0].getType().isBitVector();
+}
+
 }
 }
 }

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 3ef6df3fcd6717907e9b01b6b061b931739f18fb..5a99f8e30dc234fdd59834d52cc04ae72e829f2d 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -618,8 +618,7 @@ void TheoryStrings::preRegisterTerm(TNode n) {
           if( options::stringExp() ){
             //collect extended functions here: some may not be asserted to strings (such as those with return type Int),
             //  but we need to record them so they are treated properly
-            std::map< Node, bool > visited;
-            collectExtendedFuncTerms( n, visited );          
+            d_extt->registerTermRec( n );       
           }
         }
         //concat terms do not contribute to theory combination?  TODO: verify
@@ -1007,8 +1006,7 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
   }
   Trace("strings-pending-debug") << "  Now collect terms" << std::endl;
   //collect extended function terms in the atom
-  std::map< Node, bool > visited;
-  collectExtendedFuncTerms( atom, visited );
+  d_extt->registerTermRec( atom );
   Trace("strings-pending-debug") << "  Finished collect terms" << std::endl;
 }
 
@@ -4863,16 +4861,6 @@ Node TheoryStrings::getNormalSymRegExp(Node r, std::vector<Node> &nf_exp) {
   return ret;
 }
 
-void TheoryStrings::collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited ) {
-  if( visited.find( n )==visited.end() ){
-    visited[n] = true;
-    d_extt->registerTerm( n );
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      collectExtendedFuncTerms( n[i], visited );
-    }
-  }
-}
-
 }/* CVC4::theory::strings namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index fd984bd58f7784d77c04282a47d1ff538a72048b..6665f9e50874eddb32c8b8bfd24953c71327fe13 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -278,8 +278,6 @@ private:
     bool d_model_active;
   };
   std::map< Node, ExtfInfoTmp > d_extf_info_tmp;
-  //collect extended operator terms
-  void collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited );
 private:
   class InferInfo {
   public:

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 9e71a1ddfb5caa75156330c352d4eb5d1b4c2d23..1c0a03e9c7c557590cb7706b37bb85d91baa3473 100644 (file)
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -527,6 +527,21 @@ void ExtTheory::registerTerm( Node n ) {
   }
 }
 
+void ExtTheory::registerTermRec( Node n ) {
+  std::map< Node, bool > visited;
+  registerTermRec( n, visited );
+}
+
+void ExtTheory::registerTermRec( Node n, std::map< Node, bool >& visited ) {
+  if( visited.find( n )==visited.end() ){
+    visited[n] = true;
+    registerTerm( n );
+    for( unsigned i=0; i<n.getNumChildren(); i++ ){
+      registerTermRec( n[i], visited );
+    }
+  }
+}
+
 //mark reduced
 void ExtTheory::markReduced( Node n, bool contextDepend ) {
   d_ext_func_terms[n] = false;

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 5d64c64461521780500de60eba367483ceb0a06f..28552ed79711bb4582e91d364c589a667fa56db5 100644 (file)
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -1016,6 +1016,8 @@ protected:
   bool doInferencesInternal( int effort, std::vector< Node >& terms, std::vector< Node >& nred, bool batch, bool isRed ); 
   //send lemma
   bool sendLemma( Node lem, bool preprocess = false );
+  //register term (recursive)
+  void registerTermRec( Node n, std::map< Node, bool >& visited );
 public:
   ExtTheory( Theory * p );
   virtual ~ExtTheory(){}
@@ -1024,6 +1026,7 @@ public:
   //register term
   //  adds n to d_ext_func_terms if addFunctionKind( n.getKind() ) was called
   void registerTerm( Node n );
+  void registerTermRec( Node n );
   // set n as reduced/inactive
   //   if contextDepend = false, then n remains inactive in the duration of this user-context level
   void markReduced( Node n, bool contextDepend = true );

diff --git a/test/regress/regress0/bv/bv2nat-ground-c.smt2 b/test/regress/regress0/bv/bv2nat-ground-c.smt2
new file mode 100644 (file)
index 0000000..2bb09c2
--- /dev/null
+++ b/test/regress/regress0/bv/bv2nat-ground-c.smt2
@@ -0,0 +1,15 @@
+(set-logic QF_BVLIA)
+(set-info :status unsat)
+(declare-const a (_ BitVec 32))
+(declare-const b (_ BitVec 32))
+(declare-const c (_ BitVec 32))
+(declare-const d (_ BitVec 32))
+(declare-const e (_ BitVec 32))
+
+(assert (or (= a #x00000007) (= a #x00000005) (= a #x00000100)))
+
+(assert (not (= (bv2nat a) 7)))
+(assert (not (= (bv2nat a) 5)))
+(assert (< (bv2nat a) 10))
+
+(check-sat)

diff --git a/test/regress/regress0/bv/bv2nat-ground.smt2 b/test/regress/regress0/bv/bv2nat-ground.smt2
new file mode 100644 (file)
index 0000000..f72228b
--- /dev/null
+++ b/test/regress/regress0/bv/bv2nat-ground.smt2
@@ -0,0 +1,16 @@
+(set-logic QF_BVLIA)
+(set-info :status unsat)
+(declare-const a (_ BitVec 32))
+(declare-const b (_ BitVec 32))
+(declare-const c (_ BitVec 32))
+(declare-const d (_ BitVec 32))
+(declare-const e (_ BitVec 32))
+
+(assert (or (= a b) (= a c) (= a d) (= a e)))
+
+(assert (not (= (bv2nat a) (bv2nat b))))
+(assert (not (= (bv2nat a) (bv2nat c))))
+(assert (not (= (bv2nat a) (bv2nat d))))
+(assert (not (= (bv2nat a) (bv2nat e))))
+
+(check-sat)

diff --git a/test/regress/regress0/bv/cmu-rdk-3.smt2 b/test/regress/regress0/bv/cmu-rdk-3.smt2
new file mode 100644 (file)
index 0000000..742dd59
--- /dev/null
+++ b/test/regress/regress0/bv/cmu-rdk-3.smt2
@@ -0,0 +1,9 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+
+(declare-fun y () Int)
+(declare-fun x () Int)
+
+(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (not (not (= (ite (= (bv2nat (bvand ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))) ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1))))))) ((_ int2bv 3) 1))) 0) 1 0) 0)))) (not (= (ite (>= x 0) 1 0) 0))) (not (= (ite (>= y 0) 1 0) 0))) (not (= (ite (= x y) 1 0) 0))) (not (not (= (ite (= x 0) 1 0) 0)))) (not (not (= (ite (= y 0) 1 0) 0)))) (not (= (ite (= (bv2nat (bvand ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) x) ((_ int2bv 3) x)))) ((_ int2bv 3) 1))) 0) 1 0) 0))) (and (= x (bv2nat ((_ int2bv 3) x))) (= 1 (bv2nat ((_ int2bv 3) 1))))) (= ((_ extract 0 0) (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1))) (_ bv0 1))) (and (= y (bv2nat ((_ int2bv 3) y))) (= 1 (bv2nat ((_ int2bv 3) 1))))) (= ((_ extract 0 0) (bvashr ((_ int2bv 3) y) ((_ int2bv 3) 1))) (_ bv0 1))) (and (= (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1))) (bv2nat ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))))) (= (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1))) (bv2nat ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))))))) (= ((_ extract 0 0) (bvor ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))) ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))))) (_ bv0 1))) (and (= (bv2nat (bvor ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))) ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))))) (bv2nat ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))) ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1))))))))) (= 1 (bv2nat ((_ int2bv 3) 1))))) (= ((_ extract 0 0) (bvand ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1)))) ((_ int2bv 3) (bv2nat (bvashr ((_ int2bv 3) x) ((_ int2bv 3) 1))))))) ((_ int2bv 3) 1))) (_ bv0 1))) (and (= x (bv2nat ((_ int2bv 3) x))) (= x (bv2nat ((_ int2bv 3) x))))) (= ((_ extract 0 0) (bvor ((_ int2bv 3) x) ((_ int2bv 3) x))) (_ bv0 1))) (and (= (bv2nat (bvor ((_ int2bv 3) x) ((_ int2bv 3) x))) (bv2nat ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) x) ((_ int2bv 3) x)))))) (= 1 (bv2nat ((_ int2bv 3) 1))))) (= ((_ extract 0 0) (bvand ((_ int2bv 3) (bv2nat (bvor ((_ int2bv 3) x) ((_ int2bv 3) x)))) ((_ int2bv 3) 1))) (_ bv0 1))))
+
+(check-sat)