Home
Download
Compilation
Usage
DIMACS format
ISCAS/RTL format
Using the BASolver
To use the basolver binary, type
./bin/basolver[.version] [options] file1 [file2]
If only one file is given, it has to be in DIMACS CNF format. If two files are given, they both have to be in either ISCAS or RTL format (see format description below) and have to contain equal number of inputs and outputs. These two formats allow to conveniently encode arithmetic circuits.
Command line options are the following:
| --equiv (flag, default=off) | may be given only with two input files; if this flag is set, the solver checks the equivalence of two input circuits: it produces a formula which is unsatisfiable if and only if the two input circuits are equivalent and solves it; if this flag is unset the solver just adds the equalities stating that all corresponding inputs and outputs of two input circuits are equal and solves the resulting set |
| --html (flag, default=off) | prints html output of the solving process to the ./Outputs/ directory |
| --nosets (flag, default=off) | do not write the sets in html output |
| --booth (flag, default=off) | use special rules for Booth multipliers (under development, currently does not really help) |