mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-11 13:40:52 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2012-12-28 16:40:36 -08:00
commit 63b7f7ecd6
130 changed files with 1576 additions and 1284 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/muz_qe/dl_bmc_engine.cpp
View file

@ -963,7 +963,7 @@ namespace datalog {
sort_ref_vector new_sorts(m);
family_id dfid = m.get_family_id("datatype");
family_id dfid = m.mk_family_id("datatype");
datatype_decl_plugin* dtp = static_cast<datatype_decl_plugin*>(m.get_plugin(dfid));
VERIFY (dtp->mk_datatypes(dts.size(), dts.c_ptr(), new_sorts));

2
src/muz_qe/dl_cmds.cpp
View file

@ -75,7 +75,7 @@ struct dl_context {
if (!m_decl_plugin) {
symbol name("datalog_relation");
if (m.has_plugin(name)) {
m_decl_plugin = static_cast<datalog::dl_decl_plugin*>(m_cmd.m().get_plugin(m.get_family_id(name)));
m_decl_plugin = static_cast<datalog::dl_decl_plugin*>(m_cmd.m().get_plugin(m.mk_family_id(name)));
}
else {
m_decl_plugin = alloc(datalog::dl_decl_plugin);

1
src/muz_qe/dl_context.h
View file

@ -349,6 +349,7 @@ namespace datalog {
void cancel();
void cleanup();
void reset_cancel() { cleanup(); }
/**
\brief check if query 'q' is satisfied under asserted rules and background.

68
src/muz_qe/dl_mk_slice.cpp
View file

@ -429,6 +429,29 @@ namespace datalog {
}
}
void mk_slice::filter_unique_vars(rule& r) {
//
// Variables that occur in multiple uinterpreted predicates are not sliceable.
//
uint_set used_vars;
for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) {
app* p = r.get_tail(j);
for (unsigned i = 0; i < p->get_num_args(); ++i) {
expr* v = p->get_arg(i);
if (is_var(v)) {
unsigned vi = to_var(v)->get_idx();
add_var(vi);
if (used_vars.contains(vi)) {
m_var_is_sliceable[vi] = false;
}
else {
used_vars.insert(vi);
}
}
}
}
}
void mk_slice::solve_vars(rule& r, uint_set& used_vars, uint_set& parameter_vars) {
expr_ref_vector conjs = get_tail_conjs(r);
for (unsigned j = 0; j < conjs.size(); ++j) {
@ -475,6 +498,7 @@ namespace datalog {
}
}
}
filter_unique_vars(r);
//
// Collect the set of variables that are solved.
// Collect the occurrence count of the variables per conjunct.
@ -750,51 +774,11 @@ namespace datalog {
m_solved_vars.reset();
#if 0
uint_set used_vars;
expr_ref b(m);
TBD: buggy code:
for (unsigned i = 0; i < conjs.size(); ++i) {
expr* e = conjs[i].get();
if (is_eq(e, v, b)) {
if (v >= m_solved_vars.size()) {
m_solved_vars.resize(v+1);
}
if (v < sorts.size() && sorts[v]) {
TRACE("dl", tout << "already bound " << mk_pp(e, m) << "\n";);
add_free_vars(used_vars, e);
}
else if (m_solved_vars[v].get()) {
TRACE("dl", tout << "already solved " << mk_pp(e, m) << "\n";);
add_free_vars(used_vars, e);
add_free_vars(used_vars, m_solved_vars[v].get());
used_vars.insert(v);
}
else {
TRACE("dl", tout << "new solution " << mk_pp(e, m) << "\n";);
m_solved_vars[v] = b;
}
}
else {
TRACE("dl", tout << "not solved " << mk_pp(e, m) << "\n";);
add_free_vars(used_vars, e);
}
tail.push_back(to_app(e));
}
#endif
for (unsigned i = 0; i < conjs.size(); ++i) {
expr* e = conjs[i].get();
#if 0
if (false && is_eq(e, v, b) && m_solved_vars[v].get() && !used_vars.contains(v)) {
TRACE("dl", tout << "removing conjunct: " << mk_pp(e, m) << "\n";);
// skip conjunct
}
#endif
tail.push_back(to_app(e));
}
new_rule = rm.mk(head.get(), tail.size(), tail.c_ptr(), (const bool*) 0);
rm.fix_unbound_vars(new_rule, false);

2
src/muz_qe/dl_mk_slice.h
View file

@ -89,6 +89,8 @@ namespace datalog {
void update_predicate(app* p, app_ref& q);
void filter_unique_vars(rule& r);
void solve_vars(rule& r, uint_set& used_vars, uint_set& parameter_vars);
public:

6
src/muz_qe/dl_relation_manager.h
View file

@ -3,7 +3,7 @@ Copyright (c) 2006 Microsoft Corporation
Module Name:
dl_remation_manager.h
dl_relation_manager.h
Abstract:
@ -316,7 +316,7 @@ namespace datalog {
oldTgt:=tgt.clone();
tgt:=tgt \union src
if(tgt!=oldTgt) {
delta:=delta \union src //also “delta \union tgt” would work
delta:=delta \union src //also ?delta \union tgt? would work
}
}
@ -488,7 +488,7 @@ namespace datalog {
oldTgt:=tgt.clone();
tgt:=tgt \union src
if(tgt!=oldTgt) {
delta:=delta \union src //also “delta \union tgt” would work
delta:=delta \union src //also ?delta \union tgt? would work
}
}

2
src/muz_qe/dl_rule.cpp
View file

@ -74,7 +74,7 @@ namespace datalog {
class remove_label_cfg : public default_rewriter_cfg {
family_id m_label_fid;
public:
remove_label_cfg(ast_manager& m): m_label_fid(m.get_family_id("label")) {}
remove_label_cfg(ast_manager& m): m_label_fid(m.get_label_family_id()) {}
virtual ~remove_label_cfg() {}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result,

2
src/muz_qe/proof_utils.cpp
View file

@ -489,7 +489,7 @@ static void permute_unit_resolution(expr_ref_vector& refs, obj_map<proof,proof*>
parameter const* params = thLemma->get_decl()->get_parameters();
unsigned num_params = thLemma->get_decl()->get_num_parameters();
SASSERT(params[0].is_symbol());
family_id tid = m.get_family_id(params[0].get_symbol());
family_id tid = m.mk_family_id(params[0].get_symbol());
SASSERT(tid != null_family_id);
prNew = m.mk_th_lemma(tid, m.get_fact(pr),
premises.size(), premises.c_ptr(), num_params-1, params+1);

4
src/muz_qe/qe_arith_plugin.cpp
View file

@ -1512,7 +1512,7 @@ public:
public:
arith_plugin(i_solver_context& ctx, ast_manager& m, smt_params& p):
qe_solver_plugin(m, m.get_family_id("arith"), ctx),
qe_solver_plugin(m, m.mk_family_id("arith"), ctx),
m_util(m, p, ctx),
m_trail(m)
{}
@ -2403,7 +2403,7 @@ public:
bool m_produce_models;
public:
nlarith_plugin(i_solver_context& ctx, ast_manager& m, bool produce_models) :
qe_solver_plugin(m, m.get_family_id("arith"), ctx),
qe_solver_plugin(m, m.mk_family_id("arith"), ctx),
m_rewriter(m),
m_util(m),
m_replacer(mk_default_expr_replacer(m)),

2
src/muz_qe/qe_array_plugin.cpp
View file

@ -16,7 +16,7 @@ namespace qe {
public:
array_plugin(i_solver_context& ctx, ast_manager& m) :
qe_solver_plugin(m, m.get_family_id("array"), ctx),
qe_solver_plugin(m, m.mk_family_id("array"), ctx),
m_replace(mk_default_expr_replacer(m))
{
}

2
src/muz_qe/qe_bv_plugin.cpp
View file

@ -32,7 +32,7 @@ namespace qe {
bv_util m_bv;
public:
bv_plugin(i_solver_context& ctx, ast_manager& m):
qe_solver_plugin(m, m.get_family_id("bv"), ctx),
qe_solver_plugin(m, m.mk_family_id("bv"), ctx),
m_replace(mk_default_expr_replacer(m)),
m_bv(m)
{}

2
src/muz_qe/qe_datatype_plugin.cpp
View file

@ -422,7 +422,7 @@ namespace qe {
public:
datatype_plugin(i_solver_context& ctx, ast_manager& m) :
qe_solver_plugin(m, m.get_family_id("datatype"), ctx),
qe_solver_plugin(m, m.mk_family_id("datatype"), ctx),
m_datatype_util(m),
m_replace(mk_default_expr_replacer(m)),
m_trail(m)

2
src/muz_qe/qe_dl_plugin.cpp
View file

@ -45,7 +45,7 @@ namespace qe {
public:
dl_plugin(i_solver_context& ctx, ast_manager& m) :
qe_solver_plugin(m, m.get_family_id("datalog_relation"), ctx),
qe_solver_plugin(m, m.mk_family_id("datalog_relation"), ctx),
m_replace(mk_default_expr_replacer(m)),
m_util(m),
m_trail(m)

56
src/muz_qe/qe_lite.cpp
View file

@ -971,15 +971,15 @@ namespace fm {
}
bool is_linear_ineq(expr * t) const {
bool result = false;
m.is_not(t, t);
expr * lhs, * rhs;
TRACE("is_occ_bug", tout << mk_pp(t, m) << "\n";);
if (m_util.is_le(t, lhs, rhs) || m_util.is_ge(t, lhs, rhs)) {
if (!m_util.is_numeral(rhs))
return false;
return is_linear_pol(lhs);
result = m_util.is_numeral(rhs) && is_linear_pol(lhs);
}
return false;
TRACE("qe_lite", tout << mk_pp(t, m) << " " << (result?"true":"false") << "\n";);
return result;
}
bool is_occ(expr * t) {
@ -1049,7 +1049,7 @@ namespace fm {
cnstr->m_xs = reinterpret_cast<var*>(mem_xs);
cnstr->m_as = reinterpret_cast<rational*>(mem_as);
for (unsigned i = 0; i < num_vars; i++) {
TRACE("mk_constraint_bug", tout << "xs[" << i << "]: " << xs[i] << "\n";);
TRACE("qe_lite", tout << "xs[" << i << "]: " << xs[i] << "\n";);
cnstr->m_xs[i] = xs[i];
new (cnstr->m_as + i) rational(as[i]);
}
@ -1241,7 +1241,7 @@ namespace fm {
if (c2->m_dead)
continue;
if (subsumes(c, *c2)) {
TRACE("fm_subsumption", display(tout, c); tout << "\nsubsumed:\n"; display(tout, *c2); tout << "\n";);
TRACE("qe_lite", display(tout, c); tout << "\nsubsumed:\n"; display(tout, *c2); tout << "\n";);
c2->m_dead = true;
continue;
}
@ -1284,12 +1284,12 @@ namespace fm {
}
void updt_params() {
m_fm_real_only = true;
m_fm_real_only = false;
m_fm_limit = 5000000;
m_fm_cutoff1 = 8;
m_fm_cutoff2 = 256;
m_fm_extra = 0;
m_fm_occ = false;
m_fm_occ = true;
}
void set_cancel(bool f) {
@ -1318,7 +1318,7 @@ namespace fm {
expr * f = g[i];
if (is_occ(f))
continue;
TRACE("is_occ_bug", tout << "not OCC:\n" << mk_ismt2_pp(f, m) << "\n";);
TRACE("qe_lite", tout << "not OCC:\n" << mk_ismt2_pp(f, m) << "\n";);
quick_for_each_expr(proc, visited, f);
}
}
@ -1447,6 +1447,7 @@ namespace fm {
SASSERT(m_uppers.size() == m_is_int.size());
SASSERT(m_forbidden.size() == m_is_int.size());
SASSERT(m_var2pos.size() == m_is_int.size());
TRACE("qe_lite", tout << mk_pp(t,m) << " |-> " << x << " forbidden: " << forbidden << "\n";);
return x;
}
@ -1468,7 +1469,7 @@ namespace fm {
x = mk_var(t);
SASSERT(m_expr2var.contains(t));
SASSERT(m_var2expr.get(x) == t);
TRACE("to_var_bug", tout << mk_ismt2_pp(t, m) << " --> " << x << "\n";);
TRACE("qe_lite", tout << mk_ismt2_pp(t, m) << " --> " << x << "\n";);
return x;
}
@ -1488,6 +1489,7 @@ namespace fm {
void add_constraint(expr * f, expr_dependency * dep) {
TRACE("qe_lite", tout << mk_pp(f, m) << "\n";);
SASSERT(!m.is_or(f) || m_fm_occ);
sbuffer<literal> lits;
sbuffer<var> xs;
@ -1524,7 +1526,7 @@ namespace fm {
neg = !neg;
expr * lhs = to_app(l)->get_arg(0);
expr * rhs = to_app(l)->get_arg(1);
m_util.is_numeral(rhs, c);
VERIFY (m_util.is_numeral(rhs, c));
if (neg)
c.neg();
unsigned num_mons;
@ -1567,7 +1569,7 @@ namespace fm {
}
}
TRACE("to_var_bug", tout << "before mk_constraint: "; for (unsigned i = 0; i < xs.size(); i++) tout << " " << xs[i]; tout << "\n";);
TRACE("qe_lite", tout << "before mk_constraint: "; for (unsigned i = 0; i < xs.size(); i++) tout << " " << xs[i]; tout << "\n";);
constraint * new_c = mk_constraint(lits.size(),
lits.c_ptr(),
@ -1578,7 +1580,7 @@ namespace fm {
strict,
dep);
TRACE("to_var_bug", tout << "add_constraint: "; display(tout, *new_c); tout << "\n";);
TRACE("qe_lite", tout << "add_constraint: "; display(tout, *new_c); tout << "\n";);
VERIFY(register_constraint(new_c));
}
@ -1591,7 +1593,7 @@ namespace fm {
if (is_false(*c)) {
del_constraint(c);
m_inconsistent = true;
TRACE("add_constraint_bug", tout << "is false "; display(tout, *c); tout << "\n";);
TRACE("qe_lite", tout << "is false "; display(tout, *c); tout << "\n";);
return false;
}
@ -1614,7 +1616,7 @@ namespace fm {
return true;
}
else {
TRACE("add_constraint_bug", tout << "all variables are forbidden "; display(tout, *c); tout << "\n";);
TRACE("qe_lite", tout << "all variables are forbidden "; display(tout, *c); tout << "\n";);
m_new_fmls.push_back(to_expr(*c));
del_constraint(c);
return false;
@ -1668,7 +1670,7 @@ namespace fm {
}
// x_cost_lt is not a total order on variables
std::stable_sort(x_cost_vector.begin(), x_cost_vector.end(), x_cost_lt(m_is_int));
TRACE("fm",
TRACE("qe_lite",
svector<x_cost>::iterator it2 = x_cost_vector.begin();
svector<x_cost>::iterator end2 = x_cost_vector.end();
for (; it2 != end2; ++it2) {
@ -1854,7 +1856,7 @@ namespace fm {
if (new_xs.empty() && (new_c.is_pos() || (!new_strict && new_c.is_zero()))) {
// literal is true
TRACE("fm", tout << "resolution " << x << " consequent literal is always true: \n";
TRACE("qe_lite", tout << "resolution " << x << " consequent literal is always true: \n";
display(tout, l);
tout << "\n";
display(tout, u); tout << "\n";);
@ -1898,7 +1900,7 @@ namespace fm {
}
if (tautology) {
TRACE("fm", tout << "resolution " << x << " tautology: \n";
TRACE("qe_lite", tout << "resolution " << x << " tautology: \n";
display(tout, l);
tout << "\n";
display(tout, u); tout << "\n";);
@ -1908,7 +1910,7 @@ namespace fm {
expr_dependency * new_dep = m.mk_join(l.m_dep, u.m_dep);
if (new_lits.empty() && new_xs.empty() && (new_c.is_neg() || (new_strict && new_c.is_zero()))) {
TRACE("fm", tout << "resolution " << x << " inconsistent: \n";
TRACE("qe_lite", tout << "resolution " << x << " inconsistent: \n";
display(tout, l);
tout << "\n";
display(tout, u); tout << "\n";);
@ -1926,7 +1928,7 @@ namespace fm {
new_strict,
new_dep);
TRACE("fm", tout << "resolution " << x << "\n";
TRACE("qe_lite", tout << "resolution " << x << "\n";
display(tout, l);
tout << "\n";
display(tout, u);
@ -1949,7 +1951,7 @@ namespace fm {
if (l.empty() || u.empty()) {
// easy case
mark_constraints_dead(x);
TRACE("fm", tout << "variable was eliminated (trivial case)\n";);
TRACE("qe_lite", tout << "variable was eliminated (trivial case)\n";);
return true;
}
@ -1967,7 +1969,7 @@ namespace fm {
m_counter += num_lowers * num_uppers;
TRACE("fm_bug", tout << "eliminating " << mk_ismt2_pp(m_var2expr.get(x), m) << "\nlowers:\n";
TRACE("qe_lite", tout << "eliminating " << mk_ismt2_pp(m_var2expr.get(x), m) << "\nlowers:\n";
display_constraints(tout, l); tout << "uppers:\n"; display_constraints(tout, u););
unsigned num_old_cnstrs = num_uppers + num_lowers;
@ -1977,7 +1979,7 @@ namespace fm {
for (unsigned i = 0; i < num_lowers; i++) {
for (unsigned j = 0; j < num_uppers; j++) {
if (m_inconsistent || num_new_cnstrs > limit) {
TRACE("fm", tout << "too many new constraints: " << num_new_cnstrs << "\n";);
TRACE("qe_lite", tout << "too many new constraints: " << num_new_cnstrs << "\n";);
del_constraints(new_constraints.size(), new_constraints.c_ptr());
return false;
}
@ -2002,7 +2004,7 @@ namespace fm {
backward_subsumption(*c);
register_constraint(c);
}
TRACE("fm", tout << "variables was eliminated old: " << num_old_cnstrs << " new_constraints: " << sz << "\n";);
TRACE("qe_lite", tout << "variables was eliminated old: " << num_old_cnstrs << " new_constraints: " << sz << "\n";);
return true;
}
@ -2018,7 +2020,7 @@ namespace fm {
if (!c->m_dead) {
c->m_dead = true;
expr * new_f = to_expr(*c);
TRACE("fm_bug", tout << "asserting...\n" << mk_ismt2_pp(new_f, m) << "\nnew_dep: " << c->m_dep << "\n";);
TRACE("qe_lite", tout << "asserting...\n" << mk_ismt2_pp(new_f, m) << "\nnew_dep: " << c->m_dep << "\n";);
m_new_fmls.push_back(new_f);
}
}
@ -2049,7 +2051,7 @@ namespace fm {
m_new_fmls.push_back(m.mk_false());
}
else {
TRACE("fm", display(tout););
TRACE("qe_lite", display(tout););
subsume();
var_vector candidates;