Skip to content

Commit

Permalink
introduce globally visible macro for controlling use of ternary, turn…
Browse files Browse the repository at this point in the history 
… them off
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Oct 25, 2022
1 parent c62c5e9 commit 154fed7
Show file tree
Hide file tree
Showing 7 changed files with 55 additions and 6 deletions.
2 changes: 2 additions & 0 deletions src/sat/sat_drat.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -445,8 +445,10 @@ namespace sat {
return false;
case justification::BINARY:
return contains(c, j.get_literal());
#if ENABLE_TERNARY
case justification::TERNARY:
return contains(c, j.get_literal1(), j.get_literal2());
#endif
case justification::CLAUSE:
return contains(s.get_clause(j));
default:
Expand Down
6 changes: 4 additions & 2 deletions src/sat/sat_gc.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,8 +20,6 @@ Revision History:

#include "sat/sat_solver.h"

#define ENABLE_TERNARY true

namespace sat {

// -----------------------
Expand Down Expand Up @@ -180,6 +178,7 @@ namespace sat {
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat-gc :strategy " << st_name << " :deleted " << (sz - new_sz) << ")\n";);
}

#if ENABLE_TERNARY
bool solver::can_delete3(literal l1, literal l2, literal l3) const {
if (value(l1) == l_true &&
value(l2) == l_false &&
Expand All @@ -193,16 +192,19 @@ namespace sat {
}
return true;
}
#endif

bool solver::can_delete(clause const & c) const {
if (c.on_reinit_stack())
return false;
#if ENABLE_TERNARY
if (ENABLE_TERNARY && c.size() == 3) {
return
can_delete3(c[0],c[1],c[2]) &&
can_delete3(c[1],c[0],c[2]) &&
can_delete3(c[2],c[0],c[1]);
}
#endif
literal l0 = c[0];
if (value(l0) != l_true)
return true;
Expand Down
12 changes: 11 additions & 1 deletion src/sat/sat_justification.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,11 @@ namespace sat {

class justification {
public:
enum kind { NONE = 0, BINARY = 1, TERNARY = 2, CLAUSE = 3, EXT_JUSTIFICATION = 4};
enum kind { NONE = 0, BINARY = 1,
#if ENABLE_TERNARY
TERNARY = 2,
#endif
CLAUSE = 3, EXT_JUSTIFICATION = 4};
private:
unsigned m_level;
size_t m_val1;
Expand All @@ -32,7 +36,9 @@ namespace sat {
public:
justification(unsigned lvl):m_level(lvl), m_val1(0), m_val2(NONE) {}
explicit justification(unsigned lvl, literal l):m_level(lvl), m_val1(l.to_uint()), m_val2(BINARY) {}
#if ENABLE_TERNARY
justification(unsigned lvl, literal l1, literal l2):m_level(lvl), m_val1(l1.to_uint()), m_val2(TERNARY + (l2.to_uint() << 3)) {}
#endif
explicit justification(unsigned lvl, clause_offset cls_off):m_level(lvl), m_val1(cls_off), m_val2(CLAUSE) {}
static justification mk_ext_justification(unsigned lvl, ext_justification_idx idx) { return justification(lvl, idx, EXT_JUSTIFICATION); }

Expand All @@ -45,9 +51,11 @@ namespace sat {
bool is_binary_clause() const { return m_val2 == BINARY; }
literal get_literal() const { SASSERT(is_binary_clause()); return to_literal(val1()); }

#if ENABLE_TERNARY
bool is_ternary_clause() const { return get_kind() == TERNARY; }
literal get_literal1() const { SASSERT(is_ternary_clause()); return to_literal(val1()); }
literal get_literal2() const { SASSERT(is_ternary_clause()); return to_literal(m_val2 >> 3); }
#endif

bool is_clause() const { return m_val2 == CLAUSE; }
clause_offset get_clause_offset() const { return m_val1; }
Expand All @@ -65,9 +73,11 @@ namespace sat {
case justification::BINARY:
out << "binary " << j.get_literal();
break;
#if ENABLE_TERNARY
case justification::TERNARY:
out << "ternary " << j.get_literal1() << " " << j.get_literal2();
break;
#endif
case justification::CLAUSE:
out << "clause";
break;
Expand Down
6 changes: 6 additions & 0 deletions src/sat/sat_proof_trim.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -125,8 +125,10 @@ namespace sat {
in_coi |= m_in_coi.contains(lit.index());
else if (js.is_binary_clause())
in_coi = m_in_coi.contains(js.get_literal().index());
#if ENABLE_TERNARY
else if (js.is_ternary_clause())
in_coi = m_in_coi.contains(js.get_literal1().index()) || m_in_coi.contains(js.get_literal2().index());
#endif
else
UNREACHABLE(); // approach does not work for external justifications

Expand Down Expand Up @@ -224,10 +226,12 @@ namespace sat {
case justification::BINARY:
add_dependency(j.get_literal());
break;
#if ENABLE_TERNARY
case justification::TERNARY:
add_dependency(j.get_literal1());
add_dependency(j.get_literal2());
break;
#endif
case justification::CLAUSE:
for (auto lit : s.get_clause(j))
if (s.value(lit) == l_false)
Expand Down Expand Up @@ -258,11 +262,13 @@ namespace sat {
m_clause.push_back(l);
m_clause.push_back(j.get_literal());
break;
#if ENABLE_TERNARY
case justification::TERNARY:
m_clause.push_back(l);
m_clause.push_back(j.get_literal1());
m_clause.push_back(j.get_literal2());
break;
#endif
case justification::CLAUSE:
s.get_clause(j).mark_used();
IF_VERBOSE(3, verbose_stream() << "add core " << s.get_clause(j) << "\n");
Expand Down
27 changes: 24 additions & 3 deletions src/sat/sat_solver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,6 @@ Revision History:
# include <xmmintrin.h>
#endif

#define ENABLE_TERNARY true

namespace sat {

Expand Down Expand Up @@ -576,6 +575,7 @@ namespace sat {
return reinit;
}

#if ENABLE_TERNARY
bool solver::propagate_ter_clause(clause& c) {
bool reinit = false;
if (value(c[1]) == l_false && value(c[2]) == l_false) {
Expand All @@ -595,6 +595,7 @@ namespace sat {
}
return reinit;
}
#endif

clause * solver::mk_nary_clause(unsigned num_lits, literal * lits, sat::status st) {
m_stats.m_mk_clause++;
Expand Down Expand Up @@ -1061,7 +1062,7 @@ namespace sat {

bool solver::propagate_literal(literal l, bool update) {
literal l1, l2;
lbool val1, val2;

bool keep;
unsigned curr_level = lvl(l);
TRACE("sat_propagate", tout << "propagating: " << l << "@" << curr_level << " " << m_justification[l.var()] << "\n"; );
Expand Down Expand Up @@ -1099,7 +1100,9 @@ namespace sat {
*it2 = *it;
it2++;
break;
case watched::TERNARY:
#if ENABLE_TERNARY
case watched::TERNARY: {
lbool val1, val2;
l1 = it->get_literal1();
l2 = it->get_literal2();
val1 = value(l1);
Expand All @@ -1120,6 +1123,8 @@ namespace sat {
*it2 = *it;
it2++;
break;
}
#endif
case watched::CLAUSE: {
if (value(it->get_blocked_literal()) == l_true) {
TRACE("propagate_clause_bug", tout << "blocked literal " << it->get_blocked_literal() << "\n";
Expand Down Expand Up @@ -2497,10 +2502,12 @@ namespace sat {
case justification::BINARY:
process_antecedent(~(js.get_literal()), num_marks);
break;
#if ENABLE_TERNARY
case justification::TERNARY:
process_antecedent(~(js.get_literal1()), num_marks);
process_antecedent(~(js.get_literal2()), num_marks);
break;
#endif
case justification::CLAUSE: {
clause & c = get_clause(js);
unsigned i = 0;
Expand Down Expand Up @@ -2679,11 +2686,13 @@ namespace sat {
SASSERT(consequent != null_literal);
process_antecedent_for_unsat_core(~(js.get_literal()));
break;
#if ENABLE_TERNARY
case justification::TERNARY:
SASSERT(consequent != null_literal);
process_antecedent_for_unsat_core(~(js.get_literal1()));
process_antecedent_for_unsat_core(~(js.get_literal2()));
break;
#endif
case justification::CLAUSE: {
clause & c = get_clause(js);
unsigned i = 0;
Expand Down Expand Up @@ -2820,10 +2829,12 @@ namespace sat {
case justification::BINARY:
level = update_max_level(js.get_literal(), level, unique_max);
return level;
#if ENABLE_TERNARY
case justification::TERNARY:
level = update_max_level(js.get_literal1(), level, unique_max);
level = update_max_level(js.get_literal2(), level, unique_max);
return level;
#endif
case justification::CLAUSE:
for (literal l : get_clause(js))
level = update_max_level(l, level, unique_max);
Expand Down Expand Up @@ -3175,13 +3186,15 @@ namespace sat {
return false;
}
break;
#if ENABLE_TERNARY
case justification::TERNARY:
if (!process_antecedent_for_minimization(~(js.get_literal1())) ||
!process_antecedent_for_minimization(~(js.get_literal2()))) {
reset_unmark(old_size);
return false;
}
break;
#endif
case justification::CLAUSE: {
clause & c = get_clause(js);
unsigned i = 0;
Expand Down Expand Up @@ -3337,10 +3350,12 @@ namespace sat {
case justification::BINARY:
update_lrb_reasoned(js.get_literal());
break;
#if ENABLE_TERNARY
case justification::TERNARY:
update_lrb_reasoned(js.get_literal1());
update_lrb_reasoned(js.get_literal2());
break;
#endif
case justification::CLAUSE: {
clause & c = get_clause(js);
for (literal l : c) {
Expand Down Expand Up @@ -3686,6 +3701,7 @@ namespace sat {
}
else {
clause & c = *(cw.get_clause());
#if ENABLE_TERNARY
if (ENABLE_TERNARY && c.size() == 3) {
if (propagate_ter_clause(c) && !at_base_lvl())
m_clauses_to_reinit[j++] = cw;
Expand All @@ -3695,6 +3711,7 @@ namespace sat {
c.set_reinit_stack(false);
continue;
}
#endif
detach_clause(c);
attach_clause(c, reinit);
if (reinit && !at_base_lvl())
Expand Down Expand Up @@ -3961,10 +3978,12 @@ namespace sat {
case justification::BINARY:
out << "binary " << js.get_literal() << "@" << lvl(js.get_literal());
break;
#if ENABLE_TERNARY
case justification::TERNARY:
out << "ternary " << js.get_literal1() << "@" << lvl(js.get_literal1()) << " ";
out << js.get_literal2() << "@" << lvl(js.get_literal2());
break;
#endif
case justification::CLAUSE: {
out << "(";
bool first = true;
Expand Down Expand Up @@ -4624,12 +4643,14 @@ namespace sat {
if (!check_domain(lit, ~js.get_literal())) return false;
s |= m_antecedents.find(js.get_literal().var());
break;
#if ENABLE_TERNARY
case justification::TERNARY:
if (!check_domain(lit, ~js.get_literal1()) ||
!check_domain(lit, ~js.get_literal2())) return false;
s |= m_antecedents.find(js.get_literal1().var());
s |= m_antecedents.find(js.get_literal2().var());
break;
#endif
case justification::CLAUSE: {
clause & c = get_clause(js);
for (literal l : c) {
Expand Down
2 changes: 2 additions & 0 deletions src/sat/sat_types.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,8 @@ class params_ref;
class reslimit;
class statistics;

#define ENABLE_TERNARY false

namespace sat {
#define SAT_VB_LVL 10

Expand Down
6 changes: 6 additions & 0 deletions src/sat/smt/pb_solver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -690,13 +690,15 @@ namespace pb {
inc_coeff(consequent, offset);
process_antecedent(js.get_literal(), offset);
break;
#if ENABLE_TERNARY
case sat::justification::TERNARY:
inc_bound(offset);
SASSERT (consequent != sat::null_literal);
inc_coeff(consequent, offset);
process_antecedent(js.get_literal1(), offset);
process_antecedent(js.get_literal2(), offset);
break;
#endif
case sat::justification::CLAUSE: {
inc_bound(offset);
sat::clause & c = s().get_clause(js);
Expand Down Expand Up @@ -1017,6 +1019,7 @@ namespace pb {
inc_coeff(consequent, 1);
process_antecedent(js.get_literal());
break;
#if ENABLE_TERNARY
case sat::justification::TERNARY:
SASSERT(consequent != sat::null_literal);
round_to_one(consequent.var());
Expand All @@ -1025,6 +1028,7 @@ namespace pb {
process_antecedent(js.get_literal1());
process_antecedent(js.get_literal2());
break;
#endif
case sat::justification::CLAUSE: {
sat::clause & c = s().get_clause(js);
unsigned i = 0;
Expand Down Expand Up @@ -3472,13 +3476,15 @@ namespace pb {
ineq.push(lit, offset);
ineq.push(js.get_literal(), offset);
break;
#if ENABLE_TERNARY
case sat::justification::TERNARY:
SASSERT(lit != sat::null_literal);
ineq.reset(offset);
ineq.push(lit, offset);
ineq.push(js.get_literal1(), offset);
ineq.push(js.get_literal2(), offset);
break;
#endif
case sat::justification::CLAUSE: {
ineq.reset(offset);
sat::clause & c = s().get_clause(js);
Expand Down

0 comments on commit 154fed7

Please sign in to comment.