diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-12-11 16:38:00 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-12-11 16:38:00 -0600 |
commit | 147fd723e6c13eb3dd44a43073be03a64ea3fe66 (patch) | |
tree | 0a6eb33068ff609262566fa744a885cf4658a934 /src/theory/uf | |
parent | 1c114dc487d94d72ebf3453611c42b28777d6482 (diff) |
Remove alternate versions of mbqi (#2742)
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/theory_uf_model.cpp | 84 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_model.h | 39 |
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: |