mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 00:55:31 +00:00
Code Activity

fix polysat params

Browse source
This commit is contained in:
Jakob Rath 2023-08-01 13:40:31 +02:00
parent cd373527ff
commit d943eb4787
6 changed files with 47 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/math/polysat/polysat_params.pyg
View file

@ -1,6 +1,10 @@
def_module_params('polysat',
description='polysat solver',
export=True,
params=(('log_conflicts', BOOL, True, "log conflicts"),
))
def_module_params('polysat',
description='polysat solver',
export=True,
params=(
('max_conflicts', UINT, UINT_MAX, "maximum number of conflicts before giving up"),
('max_decisions', UINT, UINT_MAX, "maximum number of decisions before giving up"),
('log', UINT, UINT_MAX, "polysat logging filter (enable logging in iteration N)"),
('log_conflicts', BOOL, False, "log conflicts"),
)
)

31
src/math/polysat/solver.cpp
View file

@ -36,6 +36,7 @@ TODO: at some point we should add proper garbage collection
#include "math/polysat/polysat_params.hpp"
#include "math/polysat/variable_elimination.h"
#include "math/polysat/polysat_ast.h"
#include "smt/params/smt_params.h"
#include <variant>
#include <filesystem>
@ -45,7 +46,7 @@ TODO: at some point we should add proper garbage collection
namespace polysat {
solver::solver(reslimit& lim):
solver::solver(reslimit& lim, smt_params const& p):
m_lim(lim),
m_viable(*this),
m_viable_fallback(*this),
@ -59,6 +60,8 @@ namespace polysat {
m_names(*this),
m_slicing(*this),
m_search(*this) {
updt_smt_params(p);
updt_polysat_params(gparams::get_module("polysat"));
}
solver::~solver() {
@ -66,20 +69,32 @@ namespace polysat {
m_conflict.reset();
}
void solver::updt_params(params_ref const& p) {
// smt.random_seed, etc.
void solver::updt_smt_params(smt_params const& p) {
m_rand.set_seed(p.m_random_seed);
}
// polysat.max_conflicts, etc.
void solver::updt_polysat_params(params_ref const& p) {
polysat_params pp(p);
m_params.append(p);
m_config.m_max_conflicts = m_params.get_uint("max_conflicts", UINT_MAX);
m_config.m_max_decisions = m_params.get_uint("max_decisions", UINT_MAX);
m_config.m_max_conflicts = pp.max_conflicts();
m_config.m_max_decisions = pp.max_decisions();
m_config.m_log_iteration = pp.log();
m_config.m_log_conflicts = pp.log_conflicts();
m_rand.set_seed(m_params.get_uint("random_seed", 0));
// TODO: log filter to enable/disable based on submodules
if (m_config.m_log_iteration == 0)
set_log_enabled(true);
else
set_log_enabled(false);
}
bool solver::should_search() {
return
m_lim.inc() &&
(m_stats.m_num_conflicts < get_config().m_max_conflicts) &&
(m_stats.m_num_decisions < get_config().m_max_decisions);
(m_stats.m_num_conflicts < config().m_max_conflicts) &&
(m_stats.m_num_decisions < config().m_max_decisions);
}
lbool solver::check_sat() {
@ -90,6 +105,8 @@ namespace polysat {
LOG("Starting");
while (should_search()) {
m_stats.m_num_iterations++;
if (m_stats.m_num_iterations == config().m_log_iteration)
set_log_enabled(true);
LOG_H1("Next solving loop iteration (#" << m_stats.m_num_iterations << ")");
LOG("Free variables: " << m_free_pvars);
LOG("Assignment: " << assignments_pp(*this));

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

@ -39,11 +39,14 @@ Author:
#include <limits>
#include <optional>
struct smt_params;
namespace polysat {
struct config {
uint64_t m_max_conflicts = std::numeric_limits<uint64_t>::max();
uint64_t m_max_decisions = std::numeric_limits<uint64_t>::max();
unsigned m_log_iteration = UINT_MAX;
bool m_log_conflicts = false;
};
@ -149,6 +152,7 @@ namespace polysat {
reslimit& m_lim;
params_ref m_params;
config m_config;
mutable scoped_ptr_vector<dd::pdd_manager> m_pdd;
viable m_viable; // viable sets per variable
@ -162,7 +166,6 @@ namespace polysat {
stats m_stats;
random_gen m_rand;
config m_config;
// Per constraint state
constraint_manager m_constraints;
name_manager m_names;
@ -372,7 +375,7 @@ namespace polysat {
public:
solver(reslimit& lim);
solver(reslimit& lim, smt_params const& p);
~solver();
@ -643,11 +646,10 @@ namespace polysat {
void collect_statistics(statistics& st) const;
void updt_smt_params(smt_params const& p);
void updt_polysat_params(params_ref const& p);
params_ref const & params() const { return m_params; }
void updt_params(params_ref const& p);
config const& get_config() const { return m_config; }
config const& config() const { return m_config; }
}; // class solver

6
src/sat/smt/bv_polysat.cpp
View file

@ -363,8 +363,10 @@ namespace bv {
void solver::polysat_set(euf::theory_var v, pdd const& p) {
#ifndef NDEBUG
expr* e = var2enode(v)->get_expr();
verbose_stream() << "polysat_set: " << expr_ref(e, m) << " -> " << p << std::endl;
IF_VERBOSE(8,
expr* e = var2enode(v)->get_expr();
verbose_stream() << "polysat_set: " << expr_ref(e, m) << " -> " << p << std::endl;
);
#endif
m_var2pdd.reserve(get_num_vars(), p);
m_var2pdd_valid.reserve(get_num_vars(), false);

6
src/sat/smt/bv_solver.cpp
View file

@ -52,17 +52,13 @@ namespace bv {
euf::th_euf_solver(ctx, symbol("bv"), id),
bv(m),
m_autil(m),
m_polysat(m.limit()),
m_polysat(m.limit(), get_config()),
m_ackerman(*this),
m_bb(m, get_config()),
m_find(*this) {
m_bb.set_flat_and_or(false);
}
void solver::updt_params(params_ref const& p) {
m_polysat.updt_params(p);
}
bool solver::is_fixed(euf::theory_var v, expr_ref& val, sat::literal_vector& lits) {
numeral n;
if (!get_fixed_value(v, n))

1
src/sat/smt/bv_solver.h
View file

@ -407,7 +407,6 @@ namespace bv {
public:
solver(euf::solver& ctx, theory_id id);
void updt_params(params_ref const& p) override;
void set_lookahead(sat::lookahead* s) override { }
void init_search() override {}
double get_reward(literal l, sat::ext_constraint_idx idx, sat::literal_occs_fun& occs) const override;