src/smt/model_postprocessor.cpp

   1 /*********************                                                        */
   2 /*! \file model_postprocessor.cpp
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): Andrew Reynolds
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief
  13  **
  14  **
  15  **/
  16
  17 #include "smt/model_postprocessor.h"
  18 #include "smt/boolean_terms.h"
  19 #include "expr/node_manager_attributes.h"
  20
  21 using namespace std;
  22 using namespace CVC4;
  23 using namespace CVC4::smt;
  24
  25 Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) {
  26   if(n.getType().isSubtypeOf(asType)) {
  27     // good to go, we have the right type
  28     return n;
  29   }
  30   if(n.getKind() == kind::LAMBDA) {
  31     Assert(asType.isFunction());
  32     Node rhs = rewriteAs(n[1], asType[1]);
  33     Node out = NodeManager::currentNM()->mkNode(kind::LAMBDA, n[0], rhs);
  34     Debug("boolean-terms") << "rewrote " << n << " as " << out << std::endl;
  35     Debug("boolean-terms") << "need type " << asType << endl;
  36     Assert(out.getType() == asType);
  37     return out;
  38   }
  39   if(!n.isConst()) {
  40     // we don't handle non-const right now
  41     return n;
  42   }
  43   if(asType.isBoolean()) {
  44     if(n.getType().isBitVector(1u)) {
  45       // type mismatch: should only happen for Boolean-term conversion under
  46       // datatype constructor applications; rewrite from BV(1) back to Boolean
  47       bool tf = (n.getConst<BitVector>().getValue() == 1);
  48       return NodeManager::currentNM()->mkConst(tf);
  49     }
  50     if(n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())) {
  51       // type mismatch: should only happen for Boolean-term conversion under
  52       // datatype constructor applications; rewrite from datatype back to Boolean
  53       Assert(n.getKind() == kind::APPLY_CONSTRUCTOR);
  54       Assert(n.getNumChildren() == 0);
  55       // we assume (by construction) false is first; see boolean_terms.cpp
  56       bool tf = (Datatype::indexOf(n.getOperator().toExpr()) == 1);
  57       Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << " ==> " << tf << endl;
  58       return NodeManager::currentNM()->mkConst(tf);
  59     }
  60   }
  61   if(n.getType().isBoolean()) {
  62     bool tf = n.getConst<bool>();
  63     if(asType.isBitVector(1u)) {
  64       return NodeManager::currentNM()->mkConst(BitVector(1u, tf ? 1u : 0u));
  65     }
  66     if(asType.isDatatype() && asType.hasAttribute(BooleanTermAttr())) {
  67       const Datatype& asDatatype = asType.getConst<Datatype>();
  68       return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, (tf ? asDatatype[0] : asDatatype[1]).getConstructor());
  69     }
  70   }
  71   if(n.getType().isRecord() && asType.isRecord()) {
  72     Debug("boolean-terms") << "+++ got a record - rewriteAs " << n << " : " << asType << endl;
  73     const Record& rec CVC4_UNUSED = n.getType().getConst<Record>();
  74     const Record& asRec = asType.getConst<Record>();
  75     Assert(rec.getNumFields() == asRec.getNumFields());
  76     Assert(n.getNumChildren() == asRec.getNumFields());
  77     NodeBuilder<> b(n.getKind());
  78     b << asType;
  79     for(size_t i = 0; i < n.getNumChildren(); ++i) {
  80       b << rewriteAs(n[i], TypeNode::fromType(asRec[i].second));
  81     }
  82     Node out = b;
  83     Debug("boolean-terms") << "+++ returning record " << out << endl;
  84     return out;
  85   }
  86   Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << endl;
  87   if(n.getType().isArray()) {
  88     Assert(asType.isArray());
  89     if(n.getKind() == kind::STORE) {
  90       return NodeManager::currentNM()->mkNode(kind::STORE,
  91                                               rewriteAs(n[0], asType),
  92                                               rewriteAs(n[1], asType[0]),
  93                                               rewriteAs(n[2], asType[1]));
  94     }
  95     Assert(n.getKind() == kind::STORE_ALL);
  96     const ArrayStoreAll& asa = n.getConst<ArrayStoreAll>();
  97     Node val = rewriteAs(asa.getExpr(), asType[1]);
  98     return NodeManager::currentNM()->mkConst(ArrayStoreAll(asType.toType(), val.toExpr()));
  99   }
 100   if(n.getType().isParametricDatatype() &&
 101      n.getType().isInstantiatedDatatype() &&
 102      asType.isParametricDatatype() &&
 103      asType.isInstantiatedDatatype() &&
 104      n.getType()[0] == asType[0]) {
 105     // Here, we're doing something like rewriting a (Pair BV1 BV1) as a
 106     // (Pair Bool Bool).
 107     const Datatype* dt2 = &asType[0].getDatatype();
 108     std::vector<TypeNode> fromParams, toParams;
 109     for(unsigned i = 0; i < dt2->getNumParameters(); ++i) {
 110       fromParams.push_back(TypeNode::fromType(dt2->getParameter(i)));
 111       toParams.push_back(asType[i + 1]);
 112     }
 113     Assert(dt2 == &Datatype::datatypeOf(n.getOperator().toExpr()));
 114     size_t ctor_ix = Datatype::indexOf(n.getOperator().toExpr());
 115     NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR);
 116     appctorb << (*dt2)[ctor_ix].getConstructor();
 117     for(size_t j = 0; j < n.getNumChildren(); ++j) {
 118       TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[ctor_ix][j].getSelector().getType()).getRangeType());
 119       asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end());
 120       appctorb << rewriteAs(n[j], asType);
 121     }
 122     Node out = appctorb;
 123     return out;
 124   }
 125   if(asType.getNumChildren() != n.getNumChildren() ||
 126      n.getMetaKind() == kind::metakind::CONSTANT) {
 127     return n;
 128   }
 129   NodeBuilder<> b(n.getKind());
 130   if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
 131     b << n.getOperator();
 132   }
 133   TypeNode::iterator t = asType.begin();
 134   for(TNode::iterator i = n.begin(); i != n.end(); ++i, ++t) {
 135     Assert(t != asType.end());
 136     b << rewriteAs(*i, *t);
 137   }
 138   Assert(t == asType.end());
 139   Debug("boolean-terms") << "+++ constructing " << b << endl;
 140   Node out = b;
 141   return out;
 142 }
 143
 144 void ModelPostprocessor::visit(TNode current, TNode parent) {
 145   Debug("tuprec") << "visiting " << current << endl;
 146   Assert(!alreadyVisited(current, TNode::null()));
 147   if(current.getType().hasAttribute(expr::DatatypeTupleAttr())) {
 148     Assert(current.getKind() == kind::APPLY_CONSTRUCTOR);
 149     TypeNode expectType = current.getType().getAttribute(expr::DatatypeTupleAttr());
 150     NodeBuilder<> b(kind::TUPLE);
 151     TypeNode::iterator t = expectType.begin();
 152     for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) {
 153       Assert(alreadyVisited(*i, TNode::null()));
 154       Assert(t != expectType.end());
 155       TNode n = d_nodes[*i];
 156       n = n.isNull() ? *i : n;
 157       if(!n.getType().isSubtypeOf(*t)) {
 158         Assert(n.getType().isBitVector(1u) ||
 159                (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())));
 160         Assert(n.isConst());
 161         Assert((*t).isBoolean());
 162         if(n.getType().isBitVector(1u)) {
 163           b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1));
 164         } else {
 165           // we assume (by construction) false is first; see boolean_terms.cpp
 166           b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1));
 167         }
 168       } else {
 169         b << n;
 170       }
 171     }
 172     Assert(t == expectType.end());
 173     d_nodes[current] = b;
 174     Debug("tuprec") << "returning " << d_nodes[current] << endl;
 175     // The assert below is too strong---we might be returning a model value but
 176     // expect a type that still uses datatypes for tuples/records.  If it's
 177     // really not the right type we should catch it in SmtEngine anyway.
 178     // Assert(d_nodes[current].getType() == expectType);
 179   } else if(current.getType().hasAttribute(expr::DatatypeRecordAttr())) {
 180     Assert(current.getKind() == kind::APPLY_CONSTRUCTOR);
 181     TypeNode expectType = current.getType().getAttribute(expr::DatatypeRecordAttr());
 182     const Record& expectRec = expectType.getConst<Record>();
 183     NodeBuilder<> b(kind::RECORD);
 184     b << current.getType().getAttribute(expr::DatatypeRecordAttr());
 185     Record::const_iterator t = expectRec.begin();
 186     for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) {
 187       Assert(alreadyVisited(*i, TNode::null()));
 188       Assert(t != expectRec.end());
 189       TNode n = d_nodes[*i];
 190       n = n.isNull() ? *i : n;
 191       if(!n.getType().isSubtypeOf(TypeNode::fromType((*t).second))) {
 192         Assert(n.getType().isBitVector(1u) ||
 193                (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())));
 194         Assert(n.isConst());
 195         Assert((*t).second.isBoolean());
 196         if(n.getType().isBitVector(1u)) {
 197           b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1));
 198         } else {
 199           // we assume (by construction) false is first; see boolean_terms.cpp
 200           b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1));
 201         }
 202       } else {
 203         b << n;
 204       }
 205     }
 206     Assert(t == expectRec.end());
 207     d_nodes[current] = b;
 208     Debug("tuprec") << "returning " << d_nodes[current] << endl;
 209     Assert(d_nodes[current].getType() == expectType);
 210   } else if(current.getKind() == kind::APPLY_CONSTRUCTOR &&
 211             ( current.getOperator().hasAttribute(BooleanTermAttr()) ||
 212               ( current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION &&
 213                 current.getOperator()[0].hasAttribute(BooleanTermAttr()) ) )) {
 214     NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
 215     Node realOp;
 216     if(current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION) {
 217       TNode oldAsc = current.getOperator().getOperator();
 218       Debug("boolean-terms") << "old asc: " << oldAsc << endl;
 219       Node newCons = current.getOperator()[0].getAttribute(BooleanTermAttr());
 220       Node newAsc = NodeManager::currentNM()->mkConst(AscriptionType(newCons.getType().toType()));
 221       Debug("boolean-terms") << "new asc: " << newAsc << endl;
 222       if(newCons.getType().getRangeType().isParametricDatatype()) {
 223         vector<TypeNode> oldParams = TypeNode::fromType(oldAsc.getConst<AscriptionType>().getType()).getRangeType().getParamTypes();
 224         vector<TypeNode> newParams = newCons.getType().getRangeType().getParamTypes();
 225         Assert(oldParams.size() == newParams.size() && oldParams.size() > 0);
 226         newAsc = NodeManager::currentNM()->mkConst(AscriptionType(newCons.getType().substitute(newParams.begin(), newParams.end(), oldParams.begin(), oldParams.end()).toType()));
 227       }
 228       realOp = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, newAsc, newCons);
 229     } else {
 230       realOp = current.getOperator().getAttribute(BooleanTermAttr());
 231     }
 232     b << realOp;
 233     Debug("boolean-terms") << "+ op " << b.getOperator() << endl;
 234     TypeNode::iterator j = realOp.getType().begin();
 235     for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++j) {
 236       Assert(j != realOp.getType().end());
 237       Assert(alreadyVisited(*i, TNode::null()));
 238       TNode repl = d_nodes[*i];
 239       repl = repl.isNull() ? *i : repl;
 240       Debug("boolean-terms") << "+ adding " << repl << " expecting " << *j << endl;
 241       b << rewriteAs(repl, *j);
 242     }
 243     Node n = b;
 244     Debug("boolean-terms") << "model-post: " << current << endl
 245                            << "- returning " << n << endl;
 246     d_nodes[current] = n;
 247   } else {
 248     // rewrite based on children
 249     bool self = true;
 250     for(size_t i = 0; i < current.getNumChildren(); ++i) {
 251       Assert(d_nodes.find(current[i]) != d_nodes.end());
 252       if(!d_nodes[current[i]].isNull()) {
 253         self = false;
 254         break;
 255       }
 256     }
 257     if(self) {
 258       Debug("tuprec") << "returning self for kind " << current.getKind() << endl;
 259       // rewrite to self
 260       d_nodes[current] = Node::null();
 261     } else {
 262       // rewrite based on children
 263       NodeBuilder<> nb(current.getKind());
 264       for(size_t i = 0; i < current.getNumChildren(); ++i) {
 265         Assert(d_nodes.find(current[i]) != d_nodes.end());
 266         TNode rw = d_nodes[current[i]];
 267         if(rw.isNull()) {
 268           rw = current[i];
 269         }
 270         nb << rw;
 271       }
 272       d_nodes[current] = nb;
 273       Debug("tuprec") << "rewrote children for kind " << current.getKind() << " got " << d_nodes[current] << endl;
 274     }
 275   }
 276 }/* ModelPostprocessor::visit() */