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

use mk_ismt2_pp() instead of mk_bounded_pp()

Browse source
This commit is contained in:
Murphy Berzish 2015-09-28 02:09:35 -04:00
parent 87b5765e3d
commit 5fe129b571
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_str.cpp
View file

@ -171,7 +171,7 @@ void theory_str::instantiate_concat_axiom(enode * cat) {
// finally assert equality between the two subexpressions // finally assert equality between the two subexpressions
app * eq = m.mk_eq(len_xy, len_x_plus_len_y); app * eq = m.mk_eq(len_xy, len_x_plus_len_y);
SASSERT(eq); SASSERT(eq);
TRACE("t_str", tout << mk_bounded_pp(eq, m) << std::endl;); TRACE("t_str", tout << mk_ismt2_pp(eq, m) << std::endl;);
assert_axiom(eq); assert_axiom(eq);
} }
@ -219,7 +219,7 @@ void theory_str::instantiate_basic_string_axioms(enode * str) {
app * lhs_ge_rhs = m_autil.mk_ge(len_str, zero); app * lhs_ge_rhs = m_autil.mk_ge(len_str, zero);
SASSERT(lhs_ge_rhs); SASSERT(lhs_ge_rhs);
// TODO verify that this works // TODO verify that this works
TRACE("t_str_detail", tout << "string axiom 1: " << mk_bounded_pp(lhs_ge_rhs, m) << std::endl;); TRACE("t_str_detail", tout << "string axiom 1: " << mk_ismt2_pp(lhs_ge_rhs, m) << std::endl;);
assert_axiom(lhs_ge_rhs); assert_axiom(lhs_ge_rhs);
} }
@ -243,7 +243,7 @@ void theory_str::instantiate_basic_string_axioms(enode * str) {
rhs = ctx.mk_eq_atom(a_str, empty_str); rhs = ctx.mk_eq_atom(a_str, empty_str);
SASSERT(rhs); SASSERT(rhs);
// build LHS <=> RHS and assert // build LHS <=> RHS and assert
TRACE("t_str_detail", tout << "string axiom 2: " << mk_bounded_pp(lhs, m) << " <=> " << mk_bounded_pp(rhs, m) << std::endl;); TRACE("t_str_detail", tout << "string axiom 2: " << mk_ismt2_pp(lhs, m) << " <=> " << mk_ismt2_pp(rhs, m) << std::endl;);
literal l(mk_eq(lhs, rhs, true)); literal l(mk_eq(lhs, rhs, true));
ctx.mark_as_relevant(l); ctx.mark_as_relevant(l);
ctx.mk_th_axiom(get_id(), 1, &l); ctx.mk_th_axiom(get_id(), 1, &l);
@ -275,7 +275,7 @@ void theory_str::instantiate_str_eq_length_axiom(enode * lhs, enode * rhs) {
// build (premise -> conclusion) and assert // build (premise -> conclusion) and assert
expr_ref axiom(m.mk_implies(premise, conclusion), m); expr_ref axiom(m.mk_implies(premise, conclusion), m);
TRACE("t_str_detail", tout << "string-eq length-eq axiom: " << mk_bounded_pp(axiom, m) << std::endl;); TRACE("t_str_detail", tout << "string-eq length-eq axiom: " << mk_ismt2_pp(axiom, m) << std::endl;);
assert_axiom(axiom); assert_axiom(axiom);
} }