mirror of
https://github.com/Z3Prover/z3
synced 2025-10-07 00:11:55 +00:00
Merge branch 'master' of https://github.com/z3prover/z3
This commit is contained in:
Nikolaj Bjorner
commit
30b0d5ba13
95 changed files with 1836 additions and 446 deletions
|
|
@ -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);
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
}
|
||||
|
||||
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -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: {
|
||||
|
|
|
|||
|
|
@ -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 {
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
||||
|
||||
|
||||
|
||||
};
|
||||
};
|
||||
|
|
|
|||
|
|
@ -317,6 +317,9 @@ namespace smt {
|
|||
|
||||
|
||||
void found_not_handled(expr* n) {
|
||||
if (a.is_div0(n)) {
|
||||
return;
|
||||
}
|
||||
m_not_handled = n;
|
||||
if (is_app(n) && is_underspecified(to_app(n))) {
|
||||
TRACE("arith", tout << "Unhandled: " << mk_pp(n, m) << "\n";);
|
||||
|
|
@ -785,7 +788,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
void internalize_eq_eh(app * atom, bool_var) {
|
||||
expr* lhs, *rhs;
|
||||
expr* lhs = 0, *rhs = 0;
|
||||
VERIFY(m.is_eq(atom, lhs, rhs));
|
||||
enode * n1 = get_enode(lhs);
|
||||
enode * n2 = get_enode(rhs);
|
||||
|
|
@ -903,7 +906,7 @@ namespace smt {
|
|||
// to_int (to_real x) = x
|
||||
// to_real(to_int(x)) <= x < to_real(to_int(x)) + 1
|
||||
void mk_to_int_axiom(app* n) {
|
||||
expr* x, *y;
|
||||
expr* x = 0, *y = 0;
|
||||
VERIFY (a.is_to_int(n, x));
|
||||
if (a.is_to_real(x, y)) {
|
||||
mk_axiom(th.mk_eq(y, n, false));
|
||||
|
|
@ -919,7 +922,7 @@ namespace smt {
|
|||
|
||||
// is_int(x) <=> to_real(to_int(x)) = x
|
||||
void mk_is_int_axiom(app* n) {
|
||||
expr* x;
|
||||
expr* x = 0;
|
||||
VERIFY(a.is_is_int(n, x));
|
||||
literal eq = th.mk_eq(a.mk_to_real(a.mk_to_int(x)), x, false);
|
||||
literal is_int = ctx().get_literal(n);
|
||||
|
|
@ -1417,12 +1420,14 @@ namespace smt {
|
|||
return;
|
||||
}
|
||||
int num_of_p = m_solver->settings().st().m_num_of_implied_bounds;
|
||||
(void)num_of_p;
|
||||
local_bound_propagator bp(*this);
|
||||
m_solver->propagate_bounds_for_touched_rows(bp);
|
||||
if (m.canceled()) {
|
||||
return;
|
||||
}
|
||||
int new_num_of_p = m_solver->settings().st().m_num_of_implied_bounds;
|
||||
(void)new_num_of_p;
|
||||
CTRACE("arith", new_num_of_p > num_of_p, tout << "found " << new_num_of_p << " implied bounds\n";);
|
||||
if (m_solver->get_status() == lp::lp_status::INFEASIBLE) {
|
||||
set_conflict();
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
@ -2246,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)) {
|
||||
|
|
@ -2316,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));
|
||||
|
|
@ -2398,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)) {
|
||||
|
|
@ -2602,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);
|
||||
|
|
@ -2615,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));
|
||||
|
|
@ -2863,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
|
||||
}
|
||||
}
|
||||
|
|
@ -3151,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);
|
||||
|
|
@ -3284,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);
|
||||
|
|
@ -3416,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();
|
||||
|
|
@ -3476,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);
|
||||
|
|
@ -3636,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));
|
||||
|
|
@ -3797,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);
|
||||
|
|
@ -4145,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;
|
||||
|
|
@ -4174,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;
|
||||
|
|
@ -4253,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)) {
|
||||
|
|
@ -4302,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;
|
||||
|
|
@ -4364,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);
|
||||
|
|
@ -4393,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);
|
||||
|
|
|
|||
|
|
@ -462,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);
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue