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, 1 deletions

diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index 386864164..d2cd8807a 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -21,6 +21,7 @@
 #include "theory/quantifiers/model_builder.h"
 #include "theory/model.h"
 #include "theory/quantifiers/relevant_domain.h"
+#include "theory/quantifiers/full_model_check.h"
 
 namespace CVC4 {
 namespace theory {
@@ -35,6 +36,8 @@ private:
 private:    //analysis of current model:
   //relevant domain
   RelevantDomain d_rel_domain;
+  //full model checker
+  fmcheck::FullModelChecker d_fmc;
   //is the exhaustive instantiation incomplete?
   bool d_incomplete_check;
 private:
@@ -51,7 +54,7 @@ private:
   //check model
   int checkModel( int checkOption );
   //exhaustively instantiate quantifier (possibly using mbqi), return number of lemmas produced
-  int exhaustiveInstantiate( Node f, bool useRelInstDomain = false );
+  int exhaustiveInstantiate( Node f, bool useRelInstDomain = false, int effort = 0 );
 private:
   //temporary statistics
   int d_triedLemmas;
@@ -63,6 +66,7 @@ public:
   ~ModelEngine(){}
   //get the builder
   ModelEngineBuilder* getModelBuilder() { return d_builder; }
+  fmcheck::FullModelChecker* getFullModelChecker() { return &d_fmc; }
 public:
   void check( Theory::Effort e );
   void registerQuantifier( Node f );