mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
updating default solver selection. Add dt2bv transformation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
a85c5f0fac
commit
56c78753f0
|
@ -156,20 +156,19 @@ namespace opt {
|
|||
symbol const& maxsat_engine = m_c.maxsat_engine();
|
||||
IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";);
|
||||
TRACE("opt", tout << "maxsmt\n";);
|
||||
if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres")) {
|
||||
if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) {
|
||||
m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints);
|
||||
}
|
||||
else if (maxsat_engine == symbol("pd-maxres")) {
|
||||
m_msolver = mk_primal_dual_maxres(m_c, m_index, m_weights, m_soft_constraints);
|
||||
}
|
||||
else {
|
||||
if (maxsat_engine != symbol::null && maxsat_engine != symbol("wmax")) {
|
||||
warning_msg("solver %s is not recognized, using default 'wmax'",
|
||||
maxsat_engine.str().c_str());
|
||||
}
|
||||
std::cout << "wmax\n";
|
||||
else if (maxsat_engine == symbol("wmax")) {
|
||||
m_msolver = mk_wmax(m_c, m_weights, m_soft_constraints);
|
||||
}
|
||||
else {
|
||||
warning_msg("solver %s is not recognized, using default 'maxres'", maxsat_engine.str().c_str());
|
||||
m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints);
|
||||
}
|
||||
|
||||
if (m_msolver) {
|
||||
m_msolver->updt_params(m_params);
|
||||
|
|
|
@ -35,6 +35,7 @@ Notes:
|
|||
#include "model_smt2_pp.h"
|
||||
#include "card2bv_tactic.h"
|
||||
#include "eq2bv_tactic.h"
|
||||
#include "dt2bv_tactic.h"
|
||||
#include "inc_sat_solver.h"
|
||||
#include "bv_decl_plugin.h"
|
||||
#include "pb_decl_plugin.h"
|
||||
|
@ -688,21 +689,19 @@ namespace opt {
|
|||
// NB: mk_elim_uncstr_tactic(m) is not sound with soft constraints
|
||||
mk_simplify_tactic(m));
|
||||
opt_params optp(m_params);
|
||||
tactic_ref tac2, tac3, tac4;
|
||||
tactic_ref tac1, tac2, tac3, tac4;
|
||||
if (optp.elim_01()) {
|
||||
tac1 = mk_dt2bv_tactic(m);
|
||||
tac2 = mk_elim01_tactic(m);
|
||||
tac3 = mk_lia2card_tactic(m);
|
||||
tac4 = mk_eq2bv_tactic(m);
|
||||
params_ref lia_p;
|
||||
lia_p.set_bool("compile_equality", optp.pb_compile_equality());
|
||||
tac3->updt_params(lia_p);
|
||||
set_simplify(and_then(tac0.get(), tac2.get(), tac3.get(), tac4.get(), mk_simplify_tactic(m)));
|
||||
set_simplify(and_then(tac0.get(), tac1.get(), tac2.get(), tac3.get(), tac4.get(), mk_simplify_tactic(m)));
|
||||
}
|
||||
else {
|
||||
tactic_ref tac1 =
|
||||
and_then(tac0.get(),
|
||||
mk_simplify_tactic(m));
|
||||
set_simplify(tac1.get());
|
||||
set_simplify(tac0.get());
|
||||
}
|
||||
proof_converter_ref pc;
|
||||
expr_dependency_ref core(m);
|
||||
|
|
|
@ -35,7 +35,8 @@ theory_wmaxsat::theory_wmaxsat(ast_manager& m, filter_model_converter& mc):
|
|||
m_zmin_cost(m_mpz),
|
||||
m_found_optimal(false),
|
||||
m_propagate(false),
|
||||
m_normalize(false)
|
||||
m_normalize(false),
|
||||
m_den(1)
|
||||
{}
|
||||
|
||||
theory_wmaxsat::~theory_wmaxsat() {
|
||||
|
|
Loading…
Reference in a new issue