Skip to content

Commit

Permalink
Merge pull request #8533 from diffblue/prop-solve-xnor
Browse files Browse the repository at this point in the history
implement `xnor` in prop_conv_solvert
tautschnig authored Dec 20, 2024

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
2 parents 857c88e + d877a12 commit d5cf498
Showing 1 changed file with 15 additions and 14 deletions.
29 changes: 15 additions & 14 deletions src/solvers/prop/prop_conv_solver.cpp
Original file line number Diff line number Diff line change
@@ -257,7 +257,7 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr)
}
else if(
expr.id() == ID_or || expr.id() == ID_and || expr.id() == ID_xor ||
expr.id() == ID_nor || expr.id() == ID_nand)
expr.id() == ID_nor || expr.id() == ID_nand || expr.id() == ID_xnor)
{
INVARIANT(
!op.empty(),
@@ -268,19 +268,20 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr)
for(const auto &operand : op)
bv.push_back(convert(operand));

if(!bv.empty())
{
if(expr.id() == ID_or)
return prop.lor(bv);
else if(expr.id() == ID_nor)
return !prop.lor(bv);
else if(expr.id() == ID_and)
return prop.land(bv);
else if(expr.id() == ID_nand)
return !prop.land(bv);
else if(expr.id() == ID_xor)
return prop.lxor(bv);
}
CHECK_RETURN(!bv.empty());

if(expr.id() == ID_or)
return prop.lor(bv);
else if(expr.id() == ID_nor)
return !prop.lor(bv);
else if(expr.id() == ID_and)
return prop.land(bv);
else if(expr.id() == ID_nand)
return !prop.land(bv);
else if(expr.id() == ID_xor)
return prop.lxor(bv);
else if(expr.id() == ID_xnor)
return !prop.lxor(bv);
}
else if(expr.id() == ID_not)
{

0 comments on commit d5cf498

Please sign in to comment.