Remove alternate versions of mbqi (#2742)

2 files changed, 0 insertions, 123 deletions

diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index a3e058569..42847dfd4 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -37,17 +37,6 @@ void UfModelTreeNode::clear(){
   d_value = Node::null();
 }
 
-bool UfModelTreeNode::hasConcreteArgumentDefinition(){
-  if( d_data.size()>1 ){
-    return true;
-  }else if( d_data.empty() ){
-    return false;
-  }else{
-    Node r;
-    return d_data.find( r )==d_data.end();
-  }
-}
-
 //set value function
 void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ){
   if( d_data.empty() ){
@@ -67,75 +56,6 @@ void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int
   }
 }
 
-//get value function
-Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex ){
-  if( !d_value.isNull() && isTotal( n.getOperator(), argIndex ) ){
-    //Notice() << "Constant, return " << d_value << ", depIndex = " << argIndex << std::endl;
-    depIndex = argIndex;
-    return d_value;
-  }else{
-    Node val;
-    int childDepIndex[2] = { argIndex, argIndex };
-    for( int i=0; i<2; i++ ){
-      //first check the argument, then check default
-      Node r;
-      if( i==0 ){
-        r = m->getRepresentative( n[ indexOrder[argIndex] ] );
-      }
-      std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
-      if( it!=d_data.end() ){
-        val = it->second.getValue( m, n, indexOrder, childDepIndex[i], argIndex+1 );
-        if( !val.isNull() ){
-          break;
-        }
-      }else{
-        //argument is not a defined argument: thus, it depends on this argument
-        childDepIndex[i] = argIndex+1;
-      }
-    }
-    //update depIndex
-    depIndex = childDepIndex[0]>childDepIndex[1] ? childDepIndex[0] : childDepIndex[1];
-    //Notice() << "Return " << val << ", depIndex = " << depIndex;
-    //Notice() << " ( " << childDepIndex[0] << ", " << childDepIndex[1] << " )" << std::endl;
-    return val;
-  }
-}
-
-Node UfModelTreeNode::getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex ){
-  if( argIndex==(int)indexOrder.size() ){
-    return d_value;
-  }else{
-    Node val;
-    bool depArg = false;
-    //will try concrete value first, then default
-    for( int i=0; i<2; i++ ){
-      Node r;
-      if( i==0 ){
-        r = m->getRepresentative( n[ indexOrder[argIndex] ] );
-      }
-      std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
-      if( it!=d_data.end() ){
-        val = it->second.getValue( m, n, indexOrder, depIndex, argIndex+1 );
-        //we have found a value
-        if( !val.isNull() ){
-          if( i==0 ){
-            depArg = true;
-          }
-          break;
-        }
-      }
-    }
-    //it depends on this argument if we found it via concrete argument value,
-    // or if found by default/disequal from some concrete argument value(s).
-    if( depArg || hasConcreteArgumentDefinition() ){
-      if( std::find( depIndex.begin(), depIndex.end(), indexOrder[argIndex] )==depIndex.end() ){
-        depIndex.push_back( indexOrder[argIndex] );
-      }
-    }
-    return val;
-  }
-}
-
 Node UfModelTreeNode::getFunctionValue(std::vector<Node>& args, int index, Node argDefaultValue, bool simplify) {
   if(!d_data.empty()) {
     Node defaultValue = argDefaultValue;
@@ -264,10 +184,6 @@ bool UfModelTreeNode::isTotal( Node op, int argIndex ){
   }
 }
 
-Node UfModelTreeNode::getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex ){
-  return d_value;
-}
-
 void indent( std::ostream& out, int ind ){
   for( int i=0; i<ind; i++ ){
     out << " ";
diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index 201faccee..ac57bde27 100644
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -31,8 +31,6 @@ public:
   std::map< Node, UfModelTreeNode > d_data;
   /** the value of this tree node (if all paths lead to same value) */
   Node d_value;
-  /** has concrete argument defintion */
-  bool hasConcreteArgumentDefinition();
 public:
   //is this model tree empty?
   bool isEmpty() { return d_data.empty() && d_value.isNull(); }
@@ -40,11 +38,6 @@ public:
   void clear();
   /** setValue function */
   void setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex );
-  /**  getValue function */
-  Node getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int& depIndex, int argIndex );
-  Node getValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, std::vector< int >& depIndex, int argIndex );
-  /** getConstant Value function */
-  Node getConstantValue( TheoryModel* m, Node n, std::vector< int >& indexOrder, int argIndex );
   /** getFunctionValue */
   Node getFunctionValue( std::vector< Node >& args, int index, Node argDefaultValue, bool simplify = true );
   /** update function */
@@ -92,36 +85,6 @@ public:
   void setDefaultValue( TheoryModel* m, Node v ){
     d_tree.setValue( m, Node::null(), v, d_index_order, false, 0 );
   }
-  /**  getValue function
-    *
-    *  returns val, the value of ground term n
-    *  Say n is f( t_0...t_n )
-    *    depIndex is the index for which every term of the form f( t_0 ... t_depIndex, *,... * ) is equal to val
-    *    for example, if g( x_0, x_1, x_2 ) := lambda x_0 x_1 x_2. if( x_1==a ) b else c,
-    *      then g( a, a, a ) would return b with depIndex = 1
-    *
-    */
-  Node getValue( TheoryModel* m, Node n, int& depIndex ){
-    return d_tree.getValue( m, n, d_index_order, depIndex, 0 );
-  }
-  /** -> implementation incomplete */
-  Node getValue( TheoryModel* m, Node n, std::vector< int >& depIndex ){
-    return d_tree.getValue( m, n, d_index_order, depIndex, 0 );
-  }
-  /** getConstantValue function
-    *
-    * given term n, where n may contain "all value" arguments, aka model basis arguments
-    *   if n is null, then every argument of n is considered "all value"
-    * if n is constant for the entire domain specified by n, then this function returns the value of its domain
-    * otherwise, it returns null
-    * for example, say the term e represents "all values"
-    *   if f( x_0, x_1 ) := if( x_0 = a ) b else if( x_1 = a ) a else b,
-    *     then f( a, e ) would return b, while f( e, a ) would return null
-    *  -> implementation incomplete
-    */
-  Node getConstantValue( TheoryModel* m, Node n ) {
-    return d_tree.getConstantValue( m, n, d_index_order, 0 );
-  }
   /** getFunctionValue
     *   Returns a representation of this function.
     */
@@ -136,8 +99,6 @@ public:
   void simplify() { d_tree.simplify( d_op, Node::null(), 0 ); }
   /** is this tree total? */
   bool isTotal() { return d_tree.isTotal( d_op, 0 ); }
-  /** is this function constant? */
-  bool isConstant( TheoryModel* m ) { return !getConstantValue( m, Node::null() ).isNull(); }
   /** is this tree empty? */
   bool isEmpty() { return d_tree.isEmpty(); }
 public: