mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 00:26:38 +00:00
Merge remote-tracking branch 'origin/polysat' into polysat
This commit is contained in:
Jakob Rath
commit
e1aa00352d
10 changed files with 3 additions and 2901 deletions
|
|
@ -12,7 +12,6 @@ z3_add_component(polysat
|
|||
forbidden_intervals.cpp
|
||||
inference_logger.cpp
|
||||
justification.cpp
|
||||
linear_solver.cpp
|
||||
log.cpp
|
||||
naming.cpp
|
||||
op_constraint.cpp
|
||||
|
|
@ -33,7 +32,6 @@ z3_add_component(polysat
|
|||
viable.cpp
|
||||
viable_fallback.cpp
|
||||
COMPONENT_DEPENDENCIES
|
||||
bigfix
|
||||
dd
|
||||
euf
|
||||
interval
|
||||
|
|
|
|||
|
|
@ -24,7 +24,7 @@ namespace polysat {
|
|||
// NB code review:
|
||||
// right, ref-count is unlikely the right mechanism.
|
||||
// In the SAT solver all clauses are managed in one arena (auxiliarary and redundant)
|
||||
// and deleted when they exist the arena.
|
||||
// and deleted when they exit the arena.
|
||||
//
|
||||
class clause {
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -1,483 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
fixplex.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Fixed-precision unsigned integer simplex tableau.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-6
|
||||
|
||||
--*/
|
||||
|
||||
#pragma once
|
||||
|
||||
#include <limits>
|
||||
#include "math/simplex/sparse_matrix.h"
|
||||
#include "fixplex_mod_interval.h"
|
||||
#include "util/heap.h"
|
||||
#include "util/map.h"
|
||||
#include "util/rational.h"
|
||||
#include "util/lbool.h"
|
||||
#include "util/uint_set.h"
|
||||
#include "util/dependency.h"
|
||||
#include "util/ref.h"
|
||||
#include "util/params.h"
|
||||
#include "util/union_find.h"
|
||||
|
||||
inline rational to_rational(uint64_t n) { return rational(n, rational::ui64()); }
|
||||
inline unsigned trailing_zeros(unsigned short n) { return trailing_zeros((uint32_t)n); }
|
||||
inline unsigned trailing_zeros(unsigned char n) { return trailing_zeros((uint32_t)n); }
|
||||
inline unsigned numeral2hash(unsigned char const& n) { return n; }
|
||||
inline unsigned numeral2hash(unsigned short const& n) { return n; }
|
||||
inline unsigned numeral2hash(uint32_t const& n) { return n; }
|
||||
inline unsigned numeral2hash(uint64_t const& n) { return static_cast<unsigned>(n ^ (n >> 32)); }
|
||||
|
||||
|
||||
namespace polysat {
|
||||
|
||||
typedef unsigned var_t;
|
||||
|
||||
struct fixplex_base {
|
||||
virtual ~fixplex_base() {}
|
||||
virtual lbool make_feasible() = 0;
|
||||
virtual void add_row(var_t base, unsigned num_vars, var_t const* vars, rational const* coeffs) = 0;
|
||||
virtual void del_row(var_t base_var) = 0;
|
||||
virtual void push() = 0;
|
||||
virtual void pop(unsigned n) = 0;
|
||||
virtual std::ostream& display(std::ostream& out) const = 0;
|
||||
virtual void collect_statistics(::statistics & st) const = 0;
|
||||
virtual void set_bounds(var_t v, rational const& lo, rational const& hi, unsigned dep) = 0;
|
||||
virtual void set_value(var_t v, rational const& val, unsigned dep) = 0;
|
||||
virtual rational get_value(var_t v) = 0;
|
||||
virtual void restore_bound() = 0;
|
||||
virtual void add_le(var_t v, var_t w, unsigned dep) = 0;
|
||||
virtual void add_lt(var_t v, var_t w, unsigned dep) = 0;
|
||||
virtual void restore_ineq() = 0;
|
||||
virtual bool inconsistent() const = 0;
|
||||
virtual unsigned_vector const& get_unsat_core() const = 0;
|
||||
virtual void updt_params(params_ref const& p) = 0;
|
||||
|
||||
};
|
||||
|
||||
struct ineq {
|
||||
var_t v = UINT_MAX;
|
||||
var_t w = UINT_MAX;
|
||||
bool strict = false;
|
||||
u_dependency* dep = nullptr;
|
||||
ineq(var_t v, var_t w, u_dependency* dep, bool s) :
|
||||
v(v), w(w), strict(s), dep(dep) {}
|
||||
|
||||
std::ostream& display(std::ostream& out) const {
|
||||
return out << "v" << v << (strict ? " < v" : " <= v") << w;
|
||||
}
|
||||
};
|
||||
|
||||
template<typename Ext>
|
||||
class fixplex : public fixplex_base {
|
||||
public:
|
||||
typedef typename Ext::numeral numeral;
|
||||
typedef typename Ext::scoped_numeral scoped_numeral;
|
||||
typedef typename Ext::manager manager;
|
||||
typedef simplex::sparse_matrix<Ext> matrix;
|
||||
typedef typename matrix::row row;
|
||||
typedef typename matrix::row_iterator row_iterator;
|
||||
typedef typename matrix::col_iterator col_iterator;
|
||||
|
||||
struct var_eq {
|
||||
var_t x, y;
|
||||
u_dependency* dep;
|
||||
var_eq(var_t x, var_t y, u_dependency* dep):
|
||||
x(x), y(y), dep(dep) {}
|
||||
};
|
||||
|
||||
protected:
|
||||
struct var_lt {
|
||||
bool operator()(var_t v1, var_t v2) const { return v1 < v2; }
|
||||
};
|
||||
typedef heap<var_lt> var_heap;
|
||||
|
||||
struct stats {
|
||||
unsigned m_num_pivots;
|
||||
unsigned m_num_infeasible;
|
||||
unsigned m_num_checks;
|
||||
unsigned m_num_approx;
|
||||
stats() { reset(); }
|
||||
void reset() {
|
||||
memset(this, 0, sizeof(*this));
|
||||
}
|
||||
};
|
||||
|
||||
enum pivot_strategy_t {
|
||||
S_BLAND,
|
||||
S_GREATEST_ERROR,
|
||||
S_LEAST_ERROR,
|
||||
S_DEFAULT
|
||||
};
|
||||
|
||||
struct var_info : public mod_interval<numeral> {
|
||||
unsigned m_base2row:29;
|
||||
unsigned m_is_base:1;
|
||||
numeral m_value = 0;
|
||||
u_dependency* m_lo_dep = nullptr;
|
||||
u_dependency* m_hi_dep = nullptr;
|
||||
var_info():
|
||||
m_base2row(0),
|
||||
m_is_base(false)
|
||||
{}
|
||||
~var_info() override {}
|
||||
var_info& operator&=(mod_interval<numeral> const& range) {
|
||||
mod_interval<numeral>::operator=(range & *this);
|
||||
return *this;
|
||||
}
|
||||
var_info& operator=(mod_interval<numeral> const& range) {
|
||||
mod_interval<numeral>::operator=(range);
|
||||
return *this;
|
||||
}
|
||||
};
|
||||
|
||||
struct row_info {
|
||||
bool m_integral { true };
|
||||
var_t m_base;
|
||||
numeral m_value;
|
||||
numeral m_base_coeff;
|
||||
};
|
||||
|
||||
struct stashed_bound : var_info {
|
||||
var_t m_var;
|
||||
stashed_bound(var_t v, var_info const& i):
|
||||
var_info(i),
|
||||
m_var(v)
|
||||
{}
|
||||
};
|
||||
|
||||
struct fix_entry {
|
||||
var_t x = null_var;
|
||||
u_dependency* dep = nullptr;
|
||||
fix_entry(var_t x, u_dependency* dep): x(x), dep(dep) {}
|
||||
fix_entry() {}
|
||||
};
|
||||
|
||||
enum trail_i {
|
||||
inc_level_i,
|
||||
set_bound_i,
|
||||
set_inconsistent_i,
|
||||
add_ineq_i,
|
||||
add_row_i,
|
||||
add_eq_i,
|
||||
fixed_val_i
|
||||
};
|
||||
|
||||
static const var_t null_var = UINT_MAX;
|
||||
reslimit& m_limit;
|
||||
mutable manager m;
|
||||
mutable matrix M;
|
||||
unsigned m_max_iterations = UINT_MAX;
|
||||
unsigned m_num_non_integral = 0;
|
||||
uint_set m_non_integral;
|
||||
var_heap m_to_patch;
|
||||
vector<var_info> m_vars;
|
||||
vector<row_info> m_rows;
|
||||
|
||||
bool m_bland = false ;
|
||||
unsigned m_blands_rule_threshold = 1000;
|
||||
unsigned m_num_repeated = 0;
|
||||
random_gen m_random;
|
||||
uint_set m_left_basis;
|
||||
unsigned_vector m_unsat_core;
|
||||
bool m_inconsistent = false;
|
||||
unsigned_vector m_base_vars;
|
||||
stats m_stats;
|
||||
vector<stashed_bound> m_stashed_bounds;
|
||||
u_dependency_manager m_deps;
|
||||
svector<trail_i> m_trail;
|
||||
svector<var_t> m_row_trail;
|
||||
|
||||
// euqality propagation
|
||||
union_find_default_ctx m_union_find_ctx;
|
||||
union_find<> m_union_find;
|
||||
vector<var_eq> m_var_eqs;
|
||||
vector<numeral> m_fixed_vals;
|
||||
map<numeral, fix_entry, typename manager::hash, typename manager::eq> m_value2fixed_var;
|
||||
uint_set m_eq_rows;
|
||||
|
||||
// inequalities
|
||||
svector<ineq> m_ineqs;
|
||||
uint_set m_ineqs_to_propagate;
|
||||
uint_set m_touched_vars;
|
||||
vector<unsigned_vector> m_var2ineqs;
|
||||
|
||||
// bound propagation
|
||||
uint_set m_bound_rows;
|
||||
|
||||
public:
|
||||
fixplex(params_ref const& p, reslimit& lim):
|
||||
m_limit(lim),
|
||||
M(m),
|
||||
m_to_patch(1024),
|
||||
m_union_find(m_union_find_ctx) {
|
||||
updt_params(p);
|
||||
}
|
||||
|
||||
~fixplex() override;
|
||||
|
||||
void push() override;
|
||||
void pop(unsigned n) override;
|
||||
bool inconsistent() const override { return m_inconsistent; }
|
||||
void updt_params(params_ref const& p) override;
|
||||
|
||||
lbool make_feasible() override;
|
||||
void add_row(var_t base, unsigned num_vars, var_t const* vars, rational const* coeffs) override;
|
||||
std::ostream& display(std::ostream& out) const override;
|
||||
void collect_statistics(::statistics & st) const override;
|
||||
void del_row(var_t base_var) override;
|
||||
void set_bounds(var_t v, rational const& lo, rational const& hi, unsigned dep) override;
|
||||
void set_value(var_t v, rational const& val, unsigned dep) override;
|
||||
rational get_value(var_t v) override;
|
||||
void restore_bound() override;
|
||||
void add_le(var_t v, var_t w, unsigned dep) override { add_ineq(v, w, dep, false); }
|
||||
void add_lt(var_t v, var_t w, unsigned dep) override { add_ineq(v, w, dep, true); }
|
||||
virtual void restore_ineq() override;
|
||||
|
||||
void set_bounds(var_t v, numeral const& lo, numeral const& hi, unsigned dep);
|
||||
void update_bounds(var_t v, numeral const& l, numeral const& h, u_dependency* dep);
|
||||
void unset_bounds(var_t v) { m_vars[v].set_free(); }
|
||||
|
||||
|
||||
numeral const& lo(var_t var) const { return m_vars[var].lo; }
|
||||
numeral const& hi(var_t var) const { return m_vars[var].hi; }
|
||||
numeral const& value(var_t var) const { return m_vars[var].m_value; }
|
||||
void set_max_iterations(unsigned n) { m_max_iterations = n; }
|
||||
unsigned get_num_vars() const { return m_vars.size(); }
|
||||
void reset();
|
||||
|
||||
vector<var_eq> const& var_eqs() const { return m_var_eqs; }
|
||||
|
||||
void add_row(var_t base, unsigned num_vars, var_t const* vars, numeral const* coeffs);
|
||||
|
||||
unsigned_vector const& get_unsat_core() const override { return m_unsat_core; }
|
||||
|
||||
private:
|
||||
|
||||
svector<std::pair<unsigned, unsigned>> stack;
|
||||
uint_set on_stack;
|
||||
lbool propagate_ineqs(unsigned idx);
|
||||
|
||||
std::ostream& display_row(std::ostream& out, row const& r, bool values = true) const;
|
||||
var_t get_base_var(row const& r) const { return m_rows[r.id()].m_base; }
|
||||
|
||||
void update_value_core(var_t v, numeral const& delta);
|
||||
void ensure_var(var_t v);
|
||||
|
||||
bool patch();
|
||||
bool propagate_ineqs();
|
||||
bool propagate_row_eqs();
|
||||
bool propagate_row_bounds();
|
||||
bool is_satisfied();
|
||||
|
||||
struct backoff {
|
||||
unsigned m_tries = 0;
|
||||
unsigned m_delay = 1;
|
||||
bool should_propagate() {
|
||||
return ++m_tries >= m_delay;
|
||||
}
|
||||
void update(bool progress) {
|
||||
m_tries = 0;
|
||||
if (progress)
|
||||
m_delay = 1;
|
||||
else
|
||||
++m_delay;
|
||||
}
|
||||
};
|
||||
|
||||
backoff m_propagate_eqs_backoff;
|
||||
backoff m_propagate_bounds_backoff;
|
||||
|
||||
|
||||
|
||||
var_t select_smallest_var() { return m_to_patch.empty()?null_var:m_to_patch.erase_min(); }
|
||||
lbool make_var_feasible(var_t x_i);
|
||||
bool is_infeasible_row(var_t x);
|
||||
bool is_parity_infeasible_row(var_t x);
|
||||
bool is_offset_row(row const& r, numeral& cx, var_t& x, numeral& cy, var_t & y) const;
|
||||
void lookahead_eq(row const& r1, numeral const& cx, var_t x, numeral const& cy, var_t y);
|
||||
void get_offset_eqs(row const& r);
|
||||
void fixed_var_eh(u_dependency* dep, var_t x);
|
||||
var_t find(var_t x) { return m_union_find.find(x); }
|
||||
void merge(var_t x, var_t y) { m_union_find.merge(x, y); }
|
||||
void eq_eh(var_t x, var_t y, u_dependency* dep);
|
||||
bool propagate_row(row const& r);
|
||||
bool propagate_ineq(ineq const& i);
|
||||
bool propagate_strict_bounds(ineq const& i);
|
||||
bool propagate_non_strict_bounds(ineq const& i);
|
||||
bool new_bound(row const& r, var_t x, mod_interval<numeral> const& range);
|
||||
bool new_bound(ineq const& i, var_t x, numeral const& lo, numeral const& hi, u_dependency* a = nullptr, u_dependency* b = nullptr, u_dependency* c = nullptr, u_dependency* d = nullptr);
|
||||
void conflict(ineq const& i, u_dependency* a = nullptr, u_dependency* b = nullptr, u_dependency* c = nullptr, u_dependency* d = nullptr);
|
||||
void conflict(u_dependency* a);
|
||||
void conflict(u_dependency* a, u_dependency* b, u_dependency* c = nullptr, u_dependency* d = nullptr) { conflict(m_deps.mk_join(m_deps.mk_join(a, b), m_deps.mk_join(c, d))); }
|
||||
u_dependency* row2dep(row const& r);
|
||||
void pivot(var_t x_i, var_t x_j, numeral const& b, numeral const& value);
|
||||
numeral value2delta(var_t v, numeral const& new_value) const;
|
||||
numeral value2error(var_t v, numeral const& new_value) const;
|
||||
void update_value(var_t v, numeral const& delta);
|
||||
bool can_pivot(var_t x_i, numeral const& new_value, numeral const& a_ij, var_t x_j);
|
||||
bool has_minimal_trailing_zeros(var_t y, numeral const& b);
|
||||
var_t select_pivot(var_t x_i, numeral const& new_value, numeral& out_b);
|
||||
var_t select_pivot_core(var_t x, numeral const& new_value, numeral& out_b);
|
||||
bool in_bounds(var_t v) const { return in_bounds(v, value(v)); }
|
||||
bool in_bounds(var_t v, numeral const& b) const { return in_bounds(b, m_vars[v]); }
|
||||
bool in_bounds(numeral const& val, mod_interval<numeral> const& range) const { return range.contains(val); }
|
||||
bool is_free(var_t v) const { return lo(v) == hi(v); }
|
||||
bool is_non_free(var_t v) const { return !is_free(v); }
|
||||
bool is_fixed(var_t v) const { return lo(v) + 1 == hi(v); }
|
||||
bool is_valid_variable(var_t v) const { return v < m_vars.size(); }
|
||||
bool is_base(var_t x) const { return m_vars[x].m_is_base; }
|
||||
row base2row(var_t x) const { return row(m_vars[x].m_base2row); }
|
||||
numeral const& row2value(row const& r) const { return m_rows[r.id()].m_value; }
|
||||
numeral const& row2base_coeff(row const& r) const { return m_rows[r.id()].m_base_coeff; }
|
||||
var_t row2base(row const& r) const { return m_rows[r.id()].m_base; }
|
||||
bool row_is_integral(row const& r) const { return m_rows[r.id()].m_integral; }
|
||||
void set_base_value(var_t x);
|
||||
numeral solve_for(numeral const& row_value, numeral const& coeff);
|
||||
int get_num_non_free_dep_vars(var_t x_j, int best_so_far);
|
||||
void add_patch(var_t v);
|
||||
var_t select_var_to_fix();
|
||||
void check_blands_rule(var_t v);
|
||||
pivot_strategy_t pivot_strategy() { return m_bland ? S_BLAND : S_DEFAULT; }
|
||||
var_t select_error_var(bool least);
|
||||
void set_infeasible_base(var_t v);
|
||||
void set_infeasible_bounds(var_t v);
|
||||
|
||||
u_dependency* mk_leaf(unsigned dep) { return UINT_MAX == dep ? nullptr : m_deps.mk_leaf(dep); }
|
||||
|
||||
// facilities for handling inequalities
|
||||
void add_ineq(var_t v, var_t w, unsigned dep, bool strict);
|
||||
void touch_var(var_t x);
|
||||
|
||||
|
||||
bool is_solved(row const& r) const;
|
||||
bool is_solved(var_t v) const { SASSERT(is_base(v)); return is_solved(base2row(v)); }
|
||||
|
||||
bool well_formed() const;
|
||||
bool well_formed_row(row const& r) const;
|
||||
|
||||
void del_row(row const& r);
|
||||
|
||||
var_t select_pivot_blands(var_t x, numeral const& new_value, numeral& out_b);
|
||||
bool can_improve(var_t x, numeral const& new_value, var_t y, numeral const& b);
|
||||
|
||||
bool pivot_base_vars();
|
||||
bool elim_base(var_t v);
|
||||
|
||||
bool eliminate_var(
|
||||
row const& r_y,
|
||||
col_iterator const& z_col,
|
||||
unsigned tz_b,
|
||||
numeral const& old_value_y);
|
||||
};
|
||||
|
||||
template<typename uint_type>
|
||||
struct generic_uint_ext {
|
||||
typedef uint_type numeral;
|
||||
|
||||
struct manager {
|
||||
typedef uint_type numeral;
|
||||
struct hash {
|
||||
unsigned operator()(numeral const& n) const {
|
||||
return numeral2hash(n);
|
||||
}
|
||||
};
|
||||
struct eq {
|
||||
bool operator()(numeral const& a, numeral const& b) const {
|
||||
return a == b;
|
||||
}
|
||||
};
|
||||
numeral from_rational(rational const& n) { return static_cast<uint_type>(n.get_uint64()); }
|
||||
rational to_rational(numeral const& n) const { return ::to_rational(n); }
|
||||
void reset() {}
|
||||
void reset(numeral& n) { n = 0; }
|
||||
void del(numeral const& n) {}
|
||||
bool is_zero(numeral const& n) const { return n == 0; }
|
||||
bool is_one(numeral const& n) const { return n == 1; }
|
||||
bool is_even(numeral const& n) const { return (n & 1) == 0; }
|
||||
bool is_minus_one(numeral const& n) const { return n + 1 == 0; }
|
||||
void add(numeral const& a, numeral const& b, numeral& r) { r = a + b; }
|
||||
void sub(numeral const& a, numeral const& b, numeral& r) { r = a - b; }
|
||||
void mul(numeral const& a, numeral const& b, numeral& r) { r = a * b; }
|
||||
void set(numeral& r, numeral const& a) { r = a; }
|
||||
void neg(numeral& a) { a = 0 - a; }
|
||||
numeral inv(numeral const& a) { return 0 - a; }
|
||||
void swap(numeral& a, numeral& b) { std::swap(a, b); }
|
||||
unsigned trailing_zeros(numeral const& a) const { return ::trailing_zeros(a); }
|
||||
numeral mul_inverse(numeral const& x) {
|
||||
if (x == 0)
|
||||
return 0;
|
||||
numeral t0 = 1, t1 = 0 - 1;
|
||||
numeral r0 = x, r1 = 0 - x;
|
||||
while (r1 != 0) {
|
||||
numeral q = r0 / r1;
|
||||
numeral tmp = t1;
|
||||
t1 = t0 - q * t1;
|
||||
t0 = tmp;
|
||||
tmp = r1;
|
||||
r1 = r0 - q * r1;
|
||||
r0 = tmp;
|
||||
}
|
||||
return t0;
|
||||
}
|
||||
numeral gcd(numeral x, numeral y) {
|
||||
if (x == 0)
|
||||
return y;
|
||||
if (y == 0)
|
||||
return x;
|
||||
unsigned tz = trailing_zeros(x);
|
||||
numeral shift = std::min(trailing_zeros(y), tz);
|
||||
x >>= tz;
|
||||
if (x == 1)
|
||||
return x << shift;
|
||||
if (y == 1)
|
||||
return y << shift;
|
||||
if (x == y)
|
||||
return x << shift;
|
||||
do {
|
||||
tz = trailing_zeros(y);
|
||||
y >>= tz;
|
||||
if (x > y)
|
||||
swap(x, y);
|
||||
y -= x;
|
||||
}
|
||||
while (y != 0);
|
||||
return x << shift;
|
||||
}
|
||||
|
||||
std::ostream& display(std::ostream& out, numeral const& x) const {
|
||||
return out << pp(x);
|
||||
}
|
||||
};
|
||||
typedef _scoped_numeral<manager> scoped_numeral;
|
||||
|
||||
};
|
||||
|
||||
typedef generic_uint_ext<uint64_t> uint64_ext;
|
||||
|
||||
|
||||
template<typename Ext>
|
||||
inline std::ostream& operator<<(std::ostream& out, fixplex<Ext> const& fp) {
|
||||
return fp.display(out);
|
||||
}
|
||||
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, ineq const& i) {
|
||||
return i.display(out);
|
||||
}
|
||||
|
||||
|
||||
|
||||
};
|
||||
|
||||
File diff suppressed because it is too large
Load diff
|
|
@ -1,111 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
mod_interval.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Intervals over fixed precision modular arithmetic
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-6
|
||||
|
||||
--*/
|
||||
|
||||
#pragma once
|
||||
|
||||
#include "util/rational.h"
|
||||
|
||||
|
||||
template<typename Numeral>
|
||||
struct pp {
|
||||
Numeral n;
|
||||
pp(Numeral const& n):n(n) {}
|
||||
};
|
||||
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, pp<uint8_t> const& p) {
|
||||
return out << (unsigned)p.n;
|
||||
}
|
||||
|
||||
template<typename Numeral>
|
||||
inline std::ostream& operator<<(std::ostream& out, pp<Numeral> const& p) {
|
||||
if ((Numeral)(0 - p.n) < p.n)
|
||||
return out << "-" << (Numeral)(0 - p.n);
|
||||
return out << p.n;
|
||||
}
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, pp<rational> const& p) {
|
||||
return out << p.n;
|
||||
}
|
||||
|
||||
template<typename Numeral>
|
||||
class mod_interval {
|
||||
bool emp = false;
|
||||
public:
|
||||
Numeral lo { 0 };
|
||||
Numeral hi { 0 };
|
||||
mod_interval() {}
|
||||
mod_interval(Numeral const& l, Numeral const& h): lo(l), hi(h) {}
|
||||
virtual ~mod_interval() {}
|
||||
static mod_interval free() { return mod_interval(0, 0); }
|
||||
static mod_interval empty() { mod_interval i(0, 0); i.emp = true; return i; }
|
||||
|
||||
bool is_free() const { return !emp && lo == hi; }
|
||||
bool is_empty() const { return emp; }
|
||||
bool is_singleton() const { return !is_empty() && (lo + 1 == hi || (hi == 0 && is_max(lo))); }
|
||||
bool contains(Numeral const& n) const;
|
||||
bool contains(mod_interval const& other) const;
|
||||
virtual bool is_max(Numeral const& n) const { return (Numeral)(n + 1) == 0; }
|
||||
Numeral max() const;
|
||||
Numeral min() const;
|
||||
|
||||
void set_free() { lo = hi = 0; emp = false; }
|
||||
void set_bounds(Numeral const& l, Numeral const& h) { lo = l; hi = h; }
|
||||
void set_empty() { emp = true; }
|
||||
|
||||
mod_interval& intersect_ule(Numeral const& h);
|
||||
mod_interval& intersect_uge(Numeral const& l);
|
||||
mod_interval& intersect_ult(Numeral const& h);
|
||||
mod_interval& intersect_ugt(Numeral const& l);
|
||||
mod_interval& intersect_fixed(Numeral const& n);
|
||||
mod_interval& intersect_diff(Numeral const& n);
|
||||
mod_interval& update_lo(Numeral const& new_lo);
|
||||
mod_interval& update_hi(Numeral const& new_hi);
|
||||
|
||||
mod_interval operator&(mod_interval const& other) const;
|
||||
mod_interval operator+(mod_interval const& other) const;
|
||||
mod_interval operator-(mod_interval const& other) const;
|
||||
mod_interval operator*(mod_interval const& other) const;
|
||||
mod_interval operator-() const;
|
||||
mod_interval operator*(Numeral const& n) const;
|
||||
mod_interval operator+(Numeral const& n) const { return mod_interval(lo + n, hi + n); }
|
||||
mod_interval operator-(Numeral const& n) const { return mod_interval(lo - n, hi - n); }
|
||||
mod_interval& operator+=(mod_interval const& other) { *this = *this + other; return *this; }
|
||||
std::ostream& display(std::ostream& out) const {
|
||||
if (is_empty()) return out << "empty";
|
||||
if (is_free()) return out << "free";
|
||||
return out << "[" << pp(lo) << ", " << pp(hi) << "[";
|
||||
}
|
||||
Numeral closest_value(Numeral const& n) const;
|
||||
bool operator==(mod_interval const& other) const {
|
||||
if (is_empty())
|
||||
return other.is_empty();
|
||||
if (is_free())
|
||||
return other.is_free();
|
||||
return lo == other.lo && hi == other.hi;
|
||||
}
|
||||
bool operator!=(mod_interval const& other) const {
|
||||
return !(*this == other);
|
||||
}
|
||||
};
|
||||
|
||||
template<typename Numeral>
|
||||
inline std::ostream& operator<<(std::ostream& out, mod_interval<Numeral> const& i) {
|
||||
return i.display(out);
|
||||
}
|
||||
|
||||
|
|
@ -1,333 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
mod_interval_def.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Intervals over fixed precision modular arithmetic
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-19
|
||||
Jakob Rath 2021-04-6
|
||||
|
||||
--*/
|
||||
|
||||
#pragma once
|
||||
|
||||
#include "fixplex_mod_interval.h"
|
||||
|
||||
template<typename Numeral>
|
||||
bool mod_interval<Numeral>::contains(Numeral const& n) const {
|
||||
if (is_empty())
|
||||
return false;
|
||||
if (is_free())
|
||||
return true;
|
||||
if (lo < hi)
|
||||
return lo <= n && n < hi;
|
||||
else
|
||||
return lo <= n || n < hi;
|
||||
}
|
||||
|
||||
template<typename Numeral>
|
||||
bool mod_interval<Numeral>::contains(mod_interval const& other) const {
|
||||
if (is_empty())
|
||||
return other.is_empty();
|
||||
if (is_free())
|
||||
return true;
|
||||
if (hi == 0)
|
||||
return lo <= other.lo && (other.lo < other.hi || other.hi == 0);
|
||||
if (lo < hi)
|
||||
return lo <= other.lo && other.hi <= hi;
|
||||
if (other.lo < other.hi && other.hi <= hi)
|
||||
return true;
|
||||
if (other.lo < other.hi && lo <= other.lo)
|
||||
return true;
|
||||
if (other.hi == 0)
|
||||
return lo <= other.lo;
|
||||
SASSERT(other.hi < other.lo && other.hi != 0);
|
||||
SASSERT(hi < lo && hi != 0);
|
||||
return lo <= other.lo && other.hi <= hi;
|
||||
}
|
||||
|
||||
template<typename Numeral>
|
||||
mod_interval<Numeral> mod_interval<Numeral>::operator+(mod_interval<Numeral> const& other) const {
|
||||
if (is_empty())
|
||||
return *this;
|
||||
if (other.is_empty())
|
||||
return other;
|
||||
if (is_free())
|
||||
return *this;
|
||||
if (other.is_free())
|
||||
return other;
|
||||
Numeral sz = (hi - lo) + (other.hi - other.lo);
|
||||
if (sz < (hi - lo))
|
||||
return mod_interval::free();
|
||||
return mod_interval(lo + other.lo, hi + other.hi);
|
||||
}
|
||||
|
||||
template<typename Numeral>
|
||||
mod_interval<Numeral> mod_interval<Numeral>::operator-(mod_interval<Numeral> const& other) const {
|
||||
return *this + (-other);
|
||||
}
|
||||
|
||||
template<typename Numeral>
|
||||
mod_interval<Numeral> mod_interval<Numeral>::operator-() const {
|
||||
if (is_empty())
|
||||
return *this;
|
||||
if (is_free())
|
||||
return *this;
|
||||
return mod_interval(1 - hi, 1 - lo);
|
||||
}
|
||||
|
||||
template<typename Numeral>
|
||||
mod_interval<Numeral> mod_interval<Numeral>::operator*(Numeral const& n) const {
|
||||
if (is_empty())
|
||||
return *this;
|
||||
if (n == 0)
|
||||
return mod_interval(0, 1);
|
||||
if (n == 1)
|
||||
return *this;
|
||||
if (is_free())
|
||||
return *this;
|
||||
Numeral sz = hi - lo;
|
||||
if (0 - n < n) {
|
||||
Numeral mn = 0 - n;
|
||||
Numeral mz = mn * sz;
|
||||
if (mz / mn != sz)
|
||||
return mod_interval::free();
|
||||
return mod_interval((hi - 1) * n, n * lo + 1);
|
||||
}
|
||||
else {
|
||||
Numeral mz = n * sz;
|
||||
if (mz / n != sz)
|
||||
return mod_interval::free();
|
||||
return mod_interval(n * lo, n * (hi - 1) + 1);
|
||||
}
|
||||
}
|
||||
|
||||
template<typename Numeral>
|
||||
mod_interval<Numeral> mod_interval<Numeral>::operator&(mod_interval const& other) const {
|
||||
Numeral l, h;
|
||||
if (is_free() || other.is_empty())
|
||||
return other;
|
||||
if (other.is_free() || is_empty())
|
||||
return *this;
|
||||
|
||||
if (lo < hi || hi == 0) {
|
||||
if (other.lo < other.hi || other.hi == 0) {
|
||||
if (hi != 0 && hi <= other.lo)
|
||||
return mod_interval::empty();
|
||||
if (other.hi != 0 && other.hi <= lo)
|
||||
return mod_interval::empty();
|
||||
l = lo >= other.lo ? lo : other.lo;
|
||||
h = hi == 0 ? other.hi : (other.hi == 0 ? hi : (hi <= other.hi ? hi : other.hi));
|
||||
return mod_interval(l, h);
|
||||
}
|
||||
SASSERT(0 < other.hi && other.hi < other.lo);
|
||||
if (other.lo <= lo)
|
||||
return *this;
|
||||
if (other.hi <= lo && lo < hi && hi <= other.lo)
|
||||
return mod_interval::empty();
|
||||
if (lo <= other.hi && other.hi <= hi && hi <= other.lo)
|
||||
return mod_interval(lo, other.hi);
|
||||
if (hi == 0 && lo < other.hi)
|
||||
return *this;
|
||||
if (hi == 0 && other.hi <= lo)
|
||||
return mod_interval(other.lo, hi);
|
||||
if (other.hi <= lo && other.hi <= hi)
|
||||
return mod_interval(other.lo, hi);
|
||||
return *this;
|
||||
}
|
||||
SASSERT(hi < lo);
|
||||
if (other.lo < other.hi || other.hi == 0)
|
||||
return other & *this;
|
||||
SASSERT(other.hi < other.lo);
|
||||
SASSERT(hi != 0);
|
||||
SASSERT(other.hi != 0);
|
||||
if (lo <= other.hi)
|
||||
return *this;
|
||||
if (other.lo <= hi)
|
||||
return other;
|
||||
l = lo <= other.lo ? other.lo : lo;
|
||||
h = hi >= other.hi ? other.hi : hi;
|
||||
return mod_interval(l, h);
|
||||
|
||||
}
|
||||
|
||||
template<typename Numeral>
|
||||
Numeral mod_interval<Numeral>::max() const {
|
||||
if (lo < hi)
|
||||
return hi - 1;
|
||||
else
|
||||
return Numeral(0) - 1;
|
||||
}
|
||||
|
||||
template<typename Numeral>
|
||||
Numeral mod_interval<Numeral>::min() const {
|
||||
if (lo < hi || hi == 0)
|
||||
return lo;
|
||||
else
|
||||
return Numeral(0);
|
||||
}
|
||||
|
||||
|
||||
template<typename Numeral>
|
||||
Numeral mod_interval<Numeral>::closest_value(Numeral const& n) const {
|
||||
if (contains(n))
|
||||
return n;
|
||||
if (is_empty())
|
||||
return n;
|
||||
if ((Numeral)(lo - n) < (Numeral)(n - hi))
|
||||
return lo;
|
||||
return hi - 1;
|
||||
}
|
||||
|
||||
template<typename Numeral>
|
||||
mod_interval<Numeral>& mod_interval<Numeral>::intersect_uge(Numeral const& l) {
|
||||
if (is_empty())
|
||||
return *this;
|
||||
if (lo < hi && hi <= l)
|
||||
set_empty();
|
||||
else if (is_free())
|
||||
lo = l, hi = 0;
|
||||
else if ((lo < hi || hi == 0) && lo < l)
|
||||
lo = l;
|
||||
else if (hi < lo && hi <= l && l <= lo)
|
||||
hi = 0;
|
||||
else if (hi < lo && lo < l)
|
||||
hi = 0, lo = l;
|
||||
else if (0 < l && l < hi && hi < lo)
|
||||
lo = l, hi = 0;
|
||||
return *this;
|
||||
}
|
||||
|
||||
template<typename Numeral>
|
||||
mod_interval<Numeral>& mod_interval<Numeral>::intersect_ugt(Numeral const& l) {
|
||||
if (is_empty())
|
||||
return *this;
|
||||
if (is_max(l))
|
||||
set_empty();
|
||||
else if (is_free())
|
||||
lo = l + 1, hi = 0;
|
||||
else if (lo < hi && hi - 1 <= l)
|
||||
set_empty();
|
||||
else if (lo < hi && l < lo)
|
||||
return *this;
|
||||
else if (lo < hi)
|
||||
lo = l + 1;
|
||||
else if (hi < lo && hi <= l + 1 && l < lo)
|
||||
hi = 0;
|
||||
else if (hi < lo && lo <= l)
|
||||
hi = 0, lo = l + 1;
|
||||
else if (l <= hi && hi < lo)
|
||||
lo = l + 1, hi = 0;
|
||||
return *this;
|
||||
}
|
||||
|
||||
template<typename Numeral>
|
||||
mod_interval<Numeral>& mod_interval<Numeral>::intersect_ule(Numeral const& h) {
|
||||
if (is_empty())
|
||||
return *this;
|
||||
if (is_max(h))
|
||||
return *this;
|
||||
else if (is_free())
|
||||
lo = 0, hi = h + 1;
|
||||
else if (h < lo && (lo < hi || hi == 0))
|
||||
set_empty();
|
||||
else if (hi == 0 && h >= lo)
|
||||
hi = h + 1;
|
||||
else if (lo <= h && h + 1 < hi)
|
||||
hi = h + 1;
|
||||
else if (h < hi && hi < lo)
|
||||
hi = h + 1, lo = 0;
|
||||
else if (hi <= h && h < lo)
|
||||
lo = 0;
|
||||
else if (hi == 0 && hi == h && hi < lo)
|
||||
set_empty();
|
||||
else if (0 < hi && hi == h && hi < lo)
|
||||
lo = 0;
|
||||
else if (0 < hi && hi < h && hi < lo)
|
||||
lo = 0, hi = h + 1;
|
||||
return *this;
|
||||
}
|
||||
|
||||
template<typename Numeral>
|
||||
mod_interval<Numeral>& mod_interval<Numeral>::intersect_ult(Numeral const& h) {
|
||||
if (is_empty())
|
||||
return *this;
|
||||
if (h == 0)
|
||||
set_empty();
|
||||
else if (is_free())
|
||||
lo = 0, hi = h;
|
||||
else if (h <= lo && (lo < hi || hi == 0))
|
||||
set_empty();
|
||||
else if (h > lo && (h < hi || hi == 0))
|
||||
hi = h;
|
||||
else if (hi < lo && h <= hi)
|
||||
hi = h, lo = 0;
|
||||
else if (hi < h && h <= lo)
|
||||
lo = 0;
|
||||
else if (0 < hi && hi < lo && hi + 1 <= h)
|
||||
lo = 0, hi = h;
|
||||
return *this;
|
||||
}
|
||||
|
||||
|
||||
template<typename Numeral>
|
||||
mod_interval<Numeral>& mod_interval<Numeral>::intersect_fixed(Numeral const& a) {
|
||||
if (is_empty())
|
||||
return *this;
|
||||
if (!contains(a))
|
||||
set_empty();
|
||||
else if (is_max(a))
|
||||
lo = a, hi = 0;
|
||||
else
|
||||
lo = a, hi = a + 1;
|
||||
return *this;
|
||||
}
|
||||
|
||||
template<typename Numeral>
|
||||
mod_interval<Numeral>& mod_interval<Numeral>::intersect_diff(Numeral const& a) {
|
||||
if (!contains(a) || is_empty())
|
||||
return *this;
|
||||
if (a == lo && a + 1 == hi)
|
||||
set_empty();
|
||||
else if (a == lo && hi == 0 && is_max(a))
|
||||
set_empty();
|
||||
else if (is_free())
|
||||
lo = a + 1, hi = a;
|
||||
else if (0 < hi && hi < lo && a == lo)
|
||||
return *this;
|
||||
else if (a == lo && !is_max(a))
|
||||
lo = a + 1;
|
||||
else if (a + 1 == hi)
|
||||
hi = a;
|
||||
else if (hi == 0 && is_max(a))
|
||||
hi = a;
|
||||
|
||||
return *this;
|
||||
}
|
||||
|
||||
template<typename Numeral>
|
||||
mod_interval<Numeral>& mod_interval<Numeral>::update_lo(Numeral const& new_lo) {
|
||||
SASSERT(lo <= new_lo);
|
||||
if (lo < hi && hi <= new_lo)
|
||||
set_empty();
|
||||
else
|
||||
lo = new_lo;
|
||||
return *this;
|
||||
}
|
||||
|
||||
template<typename Numeral>
|
||||
mod_interval<Numeral>& mod_interval<Numeral>::update_hi(Numeral const& new_hi) {
|
||||
SASSERT(new_hi <= hi);
|
||||
if (new_hi <= lo && lo < hi)
|
||||
set_empty();
|
||||
else
|
||||
hi = new_hi;
|
||||
return *this;
|
||||
}
|
||||
|
|
@ -1,288 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
linear_solver.cpp
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-05-14
|
||||
Jakob Rath 2021-05-14
|
||||
|
||||
--*/
|
||||
|
||||
#include "math/bigfix/u256.h"
|
||||
#include "math/polysat/linear_solver.h"
|
||||
#include "math/polysat/fixplex_def.h"
|
||||
#include "math/polysat/solver.h"
|
||||
|
||||
inline unsigned numeral2hash(u256 const& n) { return n.hash(); }
|
||||
|
||||
namespace polysat {
|
||||
|
||||
void linear_solver::push() {
|
||||
m_trail.push_back(trail_i::inc_level_i);
|
||||
for (auto* f : m_fix_ptr)
|
||||
f->push();
|
||||
}
|
||||
|
||||
void linear_solver::pop(unsigned n) {
|
||||
for (auto* f : m_fix_ptr)
|
||||
f->pop(n);
|
||||
while (n > 0) {
|
||||
switch (m_trail.back()) {
|
||||
case trail_i::inc_level_i:
|
||||
--n;
|
||||
break;
|
||||
case trail_i::add_var_i: {
|
||||
auto [v, sz] = m_rows.back();
|
||||
--m_sz2num_vars[sz];
|
||||
m_rows.pop_back();
|
||||
break;
|
||||
}
|
||||
case trail_i::add_mono_i: {
|
||||
auto m = m_monomials.back();
|
||||
m_mono2var.erase(m);
|
||||
m_alloc.deallocate(m.num_vars*sizeof(unsigned), m.vars);
|
||||
m_monomials.pop_back();
|
||||
break;
|
||||
}
|
||||
case trail_i::set_active_i:
|
||||
m_active.pop_back();
|
||||
break;
|
||||
|
||||
default:
|
||||
UNREACHABLE();
|
||||
}
|
||||
m_trail.pop_back();
|
||||
}
|
||||
m_unsat_f = nullptr;
|
||||
}
|
||||
|
||||
fixplex_base* linear_solver::sz2fixplex(unsigned sz) {
|
||||
fixplex_base* b = m_fix.get(sz, nullptr);
|
||||
if (!b) {
|
||||
switch (sz) {
|
||||
case 8:
|
||||
b = alloc(fixplex<generic_uint_ext<unsigned char>>, s.params(), s.m_lim);
|
||||
break;
|
||||
case 16:
|
||||
b = alloc(fixplex<generic_uint_ext<unsigned short>>, s.params(), s.m_lim);
|
||||
break;
|
||||
case 32:
|
||||
b = alloc(fixplex<generic_uint_ext<unsigned>>, s.params(), s.m_lim);
|
||||
break;
|
||||
case 64:
|
||||
b = alloc(fixplex<uint64_ext>, s.params(), s.m_lim);
|
||||
break;
|
||||
case 128:
|
||||
NOT_IMPLEMENTED_YET();
|
||||
break;
|
||||
case 256:
|
||||
b = alloc(fixplex<generic_uint_ext<u256>>, s.params(), s.m_lim);
|
||||
break;
|
||||
default:
|
||||
NOT_IMPLEMENTED_YET();
|
||||
break;
|
||||
}
|
||||
if (b)
|
||||
m_fix_ptr.push_back(b);
|
||||
m_fix.set(sz, b);
|
||||
}
|
||||
return b;
|
||||
}
|
||||
|
||||
|
||||
var_t linear_solver::internalize_pdd(pdd const& p) {
|
||||
unsigned sz = p.power_of_2();
|
||||
linearize(p);
|
||||
if (m_vars.size() == 1 && m_coeffs.back() == 1)
|
||||
return m_vars.back();
|
||||
var_t v = fresh_var(sz);
|
||||
m_vars.push_back(v);
|
||||
m_coeffs.push_back(rational::power_of_two(sz) - 1);
|
||||
auto* f = sz2fixplex(sz);
|
||||
if (f)
|
||||
f->add_row(v, m_vars.size(), m_vars.data(), m_coeffs.data());
|
||||
return v;
|
||||
}
|
||||
|
||||
/**
|
||||
* create the row c.p() - v == 0
|
||||
* when equality is asserted, set range on v as v == 0 or v > 0.
|
||||
*/
|
||||
|
||||
|
||||
|
||||
void linear_solver::new_le(ule_constraint& c) {
|
||||
var_t v = internalize_pdd(c.lhs());
|
||||
var_t w = internalize_pdd(c.rhs());
|
||||
auto pr = std::make_pair(v, w);
|
||||
m_bool_var2row.setx(c.bvar(), pr, pr);
|
||||
}
|
||||
|
||||
//
|
||||
// v <= w:
|
||||
// static constraints:
|
||||
// - lo(v) <= lo(w)
|
||||
// - hi(v) <= hi(w)
|
||||
//
|
||||
// special case for inequalities with constant bounds
|
||||
// bounds propagation on fp, then bounds strengthening
|
||||
// based on static constraints
|
||||
// internal backtrack search over bounds
|
||||
// inequality graph (with offsets)
|
||||
//
|
||||
|
||||
void linear_solver::assert_le(bool is_positive, ule_constraint& c) {
|
||||
auto [v, w] = m_bool_var2row[c.bvar()];
|
||||
unsigned sz = c.lhs().power_of_2();
|
||||
auto* fp = sz2fixplex(sz);
|
||||
if (!fp)
|
||||
return;
|
||||
unsigned c_dep = constraint_idx2dep(m_active.size() - 1);
|
||||
rational z(0);
|
||||
if (c.rhs().is_val()) {
|
||||
bool is_max_value = false;
|
||||
if (is_positive)
|
||||
// v <= rhs
|
||||
fp->set_bounds(v, z, c.rhs().val(), c_dep);
|
||||
else if (is_max_value)
|
||||
throw default_exception("conflict not implemented");
|
||||
else
|
||||
// rhs < v
|
||||
fp->set_bounds(v, c.rhs().val() + 1, z, c_dep);
|
||||
return;
|
||||
}
|
||||
|
||||
if (c.lhs().is_val()) {
|
||||
if (is_positive)
|
||||
// w >= lhs
|
||||
fp->set_bounds(w, c.lhs().val(), z, c_dep);
|
||||
else if (c.lhs().val() == 0)
|
||||
throw default_exception("conflict not implemented");
|
||||
else
|
||||
// w < lhs
|
||||
fp->set_bounds(w, z, c.lhs().val() - 1, c_dep);
|
||||
return;
|
||||
}
|
||||
|
||||
if (is_positive)
|
||||
fp->add_le(v, w, c_dep);
|
||||
else
|
||||
fp->add_lt(w, v, c_dep);
|
||||
}
|
||||
|
||||
|
||||
void linear_solver::new_constraint(constraint& c) {
|
||||
if (c.is_ule())
|
||||
new_le(c.to_ule());
|
||||
}
|
||||
|
||||
void linear_solver::activate_constraint(bool is_positive, constraint& c) {
|
||||
if (!c.is_ule())
|
||||
return;
|
||||
m_active.push_back(&c);
|
||||
m_trail.push_back(trail_i::set_active_i);
|
||||
assert_le(is_positive, c.to_ule());
|
||||
}
|
||||
|
||||
void linear_solver::linearize(pdd const& p) {
|
||||
unsigned sz = p.power_of_2();
|
||||
m_vars.reset();
|
||||
m_coeffs.reset();
|
||||
for (auto const& m : p) {
|
||||
m_vars.push_back(mono2var(sz, m.vars));
|
||||
m_coeffs.push_back(m.coeff);
|
||||
}
|
||||
}
|
||||
|
||||
var_t linear_solver::mono2var(unsigned sz, unsigned_vector const& var) {
|
||||
mono_info m(sz, var.size(), var.data()), m1;
|
||||
if (m_mono2var.find(m, m1))
|
||||
return m1.var;
|
||||
m.vars = static_cast<unsigned*>(m_alloc.allocate(var.size()*sizeof(unsigned)));
|
||||
for (unsigned i = 0; i < var.size(); ++i)
|
||||
m.vars[i] = var[i];
|
||||
m.var = fresh_var(sz);
|
||||
m_mono2var.insert(m);
|
||||
m_monomials.push_back(m);
|
||||
m_trail.push_back(trail_i::add_mono_i);
|
||||
return m.var;
|
||||
}
|
||||
|
||||
var_t linear_solver::pvar2var(unsigned sz, pvar v) {
|
||||
unsigned_vector vars;
|
||||
vars.push_back(v);
|
||||
return mono2var(sz, vars);
|
||||
}
|
||||
|
||||
var_t linear_solver::fresh_var(unsigned sz) {
|
||||
m_sz2num_vars.reserve(sz + 1);
|
||||
m_trail.push_back(trail_i::add_var_i);
|
||||
m_rows.push_back(std::make_pair(0, sz));
|
||||
return m_sz2num_vars[sz]++;
|
||||
}
|
||||
|
||||
void linear_solver::set_value(pvar v, rational const& value, unsigned dep) {
|
||||
unsigned sz = s.size(v);
|
||||
auto* fp = sz2fixplex(sz);
|
||||
if (!fp)
|
||||
return;
|
||||
var_t w = pvar2var(sz, v);
|
||||
fp->set_value(w, value, external_dep2dep(dep));
|
||||
}
|
||||
|
||||
void linear_solver::set_bound(pvar v, rational const& lo, rational const& hi, unsigned dep) {
|
||||
unsigned sz = s.size(v);
|
||||
auto* fp = sz2fixplex(sz);
|
||||
if (!fp)
|
||||
return;
|
||||
var_t w = pvar2var(sz, v);
|
||||
fp->set_bounds(w, lo, hi, external_dep2dep(dep));
|
||||
}
|
||||
|
||||
/**
|
||||
* check integer modular feasibility under current bounds.
|
||||
* and inequalities
|
||||
*/
|
||||
lbool linear_solver::check() {
|
||||
lbool res = l_true;
|
||||
m_unsat_f = nullptr;
|
||||
for (auto* fp : m_fix_ptr) {
|
||||
lbool r = fp->make_feasible();
|
||||
if (r == l_false) {
|
||||
m_unsat_f = fp;
|
||||
return r;
|
||||
}
|
||||
if (r == l_undef)
|
||||
res = l_undef;
|
||||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
void linear_solver::unsat_core(ptr_vector<constraint>& cs, unsigned_vector& deps) {
|
||||
SASSERT(m_unsat_f);
|
||||
deps.reset();
|
||||
cs.reset();
|
||||
for (unsigned dep : m_unsat_f->get_unsat_core()) {
|
||||
if (is_constraint_dep(dep))
|
||||
cs.push_back(m_active[dep2constraint_idx(dep)]);
|
||||
else
|
||||
deps.push_back(dep2external_dep(dep));
|
||||
}
|
||||
}
|
||||
|
||||
// current value assigned to (linear) variable according to tableau.
|
||||
bool linear_solver::value(pvar v, rational& val) {
|
||||
unsigned sz = s.size(v);
|
||||
auto* fp = sz2fixplex(sz);
|
||||
if (!fp)
|
||||
return false;
|
||||
val = fp->get_value(pvar2var(sz, v));
|
||||
return true;
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
|
|
@ -1,144 +0,0 @@
|
|||
/*++
|
||||
Copyright (c) 2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
linear_solver.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Fixed-precision unsigned integer linear solver
|
||||
|
||||
This wraps around fixplex and translates polynomials
|
||||
into linear form.
|
||||
Equalities, Inequalities are converted into rows and slack variables.
|
||||
Slack variables are bounded when constraints are activated.
|
||||
It also handles backtracking state: bounds that are activated inside one
|
||||
scope are de-activated when exiting the scope.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-05-14
|
||||
Jakob Rath 2021-05-14
|
||||
|
||||
--*/
|
||||
|
||||
#pragma once
|
||||
|
||||
#include "util/hashtable.h"
|
||||
#include "util/small_object_allocator.h"
|
||||
#include "math/polysat/fixplex.h"
|
||||
#include "math/polysat/constraint.h"
|
||||
#include "math/polysat/ule_constraint.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
class solver;
|
||||
|
||||
class linear_solver {
|
||||
enum trail_i {
|
||||
inc_level_i,
|
||||
add_var_i,
|
||||
add_mono_i,
|
||||
set_active_i
|
||||
};
|
||||
|
||||
struct mono_info {
|
||||
unsigned sz { 0 };
|
||||
unsigned num_vars { 0 };
|
||||
unsigned* vars { nullptr };
|
||||
unsigned var { 0 };
|
||||
mono_info(unsigned sz, unsigned num_vars, unsigned* vars):
|
||||
sz(sz),
|
||||
num_vars(num_vars),
|
||||
vars(vars)
|
||||
{}
|
||||
mono_info() {}
|
||||
struct hash {
|
||||
unsigned operator()(mono_info const& i) const {
|
||||
// TODO
|
||||
return 0;
|
||||
}
|
||||
};
|
||||
struct eq {
|
||||
bool operator()(mono_info const& a, mono_info const& b) const {
|
||||
if (a.num_vars != b.num_vars)
|
||||
return false;
|
||||
for (unsigned i = 0; i < a.num_vars; ++i)
|
||||
if (a.vars[i] != b.vars[i])
|
||||
return false;
|
||||
return a.sz == b.sz;
|
||||
}
|
||||
};
|
||||
};
|
||||
|
||||
solver& s;
|
||||
scoped_ptr_vector<fixplex_base> m_fix;
|
||||
ptr_vector<fixplex_base> m_fix_ptr;
|
||||
svector<trail_i> m_trail;
|
||||
svector<std::pair<var_t, unsigned>> m_rows;
|
||||
unsigned_vector m_var2ext;
|
||||
unsigned_vector m_ext2var;
|
||||
ptr_vector<constraint> m_active;
|
||||
|
||||
svector<var_t> m_vars;
|
||||
vector<rational> m_coeffs;
|
||||
svector<std::pair<var_t, var_t>> m_bool_var2row;
|
||||
|
||||
hashtable<mono_info, mono_info::hash, mono_info::eq> m_mono2var;
|
||||
unsigned_vector m_sz2num_vars;
|
||||
small_object_allocator m_alloc;
|
||||
svector<mono_info> m_monomials;
|
||||
fixplex_base* m_unsat_f = nullptr;
|
||||
|
||||
fixplex_base* sz2fixplex(unsigned sz);
|
||||
|
||||
void linearize(pdd const& p);
|
||||
var_t fresh_var(unsigned sz);
|
||||
|
||||
var_t internalize_pdd(pdd const& p);
|
||||
void new_le(ule_constraint& le);
|
||||
void assert_le(bool is_positive, ule_constraint& le);
|
||||
|
||||
// bind monomial to variable.
|
||||
var_t mono2var(unsigned sz, unsigned_vector const& m);
|
||||
var_t pvar2var(unsigned sz, pvar v);
|
||||
// unsigned_vector var2mono(unsigned sz, var_t v) { throw default_exception("nyi"); }
|
||||
|
||||
// distinguish constraint and justification dependencies
|
||||
unsigned external_dep2dep(unsigned dep) const { return dep * 2; }
|
||||
unsigned constraint_idx2dep(unsigned idx) const { return 1 + (idx * 2); }
|
||||
bool is_constraint_dep(unsigned dep) const { return 0 != (dep & 0x1); }
|
||||
unsigned dep2constraint_idx(unsigned dep) const { return dep >> 2; }
|
||||
unsigned dep2external_dep(unsigned dep) const { return dep >> 2; }
|
||||
|
||||
public:
|
||||
linear_solver(solver& s):
|
||||
s(s),
|
||||
m_alloc("mononials")
|
||||
{}
|
||||
|
||||
void push();
|
||||
void pop(unsigned n);
|
||||
void new_constraint(constraint& c);
|
||||
void set_value(pvar v, rational const& value, unsigned dep);
|
||||
void set_bound(pvar v, rational const& lo, rational const& hi, unsigned dep);
|
||||
void activate_constraint(bool is_positive, constraint& c);
|
||||
void activate_constraint(signed_constraint c) { activate_constraint(c.is_positive(), *c.get()); }
|
||||
|
||||
// check integer modular feasibility under current bounds.
|
||||
lbool check();
|
||||
void unsat_core(ptr_vector<constraint>& constraints, unsigned_vector& deps);
|
||||
|
||||
// current value assigned to (linear) variable according to tableau.
|
||||
bool value(pvar v, rational& val);
|
||||
|
||||
std::ostream& display(std::ostream& out) const { return out; }
|
||||
void collect_statistics(::statistics & st) const {}
|
||||
|
||||
};
|
||||
|
||||
|
||||
|
||||
};
|
||||
|
||||
|
|
@ -15,6 +15,8 @@ Author:
|
|||
|
||||
Revision History:
|
||||
|
||||
NSB: I made util/var_queue.h a template. You can feed it a struct comprising of size/activity.
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
|
||||
|
|
|
|||
|
|
@ -139,7 +139,6 @@ namespace polysat {
|
|||
friend class inference_engine;
|
||||
friend class file_inference_logger;
|
||||
friend class forbidden_intervals;
|
||||
friend class linear_solver;
|
||||
friend class viable;
|
||||
friend class viable_fallback;
|
||||
friend class search_state;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue