Added support for proof production in Equality Engine. Cleaned up existing proof signatures and added proof signature for theory of arrays. Added new MBQI technique based on interval abstraction. Cleaned up option names. Improved symmetry breaking for uf strong solver. Other minor cleanup.

1 files changed, 5 insertions, 2 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index e9a69bd30..0388a2979 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -49,11 +49,14 @@ d_lemmas_produced_c(u){
   d_eem = new EfficientEMatcher( this );
   d_hasAddedLemma = false;
 
+  Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
   //the model object
-  if( options::fmfFullModelCheck() || options::fmfBoundInt() ){
+  if( options::mbqiMode()==quantifiers::MBQI_FMC || options::fmfBoundInt() ){
     d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" );
+  }else if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){
+    d_model = new quantifiers::FirstOrderModelQInt( this, c, "FirstOrderModelQInt" );
   }else{
-    d_model = new quantifiers::FirstOrderModelIG( c, "FirstOrderModelIG" );
+    d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
   }
 
   //add quantifiers modules