Minor improvements to cbqi, fix bug in solving with vts symbols, round up for integer lower bounds. Add presolve infrastructure to quantifiers engine, modify --cbqi-prereg-inst.

1 files changed, 5 insertions, 0 deletions

diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index 6cf64407f..492b2dedf 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -77,6 +77,11 @@ void InstantiationEngine::finishInit(){
   }
 }
 
+void InstantiationEngine::presolve() {
+  for( unsigned i=0; i<d_instStrategies.size(); ++i ){
+    d_instStrategies[i]->presolve();
+  }
+}
 
 bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){
   unsigned lastWaiting = d_quantEngine->d_lemmas_waiting.size();