Skip to content

SMT2: implement nand, nor, xnor #8530

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 18, 2024
Merged

SMT2: implement nand, nor, xnor #8530

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
32 changes: 32 additions & 0 deletions src/solvers/smt2/smt2_conv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1362,6 +1362,38 @@
}
out << ")";
}
else if(expr.id() == ID_nand || expr.id() == ID_nor || expr.id() == ID_xnor)
{
DATA_INVARIANT(

Check warning on line 1367 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L1367 

Added line #L1367 was not covered by tests
expr.is_boolean(),
"logical nand, nor, xnor expressions should have Boolean type");
DATA_INVARIANT(

Check warning on line 1370 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L1370 

Added line #L1370 was not covered by tests
expr.operands().size() >= 1,
"logical nand, nor, xnor expressions should have at least one operand");

// SMT-LIB doesn't have nand, nor, xnor
out << "(not ";

Check warning on line 1375 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L1375 

Added line #L1375 was not covered by tests
if(expr.operands().size() == 1)
convert_expr(to_multi_ary_expr(expr).op0());

Check warning on line 1377 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L1377 

Added line #L1377 was not covered by tests
else
{
if(expr.id() == ID_nand)
out << "(and";
else if(expr.id() == ID_nor)
out << "(and";
else if(expr.id() == ID_xnor)
out << "(xor";

Check warning on line 1385 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L1381-L1385 

Added lines #L1381 - L1385 were not covered by tests
else
DATA_INVARIANT(false, "unexpected expression");

Check warning on line 1387 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L1387 

Added line #L1387 was not covered by tests
for(const auto &op : expr.operands())
{
out << ' ';
convert_expr(op);

Check warning on line 1391 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L1390-L1391 

Added lines #L1390 - L1391 were not covered by tests
}
out << ')'; // or, and, xor

Check warning on line 1393 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L1393 

Added line #L1393 was not covered by tests
}
out << ')'; // not

Check warning on line 1395 in src/solvers/smt2/smt2_conv.cpp

View check run for this annotation

Codecov / codecov/patch

src/solvers/smt2/smt2_conv.cpp#L1395 

Added line #L1395 was not covered by tests
}
else if(expr.id()==ID_implies)
{
const implies_exprt &implies_expr = to_implies_expr(expr);
Expand Down
Loading