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

9 files changed, 52 insertions, 162 deletions

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index fae2c5bff..3ddf1d199 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -126,6 +126,13 @@ public:
           }
         }
       }
+    }else if( !n1.getType().isDatatype() ){
+      //also check for clashes between non-datatypes
+      Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 );
+      eq = Rewriter::rewrite( eq );
+      if( eq==NodeManager::currentNM()->mkConst(false) ){
+        return true;
+      }
     }
     return false;
   }
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 3d918277f..adcf8dacf 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -48,26 +48,26 @@ void TheoryModel::reset(){
   d_uf_models.clear();
 }
 
-Node TheoryModel::getValue( TNode n ){
+Node TheoryModel::getValue( TNode n ) const{
   //apply substitutions
   Node nn = d_substitutions.apply( n );
   //get value in model
   return getModelValue( nn );
 }
 
-Expr TheoryModel::getValue( Expr expr ){
+Expr TheoryModel::getValue( Expr expr ) const{
   Node n = Node::fromExpr( expr );
   Node ret = getValue( n );
   return ret.toExpr();
 }
 
 /** get cardinality for sort */
-Cardinality TheoryModel::getCardinality( Type t ){
+Cardinality TheoryModel::getCardinality( Type t ) const{
   TypeNode tn = TypeNode::fromType( t );
   //for now, we only handle cardinalities for uninterpreted sorts
   if( tn.isSort() ){
     if( d_rep_set.hasType( tn ) ){
-      return Cardinality( d_rep_set.d_type_reps[tn].size() );
+      return Cardinality( d_rep_set.getNumRepresentatives( tn ) );
     }else{
       return Cardinality( CardinalityUnknown() );
     }
@@ -76,8 +76,7 @@ Cardinality TheoryModel::getCardinality( Type t ){
   }
 }
 
-Node TheoryModel::getModelValue( TNode n )
-{
+Node TheoryModel::getModelValue( TNode n ) const{
   if( n.isConst() ) {
     return n;
   }
@@ -85,9 +84,10 @@ Node TheoryModel::getModelValue( TNode n )
   TypeNode t = n.getType();
   if (t.isFunction() || t.isPredicate()) {
     if (d_enableFuncModels) {
-      if (d_uf_models.find(n) != d_uf_models.end()) {
+      std::map< Node, Node >::const_iterator it = d_uf_models.find(n);
+      if (it != d_uf_models.end()) {
         // Existing function
-        return d_uf_models[n];
+        return it->second;
       }
       // Unknown function symbol: return LAMBDA x. c, where c is the first constant in the enumeration of the range type
       vector<TypeNode> argTypes = t.getArgTypes();
@@ -108,13 +108,15 @@ Node TheoryModel::getModelValue( TNode n )
     std::vector<Node> children;
     if (n.getKind() == APPLY_UF) {
       Node op = n.getOperator();
-      if (d_uf_models.find(op) == d_uf_models.end()) {
+      std::map< Node, Node >::const_iterator it = d_uf_models.find(op);
+      if (it == d_uf_models.end()) {
         // Unknown term - return first enumerated value for this type
         TypeEnumerator te(n.getType());
         return *te;
+      }else{
+        // Plug in uninterpreted function model
+        children.push_back(it->second);
       }
-      // Plug in uninterpreted function model
-      children.push_back(d_uf_models[op]);
     }
     else if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
       children.push_back(n.getOperator());
@@ -136,82 +138,11 @@ Node TheoryModel::getModelValue( TNode n )
   }
   Node val = d_equalityEngine.getRepresentative(n);
   Assert(d_reps.find(val) != d_reps.end());
-  val = d_reps[val];
-  return val;
-}
-
-
-Node TheoryModel::getInterpretedValue( TNode n ){
-  Trace("model") << "Get interpreted value of " << n << std::endl;
-  TypeNode type = n.getType();
-  if( type.isFunction() || type.isPredicate() ){
-    //for function models
-    if( d_enableFuncModels ){
-      if( d_uf_models.find( n )!=d_uf_models.end() ){
-        //pre-existing function model
-        Trace("model") << "Return function value." << std::endl;
-        return d_uf_models[n];
-      }else{
-        Trace("model") << "Return arbitrary function value." << std::endl;
-        //otherwise, choose the constant default value
-        uf::UfModelTree ufmt( n );
-        Node default_v = getInterpretedValue( NodeManager::currentNM()->mkSkolem( "defaultValueQueryVar_$$", type.getRangeType(),
-                                              "a placeholder variable to query for a default value in model construction" ) );
-        ufmt.setDefaultValue( this, default_v );
-        return ufmt.getFunctionValue( "$x" );
-      }
-    }else{
-      return n;
-    }
-  } else{
-    Trace("model-debug") << "check rep..." << std::endl;
-    Node ret;
-    //check if the representative is defined
-    n = d_equalityEngine.hasTerm( n ) ? d_equalityEngine.getRepresentative( n ) : n;
-    Trace("model-debug") << "rep is..." << n << std::endl;
-    if( d_reps.find( n )!=d_reps.end() ){
-      Trace("model") << "Return value in equality engine."<< std::endl;
-      return d_reps[n];
-    }
-    Trace("model-debug") << "check apply uf models..." << std::endl;
-    //if it is APPLY_UF, we must consult the corresponding function if it exists
-    if( n.getKind()==APPLY_UF ){
-      Node op = n.getOperator();
-      if( d_uf_models.find( op )!=d_uf_models.end() ){
-        std::vector< Node > lam_children;
-        lam_children.push_back( d_uf_models[ op ] );
-        for( int i=0; i<(int)n.getNumChildren(); i++ ){
-          lam_children.push_back( n[i] );
-        }
-        Node app_lam = NodeManager::currentNM()->mkNode( APPLY_UF, lam_children );
-        ret = Rewriter::rewrite( app_lam );
-        Trace("model") << "Consult UF model." << std::endl;
-      }
-    }
-    Trace("model-debug") << "check existing..." << std::endl;
-    if( ret.isNull() ){
-      //second, try to choose an existing term as value
-      std::vector< Node > v_emp;
-      ret = getDomainValue( type, v_emp );
-      if( !ret.isNull() ){
-        Trace("model") << "Choose existing value." << std::endl;
-      }
-    }
-    Trace("model-debug") << "check new..." << std::endl;
-    if( ret.isNull() ){
-      //otherwise, choose new value
-      ret = getNewDomainValue( type );
-      if( !ret.isNull() ){
-        Trace("model") << "Choose new value." << std::endl;
-      }
-    }
-    if( !ret.isNull() ){
-      return ret;
-    }else{
-      //otherwise, just return itself (this usually should not happen)
-      Trace("model") << "Return self." << std::endl;
-      return n;
-    }
+  std::map< Node, Node >::const_iterator it = d_reps.find( val );
+  if( it!=d_reps.end() ){
+    return it->second;
+  }else{
+    return Node::null();
   }
 }
 
@@ -710,16 +641,3 @@ void TheoryEngineModelBuilder::processBuildModel(TheoryModel* m, bool fullModel)
     }
   }
 }
-
-
-Node TheoryEngineModelBuilder::chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel ){
-  //try to get a new domain value
-  Node rep = m->getNewDomainValue( eqc.getType() );
-  if( !rep.isNull() ){
-    return rep;
-  }else{
-    //if we can't get new domain value, just return eqc itself (this typically should not happen)
-    //FIXME: Assertion failure here?
-    return eqc;
-  }
-}
diff --git a/src/theory/model.h b/src/theory/model.h
index 3c6d8e116..8498b55e1 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -55,18 +55,13 @@ protected:
   /**
    * Get model value function.  This function is called by getValue
    */
-  Node getModelValue( TNode n );
-  /** get interpreted value
-    *  This function is called when the value of the node cannot be determined by the theory rewriter
-    *  This should function should return a representative in d_reps
-    */
-  virtual Node getInterpretedValue( TNode n );
+  Node getModelValue( TNode n ) const;
 public:
   /**
    * Get value function.  This should be called only after a ModelBuilder has called buildModel(...)
    * on this model.
    */
-  Node getValue( TNode n );
+  Node getValue( TNode n ) const;
 
   /** get existing domain value, with possible exclusions
     *   This function returns a term in d_rep_set.d_type_reps[tn] but not in exclude
@@ -113,9 +108,9 @@ public:
   bool areDisequal( Node a, Node b );
 public:
   /** get value function for Exprs. */
-  Expr getValue( Expr expr );
+  Expr getValue( Expr expr ) const;
   /** get cardinality for sort */
-  Cardinality getCardinality( Type t );
+  Cardinality getCardinality( Type t ) const;
 public:
   /** print representative debug function */
   void printRepresentativeDebug( const char* c, Node r );
@@ -238,7 +233,7 @@ private:
     return *(*it).second;
   }
 
-};    
+};
 
 /** TheoryEngineModelBuilder class
   *    This model builder will consult all theories in a theory engine for
@@ -254,8 +249,6 @@ protected:
 
   /** process build model */
   virtual void processBuildModel(TheoryModel* m, bool fullModel);
-  /** choose representative for unconstrained equivalence class */
-  virtual Node chooseRepresentative(TheoryModel* m, Node eqc, bool fullModel);
   /** normalize representative */
   Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps, bool evalOnly);
 public:
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 );
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 4a5bb2247..b7d2da713 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -29,12 +29,30 @@ void RepSet::clear(){
   d_tmap.clear();

 }

 

+int RepSet::getNumRepresentatives( TypeNode tn ) const{

+  std::map< TypeNode, std::vector< Node > >::const_iterator it = d_type_reps.find( tn );

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

+    return (int)it->second.size();

+  }else{

+    return 0;

+  }

+}

+

 void RepSet::add( Node n ){

   TypeNode t = n.getType();

   d_tmap[ n ] = (int)d_type_reps[t].size();

   d_type_reps[t].push_back( n );

 }

 

+int RepSet::getIndexFor( Node n ) const {

+  std::map< Node, int >::const_iterator it = d_tmap.find( n );

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

+    return it->second;

+  }else{

+    return -1;

+  }

+}

+

 void RepSet::complete( TypeNode t ){

   if( d_type_complete.find( t )==d_type_complete.end() ){

     d_type_complete[t] = true;

diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index 3427502b1..034ecea46 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -36,11 +36,13 @@ public:
   /** clear the set */

   void clear();

   /** has type */

-  bool hasType( TypeNode tn ) { return d_type_reps.find( tn )!=d_type_reps.end(); }

+  bool hasType( TypeNode tn ) const { return d_type_reps.find( tn )!=d_type_reps.end(); }

+  /** get cardinality for type */

+  int getNumRepresentatives( TypeNode tn ) const;

   /** add representative for type */

   void add( Node n );

   /** returns index in d_type_reps for node n */

-  int getIndexFor( Node n ) { return d_tmap.find( n )!=d_tmap.end() ? d_tmap[n] : -1; }

+  int getIndexFor( Node n ) const;

   /** complete all values */

   void complete( TypeNode t );

   /** debug print */