mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix warnings and errors from the mint64 build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-05-01 19:54:40 +01:00
parent 7cb9e7381d
commit 717f131942
6 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/muz_qe/hnf.cpp
View file

@ -201,6 +201,7 @@ private:
if (!m_sorts.empty()) { if (!m_sorts.empty()) {
proof* p1 = m.mk_pull_quant(fml, to_quantifier(fml1)); proof* p1 = m.mk_pull_quant(fml, to_quantifier(fml1));
premise = mk_modus_ponens(premise, p1); premise = mk_modus_ponens(premise, p1);
fml = fml1;
} }
} }
head = fml0; head = fml0;

2
src/smt/theory_diff_logic_def.h
View file

@ -558,7 +558,7 @@ void theory_diff_logic<Ext>::new_edge(dl_var src, dl_var dst, unsigned num_edges
lits.size(), lits.c_ptr(), lits.size(), lits.c_ptr(),
params.size(), params.c_ptr()); params.size(), params.c_ptr());
} }
clause* cls = ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0); ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0);
if (dump_lemmas()) { if (dump_lemmas()) {
char const * logic = m_is_lia ? "QF_LIA" : "QF_LRA"; char const * logic = m_is_lia ? "QF_LIA" : "QF_LRA";
ctx.display_lemma_as_smt_problem(lits.size(), lits.c_ptr(), false_literal, logic); ctx.display_lemma_as_smt_problem(lits.size(), lits.c_ptr(), false_literal, logic);

3
src/smt/theory_horn_ineq.h
View file

@ -91,7 +91,6 @@ namespace smt {
typedef svector<th_var> th_var_vector; typedef svector<th_var> th_var_vector;
typedef unsigned clause_id; typedef unsigned clause_id;
typedef vector<std::pair<th_var, rational> > coeffs; typedef vector<std::pair<th_var, rational> > coeffs;
static const clause_id null_clause_id = UINT_MAX;
class clause; class clause;
class graph; class graph;
@ -108,7 +107,7 @@ namespace smt {
atom(bool_var bv, int pos, int neg) : atom(bool_var bv, int pos, int neg) :
m_bvar(bv), m_true(false), m_bvar(bv), m_true(false),
m_pos(pos), m_neg(neg) {} m_pos(pos), m_neg(neg) {}
virtual ~atom() {} ~atom() {}
bool_var get_bool_var() const { return m_bvar; } bool_var get_bool_var() const { return m_bvar; }
bool is_true() const { return m_true; } bool is_true() const { return m_true; }
void assign_eh(bool is_true) { m_true = is_true; } void assign_eh(bool is_true) { m_true = is_true; }

2
src/smt/theory_horn_ineq_def.h
View file

@ -27,6 +27,8 @@ Revision History:
namespace smt { namespace smt {
static const unsigned null_clause_id = UINT_MAX;
/** /**
A clause represents an inequality of the form A clause represents an inequality of the form

2
src/smt/theory_utvpi.h
View file

@ -78,7 +78,7 @@ namespace smt {
atom(bool_var bv, int pos, int neg) : atom(bool_var bv, int pos, int neg) :
m_bvar(bv), m_true(false), m_bvar(bv), m_true(false),
m_pos(pos), m_neg(neg) {} m_pos(pos), m_neg(neg) {}
virtual ~atom() {} ~atom() {}
bool_var get_bool_var() const { return m_bvar; } bool_var get_bool_var() const { return m_bvar; }
void assign_eh(bool is_true) { m_true = is_true; } void assign_eh(bool is_true) { m_true = is_true; }
int get_asserted_edge() const { return this->m_true?m_pos:m_neg; } int get_asserted_edge() const { return this->m_true?m_pos:m_neg; }

2
src/smt/theory_utvpi_def.h
View file

@ -54,8 +54,8 @@ namespace smt {
m_arith_eq_adapter(*this, m_params, a), m_arith_eq_adapter(*this, m_params, a),
m_zero_int(null_theory_var), m_zero_int(null_theory_var),
m_zero_real(null_theory_var), m_zero_real(null_theory_var),
m_asserted_qhead(0),
m_nc_functor(*this), m_nc_functor(*this),
m_asserted_qhead(0),
m_agility(0.5), m_agility(0.5),
m_lia(false), m_lia(false),
m_lra(false), m_lra(false),