Skip to content

Commit

Permalink
netlist output now includes AIG constraints
Browse files Browse the repository at this point in the history
The output of --show-netlist now includes the AIG constraints.
  • Loading branch information
kroening committed May 2, 2024
1 parent ee122e1 commit 4c4ad93
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 4c4ad93

Please sign in to comment.