Add simple inferences for extended bitvector functions, add a few related options. Use bv2nat, int2bv as triggers. Add regressions.

10 files changed, 166 insertions, 19 deletions

diff --git a/src/options/bv_options b/src/options/bv_options
index 341060b37..4a7cbd139 100644
--- a/src/options/bv_options
+++ b/src/options/bv_options
@@ -72,4 +72,10 @@ expert-option bvIntroducePow2 --bv-intro-pow2 bool :default false
 option bvLazyRewriteExtf --bv-lazy-rewrite-extf bool :default true :read-write
  lazily rewrite extended functions like bv2nat and int2bv
  
+option bvLazyReduceExtf --bv-lazy-reduce-extf bool :default false :read-write
+ reduce extended functions like bv2nat and int2bv at last call instead of full effort
+ 
+option bvAlgExtf --bv-alg-extf bool :default true :read-write
+ algebraic inferences for extended functions
+ 
 endmodule
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 7bcd23344..869e59502 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -66,7 +66,10 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u,
     d_eagerSolver(NULL),
     d_abstractionModule(new AbstractionModule(getFullInstanceName())),
     d_isCoreTheory(false),
-    d_calledPreregister(false)
+    d_calledPreregister(false),
+    d_needsLastCallCheck(false),
+    d_extf_range_infer(u),
+    d_extf_collapse_infer(c)
 {
   d_extt = new ExtTheory( this );
   d_extt->addFunctionKind( kind::BITVECTOR_TO_NAT );
@@ -329,7 +332,7 @@ void TheoryBV::preRegisterTerm(TNode node) {
     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
+  // AJR : equality solver currently registers all terms to ExtTheory, if we want a lazy reduction without the bv equality solver, need to call this
   //getExtTheory()->registerTermRec( node );
 }
 
@@ -374,9 +377,18 @@ void TheoryBV::checkForLemma(TNode fact) {
 
 void TheoryBV::check(Effort e)
 {
-  if (done() && !fullEffort(e)) {
+  if (done() && e<Theory::EFFORT_FULL) {
     return;
   }
+  
+  //last call : do reductions on extended bitvector functions
+  if( e==Theory::EFFORT_LAST_CALL ){
+    std::vector< Node > nred;
+    getExtTheory()->getActive( nred );
+    doExtfReductions( nred );
+    return;
+  }
+
   TimerStat::CodeTimer checkTimer(d_checkTime);
   Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
   TimerStat::CodeTimer codeTimer(d_statistics.d_solveTimer);
@@ -460,12 +472,94 @@ void TheoryBV::check(Effort e)
     if( getExtTheory()->doInferences( 0, nred ) ){
       return;
     }
-    std::vector< Node > nredr;
-    if( getExtTheory()->doReductions( 0, nred, nredr ) ){
-      return;
+    d_needsLastCallCheck = false;
+    if( !nred.empty() ){
+      //other inferences involving bv2nat, int2bv
+      if( options::bvAlgExtf() ){
+        if( doExtfInferences( nred ) ){
+          return;
+        }
+      }
+      if( !options::bvLazyReduceExtf() ){
+        if( doExtfReductions( nred ) ){
+          return;
+        }
+      }else{     
+        d_needsLastCallCheck = true;
+      }
+    }
+  }
+}
+
+bool TheoryBV::doExtfInferences( std::vector< Node >& terms ) {
+  bool sentLemma = false;
+  eq::EqualityEngine * ee = getEqualityEngine();    
+  std::map< Node, Node > op_map;
+  for( unsigned j=0; j<terms.size(); j++ ){
+    TNode n = terms[j];
+    Assert( n.getKind()==kind::BITVECTOR_TO_NAT || kind::INT_TO_BITVECTOR );
+    if( n.getKind()==kind::BITVECTOR_TO_NAT ){
+      //range lemmas
+      if( d_extf_range_infer.find( n )==d_extf_range_infer.end() ){
+        d_extf_range_infer.insert( n );
+        unsigned bvs = n[0].getType().getBitVectorSize();
+        Node min = NodeManager::currentNM()->mkConst( Rational( 0 ) );
+        Node max = NodeManager::currentNM()->mkConst( Rational( Integer(1).multiplyByPow2(bvs) ) );
+        Node lem = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, n, min ), NodeManager::currentNM()->mkNode( kind::LT, n, max ) );
+        Trace("bv-extf-lemma") << "BV extf lemma (range) : " << lem << std::endl;
+        d_out->lemma( lem );
+        sentLemma = true;
+      }
+    }
+    Node r = ( ee && ee->hasTerm( n[0] ) ) ? ee->getRepresentative( n[0] ) : n[0];
+    op_map[r] = n;
+  }
+  for( unsigned j=0; j<terms.size(); j++ ){
+    TNode n = terms[j];
+    Node r = ( ee && ee->hasTerm( n[0] ) ) ? ee->getRepresentative( n ) : n;
+    std::map< Node, Node >::iterator it = op_map.find( r );
+    if( it!=op_map.end() ){
+      Node parent = it->second;
+      Node cterm = parent[0]==n ? parent : NodeManager::currentNM()->mkNode( parent.getOperator(), n );
+      Trace("bv-extf-lemma-debug") << "BV extf collapse based on : " << n << std::endl;
+      if( d_extf_collapse_infer.find( cterm )==d_extf_collapse_infer.end() ){
+        d_extf_collapse_infer.insert( cterm );
+      
+        Node t = n[0];
+        if( n.getKind()==kind::INT_TO_BITVECTOR ){
+          Assert( t.getType().isInteger() );
+          //congruent modulo 2^( bv width )
+          unsigned bvs = n.getType().getBitVectorSize();
+          Node coeff = NodeManager::currentNM()->mkConst( Rational( Integer(1).multiplyByPow2(bvs) ) );
+          Node k = NodeManager::currentNM()->mkSkolem( "int_bv_cong", t.getType(), "for int2bv/bv2nat congruence" );
+          t = NodeManager::currentNM()->mkNode( kind::PLUS, t, NodeManager::currentNM()->mkNode( kind::MULT, coeff, k ) );
+        }
+        Node lem = parent.eqNode( t );
+        
+        if( parent[0]!=n ){
+          Assert( ee->areEqual( parent[0], n ) );
+          lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, parent[0].eqNode( n ), lem );
+        }
+        Trace("bv-extf-lemma") << "BV extf lemma (collapse) : " << lem << std::endl;
+        d_out->lemma( lem );
+        sentLemma = true;
+      }
     }
-    Assert( nredr.empty() );
   }
+  return sentLemma;
+}
+
+bool TheoryBV::doExtfReductions( std::vector< Node >& terms ) {
+  std::vector< Node > nredr;
+  if( getExtTheory()->doReductions( 0, terms, nredr ) ){
+    return true;
+  }
+  Assert( nredr.empty() );
+  return false;
+}
+
+bool TheoryBV::needsCheckLastEffort() {
+  return d_needsLastCallCheck;
 }
 
 void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){
@@ -520,18 +614,23 @@ void TheoryBV::propagate(Effort e) {
 
 
 eq::EqualityEngine * TheoryBV::getEqualityEngine() {
-  return NULL;
+  CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
+  if( core ){
+    return core->getEqualityEngine();
+  }else{
+    return NULL;
+  }
 }
 
 bool TheoryBV::getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ) {
-  CoreSolver* core = (CoreSolver*)d_subtheoryMap[SUB_CORE];
-  if( core ){
+  eq::EqualityEngine * ee = getEqualityEngine();
+  if( ee ){
     //get the constant equivalence classes
     bool retVal = false;
     for( unsigned i=0; i<vars.size(); i++ ){
       Node n = vars[i];
-      if( core->getEqualityEngine()->hasTerm( n ) ){
-        Node nr = core->getEqualityEngine()->getRepresentative( n );
+      if( ee->hasTerm( n ) ){
+        Node nr = ee->getRepresentative( n );
         if( nr.isConst() ){
           subs.push_back( nr );
           exp[n].push_back( n.eqNode( nr ) );
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 3cf471356..9973b0736 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -70,6 +70,8 @@ public:
   void preRegisterTerm(TNode n);
 
   void check(Effort e);
+  
+  bool needsCheckLastEffort();
 
   void propagate(Effort e);
 
@@ -175,7 +177,14 @@ private:
   AbstractionModule* d_abstractionModule;
   bool d_isCoreTheory;
   bool d_calledPreregister;
-
+  
+  //for extended functions
+  bool d_needsLastCallCheck;
+  context::CDHashSet<Node, NodeHashFunction> d_extf_range_infer;
+  context::CDHashSet<Node, NodeHashFunction> d_extf_collapse_infer;
+  bool doExtfInferences( std::vector< Node >& terms );
+  bool doExtfReductions( std::vector< Node >& terms );
+  
   bool wasPropagatedBySubtheory(TNode literal) const {
     return d_propagatedBy.find(literal) != d_propagatedBy.end();
   }
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 3017238ca..7ab9f7065 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -354,7 +354,7 @@ bool Trigger::isAtomicTriggerKind( Kind k ) {
   return k==APPLY_UF || k==SELECT || k==STORE ||
          k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER ||
          k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON ||
-         k==SEP_PTO;
+         k==SEP_PTO || k==BITVECTOR_TO_NAT || k==INT_TO_BITVECTOR;
 }
 
 bool Trigger::isRelationalTrigger( Node n ) {
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index cf7611dab..c21aa5445 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -582,6 +582,10 @@ void TheoryEngine::check(Theory::Effort effort) {
 
     // Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma
     if( effort == Theory::EFFORT_FULL && ! d_inConflict && ! needCheck() ) {
+      Trace("theory::assertions-model") << endl;
+      if (Trace.isOn("theory::assertions-model")) {
+        printAssertions("theory::assertions-model");
+      }
       //checks for theories requiring the model go at last call
       bool builtModel = false;
       for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
@@ -607,10 +611,6 @@ void TheoryEngine::check(Theory::Effort effort) {
           // must build model at this point
           d_curr_model_builder->buildModel(d_curr_model, true);
         }
-        Trace("theory::assertions-model") << endl;
-        if (Trace.isOn("theory::assertions-model")) {
-          printAssertions("theory::assertions-model");
-        }
       }
     }
 
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index f65fbf9a9..2aeb7a220 100644
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -96,7 +96,11 @@ SMT_TESTS = \
 	unsound1-reduced.smt2 \
 	bv2nat-ground.smt2 \
 	bv2nat-ground-c.smt2 \
-	cmu-rdk-3.smt2
+	cmu-rdk-3.smt2 \
+	bv2nat-simp-range.smt2 \
+	bv-int-collapse1.smt2 \
+	bv-int-collapse2.smt2 \
+	bv-int-collapse2-sat.smt2
 
 # Regression tests for SMT2 inputs
 SMT2_TESTS = divtest.smt2
diff --git a/test/regress/regress0/bv/bv-int-collapse1.smt2 b/test/regress/regress0/bv/bv-int-collapse1.smt2
new file mode 100644
index 000000000..5b631a7fd
--- /dev/null
+++ b/test/regress/regress0/bv/bv-int-collapse1.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-fun t () (_ BitVec 16))
+(assert (not (= t ((_ int2bv 16) (bv2nat t)))))
+(check-sat)
diff --git a/test/regress/regress0/bv/bv-int-collapse2-sat.smt2 b/test/regress/regress0/bv/bv-int-collapse2-sat.smt2
new file mode 100644
index 000000000..1a355a495
--- /dev/null
+++ b/test/regress/regress0/bv/bv-int-collapse2-sat.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-fun t () Int)
+(assert (> t 0))
+(assert (not (= t (bv2nat ((_ int2bv 16) t)))))
+(check-sat)
diff --git a/test/regress/regress0/bv/bv-int-collapse2.smt2 b/test/regress/regress0/bv/bv-int-collapse2.smt2
new file mode 100644
index 000000000..a630049cb
--- /dev/null
+++ b/test/regress/regress0/bv/bv-int-collapse2.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-fun t () Int)
+(assert (= (+ t 1) (bv2nat ((_ int2bv 16) t))))
+(check-sat)
diff --git a/test/regress/regress0/bv/bv2nat-simp-range.smt2 b/test/regress/regress0/bv/bv2nat-simp-range.smt2
new file mode 100644
index 000000000..e5ea20885
--- /dev/null
+++ b/test/regress/regress0/bv/bv2nat-simp-range.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-fun t () (_ BitVec 16))
+(assert (not (and (<= 0 (bv2nat t)) (< (bv2nat t) 65536))))
+(check-sat)