aspmt

System aspmt2smt is a prototype implementation of multi-valued propositional formulas under the stable model semantics computed by system z3 based on the
theorem on completion. The system is a toolchain that includes aspmt-compiler, f2lp, gringo, and z3.

Please follow the link to the ASPMT homepage for more information and a tutorial.

System mvsm is a prototype implementation of multi-valued propositional formulas under the stable model semantics computed by gringo/claspD by eliminating
functions in favor of predicates. The system is a toolchain that includes mvpf2lpCompiler, f2lp, gringo, claspD, and as2transition.

Both compilers are written using flex and bison.

For convenience, binaries of every tool in the chains are provided in the files section.
For instructions on running the toolchains, please refer to the readme in the Files section, and the handout
http://goo.gl/WUsIYQ.

For examples and output of the systems, see the examples folders in the Files section.