mirror of
https://github.com/Z3Prover/z3
synced 2025-04-29 03:45:51 +00:00
add cancellations
Signed-off-by: Lev Nachmanson <levnach@hotmail.com> syntax errors Signed-off-by: Lev Nachmanson <levnach@microsoft.com> use std::vector instead of vector in cut_solver temporarily Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix in is_upper_bound, is_lower_bound Signed-off-by: Lev Nachmanson <levnach@hotmail.com> add bound() for polynomial, needs more testing Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on resolve Signed-off-by: Lev Nachmanson <levnach@microsoft.com> implement resolve() Signed-off-by: Lev Nachmanson <levnach@microsoft.com> implement improves() Signed-off-by: Lev Nachmanson <levnach@hotmail.com> replace low_bound by lower_bound Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on cut_solver Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on cut_solver Signed-off-by: Lev Nachmanson <levnach@hotmail.com> better printing in cut_solver.h Signed-off-by: Lev Nachmanson <levnach@hotmail.com> add value vector to cut_solver Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on bound propagaion for cut_solver Signed-off-by: Lev Nachmanson <levnach@hotmail.com> bound propagation for integer inequalites Signed-off-by: Lev Nachmanson <levnach@hotmail.com> bound propagation for integer inequalites Signed-off-by: Lev Nachmanson <levnach@hotmail.com> bound propagattions on integers Signed-off-by: Lev Nachmanson <levnach@hotmail.com> adding m_explanation field to cut_solver Signed-off-by: Lev Nachmanson <levnach@hotmail.com> simplify bound propagation in cut_solver Signed-off-by: Lev Nachmanson <levnach@hotmail.com> calculate conflict explanation Signed-off-by: Lev Nachmanson <levnach@hotmail.com> change m_explanation type to a set Signed-off-by: Lev Nachmanson <levnach@hotmail.com> making cut_solver a member of int_solver, missing push/pop support Signed-off-by: Lev Nachmanson <levnach@hotmail.com> Nikolaj's comments Signed-off-by: Lev Nachmanson <levnach@hotmail.com> Nikolaj's comments Signed-off-by: Lev Nachmanson <levnach@hotmail.com> return explanations from cut_solver and hook up push/pop Signed-off-by: Lev Nachmanson <levnach@hotmail.com> hook up push/pop Signed-off-by: Lev Nachmanson <levnach@hotmail.com> using resize of std::vector Signed-off-by: Lev Nachmanson <levnach@hotmail.com> it is a big squashed commit Signed-off-by: Lev Nachmanson <levnach@hotmail.com> rename hpp to cpp Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fixes in push/pop of cut_solver Signed-off-by: Lev Nachmanson <levnach@hotmail.com> return simple inequalities a part of a conflict Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on propagation and the main loop Signed-off-by: Lev Nachmanson <levnach@hotmail.com> add file Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on cut_solver Signed-off-by: Lev Nachmanson <levnach@hotmail.com> init m_v[j], the var values only when j is fixed Signed-off-by: Lev Nachmanson <levnach@hotmail.com> cut_solver Signed-off-by: Lev Nachmanson <levnach@hotmail.com> handle decide in cut_solver Signed-off-by: Lev Nachmanson <levnach@hotmail.com> start on resolve_conflict Signed-off-by: Lev Nachmanson <levnach@hotmail.com> start on resolve_conflict Signed-off-by: Lev Nachmanson <levnach@hotmail.com> remove cut_solver_def.h Signed-off-by: Lev Nachmanson <levnach@hotmail.com> in the middle Signed-off-by: Lev Nachmanson <levnach@hotmail.com> change signature of resolve Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix the domain of the decided var Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on tightening of ineqs Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on tight ineqs Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on tightening Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on tightening Signed-off-by: Lev Nachmanson <levnach@hotmail.com> resolve conflict Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix in usage of resolve() Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on conflict resolution Signed-off-by: Lev Nachmanson <levnach@hotmail.com> cut_solver is not a template Signed-off-by: Lev Nachmanson <levnach@hotmail.com> represent var_info as a class, not a struct Signed-off-by: Lev Nachmanson <levnach@hotmail.com> make literal a class Signed-off-by: Lev Nachmanson <levnach@hotmail.com> better resolve_conflict scheme, and switch to *constraints in literals Signed-off-by: Lev Nachmanson <levnach@hotmail.com> debug conflict resolution in cut_solver Signed-off-by: Lev Nachmanson <levnach@hotmail.com> switch to vector Signed-off-by: Lev Nachmanson <levnach@hotmail.com> remove nondetermenistic behavior from cut_solver Signed-off-by: Lev Nachmanson <levnach@hotmail.com> debug resolve conflict Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix backjump Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix backjump Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix backjump Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix backjump Signed-off-by: Lev Nachmanson <levnach@hotmail.com> dumb explanation Signed-off-by: Lev Nachmanson <levnach@hotmail.com> get rid of a parameter Signed-off-by: Lev Nachmanson <levnach@hotmail.com> add lemmas origins Signed-off-by: Lev Nachmanson <levnach@hotmail.com> use lemma_origins to provide correct explanations Signed-off-by: Lev Nachmanson <levnach@hotmail.com> use lemma_origins to provide correct explanations Signed-off-by: Lev Nachmanson <levnach@hotmail.com> store lemmas in a separate vector Signed-off-by: Lev Nachmanson <levnach@hotmail.com> use std::unordered_set for m_dependent_constraints Signed-off-by: Lev Nachmanson <levnach@hotmail.com> use std::unordered_set for m_dependent_constraints Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix bugs with lemmas Signed-off-by: Lev Nachmanson <levnach@hotmail.com> finding conflicting cores Signed-off-by: Lev Nachmanson <levnach@hotmail.com> switch from changed variables to active_set Signed-off-by: Lev Nachmanson <levnach@hotmail.com> less active constraints Signed-off-by: Lev Nachmanson <levnach@hotmail.com> work on cut_solver.h Signed-off-by: Lev Nachmanson <levnach@hotmail.com> propagate simple constraing immediately Signed-off-by: Lev Nachmanson <levnach@hotmail.com> propagate simple constraints immediately Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fixing bugs with active set Signed-off-by: Lev Nachmanson <levnach@hotmail.com> remove const_cast Signed-off-by: Lev Nachmanson <levnach@hotmail.com> towards unbounded variables Signed-off-by: Lev Nachmanson <levnach@hotmail.com> toward unbounded variables Signed-off-by: Lev Nachmanson <levnach@hotmail.com> toward unbounded variables Signed-off-by: Lev Nachmanson <levnach@hotmail.com> make lemmas_origins a set Signed-off-by: Lev Nachmanson <levnach@hotmail.com> use correct hash and equal in m_lemma_origins Signed-off-by: Lev Nachmanson <levnach@hotmail.com> add testing code Signed-off-by: Lev Nachmanson <levnach@hotmail.com> add testing code Signed-off-by: Lev Nachmanson <levnach@hotmail.com> debug Signed-off-by: Lev Nachmanson <levnach@hotmail.com> debug unlimited vars Signed-off-by: Lev Nachmanson <levnach@hotmail.com> take in Nikolaj's comments and improvements Signed-off-by: Lev Nachmanson <levnach@hotmail.com> address the comments Signed-off-by: Lev Nachmanson <levnach@hotmail.com> handle unlimited vars in check_inconsistent Signed-off-by: Lev Nachmanson <levnach@hotmail.com> debug Signed-off-by: Lev Nachmanson <levnach@hotmail.com> detect trivial polynomials in resolve Signed-off-by: Lev Nachmanson <levnach@hotmail.com> Nikolaj's changes Signed-off-by: Lev Nachmanson <levnach@hotmail.com> simplify handling of m_global_bound_var Signed-off-by: Lev Nachmanson <levnach@hotmail.com> decide on m_global_bound_var if it is not fixed Signed-off-by: Lev Nachmanson <levnach@hotmail.com> simplify m_global_bound_var Signed-off-by: Lev Nachmanson <levnach@hotmail.com> remove m_global_bound_var, simplify the indexing of var_infos of cut_solver Signed-off-by: Lev Nachmanson <levnach@hotmail.com> do not run cut_solver with vars without any bound Signed-off-by: Lev Nachmanson <levnach@hotmail.com> small changes Signed-off-by: Lev Nachmanson <levnach@hotmail.com> add cancellation in cut_solver Signed-off-by: Lev Nachmanson <levnach@hotmail.com> do not pop lemmas during a cut_solver run Signed-off-by: Lev Nachmanson <levnach@hotmail.com> treating cut_solver as an heurisitic Signed-off-by: Lev Nachmanson <levnach@hotmail.com> prepare for cut_solver returning undef Signed-off-by: Lev Nachmanson <levnach@hotmail.com> simplify work with active_set in cut_solver, add stats Signed-off-by: Lev Nachmanson <levnach@hotmail.com> simplify var_info literals Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix a bug in fill_conflict_explanation Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix a bug in the conflict explanation Signed-off-by: Lev Nachmanson <levnach@hotmail.com> add timeout to validate_* in theory_lra.cpp Signed-off-by: Lev Nachmanson <levnach@hotmail.com> simplify cut_solver, no special treatment for simple constraints Signed-off-by: Lev Nachmanson <levnach@hotmail.com> cleanup the cancel story Signed-off-by: Lev Nachmanson <levnach@hotmail.com> cleanup cancelling Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix a bug in push/pop of cut_solver Signed-off-by: Lev Nachmanson <levnach@hotmail.com> extract a method in int_solver Signed-off-by: Lev Nachmanson <levnach@hotmail.com> some progress with the new scheme Signed-off-by: Lev Nachmanson <levnach@hotmail.com> add testing code Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fixes in test and in literal creation Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix a bug in bound propagation in cut_solver.h Signed-off-by: Lev Nachmanson <levnach@hotmail.com> simplify cut_solver Signed-off-by: Lev Nachmanson <levnach@hotmail.com> provide valid conflict explanation Signed-off-by: Lev Nachmanson <levnach@hotmail.com> use a lazy push in stacked_map Signed-off-by: Lev Nachmanson <levnach@hotmail.com> use a lazy push in stacked_map Signed-off-by: Lev Nachmanson <levnach@hotmail.com> optimize stack operations on var_info's domains Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fix a bug in tightening Signed-off-by: Lev Nachmanson <levnach@hotmail.com> use the standard tactics from qflia_tactic Signed-off-by: Lev Nachmanson <levnach@hotmail.com> spread the var domain stack over literals Signed-off-by: Lev Nachmanson <levnach@hotmail.com> spread the var domain stack over literals Signed-off-by: Lev Nachmanson <levnach@hotmail.com> avoid cycling in cut_solver.h and fixes in push/pop Signed-off-by: Lev Nachmanson <levnach@hotmail.com> fixes after rebase Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
parent
58ca4518e5
commit
6202b2f2e4
103 changed files with 7035 additions and 5106 deletions
|
|
@ -20,10 +20,9 @@ Revision History:
|
|||
#pragma once
|
||||
#include "util/vector.h"
|
||||
#include "util/lp/linear_combination_iterator.h"
|
||||
#include "util/lp/implied_bound.h"
|
||||
#include "util/lp/test_bound_analyzer.h"
|
||||
#include <functional>
|
||||
#include "util/lp/lp_bound_propagator.h"
|
||||
#include "implied_bound.h"
|
||||
#include "test_bound_analyzer.h"
|
||||
#include "util/lp/bound_propagator.h"
|
||||
// We have an equality : sum by j of row[j]*x[j] = rs
|
||||
// We try to pin a var by pushing the total by using the variable bounds
|
||||
// In a loop we drive the partial sum down, denoting the variables of this process by _u.
|
||||
|
|
@ -31,22 +30,22 @@ Revision History:
|
|||
namespace lp {
|
||||
|
||||
class bound_analyzer_on_row {
|
||||
|
||||
|
||||
linear_combination_iterator<mpq> & m_it;
|
||||
lp_bound_propagator & m_bp;
|
||||
bound_propagator & m_bp;
|
||||
unsigned m_row_or_term_index;
|
||||
int m_column_of_u; // index of an unlimited from above monoid
|
||||
// -1 means that such a value is not found, -2 means that at least two of such monoids were found
|
||||
// -1 means that such a value is not found, -2 means that at least two of such monoids were found
|
||||
int m_column_of_l; // index of an unlimited from below monoid
|
||||
impq m_rs;
|
||||
|
||||
public :
|
||||
// constructor
|
||||
bound_analyzer_on_row(
|
||||
linear_combination_iterator<mpq> &it,
|
||||
const numeric_pair<mpq>& rs,
|
||||
unsigned row_or_term_index,
|
||||
lp_bound_propagator & bp
|
||||
linear_combination_iterator<mpq> &it,
|
||||
const numeric_pair<mpq>& rs,
|
||||
unsigned row_or_term_index,
|
||||
bound_propagator & bp
|
||||
)
|
||||
:
|
||||
m_it(it),
|
||||
|
|
@ -60,7 +59,7 @@ public :
|
|||
|
||||
unsigned j;
|
||||
void analyze() {
|
||||
|
||||
|
||||
mpq a; unsigned j;
|
||||
while (((m_column_of_l != -2) || (m_column_of_u != -2)) && m_it.next(a, j))
|
||||
analyze_bound_on_var_on_coeff(j, a);
|
||||
|
|
@ -76,33 +75,33 @@ public :
|
|||
limit_all_monoids_from_above();
|
||||
}
|
||||
|
||||
bool bound_is_available(unsigned j, bool low_bound) {
|
||||
return (low_bound && low_bound_is_available(j)) ||
|
||||
(!low_bound && upper_bound_is_available(j));
|
||||
bool bound_is_available(unsigned j, bool lower_bound) {
|
||||
return (lower_bound && lower_bound_is_available(j)) ||
|
||||
(!lower_bound && upper_bound_is_available(j));
|
||||
}
|
||||
|
||||
bool upper_bound_is_available(unsigned j) const {
|
||||
switch (m_bp.get_column_type(j))
|
||||
{
|
||||
case column_type::fixed:
|
||||
case column_type::boxed:
|
||||
case column_type::upper_bound:
|
||||
return true;
|
||||
default:
|
||||
return false;
|
||||
}
|
||||
{
|
||||
case column_type::fixed:
|
||||
case column_type::boxed:
|
||||
case column_type::upper_bound:
|
||||
return true;
|
||||
default:
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
bool low_bound_is_available(unsigned j) const {
|
||||
bool lower_bound_is_available(unsigned j) const {
|
||||
switch (m_bp.get_column_type(j))
|
||||
{
|
||||
case column_type::fixed:
|
||||
case column_type::boxed:
|
||||
case column_type::low_bound:
|
||||
return true;
|
||||
default:
|
||||
return false;
|
||||
}
|
||||
{
|
||||
case column_type::fixed:
|
||||
case column_type::boxed:
|
||||
case column_type::lower_bound:
|
||||
return true;
|
||||
default:
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
const impq & ub(unsigned j) const {
|
||||
|
|
@ -110,8 +109,8 @@ public :
|
|||
return m_bp.get_upper_bound(j);
|
||||
}
|
||||
const impq & lb(unsigned j) const {
|
||||
lp_assert(low_bound_is_available(j));
|
||||
return m_bp.get_low_bound(j);
|
||||
lp_assert(lower_bound_is_available(j));
|
||||
return m_bp.get_lower_bound(j);
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -151,7 +150,7 @@ public :
|
|||
strict = !is_zero(ub(j).y);
|
||||
return a * ub(j).x;
|
||||
}
|
||||
|
||||
|
||||
strict = !is_zero(lb(j).y);
|
||||
return a * lb(j).x;
|
||||
}
|
||||
|
|
@ -160,10 +159,10 @@ public :
|
|||
if (is_neg(a)) {
|
||||
return a * ub(j).x;
|
||||
}
|
||||
|
||||
|
||||
return a * lb(j).x;
|
||||
}
|
||||
|
||||
|
||||
|
||||
void limit_all_monoids_from_above() {
|
||||
int strict = 0;
|
||||
|
|
@ -209,7 +208,7 @@ public :
|
|||
bool str;
|
||||
bool a_is_pos = is_pos(a);
|
||||
mpq bound = total / a + monoid_max_no_mult(a_is_pos, j, str);
|
||||
bool astrict = strict - static_cast<int>(str) > 0;
|
||||
bool astrict = strict - static_cast<int>(str) > 0;
|
||||
if (a_is_pos) {
|
||||
limit_j(j, bound, true, true, astrict);
|
||||
}
|
||||
|
|
@ -219,7 +218,7 @@ public :
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
void limit_monoid_u_from_below() {
|
||||
// we are going to limit from below the monoid m_column_of_u,
|
||||
// every other monoid is impossible to limit from below
|
||||
|
|
@ -240,7 +239,7 @@ public :
|
|||
}
|
||||
|
||||
bound /= u_coeff;
|
||||
|
||||
|
||||
if (numeric_traits<impq>::is_pos(u_coeff)) {
|
||||
limit_j(m_column_of_u, bound, true, true, strict);
|
||||
} else {
|
||||
|
|
@ -275,51 +274,51 @@ public :
|
|||
limit_j(m_column_of_l, bound, false, true, strict);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
// // it is the coefficent before the bounded column
|
||||
// void provide_evidence(bool coeff_is_pos) {
|
||||
// /*
|
||||
// auto & be = m_ibounds.back();
|
||||
// bool low_bound = be.m_low_bound;
|
||||
// bool lower_bound = be.m_lower_bound;
|
||||
// if (!coeff_is_pos)
|
||||
// low_bound = !low_bound;
|
||||
// lower_bound = !lower_bound;
|
||||
// auto it = m_it.clone();
|
||||
// mpq a; unsigned j;
|
||||
// while (it->next(a, j)) {
|
||||
// if (be.m_j == j) continue;
|
||||
// lp_assert(bound_is_available(j, is_neg(a) ? low_bound : !low_bound));
|
||||
// lp_assert(bound_is_available(j, is_neg(a) ? lower_bound : !lower_bound));
|
||||
// be.m_vector_of_bound_signatures.emplace_back(a, j, numeric_traits<impq>::
|
||||
// is_neg(a)? low_bound: !low_bound);
|
||||
// is_neg(a)? lower_bound: !lower_bound);
|
||||
// }
|
||||
// delete it;
|
||||
// */
|
||||
// }
|
||||
|
||||
void limit_j(unsigned j, const mpq& u, bool coeff_before_j_is_pos, bool is_low_bound, bool strict){
|
||||
m_bp.try_add_bound(u, j, is_low_bound, coeff_before_j_is_pos, m_row_or_term_index, strict);
|
||||
void limit_j(unsigned j, const mpq& u, bool coeff_before_j_is_pos, bool is_lower_bound, bool strict){
|
||||
m_bp.try_add_bound(u, j, is_lower_bound, coeff_before_j_is_pos, m_row_or_term_index, strict);
|
||||
}
|
||||
|
||||
|
||||
|
||||
void advance_u(unsigned j) {
|
||||
if (m_column_of_u == -1)
|
||||
m_column_of_u = j;
|
||||
else
|
||||
m_column_of_u = -2;
|
||||
}
|
||||
|
||||
|
||||
void advance_l(unsigned j) {
|
||||
if (m_column_of_l == -1)
|
||||
m_column_of_l = j;
|
||||
else
|
||||
m_column_of_l = -2;
|
||||
}
|
||||
|
||||
|
||||
void analyze_bound_on_var_on_coeff(int j, const mpq &a) {
|
||||
switch (m_bp.get_column_type(j)) {
|
||||
case column_type::low_bound:
|
||||
case column_type::lower_bound:
|
||||
if (numeric_traits<mpq>::is_pos(a))
|
||||
advance_u(j);
|
||||
else
|
||||
else
|
||||
advance_l(j);
|
||||
break;
|
||||
case column_type::upper_bound:
|
||||
|
|
@ -340,7 +339,7 @@ public :
|
|||
static void analyze_row(linear_combination_iterator<mpq> &it,
|
||||
const numeric_pair<mpq>& rs,
|
||||
unsigned row_or_term_index,
|
||||
lp_bound_propagator & bp
|
||||
bound_propagator & bp
|
||||
) {
|
||||
bound_analyzer_on_row a(it, rs, row_or_term_index, bp);
|
||||
a.analyze();
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue