mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-02 08:10:43 +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-10-31 10:37:10 -07:00
commit bdc28762d3
68 changed files with 200 additions and 172 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/muz_qe/datalog_parser.cpp
View file

@ -1382,12 +1382,12 @@ private:
uint64_set & sort_content = *sit->m_value;
//the +1 is for a zero element which happens to appear in the problem files
uint64 domain_size = sort_content.size()+1;
sort * s;
// sort * s;
if(!m_use_map_names) {
s = register_finite_sort(sort_name, domain_size, context::SK_UINT64);
/* s = */ register_finite_sort(sort_name, domain_size, context::SK_UINT64);
}
else {
s = register_finite_sort(sort_name, domain_size, context::SK_SYMBOL);
/* s = */ register_finite_sort(sort_name, domain_size, context::SK_SYMBOL);
}
/*

8
src/muz_qe/dl_bmc_engine.cpp
View file

@ -34,12 +34,12 @@ namespace datalog {
bmc::bmc(context& ctx):
m_ctx(ctx),
m(ctx.get_manager()),
m_cancel(false),
m_solver(m, m_fparams),
m_pinned(m),
m_rules(ctx),
m_query_pred(m),
m_answer(m),
m_cancel(false),
m_path_sort(m),
m_bv(m) {
}
@ -794,7 +794,7 @@ namespace datalog {
sort* pred_sort = m_pred2sort.find(p);
path_var = m.mk_var(0, m_path_sort);
trace_var = m.mk_var(1, pred_sort);
sort* sorts[2] = { pred_sort, m_path_sort };
// sort* sorts[2] = { pred_sort, m_path_sort };
ptr_vector<func_decl> const& cnstrs = *dtu.get_datatype_constructors(pred_sort);
ptr_vector<func_decl> const& succs = *dtu.get_datatype_constructors(m_path_sort);
SASSERT(cnstrs.size() == rls.size());
@ -966,10 +966,10 @@ namespace datalog {
datalog::rule_vector const& rules = m_rules.get_predicate_rules(p);
ptr_vector<func_decl> const& cnstrs = *dtu.get_datatype_constructors(trace_sort);
ptr_vector<func_decl> const& succs = *dtu.get_datatype_constructors(m_path_sort);
bool found = false;
// bool found = false;
for (unsigned i = 0; i < cnstrs.size(); ++i) {
if (trace->get_decl() == cnstrs[i]) {
found = true;
// found = true;
svector<std::pair<unsigned, unsigned> > positions;
scoped_coarse_proof _sc(m);
proof_ref_vector prs(m);

2
src/muz_qe/dl_bound_relation.cpp
View file

@ -395,12 +395,10 @@ namespace datalog {
uint_set::iterator it = t.lt.begin(), end = t.lt.end();
unsigned_vector ltv, lev;
for (; it != end; ++it) {
unsigned elem = *it;
ltv.push_back(renaming[*it]);
}
it = t.le.begin(), end = t.le.end();
for (; it != end; ++it) {
unsigned elem = *it;
lev.push_back(renaming[*it]);
}
TRACE("dl",

1
src/muz_qe/dl_cmds.cpp
View file

@ -228,7 +228,6 @@ public:
private:
void set_background(cmd_context& ctx) {
datalog::context& dlctx = m_dl_ctx->get_dl_context();
ast_manager& m = ctx.m();
ptr_vector<expr>::const_iterator it = ctx.begin_assertions();
ptr_vector<expr>::const_iterator end = ctx.end_assertions();
for (; it != end; ++it) {

1
src/muz_qe/dl_compiler.cpp
View file

@ -168,7 +168,6 @@ namespace datalog {
TRACE("dl", tout << "Adding unbound column " << mk_pp(pred, m_context.get_manager()) << "\n";);
IF_VERBOSE(3, {
relation_manager& rm = m_context.get_rmanager();
expr_ref e(m_context.get_manager());
compiled_rule->to_formula(e);
verbose_stream() << "Compiling unsafe rule column " << col_idx << "\n"

16
src/muz_qe/dl_context.cpp
View file

@ -457,19 +457,18 @@ namespace datalog {
/*}*/
}
SASSERT(!rel_kinds.empty());
relation_plugin * rel_plugin; //the aggregate kind of non-table plugins
relation_signature rel_sig;
// relation_plugin * rel_plugin; //the aggregate kind of non-table plugins
family_id rel_kind; //the aggregate kind of non-table plugins
if (rel_kinds.size()==1) {
rel_kind = rel_kinds[0];
rel_plugin = rel_plugins[0];
// rel_plugin = rel_plugins[0];
}
else {
relation_signature rel_sig;
//rmgr.from_predicate(pred, rel_sig);
product_relation_plugin & prod_plugin = product_relation_plugin::get_plugin(rmgr);
rel_kind = prod_plugin.get_relation_kind(rel_sig, rel_kinds);
rel_plugin = &prod_plugin;
// rel_plugin = &prod_plugin;
}
if (tr_plugin==0) {
target_kind = rel_kind;
@ -532,7 +531,6 @@ namespace datalog {
rule_ref r(rules[0].get(), rm);
get_rmanager().reset_saturated_marks();
rule_ref_vector const& rls = m_rule_set.get_rules();
bool found = false;
rule* old_rule = 0;
for (unsigned i = 0; i < rls.size(); ++i) {
if (rls[i]->name() == name) {
@ -757,6 +755,9 @@ namespace datalog {
check_existential_tail(r);
check_positive_predicates(r);
break;
default:
UNREACHABLE();
break;
}
}
@ -1550,6 +1551,8 @@ namespace datalog {
}
}
#if 0
// [Leo] dead code?
static func_decl* get_head_relation(ast_manager& m, expr* fml) {
while (is_quantifier(fml)) {
fml = to_quantifier(fml)->get_expr();
@ -1563,6 +1566,7 @@ namespace datalog {
return 0;
}
}
#endif
void context::display_smt2(
unsigned num_queries,
@ -1694,7 +1698,7 @@ namespace datalog {
max_vars.insert(s, max_var);
// index into fresh variable array.
unsigned fresh_var_idx = 0;
// unsigned fresh_var_idx = 0;
obj_map<sort, unsigned_vector>::obj_map_entry* e = var_idxs.insert_if_not_there2(s, unsigned_vector());
unsigned_vector& vars = e->get_data().m_value;
if (max_var >= vars.size()) {

4
src/muz_qe/dl_finite_product_relation.cpp
View file

@ -1001,6 +1001,9 @@ namespace datalog {
}
};
// [Leo]: gcc complained about the following class.
// It does not have a constructor and uses a reference
#if 0
class inner_relation_copier : public table_row_mutator_fn {
finite_product_relation & m_tgt;
const finite_product_relation & m_src;
@ -1023,6 +1026,7 @@ namespace datalog {
return true;
}
};
#endif
scoped_ptr<table_union_fn> m_t_union_fun;
offset_row_mapper * m_offset_mapper_obj; //initialized together with m_offset_mapper_fun, and deallocated by it

4
src/muz_qe/dl_mk_bit_blast.cpp
View file

@ -130,7 +130,7 @@ namespace datalog {
class mk_bit_blast::impl {
context & m_context;
context & m_context;
ast_manager & m;
params_ref m_params;
rule_ref_vector m_rules;
@ -161,8 +161,8 @@ namespace datalog {
impl(context& ctx):
m_context(ctx),
m(ctx.get_manager()),
m_rules(ctx.get_rule_manager()),
m_params(ctx.get_params()),
m_rules(ctx.get_rule_manager()),
m_blaster(ctx.get_manager(), m_params),
m_rewriter(ctx.get_manager(), ctx, m_rules) {
m_params.set_bool(":blast-full", true);

6
src/muz_qe/dl_mk_coalesce.cpp
View file

@ -179,9 +179,9 @@ namespace datalog {
}
rule_set* rules = alloc(rule_set, m_ctx);
rule_set::decl2rules::iterator it = source.begin_grouped_rules(), end = source.end_grouped_rules();
bool change = false;
// bool change = false;
for (; it != end; ++it) {
func_decl* p = it->m_key;
// func_decl* p = it->m_key;
rule_ref_vector d_rules(rm);
d_rules.append(it->m_value->size(), it->m_value->c_ptr());
for (unsigned i = 0; i < d_rules.size(); ++i) {
@ -191,7 +191,7 @@ namespace datalog {
merge_rules(r1, *d_rules[j].get());
d_rules[j] = d_rules.back();
d_rules.pop_back();
change = true;
// change = true;
--j;
}
}

2
src/muz_qe/dl_mk_rule_inliner.h
View file

@ -179,9 +179,9 @@ namespace datalog {
m_simp(m_context.get_rewriter()),
m_pinned(m_rm),
m_inlined_rules(m_context),
m_unifier(ctx),
m_mc(0),
m_pc(0),
m_unifier(ctx),
m_head_index(m),
m_tail_index(m),
m_subst(m),

8
src/muz_qe/dl_mk_slice.cpp
View file

@ -205,8 +205,8 @@ namespace datalog {
expr* fact0 = m.get_fact(p0);
TRACE("dl", tout << "fact0: " << mk_pp(fact0, m) << "\n";);
rule* orig0 = m_sliceform2rule.find(fact0);
rule* slice0 = m_rule2slice.find(orig0);
unsigned_vector const& renaming0 = m_renaming.find(orig0);
/* rule* slice0 = */ m_rule2slice.find(orig0);
/* unsigned_vector const& renaming0 = */ m_renaming.find(orig0);
premises.push_back(p0_new);
rule_ref r1(rm), r2(rm), r3(rm);
r1 = orig0;
@ -217,8 +217,8 @@ namespace datalog {
expr* fact1 = m.get_fact(p1);
TRACE("dl", tout << "fact1: " << mk_pp(fact1, m) << "\n";);
rule* orig1 = m_sliceform2rule.find(fact1);
rule* slice1 = m_rule2slice.find(orig1);
unsigned_vector const& renaming1 = m_renaming.find(orig1); //TBD
/* rule* slice1 = */ m_rule2slice.find(orig1);
/* unsigned_vector const& renaming1 = */ m_renaming.find(orig1); //TBD
premises.push_back(p1_new);
// TODO: work with substitutions.

4
src/muz_qe/dl_table.cpp
View file

@ -567,10 +567,10 @@ namespace datalog {
public:
eq_iterator(const equivalence_table& eq, bool end):
m_eq(eq),
m_row_obj(*this),
m_last(eq.m_uf.get_num_vars()),
m_current(end?m_last:0),
m_next(0)
m_next(0),
m_row_obj(*this)
{
while (m_current < m_last && !m_eq.is_valid(m_current)) {
m_current++;

2
src/muz_qe/dl_util.cpp
View file

@ -594,7 +594,7 @@ namespace datalog {
void del_rule(horn_subsume_model_converter* mc, rule& r) {
if (mc) {
app* head = r.get_head();
// app* head = r.get_head();
ast_manager& m = mc->get_manager();
expr_ref_vector body(m);
for (unsigned i = 0; i < r.get_tail_size(); ++i) {

1
src/muz_qe/dl_vector_relation.h
View file

@ -209,7 +209,6 @@ namespace datalog {
void mk_project(vector_relation const& r, unsigned col_cnt, unsigned const* removed_cols) {
SASSERT(is_full());
unsigned j = 0, k = 0;
unsigned_vector classRep, repNode;
unsigned result_size = get_signature().size();
unsigned input_size = r.get_signature().size();

4
src/muz_qe/pdr_context.cpp
View file

@ -57,7 +57,8 @@ namespace pdr {
// pred_tansformer
pred_transformer::pred_transformer(context& ctx, manager& pm, func_decl* head):
ctx(ctx), pm(pm), m(pm.get_manager()), m_head(head, m),
pm(pm), m(pm.get_manager()),
ctx(ctx), m_head(head, m),
m_sig(m), m_solver(pm, head->get_name()),
m_invariants(m), m_transition(m), m_initial_state(m),
m_reachable(pm, pm.get_params()) {}
@ -196,7 +197,6 @@ namespace pdr {
tactic_ref us = mk_unit_subsumption_tactic(m);
simplify_formulas(*us, m_invariants);
for (unsigned i = 0; i < m_levels.size(); ++i) {
expr_ref_vector& v = m_levels[i];
simplify_formulas(*us, m_levels[i]);
}
}

1
src/muz_qe/pdr_dl_interface.cpp
View file

@ -80,7 +80,6 @@ lbool dl_interface::query(expr * query) {
m_pdr_rules.reset();
m_ctx.get_rmanager().reset_relations();
ast_manager& m = m_ctx.get_manager();
datalog::relation_manager& rm = m_ctx.get_rmanager();
datalog::rule_manager& rule_manager = m_ctx.get_rule_manager();
datalog::rule_set old_rules(m_ctx.get_rules());
func_decl_ref query_pred(m);

3
src/muz_qe/pdr_generalizers.cpp
View file

@ -38,7 +38,7 @@ namespace pdr {
return;
}
ast_manager& m = core.get_manager();
TRACE("pdr", for (unsigned i = 0; i < core.size(); ++i) { tout << mk_pp(core[i].get(), m) << "\n"; } "\n";);
TRACE("pdr", for (unsigned i = 0; i < core.size(); ++i) { tout << mk_pp(core[i].get(), m) << "\n"; });
unsigned num_failures = 0, i = 0, old_core_size = core.size();
ptr_vector<expr> processed;
@ -109,7 +109,6 @@ namespace pdr {
{}
void core_farkas_generalizer::operator()(model_node& n, expr_ref_vector& core, bool& uses_level) {
front_end_params& p = m_ctx.get_fparams();
ast_manager& m = n.pt().get_manager();
manager& pm = n.pt().get_pdr_manager();
if (core.empty()) return;

2
src/muz_qe/pdr_interpolant_provider.cpp
View file

@ -20,7 +20,9 @@ Revision History:
--*/
//disables the warning on deprecation of fgets function -- didn't really find by what it should be replaced
#ifdef _WINDOWS
#pragma warning(disable: 4995)
#endif
#include <sstream>
#include "ast_smt_pp.h"

10
src/muz_qe/pdr_smt_context_manager.cpp
View file

@ -26,8 +26,8 @@ Revision History:
namespace pdr {
smt_context::smt_context(smt_context_manager& p, ast_manager& m, app* pred):
m_parent(p),
m_pred(pred, m),
m_parent(p),
m_in_delay_scope(false),
m_pushed(false)
{}
@ -94,8 +94,12 @@ namespace pdr {
}
smt_context_manager::smt_context_manager(front_end_params& fp, params_ref const& p, ast_manager& m):
m_fparams(fp), m_max_num_contexts(p.get_uint(":max-num-contexts", 500)),
m(m), m_num_contexts(0), m_predicate_list(m) {}
m_fparams(fp),
m(m),
m_max_num_contexts(p.get_uint(":max-num-contexts", 500)),
m_num_contexts(0),
m_predicate_list(m) {
}
smt_context_manager::~smt_context_manager() {

8
src/muz_qe/qe.cpp
View file

@ -856,8 +856,8 @@ namespace qe {
public:
nnf_normalizer(ast_manager& m, i_expr_pred& is_relevant, i_nnf_atom& mk_atom):
m_nnf_core(m, is_relevant),
m_normalize_literals(m, is_relevant, mk_atom),
m_collect_atoms(m, is_relevant)
m_collect_atoms(m, is_relevant),
m_normalize_literals(m, is_relevant, mk_atom)
{}
void operator()(expr_ref& fml, atom_set& pos, atom_set& neg) {
@ -1767,7 +1767,7 @@ namespace qe {
void propagate_assignment(model_evaluator& model_eval) {
if (m_fml) {
update_status st = update_current(model_eval, true);
/* update_status st = */ update_current(model_eval, true);
}
}
@ -2551,7 +2551,7 @@ namespace qe {
)
{
bool is_forall = old_q->is_forall();
// bool is_forall = old_q->is_forall();
app_ref_vector vars(m);
TRACE("qe", tout << "simplifying" << mk_pp(new_body, m) << "\n";);
result = new_body;

8
src/muz_qe/qe_arith_plugin.cpp
View file

@ -110,11 +110,10 @@ namespace qe {
m_minus_one_i(m_arith.mk_numeral(numeral(-1), true), m),
m_zero_r(m_arith.mk_numeral(numeral(0), false), m),
m_one_r(m_arith.mk_numeral(numeral(1), false), m),
m_tmp(m),
m_replace(mk_default_expr_replacer(m)),
m_bool_rewriter(m),
m_arith_rewriter(m),
m_tmp(m)
{
m_arith_rewriter(m) {
}
ast_manager& get_manager() { return m; }
@ -1817,7 +1816,6 @@ public:
}
--v;
is_strict = e_size <= v;
bool is_eq = false;
SASSERT(v < t_size + e_size);
if (is_strict) {
@ -1826,7 +1824,6 @@ public:
}
else if (m_util.is_real(x)) {
SASSERT(0 == (e_size & 0x1));
is_eq = (0 == (v & 0x1));
v /= 2;
e_size /= 2;
}
@ -1896,7 +1893,6 @@ public:
bounds_proc& bounds = get_bounds(x.x(), fml);
bool is_lower = bounds.le_size() + bounds.lt_size() < bounds.ge_size() + bounds.gt_size();
unsigned e_size = bounds.e_size(is_lower);
unsigned t_size = bounds.t_size(is_lower);
numeral bound1, bound2, vl, x_val;
unsigned idx1, idx2;
bool found1 = find_min_max(is_lower, false, bounds, model_eval, bound1, idx1);

4
src/muz_qe/qe_sat_tactic.cpp
View file

@ -213,12 +213,12 @@ namespace qe {
m_projection_mode_param(true),
m_strong_context_simplify_param(true),
m_ctx_simplify_local_param(false),
m_solver(m, m_fparams),
m_fml(m),
m_Ms(m),
m_assignments(m),
m_rewriter(m),
m_ctx_rewriter(m_fparams, m),
m_solver(m, m_fparams) {
m_ctx_rewriter(m_fparams, m) {
m_fparams.m_model = true;
}