summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r--src/theory/quantifiers_engine.cpp8
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index ca16d2ab1..1a5be5a57 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -252,6 +252,7 @@ Valuation& QuantifiersEngine::getValuation(){
}
void QuantifiersEngine::finishInit(){
+ Trace("quant-engine-debug") << "QuantifiersEngine : finishInit " << std::endl;
for( int i=0; i<(int)d_modules.size(); i++ ){
d_modules[i]->finishInit();
}
@@ -281,6 +282,13 @@ bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) {
return mo==m || mo==NULL;
}
+void QuantifiersEngine::presolve() {
+ Trace("quant-engine-debug") << "QuantifiersEngine : presolve " << std::endl;
+ for( unsigned i=0; i<d_modules.size(); i++ ){
+ d_modules[i]->presolve();
+ }
+}
+
void QuantifiersEngine::check( Theory::Effort e ){
CodeTimer codeTimer(d_time);
if( !getMasterEqualityEngine()->consistent() ){
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback