GitHub - jakublevy/dualiza: Binaries for dualiza.

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 638 Commits
aigs		aigs
cnfs		cnfs
doc		doc
formulas		formulas
fuzz		fuzz
.gitignore		.gitignore
.vimdir		.vimdir
LICENSE		LICENSE
NEWS		NEWS
README		README
VERSION		VERSION
aiger.c		aiger.c
aiger.h		aiger.h
bdd.c		bdd.c
bdd.h		bdd.h
buffer.c		buffer.c
buffer.h		buffer.h
circuit.c		circuit.c
circuit.h		circuit.h
clause.c		clause.c
clause.h		clause.h
cnf.c		cnf.c
cnf.h		cnf.h
coi.c		coi.c
coi.h		coi.h
configure.sh		configure.sh
cover.h		cover.h
dimacs.c		dimacs.c
dimacs.h		dimacs.h
dualiza-through-wine.sh		dualiza-through-wine.sh
elim.c		elim.c
elim.h		elim.h
encode.c		encode.c
encode.h		encode.h
example		example
flatten.c		flatten.c
flatten.h		flatten.h
headers.h		headers.h
logging.c		logging.c
logging.h		logging.h
macros.h		macros.h
main.c		main.c
makefile.in		makefile.in
mem.h		mem.h
msg.c		msg.c
msg.h		msg.h
name.c		name.c
name.h		name.h
negate.c		negate.c
negate.h		negate.h
num.c		num.c
num.h		num.h
options.c		options.c
options.h		options.h
parse.c		parse.c
parse.h		parse.h
print.c		print.c
print.h		print.h
reader.c		reader.c
reader.h		reader.h
release.sh		release.sh
resources.c		resources.c
resources.h		resources.h
signal.c		signal.c
signal.h		signal.h
simulate.c		simulate.c
simulate.h		simulate.h
solver.c		solver.c
solver.h		solver.h
stack.h		stack.h
statistics.c		statistics.c
statistics.h		statistics.h
subsume.c		subsume.c
subsume.h		subsume.h
symbols.c		symbols.c
symbols.h		symbols.h
test.sh		test.sh
utils.c		utils.c
utils.h		utils.h
version.h		version.h
version.sh		version.sh
writer.c		writer.c
writer.h		writer.h

Repository files navigation

This is Dualiza a model counter, model enumerator and SAT solver.
It works with DIMACS and AIGER files as well as plain formulas.
Examples and test scripts are in 'cnfs', 'aigs' and 'formulas'.

To compile run './configure.sh && make'.

Armin Biere
Mon Feb  5 16:31:25 CET 2018