mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-09 12:50:32 +00:00
Code Activity

assert string axiom 2

Browse source
This commit is contained in:
Murphy Berzish 2015-09-27 00:12:04 -04:00
parent 4085db9990
commit 91e9cf272a
1 changed files with 2 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_str.cpp
View file

@ -224,7 +224,6 @@ void theory_str::instantiate_basic_string_axioms(enode * str) {
assert_axiom(lhs_ge_rhs); assert_axiom(lhs_ge_rhs);
} }
/*
// build axiom 2: Length(a_str) == 0 <=> a_str == "" // build axiom 2: Length(a_str) == 0 <=> a_str == ""
{ {
// build LHS of iff // build LHS of iff
@ -246,12 +245,11 @@ void theory_str::instantiate_basic_string_axioms(enode * 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_bounded_pp(lhs, m) << " <=> " << mk_bounded_pp(rhs, m) << std::endl;);
// TODO this is kind of a hack, maybe just ctx.assert_expr() will be enough?
literal l(mk_eq(lhs, rhs, true)); literal l(mk_eq(lhs, rhs, true));
ctx.mark_as_relevant(l); ctx.mark_as_relevant(l);
assert_axiom(l); ctx.mk_th_axiom(get_id(), 1, &l);
} }
*/
} }
} }