1 /********************* */
2 /*! \file sygus_sampler.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Haniel Barbosa
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 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
12 ** \brief Implementation of sygus_sampler
15 #include "theory/quantifiers/sygus_sampler.h"
17 #include "options/base_options.h"
18 #include "options/quantifiers_options.h"
19 #include "printer/printer.h"
20 #include "theory/quantifiers/lazy_trie.h"
21 #include "util/bitvector.h"
22 #include "util/random.h"
23 #include "util/sampler.h"
27 namespace quantifiers
{
29 SygusSampler::SygusSampler()
30 : d_tds(nullptr), d_use_sygus_type(false), d_is_valid(false)
34 void SygusSampler::initialize(TypeNode tn
,
35 std::vector
<Node
>& vars
,
40 d_use_sygus_type
= false;
43 d_ftn
= TypeNode::null();
46 d_rvalue_cindices
.clear();
47 d_rvalue_null_cindices
.clear();
48 d_rstring_alphabet
.clear();
49 d_var_sygus_types
.clear();
50 d_const_sygus_types
.clear();
51 d_vars
.insert(d_vars
.end(), vars
.begin(), vars
.end());
52 std::map
<TypeNode
, unsigned> type_to_type_id
;
53 unsigned type_id_counter
= 0;
54 for (const Node
& sv
: d_vars
)
56 TypeNode svt
= sv
.getType();
60 tnid
= type_id_counter
;
65 std::map
<TypeNode
, unsigned>::iterator itt
= type_to_type_id
.find(svt
);
66 if (itt
== type_to_type_id
.end())
68 type_to_type_id
[svt
] = type_id_counter
;
76 Trace("sygus-sample-debug")
77 << "Type id for " << sv
<< " is " << tnid
<< std::endl
;
78 d_var_index
[sv
] = d_type_vars
[tnid
].size();
79 d_type_vars
[tnid
].push_back(sv
);
80 d_type_ids
[sv
] = tnid
;
82 initializeSamples(nsamples
);
85 void SygusSampler::initializeSygus(TermDbSygus
* tds
,
91 d_use_sygus_type
= useSygusType
;
94 Assert(d_ftn
.isDatatype());
95 const Datatype
& dt
= static_cast<DatatypeType
>(d_ftn
.toType()).getDatatype();
97 d_tn
= TypeNode::fromType(dt
.getSygusType());
99 Trace("sygus-sample") << "Register sampler for " << f
<< std::endl
;
105 d_rvalue_cindices
.clear();
106 d_rvalue_null_cindices
.clear();
107 d_var_sygus_types
.clear();
108 // get the sygus variable list
109 Node var_list
= Node::fromExpr(dt
.getSygusVarList());
110 if (!var_list
.isNull())
112 for (const Node
& sv
: var_list
)
114 d_vars
.push_back(sv
);
117 // register sygus type
118 registerSygusType(d_ftn
);
119 // Variables are associated with type ids based on the set of sygus types they
121 std::map
<Node
, unsigned> var_to_type_id
;
122 unsigned type_id_counter
= 0;
123 for (const Node
& sv
: d_vars
)
125 TypeNode svt
= sv
.getType();
126 // is it equivalent to a previous variable?
127 for (const std::pair
<Node
, unsigned>& v
: var_to_type_id
)
130 if (svc
.getType() == svt
)
132 if (d_var_sygus_types
[sv
].size() == d_var_sygus_types
[svc
].size())
135 for (unsigned t
= 0, size
= d_var_sygus_types
[sv
].size(); t
< size
;
138 if (d_var_sygus_types
[sv
][t
] != d_var_sygus_types
[svc
][t
])
146 var_to_type_id
[sv
] = var_to_type_id
[svc
];
151 if (var_to_type_id
.find(sv
) == var_to_type_id
.end())
153 var_to_type_id
[sv
] = type_id_counter
;
156 unsigned tnid
= var_to_type_id
[sv
];
157 Trace("sygus-sample-debug")
158 << "Type id for " << sv
<< " is " << tnid
<< std::endl
;
159 d_var_index
[sv
] = d_type_vars
[tnid
].size();
160 d_type_vars
[tnid
].push_back(sv
);
161 d_type_ids
[sv
] = tnid
;
164 initializeSamples(nsamples
);
167 void SygusSampler::initializeSamples(unsigned nsamples
)
170 std::vector
<TypeNode
> types
;
171 for (const Node
& v
: d_vars
)
173 TypeNode vt
= v
.getType();
175 Trace("sygus-sample") << " var #" << types
.size() << " : " << v
<< " : "
178 std::map
<unsigned, std::map
<Node
, std::vector
<TypeNode
> >::iterator
> sts
;
179 if (options::sygusSampleGrammar())
181 for (unsigned j
= 0, size
= types
.size(); j
< size
; j
++)
183 sts
[j
] = d_var_sygus_types
.find(d_vars
[j
]);
187 unsigned nduplicates
= 0;
188 for (unsigned i
= 0; i
< nsamples
; i
++)
190 std::vector
<Node
> sample_pt
;
191 for (unsigned j
= 0, size
= types
.size(); j
< size
; j
++)
195 if (options::sygusSampleGrammar())
197 // choose a random start sygus type, if possible
198 if (sts
[j
] != d_var_sygus_types
.end())
200 unsigned ntypes
= sts
[j
]->second
.size();
203 unsigned index
= Random::getRandom().pick(0, ntypes
- 1);
206 // currently hard coded to 0.0, 0.5
207 r
= getSygusRandomValue(sts
[j
]->second
[index
], 0.0, 0.5);
214 r
= getRandomValue(types
[j
]);
220 sample_pt
.push_back(r
);
222 if (d_samples_trie
.add(sample_pt
))
224 if (Trace
.isOn("sygus-sample"))
226 Trace("sygus-sample") << "Sample point #" << i
<< " : ";
227 for (const Node
& r
: sample_pt
)
229 Trace("sygus-sample") << r
<< " ";
231 Trace("sygus-sample") << std::endl
;
233 d_samples
.push_back(sample_pt
);
239 if (nduplicates
== nsamples
* 10)
241 Trace("sygus-sample")
242 << "...WARNING: excessive duplicates, cut off sampling at " << i
243 << "/" << nsamples
<< " points." << std::endl
;
252 bool SygusSampler::PtTrie::add(std::vector
<Node
>& pt
)
255 for (unsigned i
= 0, size
= pt
.size(); i
< size
; i
++)
257 curr
= &(curr
->d_children
[pt
[i
]]);
259 bool retVal
= curr
->d_children
.empty();
260 curr
= &(curr
->d_children
[Node::null()]);
264 Node
SygusSampler::registerTerm(Node n
, bool forceKeep
)
269 // if this is a sygus type, get its builtin analog
270 if (d_use_sygus_type
)
272 Assert(!d_ftn
.isNull());
273 bn
= d_tds
->sygusToBuiltin(n
);
274 Assert(d_builtin_to_sygus
.find(bn
) == d_builtin_to_sygus
.end()
275 || d_builtin_to_sygus
[bn
] == n
);
276 d_builtin_to_sygus
[bn
] = n
;
278 Assert(bn
.getType() == d_tn
);
279 Node res
= d_trie
.add(bn
, this, 0, d_samples
.size(), forceKeep
);
280 if (d_use_sygus_type
)
282 Assert(d_builtin_to_sygus
.find(res
) != d_builtin_to_sygus
.end());
283 res
= res
!= bn
? d_builtin_to_sygus
[res
] : n
;
290 bool SygusSampler::isContiguous(Node n
)
292 // compute free variables in n
293 std::vector
<Node
> fvs
;
294 computeFreeVariables(n
, fvs
);
295 // compute contiguous condition
296 for (const std::pair
<const unsigned, std::vector
<Node
> >& p
: d_type_vars
)
298 bool foundNotFv
= false;
299 for (const Node
& v
: p
.second
)
301 bool hasFv
= std::find(fvs
.begin(), fvs
.end(), v
) != fvs
.end();
315 void SygusSampler::computeFreeVariables(Node n
, std::vector
<Node
>& fvs
)
317 std::unordered_set
<TNode
, TNodeHashFunction
> visited
;
318 std::unordered_set
<TNode
, TNodeHashFunction
>::iterator it
;
319 std::vector
<TNode
> visit
;
326 if (visited
.find(cur
) == visited
.end())
331 if (d_var_index
.find(cur
) != d_var_index
.end())
336 for (const Node
& cn
: cur
)
341 } while (!visit
.empty());
344 bool SygusSampler::isOrdered(Node n
)
346 // compute free variables in n for each type
347 std::map
<unsigned, std::vector
<Node
> > fvs
;
349 std::unordered_set
<TNode
, TNodeHashFunction
> visited
;
350 std::unordered_set
<TNode
, TNodeHashFunction
>::iterator it
;
351 std::vector
<TNode
> visit
;
358 if (visited
.find(cur
) == visited
.end())
363 std::map
<Node
, unsigned>::iterator itv
= d_var_index
.find(cur
);
364 if (itv
!= d_var_index
.end())
366 unsigned tnid
= d_type_ids
[cur
];
367 // if this variable is out of order
368 if (itv
->second
!= fvs
[tnid
].size())
372 fvs
[tnid
].push_back(cur
);
375 for (unsigned j
= 0, nchildren
= cur
.getNumChildren(); j
< nchildren
; j
++)
377 visit
.push_back(cur
[(nchildren
- j
) - 1]);
380 } while (!visit
.empty());
384 bool SygusSampler::containsFreeVariables(Node a
, Node b
, bool strict
)
386 // compute free variables in a
387 std::vector
<Node
> fvs
;
388 computeFreeVariables(a
, fvs
);
389 std::vector
<Node
> fv_found
;
391 std::unordered_set
<TNode
, TNodeHashFunction
> visited
;
392 std::unordered_set
<TNode
, TNodeHashFunction
>::iterator it
;
393 std::vector
<TNode
> visit
;
400 if (visited
.find(cur
) == visited
.end())
405 if (std::find(fvs
.begin(), fvs
.end(), cur
) == fvs
.end())
411 if (fv_found
.size() + 1 == fvs
.size())
415 // cur should only be visited once
416 Assert(std::find(fv_found
.begin(), fv_found
.end(), cur
)
418 fv_found
.push_back(cur
);
421 for (const Node
& cn
: cur
)
426 } while (!visit
.empty());
430 void SygusSampler::getVariables(std::vector
<Node
>& vars
) const
432 vars
.insert(vars
.end(), d_vars
.begin(), d_vars
.end());
435 void SygusSampler::getSamplePoint(unsigned index
,
436 std::vector
<Node
>& vars
,
437 std::vector
<Node
>& pt
)
439 Assert(index
< d_samples
.size());
440 vars
.insert(vars
.end(), d_vars
.begin(), d_vars
.end());
441 std::vector
<Node
>& spt
= d_samples
[index
];
442 pt
.insert(pt
.end(), spt
.begin(), spt
.end());
445 void SygusSampler::addSamplePoint(std::vector
<Node
>& pt
)
447 Assert(pt
.size() == d_vars
.size());
448 d_samples
.push_back(pt
);
451 Node
SygusSampler::evaluate(Node n
, unsigned index
)
453 Assert(index
< d_samples
.size());
454 // do beta-reductions in n first
455 n
= Rewriter::rewrite(n
);
456 // use efficient rewrite for substitution + rewrite
457 Node ev
= d_eval
.eval(n
, d_vars
, d_samples
[index
]);
458 Trace("sygus-sample-ev") << "Evaluate ( " << n
<< ", " << index
<< " ) -> ";
461 Trace("sygus-sample-ev") << ev
<< std::endl
;
464 Trace("sygus-sample-ev") << "null" << std::endl
;
465 Trace("sygus-sample-ev") << "Rewrite -> ";
466 // substitution + rewrite
467 std::vector
<Node
>& pt
= d_samples
[index
];
468 ev
= n
.substitute(d_vars
.begin(), d_vars
.end(), pt
.begin(), pt
.end());
469 ev
= Rewriter::rewrite(ev
);
470 Trace("sygus-sample-ev") << ev
<< std::endl
;
474 int SygusSampler::getDiffSamplePointIndex(Node a
, Node b
)
476 for (unsigned i
= 0, nsamp
= d_samples
.size(); i
< nsamp
; i
++)
478 Node ae
= evaluate(a
, i
);
479 Node be
= evaluate(b
, i
);
488 Node
SygusSampler::getRandomValue(TypeNode tn
)
490 NodeManager
* nm
= NodeManager::currentNM();
493 return nm
->mkConst(Random::getRandom().pickWithProb(0.5));
495 else if (tn
.isBitVector())
497 unsigned sz
= tn
.getBitVectorSize();
498 return nm
->mkConst(Sampler::pickBvUniform(sz
));
500 else if (tn
.isFloatingPoint())
502 unsigned e
= tn
.getFloatingPointExponentSize();
503 unsigned s
= tn
.getFloatingPointSignificandSize();
504 return nm
->mkConst(options::sygusSampleFpUniform()
505 ? Sampler::pickFpUniform(e
, s
)
506 : Sampler::pickFpBiased(e
, s
));
508 else if (tn
.isString() || tn
.isInteger())
510 // if string, determine the alphabet
511 if (tn
.isString() && d_rstring_alphabet
.empty())
513 Trace("sygus-sample-str-alpha")
514 << "Setting string alphabet..." << std::endl
;
515 std::unordered_set
<unsigned> alphas
;
516 for (const std::pair
<const Node
, std::vector
<TypeNode
> >& c
:
519 if (c
.first
.getType().isString())
521 Trace("sygus-sample-str-alpha")
522 << "...have constant " << c
.first
<< std::endl
;
523 Assert(c
.first
.isConst());
524 std::vector
<unsigned> svec
= c
.first
.getConst
<String
>().getVec();
525 for (unsigned ch
: svec
)
531 // can limit to 1 extra characters beyond those in the grammar (2 if
532 // there are none in the grammar)
533 unsigned num_fresh_char
= alphas
.empty() ? 2 : 1;
534 unsigned fresh_char
= 0;
535 for (unsigned i
= 0; i
< num_fresh_char
; i
++)
537 while (alphas
.find(fresh_char
) != alphas
.end())
541 alphas
.insert(fresh_char
);
543 Trace("sygus-sample-str-alpha")
544 << "Sygus sampler: limit strings alphabet to : " << std::endl
546 for (unsigned ch
: alphas
)
548 d_rstring_alphabet
.push_back(ch
);
549 Trace("sygus-sample-str-alpha")
550 << " \"" << String::convertUnsignedIntToChar(ch
) << "\"";
552 Trace("sygus-sample-str-alpha") << std::endl
;
555 std::vector
<unsigned> vec
;
556 double ext_freq
= .5;
557 unsigned base
= tn
.isString() ? d_rstring_alphabet
.size() : 10;
558 while (Random::getRandom().pickWithProb(ext_freq
))
561 unsigned digit
= Random::getRandom().pick(0, base
- 1);
564 digit
= d_rstring_alphabet
[digit
];
566 vec
.push_back(digit
);
570 return nm
->mkConst(String(vec
));
572 else if (tn
.isInteger())
574 Rational
baser(base
);
576 std::vector
<Node
> sum
;
577 for (unsigned j
= 0, size
= vec
.size(); j
< size
; j
++)
579 Node digit
= nm
->mkConst(Rational(vec
[j
]) * curr
);
580 sum
.push_back(digit
);
586 ret
= nm
->mkConst(Rational(0));
588 else if (sum
.size() == 1)
594 ret
= nm
->mkNode(kind::PLUS
, sum
);
597 if (Random::getRandom().pickWithProb(0.5))
600 ret
= nm
->mkNode(kind::UMINUS
, ret
);
602 ret
= Rewriter::rewrite(ret
);
603 Assert(ret
.isConst());
607 else if (tn
.isReal())
609 Node s
= getRandomValue(nm
->integerType());
610 Node r
= getRandomValue(nm
->integerType());
611 if (!s
.isNull() && !r
.isNull())
613 Rational sr
= s
.getConst
<Rational
>();
614 Rational rr
= r
.getConst
<Rational
>();
621 return nm
->mkConst(sr
/ rr
);
625 // default: use type enumerator
626 unsigned counter
= 0;
627 while (Random::getRandom().pickWithProb(0.5))
631 Node ret
= d_tenum
.getEnumerateTerm(tn
, counter
);
634 // beyond bounds, return the first
635 ret
= d_tenum
.getEnumerateTerm(tn
, 0);
640 Node
SygusSampler::getSygusRandomValue(TypeNode tn
,
645 if (!tn
.isDatatype())
647 return getRandomValue(tn
);
649 const Datatype
& dt
= static_cast<DatatypeType
>(tn
.toType()).getDatatype();
652 return getRandomValue(tn
);
654 Assert(d_rvalue_cindices
.find(tn
) != d_rvalue_cindices
.end());
655 Trace("sygus-sample-grammar")
656 << "Sygus random value " << tn
<< ", depth = " << depth
657 << ", rchance = " << rchance
<< std::endl
;
658 // check if we terminate on this call
659 // we refuse to enumerate terms of 10+ depth as a hard limit
660 bool terminate
= Random::getRandom().pickWithProb(rchance
) || depth
>= 10;
661 // if we terminate, only nullary constructors can be chosen
662 std::vector
<unsigned>& cindices
=
663 terminate
? d_rvalue_null_cindices
[tn
] : d_rvalue_cindices
[tn
];
664 unsigned ncons
= cindices
.size();
665 // select a random constructor, or random value when index=ncons.
666 unsigned index
= Random::getRandom().pick(0, ncons
);
667 Trace("sygus-sample-grammar")
668 << "Random index 0..." << ncons
<< " was : " << index
<< std::endl
;
671 Trace("sygus-sample-grammar")
672 << "Recurse constructor index #" << index
<< std::endl
;
673 unsigned cindex
= cindices
[index
];
674 Assert(cindex
< dt
.getNumConstructors());
675 const DatatypeConstructor
& dtc
= dt
[cindex
];
676 // more likely to terminate in recursive calls
677 double rchance_new
= rchance
+ (1.0 - rchance
) * rinc
;
678 std::map
<int, Node
> pre
;
680 // generate random values for all arguments
681 for (unsigned i
= 0, nargs
= dtc
.getNumArgs(); i
< nargs
; i
++)
683 TypeNode tnc
= d_tds
->getArgType(dtc
, i
);
684 Node c
= getSygusRandomValue(tnc
, rchance_new
, rinc
, depth
+ 1);
688 Trace("sygus-sample-grammar") << "...fail." << std::endl
;
691 Trace("sygus-sample-grammar")
692 << " child #" << i
<< " : " << c
<< std::endl
;
697 Trace("sygus-sample-grammar") << "mkGeneric" << std::endl
;
698 Node ret
= d_tds
->mkGeneric(dt
, cindex
, pre
);
699 Trace("sygus-sample-grammar") << "...returned " << ret
<< std::endl
;
700 ret
= Rewriter::rewrite(ret
);
701 Trace("sygus-sample-grammar") << "...after rewrite " << ret
<< std::endl
;
702 Assert(ret
.isConst());
706 Trace("sygus-sample-grammar") << "...resort to random value" << std::endl
;
707 // if we did not generate based on the grammar, pick a random value
708 return getRandomValue(TypeNode::fromType(dt
.getSygusType()));
711 // recursion depth bounded by number of types in grammar (small)
712 void SygusSampler::registerSygusType(TypeNode tn
)
714 if (d_rvalue_cindices
.find(tn
) == d_rvalue_cindices
.end())
716 d_rvalue_cindices
[tn
].clear();
717 if (!tn
.isDatatype())
721 const Datatype
& dt
= static_cast<DatatypeType
>(tn
.toType()).getDatatype();
726 for (unsigned i
= 0, ncons
= dt
.getNumConstructors(); i
< ncons
; i
++)
728 const DatatypeConstructor
& dtc
= dt
[i
];
729 Node sop
= Node::fromExpr(dtc
.getSygusOp());
730 bool isVar
= std::find(d_vars
.begin(), d_vars
.end(), sop
) != d_vars
.end();
733 // if it is a variable, add it to the list of sygus types for that var
734 d_var_sygus_types
[sop
].push_back(tn
);
738 // otherwise, it is a constructor for sygus random value
739 d_rvalue_cindices
[tn
].push_back(i
);
740 if (dtc
.getNumArgs() == 0)
742 d_rvalue_null_cindices
[tn
].push_back(i
);
745 d_const_sygus_types
[sop
].push_back(tn
);
749 // recurse on all subfields
750 for (unsigned j
= 0, nargs
= dtc
.getNumArgs(); j
< nargs
; j
++)
752 TypeNode tnc
= d_tds
->getArgType(dtc
, j
);
753 registerSygusType(tnc
);
759 } /* CVC4::theory::quantifiers namespace */
760 } /* CVC4::theory namespace */
761 } /* CVC4 namespace */