Skip to content

Commit 0f70d29

Browse files
committed
propt::l_set_to: avoid duplicate work
Avoid calling `lcnf` with constants when the actual solving back-end will just filter them out.
1 parent 31ec09c commit 0f70d29

File tree

1 file changed

+10
-3
lines changed

1 file changed

+10
-3
lines changed

src/solvers/prop/prop.h

Lines changed: 10 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -44,13 +44,20 @@ class propt
4444

4545
virtual void l_set_to(literalt a, bool value)
4646
{
47-
set_equal(a, const_literal(value));
47+
if(value)
48+
lcnf({a});
49+
else
50+
lcnf({!a});
4851
}
4952

5053
void l_set_to_true(literalt a)
51-
{ l_set_to(a, true); }
54+
{
55+
lcnf({a});
56+
}
5257
void l_set_to_false(literalt a)
53-
{ l_set_to(a, false); }
58+
{
59+
lcnf({!a});
60+
}
5461

5562
// constraints
5663
void lcnf(literalt l0, literalt l1)

0 commit comments

Comments
 (0)