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"
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<Node>& eis, Node e)
#include "theory/quantifiers/sygus/ce_guided_conjecture.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
+#include <math.h>
+
using namespace CVC4::kind;
namespace CVC4 {
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);
}
{
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"))
}
}
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
{
"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] =
// 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;
}
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;
}
Node SygusUnifRl::addRefLemma(Node lemma,
std::map<Node, std::vector<Node>>& 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<Node> model_guards;
BoolNodePairMap cache;
// cache previous sizes
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]);
}
{
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;
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);
// 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())
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);
}
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())
NodeManager* nm = NodeManager::currentNM();
// model values for evaluation heads
std::map<Node, Node> 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<Node> exp;
// is the above explanation ready to be sent out as a lemma?
}
Trace("sygus-unif-sol") << "...ready to build solution from DT\n";
+ return extractSol(cons, hd_mv);
+}
+
+Node SygusUnifRl::DecisionTreeInfo::extractSol(Node cons,
+ std::map<Node, Node>& hd_mv)
+{
+ // rebuild decision tree using heuristic learning
+ if (options::sygusUnifBooleanHeuristicDt())
+ {
+ recomputeSolHeuristically(hd_mv);
+ }
return d_pt_sep.extractSol(cons, hd_mv);
}
return cache[root];
}
+void SygusUnifRl::DecisionTreeInfo::recomputeSolHeuristically(
+ std::map<Node, Node>& 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<Node> 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<Node>& hds,
+ std::vector<Node> conds,
+ std::map<Node, Node>& 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::pair<std::vector<Node>, std::vector<Node>>> splits;
+ double current_set_entropy = getEntropy(hds, hd_mv, ind);
+ for (unsigned i = 0, size = conds.size(); i < size; ++i)
+ {
+ std::pair<std::vector<Node>, std::vector<Node>> 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<Node>, std::vector<Node>>
+SygusUnifRl::DecisionTreeInfo::evaluateCond(std::vector<Node>& pts, Node cond)
+{
+ std::vector<Node> 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<Node>, std::vector<Node>>(good, bad);
+}
+
+double SygusUnifRl::DecisionTreeInfo::getEntropy(const std::vector<Node>& hds,
+ std::map<Node, Node>& 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)
{
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<Node, Node> cond_hd = std::pair<Node, Node>(cond, hd);
+ std::map<std::pair<Node, Node>, 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<Node> 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<Node> 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 << " ";
{
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
* 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
*
const std::vector<Node>& 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<Node, NodeHashFunction> d_sols;
* 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<Node, Node>& 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<Node, Node>& 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<Node>& hds,
+ std::vector<Node> conds,
+ std::map<Node, Node>& 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<Node>& hds,
+ std::map<Node, Node>& 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<Node>, std::vector<Node>> evaluateCond(
+ std::vector<Node>& pts, Node cond);
/** Classifies evaluation points according to enumerated condition values
*
* Maintains the invariant that points evaluated in the same way in the
LazyTrieMulti d_trie;
/** extracts solution from decision tree built */
Node extractSol(Node cons, std::map<Node, Node>& 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[<cond, hd>] = true, since
+ *
+ * (\lambda xy. x < y) 0 1 evaluates to true
+ */
+ std::map<std::pair<Node, Node>, Node> d_eval_cond_hd;
};
/**
* Utility for determining how evaluation points are separated by currently
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 */
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 \
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff