mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3 into 4tXJ7f-fix_build

Browse source 
# Conflicts:
#	src/math/automata/symbolic_automata_def.h
This commit is contained in:
Christoph M. Wintersteiger 2016-03-01 14:05:19 +00:00
commit 5c35a07a46
3 changed files with 199 additions and 201 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/math/automata/symbolic_automata.h
View file

@ -79,16 +79,18 @@ class symbolic_automata {
return m_rep; 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 contains(unsigned i) const { return m_set.contains(i); }
bool is_empty() const { return m_set.empty(); } bool is_empty() const { return m_set.empty(); }
unsigned size() const { return m_set.num_elems(); } unsigned size() const { return m_set.num_elems(); }
void remove(unsigned i) { m_set.remove(i); m_rep_chosen = false; } void remove(unsigned i) { m_set.remove(i); m_rep_chosen = false; }
void clear() { m_set.reset(); m_rep_chosen = false; } void clear() { m_set.reset(); m_rep_chosen = false; }
uint_set::iterator begin() { return m_set.begin(); } uint_set::iterator begin() const { return m_set.begin(); }
uint_set::iterator end() { return m_set.end(); } uint_set::iterator end() const { return m_set.end(); }
}; };
void add_block(block const& p1, unsigned p0_index, unsigned_vector& blocks, vector<block>& pblocks, unsigned_vector& W);
public: public:
symbolic_automata(M& m, ba_t& ba): m(m), m_ba(ba) {} symbolic_automata(M& m, ba_t& ba): m(m), m_ba(ba) {}
automaton_t* mk_determinstic(automaton_t& a); automaton_t* mk_determinstic(automaton_t& a);

329
src/math/automata/symbolic_automata_def.h
View file

@ -35,7 +35,7 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_total
moves_t mvs, new_mvs; moves_t mvs, new_mvs;
for (unsigned i = 0; i < dead_state; ++i) { for (unsigned i = 0; i < dead_state; ++i) {
mvs.reset(); mvs.reset();
a.get_moves(i, mvs, true); a.get_moves_from(i, mvs, true);
refs_t vs(m); refs_t vs(m);
for (unsigned j = 0; j < mvs.size(); ++j) { for (unsigned j = 0; j < mvs.size(); ++j) {
@ -54,7 +54,8 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_total
return a.clone(); return a.clone();
} }
new_mvs.push_back(move_t(m, dead_state, dead_state, m_ba.mk_true())); 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); return alloc(automaton_t, m, a.init(), a.final_states(), new_mvs);
} }
@ -79,48 +80,64 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_minim
template<class T, class M> template<class T, class M>
typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_minimize_total(automaton_t& fa) { void symbolic_automata<T, M>::add_block(block const& p1, unsigned p0_index, unsigned_vector& blocks, vector<block>& pblocks, unsigned_vector& W) {
vector<block> pblocks; block& p0 = pblocks[p0_index];
unsigned_vector blocks; if (p1.size() < p0.size()) {
block final_block(fa->final_states()); unsigned p1_index = pblocks.size();
block non_final_block(fa->non_final_states()); pblocks.push_back(p1);
pblocks.push_back(block(fa->final_states())); // 0 |-> final states for (uint_set::iterator it = p1.begin(), end = p1.end(); it != end; ++it) {
// pblocks.push_back(block(fa->non_final_states()); // 1 |-> non-final states p0.remove(*it);
for (unsigned i = 0; i < fa->num_states(); ++i) { blocks[*it] = p1_index;
if (fa->is_final_state(i)) { }
blocks.push_back(0); if (W.contains(p0_index)) {
W.push_back(p1_index);
}
else if (p0.size() <= p1.size()) {
W.push_back(p0_index);
} }
else { else {
W.push_back(p1_index);
}
}
}
template<class T, class M>
typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_minimize_total(automaton_t& a) {
vector<block> pblocks;
unsigned_vector blocks;
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); blocks.push_back(1);
} }
else {
blocks.push_back(0);
}
} }
vector<block> W; pblocks.push_back(block(a.final_states())); // 0 |-> final states
if (final_block.size() > non_final_block.size()) { pblocks.push_back(block(non_final)); // 1 |-> non-final states
W.push_back(1);
} unsigned_vector W;
else { W.push_back(pblocks[0].size() > pblocks[1].size() ? 1 : 0);
W.push_back(0);
}
#if 0
refs_t trail(m); refs_t trail(m);
u_map<T*> gamma; u_map<T*> gamma;
moves_t mvs; moves_t mvs;
while (!W.empty()) { while (!W.empty()) {
block R(pblocks[W.back()]); block R(pblocks[W.back()]);
W.pop_back(); W.pop_back();
block Rcopy(R);
gamma.reset(); gamma.reset();
uint_set::iterator it = Rcopy.begin(), end = Rcopy.end(); uint_set::iterator it = R.begin(), end = R.end();
for (; it != end; ++it) { for (; it != end; ++it) {
unsigned q = *it; unsigned dst = *it;
mvs.reset(); mvs.reset();
fa->get_moves_to(q, mvs); a.get_moves_to(dst, mvs);
for (unsigned i = 0; i < mvs.size(); ++i) { for (unsigned i = 0; i < mvs.size(); ++i) {
unsigned src = mvs[i].src(); unsigned src = mvs[i].src();
if (pblocks[src].size() > 1) { if (pblocks[src].size() > 1) {
T* t = mvs[i](); T* t = mvs[i].t();
T* t1;
if (gamma.find(src, t1)) { if (gamma.find(src, t1)) {
t = m_ba.mk_or(t, t1); t = m_ba.mk_or(t, t1);
trail.push_back(t); trail.push_back(t);
@ -129,177 +146,132 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_minim
} }
} }
} }
uint_set relevant; uint_set relevant1;
u_map<T*>::iterator gend = gamma.end(); typedef typename u_map<T*>::iterator gamma_iterator;
for (u_map<T*>::iterator it = gamma.begin(); it != gend; ++it) { gamma_iterator gend = gamma.end();
relevant.insert(blocks[it->m_key]); for (gamma_iterator git = gamma.begin(); git != gend; ++git) {
} unsigned p0A_index = blocks[git->m_key];
uint_set::iterator uit = relevant.begin(), uend = relevant.end(); if (relevant1.contains(p0A_index)) {
for (; uit != uend; ++uit) { continue;
unsigned p0_index = *uit;
block& p0 = pblocks[p0_index];
block p1;
for (u_map<T*>::iterator it = gamma.begin(); it != gend; ++it) {
if (p0.contains(*it)) p1.push_back(*it);
} }
if (p1.size() < p0.size()) { relevant1.insert(p0A_index);
unsigned p1_index = pblocks.size(); block& p0A = pblocks[p0A_index];
pblocks.push_back(p1); block p1;
for (uint_set::iterator it = p1.begin(), end = p1.end(); it != end; ++it) { for (gamma_iterator it = gamma.begin(); it != gend; ++it) {
p0.remove(*it); if (p0A.contains(it->m_key)) p1.insert(it->m_key);
blocks[*it] = p1_index; }
}
if (W.contains(p0_index)) { add_block(p1, p0A_index, blocks, pblocks, W);
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; bool iterate = true;
while (iterate) { while (iterate) {
iterate = false; iterate = false;
uint_set relevant; uint_set relevant2;
for (u_map<T*>::iterator it = gamma.begin(); it != gend; ++it) { for (gamma_iterator it = gamma.begin(); it != gend; ++it) {
if (pblocks[blocks[it->m_key]].size() > 1) { unsigned p0B_index = blocks[it->m_key];
relevant.insert(blocks[it->m_key]); if (pblocks[p0B_index].size() <= 1 || relevant2.contains(p0B_index)) {
continue;
} }
} relevant2.insert(p0B_index);
uint_set::iterator it = relevant.begin(), end = relevant.end(); block const& p0B = pblocks[p0B_index];
for (; it != end; ++it) { uint_set::iterator bi = p0B.begin(), be = p0B.end();
block const& p = pblocks[*it];
uint_set::iterator bi = p.begin(), be = p.end();
block p1; block p1;
p1.insert(*bi); p1.insert(*bi);
// psi = gamma[*bi]; // name of key or block? bool split_found = false;
ref_t psi(gamma[*bi], m);
++bi; ++bi;
for (; bi != be; ++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 unsigned new_init = pblocks[blocks[a.init()]].get_representative();
Func<T, T, T> MkDiff = (x, y) => solver.MkAnd(x, solver.MkNot(y));
while (!W.IsEmpty) // set moves
{ map<unsigned_pair, T*, pair_hash<unsigned_hash, unsigned_hash>, default_eq<unsigned_pair> > conds;
//keep using Bcopy until no more changes occur svector<unsigned_pair> keys;
//effectively, this replaces the loop over characters moves_t new_moves;
bool iterate = true;
//in each relevant block all states lead to B due to the initial splitting
//only relevant blocks are potentially split for (unsigned i = 0; i < a.num_states(); ++i) {
foreach (var P in relevant2) unsigned src = pblocks[blocks[i]].get_representative();
{ typename automaton_t::moves const& mvs = a.get_moves_from(i);
var PE = P.GetEnumerator(); for (unsigned j = 0; j < mvs.size(); ++j) {
PE.MoveNext(); unsigned dst = pblocks[blocks[mvs[j].dst()]].get_representative();
unsigned_pair st(src, dst);
var P1 = new Block(); T* t = 0;
bool splitFound = false; if (conds.find(st, t)) {
t = m_ba.mk_or(t, mvs[j].t());
var psi = Gamma[PE.Current]; trail.push_back(t);
P1.Add(PE.Current); //C has at least 2 elements conds.insert(st, t);
#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
}
}
} }
else {
Dictionary<Pair<int, int>, HashSet<T>> condMap = new Dictionary<Pair<int, int>, HashSet<T>>(); conds.insert(st, mvs[j].t());
foreach (var move in GetMoves()) keys.push_back(st);
{
int s = Blocks[move.SourceState].GetRepresentative();
int t = Blocks[move.TargetState].GetRepresentative();
var st = new Pair<int, int>(s, t);
HashSet<T> condSet;
if (!condMap.TryGetValue(st, out condSet))
{
condSet = new HashSet<T>();
condSet.Add(move.Label);
condMap[st] = condSet;
}
else
condSet.Add(move.Label);
} }
int newInitState = Blocks[fa.InitialState].GetRepresentative(); }
var newMoves = new List<Move<T>>(); }
var newFinals = new HashSet<int>(); for (unsigned i = 0; i < keys.size(); ++i) {
foreach (var entry in condMap) unsigned_pair st = keys[i];
newMoves.Add(Move<T>.Create(entry.Key.First, entry.Key.Second, solver.MkOr(entry.Value))); new_moves.push_back(move_t(m, st.first, st.second, conds[st]));
foreach (var f in GetFinalStates()) }
newFinals.Add(Blocks[f].GetRepresentative()); // 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); return alloc(automaton_t, m, new_init, new_final, new_moves);
res.isDeterministic = true;
res.isEpsilonFree = true;
//res.EliminateDeadStates();
return res;
#endif
return 0;
} }
template<class T, class M> template<class T, class M>
@ -314,6 +286,9 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_produ
if (a.is_final_state(a.init()) && b.is_final_state(b.init())) { if (a.is_final_state(a.init()) && b.is_final_state(b.init())) {
final.push_back(0); final.push_back(0);
} }
if (false) {
mk_minimize(a);
}
unsigned n = 1; unsigned n = 1;
moves_t mvsA, mvsB; moves_t mvsA, mvsB;
while (!todo.empty()) { while (!todo.empty()) {

63
src/tactic/bv/bv_bounds_tactic.cpp
View file

@ -164,7 +164,7 @@ struct undo_bound {
class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
typedef obj_map<expr, interval> map; typedef obj_map<expr, interval> map;
typedef obj_map<expr, bool> expr_set; typedef obj_map<expr, bool> expr_set;
typedef obj_map<expr, expr_set*> expr_list_map; typedef obj_map<expr, unsigned> expr_cnt;
ast_manager& m; ast_manager& m;
params_ref m_params; params_ref m_params;
@ -172,8 +172,8 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
bv_util m_bv; bv_util m_bv;
vector<undo_bound> m_scopes; vector<undo_bound> m_scopes;
map m_bound; map m_bound;
expr_list_map m_expr_vars; svector<expr_set*> m_expr_vars;
expr_set m_bound_exprs; svector<expr_cnt*> m_bound_exprs;
bool is_number(expr *e, uint64& n, unsigned& sz) const { bool is_number(expr *e, uint64& n, unsigned& sz) const {
rational r; rational r;
@ -233,7 +233,9 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
} }
expr_set* get_expr_vars(expr* t) { 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) if (entry)
return entry; return entry;
@ -256,23 +258,33 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
return set; return set;
} }
bool expr_has_bounds(expr* t) { expr_cnt* get_expr_bounds(expr* t) {
bool has_bounds = false; unsigned id = t->get_id();
if (m_bound_exprs.find(t, has_bounds)) m_bound_exprs.reserve(id + 1);
return has_bounds; 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); app* a = to_app(t);
if ((m_bv.is_bv_ule(t) || m_bv.is_bv_sle(t) || m.is_eq(t)) && for (unsigned i = 0; i < a->get_num_args(); ++i) {
(m_bv.is_numeral(a->get_arg(0)) || m_bv.is_numeral(a->get_arg(1)))) { expr_cnt* set_arg = get_expr_bounds(a->get_arg(i));
has_bounds = true; 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;
}
} }
return set;
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;
} }
public: public:
@ -289,8 +301,11 @@ public:
} }
virtual ~bv_bounds_simplifier() { virtual ~bv_bounds_simplifier() {
for (expr_list_map::iterator I = m_expr_vars.begin(), E = m_expr_vars.end(); I != E; ++I) { for (unsigned i = 0, e = m_expr_vars.size(); i < e; ++i) {
dealloc(I->m_value); 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)) { if (is_bound(t, t1, b)) {
return b.is_full() || m_bound.contains(t1); 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) { virtual void pop(unsigned num_scopes) {