mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

add hook to turn on xor solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-10-28 16:33:30 -07:00
parent 0e651eee04
commit e4f57a13ba
5 changed files with 27 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/sat/sat_params.pyg
View file

@ -62,6 +62,7 @@ def_module_params('sat',
('pb.resolve', SYMBOL, 'cardinality', 'resolution strategy for boolean algebra solver: cardinality, rounding'),
('pb.lemma_format', SYMBOL, 'cardinality', 'generate either cardinality or pb lemmas'),
('euf', BOOL, False, 'enable euf solver (this feature is preliminary and not ready for general consumption)'),
('enable_xor', BOOL, False, 'enable xor solver plugin in combination with pure SAT solving'),
('ddfw_search', BOOL, False, 'use ddfw local search instead of CDCL'),
('ddfw.init_clause_weight', UINT, 8, 'initial clause weight for DDFW local search'),
('ddfw.use_reward_pct', UINT, 15, 'percentage to pick highest reward variable when it has reward 0'),

1
src/sat/smt/CMakeLists.txt
View file

@ -44,6 +44,7 @@ z3_add_component(sat_smt
sat_th.cpp
tseitin_theory_checker.cpp
user_solver.cpp
xor_solver.cpp
COMPONENT_DEPENDENCIES
sat
ast

11
src/sat/smt/xor_solver.cpp
View file

@ -19,9 +19,16 @@ Abstract:
namespace xr {
solver::solver(euf::solver& ctx):
th_solver(ctx.get_manager(), symbol("xor-solver"), ctx.get_manager().get_family_id("xor-solver"))
{}
solver(ctx.get_manager(), ctx.get_si(), ctx.get_manager().get_family_id("xor")) {
m_ctx = &ctx;
}
solver::solver(ast_manager& m, sat::sat_internalizer& si, euf::theory_id id)
: euf::th_solver(m, symbol("xor"), id),
si(si) {
}
euf::th_solver* solver::clone(euf::solver& ctx) {
// and relevant copy internal state

4
src/sat/smt/xor_solver.h
View file

@ -18,9 +18,11 @@ Abstract:
namespace xr {
class solver : public euf::th_solver {
euf::solver* m_ctx = nullptr;
sat::sat_internalizer& si;
public:
solver(euf::solver& ctx);
solver(ast_manager& m, sat::sat_internalizer& si, euf::theory_id id);
th_solver* clone(euf::solver& ctx) override;
sat::literal internalize(expr* e, bool sign, bool root) override { UNREACHABLE(); return sat::null_literal; }

13
src/sat/tactic/goal2sat.cpp
View file

@ -42,6 +42,7 @@ Notes:
#include "sat/sat_drat.h"
#include "sat/tactic/goal2sat.h"
#include "sat/smt/pb_solver.h"
#include "sat/smt/xor_solver.h"
#include "sat/smt/euf_solver.h"
#include "sat/smt/sat_th.h"
#include "sat/sat_params.hpp"
@ -75,6 +76,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
func_decl_ref_vector m_unhandled_funs;
bool m_default_external;
bool m_euf = false;
bool m_xor = false;
bool m_top_level = false;
sat::literal_vector aig_lits;
@ -100,6 +102,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
m_ite_extra = p.get_bool("ite_extra", true);
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
m_euf = sp.euf();
m_xor = sp.enable_xor();
}
void throw_op_not_handled(std::string const& s) {
@ -658,6 +661,14 @@ struct goal2sat::imp : public sat::sat_internalizer {
return m_unhandled_funs;
}
void ensure_xor() {
sat::extension* ext = m_solver.get_extension();
if (ext)
return;
auto* x = alloc(xr::solver, m, *this, m.get_family_id("xor"));
m_solver.set_extension(x);
}
euf::solver* ensure_euf() {
SASSERT(m_euf);
sat::extension* ext = m_solver.get_extension();
@ -950,6 +961,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
expr_ref_vector fmls(m);
if (m_euf)
ensure_euf();
else if (m_xor)
ensure_xor();
for (unsigned idx = 0; idx < size; idx++) {
f = g.form(idx);
// Add assumptions.