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

2 files changed, 6 insertions, 4 deletions

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 ) );