mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 00:55:31 +00:00
add cube functionality
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
ae9a6664d4
commit
82922d92f7
4 changed files with 83 additions and 58 deletions
|
|
@ -820,6 +820,15 @@ namespace sat {
|
|||
}
|
||||
return out;
|
||||
}
|
||||
|
||||
void lookahead::display_search_string() {
|
||||
printf("\r");
|
||||
std::stringstream strm;
|
||||
strm << pp_prefix(m_prefix, m_trail_lim.size());
|
||||
for (unsigned i = 0; i < 50; ++i) strm << " ";
|
||||
printf(strm.str().c_str());
|
||||
fflush(stdout);
|
||||
}
|
||||
|
||||
void lookahead::construct_lookahead_table() {
|
||||
literal u = get_child(null_literal), v = null_literal;
|
||||
|
|
@ -1710,47 +1719,6 @@ namespace sat {
|
|||
return true;
|
||||
}
|
||||
|
||||
void lookahead::cube() {
|
||||
m_model.reset();
|
||||
scoped_level _sl(*this, c_fixed_truth);
|
||||
literal_vector trail;
|
||||
m_search_mode = lookahead_mode::searching;
|
||||
double freevars_threshold = 0;
|
||||
while (true) {
|
||||
TRACE("sat", display(tout););
|
||||
inc_istamp();
|
||||
checkpoint();
|
||||
literal l = choose();
|
||||
if (inconsistent()) {
|
||||
freevars_threshold = m_freevars.size();
|
||||
if (!backtrack(trail)) return;
|
||||
continue;
|
||||
}
|
||||
unsigned depth = m_trail_lim.size();
|
||||
if (l == null_literal ||
|
||||
(m_config.m_cube_cutoff != 0 && depth == m_config.m_cube_cutoff) ||
|
||||
(m_config.m_cube_cutoff == 0 && m_freevars.size() < freevars_threshold)) {
|
||||
display_cube(std::cout);
|
||||
set_conflict();
|
||||
if (!backtrack(trail)) return;
|
||||
freevars_threshold *= (1.0 - pow(m_config.m_cube_fraction, depth));
|
||||
continue;
|
||||
}
|
||||
TRACE("sat", tout << "choose: " << l << " " << trail << "\n";);
|
||||
++m_stats.m_decisions;
|
||||
IF_VERBOSE(1, printf("\r");
|
||||
std::stringstream strm;
|
||||
strm << pp_prefix(m_prefix, m_trail_lim.size());
|
||||
for (unsigned i = 0; i < 50; ++i) strm << " ";
|
||||
printf(strm.str().c_str());
|
||||
fflush(stdout);
|
||||
);
|
||||
push(l, c_fixed_truth);
|
||||
trail.push_back(l);
|
||||
SASSERT(inconsistent() || !is_unsat());
|
||||
}
|
||||
}
|
||||
|
||||
lbool lookahead::search() {
|
||||
m_model.reset();
|
||||
scoped_level _sl(*this, c_fixed_truth);
|
||||
|
|
@ -1770,19 +1738,73 @@ namespace sat {
|
|||
}
|
||||
TRACE("sat", tout << "choose: " << l << " " << trail << "\n";);
|
||||
++m_stats.m_decisions;
|
||||
IF_VERBOSE(1, printf("\r");
|
||||
std::stringstream strm;
|
||||
strm << pp_prefix(m_prefix, m_trail_lim.size());
|
||||
for (unsigned i = 0; i < 50; ++i) strm << " ";
|
||||
printf(strm.str().c_str());
|
||||
fflush(stdout);
|
||||
);
|
||||
IF_VERBOSE(1, display_search_string(););
|
||||
push(l, c_fixed_truth);
|
||||
trail.push_back(l);
|
||||
SASSERT(inconsistent() || !is_unsat());
|
||||
}
|
||||
}
|
||||
|
||||
bool lookahead::backtrack(literal_vector& trail, svector<bool> & is_decision) {
|
||||
while (inconsistent()) {
|
||||
if (trail.empty()) return false;
|
||||
if (is_decision.back()) {
|
||||
pop();
|
||||
trail.back().neg();
|
||||
assign(trail.back());
|
||||
is_decision.back() = false;
|
||||
propagate();
|
||||
}
|
||||
else {
|
||||
trail.pop_back();
|
||||
is_decision.pop_back();
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
lbool lookahead::cube() {
|
||||
lbool result = l_false;
|
||||
init_search();
|
||||
m_model.reset();
|
||||
scoped_level _sl(*this, c_fixed_truth);
|
||||
literal_vector cube;
|
||||
svector<bool> is_decision;
|
||||
m_search_mode = lookahead_mode::searching;
|
||||
double freevars_threshold = 0;
|
||||
while (true) {
|
||||
TRACE("sat", display(tout););
|
||||
inc_istamp();
|
||||
checkpoint();
|
||||
literal l = choose();
|
||||
if (inconsistent()) {
|
||||
TRACE("sat", tout << "inconsistent: " << cube << "\n";);
|
||||
freevars_threshold = m_freevars.size();
|
||||
if (!backtrack(cube, is_decision)) return result;
|
||||
continue;
|
||||
}
|
||||
if (l == null_literal) {
|
||||
return l_true;
|
||||
}
|
||||
unsigned depth = cube.size();
|
||||
if ((m_config.m_cube_cutoff != 0 && depth == m_config.m_cube_cutoff) ||
|
||||
(m_config.m_cube_cutoff == 0 && m_freevars.size() < freevars_threshold)) {
|
||||
display_cube(std::cout, cube);
|
||||
freevars_threshold *= (1.0 - pow(m_config.m_cube_fraction, depth));
|
||||
result = l_undef;
|
||||
set_conflict();
|
||||
if (!backtrack(cube, is_decision)) return result;
|
||||
continue;
|
||||
}
|
||||
TRACE("sat", tout << "choose: " << l << " cube: " << cube << "\n";);
|
||||
++m_stats.m_decisions;
|
||||
push(l, c_fixed_truth);
|
||||
cube.push_back(l);
|
||||
is_decision.push_back(true);
|
||||
SASSERT(inconsistent() || !is_unsat());
|
||||
}
|
||||
}
|
||||
|
||||
void lookahead::init_model() {
|
||||
m_model.reset();
|
||||
for (unsigned i = 0; i < m_num_vars; ++i) {
|
||||
|
|
@ -1801,12 +1823,12 @@ namespace sat {
|
|||
}
|
||||
}
|
||||
|
||||
std::ostream& lookahead::display_cube(std::ostream& out) const {
|
||||
std::ostream& lookahead::display_cube(std::ostream& out, literal_vector const& cube) const {
|
||||
out << "c";
|
||||
for (literal l : m_assumptions) {
|
||||
for (literal l : cube) {
|
||||
out << " " << ~l;
|
||||
}
|
||||
return out << "\n";
|
||||
return out << " 0\n";
|
||||
}
|
||||
|
||||
std::ostream& lookahead::display_binary(std::ostream& out) const {
|
||||
|
|
|
|||
|
|
@ -444,13 +444,15 @@ namespace sat {
|
|||
void assign(literal l);
|
||||
void propagated(literal l);
|
||||
bool backtrack(literal_vector& trail);
|
||||
bool backtrack(literal_vector& trail, svector<bool> & is_decision);
|
||||
lbool search();
|
||||
void init_model();
|
||||
std::ostream& display_binary(std::ostream& out) const;
|
||||
std::ostream& display_clauses(std::ostream& out) const;
|
||||
std::ostream& display_values(std::ostream& out) const;
|
||||
std::ostream& display_lookahead(std::ostream& out) const;
|
||||
std::ostream& display_cube(std::ostream& out) const;
|
||||
std::ostream& display_cube(std::ostream& out, literal_vector const& cube) const;
|
||||
void display_search_string();
|
||||
|
||||
void init_search();
|
||||
void checkpoint();
|
||||
|
|
@ -486,7 +488,7 @@ namespace sat {
|
|||
If cut-depth != 0, then it is used to control the depth of cuts.
|
||||
Otherwise, cut-fraction gives an adaptive threshold for creating cuts.
|
||||
*/
|
||||
void cube();
|
||||
lbool cube();
|
||||
|
||||
literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars);
|
||||
/**
|
||||
|
|
|
|||
|
|
@ -857,8 +857,7 @@ namespace sat {
|
|||
return lookahead_search();
|
||||
}
|
||||
if (m_config.m_lookahead_cube && num_lits == 0) {
|
||||
lookahead_cube();
|
||||
return l_undef;
|
||||
return lookahead_cube();
|
||||
}
|
||||
if (m_config.m_local_search) {
|
||||
return do_local_search(num_lits, lits);
|
||||
|
|
@ -952,16 +951,18 @@ namespace sat {
|
|||
return r;
|
||||
}
|
||||
|
||||
void solver::lookahead_cube() {
|
||||
lbool solver::lookahead_cube() {
|
||||
lookahead lh(*this);
|
||||
lbool r = l_undef;
|
||||
try {
|
||||
lh.cube();
|
||||
r = lh.cube();
|
||||
}
|
||||
catch (z3_exception&) {
|
||||
lh.collect_statistics(m_aux_stats);
|
||||
throw;
|
||||
}
|
||||
lh.collect_statistics(m_aux_stats);
|
||||
return r;
|
||||
}
|
||||
|
||||
lbool solver::lookahead_search() {
|
||||
|
|
|
|||
|
|
@ -403,7 +403,7 @@ namespace sat {
|
|||
void exchange_par();
|
||||
lbool check_par(unsigned num_lits, literal const* lits);
|
||||
lbool lookahead_search();
|
||||
void lookahead_cube();
|
||||
lbool lookahead_cube();
|
||||
lbool do_local_search(unsigned num_lits, literal const* lits);
|
||||
lbool do_ccc();
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue