mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-07 08:21:56 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-07-27 17:02:27 -07:00
commit b482dbd589
379 changed files with 7440 additions and 3352 deletions
Download patch file Download diff file Expand all files Collapse all files

83
src/smt/CMakeLists.txt Normal file
View file

@ -0,0 +1,83 @@
z3_add_component(smt
SOURCES
arith_eq_adapter.cpp
arith_eq_solver.cpp
asserted_formulas.cpp
cached_var_subst.cpp
cost_evaluator.cpp
dyn_ack.cpp
elim_term_ite.cpp
expr_context_simplifier.cpp
fingerprints.cpp
mam.cpp
old_interval.cpp
qi_queue.cpp
smt_almost_cg_table.cpp
smt_case_split_queue.cpp
smt_cg_table.cpp
smt_checker.cpp
smt_clause.cpp
smt_conflict_resolution.cpp
smt_consequences.cpp
smt_context.cpp
smt_context_inv.cpp
smt_context_pp.cpp
smt_context_stat.cpp
smt_enode.cpp
smt_farkas_util.cpp
smt_for_each_relevant_expr.cpp
smt_implied_equalities.cpp
smt_internalizer.cpp
smt_justification.cpp
smt_kernel.cpp
smt_literal.cpp
smt_model_checker.cpp
smt_model_finder.cpp
smt_model_generator.cpp
smt_quantifier.cpp
smt_quantifier_stat.cpp
smt_quick_checker.cpp
smt_relevancy.cpp
smt_setup.cpp
smt_solver.cpp
smt_statistics.cpp
smt_theory.cpp
smt_value_sort.cpp
smt2_extra_cmds.cpp
theory_arith.cpp
theory_array_base.cpp
theory_array.cpp
theory_array_full.cpp
theory_bv.cpp
theory_datatype.cpp
theory_dense_diff_logic.cpp
theory_diff_logic.cpp
theory_dl.cpp
theory_dummy.cpp
theory_fpa.cpp
theory_lra.cpp
theory_opt.cpp
theory_pb.cpp
theory_seq.cpp
theory_str.cpp
theory_utvpi.cpp
theory_wmaxsat.cpp
uses_theory.cpp
watch_list.cpp
COMPONENT_DEPENDENCIES
bit_blaster
cmd_context
euclid
fpa
grobner
nlsat
lp
macros
normal_forms
parser_util
pattern
proof_checker
proto_model
simplex
substitution
)

25
src/smt/cached_var_subst.cpp
View file

@ -23,7 +23,7 @@ bool cached_var_subst::key_eq_proc::operator()(cached_var_subst::key * k1, cache
return false;
if (k1->m_num_bindings != k2->m_num_bindings)
return false;
for (unsigned i = 0; i < k1->m_num_bindings; i++)
for (unsigned i = 0; i < k1->m_num_bindings; i++)
if (k1->m_bindings[i] != k2->m_bindings[i])
return false;
return true;
@ -49,9 +49,9 @@ void cached_var_subst::operator()(quantifier * qa, unsigned num_bindings, smt::e
new_key->m_qa = qa;
new_key->m_num_bindings = num_bindings;
for (unsigned i = 0; i < num_bindings; i++)
for (unsigned i = 0; i < num_bindings; i++)
new_key->m_bindings[i] = bindings[i]->get_owner();
instances::entry * entry = m_instances.insert_if_not_there2(new_key, 0);
if (entry->get_data().m_key != new_key) {
SASSERT(entry->get_data().m_value != 0);
@ -60,20 +60,27 @@ void cached_var_subst::operator()(quantifier * qa, unsigned num_bindings, smt::e
result = entry->get_data().m_value;
return;
}
m_proc(qa->get_expr(), new_key->m_num_bindings, new_key->m_bindings, result);
SASSERT(entry->get_data().m_value == 0);
try {
m_proc(qa->get_expr(), new_key->m_num_bindings, new_key->m_bindings, result);
}
catch (...) {
// CMW: The var_subst reducer was interrupted and m_instances is
// in an inconsistent state; we need to remove (new_key, 0).
m_instances.remove(new_key);
throw; // Throw on to smt::qi_queue/smt::solver.
}
// cache result
entry->get_data().m_value = result;
// remove key from cache
m_new_keys[num_bindings] = 0;
// increment reference counters
m_refs.push_back(qa);
for (unsigned i = 0; i < new_key->m_num_bindings; i++)
m_refs.push_back(new_key->m_bindings[i]);
m_refs.push_back(result);
}

19
src/smt/params/CMakeLists.txt Normal file
View file

@ -0,0 +1,19 @@
z3_add_component(smt_params
SOURCES
dyn_ack_params.cpp
preprocessor_params.cpp
qi_params.cpp
smt_params.cpp
theory_arith_params.cpp
theory_array_params.cpp
theory_bv_params.cpp
theory_pb_params.cpp
theory_str_params.cpp
COMPONENT_DEPENDENCIES
ast
bit_blaster
pattern
simplifier
PYG_FILES
smt_params_helper.pyg
)

13
src/smt/proto_model/CMakeLists.txt Normal file
View file

@ -0,0 +1,13 @@
z3_add_component(proto_model
SOURCES
array_factory.cpp
datatype_factory.cpp
numeral_factory.cpp
proto_model.cpp
struct_factory.cpp
value_factory.cpp
COMPONENT_DEPENDENCIES
model
simplifier
smt_params
)

36
src/smt/qi_queue.cpp
View file

@ -41,7 +41,7 @@ namespace smt {
init_parser_vars();
m_vals.resize(15, 0.0f);
}
qi_queue::~qi_queue() {
}
@ -50,7 +50,7 @@ namespace smt {
if (!m_parser.parse_string(m_params.m_qi_cost.c_str(), m_cost_function)) {
// it is not reasonable to abort here during the creation of smt::context just because an invalid option was provided.
// throw default_exception("invalid cost function %s", m_params.m_qi_cost.c_str());
// using warning message instead
warning_msg("invalid cost function '%s', switching to default one", m_params.m_qi_cost.c_str());
// Trying again with default function
@ -107,7 +107,7 @@ namespace smt {
m_vals[SIZE] = static_cast<float>(stat->get_size());
m_vals[DEPTH] = static_cast<float>(stat->get_depth());
m_vals[GENERATION] = static_cast<float>(generation);
m_vals[QUANT_GENERATION] = static_cast<float>(stat->get_generation());
m_vals[QUANT_GENERATION] = static_cast<float>(stat->get_generation());
m_vals[WEIGHT] = static_cast<float>(q->get_weight());
m_vals[VARS] = static_cast<float>(q->get_num_decls());
m_vals[PATTERN_WIDTH] = pat ? static_cast<float>(pat->get_num_args()) : 1.0f;
@ -118,7 +118,7 @@ namespace smt {
TRACE("qi_queue_detail", for (unsigned i = 0; i < m_vals.size(); i++) { tout << m_vals[i] << " "; } tout << "\n";);
return stat;
}
float qi_queue::get_cost(quantifier * q, app * pat, unsigned generation, unsigned min_top_generation, unsigned max_top_generation) {
quantifier_stat * stat = set_values(q, pat, generation, min_top_generation, max_top_generation, 0);
float r = m_evaluator(m_cost_function, m_vals.size(), m_vals.c_ptr());
@ -132,11 +132,11 @@ namespace smt {
float r = m_evaluator(m_new_gen_function, m_vals.size(), m_vals.c_ptr());
return static_cast<unsigned>(r);
}
void qi_queue::insert(fingerprint * f, app * pat, unsigned generation, unsigned min_top_generation, unsigned max_top_generation) {
quantifier * q = static_cast<quantifier*>(f->get_data());
float cost = get_cost(q, pat, generation, min_top_generation, max_top_generation);
TRACE("qi_queue_detail",
TRACE("qi_queue_detail",
tout << "new instance of " << q->get_qid() << ", weight " << q->get_weight()
<< ", generation: " << generation << ", scope_level: " << m_context.get_scope_level() << ", cost: " << cost << "\n";
for (unsigned i = 0; i < f->get_num_args(); i++) {
@ -157,7 +157,7 @@ namespace smt {
quantifier * qa = static_cast<quantifier*>(f->get_data());
if (curr.m_cost <= m_eager_cost_threshold) {
instantiate(curr);
instantiate(curr);
}
else if (m_params.m_qi_promote_unsat && m_checker.is_unsat(qa->get_expr(), f->get_num_args(), f->get_args())) {
// do not delay instances that produce a conflict.
@ -193,7 +193,7 @@ namespace smt {
// This nasty side-effect may change the behavior of Z3.
m_manager.trace_stream() << " #" << bindings[i]->get_owner_id();
}
#endif
if (m_manager.proofs_enabled())
m_manager.trace_stream() << " #" << proof_id;
@ -233,7 +233,7 @@ namespace smt {
if (m_manager.is_true(s_instance)) {
TRACE("checker", tout << "reduced to true, before:\n" << mk_ll_pp(instance, m_manager););
if (m_manager.has_trace_stream())
if (m_manager.has_trace_stream())
m_manager.trace_stream() << "[end-of-instance]\n";
return;
@ -278,7 +278,7 @@ namespace smt {
pr1 = m_manager.mk_modus_ponens(qi_pr, rw);
}
else {
app * bare_s_lemma = m_manager.mk_or(m_manager.mk_not(q), s_instance);
app * bare_s_lemma = m_manager.mk_or(m_manager.mk_not(q), s_instance);
proof * prs[1] = { pr.get() };
proof * cg = m_manager.mk_congruence(bare_lemma, bare_s_lemma, 1, prs);
proof * rw = m_manager.mk_rewrite(bare_s_lemma, lemma);
@ -331,13 +331,13 @@ namespace smt {
s.m_instances_lim = m_instances.size();
s.m_instantiated_trail_lim = m_instantiated_trail.size();
}
void qi_queue::pop_scope(unsigned num_scopes) {
unsigned new_lvl = m_scopes.size() - num_scopes;
scope & s = m_scopes[new_lvl];
unsigned old_sz = s.m_instantiated_trail_lim;
unsigned sz = m_instantiated_trail.size();
for (unsigned i = old_sz; i < sz; i++)
for (unsigned i = old_sz; i < sz; i++)
m_delayed_entries[m_instantiated_trail[i]].m_instantiated = false;
m_instantiated_trail.shrink(old_sz);
m_delayed_entries.shrink(s.m_delayed_entries_lim);
@ -359,7 +359,7 @@ namespace smt {
}
bool qi_queue::final_check_eh() {
TRACE("qi_queue", display_delayed_instances_stats(tout); tout << "lazy threshold: " << m_params.m_qi_lazy_threshold
TRACE("qi_queue", display_delayed_instances_stats(tout); tout << "lazy threshold: " << m_params.m_qi_lazy_threshold
<< ", scope_level: " << m_context.get_scope_level() << "\n";);
if (m_params.m_qi_conservative_final_check) {
bool init = false;
@ -379,7 +379,7 @@ namespace smt {
entry & e = m_delayed_entries[i];
TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";);
if (!e.m_instantiated && e.m_cost <= min_cost) {
TRACE("qi_queue",
TRACE("qi_queue",
tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast<quantifier*>(e.m_qb->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";);
result = false;
m_instantiated_trail.push_back(i);
@ -389,13 +389,13 @@ namespace smt {
}
return result;
}
bool result = true;
for (unsigned i = 0; i < m_delayed_entries.size(); i++) {
entry & e = m_delayed_entries[i];
TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";);
if (!e.m_instantiated && e.m_cost <= m_params.m_qi_lazy_threshold) {
TRACE("qi_queue",
TRACE("qi_queue",
tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast<quantifier*>(e.m_qb->get_data()), m_manager) << "\ncost: " << e.m_cost << "\n";);
result = false;
m_instantiated_trail.push_back(i);
@ -443,7 +443,7 @@ namespace smt {
quantifier * qa = *it2;
delayed_qa_info info;
qa2info.find(qa, info);
out << qa->get_qid() << ": " << info.m_num << " [" << info.m_min_cost << ", " << info.m_max_cost << "]\n";
out << qa->get_qid() << ": " << info.m_num << " [" << info.m_min_cost << ", " << info.m_max_cost << "]\n";
}
}
@ -482,6 +482,6 @@ namespace smt {
}
#endif
}
};

4
src/smt/smt_conflict_resolution.cpp
View file

@ -1405,6 +1405,7 @@ namespace smt {
switch (js.get_kind()) {
case b_justification::CLAUSE: {
clause * cls = js.get_clause();
TRACE("unsat_core_bug", m_ctx.display_clause_detail(tout, cls););
unsigned num_lits = cls->get_num_literals();
unsigned i = 0;
if (consequent != false_literal) {
@ -1422,8 +1423,9 @@ namespace smt {
process_antecedent_for_unsat_core(~l);
}
justification * js = cls->get_justification();
if (js)
if (js) {
process_justification_for_unsat_core(js);
}
break;
}
case b_justification::BIN_CLAUSE:

1
src/smt/smt_consequences.cpp
View file

@ -103,6 +103,7 @@ namespace smt {
void context::justify(literal lit, index_set& s) {
ast_manager& m = m_manager;
(void)m;
b_justification js = get_justification(lit.var());
switch (js.get_kind()) {
case b_justification::CLAUSE: {

8
src/smt/smt_context.cpp
View file

@ -4345,10 +4345,9 @@ namespace smt {
);
failure fl = get_last_search_failure();
if (fl == MEMOUT || fl == CANCELED || fl == TIMEOUT || fl == NUM_CONFLICTS || fl == RESOURCE_LIMIT) {
return;
TRACE("get_model", tout << "last search failure: " << fl << "\n";);
}
if (m_fparams.m_model || m_fparams.m_model_on_final_check || m_qmanager->model_based()) {
else if (m_fparams.m_model || m_fparams.m_model_on_final_check || m_qmanager->model_based()) {
m_model_generator->reset();
m_proto_model = m_model_generator->mk_model();
m_qmanager->adjust_model(m_proto_model.get());
@ -4359,6 +4358,9 @@ namespace smt {
if (m_fparams.m_model_compact)
m_proto_model->compress();
TRACE("mbqi_bug", tout << "after cleanup:\n"; model_pp(tout, *m_proto_model););
}
else {
}
}

4
src/smt/smt_internalizer.cpp
View file

@ -1034,8 +1034,10 @@ namespace smt {
lbool val = get_assignment(curr);
switch(val) {
case l_false:
TRACE("simplify_aux_clause_literals", display_literal(tout << get_assign_level(curr) << " " << get_scope_level() << " ", curr); tout << "\n"; );
simp_lits.push_back(~curr);
break; // ignore literal
break; // ignore literal
// fall through
case l_undef:
if (curr == ~prev)
return false; // clause is equivalent to true

4
src/smt/smt_quantifier.cpp
View file

@ -135,7 +135,7 @@ namespace smt {
m_qi_queue.insert(f, pat, max_generation, min_top_generation, max_top_generation); // TODO
m_num_instances++;
}
TRACE("quantifier",
TRACE("quantifier",
tout << mk_pp(q, m()) << " ";
for (unsigned i = 0; i < num_bindings; ++i) {
tout << mk_pp(bindings[i]->get_owner(), m()) << " ";
@ -372,7 +372,7 @@ namespace smt {
quantifier_manager_plugin * plugin = m_imp->m_plugin->mk_fresh();
m_imp->~imp();
m_imp = new (m_imp) imp(*this, ctx, p, plugin);
plugin->set_manager(*this);
plugin->set_manager(*this);
}
void quantifier_manager::display(std::ostream & out) const {

4
src/smt/smt_quantifier.h
View file

@ -75,7 +75,7 @@ namespace smt {
};
bool model_based() const;
bool mbqi_enabled(quantifier *q) const; // can mbqi instantiate this quantifier?
bool mbqi_enabled(quantifier *q) const; // can mbqi instantiate this quantifier?
void adjust_model(proto_model * m);
check_model_result check_model(proto_model * m, obj_map<enode, app *> const & root2value);
@ -167,7 +167,7 @@ namespace smt {
virtual void push() = 0;
virtual void pop(unsigned num_scopes) = 0;
};
};

12
src/smt/tactic/CMakeLists.txt Normal file
View file

@ -0,0 +1,12 @@
z3_add_component(smt_tactic
SOURCES
ctx_solver_simplify_tactic.cpp
smt_tactic.cpp
unit_subsumption_tactic.cpp
COMPONENT_DEPENDENCIES
smt
TACTIC_HEADERS
ctx_solver_simplify_tactic.h
smt_tactic.h
unit_subsumption_tactic.h
)

2
src/smt/tactic/smt_tactic.cpp
View file

@ -253,7 +253,7 @@ public:
if (m_ctx->canceled()) {
throw tactic_exception(Z3_CANCELED_MSG);
}
if (m_fail_if_inconclusive) {
if (m_fail_if_inconclusive && !m_candidate_models) {
std::stringstream strm;
strm << "smt tactic failed to show goal to be sat/unsat " << m_ctx->last_failure_as_string();
throw tactic_exception(strm.str().c_str());

5
src/smt/theory_arith_aux.h
View file

@ -1458,7 +1458,7 @@ namespace smt {
normalize_gain(min_gain.get_rational(), max_gain);
}
if (is_int(x_i) && !max_gain.is_rational()) {
if (is_int(x_i) && !max_gain.is_int()) {
max_gain = inf_numeral(floor(max_gain));
normalize_gain(min_gain.get_rational(), max_gain);
}
@ -1483,7 +1483,7 @@ namespace smt {
}
}
TRACE("opt",
tout << "v" << x_i << " a_ij " << a_ij << " "
tout << "v" << x_i << (is_int(x_i)?" int":" real") << " a_ij " << a_ij << " "
<< "min gain: " << min_gain << " "
<< "max gain: " << max_gain << " tighter: "
<< (is_tighter?"true":"false") << "\n";);
@ -1696,6 +1696,7 @@ namespace smt {
if (lower(x_j)) tout << "lower x_j: " << lower_bound(x_j) << " ";
tout << "value x_j: " << get_value(x_j) << "\n";
);
pivot<true>(x_i, x_j, a_ij, false);
SASSERT(is_non_base(x_i));

16
src/smt/theory_arith_core.h
View file

@ -1716,7 +1716,7 @@ namespace smt {
CASSERT("arith", check_null_var_pos());
r1.save_var_pos(m_var_pos);
//
// loop over variables in row2,
// add terms in row2 to row1.
@ -1769,7 +1769,7 @@ namespace smt {
ADD_ROW(r_entry.m_coeff = it->m_coeff; r_entry.m_coeff *= coeff,
r_entry.m_coeff += it->m_coeff * coeff);
}
r1.reset_var_pos(m_var_pos);
CASSERT("arith", check_null_var_pos());
CASSERT("row_assignment_bug", valid_row_assignment(r1));
@ -1778,7 +1778,7 @@ namespace smt {
theory_var v = r1.get_base_var();
if (is_int(v) && !get_value(v).is_int())
gcd_test(r1);
}
}
}
/**
@ -1797,6 +1797,7 @@ namespace smt {
SASSERT(!is_non_base(v));
add_row(r1, c, get_var_row(v), false);
}
get_manager().limit().inc(sz);
}
// -----------------------------------
@ -1852,6 +1853,7 @@ namespace smt {
if (is_base(v) && !m_to_patch.contains(v) && (below_lower(v) || above_upper(v))) {
m_to_patch.insert(v);
}
get_manager().limit().inc();
}
/**
@ -1928,6 +1930,8 @@ namespace smt {
DIVIDE_ROW(it->m_coeff /= tmp);
}
get_manager().limit().inc(r.size());
set_var_row(x_i, -1);
set_var_row(x_j, r_id);
@ -1937,7 +1941,7 @@ namespace smt {
set_var_kind(x_i, NON_BASE);
set_var_kind(x_j, BASE);
eliminate<Lazy>(x_j, apply_gcd_test);
eliminate<Lazy>(x_j, apply_gcd_test);
CASSERT("arith", wf_rows());
CASSERT("arith", wf_columns());
@ -1972,6 +1976,7 @@ namespace smt {
int s_pos = -1;
for (; it != end; ++it, ++i) {
if (!it->is_dead()) {
unsigned r1_sz = m_rows[r_id].size();
if (it->m_row_id != static_cast<int>(r_id)) {
row & r2 = m_rows[it->m_row_id];
theory_var s2 = r2.m_base_var;
@ -1979,13 +1984,14 @@ namespace smt {
a_kj = r2[it->m_row_idx].m_coeff;
a_kj.neg();
add_row(it->m_row_id, a_kj, r_id, apply_gcd_test);
get_manager().limit().inc((r1_sz + r2.size()) * (a_kj.storage_size()));
}
}
else {
s_pos = i;
}
}
}
}
CTRACE("eliminate", !Lazy && c.size() != 1,
tout << "eliminating v" << x_i << ", Lazy: " << Lazy << ", c.size: " << c.size() << "\n";
display(tout););

6
src/smt/theory_arith_int.h
View file

@ -201,10 +201,12 @@ namespace smt {
SASSERT(is_int(v));
SASSERT(!get_value(v).is_int());
m_stats.m_branches++;
TRACE("arith_int", tout << "branching v" << v << " = " << get_value(v) << "\n";
display_var(tout, v););
numeral k = ceil(get_value(v));
rational _k = k.to_rational();
TRACE("arith_int", tout << "branching v" << v << " = " << get_value(v) << "\n";
display_var(tout, v);
tout << "k = " << k << ", _k = "<< _k << std::endl;
);
expr_ref bound(get_manager());
expr* e = get_enode(v)->get_owner();
bound = m_util.mk_ge(e, m_util.mk_numeral(_k, m_util.is_int(e)));

806
src/smt/theory_lra.cpp
View file

File diff suppressed because it is too large Load diff

243
src/smt/theory_seq.cpp
View file

@ -1074,7 +1074,7 @@ expr_ref theory_seq::mk_first(expr* s) {
void theory_seq::mk_decompose(expr* e, expr_ref& head, expr_ref& tail) {
expr* e1, *e2;
expr* e1 = 0, *e2 = 0;
zstring s;
if (m_util.str.is_empty(e)) {
head = m_util.str.mk_unit(mk_nth(e, m_autil.mk_int(0)));
@ -1401,7 +1401,7 @@ bool theory_seq::occurs(expr* a, expr* b) {
// true if a occurs under an interpreted function or under left/right selector.
SASSERT(is_var(a));
SASSERT(m_todo.empty());
expr* e1, *e2;
expr* e1 = 0, *e2 = 0;
m_todo.push_back(b);
while (!m_todo.empty()) {
b = m_todo.back();
@ -1990,7 +1990,7 @@ bool theory_seq::solve_nc(unsigned idx) {
return true;
}
expr* e1, *e2;
expr* e1 = 0, *e2 = 0;
if (m.is_eq(c, e1, e2)) {
literal eq = mk_eq(e1, e2, false);
propagate_lit(deps, 0, 0, ~eq);
@ -2176,8 +2176,67 @@ bool theory_seq::simplify_and_solve_eqs() {
return m_new_propagation || ctx.inconsistent();
}
void theory_seq::internalize_eq_eh(app * atom, bool_var v) {}
void theory_seq::internalize_eq_eh(app * atom, bool_var v) {
}
bool theory_seq::internalize_atom(app* a, bool) {
#if 1
return internalize_term(a);
#else
if (is_skolem(m_eq, a)) {
return internalize_term(a);
}
context & ctx = get_context();
bool_var bv = ctx.mk_bool_var(a);
ctx.set_var_theory(bv, get_id());
ctx.mark_as_relevant(bv);
expr* e1, *e2;
if (m_util.str.is_in_re(a, e1, e2)) {
return internalize_term(to_app(e1)) && internalize_re(e2);
}
if (m_util.str.is_contains(a, e1, e2) ||
m_util.str.is_prefix(a, e1, e2) ||
m_util.str.is_suffix(a, e1, e2)) {
return internalize_term(to_app(e1)) && internalize_term(to_app(e2));
}
if (is_accept(a) || is_reject(a) || is_step(a) || is_skolem(symbol("seq.is_digit"), a)) {
return true;
}
UNREACHABLE();
return internalize_term(a);
#endif
}
bool theory_seq::internalize_re(expr* e) {
expr* e1, *e2;
unsigned lc, uc;
if (m_util.re.is_to_re(e, e1)) {
return internalize_term(to_app(e1));
}
if (m_util.re.is_star(e, e1) ||
m_util.re.is_plus(e, e1) ||
m_util.re.is_opt(e, e1) ||
m_util.re.is_loop(e, e1, lc) ||
m_util.re.is_loop(e, e1, lc, uc) ||
m_util.re.is_complement(e, e1)) {
return internalize_re(e1);
}
if (m_util.re.is_union(e, e1, e2) ||
m_util.re.is_intersection(e, e1, e2) ||
m_util.re.is_concat(e, e1, e2)) {
return internalize_re(e1) && internalize_re(e2);
}
if (m_util.re.is_full(e) ||
m_util.re.is_empty(e)) {
return true;
}
if (m_util.re.is_range(e, e1, e2)) {
return internalize_term(to_app(e1)) && internalize_term(to_app(e2));
}
UNREACHABLE();
return internalize_term(to_app(e));
}
bool theory_seq::internalize_term(app* term) {
context & ctx = get_context();
@ -2187,10 +2246,7 @@ bool theory_seq::internalize_term(app* term) {
return true;
}
TRACE("seq_verbose", tout << mk_pp(term, m) << "\n";);
unsigned num_args = term->get_num_args();
expr* arg;
for (unsigned i = 0; i < num_args; i++) {
arg = term->get_arg(i);
for (expr* arg : *term) {
mk_var(ensure_enode(arg));
}
if (m.is_bool(term)) {
@ -2257,7 +2313,7 @@ bool theory_seq::check_int_string() {
bool theory_seq::add_stoi_axiom(expr* e) {
context& ctx = get_context();
expr* n;
expr* n = 0;
rational val;
TRACE("seq", tout << mk_pp(e, m) << "\n";);
VERIFY(m_util.str.is_stoi(e, n));
@ -2339,7 +2395,7 @@ expr_ref theory_seq::digit2int(expr* ch) {
bool theory_seq::add_itos_axiom(expr* e) {
context& ctx = get_context();
rational val;
expr* n;
expr* n = 0;
TRACE("seq", tout << mk_pp(e, m) << "\n";);
VERIFY(m_util.str.is_itos(e, n));
if (get_num_value(n, val)) {
@ -2543,9 +2599,9 @@ void theory_seq::collect_statistics(::statistics & st) const {
void theory_seq::init_model(expr_ref_vector const& es) {
expr_ref new_s(m);
for (unsigned i = 0; i < es.size(); ++i) {
for (expr* e : es) {
dependency* eqs = 0;
expr_ref s = canonize(es[i], eqs);
expr_ref s = canonize(e, eqs);
if (is_var(s)) {
new_s = m_factory->get_fresh_value(m.get_sort(s));
m_rep.update(s, new_s, eqs);
@ -2556,13 +2612,11 @@ void theory_seq::init_model(expr_ref_vector const& es) {
void theory_seq::init_model(model_generator & mg) {
m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model());
mg.register_factory(m_factory);
for (unsigned j = 0; j < m_nqs.size(); ++j) {
ne const& n = m_nqs[j];
for (ne const& n : m_nqs) {
m_factory->register_value(n.l());
m_factory->register_value(n.r());
}
for (unsigned j = 0; j < m_nqs.size(); ++j) {
ne const& n = m_nqs[j];
for (ne const& n : m_nqs) {
for (unsigned i = 0; i < n.ls().size(); ++i) {
init_model(n.ls(i));
init_model(n.rs(i));
@ -2804,77 +2858,123 @@ bool theory_seq::canonize(expr_ref_vector const& es, expr_ref_vector& result, de
return change;
}
expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
expr_ref theory_seq::expand(expr* e, dependency*& eqs) {
unsigned sz = m_expand_todo.size();
m_expand_todo.push_back(e);
expr_ref result(m);
dependency* deps = 0;
expr_dep ed;
if (m_rep.find_cache(e0, ed)) {
eqs = m_dm.mk_join(eqs, ed.second);
result = ed.first;
return result;
while (m_expand_todo.size() != sz) {
expr* e = m_expand_todo.back();
result = expand1(e, eqs);
if (result.get()) m_expand_todo.pop_back();
}
return result;
}
expr_ref theory_seq::try_expand(expr* e, dependency*& eqs){
expr_ref result(m);
expr_dep ed;
if (m_rep.find_cache(e, ed)) {
if (e != ed.first) {
eqs = m_dm.mk_join(eqs, ed.second);
}
result = ed.first;
}
else {
m_expand_todo.push_back(e);
}
return result;
}
expr_ref theory_seq::expand1(expr* e0, dependency*& eqs) {
expr_ref result(m);
result = try_expand(e0, eqs);
if (result) return result;
dependency* deps = 0;
expr* e = m_rep.find(e0, deps);
expr* e1, *e2, *e3;
expr_ref arg1(m), arg2(m);
context& ctx = get_context();
if (m_util.str.is_concat(e, e1, e2)) {
result = mk_concat(expand(e1, deps), expand(e2, deps));
arg1 = try_expand(e1, deps);
arg2 = try_expand(e2, deps);
if (!arg1 || !arg2) return result;
result = mk_concat(arg1, arg2);
}
else if (m_util.str.is_empty(e) || m_util.str.is_string(e)) {
result = e;
}
else if (m_util.str.is_prefix(e, e1, e2)) {
result = m_util.str.mk_prefix(expand(e1, deps), expand(e2, deps));
arg1 = try_expand(e1, deps);
arg2 = try_expand(e2, deps);
if (!arg1 || !arg2) return result;
result = m_util.str.mk_prefix(arg1, arg2);
}
else if (m_util.str.is_suffix(e, e1, e2)) {
result = m_util.str.mk_suffix(expand(e1, deps), expand(e2, deps));
arg1 = try_expand(e1, deps);
arg2 = try_expand(e2, deps);
if (!arg1 || !arg2) return result;
result = m_util.str.mk_suffix(arg1, arg2);
}
else if (m_util.str.is_contains(e, e1, e2)) {
result = m_util.str.mk_contains(expand(e1, deps), expand(e2, deps));
arg1 = try_expand(e1, deps);
arg2 = try_expand(e2, deps);
if (!arg1 || !arg2) return result;
result = m_util.str.mk_contains(arg1, arg2);
}
else if (m_util.str.is_unit(e, e1)) {
result = m_util.str.mk_unit(expand(e1, deps));
arg1 = try_expand(e1, deps);
if (!arg1) return result;
result = m_util.str.mk_unit(arg1);
}
else if (m_util.str.is_index(e, e1, e2)) {
result = m_util.str.mk_index(expand(e1, deps), expand(e2, deps), m_autil.mk_int(0));
arg1 = try_expand(e1, deps);
arg2 = try_expand(e2, deps);
if (!arg1 || !arg2) return result;
result = m_util.str.mk_index(arg1, arg2, m_autil.mk_int(0));
}
else if (m_util.str.is_index(e, e1, e2, e3)) {
result = m_util.str.mk_index(expand(e1, deps), expand(e2, deps), e3);
arg1 = try_expand(e1, deps);
arg2 = try_expand(e2, deps);
if (!arg1 || !arg2) return result;
result = m_util.str.mk_index(arg1, arg2, e3);
}
else if (m.is_ite(e, e1, e2, e3)) {
if (ctx.e_internalized(e) && ctx.e_internalized(e2) && ctx.get_enode(e)->get_root() == ctx.get_enode(e2)->get_root()) {
result = expand(e2, deps);
result = try_expand(e2, deps);
if (!result) return result;
add_dependency(deps, ctx.get_enode(e), ctx.get_enode(e2));
}
else if (ctx.e_internalized(e) && ctx.e_internalized(e2) && ctx.get_enode(e)->get_root() == ctx.get_enode(e3)->get_root()) {
result = expand(e3, deps);
result = try_expand(e3, deps);
if (!result) return result;
add_dependency(deps, ctx.get_enode(e), ctx.get_enode(e3));
}
else {
literal lit(mk_literal(e1));
literal lit(mk_literal(e1));
#if 0
expr_ref sk_ite = mk_sk_ite(e1, e2, e3);
add_axiom(~lit, mk_eq(e2, sk_ite, false));
add_axiom( lit, mk_eq(e3, sk_ite, false));
result = sk_ite;
expr_ref sk_ite = mk_sk_ite(e1, e2, e3);
add_axiom(~lit, mk_eq(e2, sk_ite, false));
add_axiom( lit, mk_eq(e3, sk_ite, false));
result = sk_ite;
#else
switch (ctx.get_assignment(lit)) {
case l_true:
deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(lit)));
result = expand(e2, deps);
break;
case l_false:
deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(~lit)));
result = expand(e3, deps);
break;
case l_undef:
result = e;
m_reset_cache = true;
TRACE("seq", tout << "undef: " << result << "\n";
tout << lit << "@ level: " << ctx.get_scope_level() << "\n";);
break;
}
switch (ctx.get_assignment(lit)) {
case l_true:
deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(lit)));
result = try_expand(e2, deps);
if (!result) return result;
break;
case l_false:
deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(~lit)));
result = try_expand(e3, deps);
if (!result) return result;
break;
case l_undef:
result = e;
m_reset_cache = true;
TRACE("seq", tout << "undef: " << result << "\n";
tout << lit << "@ level: " << ctx.get_scope_level() << "\n";);
break;
}
#endif
}
}
@ -2962,6 +3062,7 @@ void theory_seq::deque_axiom(expr* n) {
add_length_axiom(n);
}
else if (m_util.str.is_empty(n) && !has_length(n) && !m_length.empty()) {
ensure_enode(n);
enforce_length(get_context().get_enode(n));
}
else if (m_util.str.is_index(n)) {
@ -3091,7 +3192,7 @@ void theory_seq::add_indexof_axiom(expr* i) {
*/
void theory_seq::add_replace_axiom(expr* r) {
expr* a, *s, *t;
expr* a = 0, *s = 0, *t = 0;
VERIFY(m_util.str.is_replace(r, a, s, t));
expr_ref x = mk_skolem(m_indexof_left, a, s);
expr_ref y = mk_skolem(m_indexof_right, a, s);
@ -3224,7 +3325,7 @@ void theory_seq::add_itos_length_axiom(expr* len) {
void theory_seq::propagate_in_re(expr* n, bool is_true) {
TRACE("seq", tout << mk_pp(n, m) << " <- " << (is_true?"true":"false") << "\n";);
expr* e1, *e2;
expr* e1 = 0, *e2 = 0;
VERIFY(m_util.str.is_in_re(n, e1, e2));
expr_ref tmp(n, m);
@ -3356,7 +3457,7 @@ bool theory_seq::get_length(expr* e, rational& val) const {
if (!tha) return false;
rational val1;
expr_ref len(m), len_val(m);
expr* e1, *e2;
expr* e1 = 0, *e2 = 0;
ptr_vector<expr> todo;
todo.push_back(e);
val.reset();
@ -3416,7 +3517,7 @@ bool theory_seq::get_length(expr* e, rational& val) const {
*/
void theory_seq::add_extract_axiom(expr* e) {
expr* s, *i, *l;
expr* s = 0, *i = 0, *l = 0;
VERIFY(m_util.str.is_extract(e, s, i, l));
if (is_tail(s, i, l)) {
add_tail_axiom(e, s);
@ -3567,8 +3668,8 @@ void theory_seq::add_at_axiom(expr* e) {
add_axiom(~i_ge_0, i_ge_len_s, mk_eq(one, len_e, false));
add_axiom(~i_ge_0, i_ge_len_s, mk_eq(i, len_x, false));
add_axiom(i_ge_0, mk_eq(s, emp, false));
add_axiom(~i_ge_len_s, mk_eq(s, emp, false));
add_axiom(i_ge_0, mk_eq(e, emp, false));
add_axiom(~i_ge_len_s, mk_eq(e, emp, false));
}
/**
@ -3576,7 +3677,7 @@ void theory_seq::add_at_axiom(expr* e) {
*/
void theory_seq::propagate_step(literal lit, expr* step) {
SASSERT(get_context().get_assignment(lit) == l_true);
expr* re, *acc, *s, *idx, *i, *j;
expr* re = 0, *acc = 0, *s = 0, *idx = 0, *i = 0, *j = 0;
VERIFY(is_step(step, s, idx, re, i, j, acc));
TRACE("seq", tout << mk_pp(step, m) << " -> " << mk_pp(acc, m) << "\n";);
propagate_lit(0, 1, &lit, mk_literal(acc));
@ -3737,7 +3838,7 @@ void theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp
void theory_seq::assign_eh(bool_var v, bool is_true) {
context & ctx = get_context();
expr* e = ctx.bool_var2expr(v);
expr* e1, *e2;
expr* e1 = 0, *e2 = 0;
expr_ref f(m);
bool change = false;
literal lit(v, !is_true);
@ -3875,7 +3976,7 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) {
enforce_length_coherence(n1, n2);
}
else if (n1 != n2 && m_util.is_re(n1->get_owner())) {
warning_msg("equality between regular expressions is not yet supported");
// ignore
// eautomaton* a1 = get_automaton(n1->get_owner());
// eautomaton* a2 = get_automaton(n2->get_owner());
// eautomaton* b1 = mk_difference(*a1, *a2);
@ -3995,7 +4096,7 @@ void theory_seq::relevant_eh(app* n) {
}
expr* arg;
if (m_util.str.is_length(n, arg) && !has_length(arg)) {
if (m_util.str.is_length(n, arg) && !has_length(arg) && get_context().e_internalized(arg)) {
enforce_length(get_context().get_enode(arg));
}
}
@ -4085,7 +4186,7 @@ expr_ref theory_seq::mk_step(expr* s, expr* idx, expr* re, unsigned i, unsigned
rej(s, idx, re, i) -> len(s) > idx if i is final
*/
void theory_seq::propagate_acc_rej_length(literal lit, expr* e) {
expr *s, * idx, *re;
expr *s = 0, *idx = 0, *re = 0;
unsigned src;
eautomaton* aut = 0;
bool is_acc;
@ -4114,7 +4215,7 @@ bool theory_seq::add_accept2step(expr* acc, bool& change) {
TRACE("seq", tout << mk_pp(acc, m) << "\n";);
SASSERT(ctx.get_assignment(acc) == l_true);
expr *e, * idx, *re;
expr *e = 0, *idx = 0, *re = 0;
expr_ref step(m);
unsigned src;
eautomaton* aut = 0;
@ -4193,7 +4294,7 @@ bool theory_seq::add_accept2step(expr* acc, bool& change) {
bool theory_seq::add_step2accept(expr* step, bool& change) {
context& ctx = get_context();
SASSERT(ctx.get_assignment(step) == l_true);
expr* re, *_acc, *s, *idx, *i, *j;
expr* re = 0, *_acc = 0, *s = 0, *idx = 0, *i = 0, *j = 0;
VERIFY(is_step(step, s, idx, re, i, j, _acc));
literal acc1 = mk_accept(s, idx, re, i);
switch (ctx.get_assignment(acc1)) {
@ -4242,7 +4343,7 @@ Recall we also have:
bool theory_seq::add_reject2reject(expr* rej, bool& change) {
context& ctx = get_context();
SASSERT(ctx.get_assignment(rej) == l_true);
expr* s, *idx, *re;
expr* s = 0, *idx = 0, *re = 0;
unsigned src;
rational r;
eautomaton* aut = 0;
@ -4304,7 +4405,7 @@ bool theory_seq::add_reject2reject(expr* rej, bool& change) {
void theory_seq::propagate_not_prefix(expr* e) {
context& ctx = get_context();
expr* e1, *e2;
expr* e1 = 0, *e2 = 0;
VERIFY(m_util.str.is_prefix(e, e1, e2));
literal lit = ctx.get_literal(e);
SASSERT(ctx.get_assignment(lit) == l_false);
@ -4333,7 +4434,7 @@ void theory_seq::propagate_not_prefix(expr* e) {
void theory_seq::propagate_not_prefix2(expr* e) {
context& ctx = get_context();
expr* e1, *e2;
expr* e1 = 0, *e2 = 0;
VERIFY(m_util.str.is_prefix(e, e1, e2));
literal lit = ctx.get_literal(e);
SASSERT(ctx.get_assignment(lit) == l_false);

8
src/smt/theory_seq.h
View file

@ -341,8 +341,8 @@ namespace smt {
virtual void init(context* ctx);
virtual final_check_status final_check_eh();
virtual bool internalize_atom(app* atom, bool) { return internalize_term(atom); }
virtual bool internalize_term(app*);
virtual bool internalize_atom(app* atom, bool);
virtual bool internalize_term(app*);
virtual void internalize_eq_eh(app * atom, bool_var v);
virtual void new_eq_eh(theory_var, theory_var);
virtual void new_diseq_eh(theory_var, theory_var);
@ -387,6 +387,7 @@ namespace smt {
vector<rational> const& ll, vector<rational> const& rl);
bool set_empty(expr* x);
bool is_complex(eq const& e);
bool internalize_re(expr* e);
bool check_extensionality();
bool check_contains();
@ -461,7 +462,10 @@ namespace smt {
expr_ref canonize(expr* e, dependency*& eqs);
bool canonize(expr* e, expr_ref_vector& es, dependency*& eqs);
bool canonize(expr_ref_vector const& es, expr_ref_vector& result, dependency*& eqs);
ptr_vector<expr> m_expand_todo;
expr_ref expand(expr* e, dependency*& eqs);
expr_ref expand1(expr* e, dependency*& eqs);
expr_ref try_expand(expr* e, dependency*& eqs);
void add_dependency(dependency*& dep, enode* a, enode* b);
void get_concat(expr* e, ptr_vector<expr>& concats);

152
src/smt/theory_str.cpp
View file

@ -21,14 +21,13 @@
#include"ast_pp.h"
#include"ast_ll_pp.h"
#include<list>
#include<vector>
#include<algorithm>
#include"theory_seq_empty.h"
#include"theory_arith.h"
#include"ast_util.h"
namespace smt {
theory_str::theory_str(ast_manager & m, theory_str_params const & params):
theory(m.mk_family_id("seq")),
m_params(params),
@ -99,7 +98,7 @@ namespace smt {
if (defaultCharset) {
// valid C strings can't contain the null byte ('\0')
charSetSize = 255;
char_set.resize(256, 0);
char_set.resize(256, 0);
int idx = 0;
// small letters
for (int i = 97; i < 123; i++) {
@ -233,11 +232,11 @@ namespace smt {
for (unsigned i = 0; i < num_args; ++i) {
enode * arg = e->get_arg(i);
theory_var v_arg = mk_var(arg);
TRACE("str", tout << "arg has theory var #" << v_arg << std::endl;);
TRACE("str", tout << "arg has theory var #" << v_arg << std::endl;); (void)v_arg;
}
theory_var v = mk_var(e);
TRACE("str", tout << "term has theory var #" << v << std::endl;);
TRACE("str", tout << "term has theory var #" << v << std::endl;); (void)v;
if (opt_EagerStringConstantLengthAssertions && u.str.is_string(term)) {
TRACE("str", tout << "eagerly asserting length of string term " << mk_pp(term, m) << std::endl;);
@ -258,7 +257,7 @@ namespace smt {
void theory_str::refresh_theory_var(expr * e) {
enode * en = ensure_enode(e);
theory_var v = mk_var(en);
theory_var v = mk_var(en); (void)v;
TRACE("str", tout << "refresh " << mk_pp(e, get_manager()) << ": v#" << v << std::endl;);
m_basicstr_axiom_todo.push_back(en);
}
@ -488,7 +487,6 @@ namespace smt {
app * theory_str::mk_str_var(std::string name) {
context & ctx = get_context();
ast_manager & m = get_manager();
TRACE("str", tout << "creating string variable " << name << " at scope level " << sLevel << std::endl;);
@ -506,7 +504,7 @@ namespace smt {
// this might help??
mk_var(ctx.get_enode(a));
m_basicstr_axiom_todo.push_back(ctx.get_enode(a));
TRACE("str", tout << "add " << mk_pp(a, m) << " to m_basicstr_axiom_todo" << std::endl;);
TRACE("str", tout << "add " << mk_pp(a, get_manager()) << " to m_basicstr_axiom_todo" << std::endl;);
variable_set.insert(a);
internal_variable_set.insert(a);
@ -517,7 +515,6 @@ namespace smt {
app * theory_str::mk_regex_rep_var() {
context & ctx = get_context();
ast_manager & m = get_manager();
sort * string_sort = u.str.mk_string_sort();
app * a = mk_fresh_const("regex", string_sort);
@ -528,7 +525,7 @@ namespace smt {
SASSERT(ctx.e_internalized(a));
mk_var(ctx.get_enode(a));
m_basicstr_axiom_todo.push_back(ctx.get_enode(a));
TRACE("str", tout << "add " << mk_pp(a, m) << " to m_basicstr_axiom_todo" << std::endl;);
TRACE("str", tout << "add " << mk_pp(a, get_manager()) << " to m_basicstr_axiom_todo" << std::endl;);
variable_set.insert(a);
//internal_variable_set.insert(a);
@ -934,8 +931,7 @@ namespace smt {
SASSERT(len_xy);
// build RHS: start by extracting x and y from Concat(x, y)
unsigned nArgs = a_cat->get_num_args();
SASSERT(nArgs == 2);
SASSERT(a_cat->get_num_args() == 2);
app * a_x = to_app(a_cat->get_arg(0));
app * a_y = to_app(a_cat->get_arg(1));
@ -1988,7 +1984,8 @@ namespace smt {
return NULL;
}
static inline std::string rational_to_string_if_exists(const rational & x, bool x_exists) {
// trace code helper
inline std::string rational_to_string_if_exists(const rational & x, bool x_exists) {
if (x_exists) {
return x.to_string();
} else {
@ -2055,7 +2052,7 @@ namespace smt {
<< "* |parent| = " << rational_to_string_if_exists(parentLen, parentLen_exists) << std::endl
<< "* |arg0| = " << rational_to_string_if_exists(arg0Len, arg0Len_exists) << std::endl
<< "* |arg1| = " << rational_to_string_if_exists(arg1Len, arg1Len_exists) << std::endl;
);
); (void)arg0Len_exists;
if (parentLen_exists && !arg1Len_exists) {
TRACE("str", tout << "make up len for arg1" << std::endl;);
@ -2126,7 +2123,8 @@ namespace smt {
<< "* |parent| = " << rational_to_string_if_exists(parentLen, parentLen_exists) << std::endl
<< "* |arg0| = " << rational_to_string_if_exists(arg0Len, arg0Len_exists) << std::endl
<< "* |arg1| = " << rational_to_string_if_exists(arg1Len, arg1Len_exists) << std::endl;
);
); (void)arg1Len_exists;
if (parentLen_exists && !arg0Len_exists) {
TRACE("str", tout << "make up len for arg0" << std::endl;);
expr_ref implyL11(m.mk_and(ctx.mk_eq_atom(mk_strlen(a_parent), mk_int(parentLen)),
@ -4497,8 +4495,6 @@ namespace smt {
}
void theory_str::process_unroll_eq_const_str(expr * unrollFunc, expr * constStr) {
ast_manager & m = get_manager();
if (!u.re.is_unroll(to_app(unrollFunc))) {
return;
}
@ -4510,8 +4506,8 @@ namespace smt {
zstring strValue;
u.str.is_string(constStr, strValue);
TRACE("str", tout << "unrollFunc: " << mk_pp(unrollFunc, m) << std::endl
<< "constStr: " << mk_pp(constStr, m) << std::endl;);
TRACE("str", tout << "unrollFunc: " << mk_pp(unrollFunc, get_manager()) << std::endl
<< "constStr: " << mk_pp(constStr, get_manager()) << std::endl;);
if (strValue == "") {
return;
@ -4656,7 +4652,7 @@ namespace smt {
}
}
bool theory_str::get_value(expr* e, rational& val) const {
bool theory_str::get_arith_value(expr* e, rational& val) const {
if (opt_DisableIntegerTheoryIntegration) {
TRACE("str", tout << "WARNING: integer theory integration disabled" << std::endl;);
return false;
@ -4785,7 +4781,7 @@ namespace smt {
}
});
if (ctx.e_internalized(len) && get_value(len, val1)) {
if (ctx.e_internalized(len) && get_arith_value(len, val1)) {
val += val1;
TRACE("str", tout << "integer theory: subexpression " << mk_ismt2_pp(len, m) << " has length " << val1 << std::endl;);
}
@ -4808,17 +4804,16 @@ namespace smt {
bool theory_str::in_same_eqc(expr * n1, expr * n2) {
if (n1 == n2) return true;
context & ctx = get_context();
ast_manager & m = get_manager();
// similar to get_eqc_value(), make absolutely sure
// that we've set this up properly for the context
if (!ctx.e_internalized(n1)) {
TRACE("str", tout << "WARNING: expression " << mk_ismt2_pp(n1, m) << " was not internalized" << std::endl;);
TRACE("str", tout << "WARNING: expression " << mk_ismt2_pp(n1, get_manager()) << " was not internalized" << std::endl;);
ctx.internalize(n1, false);
}
if (!ctx.e_internalized(n2)) {
TRACE("str", tout << "WARNING: expression " << mk_ismt2_pp(n2, m) << " was not internalized" << std::endl;);
TRACE("str", tout << "WARNING: expression " << mk_ismt2_pp(n2, get_manager()) << " was not internalized" << std::endl;);
ctx.internalize(n2, false);
}
@ -4877,7 +4872,7 @@ namespace smt {
expr * strAst = itor1->first;
expr * substrAst = itor1->second;
expr * boolVar;
expr * boolVar = NULL;
if (!contain_pair_bool_map.find(strAst, substrAst, boolVar)) {
TRACE("str", tout << "warning: no entry for boolVar in contain_pair_bool_map" << std::endl;);
}
@ -5014,7 +5009,7 @@ namespace smt {
expr * strAst = itor1->first;
expr * substrAst = itor1->second;
expr * boolVar;
expr * boolVar = NULL;
if (!contain_pair_bool_map.find(strAst, substrAst, boolVar)) {
TRACE("str", tout << "warning: no entry for boolVar in contain_pair_bool_map" << std::endl;);
}
@ -5625,8 +5620,7 @@ namespace smt {
}
void theory_str::print_grounded_concat(expr * node, std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap) {
ast_manager & m = get_manager();
TRACE("str", tout << mk_pp(node, m) << std::endl;);
TRACE("str", tout << mk_pp(node, get_manager()) << std::endl;);
if (groundedMap.find(node) != groundedMap.end()) {
std::map<std::vector<expr*>, std::set<expr*> >::iterator itor = groundedMap[node].begin();
for (; itor != groundedMap[node].end(); ++itor) {
@ -5634,13 +5628,13 @@ namespace smt {
tout << "\t[grounded] ";
std::vector<expr*>::const_iterator vIt = itor->first.begin();
for (; vIt != itor->first.end(); ++vIt) {
tout << mk_pp(*vIt, m) << ", ";
tout << mk_pp(*vIt, get_manager()) << ", ";
}
tout << std::endl;
tout << "\t[condition] ";
std::set<expr*>::iterator sIt = itor->second.begin();
for (; sIt != itor->second.end(); sIt++) {
tout << mk_pp(*sIt, m) << ", ";
tout << mk_pp(*sIt, get_manager()) << ", ";
}
tout << std::endl;
);
@ -6936,7 +6930,7 @@ namespace smt {
}
void theory_str::more_value_tests(expr * valTester, zstring valTesterValue) {
ast_manager & m = get_manager();
ast_manager & m = get_manager(); (void)m;
expr * fVar = valueTester_fvar_map[valTester];
if (m_params.m_UseBinarySearch) {
@ -6991,17 +6985,16 @@ namespace smt {
}
bool theory_str::free_var_attempt(expr * nn1, expr * nn2) {
ast_manager & m = get_manager();
zstring nn2_str;
if (internal_lenTest_vars.contains(nn1) && u.str.is_string(nn2, nn2_str)) {
TRACE("str", tout << "acting on equivalence between length tester var " << mk_ismt2_pp(nn1, m)
<< " and constant " << mk_ismt2_pp(nn2, m) << std::endl;);
TRACE("str", tout << "acting on equivalence between length tester var " << mk_pp(nn1, get_manager())
<< " and constant " << mk_pp(nn2, get_manager()) << std::endl;);
more_len_tests(nn1, nn2_str);
return true;
} else if (internal_valTest_vars.contains(nn1) && u.str.is_string(nn2, nn2_str)) {
if (nn2_str == "more") {
TRACE("str", tout << "acting on equivalence between value var " << mk_ismt2_pp(nn1, m)
<< " and constant " << mk_ismt2_pp(nn2, m) << std::endl;);
TRACE("str", tout << "acting on equivalence between value var " << mk_pp(nn1, get_manager())
<< " and constant " << mk_pp(nn2, get_manager()) << std::endl;);
more_value_tests(nn1, nn2_str);
}
return true;
@ -7302,6 +7295,7 @@ namespace smt {
// this might help??
theory_var v = mk_var(n);
TRACE("str", tout << "variable " << mk_ismt2_pp(ap, get_manager()) << " is #" << v << std::endl;);
(void)v;
}
}
} else if (ex_sort == bool_sort && !is_quantifier(ex)) {
@ -7388,7 +7382,6 @@ namespace smt {
}
void theory_str::init_search_eh() {
ast_manager & m = get_manager();
context & ctx = get_context();
TRACE("str",
@ -7396,7 +7389,7 @@ namespace smt {
unsigned nFormulas = ctx.get_num_asserted_formulas();
for (unsigned i = 0; i < nFormulas; ++i) {
expr * ex = ctx.get_asserted_formula(i);
tout << mk_ismt2_pp(ex, m) << (ctx.is_relevant(ex) ? " (rel)" : " (NOT REL)") << std::endl;
tout << mk_pp(ex, get_manager()) << (ctx.is_relevant(ex) ? " (rel)" : " (NOT REL)") << std::endl;
}
);
/*
@ -7411,36 +7404,6 @@ namespace smt {
set_up_axioms(ex);
}
/*
* Similar recursive descent, except over all initially assigned terms.
* This is done to find equalities between terms, etc. that we otherwise
* might not get a chance to see.
*/
/*
expr_ref_vector assignments(m);
ctx.get_assignments(assignments);
for (expr_ref_vector::iterator i = assignments.begin(); i != assignments.end(); ++i) {
expr * ex = *i;
if (m.is_eq(ex)) {
TRACE("str", tout << "processing assignment " << mk_ismt2_pp(ex, m) <<
": expr is equality" << std::endl;);
app * eq = (app*)ex;
SASSERT(eq->get_num_args() == 2);
expr * lhs = eq->get_arg(0);
expr * rhs = eq->get_arg(1);
enode * e_lhs = ctx.get_enode(lhs);
enode * e_rhs = ctx.get_enode(rhs);
std::pair<enode*,enode*> eq_pair(e_lhs, e_rhs);
m_str_eq_todo.push_back(eq_pair);
} else {
TRACE("str", tout << "processing assignment " << mk_ismt2_pp(ex, m)
<< ": expr ignored" << std::endl;);
}
}
*/
// this might be cheating but we need to make sure that certain maps are populated
// before the first call to new_eq_eh()
propagate();
@ -7476,8 +7439,7 @@ namespace smt {
}
void theory_str::assign_eh(bool_var v, bool is_true) {
context & ctx = get_context();
TRACE("str", tout << "assert: v" << v << " #" << ctx.bool_var2expr(v)->get_id() << " is_true: " << is_true << std::endl;);
TRACE("str", tout << "assert: v" << v << " #" << get_context().bool_var2expr(v)->get_id() << " is_true: " << is_true << std::endl;);
}
void theory_str::push_scope_eh() {
@ -7544,7 +7506,6 @@ namespace smt {
void theory_str::pop_scope_eh(unsigned num_scopes) {
sLevel -= num_scopes;
TRACE("str", tout << "pop " << num_scopes << " to " << sLevel << std::endl;);
ast_manager & m = get_manager();
TRACE_CODE(if (is_trace_enabled("t_str_dump_assign_on_scope_change")) { dump_assignments(); });
@ -7553,10 +7514,9 @@ namespace smt {
obj_map<expr, std::stack<T_cut *> >::iterator varItor = cut_var_map.begin();
while (varItor != cut_var_map.end()) {
expr * e = varItor->m_key;
std::stack<T_cut*> & val = cut_var_map[varItor->m_key];
while ((val.size() > 0) && (val.top()->level != 0) && (val.top()->level >= sLevel)) {
TRACE("str", tout << "remove cut info for " << mk_pp(e, m) << std::endl; print_cut_var(e, tout););
// TRACE("str", tout << "remove cut info for " << mk_pp(e, get_manager()) << std::endl; print_cut_var(e, tout););
// T_cut * aCut = val.top();
val.pop();
// dealloc(aCut);
@ -7578,8 +7538,7 @@ namespace smt {
ptr_vector<enode> new_m_basicstr;
for (ptr_vector<enode>::iterator it = m_basicstr_axiom_todo.begin(); it != m_basicstr_axiom_todo.end(); ++it) {
enode * e = *it;
app * a = e->get_owner();
TRACE("str", tout << "consider deleting " << mk_pp(a, get_manager())
TRACE("str", tout << "consider deleting " << mk_pp(e->get_owner(), get_manager())
<< ", enode scope level is " << e->get_iscope_lvl()
<< std::endl;);
if (e->get_iscope_lvl() <= (unsigned)sLevel) {
@ -8481,7 +8440,7 @@ namespace smt {
// check integer theory
rational Ival;
bool Ival_exists = get_value(a, Ival);
bool Ival_exists = get_arith_value(a, Ival);
if (Ival_exists) {
TRACE("str", tout << "integer theory assigns " << mk_pp(a, m) << " = " << Ival.to_string() << std::endl;);
// if that value is not -1, we can assert (str.to-int S) = Ival --> S = "Ival"
@ -8652,7 +8611,7 @@ namespace smt {
rational lenValue;
expr_ref concatlenExpr (mk_strlen(concat), m) ;
bool allLeafResolved = true;
if (! get_value(concatlenExpr, lenValue)) {
if (! get_arith_value(concatlenExpr, lenValue)) {
// the length fo concat is unresolved yet
if (get_len_value(concat, lenValue)) {
// but all leaf nodes have length information
@ -8689,7 +8648,7 @@ namespace smt {
expr * var = *it;
rational lenValue;
expr_ref varlen (mk_strlen(var), m) ;
if (! get_value(varlen, lenValue)) {
if (! get_arith_value(varlen, lenValue)) {
if (propagate_length_within_eqc(var)) {
axiomAdded = true;
}
@ -8862,7 +8821,7 @@ namespace smt {
continue;
}
bool hasEqcValue = false;
expr * eqcString = get_eqc_value(itor->first, hasEqcValue);
get_eqc_value(itor->first, hasEqcValue);
if (!hasEqcValue) {
TRACE("str", tout << "found free variable " << mk_pp(itor->first, m) << std::endl;);
needToAssignFreeVars = true;
@ -8870,7 +8829,7 @@ namespace smt {
// break;
} else {
// debug
TRACE("str", tout << "variable " << mk_pp(itor->first, m) << " = " << mk_pp(eqcString, m) << std::endl;);
// TRACE("str", tout << "variable " << mk_pp(itor->first, m) << " = " << mk_pp(eqcString, m) << std::endl;);
}
}
}
@ -9105,7 +9064,6 @@ namespace smt {
}
void theory_str::print_value_tester_list(svector<std::pair<int, expr*> > & testerList) {
ast_manager & m = get_manager();
TRACE("str",
int ss = testerList.size();
tout << "valueTesterList = {";
@ -9114,7 +9072,7 @@ namespace smt {
tout << std::endl;
}
tout << "(" << testerList[i].first << ", ";
tout << mk_ismt2_pp(testerList[i].second, m);
tout << mk_pp(testerList[i].second, get_manager());
tout << "), ";
}
tout << std::endl << "}" << std::endl;
@ -9194,7 +9152,7 @@ namespace smt {
// ----------------------------------------------------------------------------------------
int len = atoi(lenStr.encode().c_str());
bool coverAll = false;
vector<int_vector, true, long long> options;
vector<int_vector, true, size_t> options;
int_vector base;
TRACE("str", tout
@ -9217,8 +9175,8 @@ namespace smt {
coverAll = get_next_val_encode(val_range_map[lastestValIndi], base);
}
long long l = (tries) * distance;
long long h = l;
size_t l = (tries) * distance;
size_t h = l;
for (int i = 0; i < distance; i++) {
if (coverAll)
break;
@ -9239,10 +9197,10 @@ namespace smt {
);
// ----------------------------------------------------------------------------------------
expr_ref_vector orList(m), andList(m);
for (long long i = l; i < h; i++) {
for (size_t i = l; i < h; i++) {
orList.push_back(m.mk_eq(val_indicator, mk_string(longlong_to_string(i).c_str()) ));
if (m_params.m_AggressiveValueTesting) {
literal lit = mk_eq(val_indicator, mk_string(longlong_to_string(i).c_str()), false);
@ -9346,8 +9304,7 @@ namespace smt {
}
bool anEqcHasValue = false;
// Z3_ast anEqc = get_eqc_value(t, aTester, anEqcHasValue);
expr * aTester_eqc_value = get_eqc_value(aTester, anEqcHasValue);
get_eqc_value(aTester, anEqcHasValue);
if (!anEqcHasValue) {
TRACE("str", tout << "value tester " << mk_ismt2_pp(aTester, m)
<< " doesn't have an equivalence class value." << std::endl;);
@ -9359,8 +9316,8 @@ namespace smt {
<< mk_ismt2_pp(makeupAssert, m) << std::endl;);
assert_axiom(makeupAssert);
} else {
TRACE("str", tout << "value tester " << mk_ismt2_pp(aTester, m)
<< " == " << mk_ismt2_pp(aTester_eqc_value, m) << std::endl;);
// TRACE("str", tout << "value tester " << mk_ismt2_pp(aTester, m)
// << " == " << mk_ismt2_pp(aTester_eqc_value, m) << std::endl;);
}
}
@ -9514,8 +9471,8 @@ namespace smt {
items.reset();
rational low, high;
bool low_exists = lower_bound(cntInUnr, low);
bool high_exists = upper_bound(cntInUnr, high);
bool low_exists = lower_bound(cntInUnr, low); (void)low_exists;
bool high_exists = upper_bound(cntInUnr, high); (void)high_exists;
TRACE("str",
tout << "unroll " << mk_pp(unrFunc, mgr) << std::endl;
@ -9523,7 +9480,7 @@ namespace smt {
bool unrLenValue_exists = get_len_value(unrFunc, unrLenValue);
tout << "unroll length: " << (unrLenValue_exists ? unrLenValue.to_string() : "?") << std::endl;
rational cntInUnrValue;
bool cntHasValue = get_value(cntInUnr, cntInUnrValue);
bool cntHasValue = get_arith_value(cntInUnr, cntInUnrValue);
tout << "unroll count: " << (cntHasValue ? cntInUnrValue.to_string() : "?")
<< " low = "
<< (low_exists ? low.to_string() : "?")
@ -10266,7 +10223,7 @@ namespace smt {
} else {
tout << "no eqc string constant";
}
tout << std::endl;);
tout << std::endl;); (void)effectiveInScope;
if (effectiveLenInd == lenTesterInCbEq) {
effectiveLenIndiStr = lenTesterValue;
} else {
@ -10351,7 +10308,6 @@ namespace smt {
void theory_str::process_free_var(std::map<expr*, int> & freeVar_map) {
context & ctx = get_context();
ast_manager & m = get_manager();
std::set<expr*> eqcRepSet;
std::set<expr*> leafVarSet;
@ -10378,8 +10334,8 @@ namespace smt {
}
}
if (duplicated && dupVar != NULL) {
TRACE("str", tout << "Duplicated free variable found:" << mk_ismt2_pp(freeVar, m)
<< " = " << mk_ismt2_pp(dupVar, m) << " (SKIP)" << std::endl;);
TRACE("str", tout << "Duplicated free variable found:" << mk_pp(freeVar, get_manager())
<< " = " << mk_ismt2_pp(dupVar, get_manager()) << " (SKIP)" << std::endl;);
continue;
} else {
eqcRepSet.insert(freeVar);

4
src/smt/theory_str.h
View file

@ -219,7 +219,7 @@ protected:
/*
* If DisableIntegerTheoryIntegration is set to true,
* ALL calls to the integer theory integration methods
* (get_value, get_len_value, lower_bound, upper_bound)
* (get_arith_value, get_len_value, lower_bound, upper_bound)
* will ignore what the arithmetic solver believes about length terms,
* and will return no information.
*
@ -464,7 +464,7 @@ protected:
bool in_same_eqc(expr * n1, expr * n2);
expr * collect_eq_nodes(expr * n, expr_ref_vector & eqcSet);
bool get_value(expr* e, rational& val) const;
bool get_arith_value(expr* e, rational& val) const;
bool get_len_value(expr* e, rational& val);
bool lower_bound(expr* _e, rational& lo);
bool upper_bound(expr* _e, rational& hi);