mirror of
https://github.com/Z3Prover/z3
synced 2026-02-16 05:41:43 +00:00
62b3668beb
Issue #7502 shows that running nlsat eagerly during final check can block quantifier instantiation. To give space for quantifier instances we introduce two levels for final check such that nlsat is only applied in the second and final level.
1462 lines
44 KiB
C++
1462 lines
44 KiB
C++
/*++
|
|
Copyright (c) 2006 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
theory_diff_logic_def.h
|
|
|
|
Abstract:
|
|
|
|
Difference Logic
|
|
|
|
Author:
|
|
|
|
Leonardo de Moura (leonardo) 2006-11-29.
|
|
Nikolaj Bjorner (nbjorner) 2008-05-11
|
|
|
|
Revision History:
|
|
|
|
2008-05-11 ported from v1.2. Add theory propagation.
|
|
|
|
--*/
|
|
#pragma once
|
|
|
|
#include "util/map.h"
|
|
#include "util/warning.h"
|
|
#include "ast/ast_pp.h"
|
|
#include "smt/theory_diff_logic.h"
|
|
#include "smt/smt_context.h"
|
|
#include "smt/smt_model_generator.h"
|
|
#include "model/model_implicant.h"
|
|
|
|
|
|
using namespace smt;
|
|
|
|
|
|
template<typename Ext>
|
|
theory_diff_logic<Ext>::theory_diff_logic(context& ctx):
|
|
theory(ctx, ctx.get_manager().mk_family_id("arith")),
|
|
m_params(ctx.get_fparams()),
|
|
m_util(ctx.get_manager()),
|
|
m_arith_eq_adapter(*this, m_util),
|
|
m_consistent(true),
|
|
m_izero(null_theory_var),
|
|
m_rzero(null_theory_var),
|
|
m_terms(ctx.get_manager()),
|
|
m_asserted_qhead(0),
|
|
m_num_core_conflicts(0),
|
|
m_num_propagation_calls(0),
|
|
m_agility(0.5),
|
|
m_lia_or_lra(not_set),
|
|
m_non_diff_logic_exprs(false),
|
|
m_factory(nullptr),
|
|
m_nc_functor(*this),
|
|
m_S(ctx.get_manager().limit()),
|
|
m_num_simplex_edges(0) {
|
|
}
|
|
|
|
template<typename Ext>
|
|
std::ostream& theory_diff_logic<Ext>::atom::display(theory_diff_logic const& th, std::ostream& out) const {
|
|
context& ctx = th.get_context();
|
|
lbool asgn = ctx.get_assignment(m_bvar);
|
|
//SASSERT(asgn == l_undef || ((asgn == l_true) == m_true));
|
|
bool sign = (l_undef == asgn) || m_true;
|
|
return out << literal(m_bvar, sign)
|
|
<< " " << mk_pp(ctx.bool_var2expr(m_bvar), th.get_manager()) << " ";
|
|
if (l_undef == asgn) {
|
|
out << "unassigned\n";
|
|
}
|
|
else {
|
|
th.m_graph.display_edge(out, get_asserted_edge());
|
|
}
|
|
return out;
|
|
}
|
|
|
|
// -----------------------------------------
|
|
// theory_diff_logic::nc_functor
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::nc_functor::reset() {
|
|
m_antecedents.reset();
|
|
}
|
|
|
|
|
|
// -----------------------------------------
|
|
// theory_diff_logic
|
|
|
|
|
|
template<typename Ext>
|
|
bool theory_diff_logic<Ext>::internalize_term(app * term) {
|
|
if (!m_consistent)
|
|
return false;
|
|
bool result = null_theory_var != mk_term(term);
|
|
CTRACE(arith, !result, tout << "Did not internalize " << mk_pp(term, m) << "\n";);
|
|
if (!result) {
|
|
TRACE(non_diff_logic, tout << "Terms may not be internalized\n";);
|
|
found_non_diff_logic_expr(term);
|
|
}
|
|
return result;
|
|
}
|
|
|
|
template<typename numeral>
|
|
class diff_logic_bounds {
|
|
bool m_inf_is_set;
|
|
bool m_sup_is_set;
|
|
bool m_eq_found;
|
|
literal m_inf_l;
|
|
literal m_sup_l;
|
|
literal m_eq_l;
|
|
numeral m_inf_w;
|
|
numeral m_sup_w;
|
|
numeral m_w;
|
|
|
|
public:
|
|
diff_logic_bounds() {
|
|
reset(numeral(0));
|
|
}
|
|
void reset(numeral const& w) {
|
|
m_inf_is_set = false;
|
|
m_sup_is_set = false;
|
|
m_eq_found = false;
|
|
m_inf_l = null_literal;
|
|
m_sup_l = null_literal;
|
|
m_eq_l = null_literal;
|
|
m_w = w;
|
|
}
|
|
|
|
void operator()(numeral const& w, literal l) {
|
|
if (l != null_literal) {
|
|
if ((w < m_w) && (!m_inf_is_set || w > m_inf_w)) {
|
|
m_inf_w = w;
|
|
m_inf_l = l;
|
|
m_inf_is_set = true;
|
|
}
|
|
else if ((w > m_w) && (!m_sup_is_set || w < m_sup_w)) {
|
|
m_sup_w = w;
|
|
m_sup_l = l;
|
|
m_sup_is_set = true;
|
|
}
|
|
else if (w == m_w) {
|
|
m_eq_found = true;
|
|
m_eq_l = l;
|
|
}
|
|
}
|
|
}
|
|
|
|
bool get_inf(numeral& w, literal& l) const {
|
|
w = m_inf_w;
|
|
l = m_inf_l;
|
|
return m_inf_is_set;
|
|
}
|
|
|
|
bool get_sup(numeral& w, literal& l) const {
|
|
w = m_sup_w;
|
|
l = m_sup_l;
|
|
return m_sup_is_set;
|
|
}
|
|
|
|
bool get_eq(literal& l) const {
|
|
l = m_eq_l;
|
|
return m_eq_found;
|
|
}
|
|
|
|
};
|
|
|
|
//
|
|
// Atoms are of the form x + -1*y <= k, or x + -1*y = k
|
|
//
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::found_non_diff_logic_expr(expr * n) {
|
|
if (!m_non_diff_logic_exprs) {
|
|
TRACE(non_diff_logic, tout << "found non diff logic expression:\n" << mk_pp(n, m) << "\n";);
|
|
IF_VERBOSE(0, verbose_stream() << "(smt.diff_logic: non-diff logic expression " << mk_pp(n, m) << ")\n";);
|
|
ctx.push_trail(value_trail<bool>(m_non_diff_logic_exprs));
|
|
m_non_diff_logic_exprs = true;
|
|
}
|
|
}
|
|
|
|
template<typename Ext>
|
|
bool theory_diff_logic<Ext>::internalize_atom(app * n, bool gate_ctx) {
|
|
if (!m_consistent)
|
|
return false;
|
|
if (!m_util.is_le(n) && !m_util.is_ge(n)) {
|
|
found_non_diff_logic_expr(n);
|
|
return false;
|
|
}
|
|
SASSERT(m_util.is_le(n) || m_util.is_ge(n));
|
|
SASSERT(!ctx.b_internalized(n));
|
|
|
|
bool is_ge = m_util.is_ge(n);
|
|
bool_var bv;
|
|
rational kr;
|
|
theory_var source, target; // target - source <= k
|
|
app * lhs = to_app(n->get_arg(0));
|
|
app * rhs = to_app(n->get_arg(1));
|
|
if (!m_util.is_numeral(rhs)) {
|
|
std::swap(rhs, lhs);
|
|
is_ge = !is_ge;
|
|
}
|
|
if (!m_util.is_numeral(rhs, kr)) {
|
|
found_non_diff_logic_expr(n);
|
|
return false;
|
|
}
|
|
numeral k(kr);
|
|
|
|
m_terms.reset();
|
|
m_signs.reset();
|
|
m_terms.push_back(lhs);
|
|
m_signs.push_back(true);
|
|
if (!decompose_linear(m_terms, m_signs)) {
|
|
found_non_diff_logic_expr(n);
|
|
return false;
|
|
}
|
|
SASSERT(m_signs.size() == m_terms.size());
|
|
if (m_terms.size() == 2 && m_signs[0] != m_signs[1]) {
|
|
app* a = m_terms.get(0), *b = m_terms.get(1);
|
|
bool sign0 = m_signs[0];
|
|
target = mk_var(a);
|
|
source = mk_var(b);
|
|
if (!sign0) {
|
|
std::swap(target, source);
|
|
}
|
|
}
|
|
else {
|
|
target = mk_var(lhs);
|
|
source = get_zero(m_util.is_int(lhs));
|
|
}
|
|
|
|
if (is_ge) {
|
|
std::swap(target, source);
|
|
k.neg();
|
|
}
|
|
|
|
if (ctx.b_internalized(n)) return true;
|
|
bv = ctx.mk_bool_var(n);
|
|
ctx.set_var_theory(bv, get_id());
|
|
literal l(bv);
|
|
|
|
//
|
|
// Create axioms for situations as:
|
|
// x - y <= 5 => x - y <= 7
|
|
//
|
|
|
|
if (m_params.m_arith_add_binary_bounds) {
|
|
literal l0;
|
|
numeral k0;
|
|
diff_logic_bounds<numeral> bounds;
|
|
bounds.reset(k);
|
|
m_graph.enumerate_edges(source, target, bounds);
|
|
if (bounds.get_eq(l0)) {
|
|
ctx.mk_th_axiom(get_id(),~l0,l);
|
|
ctx.mk_th_axiom(get_id(),~l,l0);
|
|
}
|
|
else {
|
|
if (bounds.get_inf(k0, l0)) {
|
|
SASSERT(k0 <= k);
|
|
ctx.mk_th_axiom(get_id(),~l0,l);
|
|
}
|
|
if (bounds.get_sup(k0, l0)) {
|
|
SASSERT(k <= k0);
|
|
ctx.mk_th_axiom(get_id(),~l,l0);
|
|
}
|
|
}
|
|
}
|
|
|
|
edge_id pos = m_graph.add_edge(source, target, k, l);
|
|
k.neg();
|
|
if (m_util.is_int(lhs)) {
|
|
SASSERT(k.is_int());
|
|
k -= numeral(1);
|
|
}
|
|
else {
|
|
k -= this->m_epsilon;
|
|
}
|
|
edge_id neg = m_graph.add_edge(target, source, k, ~l);
|
|
atom * a = alloc(atom, bv, pos, neg);
|
|
m_atoms.push_back(a);
|
|
m_bool_var2atom.insert(bv, a);
|
|
|
|
TRACE(arith,
|
|
tout << mk_pp(n, m) << "\n";
|
|
m_graph.display_edge(tout << "pos: ", pos);
|
|
m_graph.display_edge(tout << "neg: ", neg);
|
|
);
|
|
|
|
return true;
|
|
}
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::internalize_eq_eh(app * atom, bool_var v) {
|
|
TRACE(arith, tout << mk_pp(atom, m) << "\n";);
|
|
app * lhs = to_app(atom->get_arg(0));
|
|
app * rhs = to_app(atom->get_arg(1));
|
|
app * s;
|
|
if (m_util.is_add(lhs) && to_app(lhs)->get_num_args() == 2 &&
|
|
is_negative(to_app(to_app(lhs)->get_arg(1)), s) && m_util.is_numeral(rhs)) {
|
|
// force axioms for (= (+ x (* -1 y)) k)
|
|
// this is necessary because (+ x (* -1 y)) is not a diff logic term.
|
|
m_arith_eq_adapter.mk_axioms(ctx.get_enode(lhs), ctx.get_enode(rhs));
|
|
return;
|
|
}
|
|
|
|
if (m_params.m_arith_eager_eq_axioms) {
|
|
enode * n1 = ctx.get_enode(lhs);
|
|
enode * n2 = ctx.get_enode(rhs);
|
|
if (n1->get_th_var(get_id()) != null_theory_var &&
|
|
n2->get_th_var(get_id()) != null_theory_var)
|
|
m_arith_eq_adapter.mk_axioms(n1, n2);
|
|
}
|
|
}
|
|
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::assign_eh(bool_var v, bool is_true) {
|
|
m_stats.m_num_assertions++;
|
|
atom * a = nullptr;
|
|
VERIFY (m_bool_var2atom.find(v, a));
|
|
SASSERT(a);
|
|
SASSERT(ctx.get_assignment(v) != l_undef);
|
|
SASSERT((ctx.get_assignment(v) == l_true) == is_true);
|
|
a->assign_eh(is_true);
|
|
m_asserted_atoms.push_back(a);
|
|
}
|
|
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::collect_statistics(::statistics & st) const {
|
|
st.update("dl conflicts", m_stats.m_num_conflicts);
|
|
st.update("dl asserts", m_stats.m_num_assertions);
|
|
st.update("core->dl eqs", m_stats.m_num_core2th_eqs);
|
|
st.update("core->dl diseqs", m_stats.m_num_core2th_diseqs);
|
|
m_arith_eq_adapter.collect_statistics(st);
|
|
m_graph.collect_statistics(st);
|
|
}
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::push_scope_eh() {
|
|
TRACE(arith, tout << "push\n";);
|
|
theory::push_scope_eh();
|
|
m_graph.push();
|
|
m_scopes.push_back(scope());
|
|
scope & s = m_scopes.back();
|
|
s.m_atoms_lim = m_atoms.size();
|
|
s.m_asserted_atoms_lim = m_asserted_atoms.size();
|
|
s.m_asserted_qhead_old = m_asserted_qhead;
|
|
}
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::pop_scope_eh(unsigned num_scopes) {
|
|
TRACE(arith, tout << "pop " << num_scopes << "\n";);
|
|
unsigned lvl = m_scopes.size();
|
|
SASSERT(num_scopes <= lvl);
|
|
unsigned new_lvl = lvl - num_scopes;
|
|
scope & s = m_scopes[new_lvl];
|
|
del_atoms(s.m_atoms_lim);
|
|
m_asserted_atoms.shrink(s.m_asserted_atoms_lim);
|
|
m_asserted_qhead = s.m_asserted_qhead_old;
|
|
m_scopes.shrink(new_lvl);
|
|
unsigned num_edges = m_graph.get_num_edges();
|
|
m_graph.pop(num_scopes);
|
|
CTRACE(arith, !m_graph.is_feasible_dbg(), m_graph.display(tout););
|
|
if (num_edges != m_graph.get_num_edges() && m_num_simplex_edges > 0) {
|
|
m_S.reset();
|
|
m_num_simplex_edges = 0;
|
|
m_objective_rows.reset();
|
|
}
|
|
theory::pop_scope_eh(num_scopes);
|
|
}
|
|
|
|
template<typename Ext>
|
|
final_check_status theory_diff_logic<Ext>::final_check_eh(unsigned level) {
|
|
|
|
if (can_propagate()) {
|
|
propagate_core();
|
|
return FC_CONTINUE;
|
|
}
|
|
|
|
TRACE(arith_final, display(tout); );
|
|
if (!is_consistent())
|
|
return FC_CONTINUE;
|
|
SASSERT(is_consistent());
|
|
if (m_non_diff_logic_exprs) {
|
|
return FC_GIVEUP;
|
|
}
|
|
|
|
for (enode* n : ctx.enodes()) {
|
|
family_id fid = n->get_expr()->get_family_id();
|
|
if (fid != get_family_id() &&
|
|
fid != m.get_basic_family_id() &&
|
|
!is_uninterp_const(n->get_expr())) {
|
|
TRACE(arith, tout << mk_pp(n->get_expr(), m) << "\n";);
|
|
return FC_GIVEUP;
|
|
}
|
|
}
|
|
|
|
// either will already be zero (as we don't do mixed constraints).
|
|
m_graph.set_to_zero(get_zero(true), get_zero(false));
|
|
|
|
return FC_DONE;
|
|
}
|
|
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::del_atoms(unsigned old_size) {
|
|
typename atoms::iterator begin = m_atoms.begin() + old_size;
|
|
typename atoms::iterator it = m_atoms.end();
|
|
while (it != begin) {
|
|
--it;
|
|
atom * a = *it;
|
|
bool_var bv = a->get_bool_var();
|
|
m_bool_var2atom.erase(bv);
|
|
dealloc(a);
|
|
}
|
|
m_atoms.shrink(old_size);
|
|
}
|
|
|
|
|
|
template<typename Ext>
|
|
bool theory_diff_logic<Ext>::decompose_linear(app_ref_vector& terms, bool_vector& signs) {
|
|
for (unsigned i = 0; i < terms.size(); ++i) {
|
|
app* n = terms.get(i);
|
|
bool sign;
|
|
if (m_util.is_add(n)) {
|
|
expr* arg = n->get_arg(0);
|
|
if (!is_app(arg)) return false;
|
|
expr_ref _n(n, m);
|
|
terms[i] = to_app(arg);
|
|
sign = signs[i];
|
|
for (unsigned j = 1; j < n->get_num_args(); ++j) {
|
|
arg = n->get_arg(j);
|
|
if (!is_app(arg)) return false;
|
|
terms.push_back(to_app(arg));
|
|
signs.push_back(sign);
|
|
}
|
|
--i;
|
|
continue;
|
|
}
|
|
expr* x, *y;
|
|
if (m_util.is_mul(n, x, y)) {
|
|
if (is_sign(x, sign) && is_app(y)) {
|
|
terms[i] = to_app(y);
|
|
signs[i] = (signs[i] == sign);
|
|
--i;
|
|
}
|
|
else if (is_sign(y, sign) && is_app(x)) {
|
|
terms[i] = to_app(x);
|
|
signs[i] = (signs[i] == sign);
|
|
--i;
|
|
}
|
|
continue;
|
|
}
|
|
if (m_util.is_uminus(n, x) && is_app(x)) {
|
|
terms[i] = to_app(x);
|
|
signs[i] = !signs[i];
|
|
--i;
|
|
continue;
|
|
}
|
|
}
|
|
return true;
|
|
}
|
|
|
|
template<typename Ext>
|
|
bool theory_diff_logic<Ext>::is_sign(expr* n, bool& sign) {
|
|
rational r;
|
|
expr* x;
|
|
if (m_util.is_numeral(n, r)) {
|
|
if (r.is_one()) {
|
|
sign = true;
|
|
return true;
|
|
}
|
|
if (r.is_minus_one()) {
|
|
sign = false;
|
|
return true;
|
|
}
|
|
}
|
|
else if (m_util.is_uminus(n, x)) {
|
|
if (is_sign(x, sign)) {
|
|
sign = !sign;
|
|
return true;
|
|
}
|
|
}
|
|
return false;
|
|
}
|
|
|
|
template<typename Ext>
|
|
bool theory_diff_logic<Ext>::is_negative(app* n, app*& m) {
|
|
expr* a0, *a1, *a2;
|
|
rational r;
|
|
if (!m_util.is_mul(n, a0, a1)) {
|
|
return false;
|
|
}
|
|
if (m_util.is_numeral(a1)) {
|
|
std::swap(a0, a1);
|
|
}
|
|
if (m_util.is_numeral(a0, r) && r.is_minus_one() && is_app(a1)) {
|
|
m = to_app(a1);
|
|
return true;
|
|
}
|
|
if (m_util.is_uminus(a1)) {
|
|
std::swap(a0, a1);
|
|
}
|
|
if (m_util.is_uminus(a0, a2) && m_util.is_numeral(a2, r) && r.is_one() && is_app(a1)) {
|
|
m = to_app(a1);
|
|
return true;
|
|
}
|
|
return false;
|
|
}
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::propagate() {
|
|
if (m_params.m_arith_adaptive) {
|
|
|
|
switch (m_params.m_arith_propagation_strategy) {
|
|
|
|
case arith_prop_strategy::ARITH_PROP_PROPORTIONAL: {
|
|
|
|
++m_num_propagation_calls;
|
|
if (m_num_propagation_calls * (m_stats.m_num_conflicts + 1) >
|
|
m_params.m_arith_adaptive_propagation_threshold * ctx.m_stats.m_num_conflicts) {
|
|
m_num_propagation_calls = 1;
|
|
TRACE(arith_prop, tout << "propagating: " << m_num_propagation_calls << "\n";);
|
|
propagate_core();
|
|
}
|
|
else {
|
|
TRACE(arith_prop, tout << "skipping propagation " << m_num_propagation_calls << "\n";);
|
|
}
|
|
break;
|
|
}
|
|
case arith_prop_strategy::ARITH_PROP_AGILITY: {
|
|
// update agility with factor generated by other conflicts.
|
|
|
|
double g = m_params.m_arith_adaptive_propagation_threshold;
|
|
while (m_num_core_conflicts < ctx.m_stats.m_num_conflicts) {
|
|
m_agility = m_agility*g;
|
|
++m_num_core_conflicts;
|
|
}
|
|
++m_num_propagation_calls;
|
|
bool do_propagate = (m_num_propagation_calls * m_agility > m_params.m_arith_adaptive_propagation_threshold);
|
|
TRACE(arith_prop, tout << (do_propagate?"propagating: ":"skipping ")
|
|
<< " " << m_num_propagation_calls
|
|
<< " agility: " << m_agility << "\n";);
|
|
if (do_propagate) {
|
|
m_num_propagation_calls = 0;
|
|
propagate_core();
|
|
}
|
|
break;
|
|
}
|
|
default:
|
|
SASSERT(false);
|
|
propagate_core();
|
|
}
|
|
}
|
|
else {
|
|
propagate_core();
|
|
}
|
|
}
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::inc_conflicts() {
|
|
ctx.push_trail(value_trail<bool>(m_consistent));
|
|
m_consistent = false;
|
|
m_stats.m_num_conflicts++;
|
|
if (m_params.m_arith_adaptive) {
|
|
double g = m_params.m_arith_adaptive_propagation_threshold;
|
|
m_agility = m_agility*g + 1 - g;
|
|
}
|
|
}
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::propagate_core() {
|
|
bool consistent = true;
|
|
while (consistent && can_propagate()) {
|
|
atom * a = m_asserted_atoms[m_asserted_qhead];
|
|
m_asserted_qhead++;
|
|
consistent = propagate_atom(a);
|
|
}
|
|
}
|
|
|
|
template<typename Ext>
|
|
bool theory_diff_logic<Ext>::propagate_atom(atom* a) {
|
|
TRACE(arith, a->display(*this, tout); tout << "\n";);
|
|
if (ctx.inconsistent()) {
|
|
return false;
|
|
}
|
|
int edge_id = a->get_asserted_edge();
|
|
if (!m_graph.enable_edge(edge_id)) {
|
|
TRACE(arith, display(tout););
|
|
set_neg_cycle_conflict();
|
|
|
|
return false;
|
|
}
|
|
return true;
|
|
}
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::new_edge(dl_var src, dl_var dst, unsigned num_edges, edge_id const* edges) {
|
|
|
|
if (!theory_resolve()) {
|
|
return;
|
|
}
|
|
|
|
TRACE(dl_activity, tout << "\n";);
|
|
|
|
numeral w(0);
|
|
for (unsigned i = 0; i < num_edges; ++i) {
|
|
w += m_graph.get_weight(edges[i]);
|
|
}
|
|
enode* e1 = get_enode(src);
|
|
enode* e2 = get_enode(dst);
|
|
expr* n1 = e1->get_expr();
|
|
expr* n2 = e2->get_expr();
|
|
bool is_int = m_util.is_int(n1);
|
|
rational num = w.get_rational().to_rational();
|
|
|
|
expr_ref le(m);
|
|
if (w.is_rational()) {
|
|
// x - y <= w
|
|
expr* n3 = m_util.mk_numeral(num, is_int);
|
|
n2 = m_util.mk_mul(m_util.mk_numeral(rational(-1), is_int), n2);
|
|
le = m_util.mk_le(m_util.mk_add(n1,n2), n3);
|
|
}
|
|
else {
|
|
// x - y < w
|
|
// <=>
|
|
// not (x - y >= w)
|
|
// <=>
|
|
// not (y - x <= -w)
|
|
//
|
|
SASSERT(w.get_infinitesimal().is_neg());
|
|
expr* n3 = m_util.mk_numeral(-num, is_int);
|
|
n1 = m_util.mk_mul(m_util.mk_numeral(rational(-1), is_int), n1);
|
|
le = m_util.mk_le(m_util.mk_add(n2,n1), n3);
|
|
le = m.mk_not(le);
|
|
}
|
|
if (m.has_trace_stream())log_axiom_instantiation(le);
|
|
ctx.internalize(le, false);
|
|
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
|
ctx.mark_as_relevant(le.get());
|
|
literal lit(ctx.get_literal(le));
|
|
bool_var bv = lit.var();
|
|
atom* a = nullptr;
|
|
m_bool_var2atom.find(bv, a);
|
|
SASSERT(a);
|
|
|
|
literal_vector lits;
|
|
for (unsigned i = 0; i < num_edges; ++i) {
|
|
lits.push_back(~m_graph.get_explanation(edges[i]));
|
|
}
|
|
lits.push_back(lit);
|
|
|
|
TRACE(dl_activity,
|
|
tout << mk_pp(le, m) << "\n";
|
|
tout << "edge: " << a->get_pos() << "\n";
|
|
ctx.display_literals_verbose(tout, lits.size(), lits.data());
|
|
tout << "\n";
|
|
);
|
|
|
|
justification * js = nullptr;
|
|
if (m.proofs_enabled()) {
|
|
vector<parameter> params;
|
|
params.push_back(parameter(symbol("farkas")));
|
|
params.resize(lits.size()+1, parameter(rational(1)));
|
|
js = new (ctx.get_region()) theory_lemma_justification(get_id(), ctx,
|
|
lits.size(), lits.data(),
|
|
params.size(), params.data());
|
|
}
|
|
ctx.mk_clause(lits.size(), lits.data(), js, CLS_TH_LEMMA, nullptr);
|
|
|
|
#if 0
|
|
TRACE(arith,
|
|
tout << "shortcut:\n";
|
|
for (unsigned i = 0; i < num_edges; ++i) {
|
|
edge_id e = edges[i];
|
|
// tgt <= src + w
|
|
numeral w = m_graph.get_weight(e);
|
|
dl_var tgt = m_graph.get_target(e);
|
|
dl_var src = m_graph.get_source(e);
|
|
if (i + 1 < num_edges) {
|
|
dl_var tgt2 = m_graph.get_target(edges[i+1]);
|
|
SASSERT(src == tgt2);
|
|
}
|
|
tout << "$" << tgt << " <= $" << src << " + " << w << "\n";
|
|
}
|
|
{
|
|
numeral w = m_graph.get_weight(e_id);
|
|
dl_var tgt = m_graph.get_target(e_id);
|
|
dl_var src = m_graph.get_source(e_id);
|
|
tout << "$" << tgt << " <= $" << src << " + " << w << "\n";
|
|
}
|
|
);
|
|
#endif
|
|
|
|
}
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::set_neg_cycle_conflict() {
|
|
m_nc_functor.reset();
|
|
m_graph.traverse_neg_cycle2(m_params.m_arith_stronger_lemmas, m_nc_functor);
|
|
inc_conflicts();
|
|
literal_vector const& lits = m_nc_functor.get_lits();
|
|
TRACE(arith_conflict,
|
|
tout << "conflict: ";
|
|
for (literal lit : lits) ctx.display_literal_info(tout, lit);
|
|
tout << "\n";);
|
|
|
|
vector<parameter> params;
|
|
if (m.proofs_enabled()) {
|
|
params.push_back(parameter(symbol("farkas")));
|
|
for (unsigned i = 0; i <= lits.size(); ++i) {
|
|
params.push_back(parameter(rational(1)));
|
|
}
|
|
}
|
|
|
|
ctx.set_conflict(
|
|
ctx.mk_justification(
|
|
ext_theory_conflict_justification(
|
|
get_id(), ctx,
|
|
lits.size(), lits.data(), 0, nullptr, params.size(), params.data())));
|
|
|
|
}
|
|
|
|
template<typename Ext>
|
|
bool theory_diff_logic<Ext>::is_offset(app* n, app*& v, app*& offset, rational& r) {
|
|
if (!m_util.is_add(n)) {
|
|
return false;
|
|
}
|
|
|
|
if (n->get_num_args() == 2 && m_util.is_numeral(n->get_arg(0), r)) {
|
|
v = to_app(n->get_arg(1));
|
|
offset = to_app(n->get_arg(0));
|
|
return true;
|
|
}
|
|
if (n->get_num_args() == 2 && m_util.is_numeral(n->get_arg(1), r)) {
|
|
v = to_app(n->get_arg(0));
|
|
offset = to_app(n->get_arg(1));
|
|
return true;
|
|
}
|
|
return false;
|
|
}
|
|
|
|
template<typename Ext>
|
|
theory_var theory_diff_logic<Ext>::mk_term(app* n) {
|
|
SASSERT(!m_util.is_sub(n));
|
|
SASSERT(!m_util.is_uminus(n));
|
|
app* a, *offset;
|
|
theory_var source, target;
|
|
enode* e;
|
|
|
|
TRACE(arith, tout << mk_pp(n, m) << "\n";);
|
|
|
|
rational r;
|
|
if (m_util.is_numeral(n, r)) {
|
|
return mk_num(n, r);
|
|
}
|
|
else if (is_offset(n, a, offset, r)) {
|
|
// n = a + k
|
|
source = mk_var(a);
|
|
for (unsigned i = 0; i < n->get_num_args(); ++i) {
|
|
expr* arg = n->get_arg(i);
|
|
if (!ctx.e_internalized(arg)) {
|
|
ctx.internalize(arg, false);
|
|
}
|
|
}
|
|
e = ctx.mk_enode(n, false, false, true);
|
|
target = mk_var(e);
|
|
numeral k(r);
|
|
// target - source <= k, source - target <= -k
|
|
m_graph.enable_edge(m_graph.add_edge(source, target, k, null_literal));
|
|
m_graph.enable_edge(m_graph.add_edge(target, source, -k, null_literal));
|
|
return target;
|
|
}
|
|
else if (m_util.is_arith_expr(n)) {
|
|
return null_theory_var;
|
|
}
|
|
else {
|
|
return mk_var(n);
|
|
}
|
|
}
|
|
|
|
|
|
template<typename Ext>
|
|
theory_var theory_diff_logic<Ext>::mk_num(app* n, rational const& r) {
|
|
theory_var v = null_theory_var;
|
|
enode* e = nullptr;
|
|
if (r.is_zero()) {
|
|
v = get_zero(m_util.is_int(n));
|
|
}
|
|
else if (ctx.e_internalized(n)) {
|
|
e = ctx.get_enode(n);
|
|
v = e->get_th_var(get_id());
|
|
SASSERT(v != null_theory_var);
|
|
}
|
|
else {
|
|
theory_var zero = get_zero(m_util.is_int(n));
|
|
SASSERT(n->get_num_args() == 0);
|
|
e = ctx.mk_enode(n, false, false, true);
|
|
v = mk_var(e);
|
|
// internalizer is marking enodes as interpreted whenever the associated ast is a value and a constant.
|
|
// e->mark_as_interpreted();
|
|
numeral k(r);
|
|
// v = k: v - zero <= k, zero - v <= - k
|
|
m_graph.enable_edge(m_graph.add_edge(zero, v, k, null_literal));
|
|
m_graph.enable_edge(m_graph.add_edge(v, zero, -k, null_literal));
|
|
}
|
|
return v;
|
|
}
|
|
|
|
|
|
template<typename Ext>
|
|
theory_var theory_diff_logic<Ext>::mk_var(enode* n) {
|
|
theory_var v = theory::mk_var(n);
|
|
TRACE(diff_logic_vars, tout << "mk_var: " << v << "\n";);
|
|
m_graph.init_var(v);
|
|
ctx.attach_th_var(n, this, v);
|
|
set_sort(n->get_expr());
|
|
return v;
|
|
}
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::set_sort(expr* n) {
|
|
if (m_util.is_numeral(n))
|
|
return;
|
|
if (m_util.is_int(n)) {
|
|
if (m_lia_or_lra == is_lra) {
|
|
throw default_exception("difference logic does not work with mixed sorts");
|
|
}
|
|
m_lia_or_lra = is_lia;
|
|
}
|
|
else {
|
|
if (m_lia_or_lra == is_lia) {
|
|
throw default_exception("difference logic does not work with mixed sorts");
|
|
}
|
|
m_lia_or_lra = is_lra;
|
|
}
|
|
}
|
|
|
|
|
|
template<typename Ext>
|
|
theory_var theory_diff_logic<Ext>::mk_var(app* n) {
|
|
enode* e = nullptr;
|
|
theory_var v = null_theory_var;
|
|
if (!ctx.e_internalized(n)) {
|
|
ctx.internalize(n, false);
|
|
}
|
|
e = ctx.get_enode(n);
|
|
v = e->get_th_var(get_id());
|
|
|
|
if (v == null_theory_var) {
|
|
v = mk_var(e);
|
|
}
|
|
if (is_interpreted(n)) {
|
|
TRACE(non_diff_logic, tout << "Variable should not be interpreted\n";);
|
|
found_non_diff_logic_expr(n);
|
|
}
|
|
TRACE(arith, tout << mk_pp(n, m) << " |-> " << v << "\n";);
|
|
return v;
|
|
}
|
|
|
|
|
|
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::reset_eh() {
|
|
for (unsigned i = 0; i < m_atoms.size(); ++i) {
|
|
dealloc(m_atoms[i]);
|
|
}
|
|
m_graph .reset();
|
|
m_izero = null_theory_var;
|
|
m_rzero = null_theory_var;
|
|
m_atoms .reset();
|
|
m_asserted_atoms .reset();
|
|
m_stats .reset();
|
|
m_scopes .reset();
|
|
m_asserted_qhead = 0;
|
|
m_num_core_conflicts = 0;
|
|
m_num_propagation_calls = 0;
|
|
m_agility = 0.5;
|
|
m_lia_or_lra = not_set;
|
|
m_non_diff_logic_exprs = false;
|
|
m_objectives .reset();
|
|
m_objective_consts.reset();
|
|
m_objective_assignments.reset();
|
|
theory::reset_eh();
|
|
}
|
|
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::compute_delta() {
|
|
m_delta = rational(1);
|
|
m_graph.set_to_zero(get_zero(true), get_zero(false));
|
|
unsigned num_edges = m_graph.get_num_edges();
|
|
for (unsigned i = 0; i < num_edges; ++i) {
|
|
if (!m_graph.is_enabled(i)) {
|
|
continue;
|
|
}
|
|
numeral w = m_graph.get_weight(i);
|
|
dl_var tgt = m_graph.get_target(i);
|
|
dl_var src = m_graph.get_source(i);
|
|
rational n_x = m_graph.get_assignment(tgt).get_rational().to_rational();
|
|
rational k_x = m_graph.get_assignment(tgt).get_infinitesimal().to_rational();
|
|
rational n_y = m_graph.get_assignment(src).get_rational().to_rational();
|
|
rational k_y = m_graph.get_assignment(src).get_infinitesimal().to_rational();
|
|
rational n_c = w.get_rational().to_rational();
|
|
rational k_c = w.get_infinitesimal().to_rational();
|
|
TRACE(arith, tout << "(n_x,k_x): " << n_x << ", " << k_x << ", (n_y,k_y): "
|
|
<< n_y << ", " << k_y << ", (n_c,k_c): " << n_c << ", " << k_c << "\n";);
|
|
if (n_x < n_y + n_c && k_x > k_y + k_c) {
|
|
rational new_delta = (n_y + n_c - n_x) / (2*(k_x - k_y - k_c));
|
|
if (new_delta < m_delta) {
|
|
TRACE(arith, tout << "new delta: " << new_delta << "\n";);
|
|
m_delta = new_delta;
|
|
}
|
|
}
|
|
}
|
|
}
|
|
|
|
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::init_model(smt::model_generator & m) {
|
|
m_factory = alloc(arith_factory, get_manager());
|
|
m.register_factory(m_factory);
|
|
compute_delta();
|
|
}
|
|
|
|
|
|
template<typename Ext>
|
|
model_value_proc * theory_diff_logic<Ext>::mk_value(enode * n, model_generator & mg) {
|
|
theory_var v = n->get_th_var(get_id());
|
|
SASSERT(v != null_theory_var);
|
|
rational num;
|
|
if (!m_util.is_numeral(n->get_expr(), num)) {
|
|
numeral val = m_graph.get_assignment(v);
|
|
num = val.get_rational().to_rational() + m_delta * val.get_infinitesimal().to_rational();
|
|
}
|
|
TRACE(arith, tout << mk_pp(n->get_expr(), m) << " |-> " << num << "\n";);
|
|
bool is_int = m_util.is_int(n->get_expr());
|
|
if (is_int && !num.is_int())
|
|
throw default_exception("difference logic solver was used on mixed int/real problem");
|
|
return alloc(expr_wrapper_proc, m_factory->mk_num_value(num, is_int));
|
|
}
|
|
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::display(std::ostream & out) const {
|
|
out << "atoms\n";
|
|
for (atom* a : m_atoms) {
|
|
a->display(*this, out) << "\n";
|
|
}
|
|
out << "graph\n";
|
|
m_graph.display(out);
|
|
}
|
|
|
|
template<typename Ext>
|
|
bool theory_diff_logic<Ext>::is_consistent() const {
|
|
DEBUG_CODE(
|
|
for (unsigned i = 0; m_graph.is_feasible_dbg() && i < m_atoms.size(); ++i) {
|
|
atom* a = m_atoms[i];
|
|
bool_var bv = a->get_bool_var();
|
|
lbool asgn = ctx.get_assignment(bv);
|
|
if (ctx.is_relevant(ctx.bool_var2expr(bv)) && asgn != l_undef) {
|
|
SASSERT((asgn == l_true) == a->is_true());
|
|
int edge_id = a->get_asserted_edge();
|
|
SASSERT(m_graph.is_enabled(edge_id));
|
|
SASSERT(m_graph.is_feasible(edge_id));
|
|
}
|
|
});
|
|
return m_consistent;
|
|
}
|
|
|
|
|
|
template<class Ext>
|
|
theory_var theory_diff_logic<Ext>::expand(bool pos, theory_var v, rational & k) {
|
|
enode* e = get_enode(v);
|
|
rational r;
|
|
for (;;) {
|
|
app* n = e->get_expr();
|
|
if (m_util.is_add(n) && n->get_num_args() == 2) {
|
|
app* x = to_app(n->get_arg(0));
|
|
app* y = to_app(n->get_arg(1));
|
|
if (m_util.is_numeral(x, r)) {
|
|
e = ctx.get_enode(y);
|
|
}
|
|
else if (m_util.is_numeral(y, r)) {
|
|
e = ctx.get_enode(x);
|
|
}
|
|
v = e->get_th_var(get_id());
|
|
SASSERT(v != null_theory_var);
|
|
if (v == null_theory_var) {
|
|
break;
|
|
}
|
|
if (pos) {
|
|
k += r;
|
|
}
|
|
else {
|
|
k -= r;
|
|
}
|
|
}
|
|
else {
|
|
break;
|
|
}
|
|
}
|
|
return v;
|
|
}
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::new_eq_or_diseq(bool is_eq, theory_var v1, theory_var v2, justification& eq_just) {
|
|
rational k;
|
|
theory_var s = expand(true, v1, k);
|
|
theory_var t = expand(false, v2, k);
|
|
|
|
if (s == t) {
|
|
if (is_eq != k.is_zero()) {
|
|
// conflict 0 /= k;
|
|
inc_conflicts();
|
|
ctx.set_conflict(&eq_just);
|
|
}
|
|
}
|
|
else {
|
|
//
|
|
// Create equality ast, internalize_atom
|
|
// assign the corresponding equality literal.
|
|
//
|
|
|
|
|
|
app_ref eq(m), s2(m), t2(m);
|
|
app* s1 = get_enode(s)->get_expr();
|
|
app* t1 = get_enode(t)->get_expr();
|
|
s2 = m_util.mk_sub(t1, s1);
|
|
t2 = m_util.mk_numeral(k, s2->get_sort());
|
|
// t1 - s1 = k
|
|
eq = m.mk_eq(s2.get(), t2.get());
|
|
if (m.has_trace_stream()) {
|
|
app_ref body(m);
|
|
body = m.mk_eq(m.mk_eq(m_util.mk_add(s1, t2), t1), eq);
|
|
log_axiom_instantiation(body);
|
|
}
|
|
|
|
TRACE(diff_logic,
|
|
tout << v1 << " .. " << v2 << "\n";
|
|
tout << mk_pp(eq.get(), m) <<"\n";);
|
|
|
|
if (!internalize_atom(eq.get(), false)) {
|
|
UNREACHABLE();
|
|
}
|
|
|
|
if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n";
|
|
|
|
literal l(ctx.get_literal(eq.get()));
|
|
if (!is_eq) {
|
|
l = ~l;
|
|
}
|
|
|
|
ctx.assign(l, b_justification(&eq_just), false);
|
|
}
|
|
}
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::new_eq_eh(
|
|
theory_var v1, theory_var v2, justification& j) {
|
|
m_stats.m_num_core2th_eqs++;
|
|
new_eq_or_diseq(true, v1, v2, j);
|
|
}
|
|
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::new_diseq_eh(
|
|
theory_var v1, theory_var v2, justification& j) {
|
|
m_stats.m_num_core2th_diseqs++;
|
|
new_eq_or_diseq(false, v1, v2, j);
|
|
}
|
|
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::new_eq_eh(theory_var v1, theory_var v2) {
|
|
m_arith_eq_adapter.new_eq_eh(v1, v2);
|
|
}
|
|
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::new_diseq_eh(theory_var v1, theory_var v2) {
|
|
m_arith_eq_adapter.new_diseq_eh(v1, v2);
|
|
}
|
|
|
|
|
|
|
|
struct imp_functor {
|
|
conflict_resolution & m_cr;
|
|
imp_functor(conflict_resolution& cr) : m_cr(cr) {}
|
|
void operator()(literal l) {
|
|
m_cr.mark_literal(l);
|
|
}
|
|
};
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::get_eq_antecedents(
|
|
theory_var v1, theory_var v2, unsigned timestamp, conflict_resolution & cr) {
|
|
imp_functor functor(cr);
|
|
VERIFY(m_graph.find_shortest_zero_edge_path(v1, v2, timestamp, functor));
|
|
VERIFY(m_graph.find_shortest_zero_edge_path(v2, v1, timestamp, functor));
|
|
}
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::get_implied_bound_antecedents(edge_id bridge_edge, edge_id subsumed_edge, conflict_resolution & cr) {
|
|
imp_functor f(cr);
|
|
m_graph.explain_subsumed_lazy(bridge_edge, subsumed_edge, f);
|
|
}
|
|
|
|
template<typename Ext>
|
|
unsigned theory_diff_logic<Ext>::node2simplex(unsigned v) {
|
|
return m_objectives.size() + 2*v + 1;
|
|
}
|
|
template<typename Ext>
|
|
unsigned theory_diff_logic<Ext>::edge2simplex(unsigned e) {
|
|
return m_objectives.size() + 2*e;
|
|
}
|
|
template<typename Ext>
|
|
unsigned theory_diff_logic<Ext>::obj2simplex(unsigned e) {
|
|
return e;
|
|
}
|
|
|
|
template<typename Ext>
|
|
unsigned theory_diff_logic<Ext>::num_simplex_vars() {
|
|
return m_objectives.size() + std::max(2*m_graph.get_num_edges(),2*m_graph.get_num_nodes()+1);
|
|
}
|
|
|
|
template<typename Ext>
|
|
bool theory_diff_logic<Ext>::is_simplex_edge(unsigned e) {
|
|
if (e < m_objectives.size()) return false;
|
|
e -= m_objectives.size();
|
|
return (0 == (e & 0x1));
|
|
}
|
|
|
|
template<typename Ext>
|
|
unsigned theory_diff_logic<Ext>::simplex2edge(unsigned e) {
|
|
SASSERT(is_simplex_edge(e));
|
|
return (e - m_objectives.size())/2;
|
|
}
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
|
|
m_graph.set_to_zero(get_zero(true), get_zero(false));
|
|
unsynch_mpq_inf_manager inf_mgr;
|
|
unsynch_mpq_manager& mgr = inf_mgr.get_mpq_manager();
|
|
unsigned num_nodes = m_graph.get_num_nodes();
|
|
vector<dl_edge<GExt> > const& es = m_graph.get_all_edges();
|
|
S.ensure_var(num_simplex_vars());
|
|
for (unsigned i = 0; i < num_nodes; ++i) {
|
|
numeral const& a = m_graph.get_assignment(i);
|
|
rational fin = a.get_rational().to_rational();
|
|
rational inf = a.get_infinitesimal().to_rational();
|
|
mpq_inf q;
|
|
inf_mgr.set(q, fin.to_mpq(), inf.to_mpq());
|
|
S.set_value(node2simplex(i), q);
|
|
inf_mgr.del(q);
|
|
}
|
|
S.set_lower(node2simplex(get_zero(true)), mpq_inf(mpq(0), mpq(0)));
|
|
S.set_upper(node2simplex(get_zero(true)), mpq_inf(mpq(0), mpq(0)));
|
|
S.set_lower(node2simplex(get_zero(false)), mpq_inf(mpq(0), mpq(0)));
|
|
S.set_upper(node2simplex(get_zero(false)), mpq_inf(mpq(0), mpq(0)));
|
|
svector<unsigned> vars;
|
|
scoped_mpq_vector coeffs(mgr);
|
|
coeffs.push_back(mpq(1));
|
|
coeffs.push_back(mpq(-1));
|
|
coeffs.push_back(mpq(-1));
|
|
vars.resize(3);
|
|
for (unsigned i = m_num_simplex_edges; i < es.size(); ++i) {
|
|
// t - s <= w
|
|
// =>
|
|
// t - s - b = 0, b >= w
|
|
dl_edge<GExt> const& e = es[i];
|
|
unsigned base_var = edge2simplex(i);
|
|
vars[0] = node2simplex(e.get_target());
|
|
vars[1] = node2simplex(e.get_source());
|
|
vars[2] = base_var;
|
|
S.add_row(base_var, 3, vars.data(), coeffs.data());
|
|
}
|
|
m_num_simplex_edges = es.size();
|
|
for (unsigned i = 0; i < es.size(); ++i) {
|
|
dl_edge<GExt> const& e = es[i];
|
|
unsigned base_var = edge2simplex(i);
|
|
if (e.is_enabled()) {
|
|
numeral const& w = e.get_weight();
|
|
rational fin = w.get_rational().to_rational();
|
|
rational inf = w.get_infinitesimal().to_rational();
|
|
mpq_inf q;
|
|
inf_mgr.set(q, fin.to_mpq(), inf.to_mpq());
|
|
S.set_upper(base_var, q);
|
|
inf_mgr.del(q);
|
|
}
|
|
else {
|
|
S.unset_upper(base_var);
|
|
}
|
|
}
|
|
for (unsigned v = m_objective_rows.size(); v < m_objectives.size(); ++v) {
|
|
unsigned w = obj2simplex(v);
|
|
objective_term const& objective = m_objectives[v];
|
|
|
|
// add objective function as row.
|
|
coeffs.reset();
|
|
vars.reset();
|
|
for (auto const& o : objective) {
|
|
coeffs.push_back(o.second.to_mpq());
|
|
vars.push_back(node2simplex(o.first));
|
|
}
|
|
coeffs.push_back(mpq(1));
|
|
vars.push_back(w);
|
|
Simplex::row row = S.add_row(w, vars.size(), vars.data(), coeffs.data());
|
|
m_objective_rows.push_back(row);
|
|
}
|
|
}
|
|
|
|
template<typename Ext>
|
|
typename theory_diff_logic<Ext>::inf_eps theory_diff_logic<Ext>::value(theory_var v) {
|
|
objective_term const& objective = m_objectives[v];
|
|
inf_eps r = inf_eps(m_objective_consts[v]);
|
|
for (auto const& o : objective) {
|
|
numeral n = m_graph.get_assignment(o.first);
|
|
rational r1 = n.get_rational().to_rational();
|
|
rational r2 = n.get_infinitesimal().to_rational();
|
|
r += o.second * inf_eps(rational(0), inf_rational(r1, r2));
|
|
}
|
|
return r;
|
|
}
|
|
|
|
|
|
|
|
template<typename Ext>
|
|
typename theory_diff_logic<Ext>::inf_eps
|
|
theory_diff_logic<Ext>::maximize(theory_var v, expr_ref& blocker, bool& has_shared) {
|
|
SASSERT(is_consistent());
|
|
|
|
has_shared = false;
|
|
Simplex& S = m_S;
|
|
|
|
CTRACE(arith,!m_graph.is_feasible_dbg(), m_graph.display(tout););
|
|
SASSERT(m_graph.is_feasible_dbg());
|
|
|
|
update_simplex(S);
|
|
|
|
TRACE(arith,
|
|
objective_term const& objective = m_objectives[v];
|
|
for (auto const& o : objective) {
|
|
tout << "Coefficient " << o.second
|
|
<< " of theory_var " << o.first << "\n";
|
|
}
|
|
tout << "Free coefficient " << m_objective_consts[v] << "\n";
|
|
);
|
|
|
|
TRACE(opt,
|
|
S.display(tout);
|
|
for (unsigned i = 0; i < m_graph.get_num_nodes(); ++i)
|
|
tout << "$" << i << ": " << node2simplex(i) << "\n";
|
|
display(tout);
|
|
);
|
|
|
|
// optimize
|
|
lbool is_sat = S.make_feasible();
|
|
if (is_sat == l_undef) {
|
|
blocker = m.mk_false();
|
|
return inf_eps::infinity();
|
|
}
|
|
TRACE(opt, S.display(tout); );
|
|
SASSERT(is_sat != l_false);
|
|
unsigned w = obj2simplex(v);
|
|
lbool is_fin = S.minimize(w);
|
|
switch (is_fin) {
|
|
case l_true: {
|
|
simplex::mpq_ext::eps_numeral const& val = S.get_value(w);
|
|
inf_rational r(-rational(val.first), -rational(val.second));
|
|
Simplex::row row = m_objective_rows[v];
|
|
Simplex::row_iterator it = S.row_begin(row), end = S.row_end(row);
|
|
expr_ref_vector& core = m_objective_assignments[v];
|
|
expr_ref tmp(m);
|
|
core.reset();
|
|
for (; it != end; ++it) {
|
|
unsigned v = it->var();
|
|
if (is_simplex_edge(v)) {
|
|
unsigned edge_id = simplex2edge(v);
|
|
literal lit = m_graph.get_explanation(edge_id);
|
|
if (lit != null_literal) {
|
|
ctx.literal2expr(lit, tmp);
|
|
core.push_back(tmp);
|
|
}
|
|
}
|
|
}
|
|
ensure_rational_solution(S);
|
|
TRACE(opt, tout << r << " " << "\n";
|
|
S.display_row(tout, row, true);
|
|
S.display(tout);
|
|
);
|
|
|
|
for (unsigned i = 0; i < m_graph.get_num_nodes(); ++i) {
|
|
unsigned w = node2simplex(i);
|
|
auto const& val = S.get_value(w);
|
|
SASSERT(rational(val.second).is_zero());
|
|
rational r = rational(val.first);
|
|
m_graph.set_assignment(i, numeral(r));
|
|
}
|
|
CTRACE(arith,!m_graph.is_feasible_dbg(), m_graph.display(tout););
|
|
SASSERT(m_graph.is_feasible_dbg());
|
|
inf_eps r1(rational(0), r);
|
|
blocker = mk_gt(v, r1);
|
|
return inf_eps(rational(0), r + m_objective_consts[v]);
|
|
}
|
|
default:
|
|
TRACE(opt, tout << "unbounded\n"; );
|
|
blocker = m.mk_false();
|
|
return inf_eps::infinity();
|
|
}
|
|
}
|
|
|
|
template<typename Ext>
|
|
theory_var theory_diff_logic<Ext>::add_objective(app* term) {
|
|
objective_term objective;
|
|
theory_var result = m_objectives.size();
|
|
rational q(1), r(0);
|
|
expr_ref_vector vr(m);
|
|
if (!is_linear(m, term)) {
|
|
result = null_theory_var;
|
|
}
|
|
else if (internalize_objective(term, q, r, objective)) {
|
|
m_objectives.push_back(objective);
|
|
m_objective_consts.push_back(r);
|
|
m_objective_assignments.push_back(vr);
|
|
}
|
|
else {
|
|
result = null_theory_var;
|
|
}
|
|
return result;
|
|
}
|
|
|
|
template<typename Ext>
|
|
expr_ref theory_diff_logic<Ext>::mk_ineq(theory_var v, inf_eps const& val, bool is_strict) {
|
|
objective_term const& t = m_objectives[v];
|
|
expr_ref e(m), f(m), f2(m);
|
|
if (t.size() == 1 && t[0].second.is_one()) {
|
|
f = get_enode(t[0].first)->get_expr();
|
|
}
|
|
else if (t.size() == 1 && t[0].second.is_minus_one()) {
|
|
f = m_util.mk_uminus(get_enode(t[0].first)->get_expr());
|
|
}
|
|
else if (t.size() == 2 && t[0].second.is_one() && t[1].second.is_minus_one()) {
|
|
f = get_enode(t[0].first)->get_expr();
|
|
f2 = get_enode(t[1].first)->get_expr();
|
|
f = m_util.mk_sub(f, f2);
|
|
}
|
|
else if (t.size() == 2 && t[1].second.is_one() && t[0].second.is_minus_one()) {
|
|
f = get_enode(t[1].first)->get_expr();
|
|
f2 = get_enode(t[0].first)->get_expr();
|
|
f = m_util.mk_sub(f, f2);
|
|
}
|
|
else {
|
|
//
|
|
expr_ref_vector const& core = m_objective_assignments[v];
|
|
f = m.mk_and(core.size(), core.data());
|
|
if (is_strict) {
|
|
f = m.mk_not(f);
|
|
}
|
|
return f;
|
|
}
|
|
|
|
inf_eps new_val = val; // - inf_rational(m_objective_consts[v]);
|
|
e = m_util.mk_numeral(new_val.get_rational(), f->get_sort());
|
|
|
|
if (new_val.get_infinitesimal().is_neg()) {
|
|
if (is_strict) {
|
|
f = m_util.mk_ge(f, e);
|
|
}
|
|
else {
|
|
expr_ref_vector const& core = m_objective_assignments[v];
|
|
f = m.mk_and(core.size(), core.data());
|
|
}
|
|
}
|
|
else {
|
|
if (is_strict) {
|
|
f = m_util.mk_gt(f, e);
|
|
}
|
|
else {
|
|
f = m_util.mk_ge(f, e);
|
|
}
|
|
}
|
|
return f;
|
|
}
|
|
|
|
template<typename Ext>
|
|
expr_ref theory_diff_logic<Ext>::mk_gt(theory_var v, inf_eps const& val) {
|
|
return mk_ineq(v, val, true);
|
|
}
|
|
|
|
template<typename Ext>
|
|
expr_ref theory_diff_logic<Ext>::mk_ge(generic_model_converter& fm, theory_var v, inf_eps const& val) {
|
|
return mk_ineq(v, val, false);
|
|
}
|
|
|
|
#if 0
|
|
model_ref mdl;
|
|
ctx.get_model(mdl);
|
|
ptr_vector<expr> formulas(ctx.get_num_asserted_formulas(), ctx.get_asserted_formulas());
|
|
model_implicant impl_extractor(m);
|
|
expr_ref_vector implicants = impl_extractor.minimize_literals(formulas, mdl);
|
|
return m.mk_and(o, m.mk_not(m.mk_and(implicants.size(), implicants.c_ptr())));
|
|
#endif
|
|
|
|
template<typename Ext>
|
|
bool theory_diff_logic<Ext>::internalize_objective(expr * n, rational const& m, rational& q, objective_term & objective) {
|
|
|
|
// Compile term into objective_term format
|
|
rational r;
|
|
expr* x, *y;
|
|
if (m_util.is_numeral(n, r)) {
|
|
q += r;
|
|
}
|
|
else if (m_util.is_add(n)) {
|
|
for (unsigned i = 0; i < to_app(n)->get_num_args(); ++i) {
|
|
if (!internalize_objective(to_app(n)->get_arg(i), m, q, objective)) {
|
|
return false;
|
|
}
|
|
}
|
|
}
|
|
else if (m_util.is_mul(n, x, y) && m_util.is_numeral(x, r)) {
|
|
return internalize_objective(y, m*r, q, objective);
|
|
}
|
|
else if (m_util.is_mul(n, y, x) && m_util.is_numeral(x, r)) {
|
|
return internalize_objective(y, m*r, q, objective);
|
|
}
|
|
else if (!is_app(n)) {
|
|
return false;
|
|
}
|
|
else if (to_app(n)->get_family_id() == m_util.get_family_id()) {
|
|
return false;
|
|
}
|
|
else {
|
|
theory_var v = mk_var(to_app(n));
|
|
objective.push_back(std::make_pair(v, m));
|
|
}
|
|
return true;
|
|
}
|
|
|
|
template<typename Ext>
|
|
theory* theory_diff_logic<Ext>::mk_fresh(context* new_ctx) {
|
|
return alloc(theory_diff_logic<Ext>, *new_ctx);
|
|
}
|
|
|
|
template<typename Ext>
|
|
void theory_diff_logic<Ext>::init_zero() {
|
|
if (m_izero != null_theory_var) return;
|
|
TRACE(arith, tout << "init zero\n";);
|
|
app* zero;
|
|
enode* e;
|
|
zero = m_util.mk_numeral(rational(0), true);
|
|
e = ctx.mk_enode(zero, false, false, true);
|
|
SASSERT(!is_attached_to_var(e));
|
|
m_izero = mk_var(e);
|
|
|
|
zero = m_util.mk_numeral(rational(0), false);
|
|
e = ctx.mk_enode(zero, false, false, true);
|
|
SASSERT(!is_attached_to_var(e));
|
|
m_rzero = mk_var(e);
|
|
}
|
|
|
|
|