From c9269c198382375fe923a3a52ca405578d403d91 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Andres=20N=C3=B6tzli?= Date: Mon, 29 Feb 2016 19:12:14 -0800 Subject: [PATCH 01/11] Fix documentation for floating-point comparisons --- src/api/python/z3.py | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 3a8800f1d..305733aa7 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -8824,7 +8824,7 @@ def _check_fp_args(a, b): _z3_assert(is_fp(a) or is_fp(b), "At least one of the arguments must be a Z3 floating-point expression") def fpLT(a, b, ctx=None): - """Create the Z3 floating-point expression `other <= self`. + """Create the Z3 floating-point expression `other < self`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpLT(x, y) @@ -8846,7 +8846,7 @@ def fpLEQ(a, b, ctx=None): return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx) def fpGT(a, b, ctx=None): - """Create the Z3 floating-point expression `other <= self`. + """Create the Z3 floating-point expression `other > self`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpGT(x, y) @@ -8857,11 +8857,9 @@ def fpGT(a, b, ctx=None): return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx) def fpGEQ(a, b, ctx=None): - """Create the Z3 floating-point expression `other <= self`. + """Create the Z3 floating-point expression `other >= self`. >>> x, y = FPs('x y', FPSort(8, 24)) - >>> x + y - x + y >>> fpGEQ(x, y) x >= y >>> (x >= y).sexpr() @@ -8870,7 +8868,7 @@ def fpGEQ(a, b, ctx=None): return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx) def fpEQ(a, b, ctx=None): - """Create the Z3 floating-point expression `other <= self`. + """Create the Z3 floating-point expression `fpEQ(other, self)`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpEQ(x, y) @@ -8881,7 +8879,7 @@ def fpEQ(a, b, ctx=None): return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx) def fpNEQ(a, b, ctx=None): - """Create the Z3 floating-point expression `other <= self`. + """Create the Z3 floating-point expression `Not(fpEQ(other, self))`. >>> x, y = FPs('x y', FPSort(8, 24)) >>> fpNEQ(x, y) From 6cf76f2113b5ea8442156c3e4097f378f82446a5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 29 Feb 2016 20:23:20 -0800 Subject: [PATCH 02/11] remove references to _DEBUG use Z3DEBUG instead Signed-off-by: Nikolaj Bjorner --- src/math/automata/symbolic_automata_def.h | 23 ++++++++++++----------- src/muz/rel/dl_base.h | 4 ---- src/util/memory_manager.cpp | 2 +- src/util/memory_manager.h | 2 +- 4 files changed, 14 insertions(+), 17 deletions(-) diff --git a/src/math/automata/symbolic_automata_def.h b/src/math/automata/symbolic_automata_def.h index db6172d49..213a4b2f9 100644 --- a/src/math/automata/symbolic_automata_def.h +++ b/src/math/automata/symbolic_automata_def.h @@ -75,23 +75,24 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_minim return 0; } - block final_block(fa->final_states()); - block non_final_block(fa->non_final_states()); - vector blocks; + vector pblocks; + unsigned_vector blocks; + pblocks.push_back(block(fa->final_states())); // 0 |-> final states + pblocks.push_back(block(fa->non_final_states()); // 1 |-> non-final states for (unsigned i = 0; i < fa->num_states(); ++i) { - if (fa->is_final_state(i)) { - blocks.push_back(final_block); + if (fa->is_final_state(i)) { + blocks.push_back(0); } else { - blocks.push_back(non_final_block); + blocks.push_back(1); } } vector W; if (final_block.size() > non_final_block.size()) { - W.push_back(non_final_block); + W.push_back(1); } else { - W.push_back(final_block); + W.push_back(0); } #if 0 @@ -111,7 +112,7 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_minim fa->get_moves_to(q, mvs); for (unsigned i = 0; i < mvs.size(); ++i) { unsigned src = mvs[i].src(); - if (blocks[src].size() > 1) { + if (pblocks[src].size() > 1) { T* t = mvs[i](); if (gamma.find(src, t1)) { t = m_ba.mk_or(t, t1); @@ -121,10 +122,10 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_minim } } } - hashtable relevant; + uint_set relevant; u_map::iterator end = gamma.end(); for (u_map::iterator it = gamma.begin(); it != end; ++it) { - relevant.insert(blocks[it->m_key]); + relevant.insert(it->m_key); } } diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h index 781c8539d..1c7a81444 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -435,11 +435,7 @@ namespace datalog { void destroy() { SASSERT(this); this->~base_ancestor(); -#if _DEBUG - memory::deallocate(__FILE__, __LINE__, this); -#else memory::deallocate(this); -#endif } public: /** diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index 91d27ed27..76069ce44 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -198,7 +198,7 @@ void memory::display_i_max_usage(std::ostream & os) { << "\n"; } -#if _DEBUG +#if Z3DEBUG void memory::deallocate(char const * file, int line, void * p) { deallocate(p); TRACE_CODE(if (!g_finalizing) TRACE("memory", tout << "dealloc " << std::hex << p << std::dec << " " << file << ":" << line << "\n";);); diff --git a/src/util/memory_manager.h b/src/util/memory_manager.h index b6831faa7..aac61ea2a 100644 --- a/src/util/memory_manager.h +++ b/src/util/memory_manager.h @@ -60,7 +60,7 @@ public: static void deallocate(void* p); static ALLOC_ATTR void* allocate(size_t s); static ALLOC_ATTR void* reallocate(void *p, size_t s); -#if _DEBUG +#if Z3DEBUG static void deallocate(char const* file, int line, void* p); static ALLOC_ATTR void* allocate(char const* file, int line, char const* obj, size_t s); #endif From b90bc4e685826a7c0a13283b4a00707cb45e6e84 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 29 Feb 2016 21:15:44 -0800 Subject: [PATCH 03/11] fix build Signed-off-by: Nikolaj Bjorner --- src/math/automata/symbolic_automata_def.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/automata/symbolic_automata_def.h b/src/math/automata/symbolic_automata_def.h index 213a4b2f9..99ad9e9bc 100644 --- a/src/math/automata/symbolic_automata_def.h +++ b/src/math/automata/symbolic_automata_def.h @@ -78,7 +78,7 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_minim vector pblocks; unsigned_vector blocks; pblocks.push_back(block(fa->final_states())); // 0 |-> final states - pblocks.push_back(block(fa->non_final_states()); // 1 |-> non-final states +// pblocks.push_back(block(fa->non_final_states()); // 1 |-> non-final states for (unsigned i = 0; i < fa->num_states(); ++i) { if (fa->is_final_state(i)) { blocks.push_back(0); From 4a15d756d76a7bd24e3d9ae4c8b71a92f2d3ba86 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 29 Feb 2016 22:16:03 -0800 Subject: [PATCH 04/11] uint64_t -> uint64 for cross platform Signed-off-by: Nikolaj Bjorner --- src/math/automata/symbolic_automata.h | 2 + src/math/automata/symbolic_automata_def.h | 177 +++++++++++++++++++++- src/tactic/bv/bv_bounds_tactic.cpp | 10 +- 3 files changed, 178 insertions(+), 11 deletions(-) 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; From 570bc3c9c188811486fa8e598bc02194c21a2bad Mon Sep 17 00:00:00 2001 From: Andres Notzli Date: Mon, 29 Feb 2016 23:41:33 -0800 Subject: [PATCH 05/11] Fix build Previous commits seem to have removed some variable declarations, so the build did not work. This patch reintroduces the variables. --- src/math/automata/symbolic_automata_def.h | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/math/automata/symbolic_automata_def.h b/src/math/automata/symbolic_automata_def.h index f37384b2c..953bc83dd 100644 --- a/src/math/automata/symbolic_automata_def.h +++ b/src/math/automata/symbolic_automata_def.h @@ -79,9 +79,11 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_minim template -typename symbolic_automata::automaton_t* symbolic_automata::mk_minimize_total(automaton_t& a) { +typename symbolic_automata::automaton_t* symbolic_automata::mk_minimize_total(automaton_t& fa) { vector pblocks; unsigned_vector blocks; + block final_block(fa->final_states()); + block non_final_block(fa->non_final_states()); pblocks.push_back(block(fa->final_states())); // 0 |-> final states // pblocks.push_back(block(fa->non_final_states()); // 1 |-> non-final states for (unsigned i = 0; i < fa->num_states(); ++i) { From 830a99aab40abc04b0c6bd856620b429d37fcb69 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 1 Mar 2016 00:04:03 -0800 Subject: [PATCH 06/11] finish minimization Signed-off-by: Nikolaj Bjorner --- src/math/automata/symbolic_automata.h | 8 +- src/math/automata/symbolic_automata_def.h | 316 ++++++++++------------ 2 files changed, 151 insertions(+), 173 deletions(-) diff --git a/src/math/automata/symbolic_automata.h b/src/math/automata/symbolic_automata.h index ddd938cac..cd553eeef 100644 --- a/src/math/automata/symbolic_automata.h +++ b/src/math/automata/symbolic_automata.h @@ -79,16 +79,18 @@ class symbolic_automata { return m_rep; } - void add(unsigned i) { m_set.insert(i); } + void insert(unsigned i) { m_set.insert(i); } bool contains(unsigned i) const { return m_set.contains(i); } bool is_empty() const { return m_set.empty(); } unsigned size() const { return m_set.num_elems(); } void remove(unsigned i) { m_set.remove(i); m_rep_chosen = false; } void clear() { m_set.reset(); m_rep_chosen = false; } - uint_set::iterator begin() { return m_set.begin(); } - uint_set::iterator end() { return m_set.end(); } + uint_set::iterator begin() const { return m_set.begin(); } + uint_set::iterator end() const { return m_set.end(); } }; + void add_block(block const& p1, unsigned p0_index, unsigned_vector& blocks, vector& pblocks, unsigned_vector& W); + public: symbolic_automata(M& m, ba_t& ba): m(m), m_ba(ba) {} automaton_t* mk_determinstic(automaton_t& a); diff --git a/src/math/automata/symbolic_automata_def.h b/src/math/automata/symbolic_automata_def.h index f37384b2c..87e0f7b2d 100644 --- a/src/math/automata/symbolic_automata_def.h +++ b/src/math/automata/symbolic_automata_def.h @@ -35,7 +35,7 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_total moves_t mvs, new_mvs; for (unsigned i = 0; i < dead_state; ++i) { mvs.reset(); - a.get_moves(i, mvs, true); + a.get_moves_from(i, mvs, true); refs_t vs(m); for (unsigned j = 0; j < mvs.size(); ++j) { @@ -54,7 +54,8 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_total return a.clone(); } new_mvs.push_back(move_t(m, dead_state, dead_state, m_ba.mk_true())); - automaton_t::append_moves(0, a, new_mvs); + + // TBD private: automaton_t::append_moves(0, a, new_mvs); return alloc(automaton_t, m, a.init(), a.final_states(), new_mvs); } @@ -78,47 +79,65 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_minim } +template +void symbolic_automata::add_block(block const& p1, unsigned p0_index, unsigned_vector& blocks, vector& pblocks, unsigned_vector& W) { + block& p0 = pblocks[p0_index]; + 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); + } + } +} + 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 -// pblocks.push_back(block(fa->non_final_states()); // 1 |-> non-final states - for (unsigned i = 0; i < fa->num_states(); ++i) { - if (fa->is_final_state(i)) { - blocks.push_back(0); - } - else { + unsigned_vector non_final; + for (unsigned i = 0; i < a.num_states(); ++i) { + if (!a.is_final_state(i)) { + non_final.push_back(i); blocks.push_back(1); } + else { + blocks.push_back(0); + } } - vector W; - if (final_block.size() > non_final_block.size()) { - W.push_back(1); - } - else { - W.push_back(0); - } - -#if 0 - + pblocks.push_back(block(a.final_states())); // 0 |-> final states + pblocks.push_back(block(non_final)); // 1 |-> non-final states + + unsigned_vector W; + W.push_back(pblocks[0].size() > pblocks[1].size() ? 1 : 0); + refs_t trail(m); u_map gamma; moves_t mvs; while (!W.empty()) { block R(pblocks[W.back()]); W.pop_back(); - block Rcopy(R); gamma.reset(); - uint_set::iterator it = Rcopy.begin(), end = Rcopy.end(); + uint_set::iterator it = R.begin(), end = R.end(); for (; it != end; ++it) { - unsigned q = *it; + unsigned dst = *it; mvs.reset(); - fa->get_moves_to(q, mvs); + a.get_moves_to(dst, mvs); for (unsigned i = 0; i < mvs.size(); ++i) { unsigned src = mvs[i].src(); if (pblocks[src].size() > 1) { - T* t = mvs[i](); + T* t = mvs[i].t(); + T* t1; if (gamma.find(src, t1)) { t = m_ba.mk_or(t, t1); trail.push_back(t); @@ -127,177 +146,131 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_minim } } } - uint_set relevant; + uint_set relevant1; 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]; + for (u_map::iterator git = gamma.begin(); git != gend; ++git) { + unsigned p0A_index = blocks[git->m_key]; + if (relevant1.contains(p0A_index)) { + continue; + } + relevant1.insert(p0A_index); + block& p0A = pblocks[p0A_index]; block p1; for (u_map::iterator it = gamma.begin(); it != gend; ++it) { - if (p0.contains(*it)) p1.push_back(*it); + if (p0A.contains(it->m_key)) p1.insert(it->m_key); } - 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); - } - } + + add_block(p1, p0A_index, blocks, pblocks, W); + bool iterate = true; while (iterate) { iterate = false; - uint_set relevant; + uint_set relevant2; for (u_map::iterator it = gamma.begin(); it != gend; ++it) { - if (pblocks[blocks[it->m_key]].size() > 1) { - relevant.insert(blocks[it->m_key]); + unsigned p0B_index = blocks[it->m_key]; + if (pblocks[p0B_index].size() <= 1 || relevant2.contains(p0B_index)) { + continue; } - } - 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(); + relevant2.insert(p0B_index); + block const& p0B = pblocks[p0B_index]; + uint_set::iterator bi = p0B.begin(), be = p0B.end(); block p1; p1.insert(*bi); - // psi = gamma[*bi]; // name of key or block? + bool split_found = false; + ref_t psi(gamma[*bi], m); ++bi; for (; bi != be; ++bi) { - + unsigned q = *bi; + ref_t phi(gamma[q], m); + if (split_found) { + ref_t phi_and_psi(m_ba.mk_and(phi, psi), m); + switch (m_ba.is_sat(phi_and_psi)) { + case l_true: + p1.insert(q); + break; + case l_undef: + return 0; + default: + break; + } + } + else { + ref_t psi_min_phi(m_ba.mk_and(psi, m_ba.mk_not(phi)), m); + lbool is_sat = m_ba.is_sat(psi_min_phi); + if (is_sat == l_undef) { + return 0; + } + if (is_sat == l_true) { + psi = psi_min_phi; + split_found = true; + continue; + } + // psi is a subset of phi + ref_t phi_min_psi(m_ba.mk_and(phi, m_ba.mk_not(psi)), m); + is_sat = m_ba.is_sat(phi_min_psi); + if (is_sat == l_undef) { + return 0; + } + else if (is_sat == l_false) { + p1.insert(q); // psi and phi are equivalent + } + else { + p1.clear(); + p1.insert(q); + psi = phi_min_psi; + split_found = true; + } + } } + if (p1.size() < p0B.size() && p0B.size() > 2) iterate = true; + add_block(p1, p0B_index, blocks, pblocks, W); } } } } -#endif -#if 0 - Func MkDiff = (x, y) => solver.MkAnd(x, solver.MkNot(y)); + unsigned new_init = pblocks[blocks[a.init()]].get_representative(); - 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 + // set moves + map, default_eq > conds; + svector keys; + moves_t new_moves; - //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 - } - } + for (unsigned i = 0; i < a.num_states(); ++i) { + unsigned src = pblocks[blocks[i]].get_representative(); + automaton_t::moves const& mvs = a.get_moves_from(i); + for (unsigned j = 0; j < mvs.size(); ++j) { + unsigned dst = pblocks[blocks[mvs[j].dst()]].get_representative(); + unsigned_pair st(src, dst); + T* t = 0; + if (conds.find(st, t)) { + t = m_ba.mk_or(t, mvs[j].t()); + trail.push_back(t); + conds.insert(st, t); } - - 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); + else { + conds.insert(st, mvs[j].t()); + keys.push_back(st); } - 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()); + } + } + for (unsigned i = 0; i < keys.size(); ++i) { + unsigned_pair st = keys[i]; + new_moves.push_back(move_t(m, st.first, st.second, conds[st])); + } + // set final states. + unsigned_vector new_final; + uint_set new_final_set; + for (unsigned i = 0; i < a.final_states().size(); ++i) { + unsigned f = pblocks[blocks[a.final_states()[i]]].get_representative(); + if (!new_final_set.contains(f)) { + new_final_set.insert(f); + new_final.push_back(f); + } + } - var res = Create(newInitState, newFinals, newMoves); - res.isDeterministic = true; - res.isEpsilonFree = true; - //res.EliminateDeadStates(); - return res; -#endif - - return 0; - + return alloc(automaton_t, m, new_init, new_final, new_moves); } template @@ -312,6 +285,9 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_produ if (a.is_final_state(a.init()) && b.is_final_state(b.init())) { final.push_back(0); } + if (false) { + mk_minimize(a); + } unsigned n = 1; moves_t mvsA, mvsB; while (!todo.empty()) { From 91d6b2cbbb969655d5ba55c5bc25f2b23f1907d2 Mon Sep 17 00:00:00 2001 From: Andres Notzli Date: Tue, 1 Mar 2016 00:21:10 -0800 Subject: [PATCH 07/11] [Z3py] Consistent behavior of eq and ne for FP Before, x == y and x != y were returning inconsistent expressions (i.e. `Not(x == y)` was not the same as `x != y`): >>> x = FP('x', Float32()) >>> y = FP('y', Float32()) >>> (x == y).sexpr() '(= x y)' >>> (x != y).sexpr() '(not (fp.eq x y))' `=` does not have the same semantics as `fp.eq` (e.g. `fp.eq` of +0.0 and -0.0 is true while it is false for `=`). This patch removes the __ne__ method from FPRef, so `x == y` and `x != y` use the inherited operations while fpEQ and fpNEQ can be used to refer to `fp.eq(..)`/`Not(fp.eq(..))`. --- src/api/python/z3.py | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 305733aa7..814198d22 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -8099,10 +8099,6 @@ class FPRef(ExprRef): def __gt__(self, other): return fpGT(self, other, self.ctx) - def __ne__(self, other): - return fpNEQ(self, other, self.ctx) - - def __add__(self, other): """Create the Z3 expression `self + other`. From 10ea36bfed4818320db66e68ab123459caaf201b Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 1 Mar 2016 10:00:58 +0000 Subject: [PATCH 08/11] fix build with gcc --- src/math/automata/symbolic_automata_def.h | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/math/automata/symbolic_automata_def.h b/src/math/automata/symbolic_automata_def.h index 87e0f7b2d..a7b076a2c 100644 --- a/src/math/automata/symbolic_automata_def.h +++ b/src/math/automata/symbolic_automata_def.h @@ -147,8 +147,9 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_minim } } uint_set relevant1; - u_map::iterator gend = gamma.end(); - for (u_map::iterator git = gamma.begin(); git != gend; ++git) { + typedef typename u_map::iterator gamma_iterator; + gamma_iterator gend = gamma.end(); + for (gamma_iterator git = gamma.begin(); git != gend; ++git) { unsigned p0A_index = blocks[git->m_key]; if (relevant1.contains(p0A_index)) { continue; @@ -156,7 +157,7 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_minim relevant1.insert(p0A_index); block& p0A = pblocks[p0A_index]; block p1; - for (u_map::iterator it = gamma.begin(); it != gend; ++it) { + for (iterator it = gamma.begin(); it != gend; ++it) { if (p0A.contains(it->m_key)) p1.insert(it->m_key); } @@ -166,7 +167,7 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_minim while (iterate) { iterate = false; uint_set relevant2; - for (u_map::iterator it = gamma.begin(); it != gend; ++it) { + for (gamma_iterator it = gamma.begin(); it != gend; ++it) { unsigned p0B_index = blocks[it->m_key]; if (pblocks[p0B_index].size() <= 1 || relevant2.contains(p0B_index)) { continue; @@ -239,7 +240,7 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_minim for (unsigned i = 0; i < a.num_states(); ++i) { unsigned src = pblocks[blocks[i]].get_representative(); - automaton_t::moves const& mvs = a.get_moves_from(i); + typename automaton_t::moves const& mvs = a.get_moves_from(i); for (unsigned j = 0; j < mvs.size(); ++j) { unsigned dst = pblocks[blocks[mvs[j].dst()]].get_representative(); unsigned_pair st(src, dst); From 33431ef9220e02b311ae3bf6f8479037af8ae92e Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 1 Mar 2016 10:02:24 +0000 Subject: [PATCH 09/11] fix build with gcc --- src/math/automata/symbolic_automata_def.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/automata/symbolic_automata_def.h b/src/math/automata/symbolic_automata_def.h index a7b076a2c..50c115d39 100644 --- a/src/math/automata/symbolic_automata_def.h +++ b/src/math/automata/symbolic_automata_def.h @@ -157,7 +157,7 @@ typename symbolic_automata::automaton_t* symbolic_automata::mk_minim relevant1.insert(p0A_index); block& p0A = pblocks[p0A_index]; block p1; - for (iterator it = gamma.begin(); it != gend; ++it) { + for (gamma_iterator it = gamma.begin(); it != gend; ++it) { if (p0A.contains(it->m_key)) p1.insert(it->m_key); } From 62e46aacd9819ac46aa5637fbb3272d3b2594b86 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 1 Mar 2016 11:31:08 +0000 Subject: [PATCH 10/11] bv_bounds: make may_simplify more precise to skip exprs with just 1 bound expr speedups up to 3x in selected benchmarks --- src/tactic/bv/bv_bounds_tactic.cpp | 63 ++++++++++++++++++++---------- 1 file changed, 42 insertions(+), 21 deletions(-) diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index 2d266aed8..e67c2470b 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -164,7 +164,7 @@ struct undo_bound { class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { typedef obj_map map; typedef obj_map expr_set; - typedef obj_map expr_list_map; + typedef obj_map expr_cnt; ast_manager& m; params_ref m_params; @@ -172,8 +172,8 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { bv_util m_bv; vector m_scopes; map m_bound; - expr_list_map m_expr_vars; - expr_set m_bound_exprs; + svector m_expr_vars; + svector m_bound_exprs; bool is_number(expr *e, uint64& n, unsigned& sz) const { rational r; @@ -233,7 +233,9 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { } expr_set* get_expr_vars(expr* t) { - expr_set*& entry = m_expr_vars.insert_if_not_there2(t, 0)->get_data().m_value; + unsigned id = t->get_id(); + m_expr_vars.reserve(id + 1); + expr_set*& entry = m_expr_vars[id]; if (entry) return entry; @@ -256,23 +258,33 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { return set; } - bool expr_has_bounds(expr* t) { - bool has_bounds = false; - if (m_bound_exprs.find(t, has_bounds)) - return has_bounds; + expr_cnt* get_expr_bounds(expr* t) { + unsigned id = t->get_id(); + m_bound_exprs.reserve(id + 1); + expr_cnt*& entry = m_bound_exprs[id]; + if (entry) + return entry; + + expr_cnt* set = alloc(expr_cnt); + entry = set; + + if (!is_app(t)) + return set; + + interval b; + expr* e; + if (is_bound(t, e, b)) { + set->insert_if_not_there2(e, 0)->get_data().m_value++; + } app* a = to_app(t); - if ((m_bv.is_bv_ule(t) || m_bv.is_bv_sle(t) || m.is_eq(t)) && - (m_bv.is_numeral(a->get_arg(0)) || m_bv.is_numeral(a->get_arg(1)))) { - has_bounds = true; + for (unsigned i = 0; i < a->get_num_args(); ++i) { + expr_cnt* set_arg = get_expr_bounds(a->get_arg(i)); + for (expr_cnt::iterator I = set_arg->begin(), E = set_arg->end(); I != E; ++I) { + set->insert_if_not_there2(I->m_key, 0)->get_data().m_value += I->m_value; + } } - - for (unsigned i = 0; !has_bounds && i < a->get_num_args(); ++i) { - has_bounds = expr_has_bounds(a->get_arg(i)); - } - - m_bound_exprs.insert(t, has_bounds); - return has_bounds; + return set; } public: @@ -289,8 +301,11 @@ public: } virtual ~bv_bounds_simplifier() { - for (expr_list_map::iterator I = m_expr_vars.begin(), E = m_expr_vars.end(); I != E; ++I) { - dealloc(I->m_value); + for (unsigned i = 0, e = m_expr_vars.size(); i < e; ++i) { + dealloc(m_expr_vars[i]); + } + for (unsigned i = 0, e = m_bound_exprs.size(); i < e; ++i) { + dealloc(m_bound_exprs[i]); } } @@ -393,7 +408,13 @@ public: if (is_bound(t, t1, b)) { return b.is_full() || m_bound.contains(t1); } - return expr_has_bounds(t); + + expr_cnt* bounds = get_expr_bounds(t); + for (expr_cnt::iterator I = bounds->begin(), E = bounds->end(); I != E; ++I) { + if (I->m_value > 1 || m_bound.contains(I->m_key)) + return true; + } + return false; } virtual void pop(unsigned num_scopes) { From c171170bedc4d519594aeb2d8415905d0dd10414 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 1 Mar 2016 15:31:20 +0000 Subject: [PATCH 11/11] Fixed FP string input conversions. Fixes #464 --- src/api/api_numeral.cpp | 6 ++++-- src/util/mpf.cpp | 15 ++++++++++++--- 2 files changed, 16 insertions(+), 5 deletions(-) diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index 770054870..491d9f597 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -68,8 +68,10 @@ extern "C" { (' ' == *m) || ('\n' == *m) || ('.' == *m) || ('e' == *m) || ('E' == *m) || - ('p' == *m && is_float) || - ('P' == *m && is_float))) { + (is_float && + ('p' == *m) || + ('P' == *m) || + ('+' == *m)))) { SET_ERROR_CODE(Z3_PARSER_ERROR); return 0; } diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 899b8635b..1d7ed1bb3 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -205,15 +205,23 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode // We expect [i].[f]P[e], where P means that the exponent is interpreted as 2^e instead of 10^e. std::string v(value); - size_t e_pos = v.find('p'); - if (e_pos == std::string::npos) e_pos = v.find('P'); std::string f, e; + bool sgn = false; + if (v.substr(0, 1) == "-") { + sgn = true; + v = v.substr(1); + } + else if (v.substr(0, 1) == "+") + v = v.substr(1); + + size_t e_pos = v.find('p'); + if (e_pos == std::string::npos) e_pos = v.find('P'); f = (e_pos != std::string::npos) ? v.substr(0, e_pos) : v; e = (e_pos != std::string::npos) ? v.substr(e_pos+1) : "0"; - TRACE("mpf_dbg", tout << " f = " << f << " e = " << e << std::endl;); + TRACE("mpf_dbg", tout << "sgn = " << sgn << " f = " << f << " e = " << e << std::endl;); scoped_mpq q(m_mpq_manager); m_mpq_manager.set(q, f.c_str()); @@ -222,6 +230,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode m_mpz_manager.set(ex, e.c_str()); set(o, ebits, sbits, rm, ex, q); + o.sign = sgn; TRACE("mpf_dbg", tout << "set: res = " << to_string(o) << std::endl;); }