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

fix #1817

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-09-10 08:57:35 -07:00
parent 12f9336fec
commit fae66671d8
3 changed files with 22 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

41
src/smt/smt_internalizer.cpp
View file

@ -216,13 +216,17 @@ namespace smt {
SASSERT(m_manager.is_bool(n));
if (is_gate(m_manager, n)) {
switch(to_app(n)->get_decl_kind()) {
case OP_AND:
UNREACHABLE();
case OP_AND: {
for (expr * arg : *to_app(n)) {
internalize(arg, true);
literal lit = get_literal(arg);
mk_root_clause(1, &lit, pr);
}
break;
}
case OP_OR: {
literal_buffer lits;
unsigned num = to_app(n)->get_num_args();
for (unsigned i = 0; i < num; i++) {
expr * arg = to_app(n)->get_arg(i);
for (expr * arg : *to_app(n)) {
internalize(arg, true);
lits.push_back(get_literal(arg));
}
@ -294,8 +298,7 @@ namespace smt {
sort * s = m_manager.get_sort(n->get_arg(0));
sort_ref u(m_manager.mk_fresh_sort("distinct-elems"), m_manager);
func_decl_ref f(m_manager.mk_fresh_func_decl("distinct-aux-f", "", 1, &s, u), m_manager);
for (unsigned i = 0; i < num_args; i++) {
expr * arg = n->get_arg(i);
for (expr * arg : *n) {
app_ref fapp(m_manager.mk_app(f, arg), m_manager);
app_ref val(m_manager.mk_fresh_const("unique-value", u), m_manager);
enode * e = mk_enode(val, false, false, true);
@ -826,9 +829,7 @@ namespace smt {
void context::internalize_uninterpreted(app * n) {
SASSERT(!e_internalized(n));
// process args
unsigned num = n->get_num_args();
for (unsigned i = 0; i < num; i++) {
expr * arg = n->get_arg(i);
for (expr * arg : *n) {
internalize(arg, false);
SASSERT(e_internalized(arg));
}
@ -1542,10 +1543,9 @@ namespace smt {
void context::add_and_rel_watches(app * n) {
if (relevancy()) {
relevancy_eh * eh = m_relevancy_propagator->mk_and_relevancy_eh(n);
unsigned num = n->get_num_args();
for (unsigned i = 0; i < num; i++) {
for (expr * arg : *n) {
// if one child is assigned to false, the and-parent must be notified
literal l = get_literal(n->get_arg(i));
literal l = get_literal(arg);
add_rel_watch(~l, eh);
}
}
@ -1554,10 +1554,9 @@ namespace smt {
void context::add_or_rel_watches(app * n) {
if (relevancy()) {
relevancy_eh * eh = m_relevancy_propagator->mk_or_relevancy_eh(n);
unsigned num = n->get_num_args();
for (unsigned i = 0; i < num; i++) {
for (expr * arg : *n) {
// if one child is assigned to true, the or-parent must be notified
literal l = get_literal(n->get_arg(i));
literal l = get_literal(arg);
add_rel_watch(l, eh);
}
}
@ -1588,9 +1587,8 @@ namespace smt {
TRACE("mk_and_cnstr", tout << "l: "; display_literal(tout, l); tout << "\n";);
literal_buffer buffer;
buffer.push_back(l);
unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
literal l_arg = get_literal(n->get_arg(i));
for (expr * arg : *n) {
literal l_arg = get_literal(arg);
TRACE("mk_and_cnstr", tout << "l_arg: "; display_literal(tout, l_arg); tout << "\n";);
mk_gate_clause(~l, l_arg);
buffer.push_back(~l_arg);
@ -1602,9 +1600,8 @@ namespace smt {
literal l = get_literal(n);
literal_buffer buffer;
buffer.push_back(~l);
unsigned num_args = n->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
literal l_arg = get_literal(n->get_arg(i));
for (expr * arg : *n) {
literal l_arg = get_literal(arg);
mk_gate_clause(l, ~l_arg);
buffer.push_back(l_arg);
}

1
src/smt/theory_arith_core.h
View file

@ -484,7 +484,6 @@ namespace smt {
void theory_arith<Ext>::mk_idiv_mod_axioms(expr * dividend, expr * divisor) {
if (!m_util.is_zero(divisor)) {
ast_manager & m = get_manager();
bool is_numeral = m_util.is_numeral(divisor);
// if divisor is zero, then idiv and mod are uninterpreted functions.
expr_ref div(m), mod(m), zero(m), abs_divisor(m), one(m);
expr_ref eqz(m), eq(m), lower(m), upper(m);

8
src/smt/theory_lra.cpp
View file

@ -692,9 +692,7 @@ class theory_lra::imp {
++m_stats.m_add_rows;
}
void internalize_eq(theory_var v1, theory_var v2) {
enode* n1 = get_enode(v1);
enode* n2 = get_enode(v2);
void internalize_eq(theory_var v1, theory_var v2) {
app_ref term(m.mk_fresh_const("eq", a.mk_real()), m);
scoped_internalize_state st(*this);
st.vars().push_back(v1);
@ -707,8 +705,8 @@ class theory_lra::imp {
add_def_constraint(m_solver->add_var_bound(vi, lp::GE, rational::zero()));
TRACE("arith",
{
expr* o1 = n1->get_owner();
expr* o2 = n2->get_owner();
expr* o1 = get_enode(v1)->get_owner();
expr* o2 = get_enode(v2)->get_owner();
tout << "v" << v1 << " = " << "v" << v2 << ": "
<< mk_pp(o1, m) << " = " << mk_pp(o2, m) << "\n";
});