Refactoring to prepare for MBQI with integer quantification. Minor bug fixes.

4 files changed, 5 insertions, 131 deletions

diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am
index ec834522f..77f102cf8 100644
--- a/src/theory/arrays/Makefile.am
+++ b/src/theory/arrays/Makefile.am
@@ -16,9 +16,7 @@ libarrays_la_SOURCES = \
 	array_info.h \
 	array_info.cpp \
 	static_fact_manager.h \
-	static_fact_manager.cpp \
-	theory_arrays_model.h \
-	theory_arrays_model.cpp
+	static_fact_manager.cpp
 
 EXTRA_DIST = \
 	kinds
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 89f1dbf2c..98346d0e3 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -21,7 +21,6 @@
 #include <map>
 #include "theory/rewriter.h"
 #include "expr/command.h"
-#include "theory/arrays/theory_arrays_model.h"
 #include "theory/model.h"
 #include "theory/arrays/options.h"
 #include "smt/logic_exception.h"
@@ -495,7 +494,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
   }
   case kind::STORE_ALL: {
     throw LogicException("Array theory solver does not yet support assertions using constant array value");
-  }    
+  }
   default:
     // Variables etc
     if (node.getType().isArray()) {
@@ -1082,7 +1081,7 @@ void TheoryArrays::checkModel(Effort e)
     if (constraintIdx == d_modelConstraints.size()) {
       break;
     }
-    
+
     if (assertion.getKind() == kind::EQUAL && assertion[0].getType().isArray()) {
       assertionToCheck = solveWrite(expandStores(assertion[0], assumptions).eqNode(expandStores(assertion[1], assumptions)), true, true, false);
       if (assertionToCheck.getKind() == kind::AND &&
@@ -1429,7 +1428,7 @@ Node TheoryArrays::getModelValRec(TNode node)
             }
             ++d_numGetModelValConflicts;
             getSatContext()->pop();
-          } 
+          }
           ++te;
           if (te.isFinished()) {
             Assert(false);
@@ -1466,7 +1465,7 @@ bool TheoryArrays::hasLoop(TNode node, TNode target)
       return true;
     }
   }
-  
+
   return false;
 }
 
diff --git a/src/theory/arrays/theory_arrays_model.cpp b/src/theory/arrays/theory_arrays_model.cpp
deleted file mode 100644
index b5c81ef69..000000000
--- a/src/theory/arrays/theory_arrays_model.cpp
+++ /dev/null
@@ -1,65 +0,0 @@
-/*********************                                                        */
-/*! \file theory_arrays_model.cpp
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** 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/model.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, TheoryModel* m ) : d_arr( arr ){
-  d_base_arr = arr;
-  while( d_base_arr.getKind()==STORE ){
-    Node ri = m->getRepresentative( d_base_arr[1] );
-    if( d_values.find( ri )==d_values.end() ){
-      d_values[ ri ] = m->getRepresentative( d_base_arr[2] );
-    }
-    d_base_arr = d_base_arr[0];
-  }
-}
-
-Node ArrayModel::getValue( TheoryModel* m, Node i ){
-  i = m->getRepresentative( i );
-  std::map< Node, Node >::iterator it = d_values.find( i );
-  if( it!=d_values.end() ){
-    return it->second;
-  }else{
-    return NodeManager::currentNM()->mkNode( SELECT, getArrayValue(), i );
-    //return d_default_value;   //TODO: guarantee I can return this here
-  }
-}
-
-void ArrayModel::setValue( TheoryModel* m, Node i, Node e ){
-  Node ri = m->getRepresentative( i );
-  if( d_values.find( ri )==d_values.end() ){
-    d_values[ ri ] = m->getRepresentative( e );
-  }
-}
-
-void ArrayModel::setDefaultArray( Node arr ){
-  d_base_arr = arr;
-}
-
-Node ArrayModel::getArrayValue(){
-  Node curr = d_base_arr;
-  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
deleted file mode 100644
index 66dc80568..000000000
--- a/src/theory/arrays/theory_arrays_model.h
+++ /dev/null
@@ -1,58 +0,0 @@
-/*********************                                                        */
-/*! \file theory_arrays_model.h
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013  New York University and The University of Iowa
- ** 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 {
-
-class TheoryModel;
-
-namespace arrays {
-
-class ArrayModel{
-protected:
-  /** the array this model is for */
-  Node d_arr;
-public:
-  ArrayModel(){}
-  ArrayModel( Node arr, TheoryModel* m );
-  ~ArrayModel() {}
-public:
-  /** pre-defined values */
-  std::map< Node, Node > d_values;
-  /** base array */
-  Node d_base_arr;
-  /** get value, return arguments that the value depends on */
-  Node getValue( TheoryModel* m, Node i );
-  /** set value */
-  void setValue( TheoryModel* m, Node i, Node e );
-  /** set default */
-  void setDefaultArray( Node arr );
-public:
-  /** get array value */
-  Node getArrayValue();
-};/* class ArrayModel */
-
-}
-}
-}
-
-#endif
\ No newline at end of file