mirror of
https://github.com/Z3Prover/z3
synced 2025-04-28 19:35:50 +00:00
fix a few compilation warnings
- remove unused variables and class fields - add support for gcc 4.5 & clang's __builtin_unreachable - fix 2 bugs related to strict aliasing - remove a few unused function parameters Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
This commit is contained in:
Nuno Lopes
parent
0673f645c9
commit
7ce88d4da9
46 changed files with 97 additions and 122 deletions
|
|
@ -300,7 +300,7 @@ std::ostream & operator<<(std::ostream & out, func_decl_info const & info) {
|
|||
//
|
||||
// -----------------------------------
|
||||
|
||||
char const * g_ast_kind_names[] = {"application", "variable", "quantifier", "sort", "function declaration" };
|
||||
static char const * g_ast_kind_names[] = {"application", "variable", "quantifier", "sort", "function declaration" };
|
||||
|
||||
char const * get_ast_kind_name(ast_kind k) {
|
||||
return g_ast_kind_names[k];
|
||||
|
|
|
|||
|
|
@ -1193,7 +1193,6 @@ enum pattern_op_kind {
|
|||
heurisitic quantifier instantiation.
|
||||
*/
|
||||
class pattern_decl_plugin : public decl_plugin {
|
||||
sort * m_list;
|
||||
public:
|
||||
virtual decl_plugin * mk_fresh() { return alloc(pattern_decl_plugin); }
|
||||
|
||||
|
|
|
|||
|
|
@ -326,6 +326,7 @@ namespace datalog {
|
|||
}
|
||||
unsigned index0;
|
||||
sort* last_sort = 0;
|
||||
SASSERT(num_params > 0);
|
||||
for (unsigned i = 0; i < num_params; ++i) {
|
||||
parameter const& p = params[i];
|
||||
if (!p.is_int()) {
|
||||
|
|
|
|||
|
|
@ -200,6 +200,7 @@ func_decl * float_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_par
|
|||
}
|
||||
else {
|
||||
m_manager->raise_exception("sort of floating point constant was not specified");
|
||||
UNREACHABLE();
|
||||
}
|
||||
|
||||
SASSERT(is_sort_of(s, m_family_id, FLOAT_SORT));
|
||||
|
|
|
|||
|
|
@ -79,7 +79,6 @@ void func_decl_dependencies::collect_ng_func_decls(expr * n, func_decl_set * s)
|
|||
*/
|
||||
class func_decl_dependencies::top_sort {
|
||||
enum color { OPEN, IN_PROGRESS, CLOSED };
|
||||
ast_manager & m_manager;
|
||||
dependency_graph & m_deps;
|
||||
|
||||
typedef obj_map<func_decl, color> color_map;
|
||||
|
|
@ -177,7 +176,7 @@ class func_decl_dependencies::top_sort {
|
|||
}
|
||||
|
||||
public:
|
||||
top_sort(ast_manager & m, dependency_graph & deps):m_manager(m), m_deps(deps) {}
|
||||
top_sort(dependency_graph & deps) : m_deps(deps) {}
|
||||
|
||||
bool operator()(func_decl * new_decl) {
|
||||
|
||||
|
|
@ -198,7 +197,7 @@ bool func_decl_dependencies::insert(func_decl * f, func_decl_set * s) {
|
|||
|
||||
m_deps.insert(f, s);
|
||||
|
||||
top_sort cycle_detector(m_manager, m_deps);
|
||||
top_sort cycle_detector(m_deps);
|
||||
if (cycle_detector(f)) {
|
||||
m_deps.erase(f);
|
||||
dealloc(s);
|
||||
|
|
|
|||
|
|
@ -22,10 +22,9 @@ Revision History:
|
|||
#include"uint_set.h"
|
||||
#include"var_subst.h"
|
||||
|
||||
quasi_macros::quasi_macros(ast_manager & m, macro_manager & mm, basic_simplifier_plugin & p, simplifier & s) :
|
||||
quasi_macros::quasi_macros(ast_manager & m, macro_manager & mm, simplifier & s) :
|
||||
m_manager(m),
|
||||
m_macro_manager(mm),
|
||||
m_bsimp(p),
|
||||
m_simplifier(s),
|
||||
m_new_vars(m),
|
||||
m_new_eqs(m),
|
||||
|
|
|
|||
|
|
@ -32,7 +32,6 @@ class quasi_macros {
|
|||
|
||||
ast_manager & m_manager;
|
||||
macro_manager & m_macro_manager;
|
||||
basic_simplifier_plugin & m_bsimp;
|
||||
simplifier & m_simplifier;
|
||||
occurrences_map m_occurrences;
|
||||
ptr_vector<expr> m_todo;
|
||||
|
|
@ -57,7 +56,7 @@ class quasi_macros {
|
|||
void apply_macros(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);
|
||||
|
||||
public:
|
||||
quasi_macros(ast_manager & m, macro_manager & mm, basic_simplifier_plugin & p, simplifier & s);
|
||||
quasi_macros(ast_manager & m, macro_manager & mm, simplifier & s);
|
||||
~quasi_macros();
|
||||
|
||||
/**
|
||||
|
|
|
|||
|
|
@ -30,7 +30,7 @@ class recurse_expr : public Visitor {
|
|||
vector<T, CallDestructors> m_results2;
|
||||
|
||||
bool is_cached(expr * n) const { T c; return m_cache.find(n, c); }
|
||||
T get_cached(expr * n) const { T c; m_cache.find(n, c); return c; }
|
||||
T get_cached(expr * n) const { return m_cache.find(n); }
|
||||
void cache_result(expr * n, T c) { m_cache.insert(n, c); }
|
||||
|
||||
void visit(expr * n, bool & visited);
|
||||
|
|
|
|||
|
|
@ -18,10 +18,6 @@ Revision History:
|
|||
--*/
|
||||
#include"matcher.h"
|
||||
|
||||
matcher::matcher(ast_manager & m):
|
||||
m_manager(m) {
|
||||
}
|
||||
|
||||
bool matcher::operator()(expr * e1, expr * e2, substitution & s) {
|
||||
reset();
|
||||
m_subst = &s;
|
||||
|
|
|
|||
|
|
@ -30,7 +30,6 @@ class matcher {
|
|||
typedef pair_hash<obj_ptr_hash<expr>, obj_ptr_hash<expr> > expr_pair_hash;
|
||||
typedef hashtable<expr_pair, expr_pair_hash, default_eq<expr_pair> > cache;
|
||||
|
||||
ast_manager & m_manager;
|
||||
substitution * m_subst;
|
||||
// cache m_cache;
|
||||
svector<expr_pair> m_todo;
|
||||
|
|
@ -38,7 +37,7 @@ class matcher {
|
|||
void reset();
|
||||
|
||||
public:
|
||||
matcher(ast_manager & m);
|
||||
matcher() {}
|
||||
|
||||
/**
|
||||
\brief Return true if e2 is an instance of e1.
|
||||
|
|
|
|||
|
|
@ -148,7 +148,7 @@ void substitution::apply(unsigned num_actual_offsets, unsigned const * deltas, e
|
|||
expr * arg = to_app(e)->get_arg(i);
|
||||
expr * new_arg;
|
||||
|
||||
m_apply_cache.find(expr_offset(arg, off), new_arg);
|
||||
VERIFY(m_apply_cache.find(expr_offset(arg, off), new_arg));
|
||||
new_args.push_back(new_arg);
|
||||
if (arg != new_arg)
|
||||
has_new_args = true;
|
||||
|
|
|
|||
|
|
@ -85,7 +85,6 @@ namespace subpaving {
|
|||
};
|
||||
|
||||
class context_mpf_wrapper : public context_wrapper<context_mpf> {
|
||||
f2n<mpf_manager> & m_fm;
|
||||
unsynch_mpq_manager & m_qm;
|
||||
scoped_mpf m_c;
|
||||
scoped_mpf_vector m_as;
|
||||
|
|
@ -103,7 +102,6 @@ namespace subpaving {
|
|||
public:
|
||||
context_mpf_wrapper(f2n<mpf_manager> & fm, params_ref const & p, small_object_allocator * a):
|
||||
context_wrapper<context_mpf>(fm, p, a),
|
||||
m_fm(fm),
|
||||
m_qm(fm.m().mpq_manager()),
|
||||
m_c(fm.m()),
|
||||
m_as(fm.m()),
|
||||
|
|
@ -145,7 +143,6 @@ namespace subpaving {
|
|||
};
|
||||
|
||||
class context_hwf_wrapper : public context_wrapper<context_hwf> {
|
||||
f2n<hwf_manager> & m_fm;
|
||||
unsynch_mpq_manager & m_qm;
|
||||
hwf m_c;
|
||||
svector<hwf> m_as;
|
||||
|
|
@ -166,7 +163,6 @@ namespace subpaving {
|
|||
public:
|
||||
context_hwf_wrapper(f2n<hwf_manager> & fm, unsynch_mpq_manager & qm, params_ref const & p, small_object_allocator * a):
|
||||
context_wrapper<context_hwf>(fm, p, a),
|
||||
m_fm(fm),
|
||||
m_qm(qm) {
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -647,7 +647,6 @@ namespace datalog {
|
|||
}
|
||||
}
|
||||
ast_manager& m = get_manager();
|
||||
datalog::rule_manager& rm = get_rule_manager();
|
||||
contains_pred contains_p(*this);
|
||||
check_pred check_pred(contains_p, get_manager());
|
||||
|
||||
|
|
|
|||
|
|
@ -99,11 +99,9 @@ namespace datalog {
|
|||
}
|
||||
|
||||
class interval_relation_plugin::rename_fn : public convenient_relation_rename_fn {
|
||||
interval_relation_plugin& m_plugin;
|
||||
public:
|
||||
rename_fn(interval_relation_plugin& p, const relation_signature & orig_sig, unsigned cycle_len, const unsigned * cycle)
|
||||
: convenient_relation_rename_fn(orig_sig, cycle_len, cycle),
|
||||
m_plugin(p){
|
||||
rename_fn(const relation_signature & orig_sig, unsigned cycle_len, const unsigned * cycle)
|
||||
: convenient_relation_rename_fn(orig_sig, cycle_len, cycle) {
|
||||
}
|
||||
|
||||
virtual relation_base * operator()(const relation_base & _r) {
|
||||
|
|
@ -120,7 +118,7 @@ namespace datalog {
|
|||
if(!check_kind(r)) {
|
||||
return 0;
|
||||
}
|
||||
return alloc(rename_fn, *this, r.get_signature(), cycle_len, permutation_cycle);
|
||||
return alloc(rename_fn, r.get_signature(), cycle_len, permutation_cycle);
|
||||
}
|
||||
|
||||
interval interval_relation_plugin::unite(interval const& src1, interval const& src2) {
|
||||
|
|
@ -194,11 +192,9 @@ namespace datalog {
|
|||
}
|
||||
|
||||
class interval_relation_plugin::union_fn : public relation_union_fn {
|
||||
interval_relation_plugin& m_plugin;
|
||||
bool m_is_widen;
|
||||
public:
|
||||
union_fn(interval_relation_plugin& p, bool is_widen) :
|
||||
m_plugin(p),
|
||||
union_fn(bool is_widen) :
|
||||
m_is_widen(is_widen) {
|
||||
}
|
||||
|
||||
|
|
@ -223,7 +219,7 @@ namespace datalog {
|
|||
if (!check_kind(tgt) || !check_kind(src) || (delta && !check_kind(*delta))) {
|
||||
return 0;
|
||||
}
|
||||
return alloc(union_fn, *this, false);
|
||||
return alloc(union_fn, false);
|
||||
}
|
||||
|
||||
relation_union_fn * interval_relation_plugin::mk_widen_fn(
|
||||
|
|
@ -232,7 +228,7 @@ namespace datalog {
|
|||
if (!check_kind(tgt) || !check_kind(src) || (delta && !check_kind(*delta))) {
|
||||
return 0;
|
||||
}
|
||||
return alloc(union_fn, *this, true);
|
||||
return alloc(union_fn, true);
|
||||
}
|
||||
|
||||
class interval_relation_plugin::filter_identical_fn : public relation_mutator_fn {
|
||||
|
|
|
|||
|
|
@ -141,7 +141,6 @@ namespace datalog {
|
|||
func_decl_ref_vector const& new_funcs() const { return m_new_funcs; }
|
||||
|
||||
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
|
||||
rule_manager& rm = m_context.get_rule_manager();
|
||||
bool found = false;
|
||||
for (unsigned j = 0; !found && j < num; ++j) {
|
||||
found = m_util.is_mkbv(args[j]);
|
||||
|
|
|
|||
|
|
@ -527,11 +527,10 @@ namespace datalog {
|
|||
}
|
||||
|
||||
class explanation_relation_plugin::intersection_filter_fn : public relation_intersection_filter_fn {
|
||||
explanation_relation_plugin & m_plugin;
|
||||
func_decl_ref m_union_decl;
|
||||
public:
|
||||
intersection_filter_fn(explanation_relation_plugin & plugin)
|
||||
: m_plugin(plugin), m_union_decl(plugin.m_union_decl) {}
|
||||
: m_union_decl(plugin.m_union_decl) {}
|
||||
|
||||
virtual void operator()(relation_base & tgt0, const relation_base & src0) {
|
||||
explanation_relation & tgt = static_cast<explanation_relation &>(tgt0);
|
||||
|
|
|
|||
|
|
@ -938,11 +938,8 @@ namespace datalog {
|
|||
|
||||
|
||||
class karr_relation_plugin::union_fn : public relation_union_fn {
|
||||
karr_relation_plugin& m_plugin;
|
||||
public:
|
||||
union_fn(karr_relation_plugin& p) :
|
||||
m_plugin(p) {
|
||||
}
|
||||
union_fn() {}
|
||||
|
||||
virtual void operator()(relation_base & _r, const relation_base & _src, relation_base * _delta) {
|
||||
|
||||
|
|
@ -966,7 +963,7 @@ namespace datalog {
|
|||
if (!check_kind(tgt) || !check_kind(src) || (delta && !check_kind(*delta))) {
|
||||
return 0;
|
||||
}
|
||||
return alloc(union_fn, *this);
|
||||
return alloc(union_fn);
|
||||
}
|
||||
|
||||
class karr_relation_plugin::filter_identical_fn : public relation_mutator_fn {
|
||||
|
|
|
|||
|
|
@ -320,9 +320,7 @@ namespace datalog {
|
|||
if(!m_ground_unconditional_rule_heads.contains(pred)) {
|
||||
m_ground_unconditional_rule_heads.insert(pred, alloc(obj_hashtable<app>));
|
||||
}
|
||||
obj_hashtable<app> * head_store;
|
||||
m_ground_unconditional_rule_heads.find(pred, head_store);
|
||||
head_store->insert(head);
|
||||
m_ground_unconditional_rule_heads.find(pred)->insert(head);
|
||||
|
||||
next_rule:;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1090,12 +1090,10 @@ namespace datalog {
|
|||
|
||||
class relation_manager::default_table_rename_fn
|
||||
: public convenient_table_rename_fn, auxiliary_table_transformer_fn {
|
||||
const unsigned m_cycle_len;
|
||||
public:
|
||||
default_table_rename_fn(const table_signature & orig_sig, unsigned permutation_cycle_len,
|
||||
const unsigned * permutation_cycle)
|
||||
: convenient_table_rename_fn(orig_sig, permutation_cycle_len, permutation_cycle),
|
||||
m_cycle_len(permutation_cycle_len) {
|
||||
: convenient_table_rename_fn(orig_sig, permutation_cycle_len, permutation_cycle) {
|
||||
SASSERT(permutation_cycle_len>=2);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -661,17 +661,15 @@ namespace datalog {
|
|||
SASSERT(res_idx<m_allocated_kinds.size());
|
||||
ids.insert(spec, res_idx);
|
||||
|
||||
family_id2spec * idspecs;
|
||||
VERIFY( m_kind_specs.find(sig, idspecs) );
|
||||
family_id2spec * idspecs = m_kind_specs.find(sig);
|
||||
idspecs->insert(m_allocated_kinds[res_idx], spec);
|
||||
}
|
||||
return m_allocated_kinds[res_idx];
|
||||
}
|
||||
|
||||
void get_relation_spec(const relation_signature & sig, family_id kind, Spec & spec) {
|
||||
family_id2spec * idspecs;
|
||||
VERIFY( m_kind_specs.find(sig, idspecs) );
|
||||
VERIFY( idspecs->find(kind, spec) );
|
||||
family_id2spec * idspecs = m_kind_specs.find(sig);
|
||||
spec = idspecs->find(kind);
|
||||
}
|
||||
|
||||
};
|
||||
|
|
|
|||
|
|
@ -198,8 +198,6 @@ namespace datalog {
|
|||
{
|
||||
bool values_match(const expr * v1, const expr * v2);
|
||||
|
||||
ast_manager & m_manager;
|
||||
|
||||
unsigned_vector m_args1;
|
||||
unsigned_vector m_args2;
|
||||
|
||||
|
|
@ -211,7 +209,7 @@ namespace datalog {
|
|||
static unsigned expr_cont_get_size(const ptr_vector<expr> & v) { return v.size(); }
|
||||
static expr * expr_cont_get(const ptr_vector<expr> & v, unsigned i) { return v[i]; }
|
||||
public:
|
||||
variable_intersection(ast_manager & m) : m_manager(m), m_consts(m) {}
|
||||
variable_intersection(ast_manager & m) : m_consts(m) {}
|
||||
|
||||
unsigned size() const {
|
||||
return m_args1.size();
|
||||
|
|
|
|||
|
|
@ -1028,7 +1028,6 @@ namespace nlarith {
|
|||
};
|
||||
|
||||
class sqrt_subst : public isubst {
|
||||
bool m_even;
|
||||
sqrt_form const& m_s;
|
||||
public:
|
||||
sqrt_subst(imp& i, sqrt_form const& s): isubst(i), m_s(s) {}
|
||||
|
|
|
|||
|
|
@ -1285,7 +1285,7 @@ namespace pdr {
|
|||
obj_hashtable<func_decl>::iterator itf = deps.begin(), endf = deps.end();
|
||||
for (; itf != endf; ++itf) {
|
||||
TRACE("pdr", tout << mk_pp(pred, m) << " " << mk_pp(*itf, m) << "\n";);
|
||||
VERIFY (rels.find(*itf, pt_user));
|
||||
pt_user = rels.find(*itf);
|
||||
pt_user->add_use(pt);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -418,11 +418,10 @@ namespace pdr {
|
|||
|
||||
class farkas_learner::constant_replacer_cfg : public default_rewriter_cfg
|
||||
{
|
||||
ast_manager& m;
|
||||
const obj_map<expr, expr *>& m_translation;
|
||||
public:
|
||||
constant_replacer_cfg(ast_manager& m, const obj_map<expr, expr *>& translation)
|
||||
: m(m), m_translation(translation)
|
||||
constant_replacer_cfg(const obj_map<expr, expr *>& translation)
|
||||
: m_translation(translation)
|
||||
{ }
|
||||
|
||||
bool get_subst(expr * s, expr * & t, proof * & t_pr) {
|
||||
|
|
|
|||
|
|
@ -1093,8 +1093,7 @@ namespace qe {
|
|||
bool has_branch(rational const& branch_id) const { return m_branch_index.contains(branch_id); }
|
||||
|
||||
search_tree* child(rational const& branch_id) const {
|
||||
unsigned idx;
|
||||
VERIFY(m_branch_index.find(branch_id, idx));
|
||||
unsigned idx = m_branch_index.find(branch_id);
|
||||
return m_children[idx];
|
||||
}
|
||||
|
||||
|
|
@ -1963,7 +1962,6 @@ namespace qe {
|
|||
expr_ref m_assumption;
|
||||
bool m_produce_models;
|
||||
ptr_vector<quant_elim_plugin> m_plugins;
|
||||
unsigned m_name_counter; // fresh-id
|
||||
volatile bool m_cancel;
|
||||
bool m_eliminate_variables_as_block;
|
||||
|
||||
|
|
@ -1973,7 +1971,6 @@ namespace qe {
|
|||
m_fparams(p),
|
||||
m_assumption(m),
|
||||
m_produce_models(m_fparams.m_model),
|
||||
m_name_counter(0),
|
||||
m_cancel(false),
|
||||
m_eliminate_variables_as_block(true)
|
||||
{
|
||||
|
|
|
|||
|
|
@ -12,14 +12,12 @@ namespace qe {
|
|||
// dl_plugin
|
||||
|
||||
class eq_atoms {
|
||||
ast_manager& m;
|
||||
expr_ref_vector m_eqs;
|
||||
expr_ref_vector m_neqs;
|
||||
app_ref_vector m_eq_atoms;
|
||||
app_ref_vector m_neq_atoms;
|
||||
public:
|
||||
eq_atoms(ast_manager& m):
|
||||
m(m),
|
||||
m_eqs(m),
|
||||
m_neqs(m),
|
||||
m_eq_atoms(m),
|
||||
|
|
|
|||
|
|
@ -740,7 +740,6 @@ namespace tb {
|
|||
typedef svector<double> double_vector;
|
||||
typedef obj_map<func_decl, double_vector> score_map;
|
||||
typedef obj_map<app, double> pred_map;
|
||||
datalog::context& m_ctx;
|
||||
ast_manager& m;
|
||||
datatype_util dt;
|
||||
score_map m_score_map;
|
||||
|
|
@ -750,19 +749,16 @@ namespace tb {
|
|||
pred_map m_pred_map;
|
||||
expr_ref_vector m_refs;
|
||||
double m_weight_multiply;
|
||||
unsigned m_num_invocations;
|
||||
unsigned m_update_frequency;
|
||||
unsigned m_next_update;
|
||||
|
||||
|
||||
public:
|
||||
selection(datalog::context& ctx):
|
||||
m_ctx(ctx),
|
||||
m(ctx.get_manager()),
|
||||
dt(m),
|
||||
m_refs(m),
|
||||
m_weight_multiply(1.0),
|
||||
m_num_invocations(0),
|
||||
m_update_frequency(20),
|
||||
m_next_update(20) {
|
||||
set_strategy(ctx.get_params().tab_selection());
|
||||
|
|
|
|||
|
|
@ -1472,7 +1472,7 @@ private:
|
|||
|
||||
SASSERT(sorts.size() > 0);
|
||||
|
||||
idbuilder* pop_q = new (region) pop_quantifier(this, (head_symbol == m_forall), weight, qid, skid, patterns, no_patterns, sorts, vars, local_scope, current);
|
||||
idbuilder* pop_q = new (region) pop_quantifier(this, (head_symbol == m_forall), weight, qid, skid, patterns, no_patterns, sorts, vars, local_scope);
|
||||
|
||||
expr_ref_vector * empty_v = alloc(expr_ref_vector, m_manager);
|
||||
up.push_back(new (region) parse_frame(current, pop_q, empty_v, 0, m_binding_level));
|
||||
|
|
@ -2522,7 +2522,7 @@ private:
|
|||
class pop_quantifier : public idbuilder {
|
||||
public:
|
||||
pop_quantifier(smtparser * smt, bool is_forall, int weight, symbol const& qid, symbol const& skid, expr_ref_buffer & patterns, expr_ref_buffer & no_patterns, sort_ref_buffer & sorts,
|
||||
svector<symbol>& vars, symbol_table<idbuilder*> & local_scope, proto_expr* p_expr):
|
||||
svector<symbol>& vars, symbol_table<idbuilder*> & local_scope):
|
||||
m_smt(smt),
|
||||
m_is_forall(is_forall),
|
||||
m_weight(weight),
|
||||
|
|
@ -2531,8 +2531,7 @@ private:
|
|||
m_patterns(m_smt->m_manager),
|
||||
m_no_patterns(m_smt->m_manager),
|
||||
m_sorts(m_smt->m_manager),
|
||||
m_local_scope(local_scope),
|
||||
m_p_expr(p_expr) {
|
||||
m_local_scope(local_scope) {
|
||||
SASSERT(sorts.size() == vars.size());
|
||||
|
||||
m_vars.append(vars);
|
||||
|
|
@ -2619,7 +2618,6 @@ private:
|
|||
sort_ref_buffer m_sorts;
|
||||
svector<symbol> m_vars;
|
||||
symbol_table<idbuilder*>& m_local_scope;
|
||||
proto_expr* m_p_expr;
|
||||
};
|
||||
|
||||
class builtin_builder : public idbuilder {
|
||||
|
|
|
|||
|
|
@ -243,7 +243,6 @@ namespace smt2 {
|
|||
}
|
||||
|
||||
scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive):
|
||||
m_ctx(ctx),
|
||||
m_interactive(interactive),
|
||||
m_spos(0),
|
||||
m_curr(0), // avoid Valgrind warning
|
||||
|
|
|
|||
|
|
@ -31,7 +31,6 @@ namespace smt2 {
|
|||
|
||||
class scanner {
|
||||
private:
|
||||
cmd_context & m_ctx;
|
||||
bool m_interactive;
|
||||
int m_spos; // position in the current line of the stream
|
||||
char m_curr; // current char;
|
||||
|
|
|
|||
|
|
@ -408,7 +408,7 @@ void asserted_formulas::apply_quasi_macros() {
|
|||
TRACE("before_quasi_macros", display(tout););
|
||||
expr_ref_vector new_exprs(m_manager);
|
||||
proof_ref_vector new_prs(m_manager);
|
||||
quasi_macros proc(m_manager, m_macro_manager, *m_bsimp, m_simplifier);
|
||||
quasi_macros proc(m_manager, m_macro_manager, m_simplifier);
|
||||
while (proc(m_asserted_formulas.size() - m_asserted_qhead,
|
||||
m_asserted_formulas.c_ptr() + m_asserted_qhead,
|
||||
m_asserted_formula_prs.c_ptr() + m_asserted_qhead,
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
char const * g_pattern_database =
|
||||
static char const * g_pattern_database =
|
||||
"(benchmark patterns \n"
|
||||
" :status unknown \n"
|
||||
" :logic ALL \n"
|
||||
|
|
|
|||
|
|
@ -311,7 +311,7 @@ bool expr_context_simplifier::is_false(expr* e) const {
|
|||
//
|
||||
|
||||
expr_strong_context_simplifier::expr_strong_context_simplifier(smt_params& p, ast_manager& m):
|
||||
m_manager(m), m_params(p), m_arith(m), m_id(0), m_fn(0,m), m_solver(m, p) {
|
||||
m_manager(m), m_arith(m), m_fn(0,m), m_solver(m, p) {
|
||||
sort* i_sort = m_arith.mk_int();
|
||||
m_fn = m.mk_func_decl(symbol(0xbeef101), i_sort, m.mk_bool_sort());
|
||||
}
|
||||
|
|
|
|||
|
|
@ -57,9 +57,7 @@ private:
|
|||
|
||||
class expr_strong_context_simplifier {
|
||||
ast_manager& m_manager;
|
||||
smt_params & m_params;
|
||||
arith_util m_arith;
|
||||
unsigned m_id;
|
||||
func_decl_ref m_fn;
|
||||
smt::kernel m_solver;
|
||||
|
||||
|
|
|
|||
|
|
@ -1849,11 +1849,9 @@ namespace smt {
|
|||
unsigned m_curr_max_generation; // temporary var used to store a copy of m_max_generation
|
||||
unsigned m_num_args;
|
||||
unsigned m_oreg;
|
||||
unsigned m_ireg;
|
||||
enode * m_n1;
|
||||
enode * m_n2;
|
||||
enode * m_app;
|
||||
instruction * m_alt;
|
||||
const bind * m_b;
|
||||
ptr_vector<enode> m_used_enodes;
|
||||
unsigned m_curr_used_enodes_size;
|
||||
|
|
|
|||
|
|
@ -68,14 +68,11 @@ namespace smt {
|
|||
bv_util& b() { return m_bv; }
|
||||
|
||||
class dl_value_proc : public smt::model_value_proc {
|
||||
smt::model_generator & m_mg;
|
||||
theory_dl& m_th;
|
||||
smt::enode* m_node;
|
||||
public:
|
||||
|
||||
dl_value_proc(smt::model_generator & m, theory_dl& th, smt::enode* n):
|
||||
m_mg(m), m_th(th), m_node(n)
|
||||
{ }
|
||||
dl_value_proc(theory_dl& th, smt::enode* n) : m_th(th), m_node(n) {}
|
||||
|
||||
virtual void get_dependencies(buffer<smt::model_value_dependency> & result) {}
|
||||
|
||||
|
|
@ -165,8 +162,8 @@ namespace smt {
|
|||
m.register_factory(alloc(dl_factory, m_util, m.get_model()));
|
||||
}
|
||||
|
||||
virtual smt::model_value_proc * mk_value(smt::enode * n, smt::model_generator & m) {
|
||||
return alloc(dl_value_proc, m, *this, n);
|
||||
virtual smt::model_value_proc * mk_value(smt::enode * n) {
|
||||
return alloc(dl_value_proc, *this, n);
|
||||
}
|
||||
|
||||
virtual void apply_sort_cnstr(enode * n, sort * s) {
|
||||
|
|
|
|||
|
|
@ -67,7 +67,7 @@ class quasi_macros_tactic : public tactic {
|
|||
simp.register_plugin(bvsimp);
|
||||
|
||||
macro_manager mm(m_manager, simp);
|
||||
quasi_macros qm(m_manager, mm, *bsimp, simp);
|
||||
quasi_macros qm(m_manager, mm, simp);
|
||||
bool more = true;
|
||||
|
||||
expr_ref_vector forms(m_manager), new_forms(m_manager);
|
||||
|
|
|
|||
|
|
@ -442,11 +442,10 @@ expr * ufbv_rewriter::rewrite(expr * n) {
|
|||
}
|
||||
|
||||
class ufbv_rewriter::add_back_idx_proc {
|
||||
ast_manager & m_manager;
|
||||
back_idx_map & m_back_idx;
|
||||
expr * m_expr;
|
||||
public:
|
||||
add_back_idx_proc(ast_manager & m, back_idx_map & bi, expr * e):m_manager(m),m_back_idx(bi),m_expr(e) {}
|
||||
add_back_idx_proc(back_idx_map & bi, expr * e):m_back_idx(bi),m_expr(e) {}
|
||||
void operator()(var * n) {}
|
||||
void operator()(quantifier * n) {}
|
||||
void operator()(app * n) {
|
||||
|
|
@ -469,11 +468,10 @@ public:
|
|||
};
|
||||
|
||||
class ufbv_rewriter::remove_back_idx_proc {
|
||||
ast_manager & m_manager;
|
||||
back_idx_map & m_back_idx;
|
||||
expr * m_expr;
|
||||
public:
|
||||
remove_back_idx_proc(ast_manager & m, back_idx_map & bi, expr * e):m_manager(m),m_back_idx(bi),m_expr(e) {}
|
||||
remove_back_idx_proc(back_idx_map & bi, expr * e):m_back_idx(bi),m_expr(e) {}
|
||||
void operator()(var * n) {}
|
||||
void operator()(quantifier * n) {}
|
||||
void operator()(app * n) {
|
||||
|
|
@ -511,7 +509,7 @@ void ufbv_rewriter::reschedule_processed(func_decl * f) {
|
|||
expr * p = *sit;
|
||||
// remove p from m_processed and m_back_idx
|
||||
m_processed.remove(p);
|
||||
remove_back_idx_proc proc(m_manager, m_back_idx, p); // this could change it->m_value, thus we need the `temp' set.
|
||||
remove_back_idx_proc proc(m_back_idx, p); // this could change it->m_value, thus we need the `temp' set.
|
||||
for_each_expr(proc, p);
|
||||
// insert p into m_todo
|
||||
m_todo.push_back(p);
|
||||
|
|
@ -619,7 +617,7 @@ void ufbv_rewriter::reschedule_demodulators(func_decl * f, expr * lhs) {
|
|||
// remove d from m_back_idx
|
||||
// just remember it here, because otherwise it and/or esit might become invalid?
|
||||
// to_remove.insert(d);
|
||||
remove_back_idx_proc proc(m_manager, m_back_idx, d);
|
||||
remove_back_idx_proc proc(m_back_idx, d);
|
||||
for_each_expr(proc, d);
|
||||
// insert d into m_todo
|
||||
m_todo.push_back(d);
|
||||
|
|
@ -674,7 +672,7 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const *
|
|||
// insert n' into m_processed
|
||||
m_processed.insert(np);
|
||||
// update m_back_idx (traverse n' and for each uninterpreted function declaration f in n' add the entry f->n' to m_back_idx)
|
||||
add_back_idx_proc proc(m_manager, m_back_idx, np);
|
||||
add_back_idx_proc proc(m_back_idx, np);
|
||||
for_each_expr(proc, np);
|
||||
} else {
|
||||
// np is a demodulator that allows us to replace 'large' with 'small'.
|
||||
|
|
@ -702,7 +700,7 @@ void ufbv_rewriter::operator()(unsigned n, expr * const * exprs, proof * const *
|
|||
insert_fwd_idx(large, small, to_quantifier(np));
|
||||
|
||||
// update m_back_idx
|
||||
add_back_idx_proc proc(m_manager, m_back_idx, np);
|
||||
add_back_idx_proc proc(m_back_idx, np);
|
||||
for_each_expr(proc, np);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -26,7 +26,7 @@ void tst_match(ast_manager & m, app * t, app * i) {
|
|||
substitution s(m);
|
||||
s.reserve(2, 10); // reserving a big number of variables to be safe.
|
||||
|
||||
matcher match(m);
|
||||
matcher match;
|
||||
std::cout << "Is " << mk_pp(i, m) << " an instance of " << mk_pp(t, m) << "\n";
|
||||
if (match(t, i, s)) {
|
||||
std::cout << "yes\n";
|
||||
|
|
|
|||
|
|
@ -19,6 +19,7 @@ Revision History:
|
|||
#include"bit_util.h"
|
||||
#include"util.h"
|
||||
#include"debug.h"
|
||||
#include <cstring>
|
||||
|
||||
/**
|
||||
\brief (Debugging version) Return the position of the most significant (set) bit of a
|
||||
|
|
@ -67,7 +68,11 @@ unsigned msb_pos(unsigned v) {
|
|||
*/
|
||||
unsigned nlz_core(unsigned x) {
|
||||
SASSERT(x != 0);
|
||||
#ifdef __GNUC__
|
||||
return __builtin_clz(x);
|
||||
#else
|
||||
return 31 - msb_pos(x);
|
||||
#endif
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -92,8 +97,15 @@ unsigned nlz(unsigned sz, unsigned const * data) {
|
|||
*/
|
||||
unsigned ntz_core(unsigned x) {
|
||||
SASSERT(x != 0);
|
||||
#ifdef __GNUC__
|
||||
return __builtin_ctz(x);
|
||||
#else
|
||||
float f = static_cast<float>(x & static_cast<unsigned>(-static_cast<int>(x)));
|
||||
return (*reinterpret_cast<unsigned *>(&f) >> 23) - 0x7f;
|
||||
unsigned u;
|
||||
SASSERT(sizeof(u) == sizeof(f));
|
||||
memcpy(&u, &f, sizeof(u));
|
||||
return (u >> 23) - 0x7f;
|
||||
#endif
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
|
|||
|
|
@ -24,7 +24,7 @@ Revision History:
|
|||
#include"str_hashtable.h"
|
||||
#include"z3_exception.h"
|
||||
|
||||
volatile bool g_enable_assertions = true;
|
||||
static volatile bool g_enable_assertions = true;
|
||||
|
||||
void enable_assertions(bool f) {
|
||||
g_enable_assertions = f;
|
||||
|
|
@ -41,7 +41,7 @@ void notify_assertion_violation(const char * fileName, int line, const char * co
|
|||
std::cerr << condition << "\n";
|
||||
}
|
||||
|
||||
str_hashtable* g_enabled_debug_tags = 0;
|
||||
static str_hashtable* g_enabled_debug_tags = 0;
|
||||
|
||||
static void init_debug_table() {
|
||||
if (!g_enabled_debug_tags) {
|
||||
|
|
|
|||
|
|
@ -29,6 +29,10 @@ bool assertions_enabled();
|
|||
#include<crtdbg.h>
|
||||
#endif
|
||||
|
||||
#ifndef __has_builtin
|
||||
# define __has_builtin(x) 0
|
||||
#endif
|
||||
|
||||
#include"error_codes.h"
|
||||
#include"warning.h"
|
||||
|
||||
|
|
@ -53,7 +57,14 @@ bool is_debug_enabled(const char * tag);
|
|||
#define SASSERT(COND) DEBUG_CODE(if (assertions_enabled() && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); INVOKE_DEBUGGER(); })
|
||||
#define CASSERT(TAG, COND) DEBUG_CODE(if (assertions_enabled() && is_debug_enabled(TAG) && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); INVOKE_DEBUGGER(); })
|
||||
#define XASSERT(COND, EXTRA_CODE) DEBUG_CODE(if (assertions_enabled() && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); { EXTRA_CODE } INVOKE_DEBUGGER(); })
|
||||
|
||||
#if (defined(__GNUC__) && ((__GNUC__ * 100 + __GNUC_MINOR__) >= 405)) || __has_builtin(__builtin_unreachable)
|
||||
// only available in gcc >= 4.5 and in newer versions of clang
|
||||
# define UNREACHABLE() __builtin_unreachable()
|
||||
#else
|
||||
#define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNREACHABLE CODE WAS REACHED."); INVOKE_DEBUGGER();)
|
||||
#endif
|
||||
|
||||
#define NOT_IMPLEMENTED_YET() { std::cerr << "NOT IMPLEMENTED YET!\n"; UNREACHABLE(); exit(ERR_NOT_IMPLEMENTED_YET); } ((void) 0)
|
||||
|
||||
#ifdef Z3DEBUG
|
||||
|
|
|
|||
|
|
@ -22,7 +22,7 @@ Notes:
|
|||
|
||||
extern void gparams_register_modules();
|
||||
|
||||
char const * g_old_params_names[] = {
|
||||
static char const * g_old_params_names[] = {
|
||||
"arith_adaptive","arith_adaptive_assertion_threshold","arith_adaptive_gcd","arith_adaptive_propagation_threshold","arith_add_binary_bounds","arith_blands_rule_threshold","arith_branch_cut_ratio","arith_dump_lemmas","arith_eager_eq_axioms","arith_eager_gcd","arith_eq_bounds","arith_euclidean_solver","arith_expand_eqs","arith_force_simplex","arith_gcd_test","arith_ignore_int","arith_lazy_adapter","arith_lazy_pivoting","arith_max_lemma_size","arith_process_all_eqs","arith_propagate_eqs","arith_propagation_mode","arith_propagation_threshold","arith_prop_strategy","arith_random_initial_value","arith_random_lower","arith_random_seed","arith_random_upper","arith_reflect","arith_skip_big_coeffs","arith_small_lemma_size","arith_solver","arith_stronger_lemmas","array_always_prop_upward","array_canonize","array_cg","array_delay_exp_axiom","array_extensional","array_laziness","array_lazy_ieq","array_lazy_ieq_delay","array_solver","array_weak","async_commands","at_labels_cex","auto_config","bb_eager","bb_ext_gates","bb_quantifiers","bin_clauses","bit2int","bv2int_distribute","bv_blast_max_size","bv_cc","bv_enable_int2bv_propagation","bv_lazy_le","bv_max_sharing","bv_reflect","bv_solver","case_split","check_at_labels","check_proof","cnf_factor","cnf_mode","context_simplifier","dack","dack_eq","dack_factor","dack_gc","dack_gc_inv_decay","dack_threshold","default_qid","default_table","default_table_checked","delay_units","delay_units_threshold","der","display_config","display_dot_proof","display_error_for_visual_studio","display_features","display_proof","display_unsat_core","distribute_forall","dt_lazy_splits","dump_goal_as_smt","elim_and","elim_bounds","elim_nlarith_quantifiers","elim_quantifiers","elim_term_ite","ematching","engine","eq_propagation","hi_div0","ignore_bad_patterns","ignore_setparameter","instruction_max","inst_gen","interactive","internalizer_nnf","lemma_gc_factor","lemma_gc_half","lemma_gc_initial","lemma_gc_new_clause_activity","lemma_gc_new_clause_relevancy","lemma_gc_new_old_ratio","lemma_gc_old_clause_activity","lemma_gc_old_clause_relevancy","lemma_gc_strategy","lift_ite","lookahead_diseq","macro_finder","max_conflicts","max_counterexamples","mbqi","mbqi_force_template","mbqi_max_cexs","mbqi_max_cexs_incr","mbqi_max_iterations","mbqi_trace","minimize_lemmas","model","model_compact","model_completion","model_display_arg_sort","model_hide_unused_partitions","model_on_final_check","model_on_timeout","model_partial","model_v1","model_v2","model_validate","new_core2th_eq","ng_lift_ite","nl_arith","nl_arith_branching","nl_arith_gb","nl_arith_gb_eqs","nl_arith_gb_perturbate","nl_arith_gb_threshold","nl_arith_max_degree","nl_arith_rounds","nnf_factor","nnf_ignore_labels","nnf_mode","nnf_sk_hack","order","order_var_weight","order_weights","phase_selection","pi_arith","pi_arith_weight","pi_avoid_skolems","pi_block_looop_patterns","pi_max_multi_patterns","pi_non_nested_arith_weight","pi_nopat_weight","pi_pull_quantifiers","pi_use_database","pi_warnings","pp_bounded","pp_bv_literals","pp_bv_neg","pp_decimal","pp_decimal_precision","pp_fixed_indent","pp_flat_assoc","pp_max_depth","pp_max_indent","pp_max_num_lines","pp_max_ribbon","pp_max_width","pp_min_alias_size","pp_simplify_implies","pp_single_line","precedence","precedence_gen","pre_demodulator","pre_simplifier","pre_simplify_expr","profile_res_sub","progress_sampling_freq","proof_mode","propagate_booleans","propagate_values","pull_cheap_ite_trees","pull_nested_quantifiers","qi_conservative_final_check","qi_cost","qi_eager_threshold","qi_lazy_instantiation","qi_lazy_quick_checker","qi_lazy_threshold","qi_max_eager_multi_patterns","qi_max_instances","qi_max_lazy_multi_pattern_matching","qi_new_gen","qi_profile","qi_profile_freq","qi_promote_unsat","qi_quick_checker","quasi_macros","random_case_split_freq","random_initial_activity","random_seed","recent_lemma_threshold","reduce_args","refine_inj_axiom","relevancy","relevancy_lemma","rel_case_split_order","restart_adaptive","restart_agility_threshold","restart_factor","restart_initial","restart_strategy","restricted_quasi_macros","simplify_clauses","smtlib2_compliant","smtlib_category","smtlib_dump_lemmas","smtlib_logic","smtlib_source_info","smtlib_trace_path","soft_timeout","solver","spc_bs","spc_es","spc_factor_subsumption_index_opt","spc_initial_subsumption_index_opt","spc_max_subsumption_index_features","spc_min_func_freq_subsumption_index","spc_num_iterations","spc_trace","statistics","strong_context_simplifier","tick","trace","trace_file_name","type_check","user_theory_persist_axioms","user_theory_preprocess_axioms","verbose","warning","well_sorted_check","z3_solver_ll_pp","z3_solver_smt_pp", 0 };
|
||||
|
||||
bool is_old_param_name(symbol const & name) {
|
||||
|
|
@ -35,7 +35,7 @@ bool is_old_param_name(symbol const & name) {
|
|||
return false;
|
||||
}
|
||||
|
||||
char const * g_params_renames[] = {
|
||||
static char const * g_params_renames[] = {
|
||||
"proof_mode", "proof",
|
||||
"soft_timeout", "timeout",
|
||||
"mbqi", "smt.mbqi",
|
||||
|
|
|
|||
|
|
@ -28,6 +28,12 @@ class hwf {
|
|||
friend class hwf_manager;
|
||||
double value;
|
||||
hwf & operator=(hwf const & other) { UNREACHABLE(); return *this; }
|
||||
uint64 get_raw() const {
|
||||
uint64 n;
|
||||
SASSERT(sizeof(n) == sizeof(value));
|
||||
memcpy(&n, &value, sizeof(value));
|
||||
return n;
|
||||
}
|
||||
|
||||
public:
|
||||
hwf() {}
|
||||
|
|
@ -122,16 +128,15 @@ public:
|
|||
|
||||
|
||||
bool sgn(hwf const & x) const {
|
||||
uint64 raw = *reinterpret_cast<uint64 const *>(&x.value);
|
||||
return (raw & 0x8000000000000000ull) != 0;
|
||||
return (x.get_raw() & 0x8000000000000000ull) != 0;
|
||||
}
|
||||
|
||||
const uint64 sig(hwf const & x) const {
|
||||
return *reinterpret_cast<uint64 const *>(&x.value) & 0x000FFFFFFFFFFFFFull;
|
||||
return x.get_raw() & 0x000FFFFFFFFFFFFFull;
|
||||
}
|
||||
|
||||
const int exp(hwf const & x) const {
|
||||
return ((*reinterpret_cast<uint64 const *>(&x.value) & 0x7FF0000000000000ull) >> 52) - 1023;
|
||||
return ((x.get_raw() & 0x7FF0000000000000ull) >> 52) - 1023;
|
||||
}
|
||||
|
||||
bool is_nan(hwf const & x);
|
||||
|
|
@ -151,7 +156,7 @@ public:
|
|||
void mk_pinf(hwf & o);
|
||||
void mk_ninf(hwf & o);
|
||||
|
||||
unsigned hash(hwf const & a) { return hash_ull(*reinterpret_cast<const unsigned long long*>(&a.value)); }
|
||||
unsigned hash(hwf const & a) { return hash_ull(a.get_raw()); }
|
||||
|
||||
inline void set_rounding_mode(mpf_rounding_mode rm);
|
||||
|
||||
|
|
|
|||
|
|
@ -27,14 +27,14 @@ void mem_finalize();
|
|||
out_of_memory_error::out_of_memory_error():z3_error(ERR_MEMOUT) {
|
||||
}
|
||||
|
||||
volatile bool g_memory_out_of_memory = false;
|
||||
bool g_memory_initialized = false;
|
||||
long long g_memory_alloc_size = 0;
|
||||
long long g_memory_max_size = 0;
|
||||
long long g_memory_max_used_size = 0;
|
||||
long long g_memory_watermark = 0;
|
||||
bool g_exit_when_out_of_memory = false;
|
||||
char const * g_out_of_memory_msg = "ERROR: out of memory";
|
||||
static volatile bool g_memory_out_of_memory = false;
|
||||
static bool g_memory_initialized = false;
|
||||
static long long g_memory_alloc_size = 0;
|
||||
static long long g_memory_max_size = 0;
|
||||
static long long g_memory_max_used_size = 0;
|
||||
static long long g_memory_watermark = 0;
|
||||
static bool g_exit_when_out_of_memory = false;
|
||||
static char const * g_out_of_memory_msg = "ERROR: out of memory";
|
||||
|
||||
void memory::exit_when_out_of_memory(bool flag, char const * msg) {
|
||||
g_exit_when_out_of_memory = flag;
|
||||
|
|
|
|||
|
|
@ -60,11 +60,11 @@ void myInvalidParameterHandler(
|
|||
#define END_ERR_HANDLER() {}
|
||||
#endif
|
||||
|
||||
bool g_warning_msgs = true;
|
||||
bool g_use_std_stdout = false;
|
||||
std::ostream* g_error_stream = 0;
|
||||
std::ostream* g_warning_stream = 0;
|
||||
bool g_show_error_msg_prefix = true;
|
||||
static bool g_warning_msgs = true;
|
||||
static bool g_use_std_stdout = false;
|
||||
static std::ostream* g_error_stream = 0;
|
||||
static std::ostream* g_warning_stream = 0;
|
||||
static bool g_show_error_msg_prefix = true;
|
||||
|
||||
void send_warnings_to_stdout(bool flag) {
|
||||
g_use_std_stdout = flag;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue