mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 01:18:45 +00:00
Code Activity

fix build with gcc 5

Browse source
This commit is contained in:
Nuno Lopes 2016-02-29 14:34:48 +00:00
parent 7656adc483
commit 006dc147a8
3 changed files with 11 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/ast/rewriter/seq_rewriter.cpp
View file

@ -93,29 +93,29 @@ public:
} }
if (m.are_distinct(x->get_char(), y->get_char())) { if (m.are_distinct(x->get_char(), y->get_char())) {
expr_ref fml(m.mk_false(), m); expr_ref fml(m.mk_false(), m);
return sym_expr::mk_pred(fml, x->sort()); return sym_expr::mk_pred(fml, x->get_sort());
} }
} }
var_ref v(m.mk_var(0, x->sort()), m); var_ref v(m.mk_var(0, x->get_sort()), m);
expr_ref fml1 = x->accept(v); expr_ref fml1 = x->accept(v);
expr_ref fml2 = y->accept(v); expr_ref fml2 = y->accept(v);
if (m.is_true(fml1)) return y; if (m.is_true(fml1)) return y;
if (m.is_true(fml2)) return x; if (m.is_true(fml2)) return x;
expr_ref fml(m.mk_and(fml1, fml2), m); expr_ref fml(m.mk_and(fml1, fml2), m);
return sym_expr::mk_pred(fml, x->sort()); return sym_expr::mk_pred(fml, x->get_sort());
} }
virtual T mk_or(T x, T y) { virtual T mk_or(T x, T y) {
if (x->is_char() && y->is_char() && if (x->is_char() && y->is_char() &&
x->get_char() == y->get_char()) { x->get_char() == y->get_char()) {
return x; return x;
} }
var_ref v(m.mk_var(0, x->sort()), m); var_ref v(m.mk_var(0, x->get_sort()), m);
expr_ref fml1 = x->accept(v); expr_ref fml1 = x->accept(v);
expr_ref fml2 = y->accept(v); expr_ref fml2 = y->accept(v);
if (m.is_false(fml1)) return y; if (m.is_false(fml1)) return y;
if (m.is_false(fml2)) return x; if (m.is_false(fml2)) return x;
expr_ref fml(m.mk_or(fml1, fml2), m); expr_ref fml(m.mk_or(fml1, fml2), m);
return sym_expr::mk_pred(fml, x->sort()); return sym_expr::mk_pred(fml, x->get_sort());
} }
virtual T mk_and(unsigned sz, T const* ts) { virtual T mk_and(unsigned sz, T const* ts) {
@ -151,7 +151,7 @@ public:
if (x->is_range()) { if (x->is_range()) {
// TBD check lower is below upper. // TBD check lower is below upper.
} }
expr_ref v(m.mk_fresh_const("x", x->sort()), m); expr_ref v(m.mk_fresh_const("x", x->get_sort()), m);
expr_ref fml = x->accept(v); expr_ref fml = x->accept(v);
if (m.is_true(fml)) { if (m.is_true(fml)) {
return l_true; return l_true;
@ -162,9 +162,9 @@ public:
return m_solver.check_sat(fml); return m_solver.check_sat(fml);
} }
virtual T mk_not(T x) { virtual T mk_not(T x) {
var_ref v(m.mk_var(0, x->sort()), m); var_ref v(m.mk_var(0, x->get_sort()), m);
expr_ref fml(m.mk_not(x->accept(v)), m); expr_ref fml(m.mk_not(x->accept(v)), m);
return sym_expr::mk_pred(fml, x->sort()); return sym_expr::mk_pred(fml, x->get_sort());
} }
}; };

2
src/ast/rewriter/seq_rewriter.h
View file

@ -51,7 +51,7 @@ public:
bool is_char() const { return m_ty == t_char; } bool is_char() const { return m_ty == t_char; }
bool is_pred() const { return !is_char(); } bool is_pred() const { return !is_char(); }
bool is_range() const { return m_ty == t_range; } bool is_range() const { return m_ty == t_range; }
sort* sort() const { return m_sort; } sort* get_sort() const { return m_sort; }
expr* get_char() const { SASSERT(is_char()); return m_t; } expr* get_char() const { SASSERT(is_char()); return m_t; }
}; };

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

@ -32,14 +32,14 @@ typedef std::pair<unsigned, unsigned> unsigned_pair;
template<class T, class M> template<class T, class M>
typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_total(automaton_t& a) { typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_total(automaton_t& a) {
unsigned dead_state = a.num_states(); unsigned dead_state = a.num_states();
moves_t 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(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) {
mv.push_back(mvs[j]()); vs.push_back(mvs[j]());
} }
ref_t cond(m_ba.mk_not(m_ba.mk_or(vs.size(), vs.c_ptr())), m); ref_t cond(m_ba.mk_not(m_ba.mk_or(vs.size(), vs.c_ptr())), m);
lbool is_sat = m_ba.is_sat(cond); lbool is_sat = m_ba.is_sat(cond);