diff --git a/src/math/automata/symbolic_automata.h b/src/math/automata/symbolic_automata.h index d77e0548d..ddd938cac 100644 --- a/src/math/automata/symbolic_automata.h +++ b/src/math/automata/symbolic_automata.h @@ -96,6 +96,8 @@ public: automaton_t* remove_epsilons(automaton_t& a); automaton_t* mk_total(automaton_t& a); automaton_t* mk_minimize(automaton_t& a); + automaton_t* mk_minimize_total(automaton_t& a); + automaton_t* mk_difference(automaton_t& a, automaton_t& b); automaton_t* mk_product(automaton_t& a, automaton_t& b); }; diff --git a/src/math/automata/symbolic_automata_def.h b/src/math/automata/symbolic_automata_def.h index 99ad9e9bc..f37384b2c 100644 --- a/src/math/automata/symbolic_automata_def.h +++ b/src/math/automata/symbolic_automata_def.h @@ -74,7 +74,12 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_minim if (!fa) { return 0; } - + return mk_minimize_total(*fa.get()); +} + + +template +typename symbolic_automata::automaton_t* symbolic_automata::mk_minimize_total(automaton_t& a) { vector pblocks; unsigned_vector blocks; pblocks.push_back(block(fa->final_states())); // 0 |-> final states @@ -101,7 +106,7 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_minim u_map gamma; moves_t mvs; while (!W.empty()) { - block R(W.back()); + block R(pblocks[W.back()]); W.pop_back(); block Rcopy(R); gamma.reset(); @@ -123,13 +128,173 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_minim } } uint_set relevant; - u_map::iterator end = gamma.end(); - for (u_map::iterator it = gamma.begin(); it != end; ++it) { - relevant.insert(it->m_key); + u_map::iterator gend = gamma.end(); + for (u_map::iterator it = gamma.begin(); it != gend; ++it) { + relevant.insert(blocks[it->m_key]); + } + uint_set::iterator uit = relevant.begin(), uend = relevant.end(); + for (; uit != uend; ++uit) { + unsigned p0_index = *uit; + block& p0 = pblocks[p0_index]; + block p1; + for (u_map::iterator it = gamma.begin(); it != gend; ++it) { + if (p0.contains(*it)) p1.push_back(*it); + } + if (p1.size() < p0.size()) { + unsigned p1_index = pblocks.size(); + pblocks.push_back(p1); + for (uint_set::iterator it = p1.begin(), end = p1.end(); it != end; ++it) { + p0.remove(*it); + blocks[*it] = p1_index; + } + if (W.contains(p0_index)) { + W.push_back(p1_index); + } + else if (p0.size() <= p1.size()) { + W.push_back(p0_index); + } + else { + W.push_back(p1_index); + } + } + bool iterate = true; + while (iterate) { + iterate = false; + uint_set relevant; + for (u_map::iterator it = gamma.begin(); it != gend; ++it) { + if (pblocks[blocks[it->m_key]].size() > 1) { + relevant.insert(blocks[it->m_key]); + } + } + uint_set::iterator it = relevant.begin(), end = relevant.end(); + for (; it != end; ++it) { + block const& p = pblocks[*it]; + uint_set::iterator bi = p.begin(), be = p.end(); + + block p1; + p1.insert(*bi); + // psi = gamma[*bi]; // name of key or block? + ++bi; + for (; bi != be; ++bi) { + + } + } + } } - } #endif + +#if 0 + Func MkDiff = (x, y) => solver.MkAnd(x, solver.MkNot(y)); + + while (!W.IsEmpty) + { + //keep using Bcopy until no more changes occur + //effectively, this replaces the loop over characters + bool iterate = true; + //in each relevant block all states lead to B due to the initial splitting + + //only relevant blocks are potentially split + foreach (var P in relevant2) + { + var PE = P.GetEnumerator(); + PE.MoveNext(); + + var P1 = new Block(); + bool splitFound = false; + + var psi = Gamma[PE.Current]; + P1.Add(PE.Current); //C has at least 2 elements + + #region compute C1 as the new sub-block of C + while (PE.MoveNext()) + { + var q = PE.Current; + var phi = Gamma[q]; + if (splitFound) + { + var psi_and_phi = solver.MkAnd(psi, phi); + if (solver.IsSatisfiable(psi_and_phi)) + P1.Add(q); + } + else + { + var psi_min_phi = MkDiff(psi, phi); + if (solver.IsSatisfiable(psi_min_phi)) + { + psi = psi_min_phi; + splitFound = true; + } + else // [[psi]] is subset of [[phi]] + { + var phi_min_psi = MkDiff(phi, psi); + if (!solver.IsSatisfiable(phi_min_psi)) + P1.Add(q); //psi and phi are equivalent + else + { + //there is some a: q --a--> B and p --a--> compl(B) for all p in C1 + P1.Clear(); + P1.Add(q); + psi = phi_min_psi; + splitFound = true; + } + } + } + } + #endregion + + #region split P + if (P1.Count < P.Count) + { + iterate = (iterate || (P.Count > 2)); //otherwise C was split into singletons + foreach (var p in P1) + { + P.Remove(p); + Blocks[p] = P1; + } + + if (W.Contains(P)) + W.Push(P1); + else if (P.Count <= P1.Count) + W.Push(P); + else + W.Push(P1); + } + #endregion + } + } + } + + Dictionary, HashSet> condMap = new Dictionary, HashSet>(); + foreach (var move in GetMoves()) + { + int s = Blocks[move.SourceState].GetRepresentative(); + int t = Blocks[move.TargetState].GetRepresentative(); + var st = new Pair(s, t); + HashSet condSet; + if (!condMap.TryGetValue(st, out condSet)) + { + condSet = new HashSet(); + condSet.Add(move.Label); + condMap[st] = condSet; + } + else + condSet.Add(move.Label); + } + int newInitState = Blocks[fa.InitialState].GetRepresentative(); + var newMoves = new List>(); + var newFinals = new HashSet(); + foreach (var entry in condMap) + newMoves.Add(Move.Create(entry.Key.First, entry.Key.Second, solver.MkOr(entry.Value))); + foreach (var f in GetFinalStates()) + newFinals.Add(Blocks[f].GetRepresentative()); + + var res = Create(newInitState, newFinals, newMoves); + res.isDeterministic = true; + res.isEpsilonFree = true; + //res.EliminateDeadStates(); + return res; +#endif return 0; diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index 15bfa69d2..2d266aed8 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -22,7 +22,7 @@ Author: #include "ast_pp.h" #include -static uint64_t uMaxInt(unsigned sz) { +static uint64 uMaxInt(unsigned sz) { SASSERT(sz <= 64); return ULLONG_MAX >> (64u - sz); } @@ -32,12 +32,12 @@ namespace { struct interval { // l < h: [l, h] // l > h: [0, h] U [l, UMAX_INT] - uint64_t l, h; + uint64 l, h; unsigned sz; bool tight; interval() {} - interval(uint64_t l, uint64_t h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) { + interval(uint64 l, uint64 h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) { // canonicalize full set if (is_wrapped() && l == h + 1) { this->l = 0; @@ -175,7 +175,7 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { expr_list_map m_expr_vars; expr_set m_bound_exprs; - bool is_number(expr *e, uint64_t& n, unsigned& sz) const { + bool is_number(expr *e, uint64& n, unsigned& sz) const { rational r; if (m_bv.is_numeral(e, r, sz) && sz <= 64) { n = r.get_uint64(); @@ -185,7 +185,7 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { } bool is_bound(expr *e, expr*& v, interval& b) const { - uint64_t n; + uint64 n; expr *lhs, *rhs; unsigned sz;