mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
Merge remote-tracking branch 'upstream/master' into develop
This commit is contained in:
commit
82d472a227
|
@ -1002,14 +1002,6 @@ class smt2_printer {
|
|||
reset_stacks();
|
||||
SASSERT(&(r.get_manager()) == &(fm()));
|
||||
m_soccs(n);
|
||||
TRACE("smt2_pp_shared",
|
||||
tout << "shared terms for:\n" << mk_pp(n, m()) << "\n";
|
||||
tout << "------>\n";
|
||||
shared_occs::iterator it = m_soccs.begin_shared();
|
||||
shared_occs::iterator end = m_soccs.end_shared();
|
||||
for (; it != end; ++it) {
|
||||
tout << mk_pp(*it, m()) << "\n";
|
||||
});
|
||||
m_root = n;
|
||||
push_frame(n, true);
|
||||
while (!m_frame_stack.empty()) {
|
||||
|
|
|
@ -551,13 +551,13 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
|
|||
// case 1: pos<0 or len<0
|
||||
// rewrite to ""
|
||||
if ( (constantPos && pos.is_neg()) || (constantLen && len.is_neg()) ) {
|
||||
result = m_util.str.mk_string(symbol(""));
|
||||
result = m_util.str.mk_empty(m().get_sort(a));
|
||||
return BR_DONE;
|
||||
}
|
||||
// case 1.1: pos >= length(base)
|
||||
// rewrite to ""
|
||||
if (constantBase && constantPos && pos.get_unsigned() >= s.length()) {
|
||||
result = m_util.str.mk_string(symbol(""));
|
||||
result = m_util.str.mk_empty(m().get_sort(a));
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
|
@ -663,20 +663,21 @@ br_status seq_rewriter::mk_seq_contains(expr* a, expr* b, expr_ref& result) {
|
|||
br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) {
|
||||
zstring c;
|
||||
rational r;
|
||||
if (m_util.str.is_string(a, c) && m_autil.is_numeral(b, r)) {
|
||||
if (m_autil.is_numeral(b, r)) {
|
||||
if (r.is_neg()) {
|
||||
result = m_util.str.mk_string(symbol(""));
|
||||
result = m_util.str.mk_empty(m().get_sort(a));
|
||||
return BR_DONE;
|
||||
}
|
||||
unsigned len = 0;
|
||||
bool bounded = min_length(1, &a, len);
|
||||
if (bounded && r >= rational(len)) {
|
||||
result = m_util.str.mk_empty(m().get_sort(a));
|
||||
return BR_DONE;
|
||||
} else if (r.is_unsigned()) {
|
||||
unsigned j = r.get_unsigned();
|
||||
if (j < c.length()) {
|
||||
result = m_util.str.mk_string(c.extract(j, 1));
|
||||
return BR_DONE;
|
||||
} else {
|
||||
result = m_util.str.mk_string(symbol(""));
|
||||
return BR_DONE;
|
||||
}
|
||||
}
|
||||
if (m_util.str.is_string(a, c) && r.is_unsigned() && r < rational(c.length())) {
|
||||
result = m_util.str.mk_string(c.extract(r.get_unsigned(), 1));
|
||||
return BR_DONE;
|
||||
}
|
||||
}
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
@ -734,6 +735,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
|
|||
bool isc2 = m_util.str.is_string(b, s2);
|
||||
if (isc1 && isc2) {
|
||||
result = m().mk_bool_val(s1.prefixof(s2));
|
||||
TRACE("seq", tout << result << "\n";);
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.str.is_empty(a)) {
|
||||
|
@ -747,6 +749,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
|
|||
expr_ref_vector as(m()), bs(m());
|
||||
|
||||
if (a1 != b1 && isc1 && isc2) {
|
||||
TRACE("seq", tout << s1 << " " << s2 << "\n";);
|
||||
if (s1.length() <= s2.length()) {
|
||||
if (s1.prefixof(s2)) {
|
||||
if (a == a1) {
|
||||
|
@ -791,26 +794,27 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
|
|||
m_util.str.get_concat(a, as);
|
||||
m_util.str.get_concat(b, bs);
|
||||
unsigned i = 0;
|
||||
bool all_values = true;
|
||||
expr_ref_vector eqs(m());
|
||||
for (; i < as.size() && i < bs.size(); ++i) {
|
||||
expr* a = as[i].get(), *b = bs[i].get();
|
||||
if (a == b) {
|
||||
continue;
|
||||
}
|
||||
all_values &= m().is_value(a) && m().is_value(b);
|
||||
if (all_values) {
|
||||
result = m().mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
if (m_util.str.is_unit(a) && m_util.str.is_unit(b)) {
|
||||
eqs.push_back(m().mk_eq(a, b));
|
||||
continue;
|
||||
}
|
||||
if (m().is_value(a) && m().is_value(b) && m_util.str.is_string(a) && m_util.str.is_string(b)) {
|
||||
TRACE("seq", tout << mk_pp(a, m()) << " != " << mk_pp(b, m()) << "\n";);
|
||||
result = m().mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
|
||||
break;
|
||||
}
|
||||
if (i == as.size()) {
|
||||
result = mk_and(eqs);
|
||||
TRACE("seq", tout << result << "\n";);
|
||||
if (m().is_true(result)) {
|
||||
return BR_DONE;
|
||||
}
|
||||
|
@ -822,6 +826,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
|
|||
eqs.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j].get()));
|
||||
}
|
||||
result = mk_and(eqs);
|
||||
TRACE("seq", tout << result << "\n";);
|
||||
return BR_REWRITE3;
|
||||
}
|
||||
if (i > 0) {
|
||||
|
@ -829,6 +834,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
|
|||
a = m_util.str.mk_concat(as.size() - i, as.c_ptr() + i);
|
||||
b = m_util.str.mk_concat(bs.size() - i, bs.c_ptr() + i);
|
||||
result = m_util.str.mk_prefix(a, b);
|
||||
TRACE("seq", tout << result << "\n";);
|
||||
return BR_DONE;
|
||||
}
|
||||
else {
|
||||
|
|
|
@ -1517,13 +1517,24 @@ void bv_simplifier_plugin::mk_bv2int(expr * arg, sort* range, expr_ref & result)
|
|||
result = m_arith.mk_add(tmp1, tmp2);
|
||||
}
|
||||
// commented out to reproduce bug in reduction of int2bv/bv2int
|
||||
else if (m_util.is_concat(arg)) {
|
||||
expr_ref tmp1(m_manager), tmp2(m_manager);
|
||||
unsigned sz2 = get_bv_size(to_app(arg)->get_arg(1));
|
||||
mk_bv2int(to_app(arg)->get_arg(0), range, tmp1);
|
||||
mk_bv2int(to_app(arg)->get_arg(1), range, tmp2);
|
||||
tmp1 = m_arith.mk_mul(m_arith.mk_numeral(power(numeral(2), sz2), true), tmp1);
|
||||
result = m_arith.mk_add(tmp1, tmp2);
|
||||
else if (m_util.is_concat(arg) && to_app(arg)->get_num_args() > 0) {
|
||||
expr_ref_vector args(m_manager);
|
||||
unsigned num_args = to_app(arg)->get_num_args();
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
expr_ref tmp(m_manager);
|
||||
mk_bv2int(to_app(arg)->get_arg(i), range, tmp);
|
||||
args.push_back(tmp);
|
||||
}
|
||||
unsigned sz = get_bv_size(to_app(arg)->get_arg(num_args-1));
|
||||
for (unsigned i = num_args - 1; i > 0; ) {
|
||||
expr_ref tmp(m_manager);
|
||||
--i;
|
||||
tmp = args[i].get();
|
||||
tmp = m_arith.mk_mul(m_arith.mk_numeral(power(numeral(2), sz), true), tmp);
|
||||
args[i] = tmp;
|
||||
sz += get_bv_size(to_app(arg)->get_arg(i));
|
||||
}
|
||||
result = m_arith.mk_add(args.size(), args.c_ptr());
|
||||
}
|
||||
else {
|
||||
parameter parameter(range);
|
||||
|
|
|
@ -126,6 +126,12 @@ namespace datalog {
|
|||
app* s;
|
||||
var* v;
|
||||
|
||||
// disable Ackerman reduction if head contains a non-variable or non-constant argument.
|
||||
for (unsigned i = 0; i < to_app(head)->get_num_args(); ++i) {
|
||||
expr* arg = to_app(head)->get_arg(i);
|
||||
if (!is_var(arg) && !m.is_value(arg)) return false;
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < conjs.size(); ++i) {
|
||||
expr* e = conjs[i].get();
|
||||
if (is_select_eq_var(e, s, v)) {
|
||||
|
@ -281,6 +287,7 @@ namespace datalog {
|
|||
m_rewriter(body);
|
||||
sub(head);
|
||||
m_rewriter(head);
|
||||
TRACE("dl", tout << body << " => " << head << "\n";);
|
||||
change = ackermanize(r, body, head);
|
||||
if (!change) {
|
||||
rules.add_rule(&r);
|
||||
|
|
|
@ -394,10 +394,6 @@ namespace datalog {
|
|||
m_simp(a, simp1_res);
|
||||
(*m_rw)(simp1_res.get(), res);
|
||||
|
||||
/*if (simp1_res.get()!=res.get()) {
|
||||
std::cout<<"pre norm:\n"<<mk_pp(simp1_res.get(),m)<<"post norm:\n"<<mk_pp(res.get(),m)<<"\n";
|
||||
}*/
|
||||
|
||||
m_simp(res.get(), res);
|
||||
}
|
||||
|
||||
|
|
|
@ -50,6 +50,7 @@ namespace opt {
|
|||
if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) {
|
||||
m_params.m_relevancy_lvl = 0;
|
||||
}
|
||||
// m_params.m_auto_config = false;
|
||||
}
|
||||
|
||||
unsigned opt_solver::m_dump_count = 0;
|
||||
|
|
|
@ -96,7 +96,6 @@ namespace sat {
|
|||
if (!process(c))
|
||||
continue; // clause was removed
|
||||
*it2 = *it;
|
||||
// throw exception to test bug fix: if (it2 != it) throw solver_exception("trigger bug");
|
||||
++it2;
|
||||
}
|
||||
s.m_clauses.set_end(it2);
|
||||
|
@ -129,14 +128,14 @@ namespace sat {
|
|||
// check if the clause is already satisfied
|
||||
for (i = 0; i < sz; i++) {
|
||||
if (s.value(c[i]) == l_true) {
|
||||
s.dettach_clause(c);
|
||||
s.detach_clause(c);
|
||||
s.del_clause(c);
|
||||
return false;
|
||||
}
|
||||
}
|
||||
// try asymmetric branching
|
||||
// clause must not be used for propagation
|
||||
s.dettach_clause(c);
|
||||
solver::scoped_detach scoped_d(s, c);
|
||||
s.push();
|
||||
for (i = 0; i < sz - 1; i++) {
|
||||
literal l = c[i];
|
||||
|
@ -154,7 +153,6 @@ namespace sat {
|
|||
SASSERT(s.m_qhead == s.m_trail.size());
|
||||
if (i == sz - 1) {
|
||||
// clause size can't be reduced.
|
||||
s.attach_clause(c);
|
||||
return true;
|
||||
}
|
||||
// clause can be reduced
|
||||
|
@ -188,19 +186,18 @@ namespace sat {
|
|||
case 1:
|
||||
TRACE("asymm_branch", tout << "produced unit clause: " << c[0] << "\n";);
|
||||
s.assign(c[0], justification());
|
||||
s.del_clause(c);
|
||||
s.propagate_core(false);
|
||||
scoped_d.del_clause();
|
||||
SASSERT(s.inconsistent() || s.m_qhead == s.m_trail.size());
|
||||
return false; // check_missed_propagation() may fail, since m_clauses is not in a consistent state.
|
||||
case 2:
|
||||
SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
|
||||
s.mk_bin_clause(c[0], c[1], false);
|
||||
s.del_clause(c);
|
||||
scoped_d.del_clause();
|
||||
SASSERT(s.m_qhead == s.m_trail.size());
|
||||
return false;
|
||||
default:
|
||||
c.shrink(new_sz);
|
||||
s.attach_clause(c);
|
||||
SASSERT(s.m_qhead == s.m_trail.size());
|
||||
return true;
|
||||
}
|
||||
|
|
|
@ -94,7 +94,7 @@ namespace sat {
|
|||
continue;
|
||||
}
|
||||
if (!c.frozen())
|
||||
m_solver.dettach_clause(c);
|
||||
m_solver.detach_clause(c);
|
||||
// apply substitution
|
||||
for (i = 0; i < sz; i++) {
|
||||
SASSERT(!m_solver.was_eliminated(c[i].var()));
|
||||
|
|
|
@ -168,14 +168,13 @@ namespace sat {
|
|||
m_need_cleanup = false;
|
||||
m_use_list.init(s.num_vars());
|
||||
init_visited();
|
||||
bool learned_in_use_lists = false;
|
||||
m_learned_in_use_lists = false;
|
||||
if (learned) {
|
||||
register_clauses(s.m_learned);
|
||||
learned_in_use_lists = true;
|
||||
m_learned_in_use_lists = true;
|
||||
}
|
||||
register_clauses(s.m_clauses);
|
||||
|
||||
|
||||
if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls))
|
||||
elim_blocked_clauses();
|
||||
|
||||
|
@ -184,7 +183,9 @@ namespace sat {
|
|||
|
||||
m_sub_counter = m_subsumption_limit;
|
||||
m_elim_counter = m_res_limit;
|
||||
unsigned old_num_elim_vars = m_num_elim_vars;
|
||||
m_old_num_elim_vars = m_num_elim_vars;
|
||||
|
||||
scoped_finalize _scoped_finalize(*this);
|
||||
|
||||
do {
|
||||
if (m_subsumption)
|
||||
|
@ -199,20 +200,22 @@ namespace sat {
|
|||
break;
|
||||
}
|
||||
while (!m_sub_todo.empty());
|
||||
}
|
||||
|
||||
bool vars_eliminated = m_num_elim_vars > old_num_elim_vars;
|
||||
void simplifier::scoped_finalize_fn() {
|
||||
bool vars_eliminated = m_num_elim_vars > m_old_num_elim_vars;
|
||||
|
||||
if (m_need_cleanup) {
|
||||
TRACE("after_simplifier", tout << "cleanning watches...\n";);
|
||||
cleanup_watches();
|
||||
cleanup_clauses(s.m_learned, true, vars_eliminated, learned_in_use_lists);
|
||||
cleanup_clauses(s.m_learned, true, vars_eliminated, m_learned_in_use_lists);
|
||||
cleanup_clauses(s.m_clauses, false, vars_eliminated, true);
|
||||
}
|
||||
else {
|
||||
TRACE("after_simplifier", tout << "skipping cleanup...\n";);
|
||||
if (vars_eliminated) {
|
||||
// must remove learned clauses with eliminated variables
|
||||
cleanup_clauses(s.m_learned, true, true, learned_in_use_lists);
|
||||
cleanup_clauses(s.m_learned, true, true, m_learned_in_use_lists);
|
||||
}
|
||||
}
|
||||
CASSERT("sat_solver", s.check_invariant());
|
||||
|
@ -279,7 +282,10 @@ namespace sat {
|
|||
unsigned sz = c.size();
|
||||
if (sz == 0) {
|
||||
s.set_conflict(justification());
|
||||
return;
|
||||
for (; it != end; ++it, ++it2) {
|
||||
*it2 = *it;
|
||||
}
|
||||
break;
|
||||
}
|
||||
if (sz == 1) {
|
||||
s.assign(c[0], justification());
|
||||
|
|
|
@ -91,6 +91,9 @@ namespace sat {
|
|||
unsigned m_num_sub_res;
|
||||
unsigned m_num_elim_lits;
|
||||
|
||||
bool m_learned_in_use_lists;
|
||||
unsigned m_old_num_elim_vars;
|
||||
|
||||
struct size_lt {
|
||||
bool operator()(clause const * c1, clause const * c2) const { return c1->size() > c2->size(); }
|
||||
};
|
||||
|
@ -170,6 +173,14 @@ namespace sat {
|
|||
struct subsumption_report;
|
||||
struct elim_var_report;
|
||||
|
||||
class scoped_finalize {
|
||||
simplifier& s;
|
||||
public:
|
||||
scoped_finalize(simplifier& s) : s(s) {}
|
||||
~scoped_finalize() { s.scoped_finalize_fn(); }
|
||||
};
|
||||
void scoped_finalize_fn();
|
||||
|
||||
public:
|
||||
simplifier(solver & s, params_ref const & p);
|
||||
~simplifier();
|
||||
|
|
|
@ -462,25 +462,25 @@ namespace sat {
|
|||
return simplify_clause_core<false>(num_lits, lits);
|
||||
}
|
||||
|
||||
void solver::dettach_bin_clause(literal l1, literal l2, bool learned) {
|
||||
void solver::detach_bin_clause(literal l1, literal l2, bool learned) {
|
||||
get_wlist(~l1).erase(watched(l2, learned));
|
||||
get_wlist(~l2).erase(watched(l1, learned));
|
||||
}
|
||||
|
||||
void solver::dettach_clause(clause & c) {
|
||||
void solver::detach_clause(clause & c) {
|
||||
if (c.size() == 3)
|
||||
dettach_ter_clause(c);
|
||||
detach_ter_clause(c);
|
||||
else
|
||||
dettach_nary_clause(c);
|
||||
detach_nary_clause(c);
|
||||
}
|
||||
|
||||
void solver::dettach_nary_clause(clause & c) {
|
||||
void solver::detach_nary_clause(clause & c) {
|
||||
clause_offset cls_off = get_offset(c);
|
||||
erase_clause_watch(get_wlist(~c[0]), cls_off);
|
||||
erase_clause_watch(get_wlist(~c[1]), cls_off);
|
||||
}
|
||||
|
||||
void solver::dettach_ter_clause(clause & c) {
|
||||
void solver::detach_ter_clause(clause & c) {
|
||||
erase_ternary_watch(get_wlist(~c[0]), c[1], c[2]);
|
||||
erase_ternary_watch(get_wlist(~c[1]), c[0], c[2]);
|
||||
erase_ternary_watch(get_wlist(~c[2]), c[0], c[1]);
|
||||
|
@ -1493,7 +1493,7 @@ namespace sat {
|
|||
for (unsigned i = new_sz; i < sz; i++) {
|
||||
clause & c = *(m_learned[i]);
|
||||
if (can_delete(c)) {
|
||||
dettach_clause(c);
|
||||
detach_clause(c);
|
||||
del_clause(c);
|
||||
}
|
||||
else {
|
||||
|
@ -1551,7 +1551,7 @@ namespace sat {
|
|||
else {
|
||||
c.inc_inact_rounds();
|
||||
if (c.inact_rounds() > m_config.m_gc_k) {
|
||||
dettach_clause(c);
|
||||
detach_clause(c);
|
||||
del_clause(c);
|
||||
m_stats.m_gc_clause++;
|
||||
deleted++;
|
||||
|
@ -1562,7 +1562,7 @@ namespace sat {
|
|||
if (psm(c) > static_cast<unsigned>(c.size() * m_min_d_tk)) {
|
||||
// move to frozen;
|
||||
TRACE("sat_frozen", tout << "freezing size: " << c.size() << " psm: " << psm(c) << " " << c << "\n";);
|
||||
dettach_clause(c);
|
||||
detach_clause(c);
|
||||
c.reset_inact_rounds();
|
||||
c.freeze();
|
||||
m_num_frozen++;
|
||||
|
@ -2595,7 +2595,7 @@ namespace sat {
|
|||
}
|
||||
else {
|
||||
clause & c = *(cw.get_clause());
|
||||
dettach_clause(c);
|
||||
detach_clause(c);
|
||||
attach_clause(c, reinit);
|
||||
if (scope_lvl() > 0 && reinit) {
|
||||
// clause propagated literal, must keep it in the reinit stack.
|
||||
|
@ -2628,7 +2628,7 @@ namespace sat {
|
|||
for (unsigned i = 0; i < clauses.size(); ++i) {
|
||||
clause & c = *(clauses[i]);
|
||||
if (c.contains(lit)) {
|
||||
dettach_clause(c);
|
||||
detach_clause(c);
|
||||
del_clause(c);
|
||||
}
|
||||
else {
|
||||
|
@ -2646,7 +2646,7 @@ namespace sat {
|
|||
literal l1 = m_user_bin_clauses[i].first;
|
||||
literal l2 = m_user_bin_clauses[i].second;
|
||||
if (nlit == l1 || nlit == l2) {
|
||||
dettach_bin_clause(l1, l2, learned);
|
||||
detach_bin_clause(l1, l2, learned);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
@ -195,15 +195,34 @@ namespace sat {
|
|||
bool attach_nary_clause(clause & c);
|
||||
void attach_clause(clause & c, bool & reinit);
|
||||
void attach_clause(clause & c) { bool reinit; attach_clause(c, reinit); }
|
||||
class scoped_detach {
|
||||
solver& s;
|
||||
clause& c;
|
||||
bool m_deleted;
|
||||
public:
|
||||
scoped_detach(solver& s, clause& c): s(s), c(c), m_deleted(false) {
|
||||
s.detach_clause(c);
|
||||
}
|
||||
~scoped_detach() {
|
||||
if (!m_deleted) s.attach_clause(c);
|
||||
}
|
||||
|
||||
void del_clause() {
|
||||
if (!m_deleted) {
|
||||
s.del_clause(c);
|
||||
m_deleted = true;
|
||||
}
|
||||
}
|
||||
};
|
||||
unsigned select_watch_lit(clause const & cls, unsigned starting_at) const;
|
||||
unsigned select_learned_watch_lit(clause const & cls) const;
|
||||
bool simplify_clause(unsigned & num_lits, literal * lits) const;
|
||||
template<bool lvl0>
|
||||
bool simplify_clause_core(unsigned & num_lits, literal * lits) const;
|
||||
void dettach_bin_clause(literal l1, literal l2, bool learned);
|
||||
void dettach_clause(clause & c);
|
||||
void dettach_nary_clause(clause & c);
|
||||
void dettach_ter_clause(clause & c);
|
||||
void detach_bin_clause(literal l1, literal l2, bool learned);
|
||||
void detach_clause(clause & c);
|
||||
void detach_nary_clause(clause & c);
|
||||
void detach_ter_clause(clause & c);
|
||||
void push_reinit_stack(clause & c);
|
||||
|
||||
// -----------------------
|
||||
|
|
|
@ -40,7 +40,7 @@ namespace smt {
|
|||
template<typename Ext>
|
||||
void theory_arith<Ext>::found_underspecified_op(app * n) {
|
||||
if (!m_found_underspecified_op) {
|
||||
TRACE("arith", tout << "found non underspecificed expression:\n" << mk_pp(n, get_manager()) << "\n";);
|
||||
TRACE("arith", tout << "found underspecificed expression:\n" << mk_pp(n, get_manager()) << "\n";);
|
||||
get_context().push_trail(value_trail<context, bool>(m_found_underspecified_op));
|
||||
m_found_underspecified_op = true;
|
||||
}
|
||||
|
@ -395,6 +395,7 @@ namespace smt {
|
|||
|
||||
template<typename Ext>
|
||||
theory_var theory_arith<Ext>::internalize_div(app * n) {
|
||||
if (!m_util.is_numeral(n->get_arg(1))) found_underspecified_op(n);
|
||||
found_underspecified_op(n);
|
||||
theory_var s = mk_binary_op(n);
|
||||
context & ctx = get_context();
|
||||
|
@ -418,7 +419,7 @@ namespace smt {
|
|||
template<typename Ext>
|
||||
theory_var theory_arith<Ext>::internalize_mod(app * n) {
|
||||
TRACE("arith_mod", tout << "internalizing...\n" << mk_pp(n, get_manager()) << "\n";);
|
||||
found_underspecified_op(n);
|
||||
if (!m_util.is_numeral(n->get_arg(1))) found_underspecified_op(n);
|
||||
theory_var s = mk_binary_op(n);
|
||||
context & ctx = get_context();
|
||||
if (!ctx.relevancy())
|
||||
|
@ -428,7 +429,7 @@ namespace smt {
|
|||
|
||||
template<typename Ext>
|
||||
theory_var theory_arith<Ext>::internalize_rem(app * n) {
|
||||
found_underspecified_op(n);
|
||||
if (!m_util.is_numeral(n->get_arg(1))) found_underspecified_op(n);
|
||||
theory_var s = mk_binary_op(n);
|
||||
context & ctx = get_context();
|
||||
if (!ctx.relevancy()) {
|
||||
|
|
|
@ -206,7 +206,8 @@ namespace smt {
|
|||
numeral k = ceil(get_value(v));
|
||||
rational _k = k.to_rational();
|
||||
expr_ref bound(get_manager());
|
||||
bound = m_util.mk_ge(get_enode(v)->get_owner(), m_util.mk_numeral(_k, true));
|
||||
expr* e = get_enode(v)->get_owner();
|
||||
bound = m_util.mk_ge(e, m_util.mk_numeral(_k, m_util.is_int(e)));
|
||||
TRACE("arith_int", tout << mk_bounded_pp(bound, get_manager()) << "\n";);
|
||||
context & ctx = get_context();
|
||||
ctx.internalize(bound, true);
|
||||
|
@ -371,7 +372,7 @@ namespace smt {
|
|||
|
||||
ctx.mk_th_axiom(get_id(), l1, l2);
|
||||
|
||||
TRACE("theory_arith_int",
|
||||
TRACE("arith_int",
|
||||
tout << "cut: (or " << mk_pp(p1, get_manager()) << " " << mk_pp(p2, get_manager()) << ")\n";
|
||||
);
|
||||
|
||||
|
@ -1407,6 +1408,7 @@ namespace smt {
|
|||
if (m_params.m_arith_int_eq_branching && branch_infeasible_int_equality()) {
|
||||
return FC_CONTINUE;
|
||||
}
|
||||
|
||||
theory_var int_var = find_infeasible_int_base_var();
|
||||
if (int_var != null_theory_var) {
|
||||
TRACE("arith_int", tout << "v" << int_var << " does not have an integer assignment: " << get_value(int_var) << "\n";);
|
||||
|
|
|
@ -607,12 +607,13 @@ namespace smt {
|
|||
}
|
||||
expr_ref sum(m);
|
||||
arith_simp().mk_add(sz, args.c_ptr(), sum);
|
||||
literal l(mk_eq(n, sum, false));
|
||||
TRACE("bv",
|
||||
tout << mk_pp(n, m) << "\n";
|
||||
tout << mk_pp(sum, m) << "\n";
|
||||
ctx.display_literal_verbose(tout, l);
|
||||
tout << "\n";
|
||||
);
|
||||
|
||||
literal l(mk_eq(n, sum, false));
|
||||
|
||||
ctx.mark_as_relevant(l);
|
||||
ctx.mk_th_axiom(get_id(), 1, &l);
|
||||
|
|
|
@ -901,7 +901,7 @@ namespace smt {
|
|||
objective_term const& objective = m_objectives[v];
|
||||
has_shared = false;
|
||||
|
||||
IF_VERBOSE(1,
|
||||
IF_VERBOSE(4,
|
||||
for (unsigned i = 0; i < objective.size(); ++i) {
|
||||
verbose_stream() << objective[i].second
|
||||
<< " * v" << objective[i].first << " ";
|
||||
|
@ -991,9 +991,12 @@ namespace smt {
|
|||
if (num_nodes <= v && v < num_nodes + num_edges) {
|
||||
unsigned edge_id = v - num_nodes;
|
||||
literal lit = m_edges[edge_id].m_justification;
|
||||
get_context().literal2expr(lit, tmp);
|
||||
core.push_back(tmp);
|
||||
if (lit != null_literal) {
|
||||
get_context().literal2expr(lit, tmp);
|
||||
core.push_back(tmp);
|
||||
}
|
||||
}
|
||||
TRACE("opt", tout << core << "\n";);
|
||||
}
|
||||
for (unsigned i = 0; i < num_nodes; ++i) {
|
||||
mpq_inf const& val = S.get_value(i);
|
||||
|
|
|
@ -2719,7 +2719,9 @@ bool theory_seq::can_propagate() {
|
|||
|
||||
expr_ref theory_seq::canonize(expr* e, dependency*& eqs) {
|
||||
expr_ref result = expand(e, eqs);
|
||||
TRACE("seq", tout << mk_pp(e, m) << " expands to " << result << "\n";);
|
||||
m_rewrite(result);
|
||||
TRACE("seq", tout << mk_pp(e, m) << " rewrites to " << result << "\n";);
|
||||
return result;
|
||||
}
|
||||
|
||||
|
@ -4469,10 +4471,11 @@ bool theory_seq::canonizes(bool sign, expr* e) {
|
|||
context& ctx = get_context();
|
||||
dependency* deps = 0;
|
||||
expr_ref cont = canonize(e, deps);
|
||||
TRACE("seq", tout << mk_pp(e, m) << " -> " << cont << "\n";);
|
||||
TRACE("seq", tout << mk_pp(e, m) << " -> " << cont << "\n";
|
||||
if (deps) display_deps(tout, deps););
|
||||
if ((m.is_true(cont) && !sign) ||
|
||||
(m.is_false(cont) && sign)) {
|
||||
TRACE("seq", display(tout););
|
||||
TRACE("seq", display(tout); tout << ctx.get_assignment(ctx.get_literal(e)) << "\n";);
|
||||
propagate_lit(deps, 0, 0, ctx.get_literal(e));
|
||||
return true;
|
||||
}
|
||||
|
|
|
@ -52,6 +52,7 @@ Revision History:
|
|||
|
||||
#ifdef USE_INTRINSICS
|
||||
#include <emmintrin.h>
|
||||
#include <smmintrin.h>
|
||||
#endif
|
||||
|
||||
hwf_manager::hwf_manager() :
|
||||
|
|
|
@ -88,9 +88,6 @@ public:
|
|||
bool is_pzero(hwf const & x);
|
||||
|
||||
bool is_one(hwf const & x);
|
||||
|
||||
// structural eq
|
||||
bool eq_core(hwf const & x, hwf const & y);
|
||||
|
||||
bool eq(hwf const & x, hwf const & y);
|
||||
bool lt(hwf const & x, hwf const & y);
|
||||
|
|
|
@ -70,6 +70,7 @@ void small_object_allocator::reset() {
|
|||
|
||||
void small_object_allocator::deallocate(size_t size, void * p) {
|
||||
if (size == 0) return;
|
||||
|
||||
#if defined(Z3DEBUG) && !defined(_WINDOWS)
|
||||
// Valgrind friendly
|
||||
memory::deallocate(p);
|
||||
|
@ -93,6 +94,7 @@ void small_object_allocator::deallocate(size_t size, void * p) {
|
|||
|
||||
void * small_object_allocator::allocate(size_t size) {
|
||||
if (size == 0) return 0;
|
||||
|
||||
#if defined(Z3DEBUG) && !defined(_WINDOWS)
|
||||
// Valgrind friendly
|
||||
return memory::allocate(size);
|
||||
|
|
Loading…
Reference in a new issue