diff options
Diffstat (limited to 'src/theory/quantifiers/ambqi_builder.cpp')
-rw-r--r-- | src/theory/quantifiers/ambqi_builder.cpp | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp index 29bbc6a2c..c418d0fb1 100644 --- a/src/theory/quantifiers/ambqi_builder.cpp +++ b/src/theory/quantifiers/ambqi_builder.cpp @@ -12,17 +12,19 @@ ** \brief Implementation of abstract MBQI builder **/ - -#include "options/quantifiers_options.h" #include "theory/quantifiers/ambqi_builder.h" +#include "options/quantifiers_options.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" using namespace std; -using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + void AbsDef::construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth ) { d_def.clear(); @@ -807,7 +809,7 @@ bool AbsMbqiBuilder::processBuildModel(TheoryModel* m) { } if( fapps.empty() ){ //choose arbitrary value - Node mbt = d_qe->getTermDatabase()->getModelBasisOpTerm(f); + Node mbt = fm->getModelBasisOpTerm(f); Trace("ambqi-model-debug") << "Initial terms empty, add " << mbt << std::endl; fapps.push_back( mbt ); } @@ -958,3 +960,7 @@ bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNod return true; } } + +}/* namespace CVC4::theory::quantifiers */ +}/* namespace CVC4::theory */ +}/* namespace CVC4 */ |