mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
some compile warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
414db51d5a
commit
518296dbc1
|
@ -1785,8 +1785,9 @@ bool ast_manager::slow_not_contains(ast const * n) {
|
|||
}
|
||||
#endif
|
||||
|
||||
static unsigned s_count = 0;
|
||||
#if 0
|
||||
static unsigned s_count = 0;
|
||||
|
||||
static void track_id(ast_manager& m, ast* n, unsigned id) {
|
||||
if (n->get_id() != id) return;
|
||||
++s_count;
|
||||
|
@ -1826,7 +1827,7 @@ ast * ast_manager::register_node_core(ast * n) {
|
|||
|
||||
// track_id(*this, n, 3);
|
||||
|
||||
TRACE("ast", tout << (s_count++) << " Object " << n->m_id << " was created.\n";);
|
||||
// TRACE("ast", tout << (s_count++) << " Object " << n->m_id << " was created.\n";);
|
||||
TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);
|
||||
// increment reference counters
|
||||
switch (n->get_kind()) {
|
||||
|
|
|
@ -22,7 +22,7 @@ namespace euf {
|
|||
|
||||
// one table per func_decl implementation
|
||||
unsigned etable::cg_hash::operator()(enode * n) const {
|
||||
SASSERT(decl(n)->is_flat_associative() || num_args(n) >= 3);
|
||||
SASSERT(decl(n)->is_flat_associative() || n->num_args() >= 3);
|
||||
unsigned a, b, c;
|
||||
a = b = 0x9e3779b9;
|
||||
c = 11;
|
||||
|
@ -51,8 +51,8 @@ namespace euf {
|
|||
|
||||
bool etable::cg_eq::operator()(enode * n1, enode * n2) const {
|
||||
SASSERT(decl(n1) == decl(n2));
|
||||
unsigned num = num_args(n1);
|
||||
if (num != num_args(n2)) {
|
||||
unsigned num = n1->num_args();
|
||||
if (num != n2->num_args()) {
|
||||
return false;
|
||||
}
|
||||
for (unsigned i = 0; i < num; i++)
|
||||
|
@ -96,7 +96,7 @@ namespace euf {
|
|||
}
|
||||
|
||||
unsigned etable::set_table_id(enode * n) {
|
||||
func_decl * f = n->get_decl();
|
||||
func_decl * f = decl(n);
|
||||
unsigned tid;
|
||||
decl_info d(f, n->num_args());
|
||||
if (!m_func_decl2id.find(d, tid)) {
|
||||
|
|
|
@ -24,7 +24,6 @@ namespace euf {
|
|||
|
||||
// one table per function symbol
|
||||
|
||||
static unsigned num_args(enode* n) { return n->num_args(); }
|
||||
static func_decl* decl(enode* n) { return n->get_decl(); }
|
||||
|
||||
|
||||
|
@ -36,7 +35,7 @@ namespace euf {
|
|||
|
||||
struct cg_unary_hash {
|
||||
unsigned operator()(enode * n) const {
|
||||
SASSERT(num_args(n) == 1);
|
||||
SASSERT(n->num_args() == 1);
|
||||
return get_root(n, 0)->hash();
|
||||
}
|
||||
};
|
||||
|
@ -44,8 +43,8 @@ namespace euf {
|
|||
struct cg_unary_eq {
|
||||
|
||||
bool operator()(enode * n1, enode * n2) const {
|
||||
SASSERT(num_args(n1) == 1);
|
||||
SASSERT(num_args(n2) == 1);
|
||||
SASSERT(n1->num_args() == 1);
|
||||
SASSERT(n2->num_args() == 1);
|
||||
SASSERT(decl(n1) == decl(n2));
|
||||
return get_root(n1, 0) == get_root(n2, 0);
|
||||
}
|
||||
|
@ -55,15 +54,15 @@ namespace euf {
|
|||
|
||||
struct cg_binary_hash {
|
||||
unsigned operator()(enode * n) const {
|
||||
SASSERT(num_args(n) == 2);
|
||||
SASSERT(n->num_args() == 2);
|
||||
return combine_hash(get_root(n, 0)->hash(), get_root(n, 1)->hash());
|
||||
}
|
||||
};
|
||||
|
||||
struct cg_binary_eq {
|
||||
bool operator()(enode * n1, enode * n2) const {
|
||||
SASSERT(num_args(n1) == 2);
|
||||
SASSERT(num_args(n2) == 2);
|
||||
SASSERT(n1->num_args() == 2);
|
||||
SASSERT(n2->num_args() == 2);
|
||||
SASSERT(decl(n1) == decl(n2));
|
||||
return
|
||||
get_root(n1, 0) == get_root(n2, 0) &&
|
||||
|
@ -75,7 +74,7 @@ namespace euf {
|
|||
|
||||
struct cg_comm_hash {
|
||||
unsigned operator()(enode * n) const {
|
||||
SASSERT(num_args(n) == 2);
|
||||
SASSERT(n->num_args() == 2);
|
||||
unsigned h1 = get_root(n, 0)->hash();
|
||||
unsigned h2 = get_root(n, 1)->hash();
|
||||
if (h1 > h2)
|
||||
|
@ -88,8 +87,8 @@ namespace euf {
|
|||
bool & m_commutativity;
|
||||
cg_comm_eq( bool & c): m_commutativity(c) {}
|
||||
bool operator()(enode * n1, enode * n2) const {
|
||||
SASSERT(num_args(n1) == 2);
|
||||
SASSERT(num_args(n2) == 2);
|
||||
SASSERT(n1->num_args() == 2);
|
||||
SASSERT(n2->num_args() == 2);
|
||||
|
||||
SASSERT(decl(n1) == decl(n2));
|
||||
enode* c1_1 = get_root(n1, 0);
|
||||
|
|
|
@ -753,8 +753,6 @@ namespace bv {
|
|||
literal_vector eqs;
|
||||
eqs.push_back(oeq);
|
||||
for (unsigned i = 0; i < sz; ++i) {
|
||||
literal l1 = m_bits[v1][i];
|
||||
literal l2 = m_bits[v2][i];
|
||||
expr_ref e1(m), e2(m);
|
||||
e1 = bv.mk_bit2bool(o1, i);
|
||||
e2 = bv.mk_bit2bool(o2, i);
|
||||
|
|
|
@ -399,8 +399,7 @@ namespace smt {
|
|||
unsigned m_next_node_id;
|
||||
key2node m_uvars;
|
||||
key2node m_A_f_is;
|
||||
|
||||
context * m_context;
|
||||
random_gen m_rand;
|
||||
|
||||
// Mapping from sort to auxiliary constant.
|
||||
// This auxiliary constant is used as a "witness" that is asserted as different from a
|
||||
|
@ -472,22 +471,18 @@ namespace smt {
|
|||
m_bv(m),
|
||||
m_array(m),
|
||||
m_next_node_id(0),
|
||||
m_context(nullptr),
|
||||
m_ks(m),
|
||||
m_model(nullptr),
|
||||
m_eval_cache_range(m),
|
||||
m_new_constraints(nullptr) {
|
||||
m_new_constraints(nullptr),
|
||||
m_rand(static_cast<unsigned>(m.limit().count())) {
|
||||
m.limit().inc();
|
||||
}
|
||||
|
||||
virtual ~auf_solver() {
|
||||
flush_nodes();
|
||||
reset_eval_cache();
|
||||
}
|
||||
|
||||
void set_context(context * ctx) {
|
||||
SASSERT(m_context== nullptr);
|
||||
m_context = ctx;
|
||||
}
|
||||
|
||||
ast_manager & get_manager() const { return m; }
|
||||
|
||||
|
@ -1075,7 +1070,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
void mk_inverses() {
|
||||
unsigned offset = m_context->get_random_value();
|
||||
unsigned offset = m_rand();
|
||||
for (unsigned i = m_root_nodes.size(); i-- > 0; ) {
|
||||
node* n = m_root_nodes[(i + offset) % m_root_nodes.size()];
|
||||
SASSERT(n->is_root());
|
||||
|
@ -1121,7 +1116,10 @@ namespace smt {
|
|||
The subclasses are defined in the .cpp file.
|
||||
*/
|
||||
class qinfo {
|
||||
protected:
|
||||
ast_manager& m;
|
||||
public:
|
||||
qinfo(ast_manager& m) :m(m) {}
|
||||
virtual ~qinfo() {}
|
||||
virtual char const * get_kind() const = 0;
|
||||
virtual bool is_equal(qinfo const * qi) const = 0;
|
||||
|
@ -1144,7 +1142,7 @@ namespace smt {
|
|||
unsigned m_arg_i;
|
||||
unsigned m_var_j;
|
||||
public:
|
||||
f_var(func_decl * f, unsigned i, unsigned j):m_f(f), m_arg_i(i), m_var_j(j) {}
|
||||
f_var(ast_manager& m, func_decl * f, unsigned i, unsigned j): qinfo(m), m_f(f), m_arg_i(i), m_var_j(j) {}
|
||||
~f_var() override {}
|
||||
|
||||
char const * get_kind() const override {
|
||||
|
@ -1166,7 +1164,6 @@ namespace smt {
|
|||
node * n1 = s.get_A_f_i(m_f, m_arg_i);
|
||||
node * n2 = s.get_uvar(q, m_var_j);
|
||||
CTRACE("model_finder", n1->get_sort() != n2->get_sort(),
|
||||
ast_manager & m = ctx->get_manager();
|
||||
tout << "sort bug:\n" << mk_ismt2_pp(q->get_expr(), m) << "\n" << mk_ismt2_pp(q, m) << "\n";
|
||||
tout << "decl(0): " << q->get_decl_name(0) << "\n";
|
||||
tout << "f: " << m_f->get_name() << " i: " << m_arg_i << "\n";
|
||||
|
@ -1224,7 +1221,7 @@ namespace smt {
|
|||
expr_ref m_offset;
|
||||
public:
|
||||
f_var_plus_offset(ast_manager & m, func_decl * f, unsigned i, unsigned j, expr * offset):
|
||||
f_var(f, i, j),
|
||||
f_var(m, f, i, j),
|
||||
m_offset(offset, m) {
|
||||
}
|
||||
~f_var_plus_offset() override {}
|
||||
|
@ -1261,12 +1258,12 @@ namespace smt {
|
|||
node * S_j = s.get_uvar(q, m_var_j);
|
||||
for (enode * n : ctx->enodes_of(m_f)) {
|
||||
if (ctx->is_relevant(n)) {
|
||||
arith_rewriter arith_rw(ctx->get_manager());
|
||||
bv_util bv(ctx->get_manager());
|
||||
bv_rewriter bv_rw(ctx->get_manager());
|
||||
arith_rewriter arith_rw(m);
|
||||
bv_util bv(m);
|
||||
bv_rewriter bv_rw(m);
|
||||
enode * e_arg = n->get_arg(m_arg_i);
|
||||
expr * arg = e_arg->get_owner();
|
||||
expr_ref arg_minus_k(ctx->get_manager());
|
||||
expr_ref arg_minus_k(m);
|
||||
if (bv.is_bv(arg))
|
||||
bv_rw.mk_sub(arg, m_offset, arg_minus_k);
|
||||
else
|
||||
|
@ -1376,7 +1373,6 @@ namespace smt {
|
|||
|
||||
class select_var : public qinfo {
|
||||
protected:
|
||||
ast_manager & m;
|
||||
array_util m_array;
|
||||
app * m_select; // It must satisfy is_auf_select... see bool is_auf_select(expr * t) const
|
||||
unsigned m_arg_i;
|
||||
|
@ -1393,7 +1389,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
public:
|
||||
select_var(ast_manager & m, app * s, unsigned i, unsigned j):m(m), m_array(m), m_select(s), m_arg_i(i), m_var_j(j) {}
|
||||
select_var(ast_manager & m, app * s, unsigned i, unsigned j):qinfo(m), m_array(m), m_select(s), m_arg_i(i), m_var_j(j) {}
|
||||
~select_var() override {}
|
||||
|
||||
char const * get_kind() const override {
|
||||
|
@ -1459,7 +1455,7 @@ namespace smt {
|
|||
unsigned m_var_i;
|
||||
unsigned m_var_j;
|
||||
public:
|
||||
var_pair(unsigned i, unsigned j):m_var_i(i), m_var_j(j) {
|
||||
var_pair(ast_manager& m, unsigned i, unsigned j): qinfo(m), m_var_i(i), m_var_j(j) {
|
||||
if (m_var_i > m_var_j)
|
||||
std::swap(m_var_i, m_var_j);
|
||||
}
|
||||
|
@ -1484,7 +1480,7 @@ namespace smt {
|
|||
|
||||
class x_eq_y : public var_pair {
|
||||
public:
|
||||
x_eq_y(unsigned i, unsigned j):var_pair(i, j) {}
|
||||
x_eq_y(ast_manager& m, unsigned i, unsigned j):var_pair(m, i, j) {}
|
||||
char const * get_kind() const override { return "x_eq_y"; }
|
||||
|
||||
void process_auf(quantifier * q, auf_solver & s, context * ctx) override {
|
||||
|
@ -1498,7 +1494,7 @@ namespace smt {
|
|||
|
||||
class x_neq_y : public var_pair {
|
||||
public:
|
||||
x_neq_y(unsigned i, unsigned j):var_pair(i, j) {}
|
||||
x_neq_y(ast_manager& m, unsigned i, unsigned j):var_pair(m, i, j) {}
|
||||
char const * get_kind() const override { return "x_neq_y"; }
|
||||
|
||||
void process_auf(quantifier * q, auf_solver & s, context * ctx) override {
|
||||
|
@ -1510,7 +1506,7 @@ namespace smt {
|
|||
|
||||
class x_leq_y : public var_pair {
|
||||
public:
|
||||
x_leq_y(unsigned i, unsigned j):var_pair(i, j) {}
|
||||
x_leq_y(ast_manager& m, unsigned i, unsigned j):var_pair(m, i, j) {}
|
||||
char const * get_kind() const override { return "x_leq_y"; }
|
||||
|
||||
void process_auf(quantifier * q, auf_solver & s, context * ctx) override {
|
||||
|
@ -1524,7 +1520,7 @@ namespace smt {
|
|||
// signed bit-vector comparison
|
||||
class x_sleq_y : public x_leq_y {
|
||||
public:
|
||||
x_sleq_y(unsigned i, unsigned j):x_leq_y(i, j) {}
|
||||
x_sleq_y(ast_manager& m, unsigned i, unsigned j):x_leq_y(m, i, j) {}
|
||||
char const * get_kind() const override { return "x_sleq_y"; }
|
||||
|
||||
void process_auf(quantifier * q, auf_solver & s, context * ctx) override {
|
||||
|
@ -1542,6 +1538,7 @@ namespace smt {
|
|||
expr_ref m_t;
|
||||
public:
|
||||
var_expr_pair(ast_manager & m, unsigned i, expr * t):
|
||||
qinfo(m),
|
||||
m_var_i(i), m_t(t, m) {}
|
||||
~var_expr_pair() override {}
|
||||
|
||||
|
@ -1553,7 +1550,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
void display(std::ostream & out) const override {
|
||||
out << "(" << get_kind() << ":v!" << m_var_i << ":" << mk_bounded_pp(m_t.get(), m_t.get_manager()) << ")";
|
||||
out << "(" << get_kind() << ":v!" << m_var_i << ":" << mk_bounded_pp(m_t.get(), m) << ")";
|
||||
}
|
||||
};
|
||||
|
||||
|
@ -1570,7 +1567,6 @@ namespace smt {
|
|||
|
||||
void populate_inst_sets(quantifier * q, auf_solver & slv, context * ctx) override {
|
||||
unsigned num_vars = q->get_num_decls();
|
||||
ast_manager & m = ctx->get_manager();
|
||||
sort * s = q->get_decl_sort(num_vars - m_var_i - 1);
|
||||
if (m.is_uninterp(s)) {
|
||||
// For uninterpreted sorts, we add all terms in the context.
|
||||
|
@ -2101,7 +2097,7 @@ namespace smt {
|
|||
expr * arg = t->get_arg(i);
|
||||
if (is_var(arg)) {
|
||||
SASSERT(t->get_decl()->get_domain(i) == to_var(arg)->get_sort());
|
||||
insert_qinfo(alloc(f_var, t->get_decl(), i, to_var(arg)->get_idx()));
|
||||
insert_qinfo(alloc(f_var, m, t->get_decl(), i, to_var(arg)->get_idx()));
|
||||
continue;
|
||||
}
|
||||
|
||||
|
@ -2231,17 +2227,17 @@ namespace smt {
|
|||
}
|
||||
else if (is_x_eq_y_atom(atom, v1, v2)) {
|
||||
if (sign)
|
||||
insert_qinfo(alloc(x_neq_y, v1->get_idx(), v2->get_idx()));
|
||||
insert_qinfo(alloc(x_neq_y, m, v1->get_idx(), v2->get_idx()));
|
||||
else {
|
||||
m_info->m_has_x_eq_y = true; // this atom is in the fringe of AUF
|
||||
insert_qinfo(alloc(x_eq_y, v1->get_idx(), v2->get_idx()));
|
||||
insert_qinfo(alloc(x_eq_y, m, v1->get_idx(), v2->get_idx()));
|
||||
}
|
||||
}
|
||||
else if (sign && is_x_gle_y_atom(atom, v1, v2)) {
|
||||
if (is_signed_le(atom))
|
||||
insert_qinfo(alloc(x_sleq_y, v1->get_idx(), v2->get_idx()));
|
||||
insert_qinfo(alloc(x_sleq_y, m, v1->get_idx(), v2->get_idx()));
|
||||
else
|
||||
insert_qinfo(alloc(x_leq_y, v1->get_idx(), v2->get_idx()));
|
||||
insert_qinfo(alloc(x_leq_y, m, v1->get_idx(), v2->get_idx()));
|
||||
}
|
||||
else if (is_x_gle_t_atom(atom, sign, v, t)) {
|
||||
insert_qinfo(alloc(x_gle_t, m, v->get_idx(), t));
|
||||
|
@ -3191,9 +3187,8 @@ namespace smt {
|
|||
}
|
||||
|
||||
void model_finder::set_context(context * ctx) {
|
||||
SASSERT(m_context == 0);
|
||||
SASSERT(m_context == nullptr);
|
||||
m_context = ctx;
|
||||
m_auf_solver->set_context(ctx);
|
||||
m_nm_solver->set_params(ctx->get_fparams());
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue