From: Fabio Somenzi (Fabio_at_colorado.edu)
Date: Mon Jul 05 2004 - 15:40:24 MDT
>>>>> "F" == Fabio <fabio.marcone_at_libero.it> writes:
F> Hi!
F> I need to print a cnf that describes a flattaned network. is it
F> possible? I found how print a cnf counterexample in
F> bounded_model_check but I need to have cnf file of the network,
F> not of the counterexample.
The -o option of BMC actually saves the last CNF formula that is sent
to the SAT solver in the course of the BMC experiment. This is
neither the "CNF counterexample" as erroneously suggested by the "help
bmc" output, nor the CNF of the circuit, though, at least for k=1,
it's closer to the latter.
Fabio
This archive was generated by hypermail 2.1.7 : Mon Jul 05 2004 - 15:40:52 MDT