src/theory/quantifiers/sygus/term_database_sygus.cpp

   1 /*********************                                                        */
   2 /*! \file term_database_sygus.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Andres Noetzli
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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 term database sygus class
  13  **/
  14
  15 #include "theory/quantifiers/sygus/term_database_sygus.h"
  16
  17 #include "base/check.h"
  18 #include "expr/sygus_datatype.h"
  19 #include "options/base_options.h"
  20 #include "options/datatypes_options.h"
  21 #include "options/quantifiers_options.h"
  22 #include "printer/printer.h"
  23 #include "theory/arith/arith_msum.h"
  24 #include "theory/datatypes/theory_datatypes_utils.h"
  25 #include "theory/quantifiers/quantifiers_attributes.h"
  26 #include "theory/quantifiers/term_database.h"
  27 #include "theory/quantifiers/term_util.h"
  28 #include "theory/quantifiers_engine.h"
  29
  30 using namespace CVC4::kind;
  31
  32 namespace CVC4 {
  33 namespace theory {
  34 namespace quantifiers {
  35
  36 std::ostream& operator<<(std::ostream& os, EnumeratorRole r)
  37 {
  38   switch (r)
  39   {
  40     case ROLE_ENUM_POOL: os << "POOL"; break;
  41     case ROLE_ENUM_SINGLE_SOLUTION: os << "SINGLE_SOLUTION"; break;
  42     case ROLE_ENUM_MULTI_SOLUTION: os << "MULTI_SOLUTION"; break;
  43     case ROLE_ENUM_CONSTRAINED: os << "CONSTRAINED"; break;
  44     default: os << "enum_" << static_cast<unsigned>(r); break;
  45   }
  46   return os;
  47 }
  48
  49 TermDbSygus::TermDbSygus(context::Context* c, QuantifiersEngine* qe)
  50     : d_quantEngine(qe),
  51       d_syexp(new SygusExplain(this)),
  52       d_ext_rw(new ExtendedRewriter(true)),
  53       d_eval(new Evaluator),
  54       d_funDefEval(new FunDefEvaluator),
  55       d_eval_unfold(new SygusEvalUnfold(this))
  56 {
  57   d_true = NodeManager::currentNM()->mkConst( true );
  58   d_false = NodeManager::currentNM()->mkConst( false );
  59 }
  60
  61 bool TermDbSygus::reset( Theory::Effort e ) {
  62   return true;
  63 }
  64
  65 TNode TermDbSygus::getFreeVar( TypeNode tn, int i, bool useSygusType ) {
  66   unsigned sindex = 0;
  67   TypeNode vtn = tn;
  68   if( useSygusType ){
  69     if( tn.isDatatype() ){
  70       const DType& dt = tn.getDType();
  71       if( !dt.getSygusType().isNull() ){
  72         vtn = dt.getSygusType();
  73         sindex = 1;
  74       }
  75     }
  76   }
  77   while( i>=(int)d_fv[sindex][tn].size() ){
  78     std::stringstream ss;
  79     if( tn.isDatatype() ){
  80       const DType& dt = tn.getDType();
  81       ss << "fv_" << dt.getName() << "_" << i;
  82     }else{
  83       ss << "fv_" << tn << "_" << i;
  84     }
  85     Assert(!vtn.isNull());
  86     Node v = NodeManager::currentNM()->mkSkolem( ss.str(), vtn, "for sygus normal form testing" );
  87     d_fv_stype[v] = tn;
  88     d_fv_num[v] = i;
  89     d_fv[sindex][tn].push_back( v );
  90   }
  91   return d_fv[sindex][tn][i];
  92 }
  93
  94 TNode TermDbSygus::getFreeVarInc( TypeNode tn, std::map< TypeNode, int >& var_count, bool useSygusType ) {
  95   std::map< TypeNode, int >::iterator it = var_count.find( tn );
  96   if( it==var_count.end() ){
  97     var_count[tn] = 1;
  98     return getFreeVar( tn, 0, useSygusType );
  99   }else{
 100     int index = it->second;
 101     var_count[tn]++;
 102     return getFreeVar( tn, index, useSygusType );
 103   }
 104 }
 105
 106 bool TermDbSygus::hasFreeVar( Node n, std::map< Node, bool >& visited ){
 107   if( visited.find( n )==visited.end() ){
 108     visited[n] = true;
 109     if( isFreeVar( n ) ){
 110       return true;
 111     }
 112     for( unsigned i=0; i<n.getNumChildren(); i++ ){
 113       if( hasFreeVar( n[i], visited ) ){
 114         return true;
 115       }
 116     }
 117   }
 118   return false;
 119 }
 120
 121 bool TermDbSygus::hasFreeVar( Node n ) {
 122   std::map< Node, bool > visited;
 123   return hasFreeVar( n, visited );
 124 }
 125
 126 Node TermDbSygus::getProxyVariable(TypeNode tn, Node c)
 127 {
 128   Assert(tn.isDatatype());
 129   Assert(tn.getDType().isSygus());
 130   Assert(tn.getDType().getSygusType().isComparableTo(c.getType()));
 131
 132   std::map<Node, Node>::iterator it = d_proxy_vars[tn].find(c);
 133   if (it == d_proxy_vars[tn].end())
 134   {
 135     SygusTypeInfo& ti = getTypeInfo(tn);
 136     int anyC = ti.getAnyConstantConsNum();
 137     Node k;
 138     if (anyC == -1)
 139     {
 140       k = NodeManager::currentNM()->mkSkolem("sy", tn, "sygus proxy");
 141       SygusPrintProxyAttribute spa;
 142       k.setAttribute(spa, c);
 143     }
 144     else
 145     {
 146       const DType& dt = tn.getDType();
 147       k = NodeManager::currentNM()->mkNode(
 148           APPLY_CONSTRUCTOR, dt[anyC].getConstructor(), c);
 149     }
 150     d_proxy_vars[tn][c] = k;
 151     return k;
 152   }
 153   return it->second;
 154 }
 155
 156 TypeNode TermDbSygus::getSygusTypeForVar( Node v ) {
 157   Assert(d_fv_stype.find(v) != d_fv_stype.end());
 158   return d_fv_stype[v];
 159 }
 160
 161 Node TermDbSygus::mkGeneric(const DType& dt,
 162                             unsigned c,
 163                             std::map<TypeNode, int>& var_count,
 164                             std::map<int, Node>& pre,
 165                             bool doBetaRed)
 166 {
 167   Assert(c < dt.getNumConstructors());
 168   Assert(dt.isSygus());
 169   Assert(!dt[c].getSygusOp().isNull());
 170   std::vector< Node > children;
 171   Trace("sygus-db-debug") << "mkGeneric " << dt.getName() << " " << c << "..."
 172                           << std::endl;
 173   for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++)
 174   {
 175     Node a;
 176     std::map< int, Node >::iterator it = pre.find( i );
 177     if( it!=pre.end() ){
 178       a = it->second;
 179       Trace("sygus-db-debug") << "From pre: " << a << std::endl;
 180     }else{
 181       TypeNode tna = dt[c].getArgType(i);
 182       a = getFreeVarInc( tna, var_count, true );
 183     }
 184     Trace("sygus-db-debug")
 185         << "  child " << i << " : " << a << " : " << a.getType() << std::endl;
 186     Assert(!a.isNull());
 187     children.push_back( a );
 188   }
 189   Node ret = datatypes::utils::mkSygusTerm(dt, c, children, doBetaRed);
 190   Trace("sygus-db-debug") << "mkGeneric returns " << ret << std::endl;
 191   return ret;
 192 }
 193
 194 Node TermDbSygus::mkGeneric(const DType& dt,
 195                             int c,
 196                             std::map<int, Node>& pre,
 197                             bool doBetaRed)
 198 {
 199   std::map<TypeNode, int> var_count;
 200   return mkGeneric(dt, c, var_count, pre, doBetaRed);
 201 }
 202
 203 Node TermDbSygus::mkGeneric(const DType& dt, int c, bool doBetaRed)
 204 {
 205   std::map<int, Node> pre;
 206   return mkGeneric(dt, c, pre, doBetaRed);
 207 }
 208
 209 struct CanonizeBuiltinAttributeId
 210 {
 211 };
 212 using CanonizeBuiltinAttribute =
 213     expr::Attribute<CanonizeBuiltinAttributeId, Node>;
 214
 215 Node TermDbSygus::canonizeBuiltin(Node n)
 216 {
 217   std::map<TypeNode, int> var_count;
 218   return canonizeBuiltin(n, var_count);
 219 }
 220
 221 Node TermDbSygus::canonizeBuiltin(Node n, std::map<TypeNode, int>& var_count)
 222 {
 223   // has it already been computed?
 224   if (var_count.empty() && n.hasAttribute(CanonizeBuiltinAttribute()))
 225   {
 226     Node ret = n.getAttribute(CanonizeBuiltinAttribute());
 227     Trace("sygus-db-canon") << "cached " << n << " : " << ret << "\n";
 228     return ret;
 229   }
 230   Trace("sygus-db-canon") << "  CanonizeBuiltin : compute for " << n << "\n";
 231   Node ret = n;
 232   // it is symbolic if it represents "any constant"
 233   if (n.getKind() == APPLY_SELECTOR_TOTAL)
 234   {
 235     ret = getFreeVarInc(n[0].getType(), var_count, true);
 236   }
 237   else if (n.getKind() != APPLY_CONSTRUCTOR)
 238   {
 239     ret = n;
 240   }
 241   else
 242   {
 243     Assert(n.getKind() == APPLY_CONSTRUCTOR);
 244     bool childChanged = false;
 245     std::vector<Node> children;
 246     children.push_back(n.getOperator());
 247     for (unsigned j = 0, size = n.getNumChildren(); j < size; ++j)
 248     {
 249       Node child = canonizeBuiltin(n[j], var_count);
 250       children.push_back(child);
 251       childChanged = childChanged || child != n[j];
 252     }
 253     if (childChanged)
 254     {
 255       ret = NodeManager::currentNM()->mkNode(APPLY_CONSTRUCTOR, children);
 256     }
 257   }
 258   // cache if we had a fresh variable count
 259   if (var_count.empty())
 260   {
 261     n.setAttribute(CanonizeBuiltinAttribute(), ret);
 262   }
 263   Trace("sygus-db-canon") << "  ...normalized " << n << " --> " << ret
 264                           << std::endl;
 265   Assert(ret.getType().isComparableTo(n.getType()));
 266   return ret;
 267 }
 268
 269 struct SygusToBuiltinAttributeId
 270 {
 271 };
 272 typedef expr::Attribute<SygusToBuiltinAttributeId, Node>
 273     SygusToBuiltinAttribute;
 274
 275 Node TermDbSygus::sygusToBuiltin(Node n, TypeNode tn)
 276 {
 277   if (n.isConst())
 278   {
 279     // if its a constant, we use the datatype utility version
 280     return datatypes::utils::sygusToBuiltin(n);
 281   }
 282   Assert(n.getType().isComparableTo(tn));
 283   if (!tn.isDatatype())
 284   {
 285     return n;
 286   }
 287   // has it already been computed?
 288   if (n.hasAttribute(SygusToBuiltinAttribute()))
 289   {
 290     return n.getAttribute(SygusToBuiltinAttribute());
 291   }
 292   Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n
 293                           << ", type = " << tn << std::endl;
 294   const DType& dt = tn.getDType();
 295   if (!dt.isSygus())
 296   {
 297     return n;
 298   }
 299   if (n.getKind() == APPLY_CONSTRUCTOR)
 300   {
 301     unsigned i = datatypes::utils::indexOf(n.getOperator());
 302     Assert(n.getNumChildren() == dt[i].getNumArgs());
 303     std::map<int, Node> pre;
 304     for (unsigned j = 0, size = n.getNumChildren(); j < size; j++)
 305     {
 306       pre[j] = sygusToBuiltin(n[j], dt[i].getArgType(j));
 307       Trace("sygus-db-debug")
 308           << "sygus to builtin " << n[j] << " is " << pre[j] << std::endl;
 309     }
 310     Node ret = mkGeneric(dt, i, pre);
 311     Trace("sygus-db-debug")
 312         << "SygusToBuiltin : Generic is " << ret << std::endl;
 313     // cache
 314     n.setAttribute(SygusToBuiltinAttribute(), ret);
 315     return ret;
 316   }
 317   if (n.hasAttribute(SygusPrintProxyAttribute()))
 318   {
 319     // this variable was associated by an attribute to a builtin node
 320     return n.getAttribute(SygusPrintProxyAttribute());
 321   }
 322   Assert(isFreeVar(n));
 323   // map to builtin variable type
 324   int fv_num = getVarNum(n);
 325   Assert(!dt.getSygusType().isNull());
 326   TypeNode vtn = dt.getSygusType();
 327   Node ret = getFreeVar(vtn, fv_num);
 328   return ret;
 329 }
 330
 331 unsigned TermDbSygus::getSygusTermSize( Node n ){
 332   if (n.getKind() != APPLY_CONSTRUCTOR)
 333   {
 334     return 0;
 335   }
 336   unsigned sum = 0;
 337   for (unsigned i = 0; i < n.getNumChildren(); i++)
 338   {
 339     sum += getSygusTermSize(n[i]);
 340   }
 341   const DType& dt = datatypes::utils::datatypeOf(n.getOperator());
 342   int cindex = datatypes::utils::indexOf(n.getOperator());
 343   Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors());
 344   unsigned weight = dt[cindex].getWeight();
 345   return weight + sum;
 346 }
 347
 348 bool TermDbSygus::registerSygusType(TypeNode tn)
 349 {
 350   std::map<TypeNode, bool>::iterator it = d_registerStatus.find(tn);
 351   if (it != d_registerStatus.end())
 352   {
 353     // already registered
 354     return it->second;
 355   }
 356   d_registerStatus[tn] = false;
 357   // it must be a sygus datatype
 358   if (!tn.isDatatype())
 359   {
 360     return false;
 361   }
 362   const DType& dt = tn.getDType();
 363   if (!dt.isSygus())
 364   {
 365     return false;
 366   }
 367   d_registerStatus[tn] = true;
 368   SygusTypeInfo& sti = d_tinfo[tn];
 369   sti.initialize(this, tn);
 370   return true;
 371 }
 372
 373 void TermDbSygus::registerEnumerator(Node e,
 374                                      Node f,
 375                                      SynthConjecture* conj,
 376                                      EnumeratorRole erole,
 377                                      bool useSymbolicCons)
 378 {
 379   if (d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end())
 380   {
 381     // already registered
 382     return;
 383   }
 384   Trace("sygus-db") << "Register enumerator : " << e << std::endl;
 385   // register its type
 386   TypeNode et = e.getType();
 387   registerSygusType(et);
 388   d_enum_to_conjecture[e] = conj;
 389   d_enum_to_synth_fun[e] = f;
 390   NodeManager* nm = NodeManager::currentNM();
 391
 392   Trace("sygus-db") << "  registering symmetry breaking clauses..."
 393                     << std::endl;
 394   d_enum_to_using_sym_cons[e] = useSymbolicCons;
 395   // depending on if we are using symbolic constructors, introduce symmetry
 396   // breaking lemma templates for each relevant subtype of the grammar
 397   SygusTypeInfo& eti = getTypeInfo(et);
 398   std::vector<TypeNode> sf_types;
 399   eti.getSubfieldTypes(sf_types);
 400   // for each type of subfield type of this enumerator
 401   for (unsigned i = 0, ntypes = sf_types.size(); i < ntypes; i++)
 402   {
 403     std::vector<unsigned> rm_indices;
 404     TypeNode stn = sf_types[i];
 405     Assert(stn.isDatatype());
 406     SygusTypeInfo& sti = getTypeInfo(stn);
 407     const DType& dt = stn.getDType();
 408     int anyC = sti.getAnyConstantConsNum();
 409     for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
 410     {
 411       bool isAnyC = static_cast<int>(i) == anyC;
 412       if (isAnyC && !useSymbolicCons)
 413       {
 414         // if we are not using the any constant constructor
 415         // do not use the symbolic constructor
 416         rm_indices.push_back(i);
 417       }
 418       else if (anyC != -1 && !isAnyC && useSymbolicCons)
 419       {
 420         // if we are using the any constant constructor, do not use any
 421         // concrete constant
 422         Node c_op = sti.getConsNumConst(i);
 423         if (!c_op.isNull())
 424         {
 425           rm_indices.push_back(i);
 426         }
 427       }
 428     }
 429     for (unsigned& rindex : rm_indices)
 430     {
 431       // make the apply-constructor corresponding to an application of the
 432       // constant or "any constant" constructor
 433       // we call getInstCons since in the case of any constant constructors, it
 434       // is necessary to generate a term of the form any_constant( x.0 ) for a
 435       // fresh variable x.0.
 436       Node fv = getFreeVar(stn, 0);
 437       Node exc_val = datatypes::utils::getInstCons(fv, dt, rindex);
 438       // should not include the constuctor in any subterm
 439       Node x = getFreeVar(stn, 0);
 440       Trace("sygus-db") << "Construct symmetry breaking lemma from " << x
 441                         << " == " << exc_val << std::endl;
 442       Node lem = getExplain()->getExplanationForEquality(x, exc_val);
 443       lem = lem.negate();
 444       Trace("cegqi-lemma")
 445           << "Cegqi::Lemma : exclude symbolic cons lemma (template) : " << lem
 446           << std::endl;
 447       // the size of the subterm we are blocking is the weight of the
 448       // constructor (usually zero)
 449       registerSymBreakLemma(e, lem, stn, dt[rindex].getWeight());
 450     }
 451   }
 452   Trace("sygus-db") << "  ...finished" << std::endl;
 453
 454   // determine if we are actively-generated
 455   bool isActiveGen = false;
 456   if (options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE)
 457   {
 458     if (erole == ROLE_ENUM_MULTI_SOLUTION || erole == ROLE_ENUM_CONSTRAINED)
 459     {
 460       // If the enumerator is a solution for a conjecture with multiple
 461       // functions, we do not use active generation. If we did, we would have to
 462       // generate a "product" of two actively-generated enumerators. That is,
 463       // given a conjecture with two functions-to-synthesize with enumerators
 464       // e_f and e_g, and if these enumerators generated:
 465       // e_f -> t1, ..., tn
 466       // e_g -> s1, ..., sm
 467       // The sygus module in charge of this conjecture would expect
 468       // constructCandidates calls of the form
 469       //   (e_f,e_g) -> (ti, sj)
 470       // for each i,j. We instead use passive enumeration in this case.
 471       //
 472       // If the enumerator is constrained, it cannot be actively generated.
 473     }
 474     else if (erole == ROLE_ENUM_POOL)
 475     {
 476       // If the enumerator is used for generating a pool of values, we always
 477       // use active generation.
 478       isActiveGen = true;
 479     }
 480     else if (erole == ROLE_ENUM_SINGLE_SOLUTION)
 481     {
 482       // If the enumerator is the single function-to-synthesize, if auto is
 483       // enabled, we infer whether it is better to enable active generation.
 484       if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_AUTO)
 485       {
 486         // We use active generation if the grammar of the enumerator does not
 487         // have ITE and is not Boolean. Experimentally, it is better to
 488         // use passive generation for these cases since it enables useful
 489         // search space pruning techniques, e.g. evaluation unfolding,
 490         // conjecture-specific symmetry breaking. Also, if sygus-stream is
 491         // enabled, we always use active generation, since the use cases of
 492         // sygus stream are to find many solutions to an easy problem, where
 493         // the bottleneck often becomes the large number of "exclude the current
 494         // solution" clauses.
 495         const DType& dt = et.getDType();
 496         if (options::sygusStream()
 497             || (!eti.hasIte() && !dt.getSygusType().isBoolean()))
 498         {
 499           isActiveGen = true;
 500         }
 501       }
 502       else
 503       {
 504         isActiveGen = true;
 505       }
 506     }
 507     else
 508     {
 509       Unreachable() << "Unknown enumerator mode in registerEnumerator";
 510     }
 511   }
 512   Trace("sygus-db") << "isActiveGen for " << e << ", role = " << erole
 513                     << " returned " << isActiveGen << std::endl;
 514   // Currently, actively-generated enumerators are either basic or variable
 515   // agnostic.
 516   bool isVarAgnostic =
 517       isActiveGen
 518       && options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_VAR_AGNOSTIC;
 519   d_enum_var_agnostic[e] = isVarAgnostic;
 520   if (isVarAgnostic)
 521   {
 522     // requires variable subclasses
 523     eti.initializeVarSubclasses();
 524     // If no subclass has more than one variable, do not use variable agnostic
 525     // enumeration
 526     bool useVarAgnostic = !eti.isSubclassVarTrivial();
 527     if (!useVarAgnostic)
 528     {
 529       Trace("sygus-db")
 530           << "...disabling variable agnostic for " << e
 531           << " since it has no subclass with more than one variable."
 532           << std::endl;
 533       d_enum_var_agnostic[e] = false;
 534       isActiveGen = false;
 535     }
 536   }
 537   d_enum_active_gen[e] = isActiveGen;
 538   d_enum_basic[e] = isActiveGen && !isVarAgnostic;
 539
 540   // We make an active guard if we will be explicitly blocking solutions for
 541   // the enumerator. This is the case if the role of the enumerator is to
 542   // populate a pool of terms, or (some cases) of when it is actively generated.
 543   if (isActiveGen || erole == ROLE_ENUM_POOL)
 544   {
 545     // make the guard
 546     Node ag = nm->mkSkolem("eG", nm->booleanType());
 547     // must ensure it is a literal immediately here
 548     ag = d_quantEngine->getValuation().ensureLiteral(ag);
 549     // must ensure that it is asserted as a literal before we begin solving
 550     Node lem = nm->mkNode(OR, ag, ag.negate());
 551     d_quantEngine->getOutputChannel().requirePhase(ag, true);
 552     d_quantEngine->getOutputChannel().lemma(lem);
 553     d_enum_to_active_guard[e] = ag;
 554   }
 555 }
 556
 557 bool TermDbSygus::isEnumerator(Node e) const
 558 {
 559   return d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end();
 560 }
 561
 562 SynthConjecture* TermDbSygus::getConjectureForEnumerator(Node e) const
 563 {
 564   std::map<Node, SynthConjecture*>::const_iterator itm =
 565       d_enum_to_conjecture.find(e);
 566   if (itm != d_enum_to_conjecture.end()) {
 567     return itm->second;
 568   }
 569   return nullptr;
 570 }
 571
 572 Node TermDbSygus::getSynthFunForEnumerator(Node e) const
 573 {
 574   std::map<Node, Node>::const_iterator itsf = d_enum_to_synth_fun.find(e);
 575   if (itsf != d_enum_to_synth_fun.end())
 576   {
 577     return itsf->second;
 578   }
 579   return Node::null();
 580 }
 581
 582 Node TermDbSygus::getActiveGuardForEnumerator(Node e) const
 583 {
 584   std::map<Node, Node>::const_iterator itag = d_enum_to_active_guard.find(e);
 585   if (itag != d_enum_to_active_guard.end()) {
 586     return itag->second;
 587   }
 588   return Node::null();
 589 }
 590
 591 bool TermDbSygus::usingSymbolicConsForEnumerator(Node e) const
 592 {
 593   std::map<Node, bool>::const_iterator itus = d_enum_to_using_sym_cons.find(e);
 594   if (itus != d_enum_to_using_sym_cons.end())
 595   {
 596     return itus->second;
 597   }
 598   return false;
 599 }
 600
 601 bool TermDbSygus::isVariableAgnosticEnumerator(Node e) const
 602 {
 603   std::map<Node, bool>::const_iterator itus = d_enum_var_agnostic.find(e);
 604   if (itus != d_enum_var_agnostic.end())
 605   {
 606     return itus->second;
 607   }
 608   return false;
 609 }
 610
 611 bool TermDbSygus::isBasicEnumerator(Node e) const
 612 {
 613   std::map<Node, bool>::const_iterator itus = d_enum_basic.find(e);
 614   if (itus != d_enum_basic.end())
 615   {
 616     return itus->second;
 617   }
 618   return false;
 619 }
 620
 621 bool TermDbSygus::isPassiveEnumerator(Node e) const
 622 {
 623   std::map<Node, bool>::const_iterator itus = d_enum_active_gen.find(e);
 624   if (itus != d_enum_active_gen.end())
 625   {
 626     return !itus->second;
 627   }
 628   return true;
 629 }
 630
 631 void TermDbSygus::getEnumerators(std::vector<Node>& mts)
 632 {
 633   for (std::map<Node, SynthConjecture*>::iterator itm =
 634            d_enum_to_conjecture.begin();
 635        itm != d_enum_to_conjecture.end();
 636        ++itm)
 637   {
 638     mts.push_back( itm->first );
 639   }
 640 }
 641
 642 void TermDbSygus::registerSymBreakLemma(
 643     Node e, Node lem, TypeNode tn, unsigned sz, bool isTempl)
 644 {
 645   d_enum_to_sb_lemmas[e].push_back(lem);
 646   d_sb_lemma_to_type[lem] = tn;
 647   d_sb_lemma_to_size[lem] = sz;
 648   d_sb_lemma_to_isTempl[lem] = isTempl;
 649 }
 650
 651 bool TermDbSygus::hasSymBreakLemmas(std::vector<Node>& enums) const
 652 {
 653   if (!d_enum_to_sb_lemmas.empty())
 654   {
 655     for (std::pair<const Node, std::vector<Node> > sb : d_enum_to_sb_lemmas)
 656     {
 657       enums.push_back(sb.first);
 658     }
 659     return true;
 660   }
 661   return false;
 662 }
 663
 664 void TermDbSygus::getSymBreakLemmas(Node e, std::vector<Node>& lemmas) const
 665 {
 666   std::map<Node, std::vector<Node> >::const_iterator itsb =
 667       d_enum_to_sb_lemmas.find(e);
 668   if (itsb != d_enum_to_sb_lemmas.end())
 669   {
 670     lemmas.insert(lemmas.end(), itsb->second.begin(), itsb->second.end());
 671   }
 672 }
 673
 674 TypeNode TermDbSygus::getTypeForSymBreakLemma(Node lem) const
 675 {
 676   std::map<Node, TypeNode>::const_iterator it = d_sb_lemma_to_type.find(lem);
 677   Assert(it != d_sb_lemma_to_type.end());
 678   return it->second;
 679 }
 680 unsigned TermDbSygus::getSizeForSymBreakLemma(Node lem) const
 681 {
 682   std::map<Node, unsigned>::const_iterator it = d_sb_lemma_to_size.find(lem);
 683   Assert(it != d_sb_lemma_to_size.end());
 684   return it->second;
 685 }
 686
 687 bool TermDbSygus::isSymBreakLemmaTemplate(Node lem) const
 688 {
 689   std::map<Node, bool>::const_iterator it = d_sb_lemma_to_isTempl.find(lem);
 690   Assert(it != d_sb_lemma_to_isTempl.end());
 691   return it->second;
 692 }
 693
 694 void TermDbSygus::clearSymBreakLemmas(Node e) { d_enum_to_sb_lemmas.erase(e); }
 695
 696 bool TermDbSygus::isRegistered(TypeNode tn) const
 697 {
 698   return d_tinfo.find(tn) != d_tinfo.end();
 699 }
 700
 701 TypeNode TermDbSygus::sygusToBuiltinType( TypeNode tn ) {
 702   std::map<TypeNode, SygusTypeInfo>::iterator it = d_tinfo.find(tn);
 703   Assert(it != d_tinfo.end());
 704   return it->second.getBuiltinType();
 705 }
 706
 707 void TermDbSygus::toStreamSygus(const char* c, Node n)
 708 {
 709   if (Trace.isOn(c))
 710   {
 711     if (n.isNull())
 712     {
 713       Trace(c) << n;
 714     }
 715     else
 716     {
 717       std::stringstream ss;
 718       Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, n);
 719       Trace(c) << ss.str();
 720     }
 721   }
 722 }
 723
 724 SygusTypeInfo& TermDbSygus::getTypeInfo(TypeNode tn)
 725 {
 726   AlwaysAssert(d_tinfo.find(tn) != d_tinfo.end());
 727   return d_tinfo[tn];
 728 }
 729
 730 Node TermDbSygus::rewriteNode(Node n) const
 731 {
 732   Node res = Rewriter::rewrite(n);
 733   if (res.isConst())
 734   {
 735     // constant, we are done
 736     return res;
 737   }
 738   if (options::sygusRecFun())
 739   {
 740     if (d_funDefEval->hasDefinitions())
 741     {
 742       // If recursive functions are enabled, then we use the recursive function
 743       // evaluation utility.
 744       Node fres = d_funDefEval->evaluate(res);
 745       if (!fres.isNull())
 746       {
 747         return fres;
 748       }
 749       // It may have failed, in which case there are undefined symbols in res or
 750       // we reached the limit of evaluations. In this case, we revert to the
 751       // result of rewriting in the return statement below.
 752     }
 753   }
 754   return res;
 755 }
 756
 757 unsigned TermDbSygus::getSelectorWeight(TypeNode tn, Node sel)
 758 {
 759   std::map<TypeNode, std::map<Node, unsigned> >::iterator itsw =
 760       d_sel_weight.find(tn);
 761   if (itsw == d_sel_weight.end())
 762   {
 763     d_sel_weight[tn].clear();
 764     itsw = d_sel_weight.find(tn);
 765     const DType& dt = tn.getDType();
 766     Trace("sygus-db") << "Compute selector weights for " << dt.getName()
 767                       << std::endl;
 768     for (unsigned i = 0, size = dt.getNumConstructors(); i < size; i++)
 769     {
 770       unsigned cw = dt[i].getWeight();
 771       for (unsigned j = 0, size2 = dt[i].getNumArgs(); j < size2; j++)
 772       {
 773         Node csel = dt[i].getSelectorInternal(tn, j);
 774         std::map<Node, unsigned>::iterator its = itsw->second.find(csel);
 775         if (its == itsw->second.end() || cw < its->second)
 776         {
 777           d_sel_weight[tn][csel] = cw;
 778           Trace("sygus-db") << "  w(" << csel << ") <= " << cw << std::endl;
 779         }
 780       }
 781     }
 782   }
 783   Assert(itsw->second.find(sel) != itsw->second.end());
 784   return itsw->second[sel];
 785 }
 786
 787 TypeNode TermDbSygus::getArgType(const DTypeConstructor& c, unsigned i) const
 788 {
 789   Assert(i < c.getNumArgs());
 790   return c.getArgType(i);
 791 }
 792
 793 bool TermDbSygus::isTypeMatch(const DTypeConstructor& c1,
 794                               const DTypeConstructor& c2)
 795 {
 796   if( c1.getNumArgs()!=c2.getNumArgs() ){
 797     return false;
 798   }else{
 799     for( unsigned i=0; i<c1.getNumArgs(); i++ ){
 800       if( getArgType( c1, i )!=getArgType( c2, i ) ){
 801         return false;
 802       }
 803     }
 804     return true;
 805   }
 806 }
 807
 808 bool TermDbSygus::isSymbolicConsApp(Node n) const
 809 {
 810   if (n.getKind() != APPLY_CONSTRUCTOR)
 811   {
 812     return false;
 813   }
 814   TypeNode tn = n.getType();
 815   Assert(tn.isDatatype());
 816   const DType& dt = tn.getDType();
 817   Assert(dt.isSygus());
 818   unsigned cindex = datatypes::utils::indexOf(n.getOperator());
 819   Node sygusOp = dt[cindex].getSygusOp();
 820   // it is symbolic if it represents "any constant"
 821   return sygusOp.getAttribute(SygusAnyConstAttribute());
 822 }
 823
 824 bool TermDbSygus::canConstructKind(TypeNode tn,
 825                                    Kind k,
 826                                    std::vector<TypeNode>& argts,
 827                                    bool aggr)
 828 {
 829   Assert(isRegistered(tn));
 830   SygusTypeInfo& ti = getTypeInfo(tn);
 831   int c = ti.getKindConsNum(k);
 832   const DType& dt = tn.getDType();
 833   if (c != -1)
 834   {
 835     for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++)
 836     {
 837       argts.push_back(dt[c].getArgType(i));
 838     }
 839     return true;
 840   }
 841   if (!options::sygusSymBreakAgg())
 842   {
 843     return false;
 844   }
 845   if (sygusToBuiltinType(tn).isBoolean())
 846   {
 847     if (k == ITE)
 848     {
 849       // ite( b1, b2, b3 ) <---- and( or( ~b1, b2 ), or( b1, b3 ) )
 850       std::vector<TypeNode> conj_types;
 851       if (canConstructKind(tn, AND, conj_types, true) && conj_types.size() == 2)
 852       {
 853         bool success = true;
 854         std::vector<TypeNode> disj_types[2];
 855         for (unsigned c = 0; c < 2; c++)
 856         {
 857           if (!canConstructKind(conj_types[c], OR, disj_types[c], true)
 858               || disj_types[c].size() != 2)
 859           {
 860             success = false;
 861             break;
 862           }
 863         }
 864         if (success)
 865         {
 866           for (unsigned r = 0; r < 2; r++)
 867           {
 868             for (unsigned d = 0, size = disj_types[r].size(); d < size; d++)
 869             {
 870               TypeNode dtn = disj_types[r][d];
 871               // must have negation that occurs in the other conjunct
 872               std::vector<TypeNode> ntypes;
 873               if (canConstructKind(dtn, NOT, ntypes) && ntypes.size() == 1)
 874               {
 875                 TypeNode ntn = ntypes[0];
 876                 for (unsigned dd = 0, size = disj_types[1 - r].size();
 877                      dd < size;
 878                      dd++)
 879                 {
 880                   if (disj_types[1 - r][dd] == ntn)
 881                   {
 882                     argts.push_back(ntn);
 883                     argts.push_back(disj_types[r][d]);
 884                     argts.push_back(disj_types[1 - r][1 - dd]);
 885                     if (Trace.isOn("sygus-cons-kind"))
 886                     {
 887                       Trace("sygus-cons-kind")
 888                           << "Can construct kind " << k << " in " << tn
 889                           << " via child types:" << std::endl;
 890                       for (unsigned i = 0; i < 3; i++)
 891                       {
 892                         Trace("sygus-cons-kind")
 893                             << "  " << argts[i] << std::endl;
 894                       }
 895                     }
 896                     return true;
 897                   }
 898                 }
 899               }
 900             }
 901           }
 902         }
 903       }
 904     }
 905   }
 906   // could try aggressive inferences here, such as
 907   // (and b1 b2) <---- (not (or (not b1) (not b2)))
 908   // (or b1 b2)  <---- (not (and (not b1) (not b2)))
 909   return false;
 910 }
 911
 912 bool TermDbSygus::involvesDivByZero( Node n, std::map< Node, bool >& visited ){
 913   if( visited.find( n )==visited.end() ){
 914     visited[n] = true;
 915     Kind k = n.getKind();
 916     if( k==DIVISION || k==DIVISION_TOTAL || k==INTS_DIVISION || k==INTS_DIVISION_TOTAL ||
 917         k==INTS_MODULUS || k==INTS_MODULUS_TOTAL ){
 918       if( n[1].isConst() ){
 919         if (n[1]
 920             == d_quantEngine->getTermUtil()->getTypeValue(n[1].getType(), 0))
 921         {
 922           return true;
 923         }
 924       }else{
 925         // if it has free variables it might be a non-zero constant
 926         if( !hasFreeVar( n[1] ) ){
 927           return true;
 928         }
 929       }
 930     }
 931     for( unsigned i=0; i<n.getNumChildren(); i++ ){
 932       if( involvesDivByZero( n[i], visited ) ){
 933         return true;
 934       }
 935     }
 936   }
 937   return false;
 938 }
 939
 940 bool TermDbSygus::involvesDivByZero( Node n ) {
 941   std::map< Node, bool > visited;
 942   return involvesDivByZero( n, visited );
 943 }
 944
 945 Node TermDbSygus::getAnchor( Node n ) {
 946   if( n.getKind()==APPLY_SELECTOR_TOTAL ){
 947     return getAnchor( n[0] );
 948   }else{
 949     return n;
 950   }
 951 }
 952
 953 unsigned TermDbSygus::getAnchorDepth( Node n ) {
 954   if( n.getKind()==APPLY_SELECTOR_TOTAL ){
 955     return 1+getAnchorDepth( n[0] );
 956   }else{
 957     return 0;
 958   }
 959 }
 960
 961 Node TermDbSygus::evaluateBuiltin(TypeNode tn,
 962                                   Node bn,
 963                                   std::vector<Node>& args,
 964                                   bool tryEval)
 965 {
 966   if (args.empty())
 967   {
 968     return Rewriter::rewrite( bn );
 969   }
 970   Assert(isRegistered(tn));
 971   SygusTypeInfo& ti = getTypeInfo(tn);
 972   const std::vector<Node>& varlist = ti.getVarList();
 973   Assert(varlist.size() == args.size());
 974
 975   Node res;
 976   if (tryEval && options::sygusEvalOpt())
 977   {
 978     // Try evaluating, which is much faster than substitution+rewriting.
 979     // This may fail if there is a subterm of bn under the
 980     // substitution that is not constant, or if an operator in bn is not
 981     // supported by the evaluator
 982     res = d_eval->eval(bn, varlist, args);
 983   }
 984   if (!res.isNull())
 985   {
 986     Assert(res
 987            == Rewriter::rewrite(bn.substitute(
 988                varlist.begin(), varlist.end(), args.begin(), args.end())));
 989     return res;
 990   }
 991   res = bn.substitute(varlist.begin(), varlist.end(), args.begin(), args.end());
 992   // Call the rewrite node function, which may involve recursive function
 993   // evaluation.
 994   return rewriteNode(res);
 995 }
 996
 997 Node TermDbSygus::evaluateWithUnfolding(
 998     Node n, std::unordered_map<Node, Node, NodeHashFunction>& visited)
 999 {
1000   std::unordered_map<Node, Node, NodeHashFunction>::iterator it =
1001       visited.find(n);
1002   if( it==visited.end() ){
1003     Node ret = n;
1004     while (ret.getKind() == DT_SYGUS_EVAL
1005            && ret[0].getKind() == APPLY_CONSTRUCTOR)
1006     {
1007       if (ret == n && ret[0].isConst())
1008       {
1009         // use rewriting, possibly involving recursive functions
1010         ret = rewriteNode(ret);
1011       }
1012       else
1013       {
1014         ret = d_eval_unfold->unfold(ret);
1015       }
1016     }
1017     if( ret.getNumChildren()>0 ){
1018       std::vector< Node > children;
1019       if( ret.getMetaKind() == kind::metakind::PARAMETERIZED ){
1020         children.push_back( ret.getOperator() );
1021       }
1022       bool childChanged = false;
1023       for( unsigned i=0; i<ret.getNumChildren(); i++ ){
1024         Node nc = evaluateWithUnfolding(ret[i], visited);
1025         childChanged = childChanged || nc!=ret[i];
1026         children.push_back( nc );
1027       }
1028       if( childChanged ){
1029         ret = NodeManager::currentNM()->mkNode( ret.getKind(), children );
1030       }
1031       ret = getExtRewriter()->extendedRewrite(ret);
1032       // use rewriting, possibly involving recursive functions
1033       ret = rewriteNode(ret);
1034     }
1035     visited[n] = ret;
1036     return ret;
1037   }else{
1038     return it->second;
1039   }
1040 }
1041
1042 Node TermDbSygus::evaluateWithUnfolding(Node n)
1043 {
1044   std::unordered_map<Node, Node, NodeHashFunction> visited;
1045   return evaluateWithUnfolding(n, visited);
1046 }
1047
1048 bool TermDbSygus::isEvaluationPoint(Node n) const
1049 {
1050   if (n.getKind() != DT_SYGUS_EVAL)
1051   {
1052     return false;
1053   }
1054   if (!n[0].isVar())
1055   {
1056     return false;
1057   }
1058   for (unsigned i = 1, nchild = n.getNumChildren(); i < nchild; i++)
1059   {
1060     if (!n[i].isConst())
1061     {
1062       return false;
1063     }
1064   }
1065   return true;
1066 }
1067
1068 }/* CVC4::theory::quantifiers namespace */
1069 }/* CVC4::theory namespace */
1070 }/* CVC4 namespace */