diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-18 22:50:05 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-18 22:50:05 -0600 |
commit | f47f24528f5d19ac0affd572f3d34c090e97f9f9 (patch) | |
tree | 6a21c1964d862f99d9137f968881a0da33c59d1d /src/theory/quantifiers_engine.cpp | |
parent | 793361d81f0766c6a28ff699ed5447d9b8f8c123 (diff) |
Implement dynamic splitting for quantified formulas. Minor refactoring of reductions in quantifiers engine.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 28 |
1 files changed, 12 insertions, 16 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ce6c929b2..cfb3fda94 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -39,6 +39,7 @@ #include "theory/quantifiers/rewrite_engine.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/trigger.h" +#include "theory/quantifiers/quant_split.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf.h" @@ -121,6 +122,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_sg_gen = NULL; d_inst_engine = NULL; d_i_cbqi = NULL; + d_qsplit = NULL; d_model_engine = NULL; d_bint = NULL; d_rr_engine = NULL; @@ -161,6 +163,7 @@ QuantifiersEngine::~QuantifiersEngine(){ delete d_uee; delete d_fs; delete d_i_cbqi; + delete d_qsplit; } EqualityQueryQuantifiersEngine* QuantifiersEngine::getEqualityQuery() { @@ -237,6 +240,11 @@ void QuantifiersEngine::finishInit(){ d_lte_part_inst = new quantifiers::LtePartialInst( this, c ); d_modules.push_back( d_lte_part_inst ); } + if( ( options::finiteModelFind() && options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ) || + options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_AGG ){ + d_qsplit = new quantifiers::QuantDSplit( this, c ); + d_modules.push_back( d_qsplit ); + } if( options::quantAlphaEquiv() ){ d_alpha_equiv = new quantifiers::AlphaEquivalence( this ); } @@ -367,9 +375,9 @@ void QuantifiersEngine::check( Theory::Effort e ){ } Trace("quant-engine-debug") << std::endl; Trace("quant-engine-debug") << " # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl; - if( d_model->getNumToReduceQuantifiers()>0 ){ - Trace("quant-engine-debug") << " # quantified formulas to reduce = " << d_model->getNumToReduceQuantifiers() << std::endl; - } + //if( d_model->getNumToReduceQuantifiers()>0 ){ + // Trace("quant-engine-debug") << " # quantified formulas to reduce = " << d_model->getNumToReduceQuantifiers() << std::endl; + //} if( !d_lemmas_waiting.empty() ){ Trace("quant-engine-debug") << " lemmas waiting = " << d_lemmas_waiting.size() << std::endl; } @@ -513,25 +521,13 @@ bool QuantifiersEngine::reduceQuantifier( Node q ) { if( d_alpha_equiv ){ Trace("quant-engine-red") << "Alpha equivalence " << q << "?" << std::endl; //add equivalence with another quantified formula - if( !d_alpha_equiv->registerQuantifier( q ) ){ + if( d_alpha_equiv->reduceQuantifier( q ) ){ Trace("quant-engine-red") << "...alpha equivalence success." << std::endl; ++(d_statistics.d_red_alpha_equiv); d_quants_red[q] = true; return true; } } - if( d_lte_part_inst && !q.getAttribute(LtePartialInstAttribute()) ){ - //will partially instantiate - Trace("quant-engine-red") << "LTE: Partially instantiate " << q << "?" << std::endl; - if( d_lte_part_inst->addQuantifier( q ) ){ - Trace("quant-engine-red") << "...LTE partially instantiate success." << std::endl; - //delayed reduction : assert to model - d_model->assertQuantifier( q, true ); - ++(d_statistics.d_red_lte_partial_inst); - d_quants_red[q] = true; - return true; - } - } d_quants_red[q] = false; return false; }else{ |