mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 07:13:41 +00:00
Code Activity

EndsWith axiomatization in theory_str

Browse source
This commit is contained in:
Murphy Berzish 2016-06-14 18:05:24 -04:00
parent fd38b4c729
commit 989d6b577b
1 changed files with 22 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

39
src/smt/theory_str.cpp
View file

@ -832,7 +832,6 @@ void theory_str::instantiate_axiom_StartsWith(enode * e) {
SASSERT(topLevelCond); SASSERT(topLevelCond);
expr_ref finalAxiom(m.mk_ite(topLevelCond, then1, m.mk_not(expr)), m); expr_ref finalAxiom(m.mk_ite(topLevelCond, then1, m.mk_not(expr)), m);
SASSERT(finalAxiom); SASSERT(finalAxiom);
assert_axiom(finalAxiom); assert_axiom(finalAxiom);
} }
@ -850,22 +849,28 @@ void theory_str::instantiate_axiom_EndsWith(enode * e) {
TRACE("t_str_detail", tout << "instantiate EndsWith axiom for " << mk_pp(expr, m) << std::endl;); TRACE("t_str_detail", tout << "instantiate EndsWith axiom for " << mk_pp(expr, m) << std::endl;);
// TODO NEXT expr_ref ts0(mk_str_var("ts0"), m);
NOT_IMPLEMENTED_YET(); expr_ref ts1(mk_str_var("ts1"), m);
/*
Z3_ast resBoolVar = my_mk_internal_bool_var(t); expr_ref_vector innerItems(m);
Z3_ast ts0 = my_mk_internal_string_var(t); innerItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(ts0, ts1)));
Z3_ast ts1 = my_mk_internal_string_var(t); innerItems.push_back(ctx.mk_eq_atom(mk_strlen(ts1), mk_strlen(expr->get_arg(1))));
// boolVar = endswith(arg[0], arg[1]) innerItems.push_back(m.mk_ite(ctx.mk_eq_atom(ts1, expr->get_arg(1)), expr, m.mk_not(expr)));
// -------------------------------------------- expr_ref then1(m.mk_and(innerItems.size(), innerItems.c_ptr()), m);
std::vector<Z3_ast> innerItems; SASSERT(then1);
innerItems.push_back( Z3_mk_eq(ctx, args[0], mk_concat(t, ts0, ts1)) );
innerItems.push_back( Z3_mk_eq(ctx, mk_length(t, ts1), mk_length(t, args[1])) ); // the top-level condition is Length(arg0) >= Length(arg1)
innerItems.push_back( Z3_mk_ite(ctx, Z3_mk_eq(ctx, ts1, args[1]), Z3_mk_eq(ctx, resBoolVar, Z3_mk_true(ctx)), Z3_mk_eq(ctx, resBoolVar, Z3_mk_false(ctx) ) ) ); expr_ref topLevelCond(
Z3_ast then1 = mk_and_fromVector(t, innerItems); m_autil.mk_ge(
breakdownAssert = Z3_mk_ite(ctx, Z3_mk_ge(ctx, mk_length(t, args[0]), mk_length(t, args[1])), then1, Z3_mk_eq(ctx, resBoolVar, Z3_mk_false(ctx) ) ); m_autil.mk_add(
reduceAst = resBoolVar; mk_strlen(expr->get_arg(0)), m_autil.mk_mul(mk_int(-1), mk_strlen(expr->get_arg(1)))),
*/ mk_int(0))
, m);
SASSERT(topLevelCond);
expr_ref finalAxiom(m.mk_ite(topLevelCond, then1, m.mk_not(expr)), m);
SASSERT(finalAxiom);
assert_axiom(finalAxiom);
} }
void theory_str::attach_new_th_var(enode * n) { void theory_str::attach_new_th_var(enode * n) {