Preliminary version of finite model finding over bounded integer quantification. Minor update to casc script.

2 files changed, 9 insertions, 1 deletions

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index d911ecf77..060f6dbba 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -67,6 +67,8 @@
 
 #include "theory/arith/options.h"
 
+#include "theory/quantifiers/bounded_integers.h"
+
 #include <stdint.h>
 
 #include <vector>
@@ -89,6 +91,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context
   d_unknownsInARow(0),
   d_hasDoneWorkSinceCut(false),
   d_learner(u),
+  d_quantEngine(qe),
   d_assertionsThatDoNotMatchTheirLiterals(c),
   d_nextIntegerCheckVar(0),
   d_constantIntegerVariables(c),
@@ -1373,6 +1376,10 @@ Constraint TheoryArithPrivate::constraintFromFactQueue(){
   Assert(!done());
   TNode assertion = get();
 
+  if( options::finiteModelFind() ){
+    d_quantEngine->getBoundedIntegers()->assertNode(assertion);
+  }
+
   Kind simpleKind = Comparison::comparisonKind(assertion);
   Constraint constraint = d_constraintDatabase.lookup(assertion);
   if(constraint == NullConstraint){
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 2ea3bb68e..86c8e213e 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -132,7 +132,8 @@ private:
   /** Static learner. */
   ArithStaticLearner d_learner;
 
-
+  /** quantifiers engine */
+  QuantifiersEngine * d_quantEngine;
   //std::vector<ArithVar> d_pool;
 public:
   void releaseArithVar(ArithVar v);