cnfgen.clitools.cnfgen module

Utilities to build CNF formulas interesting for proof complexity.

The module cnfgen contains facilities to generate cnf formulas, in order to be printed in dimacs or LaTeX formats. Such formulas are ready to be fed to sat solvers. In particular the module implements both a library of CNF generators and a command line utility.

Create the CNFs:

>>> from cnfgen.formula.cnf import CNF
>>> c=CNF([ [1, 2, -3], [-2, 4] ])
>>> print( c.to_dimacs() )
p cnf 4 2
1 2 -3 0
-2 4 0
<BLANKLINE>

You can add clauses later in the process:

>>> c.add_clause( [-3, 4, -5] )
>>> print( c.to_dimacs())
p cnf 5 3
1 2 -3 0
-2 4 0
-3 4 -5 0
<BLANKLINE>

build_latex_cmdline_description(argv, args, t_args)

Build the latex documentation of the components of the formula.

Insert additonal latex documentation of the formula. For example it includes the input files used to build it.

Parameters:

argv : list(str)

arguments on command line

args:

parsed arguments for the formula

t_args: list

group of parsed arguments for the transformations

cli(argv=None, mode='output')

CNFgen main command line interface

This function provide the main interface to CNFgen. It sets up the command line, parses the command line arguments, builds the appropriate formula and outputs its representation.

Parameters:

argv: list, optional

The list of token with the command line arguments/options.

mode: str

One among ‘formula’, ‘string’, ‘output’ (latter is the default) - ‘formula’ return a CNF object - ‘string’ return the string with the output of CNFgen - ‘output’ output the formula to the user

Raises:

CLIError:

The command line arguments are wrong or inconsistent

main()

The starting point of CNFgen program

parse_command_line(argv, fparser, tparser)

Parser command line arguments

Split command line around ‘-T’ options in parts. Extract the formula generator setup from the first part, and extract a chain of formula transformation commands

setup_command_line_parsers(progname, fhelpers, thelpers)

Create the parser for formula and transformation arguments.

General options - query version - verbosity/silence - outputfile - outputformat - random seed

Formula options via subcommands - one for each formula helper