Support for separation logic. Enable cbqi by default for pure BV.

5 files changed, 27 insertions, 26 deletions

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index d2637a555..523d868b5 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -190,7 +190,7 @@ bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visit
 bool InstStrategyCbqi::hasNonCbqiVariable( Node q ){
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
     TypeNode tn = q[0][i].getType();
-    if( !tn.isInteger() && !tn.isReal() && !tn.isBoolean() ){
+    if( !tn.isInteger() && !tn.isReal() && !tn.isBoolean() && !tn.isBitVector() ){
       if( options::cbqiSplx() ){
         return true;
       }else{
@@ -242,7 +242,7 @@ Node InstStrategyCbqi::getNextDecisionRequest(){
       Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
       bool value;
       if( !d_quantEngine->getValuation().hasSatValue( cel, value ) ){
-        Trace("cbqi-debug2") << "CBQI: get next decision " << cel << std::endl;
+        Trace("cbqi-dec") << "CBQI: get next decision " << cel << std::endl;
         return cel;
       }
     }
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index f855154af..5d575969f 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -153,27 +153,23 @@ int ModelEngine::checkModel(){
   //d_quantEngine->getEqualityQuery()->flattenRepresentatives( fm->d_rep_set.d_type_reps );
 
   //for debugging
-  if( Trace.isOn("model-engine") || Trace.isOn("model-engine-debug") ){
-    for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
-         it != fm->d_rep_set.d_type_reps.end(); ++it ){
-      if( it->first.isSort() ){
-        Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
-        if( Trace.isOn("model-engine-debug") ){
-          Trace("model-engine-debug") << "        Reps : ";
-          for( size_t i=0; i<it->second.size(); i++ ){
-            Trace("model-engine-debug") << it->second[i] << "  ";
-          }
-          Trace("model-engine-debug") << std::endl;
-          Trace("model-engine-debug") << "   Term reps : ";
-          for( size_t i=0; i<it->second.size(); i++ ){
-            Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 );
-            Trace("model-engine-debug") << r << " ";
-          }
-          Trace("model-engine-debug") << std::endl;
-          Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first);
-          Trace("model-engine-debug") << "  Basis term : " << mbt << std::endl;
-        }
+  for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
+       it != fm->d_rep_set.d_type_reps.end(); ++it ){
+    if( it->first.isSort() ){
+      Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
+      Trace("model-engine-debug") << "        Reps : ";
+      for( size_t i=0; i<it->second.size(); i++ ){
+        Trace("model-engine-debug") << it->second[i] << "  ";
+      }
+      Trace("model-engine-debug") << std::endl;
+      Trace("model-engine-debug") << "   Term reps : ";
+      for( size_t i=0; i<it->second.size(); i++ ){
+        Node r = d_quantEngine->getEqualityQuery()->getInternalRepresentative( it->second[i], Node::null(), 0 );
+        Trace("model-engine-debug") << r << " ";
       }
+      Trace("model-engine-debug") << std::endl;
+      Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first);
+      Trace("model-engine-debug") << "  Basis term : " << mbt << std::endl;
     }
   }
 
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 437f1bddf..b9aab0236 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -382,7 +382,7 @@ void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int
 }
 
 void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) {
-  if( n.getKind()==AND || n.getKind()==OR ){
+  if( n.getKind()==AND || n.getKind()==OR || n.getKind()==SEP_STAR ){
     newHasPol = hasPol;
     newPol = pol;
   }else if( n.getKind()==IMPLIES ){
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index c34d86497..9f222431e 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1925,7 +1925,7 @@ bool TermDb::containsUninterpretedConstant( Node n ) {
     bool ret = false;
     if( n.getKind()==UNINTERPRETED_CONSTANT ){
       ret = true;
-    }else{
+    }else if( n.getKind()!=SEP_NIL ){  //sep.nil has dummy argument FIXME
       for( unsigned i=0; i<n.getNumChildren(); i++ ){
         if( containsUninterpretedConstant( n[i] ) ){
           ret = true;
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 802acc089..ee091919d 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -375,8 +375,13 @@ bool Trigger::isRelationalTriggerKind( Kind k ) {
 }
   
 bool Trigger::isCbqiKind( Kind k ) {
-  return quantifiers::TermDb::isBoolConnective( k ) || k==PLUS || k==GEQ || k==EQUAL || k==MULT ||
-         k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER;
+  if( quantifiers::TermDb::isBoolConnective( k ) || k==PLUS || k==GEQ || k==EQUAL || k==MULT ){
+    return true;
+  }else{
+    //CBQI typically works for satisfaction-complete theories
+    TheoryId t = kindToTheoryId( k );
+    return t==THEORY_BV || t==THEORY_DATATYPES;
+  }
 }
 
 bool Trigger::isSimpleTrigger( Node n ){