mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-11-28 13:50:40 -08:00
commit 45dd820b6c
16 changed files with 86 additions and 73 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_recfun.h
View file

@ -69,7 +69,7 @@ namespace smt {
recfun::case_def const * m_cdef;
ptr_vector<expr> m_args;
body_expansion(recfun::util& u, app * n) : m_pred(n), m_cdef(0), m_args() {
body_expansion(recfun::util& u, app * n) : m_pred(n), m_cdef(nullptr), m_args() {
m_cdef = &u.get_case_def(n);
m_args.append(n->get_num_args(), n->get_args());
}

75
src/smt/theory_str.cpp
View file

@ -505,7 +505,7 @@ namespace smt {
app * a = mk_fresh_const(name.c_str(), int_sort);
ctx.internalize(a, false);
SASSERT(ctx.get_enode(a) != NULL);
SASSERT(ctx.get_enode(a) != nullptr);
SASSERT(ctx.e_internalized(a));
ctx.mark_as_relevant(a);
// I'm assuming that this combination will do the correct thing in the integer theory.
@ -544,7 +544,7 @@ namespace smt {
// I have a hunch that this may not get internalized for free...
ctx.internalize(a, false);
SASSERT(ctx.get_enode(a) != NULL);
SASSERT(ctx.get_enode(a) != nullptr);
SASSERT(ctx.e_internalized(a));
// this might help??
mk_var(ctx.get_enode(a));
@ -566,7 +566,7 @@ namespace smt {
m_trail.push_back(a);
ctx.internalize(a, false);
SASSERT(ctx.get_enode(a) != NULL);
SASSERT(ctx.get_enode(a) != nullptr);
SASSERT(ctx.e_internalized(a));
mk_var(ctx.get_enode(a));
m_basicstr_axiom_todo.push_back(ctx.get_enode(a));
@ -617,7 +617,7 @@ namespace smt {
app * a = mk_fresh_const(name.c_str(), string_sort);
ctx.internalize(a, false);
SASSERT(ctx.get_enode(a) != NULL);
SASSERT(ctx.get_enode(a) != nullptr);
// this might help??
mk_var(ctx.get_enode(a));
@ -710,7 +710,7 @@ namespace smt {
* Returns the simplified concatenation of two expressions,
* where either both expressions are constant strings
* or one expression is the empty string.
* If this precondition does not hold, the function returns NULL.
* If this precondition does not hold, the function returns nullptr.
* (note: this function was strTheory::Concat())
*/
expr * theory_str::mk_concat_const_str(expr * n1, expr * n2) {
@ -1661,53 +1661,66 @@ namespace smt {
}
}
// (str.replace s t t') is the string obtained by replacing the first occurrence
// of t in s, if any, by t'. Note that if t is empty, the result is to prepend
// t' to s; also, if t does not occur in s then the result is s.
void theory_str::instantiate_axiom_Replace(enode * e) {
context & ctx = get_context();
ast_manager & m = get_manager();
app * expr = e->get_owner();
if (axiomatized_terms.contains(expr)) {
TRACE("str", tout << "already set up Replace axiom for " << mk_pp(expr, m) << std::endl;);
app * ex = e->get_owner();
if (axiomatized_terms.contains(ex)) {
TRACE("str", tout << "already set up Replace axiom for " << mk_pp(ex, m) << std::endl;);
return;
}
axiomatized_terms.insert(expr);
axiomatized_terms.insert(ex);
TRACE("str", tout << "instantiate Replace axiom for " << mk_pp(expr, m) << std::endl;);
TRACE("str", tout << "instantiate Replace axiom for " << mk_pp(ex, m) << std::endl;);
expr_ref x1(mk_str_var("x1"), m);
expr_ref x2(mk_str_var("x2"), m);
expr_ref i1(mk_int_var("i1"), m);
expr_ref result(mk_str_var("result"), m);
expr * replaceS;
expr * replaceT;
expr * replaceTPrime;
u.str.is_replace(ex, replaceS, replaceT, replaceTPrime);
// t empty => result = (str.++ t' s)
expr_ref emptySrcAst(ctx.mk_eq_atom(replaceT, mk_string("")), m);
expr_ref prependTPrimeToS(ctx.mk_eq_atom(result, mk_concat(replaceTPrime, replaceS)), m);
// condAst = Contains(args[0], args[1])
expr_ref condAst(mk_contains(expr->get_arg(0), expr->get_arg(1)), m);
expr_ref condAst(mk_contains(ex->get_arg(0), ex->get_arg(1)), m);
// -----------------------
// true branch
expr_ref_vector thenItems(m);
// args[0] = x1 . args[1] . x2
thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x1, mk_concat(expr->get_arg(1), x2))));
thenItems.push_back(ctx.mk_eq_atom(ex->get_arg(0), mk_concat(x1, mk_concat(ex->get_arg(1), x2))));
// i1 = |x1|
thenItems.push_back(ctx.mk_eq_atom(i1, mk_strlen(x1)));
// args[0] = x3 . x4 /\ |x3| = |x1| + |args[1]| - 1 /\ ! contains(x3, args[1])
expr_ref x3(mk_str_var("x3"), m);
expr_ref x4(mk_str_var("x4"), m);
expr_ref tmpLen(m_autil.mk_add(i1, mk_strlen(expr->get_arg(1)), mk_int(-1)), m);
thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x3, x4)));
expr_ref tmpLen(m_autil.mk_add(i1, mk_strlen(ex->get_arg(1)), mk_int(-1)), m);
thenItems.push_back(ctx.mk_eq_atom(ex->get_arg(0), mk_concat(x3, x4)));
thenItems.push_back(ctx.mk_eq_atom(mk_strlen(x3), tmpLen));
thenItems.push_back(mk_not(m, mk_contains(x3, expr->get_arg(1))));
thenItems.push_back(ctx.mk_eq_atom(result, mk_concat(x1, mk_concat(expr->get_arg(2), x2))));
thenItems.push_back(mk_not(m, mk_contains(x3, ex->get_arg(1))));
thenItems.push_back(ctx.mk_eq_atom(result, mk_concat(x1, mk_concat(ex->get_arg(2), x2))));
// -----------------------
// false branch
expr_ref elseBranch(ctx.mk_eq_atom(result, expr->get_arg(0)), m);
expr_ref elseBranch(ctx.mk_eq_atom(result, ex->get_arg(0)), m);
th_rewriter rw(m);
expr_ref breakdownAssert(m.mk_ite(condAst, m.mk_and(thenItems.size(), thenItems.c_ptr()), elseBranch), m);
expr_ref breakdownAssert(m.mk_ite(emptySrcAst, prependTPrimeToS,
m.mk_ite(condAst, mk_and(thenItems), elseBranch)), m);
expr_ref breakdownAssert_rw(breakdownAssert, m);
rw(breakdownAssert_rw);
assert_axiom(breakdownAssert_rw);
expr_ref reduceToResult(ctx.mk_eq_atom(expr, result), m);
expr_ref reduceToResult(ctx.mk_eq_atom(ex, result), m);
expr_ref reduceToResult_rw(reduceToResult, m);
rw(reduceToResult_rw);
assert_axiom(reduceToResult_rw);
@ -2148,7 +2161,7 @@ namespace smt {
// Evaluates the concatenation (n1 . n2) with respect to
// the current equivalence classes of n1 and n2.
// Returns a constant string expression representing this concatenation
// if one can be determined, or NULL if this is not possible.
// if one can be determined, or nullptr if this is not possible.
expr * theory_str::eval_concat(expr * n1, expr * n2) {
bool n1HasEqcValue = false;
bool n2HasEqcValue = false;
@ -2222,7 +2235,7 @@ namespace smt {
for (enode_vector::iterator parent_it = current_parents.begin(); parent_it != current_parents.end(); ++parent_it) {
enode * e_parent = *parent_it;
SASSERT(e_parent != NULL);
SASSERT(e_parent != nullptr);
app * a_parent = e_parent->get_owner();
TRACE("str", tout << "considering parent " << mk_ismt2_pp(a_parent, m) << std::endl;);
@ -5575,7 +5588,7 @@ namespace smt {
tout << " " << mk_pp(el, m);
}
tout << std::endl;
if (constStrAst == NULL) {
if (constStrAst == nullptr) {
tout << "constStrAst = NULL" << std::endl;
} else {
tout << "constStrAst = " << mk_pp(constStrAst, m) << std::endl;
@ -7787,7 +7800,7 @@ namespace smt {
generate_mutual_exclusion(arrangement_disjunction);
}
} /* (arg1Len != 1 || arg2Len != 1) */
} /* if (Concat(arg1, arg2) == NULL) */
} /* if (Concat(arg1, arg2) == nullptr) */
}
}
}
@ -10417,12 +10430,12 @@ namespace smt {
}
} // foreach(term in str_in_re_terms)
eautomaton * aut_inter = NULL;
eautomaton * aut_inter = nullptr;
CTRACE("str", !intersect_constraints.empty(), tout << "check intersection of automata constraints for " << mk_pp(str, m) << std::endl;);
for (svector<regex_automaton_under_assumptions>::iterator aut_it = intersect_constraints.begin();
aut_it != intersect_constraints.end(); ++aut_it) {
regex_automaton_under_assumptions aut = *aut_it;
if (aut_inter == NULL) {
if (aut_inter == nullptr) {
// start somewhere
aut_inter = aut.get_automaton();
used_intersect_constraints.push_back(aut);
@ -10472,7 +10485,7 @@ namespace smt {
}
}
} // foreach(entry in intersect_constraints)
if (aut_inter != NULL) {
if (aut_inter != nullptr) {
aut_inter->compress();
}
TRACE("str", tout << "intersected " << used_intersect_constraints.size() << " constraints" << std::endl;);
@ -10503,7 +10516,7 @@ namespace smt {
}
conflict_lhs = mk_and(conflict_terms);
if (used_intersect_constraints.size() > 1 && aut_inter != NULL) {
if (used_intersect_constraints.size() > 1 && aut_inter != nullptr) {
// check whether the intersection is only the empty string
unsigned initial_state = aut_inter->init();
if (aut_inter->final_states().size() == 1 && aut_inter->is_final_state(initial_state)) {
@ -10521,7 +10534,7 @@ namespace smt {
}
}
if (aut_inter != NULL && aut_inter->is_empty()) {
if (aut_inter != nullptr && aut_inter->is_empty()) {
TRACE("str", tout << "product automaton is empty; asserting conflict clause" << std::endl;);
expr_ref conflict_clause(m.mk_not(mk_and(conflict_terms)), m);
assert_axiom(conflict_clause);
@ -11809,7 +11822,7 @@ namespace smt {
expr_ref assertL(mk_and(and_items_LHS), m);
SASSERT(assertL);
expr * finalAxiom = m.mk_or(m.mk_not(assertL), lenTestAssert.get());
SASSERT(finalAxiom != NULL);
SASSERT(finalAxiom != nullptr);
TRACE("str", tout << "crash avoidance finalAxiom: " << mk_pp(finalAxiom, m) << std::endl;);
return finalAxiom;
} else {
@ -12095,7 +12108,7 @@ namespace smt {
lenTester_fvar_map.insert(indicator, freeVar);
expr * lenTestAssert = gen_len_test_options(freeVar, indicator, testNum);
SASSERT(lenTestAssert != NULL);
SASSERT(lenTestAssert != nullptr);
return lenTestAssert;
} else {
TRACE("str", tout << "found previous in-scope length assertions" << std::endl;);
@ -12201,7 +12214,7 @@ namespace smt {
testNum = i + 1;
}
expr * lenTestAssert = gen_len_test_options(freeVar, indicator, testNum);
SASSERT(lenTestAssert != NULL);
SASSERT(lenTestAssert != nullptr);
return lenTestAssert;
} else {
// if we are performing automata-based reasoning and the term associated with