Support verification conditions (definedness conditions) in generated AIGs

GaloisInc / jvm-verifier

The Java Symbolic Simulator, part of SAW.

BSD 3-Clause "New" or "Revised" License

10 stars 2 forks source link

Support verification conditions (definedness conditions) in generated AIGs #4

Open atomb opened 9 years ago

atomb commented 9 years ago

The AIGs generated by the Java API function Symbolic.writeAiger assume definedness. Sometimes this is useful, but it would be convenient to allow generation of AIGs that include the definedness conditions as well.