mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 09:35:32 +00:00
ccc
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
86a54dfec8
commit
07fe45e923
4 changed files with 340 additions and 720 deletions
|
|
@ -35,11 +35,11 @@ std::ostream& ccc::pp(std::ostream& out, svector<decision> const& v) {
|
|||
return out;
|
||||
}
|
||||
|
||||
lbool ccc::cube() {
|
||||
lbool ccc::cube2() {
|
||||
unsigned branch_id = 0;
|
||||
unsigned_vector id_trail;
|
||||
|
||||
lookahead lh(s);
|
||||
lookahead lh(m_s);
|
||||
lh.init_search();
|
||||
lh.m_model.reset();
|
||||
|
||||
|
|
@ -47,13 +47,115 @@ lbool ccc::cube() {
|
|||
literal_vector trail;
|
||||
svector<decision> decisions;
|
||||
lh.m_search_mode = lookahead_mode::searching;
|
||||
lh.m_blocked_literal = null_literal;
|
||||
lbool r = cube2(branch_id, decisions, lh);
|
||||
if (r == l_true) {
|
||||
m_model = lh.get_model();
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
lbool ccc::cube2(unsigned& branch_id, svector<decision>& decisions, lookahead& lh) {
|
||||
m_s.checkpoint();
|
||||
|
||||
if (lh.inconsistent()) {
|
||||
return l_false;
|
||||
}
|
||||
|
||||
lh.inc_istamp();
|
||||
|
||||
// check if CDCL solver got ahead.
|
||||
bool repeat = false;
|
||||
#pragma omp critical (ccc_solved)
|
||||
{
|
||||
while (!m_solved.empty()) {
|
||||
unsigned solved_id = m_solved.top();
|
||||
if (contains_branch(decisions, solved_id)) {
|
||||
IF_VERBOSE(1, verbose_stream() << "conquer " << decisions.size() << "\n";);
|
||||
repeat = true;
|
||||
break;
|
||||
}
|
||||
else {
|
||||
m_solved.pop();
|
||||
}
|
||||
}
|
||||
}
|
||||
if (repeat) return l_false;
|
||||
|
||||
literal l = lh.choose();
|
||||
if (lh.inconsistent()) {
|
||||
return l_false;
|
||||
}
|
||||
|
||||
if (l == null_literal) {
|
||||
return l_true;
|
||||
}
|
||||
|
||||
if (!decisions.empty()) {
|
||||
#pragma omp critical (ccc_decisions)
|
||||
{
|
||||
m_decisions.push(decisions.back());
|
||||
}
|
||||
}
|
||||
|
||||
// update trail and set of ids
|
||||
|
||||
++branch_id;
|
||||
++lh.m_stats.m_decisions;
|
||||
unsigned parent_id = decisions.empty() ? 0 : decisions.back().m_id;
|
||||
decision d(branch_id, decisions.size() + 1, l, null_literal, parent_id);
|
||||
decisions.push_back(d);
|
||||
|
||||
#pragma omp critical (ccc_log)
|
||||
{
|
||||
IF_VERBOSE(1, verbose_stream() << "select " << pp_prefix(lh.m_prefix, lh.m_trail_lim.size()) << ": " << l << " " << lh.m_trail.size() << "\n";);
|
||||
IF_VERBOSE(2, pp(verbose_stream(), decisions) << "\n"; );
|
||||
}
|
||||
TRACE("sat", tout << "choose: " << l << " " << trail << "\n";);
|
||||
lh.push(l, lh.c_fixed_truth);
|
||||
lbool r = cube2(branch_id, decisions, lh);
|
||||
if (r == l_false) {
|
||||
lh.pop();
|
||||
lh.flip_prefix();
|
||||
lh.push(~l, lh.c_fixed_truth);
|
||||
decisions.back().m_last = ~l;
|
||||
r = cube2(branch_id, decisions, lh);
|
||||
if (r == l_false) {
|
||||
lh.pop();
|
||||
decisions.pop_back();
|
||||
}
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
bool ccc::contains_branch(svector<decision> const& decisions, unsigned branch_id) const {
|
||||
for (unsigned i = 0; i < decisions.size(); ++i) {
|
||||
if (branch_id == decisions[i].m_id) return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
lbool ccc::cube() {
|
||||
unsigned branch_id = 0;
|
||||
unsigned_vector id_trail;
|
||||
|
||||
lookahead lh(m_s);
|
||||
lh.init_search();
|
||||
lh.m_model.reset();
|
||||
|
||||
lookahead::scoped_level _sl(lh, lh.c_fixed_truth);
|
||||
literal_vector trail;
|
||||
svector<decision> decisions;
|
||||
lh.m_search_mode = lookahead_mode::searching;
|
||||
lh.m_blocked_literal = null_literal;
|
||||
while (!m_cancel) {
|
||||
|
||||
s.checkpoint();
|
||||
m_s.checkpoint();
|
||||
|
||||
SASSERT(trail.size() <= decisions.size());
|
||||
while (trail.size() < decisions.size()) {
|
||||
check_non_model("lh inconsistent ", decisions);
|
||||
//check_non_model("lh inconsistent ", decisions);
|
||||
decisions.pop_back();
|
||||
id_trail.pop_back();
|
||||
}
|
||||
|
|
@ -76,6 +178,7 @@ lbool ccc::cube() {
|
|||
if (!m_solved.empty()) {
|
||||
unsigned solved_id = m_solved.top();
|
||||
if (id_trail.contains(solved_id)) {
|
||||
IF_VERBOSE(1, verbose_stream() << "cconquer " << decisions.size() << "\n";);
|
||||
lh.set_conflict();
|
||||
}
|
||||
else {
|
||||
|
|
@ -86,7 +189,6 @@ lbool ccc::cube() {
|
|||
}
|
||||
if (repeat) continue;
|
||||
|
||||
|
||||
literal l = lh.choose();
|
||||
if (lh.inconsistent()) {
|
||||
if (!lh.backtrack(trail)) return l_false;
|
||||
|
|
@ -102,17 +204,17 @@ lbool ccc::cube() {
|
|||
++branch_id;
|
||||
++lh.m_stats.m_decisions;
|
||||
unsigned parent_id = id_trail.empty() ? 0 : id_trail.back();
|
||||
decision d(branch_id, trail.size() + 1, l, parent_id);
|
||||
decision d(branch_id, trail.size() + 1, l, lh.m_blocked_literal, parent_id);
|
||||
id_trail.push_back(branch_id);
|
||||
trail.push_back(l);
|
||||
decisions.push_back(d);
|
||||
SASSERT(id_trail.size() == trail.size());
|
||||
lh.m_blocked_literal = null_literal;
|
||||
|
||||
#pragma omp critical (ccc_log)
|
||||
{
|
||||
IF_VERBOSE(1, verbose_stream() << "select " << pp_prefix(lh.m_prefix, lh.m_trail_lim.size()) << ": " << l << " " << lh.m_trail.size() << " " << trail << "\n";
|
||||
pp(verbose_stream(), decisions) << "\n";
|
||||
);
|
||||
IF_VERBOSE(1, verbose_stream() << "select " << pp_prefix(lh.m_prefix, lh.m_trail_lim.size()) << ": " << l << " " << lh.m_trail.size() << "\n";);
|
||||
IF_VERBOSE(2, verbose_stream() << " " << trail << "\n"; pp(verbose_stream(), decisions) << "\n"; );
|
||||
}
|
||||
#pragma omp critical (ccc_decisions)
|
||||
{
|
||||
|
|
@ -148,7 +250,6 @@ lbool ccc::conquer(solver& s) {
|
|||
s.simplify_problem();
|
||||
if (s.check_inconsistent()) return l_false;
|
||||
s.gc();
|
||||
|
||||
}
|
||||
}
|
||||
catch (solver::abort_solver) {
|
||||
|
|
@ -157,41 +258,110 @@ lbool ccc::conquer(solver& s) {
|
|||
}
|
||||
|
||||
void ccc::replay_decisions(solver& s, svector<decision>& decisions) {
|
||||
// replay decisions
|
||||
bool shortcut = false;
|
||||
s.propagate(true);
|
||||
for (unsigned i = s.scope_lvl(); !shortcut && !s.inconsistent() && i < decisions.size(); ++i) {
|
||||
for (unsigned i = s.scope_lvl(); !s.inconsistent() && i < decisions.size(); ++i) {
|
||||
decision d = decisions[i];
|
||||
literal lit = d.m_last;
|
||||
lbool val = s.value(lit);
|
||||
#pragma omp critical (ccc_log)
|
||||
{
|
||||
IF_VERBOSE(1, verbose_stream() << "replay " << lit << " " << val << "\n";);
|
||||
IF_VERBOSE(2, verbose_stream() << "replay " << lit << " " << val << "\n";);
|
||||
}
|
||||
switch (val) {
|
||||
if (!push_decision(s, d)) {
|
||||
// negation of decision is implied.
|
||||
// check_non_model("replay", decisions);
|
||||
decisions.resize(i);
|
||||
return;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
bool ccc::push_decision(solver& s, decision const& d) {
|
||||
literal lit = d.m_last;
|
||||
switch (s.value(lit)) {
|
||||
case l_false:
|
||||
#pragma omp critical (ccc_solved)
|
||||
{
|
||||
m_solved.push(d.m_id);
|
||||
}
|
||||
//TBD:
|
||||
s.m_restart_threshold = s.m_config.m_restart_initial;
|
||||
//s.m_conflicts_since_last_restart = 0;
|
||||
return false;
|
||||
case l_true:
|
||||
s.push();
|
||||
break;
|
||||
case l_undef:
|
||||
s.push();
|
||||
s.assign(lit, justification());
|
||||
s.propagate(true);
|
||||
break;
|
||||
}
|
||||
literal blocked = d.m_blocked;
|
||||
if (false && blocked != null_literal) {
|
||||
switch (s.value(blocked)) {
|
||||
case l_false:
|
||||
#pragma omp critical (ccc_solved)
|
||||
{
|
||||
m_solved.push(d.m_id);
|
||||
}
|
||||
check_non_model("replay", decisions);
|
||||
decisions.resize(i);
|
||||
shortcut = true;
|
||||
return false;
|
||||
case l_true:
|
||||
break;
|
||||
case l_undef:
|
||||
s.push();
|
||||
s.assign(lit, justification());
|
||||
s.propagate(false);
|
||||
//s.assign(blocked, justification());
|
||||
//s.propagate(true);
|
||||
break;
|
||||
case l_true:
|
||||
s.push();
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
lbool ccc::bounded_search(solver& s, svector<decision>& decisions) {
|
||||
bool ccc::cube_decision(solver& s, svector<decision>& decisions) {
|
||||
decision d;
|
||||
bool use_cube_decision = false;
|
||||
SASSERT(s.m_qhead == s.m_trail.size());
|
||||
get_cube:
|
||||
#pragma omp critical (ccc_decisions)
|
||||
{
|
||||
if (!m_decisions.empty()) {
|
||||
d = m_decisions.pop();
|
||||
use_cube_decision = true;
|
||||
}
|
||||
}
|
||||
|
||||
if (!use_cube_decision) {
|
||||
return false;
|
||||
}
|
||||
|
||||
if (!decisions.empty() && decisions.back().m_depth + 1 < d.m_depth) {
|
||||
goto get_cube;
|
||||
}
|
||||
|
||||
while (!decisions.empty() && decisions.back().m_depth >= d.m_depth) {
|
||||
// check_non_model("cube decision", decisions);
|
||||
decisions.pop_back();
|
||||
}
|
||||
SASSERT(decisions.empty() || decisions.back().m_depth + 1 == d.m_depth);
|
||||
SASSERT(decisions.empty() || decisions.back().m_id == d.m_parent);
|
||||
s.pop_reinit(s.scope_lvl() - decisions.size());
|
||||
SASSERT(s.m_qhead == s.m_trail.size());
|
||||
SASSERT(s.scope_lvl() == decisions.size());
|
||||
#pragma omp critical (ccc_log)
|
||||
{
|
||||
literal lit = d.m_last;
|
||||
IF_VERBOSE(1, verbose_stream() << "cube " << decisions.size() << "\n";);
|
||||
IF_VERBOSE(2, pp(verbose_stream() << "push ", decisions) << " @ " << s.scope_lvl() << " " << s.value(lit) << "\n";
|
||||
if (s.value(lit) == l_false) verbose_stream() << "level: " << s.lvl(lit) << "\n";);
|
||||
}
|
||||
if (push_decision(s, d)) {
|
||||
decisions.push_back(d);
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
lbool ccc::bounded_search(solver& s, svector<decision>& decisions) {
|
||||
while (true) {
|
||||
s.checkpoint();
|
||||
bool done = false;
|
||||
|
|
@ -202,50 +372,8 @@ lbool ccc::bounded_search(solver& s, svector<decision>& decisions) {
|
|||
}
|
||||
|
||||
s.gc();
|
||||
|
||||
decision d;
|
||||
bool cube_decision = false;
|
||||
#pragma omp critical (ccc_decisions)
|
||||
{
|
||||
if (!m_decisions.empty()) {
|
||||
d = m_decisions.pop();
|
||||
cube_decision = true;
|
||||
}
|
||||
}
|
||||
|
||||
if (cube_decision) {
|
||||
if (d.m_depth > 1 + decisions.size()) continue;
|
||||
while (!decisions.empty() && decisions.back().m_depth >= d.m_depth) {
|
||||
SASSERT(decisions.back().m_depth == decisions.size());
|
||||
check_non_model("cube decision", decisions);
|
||||
decisions.pop_back();
|
||||
}
|
||||
SASSERT(decisions.empty() || decisions.back().m_depth + 1 == d.m_depth);
|
||||
SASSERT(decisions.empty() || decisions.back().m_id == d.m_parent);
|
||||
decisions.push_back(d);
|
||||
s.pop_reinit(s.m_scope_lvl + 1 - d.m_depth); // TBD: check alignment of scopes
|
||||
literal lit = d.m_last;
|
||||
#pragma omp critical (ccc_log)
|
||||
{
|
||||
IF_VERBOSE(1, pp(verbose_stream() << "push ", decisions) << " @ " << s.scope_lvl() << " " << s.value(lit) << "\n";
|
||||
if (s.value(lit) == l_false) verbose_stream() << "level: " << s.lvl(lit) << "\n";);
|
||||
}
|
||||
switch (s.value(lit)) {
|
||||
case l_false:
|
||||
decisions.pop_back();
|
||||
#pragma omp critical (ccc_solved)
|
||||
{
|
||||
m_solved.push(d.m_id);
|
||||
}
|
||||
break;
|
||||
case l_true:
|
||||
case l_undef:
|
||||
s.push();
|
||||
s.assign(lit, justification());
|
||||
break;
|
||||
}
|
||||
}
|
||||
else if (!s.decide()) {
|
||||
|
||||
if (!cube_decision(s, decisions) && !s.decide()) {
|
||||
lbool is_sat = s.final_check();
|
||||
if (is_sat != l_undef) {
|
||||
return is_sat;
|
||||
|
|
@ -254,521 +382,6 @@ lbool ccc::bounded_search(solver& s, svector<decision>& decisions) {
|
|||
}
|
||||
}
|
||||
|
||||
void ccc::set_model() {
|
||||
push_model(1, false);
|
||||
push_model(2, false);
|
||||
push_model(3, false);
|
||||
push_model(4, false);
|
||||
push_model(5, false);
|
||||
push_model(6, false);
|
||||
push_model(7, false);
|
||||
push_model(8, false);
|
||||
push_model(9, true);
|
||||
push_model(10, true);
|
||||
push_model(11, true);
|
||||
push_model(12, true);
|
||||
push_model(13, true);
|
||||
push_model(14, true);
|
||||
push_model(15, true);
|
||||
push_model(16, true);
|
||||
push_model(17, true);
|
||||
push_model(18, true);
|
||||
push_model(19, true);
|
||||
push_model(20, true);
|
||||
push_model(21, true);
|
||||
push_model(22, true);
|
||||
push_model(23, true);
|
||||
push_model(24, true);
|
||||
push_model(25, true);
|
||||
push_model(26, true);
|
||||
push_model(27, true);
|
||||
push_model(28, true);
|
||||
push_model(29, true);
|
||||
push_model(30, true);
|
||||
push_model(31, true);
|
||||
push_model(32, true);
|
||||
push_model(33, true);
|
||||
push_model(34, true);
|
||||
push_model(35, true);
|
||||
push_model(36, true);
|
||||
push_model(37, true);
|
||||
push_model(38, true);
|
||||
push_model(39, true);
|
||||
push_model(40, true);
|
||||
push_model(41, false);
|
||||
push_model(42, true);
|
||||
push_model(43, true);
|
||||
push_model(44, true);
|
||||
push_model(45, true);
|
||||
push_model(46, true);
|
||||
push_model(47, true);
|
||||
push_model(48, false);
|
||||
push_model(49, true);
|
||||
push_model(50, true);
|
||||
push_model(51, true);
|
||||
push_model(52, true);
|
||||
push_model(53, true);
|
||||
push_model(54, false);
|
||||
push_model(55, true);
|
||||
push_model(56, true);
|
||||
push_model(57, true);
|
||||
push_model(58, true);
|
||||
push_model(59, true);
|
||||
push_model(60, true);
|
||||
push_model(61, true);
|
||||
push_model(62, true);
|
||||
push_model(63, true);
|
||||
push_model(64, true);
|
||||
push_model(65, true);
|
||||
push_model(66, true);
|
||||
push_model(67, true);
|
||||
push_model(68, false);
|
||||
push_model(69, true);
|
||||
push_model(70, true);
|
||||
push_model(71, false);
|
||||
push_model(72, true);
|
||||
push_model(73, true);
|
||||
push_model(74, true);
|
||||
push_model(75, true);
|
||||
push_model(76, true);
|
||||
push_model(77, true);
|
||||
push_model(78, true);
|
||||
push_model(79, true);
|
||||
push_model(80, true);
|
||||
push_model(81, true);
|
||||
push_model(82, false);
|
||||
push_model(83, true);
|
||||
push_model(84, true);
|
||||
push_model(85, true);
|
||||
push_model(86, true);
|
||||
push_model(87, true);
|
||||
push_model(88, true);
|
||||
push_model(89, true);
|
||||
push_model(90, true);
|
||||
push_model(91, false);
|
||||
push_model(92, true);
|
||||
push_model(93, true);
|
||||
push_model(94, true);
|
||||
push_model(95, true);
|
||||
push_model(96, true);
|
||||
push_model(97, true);
|
||||
push_model(98, true);
|
||||
push_model(99, false);
|
||||
push_model(100, true);
|
||||
push_model(101, true);
|
||||
push_model(102, true);
|
||||
push_model(103, true);
|
||||
push_model(104, true);
|
||||
push_model(105, true);
|
||||
push_model(106, true);
|
||||
push_model(107, true);
|
||||
push_model(108, true);
|
||||
push_model(109, true);
|
||||
push_model(110, true);
|
||||
push_model(111, true);
|
||||
push_model(112, true);
|
||||
push_model(113, false);
|
||||
push_model(114, true);
|
||||
push_model(115, true);
|
||||
push_model(116, true);
|
||||
push_model(117, true);
|
||||
push_model(118, true);
|
||||
push_model(119, true);
|
||||
push_model(120, false);
|
||||
push_model(121, true);
|
||||
push_model(122, true);
|
||||
push_model(123, true);
|
||||
push_model(124, true);
|
||||
push_model(125, true);
|
||||
push_model(126, false);
|
||||
push_model(127, true);
|
||||
push_model(128, true);
|
||||
push_model(129, true);
|
||||
push_model(130, true);
|
||||
push_model(131, true);
|
||||
push_model(132, true);
|
||||
push_model(133, true);
|
||||
push_model(134, true);
|
||||
push_model(135, true);
|
||||
push_model(136, true);
|
||||
push_model(137, true);
|
||||
push_model(138, true);
|
||||
push_model(139, false);
|
||||
push_model(140, true);
|
||||
push_model(141, true);
|
||||
push_model(142, true);
|
||||
push_model(143, false);
|
||||
push_model(144, true);
|
||||
push_model(145, true);
|
||||
push_model(146, true);
|
||||
push_model(147, true);
|
||||
push_model(148, false);
|
||||
push_model(149, true);
|
||||
push_model(150, true);
|
||||
push_model(151, true);
|
||||
push_model(152, true);
|
||||
push_model(153, true);
|
||||
push_model(154, true);
|
||||
push_model(155, true);
|
||||
push_model(156, true);
|
||||
push_model(157, true);
|
||||
push_model(158, true);
|
||||
push_model(159, true);
|
||||
push_model(160, false);
|
||||
push_model(161, true);
|
||||
push_model(162, true);
|
||||
push_model(163, true);
|
||||
push_model(164, false);
|
||||
push_model(165, true);
|
||||
push_model(166, true);
|
||||
push_model(167, true);
|
||||
push_model(168, true);
|
||||
push_model(169, true);
|
||||
push_model(170, true);
|
||||
push_model(171, true);
|
||||
push_model(172, true);
|
||||
push_model(173, true);
|
||||
push_model(174, true);
|
||||
push_model(175, true);
|
||||
push_model(176, true);
|
||||
push_model(177, true);
|
||||
push_model(178, true);
|
||||
push_model(179, true);
|
||||
push_model(180, true);
|
||||
push_model(181, true);
|
||||
push_model(182, true);
|
||||
push_model(183, true);
|
||||
push_model(184, true);
|
||||
push_model(185, false);
|
||||
push_model(186, true);
|
||||
push_model(187, true);
|
||||
push_model(188, true);
|
||||
push_model(189, true);
|
||||
push_model(190, true);
|
||||
push_model(191, true);
|
||||
push_model(192, false);
|
||||
push_model(193, true);
|
||||
push_model(194, true);
|
||||
push_model(195, true);
|
||||
push_model(196, true);
|
||||
push_model(197, true);
|
||||
push_model(198, false);
|
||||
push_model(199, true);
|
||||
push_model(200, true);
|
||||
push_model(201, true);
|
||||
push_model(202, true);
|
||||
push_model(203, true);
|
||||
push_model(204, true);
|
||||
push_model(205, true);
|
||||
push_model(206, true);
|
||||
push_model(207, true);
|
||||
push_model(208, true);
|
||||
push_model(209, true);
|
||||
push_model(210, false);
|
||||
push_model(211, false);
|
||||
push_model(212, true);
|
||||
push_model(213, true);
|
||||
push_model(214, true);
|
||||
push_model(215, true);
|
||||
push_model(216, true);
|
||||
push_model(217, true);
|
||||
push_model(218, true);
|
||||
push_model(219, true);
|
||||
push_model(220, true);
|
||||
push_model(221, true);
|
||||
push_model(222, true);
|
||||
push_model(223, true);
|
||||
push_model(224, true);
|
||||
push_model(225, false);
|
||||
push_model(226, true);
|
||||
push_model(227, true);
|
||||
push_model(228, true);
|
||||
push_model(229, true);
|
||||
push_model(230, true);
|
||||
push_model(231, false);
|
||||
push_model(232, true);
|
||||
push_model(233, true);
|
||||
push_model(234, true);
|
||||
push_model(235, false);
|
||||
push_model(236, true);
|
||||
push_model(237, true);
|
||||
push_model(238, true);
|
||||
push_model(239, true);
|
||||
push_model(240, true);
|
||||
push_model(241, true);
|
||||
push_model(242, true);
|
||||
push_model(243, true);
|
||||
push_model(244, true);
|
||||
push_model(245, true);
|
||||
push_model(246, true);
|
||||
push_model(247, true);
|
||||
push_model(248, true);
|
||||
push_model(249, false);
|
||||
push_model(250, true);
|
||||
push_model(251, true);
|
||||
push_model(252, true);
|
||||
push_model(253, true);
|
||||
push_model(254, true);
|
||||
push_model(255, true);
|
||||
push_model(256, true);
|
||||
push_model(257, true);
|
||||
push_model(258, true);
|
||||
push_model(259, true);
|
||||
push_model(260, true);
|
||||
push_model(261, true);
|
||||
push_model(262, true);
|
||||
push_model(263, false);
|
||||
push_model(264, true);
|
||||
push_model(265, true);
|
||||
push_model(266, true);
|
||||
push_model(267, true);
|
||||
push_model(268, true);
|
||||
push_model(269, false);
|
||||
push_model(270, true);
|
||||
push_model(271, true);
|
||||
push_model(272, true);
|
||||
push_model(273, false);
|
||||
push_model(274, true);
|
||||
push_model(275, true);
|
||||
push_model(276, true);
|
||||
push_model(277, true);
|
||||
push_model(278, true);
|
||||
push_model(279, true);
|
||||
push_model(280, true);
|
||||
push_model(281, true);
|
||||
push_model(282, true);
|
||||
push_model(283, true);
|
||||
push_model(284, false);
|
||||
push_model(285, true);
|
||||
push_model(286, true);
|
||||
push_model(287, true);
|
||||
push_model(288, true);
|
||||
push_model(289, true);
|
||||
push_model(290, true);
|
||||
push_model(291, true);
|
||||
push_model(292, true);
|
||||
push_model(293, true);
|
||||
push_model(294, false);
|
||||
push_model(295, true);
|
||||
push_model(296, true);
|
||||
push_model(297, true);
|
||||
push_model(298, true);
|
||||
push_model(299, true);
|
||||
push_model(300, true);
|
||||
push_model(301, false);
|
||||
push_model(302, true);
|
||||
push_model(303, true);
|
||||
push_model(304, true);
|
||||
push_model(305, false);
|
||||
push_model(306, true);
|
||||
push_model(307, true);
|
||||
push_model(308, true);
|
||||
push_model(309, true);
|
||||
push_model(310, true);
|
||||
push_model(311, true);
|
||||
push_model(312, true);
|
||||
push_model(313, true);
|
||||
push_model(314, true);
|
||||
push_model(315, true);
|
||||
push_model(316, true);
|
||||
push_model(317, true);
|
||||
push_model(318, true);
|
||||
push_model(319, false);
|
||||
push_model(320, true);
|
||||
push_model(321, true);
|
||||
push_model(322, true);
|
||||
push_model(323, true);
|
||||
push_model(324, true);
|
||||
push_model(325, true);
|
||||
push_model(326, false);
|
||||
push_model(327, true);
|
||||
push_model(328, true);
|
||||
push_model(329, true);
|
||||
push_model(330, true);
|
||||
push_model(331, true);
|
||||
push_model(332, true);
|
||||
push_model(333, true);
|
||||
push_model(334, false);
|
||||
push_model(335, true);
|
||||
push_model(336, true);
|
||||
push_model(337, true);
|
||||
push_model(338, true);
|
||||
push_model(339, true);
|
||||
push_model(340, false);
|
||||
push_model(341, true);
|
||||
push_model(342, true);
|
||||
push_model(343, true);
|
||||
push_model(344, true);
|
||||
push_model(345, true);
|
||||
push_model(346, true);
|
||||
push_model(347, true);
|
||||
push_model(348, true);
|
||||
push_model(349, true);
|
||||
push_model(350, true);
|
||||
push_model(351, true);
|
||||
push_model(352, true);
|
||||
push_model(353, false);
|
||||
push_model(354, true);
|
||||
push_model(355, true);
|
||||
push_model(356, true);
|
||||
push_model(357, true);
|
||||
push_model(358, true);
|
||||
push_model(359, true);
|
||||
push_model(360, true);
|
||||
push_model(361, true);
|
||||
push_model(362, false);
|
||||
push_model(363, false);
|
||||
push_model(364, true);
|
||||
push_model(365, true);
|
||||
push_model(366, true);
|
||||
push_model(367, true);
|
||||
push_model(368, true);
|
||||
push_model(369, true);
|
||||
push_model(370, true);
|
||||
push_model(371, true);
|
||||
push_model(372, true);
|
||||
push_model(373, true);
|
||||
push_model(374, false);
|
||||
push_model(375, true);
|
||||
push_model(376, true);
|
||||
push_model(377, true);
|
||||
push_model(378, true);
|
||||
push_model(379, true);
|
||||
push_model(380, true);
|
||||
push_model(381, true);
|
||||
push_model(382, true);
|
||||
push_model(383, true);
|
||||
push_model(384, true);
|
||||
push_model(385, true);
|
||||
push_model(386, true);
|
||||
push_model(387, true);
|
||||
push_model(388, false);
|
||||
push_model(389, true);
|
||||
push_model(390, true);
|
||||
push_model(391, true);
|
||||
push_model(392, true);
|
||||
push_model(393, true);
|
||||
push_model(394, false);
|
||||
push_model(395, true);
|
||||
push_model(396, true);
|
||||
push_model(397, true);
|
||||
push_model(398, true);
|
||||
push_model(399, true);
|
||||
push_model(400, true);
|
||||
push_model(401, false);
|
||||
push_model(402, true);
|
||||
push_model(403, true);
|
||||
push_model(404, true);
|
||||
push_model(405, true);
|
||||
push_model(406, true);
|
||||
push_model(407, true);
|
||||
push_model(408, false);
|
||||
push_model(409, true);
|
||||
push_model(410, true);
|
||||
push_model(411, true);
|
||||
push_model(412, true);
|
||||
push_model(413, true);
|
||||
push_model(414, false);
|
||||
push_model(415, true);
|
||||
push_model(416, true);
|
||||
push_model(417, true);
|
||||
push_model(418, true);
|
||||
push_model(419, true);
|
||||
push_model(420, true);
|
||||
push_model(421, true);
|
||||
push_model(422, true);
|
||||
push_model(423, true);
|
||||
push_model(424, true);
|
||||
push_model(425, true);
|
||||
push_model(426, true);
|
||||
push_model(427, true);
|
||||
push_model(428, true);
|
||||
push_model(429, false);
|
||||
push_model(430, true);
|
||||
push_model(431, false);
|
||||
push_model(432, true);
|
||||
push_model(433, true);
|
||||
push_model(434, true);
|
||||
push_model(435, true);
|
||||
push_model(436, true);
|
||||
push_model(437, true);
|
||||
push_model(438, true);
|
||||
push_model(439, true);
|
||||
push_model(440, true);
|
||||
push_model(441, true);
|
||||
push_model(442, false);
|
||||
push_model(443, true);
|
||||
push_model(444, true);
|
||||
push_model(445, true);
|
||||
push_model(446, true);
|
||||
push_model(447, true);
|
||||
push_model(448, true);
|
||||
push_model(449, true);
|
||||
push_model(450, true);
|
||||
push_model(451, true);
|
||||
push_model(452, true);
|
||||
push_model(453, false);
|
||||
push_model(454, true);
|
||||
push_model(455, true);
|
||||
push_model(456, true);
|
||||
push_model(457, true);
|
||||
push_model(458, false);
|
||||
push_model(459, true);
|
||||
push_model(460, true);
|
||||
push_model(461, true);
|
||||
push_model(462, true);
|
||||
push_model(463, true);
|
||||
push_model(464, true);
|
||||
push_model(465, true);
|
||||
push_model(466, true);
|
||||
push_model(467, false);
|
||||
push_model(468, true);
|
||||
push_model(469, true);
|
||||
push_model(470, true);
|
||||
push_model(471, true);
|
||||
push_model(472, true);
|
||||
push_model(473, true);
|
||||
push_model(474, true);
|
||||
push_model(475, true);
|
||||
push_model(476, false);
|
||||
push_model(477, true);
|
||||
push_model(478, true);
|
||||
push_model(479, true);
|
||||
push_model(480, true);
|
||||
push_model(481, true);
|
||||
push_model(482, true);
|
||||
push_model(483, true);
|
||||
push_model(484, true);
|
||||
push_model(485, false);
|
||||
push_model(486, true);
|
||||
push_model(487, true);
|
||||
push_model(488, true);
|
||||
push_model(489, true);
|
||||
push_model(490, true);
|
||||
push_model(491, true);
|
||||
push_model(492, true);
|
||||
push_model(493, true);
|
||||
push_model(494, false);
|
||||
push_model(495, true);
|
||||
push_model(496, false);
|
||||
push_model(497, true);
|
||||
push_model(498, true);
|
||||
push_model(499, true);
|
||||
push_model(500, true);
|
||||
push_model(501, true);
|
||||
push_model(502, true);
|
||||
push_model(503, true);
|
||||
push_model(504, true);
|
||||
push_model(505, false);
|
||||
push_model(506, true);
|
||||
push_model(507, true);
|
||||
push_model(508, true);
|
||||
push_model(509, true);
|
||||
push_model(510, true);
|
||||
push_model(511, true);
|
||||
push_model(512, true);
|
||||
|
||||
}
|
||||
|
||||
void ccc::push_model(unsigned v, bool sign) {
|
||||
if (m_values.size() <= v) {
|
||||
|
|
@ -796,11 +409,11 @@ lbool ccc::search() {
|
|||
ERROR_EX
|
||||
};
|
||||
|
||||
set_model();
|
||||
// set_model();
|
||||
|
||||
m_cancel = false;
|
||||
|
||||
scoped_limits scoped_rlimit(s.rlimit());
|
||||
scoped_limits scoped_rlimit(m_s.rlimit());
|
||||
vector<reslimit> limits;
|
||||
ptr_vector<solver> solvers;
|
||||
int finished_id = -1;
|
||||
|
|
@ -808,18 +421,15 @@ lbool ccc::search() {
|
|||
par_exception_kind ex_kind;
|
||||
unsigned error_code = 0;
|
||||
lbool result = l_undef;
|
||||
bool canceled = false;
|
||||
|
||||
int num_threads = 2; // for ccc-infinity only two threads. s.m_config.m_num_threads + 1;
|
||||
for (int i = 1; i < num_threads; ++i) {
|
||||
limits.push_back(reslimit());
|
||||
}
|
||||
|
||||
for (int i = 1; i < num_threads; ++i) {
|
||||
s.m_params.set_uint("random_seed", s.m_rand());
|
||||
solver* s1 = alloc(sat::solver, s.m_params, limits[i-1]);
|
||||
limits.push_back(reslimit());
|
||||
m_s.m_params.set_uint("random_seed", m_s.m_rand());
|
||||
solver* s1 = alloc(sat::solver, m_s.m_params, limits.back());
|
||||
solvers.push_back(s1);
|
||||
s1->copy(s);
|
||||
s1->copy(m_s);
|
||||
scoped_rlimit.push_child(&s1->rlimit());
|
||||
}
|
||||
|
||||
|
|
@ -828,7 +438,7 @@ lbool ccc::search() {
|
|||
try {
|
||||
lbool r = l_undef;
|
||||
if (i == 0) {
|
||||
r = cube();
|
||||
r = cube2();
|
||||
}
|
||||
else {
|
||||
r = conquer(*solvers[i-1]);
|
||||
|
|
@ -884,7 +494,6 @@ lbool ccc::search() {
|
|||
}
|
||||
#endif
|
||||
|
||||
|
||||
return result;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -29,15 +29,16 @@ namespace sat {
|
|||
unsigned m_id;
|
||||
unsigned m_depth;
|
||||
literal m_last;
|
||||
literal m_blocked;
|
||||
unsigned m_parent;
|
||||
decision(unsigned id, unsigned d, literal last, unsigned parent_id):
|
||||
m_id(id), m_depth(d), m_last(last), m_parent(parent_id) {}
|
||||
decision(unsigned id, unsigned d, literal last, literal blocked, unsigned parent_id):
|
||||
m_id(id), m_depth(d), m_last(last), m_blocked(blocked), m_parent(parent_id) {}
|
||||
decision(): m_id(0), m_depth(0), m_last(null_literal), m_parent(0) {}
|
||||
|
||||
std::ostream& pp(std::ostream& out) const;
|
||||
};
|
||||
|
||||
solver& s;
|
||||
solver& m_s;
|
||||
queue<unsigned> m_solved;
|
||||
queue<decision> m_decisions;
|
||||
model m_model;
|
||||
|
|
@ -56,8 +57,14 @@ namespace sat {
|
|||
};
|
||||
|
||||
lbool conquer(solver& s);
|
||||
bool cube_decision(solver& s, svector<decision>& decisions);
|
||||
|
||||
lbool bounded_search(solver& s, svector<decision>& decisions);
|
||||
lbool cube();
|
||||
bool push_decision(solver& s, decision const& d);
|
||||
|
||||
lbool cube2();
|
||||
lbool cube2(unsigned& branch_id, svector<decision>& decisions, lookahead& lh);
|
||||
|
||||
void replay_decisions(solver& s, svector<decision>& decisions);
|
||||
|
||||
|
|
@ -69,9 +76,11 @@ namespace sat {
|
|||
|
||||
void check_non_model(char const* fn, svector<decision> const& decisions);
|
||||
|
||||
bool contains_branch(svector<decision> const& decisions, unsigned branch_id) const;
|
||||
|
||||
public:
|
||||
|
||||
ccc(solver& s): s(s) {}
|
||||
ccc(solver& s): m_s(s) {}
|
||||
|
||||
lbool search();
|
||||
|
||||
|
|
|
|||
|
|
@ -161,6 +161,7 @@ namespace sat {
|
|||
lookahead_mode m_search_mode; // mode of search
|
||||
stats m_stats;
|
||||
model m_model;
|
||||
literal m_blocked_literal;
|
||||
|
||||
// ---------------------------------------
|
||||
// truth values
|
||||
|
|
@ -1712,7 +1713,8 @@ namespace sat {
|
|||
if (trail.empty()) return false;
|
||||
pop();
|
||||
flip_prefix();
|
||||
assign(~trail.back());
|
||||
m_blocked_literal = trail.back();
|
||||
assign(~m_blocked_literal);
|
||||
trail.pop_back();
|
||||
propagate();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -76,18 +76,18 @@ namespace sat {
|
|||
lowlink.resize(num_lits, UINT_MAX);
|
||||
in_s.resize(num_lits, false);
|
||||
literal_vector roots;
|
||||
roots.resize(m_solver.num_vars(), null_literal);
|
||||
roots.resize(m_solver.num_vars(), null_literal);
|
||||
unsigned next_index = 0;
|
||||
svector<frame> frames;
|
||||
bool_var_vector to_elim;
|
||||
|
||||
for (unsigned l_idx = 0; l_idx < num_lits; l_idx++) {
|
||||
if (index[l_idx] != UINT_MAX)
|
||||
continue;
|
||||
if (m_solver.was_eliminated(to_literal(l_idx).var()))
|
||||
continue;
|
||||
|
||||
m_solver.checkpoint();
|
||||
for (unsigned l_idx = 0; l_idx < num_lits; l_idx++) {
|
||||
if (index[l_idx] != UINT_MAX)
|
||||
continue;
|
||||
if (m_solver.was_eliminated(to_literal(l_idx).var()))
|
||||
continue;
|
||||
|
||||
m_solver.checkpoint();
|
||||
|
||||
#define NEW_NODE(LIDX) { \
|
||||
index[LIDX] = next_index; \
|
||||
|
|
@ -99,121 +99,121 @@ namespace sat {
|
|||
frames.push_back(frame(LIDX, wlist.begin(), wlist.end())); \
|
||||
}
|
||||
|
||||
NEW_NODE(l_idx);
|
||||
NEW_NODE(l_idx);
|
||||
|
||||
while (!frames.empty()) {
|
||||
loop:
|
||||
frame & fr = frames.back();
|
||||
unsigned l_idx = fr.m_lidx;
|
||||
if (!fr.m_first) {
|
||||
// after visiting child
|
||||
literal l2 = fr.m_it->get_literal();
|
||||
unsigned l2_idx = l2.index();
|
||||
SASSERT(index[l2_idx] != UINT_MAX);
|
||||
if (lowlink[l2_idx] < lowlink[l_idx])
|
||||
lowlink[l_idx] = lowlink[l2_idx];
|
||||
fr.m_it++;
|
||||
}
|
||||
fr.m_first = false;
|
||||
while (fr.m_it != fr.m_end) {
|
||||
if (!fr.m_it->is_binary_clause()) {
|
||||
fr.m_it++;
|
||||
continue;
|
||||
}
|
||||
literal l2 = fr.m_it->get_literal();
|
||||
unsigned l2_idx = l2.index();
|
||||
if (index[l2_idx] == UINT_MAX) {
|
||||
NEW_NODE(l2_idx);
|
||||
goto loop;
|
||||
}
|
||||
else if (in_s[l2_idx]) {
|
||||
if (index[l2_idx] < lowlink[l_idx])
|
||||
lowlink[l_idx] = index[l2_idx];
|
||||
}
|
||||
fr.m_it++;
|
||||
}
|
||||
// visited all successors
|
||||
if (lowlink[l_idx] == index[l_idx]) {
|
||||
// found new SCC
|
||||
CTRACE("scc_cycle", s.back() != l_idx, {
|
||||
tout << "cycle: ";
|
||||
unsigned j = s.size() - 1;
|
||||
unsigned l2_idx;
|
||||
do {
|
||||
l2_idx = s[j];
|
||||
j--;
|
||||
tout << to_literal(l2_idx) << " ";
|
||||
} while (l2_idx != l_idx);
|
||||
tout << "\n";
|
||||
});
|
||||
while (!frames.empty()) {
|
||||
loop:
|
||||
frame & fr = frames.back();
|
||||
unsigned l_idx = fr.m_lidx;
|
||||
if (!fr.m_first) {
|
||||
// after visiting child
|
||||
literal l2 = fr.m_it->get_literal();
|
||||
unsigned l2_idx = l2.index();
|
||||
SASSERT(index[l2_idx] != UINT_MAX);
|
||||
if (lowlink[l2_idx] < lowlink[l_idx])
|
||||
lowlink[l_idx] = lowlink[l2_idx];
|
||||
fr.m_it++;
|
||||
}
|
||||
fr.m_first = false;
|
||||
while (fr.m_it != fr.m_end) {
|
||||
if (!fr.m_it->is_binary_clause()) {
|
||||
fr.m_it++;
|
||||
continue;
|
||||
}
|
||||
literal l2 = fr.m_it->get_literal();
|
||||
unsigned l2_idx = l2.index();
|
||||
if (index[l2_idx] == UINT_MAX) {
|
||||
NEW_NODE(l2_idx);
|
||||
goto loop;
|
||||
}
|
||||
else if (in_s[l2_idx]) {
|
||||
if (index[l2_idx] < lowlink[l_idx])
|
||||
lowlink[l_idx] = index[l2_idx];
|
||||
}
|
||||
fr.m_it++;
|
||||
}
|
||||
// visited all successors
|
||||
if (lowlink[l_idx] == index[l_idx]) {
|
||||
// found new SCC
|
||||
CTRACE("scc_cycle", s.back() != l_idx, {
|
||||
tout << "cycle: ";
|
||||
unsigned j = s.size() - 1;
|
||||
unsigned l2_idx;
|
||||
do {
|
||||
l2_idx = s[j];
|
||||
j--;
|
||||
tout << to_literal(l2_idx) << " ";
|
||||
} while (l2_idx != l_idx);
|
||||
tout << "\n";
|
||||
});
|
||||
|
||||
SASSERT(!s.empty());
|
||||
literal l = to_literal(l_idx);
|
||||
bool_var v = l.var();
|
||||
if (roots[v] != null_literal) {
|
||||
// variable was already assigned... just consume stack
|
||||
TRACE("scc_detail", tout << "consuming stack...\n";);
|
||||
unsigned l2_idx;
|
||||
do {
|
||||
l2_idx = s.back();
|
||||
s.pop_back();
|
||||
in_s[l2_idx] = false;
|
||||
SASSERT(roots[to_literal(l2_idx).var()].var() == roots[v].var());
|
||||
} while (l2_idx != l_idx);
|
||||
}
|
||||
else {
|
||||
// check if the SCC has an external variable, and check for conflicts
|
||||
TRACE("scc_detail", tout << "assigning roots...\n";);
|
||||
literal r = null_literal;
|
||||
unsigned j = s.size() - 1;
|
||||
unsigned l2_idx;
|
||||
do {
|
||||
l2_idx = s[j];
|
||||
j--;
|
||||
if (to_literal(l2_idx) == ~l) {
|
||||
m_solver.set_conflict(justification());
|
||||
return 0;
|
||||
}
|
||||
if (m_solver.is_external(to_literal(l2_idx).var())) {
|
||||
r = to_literal(l2_idx);
|
||||
break;
|
||||
}
|
||||
} while (l2_idx != l_idx);
|
||||
|
||||
SASSERT(!s.empty());
|
||||
literal l = to_literal(l_idx);
|
||||
bool_var v = l.var();
|
||||
if (roots[v] != null_literal) {
|
||||
// variable was already assigned... just consume stack
|
||||
TRACE("scc_detail", tout << "consuming stack...\n";);
|
||||
unsigned l2_idx;
|
||||
do {
|
||||
l2_idx = s.back();
|
||||
s.pop_back();
|
||||
in_s[l2_idx] = false;
|
||||
SASSERT(roots[to_literal(l2_idx).var()].var() == roots[v].var());
|
||||
} while (l2_idx != l_idx);
|
||||
}
|
||||
else {
|
||||
// check if the SCC has an external variable, and check for conflicts
|
||||
TRACE("scc_detail", tout << "assigning roots...\n";);
|
||||
literal r = null_literal;
|
||||
unsigned j = s.size() - 1;
|
||||
unsigned l2_idx;
|
||||
do {
|
||||
l2_idx = s[j];
|
||||
j--;
|
||||
if (to_literal(l2_idx) == ~l) {
|
||||
m_solver.set_conflict(justification());
|
||||
return 0;
|
||||
}
|
||||
if (m_solver.is_external(to_literal(l2_idx).var())) {
|
||||
r = to_literal(l2_idx);
|
||||
break;
|
||||
}
|
||||
} while (l2_idx != l_idx);
|
||||
if (r == null_literal) {
|
||||
// SCC does not contain external variable
|
||||
r = to_literal(l_idx);
|
||||
}
|
||||
|
||||
if (r == null_literal) {
|
||||
// SCC does not contain external variable
|
||||
r = to_literal(l_idx);
|
||||
}
|
||||
TRACE("scc_detail", tout << "r: " << r << "\n";);
|
||||
|
||||
TRACE("scc_detail", tout << "r: " << r << "\n";);
|
||||
|
||||
do {
|
||||
l2_idx = s.back();
|
||||
s.pop_back();
|
||||
in_s[l2_idx] = false;
|
||||
literal l2 = to_literal(l2_idx);
|
||||
bool_var v2 = l2.var();
|
||||
if (roots[v2] == null_literal) {
|
||||
if (l2.sign()) {
|
||||
roots[v2] = ~r;
|
||||
}
|
||||
else {
|
||||
roots[v2] = r;
|
||||
}
|
||||
if (v2 != r.var())
|
||||
to_elim.push_back(v2);
|
||||
}
|
||||
} while (l2_idx != l_idx);
|
||||
}
|
||||
}
|
||||
frames.pop_back();
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < m_solver.num_vars(); ++i) {
|
||||
if (roots[i] == null_literal) {
|
||||
roots[i] = literal(i, false);
|
||||
}
|
||||
}
|
||||
do {
|
||||
l2_idx = s.back();
|
||||
s.pop_back();
|
||||
in_s[l2_idx] = false;
|
||||
literal l2 = to_literal(l2_idx);
|
||||
bool_var v2 = l2.var();
|
||||
if (roots[v2] == null_literal) {
|
||||
if (l2.sign()) {
|
||||
roots[v2] = ~r;
|
||||
}
|
||||
else {
|
||||
roots[v2] = r;
|
||||
}
|
||||
if (v2 != r.var())
|
||||
to_elim.push_back(v2);
|
||||
}
|
||||
} while (l2_idx != l_idx);
|
||||
}
|
||||
}
|
||||
frames.pop_back();
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < m_solver.num_vars(); ++i) {
|
||||
if (roots[i] == null_literal) {
|
||||
roots[i] = literal(i, false);
|
||||
}
|
||||
}
|
||||
TRACE("scc", for (unsigned i = 0; i < roots.size(); i++) { tout << i << " -> " << roots[i] << "\n"; }
|
||||
tout << "to_elim: "; for (unsigned i = 0; i < to_elim.size(); i++) tout << to_elim[i] << " "; tout << "\n";);
|
||||
m_num_elim += to_elim.size();
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue