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

add parameter class for polysat

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-04-12 10:35:23 +02:00
parent f2b9c27ed6
commit afa7162ab1
4 changed files with 25 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/CMakeLists.txt
View file

@ -28,4 +28,6 @@ z3_add_component(polysat
simplex simplex
interval interval
bigfix bigfix
PYG_FILES
polysat_params.pyg
) )

6
src/math/polysat/polysat_params.pyg Normal file
View file

@ -0,0 +1,6 @@
def_module_params('polysat',
description='polysat solver',
export=True,
params=(('log_conflicts', BOOL, True, "log conflicts"),
))

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

@ -20,6 +20,7 @@ Author:
#include "math/polysat/explain.h" #include "math/polysat/explain.h"
#include "math/polysat/log.h" #include "math/polysat/log.h"
#include "math/polysat/variable_elimination.h" #include "math/polysat/variable_elimination.h"
#include "math/polysat/polysat_params.hpp"
// For development; to be removed once the linear solver works well enough // For development; to be removed once the linear solver works well enough
#define ENABLE_LINEAR_SOLVER 0 #define ENABLE_LINEAR_SOLVER 0
@ -48,16 +49,18 @@ namespace polysat {
} }
void solver::updt_params(params_ref const& p) { void solver::updt_params(params_ref const& p) {
polysat_params pp(p);
m_params.append(p); m_params.append(p);
m_max_conflicts = m_params.get_uint("max_conflicts", UINT_MAX); m_config.m_max_conflicts = m_params.get_uint("max_conflicts", UINT_MAX);
m_max_decisions = m_params.get_uint("max_decisions", UINT_MAX); m_config.m_max_decisions = m_params.get_uint("max_decisions", UINT_MAX);
m_config.m_log_conflicts = pp.log_conflicts();
} }
bool solver::should_search() { bool solver::should_search() {
return return
m_lim.inc() && m_lim.inc() &&
(m_stats.m_num_conflicts < m_max_conflicts) && (m_stats.m_num_conflicts < get_config().m_max_conflicts) &&
(m_stats.m_num_decisions < m_max_decisions); (m_stats.m_num_decisions < get_config().m_max_decisions);
} }
lbool solver::check_sat() { lbool solver::check_sat() {
@ -86,7 +89,7 @@ namespace polysat {
lbool solver::unit_propagate() { lbool solver::unit_propagate() {
return l_undef; return l_undef;
// disabled to allow debugging unsoundness for watched literals // disabled to allow debugging unsoundness for watched literals
flet<uint64_t> _max_d(m_max_conflicts, m_stats.m_num_conflicts + 2); flet<uint64_t> _max_d(m_config.m_max_conflicts, m_stats.m_num_conflicts + 2);
return check_sat(); return check_sat();
} }

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

@ -39,6 +39,12 @@ Author:
namespace polysat { 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();
bool m_log_conflicts = false;
};
class solver { class solver {
struct stats { struct stats {
@ -94,9 +100,7 @@ namespace polysat {
var_queue m_free_pvars; // free poly vars var_queue m_free_pvars; // free poly vars
stats m_stats; stats m_stats;
uint64_t m_max_conflicts = std::numeric_limits<uint64_t>::max(); config m_config;
uint64_t m_max_decisions = std::numeric_limits<uint64_t>::max();
// Per constraint state // Per constraint state
constraint_manager m_constraints; constraint_manager m_constraints;
@ -402,6 +406,8 @@ namespace polysat {
void updt_params(params_ref const& p); void updt_params(params_ref const& p);
config const& get_config() const { return m_config; }
}; // class solver }; // class solver
class assignments_pp { class assignments_pp {