diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-09-29 14:28:52 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-09-29 14:28:52 -0500 |
| commit | b48120e1c224208eaef28f86e77830f211852f9b (patch) | |
| tree | 28d9329c1cc13d5e99e8ac38212efb88c20c7ffa /src/theory/quantifiers_engine.cpp | |
| parent | 8011f2715fa6ba312fd766cab5249648598310d4 (diff) | |
Simplify representation of inversion Skolems for bv cegqi (#1164)
* Simplify intermediate representation of inversion skolems for cegqi bit-vectors. Cache bv inversion status globally in QuantifierEngine. Generalize virtual term policy for marking eligible instantiation terms. Enable regression.
* Enable other regression
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 8649c7bdd..2d1ae7983 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -24,6 +24,7 @@ #include "theory/quantifiers/ambqi_builder.h" #include "theory/quantifiers/bounded_integers.h" #include "theory/quantifiers/ce_guided_instantiation.h" +#include "theory/quantifiers/ceg_t_instantiator.h" #include "theory/quantifiers/conjecture_generator.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/full_model_check.h" @@ -130,6 +131,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_uee = NULL; d_fs = NULL; d_rel_dom = NULL; + d_bv_invert = NULL; d_builder = NULL; d_total_inst_count_debug = 0; @@ -160,6 +162,7 @@ QuantifiersEngine::~QuantifiersEngine(){ delete d_qcf; delete d_quant_rel; delete d_rel_dom; + delete d_bv_invert; delete d_model; delete d_tr_trie; delete d_term_db; @@ -217,9 +220,10 @@ void QuantifiersEngine::finishInit(){ if( options::cbqi() ){ d_i_cbqi = new quantifiers::InstStrategyCegqi( this ); d_modules.push_back( d_i_cbqi ); - //if( options::cbqiModel() ){ - // needsBuilder = true; - //} + if( options::cbqiBv() ){ + // if doing instantiation for BV, need the inverter class + d_bv_invert = new quantifiers::BvInverter; + } } if( options::ceGuidedInst() ){ d_ceg_inst = new quantifiers::CegInstantiation( this, c ); |