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/cvc4_check.h"
18 #include "options/base_options.h"
19 #include "options/quantifiers_options.h"
20 #include "printer/printer.h"
21 #include "theory/arith/arith_msum.h"
22 #include "theory/datatypes/datatypes_rewriter.h"
23 #include "theory/quantifiers/quantifiers_attributes.h"
24 #include "theory/quantifiers/term_database.h"
25 #include "theory/quantifiers/term_util.h"
26 #include "theory/quantifiers_engine.h"
27
28 using namespace CVC4::kind;
29
30 namespace CVC4 {
31 namespace theory {
32 namespace quantifiers {
33
add(Node v,std::vector<TypeNode> & types)34 void TypeNodeIdTrie::add(Node v, std::vector<TypeNode>& types)
35 {
36 TypeNodeIdTrie* tnt = this;
37 for (unsigned i = 0, size = types.size(); i < size; i++)
38 {
39 tnt = &tnt->d_children[types[i]];
40 }
41 tnt->d_data.push_back(v);
42 }
43
assignIds(std::map<Node,unsigned> & assign,unsigned & idCount)44 void TypeNodeIdTrie::assignIds(std::map<Node, unsigned>& assign,
45 unsigned& idCount)
46 {
47 if (!d_data.empty())
48 {
49 for (const Node& v : d_data)
50 {
51 assign[v] = idCount;
52 }
53 idCount++;
54 }
55 for (std::pair<const TypeNode, TypeNodeIdTrie>& c : d_children)
56 {
57 c.second.assignIds(assign, idCount);
58 }
59 }
60
operator <<(std::ostream & os,EnumeratorRole r)61 std::ostream& operator<<(std::ostream& os, EnumeratorRole r)
62 {
63 switch (r)
64 {
65 case ROLE_ENUM_POOL: os << "POOL"; break;
66 case ROLE_ENUM_SINGLE_SOLUTION: os << "SINGLE_SOLUTION"; break;
67 case ROLE_ENUM_MULTI_SOLUTION: os << "MULTI_SOLUTION"; break;
68 case ROLE_ENUM_CONSTRAINED: os << "CONSTRAINED"; break;
69 default: os << "enum_" << static_cast<unsigned>(r); break;
70 }
71 return os;
72 }
73
TermDbSygus(context::Context * c,QuantifiersEngine * qe)74 TermDbSygus::TermDbSygus(context::Context* c, QuantifiersEngine* qe)
75 : d_quantEngine(qe),
76 d_syexp(new SygusExplain(this)),
77 d_ext_rw(new ExtendedRewriter(true)),
78 d_eval(new Evaluator),
79 d_eval_unfold(new SygusEvalUnfold(this))
80 {
81 d_true = NodeManager::currentNM()->mkConst( true );
82 d_false = NodeManager::currentNM()->mkConst( false );
83 }
84
reset(Theory::Effort e)85 bool TermDbSygus::reset( Theory::Effort e ) {
86 return true;
87 }
88
getFreeVar(TypeNode tn,int i,bool useSygusType)89 TNode TermDbSygus::getFreeVar( TypeNode tn, int i, bool useSygusType ) {
90 unsigned sindex = 0;
91 TypeNode vtn = tn;
92 if( useSygusType ){
93 if( tn.isDatatype() ){
94 const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
95 if( !dt.getSygusType().isNull() ){
96 vtn = TypeNode::fromType( dt.getSygusType() );
97 sindex = 1;
98 }
99 }
100 }
101 while( i>=(int)d_fv[sindex][tn].size() ){
102 std::stringstream ss;
103 if( tn.isDatatype() ){
104 const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
105 ss << "fv_" << dt.getName() << "_" << i;
106 }else{
107 ss << "fv_" << tn << "_" << i;
108 }
109 Assert( !vtn.isNull() );
110 Node v = NodeManager::currentNM()->mkSkolem( ss.str(), vtn, "for sygus normal form testing" );
111 d_fv_stype[v] = tn;
112 d_fv_num[v] = i;
113 d_fv[sindex][tn].push_back( v );
114 }
115 return d_fv[sindex][tn][i];
116 }
117
getFreeVarInc(TypeNode tn,std::map<TypeNode,int> & var_count,bool useSygusType)118 TNode TermDbSygus::getFreeVarInc( TypeNode tn, std::map< TypeNode, int >& var_count, bool useSygusType ) {
119 std::map< TypeNode, int >::iterator it = var_count.find( tn );
120 if( it==var_count.end() ){
121 var_count[tn] = 1;
122 return getFreeVar( tn, 0, useSygusType );
123 }else{
124 int index = it->second;
125 var_count[tn]++;
126 return getFreeVar( tn, index, useSygusType );
127 }
128 }
129
hasFreeVar(Node n,std::map<Node,bool> & visited)130 bool TermDbSygus::hasFreeVar( Node n, std::map< Node, bool >& visited ){
131 if( visited.find( n )==visited.end() ){
132 visited[n] = true;
133 if( isFreeVar( n ) ){
134 return true;
135 }
136 for( unsigned i=0; i<n.getNumChildren(); i++ ){
137 if( hasFreeVar( n[i], visited ) ){
138 return true;
139 }
140 }
141 }
142 return false;
143 }
144
hasFreeVar(Node n)145 bool TermDbSygus::hasFreeVar( Node n ) {
146 std::map< Node, bool > visited;
147 return hasFreeVar( n, visited );
148 }
149
getProxyVariable(TypeNode tn,Node c)150 Node TermDbSygus::getProxyVariable(TypeNode tn, Node c)
151 {
152 Assert(tn.isDatatype());
153 Assert(static_cast<DatatypeType>(tn.toType()).getDatatype().isSygus());
154 Assert(
155 TypeNode::fromType(
156 static_cast<DatatypeType>(tn.toType()).getDatatype().getSygusType())
157 .isComparableTo(c.getType()));
158
159 std::map<Node, Node>::iterator it = d_proxy_vars[tn].find(c);
160 if (it == d_proxy_vars[tn].end())
161 {
162 int anyC = getAnyConstantConsNum(tn);
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 Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
173 k = NodeManager::currentNM()->mkNode(
174 APPLY_CONSTRUCTOR, Node::fromExpr(dt[anyC].getConstructor()), c);
175 }
176 d_proxy_vars[tn][c] = k;
177 return k;
178 }
179 return it->second;
180 }
181
getSygusTypeForVar(Node v)182 TypeNode TermDbSygus::getSygusTypeForVar( Node v ) {
183 Assert( d_fv_stype.find( v )!=d_fv_stype.end() );
184 return d_fv_stype[v];
185 }
186
mkGeneric(const Datatype & dt,unsigned c,std::map<TypeNode,int> & var_count,std::map<int,Node> & pre)187 Node TermDbSygus::mkGeneric(const Datatype& dt,
188 unsigned c,
189 std::map<TypeNode, int>& var_count,
190 std::map<int, Node>& pre)
191 {
192 Assert(c < dt.getNumConstructors());
193 Assert( dt.isSygus() );
194 Assert( !dt[c].getSygusOp().isNull() );
195 std::vector< Node > children;
196 Trace("sygus-db-debug") << "mkGeneric " << dt.getName() << " " << c << "..."
197 << std::endl;
198 for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++)
199 {
200 Node a;
201 std::map< int, Node >::iterator it = pre.find( i );
202 if( it!=pre.end() ){
203 a = it->second;
204 }else{
205 TypeNode tna = TypeNode::fromType(dt[c].getArgType(i));
206 a = getFreeVarInc( tna, var_count, true );
207 }
208 Trace("sygus-db-debug")
209 << " child " << i << " : " << a << " : " << a.getType() << std::endl;
210 Assert( !a.isNull() );
211 children.push_back( a );
212 }
213 return datatypes::DatatypesRewriter::mkSygusTerm(dt, c, children);
214 }
215
mkGeneric(const Datatype & dt,int c,std::map<int,Node> & pre)216 Node TermDbSygus::mkGeneric(const Datatype& dt, int c, std::map<int, Node>& pre)
217 {
218 std::map<TypeNode, int> var_count;
219 return mkGeneric(dt, c, var_count, pre);
220 }
221
mkGeneric(const Datatype & dt,int c)222 Node TermDbSygus::mkGeneric(const Datatype& dt, int c)
223 {
224 std::map<int, Node> pre;
225 return mkGeneric(dt, c, pre);
226 }
227
228 struct CanonizeBuiltinAttributeId
229 {
230 };
231 using CanonizeBuiltinAttribute =
232 expr::Attribute<CanonizeBuiltinAttributeId, Node>;
233
canonizeBuiltin(Node n)234 Node TermDbSygus::canonizeBuiltin(Node n)
235 {
236 std::map<TypeNode, int> var_count;
237 return canonizeBuiltin(n, var_count);
238 }
239
canonizeBuiltin(Node n,std::map<TypeNode,int> & var_count)240 Node TermDbSygus::canonizeBuiltin(Node n, std::map<TypeNode, int>& var_count)
241 {
242 // has it already been computed?
243 if (var_count.empty() && n.hasAttribute(CanonizeBuiltinAttribute()))
244 {
245 Node ret = n.getAttribute(CanonizeBuiltinAttribute());
246 Trace("sygus-db-canon") << "cached " << n << " : " << ret << "\n";
247 return ret;
248 }
249 Trace("sygus-db-canon") << " CanonizeBuiltin : compute for " << n << "\n";
250 Node ret = n;
251 // it is symbolic if it represents "any constant"
252 if (n.getKind() == APPLY_SELECTOR_TOTAL)
253 {
254 ret = getFreeVarInc(n[0].getType(), var_count, true);
255 }
256 else if (n.getKind() != APPLY_CONSTRUCTOR)
257 {
258 ret = n;
259 }
260 else
261 {
262 Assert(n.getKind() == APPLY_CONSTRUCTOR);
263 bool childChanged = false;
264 std::vector<Node> children;
265 children.push_back(n.getOperator());
266 for (unsigned j = 0, size = n.getNumChildren(); j < size; ++j)
267 {
268 Node child = canonizeBuiltin(n[j], var_count);
269 children.push_back(child);
270 childChanged = childChanged || child != n[j];
271 }
272 if (childChanged)
273 {
274 ret = NodeManager::currentNM()->mkNode(APPLY_CONSTRUCTOR, children);
275 }
276 }
277 // cache if we had a fresh variable count
278 if (var_count.empty())
279 {
280 n.setAttribute(CanonizeBuiltinAttribute(), ret);
281 }
282 Trace("sygus-db-canon") << " ...normalized " << n << " --> " << ret
283 << std::endl;
284 Assert(ret.getType().isComparableTo(n.getType()));
285 return ret;
286 }
287
288 struct SygusToBuiltinAttributeId
289 {
290 };
291 typedef expr::Attribute<SygusToBuiltinAttributeId, Node>
292 SygusToBuiltinAttribute;
293
sygusToBuiltin(Node n,TypeNode tn)294 Node TermDbSygus::sygusToBuiltin(Node n, TypeNode tn)
295 {
296 Assert(n.getType().isComparableTo(tn));
297 if (!tn.isDatatype())
298 {
299 return n;
300 }
301 // has it already been computed?
302 if (n.hasAttribute(SygusToBuiltinAttribute()))
303 {
304 return n.getAttribute(SygusToBuiltinAttribute());
305 }
306 Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n
307 << ", type = " << tn << std::endl;
308 const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
309 if (!dt.isSygus())
310 {
311 return n;
312 }
313 if (n.getKind() == APPLY_CONSTRUCTOR)
314 {
315 unsigned i = datatypes::DatatypesRewriter::indexOf(n.getOperator());
316 Assert(n.getNumChildren() == dt[i].getNumArgs());
317 std::map<int, Node> pre;
318 for (unsigned j = 0, size = n.getNumChildren(); j < size; j++)
319 {
320 pre[j] = sygusToBuiltin(n[j], TypeNode::fromType(dt[i].getArgType(j)));
321 }
322 Node ret = mkGeneric(dt, i, pre);
323 Trace("sygus-db-debug")
324 << "SygusToBuiltin : Generic is " << ret << std::endl;
325 // cache
326 n.setAttribute(SygusToBuiltinAttribute(), ret);
327 return ret;
328 }
329 if (n.hasAttribute(SygusPrintProxyAttribute()))
330 {
331 // this variable was associated by an attribute to a builtin node
332 return n.getAttribute(SygusPrintProxyAttribute());
333 }
334 Assert(isFreeVar(n));
335 // map to builtin variable type
336 int fv_num = getVarNum(n);
337 Assert(!dt.getSygusType().isNull());
338 TypeNode vtn = TypeNode::fromType(dt.getSygusType());
339 Node ret = getFreeVar(vtn, fv_num);
340 return ret;
341 }
342
sygusSubstituted(TypeNode tn,Node n,std::vector<Node> & args)343 Node TermDbSygus::sygusSubstituted( TypeNode tn, Node n, std::vector< Node >& args ) {
344 Assert( d_var_list[tn].size()==args.size() );
345 return n.substitute( d_var_list[tn].begin(), d_var_list[tn].end(), args.begin(), args.end() );
346 }
347
getSygusTermSize(Node n)348 unsigned TermDbSygus::getSygusTermSize( Node n ){
349 if (n.getKind() != APPLY_CONSTRUCTOR)
350 {
351 return 0;
352 }
353 unsigned sum = 0;
354 for (unsigned i = 0; i < n.getNumChildren(); i++)
355 {
356 sum += getSygusTermSize(n[i]);
357 }
358 const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
359 int cindex = datatypes::DatatypesRewriter::indexOf(n.getOperator());
360 Assert(cindex >= 0 && cindex < (int)dt.getNumConstructors());
361 unsigned weight = dt[cindex].getWeight();
362 return weight + sum;
363 }
364
registerSygusType(TypeNode tn)365 void TermDbSygus::registerSygusType( TypeNode tn ) {
366 std::map< TypeNode, TypeNode >::iterator itr = d_register.find( tn );
367 if( itr==d_register.end() ){
368 d_register[tn] = TypeNode::null();
369 if( tn.isDatatype() ){
370 const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
371 Trace("sygus-db") << "Register type " << dt.getName() << "..." << std::endl;
372 TypeNode btn = TypeNode::fromType( dt.getSygusType() );
373 d_register[tn] = btn;
374 if( !d_register[tn].isNull() ){
375 // get the sygus variable list
376 Node var_list = Node::fromExpr( dt.getSygusVarList() );
377 if( !var_list.isNull() ){
378 for( unsigned j=0; j<var_list.getNumChildren(); j++ ){
379 Node sv = var_list[j];
380 SygusVarNumAttribute svna;
381 sv.setAttribute( svna, j );
382 d_var_list[tn].push_back( sv );
383 }
384 }else{
385 // no arguments to synthesis functions
386 d_var_list[tn].clear();
387 }
388 // register connected types
389 for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
390 {
391 for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
392 {
393 TypeNode ctn = TypeNode::fromType(dt[i].getArgType(j));
394 registerSygusType(ctn);
395 // carry type attributes
396 if (d_has_subterm_sym_cons.find(ctn)
397 != d_has_subterm_sym_cons.end())
398 {
399 d_has_subterm_sym_cons[tn] = true;
400 }
401 }
402 }
403 //iterate over constructors
404 for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
405 Expr sop = dt[i].getSygusOp();
406 Assert( !sop.isNull() );
407 Node n = Node::fromExpr( sop );
408 Trace("sygus-db") << " Operator #" << i << " : " << sop;
409 if( sop.getKind() == kind::BUILTIN ){
410 Kind sk = NodeManager::operatorToKind( n );
411 Trace("sygus-db") << ", kind = " << sk;
412 d_kinds[tn][sk] = i;
413 d_arg_kind[tn][i] = sk;
414 }
415 else if (sop.isConst() && dt[i].getNumArgs() == 0)
416 {
417 Trace("sygus-db") << ", constant";
418 d_consts[tn][n] = i;
419 d_arg_const[tn][i] = n;
420 }
421 else if (sop.getKind() == LAMBDA)
422 {
423 // do type checking
424 Assert(sop[0].getNumChildren() == dt[i].getNumArgs());
425 for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
426 {
427 TypeNode ct = TypeNode::fromType(dt[i].getArgType(j));
428 TypeNode cbt = sygusToBuiltinType(ct);
429 TypeNode lat = TypeNode::fromType(sop[0][j].getType());
430 CVC4_CHECK(cbt.isSubtypeOf(lat))
431 << "In sygus datatype " << dt.getName()
432 << ", argument to a lambda constructor is not " << lat
433 << std::endl;
434 }
435 }
436 // symbolic constructors
437 if (n.getAttribute(SygusAnyConstAttribute()))
438 {
439 d_sym_cons_any_constant[tn] = i;
440 d_has_subterm_sym_cons[tn] = true;
441 }
442 // TODO (as part of #1170): we still do not properly catch type
443 // errors in sygus grammars for arguments of builtin operators.
444 // The challenge is that we easily ask for expected argument types of
445 // builtin operators e.g. PLUS. Hence the call to mkGeneric below
446 // will throw a type exception.
447 d_ops[tn][n] = i;
448 d_arg_ops[tn][i] = n;
449 Trace("sygus-db") << std::endl;
450 // ensure that terms that this constructor encodes are
451 // of the type specified in the datatype. This will fail if
452 // e.g. bitvector-and is a constructor of an integer grammar.
453 Node g = mkGeneric(dt, i);
454 TypeNode gtn = g.getType();
455 CVC4_CHECK(gtn.isSubtypeOf(btn))
456 << "Sygus datatype " << dt.getName()
457 << " encodes terms that are not of type " << btn << std::endl;
458 Trace("sygus-db") << "...done register Operator #" << i << std::endl;
459 }
460 // compute min type depth information
461 computeMinTypeDepthInternal(tn, tn, 0);
462 }
463 }
464 }
465 }
466
registerEnumerator(Node e,Node f,SynthConjecture * conj,EnumeratorRole erole,bool useSymbolicCons)467 void TermDbSygus::registerEnumerator(Node e,
468 Node f,
469 SynthConjecture* conj,
470 EnumeratorRole erole,
471 bool useSymbolicCons)
472 {
473 if (d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end())
474 {
475 // already registered
476 return;
477 }
478 Trace("sygus-db") << "Register enumerator : " << e << std::endl;
479 // register its type
480 TypeNode et = e.getType();
481 registerSygusType(et);
482 d_enum_to_conjecture[e] = conj;
483 d_enum_to_synth_fun[e] = f;
484 NodeManager* nm = NodeManager::currentNM();
485
486 Trace("sygus-db") << " registering symmetry breaking clauses..."
487 << std::endl;
488 d_enum_to_using_sym_cons[e] = useSymbolicCons;
489 // depending on if we are using symbolic constructors, introduce symmetry
490 // breaking lemma templates for each relevant subtype of the grammar
491 std::vector<TypeNode> sf_types;
492 getSubfieldTypes(et, sf_types);
493 // maps variables to the list of subfield types they occur in
494 std::map<Node, std::vector<TypeNode> > type_occurs;
495 std::map<TypeNode, std::vector<Node> >::iterator itv = d_var_list.find(et);
496 Assert(itv != d_var_list.end());
497 for (const Node& v : itv->second)
498 {
499 type_occurs[v].clear();
500 }
501 // for each type of subfield type of this enumerator
502 for (unsigned i = 0, ntypes = sf_types.size(); i < ntypes; i++)
503 {
504 std::vector<unsigned> rm_indices;
505 TypeNode stn = sf_types[i];
506 Assert(stn.isDatatype());
507 const Datatype& dt = stn.getDatatype();
508 int anyC = getAnyConstantConsNum(stn);
509 for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
510 {
511 Expr sop = dt[i].getSygusOp();
512 Assert(!sop.isNull());
513 bool isAnyC = static_cast<int>(i) == anyC;
514 Node sopn = Node::fromExpr(sop);
515 if (type_occurs.find(sopn) != type_occurs.end())
516 {
517 // if it is a variable, store that it occurs in stn
518 type_occurs[sopn].push_back(stn);
519 }
520 else if (isAnyC && !useSymbolicCons)
521 {
522 // if we are not using the any constant constructor
523 // do not use the symbolic constructor
524 rm_indices.push_back(i);
525 }
526 else if (anyC != -1 && !isAnyC && useSymbolicCons)
527 {
528 // if we are using the any constant constructor, do not use any
529 // concrete constant
530 Node c_op = getConsNumConst(stn, i);
531 if (!c_op.isNull())
532 {
533 rm_indices.push_back(i);
534 }
535 }
536 }
537 for (unsigned& rindex : rm_indices)
538 {
539 // make the apply-constructor corresponding to an application of the
540 // constant or "any constant" constructor
541 // we call getInstCons since in the case of any constant constructors, it
542 // is necessary to generate a term of the form any_constant( x.0 ) for a
543 // fresh variable x.0.
544 Node fv = getFreeVar(stn, 0);
545 Node exc_val = datatypes::DatatypesRewriter::getInstCons(fv, dt, rindex);
546 // should not include the constuctor in any subterm
547 Node x = getFreeVar(stn, 0);
548 Trace("sygus-db") << "Construct symmetry breaking lemma from " << x
549 << " == " << exc_val << std::endl;
550 Node lem = getExplain()->getExplanationForEquality(x, exc_val);
551 lem = lem.negate();
552 Trace("cegqi-lemma")
553 << "Cegqi::Lemma : exclude symbolic cons lemma (template) : " << lem
554 << std::endl;
555 // the size of the subterm we are blocking is the weight of the
556 // constructor (usually zero)
557 registerSymBreakLemma(e, lem, stn, dt[rindex].getWeight());
558 }
559 }
560 Trace("sygus-db") << " ...finished" << std::endl;
561
562 // determine if we are actively-generated
563 bool isActiveGen = false;
564 if (options::sygusActiveGenMode() != SYGUS_ACTIVE_GEN_NONE)
565 {
566 if (erole == ROLE_ENUM_MULTI_SOLUTION || erole == ROLE_ENUM_CONSTRAINED)
567 {
568 // If the enumerator is a solution for a conjecture with multiple
569 // functions, we do not use active generation. If we did, we would have to
570 // generate a "product" of two actively-generated enumerators. That is,
571 // given a conjecture with two functions-to-synthesize with enumerators
572 // e_f and e_g, and if these enumerators generated:
573 // e_f -> t1, ..., tn
574 // e_g -> s1, ..., sm
575 // The sygus module in charge of this conjecture would expect
576 // constructCandidates calls of the form
577 // (e_f,e_g) -> (ti, sj)
578 // for each i,j. We instead use passive enumeration in this case.
579 //
580 // If the enumerator is constrained, it cannot be actively generated.
581 }
582 else if (erole == ROLE_ENUM_POOL)
583 {
584 // If the enumerator is used for generating a pool of values, we always
585 // use active generation.
586 isActiveGen = true;
587 }
588 else if (erole == ROLE_ENUM_SINGLE_SOLUTION)
589 {
590 // If the enumerator is the single function-to-synthesize, if auto is
591 // enabled, we infer whether it is better to enable active generation.
592 if (options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_AUTO)
593 {
594 // We use active generation if the grammar of the enumerator does not
595 // have ITE and is not Boolean. Experimentally, it is better to
596 // use passive generation for these cases since it enables useful
597 // search space pruning techniques, e.g. evaluation unfolding,
598 // conjecture-specific symmetry breaking. Also, if sygus-stream is
599 // enabled, we always use active generation, since the use cases of
600 // sygus stream are to find many solutions to an easy problem, where
601 // the bottleneck often becomes the large number of "exclude the current
602 // solution" clauses.
603 const Datatype& dt = et.getDatatype();
604 if (options::sygusStream()
605 || (!hasKind(et, ITE) && !dt.getSygusType().isBoolean()))
606 {
607 isActiveGen = true;
608 }
609 }
610 else
611 {
612 isActiveGen = true;
613 }
614 }
615 else
616 {
617 Unreachable("Unknown enumerator mode in registerEnumerator");
618 }
619 }
620 Trace("sygus-db") << "isActiveGen for " << e << ", role = " << erole
621 << " returned " << isActiveGen << std::endl;
622 // Currently, actively-generated enumerators are either basic or variable
623 // agnostic.
624 bool isVarAgnostic =
625 isActiveGen
626 && options::sygusActiveGenMode() == SYGUS_ACTIVE_GEN_VAR_AGNOSTIC;
627 d_enum_var_agnostic[e] = isVarAgnostic;
628 if (isVarAgnostic)
629 {
630 // if not done so already, compute type class identifiers for each variable
631 if (d_var_subclass_id.find(et) == d_var_subclass_id.end())
632 {
633 d_var_subclass_id[et].clear();
634 TypeNodeIdTrie tnit;
635 for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs)
636 {
637 tnit.add(to.first, to.second);
638 }
639 // 0 is reserved for "no type class id"
640 unsigned typeIdCount = 1;
641 tnit.assignIds(d_var_subclass_id[et], typeIdCount);
642 // assign the list and reverse map to index
643 for (std::pair<const Node, std::vector<TypeNode> >& to : type_occurs)
644 {
645 Node v = to.first;
646 unsigned sc = d_var_subclass_id[et][v];
647 Trace("sygus-db") << v << " has subclass id " << sc << std::endl;
648 d_var_subclass_list_index[et][v] = d_var_subclass_list[et][sc].size();
649 d_var_subclass_list[et][sc].push_back(v);
650 }
651 }
652 // If no subclass has more than one variable, do not use variable agnostic
653 // enumeration
654 bool useVarAgnostic = false;
655 for (std::pair<const unsigned, std::vector<Node> >& p :
656 d_var_subclass_list[et])
657 {
658 if (p.second.size() > 1)
659 {
660 useVarAgnostic = true;
661 }
662 }
663 if (!useVarAgnostic)
664 {
665 Trace("sygus-db")
666 << "...disabling variable agnostic for " << e
667 << " since it has no subclass with more than one variable."
668 << std::endl;
669 d_enum_var_agnostic[e] = false;
670 isActiveGen = false;
671 }
672 }
673 d_enum_active_gen[e] = isActiveGen;
674 d_enum_basic[e] = isActiveGen && !isVarAgnostic;
675
676 // We make an active guard if we will be explicitly blocking solutions for
677 // the enumerator. This is the case if the role of the enumerator is to
678 // populate a pool of terms, or (some cases) of when it is actively generated.
679 if (isActiveGen || erole == ROLE_ENUM_POOL)
680 {
681 // make the guard
682 Node ag = nm->mkSkolem("eG", nm->booleanType());
683 // must ensure it is a literal immediately here
684 ag = d_quantEngine->getValuation().ensureLiteral(ag);
685 // must ensure that it is asserted as a literal before we begin solving
686 Node lem = nm->mkNode(OR, ag, ag.negate());
687 d_quantEngine->getOutputChannel().requirePhase(ag, true);
688 d_quantEngine->getOutputChannel().lemma(lem);
689 d_enum_to_active_guard[e] = ag;
690 }
691 }
692
isEnumerator(Node e) const693 bool TermDbSygus::isEnumerator(Node e) const
694 {
695 return d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end();
696 }
697
getConjectureForEnumerator(Node e) const698 SynthConjecture* TermDbSygus::getConjectureForEnumerator(Node e) const
699 {
700 std::map<Node, SynthConjecture*>::const_iterator itm =
701 d_enum_to_conjecture.find(e);
702 if (itm != d_enum_to_conjecture.end()) {
703 return itm->second;
704 }
705 return nullptr;
706 }
707
getSynthFunForEnumerator(Node e) const708 Node TermDbSygus::getSynthFunForEnumerator(Node e) const
709 {
710 std::map<Node, Node>::const_iterator itsf = d_enum_to_synth_fun.find(e);
711 if (itsf != d_enum_to_synth_fun.end())
712 {
713 return itsf->second;
714 }
715 return Node::null();
716 }
717
getActiveGuardForEnumerator(Node e) const718 Node TermDbSygus::getActiveGuardForEnumerator(Node e) const
719 {
720 std::map<Node, Node>::const_iterator itag = d_enum_to_active_guard.find(e);
721 if (itag != d_enum_to_active_guard.end()) {
722 return itag->second;
723 }
724 return Node::null();
725 }
726
usingSymbolicConsForEnumerator(Node e) const727 bool TermDbSygus::usingSymbolicConsForEnumerator(Node e) const
728 {
729 std::map<Node, bool>::const_iterator itus = d_enum_to_using_sym_cons.find(e);
730 if (itus != d_enum_to_using_sym_cons.end())
731 {
732 return itus->second;
733 }
734 return false;
735 }
736
isVariableAgnosticEnumerator(Node e) const737 bool TermDbSygus::isVariableAgnosticEnumerator(Node e) const
738 {
739 std::map<Node, bool>::const_iterator itus = d_enum_var_agnostic.find(e);
740 if (itus != d_enum_var_agnostic.end())
741 {
742 return itus->second;
743 }
744 return false;
745 }
746
isBasicEnumerator(Node e) const747 bool TermDbSygus::isBasicEnumerator(Node e) const
748 {
749 std::map<Node, bool>::const_iterator itus = d_enum_basic.find(e);
750 if (itus != d_enum_basic.end())
751 {
752 return itus->second;
753 }
754 return false;
755 }
756
isPassiveEnumerator(Node e) const757 bool TermDbSygus::isPassiveEnumerator(Node e) const
758 {
759 std::map<Node, bool>::const_iterator itus = d_enum_active_gen.find(e);
760 if (itus != d_enum_active_gen.end())
761 {
762 return !itus->second;
763 }
764 return true;
765 }
766
getEnumerators(std::vector<Node> & mts)767 void TermDbSygus::getEnumerators(std::vector<Node>& mts)
768 {
769 for (std::map<Node, SynthConjecture*>::iterator itm =
770 d_enum_to_conjecture.begin();
771 itm != d_enum_to_conjecture.end();
772 ++itm)
773 {
774 mts.push_back( itm->first );
775 }
776 }
777
registerSymBreakLemma(Node e,Node lem,TypeNode tn,unsigned sz,bool isTempl)778 void TermDbSygus::registerSymBreakLemma(
779 Node e, Node lem, TypeNode tn, unsigned sz, bool isTempl)
780 {
781 d_enum_to_sb_lemmas[e].push_back(lem);
782 d_sb_lemma_to_type[lem] = tn;
783 d_sb_lemma_to_size[lem] = sz;
784 d_sb_lemma_to_isTempl[lem] = isTempl;
785 }
786
hasSymBreakLemmas(std::vector<Node> & enums) const787 bool TermDbSygus::hasSymBreakLemmas(std::vector<Node>& enums) const
788 {
789 if (!d_enum_to_sb_lemmas.empty())
790 {
791 for (std::pair<const Node, std::vector<Node> > sb : d_enum_to_sb_lemmas)
792 {
793 enums.push_back(sb.first);
794 }
795 return true;
796 }
797 return false;
798 }
799
getSymBreakLemmas(Node e,std::vector<Node> & lemmas) const800 void TermDbSygus::getSymBreakLemmas(Node e, std::vector<Node>& lemmas) const
801 {
802 std::map<Node, std::vector<Node> >::const_iterator itsb =
803 d_enum_to_sb_lemmas.find(e);
804 if (itsb != d_enum_to_sb_lemmas.end())
805 {
806 lemmas.insert(lemmas.end(), itsb->second.begin(), itsb->second.end());
807 }
808 }
809
getTypeForSymBreakLemma(Node lem) const810 TypeNode TermDbSygus::getTypeForSymBreakLemma(Node lem) const
811 {
812 std::map<Node, TypeNode>::const_iterator it = d_sb_lemma_to_type.find(lem);
813 Assert(it != d_sb_lemma_to_type.end());
814 return it->second;
815 }
getSizeForSymBreakLemma(Node lem) const816 unsigned TermDbSygus::getSizeForSymBreakLemma(Node lem) const
817 {
818 std::map<Node, unsigned>::const_iterator it = d_sb_lemma_to_size.find(lem);
819 Assert(it != d_sb_lemma_to_size.end());
820 return it->second;
821 }
822
isSymBreakLemmaTemplate(Node lem) const823 bool TermDbSygus::isSymBreakLemmaTemplate(Node lem) const
824 {
825 std::map<Node, bool>::const_iterator it = d_sb_lemma_to_isTempl.find(lem);
826 Assert(it != d_sb_lemma_to_isTempl.end());
827 return it->second;
828 }
829
clearSymBreakLemmas(Node e)830 void TermDbSygus::clearSymBreakLemmas(Node e) { d_enum_to_sb_lemmas.erase(e); }
831
isRegistered(TypeNode tn) const832 bool TermDbSygus::isRegistered(TypeNode tn) const
833 {
834 return d_register.find( tn )!=d_register.end();
835 }
836
sygusToBuiltinType(TypeNode tn)837 TypeNode TermDbSygus::sygusToBuiltinType( TypeNode tn ) {
838 Assert( isRegistered( tn ) );
839 return d_register[tn];
840 }
841
toStreamSygus(const char * c,Node n)842 void TermDbSygus::toStreamSygus(const char* c, Node n)
843 {
844 if (Trace.isOn(c))
845 {
846 if (n.isNull())
847 {
848 Trace(c) << n;
849 }
850 else
851 {
852 std::stringstream ss;
853 Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, n);
854 Trace(c) << ss.str();
855 }
856 }
857 }
858
computeMinTypeDepthInternal(TypeNode root_tn,TypeNode tn,unsigned type_depth)859 void TermDbSygus::computeMinTypeDepthInternal( TypeNode root_tn, TypeNode tn, unsigned type_depth ) {
860 std::map< TypeNode, unsigned >::iterator it = d_min_type_depth[root_tn].find( tn );
861 if( it==d_min_type_depth[root_tn].end() || type_depth<it->second ){
862 if (!tn.isDatatype())
863 {
864 // do not recurse to non-datatype types
865 return;
866 }
867 d_min_type_depth[root_tn][tn] = type_depth;
868 const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
869 //compute for connected types
870 for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
871 for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
872 computeMinTypeDepthInternal( root_tn, getArgType( dt[i], j ), type_depth+1 );
873 }
874 }
875 }
876 }
877
getMinTypeDepth(TypeNode root_tn,TypeNode tn)878 unsigned TermDbSygus::getMinTypeDepth( TypeNode root_tn, TypeNode tn ){
879 std::map< TypeNode, unsigned >::iterator it = d_min_type_depth[root_tn].find( tn );
880 if( it==d_min_type_depth[root_tn].end() ){
881 Assert( d_min_type_depth[root_tn].find( tn )!=d_min_type_depth[root_tn].end() );
882 return d_min_type_depth[root_tn][tn];
883 }else{
884 return it->second;
885 }
886 }
887
getMinTermSize(TypeNode tn)888 unsigned TermDbSygus::getMinTermSize( TypeNode tn ) {
889 Assert( isRegistered( tn ) );
890 std::map< TypeNode, unsigned >::iterator it = d_min_term_size.find( tn );
891 if( it==d_min_term_size.end() ){
892 const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
893 for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
894 if (dt[i].getNumArgs() == 0)
895 {
896 d_min_term_size[tn] = 0;
897 return 0;
898 }
899 }
900 // TODO : improve
901 d_min_term_size[tn] = 1;
902 return 1;
903 }else{
904 return it->second;
905 }
906 }
907
getMinConsTermSize(TypeNode tn,unsigned cindex)908 unsigned TermDbSygus::getMinConsTermSize( TypeNode tn, unsigned cindex ) {
909 Assert( isRegistered( tn ) );
910 std::map< unsigned, unsigned >::iterator it = d_min_cons_term_size[tn].find( cindex );
911 if( it==d_min_cons_term_size[tn].end() ){
912 const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
913 Assert( cindex<dt.getNumConstructors() );
914 unsigned ret = 0;
915 if( dt[cindex].getNumArgs()>0 ){
916 ret = 1;
917 for( unsigned i=0; i<dt[cindex].getNumArgs(); i++ ){
918 ret += getMinTermSize( getArgType( dt[cindex], i ) );
919 }
920 }
921 d_min_cons_term_size[tn][cindex] = ret;
922 return ret;
923 }else{
924 return it->second;
925 }
926 }
927
getSelectorWeight(TypeNode tn,Node sel)928 unsigned TermDbSygus::getSelectorWeight(TypeNode tn, Node sel)
929 {
930 std::map<TypeNode, std::map<Node, unsigned> >::iterator itsw =
931 d_sel_weight.find(tn);
932 if (itsw == d_sel_weight.end())
933 {
934 d_sel_weight[tn].clear();
935 itsw = d_sel_weight.find(tn);
936 Type t = tn.toType();
937 const Datatype& dt = static_cast<DatatypeType>(t).getDatatype();
938 Trace("sygus-db") << "Compute selector weights for " << dt.getName()
939 << std::endl;
940 for (unsigned i = 0, size = dt.getNumConstructors(); i < size; i++)
941 {
942 unsigned cw = dt[i].getWeight();
943 for (unsigned j = 0, size2 = dt[i].getNumArgs(); j < size2; j++)
944 {
945 Node csel = Node::fromExpr(dt[i].getSelectorInternal(t, j));
946 std::map<Node, unsigned>::iterator its = itsw->second.find(csel);
947 if (its == itsw->second.end() || cw < its->second)
948 {
949 d_sel_weight[tn][csel] = cw;
950 Trace("sygus-db") << " w(" << csel << ") <= " << cw << std::endl;
951 }
952 }
953 }
954 }
955 Assert(itsw->second.find(sel) != itsw->second.end());
956 return itsw->second[sel];
957 }
958
getSubfieldTypes(TypeNode tn,std::vector<TypeNode> & sf_types)959 void TermDbSygus::getSubfieldTypes(TypeNode tn, std::vector<TypeNode>& sf_types)
960 {
961 std::map<TypeNode, std::map<TypeNode, unsigned> >::iterator it =
962 d_min_type_depth.find(tn);
963 Assert(it != d_min_type_depth.end());
964 for (const std::pair<const TypeNode, unsigned>& st : it->second)
965 {
966 sf_types.push_back(st.first);
967 }
968 }
969
getKindConsNum(TypeNode tn,Kind k)970 int TermDbSygus::getKindConsNum( TypeNode tn, Kind k ) {
971 Assert( isRegistered( tn ) );
972 std::map< TypeNode, std::map< Kind, int > >::iterator itt = d_kinds.find( tn );
973 if( itt!=d_kinds.end() ){
974 std::map< Kind, int >::iterator it = itt->second.find( k );
975 if( it!=itt->second.end() ){
976 return it->second;
977 }
978 }
979 return -1;
980 }
981
getConstConsNum(TypeNode tn,Node n)982 int TermDbSygus::getConstConsNum( TypeNode tn, Node n ){
983 Assert( isRegistered( tn ) );
984 std::map< TypeNode, std::map< Node, int > >::iterator itt = d_consts.find( tn );
985 if( itt!=d_consts.end() ){
986 std::map< Node, int >::iterator it = itt->second.find( n );
987 if( it!=itt->second.end() ){
988 return it->second;
989 }
990 }
991 return -1;
992 }
993
getOpConsNum(TypeNode tn,Node n)994 int TermDbSygus::getOpConsNum( TypeNode tn, Node n ) {
995 std::map< Node, int >::iterator it = d_ops[tn].find( n );
996 if( it!=d_ops[tn].end() ){
997 return it->second;
998 }else{
999 return -1;
1000 }
1001 }
1002
hasKind(TypeNode tn,Kind k)1003 bool TermDbSygus::hasKind( TypeNode tn, Kind k ) {
1004 return getKindConsNum( tn, k )!=-1;
1005 }
hasConst(TypeNode tn,Node n)1006 bool TermDbSygus::hasConst( TypeNode tn, Node n ) {
1007 return getConstConsNum( tn, n )!=-1;
1008 }
hasOp(TypeNode tn,Node n)1009 bool TermDbSygus::hasOp( TypeNode tn, Node n ) {
1010 return getOpConsNum( tn, n )!=-1;
1011 }
1012
getConsNumOp(TypeNode tn,int i)1013 Node TermDbSygus::getConsNumOp( TypeNode tn, int i ) {
1014 Assert( isRegistered( tn ) );
1015 std::map< TypeNode, std::map< int, Node > >::iterator itt = d_arg_ops.find( tn );
1016 if( itt!=d_arg_ops.end() ){
1017 std::map< int, Node >::iterator itn = itt->second.find( i );
1018 if( itn!=itt->second.end() ){
1019 return itn->second;
1020 }
1021 }
1022 return Node::null();
1023 }
1024
getConsNumConst(TypeNode tn,int i)1025 Node TermDbSygus::getConsNumConst( TypeNode tn, int i ) {
1026 Assert( isRegistered( tn ) );
1027 std::map< TypeNode, std::map< int, Node > >::iterator itt = d_arg_const.find( tn );
1028 if( itt!=d_arg_const.end() ){
1029 std::map< int, Node >::iterator itn = itt->second.find( i );
1030 if( itn!=itt->second.end() ){
1031 return itn->second;
1032 }
1033 }
1034 return Node::null();
1035 }
1036
getConsNumKind(TypeNode tn,int i)1037 Kind TermDbSygus::getConsNumKind( TypeNode tn, int i ) {
1038 Assert( isRegistered( tn ) );
1039 std::map< TypeNode, std::map< int, Kind > >::iterator itt = d_arg_kind.find( tn );
1040 if( itt!=d_arg_kind.end() ){
1041 std::map< int, Kind >::iterator itk = itt->second.find( i );
1042 if( itk!=itt->second.end() ){
1043 return itk->second;
1044 }
1045 }
1046 return UNDEFINED_KIND;
1047 }
1048
isKindArg(TypeNode tn,int i)1049 bool TermDbSygus::isKindArg( TypeNode tn, int i ) {
1050 return getConsNumKind( tn, i )!=UNDEFINED_KIND;
1051 }
1052
isConstArg(TypeNode tn,int i)1053 bool TermDbSygus::isConstArg( TypeNode tn, int i ) {
1054 Assert( isRegistered( tn ) );
1055 std::map< TypeNode, std::map< int, Node > >::iterator itt = d_arg_const.find( tn );
1056 if( itt!=d_arg_const.end() ){
1057 return itt->second.find( i )!=itt->second.end();
1058 }else{
1059 return false;
1060 }
1061 }
1062
getArgType(const DatatypeConstructor & c,unsigned i) const1063 TypeNode TermDbSygus::getArgType(const DatatypeConstructor& c, unsigned i) const
1064 {
1065 Assert(i < c.getNumArgs());
1066 return TypeNode::fromType(
1067 static_cast<SelectorType>(c[i].getType()).getRangeType());
1068 }
1069
isTypeMatch(const DatatypeConstructor & c1,const DatatypeConstructor & c2)1070 bool TermDbSygus::isTypeMatch( const DatatypeConstructor& c1, const DatatypeConstructor& c2 ) {
1071 if( c1.getNumArgs()!=c2.getNumArgs() ){
1072 return false;
1073 }else{
1074 for( unsigned i=0; i<c1.getNumArgs(); i++ ){
1075 if( getArgType( c1, i )!=getArgType( c2, i ) ){
1076 return false;
1077 }
1078 }
1079 return true;
1080 }
1081 }
1082
getAnyConstantConsNum(TypeNode tn) const1083 int TermDbSygus::getAnyConstantConsNum(TypeNode tn) const
1084 {
1085 Assert(isRegistered(tn));
1086 std::map<TypeNode, unsigned>::const_iterator itt =
1087 d_sym_cons_any_constant.find(tn);
1088 if (itt != d_sym_cons_any_constant.end())
1089 {
1090 return static_cast<int>(itt->second);
1091 }
1092 return -1;
1093 }
1094
hasSubtermSymbolicCons(TypeNode tn) const1095 bool TermDbSygus::hasSubtermSymbolicCons(TypeNode tn) const
1096 {
1097 return d_has_subterm_sym_cons.find(tn) != d_has_subterm_sym_cons.end();
1098 }
1099
getSubclassForVar(TypeNode tn,Node n) const1100 unsigned TermDbSygus::getSubclassForVar(TypeNode tn, Node n) const
1101 {
1102 std::map<TypeNode, std::map<Node, unsigned> >::const_iterator itc =
1103 d_var_subclass_id.find(tn);
1104 if (itc == d_var_subclass_id.end())
1105 {
1106 Assert(false);
1107 return 0;
1108 }
1109 std::map<Node, unsigned>::const_iterator itcc = itc->second.find(n);
1110 if (itcc == itc->second.end())
1111 {
1112 Assert(false);
1113 return 0;
1114 }
1115 return itcc->second;
1116 }
1117
getNumSubclassVars(TypeNode tn,unsigned sc) const1118 unsigned TermDbSygus::getNumSubclassVars(TypeNode tn, unsigned sc) const
1119 {
1120 std::map<TypeNode, std::map<unsigned, std::vector<Node> > >::const_iterator
1121 itv = d_var_subclass_list.find(tn);
1122 if (itv == d_var_subclass_list.end())
1123 {
1124 Assert(false);
1125 return 0;
1126 }
1127 std::map<unsigned, std::vector<Node> >::const_iterator itvv =
1128 itv->second.find(sc);
1129 if (itvv == itv->second.end())
1130 {
1131 Assert(false);
1132 return 0;
1133 }
1134 return itvv->second.size();
1135 }
getVarSubclassIndex(TypeNode tn,unsigned sc,unsigned i) const1136 Node TermDbSygus::getVarSubclassIndex(TypeNode tn,
1137 unsigned sc,
1138 unsigned i) const
1139 {
1140 std::map<TypeNode, std::map<unsigned, std::vector<Node> > >::const_iterator
1141 itv = d_var_subclass_list.find(tn);
1142 if (itv == d_var_subclass_list.end())
1143 {
1144 Assert(false);
1145 return Node::null();
1146 }
1147 std::map<unsigned, std::vector<Node> >::const_iterator itvv =
1148 itv->second.find(sc);
1149 if (itvv == itv->second.end() || i >= itvv->second.size())
1150 {
1151 Assert(false);
1152 return Node::null();
1153 }
1154 return itvv->second[i];
1155 }
1156
getIndexInSubclassForVar(TypeNode tn,Node v,unsigned & index) const1157 bool TermDbSygus::getIndexInSubclassForVar(TypeNode tn,
1158 Node v,
1159 unsigned& index) const
1160 {
1161 std::map<TypeNode, std::map<Node, unsigned> >::const_iterator itv =
1162 d_var_subclass_list_index.find(tn);
1163 if (itv == d_var_subclass_list_index.end())
1164 {
1165 return false;
1166 }
1167 std::map<Node, unsigned>::const_iterator itvv = itv->second.find(v);
1168 if (itvv == itv->second.end())
1169 {
1170 return false;
1171 }
1172 index = itvv->second;
1173 return true;
1174 }
1175
isSymbolicConsApp(Node n) const1176 bool TermDbSygus::isSymbolicConsApp(Node n) const
1177 {
1178 if (n.getKind() != APPLY_CONSTRUCTOR)
1179 {
1180 return false;
1181 }
1182 TypeNode tn = n.getType();
1183 Assert(tn.isDatatype());
1184 const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
1185 Assert(dt.isSygus());
1186 unsigned cindex = datatypes::DatatypesRewriter::indexOf(n.getOperator());
1187 Node sygusOp = Node::fromExpr(dt[cindex].getSygusOp());
1188 // it is symbolic if it represents "any constant"
1189 return sygusOp.getAttribute(SygusAnyConstAttribute());
1190 }
1191
canConstructKind(TypeNode tn,Kind k,std::vector<TypeNode> & argts,bool aggr)1192 bool TermDbSygus::canConstructKind(TypeNode tn,
1193 Kind k,
1194 std::vector<TypeNode>& argts,
1195 bool aggr)
1196 {
1197 int c = getKindConsNum(tn, k);
1198 const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
1199 if (c != -1)
1200 {
1201 for (unsigned i = 0, nargs = dt[c].getNumArgs(); i < nargs; i++)
1202 {
1203 argts.push_back(TypeNode::fromType(dt[c].getArgType(i)));
1204 }
1205 return true;
1206 }
1207 if (!options::sygusSymBreakAgg())
1208 {
1209 return false;
1210 }
1211 if (sygusToBuiltinType(tn).isBoolean())
1212 {
1213 if (k == ITE)
1214 {
1215 // ite( b1, b2, b3 ) <---- and( or( ~b1, b2 ), or( b1, b3 ) )
1216 std::vector<TypeNode> conj_types;
1217 if (canConstructKind(tn, AND, conj_types, true) && conj_types.size() == 2)
1218 {
1219 bool success = true;
1220 std::vector<TypeNode> disj_types[2];
1221 for (unsigned c = 0; c < 2; c++)
1222 {
1223 if (!canConstructKind(conj_types[c], OR, disj_types[c], true)
1224 || disj_types[c].size() != 2)
1225 {
1226 success = false;
1227 break;
1228 }
1229 }
1230 if (success)
1231 {
1232 for (unsigned r = 0; r < 2; r++)
1233 {
1234 for (unsigned d = 0, size = disj_types[r].size(); d < size; d++)
1235 {
1236 TypeNode dtn = disj_types[r][d];
1237 // must have negation that occurs in the other conjunct
1238 std::vector<TypeNode> ntypes;
1239 if (canConstructKind(dtn, NOT, ntypes) && ntypes.size() == 1)
1240 {
1241 TypeNode ntn = ntypes[0];
1242 for (unsigned dd = 0, size = disj_types[1 - r].size();
1243 dd < size;
1244 dd++)
1245 {
1246 if (disj_types[1 - r][dd] == ntn)
1247 {
1248 argts.push_back(ntn);
1249 argts.push_back(disj_types[r][d]);
1250 argts.push_back(disj_types[1 - r][1 - dd]);
1251 if (Trace.isOn("sygus-cons-kind"))
1252 {
1253 Trace("sygus-cons-kind")
1254 << "Can construct kind " << k << " in " << tn
1255 << " via child types:" << std::endl;
1256 for (unsigned i = 0; i < 3; i++)
1257 {
1258 Trace("sygus-cons-kind")
1259 << " " << argts[i] << std::endl;
1260 }
1261 }
1262 return true;
1263 }
1264 }
1265 }
1266 }
1267 }
1268 }
1269 }
1270 }
1271 }
1272 // could try aggressive inferences here, such as
1273 // (and b1 b2) <---- (not (or (not b1) (not b2)))
1274 // (or b1 b2) <---- (not (and (not b1) (not b2)))
1275 return false;
1276 }
1277
minimizeBuiltinTerm(Node n)1278 Node TermDbSygus::minimizeBuiltinTerm( Node n ) {
1279 if( ( n.getKind()==EQUAL || n.getKind()==LEQ || n.getKind()==LT || n.getKind()==GEQ || n.getKind()==GT ) &&
1280 ( n[0].getType().isInteger() || n[0].getType().isReal() ) ){
1281 bool changed = false;
1282 std::vector< Node > mon[2];
1283 for( unsigned r=0; r<2; r++ ){
1284 unsigned ro = r==0 ? 1 : 0;
1285 Node c;
1286 Node nc;
1287 if( n[r].getKind()==PLUS ){
1288 for( unsigned i=0; i<n[r].getNumChildren(); i++ ){
1289 if (ArithMSum::getMonomial(n[r][i], c, nc)
1290 && c.getConst<Rational>().isNegativeOne())
1291 {
1292 mon[ro].push_back( nc );
1293 changed = true;
1294 }else{
1295 if( !n[r][i].isConst() || !n[r][i].getConst<Rational>().isZero() ){
1296 mon[r].push_back( n[r][i] );
1297 }
1298 }
1299 }
1300 }else{
1301 if (ArithMSum::getMonomial(n[r], c, nc)
1302 && c.getConst<Rational>().isNegativeOne())
1303 {
1304 mon[ro].push_back( nc );
1305 changed = true;
1306 }else{
1307 if( !n[r].isConst() || !n[r].getConst<Rational>().isZero() ){
1308 mon[r].push_back( n[r] );
1309 }
1310 }
1311 }
1312 }
1313 if( changed ){
1314 Node nn[2];
1315 for( unsigned r=0; r<2; r++ ){
1316 nn[r] = mon[r].size()==0 ? NodeManager::currentNM()->mkConst( Rational(0) ) : ( mon[r].size()==1 ? mon[r][0] : NodeManager::currentNM()->mkNode( PLUS, mon[r] ) );
1317 }
1318 return NodeManager::currentNM()->mkNode( n.getKind(), nn[0], nn[1] );
1319 }
1320 }
1321 return n;
1322 }
1323
expandBuiltinTerm(Node t)1324 Node TermDbSygus::expandBuiltinTerm( Node t ){
1325 if( t.getKind()==EQUAL ){
1326 if( t[0].getType().isReal() ){
1327 return NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, t[0], t[1] ),
1328 NodeManager::currentNM()->mkNode( LEQ, t[1], t[0] ) );
1329 }else if( t[0].getType().isBoolean() ){
1330 return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ),
1331 NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[1].negate() ) );
1332 }
1333 }else if( t.getKind()==ITE && t.getType().isBoolean() ){
1334 return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ),
1335 NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[2] ) );
1336 }
1337 return Node::null();
1338 }
1339
1340
getComparisonKind(TypeNode tn)1341 Kind TermDbSygus::getComparisonKind( TypeNode tn ) {
1342 if( tn.isInteger() || tn.isReal() ){
1343 return LT;
1344 }else if( tn.isBitVector() ){
1345 return BITVECTOR_ULT;
1346 }else{
1347 return UNDEFINED_KIND;
1348 }
1349 }
1350
getPlusKind(TypeNode tn,bool is_neg)1351 Kind TermDbSygus::getPlusKind( TypeNode tn, bool is_neg ) {
1352 if( tn.isInteger() || tn.isReal() ){
1353 return is_neg ? MINUS : PLUS;
1354 }else if( tn.isBitVector() ){
1355 return is_neg ? BITVECTOR_SUB : BITVECTOR_PLUS;
1356 }else{
1357 return UNDEFINED_KIND;
1358 }
1359 }
1360
involvesDivByZero(Node n,std::map<Node,bool> & visited)1361 bool TermDbSygus::involvesDivByZero( Node n, std::map< Node, bool >& visited ){
1362 if( visited.find( n )==visited.end() ){
1363 visited[n] = true;
1364 Kind k = n.getKind();
1365 if( k==DIVISION || k==DIVISION_TOTAL || k==INTS_DIVISION || k==INTS_DIVISION_TOTAL ||
1366 k==INTS_MODULUS || k==INTS_MODULUS_TOTAL ){
1367 if( n[1].isConst() ){
1368 if (n[1]
1369 == d_quantEngine->getTermUtil()->getTypeValue(n[1].getType(), 0))
1370 {
1371 return true;
1372 }
1373 }else{
1374 // if it has free variables it might be a non-zero constant
1375 if( !hasFreeVar( n[1] ) ){
1376 return true;
1377 }
1378 }
1379 }
1380 for( unsigned i=0; i<n.getNumChildren(); i++ ){
1381 if( involvesDivByZero( n[i], visited ) ){
1382 return true;
1383 }
1384 }
1385 }
1386 return false;
1387 }
1388
involvesDivByZero(Node n)1389 bool TermDbSygus::involvesDivByZero( Node n ) {
1390 std::map< Node, bool > visited;
1391 return involvesDivByZero( n, visited );
1392 }
1393
doStrReplace(std::string & str,const std::string & oldStr,const std::string & newStr)1394 void doStrReplace(std::string& str, const std::string& oldStr, const std::string& newStr){
1395 size_t pos = 0;
1396 while((pos = str.find(oldStr, pos)) != std::string::npos){
1397 str.replace(pos, oldStr.length(), newStr);
1398 pos += newStr.length();
1399 }
1400 }
1401
getAnchor(Node n)1402 Node TermDbSygus::getAnchor( Node n ) {
1403 if( n.getKind()==APPLY_SELECTOR_TOTAL ){
1404 return getAnchor( n[0] );
1405 }else{
1406 return n;
1407 }
1408 }
1409
getAnchorDepth(Node n)1410 unsigned TermDbSygus::getAnchorDepth( Node n ) {
1411 if( n.getKind()==APPLY_SELECTOR_TOTAL ){
1412 return 1+getAnchorDepth( n[0] );
1413 }else{
1414 return 0;
1415 }
1416 }
1417
unfold(Node en,std::map<Node,Node> & vtm,std::vector<Node> & exp,bool track_exp)1418 Node TermDbSygus::unfold( Node en, std::map< Node, Node >& vtm, std::vector< Node >& exp, bool track_exp ) {
1419 if (en.getKind() != DT_SYGUS_EVAL)
1420 {
1421 Assert(en.isConst());
1422 return en;
1423 }
1424 Trace("sygus-db-debug") << "Unfold : " << en << std::endl;
1425 Node ev = en[0];
1426 if (track_exp)
1427 {
1428 std::map<Node, Node>::iterator itv = vtm.find(en[0]);
1429 Assert(itv != vtm.end());
1430 if (itv != vtm.end())
1431 {
1432 ev = itv->second;
1433 }
1434 Assert(en[0].getType() == ev.getType());
1435 Assert(ev.isConst());
1436 }
1437 Assert(ev.getKind() == kind::APPLY_CONSTRUCTOR);
1438 std::vector<Node> args;
1439 for (unsigned i = 1, nchild = en.getNumChildren(); i < nchild; i++)
1440 {
1441 args.push_back(en[i]);
1442 }
1443
1444 Type headType = en[0].getType().toType();
1445 NodeManager* nm = NodeManager::currentNM();
1446 const Datatype& dt = static_cast<DatatypeType>(headType).getDatatype();
1447 unsigned i = datatypes::DatatypesRewriter::indexOf(ev.getOperator());
1448 if (track_exp)
1449 {
1450 // explanation
1451 Node ee = nm->mkNode(
1452 kind::APPLY_TESTER, Node::fromExpr(dt[i].getTester()), en[0]);
1453 if (std::find(exp.begin(), exp.end(), ee) == exp.end())
1454 {
1455 exp.push_back(ee);
1456 }
1457 }
1458 // if we are a symbolic constructor, unfolding returns the subterm itself
1459 Node sop = Node::fromExpr(dt[i].getSygusOp());
1460 if (sop.getAttribute(SygusAnyConstAttribute()))
1461 {
1462 Trace("sygus-db-debug") << "...it is an any-constant constructor"
1463 << std::endl;
1464 Assert(dt[i].getNumArgs() == 1);
1465 if (en[0].getKind() == APPLY_CONSTRUCTOR)
1466 {
1467 return en[0][0];
1468 }
1469 else
1470 {
1471 return nm->mkNode(
1472 APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headType, 0), en[0]);
1473 }
1474 }
1475
1476 Assert(!dt.isParametric());
1477 std::map<int, Node> pre;
1478 for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
1479 {
1480 std::vector<Node> cc;
1481 Node s;
1482 // get the j^th subfield of en
1483 if (en[0].getKind() == kind::APPLY_CONSTRUCTOR)
1484 {
1485 // if it is a concrete constructor application, as an optimization,
1486 // just return the argument
1487 s = en[0][j];
1488 }
1489 else
1490 {
1491 s = nm->mkNode(kind::APPLY_SELECTOR_TOTAL,
1492 dt[i].getSelectorInternal(headType, j),
1493 en[0]);
1494 }
1495 cc.push_back(s);
1496 if (track_exp)
1497 {
1498 // update vtm map
1499 vtm[s] = ev[j];
1500 }
1501 cc.insert(cc.end(), args.begin(), args.end());
1502 pre[j] = nm->mkNode(DT_SYGUS_EVAL, cc);
1503 }
1504 Node ret = mkGeneric(dt, i, pre);
1505 // if it is a variable, apply the substitution
1506 if (ret.getKind() == kind::BOUND_VARIABLE)
1507 {
1508 Assert(ret.hasAttribute(SygusVarNumAttribute()));
1509 int i = ret.getAttribute(SygusVarNumAttribute());
1510 Assert(Node::fromExpr(dt.getSygusVarList())[i] == ret);
1511 return args[i];
1512 }
1513 ret = Rewriter::rewrite(ret);
1514 return ret;
1515 }
1516
unfold(Node en)1517 Node TermDbSygus::unfold(Node en)
1518 {
1519 std::map<Node, Node> vtm;
1520 std::vector<Node> exp;
1521 return unfold(en, vtm, exp, false);
1522 }
1523
getEagerUnfold(Node n,std::map<Node,Node> & visited)1524 Node TermDbSygus::getEagerUnfold( Node n, std::map< Node, Node >& visited ) {
1525 std::map< Node, Node >::iterator itv = visited.find( n );
1526 if( itv==visited.end() ){
1527 Trace("cegqi-eager-debug") << "getEagerUnfold " << n << std::endl;
1528 Node ret;
1529 if (n.getKind() == DT_SYGUS_EVAL)
1530 {
1531 TypeNode tn = n[0].getType();
1532 Trace("cegqi-eager-debug") << "check " << n[0].getType() << std::endl;
1533 if( tn.isDatatype() ){
1534 const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
1535 if( dt.isSygus() ){
1536 Trace("cegqi-eager") << "Unfold eager : " << n << std::endl;
1537 Node bTerm = sygusToBuiltin( n[0], tn );
1538 Trace("cegqi-eager") << "Built-in term : " << bTerm << std::endl;
1539 std::vector< Node > vars;
1540 std::vector< Node > subs;
1541 Node var_list = Node::fromExpr( dt.getSygusVarList() );
1542 Assert( var_list.getNumChildren()+1==n.getNumChildren() );
1543 for( unsigned j=0; j<var_list.getNumChildren(); j++ ){
1544 vars.push_back( var_list[j] );
1545 }
1546 for( unsigned j=1; j<n.getNumChildren(); j++ ){
1547 Node nc = getEagerUnfold( n[j], visited );
1548 subs.push_back( nc );
1549 Assert(subs[j - 1].getType().isComparableTo(
1550 var_list[j - 1].getType()));
1551 }
1552 Assert( vars.size()==subs.size() );
1553 bTerm = bTerm.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
1554 Trace("cegqi-eager") << "Built-in term after subs : " << bTerm << std::endl;
1555 Trace("cegqi-eager-debug") << "Types : " << bTerm.getType() << " " << n.getType() << std::endl;
1556 Assert(n.getType().isComparableTo(bTerm.getType()));
1557 ret = bTerm;
1558 }
1559 }
1560 }
1561 if( ret.isNull() ){
1562 if( n.getKind()!=FORALL ){
1563 bool childChanged = false;
1564 std::vector< Node > children;
1565 for( unsigned i=0; i<n.getNumChildren(); i++ ){
1566 Node nc = getEagerUnfold( n[i], visited );
1567 childChanged = childChanged || n[i]!=nc;
1568 children.push_back( nc );
1569 }
1570 if( childChanged ){
1571 if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
1572 children.insert( children.begin(), n.getOperator() );
1573 }
1574 ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
1575 }
1576 }
1577 if( ret.isNull() ){
1578 ret = n;
1579 }
1580 }
1581 visited[n] = ret;
1582 return ret;
1583 }else{
1584 return itv->second;
1585 }
1586 }
1587
evaluateBuiltin(TypeNode tn,Node bn,std::vector<Node> & args,bool tryEval)1588 Node TermDbSygus::evaluateBuiltin(TypeNode tn,
1589 Node bn,
1590 std::vector<Node>& args,
1591 bool tryEval)
1592 {
1593 if( !args.empty() ){
1594 std::map< TypeNode, std::vector< Node > >::iterator it = d_var_list.find( tn );
1595 Assert( it!=d_var_list.end() );
1596 Assert( it->second.size()==args.size() );
1597
1598 Node res;
1599 if (tryEval && options::sygusEvalOpt())
1600 {
1601 // Try evaluating, which is much faster than substitution+rewriting.
1602 // This may fail if there is a subterm of bn under the
1603 // substitution that is not constant, or if an operator in bn is not
1604 // supported by the evaluator
1605 res = d_eval->eval(bn, it->second, args);
1606 }
1607 if (!res.isNull())
1608 {
1609 Assert(res
1610 == Rewriter::rewrite(bn.substitute(it->second.begin(),
1611 it->second.end(),
1612 args.begin(),
1613 args.end())));
1614 return res;
1615 }
1616 else
1617 {
1618 return Rewriter::rewrite(bn.substitute(
1619 it->second.begin(), it->second.end(), args.begin(), args.end()));
1620 }
1621 }else{
1622 return Rewriter::rewrite( bn );
1623 }
1624 }
1625
evaluateWithUnfolding(Node n,std::unordered_map<Node,Node,NodeHashFunction> & visited)1626 Node TermDbSygus::evaluateWithUnfolding(
1627 Node n, std::unordered_map<Node, Node, NodeHashFunction>& visited)
1628 {
1629 std::unordered_map<Node, Node, NodeHashFunction>::iterator it =
1630 visited.find(n);
1631 if( it==visited.end() ){
1632 Node ret = n;
1633 while (ret.getKind() == DT_SYGUS_EVAL
1634 && ret[0].getKind() == APPLY_CONSTRUCTOR)
1635 {
1636 ret = unfold( ret );
1637 }
1638 if( ret.getNumChildren()>0 ){
1639 std::vector< Node > children;
1640 if( ret.getMetaKind() == kind::metakind::PARAMETERIZED ){
1641 children.push_back( ret.getOperator() );
1642 }
1643 bool childChanged = false;
1644 for( unsigned i=0; i<ret.getNumChildren(); i++ ){
1645 Node nc = evaluateWithUnfolding( ret[i], visited );
1646 childChanged = childChanged || nc!=ret[i];
1647 children.push_back( nc );
1648 }
1649 if( childChanged ){
1650 ret = NodeManager::currentNM()->mkNode( ret.getKind(), children );
1651 }
1652 ret = getExtRewriter()->extendedRewrite(ret);
1653 }
1654 visited[n] = ret;
1655 return ret;
1656 }else{
1657 return it->second;
1658 }
1659 }
1660
evaluateWithUnfolding(Node n)1661 Node TermDbSygus::evaluateWithUnfolding( Node n ) {
1662 std::unordered_map<Node, Node, NodeHashFunction> visited;
1663 return evaluateWithUnfolding( n, visited );
1664 }
1665
isEvaluationPoint(Node n) const1666 bool TermDbSygus::isEvaluationPoint(Node n) const
1667 {
1668 if (n.getKind() != DT_SYGUS_EVAL)
1669 {
1670 return false;
1671 }
1672 if (!n[0].isVar())
1673 {
1674 return false;
1675 }
1676 for (unsigned i = 1, nchild = n.getNumChildren(); i < nchild; i++)
1677 {
1678 if (!n[i].isConst())
1679 {
1680 return false;
1681 }
1682 }
1683 return true;
1684 }
1685
1686 }/* CVC4::theory::quantifiers namespace */
1687 }/* CVC4::theory namespace */
1688 }/* CVC4 namespace */
1689
1690