mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
moving parameters to theory_pb
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
4027de42f6
commit
c5b82796ca
|
@ -55,8 +55,6 @@ namespace opt {
|
|||
unsigned m_lower;
|
||||
model_ref m_model;
|
||||
|
||||
bool m_use_new_bv_solver;
|
||||
|
||||
imp(ast_manager& m, opt_solver& s, expr_ref_vector const& soft):
|
||||
m(m),
|
||||
m_opt_solver(s),
|
||||
|
@ -65,8 +63,7 @@ namespace opt {
|
|||
m_orig_soft(soft),
|
||||
m_aux(m),
|
||||
m_upper(0),
|
||||
m_lower(0),
|
||||
m_use_new_bv_solver(false)
|
||||
m_lower(0)
|
||||
{
|
||||
m_upper = m_soft.size() + 1;
|
||||
m_assignment.resize(m_soft.size(), false);
|
||||
|
@ -118,48 +115,6 @@ namespace opt {
|
|||
}
|
||||
}
|
||||
|
||||
void quick_explain(expr_ref_vector const& assumptions, expr_ref_vector & literals, bool has_set, expr_set & core) {
|
||||
if (has_set && s().check_sat(assumptions.size(), assumptions.c_ptr()) == l_false) {
|
||||
core.reset();
|
||||
return;
|
||||
}
|
||||
|
||||
SASSERT(!literals.empty());
|
||||
if (literals.size() == 1) {
|
||||
core.reset();
|
||||
core.insert(literals[0].get());
|
||||
return;
|
||||
}
|
||||
|
||||
unsigned mid = literals.size()/2;
|
||||
expr_ref_vector ls1(m), ls2(m);
|
||||
ls1.append(mid, literals.c_ptr());
|
||||
ls2.append(literals.size()-mid, literals.c_ptr() + mid);
|
||||
#if Z3DEBUG
|
||||
expr_ref_vector ls(m);
|
||||
ls.append(ls1);
|
||||
ls.append(ls2);
|
||||
SASSERT(ls.size() == literals.size());
|
||||
for (unsigned i = 0; i < literals.size(); ++i) {
|
||||
SASSERT(ls[i].get() == literals[i].get());
|
||||
}
|
||||
#endif
|
||||
expr_ref_vector as1(m);
|
||||
as1.append(assumptions);
|
||||
as1.append(ls1);
|
||||
expr_set core2;
|
||||
quick_explain(as1, ls2, !ls1.empty(), core2);
|
||||
|
||||
expr_ref_vector as2(m), cs2(m);
|
||||
as2.append(assumptions);
|
||||
set2vector(core2, cs2);
|
||||
as2.append(cs2);
|
||||
expr_set core1;
|
||||
quick_explain(as2, ls1, !core2.empty(), core1);
|
||||
|
||||
set_union(core1, core2, core);
|
||||
}
|
||||
|
||||
lbool step() {
|
||||
IF_VERBOSE(1, verbose_stream() << "(opt.max_sat step " << m_soft.size() + 2 - m_upper << ")\n";);
|
||||
expr_ref_vector assumptions(m), block_vars(m);
|
||||
|
@ -172,38 +127,7 @@ namespace opt {
|
|||
}
|
||||
|
||||
ptr_vector<expr> core;
|
||||
if (m_use_new_bv_solver) {
|
||||
// Binary search for minimal unsat core
|
||||
expr_set core_set;
|
||||
expr_ref_vector empty(m);
|
||||
quick_explain(empty, assumptions, true, core_set);
|
||||
expr_set::iterator it = core_set.begin(), end = core_set.end();
|
||||
for (; it != end; ++it) {
|
||||
core.push_back(*it);
|
||||
}
|
||||
|
||||
//// Forward linear search for unsat core
|
||||
//unsigned i = 0;
|
||||
//while (s().check_sat(core.size(), core.c_ptr()) != l_false) {
|
||||
// IF_VERBOSE(0, verbose_stream() << "(opt.max_sat get-unsat-core round " << i << ")\n";);
|
||||
// core.push_back(assumptions[i].get());
|
||||
// ++i;
|
||||
//}
|
||||
|
||||
//// Backward linear search for unsat core
|
||||
//unsigned i = 0;
|
||||
//core.append(assumptions.size(), assumptions.c_ptr());
|
||||
//while (!core.empty() && s().check_sat(core.size()-1, core.c_ptr()) == l_false) {
|
||||
// IF_VERBOSE(0, verbose_stream() << "(opt.max_sat get-unsat-core round " << i << ")\n";);
|
||||
// core.pop_back();
|
||||
// ++i;
|
||||
//}
|
||||
|
||||
IF_VERBOSE(1, verbose_stream() << "(opt.max_sat unsat-core of size " << core.size() << ")\n";);
|
||||
}
|
||||
else {
|
||||
s().get_unsat_core(core);
|
||||
}
|
||||
s().get_unsat_core(core);
|
||||
|
||||
SASSERT(!core.empty());
|
||||
|
||||
|
@ -266,23 +190,6 @@ namespace opt {
|
|||
for (unsigned i = 0; i < num_assertions; ++i) {
|
||||
g.assert_expr(current_solver.get_assertion(i));
|
||||
}
|
||||
#if 0
|
||||
// TBD: this leaks references somehow
|
||||
probe_ref p = mk_is_qfbv_probe();
|
||||
bool all_bv = (*p)(g).is_true();
|
||||
if (all_bv) {
|
||||
smt::context & ctx = m_opt_solver.get_context();
|
||||
tactic_ref t = mk_qfbv_tactic(m, ctx.get_params());
|
||||
// The new SAT solver hasn't supported unsat core yet
|
||||
m_s = mk_tactic2solver(m, t.get());
|
||||
SASSERT(m_s != &m_opt_solver);
|
||||
for (unsigned i = 0; i < num_assertions; ++i) {
|
||||
m_s->assert_expr(current_solver.get_assertion(i));
|
||||
}
|
||||
m_use_new_bv_solver = true;
|
||||
IF_VERBOSE(1, verbose_stream() << "Force to use the new BV solver." << std::endl;);
|
||||
}
|
||||
#endif
|
||||
}
|
||||
|
||||
// TBD: bug when cancel flag is set, fu_malik returns is_sat == l_true instead of l_undef
|
||||
|
@ -371,10 +278,51 @@ namespace opt {
|
|||
void fu_malik::updt_params(params_ref& p) {
|
||||
// no-op
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
};
|
||||
|
||||
#if 0
|
||||
void quick_explain(expr_ref_vector const& assumptions, expr_ref_vector & literals, bool has_set, expr_set & core) {
|
||||
if (has_set && s().check_sat(assumptions.size(), assumptions.c_ptr()) == l_false) {
|
||||
core.reset();
|
||||
return;
|
||||
}
|
||||
|
||||
SASSERT(!literals.empty());
|
||||
if (literals.size() == 1) {
|
||||
core.reset();
|
||||
core.insert(literals[0].get());
|
||||
return;
|
||||
}
|
||||
|
||||
unsigned mid = literals.size()/2;
|
||||
expr_ref_vector ls1(m), ls2(m);
|
||||
ls1.append(mid, literals.c_ptr());
|
||||
ls2.append(literals.size()-mid, literals.c_ptr() + mid);
|
||||
#if Z3DEBUG
|
||||
expr_ref_vector ls(m);
|
||||
ls.append(ls1);
|
||||
ls.append(ls2);
|
||||
SASSERT(ls.size() == literals.size());
|
||||
for (unsigned i = 0; i < literals.size(); ++i) {
|
||||
SASSERT(ls[i].get() == literals[i].get());
|
||||
}
|
||||
#endif
|
||||
expr_ref_vector as1(m);
|
||||
as1.append(assumptions);
|
||||
as1.append(ls1);
|
||||
expr_set core2;
|
||||
quick_explain(as1, ls2, !ls1.empty(), core2);
|
||||
|
||||
expr_ref_vector as2(m), cs2(m);
|
||||
as2.append(assumptions);
|
||||
set2vector(core2, cs2);
|
||||
as2.append(cs2);
|
||||
expr_set core1;
|
||||
quick_explain(as2, ls1, !core2.empty(), core1);
|
||||
|
||||
set_union(core1, core2, core);
|
||||
}
|
||||
|
||||
#endif
|
||||
|
||||
|
||||
|
|
|
@ -54,13 +54,6 @@ namespace opt {
|
|||
m_dump_benchmarks = p.dump_benchmarks();
|
||||
m_params.updt_params(_p);
|
||||
m_context.updt_params(_p);
|
||||
smt::theory_id th_id = m.get_family_id("pb");
|
||||
smt::theory* _th = get_context().get_theory(th_id);
|
||||
if (_th) {
|
||||
smt::theory_pb* th = dynamic_cast<smt::theory_pb*>(_th);
|
||||
th->set_conflict_frequency(p.pb_conflict_freq());
|
||||
th->set_learn_complements(p.pb_learn_comp());
|
||||
}
|
||||
}
|
||||
|
||||
void opt_solver::collect_param_descrs(param_descrs & r) {
|
||||
|
|
|
@ -247,6 +247,7 @@ namespace opt {
|
|||
inf_eps obj = m_s->get_objective_value(obj_index);
|
||||
if (obj > m_lower[obj_index]) {
|
||||
m_lower[obj_index] = obj;
|
||||
IF_VERBOSE(1, verbose_stream() << "(optsmt lower bound: " << obj << ")\n";);
|
||||
for (unsigned i = obj_index+1; i < m_vars.size(); ++i) {
|
||||
m_s->maximize_objective(i);
|
||||
m_lower[i] = m_s->get_objective_value(i);
|
||||
|
|
|
@ -1,17 +0,0 @@
|
|||
Create file with command-line extensions.
|
||||
Similar to muz\fp\dl_cmds:
|
||||
- Add command (minimize <term>)
|
||||
- Add command (assert-weighted <expr> <weight> [:id]) the weight is a positive
|
||||
rational number, 1 can be handled as a special case sd not weighted SAT,
|
||||
but as ordinary MAXSAT (e.g., using Fu Malik algorithm. This is a sample).
|
||||
Identifier is optional and used to group constraints together.
|
||||
The F# sample illustrates what is meant.
|
||||
|
||||
Next steps:
|
||||
- replace solver by opt_solver.
|
||||
- create a file called opt_solver, copy most from smt_solver into it.
|
||||
Add some functions to enable/disable post-optimization on feasiable state.
|
||||
- Add methods to theory_arith.h to enable/disable post-optimization
|
||||
- Add method(s) to theory_arith.h to register objective functions.
|
||||
- Add post-optimization step to theory_arith_core.h
|
||||
- (Figure out how to do multi-objective in this framework directly besides naive loop)
|
|
@ -826,25 +826,11 @@ namespace opt {
|
|||
pb_util u(m);
|
||||
lbool is_sat = bound(al, ws, bs, k);
|
||||
if (is_sat != l_true) return is_sat;
|
||||
#if 0
|
||||
rational mininc(0);
|
||||
for (unsigned i = 0; i < ws.size(); ++i) {
|
||||
if (mininc.is_zero() || mininc > ws[i]) {
|
||||
mininc = ws[i];
|
||||
}
|
||||
}
|
||||
k += mininc;
|
||||
#else
|
||||
expr_ref_vector al2(m);
|
||||
al2.append(al);
|
||||
// w_j*b_j > k
|
||||
rational k0 = k;
|
||||
al2.push_back(m.mk_not(u.mk_le(ws.size(), ws.c_ptr(), bs.c_ptr(), k)));
|
||||
is_sat = bound(al2, ws, bs, k);
|
||||
if (is_sat == l_true) {
|
||||
SASSERT(k > k0);
|
||||
}
|
||||
#endif
|
||||
return is_sat;
|
||||
}
|
||||
|
||||
|
|
|
@ -47,6 +47,7 @@ void smt_params::updt_params(params_ref const & p) {
|
|||
qi_params::updt_params(p);
|
||||
theory_arith_params::updt_params(p);
|
||||
theory_bv_params::updt_params(p);
|
||||
theory_pb_params::updt_params(p);
|
||||
updt_local_params(p);
|
||||
}
|
||||
|
||||
|
|
|
@ -25,6 +25,7 @@ Revision History:
|
|||
#include"theory_arith_params.h"
|
||||
#include"theory_array_params.h"
|
||||
#include"theory_bv_params.h"
|
||||
#include"theory_pb_params.h"
|
||||
#include"theory_datatype_params.h"
|
||||
#include"preprocessor_params.h"
|
||||
#include"context_params.h"
|
||||
|
@ -73,7 +74,8 @@ struct smt_params : public preprocessor_params,
|
|||
public qi_params,
|
||||
public theory_arith_params,
|
||||
public theory_array_params,
|
||||
public theory_bv_params,
|
||||
public theory_bv_params,
|
||||
public theory_pb_params,
|
||||
public theory_datatype_params {
|
||||
bool m_display_proof;
|
||||
bool m_display_dot_proof;
|
||||
|
|
|
@ -41,4 +41,8 @@ def_module_params(module_name='smt',
|
|||
('arith.propagation_mode', UINT, 2, '0 - no propagation, 1 - propagate existing literals, 2 - refine bounds'),
|
||||
('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),
|
||||
('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),
|
||||
('arith.ignore_int', BOOL, False, 'treat integer variables as real')))
|
||||
('arith.ignore_int', BOOL, False, 'treat integer variables as real'),
|
||||
('pb.conflict_frequency', UINT, 0, 'conflict frequency for Pseudo-Boolean theory'),
|
||||
('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'),
|
||||
('pb.enable_compilation', BOOL, True, 'enable compilation into sorting circuits for Pseudo-Boolean')))
|
||||
|
||||
|
|
27
src/smt/params/theory_pb_params.cpp
Normal file
27
src/smt/params/theory_pb_params.cpp
Normal file
|
@ -0,0 +1,27 @@
|
|||
/*++
|
||||
Copyright (c) 2014 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
theory_pb_params.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2014-01-01
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#include"theory_pb_params.h"
|
||||
#include"smt_params_helper.hpp"
|
||||
|
||||
void theory_pb_params::updt_params(params_ref const & _p) {
|
||||
smt_params_helper p(_p);
|
||||
m_pb_conflict_frequency = p.pb_conflict_frequency();
|
||||
m_pb_learn_complements = p.pb_learn_complements();
|
||||
m_pb_enable_compilation = p.pb_enable_compilation();
|
||||
}
|
39
src/smt/params/theory_pb_params.h
Normal file
39
src/smt/params/theory_pb_params.h
Normal file
|
@ -0,0 +1,39 @@
|
|||
/*++
|
||||
Copyright (c) 2013 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
theory_pb_params.h
|
||||
|
||||
Abstract:
|
||||
|
||||
<abstract>
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2014-01-01
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
#ifndef _THEORY_PB_PARAMS_H_
|
||||
#define _THEORY_PB_PARAMS_H_
|
||||
|
||||
#include"params.h"
|
||||
|
||||
|
||||
struct theory_pb_params {
|
||||
unsigned m_pb_conflict_frequency;
|
||||
bool m_pb_learn_complements;
|
||||
bool m_pb_enable_compilation;
|
||||
theory_pb_params(params_ref const & p = params_ref()):
|
||||
m_pb_conflict_frequency(0),
|
||||
m_pb_learn_complements(true),
|
||||
m_pb_enable_compilation(true)
|
||||
{}
|
||||
|
||||
void updt_params(params_ref const & p);
|
||||
};
|
||||
|
||||
#endif /* _THEORY_PB_PARAMS_H_ */
|
||||
|
|
@ -793,7 +793,7 @@ namespace smt {
|
|||
|
||||
void setup::setup_card() {
|
||||
// m_context.register_plugin(alloc(theory_card, m_manager));
|
||||
m_context.register_plugin(alloc(theory_pb, m_manager));
|
||||
m_context.register_plugin(alloc(theory_pb, m_manager, m_params));
|
||||
}
|
||||
|
||||
void setup::setup_unknown() {
|
||||
|
|
|
@ -42,7 +42,7 @@ namespace smt {
|
|||
class setup {
|
||||
context & m_context;
|
||||
ast_manager & m_manager;
|
||||
smt_params & m_params;
|
||||
smt_params & m_params;
|
||||
symbol m_logic;
|
||||
bool m_already_configured;
|
||||
void setup_auto_config();
|
||||
|
|
|
@ -816,20 +816,23 @@ namespace smt {
|
|||
return true;
|
||||
}
|
||||
|
||||
theory_pb::theory_pb(ast_manager& m):
|
||||
theory_pb::theory_pb(ast_manager& m, theory_pb_params& p):
|
||||
theory(m.mk_family_id("pb")),
|
||||
m_params(p),
|
||||
m_util(m),
|
||||
m_lemma(null_literal),
|
||||
m_learn_complements(false),
|
||||
m_conflict_frequency(0xF)
|
||||
{}
|
||||
m_lemma(null_literal)
|
||||
{
|
||||
m_learn_complements = p.m_pb_learn_complements;
|
||||
m_conflict_frequency = p.m_pb_conflict_frequency;
|
||||
m_enable_compilation = p.m_pb_enable_compilation;
|
||||
}
|
||||
|
||||
theory_pb::~theory_pb() {
|
||||
reset_eh();
|
||||
}
|
||||
|
||||
theory * theory_pb::mk_fresh(context * new_ctx) {
|
||||
return alloc(theory_pb, new_ctx->get_manager());
|
||||
return alloc(theory_pb, new_ctx->get_manager(), m_params);
|
||||
}
|
||||
|
||||
bool theory_pb::internalize_atom(app * atom, bool gate_ctx) {
|
||||
|
@ -910,20 +913,21 @@ namespace smt {
|
|||
|
||||
|
||||
// pre-compile threshold for cardinality
|
||||
bool is_cardinality = true;
|
||||
for (unsigned i = 0; is_cardinality && i < args.size(); ++i) {
|
||||
is_cardinality = (args[i].second < rational(8));
|
||||
bool enable_compile = m_enable_compilation;
|
||||
for (unsigned i = 0; enable_compile && i < args.size(); ++i) {
|
||||
enable_compile = (args[i].second < rational(8));
|
||||
}
|
||||
if (is_cardinality) {
|
||||
if (enable_compile) {
|
||||
unsigned log = 1, n = 1;
|
||||
while (n <= args.size()) {
|
||||
++log;
|
||||
n *= 2;
|
||||
}
|
||||
unsigned th = 10*args.size()*log;
|
||||
unsigned th = args.size()*log; // 10*
|
||||
c->m_compilation_threshold = th;
|
||||
IF_VERBOSE(2, verbose_stream() << "(smt.pb setting compilation threhshold to " << th << ")\n";);
|
||||
TRACE("pb", tout << "compilation threshold: " << th << "\n";);
|
||||
}
|
||||
}
|
||||
else {
|
||||
c->m_compilation_threshold = UINT_MAX;
|
||||
}
|
||||
|
@ -1429,6 +1433,14 @@ namespace smt {
|
|||
literal_vector in;
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
rational n = c.coeff(i);
|
||||
lbool val = ctx.get_assignment(c.lit());
|
||||
if (val != l_undef &&
|
||||
ctx.get_assign_level(thl) == ctx.get_base_level()) {
|
||||
if (val == l_true) {
|
||||
k -= n.get_unsigned();
|
||||
}
|
||||
continue;
|
||||
}
|
||||
while (n.is_pos()) {
|
||||
in.push_back(c.lit(i));
|
||||
n -= rational::one();
|
||||
|
@ -1765,7 +1777,7 @@ namespace smt {
|
|||
// same order as the assignment stack.
|
||||
// It is not a correctness bug but causes to miss lemmas.
|
||||
//
|
||||
IF_VERBOSE(1, display_resolved_lemma(verbose_stream()););
|
||||
IF_VERBOSE(2, display_resolved_lemma(verbose_stream()););
|
||||
TRACE("pb", display_resolved_lemma(tout););
|
||||
return false;
|
||||
}
|
||||
|
@ -1851,12 +1863,12 @@ namespace smt {
|
|||
// 3x + 3y + z + u >= 4
|
||||
// ~x /\ ~y => z + u >=
|
||||
|
||||
IF_VERBOSE(2, display(verbose_stream() << "lemma1: ", m_lemma););
|
||||
IF_VERBOSE(4, display(verbose_stream() << "lemma1: ", m_lemma););
|
||||
hoist_maximal_values();
|
||||
lbool is_true = m_lemma.normalize();
|
||||
m_lemma.prune();
|
||||
|
||||
IF_VERBOSE(2, display(verbose_stream() << "lemma2: ", m_lemma););
|
||||
IF_VERBOSE(4, display(verbose_stream() << "lemma2: ", m_lemma););
|
||||
switch(is_true) {
|
||||
case l_true:
|
||||
UNREACHABLE();
|
||||
|
|
|
@ -23,6 +23,7 @@ Notes:
|
|||
#include "smt_theory.h"
|
||||
#include "pb_decl_plugin.h"
|
||||
#include "smt_clause.h"
|
||||
#include "theory_pb_params.h"
|
||||
|
||||
namespace smt {
|
||||
class theory_pb : public theory {
|
||||
|
@ -59,7 +60,7 @@ namespace smt {
|
|||
unsigned m_num_propagations;
|
||||
unsigned m_compilation_threshold;
|
||||
lbool m_compiled;
|
||||
|
||||
|
||||
ineq(literal l) : m_lit(l) {
|
||||
reset();
|
||||
}
|
||||
|
@ -102,7 +103,8 @@ namespace smt {
|
|||
};
|
||||
|
||||
typedef ptr_vector<ineq> watch_list;
|
||||
|
||||
|
||||
theory_pb_params m_params;
|
||||
u_map<watch_list*> m_watch; // per literal.
|
||||
u_map<ineq*> m_ineqs; // per inequality.
|
||||
unsigned_vector m_ineqs_trail;
|
||||
|
@ -115,6 +117,7 @@ namespace smt {
|
|||
ptr_vector<ineq> m_to_compile; // inequalities to compile.
|
||||
unsigned m_conflict_frequency;
|
||||
bool m_learn_complements;
|
||||
bool m_enable_compilation;
|
||||
|
||||
// internalize_atom:
|
||||
literal compile_arg(expr* arg);
|
||||
|
@ -172,7 +175,7 @@ namespace smt {
|
|||
void validate_assign(ineq const& c, literal_vector const& lits, literal l) const;
|
||||
void validate_watch(ineq const& c) const;
|
||||
public:
|
||||
theory_pb(ast_manager& m);
|
||||
theory_pb(ast_manager& m, theory_pb_params& p);
|
||||
|
||||
virtual ~theory_pb();
|
||||
|
||||
|
@ -194,9 +197,6 @@ namespace smt {
|
|||
virtual model_value_proc * mk_value(enode * n, model_generator & mg);
|
||||
virtual void init_model(model_generator & m);
|
||||
|
||||
void set_conflict_frequency(unsigned f) { m_conflict_frequency = f; }
|
||||
void set_learn_complements(bool l) { m_learn_complements = l; }
|
||||
|
||||
static literal assert_ge(context& ctx, unsigned k, unsigned n, literal const* xs);
|
||||
};
|
||||
};
|
||||
|
|
|
@ -71,6 +71,7 @@ class lia2pb_tactic : public tactic {
|
|||
if (m_bm.has_lower(n, l, s) &&
|
||||
m_bm.has_upper(n, u, s) &&
|
||||
l.is_zero() &&
|
||||
!u.is_neg() &&
|
||||
u.get_num_bits() <= m_max_bits) {
|
||||
|
||||
return true;
|
||||
|
|
Loading…
Reference in a new issue