diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-13 12:17:46 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-13 12:17:46 +0100 |
commit | 52514cada7c0c7c4fff69c85e0bd735abfdc03fd (patch) | |
tree | 401b5ab2efae7a0d3971d07d01ff61b0ab18fbcd /src/theory/quantifiers_engine.cpp | |
parent | 0e761324a33a993ae9a268bc2d2ed46f7e86b42d (diff) |
Remove two obsolete versions of MBQI.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 11 |
1 files changed, 2 insertions, 9 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index eabba85bf..c10992435 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -34,7 +34,6 @@ #include "theory/uf/options.h" #include "theory/uf/theory_uf.h" #include "theory/quantifiers/full_model_check.h" -#include "theory/quantifiers/qinterval_builder.h" #include "theory/quantifiers/ambqi_builder.h" using namespace std; @@ -91,8 +90,6 @@ d_lemmas_produced_c(u){ options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || options::fmfBoundInt() || options::mbqiMode()==quantifiers::MBQI_TRUST ){ d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" ); - }else if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){ - d_model = new quantifiers::FirstOrderModelQInt( this, c, "FirstOrderModelQInt" ); }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){ d_model = new quantifiers::FirstOrderModelAbs( this, c, "FirstOrderModelAbs" ); }else{ @@ -163,15 +160,9 @@ d_lemmas_produced_c(u){ options::mbqiMode()==quantifiers::MBQI_TRUST || options::fmfBoundInt() ){ Trace("quant-engine-debug") << "...make fmc builder." << std::endl; d_builder = new quantifiers::fmcheck::FullModelChecker( c, this ); - }else if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){ - Trace("quant-engine-debug") << "...make interval builder." << std::endl; - d_builder = new quantifiers::QIntervalBuilder( c, this ); }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){ Trace("quant-engine-debug") << "...make abs mbqi builder." << std::endl; d_builder = new quantifiers::AbsMbqiBuilder( c, this ); - }else if( options::mbqiMode()==quantifiers::MBQI_INST_GEN ){ - Trace("quant-engine-debug") << "...make inst-gen builder." << std::endl; - d_builder = new quantifiers::QModelBuilderInstGen( c, this ); }else{ Trace("quant-engine-debug") << "...make default model builder." << std::endl; d_builder = new quantifiers::QModelBuilderDefault( c, this ); @@ -676,6 +667,7 @@ Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& terms ) { return getInstantiation( f, d_term_db->d_inst_constants[f], terms ); } +/* bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){ if( options::incrementalSolving() ){ if( d_c_inst_match_trie.find( f )!=d_c_inst_match_trie.end() ){ @@ -696,6 +688,7 @@ bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, b } return false; } +*/ bool QuantifiersEngine::addLemma( Node lem, bool doCache ){ if( doCache ){ |