merging fmf-devel branch, includes refactored datatype theory, updates to model.h/cpp to prepare for release, and major refactoring of quantifiers/finite model finding. Note that new datatype theory does not insist upon any interpretation for selectors applied to incorrect constructors and consequently some answers may differ with previous version

5 files changed, 162 insertions, 5 deletions

diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am
index c429fc0c6..e4c814660 100644
--- a/src/theory/arrays/Makefile.am
+++ b/src/theory/arrays/Makefile.am
@@ -18,6 +18,8 @@ libarrays_la_SOURCES = \
 	static_fact_manager.h \
 	static_fact_manager.cpp \
 	theory_arrays_instantiator.h \
-	theory_arrays_instantiator.cpp
+	theory_arrays_instantiator.cpp \
+	theory_arrays_model.h \
+	theory_arrays_model.cpp
 
 EXTRA_DIST = kinds
diff --git a/src/theory/arrays/theory_arrays_instantiator.cpp b/src/theory/arrays/theory_arrays_instantiator.cpp
index ca9001fe5..67c42d124 100644
--- a/src/theory/arrays/theory_arrays_instantiator.cpp
+++ b/src/theory/arrays/theory_arrays_instantiator.cpp
@@ -17,7 +17,7 @@
 #include "theory/theory_engine.h"
 #include "theory/arrays/theory_arrays_instantiator.h"
 #include "theory/arrays/theory_arrays.h"
-#include "theory/uf/theory_uf_candidate_generator.h"
+#include "theory/rr_candidate_generator.h"
 
 using namespace std;
 using namespace CVC4;
@@ -61,15 +61,19 @@ bool InstantiatorTheoryArrays::hasTerm( Node a ){
 }
 
 bool InstantiatorTheoryArrays::areEqual( Node a, Node b ){
-  if( hasTerm( a ) && hasTerm( b ) ){
+  if( a==b ){
+    return true;
+  }else if( hasTerm( a ) && hasTerm( b ) ){
     return ((TheoryArrays*)d_th)->getEqualityEngine()->areEqual( a, b );
   }else{
-    return a==b;
+    return false;
   }
 }
 
 bool InstantiatorTheoryArrays::areDisequal( Node a, Node b ){
-  if( hasTerm( a ) && hasTerm( b ) ){
+  if( a==b ){
+    return false;
+  }else if( hasTerm( a ) && hasTerm( b ) ){
     return ((TheoryArrays*)d_th)->getEqualityEngine()->areDisequal( a, b, false );
   }else{
     return false;
@@ -84,6 +88,23 @@ Node InstantiatorTheoryArrays::getRepresentative( Node a ){
   }
 }
 
+eq::EqualityEngine* InstantiatorTheoryArrays::getEqualityEngine(){
+  return ((TheoryArrays*)d_th)->getEqualityEngine();
+}
+
+void InstantiatorTheoryArrays::getEquivalenceClass( Node a, std::vector< Node >& eqc ){
+  if( hasTerm( a ) ){
+    a = getEqualityEngine()->getRepresentative( a );
+    eq::EqClassIterator eqc_iter( a, getEqualityEngine() );
+    while( !eqc_iter.isFinished() ){
+      if( std::find( eqc.begin(), eqc.end(), *eqc_iter )==eqc.end() ){
+        eqc.push_back( *eqc_iter );
+      }
+      eqc_iter++;
+    }
+  }
+}
+
 rrinst::CandidateGenerator* InstantiatorTheoryArrays::getRRCanGenClasses(){
   arrays::TheoryArrays* ar = static_cast<arrays::TheoryArrays *>(getTheory());
   eq::EqualityEngine* ee =
diff --git a/src/theory/arrays/theory_arrays_instantiator.h b/src/theory/arrays/theory_arrays_instantiator.h
index f711229b2..23899afc1 100644
--- a/src/theory/arrays/theory_arrays_instantiator.h
+++ b/src/theory/arrays/theory_arrays_instantiator.h
@@ -49,6 +49,8 @@ public:
   bool areEqual( Node a, Node b );
   bool areDisequal( Node a, Node b );
   Node getRepresentative( Node a );
+  eq::EqualityEngine* getEqualityEngine();
+  void getEquivalenceClass( Node a, std::vector< Node >& eqc );
   /** general creators of candidate generators */
   rrinst::CandidateGenerator* getRRCanGenClasses();
   rrinst::CandidateGenerator* getRRCanGenClass();
diff --git a/src/theory/arrays/theory_arrays_model.cpp b/src/theory/arrays/theory_arrays_model.cpp
new file mode 100644
index 000000000..49da2f851
--- /dev/null
+++ b/src/theory/arrays/theory_arrays_model.cpp
@@ -0,0 +1,70 @@
+/*********************                                                        */

+/*! \file theory_arrays_model.cpp

+ ** \verbatim

+ ** Original author: ajreynol

+ ** Major contributors: none

+ ** Minor contributors (to current version): none

+ ** This file is part of the CVC4 prototype.

+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)

+ ** Courant Institute of Mathematical Sciences

+ ** New York University

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

+ **

+ ** \brief Implementation of theory_arrays_model class

+ **/

+

+#include "theory/theory_engine.h"

+#include "theory/arrays/theory_arrays_model.h"

+#include "theory/quantifiers/first_order_model.h"

+#include "theory/quantifiers/term_database.h"

+

+using namespace std;

+using namespace CVC4;

+using namespace CVC4::kind;

+using namespace CVC4::context;

+using namespace CVC4::theory;

+using namespace CVC4::theory::arrays;

+

+ArrayModel::ArrayModel( Node arr, quantifiers::FirstOrderModel* m ) : d_model( m ), d_arr( arr ){

+  Assert( arr.getKind()!=STORE );

+  //look at ground assertions

+  Node sel = NodeManager::currentNM()->mkNode( SELECT, arr, NodeManager::currentNM()->mkVar( arr.getType().getArrayIndexType() ) );

+  Node sel_op = sel.getOperator();  //FIXME: easier way to do this?

+  for( size_t i=0; i<d_model->getTermDatabase()->d_op_map[ sel_op ].size(); i++ ){

+    Node n = d_model->getTermDatabase()->d_op_map[ sel_op ][i];

+    Assert( n.getKind()==SELECT );

+    if( m->areEqual( n[0], arr ) ){

+      //d_model->getTermDatabase()->computeModelBasisArgAttribute( n );

+      //if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){

+        Node r = d_model->getRepresentative( n );

+        Node i = d_model->getRepresentative( n[1] );

+        d_values[i] = r;

+      //}

+    }

+  }

+}

+

+Node ArrayModel::getValue( Node n ){

+  Assert( n.getKind()==SELECT );

+  Assert( n[0]==d_arr );

+  std::map< Node, Node >::iterator it = d_values.find( n[0] );

+  if( it!=d_values.end() ){

+    return it->second;

+  }else{

+    return n;

+    //return d_default_value;   TODO: guarentee I can return this here

+  }

+}

+

+void ArrayModel::setDefaultValue( Node v ){

+  d_default_value = v;

+}

+

+Node ArrayModel::getArrayValue(){

+  Node curr = d_arr;    //TODO: make constant default

+  for( std::map< Node, Node >::iterator it = d_values.begin(); it != d_values.end(); ++it ){

+    curr = NodeManager::currentNM()->mkNode( STORE, curr, it->first, it->second );

+  }

+  return curr;

+}

diff --git a/src/theory/arrays/theory_arrays_model.h b/src/theory/arrays/theory_arrays_model.h
new file mode 100644
index 000000000..3895388e3
--- /dev/null
+++ b/src/theory/arrays/theory_arrays_model.h
@@ -0,0 +1,62 @@
+/*********************                                                        */

+/*! \file theory_arrays_model.h

+ ** \verbatim

+ ** Original author: ajreynol

+ ** Major contributors: none

+ ** Minor contributors (to current version): none

+ ** This file is part of the CVC4 prototype.

+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)

+ ** Courant Institute of Mathematical Sciences

+ ** New York University

+ ** See the file COPYING in the top-level source directory for licensing

+ ** information.\endverbatim

+ **

+ ** \brief MODEL for theory of arrays

+ **/

+

+

+#include "cvc4_private.h"

+

+#ifndef __CVC4__THEORY_ARRAYS_MODEL_H

+#define __CVC4__THEORY_ARRAYS_MODEL_H

+

+#include "theory/quantifiers_engine.h"

+

+namespace CVC4 {

+namespace theory {

+

+namespace quantifiers{

+  class FirstOrderModel;

+}

+

+namespace arrays {

+

+class ArrayModel{

+protected:

+  /** reference to model */

+  quantifiers::FirstOrderModel* d_model;

+  /** the array this model is for */

+  Node d_arr;

+public:

+  ArrayModel(){}

+  ArrayModel( Node arr, quantifiers::FirstOrderModel* m );

+  ~ArrayModel() {}

+public:

+  /** pre-defined values */

+  std::map< Node, Node > d_values;

+  /** default value */

+  Node d_default_value;

+  /** get value, return arguments that the value depends on */

+  Node getValue( Node n );

+  /** set default */

+  void setDefaultValue( Node v );

+public:

+  /** get array value */

+  Node getArrayValue();

+};/* class ArrayModel */

+

+}

+}

+}

+

+#endif
\ No newline at end of file