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 (!checkExistsOnly
)
243 // remove it if checkExistsOnly = false
244 d_term
= Node::null();
250 Assert(!checkExistsOnly
&& checkSubsume
);
254 NodeManager
* nm
= NodeManager::currentNM();
256 Assert(pol
|| (vals
[index
].isConst() && vals
[index
].getType().isBoolean()));
257 Node cv
= pol
? vals
[index
] : nm
->mkConst(!vals
[index
].getConst
<bool>());
258 // if checkExistsOnly = false, check if the current value is subsumed if
259 // checkSubsume = true, if so, don't add
260 if (!checkExistsOnly
&& checkSubsume
)
262 Assert(cv
.isConst() && cv
.getType().isBoolean());
263 std::vector
<bool> check_subsumed_by
;
266 if (!cv
.getConst
<bool>())
268 check_subsumed_by
.push_back(spol
);
271 else if (status
== -1)
273 check_subsumed_by
.push_back(spol
);
274 if (!cv
.getConst
<bool>())
276 check_subsumed_by
.push_back(!spol
);
279 // check for subsumed nodes
280 for (unsigned i
= 0, size
= check_subsumed_by
.size(); i
< size
; i
++)
282 bool csbi
= check_subsumed_by
[i
];
283 Node csval
= nm
->mkConst(csbi
);
285 std::map
<Node
, SubsumeTrie
>::iterator itc
= d_children
.find(csval
);
286 if (itc
!= d_children
.end())
288 Node ret
= itc
->second
.addTermInternal(t
,
306 std::vector
<bool> check_subsume
;
311 std::map
<Node
, SubsumeTrie
>::iterator itc
= d_children
.find(cv
);
312 if (itc
!= d_children
.end())
314 ret
= itc
->second
.addTermInternal(t
,
328 ret
= d_children
[cv
].addTermInternal(t
,
339 // we were subsumed by ret, return
345 Assert(cv
.isConst() && cv
.getType().isBoolean());
346 // check for subsuming
347 if (cv
.getConst
<bool>())
349 check_subsume
.push_back(!spol
);
353 else if (status
== 1)
355 Assert(checkSubsume
);
356 Assert(cv
.isConst() && cv
.getType().isBoolean());
357 check_subsume
.push_back(!spol
);
358 if (cv
.getConst
<bool>())
360 check_subsume
.push_back(spol
);
365 // check for subsumed terms
366 for (unsigned i
= 0, size
= check_subsume
.size(); i
< size
; i
++)
368 Node csval
= nm
->mkConst
<bool>(check_subsume
[i
]);
369 std::map
<Node
, SubsumeTrie
>::iterator itc
= d_children
.find(csval
);
370 if (itc
!= d_children
.end())
372 itc
->second
.addTermInternal(t
,
382 if (itc
->second
.isEmpty())
384 Assert(!checkExistsOnly
);
385 d_children
.erase(csval
);
393 Node
SubsumeTrie::addTerm(Node t
,
394 const std::vector
<Node
>& vals
,
396 std::vector
<Node
>& subsumed
)
398 return addTermInternal(t
, vals
, pol
, subsumed
, true, 0, 0, false, true);
401 Node
SubsumeTrie::addCond(Node c
, const std::vector
<Node
>& vals
, bool pol
)
403 std::vector
<Node
> subsumed
;
404 return addTermInternal(c
, vals
, pol
, subsumed
, true, 0, 0, false, false);
407 void SubsumeTrie::getSubsumed(const std::vector
<Node
>& vals
,
409 std::vector
<Node
>& subsumed
)
411 addTermInternal(Node::null(), vals
, pol
, subsumed
, true, 0, 1, true, true);
414 void SubsumeTrie::getSubsumedBy(const std::vector
<Node
>& vals
,
416 std::vector
<Node
>& subsumed_by
)
420 Node::null(), vals
, !pol
, subsumed_by
, false, 0, 1, true, true);
423 void SubsumeTrie::getLeavesInternal(const std::vector
<Node
>& vals
,
425 std::map
<int, std::vector
<Node
> >& v
,
429 if (index
== vals
.size())
431 Assert(!d_term
.isNull());
432 Assert(std::find(v
[status
].begin(), v
[status
].end(), d_term
)
434 v
[status
].push_back(d_term
);
438 Assert(vals
[index
].isConst() && vals
[index
].getType().isBoolean());
439 bool curr_val_true
= vals
[index
].getConst
<bool>() == pol
;
440 for (std::map
<Node
, SubsumeTrie
>::iterator it
= d_children
.begin();
441 it
!= d_children
.end();
444 int new_status
= status
;
445 // if the current value is true
450 Assert(it
->first
.isConst() && it
->first
.getType().isBoolean());
451 new_status
= (it
->first
.getConst
<bool>() ? 1 : -1);
452 if (status
!= -2 && new_status
!= status
)
458 it
->second
.getLeavesInternal(vals
, pol
, v
, index
+ 1, new_status
);
463 void SubsumeTrie::getLeaves(const std::vector
<Node
>& vals
,
465 std::map
<int, std::vector
<Node
> >& v
)
467 getLeavesInternal(vals
, pol
, v
, 0, -2);
470 SygusUnifIo::SygusUnifIo()
471 : d_check_sol(false),
473 d_sol_cons_nondet(false),
474 d_solConsUsingInfoGain(false)
476 d_true
= NodeManager::currentNM()->mkConst(true);
477 d_false
= NodeManager::currentNM()->mkConst(false);
480 SygusUnifIo::~SygusUnifIo() {}
481 void SygusUnifIo::initializeCandidate(
482 QuantifiersEngine
* qe
,
484 std::vector
<Node
>& enums
,
485 std::map
<Node
, std::vector
<Node
>>& strategy_lemmas
)
488 d_examples_out
.clear();
491 SygusUnif::initializeCandidate(qe
, f
, enums
, strategy_lemmas
);
492 // learn redundant operators based on the strategy
493 d_strategy
[f
].staticLearnRedundantOps(strategy_lemmas
);
496 void SygusUnifIo::addExample(const std::vector
<Node
>& input
, Node output
)
498 d_examples
.push_back(input
);
499 d_examples_out
.push_back(output
);
502 void SygusUnifIo::computeExamples(Node e
, Node bv
, std::vector
<Node
>& exOut
)
504 std::map
<Node
, std::vector
<Node
>>& eoc
= d_exOutCache
[e
];
505 std::map
<Node
, std::vector
<Node
>>::iterator it
= eoc
.find(bv
);
508 exOut
.insert(exOut
.end(), it
->second
.begin(), it
->second
.end());
511 TypeNode xtn
= e
.getType();
512 std::vector
<Node
>& eocv
= eoc
[bv
];
513 for (size_t j
= 0, size
= d_examples
.size(); j
< size
; j
++)
515 Node res
= d_tds
->evaluateBuiltin(xtn
, bv
, d_examples
[j
]);
516 exOut
.push_back(res
);
521 void SygusUnifIo::clearExampleCache(Node e
, Node bv
)
523 std::map
<Node
, std::vector
<Node
>>& eoc
= d_exOutCache
[e
];
524 Assert(eoc
.find(bv
) != eoc
.end());
528 void SygusUnifIo::notifyEnumeration(Node e
, Node v
, std::vector
<Node
>& lemmas
)
530 Trace("sygus-sui-enum") << "Notify enumeration for " << e
<< " : " << v
532 Node c
= d_candidate
;
533 Assert(!d_examples
.empty());
534 Assert(d_examples
.size() == d_examples_out
.size());
536 EnumInfo
& ei
= d_strategy
[c
].getEnumInfo(e
);
537 // The explanation for why the current value should be excluded in future
541 std::vector
<Node
> base_results
;
542 TypeNode xtn
= e
.getType();
543 Node bv
= d_tds
->sygusToBuiltin(v
, xtn
);
544 bv
= d_tds
->getExtRewriter()->extendedRewrite(bv
);
545 Trace("sygus-sui-enum") << "PBE Compute Examples for " << bv
<< std::endl
;
546 // compte the results (should be cached)
547 computeExamples(e
, bv
, base_results
);
548 // don't need it after this
549 clearExampleCache(e
, bv
);
550 // get the results for each slave enumerator
551 std::map
<Node
, std::vector
<Node
>> srmap
;
552 Evaluator
* ev
= d_tds
->getEvaluator();
553 bool tryEval
= options::sygusEvalOpt();
554 for (const Node
& xs
: ei
.d_enum_slave
)
556 Assert(srmap
.find(xs
) == srmap
.end());
557 EnumInfo
& eiv
= d_strategy
[c
].getEnumInfo(xs
);
558 Node templ
= eiv
.d_template
;
561 TNode templ_var
= eiv
.d_template_arg
;
562 std::vector
<Node
> args
;
563 args
.push_back(templ_var
);
564 std::vector
<Node
> sresults
;
565 for (const Node
& res
: base_results
)
568 std::vector
<Node
> vals
;
569 vals
.push_back(tres
);
573 sres
= ev
->eval(templ
, args
, vals
);
577 // fall back on rewriter
578 sres
= templ
.substitute(templ_var
, tres
);
579 sres
= Rewriter::rewrite(sres
);
581 sresults
.push_back(sres
);
583 srmap
[xs
] = sresults
;
587 srmap
[xs
] = base_results
;
591 // is it excluded for domain-specific reason?
592 std::vector
<Node
> exp_exc_vec
;
593 Assert(d_tds
->isEnumerator(e
));
594 bool isPassive
= d_tds
->isPassiveEnumerator(e
);
595 if (getExplanationForEnumeratorExclude(e
, v
, base_results
, exp_exc_vec
))
599 Assert(!exp_exc_vec
.empty());
600 exp_exc
= exp_exc_vec
.size() == 1
602 : NodeManager::currentNM()->mkNode(AND
, exp_exc_vec
);
604 Trace("sygus-sui-enum")
605 << " ...fail : term is excluded (domain-specific)" << std::endl
;
610 Assert(!ei
.d_enum_slave
.empty());
611 // explanation for why this value should be excluded
612 for (unsigned s
= 0; s
< ei
.d_enum_slave
.size(); s
++)
614 Node xs
= ei
.d_enum_slave
[s
];
615 EnumInfo
& eiv
= d_strategy
[c
].getEnumInfo(xs
);
616 EnumCache
& ecv
= d_ecache
[xs
];
617 Trace("sygus-sui-enum") << "Process " << xs
<< " from " << s
<< std::endl
;
618 // bool prevIsCover = false;
619 if (eiv
.getRole() == enum_io
)
621 Trace("sygus-sui-enum") << " IO-Eval of ";
622 // prevIsCover = eiv.isFeasible();
626 Trace("sygus-sui-enum") << "Evaluation of ";
628 Trace("sygus-sui-enum") << xs
<< " : ";
629 // evaluate all input/output examples
630 std::vector
<Node
> results
;
631 std::map
<Node
, bool> cond_vals
;
632 std::map
<Node
, std::vector
<Node
>>::iterator itsr
= srmap
.find(xs
);
633 Assert(itsr
!= srmap
.end());
634 for (unsigned j
= 0, size
= itsr
->second
.size(); j
< size
; j
++)
636 Node res
= itsr
->second
[j
];
637 Assert(res
.isConst());
639 if (eiv
.getRole() == enum_io
)
641 Node out
= d_examples_out
[j
];
642 Assert(out
.isConst());
643 resb
= res
== out
? d_true
: d_false
;
649 cond_vals
[resb
] = true;
650 results
.push_back(resb
);
651 if (Trace
.isOn("sygus-sui-enum"))
653 if (resb
.getType().isBoolean())
655 Trace("sygus-sui-enum") << (resb
== d_true
? "1" : "0");
659 Trace("sygus-sui-enum") << "?";
664 if (eiv
.getRole() == enum_io
)
666 // latter is the degenerate case of no examples
667 if (cond_vals
.find(d_true
) != cond_vals
.end() || cond_vals
.empty())
669 // check subsumbed/subsuming
670 std::vector
<Node
> subsume
;
671 if (cond_vals
.find(d_false
) == cond_vals
.end())
673 // it is the entire solution, we are done
674 Trace("sygus-sui-enum")
675 << " ...success, full solution added to PBE pool : "
676 << d_tds
->sygusToBuiltin(v
) << std::endl
;
680 // it subsumes everything
681 ecv
.d_term_trie
.clear();
682 ecv
.d_term_trie
.addTerm(v
, results
, true, subsume
);
688 Node val
= ecv
.d_term_trie
.addTerm(v
, results
, true, subsume
);
691 Trace("sygus-sui-enum") << " ...success";
692 if (!subsume
.empty())
694 ecv
.d_enum_subsume
.insert(
695 ecv
.d_enum_subsume
.end(), subsume
.begin(), subsume
.end());
696 Trace("sygus-sui-enum")
697 << " and subsumed " << subsume
.size() << " terms";
699 Trace("sygus-sui-enum")
700 << "! add to PBE pool : " << d_tds
->sygusToBuiltin(v
)
706 Assert(subsume
.empty());
707 Trace("sygus-sui-enum") << " ...fail : subsumed" << std::endl
;
713 Trace("sygus-sui-enum")
714 << " ...fail : it does not satisfy examples." << std::endl
;
719 // must be unique up to examples
720 Node val
= ecv
.d_term_trie
.addCond(v
, results
, true);
723 Trace("sygus-sui-enum") << " ...success! add to PBE pool : "
724 << d_tds
->sygusToBuiltin(v
) << std::endl
;
729 Trace("sygus-sui-enum")
730 << " ...fail : term is not unique" << std::endl
;
735 // notify to retry the build of solution
738 ecv
.addEnumValue(v
, results
);
745 // exclude this value on subsequent iterations
746 if (exp_exc
.isNull())
748 Trace("sygus-sui-enum-lemma") << "Use basic exclusion." << std::endl
;
749 // if we did not already explain why this should be excluded, use default
750 exp_exc
= d_tds
->getExplain()->getExplanationForEquality(e
, v
);
752 exp_exc
= exp_exc
.negate();
753 Trace("sygus-sui-enum-lemma")
754 << "SygusUnifIo : enumeration exclude lemma : " << exp_exc
<< std::endl
;
755 lemmas
.push_back(exp_exc
);
759 bool SygusUnifIo::constructSolution(std::vector
<Node
>& sols
,
760 std::vector
<Node
>& lemmas
)
762 Node sol
= constructSolutionNode(lemmas
);
771 Node
SygusUnifIo::constructSolutionNode(std::vector
<Node
>& lemmas
)
773 Node c
= d_candidate
;
774 if (!d_solution
.isNull())
776 // already has a solution
779 // only check if an enumerator updated
782 Trace("sygus-pbe") << "Construct solution, #iterations = " << d_cond_count
785 d_solConsUsingInfoGain
= false;
786 // try multiple times if we have done multiple conditions, due to
788 unsigned sol_term_size
= 0;
789 for (unsigned i
= 0; i
<= d_cond_count
; i
++)
791 Trace("sygus-pbe-dt") << "ConstructPBE for candidate: " << c
<< std::endl
;
792 // initialize a call to construct solution
793 initializeConstructSol();
794 initializeConstructSolFor(c
);
795 // call the virtual construct solution method
796 Node e
= d_strategy
[c
].getRootEnumerator();
797 Node vcc
= constructSol(c
, e
, role_equal
, 1, lemmas
);
798 // if we constructed the solution, and we either did not previously have
799 // a solution, or the new solution is better (smaller).
801 && (d_solution
.isNull()
802 || (!d_solution
.isNull()
803 && d_tds
->getSygusTermSize(vcc
) < sol_term_size
)))
805 Trace("sygus-pbe") << "**** SygusUnif SOLVED : " << c
<< " = " << vcc
807 Trace("sygus-pbe") << "...solved at iteration " << i
<< std::endl
;
809 sol_term_size
= d_tds
->getSygusTermSize(vcc
);
810 // We've determined its feasible, now, enable information gain and
811 // retry. We do this since information gain comes with an overhead,
812 // and we want testing feasibility to be fast.
813 if (!d_solConsUsingInfoGain
)
815 d_solConsUsingInfoGain
= true;
819 else if (!d_sol_cons_nondet
)
824 if (!d_solution
.isNull())
828 Trace("sygus-pbe") << "...failed to solve." << std::endl
;
833 // ------------------------------------ solution construction from enumeration
835 bool SygusUnifIo::useStrContainsEnumeratorExclude(Node e
)
837 TypeNode xbt
= d_tds
->sygusToBuiltinType(e
.getType());
840 std::map
<Node
, bool>::iterator itx
= d_use_str_contains_eexc
.find(e
);
841 if (itx
!= d_use_str_contains_eexc
.end())
845 Trace("sygus-sui-enum-debug")
846 << "Is " << e
<< " is str.contains exclusion?" << std::endl
;
847 d_use_str_contains_eexc
[e
] = true;
848 Node c
= d_candidate
;
849 EnumInfo
& ei
= d_strategy
[c
].getEnumInfo(e
);
850 for (const Node
& sn
: ei
.d_enum_slave
)
852 EnumInfo
& eis
= d_strategy
[c
].getEnumInfo(sn
);
853 EnumRole er
= eis
.getRole();
854 if (er
!= enum_io
&& er
!= enum_concat_term
)
856 Trace("sygus-sui-enum-debug") << " incompatible slave : " << sn
857 << ", role = " << er
<< std::endl
;
858 d_use_str_contains_eexc
[e
] = false;
861 if (eis
.isConditional())
863 Trace("sygus-sui-enum-debug")
864 << " conditional slave : " << sn
<< std::endl
;
865 d_use_str_contains_eexc
[e
] = false;
869 Trace("sygus-sui-enum-debug")
870 << "...can use str.contains exclusion." << std::endl
;
871 return d_use_str_contains_eexc
[e
];
876 bool SygusUnifIo::getExplanationForEnumeratorExclude(
879 std::vector
<Node
>& results
,
880 std::vector
<Node
>& exp
)
882 NodeManager
* nm
= NodeManager::currentNM();
883 if (useStrContainsEnumeratorExclude(e
))
885 // This check whether the example evaluates to something that is larger than
886 // the output for some input/output pair. If so, then this term is never
887 // useful. We generalize its explanation below.
889 if (Trace
.isOn("sygus-sui-cterm-debug"))
891 Trace("sygus-sui-enum") << std::endl
;
893 // check if all examples had longer length that the output
894 Assert(d_examples_out
.size() == results
.size());
895 Trace("sygus-sui-cterm-debug")
896 << "Check enumerator exclusion for " << e
<< " -> "
897 << d_tds
->sygusToBuiltin(v
) << " based on str.contains." << std::endl
;
898 std::vector
<unsigned> cmp_indices
;
899 for (unsigned i
= 0, size
= results
.size(); i
< size
; i
++)
901 Assert(results
[i
].isConst());
902 Assert(d_examples_out
[i
].isConst());
903 Trace("sygus-sui-cterm-debug")
904 << " " << results
[i
] << " <> " << d_examples_out
[i
];
905 Node cont
= nm
->mkNode(STRING_STRCTN
, d_examples_out
[i
], results
[i
]);
906 Node contr
= Rewriter::rewrite(cont
);
907 if (contr
== d_false
)
909 cmp_indices
.push_back(i
);
910 Trace("sygus-sui-cterm-debug") << "...not contained." << std::endl
;
914 Trace("sygus-sui-cterm-debug") << "...contained." << std::endl
;
917 if (!cmp_indices
.empty())
919 // we check invariance with respect to a negative contains test
920 NegContainsSygusInvarianceTest ncset
;
921 ncset
.init(e
, d_examples
, d_examples_out
, cmp_indices
);
922 // construct the generalized explanation
923 d_tds
->getExplain()->getExplanationFor(e
, v
, exp
, ncset
);
924 Trace("sygus-sui-cterm")
925 << "PBE-cterm : enumerator exclude " << d_tds
->sygusToBuiltin(v
)
926 << " due to negative containment." << std::endl
;
933 void SygusUnifIo::EnumCache::addEnumValue(Node v
, std::vector
<Node
>& results
)
935 // should not have been enumerated before
936 Assert(d_enum_val_to_index
.find(v
) == d_enum_val_to_index
.end());
937 d_enum_val_to_index
[v
] = d_enum_vals
.size();
938 d_enum_vals
.push_back(v
);
939 d_enum_vals_res
.push_back(results
);
942 void SygusUnifIo::initializeConstructSol()
944 d_context
.initialize(this);
945 d_sol_cons_nondet
= false;
948 void SygusUnifIo::initializeConstructSolFor(Node f
)
950 Assert(d_candidate
== f
);
953 Node
SygusUnifIo::constructSol(
954 Node f
, Node e
, NodeRole nrole
, int ind
, std::vector
<Node
>& lemmas
)
956 Assert(d_candidate
== f
);
957 UnifContextIo
& x
= d_context
;
958 TypeNode etn
= e
.getType();
959 if (Trace
.isOn("sygus-sui-dt-debug"))
961 indent("sygus-sui-dt-debug", ind
);
962 Trace("sygus-sui-dt-debug") << "ConstructPBE: (" << e
<< ", " << nrole
963 << ") for type " << etn
<< " in context ";
964 print_val("sygus-sui-dt-debug", x
.d_vals
);
965 NodeRole ctx_role
= x
.getCurrentRole();
966 Trace("sygus-sui-dt-debug") << ", context role [" << ctx_role
;
967 if (ctx_role
== role_string_prefix
|| ctx_role
== role_string_suffix
)
969 Trace("sygus-sui-dt-debug") << ", string pos : ";
970 for (unsigned i
= 0, size
= x
.d_str_pos
.size(); i
< size
; i
++)
972 Trace("sygus-sui-dt-debug") << " " << x
.d_str_pos
[i
];
975 Trace("sygus-sui-dt-debug") << "]";
976 Trace("sygus-sui-dt-debug") << std::endl
;
978 // enumerator type info
979 EnumTypeInfo
& tinfo
= d_strategy
[f
].getEnumTypeInfo(etn
);
981 // get the enumerator information
982 EnumInfo
& einfo
= d_strategy
[f
].getEnumInfo(e
);
984 EnumCache
& ecache
= d_ecache
[e
];
987 if (nrole
== role_equal
)
989 if (!x
.isReturnValueModified())
991 if (ecache
.isSolved())
993 // this type has a complete solution
994 ret_dt
= ecache
.getSolved();
995 indent("sygus-sui-dt", ind
);
996 Trace("sygus-sui-dt") << "return PBE: success : solved "
997 << d_tds
->sygusToBuiltin(ret_dt
) << std::endl
;
998 Assert(!ret_dt
.isNull());
1002 // could be conditionally solved
1003 std::vector
<Node
> subsumed_by
;
1004 ecache
.d_term_trie
.getSubsumedBy(x
.d_vals
, true, subsumed_by
);
1005 if (!subsumed_by
.empty())
1007 ret_dt
= constructBestSolvedTerm(e
, subsumed_by
);
1008 indent("sygus-sui-dt", ind
);
1009 Trace("sygus-sui-dt") << "return PBE: success : conditionally solved"
1010 << d_tds
->sygusToBuiltin(ret_dt
) << std::endl
;
1014 indent("sygus-sui-dt-debug", ind
);
1015 Trace("sygus-sui-dt-debug")
1016 << " ...not currently conditionally solved." << std::endl
;
1020 if (ret_dt
.isNull())
1022 if (d_tds
->sygusToBuiltinType(e
.getType()).isString())
1024 // check if a current value that closes all examples
1025 // get the term enumerator for this type
1026 std::map
<EnumRole
, Node
>::iterator itnt
=
1027 tinfo
.d_enum
.find(enum_concat_term
);
1028 if (itnt
!= tinfo
.d_enum
.end())
1030 Node et
= itnt
->second
;
1032 EnumCache
& ecachet
= d_ecache
[et
];
1033 // get the current examples
1034 std::vector
<String
> ex_vals
;
1035 x
.getCurrentStrings(this, d_examples_out
, ex_vals
);
1036 Assert(ecache
.d_enum_vals
.size() == ecache
.d_enum_vals_res
.size());
1038 // test each example in the term enumerator for the type
1039 std::vector
<Node
> str_solved
;
1040 for (unsigned i
= 0, size
= ecachet
.d_enum_vals
.size(); i
< size
; i
++)
1042 if (x
.isStringSolved(this, ex_vals
, ecachet
.d_enum_vals_res
[i
]))
1044 str_solved
.push_back(ecachet
.d_enum_vals
[i
]);
1047 if (!str_solved
.empty())
1049 ret_dt
= constructBestSolvedTerm(e
, str_solved
);
1050 indent("sygus-sui-dt", ind
);
1051 Trace("sygus-sui-dt") << "return PBE: success : string solved "
1052 << d_tds
->sygusToBuiltin(ret_dt
) << std::endl
;
1056 indent("sygus-sui-dt-debug", ind
);
1057 Trace("sygus-sui-dt-debug")
1058 << " ...not currently string solved." << std::endl
;
1064 else if (nrole
== role_string_prefix
|| nrole
== role_string_suffix
)
1066 // check if each return value is a prefix/suffix of all open examples
1067 if (!x
.isReturnValueModified() || x
.getCurrentRole() == nrole
)
1069 std::map
<Node
, std::vector
<unsigned> > incr
;
1070 bool isPrefix
= nrole
== role_string_prefix
;
1071 std::map
<Node
, unsigned> total_inc
;
1072 std::vector
<Node
> inc_strs
;
1073 // make the value of the examples
1074 std::vector
<String
> ex_vals
;
1075 x
.getCurrentStrings(this, d_examples_out
, ex_vals
);
1076 if (Trace
.isOn("sygus-sui-dt-debug"))
1078 indent("sygus-sui-dt-debug", ind
);
1079 Trace("sygus-sui-dt-debug") << "current strings : " << std::endl
;
1080 for (unsigned i
= 0, size
= ex_vals
.size(); i
< size
; i
++)
1082 indent("sygus-sui-dt-debug", ind
+ 1);
1083 Trace("sygus-sui-dt-debug") << ex_vals
[i
] << std::endl
;
1087 // check if there is a value for which is a prefix/suffix of all active
1089 Assert(ecache
.d_enum_vals
.size() == ecache
.d_enum_vals_res
.size());
1091 for (unsigned i
= 0, size
= ecache
.d_enum_vals
.size(); i
< size
; i
++)
1093 Node val_t
= ecache
.d_enum_vals
[i
];
1094 Assert(incr
.find(val_t
) == incr
.end());
1095 indent("sygus-sui-dt-debug", ind
);
1096 Trace("sygus-sui-dt-debug") << "increment string values : ";
1097 TermDbSygus::toStreamSygus("sygus-sui-dt-debug", val_t
);
1098 Trace("sygus-sui-dt-debug") << " : ";
1099 Assert(ecache
.d_enum_vals_res
[i
].size() == d_examples_out
.size());
1101 bool exsuccess
= x
.getStringIncrement(this,
1104 ecache
.d_enum_vals_res
[i
],
1110 Trace("sygus-sui-dt-debug") << "...fail" << std::endl
;
1114 total_inc
[val_t
] = tot
;
1115 inc_strs
.push_back(val_t
);
1116 Trace("sygus-sui-dt-debug")
1117 << "...success, total increment = " << tot
<< std::endl
;
1123 // solution construction for strings concatenation is non-deterministic
1124 // with respect to failure/success.
1125 d_sol_cons_nondet
= true;
1126 ret_dt
= constructBestStringToConcat(inc_strs
, total_inc
, incr
);
1127 Assert(!ret_dt
.isNull());
1128 indent("sygus-sui-dt", ind
);
1129 Trace("sygus-sui-dt")
1130 << "PBE: CONCAT strategy : choose " << (isPrefix
? "pre" : "suf")
1131 << "fix value " << d_tds
->sygusToBuiltin(ret_dt
) << std::endl
;
1132 // update the context
1133 bool ret
= x
.updateStringPosition(this, incr
[ret_dt
], nrole
);
1134 AlwaysAssert(ret
== (total_inc
[ret_dt
] > 0));
1138 indent("sygus-sui-dt", ind
);
1139 Trace("sygus-sui-dt") << "PBE: failed CONCAT strategy, no values are "
1140 << (isPrefix
? "pre" : "suf")
1141 << "fix of all examples." << std::endl
;
1146 indent("sygus-sui-dt", ind
);
1147 Trace("sygus-sui-dt")
1148 << "PBE: failed CONCAT strategy, prefix/suffix mismatch."
1152 if (!ret_dt
.isNull() || einfo
.isTemplated())
1154 Assert(ret_dt
.isNull() || ret_dt
.getType() == e
.getType());
1155 indent("sygus-sui-dt", ind
);
1156 Trace("sygus-sui-dt") << "ConstructPBE: returned (pre-strategy) " << ret_dt
1160 // we will try a single strategy
1161 EnumTypeInfoStrat
* etis
= nullptr;
1162 std::map
<NodeRole
, StrategyNode
>::iterator itsn
= tinfo
.d_snodes
.find(nrole
);
1163 if (itsn
== tinfo
.d_snodes
.end())
1165 indent("sygus-sui-dt", ind
);
1166 Trace("sygus-sui-dt") << "ConstructPBE: returned (no-strategy) " << ret_dt
1171 StrategyNode
& snode
= itsn
->second
;
1172 if (x
.d_visit_role
[e
].find(nrole
) != x
.d_visit_role
[e
].end())
1174 // already visited and context not changed (notice d_visit_role is cleared
1175 // when the context changes).
1176 indent("sygus-sui-dt", ind
);
1177 Trace("sygus-sui-dt") << "ConstructPBE: returned (already visited) "
1178 << ret_dt
<< std::endl
;
1181 x
.d_visit_role
[e
][nrole
] = true;
1182 // try a random strategy
1183 if (snode
.d_strats
.size() > 1)
1186 snode
.d_strats
.begin(), snode
.d_strats
.end(), Random::getRandom());
1188 // ITE always first if we have not yet solved
1189 // the reasoning is that splitting on conditions only subdivides the problem
1190 // and cannot be the source of failure, whereas the wrong choice for a
1191 // concatenation term may lead to failure
1192 if (d_solution
.isNull())
1194 for (unsigned i
= 0; i
< snode
.d_strats
.size(); i
++)
1196 if (snode
.d_strats
[i
]->d_this
== strat_ITE
)
1199 EnumTypeInfoStrat
* etis
= snode
.d_strats
[i
];
1200 snode
.d_strats
[i
] = snode
.d_strats
[0];
1201 snode
.d_strats
[0] = etis
;
1207 // iterate over the strategies
1208 unsigned sindex
= 0;
1209 bool did_recurse
= false;
1210 while (ret_dt
.isNull() && !did_recurse
&& sindex
< snode
.d_strats
.size())
1212 if (snode
.d_strats
[sindex
]->isValid(x
))
1214 etis
= snode
.d_strats
[sindex
];
1215 Assert(etis
!= nullptr);
1216 StrategyType strat
= etis
->d_this
;
1217 indent("sygus-sui-dt", ind
+ 1);
1218 Trace("sygus-sui-dt")
1219 << "...try STRATEGY " << strat
<< "..." << std::endl
;
1221 std::map
<unsigned, Node
> look_ahead_solved_children
;
1222 std::vector
<Node
> dt_children_cons
;
1223 bool success
= true;
1226 Node split_cond_enum
;
1227 unsigned split_cond_res_index
= 0;
1228 CVC4_UNUSED
bool set_split_cond_res_index
= false;
1230 for (unsigned sc
= 0, size
= etis
->d_cenum
.size(); sc
< size
; sc
++)
1232 indent("sygus-sui-dt", ind
+ 1);
1233 Trace("sygus-sui-dt")
1234 << "construct PBE child #" << sc
<< "..." << std::endl
;
1236 std::map
<unsigned, Node
>::iterator itla
=
1237 look_ahead_solved_children
.find(sc
);
1238 if (itla
!= look_ahead_solved_children
.end())
1240 rec_c
= itla
->second
;
1241 indent("sygus-sui-dt-debug", ind
+ 1);
1242 Trace("sygus-sui-dt-debug")
1243 << "ConstructPBE: look ahead solved : "
1244 << d_tds
->sygusToBuiltin(rec_c
) << std::endl
;
1248 std::pair
<Node
, NodeRole
>& cenum
= etis
->d_cenum
[sc
];
1250 // update the context
1251 std::vector
<Node
> prev
;
1252 if (strat
== strat_ITE
&& sc
> 0)
1254 EnumCache
& ecache_cond
= d_ecache
[split_cond_enum
];
1255 Assert(set_split_cond_res_index
);
1256 Assert(split_cond_res_index
< ecache_cond
.d_enum_vals_res
.size());
1258 bool ret
= x
.updateContext(
1260 ecache_cond
.d_enum_vals_res
[split_cond_res_index
],
1266 if (strat
== strat_ITE
&& sc
== 0)
1268 Node ce
= cenum
.first
;
1270 EnumCache
& ecache_child
= d_ecache
[ce
];
1272 // get the conditionals in the current context : they must be
1274 std::map
<int, std::vector
<Node
> > possible_cond
;
1275 std::map
<Node
, int> solved_cond
; // stores branch
1276 ecache_child
.d_term_trie
.getLeaves(x
.d_vals
, true, possible_cond
);
1278 std::map
<int, std::vector
<Node
> >::iterator itpc
=
1279 possible_cond
.find(0);
1280 if (itpc
!= possible_cond
.end())
1282 if (Trace
.isOn("sygus-sui-dt-debug"))
1284 indent("sygus-sui-dt-debug", ind
+ 1);
1285 Trace("sygus-sui-dt-debug")
1286 << "PBE : We have " << itpc
->second
.size()
1287 << " distinguishable conditionals:" << std::endl
;
1288 for (Node
& cond
: itpc
->second
)
1290 indent("sygus-sui-dt-debug", ind
+ 2);
1291 Trace("sygus-sui-dt-debug")
1292 << d_tds
->sygusToBuiltin(cond
) << std::endl
;
1296 // otherwise, guess a conditional
1299 rec_c
= constructBestConditional(ce
, itpc
->second
);
1300 Assert(!rec_c
.isNull());
1301 indent("sygus-sui-dt", ind
);
1302 Trace("sygus-sui-dt")
1303 << "PBE: ITE strategy : choose best conditional "
1304 << d_tds
->sygusToBuiltin(rec_c
) << std::endl
;
1309 // TODO (#1250) : degenerate case where children have different
1311 indent("sygus-sui-dt", ind
);
1312 Trace("sygus-sui-dt") << "return PBE: failed ITE strategy, "
1313 "cannot find a distinguishable condition"
1316 if (!rec_c
.isNull())
1318 Assert(ecache_child
.d_enum_val_to_index
.find(rec_c
)
1319 != ecache_child
.d_enum_val_to_index
.end());
1320 split_cond_res_index
= ecache_child
.d_enum_val_to_index
[rec_c
];
1321 set_split_cond_res_index
= true;
1322 split_cond_enum
= ce
;
1323 Assert(split_cond_res_index
1324 < ecache_child
.d_enum_vals_res
.size());
1330 rec_c
= constructSol(f
, cenum
.first
, cenum
.second
, ind
+ 2, lemmas
);
1333 // undo update the context
1334 if (strat
== strat_ITE
&& sc
> 0)
1339 if (!rec_c
.isNull())
1341 dt_children_cons
.push_back(rec_c
);
1351 Assert(dt_children_cons
.size() == etis
->d_sol_templ_args
.size());
1352 // ret_dt = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR,
1354 ret_dt
= etis
->d_sol_templ
;
1355 ret_dt
= ret_dt
.substitute(etis
->d_sol_templ_args
.begin(),
1356 etis
->d_sol_templ_args
.end(),
1357 dt_children_cons
.begin(),
1358 dt_children_cons
.end());
1359 indent("sygus-sui-dt-debug", ind
);
1360 Trace("sygus-sui-dt-debug")
1361 << "PBE: success : constructed for strategy " << strat
<< std::endl
;
1365 indent("sygus-sui-dt-debug", ind
);
1366 Trace("sygus-sui-dt-debug")
1367 << "PBE: failed for strategy " << strat
<< std::endl
;
1374 Assert(ret_dt
.isNull() || ret_dt
.getType() == e
.getType());
1375 indent("sygus-sui-dt", ind
);
1376 Trace("sygus-sui-dt") << "ConstructPBE: returned " << ret_dt
<< std::endl
;
1380 Node
SygusUnifIo::constructBestConditional(Node ce
,
1381 const std::vector
<Node
>& conds
)
1383 if (!d_solConsUsingInfoGain
)
1385 return SygusUnif::constructBestConditional(ce
, conds
);
1387 UnifContextIo
& x
= d_context
;
1388 // use information gain heuristic
1389 Trace("sygus-sui-dt-igain") << "Best information gain in context ";
1390 print_val("sygus-sui-dt-igain", x
.d_vals
);
1391 Trace("sygus-sui-dt-igain") << std::endl
;
1392 // set of indices that are active in this branch, i.e. x.d_vals[i] is true
1393 std::vector
<unsigned> activeIndices
;
1394 // map (j,t,s) -> n, such that the j^th condition in the vector conds
1395 // evaluates to t (typically true/false) on n active I/O pairs with output s.
1396 std::map
<unsigned, std::map
<Node
, std::map
<Node
, unsigned>>> eval
;
1397 // map (j,t) -> m, such that the j^th condition in the vector conds
1398 // evaluates to t (typically true/false) for m active I/O pairs.
1399 std::map
<unsigned, std::map
<Node
, unsigned>> evalCount
;
1400 unsigned nconds
= conds
.size();
1401 EnumCache
& ecache
= d_ecache
[ce
];
1402 // Get the index of conds[j] in the enumerator cache, this is to look up
1403 // its evaluation on each point.
1404 std::vector
<unsigned> eindex
;
1405 for (unsigned j
= 0; j
< nconds
; j
++)
1407 eindex
.push_back(ecache
.d_enum_val_to_index
[conds
[j
]]);
1409 unsigned activePoints
= 0;
1410 for (unsigned i
= 0, npoints
= x
.d_vals
.size(); i
< npoints
; i
++)
1412 if (x
.d_vals
[i
].getConst
<bool>())
1415 Node eo
= d_examples_out
[i
];
1416 for (unsigned j
= 0; j
< nconds
; j
++)
1418 Node resn
= ecache
.d_enum_vals_res
[eindex
[j
]][i
];
1419 Assert(resn
.isConst());
1420 eval
[j
][resn
][eo
]++;
1421 evalCount
[j
][resn
]++;
1425 AlwaysAssert(activePoints
> 0);
1426 // find the condition that leads to the lowest entropy
1427 // initially set minEntropy to > 1.0.
1428 double minEntropy
= 2.0;
1429 unsigned bestIndex
= 0;
1430 for (unsigned j
= 0; j
< nconds
; j
++)
1432 // To compute the entropy for a condition C, for pair of terms (s, t), let
1433 // prob(t) be the probability C evaluates to t on an active point,
1434 // prob(s|t) be the probability that an active point on which C
1435 // evaluates to t has output s.
1436 // Then, the entropy of C is:
1437 // sum{t}. prob(t)*( sum{s}. -prob(s|t)*log2(prob(s|t)) )
1438 // where notice this is always between 0 and 1.
1439 double entropySum
= 0.0;
1440 Trace("sygus-sui-dt-igain") << j
<< " : ";
1441 for (std::pair
<const Node
, std::map
<Node
, unsigned>>& ej
: eval
[j
])
1443 unsigned ecount
= evalCount
[j
][ej
.first
];
1446 double probBranch
= double(ecount
) / double(activePoints
);
1447 Trace("sygus-sui-dt-igain") << ej
.first
<< " -> ( ";
1448 for (std::pair
<const Node
, unsigned>& eej
: ej
.second
)
1452 double probVal
= double(eej
.second
) / double(ecount
);
1453 Trace("sygus-sui-dt-igain")
1454 << eej
.first
<< ":" << eej
.second
<< " ";
1455 double factor
= -probVal
* log2(probVal
);
1456 entropySum
+= probBranch
* factor
;
1459 Trace("sygus-sui-dt-igain") << ") ";
1462 Trace("sygus-sui-dt-igain") << "..." << entropySum
<< std::endl
;
1463 if (entropySum
< minEntropy
)
1465 minEntropy
= entropySum
;
1470 Assert(!conds
.empty());
1471 return conds
[bestIndex
];
1474 } /* CVC4::theory::quantifiers namespace */
1475 } /* CVC4::theory namespace */
1476 } /* CVC4 namespace */