mirror of
https://github.com/Z3Prover/z3
synced 2025-10-07 08:21:56 +00:00
Dev (#63)
* introduce int_solver.h Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * add int_solver class Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * track which var is an integer Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add queries for integrality of vars Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * resurrect lp_tst in its own director lp Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add file Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add_constraint has got a body Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * fix add_constraint and substitute_terms_in_linear_expression Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * after merge with Z3Prover Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * adding stub check_int_feasibility() Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Dev (#50) * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * small fix in lar_solver.cpp Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * adding some content to the new check_int_feasibility() Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Dev (#51) * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding more nlsat Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * nlsat integration Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding constraints Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add missing initialization Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * test Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * Dev (#53) * change in a comment Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Disabled debug output * removing FOCI2 interface from interp * remove foci reference from cmakelist.txt Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding more nlsat Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * nlsat integration Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding constraints Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add missing initialization Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * debugging nra Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * updates to nra_solver integration to call it directly from theory_lra instead of over lar_solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * n/a Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * integrate nlsat Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * tidy Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * preserve is_int flag Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * remove a debug printout Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Dev (#54) * change in a comment Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * Disabled debug output * removing FOCI2 interface from interp * remove foci reference from cmakelist.txt Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * initial skeletons for nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding more nlsat Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * nlsat integration Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding constraints Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add missing initialization Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding nra Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * debugging nra Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * updates to nra_solver integration to call it directly from theory_lra instead of over lar_solver Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * n/a Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * integrate nlsat Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * tidy Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * use integer test from lra solver, updated it to work on term variables Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix equality check in assume-eq Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix model_is_int_feasible Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * untested gcd_test() Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * call fill_explanation_from_fixed_columns() Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add the call to pivot_fixed_vars_from_basis() to int_solver.cpp::check() Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * port more of theory_arith_int.h Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * use statistics of lar_solver by theory_lra.cpp Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * port more code to int_solver.cpp Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add an assert Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * more int porting Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * fix a bug in pivot_fixed_vars_from_basis Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * small change Signed-off-by: Lev Nachmanson <levnach@hotmail.com> * implement find_inf_int_base_column() Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * catch unregistered vars in add_var_bound Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add a file Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * compile for vs2012 Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * fix asserts in add_var_bound Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * fix the lp_solver init when workig on an mps file Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * towards int_solver::check() Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * change in int_solver::check() signature Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add handlers for lia moves Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * spacing Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * return branch from int_solver::check() Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * add a stub for mk_gomory_cut Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * Dev (#59) * add handlers for lia moves Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * spacing Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Dev (#60) * add handlers for lia moves Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * spacing Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Dev (#61) * add handlers for lia moves Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * spacing Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * more TRACE(arith_int) Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * fix the build Signed-off-by: Lev Nachmanson <levnach@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Dev (#62) * add handlers for lia moves Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * spacing Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * loops Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * build fix Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
Lev Nachmanson
parent
a28a8304b7
commit
4c23527974
5 changed files with 291 additions and 57 deletions
|
|
@ -201,10 +201,12 @@ namespace smt {
|
|||
SASSERT(is_int(v));
|
||||
SASSERT(!get_value(v).is_int());
|
||||
m_stats.m_branches++;
|
||||
TRACE("arith_int", tout << "branching v" << v << " = " << get_value(v) << "\n";
|
||||
display_var(tout, v););
|
||||
numeral k = ceil(get_value(v));
|
||||
rational _k = k.to_rational();
|
||||
TRACE("arith_int", tout << "branching v" << v << " = " << get_value(v) << "\n";
|
||||
display_var(tout, v);
|
||||
tout << "k = " << k << ", _k = "<< _k << std::endl;
|
||||
);
|
||||
expr_ref bound(get_manager());
|
||||
expr* e = get_enode(v)->get_owner();
|
||||
bound = m_util.mk_ge(e, m_util.mk_numeral(_k, m_util.is_int(e)));
|
||||
|
|
|
|||
|
|
@ -54,13 +54,15 @@ namespace lp {
|
|||
class bound {
|
||||
smt::bool_var m_bv;
|
||||
smt::theory_var m_var;
|
||||
bool m_is_int;
|
||||
rational m_value;
|
||||
bound_kind m_bound_kind;
|
||||
|
||||
public:
|
||||
bound(smt::bool_var bv, smt::theory_var v, rational const & val, bound_kind k):
|
||||
bound(smt::bool_var bv, smt::theory_var v, bool is_int, rational const & val, bound_kind k):
|
||||
m_bv(bv),
|
||||
m_var(v),
|
||||
m_is_int(is_int),
|
||||
m_value(val),
|
||||
m_bound_kind(k) {
|
||||
}
|
||||
|
|
@ -68,11 +70,18 @@ namespace lp {
|
|||
smt::theory_var get_var() const { return m_var; }
|
||||
smt::bool_var get_bv() const { return m_bv; }
|
||||
bound_kind get_bound_kind() const { return m_bound_kind; }
|
||||
bool is_int() const { return m_is_int; }
|
||||
rational const& get_value() const { return m_value; }
|
||||
inf_rational get_value(bool is_true) const {
|
||||
if (is_true) return inf_rational(m_value); // v >= value or v <= value
|
||||
if (m_bound_kind == lower_t) return inf_rational(m_value, false); // v <= value - epsilon
|
||||
return inf_rational(m_value, true); // v >= value + epsilon
|
||||
if (m_is_int) {
|
||||
if (m_bound_kind == lower_t) return inf_rational(m_value - rational::one()); // v <= value - 1
|
||||
return inf_rational(m_value + rational::one()); // v >= value + 1
|
||||
}
|
||||
else {
|
||||
if (m_bound_kind == lower_t) return inf_rational(m_value, false); // v <= value - epsilon
|
||||
return inf_rational(m_value, true); // v >= value + epsilon
|
||||
}
|
||||
}
|
||||
virtual std::ostream& display(std::ostream& out) const {
|
||||
return out << "v" << get_var() << " " << get_bound_kind() << " " << m_value;
|
||||
|
|
@ -305,7 +314,6 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
void found_not_handled(expr* n) {
|
||||
m_not_handled = n;
|
||||
if (is_app(n) && is_underspecified(to_app(n))) {
|
||||
|
|
@ -756,7 +764,7 @@ namespace smt {
|
|||
found_not_handled(atom);
|
||||
return true;
|
||||
}
|
||||
lp::bound* b = alloc(lp::bound, bv, v, r, k);
|
||||
lp::bound* b = alloc(lp::bound, bv, v, is_int(v), r, k);
|
||||
m_bounds[v].push_back(b);
|
||||
updt_unassigned_bounds(v, +1);
|
||||
m_bounds_trail.push_back(v);
|
||||
|
|
@ -1211,33 +1219,49 @@ namespace smt {
|
|||
return FC_GIVEUP;
|
||||
}
|
||||
|
||||
// create a bound atom representing term >= k
|
||||
lp::bound* mk_bound(lean::lar_term const& term, rational const& k) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
lp::bound_kind bkind = lp::bound_kind::lower_t;
|
||||
bool_var bv = null_bool_var;
|
||||
theory_var v = null_theory_var;
|
||||
lp::bound* result = alloc(lp::bound, bv, v, k, bkind);
|
||||
return result;
|
||||
// create a bound atom representing term <= k
|
||||
app_ref mk_bound(lean::lar_term const& term, rational const& k) {
|
||||
SASSERT(k.is_int());
|
||||
app_ref t = mk_term(term, true);
|
||||
app_ref atom(a.mk_le(t, a.mk_numeral(k, true)), m);
|
||||
TRACE("arith", tout << atom << "\n";
|
||||
m_solver->print_term(term, tout << "bound atom: "); tout << " <= " << k << "\n";
|
||||
display(tout);
|
||||
);
|
||||
ctx().internalize(atom, true);
|
||||
ctx().mark_as_relevant(atom.get());
|
||||
return atom;
|
||||
}
|
||||
|
||||
lbool check_lia() {
|
||||
std::cout << "called check_lia()\n";
|
||||
if (m.canceled()) return l_undef;
|
||||
lean::lar_term term;
|
||||
lean::mpq k;
|
||||
lean::explanation ex; // TBD, this should be streamlined accross different explanations
|
||||
switch(m_lia->check(term, k, ex)) {
|
||||
case lean::lia_move::ok:
|
||||
return l_true;
|
||||
case lean::lia_move::branch:
|
||||
case lean::lia_move::branch: {
|
||||
(void)mk_bound(term, k);
|
||||
// branch on term <= k
|
||||
NOT_IMPLEMENTED_YET();
|
||||
// at this point we have a new unassigned atom that the
|
||||
// SAT core assigns a value to
|
||||
return l_false;
|
||||
case lean::lia_move::cut:
|
||||
}
|
||||
case lean::lia_move::cut: {
|
||||
// m_explanation implies term <= k
|
||||
m_explanation = ex.m_explanation;
|
||||
NOT_IMPLEMENTED_YET();
|
||||
app_ref b = mk_bound(term, k);
|
||||
m_eqs.reset();
|
||||
m_core.reset();
|
||||
m_params.reset();
|
||||
for (auto const& ev : ex.m_explanation) {
|
||||
if (!ev.first.is_zero()) {
|
||||
set_evidence(ev.second);
|
||||
}
|
||||
}
|
||||
assign(literal(ctx().get_bool_var(b), false));
|
||||
return l_false;
|
||||
}
|
||||
case lean::lia_move::conflict:
|
||||
// ex contains unsat core
|
||||
m_explanation = ex.m_explanation;
|
||||
|
|
@ -2030,12 +2054,13 @@ namespace smt {
|
|||
st.coeffs().push_back(rational::one());
|
||||
init_left_side(st);
|
||||
lean::lconstraint_kind k = lean::EQ;
|
||||
bool is_int = b.is_int();
|
||||
switch (b.get_bound_kind()) {
|
||||
case lp::lower_t:
|
||||
k = is_true ? lean::GE : lean::LT;
|
||||
k = is_true ? lean::GE : (is_int ? lean::LE : lean::LT);
|
||||
break;
|
||||
case lp::upper_t:
|
||||
k = is_true ? lean::LE : lean::GT;
|
||||
k = is_true ? lean::LE : (is_int ? lean::GE : lean::GT);
|
||||
break;
|
||||
}
|
||||
if (k == lean::LT || k == lean::LE) {
|
||||
|
|
@ -2045,7 +2070,15 @@ namespace smt {
|
|||
++m_stats.m_assert_upper;
|
||||
}
|
||||
auto vi = get_var_index(b.get_var());
|
||||
auto ci = m_solver->add_var_bound(vi, k, b.get_value());
|
||||
rational bound = b.get_value();
|
||||
lean::constraint_index ci;
|
||||
if (is_int && !is_true) {
|
||||
rational bound = b.get_value(false).get_rational();
|
||||
ci = m_solver->add_var_bound(vi, k, bound);
|
||||
}
|
||||
else {
|
||||
ci = m_solver->add_var_bound(vi, k, b.get_value());
|
||||
}
|
||||
TRACE("arith", tout << "v" << b.get_var() << "\n";);
|
||||
add_ineq_constraint(ci, literal(bv, !is_true));
|
||||
|
||||
|
|
@ -2499,19 +2532,32 @@ namespace smt {
|
|||
return internalize_def(term);
|
||||
}
|
||||
|
||||
app_ref mk_term(lean::lar_term const& term, bool is_int) {
|
||||
expr_ref_vector args(m);
|
||||
for (auto & ti : term.m_coeffs) {
|
||||
theory_var w = m_var_index2theory_var[ti.first];
|
||||
expr* o = get_enode(w)->get_owner();
|
||||
if (ti.second.is_one()) {
|
||||
args.push_back(o);
|
||||
}
|
||||
else {
|
||||
args.push_back(a.mk_mul(a.mk_numeral(ti.second, is_int), o));
|
||||
}
|
||||
}
|
||||
if (!term.m_v.is_zero()) {
|
||||
args.push_back(a.mk_numeral(term.m_v, is_int));
|
||||
}
|
||||
if (args.size() == 1) {
|
||||
return app_ref(to_app(args[0].get()), m);
|
||||
}
|
||||
return app_ref(a.mk_add(args.size(), args.c_ptr()), m);
|
||||
}
|
||||
|
||||
app_ref mk_obj(theory_var v) {
|
||||
lean::var_index vi = m_theory_var2var_index[v];
|
||||
bool is_int = a.is_int(get_enode(v)->get_owner());
|
||||
if (m_solver->is_term(vi)) {
|
||||
expr_ref_vector args(m);
|
||||
const lean::lar_term& term = m_solver->get_term(vi);
|
||||
for (auto & ti : term.m_coeffs) {
|
||||
theory_var w = m_var_index2theory_var[ti.first];
|
||||
expr* o = get_enode(w)->get_owner();
|
||||
args.push_back(a.mk_mul(a.mk_numeral(ti.second, is_int), o));
|
||||
}
|
||||
args.push_back(a.mk_numeral(term.m_v, is_int));
|
||||
return app_ref(a.mk_add(args.size(), args.c_ptr()), m);
|
||||
if (m_solver->is_term(vi)) {
|
||||
return mk_term(m_solver->get_term(vi), is_int);
|
||||
}
|
||||
else {
|
||||
theory_var w = m_var_index2theory_var[vi];
|
||||
|
|
@ -2537,7 +2583,7 @@ namespace smt {
|
|||
// ctx().set_enode_flag(bv, true);
|
||||
lp::bound_kind bkind = lp::bound_kind::lower_t;
|
||||
if (is_strict) bkind = lp::bound_kind::upper_t;
|
||||
lp::bound* a = alloc(lp::bound, bv, v, r, bkind);
|
||||
lp::bound* a = alloc(lp::bound, bv, v, is_int, r, bkind);
|
||||
mk_bound_axioms(*a);
|
||||
updt_unassigned_bounds(v, +1);
|
||||
m_bounds[v].push_back(a);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue