toysolver-0.8.1: toysolver.cabal
cabal-version: 2.4
Name: toysolver
Version: 0.8.1
License: BSD-3-Clause
License-File: COPYING
Author: Masahiro Sakai (masahiro.sakai@gmail.com)
Maintainer: masahiro.sakai@gmail.com
Category: Algorithms, Optimisation, Optimization, Theorem Provers, Constraints, Logic, Formal Methods, SMT
Synopsis: Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc
Description: Toy-level solver implementation of various problems including SAT, SMT, Max-SAT, PBS/PBO (Pseudo Boolean Satisfaction/Optimization), MILP (Mixed Integer Linear Programming) and non-linear real arithmetic.
Homepage: https://github.com/msakai/toysolver/
Bug-Reports: https://github.com/msakai/toysolver/issues
Tested-With:
GHC ==8.6.5
GHC ==8.8.4
GHC ==8.10.7
GHC ==9.0.2
GHC ==9.2.3
Extra-Source-Files:
README.md
INSTALL.md
CHANGELOG.markdown
COPYING
COPYING-GPL
app/toysat-ipasir/ipasir.h
app/toysat-ipasir/ipasir.map
misc/build_bdist_linux.sh
misc/build_bdist_macos.sh
misc/build_bdist_win32.sh
misc/build_bdist_win64.sh
misc/build_bdist_maxsat_evaluation.sh
misc/build_bdist_pb_evaluation.sh
misc/build_bdist_qbf_evaluation.sh
misc/build_bdist_smtcomp.sh
misc/maxsat/toysat/README.md
misc/maxsat/toysat/toysat
misc/maxsat/toysat_ls/README.md
misc/maxsat/toysat_ls/toysat_ls
misc/pb/README.md
misc/qbf/README.md
misc/smtcomp/bin/starexec_run_default
misc/smtcomp/starexec_description.txt
src/ToySolver/Data/Polyhedron.hs
src/ToySolver/SAT/Solver/MessagePassing/SurveyPropagation/sp.cl
samples/gcnf/*.cnf
samples/gcnf/*.gcnf
samples/lp/*.lp
samples/lp/*.sol
samples/lp/*.txt
samples/lp/error/*.lp
samples/maxsat/*.cnf
samples/maxsat/*.wcnf
samples/mps/*.mps
samples/pbo/*.opb
samples/pbs/*.opb
samples/sat/*.cnf
samples/wbo/*.wbo
samples/sdp/*.dat
samples/sdp/*.dat-s
samples/smt/*.smt2
samples/smt/*.ys
samples/qbf/*.qdimacs
samples/programs/sudoku/*.sdk
samples/programs/knapsack/README.md
samples/programs/knapsack/*.txt
samples/programs/htc/test1.dat
samples/programs/htc/test2.dat
samples/programs/svm2lp/a1a
samples/programs/nonogram/*.cwd
samples/programs/nonogram/README.md
samples/programs/numberlink/README.md
samples/programs/numberlink/ADC2013/*.txt
samples/programs/numberlink/ADC2014_QA/A/*.txt
samples/programs/numberlink/ADC2014_QA/Q/*.txt
samples/programs/numberlink/ADC2016/sample/01/*.txt
benchmarks/UF250.1065.100/*.cnf
benchmarks/UUF250.1065.100/*.cnf
Build-Type: Simple
Flag ForceChar8
Description: set default encoding to char8 (not to use iconv)
Default: False
Manual: True
Flag LinuxStatic
Description: build statically linked binaries
Default: False
Manual: True
Flag WithZlib
Description: Use zlib package to support gzipped files
Default: True
Manual: True
Flag BuildToyFMF
Description: build toyfmf command
Default: False
Manual: True
Flag BuildSamplePrograms
Description: build sample programs
Default: False
Manual: True
Flag BuildMiscPrograms
Description: build misc programs
Default: False
Manual: True
Flag UseHaskeline
Description: use haskeline package
Manual: True
Default: True
Flag OpenCL
Description: use opencl package
Manual: True
Default: False
Flag ExtraBoundsChecking
Description: enable extra bounds checking for debugging
Manual: True
Default: False
source-repository head
type: git
location: git://github.com/msakai/toysolver.git
Library
Exposed: True
Hs-source-dirs: src
Build-Depends:
array >=0.5,
-- GHC >=8.6 && <9.5
base >=4.12 && <4.18,
bytestring >=0.9.2.1 && <0.12,
bytestring-builder,
bytestring-encoding >=0.1.1.0,
case-insensitive,
clock >=0.7.1,
-- IntMap.restrictKeys and IntMap.withoutKeys require containers >=0.5.8
containers >=0.5.8,
data-default,
data-default-class,
data-interval >=2.0.1 && <2.2.0,
deepseq,
directory,
extended-reals >=0.1 && <1.0,
filepath,
finite-field >=0.9.0 && <1.0.0,
-- hashUsing is available on hashable >=1.2
hashable >=1.2 && <1.5.0.0,
hashtables,
heaps,
intern >=0.9.1.2 && <1.0.0.0,
log-domain,
-- numLoopState requires loop >=0.3.0
loop >=0.3.0 && < 1.0.0,
MIP >=0.1.1.0 && <0.2,
mtl >=2.1.2,
multiset,
-- createSystemRandom requires mwc-random >=0.13.1.0
mwc-random >=0.13.1 && <0.16,
OptDir,
lattices,
megaparsec >=7 && <10,
-- Text.PrettyPrint.HughesPJClass is available on pretty >=1.1.2.0
pretty >=1.1.2.0 && <1.2,
primes,
primitive >=0.6,
process >=1.1.0.2,
pseudo-boolean >=0.1.3.0 && <0.2.0.0,
queue,
scientific,
semigroups >=0.17,
sign >=0.2.0 && <1.0.0,
stm >=2.3,
template-haskell,
temporary >=1.2,
text >=1.1.0.0,
-- defaultTimeLocale is available on time >=1.5.0
time >=1.5.0,
transformers >=0.2,
transformers-compat >=0.3,
unordered-containers >=0.2.3 && <0.3.0,
-- imapM and modify are available on vector >=0.11.0
vector >=0.11,
vector-space >=0.8.6,
xml-conduit
if flag(WithZlib)
Build-Depends: zlib
CPP-Options: "-DWITH_ZLIB"
if flag(OpenCL)
Build-Depends: OpenCL >=1.0.3.4
Exposed-Modules: ToySolver.SAT.Solver.MessagePassing.SurveyPropagation.OpenCL
if flag(ExtraBoundsChecking)
CPP-Options: "-DEXTRA_BOUNDS_CHECKING"
if impl(ghc)
Build-Depends: ghc-prim
Default-Language: Haskell2010
Other-Extensions:
BangPatterns
CPP
ConstraintKinds
DeriveDataTypeable
DeriveGeneric
ExistentialQuantification
FlexibleContexts
FlexibleInstances
FunctionalDependencies
GADTs
GeneralizedNewtypeDeriving
InstanceSigs
KindSignatures
MultiParamTypeClasses
OverloadedStrings
PatternSynonyms
Rank2Types
RecursiveDo
ScopedTypeVariables
TemplateHaskell
TypeFamilies
TypeOperators
TypeSynonymInstances
UndecidableInstances
ViewPatterns
if impl(ghc)
Other-Extensions:
MagicHash
UnboxedTuples
Exposed-Modules:
ToySolver.Arith.BoundsInference
ToySolver.Arith.CAD
ToySolver.Arith.ContiTraverso
ToySolver.Arith.Cooper
ToySolver.Arith.Cooper.Base
ToySolver.Arith.Cooper.FOL
ToySolver.Arith.DifferenceLogic
ToySolver.Arith.FourierMotzkin
ToySolver.Arith.FourierMotzkin.Base
ToySolver.Arith.FourierMotzkin.FOL
ToySolver.Arith.FourierMotzkin.Optimization
ToySolver.Arith.LPUtil
ToySolver.Arith.MIP
ToySolver.Arith.OmegaTest
ToySolver.Arith.OmegaTest.Base
ToySolver.Arith.Simplex
ToySolver.Arith.Simplex.Simple
ToySolver.Arith.Simplex.Textbook
ToySolver.Arith.Simplex.Textbook.LPSolver
ToySolver.Arith.Simplex.Textbook.LPSolver.Simple
ToySolver.Arith.Simplex.Textbook.MIPSolver.Simple
ToySolver.Arith.VirtualSubstitution
ToySolver.BitVector
ToySolver.BitVector.Base
ToySolver.BitVector.Solver
ToySolver.EUF.CongruenceClosure
ToySolver.EUF.EUFSolver
ToySolver.EUF.FiniteModelFinder
ToySolver.Combinatorial.BipartiteMatching
ToySolver.Combinatorial.HittingSet.DAA
ToySolver.Combinatorial.HittingSet.MARCO
ToySolver.Combinatorial.HittingSet.Simple
ToySolver.Combinatorial.HittingSet.HTCBDD
ToySolver.Combinatorial.HittingSet.InterestingSets
ToySolver.Combinatorial.HittingSet.SHD
ToySolver.Combinatorial.HittingSet.FredmanKhachiyan1996
ToySolver.Combinatorial.HittingSet.GurvichKhachiyan1999
ToySolver.Combinatorial.HittingSet.Util
ToySolver.Combinatorial.Knapsack.BB
ToySolver.Combinatorial.Knapsack.DPDense
ToySolver.Combinatorial.Knapsack.DPSparse
ToySolver.Combinatorial.SubsetSum
ToySolver.Converter
ToySolver.Converter.Base
ToySolver.Converter.GCNF2MaxSAT
ToySolver.Converter.ObjType
ToySolver.Converter.MIP2PB
ToySolver.Converter.MIP2SMT
ToySolver.Converter.NAESAT
ToySolver.Converter.PB
ToySolver.Converter.PB2IP
ToySolver.Converter.PB2LSP
ToySolver.Converter.PBSetObj
ToySolver.Converter.PB2SMP
ToySolver.Converter.QBF2IPC
ToySolver.Converter.QUBO
ToySolver.Converter.SAT2MIS
ToySolver.Converter.SAT2KSAT
ToySolver.Converter.SAT2MaxCut
ToySolver.Converter.SAT2MaxSAT
ToySolver.Converter.Tseitin
ToySolver.Data.AlgebraicNumber.Complex
ToySolver.Data.AlgebraicNumber.Real
ToySolver.Data.AlgebraicNumber.Root
ToySolver.Data.AlgebraicNumber.Sturm
ToySolver.Data.Boolean
ToySolver.Data.BoolExpr
ToySolver.Data.Delta
ToySolver.Data.DNF
ToySolver.Data.FOL.Arith
ToySolver.Data.FOL.Formula
ToySolver.Data.IntVar
ToySolver.Data.LA
ToySolver.Data.LA.FOL
ToySolver.Data.LBool
ToySolver.Data.OrdRel
ToySolver.Data.Polynomial
ToySolver.Data.Polynomial.Factorization.FiniteField
ToySolver.Data.Polynomial.Factorization.Hensel
ToySolver.Data.Polynomial.Factorization.Hensel.Internal
ToySolver.Data.Polynomial.Factorization.Integer
ToySolver.Data.Polynomial.Factorization.Kronecker
ToySolver.Data.Polynomial.Factorization.Rational
ToySolver.Data.Polynomial.Factorization.SquareFree
ToySolver.Data.Polynomial.Factorization.Zassenhaus
ToySolver.Data.Polynomial.GroebnerBasis
ToySolver.Data.Polynomial.Interpolation.Hermite
ToySolver.Data.Polynomial.Interpolation.Lagrange
ToySolver.FileFormat
ToySolver.FileFormat.Base
ToySolver.FileFormat.CNF
ToySolver.Graph.Base
ToySolver.Graph.ShortestPath
ToySolver.Graph.MaxCut
ToySolver.QBF
ToySolver.QUBO
ToySolver.SAT
ToySolver.SAT.Encoder.Integer
ToySolver.SAT.Encoder.PB
ToySolver.SAT.Encoder.PB.Internal.Adder
ToySolver.SAT.Encoder.PB.Internal.BDD
ToySolver.SAT.Encoder.PB.Internal.Sorter
ToySolver.SAT.Encoder.PBNLC
ToySolver.SAT.Encoder.Cardinality
ToySolver.SAT.Encoder.Cardinality.Internal.Naive
ToySolver.SAT.Encoder.Cardinality.Internal.ParallelCounter
ToySolver.SAT.Encoder.Cardinality.Internal.Totalizer
ToySolver.SAT.Encoder.Tseitin
ToySolver.SAT.ExistentialQuantification
ToySolver.SAT.Formula
ToySolver.SAT.MUS
ToySolver.SAT.MUS.Enum
ToySolver.SAT.MUS.Types
ToySolver.SAT.PBO
ToySolver.SAT.PBO.Context
ToySolver.SAT.PBO.BC
ToySolver.SAT.PBO.BCD
ToySolver.SAT.PBO.BCD2
ToySolver.SAT.PBO.MSU4
ToySolver.SAT.PBO.UnsatBased
ToySolver.SAT.Solver.CDCL
ToySolver.SAT.Solver.CDCL.Config
ToySolver.SAT.Solver.MessagePassing.SurveyPropagation
ToySolver.SAT.Solver.SLS.ProbSAT
ToySolver.SAT.Solver.SLS.UBCSAT
ToySolver.SAT.Store.CNF
ToySolver.SAT.Store.PB
ToySolver.SAT.TheorySolver
ToySolver.SAT.Types
ToySolver.SAT.Printer
ToySolver.SDP
ToySolver.SMT
ToySolver.Text.SDPFile
ToySolver.Internal.Data.IndexedPriorityQueue
ToySolver.Internal.Data.IOURef
ToySolver.Internal.Data.PriorityQueue
ToySolver.Internal.Data.SeqQueue
ToySolver.Internal.Data.Vec
ToySolver.Internal.ProcessUtil
ToySolver.Internal.TextUtil
ToySolver.Internal.Util
ToySolver.Wang
ToySolver.Version
Other-Modules:
ToySolver.Converter.PB.Internal.LargestIntersectionFinder
ToySolver.Converter.PB.Internal.Product
ToySolver.Data.AlgebraicNumber.Graeffe
ToySolver.Data.Polynomial.Base
ToySolver.SAT.MUS.Base
ToySolver.SAT.MUS.Deletion
ToySolver.SAT.MUS.Insertion
ToySolver.SAT.MUS.QuickXplain
ToySolver.SAT.MUS.Enum.Base
ToySolver.SAT.MUS.Enum.CAMUS
ToySolver.Version.TH
Paths_toysolver
autogen-modules:
Paths_toysolver
-- GHC-Prof-Options: -auto-all
Executable toysolver
Main-is: toysolver.hs
HS-Source-Dirs: app
Build-Depends:
array,
base,
containers,
data-default-class,
filepath,
MIP,
OptDir,
-- maybeReader is available on optparse-applicative >=0.13.0.0
optparse-applicative >=0.13,
pseudo-boolean,
scientific,
toysolver
Default-Language: Haskell2010
Other-Extensions: CPP
GHC-Options: -rtsopts -threaded
if flag(ForceChar8)
CPP-OPtions: "-DFORCE_CHAR8"
if flag(LinuxStatic)
GHC-Options: -static -optl-static -optl-pthread
-- GHC-Prof-Options: -auto-all
Executable toysat
Main-is: toysat.hs
HS-Source-Dirs: app/toysat
Build-Depends:
array,
base,
bytestring,
containers,
clock,
data-default-class,
filepath,
megaparsec,
MIP,
mwc-random,
-- maybeReader is available on optparse-applicative >=0.13.0.0
optparse-applicative >=0.13,
pseudo-boolean,
scientific,
time,
toysolver,
unbounded-delays,
vector
Default-Language: Haskell2010
Other-Extensions: ScopedTypeVariables, CPP
GHC-Options: -rtsopts -threaded
-- GHC-Prof-Options: -auto-all
if flag(ForceChar8)
CPP-OPtions: "-DFORCE_CHAR8"
if flag(WithZlib)
CPP-Options: "-DWITH_ZLIB"
if flag(LinuxStatic)
GHC-Options: -static -optl-static -optl-pthread
Foreign-Library toysat-ipasir
type: native-shared
if os(Windows)
options: standalone
mod-def-file: app/toysat-ipasir/ipasir.def
if os(Linux)
ld-options: -Wl,--version-script=app/toysat-ipasir/ipasir.map
build-depends:
base,
containers,
toysolver
hs-source-dirs: app/toysat-ipasir
include-dirs: app/toysat-ipasir
c-sources: app/toysat-ipasir/cbits.c
cc-options: -Wall
cpp-options: -DIPASIR_SHARED_LIB -DBUILDING_IPASIR_SHARED_LIB
includes: ipasir.h
other-modules: IPASIR
default-language: Haskell2010
Executable toysmt
HS-Source-Dirs: app/toysmt, Smtlib
Main-is: toysmt.hs
Other-Modules:
ToySolver.SMT.SMTLIB2Solver,
-- Following modules are copied from SmtLib package.
-- http://hackage.haskell.org/package/SmtLib
-- https://github.com/MfesGA/Smtlib
Smtlib.Parsers.CommonParsers,
Smtlib.Parsers.ResponseParsers,
Smtlib.Parsers.CommandsParsers,
Smtlib.Syntax.Syntax,
Smtlib.Syntax.ShowSL
Build-Depends:
base,
containers,
-- TODO: remove intern dependency
intern,
mtl,
optparse-applicative,
parsec >=3.1.2 && <4,
toysolver,
text,
transformers,
transformers-compat
if flag(UseHaskeline)
Build-Depends: haskeline >=0.7 && <0.9
CPP-Options: "-DUSE_HASKELINE_PACKAGE"
Default-Language: Haskell2010
Other-Extensions: ScopedTypeVariables, CPP
GHC-Options: -rtsopts
-- GHC-Prof-Options: -auto-all
if flag(ForceChar8)
CPP-OPtions: "-DFORCE_CHAR8"
if flag(LinuxStatic)
GHC-Options: -static -optl-static -optl-pthread
Executable toyqbf
Main-is: toyqbf.hs
HS-Source-Dirs: app
Build-Depends:
base,
containers,
data-default-class,
optparse-applicative,
toysolver
Default-Language: Haskell2010
Other-Extensions: ScopedTypeVariables, CPP
GHC-Options: -rtsopts
-- GHC-Prof-Options: -auto-all
if flag(ForceChar8)
CPP-OPtions: "-DFORCE_CHAR8"
if flag(LinuxStatic)
GHC-Options: -static -optl-static -optl-pthread
Executable toyfmf
If !flag(BuildToyFMF)
Buildable: False
Main-is: toyfmf.hs
HS-Source-Dirs: app
If flag(BuildToyFMF)
Build-Depends:
base,
containers,
intern,
logic-TPTP >=0.4.6.0 && <0.5,
optparse-applicative,
text,
toysolver
Default-Language: Haskell2010
Other-Extensions: CPP
GHC-Options: -rtsopts
if flag(ForceChar8)
CPP-OPtions: "-DFORCE_CHAR8"
if flag(LinuxStatic)
GHC-Options: -static -optl-static -optl-pthread
-- GHC-Prof-Options: -auto-all
-- Converters
Executable toyconvert
Main-is: toyconvert.hs
HS-Source-Dirs: app
Build-Depends:
base,
ansi-wl-pprint,
bytestring,
bytestring-builder,
data-default-class,
filepath,
MIP,
optparse-applicative,
pseudo-boolean,
scientific,
text,
toysolver
Default-Language: Haskell2010
Other-Extensions: CPP
GHC-Options: -rtsopts
-- GHC-Prof-Options: -auto-all
if flag(ForceChar8)
CPP-OPtions: "-DFORCE_CHAR8"
if flag(WithZlib)
CPP-Options: "-DWITH_ZLIB"
if flag(LinuxStatic)
GHC-Options: -static -optl-static -optl-pthread
-- Sample Programs
Executable sudoku
If !flag(BuildSamplePrograms)
Buildable: False
Main-is: sudoku.hs
HS-Source-Dirs: samples/programs/sudoku
Build-Depends:
array,
base,
toysolver
Default-Language: Haskell2010
Other-Extensions: CPP
GHC-Options: -rtsopts
if flag(ForceChar8)
CPP-OPtions: "-DFORCE_CHAR8"
if flag(LinuxStatic)
GHC-Options: -static -optl-static -optl-pthread
Executable nonogram
If !flag(BuildSamplePrograms)
Buildable: False
Main-is: nonogram.hs
HS-Source-Dirs: samples/programs/nonogram
Build-Depends:
array,
base,
containers,
toysolver
Default-Language: Haskell2010
Other-Extensions: CPP
GHC-Options: -rtsopts
-- GHC-Prof-Options: -auto-all
if flag(ForceChar8)
CPP-OPtions: "-DFORCE_CHAR8"
if flag(LinuxStatic)
GHC-Options: -static -optl-static -optl-pthread
Executable nqueens
If !flag(BuildSamplePrograms)
Buildable: False
Main-is: nqueens.hs
HS-Source-Dirs: samples/programs/nqueens
Build-Depends:
array,
base,
toysolver
Default-Language: Haskell2010
Other-Extensions: CPP
GHC-Options: -rtsopts
-- GHC-Prof-Options: -auto-all
if flag(ForceChar8)
CPP-OPtions: "-DFORCE_CHAR8"
if flag(LinuxStatic)
GHC-Options: -static -optl-static -optl-pthread
Executable numberlink
If !flag(BuildSamplePrograms)
Buildable: False
Main-is: numberlink.hs
HS-Source-Dirs: samples/programs/numberlink
Build-Depends:
array,
base,
bytestring,
containers,
data-default-class,
parsec,
pseudo-boolean,
toysolver
Default-Language: Haskell2010
Other-Extensions: CPP
GHC-Options: -rtsopts
-- GHC-Prof-Options: -auto-all
if flag(ForceChar8)
CPP-OPtions: "-DFORCE_CHAR8"
if flag(LinuxStatic)
GHC-Options: -static -optl-static -optl-pthread
Executable knapsack
If !flag(BuildSamplePrograms)
Buildable: False
Main-is: knapsack.hs
HS-Source-Dirs: samples/programs/knapsack
Build-Depends:
base,
toysolver
Default-Language: Haskell2010
Other-Extensions: CPP
GHC-Options: -rtsopts
-- GHC-Prof-Options: -auto-all
if flag(ForceChar8)
CPP-OPtions: "-DFORCE_CHAR8"
if flag(LinuxStatic)
GHC-Options: -static -optl-static -optl-pthread
Executable assign
If !flag(BuildSamplePrograms)
Buildable: False
Main-is: assign.hs
HS-Source-Dirs: samples/programs/assign
Build-Depends:
attoparsec,
base,
bytestring,
containers,
toysolver,
vector
Default-Language: Haskell2010
Other-Extensions: CPP
GHC-Options: -rtsopts
-- GHC-Prof-Options: -auto-all
if flag(ForceChar8)
CPP-OPtions: "-DFORCE_CHAR8"
if flag(LinuxStatic)
GHC-Options: -static -optl-static -optl-pthread
Executable shortest-path
If !flag(BuildSamplePrograms)
Buildable: False
Main-is: shortest-path.hs
HS-Source-Dirs: samples/programs/shortest-path
Build-Depends:
base,
bytestring,
containers,
unordered-containers,
toysolver
Default-Language: Haskell2010
Other-Extensions: CPP
GHC-Options: -rtsopts
-- GHC-Prof-Options: -auto-all
if flag(ForceChar8)
CPP-OPtions: "-DFORCE_CHAR8"
if flag(LinuxStatic)
GHC-Options: -static -optl-static -optl-pthread
Executable htc
If !flag(BuildSamplePrograms)
Buildable: False
Main-is: htc.hs
HS-Source-Dirs: samples/programs/htc
Build-Depends:
base,
containers,
toysolver
Default-Language: Haskell2010
Other-Extensions: CPP
GHC-Options: -rtsopts
-- GHC-Prof-Options: -auto-all
if flag(ForceChar8)
CPP-OPtions: "-DFORCE_CHAR8"
if flag(LinuxStatic)
GHC-Options: -static -optl-static -optl-pthread
Executable svm2lp
If !flag(BuildSamplePrograms)
Buildable: False
Main-is: svm2lp.hs
HS-Source-Dirs: samples/programs/svm2lp
Build-Depends:
base,
containers,
data-default-class,
MIP,
scientific,
split,
text,
toysolver
Default-Language: Haskell2010
Other-Extensions: CPP
GHC-Options: -rtsopts
-- GHC-Prof-Options: -auto-all
if flag(ForceChar8)
CPP-OPtions: "-DFORCE_CHAR8"
if flag(LinuxStatic)
GHC-Options: -static -optl-static -optl-pthread
Executable survey-propagation
if !flag(BuildSamplePrograms)
Buildable: False
Main-is: survey-propagation.hs
HS-Source-Dirs: samples/programs/survey-propagation
Build-Depends:
base,
data-default-class,
toysolver
if flag(OpenCL)
Build-Depends: OpenCL
CPP-Options: "-DENABLE_OPENCL"
Default-Language: Haskell2010
Other-Extensions: CPP
-- We use threaded RTS to avoid the error "schedule: re-entered unsafely.
-- Perhaps a 'foreign import unsafe' should be 'safe'?" on NVIDIA CUDA.
GHC-Options: -rtsopts -threaded
-- GHC-Prof-Options: -auto-all
if flag(ForceChar8)
CPP-Options: "-DFORCE_CHAR8"
if flag(LinuxStatic)
GHC-Options: -static -optl-static -optl-pthread
Executable probsat
if !flag(BuildSamplePrograms)
Buildable: False
Main-is: probsat.hs
HS-Source-Dirs: samples/programs/probsat
Build-Depends:
base,
clock,
data-default-class,
mwc-random,
optparse-applicative,
vector,
toysolver
Default-Language: Haskell2010
Other-Extensions: CPP
GHC-Options: -rtsopts
-- GHC-Prof-Options: -auto-all
if flag(ForceChar8)
CPP-Options: "-DFORCE_CHAR8"
if flag(LinuxStatic)
GHC-Options: -static -optl-static -optl-pthread
-- Misc Programs
Executable pigeonhole
If !flag(BuildMiscPrograms)
Buildable: False
Main-is: pigeonhole.hs
HS-Source-Dirs: app
Build-Depends:
base,
bytestring,
containers,
pseudo-boolean,
toysolver
Default-Language: Haskell2010
Other-Extensions: CPP
GHC-Options: -rtsopts
-- GHC-Prof-Options: -auto-all
if flag(ForceChar8)
CPP-OPtions: "-DFORCE_CHAR8"
if flag(LinuxStatic)
GHC-Options: -static -optl-static -optl-pthread
Executable maxsatverify
If !flag(BuildMiscPrograms)
Buildable: False
Main-is: maxsatverify.hs
HS-Source-Dirs: app
Build-Depends:
array,
base,
toysolver
Default-Language: Haskell2010
Other-Extensions: CPP
GHC-Options: -rtsopts
-- GHC-Prof-Options: -auto-all
if flag(ForceChar8)
CPP-OPtions: "-DFORCE_CHAR8"
if flag(LinuxStatic)
GHC-Options: -static -optl-static -optl-pthread
Executable pbverify
Main-is: pbverify.hs
If !flag(BuildMiscPrograms)
Buildable: False
HS-Source-Dirs: app
Build-Depends:
array,
base,
pseudo-boolean,
toysolver
Default-Language: Haskell2010
Other-Extensions: CPP
GHC-Options: -rtsopts
-- GHC-Prof-Options: -auto-all
if flag(ForceChar8)
CPP-OPtions: "-DFORCE_CHAR8"
if flag(LinuxStatic)
GHC-Options: -static -optl-static -optl-pthread
-- Test suites and benchmarks
Test-suite TestPolynomial
Type: exitcode-stdio-1.0
HS-Source-Dirs: test
Main-is: TestPolynomial.hs
Build-depends:
base,
containers,
data-interval,
finite-field >=0.7.0 && <1.0.0,
pretty,
tasty >=0.10.1,
tasty-hunit >=0.9 && <0.11,
tasty-quickcheck >=0.8 && <0.11,
tasty-th,
toysolver
Default-Language: Haskell2010
Other-Extensions: TemplateHaskell
Test-suite TestSuite
Type: exitcode-stdio-1.0
HS-Source-Dirs: test Smtlib app/toysmt
Main-is: TestSuite.hs
Other-Modules:
Test.AReal
Test.AReal2
Test.Arith
Test.BitVector
Test.BoolExpr
Test.BipartiteMatching
Test.CNF
Test.CongruenceClosure
Test.ContiTraverso
Test.Converter
Test.Delta
Test.FiniteModelFinder
Test.GraphShortestPath
Test.HittingSets
Test.Knapsack
Test.Misc
Test.MIPSolver
Test.ProbSAT
Test.QBF
Test.QUBO
Test.SAT
Test.SAT.Encoder
Test.SAT.ExistentialQuantification
Test.SAT.MUS
Test.SAT.TheorySolver
Test.SAT.Types
Test.SAT.Utils
Test.SDPFile
Test.Simplex
Test.SimplexTextbook
Test.SMT
Test.SMTLIB2Solver
Test.Smtlib
Test.SubsetSum
ToySolver.SMT.SMTLIB2Solver
Smtlib.Parsers.CommonParsers
Smtlib.Parsers.ResponseParsers
Smtlib.Parsers.CommandsParsers
Smtlib.Syntax.Syntax
Smtlib.Syntax.ShowSL
Build-depends:
array,
base,
bytestring,
bytestring-builder,
containers,
data-default-class,
data-interval,
deepseq,
hashable,
intern,
lattices,
megaparsec,
mtl,
mwc-random,
OptDir,
parsec >=3.1.2 && <4,
pseudo-boolean,
-- sublistOf is available on QuickCheck >=2.8
QuickCheck >=2.8 && <3,
scientific,
tasty >=0.10.1,
tasty-hunit >=0.9 && <0.11,
tasty-quickcheck >=0.8 && <0.11,
tasty-th,
text,
toysolver,
transformers,
transformers-compat,
unordered-containers,
vector,
vector-space
Default-Language: Haskell2010
Other-Extensions:
CPP
DataKinds
ScopedTypeVariables
TemplateHaskell
Benchmark BenchmarkSATLIB
type: exitcode-stdio-1.0
hs-source-dirs: benchmarks
main-is: BenchmarkSATLIB.hs
build-depends:
array,
base,
criterion >=1.0 && <1.7,
data-default-class,
toysolver
Default-Language: Haskell2010
Benchmark BenchmarkKnapsack
type: exitcode-stdio-1.0
hs-source-dirs: benchmarks
main-is: BenchmarkKnapsack.hs
build-depends:
base,
criterion >=1.0 && <1.7,
toysolver
Default-Language: Haskell2010
Benchmark BenchmarkSubsetSum
type: exitcode-stdio-1.0
hs-source-dirs: benchmarks
main-is: BenchmarkSubsetSum.hs
build-depends:
base,
criterion >=1.0 && <1.7,
toysolver,
vector
Default-Language: Haskell2010