mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

minor simplifications

Browse source
This commit is contained in:
Nuno Lopes 2020-05-31 13:26:27 +01:00
parent 07e5b228a2
commit 31e75d1401
3 changed files with 23 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/smt_context.h
View file

@ -731,13 +731,13 @@ namespace smt {
typedef std::pair<expr *, bool> expr_bool_pair; typedef std::pair<expr *, bool> expr_bool_pair;
void ts_visit_child(expr * n, bool gate_ctx, svector<int> & tcolors, svector<int> & fcolors, svector<expr_bool_pair> & todo, bool & visited); void ts_visit_child(expr * n, bool gate_ctx, svector<expr_bool_pair> & todo, bool & visited);
bool ts_visit_children(expr * n, bool gate_ctx, svector<int> & tcolors, svector<int> & fcolors, svector<expr_bool_pair> & todo); bool ts_visit_children(expr * n, bool gate_ctx, svector<expr_bool_pair> & todo);
svector<expr_bool_pair> ts_todo; svector<expr_bool_pair> ts_todo;
svector<int> tcolors; char_vector tcolors;
svector<int> fcolors; char_vector fcolors;
void top_sort_expr(expr * n, svector<expr_bool_pair> & sorted_exprs); void top_sort_expr(expr * n, svector<expr_bool_pair> & sorted_exprs);

32
src/smt/smt_internalizer.cpp
View file

@ -29,7 +29,7 @@ namespace smt {
/** /**
\brief Return true if the expression is viewed as a logical gate. \brief Return true if the expression is viewed as a logical gate.
*/ */
inline bool is_gate(ast_manager const & m, expr * n) { static bool is_gate(ast_manager const & m, expr * n) {
if (is_app(n) && to_app(n)->get_family_id() == m.get_basic_family_id()) { if (is_app(n) && to_app(n)->get_family_id() == m.get_basic_family_id()) {
switch (to_app(n)->get_decl_kind()) { switch (to_app(n)->get_decl_kind()) {
case OP_AND: case OP_AND:
@ -45,19 +45,19 @@ namespace smt {
return false; return false;
} }
#define White 0 #define White 0
#define Grey 1 #define Grey 1
#define Black 2 #define Black 2
static int get_color(svector<int> & tcolors, svector<int> & fcolors, expr * n, bool gate_ctx) { static char get_color(char_vector & tcolors, char_vector & fcolors, expr * n, bool gate_ctx) {
svector<int> & colors = gate_ctx ? tcolors : fcolors; char_vector & colors = gate_ctx ? tcolors : fcolors;
if (colors.size() > n->get_id()) if (colors.size() > n->get_id())
return colors[n->get_id()]; return colors[n->get_id()];
return White; return White;
} }
static void set_color(svector<int> & tcolors, svector<int> & fcolors, expr * n, bool gate_ctx, int color) { static void set_color(char_vector & tcolors, char_vector & fcolors, expr * n, bool gate_ctx, char color) {
svector<int> & colors = gate_ctx ? tcolors : fcolors; char_vector & colors = gate_ctx ? tcolors : fcolors;
if (colors.size() <= n->get_id()) { if (colors.size() <= n->get_id()) {
colors.resize(n->get_id()+1, White); colors.resize(n->get_id()+1, White);
} }
@ -99,14 +99,14 @@ namespace smt {
} }
} }
void context::ts_visit_child(expr * n, bool gate_ctx, svector<int> & tcolors, svector< int> & fcolors, svector<expr_bool_pair> & todo, bool & visited) { void context::ts_visit_child(expr * n, bool gate_ctx, svector<expr_bool_pair> & todo, bool & visited) {
if (get_color(tcolors, fcolors, n, gate_ctx) == White) { if (get_color(tcolors, fcolors, n, gate_ctx) == White) {
todo.push_back(expr_bool_pair(n, gate_ctx)); todo.push_back(expr_bool_pair(n, gate_ctx));
visited = false; visited = false;
} }
} }
bool context::ts_visit_children(expr * n, bool gate_ctx, svector<int> & tcolors, svector<int> & fcolors, svector<expr_bool_pair> & todo) { bool context::ts_visit_children(expr * n, bool gate_ctx, svector<expr_bool_pair> & todo) {
if (is_quantifier(n)) if (is_quantifier(n))
return true; return true;
SASSERT(is_app(n)); SASSERT(is_app(n));
@ -127,7 +127,7 @@ namespace smt {
ptr_buffer<expr> descendants; ptr_buffer<expr> descendants;
get_foreign_descendants(to_app(n), fid, descendants); get_foreign_descendants(to_app(n), fid, descendants);
for (expr * arg : descendants) { for (expr * arg : descendants) {
ts_visit_child(arg, false, tcolors, fcolors, todo, visited); ts_visit_child(arg, false, todo, visited);
} }
return visited; return visited;
} }
@ -135,9 +135,9 @@ namespace smt {
SASSERT(def_int); SASSERT(def_int);
if (m.is_term_ite(n)) { if (m.is_term_ite(n)) {
ts_visit_child(to_app(n)->get_arg(0), true, tcolors, fcolors, todo, visited); ts_visit_child(to_app(n)->get_arg(0), true, todo, visited);
ts_visit_child(to_app(n)->get_arg(1), false, tcolors, fcolors, todo, visited); ts_visit_child(to_app(n)->get_arg(1), false, todo, visited);
ts_visit_child(to_app(n)->get_arg(2), false, tcolors, fcolors, todo, visited); ts_visit_child(to_app(n)->get_arg(2), false, todo, visited);
return visited; return visited;
} }
bool new_gate_ctx = m.is_bool(n) && (is_gate(m, n) || m.is_not(n)); bool new_gate_ctx = m.is_bool(n) && (is_gate(m, n) || m.is_not(n));
@ -145,7 +145,7 @@ namespace smt {
while (j > 0) { while (j > 0) {
--j; --j;
expr * arg = to_app(n)->get_arg(j); expr * arg = to_app(n)->get_arg(j);
ts_visit_child(arg, new_gate_ctx, tcolors, fcolors, todo, visited); ts_visit_child(arg, new_gate_ctx, todo, visited);
} }
return visited; return visited;
} }
@ -162,10 +162,10 @@ namespace smt {
switch (get_color(tcolors, fcolors, curr, gate_ctx)) { switch (get_color(tcolors, fcolors, curr, gate_ctx)) {
case White: case White:
set_color(tcolors, fcolors, curr, gate_ctx, Grey); set_color(tcolors, fcolors, curr, gate_ctx, Grey);
ts_visit_children(curr, gate_ctx, tcolors, fcolors, ts_todo); ts_visit_children(curr, gate_ctx, ts_todo);
break; break;
case Grey: case Grey:
SASSERT(ts_visit_children(curr, gate_ctx, tcolors, fcolors, ts_todo)); SASSERT(ts_visit_children(curr, gate_ctx, ts_todo));
set_color(tcolors, fcolors, curr, gate_ctx, Black); set_color(tcolors, fcolors, curr, gate_ctx, Black);
if (n != curr && !m.is_not(curr)) if (n != curr && !m.is_not(curr))
sorted_exprs.push_back(expr_bool_pair(curr, gate_ctx)); sorted_exprs.push_back(expr_bool_pair(curr, gate_ctx));

8
src/smt/theory_fpa.cpp
View file

@ -380,7 +380,7 @@ namespace smt {
for (expr* arg : m_converter.m_extra_assertions) { for (expr* arg : m_converter.m_extra_assertions) {
ctx.get_rewriter()(arg, t, t_pr); ctx.get_rewriter()(arg, t, t_pr);
fmls.push_back(t); fmls.push_back(std::move(t));
} }
m_converter.m_extra_assertions.reset(); m_converter.m_extra_assertions.reset();
res = m.mk_and(fmls); res = m.mk_and(fmls);
@ -440,8 +440,7 @@ namespace smt {
for (unsigned i = 0; i < num_args; i++) for (unsigned i = 0; i < num_args; i++)
ctx.internalize(term->get_arg(i), false); ctx.internalize(term->get_arg(i), false);
enode * e = (ctx.e_internalized(term)) ? ctx.get_enode(term) : enode * e = ctx.mk_enode(term, false, false, true);
ctx.mk_enode(term, false, false, true);
if (!is_attached_to_var(e)) { if (!is_attached_to_var(e)) {
attach_new_th_var(e); attach_new_th_var(e);
@ -457,8 +456,7 @@ namespace smt {
case OP_FPA_TO_SBV: case OP_FPA_TO_SBV:
case OP_FPA_TO_REAL: case OP_FPA_TO_REAL:
case OP_FPA_TO_IEEE_BV: { case OP_FPA_TO_IEEE_BV: {
expr_ref conv(m); expr_ref conv = convert(term);
conv = convert(term);
expr_ref eq(m.mk_eq(term, conv), m); expr_ref eq(m.mk_eq(term, conv), m);
assert_cnstr(eq); assert_cnstr(eq);
assert_cnstr(mk_side_conditions()); assert_cnstr(mk_side_conditions());