src/smt/boolean_terms.cpp

   1 /*********************                                                        */
   2 /*! \file boolean_terms.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 [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 #include "smt/boolean_terms.h"
  19 #include "smt/smt_engine.h"
  20 #include "theory/theory_engine.h"
  21 #include "theory/theory_model.h"
  22 #include "theory/booleans/boolean_term_conversion_mode.h"
  23 #include "theory/booleans/options.h"
  24 #include "expr/kind.h"
  25 #include "expr/node_manager_attributes.h"
  26 #include "util/ntuple.h"
  27 #include <string>
  28 #include <algorithm>
  29 #include <set>
  30 #include <map>
  31 #include <stack>
  32
  33 using namespace std;
  34 using namespace CVC4::theory;
  35 using namespace CVC4::theory::booleans;
  36
  37 namespace CVC4 {
  38 namespace smt {
  39
  40 BooleanTermConverter::BooleanTermConverter(SmtEngine& smt) :
  41   d_smt(smt),
  42   d_ff(),
  43   d_tt(),
  44   d_ffDt(),
  45   d_ttDt(),
  46   d_varCache(smt.d_userContext),
  47   d_termCache(smt.d_userContext),
  48   d_typeCache(),
  49   d_datatypeCache(),
  50   d_datatypeReverseCache() {
  51
  52   // set up our "false" and "true" conversions based on command-line option
  53   if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS ||
  54      options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_NATIVE) {
  55     d_ff = NodeManager::currentNM()->mkConst(BitVector(1u, 0u));
  56     d_tt = NodeManager::currentNM()->mkConst(BitVector(1u, 1u));
  57   }
  58   if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_BITVECTORS) {
  59     d_ffDt = d_ff;
  60     d_ttDt = d_tt;
  61   } else {
  62     Datatype spec("BooleanTerm");
  63     // don't change the order; false is assumed to come first by the model postprocessor
  64     spec.addConstructor(DatatypeConstructor("BT_False"));
  65     spec.addConstructor(DatatypeConstructor("BT_True"));
  66     const Datatype& dt = NodeManager::currentNM()->toExprManager()->mkDatatypeType(spec).getDatatype();
  67     d_ffDt = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt["BT_False"].getConstructor()));
  68     d_ttDt = NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, Node::fromExpr(dt["BT_True"].getConstructor()));
  69     // mark this datatype type as being special for Boolean term conversion
  70     TypeNode::fromType(dt.getDatatypeType()).setAttribute(BooleanTermAttr(), Node::null());
  71     if(options::booleanTermConversionMode() == BOOLEAN_TERM_CONVERT_TO_DATATYPES) {
  72       Assert(d_ff.isNull() && d_tt.isNull());
  73       d_ff = d_ffDt;
  74       d_tt = d_ttDt;
  75     }
  76   }
  77
  78   // assert that we set it up correctly
  79   Assert(!d_ff.isNull() && !d_tt.isNull());
  80   Assert(!d_ffDt.isNull() && !d_ttDt.isNull());
  81   Assert(d_ff != d_tt);
  82   Assert(d_ff.getType() == d_tt.getType());
  83   Assert(d_ffDt != d_ttDt);
  84   Assert(d_ffDt.getType() == d_ttDt.getType());
  85
  86 }/* BooleanTermConverter::BooleanTermConverter() */
  87
  88 static inline bool isBoolean(TNode top, unsigned i) {
  89   switch(top.getKind()) {
  90   case kind::NOT:
  91   case kind::AND:
  92   case kind::IFF:
  93   case kind::IMPLIES:
  94   case kind::OR:
  95   case kind::XOR:
  96   case kind::FORALL:
  97   case kind::EXISTS:
  98   case kind::REWRITE_RULE:
  99   case kind::RR_REWRITE:
 100   case kind::RR_DEDUCTION:
 101   case kind::RR_REDUCTION:
 102   case kind::INST_PATTERN:
 103     return true;
 104
 105   case kind::ITE:
 106     if(i == 0) {
 107       return true;
 108     }
 109     return top.getType().isBoolean();
 110
 111   default:
 112     return false;
 113   }
 114 }
 115
 116 // This function rewrites "in" as an "as"---this is actually expected
 117 // to be for model-substitution, so the "in" is a Boolean-term-converted
 118 // node, and "as" is the original.  See how it's used in function
 119 // handling, below.
 120 //
 121 // Note this isn't the case any longer, and parts of what's below have
 122 // been repurposed for *forward* conversion, meaning this works in either
 123 // direction.
 124 Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() {
 125   if(in.getType() == as) {
 126     return in;
 127   }
 128   if(in.getType().isBoolean()) {
 129     Assert(d_tt.getType() == as);
 130     return NodeManager::currentNM()->mkNode(kind::ITE, in, d_tt, d_ff);
 131   }
 132   if(as.isBoolean() && in.getType().isBitVector() && in.getType().getBitVectorSize() == 1) {
 133     return NodeManager::currentNM()->mkNode(kind::EQUAL, NodeManager::currentNM()->mkConst(BitVector(1u, 1u)), in);
 134   }
 135   if(in.getType().isDatatype()) {
 136     if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) {
 137       return NodeManager::currentNM()->mkNode(kind::EQUAL, d_ttDt, in);
 138     }
 139     Assert(as.isDatatype());
 140     const Datatype* dt2 = &as.getDatatype();
 141     const Datatype* dt1;
 142     if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) {
 143       dt1 = d_datatypeCache[dt2];
 144     } else {
 145       dt1 = d_datatypeReverseCache[dt2];
 146     }
 147     Assert(dt1 != NULL, "expected datatype in cache");
 148     Assert(*dt1 == in.getType().getDatatype(), "improper rewriteAs() between datatypes");
 149     Node out;
 150     for(size_t i = 0; i < dt1->getNumConstructors(); ++i) {
 151       DatatypeConstructor ctor = (*dt1)[i];
 152       NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR);
 153       appctorb << (*dt2)[i].getConstructor();
 154       for(size_t j = 0; j < ctor.getNumArgs(); ++j) {
 155         appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()));
 156       }
 157       Node appctor = appctorb;
 158       if(i == 0) {
 159         out = appctor;
 160       } else {
 161         Node newOut = NodeManager::currentNM()->mkNode(kind::ITE, ctor.getTester(), appctor, out);
 162         out = newOut;
 163       }
 164     }
 165     return out;
 166   }
 167   if(in.getType().isArray()) {
 168     // convert in to in'
 169     // e.g. in : (Array Int Bool)
 170     // for in' : (Array Int (_ BitVec 1))
 171     // then subs  in  |=>  \array_lambda ( \lambda (x:Int) . [convert (read a' x) x]
 172     Assert(as.isArray());
 173     Assert(as.getArrayIndexType() == in.getType().getArrayIndexType());
 174     Assert(as.getArrayConstituentType() != in.getType().getArrayConstituentType());
 175     Node x = NodeManager::currentNM()->mkBoundVar(as.getArrayIndexType());
 176     Node boundvars = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, x);
 177     Node sel = NodeManager::currentNM()->mkNode(kind::SELECT, in, x);
 178     Node selprime = rewriteAs(sel, as.getArrayConstituentType());
 179     Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundvars, selprime);
 180     Node out = NodeManager::currentNM()->mkNode(kind::ARRAY_LAMBDA, lam);
 181     Assert(out.getType() == as);
 182     return out;
 183   }
 184   if(in.getType().isParametricDatatype() &&
 185      in.getType().isInstantiatedDatatype()) {
 186     // We have something here like (Pair Bool Bool)---need to dig inside
 187     // and make it (Pair BV1 BV1)
 188     Assert(as.isParametricDatatype() && as.isInstantiatedDatatype());
 189     const Datatype* dt2 = &as[0].getDatatype();
 190     std::vector<TypeNode> fromParams, toParams;
 191     for(unsigned i = 0; i < dt2->getNumParameters(); ++i) {
 192       fromParams.push_back(TypeNode::fromType(dt2->getParameter(i)));
 193       toParams.push_back(as[i + 1]);
 194     }
 195     const Datatype* dt1;
 196     if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) {
 197       dt1 = d_datatypeCache[dt2];
 198     } else {
 199       dt1 = d_datatypeReverseCache[dt2];
 200     }
 201     Assert(dt1 != NULL, "expected datatype in cache");
 202     Assert(*dt1 == in.getType()[0].getDatatype(), "improper rewriteAs() between datatypes");
 203     Node out;
 204     for(size_t i = 0; i < dt1->getNumConstructors(); ++i) {
 205       DatatypeConstructor ctor = (*dt1)[i];
 206       NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR);
 207       appctorb << (*dt2)[i].getConstructor();
 208       for(size_t j = 0; j < ctor.getNumArgs(); ++j) {
 209         TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType());
 210         asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end());
 211         appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), asType);
 212       }
 213       Node appctor = appctorb;
 214       if(i == 0) {
 215         out = appctor;
 216       } else {
 217         Node newOut = NodeManager::currentNM()->mkNode(kind::ITE, ctor.getTester(), appctor, out);
 218         out = newOut;
 219       }
 220     }
 221     return out;
 222   }
 223
 224   Unhandled(in);
 225 }
 226
 227 const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw() {
 228   const Datatype*& out = d_datatypeCache[&dt];
 229   if(out != NULL) {
 230     return *out;
 231   }
 232
 233   Debug("boolean-terms") << "convertDatatype: considering " << dt.getName() << endl;
 234   for(Datatype::const_iterator c = dt.begin(); c != dt.end(); ++c) {
 235     TypeNode t = TypeNode::fromType((*c).getConstructor().getType());
 236     for(TypeNode::const_iterator a = t.begin(); a != t.end(); ++a) {
 237       TypeNode converted = convertType(*a, true);
 238       Debug("boolean-terms") << "GOT: " << converted << ":" << converted.getId() << endl;
 239       if(*a != converted) {
 240         SortConstructorType mySelfType;
 241         set<Type> unresolvedTypes;
 242         if(dt.isParametric()) {
 243           mySelfType = NodeManager::currentNM()->toExprManager()->mkSortConstructor(dt.getName() + "'", dt.getNumParameters());
 244           unresolvedTypes.insert(mySelfType);
 245         }
 246         vector<Datatype> newDtVector;
 247         if(dt.isParametric()) {
 248           newDtVector.push_back(Datatype(dt.getName() + "'", dt.getParameters(), false));
 249         } else {
 250           newDtVector.push_back(Datatype(dt.getName() + "'", false));
 251         }
 252         Datatype& newDt = newDtVector.front();
 253         Debug("boolean-terms") << "found a Boolean arg in constructor " << (*c).getName() << endl;
 254         for(c = dt.begin(); c != dt.end(); ++c) {
 255           DatatypeConstructor ctor((*c).getName() + "'", (*c).getTesterName() + "'");
 256           t = TypeNode::fromType((*c).getConstructor().getType());
 257           for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) {
 258             Type argType = (*a).getType().getRangeType();
 259             if(argType.isDatatype() && DatatypeType(argType).getDatatype() == dt) {
 260               Debug("boolean-terms") << "argtype " << argType << " is self" << endl;
 261               if(dt.isParametric()) {
 262                 Debug("boolean-terms") << "is-parametric self is " << mySelfType << endl;
 263                 ctor.addArg((*a).getName() + "'", mySelfType.instantiate(DatatypeType(argType).getDatatype().getParameters()));
 264               } else {
 265                 ctor.addArg((*a).getName() + "'", DatatypeSelfType());
 266               }
 267             } else {
 268               Debug("boolean-terms") << "argtype " << argType << " is NOT self" << endl;
 269               converted = convertType(TypeNode::fromType(argType), true);
 270               if(TypeNode::fromType(argType) != converted) {
 271                 ctor.addArg((*a).getName() + "'", converted.toType());
 272               } else {
 273                 ctor.addArg((*a).getName() + "'", argType);
 274               }
 275             }
 276           }
 277           newDt.addConstructor(ctor);
 278         }
 279         vector<DatatypeType> newDttVector =
 280           NodeManager::currentNM()->toExprManager()->mkMutualDatatypeTypes(newDtVector, unresolvedTypes);
 281         DatatypeType& newDtt = newDttVector.front();
 282         const Datatype& newD = newDtt.getDatatype();
 283         for(c = dt.begin(); c != dt.end(); ++c) {
 284           Debug("boolean-terms") << "constructor " << (*c).getConstructor() << ":" << (*c).getConstructor().getType() << " made into " << newD[(*c).getName() + "'"].getConstructor() << ":" << newD[(*c).getName() + "'"].getConstructor().getType() << endl;
 285           const DatatypeConstructor *newC;
 286           Node::fromExpr((*(newC = &newD[(*c).getName() + "'"])).getConstructor()).setAttribute(BooleanTermAttr(), Node::fromExpr((*c).getConstructor()));// other attr?
 287           Debug("boolean-terms") << "mapped " << newD[(*c).getName() + "'"].getConstructor() << " to " << (*c).getConstructor() << endl;
 288           d_varCache[Node::fromExpr((*c).getConstructor())] = Node::fromExpr(newD[(*c).getName() + "'"].getConstructor());
 289           d_varCache[Node::fromExpr((*c).getTester())] = Node::fromExpr(newD[(*c).getName() + "'"].getTester());
 290           for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) {
 291             Node::fromExpr((*newC)[(*a).getName() + "'"].getSelector()).setAttribute(BooleanTermAttr(), Node::fromExpr((*a).getSelector()));// other attr?
 292             d_varCache[Node::fromExpr((*a).getSelector())] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'"));
 293           }
 294         }
 295         out = &newD;
 296         d_datatypeReverseCache[&newD] = &dt;
 297         return newD;
 298       }
 299     }
 300   }
 301
 302   // this is identity; don't need the reverse cache
 303   out = &dt;
 304   return dt;
 305
 306 }/* BooleanTermConverter::convertDatatype() */
 307
 308 TypeNode BooleanTermConverter::convertType(TypeNode type, bool datatypesContext) {
 309   Debug("boolean-terms") << "CONVERT-TYPE[" << type << ":" << type.getId() << ", " << datatypesContext << "]" << endl;
 310   // This function recursively converts the type.
 311   if(type.isBoolean()) {
 312     return datatypesContext ? d_ttDt.getType() : d_tt.getType();
 313   }
 314   const pair<TypeNode, bool> cacheKey(type, datatypesContext);
 315   if(d_typeCache.find(cacheKey) != d_typeCache.end()) {
 316     TypeNode out = d_typeCache[cacheKey];
 317     return out.isNull() ? type : out;
 318   }
 319   TypeNode& outNode = d_typeCache[cacheKey];
 320   if(type.getKind() == kind::DATATYPE_TYPE ||
 321      type.getKind() == kind::PARAMETRIC_DATATYPE) {
 322     bool parametric = (type.getKind() == kind::PARAMETRIC_DATATYPE);
 323     const Datatype& dt = parametric ? type[0].getConst<Datatype>() : type.getConst<Datatype>();
 324     TypeNode out = TypeNode::fromType(convertDatatype(dt).getDatatypeType());
 325     Debug("boolean-terms") << "AFTER, got "<< out << " param:" << parametric << endl;
 326     if(parametric) {
 327       // re-parameterize the translation
 328       vector<TypeNode> params = type.getParamTypes();
 329       for(size_t i = 0; i < params.size(); ++i) {
 330         Debug("boolean-terms") << "in loop, got "<< params[i] << endl;
 331         params[i] = convertType(params[i], true);
 332         Debug("boolean-terms") << "in loop, convert to "<< params[i] << endl;
 333       }
 334       params.insert(params.begin(), out[0]);
 335       out = NodeManager::currentNM()->mkTypeNode(kind::PARAMETRIC_DATATYPE, params);
 336       Debug("boolean-terms") << "got OUT: " << out << endl;
 337     }
 338     if(out != type) {
 339       outNode = out;// cache it
 340       Debug("boolean-terms") << "OUT is same as TYPE" << endl;
 341     } else Debug("boolean-terms") << "OUT is DIFFERENT FROM TYPE" << endl;
 342     return out;
 343   }
 344   if(type.isRecord()) {
 345     const Record& rec = type.getConst<Record>();
 346     vector< pair<string, Type> > flds;
 347     for(Record::const_iterator i = rec.begin(); i != rec.end(); ++i) {
 348       TypeNode converted = convertType(TypeNode::fromType((*i).second), true);
 349       if(TypeNode::fromType((*i).second) != converted) {
 350         flds.push_back(make_pair((*i).first, converted.toType()));
 351       } else {
 352         flds.push_back(*i);
 353       }
 354     }
 355     TypeNode newRec = NodeManager::currentNM()->mkRecordType(Record(flds));
 356     Debug("tuprec") << "converted " << type << " to " << newRec << endl;
 357     if(newRec != type) {
 358       outNode = newRec;// cache it
 359     }
 360     return newRec;
 361   }
 362   if(!type.isSort() && type.getNumChildren() > 0) {
 363     Debug("boolean-terms") << "here at A for " << type << ":" << type.getId() << endl;
 364     // This should handle tuples and arrays ok.
 365     // Might handle function types too, but they can't go
 366     // in other types, so it doesn't matter.
 367     NodeBuilder<> b(type.getKind());
 368     if(type.getMetaKind() == kind::metakind::PARAMETERIZED) {
 369       b << type.getOperator();
 370     }
 371     for(TypeNode::iterator i = type.begin(); i != type.end(); ++i) {
 372       b << convertType(*i, false);
 373     }
 374     TypeNode out = b;
 375     if(out != type) {
 376       outNode = out;// cache it
 377     }
 378     Debug("boolean-terms") << "here at B, returning " << out << ":" << out.getId() << endl;
 379     return out;
 380   }
 381   // leave the cache at Null
 382   return type;
 383 }/* BooleanTermConverter::convertType() */
 384
 385 // look for vars from "vars" that occur in a term-context in n; transfer them to output.
 386 static void collectVarsInTermContext(TNode n, std::set<TNode>& vars, std::set<TNode>& output, bool boolParent, std::hash_set< std::pair<TNode, bool>, PairHashFunction<TNode, bool, TNodeHashFunction, BoolHashFunction> >& alreadySeen) {
 387   if(vars.empty()) {
 388     return;
 389   }
 390   const pair<TNode, bool> cacheKey(n, boolParent);
 391   if(alreadySeen.find(cacheKey) != alreadySeen.end()) {
 392     return;
 393   }
 394   alreadySeen.insert(cacheKey);
 395
 396   if(n.isVar() && vars.find(n) != vars.end() && !boolParent) {
 397     vars.erase(n);
 398     output.insert(n);
 399     if(vars.empty()) {
 400       return;
 401     }
 402   }
 403   for(size_t i = 0; i < n.getNumChildren(); ++i) {
 404     collectVarsInTermContext(n[i], vars, output, isBoolean(n, i), alreadySeen);
 405     if(vars.empty()) {
 406       return;
 407     }
 408   }
 409 }
 410
 411 Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId parentTheory, std::map<TNode, Node>& quantBoolVars) throw() {
 412
 413   stack< triple<TNode, theory::TheoryId, bool> > worklist;
 414   worklist.push(triple<TNode, theory::TheoryId, bool>(top, parentTheory, false));
 415   stack< NodeBuilder<> > result;
 416   result.push(NodeBuilder<>(kind::TUPLE));
 417
 418   NodeManager* nm = NodeManager::currentNM();
 419
 420   while(!worklist.empty()) {
 421     top = worklist.top().first;
 422     parentTheory = worklist.top().second;
 423     bool& childrenPushed = worklist.top().third;
 424
 425     Kind k = top.getKind();
 426     kind::MetaKind mk = top.getMetaKind();
 427
 428     // we only distinguish between datatypes, booleans, and "other", and we
 429     // don't even distinguish datatypes except when in "native" conversion
 430     // mode
 431     if(parentTheory != theory::THEORY_BOOL) {
 432       if(options::booleanTermConversionMode() != BOOLEAN_TERM_CONVERT_NATIVE ||
 433          parentTheory != theory::THEORY_DATATYPES) {
 434         parentTheory = theory::THEORY_BUILTIN;
 435       }
 436     }
 437
 438     if(!childrenPushed) {
 439       Debug("boolean-terms") << "rewriteBooleanTermsRec: " << top << " - parentTheory=" << parentTheory << endl;
 440
 441       BooleanTermVarCache::iterator i = d_varCache.find(top);
 442       if(i != d_varCache.end()) {
 443         result.top() << ((*i).second.isNull() ? Node(top) : (*i).second);
 444         worklist.pop();
 445         goto next_worklist;
 446       }
 447       BooleanTermCache::iterator j = d_termCache.find(pair<Node, theory::TheoryId>(top, parentTheory));
 448       if(j != d_termCache.end()) {
 449         result.top() << ((*j).second.isNull() ? Node(top) : (*j).second);
 450         worklist.pop();
 451         goto next_worklist;
 452       }
 453
 454       if(quantBoolVars.find(top) != quantBoolVars.end()) {
 455         // this Bool variable is quantified over and we're changing it to a BitVector var
 456         if(parentTheory == theory::THEORY_BOOL) {
 457           result.top() << quantBoolVars[top].eqNode(d_tt);
 458         } else {
 459           result.top() << quantBoolVars[top];
 460         }
 461         worklist.pop();
 462         goto next_worklist;
 463       }
 464
 465       if(parentTheory != theory::THEORY_BOOL && top.getType().isBoolean()) {
 466         // still need to rewrite e.g. function applications over boolean
 467         Node topRewritten = rewriteBooleanTermsRec(top, theory::THEORY_BOOL, quantBoolVars);
 468         Node n;
 469         if(parentTheory == theory::THEORY_DATATYPES) {
 470           n = nm->mkNode(kind::ITE, topRewritten, d_ttDt, d_ffDt);
 471         } else {
 472           n = nm->mkNode(kind::ITE, topRewritten, d_tt, d_ff);
 473         }
 474         Debug("boolean-terms") << "constructed ITE: " << n << endl;
 475         result.top() << n;
 476         worklist.pop();
 477         goto next_worklist;
 478       }
 479
 480       if(mk == kind::metakind::CONSTANT) {
 481         if(k == kind::STORE_ALL) {
 482           const ArrayStoreAll& asa = top.getConst<ArrayStoreAll>();
 483           ArrayType arrType = asa.getType();
 484           TypeNode indexType = TypeNode::fromType(arrType.getIndexType());
 485           Type constituentType = arrType.getConstituentType();
 486           if(constituentType.isBoolean()) {
 487             // we have store_all(true) or store_all(false)
 488             // just turn it into store_all(1) or store_all(0)
 489             if(indexType.isBoolean()) {
 490               // change index type to BV(1) also
 491               indexType = d_tt.getType();
 492             }
 493             ArrayStoreAll asaRepl(nm->mkArrayType(indexType, d_tt.getType()).toType(),
 494                                   (asa.getExpr().getConst<bool>() ? d_tt : d_ff).toExpr());
 495             Node n = nm->mkConst(asaRepl);
 496             Debug("boolean-terms") << " returning new store_all: " << n << endl;
 497             result.top() << n;
 498             worklist.pop();
 499             goto next_worklist;
 500           }
 501           if(indexType.isBoolean()) {
 502             // must change index type to BV(1)
 503             indexType = d_tt.getType();
 504             ArrayStoreAll asaRepl(nm->mkArrayType(indexType, TypeNode::fromType(constituentType)).toType(), asa.getExpr());
 505             Node n = nm->mkConst(asaRepl);
 506             Debug("boolean-terms") << " returning new store_all: " << n << endl;
 507             result.top() << n;
 508             worklist.pop();
 509             goto next_worklist;
 510           }
 511         }
 512         result.top() << top;
 513         worklist.pop();
 514         goto next_worklist;
 515       } else if(mk == kind::metakind::VARIABLE) {
 516         TypeNode t = top.getType();
 517         if(t.isFunction()) {
 518           for(unsigned i = 0; i < t.getNumChildren(); ++i) {
 519             TypeNode newType = convertType(t[i], false);
 520             // is this the return type?  (allowed to be Bool)
 521             bool returnType = (i == t.getNumChildren() - 1);
 522             if(newType != t[i] && (!t[i].isBoolean() || !returnType)) {
 523               vector<TypeNode> argTypes = t.getArgTypes();
 524               for(unsigned j = 0; j < argTypes.size(); ++j) {
 525                 argTypes[j] = convertType(argTypes[j], false);
 526               }
 527               TypeNode rangeType = t.getRangeType();
 528               if(!rangeType.isBoolean()) {
 529                 rangeType = convertType(rangeType, false);
 530               }
 531               TypeNode newType = nm->mkFunctionType(argTypes, rangeType);
 532               Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "__boolterm__",
 533                                     newType, "a function introduced by Boolean-term conversion",
 534                                     NodeManager::SKOLEM_EXACT_NAME);
 535               Debug("boolean-terms") << "constructed func: " << n << " of type " << newType << endl;
 536               top.setAttribute(BooleanTermAttr(), n);
 537               NodeBuilder<> boundVarsBuilder(kind::BOUND_VAR_LIST);
 538               NodeBuilder<> bodyBuilder(kind::APPLY_UF);
 539               bodyBuilder << n;
 540               for(unsigned j = 0; j < t.getNumChildren() - 1; ++j) {
 541                 Node var = nm->mkBoundVar(t[j]);
 542                 boundVarsBuilder << var;
 543                 if(t[j] != argTypes[j]) {
 544                   bodyBuilder << rewriteAs(var, argTypes[j]);
 545                 } else {
 546                   bodyBuilder << var;
 547                 }
 548               }
 549               Node boundVars = boundVarsBuilder;
 550               Node body = bodyBuilder;
 551               if(t.getRangeType() != rangeType) {
 552                 Node convbody = rewriteAs(body, t.getRangeType());
 553                 body = convbody;
 554               }
 555               Node lam = nm->mkNode(kind::LAMBDA, boundVars, body);
 556               Debug("boolean-terms") << "substituting " << top << " ==> " << lam << endl;
 557               d_smt.d_theoryEngine->getModel()->addSubstitution(top, lam);
 558               d_varCache[top] = n;
 559               result.top() << n;
 560               worklist.pop();
 561               goto next_worklist;
 562             }
 563           }
 564         } else if(t.isArray()) {
 565           TypeNode indexType = convertType(t.getArrayIndexType(), false);
 566           TypeNode constituentType = convertType(t.getArrayConstituentType(), false);
 567           if(indexType != t.getArrayIndexType() && constituentType == t.getArrayConstituentType()) {
 568             TypeNode newType = nm->mkArrayType(indexType, constituentType);
 569             Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
 570                                   newType, "an array variable introduced by Boolean-term conversion",
 571                                   NodeManager::SKOLEM_EXACT_NAME);
 572             top.setAttribute(BooleanTermAttr(), n);
 573             Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
 574             Node n_ff = nm->mkNode(kind::SELECT, n, d_ff);
 575             Node n_tt = nm->mkNode(kind::SELECT, n, d_tt);
 576             Node base = nm->mkConst(ArrayStoreAll(ArrayType(top.getType().toType()), (*TypeEnumerator(n_ff.getType())).toExpr()));
 577             Node repl = nm->mkNode(kind::STORE,
 578                                    nm->mkNode(kind::STORE, base, nm->mkConst(true),
 579                                               n_tt),
 580                                    nm->mkConst(false), n_ff);
 581             Debug("boolean-terms") << "array replacement: " << top << " => " << repl << endl;
 582             d_smt.d_theoryEngine->getModel()->addSubstitution(top, repl);
 583             d_varCache[top] = n;
 584             result.top() << n;
 585             worklist.pop();
 586             goto next_worklist;
 587           } else if(indexType == t.getArrayIndexType() && constituentType != t.getArrayConstituentType()) {
 588             TypeNode newType = nm->mkArrayType(indexType, constituentType);
 589             Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
 590                                   newType, "an array variable introduced by Boolean-term conversion",
 591                                   NodeManager::SKOLEM_EXACT_NAME);
 592             top.setAttribute(BooleanTermAttr(), n);
 593             Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
 594             d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
 595             d_varCache[top] = n;
 596             result.top() << n;
 597             worklist.pop();
 598             goto next_worklist;
 599           } else if(indexType != t.getArrayIndexType() && constituentType != t.getArrayConstituentType()) {
 600             TypeNode newType = nm->mkArrayType(indexType, constituentType);
 601             Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
 602                                   newType, "an array variable introduced by Boolean-term conversion",
 603                                   NodeManager::SKOLEM_EXACT_NAME);
 604             top.setAttribute(BooleanTermAttr(), n);
 605             Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
 606             Node n_ff = nm->mkNode(kind::SELECT, n, d_ff);
 607             Node n_tt = nm->mkNode(kind::SELECT, n, d_tt);
 608             Node base = nm->mkConst(ArrayStoreAll(ArrayType(top.getType().toType()), nm->mkConst(false).toExpr()));
 609             Node repl = nm->mkNode(kind::STORE,
 610                                    nm->mkNode(kind::STORE, base, nm->mkConst(false),
 611                                               nm->mkNode(kind::EQUAL, n_ff, d_tt)), nm->mkConst(true),
 612                                    nm->mkNode(kind::EQUAL, n_tt, d_tt));
 613             Debug("boolean-terms") << "array replacement: " << top << " => " << repl << endl;
 614             d_smt.d_theoryEngine->getModel()->addSubstitution(top, repl);
 615             d_varCache[top] = n;
 616             result.top() << n;
 617             worklist.pop();
 618             goto next_worklist;
 619           }
 620           d_varCache[top] = Node::null();
 621           result.top() << top;
 622           worklist.pop();
 623           goto next_worklist;
 624         } else if(t.isTuple() || t.isRecord()) {
 625           TypeNode newType = convertType(t, true);
 626           if(t != newType) {
 627             Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
 628                                   newType, "a tuple/record variable introduced by Boolean-term conversion",
 629                                   NodeManager::SKOLEM_EXACT_NAME);
 630             top.setAttribute(BooleanTermAttr(), n);
 631             n.setAttribute(BooleanTermAttr(), top);
 632             Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl;
 633             d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
 634             Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
 635             d_varCache[top] = n;
 636             result.top() << n;
 637             worklist.pop();
 638             goto next_worklist;
 639           }
 640           d_varCache[top] = Node::null();
 641           result.top() << top;
 642           worklist.pop();
 643           goto next_worklist;
 644         } else if(t.isDatatype() || t.isParametricDatatype()) {
 645           Debug("boolean-terms") << "found a var of datatype type" << endl;
 646           TypeNode newT = convertType(t, parentTheory == theory::THEORY_DATATYPES);
 647           if(t != newT) {
 648             Assert(d_varCache.find(top) == d_varCache.end(),
 649                    "Node `%s' already in cache ?!", top.toString().c_str());
 650             Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
 651                                   newT, "a datatype variable introduced by Boolean-term conversion",
 652                                   NodeManager::SKOLEM_EXACT_NAME);
 653             Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl;
 654             top.setAttribute(BooleanTermAttr(), n);
 655             d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
 656             Debug("boolean-terms") << "constructed: " << n << " of type " << newT << endl;
 657             d_varCache[top] = n;
 658             result.top() << n;
 659             worklist.pop();
 660             goto next_worklist;
 661           } else {
 662             d_varCache[top] = Node::null();
 663             result.top() << top;
 664             worklist.pop();
 665             goto next_worklist;
 666           }
 667         } else if(t.isConstructor()) {
 668           Assert(parentTheory != theory::THEORY_BOOL);
 669           Assert(t[t.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE ||
 670                  t[t.getNumChildren() - 1].getKind() == kind::PARAMETRIC_DATATYPE);
 671           const Datatype& dt = t[t.getNumChildren() - 1].getKind() == kind::DATATYPE_TYPE ?
 672             t[t.getNumChildren() - 1].getConst<Datatype>() :
 673             t[t.getNumChildren() - 1][0].getConst<Datatype>();
 674           TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES);
 675           const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst<Datatype>();
 676           if(dt != dt2) {
 677             Assert(d_varCache.find(top) != d_varCache.end(),
 678                    "constructor `%s' not in cache", top.toString().c_str());
 679             result.top() << d_varCache[top].get();
 680             worklist.pop();
 681             goto next_worklist;
 682           }
 683           d_varCache[top] = Node::null();
 684           result.top() << top;
 685           worklist.pop();
 686           goto next_worklist;
 687         } else if(t.isTester() || t.isSelector()) {
 688           Assert(parentTheory != theory::THEORY_BOOL);
 689           const Datatype& dt = t[0].getKind() == kind::DATATYPE_TYPE ?
 690             t[0].getConst<Datatype>() :
 691             t[0][0].getConst<Datatype>();
 692           TypeNode dt2type = convertType(TypeNode::fromType(dt.getDatatypeType()), parentTheory == theory::THEORY_DATATYPES);
 693           const Datatype& dt2 = (dt2type.getKind() == kind::DATATYPE_TYPE ? dt2type : dt2type[0]).getConst<Datatype>();
 694           if(dt != dt2) {
 695             Assert(d_varCache.find(top) != d_varCache.end(),
 696                    "tester or selector `%s' not in cache", top.toString().c_str());
 697             result.top() << d_varCache[top].get();
 698             worklist.pop();
 699             goto next_worklist;
 700           } else {
 701             d_varCache[top] = Node::null();
 702             result.top() << top;
 703             worklist.pop();
 704             goto next_worklist;
 705           }
 706         } else if(!t.isSort() && t.getNumChildren() > 0) {
 707           for(TypeNode::iterator i = t.begin(); i != t.end(); ++i) {
 708             if((*i).isBoolean()) {
 709               vector<TypeNode> argTypes(t.begin(), t.end());
 710               replace(argTypes.begin(), argTypes.end(), *i, d_tt.getType());
 711               TypeNode newType = nm->mkTypeNode(t.getKind(), argTypes);
 712               Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()),
 713                                     newType, "a variable introduced by Boolean-term conversion",
 714                                     NodeManager::SKOLEM_EXACT_NAME);
 715               Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
 716               top.setAttribute(BooleanTermAttr(), n);
 717               d_varCache[top] = n;
 718               result.top() << n;
 719               worklist.pop();
 720               goto next_worklist;
 721             }
 722           }
 723         }
 724         result.top() << top;
 725         worklist.pop();
 726         goto next_worklist;
 727       }
 728       switch(k) {
 729       case kind::BOUND_VAR_LIST:
 730         result.top() << top;
 731         worklist.pop();
 732         goto next_worklist;
 733
 734       case kind::REWRITE_RULE:
 735       case kind::RR_REWRITE:
 736       case kind::RR_DEDUCTION:
 737       case kind::RR_REDUCTION:
 738         // not yet supported
 739         result.top() << top;
 740         worklist.pop();
 741         goto next_worklist;
 742
 743       case kind::FORALL:
 744       case kind::EXISTS: {
 745         Debug("bt") << "looking at quantifier -> " << top << endl;
 746         set<TNode> ourVars;
 747         set<TNode> output;
 748         for(TNode::iterator i = top[0].begin(); i != top[0].end(); ++i) {
 749           if((*i).getType().isBoolean()) {
 750             ourVars.insert(*i);
 751           } else if(convertType((*i).getType(), false) != (*i).getType()) {
 752             output.insert(*i);
 753           }
 754         }
 755         if(ourVars.empty() && output.empty()) {
 756           // Simple case, quantifier doesn't quantify over Boolean vars,
 757           // no special handling needed for quantifier.  Fall through.
 758           Debug("bt") << "- quantifier simple case (1), no Boolean vars bound" << endl;
 759         } else {
 760           hash_set< pair<TNode, bool>, PairHashFunction<TNode, bool, TNodeHashFunction, BoolHashFunction> > alreadySeen;
 761           collectVarsInTermContext(top[1], ourVars, output, true, alreadySeen);
 762           if(output.empty()) {
 763             // Simple case, quantifier quantifies over Boolean vars, but they
 764             // don't occur in term context.  Fall through.
 765             Debug("bt") << "- quantifier simple case (2), Boolean vars bound but not used in term context" << endl;
 766           } else {
 767             Debug("bt") << "- quantifier case (3), Boolean vars bound and used in term context" << endl;
 768             // We have Boolean vars appearing in term context.  Convert their
 769             // types in the quantifier.
 770             for(set<TNode>::const_iterator i = output.begin(); i != output.end(); ++i) {
 771               Node newVar = nm->mkBoundVar((*i).toString(), convertType((*i).getType(), false));
 772               Assert(quantBoolVars.find(*i) == quantBoolVars.end(), "bad quantifier: shares a bound var with another quantifier (don't do that!)");
 773               quantBoolVars[*i] = newVar;
 774             }
 775             vector<TNode> boundVars;
 776             for(TNode::iterator i = top[0].begin(); i != top[0].end(); ++i) {
 777               map<TNode, Node>::const_iterator j = quantBoolVars.find(*i);
 778               if(j == quantBoolVars.end()) {
 779                 boundVars.push_back(*i);
 780               } else {
 781                 boundVars.push_back((*j).second);
 782               }
 783             }
 784             Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, boundVars);
 785             Node body = rewriteBooleanTermsRec(top[1], theory::THEORY_BOOL, quantBoolVars);
 786             Node quant = nm->mkNode(top.getKind(), boundVarList, body);
 787             Debug("bt") << "rewrote quantifier to -> " << quant << endl;
 788             d_termCache[make_pair(top, theory::THEORY_BOOL)] = quant;
 789             d_termCache[make_pair(top, theory::THEORY_BUILTIN)] = quant.iteNode(d_tt, d_ff);
 790             d_termCache[make_pair(top, theory::THEORY_DATATYPES)] = quant.iteNode(d_tt, d_ff);
 791             result.top() << quant;
 792             worklist.pop();
 793             goto next_worklist;
 794           }
 795         }
 796         /* intentional fall-through for some cases above */
 797       }
 798
 799       default:
 800         result.push(NodeBuilder<>(k));
 801         Debug("bt") << "looking at: " << top << endl;
 802         // rewrite the operator, as necessary
 803         if(mk == kind::metakind::PARAMETERIZED) {
 804           if(k == kind::RECORD) {
 805             result.top() << convertType(top.getType(), parentTheory == theory::THEORY_DATATYPES);
 806           } else if(k == kind::APPLY_TYPE_ASCRIPTION) {
 807             Node asc = nm->mkConst(AscriptionType(convertType(TypeNode::fromType(top.getOperator().getConst<AscriptionType>().getType()), parentTheory == theory::THEORY_DATATYPES).toType()));
 808             result.top() << asc;
 809             Debug("boolean-terms") << "setting " << top.getOperator() << ":" << top.getOperator().getId() << " to point to " << asc << ":" << asc.getId() << endl;
 810             asc.setAttribute(BooleanTermAttr(), top.getOperator());
 811           } else if(kindToTheoryId(k) != THEORY_BV &&
 812                     k != kind::TUPLE_SELECT &&
 813                     k != kind::TUPLE_UPDATE &&
 814                     k != kind::RECORD_SELECT &&
 815                     k != kind::RECORD_UPDATE &&
 816                     k != kind::DIVISIBLE) {
 817             Debug("bt") << "rewriting: " << top.getOperator() << endl;
 818             result.top() << rewriteBooleanTermsRec(top.getOperator(), theory::THEORY_BUILTIN, quantBoolVars);
 819             Debug("bt") << "got: " << result.top().getOperator() << endl;
 820           } else {
 821             result.top() << top.getOperator();
 822           }
 823         }
 824         // push children
 825         for(int i = top.getNumChildren() - 1; i >= 0; --i) {
 826           Debug("bt") << "rewriting: " << top[i] << endl;
 827           worklist.push(triple<TNode, theory::TheoryId, bool>(top[i], top.getKind() == kind::CHAIN ? parentTheory : (isBoolean(top, i) ? theory::THEORY_BOOL : (top.getKind() == kind::APPLY_CONSTRUCTOR ? theory::THEORY_DATATYPES : theory::THEORY_BUILTIN)), false));
 828           //b << rewriteBooleanTermsRec(top[i], isBoolean(top, i) ? , quantBoolVars);
 829           //Debug("bt") << "got: " << b[b.getNumChildren() - 1] << endl;
 830         }
 831         childrenPushed = true;
 832       }
 833     } else {
 834       Node n = result.top();
 835       result.pop();
 836       Debug("boolean-terms") << "constructed: " << n << endl;
 837       if(parentTheory == theory::THEORY_BOOL) {
 838         if(n.getType().isBitVector() &&
 839            n.getType().getBitVectorSize() == 1) {
 840           n = nm->mkNode(kind::EQUAL, n, d_tt);
 841         } else if(n.getType().isDatatype() &&
 842                   n.getType().hasAttribute(BooleanTermAttr())) {
 843           n = nm->mkNode(kind::EQUAL, n, d_ttDt);
 844         }
 845       }
 846       d_termCache[make_pair(top, parentTheory)] = n;
 847       result.top() << n;
 848       worklist.pop();
 849       goto next_worklist;
 850     }
 851
 852   next_worklist:
 853     ;
 854   }
 855
 856   Assert(worklist.size() == 0);
 857   Assert(result.size() == 1);
 858   Node retval = result.top()[0];
 859   result.top().clear();
 860   result.pop();
 861   return retval;
 862
 863 }/* BooleanTermConverter::rewriteBooleanTermsRec() */
 864
 865 }/* CVC4::smt namespace */
 866 }/* CVC4 namespace */