diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-29 13:08:31 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-29 13:08:31 +0100 |
| commit | 51d642e075466bc6655cae9752350f6760b2bd0f (patch) | |
| tree | 9c4e752e2d7ced10854c82555fa148b8e73e6d78 /src/theory/quantifiers/instantiation_engine.cpp | |
| parent | 4a8045f5f57c1e71dc4a2cdadc02ca09114c70af (diff) | |
Restrict LtePartialInst instantiations based on E-matching, promote to quantifiers module. Refactor QuantifiersEngine registration and check.
Diffstat (limited to 'src/theory/quantifiers/instantiation_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index b53919aaf..518921433 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -64,11 +64,11 @@ void InstantiationEngine::finishInit(){ d_instStrategies.push_back( d_i_ag ); } - //local theory extensions - if( options::localTheoryExt() ){ - d_i_lte = new InstStrategyLocalTheoryExt( d_quantEngine ); - d_instStrategies.push_back( d_i_lte ); - } + //local theory extensions TODO? + //if( options::localTheoryExt() ){ + // d_i_lte = new InstStrategyLocalTheoryExt( d_quantEngine ); + // d_instStrategies.push_back( d_i_lte ); + //} //full saturation : instantiate from relevant domain, then arbitrary terms if( options::fullSaturateQuant() ){ |