GitHub - p4l1ly/antisat: antichain for symbolic alternating finite automata

p4l1ly / antisat Public

Notifications You must be signed in to change notification settings
Fork 1
Star 0

antichain for symbolic alternating finite automata

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 191 Commits
.vim		.vim
debug		debug
src/afaminisat		src/afaminisat
test		test
.gitignore		.gitignore
.vimspector.json		.vimspector.json
CMakeLists.txt		CMakeLists.txt
LICENSE		LICENSE
README		README
bench.sh		bench.sh
build_all.py		build_all.py
check_assignment.py		check_assignment.py
check_results.py		check_results.py
check_valgrind.py		check_valgrind.py
compare_benches.py		compare_benches.py
measure.py		measure.py
measure2.py		measure2.py
measure3.py		measure3.py
plot.gp		plot.gp
plot_ab.py		plot_ab.py
preplot.sh		preplot.sh
presort_clauses.py		presort_clauses.py
todo		todo

Repository files navigation

AFAMINISAT
==========

Antichain solver for alternating finite automata, created by modification of
MiniSat v1.12b. See https://github.com/p4l1ly/automata-safa and our paper:
Simplifying Alternating Automata for Emptiness Testing, Pavol Vargovčík, Lukáš
Holík

MiniSat v1.12b
========================================

This is the last version where arbitrary boolean constraints are
supported. Later versions of MiniSat only supports clauses. However,
don't be discouraged; the improvements made in v1.13 and v1.14 are
quite easily back-ported to this version, so if you really need the
functionality provided by this release, go ahead and use it (and send
us the upgrades if you make them!)