mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-04 18:30:24 +00:00
Code Activity

create helper function theory_str::assert_implication()

Browse source
This commit is contained in:
Murphy Berzish 2015-09-28 03:26:46 -04:00
parent bccadedfee
commit 62cd633b63
2 changed files with 15 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/smt/theory_str.cpp
View file

@ -34,10 +34,9 @@ theory_str::theory_str(ast_manager & m):
theory_str::~theory_str() { theory_str::~theory_str() {
} }
void theory_str::assert_axiom(ast * a) { void theory_str::assert_axiom(expr * e) {
expr * e = to_expr(a);
if (get_manager().is_true(e)) return; if (get_manager().is_true(e)) return;
TRACE("t_str_detail", tout << "asserting " << mk_ismt2_pp(a, get_manager()) << "\n";); TRACE("t_str_detail", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << "\n";);
context & ctx = get_context(); context & ctx = get_context();
if (!ctx.b_internalized(e)) { if (!ctx.b_internalized(e)) {
ctx.internalize(e, true); ctx.internalize(e, true);
@ -45,7 +44,13 @@ void theory_str::assert_axiom(ast * a) {
literal lit(ctx.get_literal(e)); literal lit(ctx.get_literal(e));
ctx.mark_as_relevant(lit); ctx.mark_as_relevant(lit);
ctx.mk_th_axiom(get_id(), 1, &lit); ctx.mk_th_axiom(get_id(), 1, &lit);
TRACE("t_str_detail", tout << "done asserting " << mk_ismt2_pp(a, get_manager()) << "\n";); TRACE("t_str_detail", tout << "done asserting " << mk_ismt2_pp(e, get_manager()) << "\n";);
}
void theory_str::assert_implication(expr * premise, expr * conclusion) {
ast_manager & m = get_manager();
expr_ref axiom(m.mk_or(m.mk_not(premise), conclusion), m);
assert_axiom(axiom);
} }
bool theory_str::internalize_atom(app * atom, bool gate_ctx) { bool theory_str::internalize_atom(app * atom, bool gate_ctx) {
@ -275,10 +280,9 @@ void theory_str::instantiate_str_eq_length_axiom(enode * lhs, enode * rhs) {
SASSERT(len_rhs); SASSERT(len_rhs);
expr_ref conclusion(ctx.mk_eq_atom(len_lhs, len_rhs), m); expr_ref conclusion(ctx.mk_eq_atom(len_lhs, len_rhs), m);
// build (premise -> conclusion) and assert TRACE("t_str_detail", tout << "string-eq length-eq axiom: "
expr_ref axiom(m.mk_implies(premise, conclusion), m); << mk_ismt2_pp(premise, m) << " -> " << mk_ismt2_pp(conclusion, m) << std::endl;);
TRACE("t_str_detail", tout << "string-eq length-eq axiom: " << mk_ismt2_pp(axiom, m) << std::endl;); assert_implication(premise, conclusion);
assert_axiom(axiom);
} }
void theory_str::attach_new_th_var(enode * n) { void theory_str::attach_new_th_var(enode * n) {
@ -380,8 +384,7 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) {
expr_ref c1(ctx.mk_eq_atom(a1, str), m); expr_ref c1(ctx.mk_eq_atom(a1, str), m);
expr_ref c2(ctx.mk_eq_atom(a2, str), m); expr_ref c2(ctx.mk_eq_atom(a2, str), m);
expr_ref conclusion(m.mk_and(c1, c2), m); expr_ref conclusion(m.mk_and(c1, c2), m);
expr_ref axiom(m.mk_or(m.mk_not(premise), conclusion), m); assert_implication(premise, conclusion);
assert_axiom(axiom);
return; return;
} }

3
src/smt/theory_str.h
View file

@ -58,7 +58,8 @@ namespace smt {
ptr_vector<enode> m_basicstr_axiom_todo; ptr_vector<enode> m_basicstr_axiom_todo;
svector<std::pair<enode*,enode*> > m_str_eq_todo; svector<std::pair<enode*,enode*> > m_str_eq_todo;
protected: protected:
void assert_axiom(ast * e); void assert_axiom(expr * e);
void assert_implication(expr * premise, expr * conclusion);
app * mk_strlen(app * e); app * mk_strlen(app * e);