some fixes for Intel benchmarks regarding quantifiers and datatypes, datatypes theory still crashes for datatypes with boolean subfields

6 files changed, 42 insertions, 19 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 66c7e4cbc..1d98ce115 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -69,6 +69,7 @@
 #include "theory/arrays/options.h"
 #include "util/sort_inference.h"
 #include "theory/quantifiers/macros.h"
+#include "theory/datatypes/options.h"
 
 using namespace std;
 using namespace CVC4;
@@ -977,6 +978,13 @@ void SmtEngine::setLogicInternal() throw() {
       setOption("check-models", SExpr("false"));
     }
   }
+
+  //datatypes theory should assign values to all datatypes terms if logic is quantified
+  if (d_logic.isQuantified() && d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
+    if( !options::dtForceAssignment.wasSetByUser() ){
+      options::dtForceAssignment.set(true);
+    }
+  }
 }
 
 void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
@@ -2253,7 +2261,7 @@ void SmtEnginePrivate::processAssertions() {
         collectSkolems((*pos).first, skolemSet, cache);
         collectSkolems((*pos).second, skolemSet, cache);
       }
-      
+
       // We need to ensure:
       // 1. iteExpr has the form (ite cond (sk = t) (sk = e))
       // 2. if some sk' in Sk appears in cond, t, or e, then sk' <_sk sk
diff --git a/src/theory/datatypes/options b/src/theory/datatypes/options
index 45849858a..d250bee74 100644
--- a/src/theory/datatypes/options
+++ b/src/theory/datatypes/options
@@ -11,5 +11,7 @@ module DATATYPES "theory/datatypes/options.h" Datatypes theory
 # cdr( nil ) has no set value.
 expert-option dtRewriteErrorSel /--disable-dt-rewrite-error-sel bool :default true
  disable rewriting incorrectly applied selectors to arbitrary ground term
+expert-option dtForceAssignment /--dt-force-assignment bool :default false :read-write
+ force the datatypes solver to give specific values to all datatypes terms before answering sat
  
 endmodule
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 9da83ce41..9e4f0de75 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -24,6 +24,7 @@
 #include "theory/datatypes/theory_datatypes_type_rules.h"
 #include "theory/model.h"
 #include "smt/options.h"
+#include "theory/quantifiers/options.h"
 
 #include <map>
 
@@ -151,7 +152,7 @@ void TheoryDatatypes::check(Effort e) {
                 }
               }
             }
-            if( !needSplit && mustSpecifyModel() ){
+            if( !needSplit && mustSpecifyAssignment() ){
               //for the sake of termination, we must choose the constructor of a ground term
               //NEED GUARENTEE: groundTerm should not contain any subterms of the same type
               //** TODO: this is probably not good enough, actually need fair enumeration strategy
@@ -164,7 +165,7 @@ void TheoryDatatypes::check(Effort e) {
             }
             if( needSplit && consIndex!=-1 ) {
               Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[consIndex].getTester() ), n );
-              Trace("dt-split") << "*************Split for possible constructor " << test << " for " << n <<  endl;
+              Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n <<  endl;
               test = Rewriter::rewrite( test );
               NodeBuilder<> nb(kind::OR);
               nb << test << test.notNode();
@@ -375,8 +376,13 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
 
 void TheoryDatatypes::addSharedTerm(TNode t) {
   Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): "
-                     << t << endl;
-  d_equalityEngine.addTriggerTerm(t, THEORY_DATATYPES);
+                     << t << " " << t.getType().isBoolean() << endl;
+  if( t.getType().isBoolean() ){
+    //d_equalityEngine.addTriggerPredicate(t, THEORY_DATATYPES);
+  }else{
+    d_equalityEngine.addTriggerTerm(t, THEORY_DATATYPES);
+  }
+  Debug("datatypes") << "TheoryDatatypes::addSharedTerm() finished" << std::endl;
 }
 
 /** propagate */
@@ -489,7 +495,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
             Node unifEq = cons1.eqNode( cons2 );
             for( int i=0; i<(int)cons1.getNumChildren(); i++ ) {
               if( cons1[i]!=cons2[i] ){
-                Node eq = cons1[i].eqNode( cons2[i] );
+                Node eq = cons1[i].getType().isBoolean() ? cons1[i].iffNode( cons2[i] ) : cons1[i].eqNode( cons2[i] );
                 d_pending.push_back( eq );
                 d_pending_exp[ eq ] = unifEq;
                 Trace("datatypes-infer") << "DtInfer : " << eq << " by " << unifEq << std::endl;
@@ -797,7 +803,7 @@ void TheoryDatatypes::processNewTerm( Node n ){
   //see if it is rewritten to be something different
   Node rn = Rewriter::rewrite( n );
   if( rn!=n ){
-    Node eq = rn.eqNode( n );
+    Node eq = n.getType().isBoolean() ? rn.iffNode( n ) : rn.eqNode( n );
     d_pending.push_back( eq );
     d_pending_exp[ eq ] = NodeManager::currentNM()->mkConst( true );
     Trace("datatypes-infer") << "DtInfer : " << eq << ", trivial" << std::endl;
@@ -851,7 +857,7 @@ void TheoryDatatypes::collapseSelectors(){
           Node sn = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR, op, cons );
           Node s = Rewriter::rewrite( sn );
           if( sn!=s ){
-            Node eq = s.eqNode( sn );
+            Node eq = s.getType().isBoolean() ? s.iffNode( sn ) : s.eqNode( sn );
             d_pending.push_back( eq );
             d_pending_exp[ eq ] = NodeManager::currentNM()->mkConst( true );
             Trace("datatypes-infer") << "DtInfer : " << eq << ", by rewrite" << std::endl;
@@ -883,7 +889,7 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
     int index = getLabelIndex( eqc, n );
     const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype();
     //must be finite or have a selector
-    if( eqc->d_selectors || dt[ index ].isFinite() || mustSpecifyModel() ){
+    if( eqc->d_selectors || dt[ index ].isFinite() || mustSpecifyAssignment() ){
       //instantiate this equivalence class
       eqc->d_inst = true;
       Node tt_cons = getInstantiateCons( tt, dt, index );
@@ -967,9 +973,12 @@ bool TheoryDatatypes::searchForCycle( Node n, Node on,
   return false;
 }
 
-bool TheoryDatatypes::mustSpecifyModel(){
-  return options::produceModels();
-  //return options::finiteModelFind() || options::produceModels();
+bool TheoryDatatypes::mustSpecifyAssignment(){
+  //FIXME: the condition finiteModelFind is an over-approximation in this function
+  //   we still may not want to specify assignments for datatypes that are truly infinite
+  //   the fix for this is to correctly compute the cardinality for datatypes containing uninterpered sorts in fmf (i.e. by assuming they are finite)
+  return options::finiteModelFind() || options::produceModels() || options::dtForceAssignment();
+  //return options::produceModels();
   //return false;
 }
 
@@ -980,7 +989,7 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
   //  (3) Instantiate : is_C( t ) => t = C( sel_1( t ) ... sel_n( t ) )
   //We may need to communicate (3) outwards if the conclusions involve other theories
   Trace("dt-lemma-debug") << "Compute for " << exp << " => " << n << std::endl;
-  if( n.getKind()==EQUAL && n[1].getKind()==APPLY_CONSTRUCTOR && exp.getKind()!=EQUAL  ){
+  if( ( n.getKind()==EQUAL || n.getKind()==IFF) && n[1].getKind()==APPLY_CONSTRUCTOR && exp.getKind()!=EQUAL  ){
     bool addLemma = false;
 #if 1
     const Datatype& dt = ((DatatypeType)(n[1].getType()).toType()).getDatatype();
@@ -997,13 +1006,15 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
       //check if we have already added this lemma
       if( std::find( d_inst_lemmas[ n[0] ].begin(), d_inst_lemmas[ n[0] ].end(), n[1] )==d_inst_lemmas[ n[0] ].end() ){
         d_inst_lemmas[ n[0] ].push_back( n[1] );
+        Trace("dt-lemma-debug") << "Communicate " << n << std::endl;
         return true;
       }else{
+        Trace("dt-lemma-debug") << "Already communicated " << n << std::endl;
         return false;
       }
     }
-    Trace("dt-lemma-debug") << "Do not need to communicate " << n << std::endl;
   }
+  Trace("dt-lemma-debug") << "Do not need to communicate " << n << std::endl;
   return false;
 }
 
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 9846e80f2..46212ccbf 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -236,7 +236,7 @@ private:
     *  This returns true when the datatypes theory is expected to specify the constructor
     *  type for all equivalence classes.
     */
-  bool mustSpecifyModel();
+  bool mustSpecifyAssignment();
   /** must communicate fact */
   bool mustCommunicateFact( Node n, Node exp );
 private:
diff --git a/src/theory/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index ea22486a6..23f0d8a54 100755
--- a/src/theory/quantifiers/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -87,6 +87,9 @@ private:
   /** generate triggers */

   void generateTriggers( Node f );

 public:

+  /** tstrt is the type of triggers to use (maximum depth, minimum depth, or all)

+      rstrt is the relevance setting for trigger (use only relevant triggers vs. use all)

+      rgfr is the frequency at which triggers are generated */

   InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt, int rstrt, int rgfr = -1 ) :

       InstStrategy( qe ), d_tr_strategy( tstrt ), d_rlv_strategy( rstrt ), d_generate_additional( false ){

     setRegenerateFrequency( rgfr );

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 579c53665..653016d1c 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -60,11 +60,10 @@ void InstantiationEngine::finishInit(){
     //d_isup->setPriorityOver( i_agm );
     //i_ag->setPriorityOver( i_agm );
   }
-  //CBQI: FIXME
   //for arithmetic
-  //if( options::cbqi() ){
-  //  addInstStrategy( new InstStrategySimplex( d_quantEngine ) );
-  //}
+  if( options::cbqi() ){
+    addInstStrategy( new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine ) );
+  }
   //for datatypes
   //if( options::cbqi() ){
   //  addInstStrategy( new InstStrategyDatatypesValue( d_quantEngine ) );