diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-01-27 11:35:22 -0600 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-01-27 11:35:22 -0600 |
| commit | bcbf52ffbe0416ecf70bdb644017c338c0540793 (patch) | |
| tree | 4f0478968f00c97b21d9fe528fa586cf7a227deb /src/theory/quantifiers/instantiation_engine.cpp | |
| parent | 7528e6596c85abc337aa9c795fc2e7627255148e (diff) | |
some fixes for Intel benchmarks regarding quantifiers and datatypes, datatypes theory still crashes for datatypes with boolean subfields
Diffstat (limited to 'src/theory/quantifiers/instantiation_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 7 |
1 files changed, 3 insertions, 4 deletions
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 ) ); |