Skip to content

implement xnor in prop_conv_solvert #8533

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Dec 20, 2024
Merged

implement xnor in prop_conv_solvert #8533

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 15 additions & 14 deletions src/solvers/prop/prop_conv_solver.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -257,7 +257,7 @@
}
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(),
Expand All @@ -268,19 +268,20 @@
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);

Check warning on line 276 in src/solvers/prop/prop_conv_solver.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/prop/prop_conv_solver.cpp#L276 

Added line #L276 was not covered by tests
else if(expr.id() == ID_and)
return prop.land(bv);
else if(expr.id() == ID_nand)
return !prop.land(bv);

Check warning on line 280 in src/solvers/prop/prop_conv_solver.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/prop/prop_conv_solver.cpp#L280 

Added line #L280 was not covered by tests
else if(expr.id() == ID_xor)
return prop.lxor(bv);
else if(expr.id() == ID_xnor)
return !prop.lxor(bv);

Check warning on line 284 in src/solvers/prop/prop_conv_solver.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/prop/prop_conv_solver.cpp#L283-L284 

Added lines #L283 - L284 were not covered by tests
}
else if(expr.id() == ID_not)
{
Expand Down
Loading