mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

fixing ci issues

Browse source 
fixing if condition
This commit is contained in:
nilsbecker 2019-02-25 19:10:47 +01:00
parent 960708e99e
commit 17adecff68
8 changed files with 16 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/bv_decl_plugin.h
View file

@ -437,7 +437,7 @@ public:
void log_bv_from_exprs(app * r, unsigned n, expr* const* es) {
if (m_manager.has_trace_stream()) {
for (unsigned i = 0; i < n; ++i) {
if (!m_manager.is_true(es[i]) && !m_manager.is_true(es[i]))
if (!m_manager.is_true(es[i]) && !m_manager.is_false(es[i]))
return;
}

4
src/smt/theory_bv.cpp
View file

@ -254,7 +254,7 @@ namespace smt {
literal l = ~(mk_eq(e1->get_owner(), e2->get_owner(), true));
context & ctx = get_context();
ast_manager & m = get_manager();
expr * eq = ctx.bool_var2expr(l.var());
expr * eq = ctx.bool_var2expr(l.var());
if (m.has_trace_stream()) {
app_ref body(m);
body = m.mk_implies(m.mk_eq(mk_bit2bool(get_enode(v1)->get_owner(), idx), m.mk_not(mk_bit2bool(get_enode(v2)->get_owner(), idx))), m.mk_not(eq));
@ -1219,7 +1219,7 @@ namespace smt {
#endif
literal_vector & lits = m_tmp_literals;
ptr_vector<expr> exprs;
expr_ref_vector exprs(m);
lits.reset();
literal eq = mk_eq(get_enode(v1)->get_owner(), get_enode(v2)->get_owner(), true);
lits.push_back(eq);

2
src/smt/theory_datatype.cpp
View file

@ -166,7 +166,7 @@ namespace smt {
func_decl * d = n->get_decl();
ptr_vector<func_decl> const & accessors = *m_util.get_constructor_accessors(d);
SASSERT(n->get_num_args() == accessors.size());
ptr_vector<app> bindings;
app_ref_vector bindings(m);
vector<std::tuple<enode *, enode *>> used_enodes;
used_enodes.push_back(std::make_tuple(nullptr, n));
for (unsigned i = 0; i < n->get_num_args(); ++i) {

2
src/smt/theory_jobscheduler.cpp
View file

@ -933,7 +933,7 @@ namespace smt {
}
}
literal_vector lits;
ptr_vector<expr> exprs;
expr_ref_vector exprs(m);
for (job_resource const& jr : jrs) {
unsigned r = jr.m_resource_id;
res_info const& ri = m_resources[r];

2
src/smt/theory_lra.cpp
View file

@ -1277,7 +1277,7 @@ public:
if (m_arith_params.m_arith_enum_const_mod && k.is_pos() && k < rational(8)) {
unsigned _k = k.get_unsigned();
literal_buffer lits;
ptr_vector<expr> exprs;
expr_ref_vector exprs(m);
for (unsigned j = 0; j < _k; ++j) {
literal mod_j = th.mk_eq(mod, a.mk_int(j), false);
lits.push_back(mod_j);

6
src/smt/theory_recfun.cpp
View file

@ -329,7 +329,7 @@ namespace smt {
// add case-axioms for all case-paths
auto & vars = e.m_def->get_vars();
literal_vector preds;
ptr_vector<expr> pred_exprs;
expr_ref_vector pred_exprs(m);
for (recfun::case_def const & c : e.m_def->get_cases()) {
// applied predicate to `args`
app_ref pred_applied = c.apply_case_predicate(e.m_args);
@ -352,7 +352,7 @@ namespace smt {
}
literal_vector guards;
ptr_vector<expr> exprs;
expr_ref_vector exprs(m);
guards.push_back(concl);
for (auto & g : c.get_guards()) {
expr_ref ga = apply_args(depth, vars, e.m_args, g);
@ -405,7 +405,7 @@ namespace smt {
expr_ref rhs = apply_args(depth, vars, args, e.m_cdef->get_rhs());
literal_vector clause;
ptr_vector<expr> exprs;
expr_ref_vector exprs(m);
for (auto & g : e.m_cdef->get_guards()) {
expr_ref guard = apply_args(depth, vars, args, g);
clause.push_back(~mk_literal(guard));

12
src/smt/theory_seq.cpp
View file

@ -3186,7 +3186,7 @@ bool theory_seq::solve_nc(unsigned idx) {
TRACE("seq", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()) << "\n";);
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
if (m.has_trace_stream()) {
ptr_vector<expr> exprs;
expr_ref_vector exprs(m);
for (literal l : lits) {
expr* e = ctx.bool_var2expr(l.var());
if (l.sign()) e = m.mk_not(e);
@ -4642,7 +4642,7 @@ void theory_seq::propagate_in_re(expr* n, bool is_true) {
unsigned_vector states;
a->get_epsilon_closure(a->init(), states);
lits.push_back(~lit);
ptr_vector<expr> exprs;
expr_ref_vector exprs(m);
for (unsigned st : states) {
literal acc = mk_accept(s, zero, re, st);
@ -5105,7 +5105,7 @@ literal theory_seq::mk_eq_empty(expr* _e, bool phase) {
return lit;
}
void theory_seq::push_lit_as_expr(literal l, ptr_vector<expr>& buf) {
void theory_seq::push_lit_as_expr(literal l, expr_ref_vector& buf) {
expr* e = get_context().bool_var2expr(l.var());
if (l.sign()) e = m.mk_not(e);
buf.push_back(e);
@ -5114,7 +5114,7 @@ void theory_seq::push_lit_as_expr(literal l, ptr_vector<expr>& buf) {
void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, literal l5) {
context& ctx = get_context();
literal_vector lits;
ptr_vector<expr> exprs;
expr_ref_vector exprs(m);
if (l1 == true_literal || l2 == true_literal || l3 == true_literal || l4 == true_literal || l5 == true_literal) return;
if (l1 != null_literal && l1 != false_literal) { ctx.mark_as_relevant(l1); lits.push_back(l1); push_lit_as_expr(l1, exprs); }
if (l2 != null_literal && l2 != false_literal) { ctx.mark_as_relevant(l2); lits.push_back(l2); push_lit_as_expr(l2, exprs); }
@ -5672,12 +5672,12 @@ void theory_seq::propagate_accept(literal lit, expr* acc) {
eautomaton::moves mvs;
aut->get_moves_from(src, mvs);
TRACE("seq", tout << mk_pp(acc, m) << " #moves " << mvs.size() << "\n";);
ptr_vector<expr> exprs;
expr_ref_vector exprs(m);
for (auto const& mv : mvs) {
expr_ref nth = mk_nth(e, idx);
expr_ref t = mv.t()->accept(nth);
get_context().get_rewriter()(t);
expr* step_e = mk_step(e, idx, re, src, mv.dst(), t);
expr_ref step_e(mk_step(e, idx, re, src, mv.dst(), t), m);
literal step = mk_literal(step_e);
lits.push_back(step);
exprs.push_back(step_e);

2
src/smt/theory_seq.h
View file

@ -547,7 +547,7 @@ namespace smt {
// terms whose meaning are encoded using axioms.
void enque_axiom(expr* e);
void deque_axiom(expr* e);
void push_lit_as_expr(literal l, ptr_vector<expr>& buf);
void push_lit_as_expr(literal l, expr_ref_vector& buf);
void add_axiom(literal l1, literal l2 = null_literal, literal l3 = null_literal, literal l4 = null_literal, literal l5 = null_literal);
void add_indexof_axiom(expr* e);
void add_replace_axiom(expr* e);