Read Me

DNFCNFConverter is a set of little tools used to convert any boolean formula to CNF or DNF
Copyright (C) 2010  Valerian Merkling niarkoleptik@gmail.com

This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.

This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA  02110-1301  USA


	Installation :

cmake .
make

Boost 1.42 needed (www.boost.org)

	Recognized formula :
	
here is the grammar	

formula = 
	literal
	| (formula '&' formula )
	| (formula '|' formula )
	| '!' formula
	|dnf
	|cnf

	literal = '!'? alnum*
	
	conjonction = '[' literal (',' literal )* ']'
	disjonction = '[' literal (',' literal )* ']'
	
	dnf = '+{' conjonction conjonction* '}'
	cnf = '*{' disjonction disjonction* '}'	


Space or linefeed are ignored, => and <=> (implication and equivalence) are not implemented yet.
Note that 'a&b' and (a) does not work, but the parser was made with boost::spirit and is easy to modify.

How to use it ?

godnf '(a&(b&c))'
echo '(a&(b&c))' | godnf
cat file | godnf

There are also some tools to read a .dac file
.dac format :
entityname group 0 1 0 0 1 1 ....
entityname group 1 0 1 0 1 1 ....


quine is used to extract a dnf from a .dac file and prepare it for qmcs
qmcs is a c++ program doing Quine Mc Cluskey simplification. http://sourceforge.net/projects/qmcs/
Note that i changed qmcs a bit (unsigned are now long long unsigned to allow larger formula)

dacquine file.dac 1 -t | qmcs		will extract the dnf of the group 1 in file.dac and send it to qmcs
dacquine file.dac 1 -o | qmcs		will extract the dnf of every instance but group 1 and send it to qmcs


dacreader is used to read a .dac file and extract the dnf of any group and make it usable by gocnf or godnf


dacreader filename [group] [maxvar] [-p|-n] [-t|-o]
maxvar allow you to work only on the n first var
-p or -n are the epuration flag. If set to -p, column (in the whole file) with only 1 or only 0 will not be used 
-t or -o are the target flag. -t will display only formula from the selected group, -o will display every formula excepted the given group.

Note that argument are optionnal from the end, like this
dacreader filename [group] [maxvar] [-p|-n]
dacreader filename [group] [maxvar]
dacreader filename [group] 
dacreader filename

It may be upgraded later.