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/inst_strategy_cbqi.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/inst_strategy_cbqi.cpp')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 6a2bd5e2e..f378b4913 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -19,6 +19,7 @@ #include "theory/theory_engine.h" #include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/first_order_model.h" using namespace std; using namespace CVC4; @@ -255,9 +256,9 @@ void InstStrategySimplex::debugPrint( const char* c ){ //} } Debug(c) << std::endl; - - for( int q=0; q<d_quantEngine->getNumQuantifiers(); q++ ){ - Node f = d_quantEngine->getQuantifier( q ); + + for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ + Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); Debug(c) << f << std::endl; Debug(c) << " Inst constants: "; for( int i=0; i<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){ |