mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-10-07 19:24:30 +01:00
commit c1b243a8e3
45 changed files with 1345 additions and 699 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/python/z3/z3.py
View file

@ -120,7 +120,7 @@ def _get_args(args):
try:
if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)):
return args[0]
elif len(args) == 1 and isinstance(args[0], set):
elif len(args) == 1 and (isinstance(args[0], set) or isinstance(args[0], AstVector)):
return [arg for arg in args[0]]
else:
return args

3
src/ast/ast.cpp
View file

@ -471,6 +471,9 @@ bool compare_nodes(ast const * n1, ast const * n2) {
compare_arrays(to_quantifier(n1)->get_decl_sorts(),
to_quantifier(n2)->get_decl_sorts(),
to_quantifier(n1)->get_num_decls()) &&
compare_arrays(to_quantifier(n1)->get_decl_names(),
to_quantifier(n2)->get_decl_names(),
to_quantifier(n1)->get_num_decls()) &&
to_quantifier(n1)->get_expr() == to_quantifier(n2)->get_expr() &&
to_quantifier(n1)->get_weight() == to_quantifier(n2)->get_weight() &&
to_quantifier(n1)->get_num_patterns() == to_quantifier(n2)->get_num_patterns() &&

9
src/ast/expr_abstract.cpp
View file

@ -19,6 +19,7 @@ Notes:
#include "ast/expr_abstract.h"
#include "util/map.h"
#include "ast/ast_pp.h"
void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result) {
@ -109,6 +110,9 @@ void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const*
void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result) {
expr_abstractor abs(m);
abs(base, num_bound, bound, n, result);
TRACE("expr_abstract",
tout << expr_ref(n, m) << "\n";
tout << result << "\n";);
}
expr_ref mk_quantifier(bool is_forall, ast_manager& m, unsigned num_bound, app* const* bound, expr* n) {
@ -123,6 +127,11 @@ expr_ref mk_quantifier(bool is_forall, ast_manager& m, unsigned num_bound, app*
}
result = m.mk_quantifier(is_forall, num_bound, sorts.c_ptr(), names.c_ptr(), result);
}
TRACE("expr_abstract",
tout << expr_ref(n, m) << "\n";
for (unsigned i = 0; i < num_bound; ++i) tout << expr_ref(bound[i], m) << " ";
tout << "\n";
tout << result << "\n";);
return result;
}

10
src/ast/expr_substitution.cpp
View file

@ -16,8 +16,9 @@ Author:
Notes:
--*/
#include "ast/expr_substitution.h"
#include "util/ref_util.h"
#include "ast/expr_substitution.h"
#include "ast/ast_pp.h"
typedef obj_map<expr, proof*> expr2proof;
typedef obj_map<expr, expr_dependency*> expr2expr_dependency;
@ -56,6 +57,13 @@ expr_substitution::~expr_substitution() {
reset();
}
std::ostream& expr_substitution::display(std::ostream& out) {
for (auto & kv : m_subst) {
out << mk_pp(kv.m_key, m()) << " |-> " << mk_pp(kv.m_value, m()) << "\n";
}
return out;
}
void expr_substitution::insert(expr * c, expr * def, proof * def_pr, expr_dependency * def_dep) {
obj_map<expr, expr*>::obj_map_entry * entry = m_subst.insert_if_not_there2(c, 0);
if (entry->get_data().m_value == 0) {

3
src/ast/expr_substitution.h
View file

@ -50,6 +50,8 @@ public:
bool contains(expr * s);
void reset();
void cleanup();
std::ostream& display(std::ostream& out);
};
class scoped_expr_substitution {
@ -84,6 +86,7 @@ public:
bool find(expr * s, expr * & def, proof * & def_pr, expr_dependency * & def_dep) { return m_subst.find(s, def, def_pr, def_dep); }
bool contains(expr * s) { return m_subst.contains(s); }
void cleanup() { m_subst.cleanup(); }
std::ostream& display(std::ostream& out) { return m_subst.display(out); }
};
#endif

6
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -1180,8 +1180,6 @@ void fpa2bv_converter::mk_abs(sort * s, expr_ref & x, expr_ref & result) {
void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 2);
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
expr * x = args[0], * y = args[1];
@ -1227,8 +1225,6 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args,
void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 2);
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
expr * x = args[0], *y = args[1];
@ -3081,8 +3077,6 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
mk_is_nan(x, x_is_nan);
sort * fp_srt = m.get_sort(x);
unsigned ebits = m_util.get_ebits(fp_srt);
unsigned sbits = m_util.get_sbits(fp_srt);
expr_ref unspec(m);
mk_to_ieee_bv_unspecified(f, num, args, unspec);

4
src/ast/rewriter/maximize_ac_sharing.cpp
View file

@ -151,11 +151,7 @@ void maximize_ac_sharing::restore_entries(unsigned old_lim) {
}
void maximize_ac_sharing::reset() {
restore_entries(0);
m_entries.reset();
m_cache.reset();
m_region.reset();
m_scopes.reset();
}
void maximize_bv_sharing::init_core() {

7
src/cmd_context/cmd_context.cpp
View file

@ -870,6 +870,12 @@ void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, s
lhs = m().mk_app(f, binding.size(), binding.c_ptr());
eq = m().mk_eq(lhs, e);
if (!ids.empty()) {
if (is_var(e)) {
ptr_vector<sort> domain;
for (expr* b : binding) domain.push_back(m().get_sort(b));
insert_macro(f->get_name(), domain.size(), domain.c_ptr(), e);
return;
}
if (!is_app(e)) {
throw cmd_exception("Z3 only supports recursive definitions that are proper terms (not binders or variables)");
}
@ -1763,6 +1769,7 @@ void cmd_context::validate_model() {
continue;
}
try {
for_each_expr(contains_underspecified, a);
for_each_expr(contains_underspecified, r);
}
catch (contains_underspecified_op_proc::found) {

29
src/interp/iz3mgr.cpp
View file

@ -33,9 +33,11 @@
#include <fstream>
#include <iostream>
#include <ostream>
#include <sstream>
#include "ast/expr_abstract.h"
#include "util/params.h"
#include "ast/used_vars.h"
using namespace stl_ext;
@ -938,3 +940,30 @@ void iz3mgr::get_bound_substitutes(stl_ext::hash_map<ast,bool> &memo, const ast
}
#endif
unsigned iz3mgr::num_free_variables(const ast &e){
used_vars uv;
uv(to_expr(e.raw()));
return uv.get_num_vars();
}
iz3mgr::ast iz3mgr::close_universally (ast e){
used_vars uv;
uv(to_expr(e.raw()));
std::vector<ast> bvs;
stl_ext::hash_map<ast,ast> subst_memo;
for (unsigned i = 0; i < uv.get_max_found_var_idx_plus_1(); i++){
if (uv.get(i)) {
std::ostringstream os;
os << "%%" << i;
ast c = make_var(os.str(),uv.get(i));
ast v = cook(m().mk_var(i,uv.get(i)));
subst_memo[v] = c;
bvs.push_back(c);
}
}
e = subst(subst_memo,e);
for (unsigned i = 0; i < bvs.size(); i++)
e = apply_quant(Forall,bvs[i],e);
return e;
}

6
src/interp/iz3mgr.h
View file

@ -661,6 +661,12 @@ class iz3mgr {
ast apply_quant(opr quantifier, ast var, ast e);
// Universally quantify all the free variables in a formula.
// Makes up names for the quntifiers.
ast close_universally (ast e);
unsigned num_free_variables(const ast &e);
/** For debugging */
void show(ast);

4
src/interp/iz3proof_itp.cpp
View file

@ -2968,9 +2968,9 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast interpolate(const node &pf){
// proof of false must be a formula, with quantified symbols
#ifndef BOGUS_QUANTS
return add_quants(z3_simplify(pf));
return close_universally(add_quants(z3_simplify(pf)));
#else
return z3_simplify(pf);
return close_universally(z3_simplify(pf));
#endif
}

5
src/interp/iz3translate.cpp
View file

@ -234,6 +234,11 @@ public:
}
}
// if(!range_is_empty(rng)){
// if (num_free_variables(con) > 0)
// rng = range_empty();
// }
if(res == INT_MAX){
if(range_is_empty(rng))
res = -1;

21
src/muz/ddnf/ddnf.cpp
View file

@ -192,10 +192,15 @@ namespace datalog {
for (unsigned i = 0; i < new_tbvs.size(); ++i) {
tbv const& nt = *new_tbvs[i];
IF_VERBOSE(10, m_tbv.display(verbose_stream() << "insert: ", nt); verbose_stream() << "\n";);
if (contains(nt)) continue;
ddnf_node* n = alloc(ddnf_node, *this, m_tbv, nt, m_noderefs.size());
m_noderefs.push_back(n);
m_nodes.insert(n);
ddnf_node* n;
if (contains(nt)) {
n = find(nt);
}
else {
n = alloc(ddnf_node, *this, m_tbv, nt, m_noderefs.size());
m_noderefs.push_back(n);
m_nodes.insert(n);
}
insert(*m_root, n, new_tbvs);
}
return find(t);
@ -275,13 +280,17 @@ namespace datalog {
void insert(ddnf_node& root, ddnf_node* new_n, ptr_vector<tbv const>& new_intersections) {
tbv const& new_tbv = new_n->get_tbv();
IF_VERBOSE(10, m_tbv.display(verbose_stream() << "root: ", root.get_tbv());
m_tbv.display(verbose_stream() << " new node ", new_tbv); verbose_stream() << "\n";);
SASSERT(m_tbv.contains(root.get_tbv(), new_tbv));
if (&root == new_n) return;
if (m_eq(&root, new_n)) return;
++m_stats.m_num_inserts;
bool inserted = false;
for (unsigned i = 0; i < root.num_children(); ++i) {
ddnf_node& child = *(root[i]);
++m_stats.m_num_comparisons;
IF_VERBOSE(10, m_tbv.display(verbose_stream() << "child ", child.get_tbv());
verbose_stream() << " contains: " << m_tbv.contains(child.get_tbv(), new_tbv) << "\n";);
if (m_tbv.contains(child.get_tbv(), new_tbv)) {
inserted = true;
insert(child, new_n, new_intersections);
@ -299,11 +308,13 @@ namespace datalog {
// checking for subset
if (m_tbv.contains(new_tbv, child.get_tbv())) {
subset_children.push_back(&child);
IF_VERBOSE(10, m_tbv.display(verbose_stream() << "contains child", child.get_tbv()); verbose_stream() << "\n";);
++m_stats.m_num_comparisons;
}
else if (m_tbv.intersect(child.get_tbv(), new_tbv, *intr)) {
// this means there is a non-full intersection
new_intersections.push_back(intr);
IF_VERBOSE(10, m_tbv.display(verbose_stream() << "intersect child ", child.get_tbv()); verbose_stream() << "\n";);
intr = m_tbv.allocate();
m_stats.m_num_comparisons += 2;
}

4
src/muz/rel/karr_relation.cpp
View file

@ -111,8 +111,8 @@ namespace datalog {
void filter_interpreted(app* cond) {
rational one(1), mone(-1);
expr* e1, *e2, *en;
var* v, *w;
expr* e1 = 0, *e2 = 0, *en = 0;
var* v = 0, *w = 0;
rational n1, n2;
expr_ref_vector conjs(m);
flatten_and(cond, conjs);

4
src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
View file

@ -398,8 +398,8 @@ namespace datalog {
}
bool mk_interp_tail_simplifier::propagate_variable_equivalences(rule * r, rule_ref& res) {
if (!m_context.get_params ().xform_tail_simplifier_pve ())
return false;
if (!m_context.get_params ().xform_tail_simplifier_pve ())
return false;
unsigned u_len = r->get_uninterpreted_tail_size();
unsigned len = r->get_tail_size();
if (u_len == len) {

2
src/parsers/smt2/smt2scanner.cpp
View file

@ -124,7 +124,7 @@ namespace smt2 {
next();
bool is_float = false;
while (true) {
while (!m_at_eof) {
char c = curr();
if ('0' <= c && c <= '9') {
m_number = rational(10)*m_number + rational(c - '0');

7
src/smt/asserted_formulas.cpp
View file

@ -170,7 +170,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 +181,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 +197,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() {

11
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++) {

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;

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";);
}
@ -407,9 +407,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);
}
@ -444,7 +446,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() << " ";
@ -508,20 +510,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() {

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) {

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))

1185
src/tactic/bv/bv_bounds_tactic.cpp
View file

File diff suppressed because it is too large Load diff

2
src/tactic/core/CMakeLists.txt
View file

@ -7,6 +7,7 @@ z3_add_component(core_tactics
ctx_simplify_tactic.cpp
der_tactic.cpp
distribute_forall_tactic.cpp
dom_simplify_tactic.cpp
elim_term_ite_tactic.cpp
elim_uncnstr_tactic.cpp
injectivity_tactic.cpp
@ -32,6 +33,7 @@ z3_add_component(core_tactics
ctx_simplify_tactic.h
der_tactic.h
distribute_forall_tactic.h
dom_simplify_tactic.h
elim_term_ite_tactic.h
elim_uncnstr_tactic.h
injectivity_tactic.h

240
src/tactic/core/dom_simplify_tactic.cpp
View file

@ -83,49 +83,66 @@ expr* expr_dominators::intersect(expr* x, expr * y) {
return x;
}
void expr_dominators::compute_dominators() {
bool expr_dominators::compute_dominators() {
expr * e = m_root;
SASSERT(m_doms.empty());
m_doms.insert(e, e);
bool change = true;
unsigned iterations = 1;
while (change) {
change = false;
SASSERT(m_post2expr.back() == e);
for (unsigned i = 0; i < m_post2expr.size() - 1; ++i) {
TRACE("simplify",
for (auto & kv : m_doms) {
tout << expr_ref(kv.m_key, m) << " |-> " << expr_ref(kv.m_value, m) << "\n";
});
SASSERT(m_post2expr.empty() || m_post2expr.back() == e);
for (unsigned i = 0; i + 1 < m_post2expr.size(); ++i) {
expr * child = m_post2expr[i];
ptr_vector<expr> const& p = m_parents[child];
SASSERT(!p.empty());
expr * new_idom = p[0], * idom2 = 0;
for (unsigned j = 1; j < p.size(); ++j) {
if (m_doms.find(p[j], idom2)) {
new_idom = intersect(new_idom, idom2);
expr * new_idom = 0, *idom2 = 0;
for (expr * pred : p) {
if (m_doms.contains(pred)) {
new_idom = !new_idom ? pred : intersect(new_idom, pred);
}
}
if (!m_doms.find(child, idom2) || idom2 != new_idom) {
if (!new_idom) {
m_doms.insert(child, p[0]);
change = true;
}
else if (!m_doms.find(child, idom2) || idom2 != new_idom) {
m_doms.insert(child, new_idom);
change = true;
}
}
iterations *= 2;
if (change && iterations > m_post2expr.size()) {
return false;
}
}
return true;
}
void expr_dominators::extract_tree() {
for (auto const& kv : m_doms) {
add_edge(m_tree, kv.m_value, kv.m_key);
}
}
}
void expr_dominators::compile(expr * e) {
bool expr_dominators::compile(expr * e) {
reset();
m_root = e;
compute_post_order();
compute_dominators();
if (!compute_dominators()) return false;
extract_tree();
TRACE("simplify", display(tout););
return true;
}
void expr_dominators::compile(unsigned sz, expr * const* es) {
bool expr_dominators::compile(unsigned sz, expr * const* es) {
expr_ref e(m.mk_and(sz, es), m);
compile(e);
return compile(e);
}
void expr_dominators::reset() {
@ -137,19 +154,39 @@ void expr_dominators::reset() {
m_root.reset();
}
std::ostream& expr_dominators::display(std::ostream& out) {
return display(out, 0, m_root);
}
std::ostream& expr_dominators::display(std::ostream& out, unsigned indent, expr* r) {
for (unsigned i = 0; i < indent; ++i) out << " ";
out << expr_ref(r, m);
if (m_tree.contains(r)) {
for (expr* child : m_tree[r]) {
if (child != r)
display(out, indent + 1, child);
}
}
out << "\n";
return out;
}
// -----------------------
// dom_simplify_tactic
dom_simplify_tactic::~dom_simplify_tactic() {
dealloc(m_simplifier);
}
tactic * dom_simplify_tactic::translate(ast_manager & m) {
return alloc(dom_simplify_tactic, m, m_simplifier->translate(m), m_params);
}
void dom_simplify_tactic::operator()(
goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
goal_ref const & in,
goal_ref_buffer & result,
model_converter_ref & mc,
proof_converter_ref & pc,
expr_dependency_ref & core) {
mc = 0; pc = 0; core = 0;
@ -162,33 +199,42 @@ void dom_simplify_tactic::operator()(
}
void dom_simplify_tactic::cleanup() {
m_trail.reset();
m_args.reset();
m_args2.reset();
m_result.reset();
m_dominators.reset();
m_trail.reset();
m_args.reset();
m_result.reset();
m_dominators.reset();
}
expr_ref dom_simplify_tactic::simplify_ite(app * ite) {
expr_ref r(m);
expr * c = 0, * t = 0, * e = 0;
expr * c = 0, *t = 0, *e = 0;
VERIFY(m.is_ite(ite, c, t, e));
unsigned old_lvl = scope_level();
expr_ref new_c = simplify(c);
expr_ref new_c = simplify_arg(c);
if (m.is_true(new_c)) {
r = simplify(t);
}
r = simplify_arg(t);
}
else if (m.is_false(new_c) || !assert_expr(new_c, false)) {
r = simplify(e);
}
r = simplify_arg(e);
}
else {
expr_ref new_t = simplify(t);
for (expr * child : tree(ite)) {
if (is_subexpr(child, t) && !is_subexpr(child, e)) {
simplify_rec(child);
}
}
pop(scope_level() - old_lvl);
expr_ref new_t = simplify_arg(t);
if (!assert_expr(new_c, true)) {
return new_t;
}
expr_ref new_e = simplify(e);
for (expr * child : tree(ite)) {
if (is_subexpr(child, e) && !is_subexpr(child, t)) {
simplify_rec(child);
}
}
pop(scope_level() - old_lvl);
expr_ref new_e = simplify_arg(e);
if (c == new_c && t == new_t && e == new_e) {
r = ite;
}
@ -197,15 +243,28 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) {
}
else {
TRACE("tactic", tout << new_c << "\n" << new_t << "\n" << new_e << "\n";);
r = m.mk_ite(new_c, new_t, new_c);
r = m.mk_ite(new_c, new_t, new_e);
}
}
return r;
}
expr_ref dom_simplify_tactic::simplify(expr * e0) {
expr_ref dom_simplify_tactic::simplify_arg(expr * e) {
expr_ref r(m);
r = get_cached(e);
(*m_simplifier)(r);
TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e, m) << " -> " << r << "\n";);
return r;
}
/**
\brief simplify e recursively.
*/
expr_ref dom_simplify_tactic::simplify_rec(expr * e0) {
expr_ref r(m);
expr* e = 0;
TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << "\n";);
if (!m_result.find(e0, e)) {
e = e0;
}
@ -224,17 +283,13 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) {
r = simplify_or(to_app(e));
}
else {
expr_dominators::tree_t const& t = m_dominators.get_tree();
if (t.contains(e)) {
ptr_vector<expr> const& children = t[e];
for (expr * child : children) {
simplify(child);
}
for (expr * child : tree(e)) {
simplify_rec(child);
}
if (is_app(e)) {
m_args.reset();
for (expr* arg : *to_app(e)) {
m_args.push_back(get_cached(arg)); // TBD is cache really applied to all sub-terms?
m_args.push_back(simplify_arg(arg));
}
r = m.mk_app(to_app(e)->get_decl(), m_args.size(), m_args.c_ptr());
}
@ -246,45 +301,64 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) {
cache(e0, r);
TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";);
--m_depth;
m_subexpr_cache.reset();
return r;
}
expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) {
expr_ref r(m);
unsigned old_lvl = scope_level();
m_args.reset();
for (expr * arg : *e) {
r = simplify(arg);
if (!assert_expr(r, !is_and)) {
r = is_and ? m.mk_false() : m.mk_true();
auto is_subexpr_arg = [&](expr * child, expr * except) {
if (!is_subexpr(child, except))
return false;
for (expr * arg : *e) {
if (arg != except && is_subexpr(child, arg))
return false;
}
m_args.push_back(r);
return true;
};
expr_ref_vector args(m);
if (m_forward) {
for (expr * arg : *e) {
#define _SIMP_ARG(arg) \
for (expr * child : tree(arg)) { \
if (is_subexpr_arg(child, arg)) { \
simplify_rec(child); \
} \
} \
r = simplify_arg(arg); \
args.push_back(r); \
if (!assert_expr(r, !is_and)) { \
r = is_and ? m.mk_false() : m.mk_true(); \
return r; \
}
_SIMP_ARG(arg);
}
}
else {
for (unsigned i = e->get_num_args(); i > 0; ) {
--i;
expr* arg = e->get_arg(i);
_SIMP_ARG(arg);
}
args.reverse();
}
pop(scope_level() - old_lvl);
m_args.reverse();
m_args2.reset();
for (expr * arg : m_args) {
r = simplify(arg);
if (!assert_expr(r, !is_and)) {
r = is_and ? m.mk_false() : m.mk_true();
}
m_args2.push_back(r);
}
pop(scope_level() - old_lvl);
m_args2.reverse();
r = is_and ? mk_and(m_args2) : mk_or(m_args2);
r = is_and ? mk_and(args) : mk_or(args);
return r;
}
void dom_simplify_tactic::init(goal& g) {
bool dom_simplify_tactic::init(goal& g) {
expr_ref_vector args(m);
unsigned sz = g.size();
for (unsigned i = 0; i < sz; ++i) args.push_back(g.form(i));
expr_ref fml = mk_and(args);
m_result.reset();
m_trail.reset();
m_dominators.compile(fml);
return m_dominators.compile(fml);
}
void dom_simplify_tactic::simplify_goal(goal& g) {
@ -296,13 +370,15 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
change = false;
// go forwards
init(g);
m_forward = true;
if (!init(g)) return;
unsigned sz = g.size();
for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) {
expr_ref r = simplify(g.form(i));
expr_ref r = simplify_rec(g.form(i));
if (i < sz - 1 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !g.proofs_enabled() && !assert_expr(r, false)) {
r = m.mk_false();
}
CTRACE("simplify", r != g.form(i), tout << r << " " << mk_pp(g.form(i), m) << "\n";);
change |= r != g.form(i);
proof* new_pr = 0;
if (g.proofs_enabled()) {
@ -313,15 +389,17 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
pop(scope_level());
// go backwards
init(g);
m_forward = false;
if (!init(g)) return;
sz = g.size();
for (unsigned i = sz; !g.inconsistent() && i > 0; ) {
--i;
expr_ref r = simplify(g.form(i));
expr_ref r = simplify_rec(g.form(i));
if (i > 0 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !g.proofs_enabled() && !assert_expr(r, false)) {
r = m.mk_false();
}
change |= r != g.form(i);
CTRACE("simplify", r != g.form(i), tout << r << " " << mk_pp(g.form(i), m) << "\n";);
proof* new_pr = 0;
if (g.proofs_enabled()) {
new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(g.form(i), r, 0, 0));
@ -333,11 +411,41 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
SASSERT(scope_level() == 0);
}
/**
\brief determine if a is dominated by b.
Walk the immediate dominators of a upwards until hitting b or a term that is deeper than b.
Save intermediary results in a cache to avoid recomputations.
*/
bool dom_simplify_tactic::is_subexpr(expr * a, expr * b) {
if (a == b)
return true;
bool r;
if (m_subexpr_cache.find(a, b, r))
return r;
if (get_depth(a) >= get_depth(b)) {
return false;
}
SASSERT(a != idom(a) && get_depth(idom(a)) > get_depth(a));
r = is_subexpr(idom(a), b);
m_subexpr_cache.insert(a, b, r);
return r;
}
ptr_vector<expr> const & dom_simplify_tactic::tree(expr * e) {
if (auto p = m_dominators.get_tree().find_core(e))
return p->get_data().get_value();
return m_empty;
}
// ----------------------
// expr_substitution_simplifier
bool expr_substitution_simplifier::assert_expr(expr * t, bool sign) {
m_scoped_substitution.push();
expr* tt;
if (!sign) {
update_substitution(t, 0);
@ -389,6 +497,8 @@ void expr_substitution_simplifier::update_substitution(expr* n, proof* pr) {
if (is_ground(n) && (m.is_eq(n, lhs, rhs) || m.is_iff(n, lhs, rhs))) {
compute_depth(lhs);
compute_depth(rhs);
m_trail.push_back(lhs);
m_trail.push_back(rhs);
if (is_gt(lhs, rhs)) {
TRACE("propagate_values", tout << "insert " << mk_pp(lhs, m) << " -> " << mk_pp(rhs, m) << "\n";);
m_scoped_substitution.insert(lhs, rhs, pr);
@ -440,3 +550,7 @@ void expr_substitution_simplifier::compute_depth(expr* e) {
m_expr2depth.insert(e, d + 1);
}
}
tactic * mk_dom_simplify_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(dom_simplify_tactic, m, alloc(expr_substitution_simplifier, m), p));
}

102
src/tactic/core/dom_simplify_tactic.h
View file

@ -23,6 +23,8 @@ Notes:
#include "ast/ast.h"
#include "ast/expr_substitution.h"
#include "tactic/tactic.h"
#include "tactic/tactical.h"
#include "util/obj_pair_hashtable.h"
class expr_dominators {
@ -43,78 +45,92 @@ private:
void compute_post_order();
expr* intersect(expr* x, expr * y);
void compute_dominators();
bool compute_dominators();
void extract_tree();
std::ostream& display(std::ostream& out, unsigned indent, expr* r);
public:
expr_dominators(ast_manager& m): m(m), m_root(m) {}
void compile(expr * e);
void compile(unsigned sz, expr * const* es);
bool compile(expr * e);
bool compile(unsigned sz, expr * const* es);
tree_t const& get_tree() { return m_tree; }
void reset();
expr* idom(expr *e) const { return m_doms[e]; }
std::ostream& display(std::ostream& out);
};
class dom_simplifier {
public:
dom_simplifier() {}
virtual ~dom_simplifier() {}
/**
\brief assert_expr performs an implicit push
*/
virtual bool assert_expr(expr * t, bool sign) = 0;
/**
\brief apply simplification.
*/
virtual void operator()(expr_ref& r) = 0;
/**
\brief pop scopes accumulated from assertions.
*/
virtual void pop(unsigned num_scopes) = 0;
virtual dom_simplifier * translate(ast_manager & m) = 0;
};
class dom_simplify_tactic : public tactic {
public:
class simplifier {
public:
virtual ~simplifier() {}
/**
\brief assert_expr performs an implicit push
*/
virtual bool assert_expr(expr * t, bool sign) = 0;
/**
\brief apply simplification.
*/
virtual void operator()(expr_ref& r) = 0;
/**
\brief pop scopes accumulated from assertions.
*/
virtual void pop(unsigned num_scopes) = 0;
virtual simplifier * translate(ast_manager & m);
};
private:
ast_manager& m;
simplifier* m_simplifier;
dom_simplifier* m_simplifier;
params_ref m_params;
expr_ref_vector m_trail, m_args, m_args2;
expr_ref_vector m_trail, m_args;
obj_map<expr, expr*> m_result;
expr_dominators m_dominators;
unsigned m_scope_level;
unsigned m_depth;
unsigned m_max_depth;
ptr_vector<expr> m_empty;
obj_pair_map<expr, expr, bool> m_subexpr_cache;
bool m_forward;
expr_ref simplify(expr* t);
expr_ref simplify_rec(expr* t);
expr_ref simplify_arg(expr* t);
expr_ref simplify_ite(app * ite);
expr_ref simplify_and(app * ite) { return simplify_and_or(true, ite); }
expr_ref simplify_or(app * ite) { return simplify_and_or(false, ite); }
expr_ref simplify_and_or(bool is_and, app * ite);
void simplify_goal(goal& g);
expr_ref get_cached(expr* t) { expr* r = 0; if (!m_result.find(r, r)) r = t; return expr_ref(r, m); }
bool is_subexpr(expr * a, expr * b);
expr_ref get_cached(expr* t) { expr* r = 0; if (!m_result.find(t, r)) r = t; return expr_ref(r, m); }
void cache(expr *t, expr* r) { m_result.insert(t, r); m_trail.push_back(r); }
ptr_vector<expr> const & tree(expr * e);
expr* idom(expr *e) const { return m_dominators.idom(e); }
unsigned scope_level() { return m_scope_level; }
void pop(unsigned n) { SASSERT(n <= m_scope_level); m_scope_level -= n; m_simplifier->pop(n); }
bool assert_expr(expr* f, bool sign) { m_scope_level++; return m_simplifier->assert_expr(f, sign); }
void init(goal& g);
bool init(goal& g);
public:
dom_simplify_tactic(ast_manager & m, simplifier* s, params_ref const & p = params_ref()):
dom_simplify_tactic(ast_manager & m, dom_simplifier* s, params_ref const & p = params_ref()):
m(m), m_simplifier(s), m_params(p),
m_trail(m), m_args(m), m_args2(m),
m_trail(m), m_args(m),
m_dominators(m),
m_scope_level(0), m_depth(0), m_max_depth(1024) {}
m_scope_level(0), m_depth(0), m_max_depth(1024), m_forward(true) {}
virtual ~dom_simplify_tactic() {}
virtual ~dom_simplify_tactic();
virtual tactic * translate(ast_manager & m);
virtual void updt_params(params_ref const & p) {}
@ -130,11 +146,12 @@ public:
virtual void cleanup();
};
class expr_substitution_simplifier : public dom_simplify_tactic::simplifier {
class expr_substitution_simplifier : public dom_simplifier {
ast_manager& m;
expr_substitution m_subst;
scoped_expr_substitution m_scoped_substitution;
obj_map<expr, unsigned> m_expr2depth;
expr_ref_vector m_trail;
// move from asserted_formulas to here..
void compute_depth(expr* e);
@ -142,7 +159,7 @@ class expr_substitution_simplifier : public dom_simplify_tactic::simplifier {
unsigned depth(expr* e) { return m_expr2depth[e]; }
public:
expr_substitution_simplifier(ast_manager& m): m(m), m_subst(m), m_scoped_substitution(m_subst) {}
expr_substitution_simplifier(ast_manager& m): m(m), m_subst(m), m_scoped_substitution(m_subst), m_trail(m) {}
virtual ~expr_substitution_simplifier() {}
virtual bool assert_expr(expr * t, bool sign);
@ -152,12 +169,17 @@ public:
virtual void pop(unsigned num_scopes) { m_scoped_substitution.pop(num_scopes); }
virtual simplifier * translate(ast_manager & m) {
virtual dom_simplifier * translate(ast_manager & m) {
SASSERT(m_subst.empty());
return alloc(expr_substitution_simplifier, m);
}
};
tactic * mk_dom_simplify_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC("dom-simplify", "apply dominator simplification rules.", "mk_dom_simplify_tactic(m, p)")
*/
#endif

4
src/test/ddnf.cpp
View file

@ -214,6 +214,10 @@ void tst_ddnf1() {
ddnf.insert(*tX1);
ddnf.insert(*t1X);
ddnf.display(std::cout);
tbvm.deallocate(tXX);
tbvm.deallocate(t1X);
tbvm.deallocate(tX1);
tbvm.deallocate(t11);
}

1
src/util/lp/indexed_vector_instances.cpp
View file

@ -33,6 +33,7 @@ template void indexed_vector<unsigned>::resize(unsigned int);
template void indexed_vector<mpq>::set_value(const mpq&, unsigned int);
template void indexed_vector<unsigned>::set_value(const unsigned&, unsigned int);
#ifdef Z3DEBUG
template bool indexed_vector<unsigned>::is_OK() const;
template bool indexed_vector<double>::is_OK() const;
template bool indexed_vector<mpq>::is_OK() const;
template bool indexed_vector<lp::numeric_pair<mpq> >::is_OK() const;

2
src/util/lp/lar_solver.h
View file

@ -417,6 +417,8 @@ public:
for (unsigned i : m_rows_with_changed_bounds.m_index) {
calculate_implied_bounds_for_row(i, bp);
if (settings().get_cancel_flag())
return;
}
m_rows_with_changed_bounds.clear();
if (!use_tableau()) {

45
src/util/lp/lp_primal_core_solver_tableau.h
View file

@ -176,25 +176,34 @@ unsigned lp_primal_core_solver<T, X>::solve_with_tableau() {
default:
break; // do nothing
}
} while (this->get_status() != FLOATING_POINT_ERROR
&&
this->get_status() != UNBOUNDED
&&
this->get_status() != OPTIMAL
&&
this->get_status() != INFEASIBLE
&&
this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements
&&
this->total_iterations() <= this->m_settings.max_total_number_of_iterations
&&
!(this->current_x_is_feasible() && this->m_look_for_feasible_solution_only));
} while (this->get_status() != FLOATING_POINT_ERROR
&&
this->get_status() != UNBOUNDED
&&
this->get_status() != OPTIMAL
&&
this->get_status() != INFEASIBLE
&&
this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements
&&
this->total_iterations() <= this->m_settings.max_total_number_of_iterations
&&
!(this->current_x_is_feasible() && this->m_look_for_feasible_solution_only)
&&
this->m_settings.get_cancel_flag() == false);
if (this->m_settings.get_cancel_flag()) {
this->set_status(CANCELLED);
}
SASSERT(this->get_status() == FLOATING_POINT_ERROR
||
this->current_x_is_feasible() == false
||
this->calc_current_x_is_feasible_include_non_basis());
SASSERT(
this->get_status() == FLOATING_POINT_ERROR
||
this->get_status() == CANCELLED
||
this->current_x_is_feasible() == false
||
this->calc_current_x_is_feasible_include_non_basis());
return this->total_iterations();
}

3
src/util/lp/lp_settings.h
View file

@ -61,7 +61,8 @@ enum lp_status {
TIME_EXHAUSTED,
ITERATIONS_EXHAUSTED,
EMPTY,
UNSTABLE
UNSTABLE,
CANCELLED
};
// when the ratio of the vector lenth to domain size to is greater than the return value we switch to solve_By_for_T_indexed_only

5
src/util/rlimit.cpp
View file

@ -21,6 +21,7 @@ Revision History:
reslimit::reslimit():
m_cancel(0),
m_suspend(false),
m_count(0),
m_limit(0) {
}
@ -31,12 +32,12 @@ uint64 reslimit::count() const {
bool reslimit::inc() {
++m_count;
return m_cancel == 0 && (m_limit == 0 || m_count <= m_limit);
return (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend;
}
bool reslimit::inc(unsigned offset) {
m_count += offset;
return m_cancel == 0 && (m_limit == 0 || m_count <= m_limit);
return (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend;
}
void reslimit::push(unsigned delta_limit) {

15
src/util/rlimit.h
View file

@ -23,12 +23,14 @@ Revision History:
class reslimit {
volatile unsigned m_cancel;
bool m_suspend;
uint64 m_count;
uint64 m_limit;
svector<uint64> m_limits;
ptr_vector<reslimit> m_children;
void set_cancel(unsigned f);
friend class scoped_suspend_rlimit;
public:
reslimit();
@ -42,7 +44,7 @@ public:
uint64 count() const;
bool get_cancel_flag() const { return m_cancel > 0; }
bool get_cancel_flag() const { return m_cancel > 0 && !m_suspend; }
char const* get_cancel_msg() const;
void cancel();
void reset_cancel();
@ -61,6 +63,17 @@ public:
};
class scoped_suspend_rlimit {
reslimit & m_limit;
public:
scoped_suspend_rlimit(reslimit& r): m_limit(r) {
r.m_suspend = true;
}
~scoped_suspend_rlimit() {
m_limit.m_suspend = false;
}
};
struct scoped_limits {
reslimit& m_limit;
unsigned m_sz;