merged fmf-devel branch, includes support for SMT2 command get-value and (extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.

1 files changed, 7 insertions, 23 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 460289439..5add52d1f 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -24,6 +24,7 @@
 #include "theory/rewriter.h"
 #include "expr/command.h"
 #include "theory/arrays/theory_arrays_instantiator.h"
+#include "theory/model.h"
 
 using namespace std;
 
@@ -57,7 +58,7 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
   d_checkTimer("theory::arrays::checkTime"),
   d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP"),
   d_ppFacts(u),
-  //  d_ppCache(u),  
+  //  d_ppCache(u),
   d_literalsToPropagate(c),
   d_literalsToPropagateIndex(c, 0),
   d_isPreRegistered(c),
@@ -211,7 +212,7 @@ Node TheoryArrays::ppRewrite(TNode term) {
                 for (j = leftWrites - 1; j > i; --j) {
                   index_j = write_j[1];
                   if (!ppDisequal(index_i, index_j)) {
-                    Node hyp2(index_i.getType() == nm->booleanType()? 
+                    Node hyp2(index_i.getType() == nm->booleanType()?
                               index_i.iffNode(index_j) : index_i.eqNode(index_j));
                     hyp << hyp2.notNode();
                   }
@@ -623,27 +624,10 @@ void TheoryArrays::computeCareGraph()
 // MODEL GENERATION
 /////////////////////////////////////////////////////////////////////////////
 
-
-Node TheoryArrays::getValue(TNode n)
-{
-  // TODO: Implement this
-  NodeManager* nodeManager = NodeManager::currentNM();
-
-  switch(n.getKind()) {
-
-  case kind::VARIABLE:
-    Unhandled(kind::VARIABLE);
-
-  case kind::EQUAL: // 2 args
-    return nodeManager->
-      mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) );
-
-  default:
-    Unhandled(n.getKind());
-  }
+void TheoryArrays::collectModelInfo( TheoryModel* m ){
+  m->assertEqualityEngine( &d_equalityEngine );
 }
 
-
 /////////////////////////////////////////////////////////////////////////////
 // NOTIFICATIONS
 /////////////////////////////////////////////////////////////////////////////
@@ -663,7 +647,7 @@ void TheoryArrays::presolve()
 void TheoryArrays::check(Effort e) {
   TimerStat::CodeTimer codeTimer(d_checkTimer);
 
-  while (!done() && !d_conflict) 
+  while (!done() && !d_conflict)
   {
     // Get all the assertions
     Assertion assertion = get();
@@ -1306,7 +1290,7 @@ void TheoryArrays::dischargeLemmas()
       d_equalityEngine.assertEquality(eq2, true, d_true);
       continue;
     }
-    
+
     Node lem = nm->mkNode(kind::OR, eq2_r, eq1_r);
 
     Trace("arrays-lem")<<"Arrays::addRowLemma adding "<<lem<<"\n";