fixed datatypes rewriter to detect clashes between non-datatype subfields. cleaned up model code, TheoryModel::getValue is now const.

4 files changed, 0 insertions, 48 deletions

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 44eb00730..dd36f9917 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -93,20 +93,6 @@ void FirstOrderModel::initializeModelForTerm( Node n ){
   }
 }
 
-Node FirstOrderModel::getInterpretedValue( TNode n ){
-  //Trace("fo-model") << "get interpreted value " << n << std::endl;
-  /*TypeNode type = n.getType();
-  if( type.isFunction() || type.isPredicate() ){
-    if( d_uf_model_tree.find( n )!=d_uf_model_tree.end() ){
-      if( d_uf_models.find( n )==d_uf_models.end() ){
-        d_uf_models[n] = d_uf_model_tree[n].getFunctionValue( "$x" );
-      }
-    }
-  }*/
-  return TheoryModel::getInterpretedValue( n );
-}
-
-
 //for evaluation of quantifier bodies
 
 void FirstOrderModel::resetEvaluate(){
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 52688a816..05a7a83c1 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -80,8 +80,6 @@ public:
   virtual ~FirstOrderModel(){}
   // reset the model
   void reset();
-  /** get interpreted value */
-  Node getInterpretedValue( TNode n );
 public:
   // initialize the model
   void initialize( bool considerAxioms = true );
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 805d27008..81efa4289 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -42,33 +42,6 @@ d_qe( qe ), d_curr_model( c, NULL ){
   d_considerAxioms = true;
 }
 
-Node ModelEngineBuilder::chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel ){
-  if( fullModel ){
-    return TheoryEngineModelBuilder::chooseRepresentative( m, eqc, fullModel );
-  }else{
-    Assert( m->d_equalityEngine.hasTerm( eqc ) );
-    Assert( m->d_equalityEngine.getRepresentative( eqc )==eqc );
-    //avoid bad representatives
-    if( isBadRepresentative( eqc ) ){
-      eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &m->d_equalityEngine );
-      while( !eqc_i.isFinished() ){
-        if( !isBadRepresentative( *eqc_i ) ){
-          return *eqc_i;
-        }
-        ++eqc_i;
-      }
-      //otherwise, make new value?
-      //Message() << "Warning: Bad rep " << eqc << std::endl;
-    }
-    return eqc;
-  }
-}
-
-bool ModelEngineBuilder::isBadRepresentative( Node n ){
-  //avoid interpreted symbols
-  return n.getKind()==SELECT || n.getKind()==APPLY_SELECTOR;
-}
-
 void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) {
   FirstOrderModel* fm = (FirstOrderModel*)m;
   if( fullModel ){
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 1366a7650..d838064de 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -45,13 +45,8 @@ protected:
   std::map< Node, uf::UfModelPreferenceData > d_uf_prefs;
   //built model uf
   std::map< Node, bool > d_uf_model_constructed;
-protected:
   /** process build model */
   void processBuildModel( TheoryModel* m, bool fullModel );
-  /** choose representative for unconstrained equivalence class */
-  Node chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel );
-  /** bad representative */
-  bool isBadRepresentative( Node n );
 protected:
   //analyze model
   void analyzeModel( FirstOrderModel* fm );