diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-12-01 02:57:59 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-12-01 02:57:59 +0000 |
commit | 959f5e77f96b406a498c3b67ce22d25e39d7bd2d (patch) | |
tree | e3cb4518ff5156de8286f9351a827bf40636804e /src/theory/quantifiers_engine.cpp | |
parent | b66fc3eac2717e8a887f1d4603c15cbcb7460e98 (diff) |
drastic simplification of quantifiers code regarding equality queries, instantiation strategies moved from instantiators to central instantiation engine, removed instantiator objects, simplified rewrite rules candidate generator to use central equality engine, efficient e-matching now uses central equality engine
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index ce62e2f8b..c04920ab8 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -14,7 +14,6 @@ #include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" -#include "theory/uf/theory_uf_instantiator.h" #include "theory/uf/theory_uf_strong_solver.h" #include "theory/uf/equality_engine.h" #include "theory/arrays/theory_arrays.h" @@ -25,6 +24,7 @@ #include "theory/quantifiers/instantiation_engine.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/trigger.h" #include "theory/rewriterules/efficient_e_matching.h" #include "theory/rewriterules/rr_trigger.h" @@ -84,9 +84,9 @@ EqualityQuery* QuantifiersEngine::getEqualityQuery() { return d_eq_query; } -Instantiator* QuantifiersEngine::getInstantiator( theory::TheoryId id ){ - return d_te->theoryOf( id )->getInstantiator(); -} +//Instantiator* QuantifiersEngine::getInstantiator( theory::TheoryId id ){ +// return d_te->theoryOf( id )->getInstantiator(); +//} context::Context* QuantifiersEngine::getSatContext(){ return d_te->theoryOf( THEORY_QUANTIFIERS )->getSatContext(); @@ -100,6 +100,12 @@ Valuation& QuantifiersEngine::getValuation(){ return d_te->theoryOf( THEORY_QUANTIFIERS )->getValuation(); } +void QuantifiersEngine::finishInit(){ + for( int i=0; i<(int)d_modules.size(); i++ ){ + d_modules[i]->finishInit(); + } +} + void QuantifiersEngine::check( Theory::Effort e ){ CodeTimer codeTimer(d_time); bool needsCheck = e>=Theory::EFFORT_LAST_CALL; //always need to check at or above last call |