3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-04-30 19:04:02 -07:00
parent bd46c52f95
commit 606754c09a
3 changed files with 37 additions and 51 deletions

View file

@ -348,6 +348,7 @@ public:
//
void compress() {
SASSERT(!m_delta.empty());
TRACE("seq", display(tout););
for (unsigned i = 0; i < m_delta.size(); ++i) {
for (unsigned j = 0; j < m_delta[i].size(); ++j) {
move const& mv = m_delta[i][j];
@ -460,6 +461,7 @@ public:
}
}
sinkify_dead_states();
TRACE("seq", display(tout););
}
bool is_sequence(unsigned& length) const {
@ -559,9 +561,8 @@ public:
template<class D>
std::ostream& display(std::ostream& out, D& displayer = D()) const {
out << "init: " << init() << "\n";
out << "final: ";
for (unsigned i = 0; i < m_final_states.size(); ++i) out << m_final_states[i] << " ";
out << "\n";
out << "final: " << m_final_states << "\n";
for (unsigned i = 0; i < m_delta.size(); ++i) {
moves const& mvs = m_delta[i];
for (move const& mv : mvs) {
@ -577,6 +578,22 @@ public:
}
private:
std::ostream& display(std::ostream& out) const {
out << "init: " << init() << "\n";
out << "final: " << m_final_states << "\n";
for (unsigned i = 0; i < m_delta.size(); ++i) {
moves const& mvs = m_delta[i];
for (move const& mv : mvs) {
out << i << " -> " << mv.dst() << " ";
if (mv.t()) {
out << "if *** ";
}
out << "\n";
}
}
return out;
}
void sinkify_dead_states() {
uint_set dead_states;
for (unsigned i = 0; i < m_delta.size(); ++i) {
@ -604,7 +621,9 @@ private:
}
to_remove.reset();
}
TRACE("seq", tout << "remove: " << dead_states << "\n";);
TRACE("seq", tout << "remove: " << dead_states << "\n";
tout << "final: " << m_final_states << "\n";
);
for (unsigned s : dead_states) {
CTRACE("seq", !m_delta[s].empty(), tout << "live state " << s << "\n";);
m_delta[s].reset();

View file

@ -379,9 +379,21 @@ typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_produ
pair2id.insert(init_pair, 0);
moves_t mvs;
unsigned_vector final;
if (a.is_final_state(a.init()) && b.is_final_state(b.init())) {
final.push_back(0);
unsigned_vector a_init, b_init;
a.get_epsilon_closure(a.init(), a_init);
for (unsigned ia : a_init) {
if (a.is_final_state(ia)) {
b.get_epsilon_closure(b.init(), b_init);
for (unsigned ib : b_init) {
if (b.is_final_state(ib)) {
final.push_back(0);
break;
}
}
break;
}
}
unsigned n = 1;
moves_t mvsA, mvsB;
while (!todo.empty()) {

View file

@ -1,45 +0,0 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
critical flet.cpp
Abstract:
Version of flet using "omp critical" directive.
Warning: it uses omp critical section "critical_flet"
Author:
Leonardo de Moura (leonardo) 2011-05-12
Revision History:
--*/
#ifndef CRITICAL_FLET_H_
#define CRITICAL_FLET_H_
template<typename T>
class critical_flet {
T & m_ref;
T m_old_value;
public:
critical_flet(T & ref, const T & new_value):
m_ref(ref),
m_old_value(ref) {
#pragma omp critical (critical_flet)
{
m_ref = new_value;
}
}
~critical_flet() {
#pragma omp critical (critical_flet)
{
m_ref = m_old_value;
}
}
};
#endif