Skip to content

Commit

Permalink
use value function in lar_solver (#4771)
Browse files Browse the repository at this point in the history 
* use value function in lar_solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add missing return

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* check_feasible is called after column is added for fixed variable

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Nov 3, 2020
1 parent 5335097 commit 620204b
Show file tree
Hide file tree
Showing 7 changed files with 41 additions and 110 deletions.
12 changes: 5 additions & 7 deletions src/math/lp/lar_solver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,6 @@ namespace lp {
lp_assert(false); // not implemented
}


lar_solver::lar_solver() :
m_status(lp_status::UNKNOWN),
m_crossed_bounds_column(-1),
Expand All @@ -37,7 +36,6 @@ namespace lp {
return m_mpq_lar_core_solver.m_r_solver.m_pivoted_rows != nullptr;
}


lar_solver::~lar_solver() {

for (auto t : m_terms)
Expand Down Expand Up @@ -415,9 +413,8 @@ namespace lp {
at_l ? lcs.m_r_upper_bounds()[j] : lcs.m_r_lower_bounds()[j]);
return true;
}
}

break;
break;
}
case column_type::lower_bound:
if (val != lcs.m_r_lower_bounds()[j]) {
set_value_for_nbasic_column(j, lcs.m_r_lower_bounds()[j]);
Expand Down Expand Up @@ -1174,13 +1171,14 @@ namespace lp {

mpq lar_solver::get_value(column_index const& j) const {
SASSERT(get_status() == lp_status::OPTIMAL || get_status() == lp_status::FEASIBLE);
SASSERT(m_columns_with_changed_bounds.empty());
numeric_pair<mpq> const& rp = get_column_value(j);
return rp.x + m_delta * rp.y;
}

mpq lar_solver::get_value(tv const& t) const {
if (t.is_var())
get_value(t.column());
return get_value(t.column());
mpq r(0);
for (const auto& p : get_term(t))
r += p.coeff() * get_value(p.column());
Expand All @@ -1189,7 +1187,7 @@ namespace lp {

impq lar_solver::get_ivalue(tv const& t) const {
if (t.is_var())
get_ivalue(t.column());
return get_ivalue(t.column());
impq r;
for (const auto& p : get_term(t))
r += p.coeff() * get_ivalue(p.column());
Expand Down
1 change: 1 addition & 0 deletions src/sat/smt/arith_internalize.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -615,6 +615,7 @@ namespace arith {
add_def_constraint(ci);
if (vi_equal != lp::null_lpvar)
report_equality_of_fixed_vars(vi, vi_equal);
m_new_eq = true;
}

bool solver::reflect(expr* n) const {
Expand Down
4 changes: 1 addition & 3 deletions src/sat/smt/arith_solver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -798,9 +798,7 @@ namespace arith {
}

rational solver::get_value(theory_var v) const {
if (v == euf::null_theory_var || !lp().external_is_used(v))
return rational::zero();
return m_solver->get_value(get_tv(v));
return is_registered_var(v) ? m_solver->get_value(get_tv(v)) : rational::zero();
}

void solver::random_update() {
Expand Down
1 change: 1 addition & 0 deletions src/sat/smt/bv_internalize.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -232,6 +232,7 @@ namespace bv {
expr_ref b2b(bv.mk_bit2bool(e, i), m);
m_bits[v].push_back(sat::null_literal);
sat::literal lit = ctx.internalize(b2b, false, false, m_is_redundant);
(void)lit;
TRACE("bv", tout << "add-bit: " << lit << " " << literal2expr(lit) << "\n";);
SASSERT(m_bits[v].back() == lit);
}
Expand Down
3 changes: 1 addition & 2 deletions src/sat/smt/euf_model.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,6 @@ namespace euf {
}

class solver::user_sort {
solver& s;
ast_manager& m;
model_ref& mdl;
expr_ref_vector& values;
Expand All @@ -76,7 +75,7 @@ namespace euf {
obj_map<sort, expr_ref_vector*> sort2values;
public:
user_sort(solver& s, expr_ref_vector& values, model_ref& mdl):
s(s), m(s.m), mdl(mdl), values(values), factory(m) {}
m(s.m), mdl(mdl), values(values), factory(m) {}

~user_sort() {
for (auto kv : sort2values)
Expand Down
1 change: 0 additions & 1 deletion src/sat/smt/user_solver.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,6 @@ namespace user {
vector<prop_info> m_prop;
unsigned_vector m_prop_lim;
vector<sat::literal_vector> m_id2justification;
unsigned m_num_scopes { 0 };
sat::literal_vector m_lits;
euf::enode_pair_vector m_eqs;
stats m_stats;
Expand Down
129 changes: 32 additions & 97 deletions src/smt/theory_lra.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -144,7 +144,6 @@ class theory_lra::imp {
typedef vector<std::pair<rational, lpvar>> var_coeffs;

var_coeffs m_left_side; // constraint left side
mutable std::unordered_map<lpvar, rational> m_variable_values; // current model
lpvar m_one_var;
lpvar m_zero_var;
lpvar m_rone_var;
Expand Down Expand Up @@ -689,7 +688,7 @@ class theory_lra::imp {
if (vi_equal != lp::null_lpvar) {
report_equality_of_fixed_vars(vi, vi_equal);
}
m_new_def = true;
}

void internalize_eq(theory_var v1, theory_var v2) {
Expand Down Expand Up @@ -867,7 +866,7 @@ class theory_lra::imp {
void init() {
if (m_solver) return;

reset_variable_values();
m_model_is_initialized = false;
m_solver = alloc(lp::lar_solver);
// initialize 0, 1 variables:
get_one(true);
Expand Down Expand Up @@ -1393,17 +1392,13 @@ class theory_lra::imp {
}

bool can_get_value(theory_var v) const {
return can_get_bound(v) && !m_variable_values.empty();
return is_registered_var(v) && m_model_is_initialized;
}

bool can_get_bound(theory_var v) const {
bool is_registered_var(theory_var v) const {
return v != null_theory_var && lp().external_is_used(v);
}

bool can_get_ivalue(theory_var v) const {
return can_get_bound(v);
}

void ensure_column(theory_var v) {
if (!lp().external_is_used(v)) {
register_theory_var_in_lar_solver(v);
Expand All @@ -1413,87 +1408,24 @@ class theory_lra::imp {
mutable vector<std::pair<lp::tv, rational>> m_todo_terms;

lp::impq get_ivalue(theory_var v) const {
SASSERT(can_get_ivalue(v));
auto t = get_tv(v);
if (!t.is_term())
return lp().get_column_value(t.id());
m_todo_terms.push_back(std::make_pair(t, rational::one()));
lp::impq result(0);
while (!m_todo_terms.empty()) {
t = m_todo_terms.back().first;
rational coeff = m_todo_terms.back().second;
m_todo_terms.pop_back();
if (t.is_term()) {
const lp::lar_term& term = lp().get_term(t);
for (const auto & i: term) {
m_todo_terms.push_back(std::make_pair(lp().column2tv(i.column()), coeff * i.coeff()));
}
}
else {
result += lp().get_column_value(t.id()) * coeff;
}
}
return result;
SASSERT(is_registered_var(v));
return lp().get_ivalue(get_tv(v));
}

rational get_value(theory_var v) const {
TRACE("arith", tout << "get_value v" << v << "\n";);
if (v == null_theory_var || !lp().external_is_used(v)) {
return rational::zero();
}

auto t = get_tv(v);
auto E = m_variable_values.end();
auto I = m_variable_values.find(t.index());
if (I != E)
return I->second;

if (!t.is_term() && lp().is_fixed(t.id()))
return lp().column_lower_bound(t.id()).x;
if (!t.is_term())
return rational::zero();

m_todo_terms.push_back(std::make_pair(t, rational::one()));
rational result(0);
while (!m_todo_terms.empty()) {
auto t2 = m_todo_terms.back().first;
rational coeff = m_todo_terms.back().second;
m_todo_terms.pop_back();
if (t2.is_term()) {
const lp::lar_term& term = lp().get_term(t2);
for (const auto & i : term) {
auto tv = lp().column2tv(i.column());
auto I = m_variable_values.find(tv.index());
if (I != E) {
result += I->second * coeff * i.coeff();
}
else {
m_todo_terms.push_back(std::make_pair(tv, coeff * i.coeff()));
}
}
}
else {
auto I = m_variable_values.find(t2.index());
std::cout << (I == E) << "\n";
if (I != E)
result += I->second * coeff;
}
}
m_variable_values.emplace(t.index(), result);
return result;
return is_registered_var(v) ? lp().get_value(get_tv(v)) : rational::zero();
}

bool m_model_is_initialized{ false };

void init_variable_values() {
reset_variable_values();
if (m.inc() && m_solver.get() && th.get_num_vars() > 0) {
lp().get_model(m_variable_values);
TRACE("arith", display(tout << "update variable values " << m_variable_values.size() << "\n"););
m_model_is_initialized = false;
if (m.inc() && m_solver.get() && th.get_num_vars() > 0) {
ctx().push_trail(value_trail<smt::context, bool>(m_model_is_initialized));
m_model_is_initialized = lp().init_model();
TRACE("arith", display(tout << "update variable values " << m_model_is_initialized << "\n"););
}
}

void reset_variable_values() {
m_variable_values.clear();
}

void random_update() {
if (m_nla)
Expand Down Expand Up @@ -1556,7 +1488,7 @@ class theory_lra::imp {
continue;
}
ensure_column(v);
if (!can_get_ivalue(v))
if (!is_registered_var(v))
continue;
theory_var other = m_model_eqs.insert_if_not_there(v);
TRACE("arith", tout << "insert: v" << v << " := " << get_value(v) << " found: v" << other << "\n";);
Expand Down Expand Up @@ -1616,13 +1548,15 @@ class theory_lra::imp {
}

final_check_status final_check_eh() {
reset_variable_values();
m_model_is_initialized = false;
IF_VERBOSE(12, verbose_stream() << "final-check " << lp().get_status() << "\n");
lbool is_sat = l_true;
SASSERT(lp().ax_is_correct());
if (lp().get_status() != lp::lp_status::OPTIMAL || lp().has_changed_columns()) {
if (lp().get_status() != lp::lp_status::OPTIMAL) { // || lp().has_changed_columns()) {
is_sat = make_feasible();
}
else
SASSERT(!lp().has_changed_columns());
final_check_status st = FC_DONE;

switch (is_sat) {
Expand Down Expand Up @@ -1790,7 +1724,7 @@ class theory_lra::imp {
theory_var v = mk_var(n);
theory_var v1 = mk_var(p);

if (!can_get_ivalue(v1))
if (!is_registered_var(v1))
continue;
lp::impq r1 = get_ivalue(v1);
rational r2;
Expand All @@ -1810,7 +1744,7 @@ class theory_lra::imp {
TRACE("arith", tout << "unbounded " << expr_ref(n, m) << "\n";);
continue;
}
if (!can_get_ivalue(v))
if (!is_registered_var(v))
continue;
lp::impq val_v = get_ivalue(v);
if (val_v.y.is_zero() && val_v.x == div(r1.x, r2)) continue;
Expand Down Expand Up @@ -2148,15 +2082,18 @@ class theory_lra::imp {
return false;
}

bool m_new_def{ false };

bool can_propagate() {
return m_asserted_atoms.size() > m_asserted_qhead;
return m_asserted_atoms.size() > m_asserted_qhead || m_new_def;
}

void propagate() {
flush_bound_axioms();
if (!can_propagate()) {
return;
}
m_new_def = false;
while (m_asserted_qhead < m_asserted_atoms.size() && !ctx().inconsistent() && m.inc()) {
bool_var bv = m_asserted_atoms[m_asserted_qhead].m_bv;
bool is_true = m_asserted_atoms[m_asserted_qhead].m_is_true;
Expand Down Expand Up @@ -3279,7 +3216,7 @@ class theory_lra::imp {
m_scopes.reset();
m_stats.reset();
m_to_check.reset();
reset_variable_values();
m_model_is_initialized = false;
}

void init_model(model_generator & mg) {
Expand Down Expand Up @@ -3351,7 +3288,7 @@ class theory_lra::imp {

bool get_value(enode* n, rational& val) {
theory_var v = n->get_th_var(get_id());
if (!can_get_bound(v)) return false;
if (!is_registered_var(v)) return false;
lpvar vi = get_lpvar(v);
if (lp().has_value(vi, val)) {
TRACE("arith", tout << expr_ref(n->get_owner(), m) << " := " << val << "\n";);
Expand Down Expand Up @@ -3385,10 +3322,8 @@ class theory_lra::imp {

bool get_lower(enode* n, rational& val, bool& is_strict) {
theory_var v = n->get_th_var(get_id());
if (!can_get_bound(v)) {
TRACE("arith", tout << "cannot get lower for " << v << "\n";);
return false;
}
if (!is_registered_var(v))
return false;
lpvar vi = get_lpvar(v);
lp::constraint_index ci;
return lp().has_lower_bound(vi, ci, val, is_strict);
Expand All @@ -3406,7 +3341,7 @@ class theory_lra::imp {

bool get_upper(enode* n, rational& val, bool& is_strict) {
theory_var v = n->get_th_var(get_id());
if (!can_get_bound(v))
if (!is_registered_var(v))
return false;
lpvar vi = get_lpvar(v);
lp::constraint_index ci;
Expand Down Expand Up @@ -3509,7 +3444,7 @@ class theory_lra::imp {
if (has_int()) {
lp().backup_x();
}
if (!can_get_bound(v)) {
if (!is_registered_var(v)) {
TRACE("arith", tout << "cannot get bound for v" << v << "\n";);
st = lp::lp_status::UNBOUNDED;
}
Expand Down Expand Up @@ -3727,7 +3662,7 @@ class theory_lra::imp {
if (!ctx().is_relevant(get_enode(v))) out << "irr: ";
out << "v" << v << " ";
if (t.is_null()) out << "null"; else out << (t.is_term() ? "t":"j") << vi;
if (use_nra_model() && can_get_ivalue(v)) m_nla->am().display(out << " = ", nl_value(v, *m_a1));
if (use_nra_model() && is_registered_var(v)) m_nla->am().display(out << " = ", nl_value(v, *m_a1));
else if (can_get_value(v)) out << " = " << get_value(v);
if (is_int(v)) out << ", int";
if (ctx().is_shared(get_enode(v))) out << ", shared";
Expand Down

0 comments on commit 620204b

Please sign in to comment.