mirror of
https://github.com/Z3Prover/z3
synced 2025-11-04 05:19:11 +00:00
Fixed warnings produced by gcc 4.6.3 when compiling in debug mode
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
b1ce9f796c
commit
d8f627c6c8
53 changed files with 116 additions and 121 deletions
|
|
@ -32,6 +32,12 @@ dotnet_fileout = '%s/Native.cs' % dotnet_dir
|
|||
##
|
||||
log_h.write('// Automatically generated file\n')
|
||||
log_h.write('#include\"z3.h\"\n')
|
||||
log_h.write('#ifdef __GNUC__\n')
|
||||
log_h.write('#define _Z3_UNUSED __attribute__((unused))\n')
|
||||
log_h.write('#else\n')
|
||||
log_h.write('#define _Z3_UNUSED\n')
|
||||
log_h.write('#endif\n')
|
||||
|
||||
##
|
||||
log_c.write('// Automatically generated file\n')
|
||||
log_c.write('#include<iostream>\n')
|
||||
|
|
@ -432,12 +438,12 @@ def mk_log_macro(file, name, params):
|
|||
cap = param_array_capacity_pos(p)
|
||||
if cap not in auxs:
|
||||
auxs.add(cap)
|
||||
file.write("unsigned Z3ARG%s; " % cap)
|
||||
file.write("unsigned _Z3_UNUSED Z3ARG%s; " % cap)
|
||||
sz = param_array_size_pos(p)
|
||||
if sz not in auxs:
|
||||
auxs.add(sz)
|
||||
file.write("unsigned * Z3ARG%s; " % sz)
|
||||
file.write("%s Z3ARG%s; " % (param2str(p), i))
|
||||
file.write("unsigned * _Z3_UNUSED Z3ARG%s; " % sz)
|
||||
file.write("%s _Z3_UNUSED Z3ARG%s; " % (param2str(p), i))
|
||||
i = i + 1
|
||||
file.write("if (_LOG_CTX.enabled()) { log_%s(" % name)
|
||||
i = 0
|
||||
|
|
|
|||
|
|
@ -130,7 +130,7 @@ namespace api {
|
|||
ast_manager& m = m_context.get_manager();
|
||||
|
||||
datalog::context ctx(m, m_context.get_fparams());
|
||||
datalog::rule_manager& rm = ctx.get_rule_manager();
|
||||
// datalog::rule_manager& rm = ctx.get_rule_manager();
|
||||
for (unsigned i = 0; i < num_rules; ++i) {
|
||||
expr* rule = rules[i], *body, *head;
|
||||
while (true) {
|
||||
|
|
|
|||
|
|
@ -225,7 +225,6 @@ bool macro_util::is_right_simple_macro(expr * n, unsigned num_decls, app * & hea
|
|||
\remark n is a "polynomial".
|
||||
*/
|
||||
bool macro_util::poly_contains_head(expr * n, func_decl * f, expr * exception) const {
|
||||
expr * curr = n;
|
||||
unsigned num_args;
|
||||
expr * const * args;
|
||||
if (is_add(n)) {
|
||||
|
|
@ -734,7 +733,6 @@ void macro_util::get_rest_clause_as_cond(expr * except_lit, expr_ref & extra_con
|
|||
|
||||
void macro_util::collect_poly_args(expr * n, expr * exception, ptr_buffer<expr> & args) {
|
||||
args.reset();
|
||||
bool stop = false;
|
||||
unsigned num_args;
|
||||
expr * const * _args;
|
||||
if (is_add(n)) {
|
||||
|
|
@ -762,7 +760,6 @@ void macro_util::add_arith_macro_candidate(app * head, unsigned num_decls, expr
|
|||
void macro_util::collect_arith_macro_candidates(expr * lhs, expr * rhs, expr * atom, unsigned num_decls, bool is_ineq, macro_candidates & r) {
|
||||
if (!is_add(lhs) && m_manager.is_eq(atom)) // this case is a simple macro.
|
||||
return;
|
||||
bool stop = false;
|
||||
ptr_buffer<expr> args;
|
||||
unsigned lhs_num_args;
|
||||
expr * const * lhs_args;
|
||||
|
|
|
|||
|
|
@ -273,13 +273,10 @@ void cnf::reduce1_or(app * n, bool in_q) {
|
|||
if (m_params.m_cnf_mode != CNF_OPPORTUNISTIC || result_size < m_params.m_cnf_factor) {
|
||||
expr_ref_buffer cheap_args(m_manager);
|
||||
proof_ref_buffer cheap_args_pr(m_manager);
|
||||
bool named_args;
|
||||
if (is_too_expensive(result_size, f_args)) {
|
||||
named_args = true;
|
||||
name_args(f_args, cheap_args, cheap_args_pr);
|
||||
}
|
||||
else {
|
||||
named_args = false;
|
||||
cheap_args.append(f_args.size(), f_args.c_ptr());
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
|
||||
/*
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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",
|
||||
|
|
|
|||
|
|
@ -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) {
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -1694,7 +1695,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()) {
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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),
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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++;
|
||||
|
|
|
|||
|
|
@ -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) {
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
|
|
|||
|
|
@ -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]);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
|
|
|||
|
|
@ -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() {
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -675,7 +675,7 @@ void theory_diff_logic<Ext>::set_neg_cycle_conflict() {
|
|||
inc_conflicts();
|
||||
literal_vector const& lits = m_nc_functor.get_lits();
|
||||
context & ctx = get_context();
|
||||
region& r = ctx.get_region();
|
||||
// region& r = ctx.get_region();
|
||||
TRACE("arith_conflict",
|
||||
//display(tout);
|
||||
tout << "conflict: ";
|
||||
|
|
|
|||
|
|
@ -1562,7 +1562,7 @@ void fpa2bv_converter::mk_leading_zeros(expr * e, unsigned max_bits, expr_ref &
|
|||
L = m_bv_util.mk_extract(bv_sz/2-1, 0, e);
|
||||
|
||||
unsigned H_size = m_bv_util.get_bv_size(H);
|
||||
unsigned L_size = m_bv_util.get_bv_size(L);
|
||||
// unsigned L_size = m_bv_util.get_bv_size(L);
|
||||
|
||||
expr_ref lzH(m), lzL(m);
|
||||
mk_leading_zeros(H, max_bits, lzH); /* recursive! */
|
||||
|
|
|
|||
|
|
@ -910,12 +910,13 @@ class sls_tactic : public tactic {
|
|||
|
||||
void randomize_local(goal_ref const & g) {
|
||||
ptr_vector<func_decl> & unsat_constants = get_unsat_constants(g);
|
||||
bool did_something = false;
|
||||
// bool did_something = false;
|
||||
for (unsigned i = 0; i < unsat_constants.size(); i++) {
|
||||
func_decl * fd = unsat_constants[i];
|
||||
mpz temp = get_random(fd->get_range());
|
||||
if (m_mpz_manager.neq(temp, get_value(fd)))
|
||||
did_something = true;
|
||||
if (m_mpz_manager.neq(temp, get_value(fd))) {
|
||||
// did_something = true;
|
||||
}
|
||||
update(fd, temp);
|
||||
m_mpz_manager.del(temp);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -84,11 +84,9 @@ protected:
|
|||
|
||||
void reduce(goal& g) {
|
||||
SASSERT(g.is_well_sorted());
|
||||
bool proofs_enabled = g.proofs_enabled();
|
||||
m_num_steps = 0;
|
||||
expr_ref fml(m);
|
||||
tactic_report report("ctx-solver-simplify", g);
|
||||
unsigned sz = g.size();
|
||||
if (g.inconsistent())
|
||||
return;
|
||||
ptr_vector<expr> fmls;
|
||||
|
|
|
|||
|
|
@ -33,7 +33,10 @@ class macro_finder_tactic : public tactic {
|
|||
bool m_cancel;
|
||||
bool m_elim_and;
|
||||
|
||||
imp(ast_manager & m, params_ref const & p) : m_manager(m),m_elim_and(false),m_cancel(false) {
|
||||
imp(ast_manager & m, params_ref const & p) :
|
||||
m_manager(m),
|
||||
m_cancel(false),
|
||||
m_elim_and(false) {
|
||||
updt_params(p);
|
||||
}
|
||||
|
||||
|
|
@ -54,7 +57,6 @@ class macro_finder_tactic : public tactic {
|
|||
fail_if_unsat_core_generation("macro-finder", g);
|
||||
|
||||
bool produce_proofs = g->proofs_enabled();
|
||||
bool produce_models = g->models_enabled();
|
||||
|
||||
simplifier simp(m_manager);
|
||||
basic_simplifier_plugin * bsimp = alloc(basic_simplifier_plugin, m_manager);
|
||||
|
|
|
|||
|
|
@ -54,7 +54,6 @@ class quasi_macros_tactic : public tactic {
|
|||
fail_if_unsat_core_generation("quasi-macros", g);
|
||||
|
||||
bool produce_proofs = g->proofs_enabled();
|
||||
bool produce_models = g->models_enabled();
|
||||
|
||||
simplifier simp(m_manager);
|
||||
basic_simplifier_plugin * bsimp = alloc(basic_simplifier_plugin, m_manager);
|
||||
|
|
|
|||
|
|
@ -49,7 +49,6 @@ class ufbv_rewriter_tactic : public tactic {
|
|||
fail_if_unsat_core_generation("ufbv-rewriter", g);
|
||||
|
||||
bool produce_proofs = g->proofs_enabled();
|
||||
bool produce_models = g->models_enabled();
|
||||
|
||||
basic_simplifier_plugin bsimp(m_manager);
|
||||
bsimp.set_eliminate_and(true);
|
||||
|
|
|
|||
|
|
@ -75,10 +75,10 @@ class tst_bv_simplifier_plugin_cls {
|
|||
public:
|
||||
|
||||
tst_bv_simplifier_plugin_cls() :
|
||||
m_bv_util(m_manager),
|
||||
m_bsimp(m_manager),
|
||||
m_arith(m_manager),
|
||||
m_simp(m_manager, m_bsimp, m_bv_params),
|
||||
m_bv_util(m_manager),
|
||||
m_fid(m_manager.get_family_id("bv")) {
|
||||
reg_decl_plugins(m_manager);
|
||||
}
|
||||
|
|
@ -88,7 +88,6 @@ public:
|
|||
void test_num(unsigned a) {
|
||||
expr_ref e(m_manager), e1(m_manager);
|
||||
app_ref ar(m_manager);
|
||||
int sa = static_cast<int>(a);
|
||||
uint64 a64 = static_cast<uint64>(a);
|
||||
|
||||
e1 = m_bv_util.mk_numeral(rational(a), 32);
|
||||
|
|
|
|||
|
|
@ -39,6 +39,6 @@ void tst_check_assumptions()
|
|||
|
||||
expr * assumpt[] = { nq.get(), nr.get() };
|
||||
//here it should crash
|
||||
lbool res2 = ctx.check(2, assumpt);
|
||||
ctx.check(2, assumpt);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -31,7 +31,7 @@ static void dl_context_simple_query_test(params_ref & params) {
|
|||
context ctx(m, fparams);
|
||||
ctx.updt_params(params);
|
||||
|
||||
lbool status = dl_context_eval_unary_predicate(m, ctx, "Z 64\n\nP(x:Z)\nP(\"a\").", "P");
|
||||
/* lbool status = */ dl_context_eval_unary_predicate(m, ctx, "Z 64\n\nP(x:Z)\nP(\"a\").", "P");
|
||||
|
||||
#if 0
|
||||
// TBD:
|
||||
|
|
|
|||
|
|
@ -48,7 +48,6 @@ void dl_query_test(ast_manager & m, front_end_params & fparams, params_ref& para
|
|||
bool use_magic_sets) {
|
||||
|
||||
dl_decl_util decl_util(m);
|
||||
relation_manager & rel_mgr_b = ctx_b.get_rmanager();
|
||||
|
||||
context ctx_q(m, fparams);
|
||||
params.set_bool(":magic-sets-for-queries", use_magic_sets);
|
||||
|
|
|
|||
|
|
@ -179,8 +179,8 @@ namespace datalog {
|
|||
Z3_ast ffx = Z3_mk_app(ctx, cons_decl, 2, zero_fx);
|
||||
Z3_ast xy[2] = { x, y };
|
||||
Z3_ast zy[2] = { z, y };
|
||||
Z3_ast ffxy[2] = { ffx, y };
|
||||
Z3_ast fxy[2] = { fx, y };
|
||||
// Z3_ast ffxy[2] = { ffx, y };
|
||||
// Z3_ast fxy[2] = { fx, y };
|
||||
Z3_ast zero_nil[2] = { zero, Z3_mk_app(ctx, nil_decl, 0, 0) };
|
||||
Z3_ast f0 = Z3_mk_app(ctx, cons_decl, 2, zero_nil);
|
||||
Z3_ast zero_f0[2] = { zero, f0 };
|
||||
|
|
|
|||
|
|
@ -73,18 +73,15 @@ static void tst_get_implied_equalities2() {
|
|||
Z3_context ctx = Z3_mk_context(cfg);
|
||||
Z3_del_config(cfg);
|
||||
Z3_sort int_ty = Z3_mk_int_sort(ctx);
|
||||
Z3_sort a_ty = Z3_mk_array_sort(ctx, int_ty, int_ty);
|
||||
Z3_ast a = mk_int_var(ctx,"a");
|
||||
Z3_ast b = mk_int_var(ctx,"b");
|
||||
Z3_ast c = mk_int_var(ctx,"c");
|
||||
Z3_ast d = mk_int_var(ctx,"d");
|
||||
Z3_ast one = Z3_mk_numeral(ctx, "1", int_ty);
|
||||
Z3_ast two = Z3_mk_numeral(ctx, "2", int_ty);
|
||||
Z3_ast x = Z3_mk_const_array(ctx, int_ty, one);
|
||||
Z3_ast y = Z3_mk_store(ctx, x, one, a);
|
||||
Z3_ast z = Z3_mk_store(ctx, y, two , b);
|
||||
Z3_ast u = Z3_mk_store(ctx, x, two , b);
|
||||
Z3_ast v = Z3_mk_store(ctx, u, one , a);
|
||||
Z3_ast one = Z3_mk_numeral(ctx, "1", int_ty);
|
||||
Z3_ast two = Z3_mk_numeral(ctx, "2", int_ty);
|
||||
Z3_ast x = Z3_mk_const_array(ctx, int_ty, one);
|
||||
Z3_ast y = Z3_mk_store(ctx, x, one, a);
|
||||
Z3_ast z = Z3_mk_store(ctx, y, two , b);
|
||||
Z3_ast u = Z3_mk_store(ctx, x, two , b);
|
||||
Z3_ast v = Z3_mk_store(ctx, u, one , a);
|
||||
unsigned const num_terms = 5;
|
||||
unsigned i;
|
||||
Z3_ast terms[5] = { x, y, z, u, v};
|
||||
|
|
|
|||
|
|
@ -92,10 +92,10 @@ static void bug_to_rational() {
|
|||
m.to_rational(a, r);
|
||||
ad = m.to_double(a);
|
||||
rd = mq.get_double(r);
|
||||
double diff = (ad-rd);
|
||||
#ifdef _WINDOWS
|
||||
// CMW: This one depends on the rounding mode,
|
||||
// which is implicit in both hwf::set and in mpq::to_double.
|
||||
double diff = (ad-rd);
|
||||
SASSERT(diff >= -DBL_EPSILON && diff <= DBL_EPSILON);
|
||||
#endif
|
||||
}
|
||||
|
|
|
|||
|
|
@ -167,8 +167,6 @@ tst_inf_rational()
|
|||
SASSERT(ceil(inf_rational(rational(1))) == rational(1));
|
||||
SASSERT(ceil(inf_rational(rational(1),true)) == rational(2));
|
||||
|
||||
unsigned h = r9.hash();
|
||||
|
||||
inf_rational x(rational(1,2),true);
|
||||
inf_rational y(1,2);
|
||||
x.swap(y);
|
||||
|
|
|
|||
|
|
@ -20,8 +20,6 @@ void tst_model_retrieval()
|
|||
|
||||
family_id array_fid = m.get_family_id(symbol("array"));
|
||||
array_util au(m);
|
||||
array_decl_plugin& ad = *static_cast<array_decl_plugin *>(m.get_plugin(array_fid));
|
||||
|
||||
|
||||
// arr_s and select_fn creation copy-pasted from z3.cpp
|
||||
|
||||
|
|
|
|||
|
|
@ -113,7 +113,7 @@ static void tst7() {
|
|||
m.display_smt2(std::cout, a); std::cout << "\n";
|
||||
}
|
||||
|
||||
// if (!qm.le(qa, qt)) { TRACE("mpff_bug", tout << fa << "\n" << qa << "\n" << qt << "\n";); UNREACHABLE(); } \
|
||||
// if (!qm.le(qa, qt)) { TRACE("mpff_bug", tout << fa << "\n" << qa << "\n" << qt << "\n";); UNREACHABLE(); }
|
||||
|
||||
|
||||
#define MK_BIN_OP(OP) \
|
||||
|
|
|
|||
|
|
@ -268,7 +268,6 @@ static void tst4() {
|
|||
static void tst5() {
|
||||
params_ref ps;
|
||||
nlsat::solver s(ps);
|
||||
unsynch_mpq_manager & qm = s.qm();
|
||||
anum_manager & am = s.am();
|
||||
nlsat::pmanager & pm = s.pm();
|
||||
nlsat::assignment as(am);
|
||||
|
|
|
|||
|
|
@ -55,7 +55,7 @@ static void tst1() {
|
|||
cell_allocator m;
|
||||
|
||||
cell * c1 = m.allocate<true>();
|
||||
cell * c2 = m.allocate<true>();
|
||||
/* cell * c2 = */ m.allocate<true>();
|
||||
|
||||
c1->m_coeff = rational(10);
|
||||
m.recycle(c1);
|
||||
|
|
|
|||
|
|
@ -112,10 +112,10 @@ static void tst2() {
|
|||
m.display_info(tout, a1); tout << "\n";
|
||||
m.display_info(tout, a2); tout << "\n";);
|
||||
for (unsigned i = 0; i < m.size(a1); i++) {
|
||||
SASSERT(m.get(a1, i) == i);
|
||||
SASSERT(static_cast<unsigned>(m.get(a1, i)) == i);
|
||||
}
|
||||
for (unsigned i = 0; i < m.size(a2); i++) {
|
||||
SASSERT(m.get(a2, i) == i);
|
||||
SASSERT(static_cast<unsigned>(m.get(a2, i)) == i);
|
||||
}
|
||||
TRACE("parray",
|
||||
m.display_info(tout, a1); tout << "\n";
|
||||
|
|
@ -161,7 +161,7 @@ static void tst3() {
|
|||
m.push_back(a4, 30);
|
||||
|
||||
for (unsigned i = 0; i < 20; i++) {
|
||||
SASSERT(m.get(a2, i) == i+1);
|
||||
SASSERT(static_cast<unsigned>(m.get(a2, i)) == i+1);
|
||||
}
|
||||
TRACE("parray",
|
||||
m.display_info(tout, a1); tout << "\n";
|
||||
|
|
@ -182,11 +182,11 @@ static void tst3() {
|
|||
SASSERT(m.size(a3) == 19);
|
||||
SASSERT(m.size(a4) == 19);
|
||||
for (unsigned i = 0; i < 20; i++) {
|
||||
SASSERT(m.get(a1, i) == i);
|
||||
SASSERT(m.get(a2, i) == i+1);
|
||||
SASSERT(i >= 18 || m.get(a4, i) == i+1);
|
||||
SASSERT(i >= 6 || m.get(a3, i) == i+1);
|
||||
SASSERT(!(6 <= i && i <= 17) || m.get(a3, i) == i);
|
||||
SASSERT(static_cast<unsigned>(m.get(a1, i)) == i);
|
||||
SASSERT(static_cast<unsigned>(m.get(a2, i)) == i+1);
|
||||
SASSERT(i >= 18 || static_cast<unsigned>(m.get(a4, i)) == i+1);
|
||||
SASSERT(i >= 6 || static_cast<unsigned>(m.get(a3, i)) == i+1);
|
||||
SASSERT(!(6 <= i && i <= 17) || static_cast<unsigned>(m.get(a3, i)) == i);
|
||||
}
|
||||
SASSERT(m.get(a4, 18) == 30);
|
||||
SASSERT(m.get(a3, 18) == 40);
|
||||
|
|
|
|||
|
|
@ -747,9 +747,6 @@ static void tst_psc() {
|
|||
polynomial_ref & d = x3;
|
||||
polynomial_ref & e = x4;
|
||||
polynomial_ref & f = x5;
|
||||
polynomial_ref & g = x6;
|
||||
polynomial_ref & h = x7;
|
||||
polynomial_ref & i = x8;
|
||||
polynomial_ref & x = x9;
|
||||
tst_psc((x^4) + a*(x^2) + b*x + c, 4*(x^3) + 2*a*x + b, 9,
|
||||
16*(a^4)*c - 4*(a^3)*(b^2) - 128*(a^2)*(c^2) + 144*a*(b^2)*c - 27*(b^4) + 256*(c^3), 8*(a^3) - 32*a*c + 36*(b^2));
|
||||
|
|
|
|||
|
|
@ -247,7 +247,7 @@ static void tst_factor_finite_1() {
|
|||
|
||||
// factor it
|
||||
upolynomial::zp_factors factors(upm);
|
||||
bool factorized = upolynomial::zp_factor(upm, K_u, factors);
|
||||
/* bool factorized = */ upolynomial::zp_factor(upm, K_u, factors);
|
||||
|
||||
// check the result
|
||||
unsigned distinct = factors.distinct_factors();
|
||||
|
|
@ -383,8 +383,8 @@ static void tst_factor_finite_3() {
|
|||
cout << "Got " << factors << endl;
|
||||
cout << "Thats " << distinct << " distinct factors, " << total << " total" << endl;
|
||||
|
||||
SASSERT(random_polynomial[random_i][0][prime_i] == distinct);
|
||||
SASSERT(random_polynomial[random_i][1][prime_i] == total);
|
||||
// SASSERT(random_polynomial[random_i][0][prime_i] == distinct);
|
||||
// SASSERT(random_polynomial[random_i][1][prime_i] == total);
|
||||
|
||||
upolynomial::numeral_vector multiplied;
|
||||
factors.multiply(multiplied);
|
||||
|
|
@ -548,7 +548,7 @@ static void tst_factor_square_free_univariate_1(unsigned max_length) {
|
|||
cout << "factoring "; upm.display(cout, f_u); cout << endl;
|
||||
cout << "expecting " << length << " factors ";
|
||||
upolynomial::factors factors(upm);
|
||||
bool ok = upolynomial::factor_square_free(upm, f_u, factors);
|
||||
/* bool ok = */ upolynomial::factor_square_free(upm, f_u, factors);
|
||||
cout << "got " << factors << endl;
|
||||
|
||||
SASSERT(factors.distinct_factors() == length);
|
||||
|
|
|
|||
|
|
@ -23,12 +23,12 @@ static void tst1() {
|
|||
SASSERT(v1.empty());
|
||||
for (unsigned i = 0; i < 1000; i++) {
|
||||
v1.push_back(i + 3);
|
||||
SASSERT(v1[i] == i + 3);
|
||||
SASSERT(static_cast<unsigned>(v1[i]) == i + 3);
|
||||
SASSERT(v1.capacity() >= v1.size());
|
||||
SASSERT(!v1.empty());
|
||||
}
|
||||
for (unsigned i = 0; i < 1000; i++) {
|
||||
SASSERT(v1[i] == i + 3);
|
||||
SASSERT(static_cast<unsigned>(v1[i]) == i + 3);
|
||||
}
|
||||
vector<int>::iterator it = v1.begin();
|
||||
vector<int>::iterator end = v1.end();
|
||||
|
|
@ -36,7 +36,7 @@ static void tst1() {
|
|||
SASSERT(*it == i + 3);
|
||||
}
|
||||
for (unsigned i = 0; i < 1000; i++) {
|
||||
SASSERT(v1.back() == 1000 - i - 1 + 3);
|
||||
SASSERT(static_cast<unsigned>(v1.back()) == 1000 - i - 1 + 3);
|
||||
SASSERT(v1.size() == 1000 - i);
|
||||
v1.pop_back();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -68,7 +68,11 @@ bool is_debug_enabled(const char * tag);
|
|||
#define MAKE_NAME2(LINE) zofty_ ## LINE
|
||||
#define MAKE_NAME(LINE) MAKE_NAME2(LINE)
|
||||
#define DBG_UNIQUE_NAME MAKE_NAME(__LINE__)
|
||||
#ifdef __GNUC__
|
||||
#define COMPILE_TIME_ASSERT(expr) extern __attribute__((unused)) char DBG_UNIQUE_NAME[expr]
|
||||
#else
|
||||
#define COMPILE_TIME_ASSERT(expr) extern char DBG_UNIQUE_NAME[expr]
|
||||
#endif
|
||||
|
||||
template<class T>
|
||||
class class_invariant
|
||||
|
|
|
|||
|
|
@ -1041,7 +1041,7 @@ private:
|
|||
for (unsigned i = 0; i < edges.size(); ++i) {
|
||||
|
||||
potential0 += m_edges[edges[i]].get_weight();
|
||||
numeral potential1 = potentials[i];
|
||||
// numeral potential1 = potentials[i];
|
||||
if (potential0 != potentials[i] ||
|
||||
nodes[i] != m_edges[edges[i]].get_source()) {
|
||||
TRACE("diff_logic_traverse", tout << "checking index " << i << " ";
|
||||
|
|
|
|||
|
|
@ -24,7 +24,9 @@ Revision History:
|
|||
#pragma fp_contract(off) // contractions off (`contraction' means x*y+z is turned into a fused-mul-add).
|
||||
#pragma fenv_access(on) // fpu environment sensitivity (needed to be allowed to make FPU mode changes).
|
||||
#else
|
||||
#ifdef _WINDOWS
|
||||
#pragma STDC FENV_ACCESS ON
|
||||
#endif
|
||||
#include <math.h>
|
||||
#include <fenv.h>
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -91,6 +91,8 @@ void disable_error_msg_prefix() {
|
|||
g_show_error_msg_prefix = false;
|
||||
}
|
||||
|
||||
#if 0
|
||||
// [Leo]: Do we need this?
|
||||
static void string2ostream(std::ostream& out, char const* msg) {
|
||||
svector<char> buff;
|
||||
buff.resize(10);
|
||||
|
|
@ -104,6 +106,7 @@ static void string2ostream(std::ostream& out, char const* msg) {
|
|||
END_ERR_HANDLER();
|
||||
out << buff.c_ptr();
|
||||
}
|
||||
#endif
|
||||
|
||||
void format2ostream(std::ostream & out, char const* msg, va_list args) {
|
||||
svector<char> buff;
|
||||
|
|
@ -147,14 +150,14 @@ void format2ostream(std::ostream & out, char const* msg, va_list args) {
|
|||
|
||||
void print_msg(std::ostream * out, const char* prefix, const char* msg, va_list args) {
|
||||
if (out) {
|
||||
string2ostream(*out, prefix);
|
||||
*out << prefix;
|
||||
format2ostream(*out, msg, args);
|
||||
string2ostream(*out, "\n");
|
||||
*out << "\n";
|
||||
out->flush();
|
||||
}
|
||||
else {
|
||||
FILE * f = g_use_std_stdout ? stdout : stderr;
|
||||
fprintf(f, prefix);
|
||||
fprintf(f, "%s", prefix);
|
||||
vfprintf(f, msg, args);
|
||||
fprintf(f, "\n");
|
||||
fflush(f);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue