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.

4 files changed, 51 insertions, 26 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";
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 25797dda3..6787f8ad8 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -219,7 +219,7 @@ class TheoryArrays : public Theory {
   private:
   public:
 
-  Node getValue(TNode n);
+  void collectModelInfo( TheoryModel* m );
 
   /////////////////////////////////////////////////////////////////////////////
   // NOTIFICATIONS
@@ -346,6 +346,12 @@ class TheoryArrays : public Theory {
   void queueRowLemma(RowLemmaType lem);
   void dischargeLemmas();
 
+  public:
+
+  eq::EqualityEngine* getEqualityEngine() {
+    return &d_equalityEngine;
+  }
+
 };/* class TheoryArrays */
 
 }/* CVC4::theory::arrays namespace */
diff --git a/src/theory/arrays/theory_arrays_instantiator.cpp b/src/theory/arrays/theory_arrays_instantiator.cpp
index 334d70eea..2e446c57f 100644
--- a/src/theory/arrays/theory_arrays_instantiator.cpp
+++ b/src/theory/arrays/theory_arrays_instantiator.cpp
@@ -51,6 +51,35 @@ void InstantiatorTheoryArrays::processResetInstantiationRound( Theory::Effort ef
 
 }
 
-int InstantiatorTheoryArrays::process( Node f, Theory::Effort effort, int e, int limitInst ){
+int InstantiatorTheoryArrays::process( Node f, Theory::Effort effort, int e ){
   return InstStrategy::STATUS_SAT;
 }
+
+bool InstantiatorTheoryArrays::hasTerm( Node a ){
+  return ((TheoryArrays*)d_th)->getEqualityEngine()->hasTerm( a );
+}
+
+bool InstantiatorTheoryArrays::areEqual( Node a, Node b ){
+  if( hasTerm( a ) && hasTerm( b ) ){
+    return ((TheoryArrays*)d_th)->getEqualityEngine()->areEqual( a, b );
+  }else{
+    return a==b;
+  }
+}
+
+bool InstantiatorTheoryArrays::areDisequal( Node a, Node b ){
+  if( hasTerm( a ) && hasTerm( b ) ){
+    return ((TheoryArrays*)d_th)->getEqualityEngine()->areDisequal( a, b, false );
+  }else{
+    return false;
+  }
+}
+
+Node InstantiatorTheoryArrays::getRepresentative( Node a ){
+  if( hasTerm( a ) ){
+    return ((TheoryArrays*)d_th)->getEqualityEngine()->getRepresentative( a );
+  }else{
+    return a;
+  }
+}
+
diff --git a/src/theory/arrays/theory_arrays_instantiator.h b/src/theory/arrays/theory_arrays_instantiator.h
index 6a7c9c3ed..ade43fdb0 100644
--- a/src/theory/arrays/theory_arrays_instantiator.h
+++ b/src/theory/arrays/theory_arrays_instantiator.h
@@ -32,7 +32,7 @@ protected:
   /** reset instantiation round */
   void processResetInstantiationRound( Theory::Effort effort );
   /** process quantifier */
-  int process( Node f, Theory::Effort effort, int e, int limitInst = 0 );
+  int process( Node f, Theory::Effort effort, int e );
 public:
   InstantiatorTheoryArrays(context::Context* c, QuantifiersEngine* ie, Theory* th);
   ~InstantiatorTheoryArrays() {}
@@ -42,6 +42,12 @@ public:
   void assertNode( Node assertion );
   /** identify */
   std::string identify() const { return std::string("InstantiatorTheoryArrays"); }
+public:
+  /** general queries about equality */
+  bool hasTerm( Node a );
+  bool areEqual( Node a, Node b );
+  bool areDisequal( Node a, Node b );
+  Node getRepresentative( Node a );
 };/* class Instantiatior */
 
 }