Add new method for checking candidate models, --fmf-fmc. Add infrastructure for handling bounded integer quantification (quantifiers/bounded_integers.h and .cpp). Add option for disabling model minimality restriction for finite model finding, --disable-uf-ss-min-model. Add option for relational triggers such as x = f(y), --relational-trigger.

1 files changed, 5 insertions, 0 deletions

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 0bb0f1f79..5c24f89b7 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -27,6 +27,7 @@
 #include "theory/quantifiers/trigger.h"
 #include "theory/rewriterules/efficient_e_matching.h"
 #include "theory/rewriterules/rr_trigger.h"
+#include "theory/quantifiers/bounded_integers.h"
 
 using namespace std;
 using namespace CVC4;
@@ -60,8 +61,12 @@ d_lemmas_produced_c(u){
   if( options::finiteModelFind() ){
     d_model_engine = new quantifiers::ModelEngine( c, this );
     d_modules.push_back( d_model_engine );
+
+    d_bint = new quantifiers::BoundedIntegers( this );
+    d_modules.push_back( d_bint );
   }else{
     d_model_engine = NULL;
+    d_bint = NULL;
   }
 
   //options