From a035836d07e831cca30eef800fdf0b3ad88e0ede Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 27 Mar 2018 12:30:15 -0500 Subject: [PATCH] Make sygus unif utility (#1720) --- src/Makefile.am | 2 + .../quantifiers/sygus/sygus_invariance.cpp | 26 +- .../quantifiers/sygus/sygus_invariance.h | 18 +- src/theory/quantifiers/sygus/sygus_pbe.cpp | 124 +- src/theory/quantifiers/sygus/sygus_pbe.h | 65 +- src/theory/quantifiers/sygus/sygus_unif.cpp | 2284 +++++++++++++++++ src/theory/quantifiers/sygus/sygus_unif.h | 758 ++++++ 7 files changed, 3092 insertions(+), 185 deletions(-) create mode 100644 src/theory/quantifiers/sygus/sygus_unif.cpp create mode 100644 src/theory/quantifiers/sygus/sygus_unif.h diff --git a/src/Makefile.am b/src/Makefile.am index 53fc3b8bd..9b1b71efc 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -472,6 +472,8 @@ libcvc4_la_SOURCES = \ theory/quantifiers/sygus/sygus_module.h \ theory/quantifiers/sygus/sygus_process_conj.cpp \ theory/quantifiers/sygus/sygus_process_conj.h \ + theory/quantifiers/sygus/sygus_unif.cpp \ + theory/quantifiers/sygus/sygus_unif.h \ theory/quantifiers/sygus/term_database_sygus.cpp \ theory/quantifiers/sygus/term_database_sygus.h \ theory/quantifiers/sygus_sampler.cpp \ diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp index 6b4c6488d..f4aa07673 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.cpp +++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp @@ -157,20 +157,16 @@ bool DivByZeroSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x) return false; } -void NegContainsSygusInvarianceTest::init(CegConjecture* conj, - Node e, +void NegContainsSygusInvarianceTest::init(Node e, + std::vector >& ex, std::vector& exo, std::vector& ncind) { - if (conj->getPbe()->hasExamples(e)) - { - Assert(conj->getPbe()->getNumExamples(e) == exo.size()); - d_enum = e; - d_exo.insert(d_exo.end(), exo.begin(), exo.end()); - d_neg_con_indices.insert( - d_neg_con_indices.end(), ncind.begin(), ncind.end()); - d_conj = conj; - } + Assert(ex.size() == exo.size()); + d_enum = e; + d_ex.insert(d_ex.end(), ex.begin(), ex.end()); + d_exo.insert(d_exo.end(), exo.begin(), exo.end()); + d_neg_con_indices.insert(d_neg_con_indices.end(), ncind.begin(), ncind.end()); } bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds, @@ -187,7 +183,7 @@ bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds, { unsigned ii = d_neg_con_indices[i]; Assert(ii < d_exo.size()); - Node nbvre = d_conj->getPbe()->evaluateBuiltin(tn, nbvr, d_enum, ii); + Node nbvre = tds->evaluateBuiltin(tn, nbvr, d_ex[ii]); Node out = d_exo[ii]; Node cont = NodeManager::currentNM()->mkNode(kind::STRING_STRCTN, out, nbvre); @@ -203,11 +199,9 @@ bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds, << tds->sygusToBuiltin(x) << " since " << std::endl; Trace("sygus-pbe-cterm") << " PBE-cterm : for input example : "; - std::vector ex; - d_conj->getPbe()->getExample(d_enum, ii, ex); - for (unsigned j = 0; j < ex.size(); j++) + for (unsigned j = 0, size = d_ex[ii].size(); j < size; j++) { - Trace("sygus-pbe-cterm") << ex[j] << " "; + Trace("sygus-pbe-cterm") << d_ex[ii][j] << " "; } Trace("sygus-pbe-cterm") << std::endl; Trace("sygus-pbe-cterm") diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h index 9e357f928..577923f5b 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.h +++ b/src/theory/quantifiers/sygus/sygus_invariance.h @@ -234,21 +234,21 @@ class DivByZeroSygusInvarianceTest : public SygusInvarianceTest class NegContainsSygusInvarianceTest : public SygusInvarianceTest { public: - NegContainsSygusInvarianceTest() : d_conj(nullptr) {} + NegContainsSygusInvarianceTest() {} /** initialize this invariance test - * cpbe is the conjecture utility. * e is the enumerator which we are reasoning about (associated with a synth * fun). - * exo is the list of outputs of the PBE conjecture. - * ncind is the set of possible indices of the PBE conjecture to check - * invariance of non-containment. + * ex is the list of inputs, + * exo is the list of outputs, + * ncind is the set of possible example indices to check invariance of + * non-containment. * For example, in the above example, when t[x1] = "ab", then this * has the index 1 since contains("de de", "ab") ---> false but not * the index 0 since contains("abc abc","ab") ---> true. */ - void init(CegConjecture* conj, - Node e, + void init(Node e, + std::vector >& ex, std::vector& exo, std::vector& ncind); @@ -259,14 +259,14 @@ class NegContainsSygusInvarianceTest : public SygusInvarianceTest private: /** The enumerator whose value we are considering in this invariance test */ Node d_enum; + /** The input examples */ + std::vector > d_ex; /** The output examples for the enumerator */ std::vector d_exo; /** The set of I/O pair indices i such that * contains( out_i, nvn[in_i] ) ---> false */ std::vector d_neg_con_indices; - /** reference to the conjecture associated with this test */ - CegConjecture* d_conj; }; } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 528f47624..347efac26 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -28,74 +28,6 @@ namespace CVC4 { namespace theory { namespace quantifiers { -void indent( const char * c, int ind ) { - if( Trace.isOn(c) ){ - for( int i=0; i& vals, bool pol = true ){ - if( Trace.isOn(c) ){ - for( unsigned i=0; i() : !vals[i].getConst() ) ? "1" : "0" ); - } - } -} - -std::ostream& operator<<(std::ostream& os, EnumRole r) -{ - switch(r){ - case enum_invalid: os << "INVALID"; break; - case enum_io: os << "IO"; break; - case enum_ite_condition: os << "CONDITION"; break; - case enum_concat_term: os << "CTERM"; break; - default: os << "enum_" << static_cast(r); break; - } - return os; -} - -std::ostream& operator<<(std::ostream& os, NodeRole r) -{ - switch (r) - { - case role_equal: os << "equal"; break; - case role_string_prefix: os << "string_prefix"; break; - case role_string_suffix: os << "string_suffix"; break; - case role_ite_condition: os << "ite_condition"; break; - default: os << "role_" << static_cast(r); break; - } - return os; -} - -EnumRole getEnumeratorRoleForNodeRole(NodeRole r) -{ - switch (r) - { - case role_equal: return enum_io; break; - case role_string_prefix: return enum_concat_term; break; - case role_string_suffix: return enum_concat_term; break; - case role_ite_condition: return enum_ite_condition; break; - default: break; - } - return enum_invalid; -} - -std::ostream& operator<<(std::ostream& os, StrategyType st) -{ - switch (st) - { - case strat_ITE: os << "ITE"; break; - case strat_CONCAT_PREFIX: os << "CONCAT_PREFIX"; break; - case strat_CONCAT_SUFFIX: os << "CONCAT_SUFFIX"; break; - case strat_ID: os << "ID"; break; - default: os << "strat_" << static_cast(st); break; - } - return os; -} - CegConjecturePbe::CegConjecturePbe(QuantifiersEngine* qe, CegConjecture* p) : SygusModule(qe, p) { @@ -971,7 +903,7 @@ void CegConjecturePbe::staticLearnRedundantOps( { itn->second.setConditional(); } - indent("sygus-unif", ind); + SygusUnif::indent("sygus-unif", ind); Trace("sygus-unif") << e << " :: node role : " << nrole; Trace("sygus-unif") << ", type : " @@ -1012,7 +944,7 @@ void CegConjecturePbe::staticLearnRedundantOps( EnumTypeInfoStrat* etis = snode.d_strats[j]; StrategyType strat = etis->d_this; bool newIsCond = isCond || strat == strat_ITE; - indent("sygus-unif", ind + 1); + SygusUnif::indent("sygus-unif", ind + 1); Trace("sygus-unif") << "Strategy : " << strat << ", from cons : " << etis->d_cons << std::endl; int cindex = Datatype::indexOf(etis->d_cons.toExpr()); @@ -1064,7 +996,7 @@ void CegConjecturePbe::staticLearnRedundantOps( } } }else{ - indent("sygus-unif", ind); + SygusUnif::indent("sygus-unif", ind); Trace("sygus-unif") << e << " :: node role : " << nrole << std::endl; } } @@ -1402,7 +1334,7 @@ bool CegConjecturePbe::getExplanationForEnumeratorExclude( { // we check invariance with respect to a negative contains test NegContainsSygusInvarianceTest ncset; - ncset.init(d_parent, x, itxo->second, cmp_indices); + ncset.init(x, d_examples[c], itxo->second, cmp_indices); // construct the generalized explanation d_tds->getExplain()->getExplanationFor(x, v, exp, ncset); Trace("sygus-pbe-cterm") @@ -1823,10 +1755,10 @@ Node CegConjecturePbe::constructSolution( TypeNode etn = e.getType(); if (Trace.isOn("sygus-pbe-dt-debug")) { - indent("sygus-pbe-dt-debug", ind); + SygusUnif::indent("sygus-pbe-dt-debug", ind); Trace("sygus-pbe-dt-debug") << "ConstructPBE: (" << e << ", " << nrole << ") for type " << etn << " in context "; - print_val("sygus-pbe-dt-debug", x.d_vals); + SygusUnif::print_val("sygus-pbe-dt-debug", x.d_vals); if (x.d_has_string_pos != role_invalid) { Trace("sygus-pbe-dt-debug") << ", string context [" << x.d_has_string_pos; @@ -1857,7 +1789,7 @@ Node CegConjecturePbe::constructSolution( { // this type has a complete solution ret_dt = einfo.getSolved(); - indent("sygus-pbe-dt", ind); + SygusUnif::indent("sygus-pbe-dt", ind); Trace("sygus-pbe-dt") << "return PBE: success : solved " << d_tds->sygusToBuiltin(ret_dt) << std::endl; Assert(!ret_dt.isNull()); @@ -1870,13 +1802,13 @@ Node CegConjecturePbe::constructSolution( if (!subsumed_by.empty()) { ret_dt = constructBestSolvedTerm(subsumed_by, x); - indent("sygus-pbe-dt", ind); + SygusUnif::indent("sygus-pbe-dt", ind); Trace("sygus-pbe-dt") << "return PBE: success : conditionally solved" << d_tds->sygusToBuiltin(ret_dt) << std::endl; } else { - indent("sygus-pbe-dt-debug", ind); + SygusUnif::indent("sygus-pbe-dt-debug", ind); Trace("sygus-pbe-dt-debug") << " ...not currently conditionally solved." << std::endl; } @@ -1924,13 +1856,13 @@ Node CegConjecturePbe::constructSolution( if (!str_solved.empty()) { ret_dt = constructBestStringSolvedTerm(str_solved, x); - indent("sygus-pbe-dt", ind); + SygusUnif::indent("sygus-pbe-dt", ind); Trace("sygus-pbe-dt") << "return PBE: success : string solved " << d_tds->sygusToBuiltin(ret_dt) << std::endl; } else { - indent("sygus-pbe-dt-debug", ind); + SygusUnif::indent("sygus-pbe-dt-debug", ind); Trace("sygus-pbe-dt-debug") << " ...not currently string solved." << std::endl; } @@ -1954,11 +1886,11 @@ Node CegConjecturePbe::constructSolution( x.getCurrentStrings(this, itx->second, ex_vals); if (Trace.isOn("sygus-pbe-dt-debug")) { - indent("sygus-pbe-dt-debug", ind); + SygusUnif::indent("sygus-pbe-dt-debug", ind); Trace("sygus-pbe-dt-debug") << "current strings : " << std::endl; for (unsigned i = 0, size = ex_vals.size(); i < size; i++) { - indent("sygus-pbe-dt-debug", ind + 1); + SygusUnif::indent("sygus-pbe-dt-debug", ind + 1); Trace("sygus-pbe-dt-debug") << ex_vals[i] << std::endl; } } @@ -1970,7 +1902,7 @@ Node CegConjecturePbe::constructSolution( for (unsigned i = 0, size = einfo.d_enum_vals.size(); i < size; i++) { Node val_t = einfo.d_enum_vals[i]; - indent("sygus-pbe-dt-debug", ind); + SygusUnif::indent("sygus-pbe-dt-debug", ind); Trace("sygus-pbe-dt-debug") << "increment string values : " << val_t << " : "; Assert(einfo.d_enum_vals_res[i].size() == itx->second.size()); @@ -1999,7 +1931,7 @@ Node CegConjecturePbe::constructSolution( { ret_dt = constructBestStringToConcat(inc_strs, total_inc, incr, x); Assert(!ret_dt.isNull()); - indent("sygus-pbe-dt", ind); + SygusUnif::indent("sygus-pbe-dt", ind); Trace("sygus-pbe-dt") << "PBE: CONCAT strategy : choose " << (isPrefix ? "pre" : "suf") << "fix value " << d_tds->sygusToBuiltin(ret_dt) << std::endl; @@ -2008,7 +1940,7 @@ Node CegConjecturePbe::constructSolution( AlwaysAssert(ret == (total_inc[ret_dt] > 0)); x.d_has_string_pos = nrole; }else{ - indent("sygus-pbe-dt", ind); + SygusUnif::indent("sygus-pbe-dt", ind); Trace("sygus-pbe-dt") << "PBE: failed CONCAT strategy, no values are " << (isPrefix ? "pre" : "suf") << "fix of all examples." << std::endl; @@ -2016,7 +1948,7 @@ Node CegConjecturePbe::constructSolution( } else { - indent("sygus-pbe-dt", ind); + SygusUnif::indent("sygus-pbe-dt", ind); Trace("sygus-pbe-dt") << "PBE: failed CONCAT strategy, prefix/suffix mismatch." << std::endl; @@ -2057,7 +1989,7 @@ Node CegConjecturePbe::constructSolution( if (etis != nullptr) { StrategyType strat = etis->d_this; - indent("sygus-pbe-dt", ind + 1); + SygusUnif::indent("sygus-pbe-dt", ind + 1); Trace("sygus-pbe-dt") << "...try STRATEGY " << strat << "..." << std::endl; @@ -2071,7 +2003,7 @@ Node CegConjecturePbe::constructSolution( for (unsigned sc = 0, size = etis->d_cenum.size(); sc < size; sc++) { - indent("sygus-pbe-dt", ind + 1); + SygusUnif::indent("sygus-pbe-dt", ind + 1); Trace("sygus-pbe-dt") << "construct PBE child #" << sc << "..." << std::endl; Node rec_c; @@ -2080,7 +2012,7 @@ Node CegConjecturePbe::constructSolution( if (itla != look_ahead_solved_children.end()) { rec_c = itla->second; - indent("sygus-pbe-dt-debug", ind + 1); + SygusUnif::indent("sygus-pbe-dt-debug", ind + 1); Trace("sygus-pbe-dt-debug") << "ConstructPBE: look ahead solved : " << d_tds->sygusToBuiltin(rec_c) << std::endl; @@ -2179,13 +2111,13 @@ Node CegConjecturePbe::constructSolution( { if (Trace.isOn("sygus-pbe-dt-debug")) { - indent("sygus-pbe-dt-debug", ind + 1); + SygusUnif::indent("sygus-pbe-dt-debug", ind + 1); Trace("sygus-pbe-dt-debug") << "PBE : We have " << itpc->second.size() << " distinguishable conditionals:" << std::endl; for (Node& cond : itpc->second) { - indent("sygus-pbe-dt-debug", ind + 2); + SygusUnif::indent("sygus-pbe-dt-debug", ind + 2); Trace("sygus-pbe-dt-debug") << d_tds->sygusToBuiltin(cond) << std::endl; } @@ -2216,7 +2148,7 @@ Node CegConjecturePbe::constructSolution( if (!solved_cond[n].empty()) { rec_c = constructBestSolvedConditional(solved_cond[n], x); - indent("sygus-pbe-dt", ind + 1); + SygusUnif::indent("sygus-pbe-dt", ind + 1); Trace("sygus-pbe-dt") << "PBE: ITE strategy : choose solved conditional " << d_tds->sygusToBuiltin(rec_c) << " with " << n @@ -2239,7 +2171,7 @@ Node CegConjecturePbe::constructSolution( { rec_c = constructBestConditional(itpc->second, x); Assert(!rec_c.isNull()); - indent("sygus-pbe-dt", ind); + SygusUnif::indent("sygus-pbe-dt", ind); Trace("sygus-pbe-dt") << "PBE: ITE strategy : choose random conditional " << d_tds->sygusToBuiltin(rec_c) << std::endl; @@ -2249,7 +2181,7 @@ Node CegConjecturePbe::constructSolution( { // TODO (#1250) : degenerate case where children have different // types? - indent("sygus-pbe-dt", ind); + SygusUnif::indent("sygus-pbe-dt", ind); Trace("sygus-pbe-dt") << "return PBE: failed ITE strategy, " "cannot find a distinguishable condition" << std::endl; @@ -2295,11 +2227,11 @@ Node CegConjecturePbe::constructSolution( etis->d_sol_templ_args.end(), dt_children_cons.begin(), dt_children_cons.end()); - indent("sygus-pbe-dt-debug", ind); + SygusUnif::indent("sygus-pbe-dt-debug", ind); Trace("sygus-pbe-dt-debug") << "PBE: success : constructed for strategy " << strat << std::endl; }else{ - indent("sygus-pbe-dt-debug", ind); + SygusUnif::indent("sygus-pbe-dt-debug", ind); Trace("sygus-pbe-dt-debug") << "PBE: failed for strategy " << strat << std::endl; } @@ -2309,7 +2241,7 @@ Node CegConjecturePbe::constructSolution( if( !ret_dt.isNull() ){ Assert( ret_dt.getType()==e.getType() ); } - indent("sygus-pbe-dt", ind); + SygusUnif::indent("sygus-pbe-dt", ind); Trace("sygus-pbe-dt") << "ConstructPBE: returned " << ret_dt << std::endl; return ret_dt; } diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index 38a170fbe..dd98dd0aa 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -19,75 +19,12 @@ #include "context/cdhashmap.h" #include "theory/quantifiers/sygus/sygus_module.h" +#include "theory/quantifiers/sygus/sygus_unif.h" namespace CVC4 { namespace theory { namespace quantifiers { -/** roles for enumerators - * - * This indicates the role of an enumerator that is allocated by approaches - * for synthesis-by-unification (see details below). - * io : the enumerator should enumerate values that are overall solutions - * for the function-to-synthesize, - * ite_condition : the enumerator should enumerate values that are useful - * in ite conditions in the ITE strategy, - * concat_term : the enumerator should enumerate values that are used as - * components of string concatenation solutions. - */ -enum EnumRole -{ - enum_invalid, - enum_io, - enum_ite_condition, - enum_concat_term, -}; -std::ostream& operator<<(std::ostream& os, EnumRole r); - -/** roles for strategy nodes - * - * This indicates the role of a strategy node, which is a subprocedure of - * CegConjecturePbe::constructSolution (see details below). - * equal : the node constructed must be equal to the overall solution for - * the function-to-synthesize, - * string_prefix/suffix : the node constructed must be a prefix/suffix - * of the function-to-synthesize, - * ite_condition : the node constructed must be a condition that makes some - * active input examples true and some input examples false. - */ -enum NodeRole -{ - role_invalid, - role_equal, - role_string_prefix, - role_string_suffix, - role_ite_condition, -}; -std::ostream& operator<<(std::ostream& os, NodeRole r); - -/** enumerator role for node role */ -EnumRole getEnumeratorRoleForNodeRole(NodeRole r); - -/** strategy types - * - * This indicates a strategy for synthesis-by-unification (see details below). - * ITE : strategy for constructing if-then-else solutions via decision - * tree learning techniques, - * CONCAT_PREFIX/SUFFIX : strategy for constructing string concatenation - * solutions via a divide and conquer approach, - * ID : identity strategy used for calling strategies on child type through - * an identity function. - */ -enum StrategyType -{ - strat_INVALID, - strat_ITE, - strat_CONCAT_PREFIX, - strat_CONCAT_SUFFIX, - strat_ID, -}; -std::ostream& operator<<(std::ostream& os, StrategyType st); - class CegConjecture; /** CegConjecturePbe diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp new file mode 100644 index 000000000..ee0590b6b --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -0,0 +1,2284 @@ +/********************* */ +/*! \file sygus_unif.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of sygus_unif + **/ + +#include "theory/quantifiers/sygus/sygus_unif.h" + +#include "theory/datatypes/datatypes_rewriter.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" +#include "theory/quantifiers/term_util.h" +#include "util/random.h" + +using namespace std; +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +std::ostream& operator<<(std::ostream& os, EnumRole r) +{ + switch (r) + { + case enum_invalid: os << "INVALID"; break; + case enum_io: os << "IO"; break; + case enum_ite_condition: os << "CONDITION"; break; + case enum_concat_term: os << "CTERM"; break; + default: os << "enum_" << static_cast(r); break; + } + return os; +} + +std::ostream& operator<<(std::ostream& os, NodeRole r) +{ + switch (r) + { + case role_equal: os << "equal"; break; + case role_string_prefix: os << "string_prefix"; break; + case role_string_suffix: os << "string_suffix"; break; + case role_ite_condition: os << "ite_condition"; break; + default: os << "role_" << static_cast(r); break; + } + return os; +} + +EnumRole getEnumeratorRoleForNodeRole(NodeRole r) +{ + switch (r) + { + case role_equal: return enum_io; break; + case role_string_prefix: return enum_concat_term; break; + case role_string_suffix: return enum_concat_term; break; + case role_ite_condition: return enum_ite_condition; break; + default: break; + } + return enum_invalid; +} + +std::ostream& operator<<(std::ostream& os, StrategyType st) +{ + switch (st) + { + case strat_ITE: os << "ITE"; break; + case strat_CONCAT_PREFIX: os << "CONCAT_PREFIX"; break; + case strat_CONCAT_SUFFIX: os << "CONCAT_SUFFIX"; break; + case strat_ID: os << "ID"; break; + default: os << "strat_" << static_cast(st); break; + } + return os; +} + +UnifContext::UnifContext() : d_has_string_pos(role_invalid) +{ + d_true = NodeManager::currentNM()->mkConst(true); + d_false = NodeManager::currentNM()->mkConst(false); +} + +bool UnifContext::updateContext(SygusUnif* pbe, + std::vector& vals, + bool pol) +{ + Assert(d_vals.size() == vals.size()); + bool changed = false; + Node poln = pol ? d_true : d_false; + for (unsigned i = 0; i < vals.size(); i++) + { + if (vals[i] != poln) + { + if (d_vals[i] == d_true) + { + d_vals[i] = d_false; + changed = true; + } + } + } + if (changed) + { + d_visit_role.clear(); + } + return changed; +} + +bool UnifContext::updateStringPosition(SygusUnif* pbe, + std::vector& pos) +{ + Assert(pos.size() == d_str_pos.size()); + bool changed = false; + for (unsigned i = 0; i < pos.size(); i++) + { + if (pos[i] > 0) + { + d_str_pos[i] += pos[i]; + changed = true; + } + } + if (changed) + { + d_visit_role.clear(); + } + return changed; +} + +bool UnifContext::isReturnValueModified() +{ + if (d_has_string_pos != role_invalid) + { + return true; + } + return false; +} + +void UnifContext::initialize(SygusUnif* pbe, Node c) +{ + Assert(d_vals.empty()); + Assert(d_str_pos.empty()); + + // initialize with #examples + Assert(pbe->d_examples.find(c) != pbe->d_examples.end()); + unsigned sz = pbe->d_examples[c].size(); + for (unsigned i = 0; i < sz; i++) + { + d_vals.push_back(d_true); + } + + if (!pbe->d_examples_out[c].empty()) + { + // output type of the examples + TypeNode exotn = pbe->d_examples_out[c][0].getType(); + + if (exotn.isString()) + { + for (unsigned i = 0; i < sz; i++) + { + d_str_pos.push_back(0); + } + } + } + d_visit_role.clear(); +} + +void UnifContext::getCurrentStrings(SygusUnif* pbe, + const std::vector& vals, + std::vector& ex_vals) +{ + bool isPrefix = d_has_string_pos == role_string_prefix; + String dummy; + for (unsigned i = 0; i < vals.size(); i++) + { + if (d_vals[i] == pbe->d_true) + { + Assert(vals[i].isConst()); + unsigned pos_value = d_str_pos[i]; + if (pos_value > 0) + { + Assert(d_has_string_pos != role_invalid); + String s = vals[i].getConst(); + Assert(pos_value <= s.size()); + ex_vals.push_back(isPrefix ? s.suffix(s.size() - pos_value) + : s.prefix(s.size() - pos_value)); + } + else + { + ex_vals.push_back(vals[i].getConst()); + } + } + else + { + // irrelevant, add dummy + ex_vals.push_back(dummy); + } + } +} + +bool UnifContext::getStringIncrement(SygusUnif* pbe, + bool isPrefix, + const std::vector& ex_vals, + const std::vector& vals, + std::vector& inc, + unsigned& tot) +{ + for (unsigned j = 0; j < vals.size(); j++) + { + unsigned ival = 0; + if (d_vals[j] == pbe->d_true) + { + // example is active in this context + Assert(vals[j].isConst()); + String mystr = vals[j].getConst(); + ival = mystr.size(); + if (mystr.size() <= ex_vals[j].size()) + { + if (!(isPrefix ? ex_vals[j].strncmp(mystr, ival) + : ex_vals[j].rstrncmp(mystr, ival))) + { + Trace("sygus-pbe-dt-debug") << "X"; + return false; + } + } + else + { + Trace("sygus-pbe-dt-debug") << "X"; + return false; + } + } + Trace("sygus-pbe-dt-debug") << ival; + tot += ival; + inc.push_back(ival); + } + return true; +} +bool UnifContext::isStringSolved(SygusUnif* pbe, + const std::vector& ex_vals, + const std::vector& vals) +{ + for (unsigned j = 0; j < vals.size(); j++) + { + if (d_vals[j] == pbe->d_true) + { + // example is active in this context + Assert(vals[j].isConst()); + String mystr = vals[j].getConst(); + if (ex_vals[j] != mystr) + { + return false; + } + } + } + return true; +} + +// status : 0 : exact, -1 : vals is subset, 1 : vals is superset +Node SubsumeTrie::addTermInternal(Node t, + const std::vector& vals, + bool pol, + std::vector& subsumed, + bool spol, + unsigned index, + int status, + bool checkExistsOnly, + bool checkSubsume) +{ + if (index == vals.size()) + { + if (status == 0) + { + // set the term if checkExistsOnly = false + if (d_term.isNull() && !checkExistsOnly) + { + d_term = t; + } + } + else if (status == 1) + { + Assert(checkSubsume); + // found a subsumed term + if (!d_term.isNull()) + { + subsumed.push_back(d_term); + if (!checkExistsOnly) + { + // remove it if checkExistsOnly = false + d_term = Node::null(); + } + } + } + else + { + Assert(!checkExistsOnly && checkSubsume); + } + return d_term; + } + NodeManager* nm = NodeManager::currentNM(); + // the current value + Assert(pol || (vals[index].isConst() && vals[index].getType().isBoolean())); + Node cv = pol ? vals[index] : nm->mkConst(!vals[index].getConst()); + // if checkExistsOnly = false, check if the current value is subsumed if + // checkSubsume = true, if so, don't add + if (!checkExistsOnly && checkSubsume) + { + Assert(cv.isConst() && cv.getType().isBoolean()); + std::vector check_subsumed_by; + if (status == 0) + { + if (!cv.getConst()) + { + check_subsumed_by.push_back(spol); + } + } + else if (status == -1) + { + check_subsumed_by.push_back(spol); + if (!cv.getConst()) + { + check_subsumed_by.push_back(!spol); + } + } + // check for subsumed nodes + for (unsigned i = 0, size = check_subsumed_by.size(); i < size; i++) + { + bool csbi = check_subsumed_by[i]; + Node csval = nm->mkConst(csbi); + // check if subsumed + std::map::iterator itc = d_children.find(csval); + if (itc != d_children.end()) + { + Node ret = itc->second.addTermInternal(t, + vals, + pol, + subsumed, + spol, + index + 1, + -1, + checkExistsOnly, + checkSubsume); + // ret subsumes t + if (!ret.isNull()) + { + return ret; + } + } + } + } + Node ret; + std::vector check_subsume; + if (status == 0) + { + if (checkExistsOnly) + { + std::map::iterator itc = d_children.find(cv); + if (itc != d_children.end()) + { + ret = itc->second.addTermInternal(t, + vals, + pol, + subsumed, + spol, + index + 1, + 0, + checkExistsOnly, + checkSubsume); + } + } + else + { + Assert(spol); + ret = d_children[cv].addTermInternal(t, + vals, + pol, + subsumed, + spol, + index + 1, + 0, + checkExistsOnly, + checkSubsume); + if (ret != t) + { + // we were subsumed by ret, return + return ret; + } + } + if (checkSubsume) + { + Assert(cv.isConst() && cv.getType().isBoolean()); + // check for subsuming + if (cv.getConst()) + { + check_subsume.push_back(!spol); + } + } + } + else if (status == 1) + { + Assert(checkSubsume); + Assert(cv.isConst() && cv.getType().isBoolean()); + check_subsume.push_back(!spol); + if (cv.getConst()) + { + check_subsume.push_back(spol); + } + } + if (checkSubsume) + { + // check for subsumed terms + for (unsigned i = 0, size = check_subsume.size(); i < size; i++) + { + Node csval = nm->mkConst(check_subsume[i]); + std::map::iterator itc = d_children.find(csval); + if (itc != d_children.end()) + { + itc->second.addTermInternal(t, + vals, + pol, + subsumed, + spol, + index + 1, + 1, + checkExistsOnly, + checkSubsume); + // clean up + if (itc->second.isEmpty()) + { + Assert(!checkExistsOnly); + d_children.erase(csval); + } + } + } + } + return ret; +} + +Node SubsumeTrie::addTerm(Node t, + const std::vector& vals, + bool pol, + std::vector& subsumed) +{ + return addTermInternal(t, vals, pol, subsumed, true, 0, 0, false, true); +} + +Node SubsumeTrie::addCond(Node c, const std::vector& vals, bool pol) +{ + std::vector subsumed; + return addTermInternal(c, vals, pol, subsumed, true, 0, 0, false, false); +} + +void SubsumeTrie::getSubsumed(const std::vector& vals, + bool pol, + std::vector& subsumed) +{ + addTermInternal(Node::null(), vals, pol, subsumed, true, 0, 1, true, true); +} + +void SubsumeTrie::getSubsumedBy(const std::vector& vals, + bool pol, + std::vector& subsumed_by) +{ + // flip polarities + addTermInternal( + Node::null(), vals, !pol, subsumed_by, false, 0, 1, true, true); +} + +void SubsumeTrie::getLeavesInternal(const std::vector& vals, + bool pol, + std::map >& v, + unsigned index, + int status) +{ + if (index == vals.size()) + { + Assert(!d_term.isNull()); + Assert(std::find(v[status].begin(), v[status].end(), d_term) + == v[status].end()); + v[status].push_back(d_term); + } + else + { + Assert(vals[index].isConst() && vals[index].getType().isBoolean()); + bool curr_val_true = vals[index].getConst() == pol; + for (std::map::iterator it = d_children.begin(); + it != d_children.end(); + ++it) + { + int new_status = status; + // if the current value is true + if (curr_val_true) + { + if (status != 0) + { + Assert(it->first.isConst() && it->first.getType().isBoolean()); + new_status = (it->first.getConst() ? 1 : -1); + if (status != -2 && new_status != status) + { + new_status = 0; + } + } + } + it->second.getLeavesInternal(vals, pol, v, index + 1, new_status); + } + } +} + +void SubsumeTrie::getLeaves(const std::vector& vals, + bool pol, + std::map >& v) +{ + getLeavesInternal(vals, pol, v, 0, -2); +} + +SygusUnif::SygusUnif(QuantifiersEngine* qe) : d_qe(qe) +{ + d_tds = qe->getTermDatabaseSygus(); + d_true = NodeManager::currentNM()->mkConst(true); + d_false = NodeManager::currentNM()->mkConst(false); +} + +SygusUnif::~SygusUnif() {} + +void SygusUnif::initialize(Node candidate, + std::vector& lemmas, + std::vector& enums) +{ + d_candidate = candidate; + // TODO +} + +void SygusUnif::resetExamples() +{ + // TODO +} + +void SygusUnif::addExample(const std::vector& input, Node output) +{ + // TODO +} + +void SygusUnif::notifyEnumeration(Node e, Node v, std::vector& lemmas) +{ + // TODO +} + +Node SygusUnif::constructSolution() +{ + Node c = d_candidate; + std::map::iterator itc = d_cinfo.find(c); + Assert(itc != d_cinfo.end()); + if (!itc->second.d_solution.isNull()) + { + // already has a solution + return itc->second.d_solution; + } + else + { + // only check if an enumerator updated + if (itc->second.d_check_sol) + { + Trace("sygus-pbe") << "Construct solution, #iterations = " + << itc->second.d_cond_count << std::endl; + itc->second.d_check_sol = false; + // try multiple times if we have done multiple conditions, due to + // non-determinism + Node vc; + for (unsigned i = 0; i <= itc->second.d_cond_count; i++) + { + Trace("sygus-pbe-dt") + << "ConstructPBE for candidate: " << c << std::endl; + Node e = itc->second.getRootEnumerator(); + UnifContext x; + x.initialize(this, c); + Node vcc = constructSolution(c, e, role_equal, x, 1); + if (!vcc.isNull()) + { + if (vc.isNull() || (!vc.isNull() + && d_tds->getSygusTermSize(vcc) + < d_tds->getSygusTermSize(vc))) + { + Trace("sygus-pbe") + << "**** PBE SOLVED : " << c << " = " << vcc << std::endl; + Trace("sygus-pbe") << "...solved at iteration " << i << std::endl; + vc = vcc; + } + } + } + if (!vc.isNull()) + { + itc->second.d_solution = vc; + return vc; + } + Trace("sygus-pbe") << "...failed to solve." << std::endl; + } + return Node::null(); + } +} + +// ----------------------------- establishing enumeration types + +void SygusUnif::registerEnumerator( + Node et, Node c, TypeNode tn, EnumRole enum_role, bool inSearch) +{ + if (d_einfo.find(et) == d_einfo.end()) + { + Trace("sygus-unif-debug") + << "...register " << et << " for " + << static_cast(tn.toType()).getDatatype().getName(); + Trace("sygus-unif-debug") << ", role = " << enum_role + << ", in search = " << inSearch << std::endl; + d_einfo[et].initialize(c, enum_role); + // if we are actually enumerating this (could be a compound node in the + // strategy) + if (inSearch) + { + std::map::iterator itn = + d_cinfo[c].d_search_enum.find(tn); + if (itn == d_cinfo[c].d_search_enum.end()) + { + // use this for the search + d_cinfo[c].d_search_enum[tn] = et; + d_cinfo[c].d_esym_list.push_back(et); + d_einfo[et].d_enum_slave.push_back(et); + } + else + { + Trace("sygus-unif-debug") + << "Make " << et << " a slave of " << itn->second << std::endl; + d_einfo[itn->second].d_enum_slave.push_back(et); + } + } + } +} + +void SygusUnif::collectEnumeratorTypes(Node e, TypeNode tn, NodeRole nrole) +{ + NodeManager* nm = NodeManager::currentNM(); + if (d_cinfo[e].d_tinfo.find(tn) == d_cinfo[e].d_tinfo.end()) + { + // register type + Trace("sygus-unif") << "Register enumerating type : " << tn << std::endl; + d_cinfo[e].initializeType(tn); + } + EnumTypeInfo& eti = d_cinfo[e].d_tinfo[tn]; + std::map::iterator itsn = eti.d_snodes.find(nrole); + if (itsn != eti.d_snodes.end()) + { + // already initialized + return; + } + StrategyNode& snode = eti.d_snodes[nrole]; + + // get the enumerator for this + EnumRole erole = getEnumeratorRoleForNodeRole(nrole); + + Node ee; + std::map::iterator iten = eti.d_enum.find(erole); + if (iten == eti.d_enum.end()) + { + ee = nm->mkSkolem("ee", tn); + eti.d_enum[erole] = ee; + Trace("sygus-unif-debug") + << "...enumerator " << ee << " for " + << static_cast(tn.toType()).getDatatype().getName() + << ", role = " << erole << std::endl; + } + else + { + ee = iten->second; + } + + // roles that we do not recurse on + if (nrole == role_ite_condition) + { + Trace("sygus-unif-debug") << "...this register (non-io)" << std::endl; + registerEnumerator(ee, e, tn, erole, true); + return; + } + + // look at information on how we will construct solutions for this type + Assert(tn.isDatatype()); + const Datatype& dt = static_cast(tn.toType()).getDatatype(); + Assert(dt.isSygus()); + + std::map > cop_to_strat; + std::map cop_to_cindex; + std::map > cop_to_child_templ; + std::map > cop_to_child_templ_arg; + std::map > cop_to_carg_list; + std::map > cop_to_child_types; + std::map > cop_to_sks; + + // whether we will enumerate the current type + bool search_this = false; + for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++) + { + Node cop = Node::fromExpr(dt[j].getConstructor()); + Node op = Node::fromExpr(dt[j].getSygusOp()); + Trace("sygus-unif-debug") << "--- Infer strategy from " << cop + << " with sygus op " << op << "..." << std::endl; + + // expand the evaluation to see if this constuctor induces a strategy + std::vector utchildren; + utchildren.push_back(cop); + std::vector sks; + std::vector sktns; + for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++) + { + Type t = dt[j][k].getRangeType(); + TypeNode ttn = TypeNode::fromType(t); + Node kv = nm->mkSkolem("ut", ttn); + sks.push_back(kv); + cop_to_sks[cop].push_back(kv); + sktns.push_back(ttn); + utchildren.push_back(kv); + } + Node ut = nm->mkNode(APPLY_CONSTRUCTOR, utchildren); + std::vector echildren; + echildren.push_back(Node::fromExpr(dt.getSygusEvaluationFunc())); + echildren.push_back(ut); + Node sbvl = Node::fromExpr(dt.getSygusVarList()); + for (const Node& sbv : sbvl) + { + echildren.push_back(sbv); + } + Node eut = nm->mkNode(APPLY_UF, echildren); + Trace("sygus-unif-debug2") + << " Test evaluation of " << eut << "..." << std::endl; + eut = d_qe->getTermDatabaseSygus()->unfold(eut); + Trace("sygus-unif-debug2") << " ...got " << eut; + Trace("sygus-unif-debug2") << ", type : " << eut.getType() << std::endl; + + // candidate strategy + if (eut.getKind() == ITE) + { + cop_to_strat[cop].push_back(strat_ITE); + } + else if (eut.getKind() == STRING_CONCAT) + { + if (nrole != role_string_suffix) + { + cop_to_strat[cop].push_back(strat_CONCAT_PREFIX); + } + if (nrole != role_string_prefix) + { + cop_to_strat[cop].push_back(strat_CONCAT_SUFFIX); + } + } + else if (dt[j].isSygusIdFunc()) + { + cop_to_strat[cop].push_back(strat_ID); + } + + // the kinds for which there is a strategy + if (cop_to_strat.find(cop) != cop_to_strat.end()) + { + // infer an injection from the arguments of the datatype + std::map templ_injection; + std::vector vs; + std::vector ss; + std::map templ_var_index; + for (unsigned k = 0, sksize = sks.size(); k < sksize; k++) + { + Assert(sks[k].getType().isDatatype()); + const Datatype& cdt = + static_cast(sks[k].getType().toType()).getDatatype(); + echildren[0] = Node::fromExpr(cdt.getSygusEvaluationFunc()); + echildren[1] = sks[k]; + Trace("sygus-unif-debug2") + << "...set eval dt to " << sks[k] << std::endl; + Node esk = nm->mkNode(APPLY_UF, echildren); + vs.push_back(esk); + Node tvar = nm->mkSkolem("templ", esk.getType()); + templ_var_index[tvar] = k; + Trace("sygus-unif-debug2") << "* template inference : looking for " + << tvar << " for arg " << k << std::endl; + ss.push_back(tvar); + Trace("sygus-unif-debug2") + << "* substitute : " << esk << " -> " << tvar << std::endl; + } + eut = eut.substitute(vs.begin(), vs.end(), ss.begin(), ss.end()); + Trace("sygus-unif-debug2") + << "Constructor " << j << ", base term is " << eut << std::endl; + std::map test_args; + if (dt[j].isSygusIdFunc()) + { + test_args[0] = eut; + } + else + { + for (unsigned k = 0, size = eut.getNumChildren(); k < size; k++) + { + test_args[k] = eut[k]; + } + } + + // TODO : prefix grouping prefix/suffix + bool isAssoc = TermUtil::isAssoc(eut.getKind()); + Trace("sygus-unif-debug2") + << eut.getKind() << " isAssoc = " << isAssoc << std::endl; + std::map > assoc_combine; + std::vector assoc_waiting; + int assoc_last_valid_index = -1; + for (std::pair& ta : test_args) + { + unsigned k = ta.first; + Node eut_c = ta.second; + // success if we can find a injection from args to sygus args + if (!inferTemplate(k, eut_c, templ_var_index, templ_injection)) + { + Trace("sygus-unif-debug") + << "...fail: could not find injection (range)." << std::endl; + cop_to_strat.erase(cop); + break; + } + std::map::iterator itti = templ_injection.find(k); + if (itti != templ_injection.end()) + { + // if associative, combine arguments if it is the same variable + if (isAssoc && assoc_last_valid_index >= 0 + && itti->second == templ_injection[assoc_last_valid_index]) + { + templ_injection.erase(k); + assoc_combine[assoc_last_valid_index].push_back(k); + } + else + { + assoc_last_valid_index = (int)k; + if (!assoc_waiting.empty()) + { + assoc_combine[k].insert(assoc_combine[k].end(), + assoc_waiting.begin(), + assoc_waiting.end()); + assoc_waiting.clear(); + } + assoc_combine[k].push_back(k); + } + } + else + { + // a ground argument + if (!isAssoc) + { + Trace("sygus-unif-debug") + << "...fail: could not find injection (functional)." + << std::endl; + cop_to_strat.erase(cop); + break; + } + else + { + if (assoc_last_valid_index >= 0) + { + assoc_combine[assoc_last_valid_index].push_back(k); + } + else + { + assoc_waiting.push_back(k); + } + } + } + } + if (cop_to_strat.find(cop) != cop_to_strat.end()) + { + // construct the templates + if (!assoc_waiting.empty()) + { + // could not find a way to fit some arguments into injection + cop_to_strat.erase(cop); + } + else + { + for (std::pair& ta : test_args) + { + unsigned k = ta.first; + Trace("sygus-unif-debug2") + << "- processing argument " << k << "..." << std::endl; + if (templ_injection.find(k) != templ_injection.end()) + { + unsigned sk_index = templ_injection[k]; + if (std::find(cop_to_carg_list[cop].begin(), + cop_to_carg_list[cop].end(), + sk_index) + == cop_to_carg_list[cop].end()) + { + cop_to_carg_list[cop].push_back(sk_index); + } + else + { + Trace("sygus-unif-debug") + << "...fail: duplicate argument used" << std::endl; + cop_to_strat.erase(cop); + break; + } + // also store the template information, if necessary + Node teut; + if (isAssoc) + { + std::vector& ac = assoc_combine[k]; + Assert(!ac.empty()); + std::vector children; + for (unsigned ack = 0, size_ac = ac.size(); ack < size_ac; + ack++) + { + children.push_back(eut[ac[ack]]); + } + teut = children.size() == 1 + ? children[0] + : nm->mkNode(eut.getKind(), children); + teut = Rewriter::rewrite(teut); + } + else + { + teut = ta.second; + } + + if (!teut.isVar()) + { + cop_to_child_templ[cop][k] = teut; + cop_to_child_templ_arg[cop][k] = ss[sk_index]; + Trace("sygus-unif-debug") + << " Arg " << k << " (template : " << teut << " arg " + << ss[sk_index] << "), index " << sk_index << std::endl; + } + else + { + Trace("sygus-unif-debug") + << " Arg " << k << ", index " << sk_index << std::endl; + Assert(teut == ss[sk_index]); + } + } + else + { + Assert(isAssoc); + } + } + } + } + } + if (cop_to_strat.find(cop) == cop_to_strat.end()) + { + Trace("sygus-unif") << "...constructor " << cop + << " does not correspond to a strategy." << std::endl; + search_this = true; + } + else + { + Trace("sygus-unif") << "-> constructor " << cop + << " matches strategy for " << eut.getKind() << "..." + << std::endl; + // collect children types + for (unsigned k = 0, size = cop_to_carg_list[cop].size(); k < size; k++) + { + TypeNode tn = sktns[cop_to_carg_list[cop][k]]; + Trace("sygus-unif-debug") + << " Child type " << k << " : " + << static_cast(tn.toType()).getDatatype().getName() + << std::endl; + cop_to_child_types[cop].push_back(tn); + } + } + } + + // check whether we should also enumerate the current type + Trace("sygus-unif-debug2") << " register this enumerator..." << std::endl; + registerEnumerator(ee, e, tn, erole, search_this); + + if (cop_to_strat.empty()) + { + Trace("sygus-unif") << "...consider " << dt.getName() << " a basic type" + << std::endl; + } + else + { + for (std::pair >& cstr : cop_to_strat) + { + Node cop = cstr.first; + Trace("sygus-unif-debug") + << "Constructor " << cop << " has " << cstr.second.size() + << " strategies..." << std::endl; + for (unsigned s = 0, ssize = cstr.second.size(); s < ssize; s++) + { + EnumTypeInfoStrat* cons_strat = new EnumTypeInfoStrat; + StrategyType strat = cstr.second[s]; + + cons_strat->d_this = strat; + cons_strat->d_cons = cop; + Trace("sygus-unif-debug") + << "Process strategy #" << s << " for operator : " << cop << " : " + << strat << std::endl; + Assert(cop_to_child_types.find(cop) != cop_to_child_types.end()); + std::vector& childTypes = cop_to_child_types[cop]; + Assert(cop_to_carg_list.find(cop) != cop_to_carg_list.end()); + std::vector& cargList = cop_to_carg_list[cop]; + + std::vector sol_templ_children; + sol_templ_children.resize(cop_to_sks[cop].size()); + + for (unsigned j = 0, csize = childTypes.size(); j < csize; j++) + { + // calculate if we should allocate a new enumerator : should be true + // if we have a new role + NodeRole nrole_c = nrole; + if (strat == strat_ITE) + { + if (j == 0) + { + nrole_c = role_ite_condition; + } + } + else if (strat == strat_CONCAT_PREFIX) + { + if ((j + 1) < childTypes.size()) + { + nrole_c = role_string_prefix; + } + } + else if (strat == strat_CONCAT_SUFFIX) + { + if (j > 0) + { + nrole_c = role_string_suffix; + } + } + // in all other cases, role is same as parent + + // register the child type + TypeNode ct = childTypes[j]; + Node csk = cop_to_sks[cop][cargList[j]]; + cons_strat->d_sol_templ_args.push_back(csk); + sol_templ_children[cargList[j]] = csk; + + EnumRole erole_c = getEnumeratorRoleForNodeRole(nrole_c); + // make the enumerator + Node et; + if (cop_to_child_templ[cop].find(j) != cop_to_child_templ[cop].end()) + { + // it is templated, allocate a fresh variable + et = nm->mkSkolem("et", ct); + Trace("sygus-unif-debug") + << "...enumerate " << et << " of type " + << ((DatatypeType)ct.toType()).getDatatype().getName(); + Trace("sygus-unif-debug") << " for arg " << j << " of " + << static_cast(tn.toType()) + .getDatatype() + .getName() + << std::endl; + registerEnumerator(et, e, ct, erole_c, true); + d_einfo[et].d_template = cop_to_child_templ[cop][j]; + d_einfo[et].d_template_arg = cop_to_child_templ_arg[cop][j]; + Assert(!d_einfo[et].d_template.isNull()); + Assert(!d_einfo[et].d_template_arg.isNull()); + } + else + { + Trace("sygus-unif-debug") + << "...child type enumerate " + << ((DatatypeType)ct.toType()).getDatatype().getName() + << ", node role = " << nrole_c << std::endl; + collectEnumeratorTypes(e, ct, nrole_c); + // otherwise use the previous + Assert(d_cinfo[e].d_tinfo[ct].d_enum.find(erole_c) + != d_cinfo[e].d_tinfo[ct].d_enum.end()); + et = d_cinfo[e].d_tinfo[ct].d_enum[erole_c]; + } + Trace("sygus-unif-debug") + << "Register child enumerator " << et << ", arg " << j << " of " + << cop << ", role = " << erole_c << std::endl; + Assert(!et.isNull()); + cons_strat->d_cenum.push_back(std::pair(et, nrole_c)); + } + // children that are unused in the strategy can be arbitrary + for (unsigned j = 0, stsize = sol_templ_children.size(); j < stsize; + j++) + { + if (sol_templ_children[j].isNull()) + { + sol_templ_children[j] = cop_to_sks[cop][j].getType().mkGroundTerm(); + } + } + sol_templ_children.insert(sol_templ_children.begin(), cop); + cons_strat->d_sol_templ = + nm->mkNode(APPLY_CONSTRUCTOR, sol_templ_children); + if (strat == strat_CONCAT_SUFFIX) + { + std::reverse(cons_strat->d_cenum.begin(), cons_strat->d_cenum.end()); + std::reverse(cons_strat->d_sol_templ_args.begin(), + cons_strat->d_sol_templ_args.end()); + } + if (Trace.isOn("sygus-unif")) + { + Trace("sygus-unif") << "Initialized strategy " << strat; + Trace("sygus-unif") + << " for " + << static_cast(tn.toType()).getDatatype().getName() + << ", operator " << cop; + Trace("sygus-unif") << ", #children = " << cons_strat->d_cenum.size() + << ", solution template = (lambda ( "; + for (const Node& targ : cons_strat->d_sol_templ_args) + { + Trace("sygus-unif") << targ << " "; + } + Trace("sygus-unif") << ") " << cons_strat->d_sol_templ << ")"; + Trace("sygus-unif") << std::endl; + } + // make the strategy + snode.d_strats.push_back(cons_strat); + } + } + } +} + +bool SygusUnif::inferTemplate(unsigned k, + Node n, + std::map& templ_var_index, + std::map& templ_injection) +{ + if (n.getNumChildren() == 0) + { + std::map::iterator itt = templ_var_index.find(n); + if (itt != templ_var_index.end()) + { + unsigned kk = itt->second; + std::map::iterator itti = templ_injection.find(k); + if (itti == templ_injection.end()) + { + Trace("sygus-unif-debug") + << "...set template injection " << k << " -> " << kk << std::endl; + templ_injection[k] = kk; + } + else if (itti->second != kk) + { + // two distinct variables in this term, we fail + return false; + } + } + return true; + } + else + { + for (unsigned i = 0; i < n.getNumChildren(); i++) + { + if (!inferTemplate(k, n[i], templ_var_index, templ_injection)) + { + return false; + } + } + } + return true; +} + +void SygusUnif::staticLearnRedundantOps(Node c, std::vector& lemmas) +{ + for (unsigned i = 0; i < d_cinfo[c].d_esym_list.size(); i++) + { + Node e = d_cinfo[c].d_esym_list[i]; + std::map::iterator itn = d_einfo.find(e); + Assert(itn != d_einfo.end()); + // see if there is anything we can eliminate + Trace("sygus-unif") + << "* Search enumerator #" << i << " : type " + << ((DatatypeType)e.getType().toType()).getDatatype().getName() + << " : "; + Trace("sygus-unif") << e << " has " << itn->second.d_enum_slave.size() + << " slaves:" << std::endl; + for (unsigned j = 0; j < itn->second.d_enum_slave.size(); j++) + { + Node es = itn->second.d_enum_slave[j]; + std::map::iterator itns = d_einfo.find(es); + Assert(itns != d_einfo.end()); + Trace("sygus-unif") << " " << es << ", role = " << itns->second.getRole() + << std::endl; + } + } + Trace("sygus-unif") << std::endl; + Trace("sygus-unif") << "Strategy for candidate " << c + << " is : " << std::endl; + std::map > visited; + std::map > needs_cons; + staticLearnRedundantOps(c, + d_cinfo[c].getRootEnumerator(), + role_equal, + visited, + needs_cons, + 0, + false); + // now, check the needs_cons map + for (std::pair >& nce : needs_cons) + { + Node em = nce.first; + const Datatype& dt = + static_cast(em.getType().toType()).getDatatype(); + for (std::pair& nc : nce.second) + { + Assert(nc.first < dt.getNumConstructors()); + if (!nc.second) + { + Node tst = + datatypes::DatatypesRewriter::mkTester(em, nc.first, dt).negate(); + if (std::find(lemmas.begin(), lemmas.end(), tst) == lemmas.end()) + { + Trace("sygus-unif") + << "...can exclude based on : " << tst << std::endl; + lemmas.push_back(tst); + } + } + } + } +} + +void SygusUnif::staticLearnRedundantOps( + Node c, + Node e, + NodeRole nrole, + std::map >& visited, + std::map >& needs_cons, + int ind, + bool isCond) +{ + std::map::iterator itn = d_einfo.find(e); + Assert(itn != d_einfo.end()); + + if (visited[e].find(nrole) == visited[e].end() + || (isCond && !itn->second.isConditional())) + { + visited[e][nrole] = true; + // if conditional + if (isCond) + { + itn->second.setConditional(); + } + indent("sygus-unif", ind); + Trace("sygus-unif") << e << " :: node role : " << nrole; + Trace("sygus-unif") + << ", type : " + << ((DatatypeType)e.getType().toType()).getDatatype().getName(); + if (isCond) + { + Trace("sygus-unif") << ", conditional"; + } + Trace("sygus-unif") << ", enum role : " << itn->second.getRole(); + + if (itn->second.isTemplated()) + { + Trace("sygus-unif") << ", templated : (lambda " + << itn->second.d_template_arg << " " + << itn->second.d_template << ")" << std::endl; + } + else + { + Trace("sygus-unif") << std::endl; + TypeNode etn = e.getType(); + + // enumerator type info + std::map::iterator itt = + d_cinfo[c].d_tinfo.find(etn); + Assert(itt != d_cinfo[c].d_tinfo.end()); + EnumTypeInfo& tinfo = itt->second; + + // strategy info + std::map::iterator itsn = + tinfo.d_snodes.find(nrole); + Assert(itsn != tinfo.d_snodes.end()); + StrategyNode& snode = itsn->second; + + if (snode.d_strats.empty()) + { + return; + } + std::map needs_cons_curr; + // various strategies + for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++) + { + EnumTypeInfoStrat* etis = snode.d_strats[j]; + StrategyType strat = etis->d_this; + bool newIsCond = isCond || strat == strat_ITE; + indent("sygus-unif", ind + 1); + Trace("sygus-unif") << "Strategy : " << strat + << ", from cons : " << etis->d_cons << std::endl; + int cindex = Datatype::indexOf(etis->d_cons.toExpr()); + Assert(cindex != -1); + needs_cons_curr[static_cast(cindex)] = false; + for (std::pair& cec : etis->d_cenum) + { + // recurse + staticLearnRedundantOps(c, + cec.first, + cec.second, + visited, + needs_cons, + ind + 2, + newIsCond); + } + } + // get the master enumerator for the type of this enumerator + std::map::iterator itse = + d_cinfo[c].d_search_enum.find(etn); + if (itse == d_cinfo[c].d_search_enum.end()) + { + return; + } + Node em = itse->second; + Assert(!em.isNull()); + // get the current datatype + const Datatype& dt = + static_cast(etn.toType()).getDatatype(); + // all constructors that are not a part of a strategy are needed + for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++) + { + if (needs_cons_curr.find(j) == needs_cons_curr.end()) + { + needs_cons_curr[j] = true; + } + } + // update the constructors that the master enumerator needs + if (needs_cons.find(em) == needs_cons.end()) + { + needs_cons[em] = needs_cons_curr; + } + else + { + for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++) + { + needs_cons[em][j] = needs_cons[em][j] || needs_cons_curr[j]; + } + } + } + } + else + { + indent("sygus-unif", ind); + Trace("sygus-unif") << e << " :: node role : " << nrole << std::endl; + } +} + +// ------------------------------------------- solution construction from +// enumeration + +void SygusUnif::addEnumeratedValue(Node x, Node v, std::vector& lems) +{ + std::map::iterator it = d_einfo.find(x); + Assert(it != d_einfo.end()); + Assert( + std::find(it->second.d_enum_vals.begin(), it->second.d_enum_vals.end(), v) + == it->second.d_enum_vals.end()); + Node c = it->second.d_parent_candidate; + // The explanation for why the current value should be excluded in future + // iterations. + Node exp_exc; + + std::map::iterator itc = d_cinfo.find(c); + Assert(itc != d_cinfo.end()); + TypeNode xtn = x.getType(); + Node bv = d_tds->sygusToBuiltin(v, xtn); + std::map > >::iterator itx = + d_examples.find(c); + std::map >::iterator itxo = d_examples_out.find(c); + Assert(itx != d_examples.end()); + Assert(itxo != d_examples_out.end()); + Assert(itx->second.size() == itxo->second.size()); + std::vector base_results; + // compte the results + for (unsigned j = 0, size = itx->second.size(); j < size; j++) + { + Node res = d_tds->evaluateBuiltin(xtn, bv, itx->second[j]); + Trace("sygus-pbe-enum-debug") + << "...got res = " << res << " from " << bv << std::endl; + base_results.push_back(res); + } + // is it excluded for domain-specific reason? + std::vector exp_exc_vec; + if (getExplanationForEnumeratorExclude( + c, x, v, base_results, it->second, exp_exc_vec)) + { + Assert(!exp_exc_vec.empty()); + exp_exc = exp_exc_vec.size() == 1 + ? exp_exc_vec[0] + : NodeManager::currentNM()->mkNode(AND, exp_exc_vec); + Trace("sygus-pbe-enum") + << " ...fail : term is excluded (domain-specific)" << std::endl; + } + else + { + // notify all slaves + Assert(!it->second.d_enum_slave.empty()); + // explanation for why this value should be excluded + for (unsigned s = 0; s < it->second.d_enum_slave.size(); s++) + { + Node xs = it->second.d_enum_slave[s]; + std::map::iterator itv = d_einfo.find(xs); + Assert(itv != d_einfo.end()); + Trace("sygus-pbe-enum") << "Process " << xs << " from " << s << std::endl; + // bool prevIsCover = false; + if (itv->second.getRole() == enum_io) + { + Trace("sygus-pbe-enum") << " IO-Eval of "; + // prevIsCover = itv->second.isFeasible(); + } + else + { + Trace("sygus-pbe-enum") << "Evaluation of "; + } + Trace("sygus-pbe-enum") << xs << " : "; + // evaluate all input/output examples + std::vector results; + Node templ = itv->second.d_template; + TNode templ_var = itv->second.d_template_arg; + std::map cond_vals; + for (unsigned j = 0, size = base_results.size(); j < size; j++) + { + Node res = base_results[j]; + Assert(res.isConst()); + if (!templ.isNull()) + { + TNode tres = res; + res = templ.substitute(templ_var, res); + res = Rewriter::rewrite(res); + Assert(res.isConst()); + } + Node resb; + if (itv->second.getRole() == enum_io) + { + Node out = itxo->second[j]; + Assert(out.isConst()); + resb = res == out ? d_true : d_false; + } + else + { + resb = res; + } + cond_vals[resb] = true; + results.push_back(resb); + if (Trace.isOn("sygus-pbe-enum")) + { + if (resb.getType().isBoolean()) + { + Trace("sygus-pbe-enum") << (resb == d_true ? "1" : "0"); + } + else + { + Trace("sygus-pbe-enum") << "?"; + } + } + } + bool keep = false; + if (itv->second.getRole() == enum_io) + { + // latter is the degenerate case of no examples + if (cond_vals.find(d_true) != cond_vals.end() || cond_vals.empty()) + { + // check subsumbed/subsuming + std::vector subsume; + if (cond_vals.find(d_false) == cond_vals.end()) + { + // it is the entire solution, we are done + Trace("sygus-pbe-enum") + << " ...success, full solution added to PBE pool : " + << d_tds->sygusToBuiltin(v) << std::endl; + if (!itv->second.isSolved()) + { + itv->second.setSolved(v); + // it subsumes everything + itv->second.d_term_trie.clear(); + itv->second.d_term_trie.addTerm(v, results, true, subsume); + } + keep = true; + } + else + { + Node val = + itv->second.d_term_trie.addTerm(v, results, true, subsume); + if (val == v) + { + Trace("sygus-pbe-enum") << " ...success"; + if (!subsume.empty()) + { + itv->second.d_enum_subsume.insert( + itv->second.d_enum_subsume.end(), + subsume.begin(), + subsume.end()); + Trace("sygus-pbe-enum") + << " and subsumed " << subsume.size() << " terms"; + } + Trace("sygus-pbe-enum") + << "! add to PBE pool : " << d_tds->sygusToBuiltin(v) + << std::endl; + keep = true; + } + else + { + Assert(subsume.empty()); + Trace("sygus-pbe-enum") << " ...fail : subsumed" << std::endl; + } + } + } + else + { + Trace("sygus-pbe-enum") + << " ...fail : it does not satisfy examples." << std::endl; + } + } + else + { + // must be unique up to examples + Node val = itv->second.d_term_trie.addCond(v, results, true); + if (val == v) + { + Trace("sygus-pbe-enum") << " ...success! add to PBE pool : " + << d_tds->sygusToBuiltin(v) << std::endl; + keep = true; + } + else + { + Trace("sygus-pbe-enum") + << " ...fail : term is not unique" << std::endl; + } + itc->second.d_cond_count++; + } + if (keep) + { + // notify the parent to retry the build of PBE + itc->second.d_check_sol = true; + itv->second.addEnumValue(this, v, results); + } + } + } + + // exclude this value on subsequent iterations + if (exp_exc.isNull()) + { + // if we did not already explain why this should be excluded, use default + exp_exc = d_tds->getExplain()->getExplanationForEquality(x, v); + } + exp_exc = exp_exc.negate(); + Trace("sygus-pbe-enum-lemma") + << "SygusUnif : enumeration exclude lemma : " << exp_exc << std::endl; + lems.push_back(exp_exc); +} + +bool SygusUnif::useStrContainsEnumeratorExclude(Node x, EnumInfo& ei) +{ + TypeNode xbt = d_tds->sygusToBuiltinType(x.getType()); + if (xbt.isString()) + { + std::map::iterator itx = d_use_str_contains_eexc.find(x); + if (itx != d_use_str_contains_eexc.end()) + { + return itx->second; + } + Trace("sygus-pbe-enum-debug") + << "Is " << x << " is str.contains exclusion?" << std::endl; + d_use_str_contains_eexc[x] = true; + for (const Node& sn : ei.d_enum_slave) + { + std::map::iterator itv = d_einfo.find(sn); + EnumRole er = itv->second.getRole(); + if (er != enum_io && er != enum_concat_term) + { + Trace("sygus-pbe-enum-debug") << " incompatible slave : " << sn + << ", role = " << er << std::endl; + d_use_str_contains_eexc[x] = false; + return false; + } + if (itv->second.isConditional()) + { + Trace("sygus-pbe-enum-debug") + << " conditional slave : " << sn << std::endl; + d_use_str_contains_eexc[x] = false; + return false; + } + } + Trace("sygus-pbe-enum-debug") + << "...can use str.contains exclusion." << std::endl; + return d_use_str_contains_eexc[x]; + } + return false; +} + +bool SygusUnif::getExplanationForEnumeratorExclude(Node c, + Node x, + Node v, + std::vector& results, + EnumInfo& ei, + std::vector& exp) +{ + if (useStrContainsEnumeratorExclude(x, ei)) + { + NodeManager* nm = NodeManager::currentNM(); + // This check whether the example evaluates to something that is larger than + // the output for some input/output pair. If so, then this term is never + // useful. We generalize its explanation below. + + if (Trace.isOn("sygus-pbe-cterm-debug")) + { + Trace("sygus-pbe-enum") << std::endl; + } + // check if all examples had longer length that the output + std::map >::iterator itxo = d_examples_out.find(c); + Assert(itxo != d_examples_out.end()); + Assert(itxo->second.size() == results.size()); + Trace("sygus-pbe-cterm-debug") + << "Check enumerator exclusion for " << x << " -> " + << d_tds->sygusToBuiltin(v) << " based on str.contains." << std::endl; + std::vector cmp_indices; + for (unsigned i = 0, size = results.size(); i < size; i++) + { + Assert(results[i].isConst()); + Assert(itxo->second[i].isConst()); + Trace("sygus-pbe-cterm-debug") + << " " << results[i] << " <> " << itxo->second[i]; + Node cont = nm->mkNode(STRING_STRCTN, itxo->second[i], results[i]); + Node contr = Rewriter::rewrite(cont); + if (contr == d_false) + { + cmp_indices.push_back(i); + Trace("sygus-pbe-cterm-debug") << "...not contained." << std::endl; + } + else + { + Trace("sygus-pbe-cterm-debug") << "...contained." << std::endl; + } + } + /* FIXME + if (!cmp_indices.empty()) + { + // we check invariance with respect to a negative contains test + NegContainsSygusInvarianceTest ncset; + ncset.init(d_parent, x, itxo->second, cmp_indices); + // construct the generalized explanation + d_tds->getExplain()->getExplanationFor(x, v, exp, ncset); + Trace("sygus-pbe-cterm") + << "PBE-cterm : enumerator exclude " << d_tds->sygusToBuiltin(v) + << " due to negative containment." << std::endl; + return true; + } + */ + } + return false; +} + +void SygusUnif::EnumInfo::addEnumValue(SygusUnif* pbe, + Node v, + std::vector& results) +{ + d_enum_val_to_index[v] = d_enum_vals.size(); + d_enum_vals.push_back(v); + d_enum_vals_res.push_back(results); +} + +void SygusUnif::EnumInfo::initialize(Node c, EnumRole role) +{ + d_parent_candidate = c; + d_role = role; +} + +void SygusUnif::EnumInfo::setSolved(Node slv) { d_enum_solved = slv; } + +void SygusUnif::CandidateInfo::initialize(Node c) +{ + d_this_candidate = c; + d_root = c.getType(); +} + +void SygusUnif::CandidateInfo::initializeType(TypeNode tn) +{ + d_tinfo[tn].d_this_type = tn; + d_tinfo[tn].d_parent = this; +} + +Node SygusUnif::CandidateInfo::getRootEnumerator() +{ + std::map::iterator it = d_tinfo[d_root].d_enum.find(enum_io); + Assert(it != d_tinfo[d_root].d_enum.end()); + return it->second; +} + +Node SygusUnif::constructBestSolvedTerm(std::vector& solved, + UnifContext& x) +{ + Assert(!solved.empty()); + return solved[0]; +} + +Node SygusUnif::constructBestStringSolvedTerm(std::vector& solved, + UnifContext& x) +{ + Assert(!solved.empty()); + return solved[0]; +} + +Node SygusUnif::constructBestSolvedConditional(std::vector& solved, + UnifContext& x) +{ + Assert(!solved.empty()); + return solved[0]; +} + +Node SygusUnif::constructBestConditional(std::vector& conds, + UnifContext& x) +{ + Assert(!conds.empty()); + double r = Random::getRandom().pickDouble(0.0, 1.0); + unsigned cindex = r * conds.size(); + if (cindex > conds.size()) + { + cindex = conds.size() - 1; + } + return conds[cindex]; +} + +Node SygusUnif::constructBestStringToConcat( + std::vector strs, + std::map total_inc, + std::map > incr, + UnifContext& x) +{ + Assert(!strs.empty()); + std::random_shuffle(strs.begin(), strs.end()); + // prefer one that has incremented by more than 0 + for (const Node& ns : strs) + { + if (total_inc[ns] > 0) + { + return ns; + } + } + return strs[0]; +} + +Node SygusUnif::constructSolution( + Node c, Node e, NodeRole nrole, UnifContext& x, int ind) +{ + TypeNode etn = e.getType(); + if (Trace.isOn("sygus-pbe-dt-debug")) + { + indent("sygus-pbe-dt-debug", ind); + Trace("sygus-pbe-dt-debug") << "ConstructPBE: (" << e << ", " << nrole + << ") for type " << etn << " in context "; + print_val("sygus-pbe-dt-debug", x.d_vals); + if (x.d_has_string_pos != role_invalid) + { + Trace("sygus-pbe-dt-debug") << ", string context [" << x.d_has_string_pos; + for (unsigned i = 0, size = x.d_str_pos.size(); i < size; i++) + { + Trace("sygus-pbe-dt-debug") << " " << x.d_str_pos[i]; + } + Trace("sygus-pbe-dt-debug") << "]"; + } + Trace("sygus-pbe-dt-debug") << std::endl; + } + // enumerator type info + std::map::iterator itt = d_cinfo[c].d_tinfo.find(etn); + Assert(itt != d_cinfo[c].d_tinfo.end()); + EnumTypeInfo& tinfo = itt->second; + + // get the enumerator information + std::map::iterator itn = d_einfo.find(e); + Assert(itn != d_einfo.end()); + EnumInfo& einfo = itn->second; + + Node ret_dt; + if (nrole == role_equal) + { + if (!x.isReturnValueModified()) + { + if (einfo.isSolved()) + { + // this type has a complete solution + ret_dt = einfo.getSolved(); + indent("sygus-pbe-dt", ind); + Trace("sygus-pbe-dt") << "return PBE: success : solved " + << d_tds->sygusToBuiltin(ret_dt) << std::endl; + Assert(!ret_dt.isNull()); + } + else + { + // could be conditionally solved + std::vector subsumed_by; + einfo.d_term_trie.getSubsumedBy(x.d_vals, true, subsumed_by); + if (!subsumed_by.empty()) + { + ret_dt = constructBestSolvedTerm(subsumed_by, x); + indent("sygus-pbe-dt", ind); + Trace("sygus-pbe-dt") << "return PBE: success : conditionally solved" + << d_tds->sygusToBuiltin(ret_dt) << std::endl; + } + else + { + indent("sygus-pbe-dt-debug", ind); + Trace("sygus-pbe-dt-debug") + << " ...not currently conditionally solved." << std::endl; + } + } + } + if (ret_dt.isNull()) + { + if (d_tds->sygusToBuiltinType(e.getType()).isString()) + { + // check if a current value that closes all examples + // get the term enumerator for this type + bool success = true; + std::map::iterator itet; + std::map::iterator itnt = + tinfo.d_enum.find(enum_concat_term); + if (itnt != itt->second.d_enum.end()) + { + Node et = itnt->second; + itet = d_einfo.find(et); + Assert(itet != d_einfo.end()); + } + else + { + success = false; + } + if (success) + { + // get the current examples + std::map >::iterator itx = + d_examples_out.find(c); + Assert(itx != d_examples_out.end()); + std::vector ex_vals; + x.getCurrentStrings(this, itx->second, ex_vals); + Assert(itn->second.d_enum_vals.size() + == itn->second.d_enum_vals_res.size()); + + // test each example in the term enumerator for the type + std::vector str_solved; + for (unsigned i = 0, size = itet->second.d_enum_vals.size(); i < size; + i++) + { + if (x.isStringSolved( + this, ex_vals, itet->second.d_enum_vals_res[i])) + { + str_solved.push_back(itet->second.d_enum_vals[i]); + } + } + if (!str_solved.empty()) + { + ret_dt = constructBestStringSolvedTerm(str_solved, x); + indent("sygus-pbe-dt", ind); + Trace("sygus-pbe-dt") << "return PBE: success : string solved " + << d_tds->sygusToBuiltin(ret_dt) << std::endl; + } + else + { + indent("sygus-pbe-dt-debug", ind); + Trace("sygus-pbe-dt-debug") + << " ...not currently string solved." << std::endl; + } + } + } + } + } + else if (nrole == role_string_prefix || nrole == role_string_suffix) + { + // check if each return value is a prefix/suffix of all open examples + if (!x.isReturnValueModified() || x.d_has_string_pos == nrole) + { + std::map > incr; + bool isPrefix = nrole == role_string_prefix; + std::map total_inc; + std::vector inc_strs; + std::map >::iterator itx = d_examples_out.find(c); + Assert(itx != d_examples_out.end()); + // make the value of the examples + std::vector ex_vals; + x.getCurrentStrings(this, itx->second, ex_vals); + if (Trace.isOn("sygus-pbe-dt-debug")) + { + indent("sygus-pbe-dt-debug", ind); + Trace("sygus-pbe-dt-debug") << "current strings : " << std::endl; + for (unsigned i = 0, size = ex_vals.size(); i < size; i++) + { + indent("sygus-pbe-dt-debug", ind + 1); + Trace("sygus-pbe-dt-debug") << ex_vals[i] << std::endl; + } + } + + // check if there is a value for which is a prefix/suffix of all active + // examples + Assert(einfo.d_enum_vals.size() == einfo.d_enum_vals_res.size()); + + for (unsigned i = 0, size = einfo.d_enum_vals.size(); i < size; i++) + { + Node val_t = einfo.d_enum_vals[i]; + indent("sygus-pbe-dt-debug", ind); + Trace("sygus-pbe-dt-debug") + << "increment string values : " << val_t << " : "; + Assert(einfo.d_enum_vals_res[i].size() == itx->second.size()); + unsigned tot = 0; + bool exsuccess = x.getStringIncrement(this, + isPrefix, + ex_vals, + einfo.d_enum_vals_res[i], + incr[val_t], + tot); + if (!exsuccess) + { + incr.erase(val_t); + Trace("sygus-pbe-dt-debug") << "...fail" << std::endl; + } + else + { + total_inc[val_t] = tot; + inc_strs.push_back(val_t); + Trace("sygus-pbe-dt-debug") + << "...success, total increment = " << tot << std::endl; + } + } + + if (!incr.empty()) + { + ret_dt = constructBestStringToConcat(inc_strs, total_inc, incr, x); + Assert(!ret_dt.isNull()); + indent("sygus-pbe-dt", ind); + Trace("sygus-pbe-dt") + << "PBE: CONCAT strategy : choose " << (isPrefix ? "pre" : "suf") + << "fix value " << d_tds->sygusToBuiltin(ret_dt) << std::endl; + // update the context + bool ret = x.updateStringPosition(this, incr[ret_dt]); + AlwaysAssert(ret == (total_inc[ret_dt] > 0)); + x.d_has_string_pos = nrole; + } + else + { + indent("sygus-pbe-dt", ind); + Trace("sygus-pbe-dt") << "PBE: failed CONCAT strategy, no values are " + << (isPrefix ? "pre" : "suf") + << "fix of all examples." << std::endl; + } + } + else + { + indent("sygus-pbe-dt", ind); + Trace("sygus-pbe-dt") + << "PBE: failed CONCAT strategy, prefix/suffix mismatch." + << std::endl; + } + } + if (ret_dt.isNull() && !einfo.isTemplated()) + { + // we will try a single strategy + EnumTypeInfoStrat* etis = nullptr; + std::map::iterator itsn = + tinfo.d_snodes.find(nrole); + if (itsn != tinfo.d_snodes.end()) + { + // strategy info + StrategyNode& snode = itsn->second; + if (x.d_visit_role[e].find(nrole) == x.d_visit_role[e].end()) + { + x.d_visit_role[e][nrole] = true; + // try a random strategy + if (snode.d_strats.size() > 1) + { + std::random_shuffle(snode.d_strats.begin(), snode.d_strats.end()); + } + // get an eligible strategy index + unsigned sindex = 0; + while (sindex < snode.d_strats.size() + && !snode.d_strats[sindex]->isValid(this, x)) + { + sindex++; + } + // if we found a eligible strategy + if (sindex < snode.d_strats.size()) + { + etis = snode.d_strats[sindex]; + } + } + } + if (etis != nullptr) + { + StrategyType strat = etis->d_this; + indent("sygus-pbe-dt", ind + 1); + Trace("sygus-pbe-dt") + << "...try STRATEGY " << strat << "..." << std::endl; + + std::map look_ahead_solved_children; + std::vector dt_children_cons; + bool success = true; + + // for ITE + Node split_cond_enum; + int split_cond_res_index = -1; + + for (unsigned sc = 0, size = etis->d_cenum.size(); sc < size; sc++) + { + indent("sygus-pbe-dt", ind + 1); + Trace("sygus-pbe-dt") + << "construct PBE child #" << sc << "..." << std::endl; + Node rec_c; + std::map::iterator itla = + look_ahead_solved_children.find(sc); + if (itla != look_ahead_solved_children.end()) + { + rec_c = itla->second; + indent("sygus-pbe-dt-debug", ind + 1); + Trace("sygus-pbe-dt-debug") + << "ConstructPBE: look ahead solved : " + << d_tds->sygusToBuiltin(rec_c) << std::endl; + } + else + { + std::pair& cenum = etis->d_cenum[sc]; + + // update the context + std::vector prev; + if (strat == strat_ITE && sc > 0) + { + std::map::iterator itnc = + d_einfo.find(split_cond_enum); + Assert(itnc != d_einfo.end()); + Assert(split_cond_res_index >= 0); + Assert(split_cond_res_index + < (int)itnc->second.d_enum_vals_res.size()); + prev = x.d_vals; + bool ret = x.updateContext( + this, + itnc->second.d_enum_vals_res[split_cond_res_index], + sc == 1); + AlwaysAssert(ret); + } + + // recurse + if (strat == strat_ITE && sc == 0) + { + Node ce = cenum.first; + + // register the condition enumerator + std::map::iterator itnc = d_einfo.find(ce); + Assert(itnc != d_einfo.end()); + EnumInfo& einfo_child = itnc->second; + + // only used if the return value is not modified + if (!x.isReturnValueModified()) + { + if (x.d_uinfo.find(ce) == x.d_uinfo.end()) + { + Trace("sygus-pbe-dt-debug2") + << " reg : PBE: Look for direct solutions for conditional " + "enumerator " + << ce << " ... " << std::endl; + Assert(einfo_child.d_enum_vals.size() + == einfo_child.d_enum_vals_res.size()); + for (unsigned i = 1; i <= 2; i++) + { + std::pair& te_pair = etis->d_cenum[i]; + Node te = te_pair.first; + std::map::iterator itnt = d_einfo.find(te); + Assert(itnt != d_einfo.end()); + bool branch_pol = (i == 1); + // for each condition, get terms that satisfy it in this + // branch + for (unsigned k = 0, size = einfo_child.d_enum_vals.size(); + k < size; + k++) + { + Node cond = einfo_child.d_enum_vals[k]; + std::vector solved; + itnt->second.d_term_trie.getSubsumedBy( + einfo_child.d_enum_vals_res[k], branch_pol, solved); + Trace("sygus-pbe-dt-debug2") + << " reg : PBE: " << d_tds->sygusToBuiltin(cond) + << " has " << solved.size() << " solutions in branch " + << i << std::endl; + if (!solved.empty()) + { + Node slv = constructBestSolvedTerm(solved, x); + Trace("sygus-pbe-dt-debug2") + << " reg : PBE: ..." << d_tds->sygusToBuiltin(slv) + << " is a solution under branch " << i; + Trace("sygus-pbe-dt-debug2") + << " of condition " << d_tds->sygusToBuiltin(cond) + << std::endl; + x.d_uinfo[ce].d_look_ahead_sols[cond][i] = slv; + } + } + } + } + } + + // get the conditionals in the current context : they must be + // distinguishable + std::map > possible_cond; + std::map solved_cond; // stores branch + einfo_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond); + + std::map >::iterator itpc = + possible_cond.find(0); + if (itpc != possible_cond.end()) + { + if (Trace.isOn("sygus-pbe-dt-debug")) + { + indent("sygus-pbe-dt-debug", ind + 1); + Trace("sygus-pbe-dt-debug") + << "PBE : We have " << itpc->second.size() + << " distinguishable conditionals:" << std::endl; + for (Node& cond : itpc->second) + { + indent("sygus-pbe-dt-debug", ind + 2); + Trace("sygus-pbe-dt-debug") + << d_tds->sygusToBuiltin(cond) << std::endl; + } + } + + // static look ahead conditional : choose conditionals that have + // solved terms in at least one branch + // only applicable if we have not modified the return value + std::map > solved_cond; + if (!x.isReturnValueModified()) + { + Assert(x.d_uinfo.find(ce) != x.d_uinfo.end()); + int solve_max = 0; + for (Node& cond : itpc->second) + { + std::map >::iterator itla = + x.d_uinfo[ce].d_look_ahead_sols.find(cond); + if (itla != x.d_uinfo[ce].d_look_ahead_sols.end()) + { + int nsolved = itla->second.size(); + solve_max = nsolved > solve_max ? nsolved : solve_max; + solved_cond[nsolved].push_back(cond); + } + } + int n = solve_max; + while (n > 0) + { + if (!solved_cond[n].empty()) + { + rec_c = constructBestSolvedConditional(solved_cond[n], x); + indent("sygus-pbe-dt", ind + 1); + Trace("sygus-pbe-dt") + << "PBE: ITE strategy : choose solved conditional " + << d_tds->sygusToBuiltin(rec_c) << " with " << n + << " solved children..." << std::endl; + std::map >::iterator itla = + x.d_uinfo[ce].d_look_ahead_sols.find(rec_c); + Assert(itla != x.d_uinfo[ce].d_look_ahead_sols.end()); + for (std::pair& las : itla->second) + { + look_ahead_solved_children[las.first] = las.second; + } + break; + } + n--; + } + } + + // otherwise, guess a conditional + if (rec_c.isNull()) + { + rec_c = constructBestConditional(itpc->second, x); + Assert(!rec_c.isNull()); + indent("sygus-pbe-dt", ind); + Trace("sygus-pbe-dt") + << "PBE: ITE strategy : choose random conditional " + << d_tds->sygusToBuiltin(rec_c) << std::endl; + } + } + else + { + // TODO (#1250) : degenerate case where children have different + // types? + indent("sygus-pbe-dt", ind); + Trace("sygus-pbe-dt") << "return PBE: failed ITE strategy, " + "cannot find a distinguishable condition" + << std::endl; + } + if (!rec_c.isNull()) + { + Assert(einfo_child.d_enum_val_to_index.find(rec_c) + != einfo_child.d_enum_val_to_index.end()); + split_cond_res_index = einfo_child.d_enum_val_to_index[rec_c]; + split_cond_enum = ce; + Assert(split_cond_res_index >= 0); + Assert(split_cond_res_index + < (int)einfo_child.d_enum_vals_res.size()); + } + } + else + { + rec_c = constructSolution(c, cenum.first, cenum.second, x, ind + 2); + } + + // undo update the context + if (strat == strat_ITE && sc > 0) + { + x.d_vals = prev; + } + } + if (!rec_c.isNull()) + { + dt_children_cons.push_back(rec_c); + } + else + { + success = false; + break; + } + } + if (success) + { + Assert(dt_children_cons.size() == etis->d_sol_templ_args.size()); + // ret_dt = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, + // dt_children ); + ret_dt = etis->d_sol_templ; + ret_dt = ret_dt.substitute(etis->d_sol_templ_args.begin(), + etis->d_sol_templ_args.end(), + dt_children_cons.begin(), + dt_children_cons.end()); + indent("sygus-pbe-dt-debug", ind); + Trace("sygus-pbe-dt-debug") + << "PBE: success : constructed for strategy " << strat << std::endl; + } + else + { + indent("sygus-pbe-dt-debug", ind); + Trace("sygus-pbe-dt-debug") + << "PBE: failed for strategy " << strat << std::endl; + } + } + } + + if (!ret_dt.isNull()) + { + Assert(ret_dt.getType() == e.getType()); + } + indent("sygus-pbe-dt", ind); + Trace("sygus-pbe-dt") << "ConstructPBE: returned " << ret_dt << std::endl; + return ret_dt; +} + +bool SygusUnif::EnumTypeInfoStrat::isValid(SygusUnif* pbe, UnifContext& x) +{ + if ((x.d_has_string_pos == role_string_prefix + && d_this == strat_CONCAT_SUFFIX) + || (x.d_has_string_pos == role_string_suffix + && d_this == strat_CONCAT_PREFIX)) + { + return false; + } + return true; +} + +SygusUnif::StrategyNode::~StrategyNode() +{ + for (unsigned j = 0, size = d_strats.size(); j < size; j++) + { + delete d_strats[j]; + } + d_strats.clear(); +} + +void SygusUnif::indent(const char* c, int ind) +{ + if (Trace.isOn(c)) + { + for (int i = 0; i < ind; i++) + { + Trace(c) << " "; + } + } +} + +void SygusUnif::print_val(const char* c, std::vector& vals, bool pol) +{ + if (Trace.isOn(c)) + { + for (unsigned i = 0; i < vals.size(); i++) + { + Trace(c) << ((pol ? vals[i].getConst() : !vals[i].getConst()) + ? "1" + : "0"); + } + } +} + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h new file mode 100644 index 000000000..68ed442a8 --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -0,0 +1,758 @@ +/********************* */ +/*! \file sygus_unif.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief sygus_unif + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H +#define __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H + +#include +#include "expr/node.h" +#include "theory/quantifiers_engine.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** roles for enumerators + * + * This indicates the role of an enumerator that is allocated by approaches + * for synthesis-by-unification (see details below). + * io : the enumerator should enumerate values that are overall solutions + * for the function-to-synthesize, + * ite_condition : the enumerator should enumerate values that are useful + * in ite conditions in the ITE strategy, + * concat_term : the enumerator should enumerate values that are used as + * components of string concatenation solutions. + */ +enum EnumRole +{ + enum_invalid, + enum_io, + enum_ite_condition, + enum_concat_term, +}; +std::ostream& operator<<(std::ostream& os, EnumRole r); + +/** roles for strategy nodes + * + * This indicates the role of a strategy node, which is a subprocedure of + * SygusUnif::constructSolution (see details below). + * equal : the node constructed must be equal to the overall solution for + * the function-to-synthesize, + * string_prefix/suffix : the node constructed must be a prefix/suffix + * of the function-to-synthesize, + * ite_condition : the node constructed must be a condition that makes some + * active input examples true and some input examples false. + */ +enum NodeRole +{ + role_invalid, + role_equal, + role_string_prefix, + role_string_suffix, + role_ite_condition, +}; +std::ostream& operator<<(std::ostream& os, NodeRole r); + +/** enumerator role for node role */ +EnumRole getEnumeratorRoleForNodeRole(NodeRole r); + +/** strategy types + * + * This indicates a strategy for synthesis-by-unification (see details below). + * ITE : strategy for constructing if-then-else solutions via decision + * tree learning techniques, + * CONCAT_PREFIX/SUFFIX : strategy for constructing string concatenation + * solutions via a divide and conquer approach, + * ID : identity strategy used for calling strategies on child type through + * an identity function. + */ +enum StrategyType +{ + strat_INVALID, + strat_ITE, + strat_CONCAT_PREFIX, + strat_CONCAT_SUFFIX, + strat_ID, +}; +std::ostream& operator<<(std::ostream& os, StrategyType st); + +class SygusUnif; + +/** Unification context + * + * This class maintains state information during calls to + * SygusUnif::constructSolution, which implements unification-based + * approaches for construction solutions to synthesis conjectures. + */ +class UnifContext +{ + public: + UnifContext(); + /** this intiializes this context for function-to-synthesize c */ + void initialize(SygusUnif* pbe, Node c); + + //----------for ITE strategy + /** the value of the context conditional + * + * This stores a list of Boolean constants that is the same length of the + * number of input/output example pairs we are considering. For each i, + * if d_vals[i] = true, i/o pair #i is active according to this context + * if d_vals[i] = false, i/o pair #i is inactive according to this context + */ + std::vector d_vals; + /** update the examples + * + * if pol=true, this method updates d_vals to d_vals & vals + * if pol=false, this method updates d_vals to d_vals & ( ~vals ) + */ + bool updateContext(SygusUnif* pbe, std::vector& vals, bool pol); + //----------end for ITE strategy + + //----------for CONCAT strategies + /** the position in the strings + * + * For each i/o example pair, this stores the length of the current solution + * for the input of the pair, where the solution for that input is a prefix + * or + * suffix of the output of the pair. For example, if our i/o pairs are: + * f( "abcd" ) = "abcdcd" + * f( "aa" ) = "aacd" + * If the solution we have currently constructed is str.++( x1, "c", ... ), + * then d_str_pos = ( 5, 3 ), where notice that + * str.++( "abc", "c" ) is a prefix of "abcdcd" and + * str.++( "aa", "c" ) is a prefix of "aacd". + */ + std::vector d_str_pos; + /** has string position + * + * Whether the solution positions indicate a prefix or suffix of the output + * examples. If this is role_invalid, then we have not updated the string + * position. + */ + NodeRole d_has_string_pos; + /** update the string examples + * + * This method updates d_str_pos to d_str_pos + pos. + */ + bool updateStringPosition(SygusUnif* pbe, std::vector& pos); + /** get current strings + * + * This returns the prefix/suffix of the string constants stored in vals + * of size d_str_pos, and stores the result in ex_vals. For example, if vals + * is (abcdcd", "aacde") and d_str_pos = ( 5, 3 ), then we add + * "d" and "de" to ex_vals. + */ + void getCurrentStrings(SygusUnif* pbe, + const std::vector& vals, + std::vector& ex_vals); + /** get string increment + * + * If this method returns true, then inc and tot are updated such that + * for all active indices i, + * vals[i] is a prefix (or suffix if isPrefix=false) of ex_vals[i], and + * inc[i] = str.len(vals[i]) + * for all inactive indices i, inc[i] = 0 + * We set tot to the sum of inc[i] for i=1,...,n. This indicates the total + * number of characters incremented across all examples. + */ + bool getStringIncrement(SygusUnif* pbe, + bool isPrefix, + const std::vector& ex_vals, + const std::vector& vals, + std::vector& inc, + unsigned& tot); + /** returns true if ex_vals[i] = vals[i] for all active indices i. */ + bool isStringSolved(SygusUnif* pbe, + const std::vector& ex_vals, + const std::vector& vals); + //----------end for CONCAT strategies + + /** is return value modified? + * + * This returns true if we are currently in a state where the return value + * of the solution has been modified, e.g. by a previous node that solved + * for a prefix. + */ + bool isReturnValueModified(); + /** visited role + * + * This is the current set of enumerator/node role pairs we are currently + * visiting. This set is cleared when the context is updated. + */ + std::map > d_visit_role; + + /** unif context enumerator information */ + class UEnumInfo + { + public: + UEnumInfo() {} + /** map from conditions and branch positions to a solved node + * + * For example, if we have: + * f( 1 ) = 2 ^ f( 3 ) = 4 ^ f( -1 ) = 1 + * Then, valid entries in this map is: + * d_look_ahead_sols[x>0][1] = x+1 + * d_look_ahead_sols[x>0][2] = 1 + * For the first entry, notice that for all input examples such that x>0 + * evaluates to true, which are (1) and (3), we have that their output + * values for x+1 under the substitution that maps x to the input value, + * resulting in 2 and 4, are equal to the output value for the respective + * pairs. + */ + std::map > d_look_ahead_sols; + }; + /** map from enumerators to the above info class */ + std::map d_uinfo; + + private: + /** true and false nodes */ + Node d_true; + Node d_false; +}; + +/** Subsumption trie +* +* This class manages a set of terms for a PBE sygus enumerator. +* +* In PBE sygus, we are interested in, for each term t, the set of I/O examples +* that it satisfies, which can be represented by a vector of Booleans. +* For example, given conjecture: +* f( 1 ) = 2 ^ f( 3 ) = 4 ^ f( -1 ) = 1 ^ f( 5 ) = 5 +* If solutions for f are of the form (lambda x. [term]), then: +* Term x satisfies 0001, +* Term x+1 satisfies 1100, +* Term 2 satisfies 0100. +* Above, term 2 is subsumed by term x+1, since the set of I/O examples that +* x+1 satisfies are a superset of those satisfied by 2. +*/ +class SubsumeTrie +{ + public: + SubsumeTrie() {} + /** + * Adds term t to the trie, removes all terms that are subsumed by t from the + * trie and adds them to subsumed. The set of I/O examples that t satisfies + * is given by (pol ? vals : !vals). + */ + Node addTerm(Node t, + const std::vector& vals, + bool pol, + std::vector& subsumed); + /** + * Adds term c to the trie, without calculating/updating based on + * subsumption. This is useful for using this class to store conditionals + * in ITE strategies, where any conditional whose set of vals is unique + * (as opposed to not subsumed) is useful. + */ + Node addCond(Node c, const std::vector& vals, bool pol); + /** + * Returns the set of terms that are subsumed by (pol ? vals : !vals). + */ + void getSubsumed(const std::vector& vals, + bool pol, + std::vector& subsumed); + /** + * Returns the set of terms that subsume (pol ? vals : !vals). This + * is for instance useful when determining whether there exists a term + * that satisfies all active examples in the decision tree learning + * algorithm. + */ + void getSubsumedBy(const std::vector& vals, + bool pol, + std::vector& subsumed_by); + /** + * Get the leaves of the trie, which we store in the map v. + * v[-1] stores the children that always evaluate to !pol, + * v[1] stores the children that always evaluate to pol, + * v[0] stores the children that both evaluate to true and false for at least + * one example. + */ + void getLeaves(const std::vector& vals, + bool pol, + std::map >& v); + /** is this trie empty? */ + bool isEmpty() { return d_term.isNull() && d_children.empty(); } + /** clear this trie */ + void clear() + { + d_term = Node::null(); + d_children.clear(); + } + + private: + /** the term at this node */ + Node d_term; + /** the children nodes of this trie */ + std::map d_children; + /** helper function for above functions */ + Node addTermInternal(Node t, + const std::vector& vals, + bool pol, + std::vector& subsumed, + bool spol, + unsigned index, + int status, + bool checkExistsOnly, + bool checkSubsume); + /** helper function for above functions */ + void getLeavesInternal(const std::vector& vals, + bool pol, + std::map >& v, + unsigned index, + int status); +}; + +/** Sygus unification utility + * + * This utility implements synthesis-by-unification style approaches for a + * single function to synthesize f. + * These approaches include a combination of: + * (1) Decision tree learning, inspired by Alur et al TACAS 2017, + * (2) Divide-and-conquer via string concatenation. + * + * This class maintains: + * (1) A "strategy tree" based on the syntactic restrictions for f that is + * constructed during initialize, + * (2) A set of input/output examples that are the specification for f. This + * can be updated via calls to resetExmaples/addExamples, + * (3) A set of terms that have been enumerated for enumerators. This can be + * updated via calls to notifyEnumeration. + * + * Based on the above, solutions can be constructed via calls to + * constructSolution. + */ +class SygusUnif +{ + friend class UnifContext; + + public: + SygusUnif(QuantifiersEngine* qe); + ~SygusUnif(); + + /** initialize + * + * This initializes this class with function-to-synthesize f. We also call + * f the candidate variable. + * + * This call constructs a set of enumerators for the relevant subfields of + * the grammar of f and adds them to enums. These enumerators are those that + * should be later given to calls to notifyEnumeration below. + * + * This also may result in lemmas being added to lemmas, + * which correspond to static symmetry breaking predicates (for example, + * those that exclude ITE from enumerators whose role is enum_io when the + * strategy is ITE_strat). + */ + void initialize(Node f, std::vector& enums, std::vector& lemmas); + /** reset examples + * + * Reset the specification for f. + * + * Notice that this does not reset the + */ + void resetExamples(); + /** add example + * + * This adds input -> output to the specification for f. The arity of + * input should be equal to the number of arguments in the sygus variable + * list of the grammar of f. That is, if we are searching for solutions for f + * of the form (lambda v1...vn. t), then the arity of input should be n. + */ + void addExample(const std::vector& input, Node output); + + /** + * Notify that the value v has been enumerated for enumerator e. This call + * will add lemmas L to lemmas such that L entails e^M != v for all future + * models M. + */ + void notifyEnumeration(Node e, Node v, std::vector& lemmas); + /** construct solution + * + * This attempts to construct a solution based on the current set of + * enumerated values. Returns null if it cannot (for example, if the + * set of enumerated values is insufficient, or if a non-deterministic + * strategy aborts). + */ + Node constructSolution(); + + //-----------------------debug printing + /** print ind indentations on trace c */ + static void indent(const char* c, int ind); + /** print (pol ? vals : !vals) as a bit-string on trace c */ + static void print_val(const char* c, + std::vector& vals, + bool pol = true); + //-----------------------end debug printing + private: + /** reference to quantifier engine */ + QuantifiersEngine* d_qe; + /** sygus term database of d_qe */ + quantifiers::TermDbSygus* d_tds; + /** true and false nodes */ + Node d_true; + Node d_false; + /** input of I/O examples */ + std::map > > d_examples; + /** output of I/O examples */ + std::map > d_examples_out; + + //------------------------------ representation of a enumeration strategy + /** + * This class stores information regarding an enumerator, including: + * - Information regarding the role of this enumerator (see EnumRole), its + * parent, whether it is templated, its slave enumerators, and so on, and + * - A database of values that have been enumerated for this enumerator. + * + * We say an enumerator is a master enumerator if it is the variable that + * we use to enumerate values for its sort. Master enumerators may have + * (possibly multiple) slave enumerators, stored in d_enum_slave. We make + * the first enumerator for each type a master enumerator, and any additional + * ones slaves of it. + */ + class EnumInfo + { + public: + EnumInfo() : d_role(enum_io), d_is_conditional(false) {} + /** initialize this class + * + * c is the parent function-to-synthesize + * role is the "role" the enumerator plays in the high-level strategy, + * which is one of enum_* above. + */ + void initialize(Node c, EnumRole role); + /** is this enumerator associated with a template? */ + bool isTemplated() { return !d_template.isNull(); } + /** set conditional + * + * This flag is set to true if this enumerator may not apply to all + * input/output examples. For example, if this enumerator is used + * as an output value beneath a conditional in an instance of strat_ITE, + * then this enumerator is conditional. + */ + void setConditional() { d_is_conditional = true; } + /** is conditional */ + bool isConditional() { return d_is_conditional; } + /** get the role of this enumerator */ + EnumRole getRole() { return d_role; } + /** + * The candidate variable that this enumerator is for (see sygus_pbe.h). + */ + Node d_parent_candidate; + /** enumerator template + * + * If d_template non-null, enumerated values V are immediately transformed to + * d_template { d_template_arg -> V }. + */ + Node d_template; + Node d_template_arg; + /** + * Slave enumerators of this enumerator. These are other enumerators that + * have the same type, but a different role in the strategy tree. We + * generally + * only use one enumerator per type, and hence these slaves are notified when + * values are enumerated for this enumerator. + */ + std::vector d_enum_slave; + + //---------------------------enumerated values + /** + * Notify this class that the term v has been enumerated for this enumerator. + * Its evaluation under the set of examples in pbe are stored in results. + */ + void addEnumValue(SygusUnif* pbe, Node v, std::vector& results); + /** + * Notify this class that slv is the complete solution to the synthesis + * conjecture. This occurs rarely, for instance, when during an ITE strategy + * we find that a single enumerated term covers all examples. + */ + void setSolved(Node slv); + /** Have we been notified that a complete solution exists? */ + bool isSolved() { return !d_enum_solved.isNull(); } + /** Get the complete solution to the synthesis conjecture. */ + Node getSolved() { return d_enum_solved; } + /** Values that have been enumerated for this enumerator */ + std::vector d_enum_vals; + /** + * This either stores the values of f( I ) for inputs + * or the value of f( I ) = O if d_role==enum_io + */ + std::vector > d_enum_vals_res; + /** + * The set of values in d_enum_vals that have been "subsumed" by others + * (see SubsumeTrie for explanation of subsumed). + */ + std::vector d_enum_subsume; + /** Map from values to their index in d_enum_vals. */ + std::map d_enum_val_to_index; + /** + * A subsumption trie containing the values in d_enum_vals. Depending on the + * role of this enumerator, values may either be added to d_term_trie with + * subsumption (if role=enum_io), or without (if role=enum_ite_condition or + * enum_concat_term). + */ + SubsumeTrie d_term_trie; + //---------------------------end enumerated values + private: + /** + * Whether an enumerated value for this conjecture has solved the entire + * conjecture. + */ + Node d_enum_solved; + /** the role of this enumerator (one of enum_* above). */ + EnumRole d_role; + /** is this enumerator conditional */ + bool d_is_conditional; + }; + /** maps enumerators to the information above */ + std::map d_einfo; + + class CandidateInfo; + class EnumTypeInfoStrat; + + /** represents a node in the strategy graph + * + * It contains a list of possible strategies which are tried during calls + * to constructSolution. + */ + class StrategyNode + { + public: + StrategyNode() {} + ~StrategyNode(); + /** the set of strategies to try at this node in the strategy graph */ + std::vector d_strats; + }; + + /** stores enumerators and strategies for a SyGuS datatype type */ + class EnumTypeInfo + { + public: + EnumTypeInfo() : d_parent(NULL) {} + /** the parent candidate info (see below) */ + CandidateInfo* d_parent; + /** the type that this information is for */ + TypeNode d_this_type; + /** map from enum roles to enumerators for this type */ + std::map d_enum; + /** map from node roles to strategy nodes */ + std::map d_snodes; + }; + + /** stores strategy and enumeration information for a function-to-synthesize + */ + class CandidateInfo + { + public: + CandidateInfo() : d_check_sol(false), d_cond_count(0) {} + Node d_this_candidate; + /** + * The root sygus datatype for the function-to-synthesize, + * which encodes the overall syntactic restrictions on the space + * of solutions. + */ + TypeNode d_root; + /** Info for sygus datatype type occurring in a field of d_root */ + std::map d_tinfo; + /** list of all enumerators for the function-to-synthesize */ + std::vector d_esym_list; + /** + * Maps sygus datatypes to their search enumerator. This is the (single) + * enumerator of that type that we enumerate values for. + */ + std::map d_search_enum; + bool d_check_sol; + unsigned d_cond_count; + Node d_solution; + void initialize(Node c); + void initializeType(TypeNode tn); + Node getRootEnumerator(); + }; + /** the candidate for this class */ + Node d_candidate; + /** maps a function-to-synthesize to the above information */ + std::map d_cinfo; + + //------------------------------ representation of an enumeration strategy + /** add enumerated value + * + * We have enumerated the value v for x. This function adds x->v to the + * relevant data structures that are used for strategy-specific construction + * of solutions when necessary, and returns a set of lemmas, which are added + * to the input argument lems. These lemmas are used to rule out models where + * x = v, to force that a new value is enumerated for x. + */ + void addEnumeratedValue(Node x, Node v, std::vector& lems); + /** domain-specific enumerator exclusion techniques + * + * Returns true if the value v for x can be excluded based on a + * domain-specific exclusion technique like the ones below. + * + * c : the candidate variable that x is enumerating for, + * results : the values of v under the input examples of c, + * ei : the enumerator information for x, + * exp : if this function returns true, then exp contains a (possibly + * generalize) explanation for why v can be excluded. + */ + bool getExplanationForEnumeratorExclude(Node c, + Node x, + Node v, + std::vector& results, + EnumInfo& ei, + std::vector& exp); + /** returns true if we can exlude values of x based on negative str.contains + * + * Values v for x may be excluded if we realize that the value of v under the + * substitution for some input example will never be contained in some output + * example. For details on this technique, see NegContainsSygusInvarianceTest + * in sygus_invariance.h. + * + * This function depends on whether x is being used to enumerate values + * for any node that is conditional in the strategy graph. For example, + * nodes that are children of ITE strategy nodes are conditional. If any node + * is conditional, then this function returns false. + */ + bool useStrContainsEnumeratorExclude(Node x, EnumInfo& ei); + /** cache for the above function */ + std::map d_use_str_contains_eexc; + + //------------------------------ strategy registration + /** collect enumerator types + * + * This builds the strategy for enumerated values of type tn for the given + * role of nrole, for solutions to function-to-synthesize c. + */ + void collectEnumeratorTypes(Node c, TypeNode tn, NodeRole nrole); + /** register enumerator + * + * This registers that et is an enumerator for function-to-synthesize c + * of type tn, having enumerator role enum_role. + * + * inSearch is whether we will enumerate values based on this enumerator. + * A strategy node is represented by a (enumerator, node role) pair. Hence, + * we may use enumerators for which this flag is false to represent strategy + * nodes that have child strategies. + */ + void registerEnumerator( + Node et, Node c, TypeNode tn, EnumRole enum_role, bool inSearch); + /** infer template */ + bool inferTemplate(unsigned k, + Node n, + std::map& templ_var_index, + std::map& templ_injection); + /** static learn redundant operators + * + * This learns static lemmas for pruning enumerative space based on the + * strategy for the function-to-synthesize c, and stores these into lemmas. + */ + void staticLearnRedundantOps(Node c, std::vector& lemmas); + /** helper for static learn redundant operators + * + * (e, nrole) specify the strategy node in the graph we are currently + * analyzing, visited stores the nodes we have already visited. + * + * This method builds the mapping needs_cons, which maps (master) enumerators + * to a map from the constructors that it needs. + * + * ind is the depth in the strategy graph we are at (for debugging). + * + * isCond is whether the current enumerator is conditional (beneath a + * conditional of an strat_ITE strategy). + */ + void staticLearnRedundantOps( + Node c, + Node e, + NodeRole nrole, + std::map >& visited, + std::map >& needs_cons, + int ind, + bool isCond); + //------------------------------ end strategy registration + + /** helper function for construct solution. + * + * Construct a solution based on enumerator e for function-to-synthesize c + * with node role nrole in context x. + * + * ind is the term depth of the context (for debugging). + */ + Node constructSolution( + Node c, Node e, NodeRole nrole, UnifContext& x, int ind); + /** Heuristically choose the best solved term from solved in context x, + * currently return the first. */ + Node constructBestSolvedTerm(std::vector& solved, UnifContext& x); + /** Heuristically choose the best solved string term from solved in context + * x, currently return the first. */ + Node constructBestStringSolvedTerm(std::vector& solved, UnifContext& x); + /** Heuristically choose the best solved conditional term from solved in + * context x, currently random */ + Node constructBestSolvedConditional(std::vector& solved, + UnifContext& x); + /** Heuristically choose the best conditional term from conds in context x, + * currently random */ + Node constructBestConditional(std::vector& conds, UnifContext& x); + /** Heuristically choose the best string to concatenate from strs to the + * solution in context x, currently random + * incr stores the vector of indices that are incremented by this solution in + * example outputs. + * total_inc[x] is the sum of incr[x] for each x in strs. + */ + Node constructBestStringToConcat(std::vector strs, + std::map total_inc, + std::map > incr, + UnifContext& x); + //------------------------------ end constructing solutions + + /** represents a strategy for a SyGuS datatype type + * + * This represents a possible strategy to apply when processing a strategy + * node in constructSolution. When applying the strategy represented by this + * class, we may make recursive calls to the children of the strategy, + * given in d_cenum. If all recursive calls to constructSolution for these + * children are successful, say: + * constructSolution( c, d_cenum[1], ... ) = t1, + * ..., + * constructSolution( c, d_cenum[n], ... ) = tn, + * Then, the solution returned by this strategy is + * d_sol_templ * { d_sol_templ_args -> (t1,...,tn) } + * where * is application of substitution. + */ + class EnumTypeInfoStrat + { + public: + /** the type of strategy this represents */ + StrategyType d_this; + /** the sygus datatype constructor that induced this strategy + * + * For example, this may be a sygus datatype whose sygus operator is ITE, + * if the strategy type above is strat_ITE. + */ + Node d_cons; + /** children of this strategy */ + std::vector > d_cenum; + /** the arguments for the (templated) solution */ + std::vector d_sol_templ_args; + /** the template for the solution */ + Node d_sol_templ; + /** Returns true if argument is valid strategy in context x */ + bool isValid(SygusUnif* pbe, UnifContext& x); + }; +}; + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ + +#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */ -- 2.30.2