diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-01-27 11:35:22 -0600 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-27 13:38:21 -0500 |
commit | 73aa7b9dbc5415b6904539c2dd24683e77ca9b20 (patch) | |
tree | 64d4301b21d3c35c84238cc4242df500f564d3a8 /src/theory/quantifiers | |
parent | 5f58ecb6638f0e0fe63b67f1790b997684655bdd (diff) |
some fixes for Intel benchmarks regarding quantifiers and datatypes, datatypes theory still crashes for datatypes with boolean subfields
(cherry picked from master bcbf52ffbe0416ecf70bdb644017c338c0540793)
Diffstat (limited to 'src/theory/quantifiers')
-rwxr-xr-x | src/theory/quantifiers/inst_strategy_e_matching.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 7 |
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 ) ); |