1 /********************* */
2 /*! \file sygus_unif_io.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_unif_io
15 #include "theory/quantifiers/sygus/sygus_unif_io.h"
17 #include "options/quantifiers_options.h"
18 #include "theory/datatypes/datatypes_rewriter.h"
19 #include "theory/evaluator.h"
20 #include "theory/quantifiers/sygus/term_database_sygus.h"
21 #include "theory/quantifiers/term_util.h"
22 #include "util/random.h"
26 using namespace CVC4::kind
;
30 namespace quantifiers
{
32 UnifContextIo::UnifContextIo() : d_curr_role(role_invalid
)
34 d_true
= NodeManager::currentNM()->mkConst(true);
35 d_false
= NodeManager::currentNM()->mkConst(false);
38 NodeRole
UnifContextIo::getCurrentRole() { return d_curr_role
; }
40 bool UnifContextIo::updateContext(SygusUnifIo
* sui
,
41 std::vector
<Node
>& vals
,
44 Assert(d_vals
.size() == vals
.size());
46 Node poln
= pol
? d_true
: d_false
;
47 for (unsigned i
= 0; i
< vals
.size(); i
++)
51 if (d_vals
[i
] == d_true
)
65 bool UnifContextIo::updateStringPosition(SygusUnifIo
* sui
,
66 std::vector
<unsigned>& pos
,
69 Assert(pos
.size() == d_str_pos
.size());
71 for (unsigned i
= 0; i
< pos
.size(); i
++)
75 d_str_pos
[i
] += pos
[i
];
87 void UnifContextIo::initialize(SygusUnifIo
* sui
)
89 // clear previous data
92 d_curr_role
= role_equal
;
95 // initialize with #examples
96 unsigned sz
= sui
->d_examples
.size();
97 for (unsigned i
= 0; i
< sz
; i
++)
99 d_vals
.push_back(d_true
);
102 if (!sui
->d_examples_out
.empty())
104 // output type of the examples
105 TypeNode exotn
= sui
->d_examples_out
[0].getType();
107 if (exotn
.isString())
109 for (unsigned i
= 0; i
< sz
; i
++)
111 d_str_pos
.push_back(0);
115 d_visit_role
.clear();
118 void UnifContextIo::getCurrentStrings(SygusUnifIo
* sui
,
119 const std::vector
<Node
>& vals
,
120 std::vector
<String
>& ex_vals
)
122 bool isPrefix
= d_curr_role
== role_string_prefix
;
124 for (unsigned i
= 0; i
< vals
.size(); i
++)
126 if (d_vals
[i
] == sui
->d_true
)
128 Assert(vals
[i
].isConst());
129 unsigned pos_value
= d_str_pos
[i
];
132 Assert(d_curr_role
!= role_invalid
);
133 String s
= vals
[i
].getConst
<String
>();
134 Assert(pos_value
<= s
.size());
135 ex_vals
.push_back(isPrefix
? s
.suffix(s
.size() - pos_value
)
136 : s
.prefix(s
.size() - pos_value
));
140 ex_vals
.push_back(vals
[i
].getConst
<String
>());
145 // irrelevant, add dummy
146 ex_vals
.push_back(dummy
);
151 bool UnifContextIo::getStringIncrement(SygusUnifIo
* sui
,
153 const std::vector
<String
>& ex_vals
,
154 const std::vector
<Node
>& vals
,
155 std::vector
<unsigned>& inc
,
158 for (unsigned j
= 0; j
< vals
.size(); j
++)
161 if (d_vals
[j
] == sui
->d_true
)
163 // example is active in this context
164 Assert(vals
[j
].isConst());
165 String mystr
= vals
[j
].getConst
<String
>();
167 if (mystr
.size() <= ex_vals
[j
].size())
169 if (!(isPrefix
? ex_vals
[j
].strncmp(mystr
, ival
)
170 : ex_vals
[j
].rstrncmp(mystr
, ival
)))
172 Trace("sygus-sui-dt-debug") << "X";
178 Trace("sygus-sui-dt-debug") << "X";
181 Trace("sygus-sui-dt-debug") << ival
;
186 // inactive in this context
187 Trace("sygus-sui-dt-debug") << "-";
193 bool UnifContextIo::isStringSolved(SygusUnifIo
* sui
,
194 const std::vector
<String
>& ex_vals
,
195 const std::vector
<Node
>& vals
)
197 for (unsigned j
= 0; j
< vals
.size(); j
++)
199 if (d_vals
[j
] == sui
->d_true
)
201 // example is active in this context
202 Assert(vals
[j
].isConst());
203 String mystr
= vals
[j
].getConst
<String
>();
204 if (ex_vals
[j
] != mystr
)
213 // status : 0 : exact, -1 : vals is subset, 1 : vals is superset
214 Node
SubsumeTrie::addTermInternal(Node t
,
215 const std::vector
<Node
>& vals
,
217 std::vector
<Node
>& subsumed
,
221 bool checkExistsOnly
,
224 if (index
== vals
.size())
228 // set the term if checkExistsOnly = false
229 if (d_term
.isNull() && !checkExistsOnly
)
234 else if (status
== 1)
236 Assert(checkSubsume
);
237 // found a subsumed term
238 if (!d_term
.isNull())
240 subsumed
.push_back(d_term
);
241 // If we are only interested in feasibility, we could set d_term to null
242 // here. However, d_term still could be useful, since it may be
243 // smaller than t and suffice as a solution under some condition.
244 // As a simple example, consider predicate synthesis and a case where we
245 // enumerate a C that is correct for all I/O points whose output is
246 // true. Then, C subsumes true. However, true may be preferred, e.g.
247 // to generate a solution ite( C, true, D ) instead of ite( C, C, D ),
248 // since true is conditionally correct under C, and is smaller than C.
253 Assert(!checkExistsOnly
&& checkSubsume
);
257 NodeManager
* nm
= NodeManager::currentNM();
259 Assert(pol
|| (vals
[index
].isConst() && vals
[index
].getType().isBoolean()));
260 Node cv
= pol
? vals
[index
] : nm
->mkConst(!vals
[index
].getConst
<bool>());
261 // if checkExistsOnly = false, check if the current value is subsumed if
262 // checkSubsume = true, if so, don't add
263 if (!checkExistsOnly
&& checkSubsume
)
265 Assert(cv
.isConst() && cv
.getType().isBoolean());
266 std::vector
<bool> check_subsumed_by
;
269 if (!cv
.getConst
<bool>())
271 check_subsumed_by
.push_back(spol
);
274 else if (status
== -1)
276 check_subsumed_by
.push_back(spol
);
277 if (!cv
.getConst
<bool>())
279 check_subsumed_by
.push_back(!spol
);
282 // check for subsumed nodes
283 for (unsigned i
= 0, size
= check_subsumed_by
.size(); i
< size
; i
++)
285 bool csbi
= check_subsumed_by
[i
];
286 Node csval
= nm
->mkConst(csbi
);
288 std::map
<Node
, SubsumeTrie
>::iterator itc
= d_children
.find(csval
);
289 if (itc
!= d_children
.end())
291 Node ret
= itc
->second
.addTermInternal(t
,
309 std::vector
<bool> check_subsume
;
314 std::map
<Node
, SubsumeTrie
>::iterator itc
= d_children
.find(cv
);
315 if (itc
!= d_children
.end())
317 ret
= itc
->second
.addTermInternal(t
,
331 ret
= d_children
[cv
].addTermInternal(t
,
342 // we were subsumed by ret, return
348 Assert(cv
.isConst() && cv
.getType().isBoolean());
349 // check for subsuming
350 if (cv
.getConst
<bool>())
352 check_subsume
.push_back(!spol
);
356 else if (status
== 1)
358 Assert(checkSubsume
);
359 Assert(cv
.isConst() && cv
.getType().isBoolean());
360 check_subsume
.push_back(!spol
);
361 if (cv
.getConst
<bool>())
363 check_subsume
.push_back(spol
);
368 // check for subsumed terms
369 for (unsigned i
= 0, size
= check_subsume
.size(); i
< size
; i
++)
371 Node csval
= nm
->mkConst
<bool>(check_subsume
[i
]);
372 std::map
<Node
, SubsumeTrie
>::iterator itc
= d_children
.find(csval
);
373 if (itc
!= d_children
.end())
375 itc
->second
.addTermInternal(t
,
385 if (itc
->second
.isEmpty())
387 Assert(!checkExistsOnly
);
388 d_children
.erase(csval
);
396 Node
SubsumeTrie::addTerm(Node t
,
397 const std::vector
<Node
>& vals
,
399 std::vector
<Node
>& subsumed
)
401 return addTermInternal(t
, vals
, pol
, subsumed
, true, 0, 0, false, true);
404 Node
SubsumeTrie::addCond(Node c
, const std::vector
<Node
>& vals
, bool pol
)
406 std::vector
<Node
> subsumed
;
407 return addTermInternal(c
, vals
, pol
, subsumed
, true, 0, 0, false, false);
410 void SubsumeTrie::getSubsumed(const std::vector
<Node
>& vals
,
412 std::vector
<Node
>& subsumed
)
414 addTermInternal(Node::null(), vals
, pol
, subsumed
, true, 0, 1, true, true);
417 void SubsumeTrie::getSubsumedBy(const std::vector
<Node
>& vals
,
419 std::vector
<Node
>& subsumed_by
)
423 Node::null(), vals
, !pol
, subsumed_by
, false, 0, 1, true, true);
426 void SubsumeTrie::getLeavesInternal(const std::vector
<Node
>& vals
,
428 std::map
<int, std::vector
<Node
> >& v
,
432 if (index
== vals
.size())
434 // by convention, if we did not test any points, then we consider the
435 // evaluation along the current path to be always false.
436 int rstatus
= status
== -2 ? -1 : status
;
437 Assert(!d_term
.isNull());
438 Assert(std::find(v
[rstatus
].begin(), v
[rstatus
].end(), d_term
)
439 == v
[rstatus
].end());
440 v
[rstatus
].push_back(d_term
);
444 Assert(vals
[index
].isConst() && vals
[index
].getType().isBoolean());
445 bool curr_val_true
= vals
[index
].getConst
<bool>() == pol
;
446 for (std::map
<Node
, SubsumeTrie
>::iterator it
= d_children
.begin();
447 it
!= d_children
.end();
450 int new_status
= status
;
451 // if the current value is true
456 Assert(it
->first
.isConst() && it
->first
.getType().isBoolean());
457 new_status
= (it
->first
.getConst
<bool>() ? 1 : -1);
458 if (status
!= -2 && new_status
!= status
)
464 it
->second
.getLeavesInternal(vals
, pol
, v
, index
+ 1, new_status
);
469 void SubsumeTrie::getLeaves(const std::vector
<Node
>& vals
,
471 std::map
<int, std::vector
<Node
> >& v
)
473 getLeavesInternal(vals
, pol
, v
, 0, -2);
476 SygusUnifIo::SygusUnifIo()
477 : d_check_sol(false),
480 d_sol_cons_nondet(false),
481 d_solConsUsingInfoGain(false)
483 d_true
= NodeManager::currentNM()->mkConst(true);
484 d_false
= NodeManager::currentNM()->mkConst(false);
487 SygusUnifIo::~SygusUnifIo() {}
488 void SygusUnifIo::initializeCandidate(
489 QuantifiersEngine
* qe
,
491 std::vector
<Node
>& enums
,
492 std::map
<Node
, std::vector
<Node
>>& strategy_lemmas
)
495 d_examples_out
.clear();
498 SygusUnif::initializeCandidate(qe
, f
, enums
, strategy_lemmas
);
499 // learn redundant operators based on the strategy
500 d_strategy
[f
].staticLearnRedundantOps(strategy_lemmas
);
503 void SygusUnifIo::addExample(const std::vector
<Node
>& input
, Node output
)
505 d_examples
.push_back(input
);
506 d_examples_out
.push_back(output
);
509 void SygusUnifIo::computeExamples(Node e
, Node bv
, std::vector
<Node
>& exOut
)
511 std::map
<Node
, std::vector
<Node
>>& eoc
= d_exOutCache
[e
];
512 std::map
<Node
, std::vector
<Node
>>::iterator it
= eoc
.find(bv
);
515 exOut
.insert(exOut
.end(), it
->second
.begin(), it
->second
.end());
518 TypeNode xtn
= e
.getType();
519 std::vector
<Node
>& eocv
= eoc
[bv
];
520 for (size_t j
= 0, size
= d_examples
.size(); j
< size
; j
++)
522 Node res
= d_tds
->evaluateBuiltin(xtn
, bv
, d_examples
[j
]);
523 exOut
.push_back(res
);
528 void SygusUnifIo::clearExampleCache(Node e
, Node bv
)
530 std::map
<Node
, std::vector
<Node
>>& eoc
= d_exOutCache
[e
];
531 Assert(eoc
.find(bv
) != eoc
.end());
535 void SygusUnifIo::notifyEnumeration(Node e
, Node v
, std::vector
<Node
>& lemmas
)
537 Trace("sygus-sui-enum") << "Notify enumeration for " << e
<< " : " << v
539 Node c
= d_candidate
;
540 Assert(!d_examples
.empty());
541 Assert(d_examples
.size() == d_examples_out
.size());
543 EnumInfo
& ei
= d_strategy
[c
].getEnumInfo(e
);
544 // The explanation for why the current value should be excluded in future
548 std::vector
<Node
> base_results
;
549 TypeNode xtn
= e
.getType();
550 Node bv
= d_tds
->sygusToBuiltin(v
, xtn
);
551 bv
= d_tds
->getExtRewriter()->extendedRewrite(bv
);
552 Trace("sygus-sui-enum") << "PBE Compute Examples for " << bv
<< std::endl
;
553 // compte the results (should be cached)
554 computeExamples(e
, bv
, base_results
);
555 // don't need it after this
556 clearExampleCache(e
, bv
);
557 // get the results for each slave enumerator
558 std::map
<Node
, std::vector
<Node
>> srmap
;
559 Evaluator
* ev
= d_tds
->getEvaluator();
560 bool tryEval
= options::sygusEvalOpt();
561 for (const Node
& xs
: ei
.d_enum_slave
)
563 Assert(srmap
.find(xs
) == srmap
.end());
564 EnumInfo
& eiv
= d_strategy
[c
].getEnumInfo(xs
);
565 Node templ
= eiv
.d_template
;
568 TNode templ_var
= eiv
.d_template_arg
;
569 std::vector
<Node
> args
;
570 args
.push_back(templ_var
);
571 std::vector
<Node
> sresults
;
572 for (const Node
& res
: base_results
)
575 std::vector
<Node
> vals
;
576 vals
.push_back(tres
);
580 sres
= ev
->eval(templ
, args
, vals
);
584 // fall back on rewriter
585 sres
= templ
.substitute(templ_var
, tres
);
586 sres
= Rewriter::rewrite(sres
);
588 sresults
.push_back(sres
);
590 srmap
[xs
] = sresults
;
594 srmap
[xs
] = base_results
;
598 // is it excluded for domain-specific reason?
599 std::vector
<Node
> exp_exc_vec
;
600 Assert(d_tds
->isEnumerator(e
));
601 bool isPassive
= d_tds
->isPassiveEnumerator(e
);
602 if (getExplanationForEnumeratorExclude(e
, v
, base_results
, exp_exc_vec
))
606 Assert(!exp_exc_vec
.empty());
607 exp_exc
= exp_exc_vec
.size() == 1
609 : NodeManager::currentNM()->mkNode(AND
, exp_exc_vec
);
611 Trace("sygus-sui-enum")
612 << " ...fail : term is excluded (domain-specific)" << std::endl
;
617 Assert(!ei
.d_enum_slave
.empty());
618 // explanation for why this value should be excluded
619 for (unsigned s
= 0; s
< ei
.d_enum_slave
.size(); s
++)
621 Node xs
= ei
.d_enum_slave
[s
];
622 EnumInfo
& eiv
= d_strategy
[c
].getEnumInfo(xs
);
623 EnumCache
& ecv
= d_ecache
[xs
];
624 Trace("sygus-sui-enum") << "Process " << xs
<< " from " << s
<< std::endl
;
625 // bool prevIsCover = false;
626 if (eiv
.getRole() == enum_io
)
628 Trace("sygus-sui-enum") << " IO-Eval of ";
629 // prevIsCover = eiv.isFeasible();
633 Trace("sygus-sui-enum") << "Evaluation of ";
635 Trace("sygus-sui-enum") << xs
<< " : ";
636 // evaluate all input/output examples
637 std::vector
<Node
> results
;
638 std::map
<Node
, bool> cond_vals
;
639 std::map
<Node
, std::vector
<Node
>>::iterator itsr
= srmap
.find(xs
);
640 Assert(itsr
!= srmap
.end());
641 for (unsigned j
= 0, size
= itsr
->second
.size(); j
< size
; j
++)
643 Node res
= itsr
->second
[j
];
644 // The value of this term for this example, or the truth value of
645 // the I/O pair if the role of this enumerator is enum_io.
647 // If the result is not constant, then we cannot determine its value
648 // on this point. In this case, resb remains null.
651 if (eiv
.getRole() == enum_io
)
653 Node out
= d_examples_out
[j
];
654 Assert(out
.isConst());
655 resb
= res
== out
? d_true
: d_false
;
662 cond_vals
[resb
] = true;
663 results
.push_back(resb
);
664 if (Trace
.isOn("sygus-sui-enum"))
668 Trace("sygus-sui-enum") << "_";
670 else if (resb
.getType().isBoolean())
672 Trace("sygus-sui-enum") << (resb
== d_true
? "1" : "0");
676 Trace("sygus-sui-enum") << "?";
681 if (eiv
.getRole() == enum_io
)
683 // latter is the degenerate case of no examples
684 if (cond_vals
.find(d_true
) != cond_vals
.end() || cond_vals
.empty())
686 // check subsumbed/subsuming
687 std::vector
<Node
> subsume
;
688 if (cond_vals
.find(d_false
) == cond_vals
.end())
690 // it is the entire solution, we are done
691 Trace("sygus-sui-enum")
692 << " ...success, full solution added to PBE pool : "
693 << d_tds
->sygusToBuiltin(v
) << std::endl
;
697 // it subsumes everything
698 ecv
.d_term_trie
.clear();
699 ecv
.d_term_trie
.addTerm(v
, results
, true, subsume
);
705 Node val
= ecv
.d_term_trie
.addTerm(v
, results
, true, subsume
);
708 Trace("sygus-sui-enum") << " ...success";
709 if (!subsume
.empty())
711 ecv
.d_enum_subsume
.insert(
712 ecv
.d_enum_subsume
.end(), subsume
.begin(), subsume
.end());
713 Trace("sygus-sui-enum")
714 << " and subsumed " << subsume
.size() << " terms";
716 Trace("sygus-sui-enum")
717 << "! add to PBE pool : " << d_tds
->sygusToBuiltin(v
)
723 Assert(subsume
.empty());
724 Trace("sygus-sui-enum") << " ...fail : subsumed" << std::endl
;
730 Trace("sygus-sui-enum")
731 << " ...fail : it does not satisfy examples." << std::endl
;
736 // must be unique up to examples
737 Node val
= ecv
.d_term_trie
.addCond(v
, results
, true);
740 Trace("sygus-sui-enum") << " ...success! add to PBE pool : "
741 << d_tds
->sygusToBuiltin(v
) << std::endl
;
746 Trace("sygus-sui-enum")
747 << " ...fail : term is not unique" << std::endl
;
752 // notify to retry the build of solution
755 ecv
.addEnumValue(v
, results
);
762 // exclude this value on subsequent iterations
763 if (exp_exc
.isNull())
765 Trace("sygus-sui-enum-lemma") << "Use basic exclusion." << std::endl
;
766 // if we did not already explain why this should be excluded, use default
767 exp_exc
= d_tds
->getExplain()->getExplanationForEquality(e
, v
);
769 exp_exc
= exp_exc
.negate();
770 Trace("sygus-sui-enum-lemma")
771 << "SygusUnifIo : enumeration exclude lemma : " << exp_exc
<< std::endl
;
772 lemmas
.push_back(exp_exc
);
776 bool SygusUnifIo::constructSolution(std::vector
<Node
>& sols
,
777 std::vector
<Node
>& lemmas
)
779 Node sol
= constructSolutionNode(lemmas
);
788 Node
SygusUnifIo::constructSolutionNode(std::vector
<Node
>& lemmas
)
790 Node c
= d_candidate
;
791 if (!d_solution
.isNull() && !options::sygusStream())
793 // already has a solution
796 // only check if an enumerator updated
799 Trace("sygus-pbe") << "Construct solution, #iterations = " << d_cond_count
803 d_solConsUsingInfoGain
= false;
804 // try multiple times if we have done multiple conditions, due to
806 for (unsigned i
= 0; i
<= d_cond_count
; i
++)
808 Trace("sygus-pbe-dt") << "ConstructPBE for candidate: " << c
<< std::endl
;
809 // initialize a call to construct solution
810 initializeConstructSol();
811 initializeConstructSolFor(c
);
812 // call the virtual construct solution method
813 Node e
= d_strategy
[c
].getRootEnumerator();
814 Node vcc
= constructSol(c
, e
, role_equal
, 1, lemmas
);
815 // if we constructed the solution, and we either did not previously have
816 // a solution, or the new solution is better (smaller).
818 && (d_solution
.isNull()
819 || (!d_solution
.isNull()
820 && d_tds
->getSygusTermSize(vcc
) < d_sol_term_size
)))
822 if (Trace
.isOn("sygus-pbe"))
824 Trace("sygus-pbe") << "**** SygusUnif SOLVED : " << c
<< " = ";
825 TermDbSygus::toStreamSygus("sygus-pbe", vcc
);
826 Trace("sygus-pbe") << std::endl
;
827 Trace("sygus-pbe") << "...solved at iteration " << i
<< std::endl
;
831 d_sol_term_size
= d_tds
->getSygusTermSize(vcc
);
832 Trace("sygus-pbe-sol")
833 << "PBE solution size: " << d_sol_term_size
<< std::endl
;
834 // We've determined its feasible, now, enable information gain and
835 // retry. We do this since information gain comes with an overhead,
836 // and we want testing feasibility to be fast.
837 if (!d_solConsUsingInfoGain
)
839 // we permanently enable information gain and minimality now
840 d_solConsUsingInfoGain
= true;
841 d_enableMinimality
= true;
845 else if (!d_sol_cons_nondet
)
850 if (!newSolution
.isNull())
854 Trace("sygus-pbe") << "...failed to solve." << std::endl
;
859 // ------------------------------------ solution construction from enumeration
861 bool SygusUnifIo::useStrContainsEnumeratorExclude(Node e
)
863 TypeNode xbt
= d_tds
->sygusToBuiltinType(e
.getType());
866 std::map
<Node
, bool>::iterator itx
= d_use_str_contains_eexc
.find(e
);
867 if (itx
!= d_use_str_contains_eexc
.end())
871 Trace("sygus-sui-enum-debug")
872 << "Is " << e
<< " is str.contains exclusion?" << std::endl
;
873 d_use_str_contains_eexc
[e
] = true;
874 Node c
= d_candidate
;
875 EnumInfo
& ei
= d_strategy
[c
].getEnumInfo(e
);
876 for (const Node
& sn
: ei
.d_enum_slave
)
878 EnumInfo
& eis
= d_strategy
[c
].getEnumInfo(sn
);
879 EnumRole er
= eis
.getRole();
880 if (er
!= enum_io
&& er
!= enum_concat_term
)
882 Trace("sygus-sui-enum-debug") << " incompatible slave : " << sn
883 << ", role = " << er
<< std::endl
;
884 d_use_str_contains_eexc
[e
] = false;
887 d_use_str_contains_eexc_conditional
[e
] = false;
888 if (eis
.isConditional())
890 Trace("sygus-sui-enum-debug")
891 << " conditional slave : " << sn
<< std::endl
;
892 d_use_str_contains_eexc_conditional
[e
] = true;
895 Trace("sygus-sui-enum-debug")
896 << "...can use str.contains exclusion." << std::endl
;
897 return d_use_str_contains_eexc
[e
];
902 bool SygusUnifIo::getExplanationForEnumeratorExclude(
905 std::vector
<Node
>& results
,
906 std::vector
<Node
>& exp
)
908 NodeManager
* nm
= NodeManager::currentNM();
909 if (useStrContainsEnumeratorExclude(e
))
911 // This check whether the example evaluates to something that is larger than
912 // the output for some input/output pair. If so, then this term is never
913 // useful. We generalize its explanation below.
915 // if the enumerator is in a conditional context, then we are stricter
916 // about when to exclude
917 bool isConditional
= d_use_str_contains_eexc_conditional
[e
];
918 if (Trace
.isOn("sygus-sui-cterm-debug"))
920 Trace("sygus-sui-enum") << std::endl
;
922 // check if all examples had longer length that the output
923 Assert(d_examples_out
.size() == results
.size());
924 Trace("sygus-sui-cterm-debug")
925 << "Check enumerator exclusion for " << e
<< " -> "
926 << d_tds
->sygusToBuiltin(v
) << " based on str.contains." << std::endl
;
927 std::vector
<unsigned> cmp_indices
;
928 for (unsigned i
= 0, size
= results
.size(); i
< size
; i
++)
930 Assert(results
[i
].isConst());
931 Assert(d_examples_out
[i
].isConst());
932 Trace("sygus-sui-cterm-debug")
933 << " " << results
[i
] << " <> " << d_examples_out
[i
];
934 Node cont
= nm
->mkNode(STRING_STRCTN
, d_examples_out
[i
], results
[i
]);
935 Node contr
= Rewriter::rewrite(cont
);
936 if (contr
== d_false
)
938 cmp_indices
.push_back(i
);
939 Trace("sygus-sui-cterm-debug") << "...not contained." << std::endl
;
943 Trace("sygus-sui-cterm-debug") << "...contained." << std::endl
;
950 if (!cmp_indices
.empty())
952 // we check invariance with respect to a negative contains test
953 NegContainsSygusInvarianceTest ncset
;
956 ncset
.setUniversal();
958 ncset
.init(e
, d_examples
, d_examples_out
, cmp_indices
);
959 // construct the generalized explanation
960 d_tds
->getExplain()->getExplanationFor(e
, v
, exp
, ncset
);
961 Trace("sygus-sui-cterm")
962 << "PBE-cterm : enumerator exclude " << d_tds
->sygusToBuiltin(v
)
963 << " due to negative containment." << std::endl
;
970 void SygusUnifIo::EnumCache::addEnumValue(Node v
, std::vector
<Node
>& results
)
972 // should not have been enumerated before
973 Assert(d_enum_val_to_index
.find(v
) == d_enum_val_to_index
.end());
974 d_enum_val_to_index
[v
] = d_enum_vals
.size();
975 d_enum_vals
.push_back(v
);
976 d_enum_vals_res
.push_back(results
);
979 void SygusUnifIo::initializeConstructSol()
981 d_context
.initialize(this);
982 d_sol_cons_nondet
= false;
985 void SygusUnifIo::initializeConstructSolFor(Node f
)
987 Assert(d_candidate
== f
);
990 Node
SygusUnifIo::constructSol(
991 Node f
, Node e
, NodeRole nrole
, int ind
, std::vector
<Node
>& lemmas
)
993 Assert(d_candidate
== f
);
994 UnifContextIo
& x
= d_context
;
995 TypeNode etn
= e
.getType();
996 if (Trace
.isOn("sygus-sui-dt-debug"))
998 indent("sygus-sui-dt-debug", ind
);
999 Trace("sygus-sui-dt-debug") << "ConstructPBE: (" << e
<< ", " << nrole
1000 << ") for type " << etn
<< " in context ";
1001 print_val("sygus-sui-dt-debug", x
.d_vals
);
1002 NodeRole ctx_role
= x
.getCurrentRole();
1003 Trace("sygus-sui-dt-debug") << ", context role [" << ctx_role
;
1004 if (ctx_role
== role_string_prefix
|| ctx_role
== role_string_suffix
)
1006 Trace("sygus-sui-dt-debug") << ", string pos : ";
1007 for (unsigned i
= 0, size
= x
.d_str_pos
.size(); i
< size
; i
++)
1009 Trace("sygus-sui-dt-debug") << " " << x
.d_str_pos
[i
];
1012 Trace("sygus-sui-dt-debug") << "]";
1013 Trace("sygus-sui-dt-debug") << std::endl
;
1015 // enumerator type info
1016 EnumTypeInfo
& tinfo
= d_strategy
[f
].getEnumTypeInfo(etn
);
1018 // get the enumerator information
1019 EnumInfo
& einfo
= d_strategy
[f
].getEnumInfo(e
);
1021 EnumCache
& ecache
= d_ecache
[e
];
1023 bool retValMod
= x
.isReturnValueModified();
1027 if (nrole
== role_equal
)
1031 if (ecache
.isSolved())
1033 // this type has a complete solution
1034 ret_dt
= ecache
.getSolved();
1035 indent("sygus-sui-dt", ind
);
1036 Trace("sygus-sui-dt") << "return PBE: success : solved "
1037 << d_tds
->sygusToBuiltin(ret_dt
) << std::endl
;
1038 Assert(!ret_dt
.isNull());
1042 // could be conditionally solved
1043 std::vector
<Node
> subsumed_by
;
1044 ecache
.d_term_trie
.getSubsumedBy(x
.d_vals
, true, subsumed_by
);
1045 if (!subsumed_by
.empty())
1047 ret_dt
= constructBestSolvedTerm(e
, subsumed_by
);
1048 indent("sygus-sui-dt", ind
);
1049 Trace("sygus-sui-dt") << "return PBE: success : conditionally solved"
1050 << d_tds
->sygusToBuiltin(ret_dt
) << std::endl
;
1054 indent("sygus-sui-dt-debug", ind
);
1055 Trace("sygus-sui-dt-debug")
1056 << " ...not currently conditionally solved." << std::endl
;
1060 if (ret_dt
.isNull())
1062 if (d_tds
->sygusToBuiltinType(e
.getType()).isString())
1064 // check if a current value that closes all examples
1065 // get the term enumerator for this type
1066 std::map
<EnumRole
, Node
>::iterator itnt
=
1067 tinfo
.d_enum
.find(enum_concat_term
);
1068 if (itnt
!= tinfo
.d_enum
.end())
1070 Node et
= itnt
->second
;
1072 EnumCache
& ecachet
= d_ecache
[et
];
1073 // get the current examples
1074 std::vector
<String
> ex_vals
;
1075 x
.getCurrentStrings(this, d_examples_out
, ex_vals
);
1076 Assert(ecache
.d_enum_vals
.size() == ecache
.d_enum_vals_res
.size());
1078 // test each example in the term enumerator for the type
1079 std::vector
<Node
> str_solved
;
1080 for (unsigned i
= 0, size
= ecachet
.d_enum_vals
.size(); i
< size
; i
++)
1082 if (x
.isStringSolved(this, ex_vals
, ecachet
.d_enum_vals_res
[i
]))
1084 str_solved
.push_back(ecachet
.d_enum_vals
[i
]);
1087 if (!str_solved
.empty())
1089 ret_dt
= constructBestSolvedTerm(e
, str_solved
);
1090 indent("sygus-sui-dt", ind
);
1091 Trace("sygus-sui-dt") << "return PBE: success : string solved "
1092 << d_tds
->sygusToBuiltin(ret_dt
) << std::endl
;
1096 indent("sygus-sui-dt-debug", ind
);
1097 Trace("sygus-sui-dt-debug")
1098 << " ...not currently string solved." << std::endl
;
1103 // maybe we can find one in the cache
1104 if (ret_dt
.isNull() && !retValMod
)
1106 bool firstTime
= true;
1107 std::unordered_set
<Node
, NodeHashFunction
> intersection
;
1108 std::map
<TypeNode
, std::unordered_set
<Node
, NodeHashFunction
>>::iterator
1110 for (size_t i
= 0, nvals
= x
.d_vals
.size(); i
< nvals
; i
++)
1112 if (x
.d_vals
[i
].getConst
<bool>())
1114 pit
= d_psolutions
[i
].find(etn
);
1115 if (pit
== d_psolutions
[i
].end())
1117 // no cached solution
1118 intersection
.clear();
1123 intersection
= pit
->second
;
1128 std::vector
<Node
> rm
;
1129 for (const Node
& a
: intersection
)
1131 if (pit
->second
.find(a
) == pit
->second
.end())
1136 for (const Node
& a
: rm
)
1138 intersection
.erase(a
);
1140 if (intersection
.empty())
1147 if (!intersection
.empty())
1149 if (d_enableMinimality
)
1151 // if we are enabling minimality, the minimal cached solution may
1152 // still not be the best solution, thus we remember it and keep it if
1153 // we don't construct a better one below
1154 std::vector
<Node
> intervec
;
1156 intervec
.begin(), intersection
.begin(), intersection
.end());
1157 cached_ret_dt
= getMinimalTerm(intervec
);
1161 ret_dt
= *intersection
.begin();
1163 if (Trace
.isOn("sygus-sui-dt"))
1165 indent("sygus-sui-dt", ind
);
1166 Trace("sygus-sui-dt") << "ConstructPBE: found in cache: ";
1168 if (d_enableMinimality
)
1170 csol
= cached_ret_dt
;
1171 Trace("sygus-sui-dt") << "(minimal) ";
1173 TermDbSygus::toStreamSygus("sygus-sui-dt", csol
);
1174 Trace("sygus-sui-dt") << std::endl
;
1179 else if (nrole
== role_string_prefix
|| nrole
== role_string_suffix
)
1181 // check if each return value is a prefix/suffix of all open examples
1182 if (!retValMod
|| x
.getCurrentRole() == nrole
)
1184 std::map
<Node
, std::vector
<unsigned> > incr
;
1185 bool isPrefix
= nrole
== role_string_prefix
;
1186 std::map
<Node
, unsigned> total_inc
;
1187 std::vector
<Node
> inc_strs
;
1188 // make the value of the examples
1189 std::vector
<String
> ex_vals
;
1190 x
.getCurrentStrings(this, d_examples_out
, ex_vals
);
1191 if (Trace
.isOn("sygus-sui-dt-debug"))
1193 indent("sygus-sui-dt-debug", ind
);
1194 Trace("sygus-sui-dt-debug") << "current strings : " << std::endl
;
1195 for (unsigned i
= 0, size
= ex_vals
.size(); i
< size
; i
++)
1197 indent("sygus-sui-dt-debug", ind
+ 1);
1198 Trace("sygus-sui-dt-debug") << ex_vals
[i
] << std::endl
;
1202 // check if there is a value for which is a prefix/suffix of all active
1204 Assert(ecache
.d_enum_vals
.size() == ecache
.d_enum_vals_res
.size());
1206 for (unsigned i
= 0, size
= ecache
.d_enum_vals
.size(); i
< size
; i
++)
1208 Node val_t
= ecache
.d_enum_vals
[i
];
1209 Assert(incr
.find(val_t
) == incr
.end());
1210 indent("sygus-sui-dt-debug", ind
);
1211 Trace("sygus-sui-dt-debug") << "increment string values : ";
1212 TermDbSygus::toStreamSygus("sygus-sui-dt-debug", val_t
);
1213 Trace("sygus-sui-dt-debug") << " : ";
1214 Assert(ecache
.d_enum_vals_res
[i
].size() == d_examples_out
.size());
1216 bool exsuccess
= x
.getStringIncrement(this,
1219 ecache
.d_enum_vals_res
[i
],
1225 Trace("sygus-sui-dt-debug") << "...fail" << std::endl
;
1229 total_inc
[val_t
] = tot
;
1230 inc_strs
.push_back(val_t
);
1231 Trace("sygus-sui-dt-debug")
1232 << "...success, total increment = " << tot
<< std::endl
;
1238 // solution construction for strings concatenation is non-deterministic
1239 // with respect to failure/success.
1240 d_sol_cons_nondet
= true;
1241 ret_dt
= constructBestStringToConcat(inc_strs
, total_inc
, incr
);
1242 Assert(!ret_dt
.isNull());
1243 indent("sygus-sui-dt", ind
);
1244 Trace("sygus-sui-dt")
1245 << "PBE: CONCAT strategy : choose " << (isPrefix
? "pre" : "suf")
1246 << "fix value " << d_tds
->sygusToBuiltin(ret_dt
) << std::endl
;
1247 // update the context
1248 bool ret
= x
.updateStringPosition(this, incr
[ret_dt
], nrole
);
1249 AlwaysAssert(ret
== (total_inc
[ret_dt
] > 0));
1253 indent("sygus-sui-dt", ind
);
1254 Trace("sygus-sui-dt") << "PBE: failed CONCAT strategy, no values are "
1255 << (isPrefix
? "pre" : "suf")
1256 << "fix of all examples." << std::endl
;
1261 indent("sygus-sui-dt", ind
);
1262 Trace("sygus-sui-dt")
1263 << "PBE: failed CONCAT strategy, prefix/suffix mismatch."
1267 if (!ret_dt
.isNull() || einfo
.isTemplated())
1269 Assert(ret_dt
.isNull() || ret_dt
.getType() == e
.getType());
1270 indent("sygus-sui-dt", ind
);
1271 Trace("sygus-sui-dt") << "ConstructPBE: returned (pre-strategy) " << ret_dt
1275 // we will try a single strategy
1276 EnumTypeInfoStrat
* etis
= nullptr;
1277 std::map
<NodeRole
, StrategyNode
>::iterator itsn
= tinfo
.d_snodes
.find(nrole
);
1278 if (itsn
== tinfo
.d_snodes
.end())
1280 indent("sygus-sui-dt", ind
);
1281 Trace("sygus-sui-dt") << "ConstructPBE: returned (no-strategy) " << ret_dt
1286 StrategyNode
& snode
= itsn
->second
;
1287 if (x
.d_visit_role
[e
].find(nrole
) != x
.d_visit_role
[e
].end())
1289 // already visited and context not changed (notice d_visit_role is cleared
1290 // when the context changes).
1291 indent("sygus-sui-dt", ind
);
1292 Trace("sygus-sui-dt") << "ConstructPBE: returned (already visited) "
1293 << ret_dt
<< std::endl
;
1296 x
.d_visit_role
[e
][nrole
] = true;
1297 // try a random strategy
1298 if (snode
.d_strats
.size() > 1)
1301 snode
.d_strats
.begin(), snode
.d_strats
.end(), Random::getRandom());
1303 // ITE always first if we have not yet solved
1304 // the reasoning is that splitting on conditions only subdivides the problem
1305 // and cannot be the source of failure, whereas the wrong choice for a
1306 // concatenation term may lead to failure
1307 if (d_solution
.isNull())
1309 for (unsigned i
= 0; i
< snode
.d_strats
.size(); i
++)
1311 if (snode
.d_strats
[i
]->d_this
== strat_ITE
)
1314 EnumTypeInfoStrat
* etis
= snode
.d_strats
[i
];
1315 snode
.d_strats
[i
] = snode
.d_strats
[0];
1316 snode
.d_strats
[0] = etis
;
1322 // iterate over the strategies
1323 unsigned sindex
= 0;
1324 bool did_recurse
= false;
1325 while (ret_dt
.isNull() && !did_recurse
&& sindex
< snode
.d_strats
.size())
1327 if (snode
.d_strats
[sindex
]->isValid(x
))
1329 etis
= snode
.d_strats
[sindex
];
1330 Assert(etis
!= nullptr);
1331 StrategyType strat
= etis
->d_this
;
1332 indent("sygus-sui-dt", ind
+ 1);
1333 Trace("sygus-sui-dt")
1334 << "...try STRATEGY " << strat
<< "..." << std::endl
;
1336 std::vector
<Node
> dt_children_cons
;
1337 bool success
= true;
1340 Node split_cond_enum
;
1341 unsigned split_cond_res_index
= 0;
1342 CVC4_UNUSED
bool set_split_cond_res_index
= false;
1344 for (unsigned sc
= 0, size
= etis
->d_cenum
.size(); sc
< size
; sc
++)
1346 indent("sygus-sui-dt", ind
+ 1);
1347 Trace("sygus-sui-dt")
1348 << "construct PBE child #" << sc
<< "..." << std::endl
;
1351 std::pair
<Node
, NodeRole
>& cenum
= etis
->d_cenum
[sc
];
1353 // update the context
1354 std::vector
<Node
> prev
;
1355 if (strat
== strat_ITE
&& sc
> 0)
1357 EnumCache
& ecache_cond
= d_ecache
[split_cond_enum
];
1358 Assert(set_split_cond_res_index
);
1359 Assert(split_cond_res_index
< ecache_cond
.d_enum_vals_res
.size());
1361 x
.updateContext(this,
1362 ecache_cond
.d_enum_vals_res
[split_cond_res_index
],
1364 // return value of above call may be false in corner cases where we
1365 // must choose a non-separating condition to traverse to another
1370 if (strat
== strat_ITE
&& sc
== 0)
1372 Node ce
= cenum
.first
;
1374 EnumCache
& ecache_child
= d_ecache
[ce
];
1376 // get the conditionals in the current context : they must be
1378 std::map
<int, std::vector
<Node
> > possible_cond
;
1379 std::map
<Node
, int> solved_cond
; // stores branch
1380 ecache_child
.d_term_trie
.getLeaves(x
.d_vals
, true, possible_cond
);
1382 std::map
<int, std::vector
<Node
>>::iterator itpc
=
1383 possible_cond
.find(0);
1384 if (itpc
!= possible_cond
.end())
1386 if (Trace
.isOn("sygus-sui-dt-debug"))
1388 indent("sygus-sui-dt-debug", ind
+ 1);
1389 Trace("sygus-sui-dt-debug")
1390 << "PBE : We have " << itpc
->second
.size()
1391 << " distinguishable conditionals:" << std::endl
;
1392 for (Node
& cond
: itpc
->second
)
1394 indent("sygus-sui-dt-debug", ind
+ 2);
1395 Trace("sygus-sui-dt-debug")
1396 << d_tds
->sygusToBuiltin(cond
) << std::endl
;
1401 rec_c
= constructBestConditional(ce
, itpc
->second
);
1402 Assert(!rec_c
.isNull());
1403 indent("sygus-sui-dt", ind
);
1404 Trace("sygus-sui-dt")
1405 << "PBE: ITE strategy : choose best conditional "
1406 << d_tds
->sygusToBuiltin(rec_c
) << std::endl
;
1411 // TODO (#1250) : degenerate case where children have different
1413 indent("sygus-sui-dt", ind
);
1414 Trace("sygus-sui-dt") << "return PBE: failed ITE strategy, "
1415 "cannot find a distinguishable condition"
1418 if (!rec_c
.isNull())
1420 Assert(ecache_child
.d_enum_val_to_index
.find(rec_c
)
1421 != ecache_child
.d_enum_val_to_index
.end());
1422 split_cond_res_index
= ecache_child
.d_enum_val_to_index
[rec_c
];
1423 set_split_cond_res_index
= true;
1424 split_cond_enum
= ce
;
1425 Assert(split_cond_res_index
1426 < ecache_child
.d_enum_vals_res
.size());
1432 rec_c
= constructSol(f
, cenum
.first
, cenum
.second
, ind
+ 2, lemmas
);
1434 // undo update the context
1435 if (strat
== strat_ITE
&& sc
> 0)
1439 if (!rec_c
.isNull())
1441 dt_children_cons
.push_back(rec_c
);
1451 Assert(dt_children_cons
.size() == etis
->d_sol_templ_args
.size());
1452 // ret_dt = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR,
1454 ret_dt
= etis
->d_sol_templ
;
1455 ret_dt
= ret_dt
.substitute(etis
->d_sol_templ_args
.begin(),
1456 etis
->d_sol_templ_args
.end(),
1457 dt_children_cons
.begin(),
1458 dt_children_cons
.end());
1459 indent("sygus-sui-dt-debug", ind
);
1460 Trace("sygus-sui-dt-debug")
1461 << "PBE: success : constructed for strategy " << strat
<< std::endl
;
1465 indent("sygus-sui-dt-debug", ind
);
1466 Trace("sygus-sui-dt-debug")
1467 << "PBE: failed for strategy " << strat
<< std::endl
;
1474 // if there was a cached solution, process it now
1475 if (!cached_ret_dt
.isNull() && cached_ret_dt
!= ret_dt
)
1477 if (ret_dt
.isNull())
1479 // take the cached one if it is the only one
1480 ret_dt
= cached_ret_dt
;
1482 else if (d_enableMinimality
)
1484 Assert(ret_dt
.getType() == cached_ret_dt
.getType());
1485 // take the cached one if it is smaller
1486 std::vector
<Node
> retDts
;
1487 retDts
.push_back(cached_ret_dt
);
1488 retDts
.push_back(ret_dt
);
1489 ret_dt
= getMinimalTerm(retDts
);
1492 Assert(ret_dt
.isNull() || ret_dt
.getType() == e
.getType());
1493 if (Trace
.isOn("sygus-sui-dt"))
1495 indent("sygus-sui-dt", ind
);
1496 Trace("sygus-sui-dt") << "ConstructPBE: returned ";
1497 TermDbSygus::toStreamSygus("sygus-sui-dt", ret_dt
);
1498 Trace("sygus-sui-dt") << std::endl
;
1500 // remember the solution
1501 if (nrole
== role_equal
)
1503 if (!retValMod
&& !ret_dt
.isNull())
1505 for (size_t i
= 0, nvals
= x
.d_vals
.size(); i
< nvals
; i
++)
1507 if (x
.d_vals
[i
].getConst
<bool>())
1509 if (Trace
.isOn("sygus-sui-cache"))
1511 indent("sygus-sui-cache", ind
);
1512 Trace("sygus-sui-cache") << "Cache solution (#" << i
<< ") : ";
1513 TermDbSygus::toStreamSygus("sygus-sui-cache", ret_dt
);
1514 Trace("sygus-sui-cache") << std::endl
;
1516 d_psolutions
[i
][etn
].insert(ret_dt
);
1525 Node
SygusUnifIo::constructBestConditional(Node ce
,
1526 const std::vector
<Node
>& conds
)
1528 if (!d_solConsUsingInfoGain
)
1530 return SygusUnif::constructBestConditional(ce
, conds
);
1532 UnifContextIo
& x
= d_context
;
1533 // use information gain heuristic
1534 Trace("sygus-sui-dt-igain") << "Best information gain in context ";
1535 print_val("sygus-sui-dt-igain", x
.d_vals
);
1536 Trace("sygus-sui-dt-igain") << std::endl
;
1537 // set of indices that are active in this branch, i.e. x.d_vals[i] is true
1538 std::vector
<unsigned> activeIndices
;
1539 // map (j,t,s) -> n, such that the j^th condition in the vector conds
1540 // evaluates to t (typically true/false) on n active I/O pairs with output s.
1541 std::map
<unsigned, std::map
<Node
, std::map
<Node
, unsigned>>> eval
;
1542 // map (j,t) -> m, such that the j^th condition in the vector conds
1543 // evaluates to t (typically true/false) for m active I/O pairs.
1544 std::map
<unsigned, std::map
<Node
, unsigned>> evalCount
;
1545 unsigned nconds
= conds
.size();
1546 EnumCache
& ecache
= d_ecache
[ce
];
1547 // Get the index of conds[j] in the enumerator cache, this is to look up
1548 // its evaluation on each point.
1549 std::vector
<unsigned> eindex
;
1550 for (unsigned j
= 0; j
< nconds
; j
++)
1552 eindex
.push_back(ecache
.d_enum_val_to_index
[conds
[j
]]);
1554 unsigned activePoints
= 0;
1555 for (unsigned i
= 0, npoints
= x
.d_vals
.size(); i
< npoints
; i
++)
1557 if (x
.d_vals
[i
].getConst
<bool>())
1560 Node eo
= d_examples_out
[i
];
1561 for (unsigned j
= 0; j
< nconds
; j
++)
1563 Node resn
= ecache
.d_enum_vals_res
[eindex
[j
]][i
];
1564 Assert(resn
.isConst());
1565 eval
[j
][resn
][eo
]++;
1566 evalCount
[j
][resn
]++;
1570 AlwaysAssert(activePoints
> 0);
1571 // find the condition that leads to the lowest entropy
1572 // initially set minEntropy to > 1.0.
1573 double minEntropy
= 2.0;
1574 unsigned bestIndex
= 0;
1576 for (unsigned j
= 0; j
< nconds
; j
++)
1578 // To compute the entropy for a condition C, for pair of terms (s, t), let
1579 // prob(t) be the probability C evaluates to t on an active point,
1580 // prob(s|t) be the probability that an active point on which C
1581 // evaluates to t has output s.
1582 // Then, the entropy of C is:
1583 // sum{t}. prob(t)*( sum{s}. -prob(s|t)*log2(prob(s|t)) )
1584 // where notice this is always between 0 and 1.
1585 double entropySum
= 0.0;
1586 Trace("sygus-sui-dt-igain") << j
<< " : ";
1587 for (std::pair
<const Node
, std::map
<Node
, unsigned>>& ej
: eval
[j
])
1589 unsigned ecount
= evalCount
[j
][ej
.first
];
1592 double probBranch
= double(ecount
) / double(activePoints
);
1593 Trace("sygus-sui-dt-igain") << ej
.first
<< " -> ( ";
1594 for (std::pair
<const Node
, unsigned>& eej
: ej
.second
)
1598 double probVal
= double(eej
.second
) / double(ecount
);
1599 Trace("sygus-sui-dt-igain")
1600 << eej
.first
<< ":" << eej
.second
<< " ";
1601 double factor
= -probVal
* log2(probVal
);
1602 entropySum
+= probBranch
* factor
;
1605 Trace("sygus-sui-dt-igain") << ") ";
1608 Trace("sygus-sui-dt-igain") << "..." << entropySum
<< std::endl
;
1609 // either less, or equal and coin flip passes
1611 if (entropySum
== minEntropy
)
1614 if (Random::getRandom().pickWithProb(double(1) / double(numEqual
)))
1619 else if (entropySum
< minEntropy
)
1626 minEntropy
= entropySum
;
1631 Assert(!conds
.empty());
1632 return conds
[bestIndex
];
1635 } /* CVC4::theory::quantifiers namespace */
1636 } /* CVC4::theory namespace */
1637 } /* CVC4 namespace */