src/theory/uf/theory_uf_model.cpp

   1 /*********************                                                        */
   2 /*! \file theory_uf_model.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Mathias Preiner
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Implementation of Theory UF Model
  13  **/
  14
  15 #include "theory/uf/theory_uf_model.h"
  16
  17 #include <stack>
  18 #include <vector>
  19
  20 #include "expr/attribute.h"
  21 #include "options/quantifiers_options.h"
  22 #include "theory/quantifiers/first_order_model.h"
  23 #include "theory/theory_engine.h"
  24 #include "theory/uf/equality_engine.h"
  25 #include "theory/uf/theory_uf.h"
  26
  27 using namespace std;
  28 using namespace CVC4;
  29 using namespace CVC4::kind;
  30 using namespace CVC4::context;
  31 using namespace CVC4::theory;
  32 using namespace CVC4::theory::uf;
  33
  34 //clear
  35 void UfModelTreeNode::clear(){
  36   d_data.clear();
  37   d_value = Node::null();
  38 }
  39
  40 //set value function
  41 void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int >& indexOrder, bool ground, int argIndex ){
  42   if( d_data.empty() ){
  43     //overwrite value if either at leaf or this is a fresh tree
  44     d_value = v;
  45   }else if( !d_value.isNull() && d_value!=v ){
  46     //value is no longer constant
  47     d_value = Node::null();
  48   }
  49   if( argIndex<(int)indexOrder.size() ){
  50     //take r = null when argument is the model basis
  51     Node r;
  52     if( ground || ( !n.isNull() && !n[ indexOrder[argIndex] ].getAttribute(ModelBasisAttribute()) ) ){
  53       r = m->getRepresentative( n[ indexOrder[argIndex] ] );
  54     }
  55     d_data[ r ].setValue( m, n, v, indexOrder, ground, argIndex+1 );
  56   }
  57 }
  58
  59 Node UfModelTreeNode::getFunctionValue(std::vector<Node>& args, int index, Node argDefaultValue, bool simplify) {
  60   if(!d_data.empty()) {
  61     Node defaultValue = argDefaultValue;
  62     if(d_data.find(Node::null()) != d_data.end()) {
  63       defaultValue = d_data[Node::null()].getFunctionValue(args, index + 1, argDefaultValue, simplify);
  64     }
  65
  66     vector<Node> caseArgs;
  67     map<Node, Node> caseValues;
  68
  69     for(map< Node, UfModelTreeNode>::iterator it = d_data.begin(); it != d_data.end(); ++it) {
  70       if(!it->first.isNull()) {
  71         Node val = it->second.getFunctionValue(args, index + 1, defaultValue, simplify);
  72         caseArgs.push_back(it->first);
  73         caseValues[it->first] = val;
  74       }
  75     }
  76
  77     NodeManager* nm = NodeManager::currentNM();
  78     Node retNode = defaultValue;
  79
  80     if(!simplify) {
  81       // "non-simplifying" mode - expand function values to things like:
  82       //   IF      (x=0 AND y=0 AND z=0) THEN value1
  83       //   ELSE IF (x=0 AND y=0 AND z=1) THEN value2
  84       //   [...etc...]
  85       for(int i = (int)caseArgs.size() - 1; i >= 0; --i) {
  86         Node val = caseValues[ caseArgs[ i ] ];
  87         if(val.getKind() == ITE) {
  88           // use a stack to reverse the order, since we're traversing outside-in
  89           stack<TNode> stk;
  90           do {
  91             stk.push(val);
  92             val = val[2];
  93           } while(val.getKind() == ITE);
  94           AlwaysAssert(val == defaultValue)
  95               << "default values don't match when constructing function "
  96                  "definition!";
  97           while(!stk.empty()) {
  98             val = stk.top();
  99             stk.pop();
 100             retNode = nm->mkNode(ITE, nm->mkNode(AND, args[index].eqNode(caseArgs[i]), val[0]), val[1], retNode);
 101           }
 102         } else {
 103           retNode = nm->mkNode(ITE, args[index].eqNode(caseArgs[i]), caseValues[caseArgs[i]], retNode);
 104         }
 105       }
 106     } else {
 107       // "simplifying" mode - condense function values
 108       for(int i = (int)caseArgs.size() - 1; i >= 0; --i) {
 109         retNode = nm->mkNode(ITE, args[index].eqNode(caseArgs[i]), caseValues[caseArgs[i]], retNode);
 110       }
 111     }
 112     return retNode;
 113   } else {
 114     Assert(!d_value.isNull());
 115     return d_value;
 116   }
 117 }
 118
 119 //update function
 120 void UfModelTreeNode::update( TheoryModel* m ){
 121   if( !d_value.isNull() ){
 122     d_value = m->getRepresentative( d_value );
 123   }
 124   std::map< Node, UfModelTreeNode > old = d_data;
 125   d_data.clear();
 126   for( std::map< Node, UfModelTreeNode >::iterator it = old.begin(); it != old.end(); ++it ){
 127     Node rep = m->getRepresentative( it->first );
 128     d_data[ rep ] = it->second;
 129     d_data[ rep ].update( m );
 130   }
 131 }
 132
 133 //simplify function
 134 void UfModelTreeNode::simplify( Node op, Node defaultVal, int argIndex ){
 135   if( argIndex<(int)op.getType().getNumChildren()-1 ){
 136     std::vector< Node > eraseData;
 137     //first process the default argument
 138     Node r;
 139     std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
 140     if( it!=d_data.end() ){
 141       if( !defaultVal.isNull() && it->second.d_value==defaultVal ){
 142         eraseData.push_back( r );
 143       }else{
 144         it->second.simplify( op, defaultVal, argIndex+1 );
 145         if( !it->second.d_value.isNull() && it->second.isTotal( op, argIndex+1 ) ){
 146           defaultVal = it->second.d_value;
 147         }else{
 148           defaultVal = Node::null();
 149           if( it->second.isEmpty() ){
 150             eraseData.push_back( r );
 151           }
 152         }
 153       }
 154     }
 155     //now see if any children can be removed, and simplify the ones that cannot
 156     for (auto& kv : d_data)
 157     {
 158       if (!kv.first.isNull())
 159       {
 160         if (!defaultVal.isNull() && kv.second.d_value == defaultVal)
 161         {
 162           eraseData.push_back(kv.first);
 163         }
 164         else
 165         {
 166           kv.second.simplify(op, defaultVal, argIndex + 1);
 167           if (kv.second.isEmpty())
 168           {
 169             eraseData.push_back(kv.first);
 170           }
 171         }
 172       }
 173     }
 174     for( int i=0; i<(int)eraseData.size(); i++ ){
 175       d_data.erase( eraseData[i] );
 176     }
 177   }
 178 }
 179
 180 //is total function
 181 bool UfModelTreeNode::isTotal( Node op, int argIndex ){
 182   if( argIndex==(int)(op.getType().getNumChildren()-1) ){
 183     return !d_value.isNull();
 184   }else{
 185     Node r;
 186     std::map< Node, UfModelTreeNode >::iterator it = d_data.find( r );
 187     if( it!=d_data.end() ){
 188       return it->second.isTotal( op, argIndex+1 );
 189     }else{
 190       return false;
 191     }
 192   }
 193 }
 194
 195 void indent( std::ostream& out, int ind ){
 196   for( int i=0; i<ind; i++ ){
 197     out << " ";
 198   }
 199 }
 200
 201 void UfModelTreeNode::debugPrint( std::ostream& out, TheoryModel* m, std::vector< int >& indexOrder, int ind, int arg ){
 202   if( !d_data.empty() ){
 203     for( std::map< Node, UfModelTreeNode >::iterator it = d_data.begin(); it != d_data.end(); ++it ){
 204       if( !it->first.isNull() ){
 205         indent( out, ind );
 206         out << "if x_" << indexOrder[arg] << " == " << it->first << std::endl;
 207         it->second.debugPrint( out, m, indexOrder, ind+2, arg+1 );
 208       }
 209     }
 210     if( d_data.find( Node::null() )!=d_data.end() ){
 211       d_data[ Node::null() ].debugPrint( out, m, indexOrder, ind, arg+1 );
 212     }
 213   }else{
 214     indent( out, ind );
 215     out << "return ";
 216     out << m->getRepresentative(d_value);
 217     out << std::endl;
 218   }
 219 }
 220
 221 Node UfModelTree::getFunctionValue( std::vector< Node >& args, bool simplify ){
 222   Node body = d_tree.getFunctionValue( args, 0, Node::null(), simplify );
 223   if(simplify) {
 224     body = Rewriter::rewrite( body );
 225   }
 226   Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args);
 227   return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, body);
 228 }
 229
 230 Node UfModelTree::getFunctionValue( const char* argPrefix, bool simplify ){
 231   TypeNode type = d_op.getType();
 232   std::vector< Node > vars;
 233   for( size_t i=0; i<type.getNumChildren()-1; i++ ){
 234     std::stringstream ss;
 235     ss << argPrefix << (i+1);
 236     vars.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ) );
 237   }
 238   return getFunctionValue( vars, simplify );
 239 }