mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-05 15:33:59 +00:00
Code Activity

Merge branch 'master' of https://github.com/Nils-Becker/z3

Browse source
This commit is contained in:
nilsbecker 2018-04-08 18:27:21 +02:00
commit b3aed5987c
195 changed files with 2123 additions and 2105 deletions
Download patch file Download diff file Expand all files Collapse all files

48
src/smt/asserted_formulas.cpp
View file

@ -27,8 +27,9 @@ Revision History:
#include "ast/macros/quasi_macros.h"
#include "smt/asserted_formulas.h"
asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
asserted_formulas::asserted_formulas(ast_manager & m, smt_params & sp, params_ref const& p):
m(m),
m_smt_params(sp),
m_params(p),
m_rewriter(m),
m_substitution(m),
@ -46,7 +47,6 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
m_refine_inj_axiom(*this),
m_max_bv_sharing_fn(*this),
m_elim_term_ite(*this),
m_pull_cheap_ite_trees(*this),
m_pull_nested_quantifiers(*this),
m_elim_bvs_from_quantifiers(*this),
m_cheap_quant_fourier_motzkin(*this),
@ -66,20 +66,20 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
}
void asserted_formulas::setup() {
switch (m_params.m_lift_ite) {
switch (m_smt_params.m_lift_ite) {
case LI_FULL:
m_params.m_ng_lift_ite = LI_NONE;
m_smt_params.m_ng_lift_ite = LI_NONE;
break;
case LI_CONSERVATIVE:
if (m_params.m_ng_lift_ite == LI_CONSERVATIVE)
m_params.m_ng_lift_ite = LI_NONE;
if (m_smt_params.m_ng_lift_ite == LI_CONSERVATIVE)
m_smt_params.m_ng_lift_ite = LI_NONE;
break;
default:
break;
}
if (m_params.m_relevancy_lvl == 0)
m_params.m_relevancy_lemma = false;
if (m_smt_params.m_relevancy_lvl == 0)
m_smt_params.m_relevancy_lemma = false;
}
@ -118,21 +118,24 @@ void asserted_formulas::push_assertion(expr * e, proof * pr, vector<justified_ex
}
}
void asserted_formulas::updt_params(params_ref const& p) {
m_params.append(p);
}
void asserted_formulas::set_eliminate_and(bool flag) {
if (flag == m_elim_and) return;
m_elim_and = flag;
params_ref p;
p.set_bool("pull_cheap_ite", false);
p.set_bool("elim_and", flag);
p.set_bool("arith_ineq_lhs", true);
p.set_bool("sort_sums", true);
p.set_bool("rewrite_patterns", true);
p.set_bool("eq2ineq", m_params.m_arith_eq2ineq);
p.set_bool("gcd_rounding", true);
p.set_bool("expand_select_store", true);
p.set_bool("bv_sort_ac", true);
p.set_bool("som", true);
m_rewriter.updt_params(p);
if (m_smt_params.m_pull_cheap_ite) m_params.set_bool("pull_cheap_ite", true);
m_params.set_bool("elim_and", flag);
m_params.set_bool("arith_ineq_lhs", true);
m_params.set_bool("sort_sums", true);
m_params.set_bool("rewrite_patterns", true);
m_params.set_bool("eq2ineq", m_smt_params.m_arith_eq2ineq);
m_params.set_bool("gcd_rounding", true);
m_params.set_bool("expand_select_store", true);
m_params.set_bool("bv_sort_ac", true);
m_params.set_bool("som", true);
m_rewriter.updt_params(m_params);
flush_cache();
}
@ -144,7 +147,7 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
if (inconsistent())
return;
if (m_params.m_preprocess) {
if (m_smt_params.m_preprocess) {
TRACE("assert_expr_bug", tout << r << "\n";);
set_eliminate_and(false); // do not eliminate and before nnf.
m_rewriter(e, r, pr);
@ -227,7 +230,7 @@ void asserted_formulas::reduce() {
return;
if (m_qhead == m_formulas.size())
return;
if (!m_params.m_preprocess)
if (!m_smt_params.m_preprocess)
return;
if (m_macro_manager.has_macros())
invoke(m_find_macros);
@ -241,7 +244,6 @@ void asserted_formulas::reduce() {
if (!invoke(m_nnf_cnf)) return;
set_eliminate_and(true);
if (!invoke(m_reduce_asserted_formulas)) return;
if (!invoke(m_pull_cheap_ite_trees)) return;
if (!invoke(m_pull_nested_quantifiers)) return;
if (!invoke(m_lift_ite)) return;
if (!invoke(m_ng_lift_ite)) return;

42
src/smt/asserted_formulas.h
View file

@ -26,7 +26,6 @@ Revision History:
#include "ast/rewriter/bit2int.h"
#include "ast/rewriter/maximize_ac_sharing.h"
#include "ast/rewriter/distribute_forall.h"
#include "ast/rewriter/pull_ite_tree.h"
#include "ast/rewriter/push_app_ite.h"
#include "ast/rewriter/inj_axiom.h"
#include "ast/rewriter/bv_elim.h"
@ -44,7 +43,8 @@ Revision History:
class asserted_formulas {
ast_manager & m;
smt_params & m_params;
smt_params & m_smt_params;
params_ref m_params;
th_rewriter m_rewriter;
expr_substitution m_substitution;
scoped_expr_substitution m_scoped_substitution;
@ -89,7 +89,7 @@ class asserted_formulas {
public:
find_macros_fn(asserted_formulas& af): simplify_fmls(af, "find-macros") {}
void operator()() override { af.find_macros_core(); }
bool should_apply() const override { return af.m_params.m_macro_finder && af.has_quantifiers(); }
bool should_apply() const override { return af.m_smt_params.m_macro_finder && af.has_quantifiers(); }
void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { UNREACHABLE(); }
};
@ -97,7 +97,7 @@ class asserted_formulas {
public:
apply_quasi_macros_fn(asserted_formulas& af): simplify_fmls(af, "find-quasi-macros") {}
void operator()() override { af.apply_quasi_macros(); }
bool should_apply() const override { return af.m_params.m_quasi_macros && af.has_quantifiers(); }
bool should_apply() const override { return af.m_smt_params.m_quasi_macros && af.has_quantifiers(); }
void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { UNREACHABLE(); }
};
@ -105,7 +105,7 @@ class asserted_formulas {
public:
nnf_cnf_fn(asserted_formulas& af): simplify_fmls(af, "nnf-cnf") {}
void operator()() override { af.nnf_cnf(); }
bool should_apply() const override { return af.m_params.m_nnf_cnf || (af.m_params.m_mbqi && af.has_quantifiers()); }
bool should_apply() const override { return af.m_smt_params.m_nnf_cnf || (af.m_smt_params.m_mbqi && af.has_quantifiers()); }
void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { UNREACHABLE(); }
};
@ -113,7 +113,7 @@ class asserted_formulas {
public:
propagate_values_fn(asserted_formulas& af): simplify_fmls(af, "propagate-values") {}
void operator()() override { af.propagate_values(); }
bool should_apply() const override { return af.m_params.m_propagate_values; }
bool should_apply() const override { return af.m_smt_params.m_propagate_values; }
void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { UNREACHABLE(); }
};
@ -122,30 +122,30 @@ class asserted_formulas {
public:
distribute_forall_fn(asserted_formulas& af): simplify_fmls(af, "distribute-forall"), m_functor(af.m) {}
void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_functor(j.get_fml(), n); }
bool should_apply() const override { return af.m_params.m_distribute_forall && af.has_quantifiers(); }
bool should_apply() const override { return af.m_smt_params.m_distribute_forall && af.has_quantifiers(); }
void post_op() override { af.reduce_and_solve(); TRACE("asserted_formulas", af.display(tout);); }
};
class pattern_inference_fn : public simplify_fmls {
pattern_inference_rw m_infer;
public:
pattern_inference_fn(asserted_formulas& af): simplify_fmls(af, "pattern-inference"), m_infer(af.m, af.m_params) {}
pattern_inference_fn(asserted_formulas& af): simplify_fmls(af, "pattern-inference"), m_infer(af.m, af.m_smt_params) {}
void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_infer(j.get_fml(), n, p); }
bool should_apply() const override { return af.m_params.m_ematching && af.has_quantifiers(); }
bool should_apply() const override { return af.m_smt_params.m_ematching && af.has_quantifiers(); }
};
class refine_inj_axiom_fn : public simplify_fmls {
public:
refine_inj_axiom_fn(asserted_formulas& af): simplify_fmls(af, "refine-injectivity") {}
void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override;
bool should_apply() const override { return af.m_params.m_refine_inj_axiom && af.has_quantifiers(); }
bool should_apply() const override { return af.m_smt_params.m_refine_inj_axiom && af.has_quantifiers(); }
};
class max_bv_sharing_fn : public simplify_fmls {
public:
max_bv_sharing_fn(asserted_formulas& af): simplify_fmls(af, "maximizing-bv-sharing") {}
void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { af.m_bv_sharing(j.get_fml(), n, p); }
bool should_apply() const override { return af.m_params.m_max_bv_sharing; }
bool should_apply() const override { return af.m_smt_params.m_max_bv_sharing; }
void post_op() override { af.m_reduce_asserted_formulas(); }
};
@ -154,7 +154,7 @@ class asserted_formulas {
public:
elim_term_ite_fn(asserted_formulas& af): simplify_fmls(af, "elim-term-ite"), m_elim(af.m, af.m_defined_names) {}
void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_elim(j.get_fml(), n, p); }
bool should_apply() const override { return af.m_params.m_eliminate_term_ite && af.m_params.m_lift_ite != LI_FULL; }
bool should_apply() const override { return af.m_smt_params.m_eliminate_term_ite && af.m_smt_params.m_lift_ite != LI_FULL; }
void post_op() override { af.m_formulas.append(m_elim.new_defs()); af.reduce_and_solve(); m_elim.reset(); }
};
@ -172,13 +172,12 @@ class asserted_formulas {
#define MK_SIMPLIFIERF(NAME, FUNCTOR, MSG, APP, REDUCE) MK_SIMPLIFIERA(NAME, FUNCTOR, MSG, APP, (af.m), REDUCE)
MK_SIMPLIFIERF(pull_cheap_ite_trees, pull_cheap_ite_tree_rw, "pull-cheap-ite-trees", af.m_params.m_pull_cheap_ite_trees, false);
MK_SIMPLIFIERF(pull_nested_quantifiers, pull_nested_quant, "pull-nested-quantifiers", af.m_params.m_pull_nested_quantifiers && af.has_quantifiers(), false);
MK_SIMPLIFIERF(cheap_quant_fourier_motzkin, elim_bounds_rw, "cheap-fourier-motzkin", af.m_params.m_eliminate_bounds && af.has_quantifiers(), true);
MK_SIMPLIFIERF(elim_bvs_from_quantifiers, bv_elim_rw, "eliminate-bit-vectors-from-quantifiers", af.m_params.m_bb_quantifiers, true);
MK_SIMPLIFIERF(apply_bit2int, bit2int, "propagate-bit-vector-over-integers", af.m_params.m_simplify_bit2int, true);
MK_SIMPLIFIERA(lift_ite, push_app_ite_rw, "lift-ite", af.m_params.m_lift_ite != LI_NONE, (af.m, af.m_params.m_lift_ite == LI_CONSERVATIVE), true);
MK_SIMPLIFIERA(ng_lift_ite, ng_push_app_ite_rw, "lift-ite", af.m_params.m_ng_lift_ite != LI_NONE, (af.m, af.m_params.m_ng_lift_ite == LI_CONSERVATIVE), true);
MK_SIMPLIFIERF(pull_nested_quantifiers, pull_nested_quant, "pull-nested-quantifiers", af.m_smt_params.m_pull_nested_quantifiers && af.has_quantifiers(), false);
MK_SIMPLIFIERF(cheap_quant_fourier_motzkin, elim_bounds_rw, "cheap-fourier-motzkin", af.m_smt_params.m_eliminate_bounds && af.has_quantifiers(), true);
MK_SIMPLIFIERF(elim_bvs_from_quantifiers, bv_elim_rw, "eliminate-bit-vectors-from-quantifiers", af.m_smt_params.m_bb_quantifiers, true);
MK_SIMPLIFIERF(apply_bit2int, bit2int, "propagate-bit-vector-over-integers", af.m_smt_params.m_simplify_bit2int, true);
MK_SIMPLIFIERA(lift_ite, push_app_ite_rw, "lift-ite", af.m_smt_params.m_lift_ite != LI_NONE, (af.m, af.m_smt_params.m_lift_ite == LI_CONSERVATIVE), true);
MK_SIMPLIFIERA(ng_lift_ite, ng_push_app_ite_rw, "lift-ite", af.m_smt_params.m_ng_lift_ite != LI_NONE, (af.m, af.m_smt_params.m_ng_lift_ite == LI_CONSERVATIVE), true);
reduce_asserted_formulas_fn m_reduce_asserted_formulas;
@ -187,7 +186,6 @@ class asserted_formulas {
refine_inj_axiom_fn m_refine_inj_axiom;
max_bv_sharing_fn m_max_bv_sharing_fn;
elim_term_ite_fn m_elim_term_ite;
pull_cheap_ite_trees m_pull_cheap_ite_trees;
pull_nested_quantifiers m_pull_nested_quantifiers;
elim_bvs_from_quantifiers m_elim_bvs_from_quantifiers;
cheap_quant_fourier_motzkin m_cheap_quant_fourier_motzkin;
@ -219,14 +217,14 @@ class asserted_formulas {
bool is_gt(expr* lhs, expr* rhs);
void compute_depth(expr* e);
unsigned depth(expr* e) { return m_expr2depth[e]; }
bool pull_cheap_ite_trees();
void init(unsigned num_formulas, expr * const * formulas, proof * const * prs);
public:
asserted_formulas(ast_manager & m, smt_params & p);
asserted_formulas(ast_manager & m, smt_params & smtp, params_ref const& p);
~asserted_formulas();
void updt_params(params_ref const& p);
bool has_quantifiers() const { return m_has_quantifiers; }
void setup();
void assert_expr(expr * e, proof * in_pr);

2
src/smt/mam.cpp
View file

@ -3927,7 +3927,7 @@ namespace smt {
}
#ifdef Z3DEBUG
virtual bool check_missing_instances() {
bool check_missing_instances() override {
TRACE("missing_instance", tout << "checking for missing instances...\n";);
flet<bool> l(m_check_missing_instances, true);
rematch(false);

2
src/smt/params/preprocessor_params.cpp
View file

@ -41,7 +41,7 @@ void preprocessor_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_lift_ite);
DISPLAY_PARAM(m_ng_lift_ite);
DISPLAY_PARAM(m_pull_cheap_ite_trees);
DISPLAY_PARAM(m_pull_cheap_ite);
DISPLAY_PARAM(m_pull_nested_quantifiers);
DISPLAY_PARAM(m_eliminate_term_ite);
DISPLAY_PARAM(m_macro_finder);

4
src/smt/params/preprocessor_params.h
View file

@ -32,7 +32,7 @@ struct preprocessor_params : public pattern_inference_params,
public bit_blaster_params {
lift_ite_kind m_lift_ite;
lift_ite_kind m_ng_lift_ite; // lift ite for non ground terms
bool m_pull_cheap_ite_trees;
bool m_pull_cheap_ite;
bool m_pull_nested_quantifiers;
bool m_eliminate_term_ite;
bool m_macro_finder;
@ -54,7 +54,7 @@ public:
preprocessor_params(params_ref const & p = params_ref()):
m_lift_ite(LI_NONE),
m_ng_lift_ite(LI_NONE),
m_pull_cheap_ite_trees(false),
m_pull_cheap_ite(false),
m_pull_nested_quantifiers(false),
m_eliminate_term_ite(false),
m_macro_finder(false),

13
src/smt/smt_context.cpp
View file

@ -45,7 +45,7 @@ namespace smt {
m_fparams(p),
m_params(_p),
m_setup(*this, p),
m_asserted_formulas(m, p),
m_asserted_formulas(m, p, _p),
m_qmanager(alloc(quantifier_manager, *this, p, _p)),
m_model_generator(alloc(model_generator, m)),
m_relevancy_propagator(mk_relevancy_propagator(*this)),
@ -132,6 +132,10 @@ namespace smt {
return !m_manager.limit().inc();
}
void context::updt_params(params_ref const& p) {
m_params.append(p);
m_asserted_formulas.updt_params(p);
}
void context::copy(context& src_ctx, context& dst_ctx) {
ast_manager& dst_m = dst_ctx.get_manager();
@ -3146,6 +3150,7 @@ namespace smt {
push_scope();
for (unsigned i = 0; i < num_assumptions; i++) {
expr * curr_assumption = assumptions[i];
if (m_manager.is_true(curr_assumption)) continue;
SASSERT(is_valid_assumption(m_manager, curr_assumption));
proof * pr = m_manager.mk_asserted(curr_assumption);
internalize_assertion(curr_assumption, pr, 0);
@ -3949,7 +3954,7 @@ namespace smt {
#if 0
{
static unsigned counter = 0;
static uint64 total = 0;
static uint64_t total = 0;
static unsigned max = 0;
counter++;
total += num_lits;
@ -4316,9 +4321,7 @@ 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 {
IF_VERBOSE(11, model_pp(verbose_stream(), *m_proto_model););
}
}

2
src/smt/smt_context.h
View file

@ -263,6 +263,8 @@ namespace smt {
return m_params;
}
void updt_params(params_ref const& p);
bool get_cancel_flag();
region & get_region() {

108
src/smt/smt_context_pp.cpp
View file

@ -19,7 +19,7 @@ Revision History:
#include "smt/smt_context.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
#include "ast/ast_smt_pp.h"
#include "ast/ast_pp_util.h"
#include "util/stats.h"
namespace smt {
@ -43,11 +43,10 @@ namespace smt {
return out << "RESOURCE_LIMIT";
case THEORY:
if (!m_incomplete_theories.empty()) {
ptr_vector<theory>::const_iterator it = m_incomplete_theories.begin();
ptr_vector<theory>::const_iterator end = m_incomplete_theories.end();
for (bool first = true; it != end; ++it) {
bool first = true;
for (theory* th : m_incomplete_theories) {
if (first) first = false; else out << " ";
out << (*it)->get_name();
out << th->get_name();
}
}
else {
@ -173,12 +172,10 @@ namespace smt {
void context::display_binary_clauses(std::ostream & out) const {
bool first = true;
vector<watch_list>::const_iterator it = m_watches.begin();
vector<watch_list>::const_iterator end = m_watches.end();
for (unsigned l_idx = 0; it != end; ++it, ++l_idx) {
literal l1 = to_literal(l_idx);
unsigned l_idx = 0;
for (watch_list const& wl : m_watches) {
literal l1 = to_literal(l_idx++);
literal neg_l1 = ~l1;
watch_list const & wl = *it;
literal const * it2 = wl.begin_literals();
literal const * end2 = wl.end_literals();
for (; it2 != end2; ++it2) {
@ -291,10 +288,7 @@ namespace smt {
}
void context::display_theories(std::ostream & out) const {
ptr_vector<theory>::const_iterator it = m_theory_set.begin();
ptr_vector<theory>::const_iterator end = m_theory_set.end();
for (; it != end; ++it) {
theory * th = *it;
for (theory* th : m_theory_set) {
th->display(out);
}
}
@ -393,10 +387,8 @@ namespace smt {
#endif
m_qmanager->collect_statistics(st);
m_asserted_formulas.collect_statistics(st);
ptr_vector<theory>::const_iterator it = m_theory_set.begin();
ptr_vector<theory>::const_iterator end = m_theory_set.end();
for (; it != end; ++it) {
(*it)->collect_statistics(st);
for (theory* th : m_theory_set) {
th->collect_statistics(st);
}
}
@ -413,19 +405,23 @@ namespace smt {
}
void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents, literal consequent, symbol const& logic) const {
ast_smt_pp pp(m_manager);
pp.set_benchmark_name("lemma");
pp.set_status("unsat");
pp.set_logic(logic);
ast_pp_util visitor(m_manager);
expr_ref_vector fmls(m_manager);
visitor.collect(fmls);
expr_ref n(m_manager);
for (unsigned i = 0; i < num_antecedents; i++) {
literal l = antecedents[i];
expr_ref n(m_manager);
literal2expr(l, n);
pp.add_assumption(n);
fmls.push_back(n);
}
expr_ref n(m_manager);
literal2expr(~consequent, n);
pp.display_smt2(out, n);
if (consequent != false_literal) {
literal2expr(~consequent, n);
fmls.push_back(n);
}
if (logic != symbol::null) out << "(set-logic " << logic << ")\n";
visitor.collect(fmls);
visitor.display_decls(out);
visitor.display_asserts(out, fmls, true);
}
static unsigned g_lemma_id = 0;
@ -448,25 +444,29 @@ namespace smt {
void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents,
unsigned num_eq_antecedents, enode_pair const * eq_antecedents,
literal consequent, symbol const& logic) const {
ast_smt_pp pp(m_manager);
pp.set_benchmark_name("lemma");
pp.set_status("unsat");
pp.set_logic(logic);
ast_pp_util visitor(m_manager);
expr_ref_vector fmls(m_manager);
visitor.collect(fmls);
expr_ref n(m_manager);
for (unsigned i = 0; i < num_antecedents; i++) {
literal l = antecedents[i];
expr_ref n(m_manager);
literal2expr(l, n);
pp.add_assumption(n);
fmls.push_back(n);
}
for (unsigned i = 0; i < num_eq_antecedents; i++) {
enode_pair const & p = eq_antecedents[i];
expr_ref eq(m_manager);
eq = m_manager.mk_eq(p.first->get_owner(), p.second->get_owner());
pp.add_assumption(eq);
n = m_manager.mk_eq(p.first->get_owner(), p.second->get_owner());
fmls.push_back(n);
}
expr_ref n(m_manager);
literal2expr(~consequent, n);
pp.display_smt2(out, n);
if (consequent != false_literal) {
literal2expr(~consequent, n);
fmls.push_back(n);
}
if (logic != symbol::null) out << "(set-logic " << logic << ")\n";
visitor.collect(fmls);
visitor.display_decls(out);
visitor.display_asserts(out, fmls, true);
}
void context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents,
@ -490,10 +490,7 @@ namespace smt {
*/
void context::display_normalized_enodes(std::ostream & out) const {
out << "normalized enodes:\n";
ptr_vector<enode>::const_iterator it = m_enodes.begin();
ptr_vector<enode>::const_iterator end = m_enodes.end();
for (; it != end; ++it) {
enode * n = *it;
for (enode * n : m_enodes) {
out << "#";
out.width(5);
out << std::left << n->get_owner_id() << " #";
@ -524,28 +521,23 @@ namespace smt {
}
void context::display_enodes_lbls(std::ostream & out) const {
ptr_vector<enode>::const_iterator it = m_enodes.begin();
ptr_vector<enode>::const_iterator end = m_enodes.end();
for (; it != end; ++it) {
enode * n = *it;
for (enode* n : m_enodes) {
n->display_lbls(out);
}
}
void context::display_decl2enodes(std::ostream & out) const {
out << "decl2enodes:\n";
vector<enode_vector>::const_iterator it1 = m_decl2enodes.begin();
vector<enode_vector>::const_iterator end1 = m_decl2enodes.end();
for (unsigned id = 0; it1 != end1; ++it1, ++id) {
enode_vector const & v = *it1;
unsigned id = 0;
for (enode_vector const& v : m_decl2enodes) {
if (!v.empty()) {
out << "id " << id << " ->";
enode_vector::const_iterator it2 = v.begin();
enode_vector::const_iterator end2 = v.end();
for (; it2 != end2; ++it2)
out << " #" << (*it2)->get_owner_id();
for (enode* n : v) {
out << " #" << n->get_owner_id();
}
out << "\n";
}
++id;
}
}
@ -588,20 +580,20 @@ namespace smt {
case b_justification::BIN_CLAUSE: {
literal l2 = j.get_literal();
out << "bin-clause ";
display_literal(out, l2);
display_literal_verbose(out, l2);
break;
}
case b_justification::CLAUSE: {
clause * cls = j.get_clause();
out << "clause ";
if (cls) display_literals(out, cls->get_num_literals(), cls->begin_literals());
if (cls) display_literals_verbose(out, cls->get_num_literals(), cls->begin_literals());
break;
}
case b_justification::JUSTIFICATION: {
out << "justification " << j.get_justification()->get_from_theory() << ": ";
literal_vector lits;
const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
display_literals(out, lits);
display_literals_verbose(out, lits);
break;
}
default:

19
src/smt/smt_enode.h
View file

@ -218,6 +218,15 @@ namespace smt {
return m_args;
}
class args {
enode const& n;
public:
args(enode const& n):n(n) {}
args(enode const* n):n(*n) {}
enode_vector::const_iterator begin() const { return n.get_args(); }
enode_vector::const_iterator end() const { return n.get_args() + n.get_num_args(); }
};
// unsigned get_id() const {
// return m_id;
// }
@ -287,6 +296,16 @@ namespace smt {
return m_commutative;
}
class parents {
enode const& n;
public:
parents(enode const& _n):n(_n) {}
parents(enode const* _n):n(*_n) {}
enode_vector::const_iterator begin() const { return n.begin_parents(); }
enode_vector::const_iterator end() const { return n.end_parents(); }
};
unsigned get_num_parents() const {
return m_parents.size();
}

10
src/smt/smt_kernel.cpp
View file

@ -123,7 +123,6 @@ namespace smt {
return m_kernel.preferred_sat(asms, cores);
}
lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
return m_kernel.find_mutexes(vars, mutexes);
}
@ -196,9 +195,7 @@ namespace smt {
}
void updt_params(params_ref const & p) {
// We don't need params2smt_params anymore. smt_params has support for reading params_ref.
// The update is performed at smt_kernel "users".
// params2smt_params(p, fparams());
m_kernel.updt_params(p);
}
};
@ -218,7 +215,6 @@ namespace smt {
imp::copy(*src.m_imp, *dst.m_imp);
}
bool kernel::set_logic(symbol logic) {
return m_imp->set_logic(logic);
}
@ -263,9 +259,9 @@ namespace smt {
}
void kernel::reset() {
ast_manager & _m = m();
ast_manager & _m = m();
smt_params & fps = m_imp->fparams();
params_ref ps = m_imp->params();
params_ref ps = m_imp->params();
#pragma omp critical (smt_kernel)
{
m_imp->~imp();

2
src/smt/smt_quantifier.cpp
View file

@ -288,7 +288,7 @@ namespace smt {
final_check_status final_check_eh(bool full) {
if (full) {
IF_VERBOSE(100, verbose_stream() << "(smt.final-check \"quantifiers\")\n";);
IF_VERBOSE(100, if (!m_quantifiers.empty()) verbose_stream() << "(smt.final-check \"quantifiers\")\n";);
final_check_status result = m_qi_queue.final_check_eh() ? FC_DONE : FC_CONTINUE;
final_check_status presult = m_plugin->final_check_eh(full);
if (presult != FC_DONE)

6
src/smt/smt_relevancy.cpp
View file

@ -527,7 +527,7 @@ namespace smt {
}
#ifdef Z3DEBUG
bool check_relevancy_app(app * n) const {
bool check_relevancy_app(app * n) const {
SASSERT(is_relevant(n));
unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
@ -537,7 +537,7 @@ namespace smt {
return true;
}
virtual bool check_relevancy_or(app * n, bool root) const {
bool check_relevancy_or(app * n, bool root) const override {
lbool val = root ? l_true : m_context.find_assignment(n);
if (val == l_false)
return check_relevancy_app(n);
@ -600,7 +600,7 @@ namespace smt {
return true;
}
bool check_relevancy(expr_ref_vector const & v) const {
bool check_relevancy(expr_ref_vector const & v) const override {
SASSERT(!can_propagate());
ast_manager & m = get_manager();
unsigned sz = v.size();

2
src/smt/smt_setup.cpp
View file

@ -507,7 +507,7 @@ namespace smt {
m_params.m_nnf_cnf = false;
if (st.m_max_ite_tree_depth > 50) {
m_params.m_arith_eq2ineq = false;
m_params.m_pull_cheap_ite_trees = true;
m_params.m_pull_cheap_ite = true;
m_params.m_arith_propagate_eqs = true;
m_params.m_relevancy_lvl = 2;
m_params.m_relevancy_lemma = false;

1
src/smt/smt_types.h
View file

@ -21,6 +21,7 @@ Revision History:
#include "util/list.h"
#include "util/vector.h"
#include "util/hashtable.h"
#include "util/lbool.h"
class model;

23
src/smt/theory_arith_core.h
View file

@ -469,7 +469,8 @@ namespace smt {
if (negated) l_conseq.neg();
TRACE("arith_axiom", tout << mk_pp(ante, m) << "\n" << mk_pp(conseq, m) << "\n";
tout << s_ante << "\n" << s_conseq << "\n";);
tout << s_ante << "\n" << s_conseq << "\n";
tout << l_ante << "\n" << l_conseq << "\n";);
// literal lits[2] = {l_ante, l_conseq};
mk_clause(l_ante, l_conseq, 0, nullptr);
@ -589,13 +590,13 @@ namespace smt {
}
//
// create the term: s := to_real(to_int(x)) - x
// create the term: s := x - to_real(to_int(x))
// add the bounds 0 <= s < 1
//
template<typename Ext>
void theory_arith<Ext>::mk_to_int_axiom(app * n) {
SASSERT(m_util.is_to_int(n));
ast_manager & m = get_manager();
ast_manager & m = get_manager();
expr* x = n->get_arg(0);
// to_int (to_real x) = x
@ -603,11 +604,15 @@ namespace smt {
mk_axiom(m.mk_false(), m.mk_eq(to_app(x)->get_arg(0), n));
return;
}
expr* to_r = m_util.mk_to_real(n);
expr_ref lo(m_util.mk_le(to_r, x), m);
expr_ref hi(m_util.mk_lt(x, m_util.mk_add(to_r, m_util.mk_numeral(rational(1), false))), m);
mk_axiom(m.mk_false(), lo);
mk_axiom(m.mk_false(), hi);
expr_ref to_r(m_util.mk_to_real(n), m);
expr_ref diff(m_util.mk_add(x, m_util.mk_mul(m_util.mk_real(-1), to_r)), m);
expr_ref lo(m_util.mk_ge(diff, m_util.mk_real(0)), m);
expr_ref hi(m_util.mk_ge(diff, m_util.mk_real(1)), m);
hi = m.mk_not(hi);
mk_axiom(m.mk_false(), lo, false);
mk_axiom(m.mk_false(), hi, false);
}
template<typename Ext>
@ -1202,7 +1207,7 @@ namespace smt {
template<typename Ext>
bool theory_arith<Ext>::internalize_atom(app * n, bool gate_ctx) {
TRACE("arith_internalize", tout << "internalising atom:\n" << mk_pp(n, this->get_manager()) << "\n";);
TRACE("arith_internalize", tout << "internalizing atom:\n" << mk_pp(n, this->get_manager()) << "\n";);
context & ctx = get_context();
SASSERT(m_util.is_le(n) || m_util.is_ge(n) || m_util.is_is_int(n));
SASSERT(!ctx.b_internalized(n));

193
src/smt/theory_datatype.cpp
View file

@ -36,6 +36,41 @@ namespace smt {
theory_id get_from_theory() const override { return null_theory_id; }
};
theory_datatype::final_check_st::final_check_st(theory_datatype * th) : th(th) {
SASSERT(th->m_to_unmark.empty());
SASSERT(th->m_to_unmark2.empty());
th->m_used_eqs.reset();
th->m_stack.reset();
th->m_parent.reset();
}
theory_datatype::final_check_st::~final_check_st() {
unmark_enodes(th->m_to_unmark.size(), th->m_to_unmark.c_ptr());
unmark_enodes2(th->m_to_unmark2.size(), th->m_to_unmark2.c_ptr());
th->m_to_unmark.reset();
th->m_to_unmark2.reset();
th->m_used_eqs.reset();
th->m_stack.reset();
th->m_parent.reset();
}
void theory_datatype::oc_mark_on_stack(enode * n) {
n = n->get_root();
n->set_mark();
m_to_unmark.push_back(n);
}
void theory_datatype::oc_mark_cycle_free(enode * n) {
n = n->get_root();
n->set_mark2();
m_to_unmark2.push_back(n);
}
void theory_datatype::oc_push_stack(enode * n) {
m_stack.push_back(std::make_pair(EXIT, n));
m_stack.push_back(std::make_pair(ENTER, n));
}
theory* theory_datatype::mk_fresh(context* new_ctx) {
return alloc(theory_datatype, new_ctx->get_manager(), m_params);
@ -167,7 +202,7 @@ namespace smt {
func_decl * upd = n->get_decl();
func_decl * acc = to_func_decl(upd->get_parameter(0).get_ast());
func_decl * con = m_util.get_accessor_constructor(acc);
func_decl * rec = m_util.get_constructor_recognizer(con);
func_decl * rec = m_util.get_constructor_is(con);
ptr_vector<func_decl> const & accessors = *m_util.get_constructor_accessors(con);
app_ref rec_app(m.mk_app(rec, arg1), m);
ctx.internalize(rec_app, false);
@ -389,10 +424,11 @@ namespace smt {
final_check_status theory_datatype::final_check_eh() {
int num_vars = get_num_vars();
final_check_status r = FC_DONE;
final_check_st _guard(this); // RAII for managing state
for (int v = 0; v < num_vars; v++) {
if (v == static_cast<int>(m_find.find(v))) {
enode * node = get_enode(v);
if (occurs_check(node)) {
if (!oc_cycle_free(node) && occurs_check(node)) {
// conflict was detected...
// return...
return FC_CONTINUE;
@ -410,6 +446,73 @@ namespace smt {
return r;
}
// Assuming `app` is equal to a constructor term, return the constructor enode
inline enode * theory_datatype::oc_get_cstor(enode * app) {
theory_var v = app->get_root()->get_th_var(get_id());
SASSERT(v != null_theory_var);
v = m_find.find(v);
var_data * d = m_var_data[v];
SASSERT(d->m_constructor);
return d->m_constructor;
}
// explain the cycle root -> ... -> app -> root
void theory_datatype::occurs_check_explain(enode * app, enode * root) {
TRACE("datatype", tout << "occurs_check_explain " << mk_bounded_pp(app->get_owner(), get_manager()) << " <-> " << mk_bounded_pp(root->get_owner(), get_manager()) << "\n";);
enode* app_parent = nullptr;
// first: explain that root=v, given that app=cstor(…,v,…)
for (enode * arg : enode::args(oc_get_cstor(app))) {
// found an argument which is equal to root
if (arg->get_root() == root->get_root()) {
if (arg != root)
m_used_eqs.push_back(enode_pair(arg, root));
break;
}
}
// now explain app=cstor(..,v,..) where v=root, and recurse with parent of app
while (app->get_root() != root->get_root()) {
enode * app_cstor = oc_get_cstor(app);
if (app != app_cstor)
m_used_eqs.push_back(enode_pair(app, app_cstor));
app_parent = m_parent[app->get_root()];
app = app_parent;
}
SASSERT(app->get_root() == root->get_root());
if (app != root)
m_used_eqs.push_back(enode_pair(app, root));
}
// start exploring subgraph below `app`
bool theory_datatype::occurs_check_enter(enode * app) {
oc_mark_on_stack(app);
theory_var v = app->get_root()->get_th_var(get_id());
if (v != null_theory_var) {
v = m_find.find(v);
var_data * d = m_var_data[v];
if (d->m_constructor) {
for (enode * arg : enode::args(d->m_constructor)) {
if (oc_cycle_free(arg)) {
continue;
}
if (oc_on_stack(arg)) {
// arg was explored before app, and is still on the stack: cycle
occurs_check_explain(app, arg);
return true;
}
// explore `arg` (with parent `app`)
if (m_util.is_datatype(get_manager().get_sort(arg->get_owner()))) {
m_parent.insert(arg->get_root(), app);
oc_push_stack(arg);
}
}
}
}
return false;
}
/**
\brief Check if n can be reached starting from n and following equalities and constructors.
For example, occur_check(a1) returns true in the following set of equalities:
@ -418,17 +521,39 @@ namespace smt {
a3 = cons(v3, a1)
*/
bool theory_datatype::occurs_check(enode * n) {
TRACE("datatype", tout << "occurs check: #" << n->get_owner_id() << "\n";);
m_to_unmark.reset();
m_used_eqs.reset();
m_main = n;
bool res = occurs_check_core(m_main);
unmark_enodes(m_to_unmark.size(), m_to_unmark.c_ptr());
TRACE("datatype", tout << "occurs check: #" << n->get_owner_id() << " " << mk_bounded_pp(n->get_owner(), get_manager()) << "\n";);
m_stats.m_occurs_check++;
bool res = false;
oc_push_stack(n);
// DFS traversal from `n`. Look at top element and explore it.
while (!res && !m_stack.empty()) {
stack_op op = m_stack.back().first;
enode * app = m_stack.back().second;
m_stack.pop_back();
if (oc_cycle_free(app)) continue;
TRACE("datatype", tout << "occurs check loop: #" << app->get_owner_id() << " " << mk_bounded_pp(app->get_owner(), get_manager()) << (op==ENTER?" enter":" exit")<< "\n";);
switch (op) {
case ENTER:
res = occurs_check_enter(app);
break;
case EXIT:
oc_mark_cycle_free(app);
break;
}
}
if (res) {
// m_used_eqs should contain conflict
context & ctx = get_context();
region & r = ctx.get_region();
ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), r, 0, nullptr, m_used_eqs.size(), m_used_eqs.c_ptr())));
TRACE("occurs_check",
TRACE("datatype",
tout << "occurs_check: true\n";
for (enode_pair const& p : m_used_eqs) {
tout << "eq: #" << p.first->get_owner_id() << " #" << p.second->get_owner_id() << "\n";
@ -437,48 +562,6 @@ namespace smt {
}
return res;
}
/**
\brief Auxiliary method for occurs_check.
TODO: improve performance.
*/
bool theory_datatype::occurs_check_core(enode * app) {
if (app->is_marked())
return false;
m_stats.m_occurs_check++;
app->set_mark();
m_to_unmark.push_back(app);
TRACE("datatype", tout << "occurs check_core: #" << app->get_owner_id() << " #" << m_main->get_owner_id() << "\n";);
theory_var v = app->get_root()->get_th_var(get_id());
if (v != null_theory_var) {
v = m_find.find(v);
var_data * d = m_var_data[v];
if (d->m_constructor) {
if (app != d->m_constructor)
m_used_eqs.push_back(enode_pair(app, d->m_constructor));
unsigned num_args = d->m_constructor->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
enode * arg = d->m_constructor->get_arg(i);
if (arg->get_root() == m_main->get_root()) {
if (arg != m_main)
m_used_eqs.push_back(enode_pair(arg, m_main));
return true;
}
if (m_util.is_datatype(get_manager().get_sort(arg->get_owner())) && occurs_check_core(arg))
return true;
}
if (app != d->m_constructor) {
SASSERT(m_used_eqs.back().first == app);
SASSERT(m_used_eqs.back().second == d->m_constructor);
m_used_eqs.pop_back();
}
}
}
return false;
}
void theory_datatype::reset_eh() {
m_trail_stack.reset();
@ -710,7 +793,7 @@ namespace smt {
literal consequent;
if (!r) {
ptr_vector<func_decl> const & constructors = *m_util.get_datatype_constructors(dt);
func_decl * rec = m_util.get_constructor_recognizer(constructors[unassigned_idx]);
func_decl * rec = m_util.get_constructor_is(constructors[unassigned_idx]);
app * rec_app = get_manager().mk_app(rec, n->get_owner());
ctx.internalize(rec_app, false);
consequent = literal(ctx.get_bool_var(rec_app));
@ -751,12 +834,12 @@ namespace smt {
m_stats.m_splits++;
if (d->m_recognizers.empty()) {
r = m_util.get_constructor_recognizer(non_rec_c);
r = m_util.get_constructor_is(non_rec_c);
}
else {
enode * recognizer = d->m_recognizers[non_rec_idx];
if (recognizer == nullptr) {
r = m_util.get_constructor_recognizer(non_rec_c);
r = m_util.get_constructor_is(non_rec_c);
}
else if (!ctx.is_relevant(recognizer)) {
ctx.mark_as_relevant(recognizer);
@ -776,7 +859,7 @@ namespace smt {
if (curr == nullptr) {
ptr_vector<func_decl> const & constructors = *m_util.get_datatype_constructors(s);
// found empty slot...
r = m_util.get_constructor_recognizer(constructors[idx]);
r = m_util.get_constructor_is(constructors[idx]);
break;
}
else if (!ctx.is_relevant(curr)) {

34
src/smt/theory_datatype.h
View file

@ -26,7 +26,6 @@ Revision History:
#include "smt/proto_model/datatype_factory.h"
namespace smt {
class theory_datatype : public theory {
typedef trail_stack<theory_datatype> th_trail_stack;
typedef union_find<theory_datatype> th_union_find;
@ -73,11 +72,36 @@ namespace smt {
void propagate_recognizer(theory_var v, enode * r);
void sign_recognizer_conflict(enode * c, enode * r);
ptr_vector<enode> m_to_unmark;
enode_pair_vector m_used_eqs;
enode * m_main;
typedef enum { ENTER, EXIT } stack_op;
typedef map<enode*, enode*, obj_ptr_hash<enode>, ptr_eq<enode> > parent_tbl;
typedef std::pair<stack_op, enode*> stack_entry;
ptr_vector<enode> m_to_unmark;
ptr_vector<enode> m_to_unmark2;
enode_pair_vector m_used_eqs; // conflict, if any
parent_tbl m_parent; // parent explanation for occurs_check
svector<stack_entry> m_stack; // stack for DFS for occurs_check
void oc_mark_on_stack(enode * n);
bool oc_on_stack(enode * n) const { return n->get_root()->is_marked(); }
void oc_mark_cycle_free(enode * n);
bool oc_cycle_free(enode * n) const { return n->get_root()->is_marked2(); }
void oc_push_stack(enode * n);
// class for managing state of final_check
class final_check_st {
theory_datatype * th;
public:
final_check_st(theory_datatype * th);
~final_check_st();
};
enode * oc_get_cstor(enode * n);
bool occurs_check(enode * n);
bool occurs_check_core(enode * n);
bool occurs_check_enter(enode * n);
void occurs_check_explain(enode * top, enode * root);
void mk_split(theory_var v);

6
src/smt/theory_dl.cpp
View file

@ -182,7 +182,7 @@ namespace smt {
if (n->get_decl() != v) {
expr* rep = m().mk_app(r, n);
uint64 vl;
uint64_t vl;
if (u().is_numeral_ext(n, vl)) {
assert_cnstr(m().mk_eq(rep, mk_bv_constant(vl, s)));
}
@ -237,12 +237,12 @@ namespace smt {
return true;
}
app* mk_bv_constant(uint64 val, sort* s) {
app* mk_bv_constant(uint64_t val, sort* s) {
return b().mk_numeral(rational(val, rational::ui64()), 64);
}
app* max_value(sort* s) {
uint64 sz;
uint64_t sz;
VERIFY(u().try_get_size(s, sz));
SASSERT(sz > 0);
return mk_bv_constant(sz-1, s);

169
src/smt/theory_seq.cpp
View file

@ -2346,28 +2346,31 @@ bool theory_seq::check_int_string() {
bool change = false;
for (unsigned i = 0; i < m_int_string.size(); ++i) {
expr* e = m_int_string[i].get(), *n;
if (m_util.str.is_itos(e) && add_itos_axiom(e)) {
if (m_util.str.is_itos(e) && add_itos_val_axiom(e)) {
change = true;
}
else if (m_util.str.is_stoi(e, n) && add_stoi_axiom(e)) {
else if (m_util.str.is_stoi(e, n) && add_stoi_val_axiom(e)) {
change = true;
}
}
return change;
}
bool theory_seq::add_stoi_axiom(expr* e) {
void theory_seq::add_stoi_axiom(expr* e) {
TRACE("seq", tout << mk_pp(e, m) << "\n";);
SASSERT(m_util.str.is_stoi(e));
literal l = mk_simplified_literal(m_autil.mk_ge(e, arith_util(m).mk_int(-1)));
add_axiom(l);
}
bool theory_seq::add_stoi_val_axiom(expr* e) {
context& ctx = get_context();
expr* n = nullptr;
rational val;
TRACE("seq", tout << mk_pp(e, m) << "\n";);
VERIFY(m_util.str.is_stoi(e, n));
if (!get_num_value(e, val)) {
literal l = mk_simplified_literal(m_autil.mk_ge(e, arith_util(m).mk_int(-1)));
add_axiom(l);
TRACE("seq", tout << l << " " << ctx.get_assignment(l) << "\n";
ctx.display(tout););
return true;
return false;
}
if (!m_stoi_axioms.contains(val)) {
m_stoi_axioms.insert(val);
@ -2401,8 +2404,7 @@ bool theory_seq::add_stoi_axiom(expr* e) {
lits.push_back(~is_digit(ith_char));
nums.push_back(digit2int(ith_char));
}
for (unsigned i = sz-1, c = 1; i > 0; c *= 10) {
--i;
for (unsigned i = sz, c = 1; i-- > 0; c *= 10) {
coeff = m_autil.mk_int(c);
nums[i] = m_autil.mk_mul(coeff, nums[i].get());
}
@ -2411,9 +2413,10 @@ bool theory_seq::add_stoi_axiom(expr* e) {
lits.push_back(mk_eq(e, num, false));
++m_stats.m_add_axiom;
m_new_propagation = true;
for (unsigned i = 0; i < lits.size(); ++i) {
ctx.mark_as_relevant(lits[i]);
for (literal lit : lits) {
ctx.mark_as_relevant(lit);
}
TRACE("seq", ctx.display_literals_verbose(tout, lits); tout << "\n";);
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
m_stoi_axioms.insert(val);
m_trail_stack.push(insert_map<theory_seq, rational_set, rational>(m_stoi_axioms, val));
@ -2445,54 +2448,60 @@ expr_ref theory_seq::digit2int(expr* ch) {
return expr_ref(mk_skolem(symbol("seq.digit2int"), ch, nullptr, nullptr, m_autil.mk_int()), m);
}
bool theory_seq::add_itos_axiom(expr* e) {
void theory_seq::add_itos_axiom(expr* e) {
rational val;
expr* n = nullptr;
TRACE("seq", tout << mk_pp(e, m) << "\n";);
VERIFY(m_util.str.is_itos(e, n));
// itos(n) = "" <=> n < 0
app_ref e1(m_util.str.mk_empty(m.get_sort(e)), m);
expr_ref zero(arith_util(m).mk_int(0), m);
literal eq1 = mk_eq(e1, e, false);
literal ge0 = mk_literal(m_autil.mk_ge(n, zero));
// n >= 0 => itos(n) != ""
// itos(n) = "" or n >= 0
add_axiom(~eq1, ~ge0);
add_axiom(eq1, ge0);
// n >= 0 => stoi(itos(n)) = n
app_ref stoi(m_util.str.mk_stoi(e), m);
add_axiom(~ge0, mk_eq(stoi, n, false));
// n >= 0 => itos(n) in (0-9)+
expr_ref num_re(m);
num_re = m_util.re.mk_range(m_util.str.mk_string(symbol("0")), m_util.str.mk_string(symbol("9")));
num_re = m_util.re.mk_plus(num_re);
app_ref in_re(m_util.re.mk_in_re(e, num_re), m);
add_axiom(~ge0, mk_literal(in_re));
}
bool theory_seq::add_itos_val_axiom(expr* e) {
context& ctx = get_context();
rational val;
expr* n = nullptr;
TRACE("seq", tout << mk_pp(e, m) << "\n";);
VERIFY(m_util.str.is_itos(e, n));
if (get_num_value(n, val)) {
if (!m_itos_axioms.contains(val)) {
m_itos_axioms.insert(val);
app_ref e1(m_util.str.mk_string(symbol(val.to_string().c_str())), m);
expr_ref n1(arith_util(m).mk_numeral(val, true), m);
bool change = false;
// itos(n) = "25" <=> n = 25
literal eq1 = mk_eq(n1, n , false);
literal eq2 = mk_eq(e, e1, false);
add_axiom(~eq1, eq2);
add_axiom(~eq2, eq1);
ctx.force_phase(eq1);
ctx.force_phase(eq2);
m_trail_stack.push(insert_map<theory_seq, rational_set, rational>(m_itos_axioms, val));
m_trail_stack.push(push_replay(alloc(replay_axiom, m, e)));
return true;
}
if (get_num_value(n, val) && !val.is_neg() && !m_itos_axioms.contains(val)) {
m_itos_axioms.insert(val);
app_ref e1(m_util.str.mk_string(symbol(val.to_string().c_str())), m);
expr_ref n1(arith_util(m).mk_numeral(val, true), m);
// itos(n) = "25" <=> n = 25
literal eq1 = mk_eq(n1, n , false);
literal eq2 = mk_eq(e, e1, false);
add_axiom(~eq1, eq2);
add_axiom(~eq2, eq1);
ctx.force_phase(eq1);
ctx.force_phase(eq2);
m_trail_stack.push(insert_map<theory_seq, rational_set, rational>(m_itos_axioms, val));
m_trail_stack.push(push_replay(alloc(replay_axiom, m, e)));
change = true;
}
else {
// stoi(itos(n)) = n
app_ref e2(m_util.str.mk_stoi(e), m);
if (ctx.e_internalized(e2) && ctx.get_enode(e2)->get_root() == ctx.get_enode(n)->get_root()) {
return false;
}
add_axiom(mk_eq(e2, n, false));
#if 1
expr_ref num_re(m), opt_re(m);
num_re = m_util.re.mk_range(m_util.str.mk_string(symbol("0")), m_util.str.mk_string(symbol("9")));
num_re = m_util.re.mk_plus(num_re);
opt_re = m_util.re.mk_opt(m_util.re.mk_to_re(m_util.str.mk_string(symbol("-"))));
num_re = m_util.re.mk_concat(opt_re, num_re);
app_ref in_re(m_util.re.mk_in_re(e, num_re), m);
internalize_term(in_re);
propagate_in_re(in_re, true);
#endif
m_trail_stack.push(push_replay(alloc(replay_axiom, m, e)));
return true;
}
return false;
return change;
}
void theory_seq::apply_sort_cnstr(enode* n, sort* s) {
@ -2721,13 +2730,12 @@ public:
bool is_string = th.m_util.is_string(m_sort);
expr_ref result(th.m);
if (is_string) {
svector<unsigned> sbuffer;
unsigned_vector sbuffer;
bv_util bv(th.m);
rational val;
unsigned sz;
for (unsigned i = 0; i < m_source.size(); ++i) {
switch (m_source[i]) {
for (source_t src : m_source) {
switch (src) {
case unit_source: {
VERIFY(bv.is_numeral(values[j++], val, sz));
sbuffer.push_back(val.get_unsigned());
@ -2757,12 +2765,13 @@ public:
break;
}
}
// TRACE("seq", tout << src << " " << sbuffer << "\n";);
}
result = th.m_util.str.mk_string(zstring(sbuffer.size(), sbuffer.c_ptr()));
}
else {
for (unsigned i = 0; i < m_source.size(); ++i) {
switch (m_source[i]) {
for (source_t src : m_source) {
switch (src) {
case unit_source:
args.push_back(th.m_util.str.mk_unit(values[j++]));
break;
@ -2804,8 +2813,8 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
seq_value_proc* sv = alloc(seq_value_proc, *this, srt);
TRACE("seq", tout << mk_pp(e, m) << "\n";);
for (unsigned i = 0; i < concats.size(); ++i) {
expr* c = concats[i], *c1;
for (expr* c : concats) {
expr *c1;
TRACE("seq", tout << mk_pp(c, m) << "\n";);
if (m_util.str.is_unit(c, c1)) {
if (ctx.e_internalized(c1)) {
@ -3048,8 +3057,11 @@ expr_ref theory_seq::expand1(expr* e0, dependency*& eqs) {
enode* n2 = ctx.get_enode(e1);
res = m_util.str.mk_string(symbol(val.to_string().c_str()));
#if 1
if (val.is_neg()) {
result = e;
}
// TBD remove this: using roots is unsound for propagation.
if (n1->get_root() == n2->get_root()) {
else if (n1->get_root() == n2->get_root()) {
result = res;
deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(n1, n2)));
}
@ -3147,6 +3159,9 @@ void theory_seq::deque_axiom(expr* n) {
else if (m_util.str.is_itos(n)) {
add_itos_axiom(n);
}
else if (m_util.str.is_stoi(n)) {
add_stoi_axiom(n);
}
}
@ -3366,9 +3381,9 @@ void theory_seq::add_itos_length_axiom(expr* len) {
rational len1, len2;
rational ten(10);
if (get_num_value(n, len1)) {
bool neg = len1.is_neg();
if (neg) len1.neg();
num_char1 = neg?2:1;
if (len1.is_neg()) {
return;
}
// 0 <= x < 10
// 10 <= x < 100
// 100 <= x < 1000
@ -3387,13 +3402,12 @@ void theory_seq::add_itos_length_axiom(expr* len) {
literal len_le(mk_literal(m_autil.mk_le(len, m_autil.mk_int(num_char))));
literal len_ge(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(num_char))));
literal n_ge_0(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(0))));
add_axiom(~n_ge_0, mk_literal(m_autil.mk_ge(len, m_autil.mk_int(1))));
if (num_char == 1) {
add_axiom(len_ge);
literal n_ge_0(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(0))));
literal n_ge_10(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(10))));
add_axiom(~n_ge_0, n_ge_10, len_le);
add_axiom(~len_le, n_ge_0);
add_axiom(~len_le, ~n_ge_10);
return;
}
@ -3401,22 +3415,13 @@ void theory_seq::add_itos_length_axiom(expr* len) {
for (unsigned i = 2; i < num_char; ++i) {
hi *= ten;
}
// n <= -hi or n >= hi*10 <=> len >= num_chars
// -10*hi < n < 100*hi <=> len <= num_chars
literal n_le_hi = mk_literal(m_autil.mk_le(n, m_autil.mk_numeral(-hi, true)));
// n >= hi*10 <=> len >= num_chars
// n < 100*hi <=> len <= num_chars
literal n_ge_10hi = mk_literal(m_autil.mk_ge(n, m_autil.mk_numeral(ten*hi, true)));
literal n_le_m10hi = mk_literal(m_autil.mk_le(n, m_autil.mk_numeral(-ten*hi, true)));
literal n_ge_100hi = mk_literal(m_autil.mk_ge(n, m_autil.mk_numeral(ten*ten*hi, true)));
add_axiom(~n_le_hi, len_ge);
add_axiom(~n_ge_10hi, len_ge);
add_axiom(n_le_hi, n_ge_10hi, ~len_ge);
add_axiom(n_le_m10hi, n_ge_100hi, len_le);
add_axiom(~n_le_m10hi, ~len_le);
add_axiom(~n_ge_100hi, ~len_le);
add_axiom(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(1))));
}
@ -3729,6 +3734,7 @@ bool theory_seq::is_extract_suffix(expr* s, expr* i, expr* l) {
/*
0 <= l <= len(s) => s = ey & l = len(e)
len(s) < l => s = e
*/
void theory_seq::add_extract_prefix_axiom(expr* e, expr* s, expr* l) {
TRACE("seq", tout << mk_pp(e, m) << " " << mk_pp(s, m) << " " << mk_pp(l, m) << "\n";);
@ -3743,6 +3749,7 @@ void theory_seq::add_extract_prefix_axiom(expr* e, expr* s, expr* l) {
add_axiom(~l_ge_0, ~l_le_s, mk_seq_eq(s, ey));
add_axiom(~l_ge_0, ~l_le_s, mk_eq(l, le, false));
add_axiom(~l_ge_0, ~l_le_s, mk_eq(ls_minus_l, m_util.str.mk_length(y), false));
add_axiom(l_le_s, mk_eq(e, s, false));
}
/*
@ -4214,7 +4221,9 @@ void theory_seq::relevant_eh(app* n) {
m_util.str.is_extract(n) ||
m_util.str.is_at(n) ||
m_util.str.is_empty(n) ||
m_util.str.is_string(n)) {
m_util.str.is_string(n) ||
m_util.str.is_itos(n) ||
m_util.str.is_stoi(n)) {
enque_axiom(n);
}

6
src/smt/theory_seq.h
View file

@ -507,8 +507,10 @@ namespace smt {
void add_elim_string_axiom(expr* n);
void add_at_axiom(expr* n);
void add_in_re_axiom(expr* n);
bool add_stoi_axiom(expr* n);
bool add_itos_axiom(expr* n);
void add_itos_axiom(expr* n);
void add_stoi_axiom(expr* n);
bool add_stoi_val_axiom(expr* n);
bool add_itos_val_axiom(expr* n);
literal is_digit(expr* ch);
expr_ref digit2int(expr* ch);
void add_itos_length_axiom(expr* n);

685
src/smt/theory_str.cpp
View file

File diff suppressed because it is too large Load diff

66
src/smt/theory_str.h
View file

@ -77,25 +77,8 @@ public:
void register_value(expr * n) override { /* Ignore */ }
};
// rather than modify obj_pair_map I inherit from it and add my own helper methods
class theory_str_contain_pair_bool_map_t : public obj_pair_map<expr, expr, expr*> {
public:
expr * operator[](std::pair<expr*, expr*> key) const {
expr * value;
bool found = this->find(key.first, key.second, value);
if (found) {
return value;
} else {
TRACE("t_str", tout << "WARNING: lookup miss in contain_pair_bool_map!" << std::endl;);
return nullptr;
}
}
bool contains(std::pair<expr*, expr*> key) const {
expr * unused;
return this->find(key.first, key.second, unused);
}
};
// NSB: added operator[] and contains to obj_pair_hashtable
class theory_str_contain_pair_bool_map_t : public obj_pair_map<expr, expr, expr*> {};
template<typename Ctx>
class binary_search_trail : public trail<Ctx> {
@ -169,7 +152,7 @@ class theory_str : public theory {
struct T_cut
{
int level;
std::map<expr*, int> vars;
obj_map<expr, int> vars;
T_cut() {
level = -100;
@ -279,6 +262,7 @@ protected:
ptr_vector<enode> m_concat_axiom_todo;
ptr_vector<enode> m_string_constant_length_todo;
ptr_vector<enode> m_concat_eval_todo;
expr_ref_vector m_delayed_assertions_todo;
// enode lists for library-aware/high-level string terms (e.g. substr, contains)
ptr_vector<enode> m_library_aware_axiom_todo;
@ -292,8 +276,8 @@ protected:
int tmpXorVarCount;
int tmpLenTestVarCount;
int tmpValTestVarCount;
std::map<std::pair<expr*, expr*>, std::map<int, expr*> > varForBreakConcat;
// obj_pair_map<expr, expr, std::map<int, expr*> > varForBreakConcat;
std::map<std::pair<expr*,expr*>, std::map<int, expr*> > varForBreakConcat;
bool avoidLoopCut;
bool loopDetected;
obj_map<expr, std::stack<T_cut*> > cut_var_map;
@ -303,7 +287,7 @@ protected:
obj_hashtable<expr> variable_set;
obj_hashtable<expr> internal_variable_set;
obj_hashtable<expr> regex_variable_set;
std::map<int, std::set<expr*> > internal_variable_scope_levels;
std::map<int, obj_hashtable<expr> > internal_variable_scope_levels;
obj_hashtable<expr> internal_lenTest_vars;
obj_hashtable<expr> internal_valTest_vars;
@ -312,30 +296,31 @@ protected:
obj_hashtable<expr> input_var_in_len;
obj_map<expr, unsigned int> fvar_len_count_map;
std::map<expr*, ptr_vector<expr> > fvar_lenTester_map;
obj_map<expr, ptr_vector<expr> > fvar_lenTester_map;
obj_map<expr, expr*> lenTester_fvar_map;
std::map<expr*, std::map<int, svector<std::pair<int, expr*> > > > fvar_valueTester_map;
std::map<expr*, expr*> valueTester_fvar_map;
std::map<expr*, int_vector> val_range_map;
obj_map<expr, std::map<int, svector<std::pair<int, expr*> > > > fvar_valueTester_map;
obj_map<expr, expr*> valueTester_fvar_map;
obj_map<expr, int_vector> val_range_map;
// This can't be an expr_ref_vector because the constructor is wrong,
// we would need to modify the allocator so we pass in ast_manager
std::map<expr*, std::map<std::set<expr*>, ptr_vector<expr> > > unroll_tries_map;
std::map<expr*, expr*> unroll_var_map;
std::map<std::pair<expr*, expr*>, expr*> concat_eq_unroll_ast_map;
obj_map<expr, std::map<std::set<expr*>, ptr_vector<expr> > > unroll_tries_map;
obj_map<expr, expr*> unroll_var_map;
obj_pair_map<expr, expr, expr*> concat_eq_unroll_ast_map;
expr_ref_vector contains_map;
theory_str_contain_pair_bool_map_t contain_pair_bool_map;
//obj_map<expr, obj_pair_set<expr, expr> > contain_pair_idx_map;
std::map<expr*, std::set<std::pair<expr*, expr*> > > contain_pair_idx_map;
obj_map<expr, std::set<std::pair<expr*, expr*> > > contain_pair_idx_map;
// TBD: do a curried map for determinism.
std::map<std::pair<expr*, zstring>, expr*> regex_in_bool_map;
std::map<expr*, std::set<zstring> > regex_in_var_reg_str_map;
std::map<expr*, nfa> regex_nfa_cache; // Regex term --> NFA
obj_map<expr, std::set<zstring> > regex_in_var_reg_str_map;
obj_map<expr, nfa> regex_nfa_cache; // Regex term --> NFA
svector<char> char_set;
std::map<char, int> charSetLookupTable;
@ -447,7 +432,7 @@ protected:
void instantiate_axiom_suffixof(enode * e);
void instantiate_axiom_Contains(enode * e);
void instantiate_axiom_Indexof(enode * e);
void instantiate_axiom_Indexof2(enode * e);
void instantiate_axiom_Indexof_extended(enode * e);
void instantiate_axiom_LastIndexof(enode * e);
void instantiate_axiom_Substr(enode * e);
void instantiate_axiom_Replace(enode * e);
@ -495,10 +480,11 @@ protected:
std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr *> & varConstMap,
std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap);
expr * dealias_node(expr * node, std::map<expr*, expr*> & varAliasMap, std::map<expr*, expr*> & concatAliasMap);
void get_grounded_concats(expr* node, std::map<expr*, expr*> & varAliasMap,
std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr*> & varConstMap,
std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap,
std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
void get_grounded_concats(unsigned depth,
expr* node, std::map<expr*, expr*> & varAliasMap,
std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr*> & varConstMap,
std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap,
std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
void print_grounded_concat(expr * node, std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
void check_subsequence(expr* str, expr* strDeAlias, expr* subStr, expr* subStrDeAlias, expr* boolVar,
std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);