#include "theory/quantifiers/term_util.h"
#include "util/random.h"
+#include <math.h>
+
using namespace CVC4::kind;
namespace CVC4 {
d_str_pos.clear();
d_curr_role = role_equal;
d_visit_role.clear();
- d_uinfo.clear();
// initialize with #examples
unsigned sz = sui->d_examples.size();
}
SygusUnifIo::SygusUnifIo()
- : d_check_sol(false), d_cond_count(0), d_sol_cons_nondet(false)
+ : d_check_sol(false),
+ d_cond_count(0),
+ d_sol_cons_nondet(false),
+ d_solConsUsingInfoGain(false)
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
Trace("sygus-pbe") << "Construct solution, #iterations = " << d_cond_count
<< std::endl;
d_check_sol = false;
+ d_solConsUsingInfoGain = false;
// try multiple times if we have done multiple conditions, due to
// non-determinism
unsigned sol_term_size = 0;
Trace("sygus-pbe") << "...solved at iteration " << i << std::endl;
d_solution = vcc;
sol_term_size = d_tds->getSygusTermSize(vcc);
+ // We've determined its feasible, now, enable information gain and
+ // retry. We do this since information gain comes with an overhead,
+ // and we want testing feasibility to be fast.
+ if (!d_solConsUsingInfoGain)
+ {
+ d_solConsUsingInfoGain = true;
+ i = 0;
+ }
}
else if (!d_sol_cons_nondet)
{
ecache.d_term_trie.getSubsumedBy(x.d_vals, true, subsumed_by);
if (!subsumed_by.empty())
{
- ret_dt = constructBestSolvedTerm(subsumed_by);
+ ret_dt = constructBestSolvedTerm(e, subsumed_by);
indent("sygus-sui-dt", ind);
Trace("sygus-sui-dt") << "return PBE: success : conditionally solved"
<< d_tds->sygusToBuiltin(ret_dt) << std::endl;
}
if (!str_solved.empty())
{
- ret_dt = constructBestStringSolvedTerm(str_solved);
+ ret_dt = constructBestSolvedTerm(e, str_solved);
indent("sygus-sui-dt", ind);
Trace("sygus-sui-dt") << "return PBE: success : string solved "
<< d_tds->sygusToBuiltin(ret_dt) << std::endl;
EnumCache& ecache_child = d_ecache[ce];
- // only used if the return value is not modified
- if (!x.isReturnValueModified())
- {
- if (x.d_uinfo.find(ce) == x.d_uinfo.end())
- {
- x.d_uinfo[ce].clear();
- Trace("sygus-sui-dt-debug2")
- << " reg : PBE: Look for direct solutions for conditional "
- "enumerator "
- << ce << " ... " << std::endl;
- Assert(ecache_child.d_enum_vals.size()
- == ecache_child.d_enum_vals_res.size());
- for (unsigned i = 1; i <= 2; i++)
- {
- std::pair<Node, NodeRole>& te_pair = etis->d_cenum[i];
- Node te = te_pair.first;
- EnumCache& ecache_te = d_ecache[te];
- bool branch_pol = (i == 1);
- // for each condition, get terms that satisfy it in this
- // branch
- for (unsigned k = 0, size = ecache_child.d_enum_vals.size();
- k < size;
- k++)
- {
- Node cond = ecache_child.d_enum_vals[k];
- std::vector<Node> solved;
- ecache_te.d_term_trie.getSubsumedBy(
- ecache_child.d_enum_vals_res[k], branch_pol, solved);
- Trace("sygus-sui-dt-debug2")
- << " reg : PBE: " << d_tds->sygusToBuiltin(cond)
- << " has " << solved.size() << " solutions in branch "
- << i << std::endl;
- if (!solved.empty())
- {
- Node slv = constructBestSolvedTerm(solved);
- Trace("sygus-sui-dt-debug2")
- << " reg : PBE: ..." << d_tds->sygusToBuiltin(slv)
- << " is a solution under branch " << i;
- Trace("sygus-sui-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<int, std::vector<Node> > possible_cond;
}
}
- // 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<int, std::vector<Node> > solved_cond;
- if (!x.isReturnValueModified() && !x.d_uinfo[ce].empty())
- {
- int solve_max = 0;
- for (Node& cond : itpc->second)
- {
- std::map<Node, std::map<unsigned, Node> >::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]);
- indent("sygus-sui-dt", ind + 1);
- Trace("sygus-sui-dt")
- << "PBE: ITE strategy : choose solved conditional "
- << d_tds->sygusToBuiltin(rec_c) << " with " << n
- << " solved children..." << std::endl;
- std::map<Node, std::map<unsigned, Node> >::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<const unsigned, Node>& 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);
+ rec_c = constructBestConditional(ce, itpc->second);
Assert(!rec_c.isNull());
indent("sygus-sui-dt", ind);
Trace("sygus-sui-dt")
- << "PBE: ITE strategy : choose random conditional "
+ << "PBE: ITE strategy : choose best conditional "
<< d_tds->sygusToBuiltin(rec_c) << std::endl;
}
}
return ret_dt;
}
+Node SygusUnifIo::constructBestConditional(Node ce,
+ const std::vector<Node>& conds)
+{
+ if (!d_solConsUsingInfoGain)
+ {
+ return SygusUnif::constructBestConditional(ce, conds);
+ }
+ UnifContextIo& x = d_context;
+ // use information gain heuristic
+ Trace("sygus-sui-dt-igain") << "Best information gain in context ";
+ print_val("sygus-sui-dt-igain", x.d_vals);
+ Trace("sygus-sui-dt-igain") << std::endl;
+ // set of indices that are active in this branch, i.e. x.d_vals[i] is true
+ std::vector<unsigned> activeIndices;
+ // map (j,t,s) -> n, such that the j^th condition in the vector conds
+ // evaluates to t (typically true/false) on n active I/O pairs with output s.
+ std::map<unsigned, std::map<Node, std::map<Node, unsigned>>> eval;
+ // map (j,t) -> m, such that the j^th condition in the vector conds
+ // evaluates to t (typically true/false) for m active I/O pairs.
+ std::map<unsigned, std::map<Node, unsigned>> evalCount;
+ unsigned nconds = conds.size();
+ EnumCache& ecache = d_ecache[ce];
+ // Get the index of conds[j] in the enumerator cache, this is to look up
+ // its evaluation on each point.
+ std::vector<unsigned> eindex;
+ for (unsigned j = 0; j < nconds; j++)
+ {
+ eindex.push_back(ecache.d_enum_val_to_index[conds[j]]);
+ }
+ unsigned activePoints = 0;
+ for (unsigned i = 0, npoints = x.d_vals.size(); i < npoints; i++)
+ {
+ if (x.d_vals[i].getConst<bool>())
+ {
+ activePoints++;
+ Node eo = d_examples_out[i];
+ for (unsigned j = 0; j < nconds; j++)
+ {
+ Node resn = ecache.d_enum_vals_res[eindex[j]][i];
+ Assert(resn.isConst());
+ eval[j][resn][eo]++;
+ evalCount[j][resn]++;
+ }
+ }
+ }
+ AlwaysAssert(activePoints > 0);
+ // find the condition that leads to the lowest entropy
+ // initially set minEntropy to > 1.0.
+ double minEntropy = 2.0;
+ unsigned bestIndex = 0;
+ for (unsigned j = 0; j < nconds; j++)
+ {
+ // To compute the entropy for a condition C, for pair of terms (s, t), let
+ // prob(t) be the probability C evaluates to t on an active point,
+ // prob(s|t) be the probability that an active point on which C
+ // evaluates to t has output s.
+ // Then, the entropy of C is:
+ // sum{t}. prob(t)*( sum{s}. -prob(s|t)*log2(prob(s|t)) )
+ // where notice this is always between 0 and 1.
+ double entropySum = 0.0;
+ Trace("sygus-sui-dt-igain") << j << " : ";
+ for (std::pair<const Node, std::map<Node, unsigned>>& ej : eval[j])
+ {
+ unsigned ecount = evalCount[j][ej.first];
+ if (ecount > 0)
+ {
+ double probBranch = double(ecount) / double(activePoints);
+ Trace("sygus-sui-dt-igain") << ej.first << " -> ( ";
+ for (std::pair<const Node, unsigned>& eej : ej.second)
+ {
+ if (eej.second > 0)
+ {
+ double probVal = double(eej.second) / double(ecount);
+ Trace("sygus-sui-dt-igain")
+ << eej.first << ":" << eej.second << " ";
+ double factor = -probVal * log2(probVal);
+ entropySum += probBranch * factor;
+ }
+ }
+ Trace("sygus-sui-dt-igain") << ") ";
+ }
+ }
+ Trace("sygus-sui-dt-igain") << "..." << entropySum << std::endl;
+ if (entropySum < minEntropy)
+ {
+ minEntropy = entropySum;
+ bestIndex = j;
+ }
+ }
+
+ Assert(!conds.empty());
+ return conds[bestIndex];
+}
+
} /* CVC4::theory::quantifiers namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
*/
std::map<Node, std::map<NodeRole, bool>> 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<Node, std::map<unsigned, Node>> d_look_ahead_sols;
- /** clear */
- void clear() { d_look_ahead_sols.clear(); }
- /** is empty */
- bool empty() { return d_look_ahead_sols.empty(); }
- };
- /** map from enumerators to the above info class */
- std::map<Node, UEnumInfo> d_uinfo;
-
private:
/** true and false nodes */
Node d_true;
* which can be closed with "B", giving us (x ++ "B") as a solution.
*/
bool d_sol_cons_nondet;
+ /**
+ * Whether we are using information gain heuristic during solution
+ * construction.
+ */
+ bool d_solConsUsingInfoGain;
/** true and false nodes */
Node d_true;
Node d_false;
NodeRole nrole,
int ind,
std::vector<Node>& lemmas) override;
+ /** construct best conditional
+ *
+ * This returns the condition in conds that maximizes information gain with
+ * respect to the current active points in d_context. For example, see
+ * Alur et al. TACAS 2017 for an example of information gain.
+ */
+ Node constructBestConditional(Node ce,
+ const std::vector<Node>& conds) override;
};
} /* CVC4::theory::quantifiers namespace */
projects / cvc5.git / commitdiff