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