mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-24 03:57:51 +00:00
Code Activity

Merge remote-tracking branch 'upstream/master' into fix-length-testing

Browse source
This commit is contained in:
Murphy Berzish 2017-10-23 17:59:54 -04:00
commit 5e19e905fa
178 changed files with 3204 additions and 1694 deletions
Download patch file Download diff file Expand all files Collapse all files

103
src/smt/asserted_formulas.cpp
View file

@ -38,7 +38,7 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
m_qhead(0),
m_macro_manager(m),
m_bv_sharing(m),
m_inconsistent(false),
m_inconsistent(false),
m_has_quantifiers(false),
m_reduce_asserted_formulas(*this),
m_distribute_forall(*this),
@ -54,8 +54,8 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
m_lift_ite(*this),
m_ng_lift_ite(*this),
m_find_macros(*this),
m_propagate_values(*this),
m_nnf_cnf(*this),
m_propagate_values(*this),
m_nnf_cnf(*this),
m_apply_quasi_macros(*this) {
m_macro_finder = alloc(macro_finder, m, m_macro_manager);
@ -68,7 +68,7 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
void asserted_formulas::setup() {
switch (m_params.m_lift_ite) {
case LI_FULL:
m_params.m_ng_lift_ite = LI_NONE;
m_params.m_ng_lift_ite = LI_NONE;
break;
case LI_CONSERVATIVE:
if (m_params.m_ng_lift_ite == LI_CONSERVATIVE)
@ -77,7 +77,7 @@ void asserted_formulas::setup() {
default:
break;
}
if (m_params.m_relevancy_lvl == 0)
m_params.m_relevancy_lemma = false;
}
@ -93,7 +93,7 @@ void asserted_formulas::push_assertion(expr * e, proof * pr, vector<justified_ex
expr* e1 = 0;
if (m.is_false(e)) {
result.push_back(justified_expr(m, e, pr));
m_inconsistent = true;
m_inconsistent = true;
}
else if (m.is_true(e)) {
// skip
@ -110,8 +110,8 @@ void asserted_formulas::push_assertion(expr * e, proof * pr, vector<justified_ex
expr* arg = to_app(e1)->get_arg(i);
proof_ref _pr(m.mk_not_or_elim(pr, i), m);
expr_ref narg(mk_not(m, arg), m);
push_assertion(narg, _pr, result);
}
push_assertion(narg, _pr, result);
}
}
else {
result.push_back(justified_expr(m, e, pr));
@ -130,6 +130,7 @@ void asserted_formulas::set_eliminate_and(bool flag) {
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);
m_rewriter.updt_params(p);
flush_cache();
}
@ -139,11 +140,9 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
proof_ref in_pr(_in_pr, m), pr(_in_pr, m);
expr_ref r(e, m);
if (inconsistent())
if (inconsistent())
return;
m_has_quantifiers |= ::has_quantifiers(e);
if (m_params.m_preprocess) {
TRACE("assert_expr_bug", tout << r << "\n";);
set_eliminate_and(false); // do not eliminate and before nnf.
@ -156,6 +155,9 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
}
TRACE("assert_expr_bug", tout << "after...\n" << r << "\n";);
}
m_has_quantifiers |= ::has_quantifiers(e);
push_assertion(r, pr, m_formulas);
TRACE("asserted_formulas_bug", tout << "after assert_expr\n"; display(tout););
}
@ -170,7 +172,7 @@ void asserted_formulas::get_assertions(ptr_vector<expr> & result) const {
void asserted_formulas::push_scope() {
SASSERT(inconsistent() || m_qhead == m_formulas.size() || m.canceled());
TRACE("asserted_formulas_scopes", tout << "push:\n"; display(tout););
TRACE("asserted_formulas_scopes", tout << "before push: " << m_scopes.size() << "\n";);
m_scoped_substitution.push();
m_scopes.push_back(scope());
scope & s = m_scopes.back();
@ -181,10 +183,11 @@ void asserted_formulas::push_scope() {
m_bv_sharing.push_scope();
m_macro_manager.push_scope();
commit();
TRACE("asserted_formulas_scopes", tout << "after push: " << m_scopes.size() << "\n";);
}
void asserted_formulas::pop_scope(unsigned num_scopes) {
TRACE("asserted_formulas_scopes", tout << "before pop " << num_scopes << "\n"; display(tout););
TRACE("asserted_formulas_scopes", tout << "before pop " << num_scopes << " of " << m_scopes.size() << "\n";);
m_bv_sharing.pop_scope(num_scopes);
m_macro_manager.pop_scope(num_scopes);
unsigned new_lvl = m_scopes.size() - num_scopes;
@ -196,7 +199,7 @@ void asserted_formulas::pop_scope(unsigned num_scopes) {
m_qhead = s.m_formulas_lim;
m_scopes.shrink(new_lvl);
flush_cache();
TRACE("asserted_formulas_scopes", tout << "after pop " << num_scopes << "\n"; display(tout););
TRACE("asserted_formulas_scopes", tout << "after pop " << num_scopes << "\n";);
}
void asserted_formulas::reset() {
@ -211,7 +214,7 @@ void asserted_formulas::reset() {
bool asserted_formulas::check_well_sorted() const {
for (justified_expr const& je : m_formulas) {
if (!is_well_sorted(m, je.get_fml())) return false;
if (!is_well_sorted(m, je.get_fml())) return false;
}
return true;
}
@ -223,20 +226,20 @@ void asserted_formulas::reduce() {
return;
if (m_qhead == m_formulas.size())
return;
if (!m_params.m_preprocess)
return;
if (m_macro_manager.has_macros())
if (!m_params.m_preprocess)
return;
if (m_macro_manager.has_macros())
invoke(m_find_macros);
TRACE("before_reduce", display(tout););
CASSERT("well_sorted", check_well_sorted());
set_eliminate_and(false); // do not eliminate and before nnf.
if (!invoke(m_propagate_values)) return;
if (!invoke(m_find_macros)) return;
if (!invoke(m_nnf_cnf)) return;
set_eliminate_and(true);
if (!invoke(m_reduce_asserted_formulas)) return;
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;
@ -275,14 +278,14 @@ bool asserted_formulas::invoke(simplify_fmls& s) {
if (!s.should_apply()) return true;
IF_VERBOSE(10, verbose_stream() << "(smt." << s.id() << ")\n";);
s();
IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";);
TRACE("reduce_step_ll", ast_mark visited; display_ll(tout, visited););
CASSERT("well_sorted",check_well_sorted());
if (inconsistent() || canceled()) {
TRACE("after_reduce", display(tout););
TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited););
IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";);
TRACE("reduce_step_ll", ast_mark visited; display_ll(tout, visited););
CASSERT("well_sorted",check_well_sorted());
if (inconsistent() || canceled()) {
TRACE("after_reduce", display(tout););
TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited););
return false;
}
}
else {
return true;
}
@ -300,10 +303,10 @@ void asserted_formulas::display(std::ostream & out) const {
void asserted_formulas::display_ll(std::ostream & out, ast_mark & pp_visited) const {
if (!m_formulas.empty()) {
for (justified_expr const& f : m_formulas)
for (justified_expr const& f : m_formulas)
ast_def_ll_pp(out, m, f.get_fml(), pp_visited, true, false);
out << "asserted formulas:\n";
for (justified_expr const& f : m_formulas)
for (justified_expr const& f : m_formulas)
out << "#" << f.get_fml()->get_id() << " ";
out << "\n";
}
@ -331,9 +334,9 @@ void asserted_formulas::find_macros_core() {
void asserted_formulas::apply_quasi_macros() {
TRACE("before_quasi_macros", display(tout););
vector<justified_expr> new_fmls;
quasi_macros proc(m, m_macro_manager);
while (proc(m_formulas.size() - m_qhead,
m_formulas.c_ptr() + m_qhead,
quasi_macros proc(m, m_macro_manager);
while (proc(m_formulas.size() - m_qhead,
m_formulas.c_ptr() + m_qhead,
new_fmls)) {
swap_asserted_formulas(new_fmls);
new_fmls.reset();
@ -347,7 +350,7 @@ void asserted_formulas::nnf_cnf() {
vector<justified_expr> new_fmls;
expr_ref_vector push_todo(m);
proof_ref_vector push_todo_prs(m);
unsigned i = m_qhead;
unsigned sz = m_formulas.size();
TRACE("nnf_bug", tout << "i: " << i << " sz: " << sz << "\n";);
@ -377,7 +380,7 @@ void asserted_formulas::nnf_cnf() {
CASSERT("well_sorted",is_well_sorted(m, r1));
if (canceled()) {
return;
}
}
if (m.proofs_enabled())
pr = m.mk_modus_ponens(push_todo_prs.get(k), pr1);
push_assertion(r1, pr, new_fmls);
@ -388,8 +391,8 @@ void asserted_formulas::nnf_cnf() {
void asserted_formulas::simplify_fmls::operator()() {
vector<justified_expr> new_fmls;
unsigned sz = af.m_formulas.size();
for (unsigned i = af.m_qhead; i < sz; i++) {
unsigned sz = af.m_formulas.size();
for (unsigned i = af.m_qhead; i < sz; i++) {
auto& j = af.m_formulas[i];
expr_ref result(m);
proof_ref result_pr(m);
@ -405,8 +408,8 @@ void asserted_formulas::simplify_fmls::operator()() {
af.push_assertion(result, result_pr, new_fmls);
}
if (af.canceled()) return;
}
af.swap_asserted_formulas(new_fmls);
}
af.swap_asserted_formulas(new_fmls);
TRACE("asserted_formulas", af.display(tout););
post_op();
}
@ -472,12 +475,12 @@ void asserted_formulas::propagate_values() {
unsigned asserted_formulas::propagate_values(unsigned i) {
expr_ref n(m_formulas[i].get_fml(), m);
expr_ref new_n(m);
proof_ref new_pr(m);
m_rewriter(n, new_n, new_pr);
if (m.proofs_enabled()) {
expr_ref new_n(m);
proof_ref new_pr(m);
m_rewriter(n, new_n, new_pr);
if (m.proofs_enabled()) {
proof * pr = m_formulas[i].get_proof();
new_pr = m.mk_modus_ponens(pr, new_pr);
new_pr = m.mk_modus_ponens(pr, new_pr);
}
justified_expr j(m, new_n, new_pr);
m_formulas[i] = j;
@ -509,10 +512,10 @@ void asserted_formulas::update_substitution(expr* n, proof* pr) {
TRACE("propagate_values", tout << "incompatible " << mk_pp(n, m) << "\n";);
}
if (m.is_not(n, n1)) {
m_scoped_substitution.insert(n1, m.mk_false(), m.mk_iff_false(pr));
m_scoped_substitution.insert(n1, m.mk_false(), m.mk_iff_false(pr));
}
else {
m_scoped_substitution.insert(n, m.mk_true(), m.mk_iff_true(pr));
m_scoped_substitution.insert(n, m.mk_true(), m.mk_iff_true(pr));
}
}
@ -553,13 +556,13 @@ bool asserted_formulas::is_gt(expr* lhs, expr* rhs) {
}
UNREACHABLE();
}
return false;
}
void asserted_formulas::compute_depth(expr* e) {
ptr_vector<expr> todo;
todo.push_back(e);
todo.push_back(e);
while (!todo.empty()) {
e = todo.back();
unsigned d = 0;
@ -602,7 +605,7 @@ proof * asserted_formulas::get_inconsistency_proof() const {
return 0;
}
void asserted_formulas::refine_inj_axiom_fn::simplify(justified_expr const& j, expr_ref& n, proof_ref& p) {
void asserted_formulas::refine_inj_axiom_fn::simplify(justified_expr const& j, expr_ref& n, proof_ref& p) {
expr* f = j.get_fml();
if (is_quantifier(f) && simplify_inj_axiom(m, to_quantifier(f), n)) {
TRACE("inj_axiom", tout << "simplifying...\n" << mk_pp(f, m) << "\n" << n << "\n";);

24
src/smt/mam.cpp
View file

@ -1753,10 +1753,6 @@ namespace smt {
m_use_filters(use_filters) {
}
context & get_context() {
return m_context;
}
/**
\brief Create a new code tree for the given quantifier.
@ -2003,7 +1999,7 @@ namespace smt {
m_ast_manager(ctx.get_manager()),
m_mam(m),
m_use_filters(use_filters) {
m_args.resize(INIT_ARGS_SIZE, 0);
m_args.resize(INIT_ARGS_SIZE);
}
~interpreter() {
@ -2020,26 +2016,20 @@ namespace smt {
void execute(code_tree * t) {
TRACE("trigger_bug", tout << "execute for code tree:\n"; t->display(tout););
init(t);
enode_vector::const_iterator it = t->get_candidates().begin();
enode_vector::const_iterator end = t->get_candidates().end();
if (t->filter_candidates()) {
for (; it != end; ++it) {
enode * app = *it;
for (enode * app : t->get_candidates()) {
if (!app->is_marked() && app->is_cgr()) {
execute_core(t, app);
app->set_mark();
}
}
it = t->get_candidates().begin();
for (; it != end; ++it) {
enode * app = *it;
for (enode * app : t->get_candidates()) {
if (app->is_marked())
app->unset_mark();
}
}
else {
for (; it != end; ++it) {
enode * app = *it;
for (enode * app : t->get_candidates()) {
TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m_ast_manager) << "\n";);
if (app->is_cgr()) {
TRACE("trigger_bug", tout << "is_cgr\n";);
@ -2825,15 +2815,13 @@ namespace smt {
} // end of execute_core
void display_trees(std::ostream & out, const ptr_vector<code_tree> & trees) {
ptr_vector<code_tree>::const_iterator it = trees.begin();
ptr_vector<code_tree>::const_iterator end = trees.end();
unsigned lbl = 0;
for (; it != end; ++it, ++lbl) {
code_tree * tree = *it;
for (code_tree* tree : trees) {
if (tree) {
out << "tree for f" << lbl << "\n";
out << *tree;
}
++lbl;
}
}

5
src/smt/qi_queue.cpp
View file

@ -148,11 +148,8 @@ namespace smt {
}
void qi_queue::instantiate() {
svector<entry>::iterator it = m_new_entries.begin();
svector<entry>::iterator end = m_new_entries.end();
unsigned since_last_check = 0;
for (; it != end; ++it) {
entry & curr = *it;
for (entry & curr : m_new_entries) {
fingerprint * f = curr.m_qb;
quantifier * qa = static_cast<quantifier*>(f->get_data());

23
src/smt/smt_context.cpp
View file

@ -487,6 +487,7 @@ namespace smt {
*/
void context::add_eq(enode * n1, enode * n2, eq_justification js) {
unsigned old_trail_size = m_trail_stack.size();
scoped_suspend_rlimit _suspend_cancel(m_manager.limit());
try {
TRACE("add_eq", tout << "assigning: #" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";);
@ -541,10 +542,14 @@ namespace smt {
mark_as_relevant(r1);
}
TRACE("add_eq", tout << "to trail\n";);
push_trail(add_eq_trail(r1, n1, r2->get_num_parents()));
TRACE("add_eq", tout << "qmanager add_eq\n";);
m_qmanager->add_eq_eh(r1, r2);
TRACE("add_eq", tout << "merge theory_vars\n";);
merge_theory_vars(n2, n1, js);
// 'Proof' tree
@ -577,6 +582,7 @@ namespace smt {
#endif
TRACE("add_eq", tout << "remove_parents_from_cg_table\n";);
remove_parents_from_cg_table(r1);
enode * curr = r1;
@ -588,8 +594,10 @@ namespace smt {
SASSERT(r1->get_root() == r2);
TRACE("add_eq", tout << "reinsert_parents_into_cg_table\n";);
reinsert_parents_into_cg_table(r1, r2, n1, n2, js);
TRACE("add_eq", tout << "propagate_bool_enode_assignment\n";);
if (n2->is_bool())
propagate_bool_enode_assignment(r1, r2, n1, n2);
@ -604,6 +612,7 @@ namespace smt {
catch (...) {
// Restore trail size since procedure was interrupted in the middle.
// If the add_eq_trail remains on the trail stack, then Z3 may crash when the destructor is invoked.
TRACE("add_eq", tout << "add_eq interrupted. This is unsafe " << m_manager.limit().get_cancel_flag() << "\n";);
m_trail_stack.shrink(old_trail_size);
throw;
}
@ -972,7 +981,7 @@ namespace smt {
enode * parent = *it;
if (parent->is_cgc_enabled()) {
TRACE("add_eq_parents", tout << "removing: #" << parent->get_owner_id() << "\n";);
CTRACE("add_eq", !parent->is_cgr(),
CTRACE("add_eq", !parent->is_cgr() || !m_cg_table.contains_ptr(parent),
tout << "old num_parents: " << r2_num_parents << ", num_parents: " << r2->m_parents.size() << ", parent: #" <<
parent->get_owner_id() << ", parents: \n";
for (unsigned i = 0; i < r2->m_parents.size(); i++) {
@ -1277,7 +1286,7 @@ namespace smt {
else {
if (depth >= m_almost_cg_tables.size()) {
unsigned old_sz = m_almost_cg_tables.size();
m_almost_cg_tables.resize(depth+1, 0);
m_almost_cg_tables.resize(depth+1);
for (unsigned i = old_sz; i < depth + 1; i++)
m_almost_cg_tables[i] = alloc(almost_cg_table);
}
@ -4374,9 +4383,17 @@ namespace smt {
expr* fn = to_app(q->get_pattern(0))->get_arg(0);
expr* body = to_app(q->get_pattern(1))->get_arg(0);
SASSERT(is_app(fn));
// reverse argument order so that variable 0 starts at the beginning.
expr_ref_vector subst(m);
for (expr* arg : *to_app(fn)) {
subst.push_back(arg);
}
expr_ref bodyr(m);
var_subst sub(m, false);
sub(body, subst.size(), subst.c_ptr(), bodyr);
func_decl* f = to_app(fn)->get_decl();
func_interp* fi = alloc(func_interp, m, f->get_arity());
fi->set_else(body);
fi->set_else(bodyr);
m_model->register_decl(f, fi);
}
}

2
src/smt/smt_implied_equalities.cpp
View file

@ -284,7 +284,7 @@ namespace smt {
}
lbool reduce_cond(model_ref& model, expr* e) {
expr* e1, *e2;
expr* e1 = 0, *e2 = 0;
if (m.is_eq(e, e1, e2) && m_array_util.is_as_array(e1) && m_array_util.is_as_array(e2)) {
if (e1 == e2) {
return l_true;

20
src/smt/smt_internalizer.cpp
View file

@ -198,19 +198,19 @@ namespace smt {
if (get_depth(n) > DEEP_EXPR_THRESHOLD) {
// if the expression is deep, then execute topological sort to avoid
// stack overflow.
// a caveat is that theory internalizers do rely on recursive descent so
// internalization over these follows top-down
TRACE("deep_internalize", tout << "expression is deep: #" << n->get_id() << "\n" << mk_ll_pp(n, m_manager););
svector<expr_bool_pair> sorted_exprs;
top_sort_expr(n, sorted_exprs);
TRACE("deep_internalize",
svector<expr_bool_pair>::const_iterator it = sorted_exprs.begin();
svector<expr_bool_pair>::const_iterator end = sorted_exprs.end();
for (; it != end; ++it) {
tout << "#" << it->first->get_id() << " " << it->second << "\n";
});
svector<expr_bool_pair>::const_iterator it = sorted_exprs.begin();
svector<expr_bool_pair>::const_iterator end = sorted_exprs.end();
for (; it != end; ++it)
internalize(it->first, it->second);
TRACE("deep_internalize", for (auto & kv : sorted_exprs) tout << "#" << kv.first->get_id() << " " << kv.second << "\n"; );
for (auto & kv : sorted_exprs) {
expr* e = kv.first;
if (!is_app(e) ||
to_app(e)->get_family_id() == null_family_id ||
to_app(e)->get_family_id() == m_manager.get_basic_family_id())
internalize(e, kv.second);
}
}
SASSERT(m_manager.is_bool(n));
if (is_gate(m_manager, n)) {

18
src/smt/smt_model_generator.cpp
View file

@ -54,7 +54,7 @@ namespace smt {
ptr_vector<theory>::const_iterator it = m_context->begin_theories();
ptr_vector<theory>::const_iterator end = m_context->end_theories();
for (; it != end; ++it) {
TRACE("model_generator_bug", tout << "init_model for theory: " << (*it)->get_name() << "\n";);
TRACE("model", tout << "init_model for theory: " << (*it)->get_name() << "\n";);
(*it)->init_model(*this);
}
}
@ -91,7 +91,7 @@ namespace smt {
sort * s = m_manager.get_sort(r->get_owner());
model_value_proc * proc = 0;
if (m_manager.is_bool(s)) {
CTRACE("func_interp_bug", m_context->get_assignment(r) == l_undef,
CTRACE("model", m_context->get_assignment(r) == l_undef,
tout << mk_pp(r->get_owner(), m_manager) << "\n";);
SASSERT(m_context->get_assignment(r) != l_undef);
if (m_context->get_assignment(r) == l_true)
@ -108,7 +108,7 @@ namespace smt {
SASSERT(proc);
}
else {
TRACE("model_bug", tout << "creating fresh value for #" << r->get_owner_id() << "\n";);
TRACE("model", tout << "creating fresh value for #" << r->get_owner_id() << "\n";);
proc = alloc(fresh_value_proc, mk_extra_fresh_value(m_manager.get_sort(r->get_owner())));
}
}
@ -130,7 +130,7 @@ namespace smt {
if (!m_manager.is_model_value(n)) {
sort * s = m_manager.get_sort(r->get_owner());
n = m_model->get_fresh_value(s);
CTRACE("model_generator_bug", n == 0,
CTRACE("model", n == 0,
tout << mk_pp(r->get_owner(), m_manager) << "\nsort:\n" << mk_pp(s, m_manager) << "\n";
tout << "is_finite: " << m_model->is_finite(s) << "\n";);
}
@ -406,9 +406,11 @@ namespace smt {
*/
bool model_generator::include_func_interp(func_decl * f) const {
family_id fid = f->get_family_id();
TRACE("model", tout << f->get_name() << " " << fid << "\n";);
if (fid == null_family_id) return !m_hidden_ufs.contains(f);
if (fid == m_manager.get_basic_family_id()) return false;
theory * th = m_context->get_theory(fid);
TRACE("model", tout << th << "\n";);
if (!th) return true;
return th->include_func_interp(f);
}
@ -443,7 +445,7 @@ namespace smt {
SASSERT(m_model->has_interpretation(f));
SASSERT(m_model->get_func_interp(f) == fi);
// The entry must be new because n->get_cg() == n
TRACE("func_interp_bug",
TRACE("model",
tout << "insert new entry for:\n" << mk_ismt2_pp(n->get_owner(), m_manager) << "\nargs: ";
for (unsigned i = 0; i < num_args; i++) {
tout << "#" << n->get_arg(i)->get_owner_id() << " ";
@ -507,20 +509,20 @@ namespace smt {
void model_generator::register_macros() {
unsigned num = m_context->get_num_macros();
TRACE("register_macros", tout << "num. macros: " << num << "\n";);
TRACE("model", tout << "num. macros: " << num << "\n";);
expr_ref v(m_manager);
for (unsigned i = 0; i < num; i++) {
func_decl * f = m_context->get_macro_interpretation(i, v);
func_interp * fi = alloc(func_interp, m_manager, f->get_arity());
fi->set_else(v);
TRACE("register_macros", tout << f->get_name() << "\n" << mk_pp(v, m_manager) << "\n";);
TRACE("model", tout << f->get_name() << "\n" << mk_pp(v, m_manager) << "\n";);
m_model->register_decl(f, fi);
}
}
proto_model * model_generator::mk_model() {
SASSERT(!m_model);
TRACE("func_interp_bug", m_context->display(tout););
TRACE("model", m_context->display(tout););
init_model();
register_existing_model_values();
mk_bool_model();

1
src/smt/smt_setup.cpp
View file

@ -216,6 +216,7 @@ namespace smt {
void setup::setup_QF_DT() {
setup_QF_UF();
setup_datatypes();
}
void setup::setup_QF_BVRE() {

4
src/smt/smt_solver.cpp
View file

@ -109,8 +109,10 @@ namespace smt {
}
virtual void assert_expr(expr * t, expr * a) {
if (m_name2assertion.contains(a)) {
throw default_exception("named assertion defined twice");
}
solver_na2as::assert_expr(t, a);
SASSERT(!m_name2assertion.contains(a));
get_manager().inc_ref(t);
m_name2assertion.insert(a, t);
}

4
src/smt/smt_theory_var_list.h
View file

@ -67,9 +67,9 @@ namespace smt {
};
// 32 bit machine
COMPILE_TIME_ASSERT(sizeof(expr*) != 4 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int));
static_assert(sizeof(expr*) != 4 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int), "32 bit");
// 64 bit machine
COMPILE_TIME_ASSERT(sizeof(expr*) != 8 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int) + /* a structure must be aligned */ sizeof(int));
static_assert(sizeof(expr*) != 8 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int) + /* a structure must be aligned */ sizeof(int), "64 bit");
};
#endif /* SMT_THEORY_VAR_LIST_H_ */

2
src/smt/theory_arith_nl.h
View file

@ -780,7 +780,7 @@ namespace smt {
of a non linear monomial that is not satisfied by the current assignment.
if v >= l, then create the case split v >= l+1
else v <= u, then create the case split v <= u-1
else do nothing and return false.
else create the bound v = 0 and case split on it.
*/
template<typename Ext>
bool theory_arith<Ext>::branch_nl_int_var(theory_var v) {

67
src/smt/theory_array.cpp
View file

@ -53,18 +53,12 @@ namespace smt {
var_data * d2 = m_var_data[v2];
if (!d1->m_prop_upward && d2->m_prop_upward)
set_prop_upward(v1);
ptr_vector<enode>::iterator it = d2->m_stores.begin();
ptr_vector<enode>::iterator end = d2->m_stores.end();
for (; it != end; ++it)
add_store(v1, *it);
it = d2->m_parent_stores.begin();
end = d2->m_parent_stores.end();
for (; it != end; ++it)
add_parent_store(v1, *it);
it = d2->m_parent_selects.begin();
end = d2->m_parent_selects.end();
for (; it != end; ++it)
add_parent_select(v1, *it);
for (enode* n : d2->m_stores)
add_store(v1, n);
for (enode* n : d2->m_parent_stores)
add_parent_store(v1, n);
for (enode* n : d2->m_parent_selects)
add_parent_select(v1, n);
TRACE("array", tout << "after merge\n"; display_var(tout, v1););
}
@ -103,16 +97,11 @@ namespace smt {
d->m_parent_selects.push_back(s);
TRACE("array", tout << mk_pp(s->get_owner(), get_manager()) << " " << mk_pp(get_enode(v)->get_owner(), get_manager()) << "\n";);
m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d->m_parent_selects));
ptr_vector<enode>::iterator it = d->m_stores.begin();
ptr_vector<enode>::iterator end = d->m_stores.end();
for (; it != end; ++it) {
instantiate_axiom2a(s, *it);
for (enode* n : d->m_stores) {
instantiate_axiom2a(s, n);
}
if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
it = d->m_parent_stores.begin();
end = d->m_parent_stores.end();
for (; it != end; ++it) {
enode * store = *it;
for (enode* store : d->m_parent_stores) {
SASSERT(is_store(store));
if (!m_params.m_array_cg || store->is_cgr()) {
instantiate_axiom2b(s, store);
@ -129,27 +118,19 @@ namespace smt {
var_data * d = m_var_data[v];
d->m_parent_stores.push_back(s);
m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d->m_parent_stores));
if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
ptr_vector<enode>::iterator it = d->m_parent_selects.begin();
ptr_vector<enode>::iterator end = d->m_parent_selects.end();
for (; it != end; ++it)
if (!m_params.m_array_cg || (*it)->is_cgr())
instantiate_axiom2b(*it, s);
}
if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward)
for (enode* n : d->m_parent_selects)
if (!m_params.m_array_cg || n->is_cgr())
instantiate_axiom2b(n, s);
}
bool theory_array::instantiate_axiom2b_for(theory_var v) {
bool result = false;
var_data * d = m_var_data[v];
ptr_vector<enode>::iterator it = d->m_parent_stores.begin();
ptr_vector<enode>::iterator end = d->m_parent_stores.end();
for (; it != end; ++it) {
ptr_vector<enode>::iterator it2 = d->m_parent_selects.begin();
ptr_vector<enode>::iterator end2 = d->m_parent_selects.end();
for (; it2 != end2; ++it2)
if (instantiate_axiom2b(*it2, *it))
for (enode* n1 : d->m_parent_stores)
for (enode * n2 : d->m_parent_selects)
if (instantiate_axiom2b(n2, n1))
result = true;
}
return result;
}
@ -167,10 +148,8 @@ namespace smt {
d->m_prop_upward = true;
if (!m_params.m_array_delay_exp_axiom)
instantiate_axiom2b_for(v);
ptr_vector<enode>::iterator it = d->m_stores.begin();
ptr_vector<enode>::iterator end = d->m_stores.end();
for (; it != end; ++it)
set_prop_upward(*it);
for (enode * n : d->m_stores)
set_prop_upward(n);
}
}
@ -209,11 +188,9 @@ namespace smt {
}
d->m_stores.push_back(s);
m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d->m_stores));
ptr_vector<enode>::iterator it = d->m_parent_selects.begin();
ptr_vector<enode>::iterator end = d->m_parent_selects.end();
for (; it != end; ++it) {
SASSERT(is_select(*it));
instantiate_axiom2a(*it, s);
for (enode * n : d->m_parent_selects) {
SASSERT(is_select(n));
instantiate_axiom2a(n, s);
}
if (m_params.m_array_always_prop_upward || lambda_equiv_class_size >= 1)
set_prop_upward(s);
@ -374,7 +351,7 @@ namespace smt {
final_check_status theory_array::final_check_eh() {
m_final_check_idx++;
final_check_status r;
final_check_status r = FC_DONE;
if (m_params.m_array_lazy_ieq) {
// Delay the creation of interface equalities... The
// motivation is too give other theories and quantifier

9
src/smt/theory_array_base.cpp
View file

@ -210,17 +210,16 @@ namespace smt {
func_decl_ref_vector * theory_array_base::register_sort(sort * s_array) {
unsigned dimension = get_dimension(s_array);
func_decl_ref_vector * ext_skolems = 0;
if (!m_sort2skolem.find(s_array, ext_skolems)) {
array_util util(get_manager());
ast_manager & m = get_manager();
ext_skolems = alloc(func_decl_ref_vector, m);
for (unsigned i = 0; i < dimension; ++i) {
sort * ext_sk_domain[2] = { s_array, s_array };
parameter p(i);
func_decl * ext_sk_decl = m.mk_func_decl(get_id(), OP_ARRAY_EXT, 1, &p, 2, ext_sk_domain);
func_decl * ext_sk_decl = util.mk_array_ext(s_array, i);
ext_skolems->push_back(ext_sk_decl);
}
m_sort2skolem.insert(s_array, ext_skolems);
@ -617,8 +616,8 @@ namespace smt {
m_else_values.reset();
m_parents.reset();
m_parents.resize(num_vars, -1);
m_defaults.resize(num_vars, 0);
m_else_values.resize(num_vars, 0);
m_defaults.resize(num_vars);
m_else_values.resize(num_vars);
if (m_use_unspecified_default)
return;

2
src/smt/theory_datatype.cpp
View file

@ -620,7 +620,7 @@ namespace smt {
sort * s = recognizer->get_decl()->get_domain(0);
if (d->m_recognizers.empty()) {
SASSERT(m_util.is_datatype(s));
d->m_recognizers.resize(m_util.get_datatype_num_constructors(s), 0);
d->m_recognizers.resize(m_util.get_datatype_num_constructors(s));
}
SASSERT(d->m_recognizers.size() == m_util.get_datatype_num_constructors(s));
unsigned c_idx = m_util.get_recognizer_constructor_idx(recognizer->get_decl());

23
src/smt/theory_dense_diff_logic_def.h
View file

@ -151,14 +151,15 @@ namespace smt {
m_autil.is_numeral(rhs, _k);
numeral offset(_k);
app * s, * t;
if (m_autil.is_add(lhs) && to_app(lhs)->get_num_args() == 2 && is_times_minus_one(to_app(lhs)->get_arg(1), s)) {
t = to_app(to_app(lhs)->get_arg(0));
expr *arg1, *arg2;
if (m_autil.is_add(lhs, arg1, arg2) && is_times_minus_one(arg2, s)) {
t = to_app(arg1);
}
else if (m_autil.is_add(lhs) && to_app(lhs)->get_num_args() == 2 && is_times_minus_one(to_app(lhs)->get_arg(0), s)) {
t = to_app(to_app(lhs)->get_arg(1));
else if (m_autil.is_add(lhs, arg1, arg2) && is_times_minus_one(arg1, s)) {
t = to_app(arg2);
}
else if (m_autil.is_mul(lhs) && to_app(lhs)->get_num_args() == 2 && m_autil.is_minus_one(to_app(lhs)->get_arg(0))) {
s = to_app(to_app(lhs)->get_arg(1));
else if (m_autil.is_mul(lhs, arg1, arg2) && m_autil.is_minus_one(arg1)) {
s = to_app(arg2);
t = mk_zero_for(s);
}
else if (!m_autil.is_arith_expr(lhs)) {
@ -170,6 +171,7 @@ namespace smt {
found_non_diff_logic_expr(n);
return false;
}
TRACE("arith", tout << expr_ref(lhs, get_manager()) << " " << expr_ref(s, get_manager()) << " " << expr_ref(t, get_manager()) << "\n";);
source = internalize_term_core(s);
target = internalize_term_core(t);
if (source == null_theory_var || target == null_theory_var) {
@ -912,6 +914,8 @@ namespace smt {
}
verbose_stream() << " + " << m_objective_consts[v] << "\n";);
unsynch_mpq_manager mgr;
unsynch_mpq_inf_manager inf_mgr;
unsigned num_nodes = get_num_vars();
unsigned num_edges = m_edges.size();
S.ensure_var(num_nodes + num_edges + m_objectives.size());
@ -919,8 +923,9 @@ namespace smt {
numeral const& a = m_assignment[i];
rational fin = a.get_rational().to_rational();
rational inf = a.get_infinitesimal().to_rational();
mpq_inf q(fin.to_mpq(), inf.to_mpq());
mpq_inf q(mgr.dup(fin.to_mpq()), mgr.dup(inf.to_mpq()));
S.set_value(i, q);
inf_mgr.del(q);
}
for (unsigned i = 0; i < num_nodes; ++i) {
enode * n = get_enode(i);
@ -931,7 +936,6 @@ namespace smt {
}
}
svector<unsigned> vars;
unsynch_mpq_manager mgr;
scoped_mpq_vector coeffs(mgr);
coeffs.push_back(mpq(1));
coeffs.push_back(mpq(-1));
@ -952,8 +956,9 @@ namespace smt {
numeral const& w = e.m_offset;
rational fin = w.get_rational().to_rational();
rational inf = w.get_infinitesimal().to_rational();
mpq_inf q(fin.to_mpq(),inf.to_mpq());
mpq_inf q(mgr.dup(fin.to_mpq()), mgr.dup(inf.to_mpq()));
S.set_upper(base_var, q);
inf_mgr.del(q);
}
unsigned w = num_nodes + num_edges + v;

10
src/smt/theory_diff_logic_def.h
View file

@ -733,7 +733,6 @@ theory_var theory_diff_logic<Ext>::mk_term(app* n) {
source = mk_var(a);
for (unsigned i = 0; i < n->get_num_args(); ++i) {
expr* arg = n->get_arg(i);
std::cout << "internalize: " << mk_pp(arg, get_manager()) << " " << ctx.e_internalized(arg) << "\n";
if (!ctx.e_internalized(arg)) {
ctx.internalize(arg, false);
}
@ -1108,6 +1107,8 @@ unsigned theory_diff_logic<Ext>::simplex2edge(unsigned e) {
template<typename Ext>
void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
unsynch_mpq_manager mgr;
unsynch_mpq_inf_manager inf_mgr;
unsigned num_nodes = m_graph.get_num_nodes();
vector<dl_edge<GExt> > const& es = m_graph.get_all_edges();
S.ensure_var(num_simplex_vars());
@ -1115,13 +1116,13 @@ void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
numeral const& a = m_graph.get_assignment(i);
rational fin = a.get_rational().to_rational();
rational inf = a.get_infinitesimal().to_rational();
mpq_inf q(fin.to_mpq(), inf.to_mpq());
mpq_inf q(mgr.dup(fin.to_mpq()), mgr.dup(inf.to_mpq()));
S.set_value(node2simplex(i), q);
inf_mgr.del(q);
}
S.set_lower(node2simplex(get_zero()), mpq_inf(mpq(0), mpq(0)));
S.set_upper(node2simplex(get_zero()), mpq_inf(mpq(0), mpq(0)));
svector<unsigned> vars;
unsynch_mpq_manager mgr;
scoped_mpq_vector coeffs(mgr);
coeffs.push_back(mpq(1));
coeffs.push_back(mpq(-1));
@ -1146,8 +1147,9 @@ void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
numeral const& w = e.get_weight();
rational fin = w.get_rational().to_rational();
rational inf = w.get_infinitesimal().to_rational();
mpq_inf q(fin.to_mpq(),inf.to_mpq());
mpq_inf q(mgr.dup(fin.to_mpq()), mgr.dup(inf.to_mpq()));
S.set_upper(base_var, q);
inf_mgr.del(q);
}
else {
S.unset_upper(base_var);

18
src/smt/theory_fpa.cpp
View file

@ -884,22 +884,4 @@ namespace smt {
out << r->get_id() << " --> " << mk_ismt2_pp(n, m) << std::endl;
}
}
bool theory_fpa::include_func_interp(func_decl * f) {
TRACE("t_fpa", tout << "f = " << mk_ismt2_pp(f, get_manager()) << std::endl;);
if (f->get_family_id() == get_family_id()) {
bool include =
m_fpa_util.is_min_unspecified(f) ||
m_fpa_util.is_max_unspecified(f) ;
if (include && !m_is_added_to_model.contains(f)) {
//m_is_added_to_model.insert(f);
//get_manager().inc_ref(f);
return true;
}
return false;
}
else
return true;
}
};

3
src/smt/theory_fpa.h
View file

@ -158,7 +158,6 @@ namespace smt {
virtual char const * get_name() const { return "fpa"; }
virtual model_value_proc * mk_value(enode * n, model_generator & mg);
virtual bool include_func_interp(func_decl * f);
void assign_eh(bool_var v, bool is_true);
virtual void relevant_eh(app * n);
@ -180,8 +179,6 @@ namespace smt {
expr_ref convert_term(expr * e);
expr_ref convert_conversion_term(expr * e);
void add_trail(ast * a);
void attach_new_th_var(enode * n);
void assert_cnstr(expr * e);

6
src/smt/theory_lra.cpp
View file

@ -689,7 +689,7 @@ namespace smt {
SASSERT(!ctx().b_internalized(atom));
bool_var bv = ctx().mk_bool_var(atom);
ctx().set_var_theory(bv, get_id());
expr* n1, *n2;
expr* n1 = 0, *n2 = 0;
rational r;
lra_lp::bound_kind k;
theory_var v = null_theory_var;
@ -721,7 +721,7 @@ namespace smt {
SASSERT(!ctx().b_internalized(atom));
bool_var bv = ctx().mk_bool_var(atom);
ctx().set_var_theory(bv, get_id());
expr* n1, *n2;
expr* n1 = 0, *n2 = 0;
rational r;
lra_lp::bound_kind k;
theory_var v = null_theory_var;
@ -862,7 +862,7 @@ namespace smt {
void relevant_eh(app* n) {
TRACE("arith", tout << mk_pp(n, m) << "\n";);
expr* n1, *n2;
expr* n1 = 0, *n2 = 0;
if (a.is_mod(n, n1, n2))
mk_idiv_mod_axioms(n1, n2);
else if (a.is_rem(n, n1, n2))

3
src/smt/theory_pb.cpp
View file

@ -806,8 +806,9 @@ namespace smt {
if (c != 0) {
if (m_enable_simplex) {
row_info const& info = m_ineq_row_info.find(v);
unsynch_mpq_manager mgr;
scoped_eps_numeral coeff(m_mpq_inf_mgr);
coeff = std::make_pair(info.m_bound.to_mpq(), mpq(0));
coeff = std::make_pair(mgr.dup(info.m_bound.to_mpq()), mpq(0));
unsigned slack = info.m_slack;
if (is_true) {
update_bound(slack, literal(v), true, coeff);

1
src/smt/theory_pb.h
View file

@ -279,7 +279,6 @@ namespace smt {
//
void compile_ineq(ineq& c);
void inc_propagations(ineq& c);
unsigned get_compilation_threshold(ineq& c);
//
// Conflict resolution, cutting plane derivation.

2
src/smt/theory_seq.cpp
View file

@ -3466,6 +3466,8 @@ static bool get_arith_value(context& ctx, theory_id afid, expr* e, expr_ref& v)
bool theory_seq::get_num_value(expr* e, rational& val) const {
context& ctx = get_context();
expr_ref _val(m);
if (!ctx.e_internalized(e))
return false;
enode* next = ctx.get_enode(e), *n = next;
do {
if (get_arith_value(ctx, m_autil.get_family_id(), next->get_owner(), _val) && m_autil.is_numeral(_val, val) && val.is_int()) {

30
src/smt/theory_str.cpp
View file

@ -315,6 +315,7 @@ namespace smt {
m_trail.push_back(node);
if (!cut_var_map.contains(baseNode)) {
T_cut * varInfo = alloc(T_cut);
m_cut_allocs.push_back(varInfo);
varInfo->level = slevel;
varInfo->vars[node] = 1;
cut_var_map.insert(baseNode, std::stack<T_cut*>());
@ -323,6 +324,7 @@ namespace smt {
} else {
if (cut_var_map[baseNode].empty()) {
T_cut * varInfo = alloc(T_cut);
m_cut_allocs.push_back(varInfo);
varInfo->level = slevel;
varInfo->vars[node] = 1;
cut_var_map[baseNode].push(varInfo);
@ -330,6 +332,7 @@ namespace smt {
} else {
if (cut_var_map[baseNode].top()->level < slevel) {
T_cut * varInfo = alloc(T_cut);
m_cut_allocs.push_back(varInfo);
varInfo->level = slevel;
cut_vars_map_copy(varInfo->vars, cut_var_map[baseNode].top()->vars);
varInfo->vars[node] = 1;
@ -359,6 +362,7 @@ namespace smt {
if (!cut_var_map.contains(destNode)) {
T_cut * varInfo = alloc(T_cut);
m_cut_allocs.push_back(varInfo);
varInfo->level = slevel;
cut_vars_map_copy(varInfo->vars, cut_var_map[srcNode].top()->vars);
cut_var_map.insert(destNode, std::stack<T_cut*>());
@ -367,6 +371,7 @@ namespace smt {
} else {
if (cut_var_map[destNode].empty() || cut_var_map[destNode].top()->level < slevel) {
T_cut * varInfo = alloc(T_cut);
m_cut_allocs.push_back(varInfo);
varInfo->level = slevel;
cut_vars_map_copy(varInfo->vars, cut_var_map[destNode].top()->vars);
cut_vars_map_copy(varInfo->vars, cut_var_map[srcNode].top()->vars);
@ -8883,15 +8888,30 @@ namespace smt {
if (concat_lhs_haseqc && concat_rhs_haseqc && !var_haseqc) {
TRACE("str", tout << "backpropagate into " << mk_pp(var, m) << " = " << mk_pp(concat, m) << std::endl
<< "LHS ~= " << mk_pp(concat_lhs_str, m) << " RHS ~= " << mk_pp(concat_rhs_str, m) << std::endl;);
zstring lhsString, rhsString;
u.str.is_string(concat_lhs_str, lhsString);
u.str.is_string(concat_rhs_str, rhsString);
zstring concatString = lhsString + rhsString;
expr_ref lhs1(ctx.mk_eq_atom(concat_lhs, concat_lhs_str), m);
expr_ref lhs2(ctx.mk_eq_atom(concat_rhs, concat_rhs_str), m);
expr_ref lhs(m.mk_and(lhs1, lhs2), m);
expr_ref rhs(ctx.mk_eq_atom(concat, mk_string(concatString)), m);
assert_implication(lhs, rhs);
// special handling: don't assert that string constants are equal to themselves
expr_ref_vector lhs_terms(m);
if (!u.str.is_string(concat_lhs)) {
lhs_terms.push_back(ctx.mk_eq_atom(concat_lhs, concat_lhs_str));
}
if (!u.str.is_string(concat_rhs)) {
lhs_terms.push_back(ctx.mk_eq_atom(concat_rhs, concat_rhs_str));
}
if (lhs_terms.empty()) {
// no assumptions on LHS
expr_ref rhs(ctx.mk_eq_atom(concat, mk_string(concatString)), m);
assert_axiom(rhs);
} else {
expr_ref lhs(mk_and(lhs_terms), m);
expr_ref rhs(ctx.mk_eq_atom(concat, mk_string(concatString)), m);
assert_implication(lhs, rhs);
}
backpropagation_occurred = true;
}
}

6
src/smt/theory_str.h
View file

@ -18,9 +18,12 @@
#define _THEORY_STR_H_
#include "util/trail.h"
#include "util/union_find.h"
#include "util/scoped_ptr_vector.h"
#include "ast/ast_pp.h"
#include "ast/arith_decl_plugin.h"
#include "ast/rewriter/th_rewriter.h"
#include "ast/seq_decl_plugin.h"
#include "smt/smt_theory.h"
#include "smt/params/theory_str_params.h"
#include "smt/proto_model/value_factory.h"
@ -29,8 +32,6 @@
#include<stack>
#include<vector>
#include<map>
#include "ast/seq_decl_plugin.h"
#include "util/union_find.h"
namespace smt {
@ -292,6 +293,7 @@ protected:
bool avoidLoopCut;
bool loopDetected;
obj_map<expr, std::stack<T_cut*> > cut_var_map;
scoped_ptr_vector<T_cut> m_cut_allocs;
expr_ref m_theoryStrOverlapAssumption_term;
obj_hashtable<expr> variable_set;

4
src/smt/watch_list.h
View file

@ -85,6 +85,10 @@ namespace smt {
watch_list():
m_data(0) {
}
watch_list(watch_list && other) : m_data(0) {
std::swap(m_data, other.m_data);
}
~watch_list() {
destroy();