mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

scenario saving

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-08-13 11:01:07 -07:00
parent bd2e73014c
commit 60dbfed69e
5 changed files with 61 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/math/polysat/fixplex.h
View file

@ -28,6 +28,7 @@ Author:
#include "util/uint_set.h"
#include "util/dependency.h"
#include "util/ref.h"
#include "util/params.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); }
@ -55,6 +56,7 @@ namespace polysat {
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;
};
@ -170,14 +172,15 @@ namespace polysat {
reslimit& m_limit;
mutable manager m;
mutable matrix M;
unsigned m_max_iterations { UINT_MAX };
unsigned m_num_non_integral { 0 };
unsigned m_max_iterations = UINT_MAX;
unsigned m_num_non_integral = 0;
var_heap m_to_patch;
vector<var_info> m_vars;
vector<row_info> m_rows;
vector<var_eq> m_var_eqs;
bool m_bland { false };
unsigned m_blands_rule_threshold { 1000 };
bool m_bland = false ;
unsigned m_blands_rule_threshold = 1000;
var_t m_last_pivot_var = null_var;
random_gen m_random;
uint_set m_left_basis;
unsigned_vector m_unsat_core;
@ -198,16 +201,19 @@ namespace polysat {
svector<var_t> m_vars_to_untouch;
public:
fixplex(reslimit& lim):
fixplex(params_ref const& p, reslimit& lim):
m_limit(lim),
M(m),
m_to_patch(1024) {}
m_to_patch(1024) {
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;

14
src/math/polysat/fixplex_def.h
View file

@ -82,6 +82,12 @@ namespace polysat {
reset();
}
template<typename Ext>
void fixplex<Ext>::updt_params(params_ref const& p) {
m_max_iterations = p.get_uint("max_iterations", m_max_iterations);
}
template<typename Ext>
void fixplex<Ext>::push() {
m_trail.push_back(trail_i::inc_level_i);
@ -145,6 +151,7 @@ namespace polysat {
return l_false;
++m_stats.m_num_checks;
m_left_basis.reset();
m_last_pivot_var = null_var;
unsigned num_iterations = 0;
unsigned num_repeated = 0;
var_t v = null_var;
@ -407,6 +414,8 @@ namespace polysat {
numeral const& b = r.coeff();
if (x == y)
continue;
if (y == m_last_pivot_var)
continue;
if (!has_minimal_trailing_zeros(y, b))
continue;
numeral new_y_value = solve_for(row_value - b * value(y), b);
@ -469,7 +478,7 @@ namespace polysat {
row r = base2row(x);
for (auto const& c : M.col_entries(r)) {
var_t y = c.var();
if (x == y || y >= result)
if (x == y || y >= result || y == m_last_pivot_var)
continue;
numeral const& b = c.coeff();
if (can_improve(y, b)) {
@ -798,7 +807,8 @@ namespace polysat {
*/
template<typename Ext>
void fixplex<Ext>::pivot(var_t x, var_t y, numeral const& b, numeral const& new_value) {
++m_stats.m_num_pivots;
++m_stats.m_num_pivots;
m_last_pivot_var = x;
SASSERT(is_base(x));
SASSERT(!is_base(y));
var_info& xI = m_vars[x];

10
src/math/polysat/linear_solver.cpp
View file

@ -64,22 +64,22 @@ namespace polysat {
if (!b) {
switch (sz) {
case 8:
b = alloc(fixplex<generic_uint_ext<unsigned char>>, s.m_lim);
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.m_lim);
b = alloc(fixplex<generic_uint_ext<unsigned short>>, s.params(), s.m_lim);
break;
case 32:
b = alloc(fixplex<generic_uint_ext<unsigned>>, s.m_lim);
b = alloc(fixplex<generic_uint_ext<unsigned>>, s.params(), s.m_lim);
break;
case 64:
b = alloc(fixplex<uint64_ext>, s.m_lim);
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.m_lim);
b = alloc(fixplex<generic_uint_ext<u256>>, s.params(), s.m_lim);
break;
default:
NOT_IMPLEMENTED_YET();

4
src/math/polysat/solver.h
View file

@ -19,6 +19,7 @@ Author:
#include <limits>
#include "util/statistics.h"
#include "util/params.h"
#include "math/polysat/boolean.h"
#include "math/polysat/constraint.h"
#include "math/polysat/clause_builder.h"
@ -60,6 +61,7 @@ namespace polysat {
typedef ptr_vector<constraint> constraints;
reslimit& m_lim;
params_ref m_params;
viable m_viable; // viable sets per variable
scoped_ptr_vector<dd::pdd_manager> m_pdd;
dep_value_manager m_value_manager;
@ -326,6 +328,8 @@ namespace polysat {
void collect_statistics(statistics& st) const;
params_ref& params() { return m_params; }
};
class assignments_pp {

29
src/test/fixplex.cpp
View file

@ -12,10 +12,12 @@ namespace polysat {
typedef uint64_ext::numeral numeral;
struct solver_scope {
params_ref p;
reslimit lim;
};
struct scoped_fp : public solver_scope, public fixplex<uint64_ext> {
scoped_fp(): fixplex<uint64_ext>(lim) {}
scoped_fp(): fixplex<uint64_ext>(p, lim) {}
void run() {
std::cout << *this << "\n";
@ -369,6 +371,27 @@ namespace polysat {
std::cout << "number of failures: " << num_bad << "\n";
}
static void save_scenario(
vector<svector<std::pair<unsigned, uint64_t>>> const& rows,
svector<ineq> const& ineqs,
vector<mod_interval<uint64_t>> const& bounds) {
std::cout << "static void scenario() {";
std::cout << " vector<svector<std::pair<unsigned, uint64_t>>> rows\n;";
std::cout << " svector<ineq> ineqs\n;";
std::cout << " vector<mod_interval<uint64_t>> bounds\n";
for (auto row : rows) {
std::cout << " rows.push_back(svector<std::pair<unsigned, uint64_t>>());\n";
for (auto col : row)
std::cout << " rows.back().push_back(std::make_pair(" << col.first << ", " << col.second << ");\n";
}
for (auto ineq : ineqs)
std::cout << " ineqs.push_back(ineq(" << ineq.v << ", " << ineq.w << " " << ineq.strict << ");\n";
for (auto bound : bounds)
std::cout << " bounds.push_back(mod_interval<uint64_t>(" << bound.lo << ", " << bound.hi << ");\n";
std::cout << " test_lp(rows, ineqs, bounds);\n}\n";
}
static void test_lp(
vector<svector<std::pair<unsigned, uint64_t>>> const& rows,
svector<ineq> const& ineqs,
@ -395,6 +418,10 @@ namespace polysat {
};
scoped_fp fp;
params_ref p;
p.set_uint("max_iterations", 100);
fp.updt_params(p);
for (auto& row : rows) {
vector<rational> coeffs;
svector<var_t> vars;