Skip to content

Commit

Permalink
Merge pull request #477 from diffblue/print-netlist-constraints
Browse files Browse the repository at this point in the history
netlist output now includes AIG constraints
  • Loading branch information
kroening authored May 2, 2024
2 parents 24262e8 + 4c4ad93 commit a4621dc
Showing 1 changed file with 15 additions and 4 deletions.
19 changes: 15 additions & 4 deletions src/trans-netlist/netlist.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -56,21 +56,32 @@ void netlistt::print(std::ostream &out) const

out << "Initial state: " << '\n';

for(unsigned i=0; i<initial.size(); i++)
for(auto &c : initial)
{
out << " ";
print(out, initial[i]);
print(out, c);
out << '\n';
}

out << '\n';

out << "State invariant constraints: " << '\n';

for(auto &c : constraints)
{
out << " ";
print(out, c);
out << '\n';
}

out << '\n' << std::flush;

out << "Transition constraints: " << '\n';

for(unsigned i=0; i<transition.size(); i++)
for(auto &c : transition)
{
out << " ";
print(out, transition[i]);
print(out, c);
out << '\n';
}

Expand Down

0 comments on commit a4621dc

Please sign in to comment.