mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 01:25:31 +00:00
Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt
This commit is contained in:
Nikolaj Bjorner
commit
55ba1e9178
52 changed files with 877 additions and 311 deletions
|
|
@ -42,7 +42,8 @@ namespace sat {
|
|||
stats() { reset(); }
|
||||
void reset() { memset(this, 0, sizeof(*this)); }
|
||||
};
|
||||
|
||||
|
||||
public:
|
||||
class card {
|
||||
unsigned m_index;
|
||||
literal m_lit;
|
||||
|
|
@ -105,6 +106,7 @@ namespace sat {
|
|||
void swap(unsigned i, unsigned j) { std::swap(m_lits[i], m_lits[j]); }
|
||||
void negate() { m_lits[0].neg(); }
|
||||
};
|
||||
protected:
|
||||
|
||||
struct ineq {
|
||||
literal_vector m_lits;
|
||||
|
|
@ -304,6 +306,13 @@ namespace sat {
|
|||
void add_at_least(bool_var v, literal_vector const& lits, unsigned k);
|
||||
void add_pb_ge(bool_var v, svector<wliteral> const& wlits, unsigned k);
|
||||
void add_xor(bool_var v, literal_vector const& lits);
|
||||
unsigned num_pb() const { return m_pbs.size(); }
|
||||
pb const& get_pb(unsigned i) const { return *m_pbs[i]; }
|
||||
unsigned num_card() const { return m_cards.size(); }
|
||||
card const& get_card(unsigned i) const { return *m_cards[i]; }
|
||||
unsigned num_xor() const { return m_xors.size(); }
|
||||
xor const& get_xor(unsigned i) const { return *m_xors[i]; }
|
||||
|
||||
virtual void propagate(literal l, ext_constraint_idx idx, bool & keep);
|
||||
virtual bool resolve_conflict();
|
||||
virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r);
|
||||
|
|
|
|||
|
|
@ -126,6 +126,27 @@ namespace sat {
|
|||
m_drat_file = p.drat_file();
|
||||
m_drat = (m_drat_check || m_drat_file != symbol("")) && p.threads() == 1;
|
||||
m_dyn_sub_res = p.dyn_sub_res();
|
||||
|
||||
// Parameters used in Liang, Ganesh, Poupart, Czarnecki AAAI 2016.
|
||||
m_branching_heuristic = BH_VSIDS;
|
||||
if (p.branching_heuristic() == symbol("vsids")) {
|
||||
m_branching_heuristic = BH_VSIDS;
|
||||
}
|
||||
else if (p.branching_heuristic() == symbol("chb")) {
|
||||
m_branching_heuristic = BH_CHB;
|
||||
}
|
||||
else if (p.branching_heuristic() == symbol("lrb")) {
|
||||
m_branching_heuristic = BH_LRB;
|
||||
}
|
||||
else {
|
||||
throw sat_param_exception("invalid branching heuristic: accepted heuristics are 'vsids', 'lrb' or 'chb'");
|
||||
}
|
||||
m_anti_exploration = m_branching_heuristic != BH_VSIDS;
|
||||
m_step_size_init = 0.40;
|
||||
m_step_size_dec = 0.000001;
|
||||
m_step_size_min = 0.06;
|
||||
m_reward_multiplier = 0.9;
|
||||
m_reward_offset = 1000000.0;
|
||||
}
|
||||
|
||||
void config::collect_param_descrs(param_descrs & r) {
|
||||
|
|
|
|||
|
|
@ -44,6 +44,12 @@ namespace sat {
|
|||
GC_PSM_GLUE
|
||||
};
|
||||
|
||||
enum branching_heuristic {
|
||||
BH_VSIDS,
|
||||
BH_CHB,
|
||||
BH_LRB
|
||||
};
|
||||
|
||||
struct config {
|
||||
unsigned long long m_max_memory;
|
||||
phase_selection m_phase;
|
||||
|
|
@ -95,6 +101,14 @@ namespace sat {
|
|||
symbol m_glue_psm;
|
||||
symbol m_psm_glue;
|
||||
|
||||
// branching heuristic settings.
|
||||
branching_heuristic m_branching_heuristic;
|
||||
bool m_anti_exploration;
|
||||
double m_step_size_init;
|
||||
double m_step_size_dec;
|
||||
double m_step_size_min;
|
||||
double m_reward_multiplier;
|
||||
double m_reward_offset;
|
||||
config(params_ref const & p);
|
||||
void updt_params(params_ref const & p);
|
||||
static void collect_param_descrs(param_descrs & d);
|
||||
|
|
|
|||
|
|
@ -46,7 +46,7 @@ namespace sat {
|
|||
virtual std::ostream& display(std::ostream& out) const = 0;
|
||||
virtual std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const = 0;
|
||||
virtual void collect_statistics(statistics& st) const = 0;
|
||||
virtual extension* copy(solver* s) = 0;
|
||||
virtual extension* copy(solver* s) = 0;
|
||||
virtual void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) = 0;
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -384,6 +384,7 @@ namespace sat {
|
|||
candidate(bool_var v, float r): m_var(v), m_rating(r) {}
|
||||
};
|
||||
svector<candidate> m_candidates;
|
||||
uint_set m_select_lookahead_vars;
|
||||
|
||||
float get_rating(bool_var v) const { return m_rating[v]; }
|
||||
float get_rating(literal l) const { return get_rating(l.var()); }
|
||||
|
|
@ -468,7 +469,11 @@ namespace sat {
|
|||
for (bool_var const* it = m_freevars.begin(), * end = m_freevars.end(); it != end; ++it) {
|
||||
SASSERT(is_undef(*it));
|
||||
bool_var x = *it;
|
||||
if (newbies || active_prefix(x)) {
|
||||
if (!m_select_lookahead_vars.empty() && m_select_lookahead_vars.contains(x)) {
|
||||
m_candidates.push_back(candidate(x, m_rating[x]));
|
||||
sum += m_rating[x];
|
||||
}
|
||||
else if (newbies || active_prefix(x)) {
|
||||
m_candidates.push_back(candidate(x, m_rating[x]));
|
||||
sum += m_rating[x];
|
||||
}
|
||||
|
|
@ -1857,6 +1862,31 @@ namespace sat {
|
|||
return search();
|
||||
}
|
||||
|
||||
literal select_lookahead(bool_var_vector const& vars) {
|
||||
m_search_mode = lookahead_mode::searching;
|
||||
scoped_level _sl(*this, c_fixed_truth);
|
||||
init();
|
||||
if (inconsistent()) return null_literal;
|
||||
inc_istamp();
|
||||
for (auto v : vars) {
|
||||
m_select_lookahead_vars.insert(v);
|
||||
}
|
||||
literal l = choose();
|
||||
m_select_lookahead_vars.reset();
|
||||
if (inconsistent()) return null_literal;
|
||||
|
||||
// assign unit literals that were found during search for lookahead.
|
||||
unsigned num_assigned = 0;
|
||||
for (literal lit : m_trail) {
|
||||
if (!m_s.was_eliminated(lit.var()) && m_s.value(lit) != l_true) {
|
||||
m_s.assign(lit, justification());
|
||||
++num_assigned;
|
||||
}
|
||||
}
|
||||
IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :units " << num_assigned << ")\n";);
|
||||
return l;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief simplify set of clauses by extracting units from a lookahead at base level.
|
||||
*/
|
||||
|
|
|
|||
|
|
@ -9,6 +9,7 @@ def_module_params('sat',
|
|||
('restart.initial', UINT, 100, 'initial restart (number of conflicts)'),
|
||||
('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'),
|
||||
('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'),
|
||||
('branching.heuristic', SYMBOL, 'vsids', 'branching heuristic vsids, lrb or chb'),
|
||||
('random_freq', DOUBLE, 0.01, 'frequency of random case splits'),
|
||||
('random_seed', UINT, 0, 'random seed'),
|
||||
('burst_search', UINT, 100, 'number of conflicts before first global simplification'),
|
||||
|
|
@ -21,8 +22,7 @@ def_module_params('sat',
|
|||
('minimize_lemmas', BOOL, True, 'minimize learned clauses'),
|
||||
('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'),
|
||||
('core.minimize', BOOL, False, 'minimize computed core'),
|
||||
('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'),
|
||||
('threads', UINT, 1, 'number of parallel threads to use'),
|
||||
('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'), ('threads', UINT, 1, 'number of parallel threads to use'),
|
||||
('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'),
|
||||
('drat.file', SYMBOL, '', 'file to dump DRAT proofs'),
|
||||
('drat.check', BOOL, False, 'build up internal proof and check'),
|
||||
|
|
|
|||
|
|
@ -175,6 +175,11 @@ namespace sat {
|
|||
m_phase.push_back(PHASE_NOT_AVAILABLE);
|
||||
m_prev_phase.push_back(PHASE_NOT_AVAILABLE);
|
||||
m_assigned_since_gc.push_back(false);
|
||||
m_last_conflict.push_back(0);
|
||||
m_last_propagation.push_back(0);
|
||||
m_participated.push_back(0);
|
||||
m_canceled.push_back(0);
|
||||
m_reasoned.push_back(0);
|
||||
m_case_split_queue.mk_var_eh(v);
|
||||
m_simplifier.insert_elim_todo(v);
|
||||
SASSERT(!was_eliminated(v));
|
||||
|
|
@ -581,6 +586,29 @@ namespace sat {
|
|||
if (m_ext && m_external[v])
|
||||
m_ext->asserted(l);
|
||||
|
||||
switch (m_config.m_branching_heuristic) {
|
||||
case BH_VSIDS:
|
||||
break;
|
||||
case BH_CHB:
|
||||
m_last_propagation[v] = m_stats.m_conflict;
|
||||
break;
|
||||
case BH_LRB:
|
||||
m_participated[v] = 0;
|
||||
m_reasoned[v] = 0;
|
||||
break;
|
||||
}
|
||||
if (m_config.m_anti_exploration) {
|
||||
uint64 age = m_stats.m_conflict - m_canceled[v];
|
||||
if (age > 0) {
|
||||
double decay = pow(0.95, age);
|
||||
m_activity[v] = static_cast<unsigned>(m_activity[v] * decay);
|
||||
// NB. MapleSAT does not update canceled.
|
||||
m_canceled[v] = m_stats.m_conflict;
|
||||
m_case_split_queue.activity_changed_eh(v, false);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
SASSERT(!l.sign() || m_phase[v] == NEG_PHASE);
|
||||
SASSERT(l.sign() || m_phase[v] == POS_PHASE);
|
||||
|
||||
|
|
@ -772,12 +800,26 @@ namespace sat {
|
|||
}
|
||||
|
||||
bool solver::propagate(bool update) {
|
||||
unsigned qhead = m_qhead;
|
||||
bool r = propagate_core(update);
|
||||
if (m_config.m_branching_heuristic == BH_CHB) {
|
||||
update_chb_activity(r, qhead);
|
||||
}
|
||||
CASSERT("sat_propagate", check_invariant());
|
||||
CASSERT("sat_missed_prop", check_missed_propagation());
|
||||
return r;
|
||||
}
|
||||
|
||||
literal solver::select_lookahead(bool_var_vector const& vars) {
|
||||
lookahead lh(*this);
|
||||
literal result = lh.select_lookahead(vars);
|
||||
if (result == null_literal) {
|
||||
set_conflict(justification());
|
||||
}
|
||||
// extract unit literals from lh
|
||||
return result;
|
||||
}
|
||||
|
||||
// -----------------------
|
||||
//
|
||||
// Search
|
||||
|
|
@ -1065,6 +1107,18 @@ namespace sat {
|
|||
}
|
||||
|
||||
while (!m_case_split_queue.empty()) {
|
||||
if (m_config.m_anti_exploration) {
|
||||
next = m_case_split_queue.min_var();
|
||||
auto age = m_stats.m_conflict - m_canceled[next];
|
||||
while (age > 0) {
|
||||
double decay = pow(0.95, age);
|
||||
m_activity[next] = static_cast<unsigned>(m_activity[next] * pow(0.95, age));
|
||||
m_case_split_queue.activity_changed_eh(next, false);
|
||||
m_canceled[next] = m_stats.m_conflict;
|
||||
next = m_case_split_queue.min_var();
|
||||
age = m_stats.m_conflict - m_canceled[next];
|
||||
}
|
||||
}
|
||||
next = m_case_split_queue.next_var();
|
||||
if (value(next) == l_undef && !was_eliminated(next))
|
||||
return next;
|
||||
|
|
@ -1829,6 +1883,9 @@ namespace sat {
|
|||
m_conflicts_since_restart++;
|
||||
m_conflicts_since_gc++;
|
||||
m_stats.m_conflict++;
|
||||
if (m_step_size > m_config.m_step_size_min) {
|
||||
m_step_size -= m_config.m_step_size_dec;
|
||||
}
|
||||
|
||||
m_conflict_lvl = get_max_lvl(m_not_l, m_conflict);
|
||||
TRACE("sat", tout << "conflict detected at level " << m_conflict_lvl << " for ";
|
||||
|
|
@ -2176,7 +2233,16 @@ namespace sat {
|
|||
SASSERT(var < num_vars());
|
||||
if (!is_marked(var) && var_lvl > 0) {
|
||||
mark(var);
|
||||
inc_activity(var);
|
||||
switch (m_config.m_branching_heuristic) {
|
||||
case BH_VSIDS:
|
||||
inc_activity(var);
|
||||
break;
|
||||
case BH_CHB:
|
||||
m_last_conflict[var] = m_stats.m_conflict;
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
if (var_lvl == m_conflict_lvl)
|
||||
num_marks++;
|
||||
else
|
||||
|
|
@ -2432,6 +2498,9 @@ namespace sat {
|
|||
\brief Reset the mark of the variables in the current lemma.
|
||||
*/
|
||||
void solver::reset_lemma_var_marks() {
|
||||
if (m_config.m_branching_heuristic == BH_LRB) {
|
||||
update_lrb_reasoned();
|
||||
}
|
||||
literal_vector::iterator it = m_lemma.begin();
|
||||
literal_vector::iterator end = m_lemma.end();
|
||||
SASSERT(!is_marked((*it).var()));
|
||||
|
|
@ -2442,6 +2511,58 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
|
||||
void solver::update_lrb_reasoned() {
|
||||
unsigned sz = m_lemma.size();
|
||||
SASSERT(!is_marked(m_lemma[0].var()));
|
||||
mark(m_lemma[0].var());
|
||||
for (unsigned i = m_lemma.size(); i > 0; ) {
|
||||
--i;
|
||||
justification js = m_justification[m_lemma[i].var()];
|
||||
switch (js.get_kind()) {
|
||||
case justification::NONE:
|
||||
break;
|
||||
case justification::BINARY:
|
||||
update_lrb_reasoned(js.get_literal());
|
||||
break;
|
||||
case justification::TERNARY:
|
||||
update_lrb_reasoned(js.get_literal1());
|
||||
update_lrb_reasoned(js.get_literal2());
|
||||
break;
|
||||
case justification::CLAUSE: {
|
||||
clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset()));
|
||||
for (unsigned i = 0; i < c.size(); ++i) {
|
||||
update_lrb_reasoned(c[i]);
|
||||
}
|
||||
break;
|
||||
}
|
||||
case justification::EXT_JUSTIFICATION: {
|
||||
fill_ext_antecedents(m_lemma[i], js);
|
||||
literal_vector::iterator it = m_ext_antecedents.begin();
|
||||
literal_vector::iterator end = m_ext_antecedents.end();
|
||||
for (; it != end; ++it) {
|
||||
update_lrb_reasoned(*it);
|
||||
}
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
reset_mark(m_lemma[0].var());
|
||||
for (unsigned i = m_lemma.size(); i > sz; ) {
|
||||
--i;
|
||||
reset_mark(m_lemma[i].var());
|
||||
}
|
||||
m_lemma.shrink(sz);
|
||||
}
|
||||
|
||||
void solver::update_lrb_reasoned(literal lit) {
|
||||
bool_var v = lit.var();
|
||||
if (!is_marked(v)) {
|
||||
mark(v);
|
||||
m_reasoned[v]++;
|
||||
m_lemma.push_back(lit);
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Apply dynamic subsumption resolution to new lemma.
|
||||
Only binary and ternary clauses are used.
|
||||
|
|
@ -2618,6 +2739,18 @@ namespace sat {
|
|||
bool_var v = l.var();
|
||||
SASSERT(value(v) == l_undef);
|
||||
m_case_split_queue.unassign_var_eh(v);
|
||||
if (m_config.m_branching_heuristic == BH_LRB) {
|
||||
uint64 interval = m_stats.m_conflict - m_last_propagation[v];
|
||||
if (interval > 0) {
|
||||
auto activity = m_activity[v];
|
||||
auto reward = (m_config.m_reward_offset * (m_participated[v] + m_reasoned[v])) / interval;
|
||||
m_activity[v] = static_cast<unsigned>(m_step_size * reward + ((1 - m_step_size) * activity));
|
||||
m_case_split_queue.activity_changed_eh(v, m_activity[v] > activity);
|
||||
}
|
||||
}
|
||||
if (m_config.m_anti_exploration) {
|
||||
m_canceled[v] = m_stats.m_conflict;
|
||||
}
|
||||
}
|
||||
m_trail.shrink(old_sz);
|
||||
m_qhead = old_sz;
|
||||
|
|
@ -2800,6 +2933,8 @@ namespace sat {
|
|||
m_probing.updt_params(p);
|
||||
m_scc.updt_params(p);
|
||||
m_rand.set_seed(m_config.m_random_seed);
|
||||
|
||||
m_step_size = m_config.m_step_size_init;
|
||||
}
|
||||
|
||||
void solver::collect_param_descrs(param_descrs & d) {
|
||||
|
|
@ -2837,6 +2972,7 @@ namespace sat {
|
|||
// -----------------------
|
||||
|
||||
void solver::rescale_activity() {
|
||||
SASSERT(m_config.m_branching_heuristic == BH_VSIDS);
|
||||
svector<unsigned>::iterator it = m_activity.begin();
|
||||
svector<unsigned>::iterator end = m_activity.end();
|
||||
for (; it != end; ++it) {
|
||||
|
|
@ -2845,6 +2981,18 @@ namespace sat {
|
|||
m_activity_inc >>= 14;
|
||||
}
|
||||
|
||||
void solver::update_chb_activity(bool is_sat, unsigned qhead) {
|
||||
SASSERT(m_config.m_branching_heuristic == BH_CHB);
|
||||
double multiplier = m_config.m_reward_offset * (is_sat ? m_config.m_reward_multiplier : 1.0);
|
||||
for (unsigned i = qhead; i < m_trail.size(); ++i) {
|
||||
auto v = m_trail[i].var();
|
||||
auto reward = multiplier / (m_stats.m_conflict - m_last_conflict[v] + 1);
|
||||
auto activity = m_activity[v];
|
||||
m_activity[v] = static_cast<unsigned>(m_step_size * reward + ((1.0 - m_step_size) * activity));
|
||||
m_case_split_queue.activity_changed_eh(v, m_activity[v] > activity);
|
||||
}
|
||||
}
|
||||
|
||||
// -----------------------
|
||||
//
|
||||
// Iterators
|
||||
|
|
|
|||
|
|
@ -110,8 +110,17 @@ namespace sat {
|
|||
svector<char> m_eliminated;
|
||||
svector<char> m_external;
|
||||
svector<unsigned> m_level;
|
||||
// branch variable selection:
|
||||
svector<unsigned> m_activity;
|
||||
unsigned m_activity_inc;
|
||||
svector<uint64> m_last_conflict;
|
||||
svector<uint64> m_last_propagation;
|
||||
svector<uint64> m_participated;
|
||||
svector<uint64> m_canceled;
|
||||
svector<uint64> m_reasoned;
|
||||
int m_action;
|
||||
double m_step_size;
|
||||
// phase
|
||||
svector<char> m_phase;
|
||||
svector<char> m_prev_phase;
|
||||
svector<char> m_assigned_since_gc;
|
||||
|
|
@ -300,7 +309,7 @@ namespace sat {
|
|||
}
|
||||
void set_par(parallel* p, unsigned id);
|
||||
bool canceled() { return !m_rlimit.inc(); }
|
||||
config const& get_config() { return m_config; }
|
||||
config const& get_config() const { return m_config; }
|
||||
extension* get_extension() const { return m_ext.get(); }
|
||||
void set_extension(extension* e);
|
||||
typedef std::pair<literal, literal> bin_clause;
|
||||
|
|
@ -343,6 +352,8 @@ namespace sat {
|
|||
model_converter const & get_model_converter() const { return m_mc; }
|
||||
void set_model(model const& mdl);
|
||||
|
||||
literal select_lookahead(bool_var_vector const& vars);
|
||||
|
||||
protected:
|
||||
unsigned m_conflicts;
|
||||
unsigned m_restarts;
|
||||
|
|
@ -555,6 +566,12 @@ namespace sat {
|
|||
private:
|
||||
void rescale_activity();
|
||||
|
||||
void update_chb_activity(bool is_sat, unsigned qhead);
|
||||
|
||||
void update_lrb_reasoned();
|
||||
|
||||
void update_lrb_reasoned(literal lit);
|
||||
|
||||
// -----------------------
|
||||
//
|
||||
// Iterators
|
||||
|
|
|
|||
|
|
@ -66,7 +66,11 @@ class inc_sat_solver : public solver {
|
|||
expr_dependency_ref m_dep_core;
|
||||
svector<double> m_weights;
|
||||
std::string m_unknown;
|
||||
|
||||
// access formulas after they have been pre-processed and handled by the sat solver.
|
||||
// this allows to access the internal state of the SAT solver and carry on partial results.
|
||||
bool m_internalized; // are formulas internalized?
|
||||
bool m_internalized_converted; // have internalized formulas been converted back
|
||||
expr_ref_vector m_internalized_fmls; // formulas in internalized format
|
||||
|
||||
typedef obj_map<expr, sat::literal> dep2asm_t;
|
||||
public:
|
||||
|
|
@ -81,7 +85,10 @@ public:
|
|||
m_map(m),
|
||||
m_num_scopes(0),
|
||||
m_dep_core(m),
|
||||
m_unknown("no reason given") {
|
||||
m_unknown("no reason given"),
|
||||
m_internalized(false),
|
||||
m_internalized_converted(false),
|
||||
m_internalized_fmls(m) {
|
||||
updt_params(p);
|
||||
init_preprocess();
|
||||
}
|
||||
|
|
@ -141,6 +148,8 @@ public:
|
|||
if (r != l_true) return r;
|
||||
r = internalize_assumptions(sz, assumptions, dep2asm);
|
||||
if (r != l_true) return r;
|
||||
m_internalized = true;
|
||||
m_internalized_converted = false;
|
||||
|
||||
r = m_solver.check(m_asms.size(), m_asms.c_ptr());
|
||||
|
||||
|
|
@ -170,8 +179,11 @@ public:
|
|||
m_fmls_head_lim.push_back(m_fmls_head);
|
||||
if (m_bb_rewriter) m_bb_rewriter->push();
|
||||
m_map.push();
|
||||
m_internalized = true;
|
||||
m_internalized_converted = false;
|
||||
}
|
||||
virtual void pop(unsigned n) {
|
||||
m_internalized = false;
|
||||
if (n > m_num_scopes) { // allow inc_sat_solver to
|
||||
n = m_num_scopes; // take over for another solver.
|
||||
}
|
||||
|
|
@ -204,6 +216,7 @@ public:
|
|||
}
|
||||
virtual ast_manager& get_manager() const { return m; }
|
||||
virtual void assert_expr(expr * t) {
|
||||
m_internalized = false;
|
||||
TRACE("goal2sat", tout << mk_pp(t, m) << "\n";);
|
||||
m_fmls.push_back(t);
|
||||
}
|
||||
|
|
@ -242,6 +255,28 @@ public:
|
|||
return 0;
|
||||
}
|
||||
|
||||
virtual expr_ref lookahead(expr_ref_vector const& candidates) {
|
||||
sat::bool_var_vector vars;
|
||||
u_map<expr*> var2candidate;
|
||||
for (auto c : candidates) {
|
||||
// TBD: check membership
|
||||
sat::bool_var v = m_map.to_bool_var(c);
|
||||
SASSERT(v != sat::null_bool_var);
|
||||
vars.push_back(v);
|
||||
var2candidate.insert(v, c);
|
||||
}
|
||||
sat::literal l = m_solver.select_lookahead(vars);
|
||||
if (l == sat::null_literal) {
|
||||
return expr_ref(m.mk_true(), m);
|
||||
}
|
||||
expr* e;
|
||||
if (!var2candidate.find(l.var(), e)) {
|
||||
// TBD: if candidate set is empty, then do something else.
|
||||
e = m.mk_true();
|
||||
}
|
||||
return expr_ref(l.sign() ? m.mk_not(e) : e, m);
|
||||
}
|
||||
|
||||
virtual lbool get_consequences_core(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) {
|
||||
init_preprocess();
|
||||
TRACE("sat", tout << assumptions << "\n" << vars << "\n";);
|
||||
|
|
@ -320,9 +355,18 @@ public:
|
|||
virtual void get_labels(svector<symbol> & r) {
|
||||
}
|
||||
virtual unsigned get_num_assertions() const {
|
||||
return m_fmls.size();
|
||||
const_cast<inc_sat_solver*>(this)->convert_internalized();
|
||||
if (m_internalized && m_internalized_converted) {
|
||||
return m_internalized_fmls.size();
|
||||
}
|
||||
else {
|
||||
return m_fmls.size();
|
||||
}
|
||||
}
|
||||
virtual expr * get_assertion(unsigned idx) const {
|
||||
if (m_internalized && m_internalized_converted) {
|
||||
return m_internalized_fmls[idx];
|
||||
}
|
||||
return m_fmls[idx];
|
||||
}
|
||||
virtual unsigned get_num_assumptions() const {
|
||||
|
|
@ -332,6 +376,32 @@ public:
|
|||
return m_asmsf[idx];
|
||||
}
|
||||
|
||||
void convert_internalized() {
|
||||
if (!m_internalized) return;
|
||||
sat2goal s2g;
|
||||
model_converter_ref mc;
|
||||
goal g(m, false, false, false);
|
||||
s2g(m_solver, m_map, m_params, g, mc);
|
||||
extract_model();
|
||||
if (!m_model) {
|
||||
m_model = alloc(model, m);
|
||||
}
|
||||
model_ref mdl = m_model;
|
||||
if (m_mc) (*m_mc)(mdl);
|
||||
for (unsigned i = 0; i < mdl->get_num_constants(); ++i) {
|
||||
func_decl* c = mdl->get_constant(i);
|
||||
expr_ref eq(m.mk_eq(m.mk_const(c), mdl->get_const_interp(c)), m);
|
||||
g.assert_expr(eq);
|
||||
}
|
||||
m_internalized_fmls.reset();
|
||||
g.get_formulas(m_internalized_fmls);
|
||||
// g.display(std::cout);
|
||||
m_internalized_converted = true;
|
||||
// if (mc) mc->display(std::cout << "mc");
|
||||
// if (m_mc) m_mc->display(std::cout << "m_mc\n");
|
||||
// if (m_mc0) m_mc0->display(std::cout << "m_mc0\n");
|
||||
}
|
||||
|
||||
void init_preprocess() {
|
||||
if (m_preprocess) {
|
||||
m_preprocess->reset();
|
||||
|
|
@ -374,7 +444,7 @@ private:
|
|||
init_preprocess();
|
||||
SASSERT(g->models_enabled());
|
||||
SASSERT(!g->proofs_enabled());
|
||||
TRACE("goal2sat", g->display(tout););
|
||||
TRACE("sat", g->display(tout););
|
||||
try {
|
||||
(*m_preprocess)(g, m_subgoals, m_mc, m_pc, m_dep_core);
|
||||
}
|
||||
|
|
@ -391,7 +461,7 @@ private:
|
|||
}
|
||||
g = m_subgoals[0];
|
||||
expr_ref_vector atoms(m);
|
||||
TRACE("goal2sat", g->display_with_dependencies(tout););
|
||||
TRACE("sat", g->display_with_dependencies(tout););
|
||||
m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true);
|
||||
m_goal2sat.get_interpreted_atoms(atoms);
|
||||
if (!atoms.empty()) {
|
||||
|
|
|
|||
|
|
@ -39,6 +39,15 @@ namespace sat {
|
|||
m_queue.decreased(v);
|
||||
}
|
||||
|
||||
void activity_changed_eh(bool_var v, bool up) {
|
||||
if (m_queue.contains(v)) {
|
||||
if (up)
|
||||
m_queue.decreased(v);
|
||||
else
|
||||
m_queue.increased(v);
|
||||
}
|
||||
}
|
||||
|
||||
void mk_var_eh(bool_var v) {
|
||||
m_queue.reserve(v+1);
|
||||
m_queue.insert(v);
|
||||
|
|
@ -61,6 +70,8 @@ namespace sat {
|
|||
bool empty() const { return m_queue.empty(); }
|
||||
|
||||
bool_var next_var() { SASSERT(!empty()); return m_queue.erase_min(); }
|
||||
|
||||
bool_var min_var() { SASSERT(!empty()); return m_queue.min_value(); }
|
||||
};
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -137,7 +137,7 @@ struct goal2sat::imp {
|
|||
sat::bool_var v = m_solver.mk_var(ext);
|
||||
m_map.insert(t, v);
|
||||
l = sat::literal(v, sign);
|
||||
TRACE("goal2sat", tout << "new_var: " << v << "\n" << mk_ismt2_pp(t, m) << "\n";);
|
||||
TRACE("sat", tout << "new_var: " << v << ": " << mk_ismt2_pp(t, m) << "\n";);
|
||||
if (ext && !is_uninterp_const(t)) {
|
||||
m_interpreted_atoms.push_back(t);
|
||||
}
|
||||
|
|
@ -993,6 +993,7 @@ struct sat2goal::imp {
|
|||
expr_ref_vector m_lit2expr;
|
||||
unsigned long long m_max_memory;
|
||||
bool m_learned;
|
||||
unsigned m_glue;
|
||||
|
||||
imp(ast_manager & _m, params_ref const & p):m(_m), m_lit2expr(m) {
|
||||
updt_params(p);
|
||||
|
|
@ -1000,6 +1001,7 @@ struct sat2goal::imp {
|
|||
|
||||
void updt_params(params_ref const & p) {
|
||||
m_learned = p.get_bool("learned", false);
|
||||
m_glue = p.get_uint("glue", UINT_MAX);
|
||||
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
|
||||
}
|
||||
|
||||
|
|
@ -1042,20 +1044,71 @@ struct sat2goal::imp {
|
|||
return m_lit2expr.get(l.index());
|
||||
}
|
||||
|
||||
void assert_clauses(sat::clause * const * begin, sat::clause * const * end, goal & r) {
|
||||
void assert_pb(goal& r, sat::card_extension::pb const& p) {
|
||||
pb_util pb(m);
|
||||
ptr_buffer<expr> lits;
|
||||
vector<rational> coeffs;
|
||||
for (unsigned i = 0; i < p.size(); ++i) {
|
||||
lits.push_back(lit2expr(p[i].second));
|
||||
coeffs.push_back(rational(p[i].first));
|
||||
}
|
||||
rational k(p.k());
|
||||
expr_ref fml(pb.mk_ge(p.size(), coeffs.c_ptr(), lits.c_ptr(), k), m);
|
||||
|
||||
if (p.lit() != sat::null_literal) {
|
||||
fml = m.mk_eq(lit2expr(p.lit()), fml);
|
||||
}
|
||||
r.assert_expr(fml);
|
||||
}
|
||||
|
||||
void assert_card(goal& r, sat::card_extension::card const& c) {
|
||||
pb_util pb(m);
|
||||
ptr_buffer<expr> lits;
|
||||
for (unsigned i = 0; i < c.size(); ++i) {
|
||||
lits.push_back(lit2expr(c[i]));
|
||||
}
|
||||
expr_ref fml(pb.mk_at_most_k(c.size(), lits.c_ptr(), c.k()), m);
|
||||
|
||||
if (c.lit() != sat::null_literal) {
|
||||
fml = m.mk_eq(lit2expr(c.lit()), fml);
|
||||
}
|
||||
r.assert_expr(fml);
|
||||
}
|
||||
|
||||
void assert_xor(goal & r, sat::card_extension::xor const& x) {
|
||||
ptr_buffer<expr> lits;
|
||||
for (unsigned i = 0; i < x.size(); ++i) {
|
||||
lits.push_back(lit2expr(x[i]));
|
||||
}
|
||||
expr_ref fml(m.mk_xor(x.size(), lits.c_ptr()), m);
|
||||
|
||||
if (x.lit() != sat::null_literal) {
|
||||
fml = m.mk_eq(lit2expr(x.lit()), fml);
|
||||
}
|
||||
r.assert_expr(fml);
|
||||
}
|
||||
|
||||
void assert_clauses(sat::solver const & s, sat::clause * const * begin, sat::clause * const * end, goal & r, bool asserted) {
|
||||
ptr_buffer<expr> lits;
|
||||
for (sat::clause * const * it = begin; it != end; it++) {
|
||||
checkpoint();
|
||||
lits.reset();
|
||||
sat::clause const & c = *(*it);
|
||||
unsigned sz = c.size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
lits.push_back(lit2expr(c[i]));
|
||||
if (asserted || m_learned || c.glue() <= s.get_config().m_gc_small_lbd) {
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
lits.push_back(lit2expr(c[i]));
|
||||
}
|
||||
r.assert_expr(m.mk_or(lits.size(), lits.c_ptr()));
|
||||
}
|
||||
r.assert_expr(m.mk_or(lits.size(), lits.c_ptr()));
|
||||
}
|
||||
}
|
||||
|
||||
sat::card_extension* get_card_extension(sat::solver const& s) {
|
||||
sat::extension* ext = s.get_extension();
|
||||
return dynamic_cast<sat::card_extension*>(ext);
|
||||
}
|
||||
|
||||
void operator()(sat::solver const & s, atom2bool_var const & map, goal & r, model_converter_ref & mc) {
|
||||
if (s.inconsistent()) {
|
||||
r.assert_expr(m.mk_false());
|
||||
|
|
@ -1087,9 +1140,22 @@ struct sat2goal::imp {
|
|||
r.assert_expr(m.mk_or(lit2expr(it->first), lit2expr(it->second)));
|
||||
}
|
||||
// collect clauses
|
||||
assert_clauses(s.begin_clauses(), s.end_clauses(), r);
|
||||
if (m_learned)
|
||||
assert_clauses(s.begin_learned(), s.end_learned(), r);
|
||||
assert_clauses(s, s.begin_clauses(), s.end_clauses(), r, true);
|
||||
assert_clauses(s, s.begin_learned(), s.end_learned(), r, false);
|
||||
|
||||
// TBD: collect assertions from plugin
|
||||
sat::card_extension* ext = get_card_extension(s);
|
||||
if (ext) {
|
||||
for (unsigned i = 0; i < ext->num_pb(); ++i) {
|
||||
assert_pb(r, ext->get_pb(i));
|
||||
}
|
||||
for (unsigned i = 0; i < ext->num_card(); ++i) {
|
||||
assert_card(r, ext->get_card(i));
|
||||
}
|
||||
for (unsigned i = 0; i < ext->num_xor(); ++i) {
|
||||
assert_xor(r, ext->get_xor(i));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
};
|
||||
|
|
@ -1100,6 +1166,7 @@ sat2goal::sat2goal():m_imp(0) {
|
|||
void sat2goal::collect_param_descrs(param_descrs & r) {
|
||||
insert_max_memory(r);
|
||||
r.insert("learned", CPK_BOOL, "(default: false) collect also learned clauses.");
|
||||
r.insert("glue", CPK_UINT, "(default: max-int) collect learned clauses with glue level below parameter.");
|
||||
}
|
||||
|
||||
struct sat2goal::scoped_set_imp {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue