Name: folkung Version: 2.3 Cabal-Version: >= 1.2 Copyright: Paradox/Equinox: 2003-2007, Koen Claessen, Niklas Sorensson Minisat: 2003-2005, Niklas Een, Niklas Sorensson Author: Koen Claessen, Niklas Sorensson Category: Math Maintainer: Koen Claessen Stability: Experimental License: OtherLicense License-file: LICENSE Homepage: http://www.cs.chalmers.se/~koen/folkung/ Synopsis: First-order logic theorem prover and model finder library. Description: Folkung is a library which implements Equinox, an automated theorem prover for pure first-order logic with equality, and Paradox, a finite-domain model finder for pure first-order logic with equality. . Equinox actually implements a hierarchy of logics, realized as a stack of theorem provers that use abstraction refinement to talk with each other. In the bottom sits an efficient SAT solver (MiniSat). . The main aims of Equinox are (1) to be a theorem prover that performs well at large, automatically generated problems, coming up in for example formal verification areas, and (2) to be able to provide understandable feedback about failed proof attempts. . Paradox is a MACE-style model finder, which means that it translates a first-order problem into a sequence of SAT problems, which are solved by a SAT solver (in our case MiniSat). . Paradox is the proud winner of the SAT/Models division of the CASC World Championship on First-Order Automated Theorem Proving in 2003, 2004, 2005 and 2006. Build-Type: Simple Extra-source-files: instantiate/MiniSatInstantiateClause.h instantiate/Wrapper.h minisat/current-base/Prop.h minisat/current-base/Solver.h minisat/current-base/SolverTypes.h minisat/current-base/VarOrder.h minisat/mtl/Alg.h minisat/mtl/Heap.h minisat/mtl/Map.h minisat/mtl/Sort.h minisat/mtl/Vec.h Flag split-base Default: True Flag debug Default: False Library Build-depends: mtl if flag(split-base) Build-depends: base >= 3.0, containers else Build-depends: base < 3.0 Extensions: CPP -- Cabal-1.2 doesn't seem to parse this, using glasgow-exts instead: -- Typeoperators Generics Rank2Types ImplicitParams ForeignFunctionInterface GeneralizedNewtypeDeriving Ghc-options: -O2 -static -fglasgow-exts -fwarn-unused-imports -- -fno-exceptions gets rid of the -pgml g++ requirement on OS X Cc-options: -Wall -ffloat-store -fno-exceptions if flag(debug) Cc-options: -O0 -ggdb -DDEBUG else Cc-options: -O3 -DNDEBUG Hs-source-dirs: Haskell Install-includes: Wrapper.h Include-dirs: instantiate minisat/mtl minisat/current-base Extra-libraries: stdc++ C-sources: minisat/current-base/Solver.cpp minisat/current-base/Prop.cpp instantiate/MiniSatWrapper.cpp instantiate/MiniSatInstantiateClause.cpp Exposed-modules: Flags Form Name Folkung Parsek ParseProblem Equinox.Solve Paradox.Solve Other-modules: Clausify Sat Output Str Timeout Equinox.ConSat Equinox.Fair Equinox.FolSat Equinox.TermSat Paradox.AnalysisTypes Paradox.Flatten Paradox.Instantiate Paradox.SolveInstances