From: Haniel Barbosa Date: Thu, 13 Sep 2018 20:06:50 +0000 (-0500) Subject: Uses information gain heuristic for building better solutions from DTs (#2451) X-Git-Tag: cvc5-1.0.0~4652 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6ac8972a11047d0d858055ea89aa2acf15e2cfa7;p=cvc5.git Uses information gain heuristic for building better solutions from DTs (#2451) --- diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 01cf41518..a4fca6d3c 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -983,6 +983,14 @@ header = "options/quantifiers_options.h" default = "false" help = "Synthesize conditions indepedently from return values (may generate bigger solutions)" +[[option]] + name = "sygusUnifBooleanHeuristicDt" + category = "regular" + long = "sygus-unif-boolean-heuristic-dt" + type = "bool" + default = "false" + help = "Build boolean solutions using heuristic decision tree learning (generates smaller solutions)" + [[option]] name = "sygusUnifCondIndNoRepeatSol" category = "regular" diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 1245cba1f..19b0ad717 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -435,7 +435,8 @@ void CegisUnifEnumManager::setUpEnumerator(Node e, si.d_enums[index].push_back(e); Trace("cegis-unif-enum") << "* Registering new enumerator " << e << " to strategy point " << si.d_pt << "\n"; - d_tds->registerEnumerator(e, si.d_pt, d_parent); + d_tds->registerEnumerator( + e, si.d_pt, d_parent, options::sygusUnifCondIndependent() && index == 1); } void CegisUnifEnumManager::registerEvalPts(const std::vector& eis, Node e) diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index 51b14f3e1..66639b750 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -21,6 +21,8 @@ #include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "theory/quantifiers/sygus/term_database_sygus.h" +#include + using namespace CVC4::kind; namespace CVC4 { @@ -104,14 +106,14 @@ Node SygusUnifRl::purifyLemma(Node n, TNode cand = n[0]; Node tmp = n.substitute(cand, it->second); nv = d_tds->evaluateWithUnfolding(tmp); - Trace("sygus-unif-rl-purify") << "PurifyLemma : model value for " << tmp - << " is " << nv << "\n"; + Trace("sygus-unif-rl-purify") + << "PurifyLemma : model value for " << tmp << " is " << nv << "\n"; } else { nv = d_parent->getModelValue(n); - Trace("sygus-unif-rl-purify") << "PurifyLemma : model value for " << n - << " is " << nv << "\n"; + Trace("sygus-unif-rl-purify") + << "PurifyLemma : model value for " << n << " is " << nv << "\n"; } Assert(n != nv); } @@ -138,8 +140,8 @@ Node SygusUnifRl::purifyLemma(Node n, { if (n.getMetaKind() == metakind::PARAMETERIZED) { - Trace("sygus-unif-rl-purify-debug") << "Node " << n - << " is parameterized\n"; + Trace("sygus-unif-rl-purify-debug") + << "Node " << n << " is parameterized\n"; children.insert(children.begin(), n.getOperator()); } if (Trace.isOn("sygus-unif-rl-purify-debug")) @@ -152,8 +154,8 @@ Node SygusUnifRl::purifyLemma(Node n, } } nb = NodeManager::currentNM()->mkNode(k, children); - Trace("sygus-unif-rl-purify") << "PurifyLemma : transformed " << n - << " into " << nb << "\n"; + Trace("sygus-unif-rl-purify") + << "PurifyLemma : transformed " << n << " into " << nb << "\n"; } else { @@ -174,8 +176,8 @@ Node SygusUnifRl::purifyLemma(Node n, "head of unif evaluation point", NodeManager::SKOLEM_EXACT_NAME); // Adds new enumerator to map from candidate - Trace("sygus-unif-rl-purify") << "...new enum " << new_f - << " for candidate " << nb[0] << "\n"; + Trace("sygus-unif-rl-purify") + << "...new enum " << new_f << " for candidate " << nb[0] << "\n"; d_cand_to_eval_hds[nb[0]].push_back(new_f); // Maps new enumerator to its respective tuple of arguments d_hd_to_pt[new_f] = @@ -192,8 +194,8 @@ Node SygusUnifRl::purifyLemma(Node n, // replace first child and rebulid node Assert(children.size() > 0); children[0] = new_f; - Trace("sygus-unif-rl-purify-debug") << "Make sygus eval app " << children - << std::endl; + Trace("sygus-unif-rl-purify-debug") + << "Make sygus eval app " << children << std::endl; np = nm->mkNode(DT_SYGUS_EVAL, children); d_app_to_purified[nb] = np; } @@ -212,15 +214,15 @@ Node SygusUnifRl::purifyLemma(Node n, model_guards.push_back( NodeManager::currentNM()->mkNode(EQUAL, nv, nb).negate()); nb = nv; - Trace("sygus-unif-rl-purify") << "PurifyLemma : adding model eq " - << model_guards.back() << "\n"; + Trace("sygus-unif-rl-purify") + << "PurifyLemma : adding model eq " << model_guards.back() << "\n"; } nb = Rewriter::rewrite(nb); // every non-top level application of function-to-synthesize must be reduced // to a concrete constant Assert(!ensureConst || nb.isConst()); - Trace("sygus-unif-rl-purify-debug") << "... caching [" << n << "] = " << nb - << "\n"; + Trace("sygus-unif-rl-purify-debug") + << "... caching [" << n << "] = " << nb << "\n"; cache[BoolNodePair(ensureConst, n)] = nb; return nb; } @@ -228,8 +230,8 @@ Node SygusUnifRl::purifyLemma(Node n, Node SygusUnifRl::addRefLemma(Node lemma, std::map>& eval_hds) { - Trace("sygus-unif-rl-purify") << "Registering lemma at SygusUnif : " << lemma - << "\n"; + Trace("sygus-unif-rl-purify") + << "Registering lemma at SygusUnif : " << lemma << "\n"; std::vector model_guards; BoolNodePairMap cache; // cache previous sizes @@ -270,9 +272,9 @@ Node SygusUnifRl::addRefLemma(Node lemma, for (const Node& stratpt : d_cenum_to_stratpt[cenum]) { Assert(d_stratpt_to_dt.find(stratpt) != d_stratpt_to_dt.end()); - Trace("sygus-unif-rl-dt") << "Register point with head " - << cp.second[j] << " to strategy point " - << stratpt << "\n"; + Trace("sygus-unif-rl-dt") + << "Register point with head " << cp.second[j] + << " to strategy point " << stratpt << "\n"; // Register new point from new head d_stratpt_to_dt[stratpt].d_hds.push_back(cp.second[j]); } @@ -390,8 +392,8 @@ void SygusUnifRl::registerStrategy( { if (Trace.isOn("sygus-unif-rl-strat")) { - Trace("sygus-unif-rl-strat") << "Strategy for " << f - << " is : " << std::endl; + Trace("sygus-unif-rl-strat") + << "Strategy for " << f << " is : " << std::endl; d_strategy[f].debugPrint("sygus-unif-rl-strat"); } Trace("sygus-unif-rl-strat") << "Register..." << std::endl; @@ -491,6 +493,8 @@ void SygusUnifRl::DecisionTreeInfo::initialize(Node cond_enum, d_unif = unif; d_strategy = strategy; d_strategy_index = strategy_index; + d_true = NodeManager::currentNM()->mkConst(true); + d_false = NodeManager::currentNM()->mkConst(false); // Retrieve template EnumInfo& eiv = d_strategy->getEnumInfo(d_cond_enum); d_template = NodePair(eiv.d_template, eiv.d_template_arg); @@ -513,9 +517,9 @@ void SygusUnifRl::DecisionTreeInfo::setConditions( // add to condition pool if (options::sygusUnifCondIndependent()) { + d_cond_mvs.insert(conds.begin(), conds.end()); if (Trace.isOn("sygus-unif-cond-pool")) { - d_cond_mvs.insert(conds.begin(), conds.end()); for (const Node& condv : conds) { if (d_cond_mvs.find(condv) == d_cond_mvs.end()) @@ -545,7 +549,8 @@ Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons, Trace("sygus-unif-sol") << "Decision::buildSol with " << d_hds.size() << " evaluation heads and " << d_conds.size() << " conditions..." << std::endl; - + // reset the trie + d_pt_sep.d_trie.clear(); return options::sygusUnifCondIndependent() ? buildSolAllCond(cons, lemmas) : buildSolMinCond(cons, lemmas); } @@ -587,7 +592,7 @@ Node SygusUnifRl::DecisionTreeInfo::buildSolAllCond(Node cons, return Node::null(); } Trace("sygus-unif-sol") << "...ready to build solution from DT\n"; - Node sol = d_pt_sep.extractSol(cons, hd_mv); + Node sol = extractSol(cons, hd_mv); // repeated solution if (options::sygusUnifCondIndNoRepeatSol() && d_sols.find(sol) != d_sols.end()) @@ -604,8 +609,6 @@ Node SygusUnifRl::DecisionTreeInfo::buildSolMinCond(Node cons, NodeManager* nm = NodeManager::currentNM(); // model values for evaluation heads std::map hd_mv; - // reset the trie - d_pt_sep.d_trie.clear(); // the current explanation of why there has not yet been a separation conflict std::vector exp; // is the above explanation ready to be sent out as a lemma? @@ -818,6 +821,17 @@ Node SygusUnifRl::DecisionTreeInfo::buildSolMinCond(Node cons, } Trace("sygus-unif-sol") << "...ready to build solution from DT\n"; + return extractSol(cons, hd_mv); +} + +Node SygusUnifRl::DecisionTreeInfo::extractSol(Node cons, + std::map& hd_mv) +{ + // rebuild decision tree using heuristic learning + if (options::sygusUnifBooleanHeuristicDt()) + { + recomputeSolHeuristically(hd_mv); + } return d_pt_sep.extractSol(cons, hd_mv); } @@ -902,6 +916,153 @@ Node SygusUnifRl::DecisionTreeInfo::PointSeparator::extractSol( return cache[root]; } +void SygusUnifRl::DecisionTreeInfo::recomputeSolHeuristically( + std::map& hd_mv) +{ + // reset the trie + d_pt_sep.d_trie.clear(); + // TODO workaround and not really sure this is the last condition, since I put + // a set here. Maybe make d_cond_mvs into a vector + Node backup_last_cond = d_conds.back(); + d_conds.clear(); + for (const Node& e : d_hds) + { + d_pt_sep.d_trie.add(e, &d_pt_sep, 0); + } + // init vector of conds + std::vector conds; + conds.insert(conds.end(), d_cond_mvs.begin(), d_cond_mvs.end()); + + // recursively build trie by picking best condition for respective points + buildDtInfoGain(d_hds, conds, hd_mv, 1); + // if no condition was added (i.e. points are already classified at root + // level), use last condition as candidate + if (d_conds.empty()) + { + Trace("sygus-unif-dt") << "......using last condition " + << d_unif->d_tds->sygusToBuiltin( + backup_last_cond, backup_last_cond.getType()) + << " as candidate\n"; + d_conds.push_back(backup_last_cond); + d_pt_sep.d_trie.addClassifier(&d_pt_sep, d_conds.size() - 1); + } +} + +void SygusUnifRl::DecisionTreeInfo::buildDtInfoGain(std::vector& hds, + std::vector conds, + std::map& hd_mv, + int ind) +{ + // test if fully classified + if (hds.size() < 2) + { + indent("sygus-unif-dt", ind); + Trace("sygus-unif-dt") << "..set fully classified: " + << (hds.empty() ? "empty" : "unary") << "\n"; + return; + } + Node v1 = hd_mv[hds[0]]; + unsigned i = 1, size = hds.size(); + for (; i < size; ++i) + { + if (hd_mv[hds[i]] != v1) + { + break; + } + } + if (i == size) + { + indent("sygus-unif-dt", ind); + Trace("sygus-unif-dt") << "..set fully classified: " << hds.size() << " " + << (d_unif->d_tds->sygusToBuiltin(v1, v1.getType()) + == d_true + ? "good" + : "bad") + << " points\n"; + return; + } + // pick condition to further classify + double maxgain = -1; + unsigned picked_cond = 0; + std::vector, std::vector>> splits; + double current_set_entropy = getEntropy(hds, hd_mv, ind); + for (unsigned i = 0, size = conds.size(); i < size; ++i) + { + std::pair, std::vector> split = + evaluateCond(hds, conds[i]); + splits.push_back(split); + Assert(hds.size() == split.first.size() + split.second.size()); + double gain = + current_set_entropy + - (split.first.size() * getEntropy(split.first, hd_mv, ind) + + split.second.size() * getEntropy(split.second, hd_mv, ind)) + / hds.size(); + indent("sygus-unif-dt-debug", ind); + Trace("sygus-unif-dt-debug") + << "..gain of " + << d_unif->d_tds->sygusToBuiltin(conds[i], conds[i].getType()) << " is " + << gain << "\n"; + if (gain > maxgain) + { + maxgain = gain; + picked_cond = i; + } + } + // add picked condition + indent("sygus-unif-dt", ind); + Trace("sygus-unif-dt") << "..picked condition " + << d_unif->d_tds->sygusToBuiltin( + conds[picked_cond], + conds[picked_cond].getType()) + << "\n"; + d_conds.push_back(conds[picked_cond]); + conds.erase(conds.begin() + picked_cond); + d_pt_sep.d_trie.addClassifier(&d_pt_sep, d_conds.size() - 1); + // recurse + buildDtInfoGain(splits[picked_cond].first, conds, hd_mv, ind + 1); + buildDtInfoGain(splits[picked_cond].second, conds, hd_mv, ind + 1); +} + +std::pair, std::vector> +SygusUnifRl::DecisionTreeInfo::evaluateCond(std::vector& pts, Node cond) +{ + std::vector good, bad; + for (const Node& pt : pts) + { + if (d_pt_sep.computeCond(cond, pt) == d_true) + { + good.push_back(pt); + continue; + } + Assert(d_pt_sep.computeCond(cond, pt) == d_false); + bad.push_back(pt); + } + return std::pair, std::vector>(good, bad); +} + +double SygusUnifRl::DecisionTreeInfo::getEntropy(const std::vector& hds, + std::map& hd_mv, + int ind) +{ + double p = 0, n = 0; + TermDbSygus* tds = d_unif->d_tds; + // get number of points evaluated positively and negatively with feature + for (const Node& e : hds) + { + if (tds->sygusToBuiltin(hd_mv[e]) == d_true) + { + p++; + continue; + } + Assert(tds->sygusToBuiltin(hd_mv[e]) == d_false); + n++; + } + // compute entropy + return p == 0 || n == 0 ? 0 + : ((-p / (p + n)) * log2(p / (p + n))) + - ((n / (p + n)) * log2(n / (p + n))); +} + void SygusUnifRl::DecisionTreeInfo::PointSeparator::initialize( DecisionTreeInfo* dt) { @@ -914,16 +1075,29 @@ Node SygusUnifRl::DecisionTreeInfo::PointSeparator::evaluate(Node n, Assert(index < d_dt->d_conds.size()); // Retrieve respective built_in condition Node cond = d_dt->d_conds[index]; + return computeCond(cond, n); +} + +Node SygusUnifRl::DecisionTreeInfo::PointSeparator::computeCond(Node cond, + Node hd) +{ + std::pair cond_hd = std::pair(cond, hd); + std::map, Node>::iterator it = + d_eval_cond_hd.find(cond_hd); + if (it != d_eval_cond_hd.end()) + { + return it->second; + } TypeNode tn = cond.getType(); Node builtin_cond = d_dt->d_unif->d_tds->sygusToBuiltin(cond, tn); // Retrieve evaluation point - Assert(d_dt->d_unif->d_hd_to_pt.find(n) != d_dt->d_unif->d_hd_to_pt.end()); - std::vector pt = d_dt->d_unif->d_hd_to_pt[n]; + Assert(d_dt->d_unif->d_hd_to_pt.find(hd) != d_dt->d_unif->d_hd_to_pt.end()); + std::vector pt = d_dt->d_unif->d_hd_to_pt[hd]; // compute the result if (Trace.isOn("sygus-unif-rl-sep")) { - Trace("sygus-unif-rl-sep") << "Evaluate cond " << builtin_cond << " on pt " - << n << " ( "; + Trace("sygus-unif-rl-sep") + << "Evaluate cond " << builtin_cond << " on pt " << hd << " ( "; for (const Node& pti : pt) { Trace("sygus-unif-rl-sep") << pti << " "; @@ -939,13 +1113,14 @@ Node SygusUnifRl::DecisionTreeInfo::PointSeparator::evaluate(Node n, { res = templ.substitute(templ_var, res); res = Rewriter::rewrite(res); - Trace("sygus-unif-rl-sep") << "...after template res = " << res - << std::endl; + Trace("sygus-unif-rl-sep") + << "...after template res = " << res << std::endl; } Assert(res.isConst()); + d_eval_cond_hd[cond_hd] = res; return res; } -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index b2db53aeb..aad3c0b49 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -80,7 +80,7 @@ class SygusUnifRl : public SygusUnif * whether f is being synthesized with unification strategies. This can be * checked through wehether f has conditional or point enumerators (we use the * former) - */ + */ bool usingUnif(Node f) const; /** get condition for evaluation point * @@ -244,6 +244,9 @@ class SygusUnifRl : public SygusUnif const std::vector& conds); private: + /** true and false nodes */ + Node d_true; + Node d_false; /** Accumulates solutions built when considering all enumerated condition * values (which may generate repeated solutions) */ std::unordered_set d_sols; @@ -275,6 +278,63 @@ class SygusUnifRl : public SygusUnif * decision tree. */ Node d_cond_enum; + /** extracts solution from decision tree built + * + * Depending on the active options, the decision tree might be rebuilt + * before a solution is extracted, for example to optimize size (smaller + * DTs) or chance of having a general solution (information gain heuristics) + */ + Node extractSol(Node cons, std::map& hd_mv); + + /** rebuild decision tree using information gain heuristic + * + * In a scenario in which the decision tree potentially contains more + * conditions than necessary, it is beneficial to rebuild it in a way that + * "better" conditions occurr closer to the top. + * + * The information gain heuristic selects conditions that lead to a + * greater reduction of the Shannon entropy in the set of points + */ + void recomputeSolHeuristically(std::map& hd_mv); + /** recursively select (best) conditions to split heads + * + * At each call picks the best condition based on the information gain + * heuristic and splits the set of heads accordingly, then recurses on + * them. + * + * The base case is a set being fully classified (i.e. all heads have the + * same value) + * + * hds is the set of evaluation point heads we must classify with the + * values in conds. The classification is guided by how a condition value + * splits the heads through its evaluation on the points associated with + * the heads. The metric is based on the model values of the heads (hd_mv) + * in the resulting splits. + * + * ind is the current level of indentation (for debugging) + */ + void buildDtInfoGain(std::vector& hds, + std::vector conds, + std::map& hd_mv, + int ind); + /** computes the Shannon entropy of a set of heads + * + * The entropy depends on how many positive and negative heads are in the + * set and in their distribution. The polarity of the evaluation heads is + * queried from their model values in hd_mv. + * + * ind is the current level of indentation (for debugging) + */ + double getEntropy(const std::vector& hds, + std::map& hd_mv, + int ind); + /** evaluates a condition on a set of points + * + * The result is two sets of points: those on which the condition holds + * and those on which it does not + */ + std::pair, std::vector> evaluateCond( + std::vector& pts, Node cond); /** Classifies evaluation points according to enumerated condition values * * Maintains the invariant that points evaluated in the same way in the @@ -296,10 +356,26 @@ class SygusUnifRl : public SygusUnif LazyTrieMulti d_trie; /** extracts solution from decision tree built */ Node extractSol(Node cons, std::map& hd_mv); + /** computes the result of applying cond on the respective point of hd + * + * If for example cond is (\lambda xy. x < y) and hd is an evaluation head + * in point (hd 0 1) this function will result in true, since + * (\lambda xy. x < y) 0 1 evaluates to true + */ + Node computeCond(Node cond, Node hd); private: /** reference to parent unif util */ DecisionTreeInfo* d_dt; + /** cache of conditions evaluations on heads + * + * If for example cond is (\lambda xy. x < y) and hd is an evaluation head + * in point (hd 0 1), then after invoking computeCond(cond, hd) this map + * will contain d_eval_cond_hd[] = true, since + * + * (\lambda xy. x < y) 0 1 evaluates to true + */ + std::map, Node> d_eval_cond_hd; }; /** * Utility for determining how evaluation points are separated by currently @@ -353,8 +429,8 @@ class SygusUnifRl : public SygusUnif unsigned strategy_index); }; -} /* CVC4::theory::quantifiers namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 #endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H */ diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 8b690f3e1..45385f9c6 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1545,6 +1545,7 @@ REG1_TESTS = \ regress1/sygus/array_search_5-Q-easy.sy \ regress1/sygus/array_sum_2_5.sy \ regress1/sygus/bvudiv-by-2.sy \ + regress1/sygus/car_3.lus.sy \ regress1/sygus/cegar1.sy \ regress1/sygus/cegis-unif-inv-eq-fair.sy \ regress1/sygus/cegisunif-depth1.sy \ diff --git a/test/regress/regress1/sygus/car_3.lus.sy b/test/regress/regress1/sygus/car_3.lus.sy new file mode 100755 index 000000000..b572622f7 --- /dev/null +++ b/test/regress/regress1/sygus/car_3.lus.sy @@ -0,0 +1,537 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status --sygus-unif --sygus-unif-cond-independent --sygus-unif-boolean-heuristic-dt + +(set-logic LIA) + +(define-fun + __node_init_Sofar_0 ( + (Sofar.usr.X_a_0 Bool) + (Sofar.usr.Sofar_a_0 Bool) + (Sofar.res.init_flag_a_0 Bool) + ) Bool + + (and (= Sofar.usr.Sofar_a_0 Sofar.usr.X_a_0) Sofar.res.init_flag_a_0) +) + +(define-fun + __node_trans_Sofar_0 ( + (Sofar.usr.X_a_1 Bool) + (Sofar.usr.Sofar_a_1 Bool) + (Sofar.res.init_flag_a_1 Bool) + (Sofar.usr.X_a_0 Bool) + (Sofar.usr.Sofar_a_0 Bool) + (Sofar.res.init_flag_a_0 Bool) + ) Bool + + (and + (= Sofar.usr.Sofar_a_1 (and Sofar.usr.X_a_1 Sofar.usr.Sofar_a_0)) + (not Sofar.res.init_flag_a_1)) +) + +(define-fun + __node_init_excludes2_0 ( + (excludes2.usr.X1_a_0 Bool) + (excludes2.usr.X2_a_0 Bool) + (excludes2.usr.excludes_a_0 Bool) + (excludes2.res.init_flag_a_0 Bool) + ) Bool + + (and + (= + excludes2.usr.excludes_a_0 + (not (and excludes2.usr.X1_a_0 excludes2.usr.X2_a_0))) + excludes2.res.init_flag_a_0) +) + +(define-fun + __node_trans_excludes2_0 ( + (excludes2.usr.X1_a_1 Bool) + (excludes2.usr.X2_a_1 Bool) + (excludes2.usr.excludes_a_1 Bool) + (excludes2.res.init_flag_a_1 Bool) + (excludes2.usr.X1_a_0 Bool) + (excludes2.usr.X2_a_0 Bool) + (excludes2.usr.excludes_a_0 Bool) + (excludes2.res.init_flag_a_0 Bool) + ) Bool + + (and + (= + excludes2.usr.excludes_a_1 + (not (and excludes2.usr.X1_a_1 excludes2.usr.X2_a_1))) + (not excludes2.res.init_flag_a_1)) +) + +(define-fun + __node_init_voiture_0 ( + (voiture.usr.m_a_0 Bool) + (voiture.usr.s_a_0 Bool) + (voiture.usr.toofast_a_0 Bool) + (voiture.usr.stop_a_0 Bool) + (voiture.usr.bump_a_0 Bool) + (voiture.usr.dist_a_0 Int) + (voiture.usr.speed_a_0 Int) + (voiture.usr.time_a_0 Int) + (voiture.usr.move_a_0 Bool) + (voiture.usr.second_a_0 Bool) + (voiture.usr.meter_a_0 Bool) + (voiture.res.init_flag_a_0 Bool) + (voiture.res.abs_0_a_0 Bool) + ) Bool + + (and + (= voiture.usr.speed_a_0 0) + (= voiture.usr.toofast_a_0 (>= voiture.usr.speed_a_0 3)) + (= voiture.usr.move_a_0 true) + (= voiture.usr.time_a_0 0) + (= voiture.usr.dist_a_0 0) + (= voiture.usr.bump_a_0 (= voiture.usr.dist_a_0 10)) + (= voiture.usr.stop_a_0 (>= voiture.usr.time_a_0 4)) + (= + voiture.res.abs_0_a_0 + (and + (and + (and voiture.usr.move_a_0 (not voiture.usr.stop_a_0)) + (not voiture.usr.toofast_a_0)) + (not voiture.usr.bump_a_0))) + (= voiture.usr.second_a_0 false) + (= voiture.usr.meter_a_0 false) + voiture.res.init_flag_a_0) +) + +(define-fun + __node_trans_voiture_0 ( + (voiture.usr.m_a_1 Bool) + (voiture.usr.s_a_1 Bool) + (voiture.usr.toofast_a_1 Bool) + (voiture.usr.stop_a_1 Bool) + (voiture.usr.bump_a_1 Bool) + (voiture.usr.dist_a_1 Int) + (voiture.usr.speed_a_1 Int) + (voiture.usr.time_a_1 Int) + (voiture.usr.move_a_1 Bool) + (voiture.usr.second_a_1 Bool) + (voiture.usr.meter_a_1 Bool) + (voiture.res.init_flag_a_1 Bool) + (voiture.res.abs_0_a_1 Bool) + (voiture.usr.m_a_0 Bool) + (voiture.usr.s_a_0 Bool) + (voiture.usr.toofast_a_0 Bool) + (voiture.usr.stop_a_0 Bool) + (voiture.usr.bump_a_0 Bool) + (voiture.usr.dist_a_0 Int) + (voiture.usr.speed_a_0 Int) + (voiture.usr.time_a_0 Int) + (voiture.usr.move_a_0 Bool) + (voiture.usr.second_a_0 Bool) + (voiture.usr.meter_a_0 Bool) + (voiture.res.init_flag_a_0 Bool) + (voiture.res.abs_0_a_0 Bool) + ) Bool + + (and + (= voiture.usr.meter_a_1 (and voiture.usr.m_a_1 (not voiture.usr.s_a_1))) + (= voiture.usr.second_a_1 voiture.usr.s_a_1) + (= voiture.usr.move_a_1 voiture.res.abs_0_a_0) + (= + voiture.usr.speed_a_1 + (ite + (or (not voiture.usr.move_a_1) voiture.usr.second_a_1) + 0 + (ite + (and voiture.usr.move_a_1 voiture.usr.meter_a_1) + (+ voiture.usr.speed_a_0 1) + voiture.usr.speed_a_0))) + (= voiture.usr.toofast_a_1 (>= voiture.usr.speed_a_1 3)) + (= + voiture.usr.time_a_1 + (ite voiture.usr.second_a_1 (+ voiture.usr.time_a_0 1) voiture.usr.time_a_0)) + (= + voiture.usr.dist_a_1 + (ite + (and voiture.usr.move_a_1 voiture.usr.meter_a_1) + (+ voiture.usr.dist_a_0 1) + voiture.usr.dist_a_0)) + (= voiture.usr.bump_a_1 (= voiture.usr.dist_a_1 10)) + (= voiture.usr.stop_a_1 (>= voiture.usr.time_a_1 4)) + (= + voiture.res.abs_0_a_1 + (and + (and + (and voiture.usr.move_a_1 (not voiture.usr.stop_a_1)) + (not voiture.usr.toofast_a_1)) + (not voiture.usr.bump_a_1))) + (not voiture.res.init_flag_a_1)) +) + +(define-fun + __node_init_top_0 ( + (top.usr.m_a_0 Bool) + (top.usr.s_a_0 Bool) + (top.usr.OK_a_0 Bool) + (top.res.init_flag_a_0 Bool) + (top.res.abs_0_a_0 Bool) + (top.res.abs_1_a_0 Bool) + (top.res.abs_2_a_0 Bool) + (top.res.abs_3_a_0 Int) + (top.res.abs_4_a_0 Int) + (top.res.abs_5_a_0 Int) + (top.res.abs_6_a_0 Bool) + (top.res.abs_7_a_0 Bool) + (top.res.abs_8_a_0 Bool) + (top.res.abs_9_a_0 Bool) + (top.res.abs_10_a_0 Bool) + (top.res.inst_3_a_0 Bool) + (top.res.inst_2_a_0 Bool) + (top.res.inst_1_a_0 Bool) + (top.res.inst_0_a_0 Bool) + ) Bool + + (let + ((X1 Bool top.res.abs_10_a_0)) + (let + ((X2 Int top.res.abs_4_a_0)) + (and + (= top.usr.OK_a_0 (=> X1 (< X2 4))) + (__node_init_voiture_0 + top.usr.m_a_0 + top.usr.s_a_0 + top.res.abs_0_a_0 + top.res.abs_1_a_0 + top.res.abs_2_a_0 + top.res.abs_3_a_0 + top.res.abs_4_a_0 + top.res.abs_5_a_0 + top.res.abs_6_a_0 + top.res.abs_7_a_0 + top.res.abs_8_a_0 + top.res.inst_3_a_0 + top.res.inst_2_a_0) + (__node_init_Sofar_0 top.res.abs_9_a_0 top.res.abs_10_a_0 top.res.inst_1_a_0) + (__node_init_excludes2_0 + top.usr.m_a_0 + top.usr.s_a_0 + top.res.abs_9_a_0 + top.res.inst_0_a_0) + top.res.init_flag_a_0))) +) + +(define-fun + __node_trans_top_0 ( + (top.usr.m_a_1 Bool) + (top.usr.s_a_1 Bool) + (top.usr.OK_a_1 Bool) + (top.res.init_flag_a_1 Bool) + (top.res.abs_0_a_1 Bool) + (top.res.abs_1_a_1 Bool) + (top.res.abs_2_a_1 Bool) + (top.res.abs_3_a_1 Int) + (top.res.abs_4_a_1 Int) + (top.res.abs_5_a_1 Int) + (top.res.abs_6_a_1 Bool) + (top.res.abs_7_a_1 Bool) + (top.res.abs_8_a_1 Bool) + (top.res.abs_9_a_1 Bool) + (top.res.abs_10_a_1 Bool) + (top.res.inst_3_a_1 Bool) + (top.res.inst_2_a_1 Bool) + (top.res.inst_1_a_1 Bool) + (top.res.inst_0_a_1 Bool) + (top.usr.m_a_0 Bool) + (top.usr.s_a_0 Bool) + (top.usr.OK_a_0 Bool) + (top.res.init_flag_a_0 Bool) + (top.res.abs_0_a_0 Bool) + (top.res.abs_1_a_0 Bool) + (top.res.abs_2_a_0 Bool) + (top.res.abs_3_a_0 Int) + (top.res.abs_4_a_0 Int) + (top.res.abs_5_a_0 Int) + (top.res.abs_6_a_0 Bool) + (top.res.abs_7_a_0 Bool) + (top.res.abs_8_a_0 Bool) + (top.res.abs_9_a_0 Bool) + (top.res.abs_10_a_0 Bool) + (top.res.inst_3_a_0 Bool) + (top.res.inst_2_a_0 Bool) + (top.res.inst_1_a_0 Bool) + (top.res.inst_0_a_0 Bool) + ) Bool + + (let + ((X1 Bool top.res.abs_10_a_1)) + (let + ((X2 Int top.res.abs_4_a_1)) + (and + (= top.usr.OK_a_1 (=> X1 (< X2 4))) + (__node_trans_voiture_0 + top.usr.m_a_1 + top.usr.s_a_1 + top.res.abs_0_a_1 + top.res.abs_1_a_1 + top.res.abs_2_a_1 + top.res.abs_3_a_1 + top.res.abs_4_a_1 + top.res.abs_5_a_1 + top.res.abs_6_a_1 + top.res.abs_7_a_1 + top.res.abs_8_a_1 + top.res.inst_3_a_1 + top.res.inst_2_a_1 + top.usr.m_a_0 + top.usr.s_a_0 + top.res.abs_0_a_0 + top.res.abs_1_a_0 + top.res.abs_2_a_0 + top.res.abs_3_a_0 + top.res.abs_4_a_0 + top.res.abs_5_a_0 + top.res.abs_6_a_0 + top.res.abs_7_a_0 + top.res.abs_8_a_0 + top.res.inst_3_a_0 + top.res.inst_2_a_0) + (__node_trans_Sofar_0 + top.res.abs_9_a_1 + top.res.abs_10_a_1 + top.res.inst_1_a_1 + top.res.abs_9_a_0 + top.res.abs_10_a_0 + top.res.inst_1_a_0) + (__node_trans_excludes2_0 + top.usr.m_a_1 + top.usr.s_a_1 + top.res.abs_9_a_1 + top.res.inst_0_a_1 + top.usr.m_a_0 + top.usr.s_a_0 + top.res.abs_9_a_0 + top.res.inst_0_a_0) + (not top.res.init_flag_a_1)))) +) + + + +(synth-inv str_invariant( + (top.usr.m Bool) + (top.usr.s Bool) + (top.usr.OK Bool) + (top.res.init_flag Bool) + (top.res.abs_0 Bool) + (top.res.abs_1 Bool) + (top.res.abs_2 Bool) + (top.res.abs_3 Int) + (top.res.abs_4 Int) + (top.res.abs_5 Int) + (top.res.abs_6 Bool) + (top.res.abs_7 Bool) + (top.res.abs_8 Bool) + (top.res.abs_9 Bool) + (top.res.abs_10 Bool) + (top.res.inst_3 Bool) + (top.res.inst_2 Bool) + (top.res.inst_1 Bool) + (top.res.inst_0 Bool) +)) + + +(declare-primed-var top.usr.m Bool) +(declare-primed-var top.usr.s Bool) +(declare-primed-var top.usr.OK Bool) +(declare-primed-var top.res.init_flag Bool) +(declare-primed-var top.res.abs_0 Bool) +(declare-primed-var top.res.abs_1 Bool) +(declare-primed-var top.res.abs_2 Bool) +(declare-primed-var top.res.abs_3 Int) +(declare-primed-var top.res.abs_4 Int) +(declare-primed-var top.res.abs_5 Int) +(declare-primed-var top.res.abs_6 Bool) +(declare-primed-var top.res.abs_7 Bool) +(declare-primed-var top.res.abs_8 Bool) +(declare-primed-var top.res.abs_9 Bool) +(declare-primed-var top.res.abs_10 Bool) +(declare-primed-var top.res.inst_3 Bool) +(declare-primed-var top.res.inst_2 Bool) +(declare-primed-var top.res.inst_1 Bool) +(declare-primed-var top.res.inst_0 Bool) + +(define-fun + init ( + (top.usr.m Bool) + (top.usr.s Bool) + (top.usr.OK Bool) + (top.res.init_flag Bool) + (top.res.abs_0 Bool) + (top.res.abs_1 Bool) + (top.res.abs_2 Bool) + (top.res.abs_3 Int) + (top.res.abs_4 Int) + (top.res.abs_5 Int) + (top.res.abs_6 Bool) + (top.res.abs_7 Bool) + (top.res.abs_8 Bool) + (top.res.abs_9 Bool) + (top.res.abs_10 Bool) + (top.res.inst_3 Bool) + (top.res.inst_2 Bool) + (top.res.inst_1 Bool) + (top.res.inst_0 Bool) + ) Bool + + (let + ((X1 Bool top.res.abs_10)) + (let + ((X2 Int top.res.abs_4)) + (and + (= top.usr.OK (=> X1 (< X2 4))) + (__node_init_voiture_0 + top.usr.m + top.usr.s + top.res.abs_0 + top.res.abs_1 + top.res.abs_2 + top.res.abs_3 + top.res.abs_4 + top.res.abs_5 + top.res.abs_6 + top.res.abs_7 + top.res.abs_8 + top.res.inst_3 + top.res.inst_2) + (__node_init_Sofar_0 top.res.abs_9 top.res.abs_10 top.res.inst_1) + (__node_init_excludes2_0 + top.usr.m + top.usr.s + top.res.abs_9 + top.res.inst_0) + top.res.init_flag))) +) + +(define-fun + trans ( + + ;; Current state. + (top.usr.m Bool) + (top.usr.s Bool) + (top.usr.OK Bool) + (top.res.init_flag Bool) + (top.res.abs_0 Bool) + (top.res.abs_1 Bool) + (top.res.abs_2 Bool) + (top.res.abs_3 Int) + (top.res.abs_4 Int) + (top.res.abs_5 Int) + (top.res.abs_6 Bool) + (top.res.abs_7 Bool) + (top.res.abs_8 Bool) + (top.res.abs_9 Bool) + (top.res.abs_10 Bool) + (top.res.inst_3 Bool) + (top.res.inst_2 Bool) + (top.res.inst_1 Bool) + (top.res.inst_0 Bool) + + ;; Next state. + (top.usr.m! Bool) + (top.usr.s! Bool) + (top.usr.OK! Bool) + (top.res.init_flag! Bool) + (top.res.abs_0! Bool) + (top.res.abs_1! Bool) + (top.res.abs_2! Bool) + (top.res.abs_3! Int) + (top.res.abs_4! Int) + (top.res.abs_5! Int) + (top.res.abs_6! Bool) + (top.res.abs_7! Bool) + (top.res.abs_8! Bool) + (top.res.abs_9! Bool) + (top.res.abs_10! Bool) + (top.res.inst_3! Bool) + (top.res.inst_2! Bool) + (top.res.inst_1! Bool) + (top.res.inst_0! Bool) + + ) Bool + + (let + ((X1 Bool top.res.abs_10!)) + (let + ((X2 Int top.res.abs_4!)) + (and + (= top.usr.OK! (=> X1 (< X2 4))) + (__node_trans_voiture_0 + top.usr.m! + top.usr.s! + top.res.abs_0! + top.res.abs_1! + top.res.abs_2! + top.res.abs_3! + top.res.abs_4! + top.res.abs_5! + top.res.abs_6! + top.res.abs_7! + top.res.abs_8! + top.res.inst_3! + top.res.inst_2! + top.usr.m + top.usr.s + top.res.abs_0 + top.res.abs_1 + top.res.abs_2 + top.res.abs_3 + top.res.abs_4 + top.res.abs_5 + top.res.abs_6 + top.res.abs_7 + top.res.abs_8 + top.res.inst_3 + top.res.inst_2) + (__node_trans_Sofar_0 + top.res.abs_9! + top.res.abs_10! + top.res.inst_1! + top.res.abs_9 + top.res.abs_10 + top.res.inst_1) + (__node_trans_excludes2_0 + top.usr.m! + top.usr.s! + top.res.abs_9! + top.res.inst_0! + top.usr.m + top.usr.s + top.res.abs_9 + top.res.inst_0) + (not top.res.init_flag!)))) +) + +(define-fun + prop ( + (top.usr.m Bool) + (top.usr.s Bool) + (top.usr.OK Bool) + (top.res.init_flag Bool) + (top.res.abs_0 Bool) + (top.res.abs_1 Bool) + (top.res.abs_2 Bool) + (top.res.abs_3 Int) + (top.res.abs_4 Int) + (top.res.abs_5 Int) + (top.res.abs_6 Bool) + (top.res.abs_7 Bool) + (top.res.abs_8 Bool) + (top.res.abs_9 Bool) + (top.res.abs_10 Bool) + (top.res.inst_3 Bool) + (top.res.inst_2 Bool) + (top.res.inst_1 Bool) + (top.res.inst_0 Bool) + ) Bool + + top.usr.OK +) + +(inv-constraint str_invariant init trans prop) + +(check-synth)