mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 14:49:01 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2013-05-02 15:24:16 +01:00
parent 00d5dea9a5 78db1d0f86
commit be19c2a3a8
7 changed files with 8 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()) {
proof* p1 = m.mk_pull_quant(fml, to_quantifier(fml1));
premise = mk_modus_ponens(premise, p1);
fml = fml1;
}
}
head = fml0;

1
src/smt/diff_logic.h
View file

@ -21,6 +21,7 @@ Revision History:
#include"vector.h"
#include"heap.h"
#include"statistics.h"
#include"trace.h"
#include"warning.h"

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(),
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()) {
char const * logic = m_is_lia ? "QF_LIA" : "QF_LRA";
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 unsigned clause_id;
typedef vector<std::pair<th_var, rational> > coeffs;
static const clause_id null_clause_id = UINT_MAX;
class clause;
class graph;
@ -108,7 +107,7 @@ namespace smt {
atom(bool_var bv, int pos, int neg) :
m_bvar(bv), m_true(false),
m_pos(pos), m_neg(neg) {}
virtual ~atom() {}
~atom() {}
bool_var get_bool_var() const { return m_bvar; }
bool is_true() const { return m_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 {
static const unsigned null_clause_id = UINT_MAX;
/**
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) :
m_bvar(bv), m_true(false),
m_pos(pos), m_neg(neg) {}
virtual ~atom() {}
~atom() {}
bool_var get_bool_var() const { return m_bvar; }
void assign_eh(bool is_true) { m_true = is_true; }
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_zero_int(null_theory_var),
m_zero_real(null_theory_var),
m_asserted_qhead(0),
m_nc_functor(*this),
m_asserted_qhead(0),
m_agility(0.5),
m_lia(false),
m_lra(false),