toysolver 0.9.0 → 0.10.0

raw patch · 103 files changed

+4046/−4695 lines, 103 filesdep +integer-logarithmsdep +language-smtlibdep −ansi-wl-pprintdep ~MIPdep ~aesondep ~arraynew-component:exe:toysolver-checkPVP ok

version bump matches the API change (PVP)

Dependencies added: integer-logarithms, language-smtlib

Dependencies removed: ansi-wl-pprint

Dependency ranges changed: MIP, aeson, array, base, bytestring, hashable, intern, mtl, optparse-applicative, parsec, pseudo-boolean, temporary, text, transformers, transformers-compat

API changes (from Hackage documentation)

Files

• CHANGELOG.markdown +59/−16
• README.md +49/−12
• Smtlib/Smtlib/Parsers/CommandsParsers.hs +0/−653
• Smtlib/Smtlib/Parsers/CommonParsers.hs +0/−473
• Smtlib/Smtlib/Parsers/ResponseParsers.hs +0/−375
• Smtlib/Smtlib/Syntax/ShowSL.hs +0/−247
• Smtlib/Smtlib/Syntax/Syntax.hs +0/−279
• app/maxsatverify.hs +0/−48
• app/pbverify.hs +0/−47
• app/pigeonhole.hs +0/−1
• app/toyconvert.hs +44/−41
• app/toyqbf.hs +1/−1
• app/toysat/toysat.hs +41/−30
• app/toysmt/ToySolver/SMT/SMTLIB2Solver.hs +0/−888
• app/toysmt/toysmt.hs +77/−35
• app/toysolver.hs +132/−58
• app/toysolver_check.hs +163/−0
• samples/programs/assign/assign.hs +1/−1
• samples/programs/htc/htc.hs +1/−1
• samples/programs/knapsack/knapsack.hs +1/−1
• samples/programs/numberlink/numberlink.hs +1/−1
• samples/programs/shortest-path/shortest-path.hs +5/−10
• samples/programs/survey-propagation/survey-propagation.hs +0/−1
• samples/sat/empty-clause.cnf +0/−1
• src/ToySolver/Arith/CAD.hs +1/−3
• src/ToySolver/Arith/ContiTraverso.hs +1/−1
• src/ToySolver/Arith/Cooper/Base.hs +1/−1
• src/ToySolver/Arith/FourierMotzkin/Base.hs +1/−1
• src/ToySolver/Arith/MIP.hs +1/−1
• src/ToySolver/Arith/OmegaTest/Base.hs +1/−1
• src/ToySolver/Arith/Simplex.hs +2/−2
• src/ToySolver/Arith/Simplex/Textbook.hs +1/−1
• src/ToySolver/BitVector/Base.hs +6/−20
• src/ToySolver/BitVector/Solver.hs +3/−11
• src/ToySolver/Combinatorial/HittingSet/HTCBDD.hs +1/−3
• src/ToySolver/Combinatorial/HittingSet/SHD.hs +1/−3
• src/ToySolver/Combinatorial/Knapsack/BB.hs +3/−3
• src/ToySolver/Combinatorial/Knapsack/DPDense.hs +6/−4
• src/ToySolver/Combinatorial/Knapsack/DPSparse.hs +1/−1
• src/ToySolver/Converter/MIP.hs +226/−141
• src/ToySolver/Converter/MIP2SMT.hs +1/−1
• src/ToySolver/Converter/PB.hs +133/−80
• src/ToySolver/Converter/PB/Internal/Product.hs +2/−3
• src/ToySolver/Converter/QUBO.hs +1/−1
• src/ToySolver/Converter/SAT2MIS.hs +3/−5
• src/ToySolver/Data/AlgebraicNumber/Real.hs +1/−1
• src/ToySolver/Data/AlgebraicNumber/Root.hs +1/−1
• src/ToySolver/Data/AlgebraicNumber/Sturm.hs +15/−6
• src/ToySolver/Data/BoolExpr.hs +1/−1
• src/ToySolver/Data/LA.hs +1/−1
• src/ToySolver/Data/Polyhedron.hs +24/−27
• src/ToySolver/Data/Polynomial/Base.hs +30/−20
• src/ToySolver/Data/Polynomial/Factorization/FiniteField.hs +1/−1
• src/ToySolver/Data/Polynomial/Factorization/Kronecker.hs +1/−1
• src/ToySolver/Data/Polynomial/Factorization/Zassenhaus.hs +1/−1
• src/ToySolver/Data/Polynomial/Interpolation/Hermite.hs +1/−1
• src/ToySolver/EUF/FiniteModelFinder.hs +1/−1
• src/ToySolver/FileFormat/Base.hs +18/−3
• src/ToySolver/Internal/SolutionChecker.hs +307/−0
• src/ToySolver/QBF.hs +4/−3
• src/ToySolver/SAT/Encoder/Integer.hs +32/−8
• src/ToySolver/SAT/Encoder/PB/Internal/BCCNF.hs +2/−2
• src/ToySolver/SAT/Encoder/PB/Internal/BDD.hs +2/−2
• src/ToySolver/SAT/Encoder/PB/Internal/Sorter.hs +3/−3
• src/ToySolver/SAT/Internal/JSON.hs +25/−8
• src/ToySolver/SAT/LogParser.hs +121/−0
• src/ToySolver/SAT/MUS/Base.hs +0/−1
• src/ToySolver/SAT/MUS/Deletion.hs +1/−1
• src/ToySolver/SAT/MUS/Enum/CAMUS.hs +0/−1
• src/ToySolver/SAT/MUS/Insertion.hs +1/−1
• src/ToySolver/SAT/MUS/QuickXplain.hs +1/−1
• src/ToySolver/SAT/PBO/BCD.hs +1/−1
• src/ToySolver/SAT/Printer.hs +102/−37
• src/ToySolver/SAT/Solver/CDCL.hs +9/−24
• src/ToySolver/SAT/Solver/SLS/ProbSAT.hs +1/−14
• src/ToySolver/SAT/Solver/SLS/UBCSAT.hs +1/−1
• src/ToySolver/SAT/Types.hs +1/−1
• src/ToySolver/SMT.hs +14/−32
• src/ToySolver/SMT/SMTLIB2Solver.hs +896/−0
• src/ToySolver/Version.hs +1/−1
• test/Test/AReal.hs +32/−0
• test/Test/Arith.hs +0/−1
• test/Test/BitVector.hs +7/−6
• test/Test/ContiTraverso.hs +0/−1
• test/Test/Converter.hs +242/−7
• test/Test/MIPSolver.hs +0/−1
• test/Test/Misc.hs +16/−0
• test/Test/QUBO.hs +1/−1
• test/Test/SAT.hs +51/−0
• test/Test/SAT/Encoder.hs +27/−1
• test/Test/SAT/LogParser.hs +269/−0
• test/Test/SAT/Types.hs +1/−1
• test/Test/SAT/Utils.hs +1/−1
• test/Test/SDPFile.hs +0/−1
• test/Test/SMT.hs +29/−0
• test/Test/SMTLIB2Solver.hs +104/−72
• test/Test/Simplex.hs +0/−1
• test/Test/SimplexTextbook.hs +0/−1
• test/Test/Smtlib.hs +0/−604
• test/Test/SolutionChecker.hs +576/−0
• test/TestPolynomial.hs +2/−2
• test/TestSuite.hs +4/−2
• toysolver.cabal +92/−278

@@ -1,7 +1,50 @@+0.10.0 (Unreleased)+-----++* SMT+  * Migrate `toysmt` from the `Smtlib` fork to the newly developed [language-smtlib](https://hackage.haskell.org/package/language-smtlib) package (#206, #214)+    * The `toysmt` REPL now supports multi-line input (#206, #213)+  * Support `define-const` command in `ToySolver.SMT.SMTLIB2Solver` (#215)+  * Update the semantics of zero division on bitvectors to conform to SMT-LIB >=2.6 (#209)+  * `toysmt` now suppresses the prompt and does not use haskeline when stdin is not a terminal (#211)+  * Fix SMT model not to contain a bogus entry for an unused uninterpreted function (#216)+  * Modify the `(get-model)` command to return the definition of the zero-division function (`/0`) instead of the assertions about division by zero results (#217)+* Converter and `toyconvert` command+  * Do not produce `obj<T` constraint in `wbo2pb` when all interpretations are admissible (#157)+  * Optimize `unconstrainPB` a little (#159, #161)+  * Change `ToySolver.SAT.Encoder.Integer` to encode integer variables without introducing `<=` constraints (#162)+  * Store surplus expression instead of raw variables in `inequalitiesToEqualitiesPB` (#164)+  * Refactor `ToySolver.SAT.Encoder.Integer` (#167)+  * Improve `inequalitiesToEqualitiesPB` to produce more compact output (#168)+  * Extend `normalizePB` to transform constant terms in the objective function into non-constant terms (#169)+  * Support semi-integer variables in IP→PB conversion and improve error messages (#170)+  * Simplify JSON that represents `PBSum` (#171)+  * Scale objective function and constraints using rational instead of integer in IP→PB transformation (#172)+  * Linearize constant term in objective function when writing LP/MPS file (#185)+  * Add `--[no-]mps-obj-name` option to `toyconvert` (#188)+  * Rename `--lp` option to `--mip` and keep `--lp` as an alias (#189)+  * Optimize `pb2ip` and `wbo2ip` by not calling `convVar` repeatedly (#191)+* `toysat`+  * Conform to MaxSAT Evaluation 2024 (#177)+    * It outputs `SATISFIABLE` in MaxSAT mode if it finds a model but fails to prove optimality+    * Add `--exit-code` option to set exit code+* Dependencies+  * Stop supporting 32-bit Windows (#154)+  * Stop supporting GHC 9.4 and below (#156, #205)+  * Use `pseudo-boolean-0.1.12.0` (#158)+  * Require `aeson >=2.0`, `array >=0.5.6`, `hashable >=1.4.3`, and `optparse-applicative >=0.18` (#208)+  * Require `language-smtlib >=0.2.0.0` (#206, #214)+* Misc+  * Add `toysolver-check` command to check solution (#174, #196)+  * Improve model output speed by printing using `ByteString` (#175)+  * Build statically linked Linux binaries (#194)+  * Use Cauchy's bounds instead of Lagrange's bounds as the bounds for all roots (#203)+  * Optimize `divModMP` by rewriting it from a full-reduction strategy to the standard textbook leading-term multivariate division algorithm (#212)+ 0.9.0 (2025-02-18) ----- -* Converters updates+* Converter updates   * Add `--dump-info` option to `toyconvert` (#119, #120, #125)   * Change the signs of QUBO-related converter's representation of offset (#126)   * Change `WBO2IPInfo` not to store weights (#124)@@ -14,9 +57,9 @@   * Restructure converter modules (#142)   * Support SOS constraints over non-binary variables in `mip2pb` (#140)   * Rename `mip2pb` to `ip2pb`-* Pseudo-boolean and cardinality constarint encoder updates+* Pseudo-boolean and cardinality constraint encoder updates   * Consider polarity in encoding of pseudo-boolean and cardinality constraints (#88)-  * Add BC-CNF pseudo boolean constraint encoder (#85)+  * Add BC-CNF pseudo-boolean constraint encoder (#85)   * Support specifying PB encoding strategy (#77) * Dependencies   * Support GHC 9.4 (#92), 9.6, 9.8, 9.10@@ -28,7 +71,7 @@   * Remove features that depend on OpenCL (#90)   * Improve `ToySolver.Graph` module (#130, #150) -0.8.0+0.8.0 (2022-07-26) -----  * Separate Formula type from `ToySolver.SAT.Encoder.Tseitin` into `ToySolver.SAT.Formula` (#74)@@ -41,15 +84,15 @@ * Remove deprecated API (#56) * Support GHC-9.2 (#76) and stop supporting GHC 8.0, 8.2, and 8.4 (#50) -0.7.0+0.7.0 (2021-02-08) -----  * add `toysat-ipasir` foreign library which implements [IPASIR](https://github.com/biotomas/ipasir) API for incremental SAT solving. * `ToySolver.SAT`   * Restructure SAT solver modules under `ToySolver.SAT.Solver.*`-  * add `SequentialCounter`, `ParallelCounter` and `Totalizer` as methods for encoding cardinality constraints+  * add `SequentialCounter`, `ParallelCounter`, and `Totalizer` as methods for encoding cardinality constraints   * add `PackedLit` type to reduce memory footprint-  * use structure of array (SOA) approach to reduce memory footprint+  * use structure of array (SOA) approach to reducethe memory footprint   * add `setLearnCallback`/`clearLearnCallback` and `setTerminateCallback`/`clearTerminateCallback` which correspond to [IPASIR](https://github.com/biotomas/ipasir)'s `ipasir_set_learn()` and `ipasir_set_terminate()`.   * add `clearLogger`   * change `getFailedAssumptions` and `getAssumptionsImplications` to return `IntSet` instead of `[Int]`@@ -61,7 +104,7 @@ * stop supporting GHC-7.10 * add `ExtraBoundsChecking` flag for debugging -0.6.0+0.6.0 (2019-10-04) ----- * new solvers:   * `ToySolver.SAT.SLS.ProbSAT` and sample `probsat` program@@ -88,7 +131,7 @@ * switch from `System.Console.GetOpt` to `optparse-applicative` * stop supporting GHC-7.8 -0.5.0+0.5.0 (2017-10-09) ----- * new solvers:   * `ToySolver.BitVector`@@ -102,7 +145,7 @@   * add `--init-sp` option to initialize variable state using survey propagation   * allow using `UBCSAT` when solving PBO/WBO problems * `toysmt`-  * suport bit-vector logic+  * support bit-vector logic * `toyconvert`   * `pbconvert` and `lpconvert` were merged into a single command `toyconvert`   * add `--ksat=NUMBER` option to convert to k-SAT formula@@ -133,18 +176,18 @@ * use `clock` package for measuring duration * add simple numberlink solver sample -0.4.0+0.4.0 (2016-06-25) ------* add experimental SMT (Satisfiablity Modulo Theories) solver 'toysmt', which supports theory of uninterpreted functions and linear real arithmetics.+* add experimental SMT (Satisfiability Modulo Theories) solver 'toysmt', which supports theory of uninterpreted functions and linear real arithmetics. * fix toysat to output model in Max-SAT format instead of PB/WBO format when solving Max-SAT problems * add experimental getAssumptionsImplications functions to ToySolver.SAT module. * add getFixedLiterals to ToySolver.SAT module. * use 'mwc-random' package instead of 'random' package.-* introduce 'Config' data type in ToySolver.SAT to simplify configulation management.+* introduce 'Config' data type in ToySolver.SAT to simplify configuration management. * add subset-sum problem solver-* implement backracking and explanation generation in simplex solver and congruence closure solver.+* implement backtracking and explanation generation in simplex solver and congruence closure solver. -0.3.0+0.3.0 (2015-05-31) ------* split OPB/WBO file library into a serarate 'pseudo-boolean' library.+* split OPB/WBO file library into a separate 'pseudo-boolean' library. 

@@ -3,6 +3,7 @@  [![License](https://img.shields.io/badge/License-BSD%203--Clause-blue.svg)](https://opensource.org/licenses/BSD-3-Clause) [![Join the chat at https://gitter.im/msakai/toysolver](https://badges.gitter.im/Join%20Chat.svg)](https://gitter.im/msakai/toysolver)+[![DeepWiki](https://img.shields.io/badge/DeepWiki-msakai%2Ftoysolver-blue.svg?logo=data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAACwAAAAyCAYAAAAnWDnqAAAAAXNSR0IArs4c6QAAA05JREFUaEPtmUtyEzEQhtWTQyQLHNak2AB7ZnyXZMEjXMGeK/AIi+QuHrMnbChYY7MIh8g01fJoopFb0uhhEqqcbWTp06/uv1saEDv4O3n3dV60RfP947Mm9/SQc0ICFQgzfc4CYZoTPAswgSJCCUJUnAAoRHOAUOcATwbmVLWdGoH//PB8mnKqScAhsD0kYP3j/Yt5LPQe2KvcXmGvRHcDnpxfL2zOYJ1mFwrryWTz0advv1Ut4CJgf5uhDuDj5eUcAUoahrdY/56ebRWeraTjMt/00Sh3UDtjgHtQNHwcRGOC98BJEAEymycmYcWwOprTgcB6VZ5JK5TAJ+fXGLBm3FDAmn6oPPjR4rKCAoJCal2eAiQp2x0vxTPB3ALO2CRkwmDy5WohzBDwSEFKRwPbknEggCPB/imwrycgxX2NzoMCHhPkDwqYMr9tRcP5qNrMZHkVnOjRMWwLCcr8ohBVb1OMjxLwGCvjTikrsBOiA6fNyCrm8V1rP93iVPpwaE+gO0SsWmPiXB+jikdf6SizrT5qKasx5j8ABbHpFTx+vFXp9EnYQmLx02h1QTTrl6eDqxLnGjporxl3NL3agEvXdT0WmEost648sQOYAeJS9Q7bfUVoMGnjo4AZdUMQku50McDcMWcBPvr0SzbTAFDfvJqwLzgxwATnCgnp4wDl6Aa+Ax283gghmj+vj7feE2KBBRMW3FzOpLOADl0Isb5587h/U4gGvkt5v60Z1VLG8BhYjbzRwyQZemwAd6cCR5/XFWLYZRIMpX39AR0tjaGGiGzLVyhse5C9RKC6ai42ppWPKiBagOvaYk8lO7DajerabOZP46Lby5wKjw1HCRx7p9sVMOWGzb/vA1hwiWc6jm3MvQDTogQkiqIhJV0nBQBTU+3okKCFDy9WwferkHjtxib7t3xIUQtHxnIwtx4mpg26/HfwVNVDb4oI9RHmx5WGelRVlrtiw43zboCLaxv46AZeB3IlTkwouebTr1y2NjSpHz68WNFjHvupy3q8TFn3Hos2IAk4Ju5dCo8B3wP7VPr/FGaKiG+T+v+TQqIrOqMTL1VdWV1DdmcbO8KXBz6esmYWYKPwDL5b5FA1a0hwapHiom0r/cKaoqr+27/XcrS5UwSMbQAAAABJRU5ErkJggg==)](https://deepwiki.com/msakai/toysolver)  Hackage: [![Hackage](https://img.shields.io/hackage/v/toysolver.svg)](https://hackage.haskell.org/package/toysolver)@@ -11,9 +12,9 @@ [![Build Status](https://github.com/msakai/toysolver/workflows/build/badge.svg)](https://github.com/msakai/toysolver/actions) [![Coverage Status](https://coveralls.io/repos/msakai/toysolver/badge.svg)](https://coveralls.io/r/msakai/toysolver) -It provides solver implementations of various problems including SAT, SMT, Max-SAT, PBS (Pseudo Boolean Satisfaction), PBO (Pseudo Boolean Optimization), MILP (Mixed Integer Linear Programming) and non-linear real arithmetic.+It provides solver implementations of various problems, including SAT, SMT, Max-SAT, PBS (Pseudo Boolean Satisfaction), PBO (Pseudo Boolean Optimization), MILP (Mixed Integer Linear Programming), and non-linear real arithmetic. -In particular, it contains moderately-fast pure-Haskell SAT solver 'toysat'.+In particular, it contains a moderately fast pure-Haskell SAT solver `toysat`.  Installation ------------@@ -32,8 +33,8 @@ * Mixed Integer Linear Programming (MILP or MIP) * Boolean SATisfiability problem (SAT) * PB-    * Pseudo Boolean Satisfaction (PBS)-    * Pseudo Boolean Optimization (PBO)+    * Pseudo-Boolean Satisfaction (PBS)+    * Pseudo-Boolean Optimization (PBO)     * Weighted Boolean Optimization (WBO) * Max-SAT families     * Max-SAT@@ -45,7 +46,7 @@ Usage:      toysolver [OPTION...] [file.lp|file.mps]-    toysolver --lp [OPTION...] [file.lp|file.mps]+    toysolver --mip [OPTION...] [file.lp|file.mps]     toysolver --sat [OPTION...] [file.cnf]     toysolver --pb [OPTION...] [file.opb]     toysolver --wbo [OPTION...] [file.wbo]@@ -64,8 +65,8 @@     * Minimally Unsatisfiable Subset (MUS)     * Group-Oriented MUS (GMUS) * PB-    * Pseudo Boolean Satisfaction (PBS)-    * Pseudo Boolean Optimization (PBO)+    * Pseudo-Boolean Satisfaction (PBS)+    * Pseudo-Boolean Optimization (PBO)     * Weighted Boolean Optimization (WBO) * Max-SAT families     * Max-SAT@@ -82,7 +83,7 @@     toysat --pb [file.opb|-]     toysat --wbo [file.wbo|-]     toysat --maxsat [file.cnf|file.wcnf|-]-    toysat --lp [file.lp|file.mps|-]+    toysat --mip [file.lp|file.mps|-]  PB'12 competition result:  @@ -92,7 +93,7 @@  ### toysmt -SMT solver based on toysat.+SMT solver based on `toysat`.  Usage: @@ -102,7 +103,7 @@  ### toyfmf -SAT-based finite model finder for first order logic (FOL).+SAT-based finite model finder for first-order logic (FOL).  Usage: @@ -118,8 +119,44 @@  Supported formats: -* Input formats: .cnf .wcnf .opb .wbo .gcnf .lp .mps-* Output formats: .cnf .wcnf .opb .wbo .lsp .lp .mps .smp .smt2 .ys+|Format Name|File Extension|Input|Output|Description|+|-|-|-|-|-|+|DIMACS CNF|`.cnf`|✅|✅|Standard file format for SAT instances|+|WCNF Format|`.wcnf`|✅|✅|Standard file format for Max-SAT instances ([specification](https://maxsat-evaluations.github.io/2024/rules.html#input))|+|OPB Format|`.opb`|✅|✅|PBS (Pseudo-Boolean Satisfaction) and PBO (Pseudo-Boolean Optimization) instances ([specification](https://www.cril.univ-artois.fr/PB24/OPBcompetition.pdf))|+|WBO Format|`.wbo`|✅|✅|WBO (Weighted-Boolean Optimization) instances ([specification](https://www.cril.univ-artois.fr/PB24/OPBcompetition.pdf))|+|Group oriented CNF Input Format|`.gcnf`|✅|-|Used in Group oriented MUS track of the SAT Competition 2011 ([specification](https://web.archive.org/web/20131116055022/http://www.satcompetition.org/2011/rules.pdf))|+|LP File Format|`.lp`|✅|✅|Linear programming (LP) and mixed integer programming (MIP) problems|+|MPS File Format|`.mps`|✅|✅|Linear programming (LP) and mixed integer programming (MIP) problems|+|LSP Format|`.lsp`|-|✅|Input format for [LocalSolver](http://www.localsolver.com/) (only binary variables are supported)|+|SMP Format|`.smp`|-|✅|Input format for [Nuorium Optimizer (NUOPT)](https://www.msi.co.jp/solution/nuopt/top.html) (only binary variables are supported)|+|SMT-LIB 2 Format|`.smt2`|-|✅|Satisfiability Modulo Theories (SMT) problem instances ([website](https://smt-lib.org/))|+|Yices Input Language|`.ys`|-|✅|SMT problem instances for SMT solver [Yices](https://yices.csl.sri.com/)|+|qbsolv QUBO Input File Format|`.qubo`|✅|✅|Unconstrained quadratic binary optimization problems ([specification](https://github.com/dwavesystems/qbsolv?tab=readme-ov-file#qbsolv-qubo-input-file-format))|++### toysolver-check++Solution checker for various problem files.+Usage:++    toysolver-check [OPTION...] [problem_file] [solution_file]+    toysolver-check --mip [OPTION...] [file.lp|file.mps] [file.sol]+    toysolver-check --sat [OPTION...] [file.cnf] [file.log]+    toysolver-check --pb [OPTION...] [file.opb] [file.log]+    toysolver-check --wbo [OPTION...] [file.wbo] [file.log]+    toysolver-check --maxsat [OPTION...] [file.cnf|file.wcnf] [file.log]++    --encoding ENCODING      file encoding for LP/MPS files+    --pb-fast-parser         use attoparsec-based parser instead of+                             megaparsec-based one for speed+    --tol-integrality REAL   If a value of integer variable is within this amount+                             from its nearest integer, it is considered feasible.+                             (default: 1.0e-5)+    --tol-feasibility REAL   If the amount of violation of constraints is within+                             this amount, it is considered feasible.+                             (default: 1.0e-6)+    --tol-optimality REAL    Feasibility tolerance of dual constraints.+                             (default: 1.0e-6)  Bindings --------

@@ -1,653 +0,0 @@-{-|-Module      : Smtlib.Parsers.CommandsParsers-Description : Parsers for Smtlib Commands-Copyright   : Rogério Pontes 2015-License     : WTFPL-Maintainer  : rogerp62@outlook.com-Stability   : stable--This module contains all the required individual parsers for each Smtlib command,-plus one parser to parse an entire SMTLib2 file, parseSource.---}-module Smtlib.Parsers.CommandsParsers where--import           Control.Applicative           as Ctr hiding ((<|>))-import           Control.Monad-import           Data.Functor.Identity-import           Smtlib.Parsers.CommonParsers-import           Smtlib.Syntax.Syntax-import           Text.Parsec.Prim              as Prim-import           Text.ParserCombinators.Parsec as Pc----{--   #########################################################################-   #                                                                       #-   #                       Parser for an SMTLib2 File                      #-   #                                                                       #-   #########################################################################--}---parseSource :: ParsecT String u Identity Source-parseSource = emptySpace *> (Pc.many $ parseCommand <* Pc.try emptySpace)---{--  "###################### Parser For Commands ###############################--}-parseCommand :: ParsecT String u Identity Command-parseCommand = Pc.try parseSetLogic-           <|> Pc.try parseSetOption-           <|> Pc.try parseSetInfo-           <|> Pc.try parseDeclareSort-           <|> Pc.try parseDeclareConst-           <|> Pc.try parseDefineSort-           <|> Pc.try parseDeclareFun-           <|> Pc.try parseDefineFun-           <|> Pc.try parseDefineFunRec-           <|> Pc.try parseDefineFunsRec-           <|> Pc.try parsePush-           <|> Pc.try parsePop-           <|> Pc.try parseAssert-           <|> Pc.try parseCheckSat-           <|> Pc.try parseCheckSatAssuming-           <|> Pc.try parseGetAssertions-           <|> Pc.try parseGetModel-           <|> Pc.try parseGetProof-           <|> Pc.try parseGetUnsatCore-           <|> Pc.try parseGetUnsatAssumptions-           <|> Pc.try parseGetValue-           <|> Pc.try parseGetAssignment-           <|> Pc.try parseGetOption-           <|> Pc.try parseGetInfo-           <|> Pc.try parseReset-           <|> Pc.try parseResetAssertions-           <|> Pc.try parseEcho-           <|> parseExit----{--   #########################################################################-   #                                                                       #-   #                       Parser for each command                         #-   #                                                                       #-   #########################################################################--}-----parseSetLogic :: ParsecT String u Identity Command-parseSetLogic = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "set-logic"-  _ <- emptySpace-  symb <- symbol-  _ <- emptySpace-  _ <- aspC-  return $ SetLogic symb---parseSetOption :: ParsecT String u Identity Command-parseSetOption = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "set-option"-  _ <- emptySpace-  attr <- parseOption-  _ <- emptySpace-  _ <- aspC-  return $ SetOption attr--parseSetInfo :: ParsecT String u Identity Command-parseSetInfo = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "set-info"-  _ <- emptySpace <?> "foi aqui1?"-  attr <- parseAttribute <?> "foi aqui2?"-  _ <- emptySpace-  _ <- aspC-  return $ SetInfo attr---parseDeclareSort :: ParsecT String u Identity Command-parseDeclareSort = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "declare-sort"-  _ <- emptySpace-  symb <- symbol-  _ <- emptySpace-  nume <- numeral-  _ <- emptySpace-  _ <- aspC-  return $ DeclareSort symb (read nume :: Int)--parseDefineSort :: ParsecT String u Identity Command-parseDefineSort = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "define-sort"-  _ <- emptySpace-  symb <- symbol-  _ <- emptySpace-  _ <- aspO-  symbs <- Pc.many $ symbol <* Pc.try emptySpace-  _ <- aspC-  _ <- emptySpace-  sort <- parseSort-  _ <- emptySpace-  _ <- aspC-  return $ DefineSort symb symbs sort---parseDeclareConst :: ParsecT String u Identity Command-parseDeclareConst = do-  _ <-aspO-  _ <- emptySpace-  _ <- string "declare-const"-  _ <- emptySpace-  symb <- symbol-  _ <- emptySpace-  sort <- parseSort-  _ <- emptySpace-  _ <- aspC-  return $ DeclareConst symb sort---parseDeclareFun :: ParsecT String u Identity Command-parseDeclareFun = do-  _ <-aspO-  _ <- emptySpace-  _ <- string "declare-fun"-  _ <- emptySpace-  symb <- symbol-  _ <- emptySpace-  _ <- aspO-  _ <- emptySpace-  sorts <- Pc.many $ parseSort <* Pc.try emptySpace-  _ <- aspC-  _ <- emptySpace-  sort <- parseSort-  _ <- emptySpace-  _ <- aspC-  return $ DeclareFun symb sorts sort---parseDefineFun :: ParsecT String u Identity Command-parseDefineFun = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "define-fun"-  _ <- emptySpace-  symb <- symbol-  _ <- emptySpace-  _ <- aspO-  sVars <- Pc.many $ parseSortedVar <* Pc.try emptySpace-  _ <- aspC-  _ <- emptySpace-  sort <- parseSort-  _ <- emptySpace-  term <- parseTerm-  _ <- emptySpace-  _ <- aspC-  return $ DefineFun symb sVars sort term---parseDefineFunRec :: ParsecT String u Identity Command-parseDefineFunRec = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "define-fun-rec"-  _ <- emptySpace-  symb <- symbol-  _ <- emptySpace-  _ <- aspO-  sVars <- Pc.many $ parseSortedVar <* Pc.try emptySpace-  _ <- aspC-  _ <- emptySpace-  sort <- parseSort-  _ <- emptySpace-  term <- parseTerm-  _ <- emptySpace-  _ <- aspC-  return $ DefineFunRec symb sVars sort term---parseDefineFunsRec :: ParsecT String u Identity Command-parseDefineFunsRec = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "define-funs-rec"-  _ <- emptySpace-  _ <- aspO-  _ <- emptySpace-  fundecs <- Pc.many $ parseFunDec <* Pc.try emptySpace-  _ <- aspC-  _ <- emptySpace-  _ <- aspO-  _ <- emptySpace-  terms <- Pc.many $ parseTerm <* Pc.try emptySpace-  _ <- aspC-  _ <- emptySpace-  _ <- aspC-  return $ DefineFunsRec fundecs terms--parseFunDec :: ParsecT String u Identity FunDec-parseFunDec = do-  _ <- aspO-  _ <- emptySpace-  symb <- symbol-  _ <- emptySpace-  _ <- aspO-  _ <- emptySpace-  sVars <- Pc.many $ parseSortedVar <* Pc.try emptySpace-  _ <- aspC-  _ <- emptySpace-  sort <- parseSort-  _ <- emptySpace-  _ <- aspC-  return (FunDec symb sVars sort)---parsePush :: ParsecT String u Identity Command-parsePush = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "push"-  _ <- emptySpace-  nume <- option 1 $ do-    nume <- numeral-    _ <- emptySpace-    return (read nume :: Int)-  _ <- aspC-  return $ Push nume---parsePop :: ParsecT String u Identity Command-parsePop = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "pop"-  _ <- emptySpace-  nume <- option 1 $ do-    nume <- numeral-    _ <- emptySpace-    return (read nume :: Int)-  _ <- aspC-  return $ Pop nume----parseAssert :: ParsecT String u Identity Command-parseAssert = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "assert"-  _ <- emptySpace-  term <- parseTerm-  _ <- emptySpace-  _ <- aspC-  return $ Assert term---parseCheckSat :: ParsecT String u Identity Command-parseCheckSat = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "check-sat"-  _ <- emptySpace-  _ <- aspC-  return CheckSat--parseCheckSatAssuming :: ParsecT String u Identity Command-parseCheckSatAssuming = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "check-sat-assuming"-  _ <- emptySpace-  _ <- aspO-  emptySpace-  terms <- Pc.many $ parseTerm <* Pc.try emptySpace-  _ <- aspC-  _ <- emptySpace-  _ <- aspC-  return (CheckSatAssuming terms)---parseGetAssertions :: ParsecT String u Identity Command-parseGetAssertions = do-  _ <- aspO-  _ <-emptySpace-  _ <- string "get-assertions"-  _ <- emptySpace-  _ <- aspC-  return GetAssertions--parseGetModel :: ParsecT String u Identity Command-parseGetModel = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "get-model"-  _ <- emptySpace-  _ <-aspC-  return GetModel--parseGetProof :: ParsecT String u Identity Command-parseGetProof = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "get-proof"-  _ <- emptySpace-  _ <-aspC-  return GetProof--parseGetUnsatCore :: ParsecT String u Identity Command-parseGetUnsatCore = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "get-unsat-core"-  _ <- emptySpace-  _ <- aspC-  return GetUnsatCore--parseGetUnsatAssumptions :: ParsecT String u Identity Command-parseGetUnsatAssumptions = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "get-unsat-assumptions"-  _ <- emptySpace-  _ <- aspC-  return GetUnsatAssumptions--parseGetValue :: ParsecT String u Identity Command-parseGetValue = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "get-value"-  _ <- emptySpace-  _ <- aspO-  terms <- Pc.many1 $ parseTerm <* Pc.try emptySpace-  _ <- aspC-  _ <- emptySpace-  _ <- aspC-  return $ GetValue terms--parseGetAssignment :: ParsecT String u Identity Command-parseGetAssignment = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "get-assignment"-  _ <- emptySpace-  _ <- aspC-  return GetAssignment---parseGetOption :: ParsecT String u Identity Command-parseGetOption = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "get-option"-  _ <- emptySpace-  word <- keyword-  _ <- emptySpace-  _ <- aspC-  return $ GetOption word---parseGetInfo :: ParsecT String u Identity Command-parseGetInfo = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "get-info"-  _ <- emptySpace-  flag <- parseInfoFlags-  _ <- emptySpace-  _ <- aspC-  return $ GetInfo flag---parseEcho :: ParsecT String u Identity Command-parseEcho = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "echo"-  _ <- emptySpace-  s <- str-  _ <- emptySpace  -  _ <- aspC-  return $ Echo s---parseExit :: ParsecT String u Identity Command-parseExit = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "exit"-  _ <- emptySpace-  _ <- aspC-  return Exit---parseReset :: ParsecT String u Identity Command-parseReset = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "reset"-  _ <- emptySpace-  _ <- aspC-  return Reset---parseResetAssertions :: ParsecT String u Identity Command-parseResetAssertions = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "reset-assertions"-  _ <- emptySpace-  _ <- aspC-  return ResetAssertions---{--   #########################################################################-   #                                                                       #-   #                       Parse Command Options                           #-   #                                                                       #-   #########################################################################--}--parseOption :: ParsecT String u Identity Option-parseOption = Pc.try parsePrintSuccess-          <|> Pc.try parseExpandDefinitions-          <|> Pc.try parseInteractiveMode-          <|> Pc.try parseProduceProofs-          <|> Pc.try parseProduceUnsatCores-          <|> Pc.try parseProduceUnsatAssumptions-          <|> Pc.try parseProduceModels-          <|> Pc.try parseProduceAssignments-          <|> Pc.try parseProduceAssertions-          <|> Pc.try parseGlobalDeclarations-          <|> Pc.try parseRegularOutputChannel-          <|> Pc.try parseDiagnosticOutputChannel-          <|> Pc.try parseRandomSeed-          <|> Pc.try parseVerbosity-          <|> Pc.try parseReproducibleResourceLimit-          <|> Pc.try parseOptionAttribute----- parse PrintSucess-parsePrintSuccess :: ParsecT String u Identity Option-parsePrintSuccess = do-  _ <- string ":print-success"-  _ <- spaces-  val <- parseBool-  return $ PrintSuccess val---parseExpandDefinitions :: ParsecT String u Identity Option-parseExpandDefinitions = do-  _ <- string ":expand-definitions"-  _ <- spaces-  val <- parseBool-  return $ ExpandDefinitions val---parseInteractiveMode :: ParsecT String u Identity Option-parseInteractiveMode = do-  _ <- string ":interactive-mode"-  _ <- spaces-  val <- parseBool-  return $ InteractiveMode val--parseProduceProofs :: ParsecT String u Identity Option-parseProduceProofs = do-  _ <- string ":produce-proofs"-  _ <- spaces-  val <- parseBool-  return $ ProduceProofs val---parseProduceUnsatCores :: ParsecT String u Identity Option-parseProduceUnsatCores = do-  _ <- string ":produce-unsat-cores"-  _ <- spaces-  val <- parseBool-  return $ ProduceUnsatCores val--parseProduceUnsatAssumptions :: ParsecT String u Identity Option-parseProduceUnsatAssumptions = do-  _ <- string ":produce-unsat-assumptions"-  _ <- spaces-  val <- parseBool-  return $ ProduceUnsatAssumptions val--parseProduceModels :: ParsecT String u Identity Option-parseProduceModels = do-  _ <- string ":produce-models"-  _ <- spaces-  val <- parseBool-  return $ ProduceModels val--parseProduceAssignments :: ParsecT String u Identity Option-parseProduceAssignments = do-  _ <- string ":produce-assignments"-  _ <- spaces-  val <- parseBool-  return $ ProduceAssignments val--parseProduceAssertions :: ParsecT String u Identity Option-parseProduceAssertions = do-  _ <- string ":produce-assertions"-  _ <- spaces-  val <- parseBool-  return $ ProduceAssertions val--parseGlobalDeclarations :: ParsecT String u Identity Option-parseGlobalDeclarations = do-  _ <- string ":global-declarations"-  _ <- spaces-  val <- parseBool-  return $ GlobalDeclarations val---parseRegularOutputChannel :: ParsecT String u Identity Option-parseRegularOutputChannel = do-  _ <- string ":regular-output-channel"-  _ <- spaces-  val <- str-  return $ RegularOutputChannel val---parseDiagnosticOutputChannel :: ParsecT String u Identity Option-parseDiagnosticOutputChannel = do-  _ <- string ":diagnostic-output-channel"-  _ <- spaces-  val <- str-  return $ DiagnosticOutputChannel val--parseRandomSeed :: ParsecT String u Identity Option-parseRandomSeed = do-  _ <- string ":random-seed"-  _ <- spaces-  val <- numeral-  return $ RandomSeed (read val :: Int)---parseVerbosity :: ParsecT String u Identity Option-parseVerbosity = do-  _ <- string ":verbosity"-  _ <- spaces-  val <- numeral-  return $ Verbosity (read val :: Int)---parseReproducibleResourceLimit :: ParsecT String u Identity Option-parseReproducibleResourceLimit = do-  _ <- string ":reproducible-resource-limit"-  _ <- spaces-  val <- numeral-  return $ ReproducibleResourceLimit (read val :: Int)---parseOptionAttribute :: ParsecT String u Identity Option-parseOptionAttribute = do-  attr <- parseAttribute-  return $ OptionAttr attr-----{--   #########################################################################-   #                                                                       #-   #                       Parsers for Info FLags                          #-   #                                                                       #-   #########################################################################--}--parseInfoFlags :: ParsecT String u Identity InfoFlags-parseInfoFlags = Pc.try parseErrorBehaviour-             <|> Pc.try parseName-             <|> Pc.try parseAuthors-             <|> Pc.try parseVersion-             <|> Pc.try parseStatus-             <|> Pc.try parseReasonUnknown-             <|> Pc.try parseAllStatistics-             <|> Pc.try parseAssertionStackLevels-             <|> parseInfoKeyword---parseErrorBehaviour :: ParsecT String u Identity InfoFlags-parseErrorBehaviour = string ":error-behavior" *> return ErrorBehavior---parseName :: ParsecT String u Identity InfoFlags-parseName = string ":name" *> return Name--parseAuthors :: ParsecT String u Identity InfoFlags-parseAuthors = string ":authors" *> return Authors--parseVersion :: ParsecT String u Identity InfoFlags-parseVersion = string ":version" *> return Version--parseStatus :: ParsecT String u Identity InfoFlags-parseStatus = string ":status" *> return Status--parseReasonUnknown :: ParsecT String u Identity InfoFlags-parseReasonUnknown = string ":reason-unknown" *> return  ReasonUnknown--parseAllStatistics :: ParsecT String u Identity InfoFlags-parseAllStatistics = string ":all-statistics" *> return AllStatistics--parseAssertionStackLevels :: ParsecT String u Identity InfoFlags-parseAssertionStackLevels = string ":assertion-stack-levels" *> return AssertionStackLevels--parseInfoKeyword :: ParsecT String u Identity InfoFlags-parseInfoKeyword = liftM InfoFlags keyword

@@ -1,473 +0,0 @@-{-|-Module      : Smtlib.Parsers.CommandsParsers-Description : Common parsers for commands and responses.-Copyright   : Rogério Pontes 2015-License     : WTFPL-Maintainer  : rogerp62@outlook.com-Stability   : stable--This module contains some auxiliar parsers, used to parse commands or responses.--}-module Smtlib.Parsers.CommonParsers where---{--    In the String terminal, it does not parse C-style characters.-    Quoted Symbol does not parse all printable ASCII characters.--}--import           Control.Applicative               as Ctr hiding ((<|>))-import           Data.Functor.Identity-import qualified Data.Set                          as Set-import           Text.Parsec.Prim                  as Prim-import           Text.ParserCombinators.Parsec     as Pc-import           Smtlib.Syntax.Syntax-import           Control.Monad--(<:>) :: Applicative f => f a -> f [a] -> f [a]-(<:>) a b = (:) <$> a <*> b--(<++>) :: Applicative f => f [a] -> f [a] -> f [a]-(<++>) a b = (++) <$> a <*> b--parseBool :: ParsecT String u Identity Bool-parseBool = (true *> return True) <|> (false *> return False)----- Parse a Numeral--numeral :: ParsecT String u Identity String-numeral = many1 digit--num :: ParsecT String u Identity String-num = Pc.many digit--- Parse a decimal--decimal :: ParsecT String u Identity String-decimal = numeral <++> dot <++> Pc.try zeros <++> num--zeros :: ParsecT String u Identity String-zeros = Pc.many $ char '0'---dot :: ParsecT String u Identity String-dot = string "."---- parse a Hexadecimal--hexadecimal :: ParsecT String u Identity String-hexadecimal = string "#x" *> many1 hexDigit-----parsea a Binary-binary :: ParsecT String u Identity String-binary = string "#b" *> many1 bin--bin :: ParsecT String u Identity Char-bin = char '0' <|> char '1'-----parse a String--- Dosent parse strings with escape characters-str :: ParsecT String u Identity String-str = string "\"" <++> liftM concat (Pc.many (liftM (\c -> [c]) strChar <|> Pc.try (string "\"\""))) <++> string "\""--strChar :: ParsecT String u Identity Char-strChar = (oneOf $ ['\t','\n','\r'] ++ [c | c <- [toEnum 32 .. toEnum 126], c /= '"']) <|> satisfy (toEnum 128 <=)-----parse a Symbol-symbol :: ParsecT String u Identity String-symbol = symbol' reservedWordsSet--symbol' :: Set.Set String -> ParsecT String u Identity String-symbol' reserved = simpleSymbol' reserved <|> quotedSymbol--quotedSymbol :: ParsecT String u Identity String-quotedSymbol = char '|' *> Pc.many (noneOf "|")  <* char '|'--simpleSymbol :: ParsecT String u Identity String-simpleSymbol = simpleSymbol' reservedWordsSet--simpleSymbol' :: Set.Set String -> ParsecT String u Identity String-simpleSymbol' reserved = Pc.try $ do-  s <- (letter <|> spcSymb) <:>  sq-  guard $ s `Set.notMember` reserved-  return s-  where-    sq = Pc.many (alphaNum <|> spcSymb)--spcSymb :: ParsecT String u Identity Char-spcSymb = oneOf  "+-/*=%?!.$_~^&<>@"---- parse a key word-keyword :: ParsecT String u Identity String-keyword = char ':' <:> Pc.many (alphaNum<|> spcSymb)---aspO :: ParsecT String u Identity Char-aspO = char '('--aspC :: ParsecT String u Identity Char-aspC = char ')'--aspUS :: ParsecT String u Identity Char-aspUS = char '_'---true :: ParsecT String u Identity String-true = string "true"--false :: ParsecT String u Identity String-false = string "false"---emptySpace :: ParsecT String u Identity String-emptySpace = liftM concat $ Pc.try $ Pc.many emptySpaceSingle--emptySpace1 :: ParsecT String u Identity String-emptySpace1 = liftM concat $ Pc.try $ Pc.many1 emptySpaceSingle--emptySpaceSingle :: ParsecT String u Identity String-emptySpaceSingle = liftM (\c -> [c]) (char ' ' <|> char '\n' <|> char '\t' <|> char '\r') <|> comment--comment :: ParsecT String u Identity String-comment = char ';' <:> scan-  where-    scan  = do{ c <- char '\n' <|> char '\r'; return [c] }-          <|>-            do{ c <- anyChar; cs <- scan; return (c:cs) }--reservedWords :: ParsecT String u Identity String-reservedWords =  string "let"-             <|> string "par"-             <|> string "_"-             <|> string "!"-             <|> string "as"-             <|> string "forall"-             <|> string "exists"-             <|> string "NUMERAL"-             <|> string "DECIMAL"-             <|> string "STRING"-----{--   #########################################################################-   #                                                                       #-   #                          Parsers for Terms                            #-   #                                                                       #-   #########################################################################--}----- Term-parseTerm :: ParsecT String u Identity Term-parseTerm = parseTSPC-        <|> Pc.try parseTQID-        <|> Pc.try parseTQIT-        <|> Pc.try parseTermLet-        <|> Pc.try parseTermFA-        <|> Pc.try parseTermEX-        <|> parseTermAnnot--parseTSPC :: ParsecT String u Identity Term-parseTSPC = liftM TermSpecConstant parseSpecConstant--parseTQID :: ParsecT String u Identity Term-parseTQID = liftM TermQualIdentifier parseQualIdentifier--parseTQIT :: ParsecT String u Identity Term-parseTQIT = do-    _ <- aspO-    _ <- emptySpace-    iden <- parseQualIdentifier-    _ <- emptySpace-    terms <- Pc.many $ parseTerm <* Pc.try emptySpace-    _ <- aspC-    return $ TermQualIdentifierT iden terms--parseTermLet :: ParsecT String u Identity Term-parseTermLet = do-    _ <- aspO-    _ <- emptySpace-    _ <- string "let"-    _ <- emptySpace-    _ <- aspO-    _ <- emptySpace-    vb <- Pc.many $ parseVarBinding <* Pc.try emptySpace-    _ <- aspC-    _ <- emptySpace-    term <- parseTerm-    _ <- emptySpace-    _ <- aspC-    return $ TermLet vb term--parseTermFA :: ParsecT String u Identity Term-parseTermFA = do-    _ <- aspO-    _ <- emptySpace-    _ <- string "forall"-    _ <- emptySpace-    _ <- aspO-    sv <- Pc.many $ parseSortedVar <* Pc.try emptySpace-    _ <- aspC-    _ <- emptySpace-    term <- parseTerm-    _ <- emptySpace-    _ <- aspC-    return $ TermForall sv term---parseTermEX :: ParsecT String u Identity Term-parseTermEX = do-    _ <- aspO-    _ <- emptySpace-    _ <- string "exists"-    _ <- emptySpace-    _ <- aspO-    sv <- Pc.many $ parseSortedVar <* Pc.try emptySpace-    _ <- aspC-    _ <- emptySpace-    term <- parseTerm-    _ <- emptySpace-    _ <- aspC-    return $ TermExists sv term--parseTermAnnot :: ParsecT String u Identity Term-parseTermAnnot = do-  _ <- aspO-  _ <- emptySpace-  _ <- char '!'-  _ <- emptySpace-  term <- parseTerm-  _ <- emptySpace-  attr <- Pc.many $ parseAttribute <* Pc.try emptySpace-  _ <- aspC-  return $ TermAnnot term attr----- -- Parse Sorted Var-parseSortedVar :: ParsecT String u Identity SortedVar-parseSortedVar = do-    _ <- aspO-    _ <- emptySpace-    symb <- symbol-    _ <- emptySpace-    sort <- parseSort-    _ <- emptySpace-    _ <- aspC-    return $ SV symb sort---- -- Parse Qual identifier-parseQualIdentifier :: ParsecT String u Identity QualIdentifier-parseQualIdentifier = Pc.try parseQID <|> parseQIAs--parseQID :: ParsecT String u Identity QualIdentifier-parseQID = liftM QIdentifier parseIdentifier-----parseQIAs :: ParsecT String u Identity QualIdentifier-parseQIAs = do-  _ <- aspO-  _ <- emptySpace-  _ <- string "as"-  _ <- emptySpace1-  ident <- parseIdentifier-  _ <- emptySpace-  sort <- parseSort-  _ <- emptySpace-  _ <- aspC-  return $ QIdentifierAs ident sort----- -- Parse Var Binding-parseVarBinding :: ParsecT String u Identity VarBinding-parseVarBinding = do-    _ <- aspO-    _ <- emptySpace-    symb <- symbol-    _ <- emptySpace-    term <- parseTerm-    _ <- emptySpace-    _ <- aspC-    return $ VB symb term------{--   #########################################################################-   #                                                                       #-   #                          Parsers for Attributes                       #-   #                                                                       #-   #########################################################################--}----Parse Attribute Value-parseAttributeValue :: ParsecT String u Identity AttrValue-parseAttributeValue = parseAVSC <|> parseAVS <|> parseAVSexpr--parseAVSC :: ParsecT String u Identity AttrValue-parseAVSC = liftM AttrValueConstant parseSpecConstant--parseAVS :: ParsecT String u Identity AttrValue-parseAVS = liftM AttrValueSymbol symbol--parseAVSexpr :: ParsecT String u Identity AttrValue-parseAVSexpr = do-    _ <- aspO-    _ <- emptySpace-    expr <- Pc.many $ parseSexpr <* Pc.try emptySpace-    _ <- aspC-    return $ AttrValueSexpr expr------ Parse Attribute--parseAttribute :: ParsecT String u Identity Attribute-parseAttribute =  Pc.try parseKeyAttAttribute <|> parseKeyAttribute---parseKeyAttribute :: ParsecT String u Identity Attribute-parseKeyAttribute = liftM  Attribute keyword--parseKeyAttAttribute :: ParsecT String u Identity Attribute-parseKeyAttAttribute = do-  kw <- keyword-  _ <- emptySpace-  atr <- parseAttributeValue-  return $ AttributeVal kw atr---{--   #########################################################################-   #                                                                       #-   #                          Parsers Sort                                 #-   #                                                                       #-   #########################################################################--}---- Parse Sot--parseSort :: ParsecT String u Identity Sort-parseSort = Pc.try parseIdentifierS <|> parseIdentifierSort--parseIdentifierS :: ParsecT String u Identity Sort-parseIdentifierS = liftM SortId parseIdentifier--parseIdentifierSort :: ParsecT String u Identity Sort-parseIdentifierSort = do-    _ <- aspO-    _ <- emptySpace-    identifier <- parseIdentifier-    _ <- emptySpace-    sorts <- many1 (parseSort  <* Pc.try emptySpace)-    _ <- aspC-    return $ SortIdentifiers identifier sorts-----{--   #########################################################################-   #                                                                       #-   #                          Parsers Identifiers                          #-   #                                                                       #-   #########################################################################--}----- Parse Identifiers--parseIdentifier :: ParsecT String u Identity Identifier-parseIdentifier = parseOnlySymbol <|> parseNSymbol--parseOnlySymbol :: ParsecT String u Identity Identifier-parseOnlySymbol = liftM ISymbol symbol--parseNSymbol :: ParsecT String u Identity Identifier-parseNSymbol = do-       _ <- aspO-       _ <- emptySpace-       _ <- aspUS-       _ <- emptySpace1-       symb <- symbol-       _ <- emptySpace-       indexes <- many1 ((liftM (IndexNumeral . read) numeral <|> liftM IndexSymbol symbol) <* Pc.try spaces)-       _ <- aspC-       return $ I_Symbol symb indexes--{--   #########################################################################-   #                                                                       #-   #                          Parsers S-exprs                              #-   #                                                                       #-   #########################################################################--}----- parse S-expressions--parseSexprConstant :: ParsecT String u Identity Sexpr-parseSexprConstant = liftM SexprSpecConstant parseSpecConstant--parseSexprSymbol :: ParsecT String u Identity Sexpr-parseSexprSymbol = liftM SexprSymbol (symbol' Set.empty)--parseSexprKeyword :: ParsecT String u Identity Sexpr-parseSexprKeyword = liftM SexprKeyword keyword--parseAtomSexpr :: ParsecT String u Identity Sexpr-parseAtomSexpr = parseSexprConstant-          <|> parseSexprSymbol-          <|> parseSexprKeyword---parseListSexpr :: ParsecT String u Identity Sexpr-parseListSexpr = do-    _ <- aspO-    list <- Pc.many parseSexpr-    _ <- aspC-    return $ SexprSxp  list----parseSexpr :: ParsecT String u Identity Sexpr-parseSexpr = do-  _ <- emptySpace-  expr <- parseAtomSexpr <|> parseListSexpr-  _ <- emptySpace-  return expr------ parse Spec Constant-parseSpecConstant :: ParsecT String u Identity SpecConstant-parseSpecConstant = Pc.try parseDecimal-                <|> parseNumeral-                <|> Pc.try parseHexadecimal-                <|> parseBinary-                <|> parseString----parseNumeral :: ParsecT String u Identity SpecConstant-parseNumeral = liftM SpecConstantNumeral (read  <$> numeral)--parseDecimal :: ParsecT String u Identity SpecConstant-parseDecimal = liftM SpecConstantDecimal decimal--parseHexadecimal :: ParsecT String u Identity SpecConstant-parseHexadecimal = liftM SpecConstantHexadecimal hexadecimal--parseBinary :: ParsecT String u Identity SpecConstant-parseBinary = liftM SpecConstantBinary binary--parseString :: ParsecT String u Identity SpecConstant-parseString = liftM SpecConstantString str

@@ -1,375 +0,0 @@-{-|-Module      : Smtlib.Parsers.ResponseParsers-Description : Parsers for Smtlib commands response.-Copyright   : Rogério Pontes 2015-License     : WTFPL-Maintainer  : rogerp62@outlook.com-Stability   : stable--This module contains all the required individual parsers for each reasponse to -a Smtlib command, plus one parser to parse every result, parseCmdResult.---}--module Smtlib.Parsers.ResponseParsers where--import           Control.Applicative           as Ctr hiding ((<|>))-import           Control.Monad-import           Data.Functor.Identity-import           Smtlib.Parsers.CommonParsers-import           Smtlib.Parsers.CommandsParsers-import           Smtlib.Syntax.Syntax        as CmdRsp-import           Text.Parsec.Prim              as Prim-import           Text.ParserCombinators.Parsec as Pc----parseCmdResult :: ParsecT String u Identity CmdResponse-parseCmdResult = Pc.try parseCmdGenResponse-             <|> Pc.try parseCmdCheckSatResponse-             <|> Pc.try parseCmdGetInfoResponse-             <|> Pc.try parseCmdGetAssertions-             <|> Pc.try parseCmdGetAssignment-             <|> Pc.try parseCmdGetProof-             <|> Pc.try parseCmdGetProof-             <|> Pc.try parseCmdGetValueResponse-             <|> Pc.try parseCmdGetModelResponse-             <|> Pc.try parseCmdGetOptionResponse-             <|> Pc.try parseCmdEchoResponse--{--   #########################################################################-   #                                                                       #-   #                       Parser Cmd Gen Response                         #-   #                                                                       #-   #########################################################################--}--parseCmdGenResponse :: ParsecT String u Identity CmdResponse-parseCmdGenResponse = liftM CmdGenResponse parseGenResponse--parseGenResponse :: ParsecT String u Identity GenResponse-parseGenResponse =  parseUnsupported <|> parseSuccess <|> parseGenError--parseSuccess :: ParsecT String u Identity GenResponse-parseSuccess = string "success" *> return Success--parseUnsupported :: ParsecT String u Identity GenResponse-parseUnsupported = string "unsupported" *> return Unsupported---parseGenError :: ParsecT String u Identity GenResponse-parseGenError = do-    _ <- aspO-    _ <- emptySpace-    _ <- string "error"-    _ <- emptySpace-    err <- str-    _ <- emptySpace-    _ <- aspC-    return $ CmdRsp.Error err-------{--   #########################################################################-   #                                                                       #-   #                       Parser get info response                        #-   #                                                                       #-   #########################################################################--}--parseCmdGetInfoResponse :: ParsecT String u Identity CmdResponse-parseCmdGetInfoResponse = liftM CmdGetInfoResponse parseGetInfoResponse---parseGetInfoResponse :: ParsecT String u Identity [InfoResponse]-parseGetInfoResponse = do-    _ <-aspO-    _ <- emptySpace-    infoResp <- Pc.many $ parseInfoResponse <* Pc.try emptySpace-    _ <- aspC-    return infoResp----parseInfoResponse :: ParsecT String u Identity InfoResponse-parseInfoResponse =-    Pc.try parseResponseName <|>-    Pc.try parseResponseErrorBehavior <|>-    Pc.try parseResponseAuthors <|>-    Pc.try parseResponseVersion <|>-    Pc.try parseResponseReasonUnknown <|>-    Pc.try parseResponseAssertionStackLevels <|>-    parseResponseAttribute-----parseResponseName :: ParsecT String u Identity InfoResponse-parseResponseName = string ":name"  *> emptySpace *> liftM ResponseName str---parseResponseErrorBehavior :: ParsecT String u Identity InfoResponse-parseResponseErrorBehavior = string ":error-behavior" *> emptySpace *>-                    liftM ResponseErrorBehavior parseErrorBehavior--parseErrorBehavior :: ParsecT String u Identity ErrorBehavior-parseErrorBehavior =-    (string "immediate-exit" >> return ImmediateExit) <|>-    (string "continued-execution" >> return ContinuedExecution)---parseResponseAuthors :: ParsecT String u Identity InfoResponse-parseResponseAuthors = string ":authors" *> emptySpace *>-    liftM ResponseAuthors str--parseResponseVersion :: ParsecT String u Identity InfoResponse-parseResponseVersion = string ":version" *> emptySpace *>-     liftM ResponseVersion str----parseResponseReasonUnknown :: ParsecT String u Identity InfoResponse-parseResponseReasonUnknown = string ":reason-unknown" *> emptySpace *>-    liftM ResponseReasonUnknown parseRReasonUnknown--parseRReasonUnknown :: ParsecT String u Identity ReasonUnknown-parseRReasonUnknown =-    (string "memout" >> return Memout) <|>-    (string "incomplete" >> return Incomplete)--parseResponseAssertionStackLevels :: ParsecT String u Identity InfoResponse-parseResponseAssertionStackLevels =-  string ":assertion-stack-levels" *> emptySpace *>-    liftM ResponseAssertionStackLevels (liftM read numeral)---parseResponseAttribute :: ParsecT String u Identity InfoResponse-parseResponseAttribute = liftM ResponseAttribute parseAttribute--------{--   #########################################################################-   #                                                                       #-   #                       Parser check sat response                       #-   #                                                                       #-   #########################################################################--}----parseCmdCheckSatResponse :: ParsecT String u Identity CmdResponse-parseCmdCheckSatResponse = liftM  CmdCheckSatResponse parseCheckSatResponse------ Parser for check sat response-parseCheckSatResponse :: ParsecT String u Identity CheckSatResponse-parseCheckSatResponse =-    (string "sat" >> return Sat) <|>-    Pc.try (string "unsat" >> return Unsat) <|>-    (string "unknown" >> return Unknown)-----{--   #########################################################################-   #                                                                       #-   #                       Parser get assertions cmd                       #-   #                                                                       #-   #########################################################################--}---parseCmdGetAssertions :: ParsecT String u Identity CmdResponse-parseCmdGetAssertions =-  liftM CmdGetAssertionsResponse parseGetAssertionsResponse------ parse Get Assertion Response-parseGetAssertionsResponse :: ParsecT String u Identity [Term]-parseGetAssertionsResponse = do-    _ <- aspO-    _ <- emptySpace-    terms <- Pc.many $ parseTerm <* Pc.try emptySpace-    _ <- aspC-    return terms--{--   #########################################################################-   #                                                                       #-   #                       Parser get proof response                       #-   #                                                                       #-   #########################################################################--}---parseCmdGetProof :: ParsecT String u Identity CmdResponse-parseCmdGetProof = liftM CmdGetProofResponse parseGetProofResponse---- parse Get Proof response-parseGetProofResponse :: ParsecT String u Identity Sexpr-parseGetProofResponse = parseSexpr----{--   #########################################################################-   #                                                                       #-   #                       Parser get unsat core response                  #-   #                                                                       #-   #########################################################################--}---parseCmdGetUnsatCore :: ParsecT String u Identity CmdResponse-parseCmdGetUnsatCore =  liftM CmdGetUnsatCoreResponse parseGetUnsatCoreResp----- parse Get unsat core response-parseGetUnsatCoreResp :: ParsecT String u Identity [String]-parseGetUnsatCoreResp = do-    _ <- aspO-    _ <- emptySpace-    symb <- Pc.many $ symbol <* Pc.try emptySpace-    _ <- aspC-    return symb---{--   #########################################################################-   #                                                                       #-   #                       Parser Cmd Get value response                   #-   #                                                                       #-   #########################################################################--}---parseCmdGetValueResponse :: ParsecT String u Identity CmdResponse-parseCmdGetValueResponse = liftM CmdGetValueResponse parseGetValueResponse------ parse Get Value response-parseGetValueResponse :: ParsecT String u Identity [ValuationPair]-parseGetValueResponse =-    aspO *> (Pc.many $ parseValuationPair <* Pc.try emptySpace) <* aspC--parseValuationPair :: ParsecT String u Identity ValuationPair-parseValuationPair = do-    _ <- aspO-    _ <- emptySpace-    term1 <- parseTerm-    _ <- emptySpace-    term2 <- parseTerm-    _ <- emptySpace-    _ <- aspC-    return $ ValuationPair term1 term2---{--   #########################################################################-   #                                                                       #-   #                       Parser Cmd get assignment Resp                  #-   #                                                                       #-   #########################################################################--}---parseCmdGetAssignment :: ParsecT String u Identity CmdResponse-parseCmdGetAssignment = liftM CmdGetAssignmentResponse parseGetAssignmentResp---- parse get Assignent Response-parseGetAssignmentResp :: ParsecT String u Identity [TValuationPair]-parseGetAssignmentResp = do-    _ <- aspO-    _ <- emptySpace-    pairs <- Pc.many $ parseTValuationPair <* Pc.try emptySpace-    _ <- aspC-    return pairs---- parse t valuation pair-parseTValuationPair :: ParsecT String u Identity TValuationPair-parseTValuationPair = do-    _ <- aspO-    _ <- emptySpace-    symb <- symbol-    _ <- emptySpace-    bval <- parseBool-    _ <- emptySpace-    _ <-aspC-    return $ TValuationPair symb bval---{--   #########################################################################-   #                                                                       #-   #                       Parser Cmd Get model response                   #-   #                                                                       #-   #########################################################################--}---parseCmdGetModelResponse :: ParsecT String u Identity CmdResponse-parseCmdGetModelResponse = liftM CmdGetModelResponse parseGetModelResponse------ parse Get Model response-parseGetModelResponse :: ParsecT String u Identity [Command]-parseGetModelResponse =-    aspO *> (Pc.many $ parseCommand <* Pc.try emptySpace) <* aspC---{--   #########################################################################-   #                                                                       #-   #                       Parser Cmd get option response                  #-   #                                                                       #-   #########################################################################--}---parseCmdGetOptionResponse :: ParsecT String u Identity CmdResponse-parseCmdGetOptionResponse = liftM CmdGetOptionResponse parseGetOptionResponse----- parse Get Option Response-parseGetOptionResponse :: ParsecT String u Identity AttrValue-parseGetOptionResponse = parseAttributeValue--{--   #########################################################################-   #                                                                       #-   #                       Parser Cmd get option response                  #-   #                                                                       #-   #########################################################################--}---parseCmdEchoResponse :: ParsecT String u Identity CmdResponse-parseCmdEchoResponse = liftM CmdEchoResponse parseEchoResponse----- parse Echo Response-parseEchoResponse :: ParsecT String u Identity EchoResponse-parseEchoResponse = str--{--   #########################################################################-   #                                                                       #-   #                       Parser check-sat Alterg'os response             #-   #                                                                       #-   #########################################################################--}

@@ -1,247 +0,0 @@-{-|-Module      : Smtlib.Syntax.ShowSL-Description : Instance to print the syntax.-Copyright   : Rogério Pontes 2015-License     : WTFPL-Maintainer  : rogerp62@outlook.com-Stability   : stable--Functions to print the syntax as a SMTLib.---}-module Smtlib.Syntax.ShowSL where--import           Data.Char-import qualified Data.Set as Set-import           Data.List-import           Smtlib.Syntax.Syntax------joinA ::(ShowSL a) => [a] -> String-joinA = unwords.fmap showSL--joinNs :: [Int] -> String-joinNs = unwords.fmap show--showSymbol :: String -> String-showSymbol = showSymbol' reservedWordsSet--showSymbol' :: Set.Set String -> String -> String-showSymbol' reserved s-  | c:_ <- s, isDigit c = quoted-  | all p s && s `Set.notMember` reserved = s-  | otherwise = quoted-  where-    quoted = "|" ++ s ++ "|"-    p c = (isAscii c && isAlpha c) || isDigit c || c `elem` "~!@$%^&*_-+=<>.?/"--class ShowSL a where-  showSL :: a -> String----{--   #########################################################################-   #                                                                       #-   #                       ShowSL for an SMTLib2 File                      #-   #                                                                       #-   #########################################################################--}---instance ShowSL Command where-  showSL (SetLogic s) = "(set-logic " ++ showSymbol s ++ ")"-  showSL (SetOption opt) = "(set-option " ++ showSL opt ++ ")"-  showSL (SetInfo info) = "(set-info " ++ showSL info ++ ")"-  showSL (DeclareSort str val) =  "(declare-sort " ++ showSymbol str ++-    " " ++ show val ++ ")"-  showSL (DefineSort str strs sort) = "(define-sort " ++ showSymbol str ++-    " (" ++ unwords (map showSymbol strs) ++ ") " ++ showSL sort ++ ") "-  showSL (DeclareConst str sort) = "(declare-const  " ++ showSymbol str ++-    " " ++ showSL sort ++ ") "-  showSL (DeclareFun  str sorts sort) = "(declare-fun  " ++ showSymbol str ++-    " ("  ++ joinA sorts ++ ") " ++ showSL sort ++ ") "-  showSL (DefineFun str srvs sort term) = "(define-fun "   ++ showSymbol str ++-    " (" ++ joinA srvs ++ ") " ++ showSL sort ++ " " ++ showSL term ++ ")"-  showSL (DefineFunRec str srvs sort term) = "(define-fun-rec "   ++ showSymbol str ++-    " (" ++ joinA srvs ++ ") " ++ showSL sort ++ " " ++ showSL term ++ ")"-  showSL (DefineFunsRec fundecs terms) = "(define-funs-rec " ++-    " (" ++ joinA fundecs ++ ") (" ++ joinA terms ++ "))"-  showSL (Push n) = "(push " ++ show n ++ ")"-  showSL (Pop n) = "(pop " ++show n ++ ")"-  showSL (Assert term) = "(assert " ++ showSL term ++ ")"-  showSL CheckSat = "(check-sat)"-  showSL (CheckSatAssuming terms) = "(check-sat-assuming (" ++ joinA terms ++ "))"-  showSL GetAssertions = "(get-assertions)"-  showSL GetModel = "(get-model)"-  showSL GetProof = "(get-proof)"-  showSL GetUnsatCore = "(get-unsat-core)"-  showSL GetUnsatAssumptions = "(get-unsat-assumptions)"-  showSL (GetValue terms) = "(get-value (" ++ joinA terms ++ "))"-  showSL GetAssignment =  "(get-assignment)"-  showSL (GetOption opt) = "(get-option " ++ opt ++ ")"-  showSL (GetInfo info) = "(get-info " ++ showSL info ++ ")"-  showSL Reset = "(reset)"-  showSL ResetAssertions = "(reset-assertions)"-  showSL (Echo str) = "(echo " ++ str ++ ")"-  showSL Exit = "(exit)"---instance ShowSL Bool where-  showSL True = "true"-  showSL False = "false"--instance ShowSL Option where-  showSL (PrintSuccess b) = ":print-success " ++ showSL b-  showSL (ExpandDefinitions b) = ":expand-definitions " ++ showSL b-  showSL (InteractiveMode b) = ":interactive-mode " ++ showSL b-  showSL (ProduceProofs b) = ":produce-proofs " ++ showSL b-  showSL (ProduceUnsatCores b) = ":produce-unsat-cores " ++  showSL b-  showSL (ProduceUnsatAssumptions b) = ":produce-unsat-assumptions " ++  showSL b-  showSL (ProduceModels b) = ":produce-models " ++ showSL b-  showSL (ProduceAssignments b) = ":produce-assignments " ++ showSL b-  showSL (ProduceAssertions b) = ":produce-assertions " ++ showSL b-  showSL (GlobalDeclarations b) = ":global-declarations " ++ showSL b-  showSL (RegularOutputChannel s) = ":regular-output-channel " ++ s-  showSL (DiagnosticOutputChannel s) = ":diagnostic-output-channel " ++ s-  showSL (RandomSeed n) = ":random-seed " ++ show n-  showSL (Verbosity n) = ":verbosity " ++ show n-  showSL (ReproducibleResourceLimit n) = ":reproducible-resource-limit " ++ show n-  showSL (OptionAttr attr) = showSL attr--instance ShowSL InfoFlags where-  showSL ErrorBehavior = ":error-behavior"-  showSL Name = ":name"-  showSL Authors = ":authors"-  showSL Version = ":version"-  showSL Status = ":status"-  showSL ReasonUnknown = ":reason-unknown"-  showSL AllStatistics = ":all-statistics"-  showSL AssertionStackLevels = ":assertion-stack-levels"-  showSL (InfoFlags s) = s---instance ShowSL Term where-  showSL (TermSpecConstant sc) = showSL sc-  showSL (TermQualIdentifier qi) = showSL qi-  showSL (TermQualIdentifierT qi terms) =-    "(" ++ showSL qi ++ " " ++ joinA terms ++ ")"-  showSL (TermLet vb term) =-    "(let (" ++ joinA vb ++ ") " ++ showSL term ++ ")"-  showSL (TermForall svs term) =-    "(forall (" ++ joinA svs ++ " ) " ++ showSL term ++ ")"-  showSL (TermExists svs term) =-    "(exists (" ++ joinA svs ++ " ) " ++ showSL term ++ ")"-  showSL (TermAnnot term atts) =-    "(! " ++ showSL term ++ " " ++ joinA atts ++ ")"--instance ShowSL VarBinding where-  showSL (VB str term) = "("++ showSymbol str ++ " " ++ showSL term ++ ")"--instance ShowSL SortedVar where-  showSL (SV str sort)  = "(" ++ showSymbol str ++ " " ++ showSL sort ++ ")"--instance ShowSL QualIdentifier where-  showSL (QIdentifier iden) = showSL iden-  showSL (QIdentifierAs iden sort) =-    "(as " ++ showSL iden ++ " " ++ showSL sort ++ ")"--instance ShowSL FunDec where-  showSL (FunDec str srvs sort) =-    "(" ++ showSymbol str ++ " (" ++ joinA srvs ++ ") " ++ showSL sort ++ ")"--instance ShowSL AttrValue where-  showSL (AttrValueConstant spc) = showSL spc-  showSL (AttrValueSymbol str) = showSymbol str-  showSL (AttrValueSexpr sexprs) = "(" ++ joinA sexprs  ++ ")"--instance ShowSL Attribute where-  showSL (Attribute str) = str-  showSL (AttributeVal str attrVal) = str ++ " " ++ showSL attrVal--instance ShowSL Index where-  showSL (IndexNumeral i) = show i-  showSL (IndexSymbol str) = showSymbol str--instance ShowSL Identifier where-  showSL (ISymbol str) = showSymbol str-  showSL (I_Symbol str is) = "(_ " ++ showSymbol str ++ " " ++ joinA is  ++ ")"--instance ShowSL Sort where-  showSL (SortId iden) = showSL iden-  showSL (SortIdentifiers iden sorts) =-    "(" ++ showSL iden ++ " " ++ joinA sorts ++ ")"--instance ShowSL SpecConstant where-  showSL (SpecConstantNumeral n) = show n-  showSL (SpecConstantDecimal str) = str-  showSL (SpecConstantHexadecimal str) = "#x" ++ str-  showSL (SpecConstantBinary str)  = "#b" ++ str-  showSL (SpecConstantString str) = str--instance ShowSL Sexpr where-  showSL (SexprSpecConstant sc) = showSL sc-  showSL (SexprSymbol str) = showSymbol' Set.empty str-  showSL (SexprKeyword str) = str-  showSL (SexprSxp srps) = "(" ++ joinA srps ++ ")"---{--   #########################################################################-   #                                                                       #-   #                             Command Response                          #-   #                                                                       #-   #########################################################################--}--instance ShowSL CmdResponse where-  showSL (CmdGenResponse x) = showSL x-  showSL (CmdGetInfoResponse x) = "(" ++ joinA x ++ ")"-  showSL (CmdCheckSatResponse x) = showSL x-  showSL (CmdGetAssertionsResponse x) = "(" ++ joinA x ++ ")"-  showSL (CmdGetAssignmentResponse x) = "(" ++ joinA x ++ ")"-  showSL (CmdGetProofResponse x) = showSL x-  showSL (CmdGetUnsatCoreResponse x) = "(" ++ unwords (map showSymbol x) ++ ")"-  showSL (CmdGetUnsatAssumptionsResponse terms) = "(" ++  joinA terms ++ ")"-  showSL (CmdGetValueResponse x) = "(" ++ joinA x ++ ")"-  showSL (CmdGetModelResponse cmds) = "(" ++ joinA cmds ++ ")"-  showSL (CmdGetOptionResponse x) = showSL x-  showSL (CmdEchoResponse x) = x---instance ShowSL GenResponse where-  showSL Unsupported = "unsupported"-  showSL Success = "success"-  showSL (Error s) = "(error " ++ s ++ ")"--instance ShowSL ErrorBehavior where-  showSL ImmediateExit = "immediate-exit"-  showSL ContinuedExecution = "continued-execution"--instance ShowSL ReasonUnknown where-  showSL Memout = "memout"-  showSL Incomplete = "incomplete"--instance ShowSL CheckSatResponse where-  showSL Sat = "sat"-  showSL Unsat = "unsat"-  showSL Unknown = "unknown"--instance ShowSL InfoResponse where-  showSL (ResponseErrorBehavior x) = ":error-behavior " ++ showSL x-  showSL (ResponseName s) = ":name " ++ s-  showSL (ResponseAuthors s) = ":authors " ++ s-  showSL (ResponseVersion s) = ":version" ++ s-  showSL (ResponseReasonUnknown x) = ":reason-unknown " ++ showSL x-  showSL (ResponseAssertionStackLevels n) = ":assertion-stack-levels " ++ show n-  showSL (ResponseAttribute x)  = showSL x--instance ShowSL ValuationPair where-  showSL (ValuationPair term1 term2) =-    "(" ++ showSL term1 ++ " " ++ showSL term2 ++ ")"--instance ShowSL TValuationPair where-  showSL (TValuationPair str b) = "(" ++ showSymbol str ++ " " ++ showSL b ++ ")"

@@ -1,279 +0,0 @@-{-|-Module      : Smtlib.Parsers.CommandsParsers-Description : Smtlib Syntax-Copyright   : Rogério Pontes 2015-License     : WTFPL-Maintainer  : rogerp62@outlook.com-Stability   : stable--This module contains The syntax to create commands and responses.---}-module Smtlib.Syntax.Syntax where--import qualified Data.Set as Set--{--   #########################################################################-   #                                                                       #-   #                       Parser for an SMTLib2 File                      #-   #                                                                       #-   #########################################################################--}--reservedWordsSet :: Set.Set String-reservedWordsSet =  Set.fromList $-  ["BINARY", "DECIMAL", "HEXADECIMAL", "NUMERAL", "STRING", "_", "!", "as", "let", "exists", "forall", "par"] ++-  ["set-logic", "set-option", "set-info", "declare-sort", "define-sort", "declare-const", "declare-fun", "declare-fun-rec", "declare-funs-rec", "push", "pop", "reset", "reset-assertions", "assert", "check-sat", "check-sat-assuming", "get-assertions", "get-model", "get-proof", "get-unsat-core", "get-unsat-assumptions", "get-value", "get-assignment", "get-option", "get-info", "echo", "exit"]---type Source = [Command]---data Command = SetLogic String-             | SetOption Option-             | SetInfo Attribute-             | DeclareSort String Int-             | DefineSort String [String] Sort-             | DeclareConst String Sort-             | DeclareFun String [Sort] Sort-             | DefineFun String [SortedVar] Sort Term-             | DefineFunRec String [SortedVar] Sort Term-             | DefineFunsRec [FunDec] [Term]-             | Push Int-             | Pop Int-             | Reset-             | ResetAssertions-             | Assert Term-             | CheckSat-             | CheckSatAssuming [Term]-             | GetAssertions-             | GetModel-             | GetProof-             | GetUnsatCore-             | GetUnsatAssumptions-             | GetValue [Term]-             | GetAssignment-             | GetOption String-             | GetInfo InfoFlags-             | Echo String-             | Exit-             deriving (Show,Eq)--data Option = PrintSuccess Bool-            | ExpandDefinitions Bool-            | InteractiveMode Bool-            | ProduceProofs Bool-            | ProduceUnsatCores Bool-            | ProduceUnsatAssumptions Bool-            | ProduceModels Bool-            | ProduceAssignments Bool-            | ProduceAssertions Bool-            | GlobalDeclarations Bool-            | RegularOutputChannel String-            | DiagnosticOutputChannel String-            | RandomSeed Int-            | Verbosity Int-            | ReproducibleResourceLimit Int -- fixme-            | OptionAttr Attribute-             deriving (Show,Eq)---data InfoFlags = ErrorBehavior-               | Name-               | Authors-               | Version-               | Status-               | ReasonUnknown-               | AllStatistics-               | AssertionStackLevels-               | InfoFlags String-                deriving (Show,Eq)---- Terms--data Term = TermSpecConstant SpecConstant-          | TermQualIdentifier QualIdentifier-          | TermQualIdentifierT  QualIdentifier [Term]-          | TermLet [VarBinding] Term-          | TermForall [SortedVar] Term-          | TermExists [SortedVar] Term-          | TermAnnot Term [Attribute]-          deriving (Show,Eq)----data VarBinding = VB String Term deriving (Show,Eq)----data SortedVar = SV String Sort deriving (Show,Eq)----data QualIdentifier = QIdentifier Identifier-                    | QIdentifierAs Identifier Sort-                    deriving (Show,Eq)---data FunDec = FunDec String [SortedVar] Sort deriving (Show,Eq)-------- Attributes--data AttrValue = AttrValueConstant SpecConstant-               | AttrValueSymbol String-               | AttrValueSexpr [Sexpr]-               deriving (Show,Eq)----data Attribute = Attribute String-               | AttributeVal String AttrValue-               deriving (Show,Eq)---- Identifiers--data Index = IndexNumeral Int-           | IndexSymbol String-           deriving (Show,Eq)--data Identifier = ISymbol String-                | I_Symbol String [Index] deriving (Show,Eq)---- Sorts--data Sort = SortId Identifier | SortIdentifiers Identifier [Sort]-            deriving (Show,Eq)----- S-expressions-data SpecConstant = SpecConstantNumeral Integer-                  | SpecConstantDecimal String-                  | SpecConstantHexadecimal String-                  | SpecConstantBinary String-                  | SpecConstantString String-                  deriving (Show, Eq)----data Sexpr = SexprSpecConstant SpecConstant-           | SexprSymbol String-           | SexprKeyword String-           | SexprSxp [Sexpr]-           deriving (Show, Eq)----------{--   #########################################################################-   #                                                                       #-   #                             Command Response                          #-   #                                                                       #-   #########################################################################--}------ CmdResponse--data CmdResponse = CmdGenResponse GenResponse-                 | CmdGetInfoResponse GetInfoResponse-                 | CmdCheckSatResponse CheckSatResponse-                 | CmdGetAssertionsResponse  GetAssertionsResponse-                 | CmdGetAssignmentResponse GetAssignmentResponse-                 | CmdGetProofResponse GetProofResponse-                 | CmdGetUnsatCoreResponse GetUnsatCoreResponse-                 | CmdGetUnsatAssumptionsResponse GetUnsatAssumptionsResponse-                 | CmdGetValueResponse GetValueResponse-                 | CmdGetModelResponse GetModelResponse-                 | CmdGetOptionResponse GetOptionResponse-                 | CmdEchoResponse EchoResponse-                 deriving (Show, Eq)----- Command Responses----- Gen Response--data GenResponse =  Unsupported |  Success | Error String deriving (Show, Eq)----- Error behavior--data ErrorBehavior = ImmediateExit | ContinuedExecution deriving (Show, Eq)----- Reason unknown--data ReasonUnknown = Memout | Incomplete deriving (Show, Eq)---- Status--data CheckSatResponse = Sat | Unsat | Unknown deriving (Show, Eq)---- Info Response--type GetInfoResponse = [InfoResponse]--data InfoResponse  = ResponseErrorBehavior ErrorBehavior-                   | ResponseName String-                   | ResponseAuthors String-                   | ResponseVersion String-                   | ResponseReasonUnknown ReasonUnknown-                   | ResponseAssertionStackLevels Int-                   | ResponseAttribute Attribute-                   deriving (Show, Eq)---- Get Assertion Response--type GetAssertionsResponse = [Term]----- Get Proof Response--type GetProofResponse = Sexpr-----Get Unsat Core Response--type GetUnsatCoreResponse = [String]---- Get Unsat Assumptions Response--type GetUnsatAssumptionsResponse = [Term]---- Get Valuation Pair--data ValuationPair = ValuationPair Term Term deriving (Show, Eq)---type GetValueResponse = [ValuationPair]--type GetModelResponse = [Command]----- get Assignment Response--data TValuationPair = TValuationPair String Bool deriving (Show, Eq)--type GetAssignmentResponse = [TValuationPair]----- Get Option Response--type GetOptionResponse = AttrValue---- Echo Response--type EchoResponse = String

@@ -1,48 +0,0 @@-{-# LANGUAGE CPP #-}-module Main where--import Control.Monad-import Data.Array.IArray-import Data.IORef-import System.Environment-import Text.Printf-import qualified ToySolver.FileFormat.CNF as CNF-import ToySolver.SAT.Types-import ToySolver.Internal.Util (setEncodingChar8)--main :: IO ()-main = do-#ifdef FORCE_CHAR8-  setEncodingChar8-#endif--  [problemFile, modelFile] <- getArgs-  wcnf <- CNF.readFile problemFile-  model <- liftM readModel (readFile modelFile)-  costRef <- newIORef 0-  forM_ (CNF.wcnfClauses wcnf) $ \(w,c) ->-    unless (eval model c) $-      if w == CNF.wcnfTopCost wcnf-      then printf "violated hard constraint: %s\n" (show c)-      else do-        tc <- readIORef costRef-        writeIORef costRef $! tc + w-  printf "total cost = %d\n" =<< readIORef costRef--eval :: Model -> PackedClause -> Bool-eval m lits = or [evalLit m lit | lit <- unpackClause lits]--readModel :: String -> Model-readModel s = array (1, maximum (0 : map fst ls2)) ls2-  where-    ls = lines s-    ls2 = do-      l <- ls-      case l of-        'v':xs -> do-          w <- words xs-          case w of-            '-':ys -> return (read ys, False)-            ys -> return (read ys, True)-        _ -> mzero-

@@ -1,47 +0,0 @@-{-# LANGUAGE CPP #-}-module Main where--import Control.Monad-import Data.Array.IArray-import System.Environment-import Text.Printf-import qualified Data.PseudoBoolean as PBFile-import qualified ToySolver.FileFormat as FF-import ToySolver.SAT.Types-import ToySolver.Internal.Util (setEncodingChar8)--main :: IO ()-main = do-#ifdef FORCE_CHAR8-  setEncodingChar8-#endif--  [problemFile, modelFile] <- getArgs-  formula <- FF.readFile problemFile-  model <- liftM readModel (readFile modelFile)-  forM_ (PBFile.pbConstraints formula) $ \c ->-    unless (eval model c) $-      printf "violated: %s\n" (show c)--eval :: Model -> PBFile.Constraint -> Bool-eval m (lhs, op, rhs) = op_v lhs_v rhs-  where-    lhs_v = sum [c | (c,lits) <- lhs, all (evalLit m) lits]-    op_v  = case op of-              PBFile.Ge -> (>=)-              PBFile.Eq -> (==)--readModel :: String -> Model-readModel s = array (1, maximum (0 : map fst ls2)) ls2-  where-    ls = lines s-    ls2 = do-      l <- ls-      case l of-        'v':xs -> do-          w <- words xs-          case w of-            '-':'x':ys -> return (read ys, False)-            'x':ys -> return (read ys, True)-        _ -> mzero-

@@ -2,7 +2,6 @@ module Main where  import qualified Data.ByteString.Builder as ByteStringBuilder-import Data.List import qualified Data.Map as Map import Data.Map (Map) import System.Environment

@@ -23,7 +23,7 @@ import Data.Char import Data.Default.Class import qualified Data.Foldable as F-import Data.List+import Data.List (intercalate) import Data.Map.Lazy (Map) import Data.Maybe import Data.Scientific (Scientific)@@ -35,14 +35,8 @@ import qualified Options.Applicative import System.IO import System.Exit-import System.FilePath-#if MIN_VERSION_optparse_applicative(0,18,0) import Prettyprinter ((<+>)) import qualified Prettyprinter as PP-#else-import Text.PrettyPrint.ANSI.Leijen ((<+>))-import qualified Text.PrettyPrint.ANSI.Leijen as PP-#endif  import qualified Data.PseudoBoolean as PBFile import qualified Numeric.Optimization.MIP as MIP@@ -73,6 +67,7 @@   , optLinearizationUsingPB :: Bool   , optKSat :: Maybe Int   , optFileEncoding :: Maybe String+  , optMPSObjName :: Bool   , optRemoveUserCuts :: Bool   , optNewWCNF :: Bool   , optPBFastParser :: Bool@@ -96,6 +91,7 @@   <*> linearizationPBOption   <*> kSATOption   <*> encodingOption+  <*> mpsObjNameOption   <*> removeUserCutsOption   <*> newWCNFOption   <*> pbFastParserOption@@ -196,6 +192,17 @@       <> metavar "ENCODING"       <> help "file encoding for LP/MPS files" +    mpsObjNameOption :: Parser Bool+    mpsObjNameOption = asum+      [ flag' True+          (  long "mps-obj-name"+          <> help ("Write OBJNAME section in MPS file" ++ (if MIP.optMPSWriteObjName def then " (default)" else "")))+      , flag' False+          (  long "no-mps-obj-name"+          <> help ("Do not write OBJNAME section in MPS file" ++ (if MIP.optMPSWriteObjName def then "" else " (default)")))+      , pure (MIP.optMPSWriteObjName def)+      ]+     removeUserCutsOption :: Parser Bool     removeUserCutsOption = switch       $  long "remove-usercuts"@@ -231,8 +238,6 @@       <> long "version"       <> help "Show version" -#if MIN_VERSION_optparse_applicative(0,18,0)- supportedFormatsDoc :: PP.Doc ann supportedFormatsDoc =   PP.vsep@@ -243,20 +248,6 @@       ]   ] -#else--supportedFormatsDoc :: PP.Doc-supportedFormatsDoc =-  PP.vsep-  [ PP.text "Supported formats:"-  , PP.indent 2 $ PP.vsep-      [ PP.text "input:"  <+> (PP.align $ PP.fillSep $ map PP.text $ words ".cnf .wcnf .opb .wbo .gcnf .lp .mps .qubo")-      , PP.text "output:" <+> (PP.align $ PP.fillSep $ map PP.text $ words ".cnf .wcnf .opb .wbo .lsp .lp .mps .smp .smt2 .ys .qubo")-      ]-  ]--#endif- data Trail sol where   Trail :: (Transformer a, J.ToJSON a) => a -> Trail (Target a) @@ -268,7 +259,9 @@ readProblem :: Options -> String -> IO Problem readProblem o fname = do   enc <- T.mapM mkTextEncoding (optFileEncoding o)-  case getExt fname of+  let mipOpt = def{ MIP.optFileEncoding = enc, MIP.optMPSWriteObjName = optMPSObjName o }++  case FF.getBaseExtension fname of     ".cnf"       | optAsMaxSAT o -> do           prob <- FF.readFile fname@@ -304,10 +297,10 @@             (prob2, info2) ->               return $ ProbWBO prob2 (Trail (ComposedTransformer info1 info2))     ".lp"   -> do-      prob <- MIP.readLPFile def{ MIP.optFileEncoding = enc } fname+      prob <- MIP.readLPFile mipOpt fname       return $ ProbMIP prob (Trail IdentityTransformer)     ".mps"  -> do-      prob <- MIP.readMPSFile def{ MIP.optFileEncoding = enc } fname+      prob <- MIP.readMPSFile mipOpt fname       return $ ProbMIP prob (Trail IdentityTransformer)     ".qubo" -> do       (qubo :: QUBO.Problem Scientific) <- FF.readFile fname@@ -317,14 +310,6 @@     ext ->       error $ "unknown file extension: " ++ show ext -getExt :: String -> String-getExt name | (base, ext) <- splitExtension name =-  case map toLower ext of-#ifdef WITH_ZLIB-    ".gz" -> getExt base-#endif-    s -> s- transformProblem :: Options -> Problem -> Problem transformProblem o = transformObj o . transformPBLinearization o . transformMIPRemoveUserCuts o @@ -373,14 +358,26 @@   case wbo2maxsatWith (optPBEncoding o) wbo of     (wcnf, info') -> (wcnf, Trail (ComposedTransformer info info')) +transformNormalizeOPB :: (PBFile.Formula, Trail SAT.Model) -> (PBFile.Formula, Trail SAT.Model)+transformNormalizeOPB (opb, Trail info) =+  case normalizePB opb of+    (opb', info') -> (opb', Trail (ComposedTransformer info info'))+ transformPB2QUBO :: (PBFile.Formula, Trail SAT.Model) -> ((QUBO.Problem Integer, Integer), Trail QUBO.Solution) transformPB2QUBO (opb, Trail info) =   case pb2qubo opb of     ((qubo, th), info') -> ((qubo, th), Trail (ComposedTransformer info info')) +transformNormalizeMIP :: (MIP.Problem Scientific, Trail (Map MIP.Var Rational)) -> (MIP.Problem Scientific, Trail (Map MIP.Var Rational))+transformNormalizeMIP (ip, Trail info) =+  case normalizeMIPObjective ip of+    (ip', info') -> (ip', Trail (ComposedTransformer info info'))+ writeProblem :: Options -> Problem -> IO () writeProblem o problem = do   enc <- T.mapM mkTextEncoding (optFileEncoding o)+  let mipOpt = def{ MIP.optFileEncoding = enc, MIP.optMPSWriteObjName = optMPSObjName o }+   let mip2smtOpt =         def         { MIP2SMT.optSetLogic     = optSMTSetLogic o@@ -456,10 +453,12 @@               ProbOPB opb _ -> pb2lsp opb               ProbWBO wbo _ -> wbo2lsp wbo               ProbMIP _ _   -> pb2lsp (fst opbAndTrail)-      case getExt fname of+      case FF.getBaseExtension fname of         ".opb" -> do-          FF.writeFile fname $ normalizePB (fst opbAndTrail)-          writeInfo' (snd opbAndTrail)+          case transformNormalizeOPB opbAndTrail of+            (opb, trail) -> do+              FF.writeFile fname opb+              writeInfo' trail         ".wbo" -> do           FF.writeFile fname $ normalizeWBO (fst wboAndTrail)           writeInfo' (snd wboAndTrail)@@ -484,11 +483,15 @@             Just _ -> error "--dump-info is not supported for LSP output"             Nothing -> return ()         ".lp" -> do-          MIP.writeLPFile def{ MIP.optFileEncoding = enc } fname (fst mipAndTrail)-          writeInfo' (snd mipAndTrail)+          case transformNormalizeMIP mipAndTrail of+             (mip, Trail info) -> do+               MIP.writeLPFile mipOpt fname mip+               writeInfo info         ".mps" -> do-          MIP.writeMPSFile def{ MIP.optFileEncoding = enc } fname (fst mipAndTrail)-          writeInfo' (snd mipAndTrail)+          case transformNormalizeMIP mipAndTrail of+             (mip, Trail info) -> do+               MIP.writeMPSFile mipOpt fname mip+               writeInfo info         ".smp" -> do           withBinaryFile fname WriteMode $ \h ->             ByteStringBuilder.hPutBuilder h (pb2smp False (fst opbAndTrail))

@@ -18,7 +18,7 @@ import Control.Monad import Data.Char import qualified Data.IntSet as IntSet-import Data.List+import Data.List (sortBy) import Data.Ord import Data.Version import Options.Applicative

@@ -36,7 +36,7 @@ import qualified Data.Traversable as T import Data.Char import Data.IORef-import Data.List+import Data.List (intercalate, isSuffixOf, sort, sortBy) import Data.Maybe import Data.Ord import qualified Data.Vector.Unboxed as V@@ -50,7 +50,6 @@ import System.IO import System.Exit import System.Clock-import System.FilePath import qualified System.Info as SysInfo import qualified System.Random.MWC as Rand import Text.Printf@@ -108,6 +107,7 @@   , optFileEncoding :: Maybe String   , optMaxSATCompactVLine :: Bool   , optPBFastParser :: Bool+  , optExitCode :: Bool   }  instance Default Options where@@ -132,6 +132,7 @@     , optFileEncoding = Nothing     , optMaxSATCompactVLine = False     , optPBFastParser = False+    , optExitCode = False     }  optionsParser :: Parser Options@@ -155,6 +156,7 @@   <*> fileEncodingOption   <*> maxsatCompactVLineOption   <*> pbFastParserOption+  <*> exitCodeOption   where     fileInput :: Parser String     fileInput = strArgument $ metavar "(FILE|-)"@@ -168,7 +170,8 @@       , flag' ModePB     $ long "pb"      <> help "solve pseudo boolean problem in .opb file"       , flag' ModeWBO    $ long "wbo"     <> help "solve weighted boolean optimization problem in .wbo file"       , flag' ModeMaxSAT $ long "maxsat"  <> help "solve MaxSAT problem in .cnf or .wcnf file"-      , flag' ModeMIP    $ long "lp"      <> help "solve LP/MIP problem in .lp or .mps file"+      , flag' ModeMIP    $ long "mip"     <> help "solve LP/MIP problem in .lp or .mps file"+      , flag' ModeMIP    $ long "lp"      <> help "alias for --mip (deprecated)"       ]      randomSeedOption = optional $ fmap (Rand.toSeed . V.fromList . map read . words) $ strOption@@ -261,6 +264,9 @@       $  long "pb-fast-parser"       <> help "use attoparsec-based parser instead of megaparsec-based one for speed" +    exitCodeOption = switch+      $  long "exit-code"+      <> help "exit with an exit code based on solution status (only for SAT and MaxSAT mode)"  satConfigParser :: Parser SAT.Config satConfigParser = SAT.Config@@ -437,7 +443,7 @@         case optMode opt of           Just m  -> m           Nothing ->-            case getExt (optInput opt) of+            case FF.getBaseExtension (optInput opt) of               ".cnf"  -> ModeSAT               ".gcnf" -> ModeMUS               ".opb"  -> ModePB@@ -476,14 +482,6 @@   putCommentLine $ printf "total wall clock time = %.3fs" (durationSecs startWC endWC)   printGCStat -getExt :: String -> String-getExt name | (base, ext) <- splitExtension name =-  case map toLower ext of-#ifdef WITH_ZLIB-    ".gz" -> getExt base-#endif-    s -> s- printGCStat :: IO () #if defined(__GLASGOW_HASKELL__) printGCStat = do@@ -631,11 +629,15 @@           SAT.setVarPolarity solver v val    result <- SAT.solve solver-  putSLine $ if result then "SATISFIABLE" else "UNSATISFIABLE"-  when result $ do+  if result then do+    putSLine "SATISFIABLE"     m <- SAT.getModel solver     satPrintModel stdout m (CNF.cnfNumVars cnf)     writeSOLFile opt m Nothing (CNF.cnfNumVars cnf)+    when (optExitCode opt) $ exitWith (ExitFailure 10)+  else do+    putSLine "UNSATISFIABLE"+    when (optExitCode opt) $ exitWith (ExitFailure 20)  initPolarityUsingSP :: SAT.Solver -> Int -> Int -> [(Double, SAT.PackedClause)] -> IO (IntMap Double) initPolarityUsingSP solver nvOrig nv clauses = do@@ -983,27 +985,36 @@     case ret of       Nothing -> do         b <- PBO.isUnsat pbo-        if b-          then putSLine "UNSATISFIABLE"-          else putSLine "UNKNOWN"+        if b then do+          putSLine "UNSATISFIABLE"+          when (isMaxSat && optExitCode opt) $ exitWith (ExitFailure 20)+        else do+          putSLine "UNKNOWN"+          if isMaxSat && optExitCode opt then+            exitWith ExitSuccess -- ExitFailure 0 is prohibited+          else+            exitFailure       Just (m, val) -> do+        let printModel =+              if isMaxSat then+                if optMaxSATCompactVLine opt then+                  maxsatPrintModelCompact+                else+                  maxsatPrintModel+              else+                pbPrintModel+         b <- PBO.isOptimum pbo         if b then do           putSLine "OPTIMUM FOUND"-          if isMaxSat then-            if optMaxSATCompactVLine opt then-              maxsatPrintModelCompact stdout m nv-            else-              maxsatPrintModel stdout m nv-          else-            pbPrintModel stdout m nv+          printModel stdout m nv           writeSOLFile opt m (Just val) nv-        else if not isMaxSat then do+          when (isMaxSat && optExitCode opt) $ exitWith (ExitFailure 30)+        else do           putSLine "SATISFIABLE"-          pbPrintModel stdout m nv+          printModel stdout m nv           writeSOLFile opt m (Just val) nv-        else-          putSLine "UNKNOWN"+          when (isMaxSat && optExitCode opt) $ exitWith (ExitFailure 10)  -- ------------------------------------------------------------------------ @@ -1058,7 +1069,7 @@   case ret of     Left msg -> do       putCommentLine msg-      putSLine "UNKNOWN"+      putSLine "UNSUPPORTED"       exitFailure     Right (obj, info) -> do       (linObj, linObjOffset) <- Integer.linearize pbnlc obj@@ -1101,7 +1112,7 @@             b <- PBO.isUnsat pbo             if b               then putSLine "UNSATISFIABLE"-              else putSLine "UNKNOWN"+              else putSLine "UNKNOWN" >> exitFailure           Just (m,val) -> do             b <- PBO.isOptimum pbo             if b

@@ -1,888 +0,0 @@-{-# OPTIONS_GHC -Wall #-}--------------------------------------------------------------------------------- |--- Module      :  ToySolver.SMT.SMTLIB2Solver--- Copyright   :  (c) Masahiro Sakai 2015--- License     :  BSD-style------ Maintainer  :  masahiro.sakai@gmail.com--- Stability   :  experimental--- Portability :  portable----------------------------------------------------------------------------------module ToySolver.SMT.SMTLIB2Solver-  ( module Smtlib.Syntax.Syntax-  , ShowSL (..)--  -- * The solver type-  , Solver-  , newSolver--  -- * High-level API-  , execCommand-  , execCommandString-  , runCommand-  , runCommandString-  , printResponse--  -- * Individual commands--  -- ** (Re)starting and terminating-  , reset-  , setLogic-  , setOption-  , exit--  -- ** Modifying the assertion stack-  , push-  , pop-  , resetAssertions--  -- ** Introducing new symbols-  , declareSort-  , defineSort-  , declareConst-  , declareFun-  , defineFun-  , defineFunRec-  , defineFunsRec--  -- ** Asserting and inspecting formulas-  , assert-  , getAssertions--  -- ** Checking for satisfiability-  , checkSat-  , checkSatAssuming--  -- ** Inspecting models-  , getValue-  , getAssignment-  , getModel--  -- ** Inspecting proofs-  , getProof-  , getUnsatCore-  , getUnsatAssumptions--  -- ** Inspecting settings-  , getInfo-  , getOption--  -- ** Script information-  , setInfo-  , echo-  ) where--import qualified Control.Exception as E-import Control.Monad-import Data.Interned (unintern)-import Data.Interned.Text-import Data.IORef-import Data.Map (Map)-import qualified Data.Map as Map-import Data.Maybe (catMaybes)-import Data.Ratio-import Data.String-import qualified Data.Text as T-import qualified Data.Version as V-import Numeric (readDec, readFloat, readHex)-import System.Exit-import System.IO-import qualified Text.Parsec as Parsec--import qualified ToySolver.BitVector as BV-import qualified ToySolver.SMT as SMT-import ToySolver.Version-import Smtlib.Syntax.Syntax-import Smtlib.Syntax.ShowSL-import qualified Smtlib.Parsers.CommandsParsers as CommandsParsers---- ------------------------------------------------------------------------data Mode-  = ModeStart-  | ModeAssert-  | ModeSat-  | ModeUnsat-  deriving (Eq, Ord, Show)--type EEnv = Map String EEntry-type SortEnv = Map String SortEntry-type Env = (EEnv, SortEnv)--data EEntry-  = EFSymBuiltin InternedText-  | EFSymDeclared SMT.FSym [SMT.Sort] SMT.Sort-  | EExpr SMT.Expr Bool-  | EFunDef EEnv [(String, SMT.Sort)] SMT.Sort Term--data SortEntry-  = SortSym SMT.SSym-  | SortExpr SMT.Sort-  | SortDef SortEnv [String] Sort--interpretSort :: SortEnv -> Sort -> SMT.Sort-interpretSort env s =-  case s of-    SortId ident -> f ident []-    SortIdentifiers ident args -> f ident args-  where-    f ident@(I_Symbol "BitVec" indexes) args-      | not (null args) = E.throw $ SMT.Error (showSL ident ++ ": wrong number of arguments (" ++ show (length args) ++ " for 0)")-      | [IndexNumeral n] <- indexes = SMT.sBitVec n-      | otherwise = E.throw $ SMT.Error ("BitVec: wrong number of indexes (" ++ show (length indexes) ++ " for 1)")-    f ident@(I_Symbol _ _) _ =-      E.throw $ SMT.Error ("unknown sort: " ++ showSL ident)-    f ident@(ISymbol name) args =-      case Map.lookup name env of-        Nothing -> E.throw $ SMT.Error ("unknown sort: " ++ showSL ident)-        Just (SortSym ssym)-          | SMT.ssymArity ssym == length args -> SMT.Sort ssym args'-          | otherwise -> E.throw $ SMT.Error (showSL ident ++ ": wrong number of arguments (" ++ show (length args) ++ " for " ++ show (SMT.ssymArity ssym) ++ ")")-        Just (SortExpr s')-          | null args -> s'-          | otherwise -> E.throw $ SMT.Error (showSL ident ++ ": wrong number of arguments (" ++ show (length args) ++ " for 0)")-        Just (SortDef env' params body) ->-          interpretSort (Map.fromList (zip params (map SortExpr args')) `Map.union` env') body-      where-        args' = map (interpretSort env) args--interpretFun :: Env -> Term -> SMT.Expr-interpretFun (env,senv) t =-  case t of-    TermSpecConstant (SpecConstantNumeral n) -> SMT.EValue $ SMT.ValRational $ fromInteger n-    TermSpecConstant (SpecConstantDecimal s) -> SMT.EValue $ SMT.ValRational $ fst $ head $ readFloat s-    TermSpecConstant (SpecConstantHexadecimal s) ->-      let n = fst $ head $ readHex s-      in SMT.EValue $ SMT.ValBitVec $ BV.nat2bv (length s * 4) n-    TermSpecConstant (SpecConstantBinary s) ->-      SMT.EValue $ SMT.ValBitVec $ BV.fromDescBits [c == '1' | c <- s]-    TermSpecConstant c@(SpecConstantString _s) -> E.throw $ SMT.Error (show c)-    TermQualIdentifier qid -> f qid []-    TermQualIdentifierT  qid args -> f qid args-    TermLet bindings body ->-      interpretFun (Map.fromList [(v, EExpr (interpretFun (env,senv) t2) False) | VB v t2 <- bindings] `Map.union` env, senv) body-    TermForall _bindings _body -> E.throw $ SMT.Error "universal quantifiers are not supported yet"-    TermExists _bindings _body -> E.throw $ SMT.Error "existential quantifiers are not supported yet"-    TermAnnot t2 _ -> interpretFun (env,senv) t2 -- annotations are not supported yet-  where-    unIdentifier :: Identifier -> (String, [Index])-    unIdentifier (ISymbol name) = (name, [])-    unIdentifier (I_Symbol name indexes) = (name, indexes)--    f (QIdentifierAs ident sort) args =-      case ident of-        ISymbol ('@':s) | (n,[]):_ <- reads s ->-          SMT.EValue $ SMT.ValUninterpreted n (interpretSort senv sort)-        _ -> f (QIdentifier ident) args-    f (QIdentifier ident) args-      | ('b':'v':xs, [IndexNumeral n]) <- unIdentifier ident-      , ((x,_):_) <- readDec xs-      , x < 2^n-      = if not (null args)-        then E.throw $ SMT.Error (showSL ident ++ " does not take indexes")-        else SMT.EValue $ SMT.ValBitVec $ BV.nat2bv n x-    f qid@(QIdentifier ident) args =-      case Map.lookup name env of-        Nothing -> E.throw $ SMT.Error ("unknown function symbol: " ++ showSL qid)-        Just (EFSymBuiltin name') ->-          SMT.EAp (SMT.FSym name' indexes') (map (interpretFun (env,senv)) args)-        Just _ | not (null indexes) -> E.throw $ SMT.Error (showSL ident ++ " does not take indexes")-        Just (EExpr e _) -> e-        Just (EFSymDeclared fsym _ _) -> SMT.EAp fsym (map (interpretFun (env,senv)) args)-        Just (EFunDef env' params _y body) ->-          interpretFun (Map.fromList [(p,a) | ((p,_s),a) <- zip params (map (\t -> EExpr (interpretFun (env,senv) t) False) args) ] `Map.union` env', senv) body-      where-        (name, indexes) = unIdentifier ident-        indexes' = map g indexes-        g (IndexNumeral n) = SMT.IndexNumeral (fromIntegral n)-        g (IndexSymbol s) = SMT.IndexSymbol (fromString s)--valueToTerm :: SMT.Value -> Term-valueToTerm (SMT.ValRational v) =-  case v `compare` 0 of-    GT -> f v-    EQ -> TermSpecConstant (SpecConstantNumeral 0)-    LT -> TermQualIdentifierT (QIdentifier $ ISymbol "-") [ f (negate v) ]-  where-    f v = TermQualIdentifierT (QIdentifier $ ISymbol "/")-          [ TermSpecConstant (SpecConstantNumeral (numerator v))-          , TermSpecConstant (SpecConstantNumeral (denominator v))-          ]-valueToTerm (SMT.ValBool b) =-  TermQualIdentifier $ QIdentifier $ ISymbol $ if b then "true" else "false"-valueToTerm (SMT.ValBitVec bv) =-  TermSpecConstant (SpecConstantBinary $ [if b then '1' else '0' | b <- BV.toDescBits bv])-valueToTerm (SMT.ValUninterpreted n s) =-  TermQualIdentifier $ QIdentifierAs (ISymbol $ "@" ++ show n) (sortToSortTerm s)--fsymToIdentifier :: SMT.FSym -> Identifier-fsymToIdentifier (SMT.FSym f indexes) =-  case indexes of-    [] -> ISymbol (T.unpack $ unintern f)-    _ -> I_Symbol (T.unpack $ unintern f) (map g indexes)-  where-    g (SMT.IndexNumeral n) =  IndexNumeral (fromIntegral n)-    g (SMT.IndexSymbol s)  = IndexSymbol (T.unpack $ unintern s)--exprToTerm :: SMT.Expr -> Term-exprToTerm (SMT.EValue v) = valueToTerm v-exprToTerm (SMT.EAp f []) = TermQualIdentifier (QIdentifier (fsymToIdentifier f))-exprToTerm (SMT.EAp f xs) = TermQualIdentifierT (QIdentifier (fsymToIdentifier f)) (map exprToTerm xs)--ssymToSymbol :: SMT.SSym -> Identifier-ssymToSymbol SMT.SSymBool = ISymbol "Bool"-ssymToSymbol SMT.SSymReal = ISymbol "Real"-ssymToSymbol (SMT.SSymBitVec n) = I_Symbol "BitVec" [IndexNumeral n]-ssymToSymbol (SMT.SSymUninterpreted name _) = ISymbol (T.unpack (unintern name))--sortToSortTerm :: SMT.Sort -> Sort-sortToSortTerm (SMT.Sort s []) = SortId (ssymToSymbol s)-sortToSortTerm (SMT.Sort s xs) = SortIdentifiers (ssymToSymbol s) (map sortToSortTerm xs)---- ------------------------------------------------------------------------data Solver-  = Solver-  { svSMTSolverRef :: !(IORef SMT.Solver)-  , svEnvRef :: !(IORef Env)-  , svModeRef :: !(IORef Mode)-  , svSavedContextsRef :: !(IORef [(Maybe (EEnv, SortEnv), [Term])])-  , svStatusRef :: IORef (Maybe Bool)-  , svAssertionsRef :: IORef [Term]-  , svRegularOutputChannelRef :: !(IORef (String, Handle))-  , svDiagnosticOutputChannelRef :: !(IORef (String, Handle))-  , svPrintSuccessRef :: !(IORef Bool)-  , svProduceAssertionsRef :: !(IORef Bool)-  , svProduceAssignmentRef :: !(IORef Bool)-  , svProduceModelsRef :: !(IORef Bool)-  , svProduceUnsatAssumptionsRef :: !(IORef Bool)-  , svProduceUnsatCoresRef :: !(IORef Bool)-  , svGlobalDeclarationsRef :: !(IORef Bool)-  , svUnsatAssumptionsRef :: !(IORef [Term])-  }--newSolver :: IO Solver-newSolver = do-  solverRef <- newIORef =<< SMT.newSolver-  envRef <- newIORef initialEnv-  modeRef <- newIORef ModeStart-  savedContextsRef <- newIORef []-  statusRef <- newIORef Nothing-  assertionsRef <- newIORef ([] :: [Term])-  regOutputRef <- newIORef ("stdout", stdout)-  diagOutputRef <- newIORef ("stderr", stderr)-  printSuccessRef <- newIORef True-  produceAssertionsRef <- newIORef False-  produceAssignmentRef <- newIORef False-  produceModelsRef <- newIORef False-  produceUnsatAssumptionsRef <- newIORef False-  produceUnsatCoresRef <- newIORef False-  globalDeclarationsRef <- newIORef False-  unsatAssumptionsRef <- newIORef undefined-  return $-    Solver-    { svSMTSolverRef = solverRef-    , svEnvRef = envRef-    , svModeRef = modeRef-    , svUnsatAssumptionsRef = unsatAssumptionsRef-    , svSavedContextsRef = savedContextsRef-    , svStatusRef = statusRef-    , svAssertionsRef = assertionsRef-    , svRegularOutputChannelRef = regOutputRef-    , svDiagnosticOutputChannelRef = diagOutputRef-    , svPrintSuccessRef = printSuccessRef-    , svProduceAssertionsRef = produceAssertionsRef-    , svProduceAssignmentRef = produceAssignmentRef-    , svProduceModelsRef = produceModelsRef-    , svProduceUnsatCoresRef = produceUnsatCoresRef-    , svProduceUnsatAssumptionsRef = produceUnsatAssumptionsRef-    , svGlobalDeclarationsRef = globalDeclarationsRef-    }--initialEnv :: Env-initialEnv = (fenv, senv)-  where-    fenv = Map.fromList-      [ (name, EFSymBuiltin (fromString name))-      | name <- ["=", "true", "false", "not", "and", "or", "xor", "ite", "=>", "distinct"-                , "+", "-", "*", "/", ">=", "<=", ">", "<"-                , "extract", "concat", "bvnot", "bvneg"-                , "repeat", "zero_extend", "sign_extend", "rotate_left", "rotate_right"-                , "bvcomp"-                , "bvand", "bvor", "bvxor", "bvnand", "bvnor", "bvxnor"-                , "bvadd", "bvsub", "bvmul", "bvudiv", "bvurem", "bvsdiv", "bvsrem", "bvsmod", "bvshl", "bvlshr", "bvashr"-                , "bvule", "bvult", "bvuge", "bvugt", "bvsle", "bvslt", "bvsge", "bvsgt"-                ]-      ]-    senv = Map.fromList-      [ ("Real", SortSym SMT.SSymReal)-      , ("Bool", SortSym SMT.SSymBool)-      ]--execCommand :: Solver -> Command -> IO ()-execCommand solver cmd = do-  -- putStrLn $ showSL cmd-  printResponse solver =<< runCommand solver cmd--printResponse :: Solver -> CmdResponse -> IO ()-printResponse solver rsp = do-  b <- readIORef (svPrintSuccessRef solver)-  unless (rsp == CmdGenResponse Success && not b) $ do-    (_,h) <- readIORef (svRegularOutputChannelRef solver)-    hPutStrLn h (showSL rsp)--runCommand :: Solver -> Command -> IO CmdResponse-runCommand solver cmd = E.handle h $ do-  case cmd of-    SetLogic logic -> const (CmdGenResponse Success) <$> setLogic solver logic-    SetOption opt -> const (CmdGenResponse Success) <$> setOption solver opt-    GetOption s -> CmdGetOptionResponse <$> getOption solver s-    SetInfo attr -> const (CmdGenResponse Success) <$> setInfo solver attr-    GetInfo flags -> CmdGetInfoResponse <$> getInfo solver flags-    Push n -> const (CmdGenResponse Success) <$> push solver n-    Pop n -> const (CmdGenResponse Success) <$> pop solver n-    DeclareSort name arity -> const (CmdGenResponse Success) <$> declareSort solver name arity-    DefineSort name xs body -> const (CmdGenResponse Success) <$> defineSort solver name xs body-    DeclareConst name y -> const (CmdGenResponse Success) <$> declareConst solver name y-    DeclareFun name xs y -> const (CmdGenResponse Success) <$> declareFun solver name xs y-    DefineFun name xs y body -> const (CmdGenResponse Success) <$> defineFun solver name xs y body-    DefineFunRec name xs y body -> const (CmdGenResponse Success) <$> defineFunRec solver name xs y body-    DefineFunsRec fundecs terms -> const (CmdGenResponse Success) <$> defineFunsRec solver fundecs terms-    Assert tm -> const (CmdGenResponse Success) <$> assert solver tm-    GetAssertions -> CmdGetAssertionsResponse <$> getAssertions solver-    CheckSat -> CmdCheckSatResponse <$> checkSat solver-    CheckSatAssuming ts -> CmdCheckSatResponse <$> checkSatAssuming solver ts-    GetValue ts -> CmdGetValueResponse <$> getValue solver ts-    GetAssignment -> CmdGetAssignmentResponse <$> getAssignment solver-    GetModel -> CmdGetModelResponse <$> getModel solver-    GetProof -> CmdGetProofResponse <$> getProof solver-    GetUnsatCore -> CmdGetUnsatCoreResponse <$> getUnsatCore solver-    GetUnsatAssumptions -> CmdGetUnsatAssumptionsResponse <$> getUnsatAssumptions solver-    Reset -> const (CmdGenResponse Success) <$> reset solver-    ResetAssertions -> const (CmdGenResponse Success) <$> resetAssertions solver-    Echo s -> CmdEchoResponse <$> echo solver s-    Exit -> const (CmdGenResponse Success) <$> exit solver-  where-    h SMT.Unsupported = return (CmdGenResponse Unsupported)-    h (SMT.Error s) = return $ CmdGenResponse $-     -- GenResponse type uses strings in printed form.-     Error $ "\"" ++ concat [if c == '"' then "\"\"" else [c] | c <- s] ++ "\""--execCommandString :: Solver -> String -> IO ()-execCommandString solver cmd = do-  printResponse solver =<< runCommandString solver cmd--runCommandString :: Solver -> String -> IO CmdResponse-runCommandString solver cmd =-  case Parsec.parse (Parsec.spaces >> CommandsParsers.parseCommand <* Parsec.eof) "" cmd of-    Left err ->-      -- GenResponse type uses strings in printed form.-      return $ CmdGenResponse $ Error $ "\"" ++ concat [if c == '"' then "\"\"" else [c] | c <- show err] ++ "\""-    Right cmd ->-      runCommand solver cmd---- ------------------------------------------------------------------------reset :: Solver -> IO GenResponse-reset solver = do-  writeIORef (svSMTSolverRef solver) =<< SMT.newSolver-  writeIORef (svEnvRef solver) initialEnv-  writeIORef (svModeRef solver) ModeStart-  writeIORef (svSavedContextsRef solver) []-  writeIORef (svStatusRef solver) Nothing-  writeIORef (svRegularOutputChannelRef solver) ("stdout",stdout)-  writeIORef (svDiagnosticOutputChannelRef solver) ("stderr",stderr)-  writeIORef (svPrintSuccessRef solver) True-  writeIORef (svProduceAssertionsRef solver) False-  writeIORef (svProduceAssignmentRef solver) False-  writeIORef (svProduceModelsRef solver) False-  writeIORef (svProduceUnsatAssumptionsRef solver) False-  writeIORef (svProduceUnsatCoresRef solver) False-  writeIORef (svUnsatAssumptionsRef solver) undefined-  return Success--setLogic :: Solver -> String -> IO ()-setLogic solver logic = do-  mode <- readIORef (svModeRef solver)-  if mode /= ModeStart then do-    E.throwIO $ SMT.Error "set-logic can only be used in start mode"-  else do-    writeIORef (svModeRef solver) ModeAssert-    case logic of-      "QF_UFLRA" -> return ()-      "QF_UFRDL" -> return ()-      "QF_UF" -> return ()-      "QF_RDL" -> return ()-      "QF_LRA" -> return ()-      "QF_BV" -> return ()-      "QF_UFBV" -> return ()-      "ALL" -> return ()-      "ALL_SUPPORTED" -> return ()-      _ -> E.throwIO SMT.Unsupported--setOption :: Solver -> Option -> IO ()-setOption solver opt = do-  mode <- readIORef (svModeRef solver)-  case opt of-    PrintSuccess b -> do-      writeIORef (svPrintSuccessRef solver) b-    ExpandDefinitions _b -> do-      -- expand-definitions has been removed in SMT-LIB 2.5.-      E.throwIO SMT.Unsupported-    InteractiveMode b -> do-      -- interactive-mode is the old name for produce-assertions. Deprecated.-      unless (mode == ModeStart) $ do-        E.throwIO $ SMT.Error "interactive-mode option can be set only in start mode"-      writeIORef (svProduceAssertionsRef solver) b-      return ()-    ProduceProofs b -> do-      if mode /= ModeStart then-        E.throwIO $ SMT.Error "produce-proofs option can be set only in start mode"-      else if b then-        E.throwIO SMT.Unsupported-      else-        return ()-    ProduceUnsatCores b -> do-      unless (mode == ModeStart) $ do-        E.throwIO $ SMT.Error "produce-unsat-cores option can be set only in start mode"-      writeIORef (svProduceUnsatCoresRef solver) b-      return ()-    ProduceUnsatAssumptions b -> do-      unless (mode == ModeStart) $ do-        E.throwIO $ SMT.Error "produce-unsat-assumptions option can be set only in start mode"-      writeIORef (svProduceUnsatAssumptionsRef solver) b-      return ()-    ProduceModels b -> do-      unless (mode == ModeStart) $ do-        E.throwIO $ SMT.Error "produce-models option can be set only in start mode"-      writeIORef (svProduceModelsRef solver) b-      return ()-    ProduceAssignments b -> do-      unless (mode == ModeStart) $ do-        E.throwIO $ SMT.Error "produce-assignments option can be set only in start mode"-      writeIORef (svProduceAssignmentRef solver) b-      return ()-    ProduceAssertions b -> do-      unless (mode == ModeStart) $ do-        E.throwIO $ SMT.Error "produce-assertions option can be set only in start mode"-      writeIORef (svProduceAssertionsRef solver) b-      return ()-    GlobalDeclarations b -> do-      unless (mode == ModeStart) $ do-        E.throwIO $ SMT.Error "global-declarations option can be set only in start mode"-      writeIORef (svGlobalDeclarationsRef solver) b-      smt <- readIORef (svSMTSolverRef solver)-      SMT.setGlobalDeclarations smt b-    RegularOutputChannel fname -> do-      h <- if fname == "stdout" then-             return stdout-           else-             openFile fname AppendMode-      writeIORef (svRegularOutputChannelRef solver) (fname, h)-      return ()-    DiagnosticOutputChannel fname -> do-      h <- if fname == "stderr" then-             return stderr-           else-             openFile fname AppendMode-      writeIORef (svDiagnosticOutputChannelRef solver) (fname, h)-      return ()-    RandomSeed _i ->-      if mode /= ModeStart then-        E.throwIO $ SMT.Error "random-seed option can be set only in start mode"-      else-        E.throwIO SMT.Unsupported-    Verbosity _lv -> E.throwIO SMT.Unsupported-    ReproducibleResourceLimit _val -> do-      if mode /= ModeStart then-        E.throwIO $ SMT.Error "reproducible-resource-limit option can be set only in start mode"-      else-        E.throwIO SMT.Unsupported-    OptionAttr _attr -> E.throwIO SMT.Unsupported--getOption :: Solver -> String -> IO GetOptionResponse-getOption solver opt =-  case opt of-    ":expand-definitions" -> do-      -- expand-definitions has been removed in SMT-LIB 2.5.-      let b = False-      return $ AttrValueSymbol (showSL b)-    ":global-declarations" -> do-      b <- readIORef (svGlobalDeclarationsRef solver)-      return $ AttrValueSymbol (showSL b)-    ":interactive-mode" -> do-      -- interactive-mode is the old name for produce-assertions. Deprecated.-      b <- readIORef (svProduceAssertionsRef solver)-      return $ AttrValueSymbol (showSL b)-    ":print-success" -> do-      b <- readIORef (svPrintSuccessRef solver)-      return $ AttrValueSymbol (showSL b)-    ":produce-assertions" -> do-      b <- readIORef (svProduceAssertionsRef solver)-      return $ AttrValueSymbol (showSL b)-    ":produce-assignments" -> do-      b <- readIORef (svProduceAssignmentRef solver)-      return $ AttrValueSymbol (showSL b)-    ":produce-models" -> do-      b <- readIORef (svProduceModelsRef solver)-      return $ AttrValueSymbol (showSL b)-    ":produce-proofs" -> do-      let b = False -- default value-      return $ AttrValueSymbol (showSL b)-    ":produce-unsat-cores" -> do-      b <- readIORef (svProduceUnsatCoresRef solver)-      return $ AttrValueSymbol (showSL b)-    ":produce-unsat-assumptions" -> do-      b <- readIORef (svProduceUnsatAssumptionsRef solver)-      return $ AttrValueSymbol (showSL b)-    ":regular-output-channel" -> do-      (fname,_) <- readIORef (svRegularOutputChannelRef solver)-      return $ AttrValueConstant (SpecConstantString fname)-    ":diagnostic-output-channel" -> do-      (fname,_) <- readIORef (svDiagnosticOutputChannelRef solver)-      return $ AttrValueConstant (SpecConstantString fname)-    ":random-seed" -> do-      return $ AttrValueConstant (SpecConstantNumeral 0) -- default value-    ":reproducible-resource-limit" -> do-      return $ AttrValueConstant (SpecConstantNumeral 0) -- default value-    ":verbosity" -> do-      return $ AttrValueConstant (SpecConstantNumeral 0) -- default value-    _ -> do-      E.throwIO SMT.Unsupported--setInfo :: Solver -> Attribute -> IO ()-setInfo solver (AttributeVal ":status" (AttrValueSymbol s)) = do-  v <- case s of-         "sat" -> return $ Just True-         "unsat" -> return $ Just False-         "unknown" -> return $ Nothing-         _ -> E.throwIO $ SMT.Error $ "invalid status value: " ++ s-  writeIORef (svStatusRef solver) v-setInfo _solver _ = return ()--getInfo :: Solver -> InfoFlags -> IO GetInfoResponse-getInfo solver flags = do-  mode <- readIORef (svModeRef solver)-  case flags of-    ErrorBehavior -> return [ResponseErrorBehavior ContinuedExecution]-    Name -> return [ResponseName "toysmt"]-    Authors -> return [ResponseName "Masahiro Sakai"]-    Version -> return [ResponseVersion (V.showVersion version)]-    Status -> E.throwIO SMT.Unsupported-    ReasonUnknown -> do-      if mode /= ModeSat then-        E.throwIO $ SMT.Error "Executions of get-info with :reason-unknown are allowed only when the solver is in sat mode following a check command whose response was unknown."-      else-        return [ResponseReasonUnknown Incomplete]-    AllStatistics -> do-      if not (mode == ModeSat || mode == ModeUnsat) then-        E.throwIO $ SMT.Error "Executions of get-info with :all-statistics are allowed only when the solver is in sat or unsat mode."-      else-        E.throwIO SMT.Unsupported-    AssertionStackLevels -> do-      saved <- readIORef (svSavedContextsRef solver)-      let n = length saved-      n `seq` return [ResponseAssertionStackLevels n]-    InfoFlags _s -> do-      E.throwIO SMT.Unsupported--push :: Solver -> Int -> IO ()-push solver n = do-  replicateM_ n $ do-    (env,senv) <- readIORef (svEnvRef solver)-    assertions <- readIORef (svAssertionsRef solver)-    globalDeclarations <- readIORef (svGlobalDeclarationsRef solver)-    if globalDeclarations then-      modifyIORef (svSavedContextsRef solver) ((Nothing, assertions) :)-    else-      modifyIORef (svSavedContextsRef solver) ((Just (env,senv), assertions) :)-    SMT.push =<< readIORef (svSMTSolverRef solver)-    writeIORef (svModeRef solver) ModeAssert--pop :: Solver -> Int -> IO ()-pop solver n = do-  replicateM_ n $ do-    cs <- readIORef (svSavedContextsRef solver)-    case cs of-      [] -> E.throwIO $ SMT.Error "pop from empty context"-      ((m,assertions) : cs) -> do-        case m of-          Just (env,senv) -> writeIORef (svEnvRef solver) (env,senv)-          Nothing -> return ()-        writeIORef (svAssertionsRef solver) assertions-        writeIORef (svSavedContextsRef solver) cs-        SMT.pop =<< readIORef (svSMTSolverRef solver)-        writeIORef (svModeRef solver) ModeAssert--resetAssertions :: Solver -> IO ()-resetAssertions solver = do-  cs <- readIORef (svSavedContextsRef solver)-  pop solver (length cs)--echo :: Solver -> String -> IO String-echo _solver s = return s--declareSort :: Solver -> String -> Int -> IO ()-declareSort solver name arity = do-  smt <- readIORef (svSMTSolverRef solver)-  s <- SMT.declareSSym smt name arity-  insertSort solver name (SortSym s)-  writeIORef (svModeRef solver) ModeAssert--defineSort :: Solver -> String -> [String] -> Sort -> IO ()-defineSort solver name xs body = do-  (_, senv) <- readIORef (svEnvRef solver)-  insertSort solver name (SortDef senv xs body)-  writeIORef (svModeRef solver) ModeAssert--declareConst :: Solver -> String -> Sort -> IO ()-declareConst solver name y = declareFun solver name [] y--declareFun :: Solver -> String -> [Sort] -> Sort -> IO ()-declareFun solver name xs y = do-  smt <- readIORef (svSMTSolverRef solver)-  (_, senv) <- readIORef (svEnvRef solver)-  let argsSorts = map (interpretSort senv) xs-      resultSort = interpretSort senv y-  f <- SMT.declareFSym smt name argsSorts resultSort-  insertFun solver name (EFSymDeclared f argsSorts resultSort)-  writeIORef (svModeRef solver) ModeAssert--defineFun :: Solver -> String -> [SortedVar] -> Sort -> Term -> IO ()-defineFun solver name xs y body = do-  writeIORef (svModeRef solver) ModeAssert-  (_, senv) <- readIORef (svEnvRef solver)-  let xs' = map (\(SV x s) -> (x, interpretSort senv s)) xs-      y'  = interpretSort senv y-  if null xs' then do-    body' <- processNamed solver body-    (fenv, _) <- readIORef (svEnvRef solver)-    -- use EExpr?-    insertFun solver name (EFunDef fenv [] y' body')-  else do-    (fenv, _) <- readIORef (svEnvRef solver)-    insertFun solver name (EFunDef fenv xs' y' body)-  writeIORef (svModeRef solver) ModeAssert--defineFunRec :: Solver -> String -> [SortedVar] -> Sort -> Term -> IO ()-defineFunRec _solver _name _xs _y _body = do-  E.throwIO SMT.Unsupported--defineFunsRec :: Solver -> [FunDec] -> [Term] -> IO ()-defineFunsRec _solver _fundecs _terms = do-  E.throwIO SMT.Unsupported--assert :: Solver -> Term -> IO ()-assert solver tm = do-  let mname =-        case tm of-          TermAnnot _body attrs-            | name:_ <- [name | AttributeVal ":named" (AttrValueSymbol name) <- attrs] ->-                Just name-          _ -> Nothing-  tm' <- processNamed solver tm-  smt <- readIORef (svSMTSolverRef solver)-  env <- readIORef (svEnvRef solver)-  case mname of-    Nothing -> SMT.assert smt (interpretFun env tm')-    Just name -> SMT.assertNamed smt name (interpretFun env tm')-  do b <- readIORef (svProduceAssertionsRef solver)-     when b $ modifyIORef (svAssertionsRef solver) (tm :)-  writeIORef (svModeRef solver) ModeAssert--getAssertions :: Solver -> IO GetAssertionsResponse-getAssertions solver = do-  mode <- readIORef (svModeRef solver)-  when (mode == ModeStart) $ do-    E.throwIO $ SMT.Error "get-assertions cannot be used in start mode"-  b <- readIORef (svProduceAssertionsRef solver)-  unless b $ do-    E.throwIO $ SMT.Error ":produce-assertions is not enabled"-  reverse <$> readIORef (svAssertionsRef solver)--checkSat :: Solver -> IO CheckSatResponse-checkSat solver = checkSatAssuming solver []--checkSatAssuming :: Solver -> [Term] -> IO CheckSatResponse-checkSatAssuming solver xs = do-  smt <- readIORef (svSMTSolverRef solver)--  env <- readIORef (svEnvRef solver)-  ref <- newIORef Map.empty-  ys <- forM xs $ \x -> do-    let y = interpretFun env x-    modifyIORef ref (Map.insert y x)-    return y--  ret <- SMT.checkSATAssuming smt ys--  do expected <- readIORef (svStatusRef solver)-     writeIORef (svStatusRef solver) Nothing -- I'm not sure if we should reset or not.-     h <- snd <$> readIORef (svDiagnosticOutputChannelRef solver)-     case expected of-       Just True | not ret -> hPutStrLn h "WARNING: unexpected unsat; expecting sat"-       Just False | ret -> hPutStrLn h "WARNING: unexpected sat; expecting unsat"-       _ -> return ()-     hFlush h--  if ret then do-    writeIORef (svModeRef solver) ModeSat-    return Sat-  else do-    writeIORef (svModeRef solver) ModeUnsat-    m <- readIORef ref-    es <- SMT.getUnsatAssumptions smt-    writeIORef (svUnsatAssumptionsRef solver) [m Map.! e | e <- es]-    return Unsat--getValue :: Solver -> [Term] -> IO GetValueResponse-getValue solver ts = do-  ts <- mapM (processNamed solver) ts-  mode <- readIORef (svModeRef solver)-  unless (mode == ModeSat) $ do-    E.throwIO $ SMT.Error "get-value can only be used in sat mode"-  smt <- readIORef (svSMTSolverRef solver)-  m <- SMT.getModel smt-  env <- readIORef (svEnvRef solver)-  forM ts $ \t -> do-    let e = interpretFun env t-    let v = SMT.eval m e-    return $ ValuationPair t (valueToTerm v)--getAssignment :: Solver -> IO GetAssignmentResponse-getAssignment solver = do-  mode <- readIORef (svModeRef solver)-  unless (mode == ModeSat) $ do-    E.throwIO $ SMT.Error "get-assignment can only be used in sat mode"-  smt <- readIORef (svSMTSolverRef solver)-  m <- SMT.getModel smt-  (env, _) <- readIORef (svEnvRef solver)-  liftM concat $ forM (Map.toList env) $ \(name, entry) -> do-    case entry of-      EExpr e True -> do-        s <- SMT.exprSort smt e-        if s /= SMT.sBool then do-          return []-        else do-          let v = SMT.eval m e-          case v of-            (SMT.ValBool b) -> return [TValuationPair name b]-            _ -> E.throwIO $ SMT.Error "get-assignment: should not happen"-      _ -> return []--getModel :: Solver -> IO GetModelResponse-getModel solver = do-  mode <- readIORef (svModeRef solver)-  unless (mode == ModeSat) $ do-    E.throwIO $ SMT.Error "get-model can only be used in sat mode"-  smt <- readIORef (svSMTSolverRef solver)-  m <- SMT.getModel smt-  (env, _) <- readIORef (svEnvRef solver)-  defs <- liftM catMaybes $ forM (Map.toList env) $ \(name, entry) -> do-    case entry of-      EFSymDeclared sym argsSorts resultSort -> do-        case SMT.evalFSym m sym of-          SMT.FunDef [] val ->  do -- constant-            return $ Just $ DefineFun name [] (sortToSortTerm resultSort) (valueToTerm val)-          SMT.FunDef tbl defaultVal -> do -- proper function-            let argsSV :: [SortedVar]-                argsSV = [SV ("x!" ++ show i) (sortToSortTerm s) | (i,s) <- zip [(1::Int)..] argsSorts]-                args :: [Term]-                args = [TermQualIdentifier (QIdentifier (ISymbol x)) | SV x _ <- argsSV]-                f :: ([SMT.Value], SMT.Value) -> Term -> Term-                f (vals,val) tm =-                  TermQualIdentifierT (QIdentifier (ISymbol "ite")) [cond, valueToTerm val, tm]-                  where-                    cond =-                      case zipWith (\arg val -> TermQualIdentifierT (QIdentifier (ISymbol "=")) [arg, valueToTerm val]) args vals of-                        [c] -> c-                        cs -> TermQualIdentifierT (QIdentifier (ISymbol "and")) cs-            return $ Just $ DefineFun name argsSV (sortToSortTerm resultSort) $-              foldr f (valueToTerm defaultVal) tbl-      _ -> return Nothing-  return $ defs ++ [Assert (exprToTerm x) | x <- SMT.modelGetAssertions m]--getProof :: Solver -> IO GetProofResponse-getProof solver = do-  mode <- readIORef (svModeRef solver)-  if mode /= ModeUnsat then-    E.throwIO $ SMT.Error "get-proof can only be used in unsat mode"-  else-    E.throwIO SMT.Unsupported--getUnsatCore :: Solver -> IO GetUnsatCoreResponse-getUnsatCore solver = do-  smt <- readIORef (svSMTSolverRef solver)-  mode <- readIORef (svModeRef solver)-  unless (mode == ModeUnsat) $ do-    E.throwIO $ SMT.Error "get-unsat-core can only be used in unsat mode"-  SMT.getUnsatCore smt--getUnsatAssumptions :: Solver -> IO [Term]-getUnsatAssumptions solver = do-  mode <- readIORef (svModeRef solver)-  unless (mode == ModeUnsat) $ do-    E.throwIO $ SMT.Error "get-unsat-assumptions can only be used in unsat mode"-  readIORef (svUnsatAssumptionsRef solver)--exit :: Solver -> IO ()-exit _solver = exitSuccess---- ------------------------------------------------------------------------insertSort :: Solver -> String -> SortEntry -> IO ()-insertSort solver name sdef = do-  (fenv, senv) <- readIORef (svEnvRef solver)-  case Map.lookup name senv of-    Nothing -> writeIORef (svEnvRef solver) (fenv, Map.insert name sdef senv)-    Just _ -> E.throwIO $ SMT.Error (name ++ " is already used")--insertFun :: Solver -> String -> EEntry -> IO ()-insertFun solver name fdef = do-  (fenv, senv) <- readIORef (svEnvRef solver)-  case Map.lookup name fenv of-    Nothing -> writeIORef (svEnvRef solver) (Map.insert name fdef fenv, senv)-    Just _ -> E.throwIO $ SMT.Error (name ++ " is already used")---- TODO: check closedness of terms-processNamed :: Solver -> Term -> IO Term-processNamed solver = f-  where-    f t@(TermSpecConstant _) = return t-    f t@(TermQualIdentifier _) = return t-    f (TermQualIdentifierT qid args) = do-      args' <- mapM f args-      return $ TermQualIdentifierT qid args'-    f (TermLet bindings body) = do-      body' <- f body-      return $ TermLet bindings body'-    f (TermForall bindings body) = do-      body' <- f body-      return $ TermForall bindings body'-    f (TermExists bindings body) = do-      body' <- f body-      return $ TermExists bindings body'-    f (TermAnnot body attrs) = do-      body' <- f body-      forM_ attrs $ \attr -> do-        case attr of-          AttributeVal ":named" val ->-            case val of-              AttrValueSymbol name -> do-                env <- readIORef (svEnvRef solver)-                let e = interpretFun env body'-                -- smt <- readIORef (svSMTSolverRef solver)-                -- s <- SMT.exprSort smt e-                insertFun solver name (EExpr e True)-              _ -> E.throwIO $ SMT.Error ":named attribute value should be a symbol"-          _ -> return ()-      let attrs' = [attr | attr <- attrs, attrName attr /= ":named"]-            where-              attrName (Attribute s) = s-              attrName (AttributeVal s _v) = s-      if null attrs' then-        return body'-      else-        return $ TermAnnot body' attrs'

@@ -1,5 +1,6 @@ {-# OPTIONS_GHC -Wall #-} {-# LANGUAGE CPP #-}+{-# LANGUAGE OverloadedStrings #-} ----------------------------------------------------------------------------- -- | -- Module      :  toysmt@@ -13,25 +14,31 @@ ----------------------------------------------------------------------------- module Main where -import Control.Applicative-import Control.Monad-import Control.Monad.Trans import Data.Version import Options.Applicative hiding (Parser) import qualified Options.Applicative as Opt+import Control.Monad (when)+import qualified Data.Text.IO as T #ifdef USE_HASKELINE_PACKAGE+import Control.Monad.IO.Class (liftIO)+import Data.Text (Text)+import qualified Data.Text as T import qualified System.Console.Haskeline as Haskeline+import Language.SMTLIB.Parser (frameCommand, Result (..)) #endif+import Language.SMTLIB.Reader.Handle (newHandleReader, readCommand) import System.Exit import System.IO-import Text.Parsec hiding (many)-import Text.Parsec.String -import Smtlib.Parsers.CommandsParsers+import Language.SMTLIB (errorBundlePretty)+import Language.SMTLIB.Parser (parseScript')  import ToySolver.Version+-- 'noAnn' is re-exported by ToySolver.SMT.SMTLIB2Solver (via Language.SMTLIB.Syntax). import ToySolver.SMT.SMTLIB2Solver+#ifdef FORCE_CHAR8 import ToySolver.Internal.Util (setEncodingChar8)+#endif  data Mode   = ModeHelp@@ -87,48 +94,83 @@  loadFile :: Solver -> FilePath -> IO () loadFile solver fname = do-  ret <- parseFromFile (parseSource <* eof) fname-  case ret of+  txt <- T.readFile fname+  case parseScript' fname txt of     Left err -> do-      hPrint stderr err+      hPutStr stderr (errorBundlePretty err)       exitFailure-    Right source -> do-      forM_ source $ \cmd -> do-        execCommand solver cmd+    Right script -> do+      mapM_ (execCommand solver) script  repl :: Solver -> IO () repl solver = do+  -- Use the interactive frontend (prompt, and line editing via haskeline if+  -- available) only when stdin is connected to a terminal. When stdin is a pipe+  -- or a regular file, toysmt is typically driven by another program over the+  -- SMT-LIB protocol; in that case we suppress the prompt so that it does not+  -- pollute the response stream on stdout, and we avoid haskeline entirely.+  tty <- hIsTerminalDevice stdin #ifdef USE_HASKELINE_PACKAGE-  replHaskeline solver+  if tty then+    replHaskeline solver+  else+    replSimple False solver #else-  replSimple solver+  replSimple tty solver #endif -replSimple :: Solver -> IO ()-replSimple solver = do+replSimple :: Bool -> Solver -> IO ()+replSimple showPrompt solver = do   hSetBuffering stdin LineBuffering-  forever $ do-    putStr "toysmt> "-    hFlush stdout-    s <- getLine-    case parse (spaces >> parseCommand <* eof) "<stdin>" s of-      Left err -> do-        hPrint stderr err-      Right cmd -> do-        execCommand solver cmd+  hr <- newHandleReader stdin+  let loop = do+        when showPrompt $ do+          putStr "toysmt> "+          hFlush stdout+        r <- readCommand hr+        case r of+          Left err -> do+            hPutStrLn stderr err+            loop+          Right Nothing -> return ()+          Right (Just cmd) -> do+            execCommand solver (noAnn cmd)+            loop+  loop  #ifdef USE_HASKELINE_PACKAGE  replHaskeline :: Solver -> IO ()-replHaskeline solver = Haskeline.runInputT Haskeline.defaultSettings $ forever $ do-  m <- Haskeline.getInputLine "toysmt> "-  case m of-    Nothing -> return ()-    Just s -> do-      case parse (spaces >> parseCommand) "<stdin>" s of-        Left err -> do-          lift $ hPrint stderr err-        Right cmd -> do-          lift $ execCommand solver cmd+replHaskeline solver = Haskeline.runInputT Haskeline.defaultSettings $ loop T.empty+  where+    loop :: Text -> Haskeline.InputT IO ()+    loop buf = do+      let prompt = if T.null (T.strip buf) then "toysmt> " else "... "+      m <- Haskeline.getInputLine prompt+      case m of+        Nothing -> return ()+        Just s -> process (buf <> T.pack s <> "\n")++    process :: Text -> Haskeline.InputT IO ()+    process buf =+      case frameCommand buf of+        Partial _ -> loop buf  -- incomplete command: prompt for more input+        Done (Right cmd) rest -> do+          liftIO $ execCommand solver (noAnn cmd)+          continue rest+        Done (Left err) rest -> do+          liftIO $ hPutStr stderr (errorBundlePretty err)+          continue rest+        Failed err _ -> do+          -- A framing error (e.g. a stray top-level ')') is not consumed by the+          -- framer, so its leftover would re-trigger the same error forever.+          -- Discard the buffer and prompt afresh.+          liftIO $ hPutStrLn stderr ("framing error: " ++ show err)+          loop T.empty++    continue :: Text -> Haskeline.InputT IO ()+    continue rest+      | T.null (T.strip rest) = loop T.empty+      | otherwise             = process rest  #endif

@@ -20,7 +20,8 @@ import Data.Array.IArray import Data.Char import Data.Default.Class-import Data.List+import Data.IORef+import Data.List (intercalate) import Data.Maybe import Data.Scientific (Scientific) import qualified Data.Scientific as Scientific@@ -79,6 +80,7 @@   , optFileEncoding :: Maybe String   , optMaxSATCompactVLine :: Bool   , optPBFastParser :: Bool+  , optExitCode :: Bool   } deriving (Eq, Show)  optionsParser :: Parser Options@@ -96,6 +98,7 @@   <*> fileEncodingOption   <*> maxsatCompactVLineOption   <*> pbFastParserOption+  <*> exitCodeOption   where     fileInput :: Parser FilePath     fileInput = argument str (metavar "FILE")@@ -106,7 +109,8 @@       <|> flag' ModePB     (long "pb"     <> help "solve pseudo boolean problem in .opb file")       <|> flag' ModeWBO    (long "wbo"    <> help "solve weighted boolean optimization problem in .wbo file")       <|> flag' ModeMaxSAT (long "maxsat" <> help "solve MaxSAT problem in .cnf or .wcnf file")-      <|> flag' ModeMIP    (long "lp"     <> help "solve LP/MIP problem in .lp or .mps file")+      <|> flag' ModeMIP    (long "mip"    <> help "solve LP/MIP problem in .lp or .mps file")+      <|> flag' ModeMIP    (long "lp"     <> help "alias for --mip (deprecated)")      solverOption :: Parser String     solverOption = strOption@@ -177,6 +181,11 @@       $  long "pb-fast-parser"       <> help "use attoparsec-based parser instead of megaparsec-based one for speed" +    exitCodeOption :: Parser Bool+    exitCodeOption = switch+      $  long "exit-code"+      <> help "exit with an exit code based on solution status (only for SAT and MaxSAT mode)"+ parserInfo :: ParserInfo Options parserInfo = info (helper <*> versionOption <*> optionsParser)   $  fullDesc@@ -190,13 +199,23 @@  -- --------------------------------------------------------------------------- +data SolutionStatus+  = UNKNOWN+  | UNSUPPORTED+  | SATISFIABLE+  | UNSATISFIABLE+  | OPTIMUM_FOUND+  | UNBOUNDED+  deriving (Show, Eq, Ord, Bounded, Enum)+ run   :: String   -> Options   -> MIP.Problem Rational+  -> (SolutionStatus -> IO ())   -> (Map MIP.Var Rational -> IO ())   -> IO ()-run solver opt prob printModel = do+run solver opt prob setSolutionStatus printModel = do   unless (Set.null (MIP.semiContinuousVariables prob)) $ do     hPutStrLn stderr "semi-continuous variables are not supported."     exitFailure@@ -259,16 +278,14 @@     solveByQE =       case mapM LAFOL.fromFOLAtom (cs1 ++ cs2) of         Nothing -> do-          putSLine "UNKNOWN"-          exitFailure+          setSolutionStatus UNKNOWN         Just cs ->           case f vs2 cs ivs2 of             Nothing -> do-              putSLine "UNSATISFIABLE"-              exitFailure+              setSolutionStatus UNSATISFIABLE             Just m -> do               putOLine $ showValue (FOL.evalExpr m obj)-              putSLine "SATISFIABLE"+              setSolutionStatus SATISFIABLE               let m2 = Map.fromAscList [(v, m IntMap.! (nameToVar Map.! v)) | v <- Set.toList vs]               printModel m2        where@@ -300,19 +317,16 @@             return (cs',obj')       case prob2 of         Nothing -> do-          putSLine "UNKNOWN"-          exitFailure+          setSolutionStatus UNSUPPORTED         Just (cs',obj') ->           case TextbookMIP.optimize (MIP.objDir $ MIP.objectiveFunction prob) obj' cs' ivs2 of             TextbookMIP.OptUnsat -> do-              putSLine "UNSATISFIABLE"-              exitFailure+              setSolutionStatus UNSATISFIABLE             TextbookMIP.Unbounded -> do-              putSLine "UNBOUNDED"-              exitFailure+              setSolutionStatus UNBOUNDED             TextbookMIP.Optimum r m -> do               putOLine $ showValue r-              putSLine "OPTIMUM FOUND"+              setSolutionStatus OPTIMUM_FOUND               let m2 = Map.fromAscList [(v, m IntMap.! (nameToVar Map.! v)) | v <- Set.toList vs]               printModel m2 @@ -355,17 +369,15 @@       ret <- MIPSolver.optimize mip       case ret of         Simplex.Unsat -> do-          putSLine "UNSATISFIABLE"-          exitFailure+          setSolutionStatus UNSATISFIABLE         Simplex.Unbounded -> do-          putSLine "UNBOUNDED"+          setSolutionStatus UNBOUNDED           Just m <- MIPSolver.getBestModel mip           let m2 = Map.fromAscList [(v, m IntMap.! (nameToVar Map.! v)) | v <- Set.toList vs]           printModel m2-          exitFailure         Simplex.Optimum -> do           Just m <- MIPSolver.getBestModel mip-          putSLine "OPTIMUM FOUND"+          setSolutionStatus OPTIMUM_FOUND           let m2 = Map.fromAscList [(v, m IntMap.! (nameToVar Map.! v)) | v <- Set.toList vs]           printModel m2         Simplex.ObjLimit -> do@@ -373,21 +385,19 @@      solveByCAD       | not (IntSet.null ivs2) = do-          putSLine "UNKNOWN"+          setSolutionStatus UNSUPPORTED           putCommentLine "integer variables are not supported by CAD"-          exitFailure       | otherwise = do           let cs = map (fmap f) $ cs1 ++ cs2               vs3 = Set.fromAscList $ IntSet.toAscList vs2           case CAD.solve vs3 cs of             Nothing -> do-              putSLine "UNSATISFIABLE"-              exitFailure+              setSolutionStatus UNSATISFIABLE             Just m -> do               let m2 = IntMap.map (\x -> AReal.approx x (2^^(-64::Int))) $                          IntMap.fromAscList $ Map.toAscList $ m               putOLine $ showValue (FOL.evalExpr m2 obj)-              putSLine "SATISFIABLE"+              setSolutionStatus SATISFIABLE               let m3 = Map.fromAscList [(v, m2 IntMap.! (nameToVar Map.! v)) | v <- Set.toList vs]               printModel m3       where@@ -404,9 +414,8 @@      solveByContiTraverso       | not (vs `Set.isSubsetOf` ivs) = do-          putSLine "UNKNOWN"+          setSolutionStatus UNSUPPORTED           putCommentLine "continuous variables are not supported by Conti-Traverso algorithm"-          exitFailure       | otherwise = do           let tmp = do                 linObj <- LAFOL.fromFOLExpr obj@@ -414,18 +423,16 @@                 return (linObj, linCon)           case tmp of             Nothing -> do-              putSLine "UNKNOWN"+              setSolutionStatus UNSUPPORTED               putCommentLine "non-linear expressions are not supported by Conti-Traverso algorithm"-              exitFailure             Just (linObj, linCon) ->               case ContiTraverso.solve P.grlex vs2 (MIP.objDir $ MIP.objectiveFunction prob) linObj linCon of                 Nothing -> do-                  putSLine "UNSATISFIABLE"-                  exitFailure+                  setSolutionStatus UNSATISFIABLE                 Just m -> do                   let m2 = IntMap.map fromInteger m                   putOLine $ showValue (FOL.evalExpr m2 obj)-                  putSLine "OPTIMUM FOUND"+                  setSolutionStatus OPTIMUM_FOUND                   let m3 = Map.fromAscList [(v, m2 IntMap.! (nameToVar Map.! v)) | v <- Set.toList vs]                   printModel m3 @@ -438,8 +445,7 @@ mipPrintModel :: Handle -> Bool -> Map MIP.Var Rational -> IO () mipPrintModel h asRat m =   forM_ (Map.toList m) $ \(v, val) ->-    hPrintf h "v %s = %s\n" (MIP.fromVar v) (showRational asRat val)-+    hPrintf h "v %s = %s\n" (MIP.varName v) (showRational asRat val)  putCommentLine :: String -> IO () putCommentLine s = do@@ -467,54 +473,122 @@   setEncodingChar8 #endif -  o <- execParser parserInfo+  opt <- execParser parserInfo -  case fromMaybe ModeMIP (optMode o) of+  ref <- newIORef Nothing+  let putStatus status = do+        m <- readIORef ref+        case m of+          Just _ -> error "solution status is already set"+          Nothing -> writeIORef ref (Just status)++      setSolutionStatusSAT status = do+        putStatus status+        case status of+          UNKNOWN       -> putSLine "UNKNOWN"+          UNSUPPORTED   -> putSLine "UNKNOWN"+          SATISFIABLE   -> putSLine "SATISFIABLE"+          UNSATISFIABLE -> putSLine "UNSATISFIABLE"+          OPTIMUM_FOUND -> putSLine "SATISFIABLE"+          UNBOUNDED     -> putSLine "UNKNOWN"++      setSolutionStatusMaxSAT status = do+        putStatus status+        case status of+          UNKNOWN       -> putSLine "UNKNOWN"+          UNSUPPORTED   -> putSLine "UNKNOWN"+          SATISFIABLE   -> putSLine "SATISFIABLE"+          UNSATISFIABLE -> putSLine "UNSATISFIABLE"+          OPTIMUM_FOUND -> putSLine "OPTIMUM FOUND"+          UNBOUNDED     -> putSLine "UNKNOWN"++      setSolutionStatusPB status = do+        putStatus status+        case status of+          UNKNOWN       -> putSLine "UNKNOWN"+          UNSUPPORTED   -> putSLine "UNSUPPORTED"+          SATISFIABLE   -> putSLine "SATISFIABLE"+          UNSATISFIABLE -> putSLine "UNSATISFIABLE"+          OPTIMUM_FOUND -> putSLine "OPTIMUM FOUND"+          UNBOUNDED     -> putSLine "UNKNOWN"++  case fromMaybe ModeMIP (optMode opt) of     ModeSAT -> do-      cnf <- FF.readFile (optInput o)+      cnf <- FF.readFile (optInput opt)       let (mip,info2) = sat2ip cnf-      run (optSolver o) o (fmap fromInteger mip) $ \m -> do++      run (optSolver opt) opt (fmap fromInteger mip) setSolutionStatusSAT $ \m -> do         let m2 = transformBackward info2 m         satPrintModel stdout m2 0-        writeSOLFileSAT o m2+        writeSOLFileSAT opt m2++      when (optExitCode opt) $ do+        status <- readIORef ref+        case fromMaybe UNKNOWN status of+          UNKNOWN       -> exitSuccess+          UNSUPPORTED   -> exitSuccess+          SATISFIABLE   -> exitWith (ExitFailure 10)+          UNSATISFIABLE -> exitWith (ExitFailure 20)+          OPTIMUM_FOUND -> exitWith (ExitFailure 10)+          UNBOUNDED     -> exitSuccess+     ModePB -> do       pb <--        if optPBFastParser o then-          liftM FF.unWithFastParser $ FF.readFile (optInput o)+        if optPBFastParser opt then+          liftM FF.unWithFastParser $ FF.readFile (optInput opt)         else-          FF.readFile (optInput o)+          FF.readFile (optInput opt)       let (mip,info2) = pb2ip pb-      run (optSolver o) o (fmap fromInteger mip) $ \m -> do+      run (optSolver opt) opt (fmap fromInteger mip) setSolutionStatusPB $ \m -> do         let m2 = transformBackward info2 m         pbPrintModel stdout m2 0-        writeSOLFileSAT o m2+        writeSOLFileSAT opt m2+     ModeWBO -> do       wbo <--        if optPBFastParser o then-          liftM FF.unWithFastParser $ FF.readFile (optInput o)+        if optPBFastParser opt then+          liftM FF.unWithFastParser $ FF.readFile (optInput opt)         else-          FF.readFile (optInput o)+          FF.readFile (optInput opt)       let (mip,info2) = wbo2ip False wbo-      run (optSolver o) o (fmap fromInteger mip) $ \m -> do+      run (optSolver opt) opt (fmap fromInteger mip) setSolutionStatusPB $ \m -> do         let m2 = transformBackward info2 m         pbPrintModel stdout m2 0-        writeSOLFileSAT o m2+        writeSOLFileSAT opt m2+     ModeMaxSAT -> do-      wcnf <- FF.readFile (optInput o)+      wcnf <- FF.readFile (optInput opt)       let (mip,info2) = maxsat2ip False wcnf-      run (optSolver o) o (fmap fromInteger mip) $ \m -> do+      run (optSolver opt) opt (fmap fromInteger mip) setSolutionStatusMaxSAT $ \m -> do         let m2 = transformBackward info2 m-        if optMaxSATCompactVLine o then+        if optMaxSATCompactVLine opt then           maxsatPrintModelCompact stdout m2 0         else           maxsatPrintModel stdout m2 0-        writeSOLFileSAT o m2+        writeSOLFileSAT opt m2++      when (optExitCode opt) $ do+        status <- readIORef ref+        case fromMaybe UNKNOWN status of+          UNKNOWN       -> exitSuccess+          UNSUPPORTED   -> exitSuccess+          SATISFIABLE   -> exitWith (ExitFailure 10)+          UNSATISFIABLE -> exitWith (ExitFailure 20)+          OPTIMUM_FOUND -> exitWith (ExitFailure 30)+          UNBOUNDED     -> exitSuccess+     ModeMIP -> do-      enc <- T.mapM mkTextEncoding $ optFileEncoding o-      mip <- MIP.readFile def{ MIP.optFileEncoding = enc } (optInput o)-      run (optSolver o) o (fmap toRational mip) $ \m -> do-        mipPrintModel stdout (optPrintRational o) m-        writeSOLFileMIP o m+      enc <- T.mapM mkTextEncoding $ optFileEncoding opt+      mip <- MIP.readFile def{ MIP.optFileEncoding = enc } (optInput opt)+      run (optSolver opt) opt (fmap toRational mip) setSolutionStatusPB $ \m -> do+        mipPrintModel stdout (optPrintRational opt) m+        writeSOLFileMIP opt m++  status <- readIORef ref+  case fromMaybe UNKNOWN status of+    UNKNOWN       -> exitFailure+    UNSUPPORTED   -> exitFailure+    _ -> exitSuccess  -- FIXME: 目的関数値を表示するように writeSOLFileMIP :: Options -> Map MIP.Var Rational -> IO ()

@@ -0,0 +1,163 @@+{-# OPTIONS_GHC -Wall #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+module Main where++import Control.Monad+import qualified Data.ByteString.Lazy.Char8 as BL+import Data.Default.Class+import Data.Scientific+import qualified Data.Version as V+import qualified Numeric.Optimization.MIP as MIP+import qualified Numeric.Optimization.MIP.Solution.Gurobi as GurobiSol+import Options.Applicative hiding (Const)+import System.Exit+import System.IO++import qualified ToySolver.FileFormat as FF+import ToySolver.Internal.SolutionChecker+import ToySolver.SAT.LogParser (parseSATLog, parseMaxSATLog, parsePBLog)+import ToySolver.Internal.Util (setEncodingChar8)+import ToySolver.Version+++data Mode = ModeSAT | ModePB | ModeWBO | ModeMaxSAT | ModeMIP+  deriving (Eq, Ord, Show)++data Options = Options+  { optInputFile :: FilePath+  , optSolutionFile :: FilePath+  , optMode :: Maybe Mode+  , optFileEncoding :: Maybe String+  , optPBFastParser :: Bool+  , optMIPTol :: MIP.Tol Scientific+  }++optionsParser :: Parser Options+optionsParser = Options+  <$> fileInput+  <*> solutionFileInput+  <*> modeOption+  <*> fileEncodingOption+  <*> pbFastParserOption+  <*> mipTolOptions+  where+    fileInput :: Parser FilePath+    fileInput = argument str (metavar "FILE")++    solutionFileInput :: Parser FilePath+    solutionFileInput = argument str (metavar "SOLUTION_FILE")++    modeOption :: Parser (Maybe Mode)+    modeOption = optional $+          flag' ModeSAT    (long "sat"    <> help "load boolean satisfiability problem in .cnf file")+      <|> flag' ModePB     (long "pb"     <> help "load pseudo boolean problem in .opb file")+      <|> flag' ModeWBO    (long "wbo"    <> help "load weighted boolean optimization problem in .wbo file")+      <|> flag' ModeMaxSAT (long "maxsat" <> help "load MaxSAT problem in .cnf or .wcnf file")+      <|> flag' ModeMIP    (long "mip"    <> help "load LP/MIP problem in .lp or .mps file")+      <|> flag' ModeMIP    (long "lp"     <> help "alias for --mip (deprecated)")++    fileEncodingOption :: Parser (Maybe String)+    fileEncodingOption = optional $ strOption+      $  long "encoding"+      <> metavar "ENCODING"+      <> help "file encoding for LP/MPS files"++    pbFastParserOption :: Parser Bool+    pbFastParserOption = switch+      $  long "pb-fast-parser"+      <> help "use attoparsec-based parser instead of megaparsec-based one for speed"++    mipTolOptions :: Parser (MIP.Tol Scientific)+    mipTolOptions = MIP.Tol <$> intTol <*> feasTol <*> optTol+      where+        intTol = option auto+          $  long "tol-integrality"+          <> metavar "REAL"+          <> help "If a value of integer variable is within this amount from its nearest integer, it is considered feasible."+          <> value (MIP.integralityTol def)+          <> showDefault+        feasTol = option auto+          $  long "tol-feasibility"+          <> metavar "REAL"+          <> help "If the amount of violation of constraints is within this amount, it is considered feasible."+          <> value (MIP.feasibilityTol def)+          <> showDefault+        optTol = option auto+          $  long "tol-optimality"+          <> metavar "REAL"+          <> help "Feasibility tolerance of dual constraints."+          <> value (MIP.optimalityTol def)+          <> showDefault++parserInfo :: ParserInfo Options+parserInfo = info (helper <*> versionOption <*> optionsParser)+  $  fullDesc+  <> header "toysolver-check - a solution checker"+  where+    versionOption :: Parser (a -> a)+    versionOption = infoOption (V.showVersion version)+      $  hidden+      <> long "version"+      <> help "Show version"++main :: IO ()+main = do+#ifdef FORCE_CHAR8+  setEncodingChar8+#endif++  opt <- execParser parserInfo+  let mode =+        case optMode opt of+          Just m  -> m+          Nothing ->+            case FF.getBaseExtension (optInputFile opt) of+              ".cnf"  -> ModeSAT+              ".opb"  -> ModePB+              ".wbo"  -> ModeWBO+              ".wcnf" -> ModeMaxSAT+              ".lp"   -> ModeMIP+              ".mps"  -> ModeMIP+              _ -> ModeSAT++  (ok, ls) <- case mode of+    ModeSAT -> do+      cnf  <- FF.readFile (optInputFile opt)+      (status, m) <- liftM parseSATLog (BL.readFile (optSolutionFile opt))+      pure $ checkSATResult cnf (status, m)++    ModePB -> do+      opb <-+        if optPBFastParser opt then+          liftM FF.unWithFastParser $ FF.readFile (optInputFile opt)+        else+          FF.readFile (optInputFile opt)+      (status, o, m) <- liftM parsePBLog (BL.readFile (optSolutionFile opt))+      pure $ checkPBResult opb (status, o, m)++    ModeWBO -> do+      wbo <-+        if optPBFastParser opt then+          liftM FF.unWithFastParser $ FF.readFile (optInputFile opt)+        else+          FF.readFile (optInputFile opt)+      (status, o, m) <- liftM parsePBLog (BL.readFile (optSolutionFile opt))+      pure $ checkWBOResult wbo (status, o, m)++    ModeMaxSAT -> do+      wcnf  <- FF.readFile (optInputFile opt)+      (status, o, m) <- liftM parseMaxSATLog (BL.readFile (optSolutionFile opt))+      pure $ checkMaxSATResult wcnf (status, o, m)++    ModeMIP -> do+      enc <- mapM mkTextEncoding $ optFileEncoding opt+      mip <- MIP.readFile def{ MIP.optFileEncoding = enc } (optInputFile opt)+      sol <- GurobiSol.readFile (optSolutionFile opt)+      let tol = optMIPTol opt+      pure $ checkMIPResult tol mip sol++  mapM_ putStrLn ls++  unless ok $ exitFailure

@@ -31,7 +31,7 @@ import qualified Data.IntMap as IntMap import Data.IntSet (IntSet) import qualified Data.IntSet as IntSet-import Data.List+import Data.List (unfoldr) import qualified Data.Vector.Unboxed as VU import System.Environment import ToySolver.Combinatorial.BipartiteMatching

@@ -5,7 +5,7 @@  import Control.Monad import Data.Char-import Data.List+import Data.List (intercalate) import qualified Data.IntSet as IntSet import qualified Data.Set as Set import System.Environment

@@ -4,7 +4,7 @@ module Main where  import Control.Monad-import Data.List+import Data.List (intersperse) import System.Environment import System.IO import Text.Printf

@@ -8,7 +8,7 @@ import qualified Data.ByteString.Lazy.Char8 as BL import Data.Char import Data.Default.Class-import Data.List+import Data.List (intersperse) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Data.Maybe

@@ -11,9 +11,7 @@ import Data.Foldable (toList) import qualified Data.IntMap.Strict as IntMap import Data.Int-import Data.List import Data.Maybe-import Data.Ord import qualified Data.Sequence as Seq import System.Console.GetOpt import System.Environment@@ -64,20 +62,20 @@           let ret = ShortestPath.dijkstra ShortestPath.unit g vs           _ <- evaluate ret           when (PrintResult `elem` o) $ do-            forM_ (sortBy (comparing fst) (IntMap.toList ret)) $ \(v, (cost,_)) -> do+            forM_ (IntMap.toAscList ret) $ \(v, (cost,_)) -> do               putStrLn $ show v ++ ": " ++ show cost         "bellmanford" -> do           let ret = ShortestPath.bellmanFord ShortestPath.unit g vs           _ <- evaluate ret           when (PrintResult `elem` o) $ do-            forM_ (sortBy (comparing fst) (IntMap.toList ret)) $ \(v, (cost,_)) -> do+            forM_ (IntMap.toAscList ret) $ \(v, (cost,_)) -> do               putStrLn $ show v ++ ": " ++ show cost         "floydwarshall" -> do           let ret = ShortestPath.floydWarshall ShortestPath.unit g           _ <- evaluate ret           when (PrintResult `elem` o) $ do-            forM_ (sortBy (comparing fst) (IntMap.toList ret)) $ \(v, m) -> do-              forM_ (sortBy (comparing fst) (IntMap.toList m)) $ \(u, (cost,_)) -> do+            forM_ (IntMap.toAscList ret) $ \(v, m) -> do+              forM_ (IntMap.toAscList m) $ \(u, (cost,_)) -> do                 putStrLn $ show v ++ "-" ++ show u ++ ": " ++ show cost         _ -> error ("unknown method: " ++ method)     (_,_,errs) -> do@@ -88,10 +86,7 @@ load fname = do   s <- BL.readFile fname   let f l = do-        -- 'BL.stripPrefix' is available only on bytestring >=0.10.8.0,-        -- But we still want to support bytestring-0.10.4.0 (lts-2.22) and bytestring-0.10.6.0 (lts-3.22).-        (c,l2) <- BL.uncons l-        guard $ c == 'a'+        l2 <- BL.stripPrefix "a" l         (v,l3) <- BL.readInt $ BL.dropWhile isSpace l2         (u,l4) <- BL.readInt $ BL.dropWhile isSpace l3         (w,_)  <- BL.readInt $ BL.dropWhile isSpace l4

@@ -3,7 +3,6 @@ import Control.Exception import Control.Monad import Data.Default.Class-import Data.List import System.Console.GetOpt import System.Environment import System.Exit

@@ -1,3 +1,2 @@ p cnf 0 1 0-

@@ -52,7 +52,7 @@ import Control.Exception import Control.Monad import Control.Monad.State-import Data.List+import Data.List (intercalate, sortOn) import Data.Maybe import Data.Ord import Data.Map (Map)@@ -73,8 +73,6 @@ import ToySolver.Data.Polynomial (Polynomial, UPolynomial, X (..), PrettyVar, PrettyCoeff) import qualified ToySolver.Data.Polynomial as P import qualified ToySolver.Data.Polynomial.GroebnerBasis as GB--import Debug.Trace  -- --------------------------------------------------------------------------- 

@@ -34,7 +34,7 @@ import qualified Data.IntMap as IM import qualified Data.IntSet as IS import qualified Data.Map as Map-import Data.List+import Data.List (foldl') import Data.Monoid import Data.Ratio import Data.VectorSpace

@@ -50,7 +50,7 @@  import Control.Monad import qualified Data.Foldable as Foldable-import Data.List+import Data.List (foldl', foldl1') import Data.Maybe import qualified Data.IntMap as IM import qualified Data.IntSet as IS

@@ -53,7 +53,7 @@     ) where  import Control.Monad-import Data.List+import Data.List (foldl', foldl1') import Data.Maybe import Data.Ratio import qualified Data.IntMap as IM

@@ -62,7 +62,7 @@ import Control.Concurrent import Control.Concurrent.STM import Data.Default.Class-import Data.List+import Data.List (maximumBy) import Data.OptDir import Data.Ord import Data.IORef

@@ -43,7 +43,7 @@ import Control.Exception (assert) import Control.Monad import Data.Default.Class-import Data.List+import Data.List (foldl', foldl1', minimumBy) import Data.Maybe import Data.Ord import Data.Ratio

@@ -127,7 +127,7 @@ import Data.Char import Data.Default.Class import Data.Ord-import Data.List+import Data.List (foldl', maximumBy, minimumBy) import Data.Maybe import Data.Monoid import Data.Primitive.MutVar@@ -504,7 +504,7 @@       where         c = c1 * c2         c1 = fromIntegral $ foldl' lcm 1 [denominator c | (c, _) <- LA.terms e]-        c2 = signum $ head ([c | (c,x) <- LA.terms e] ++ [1])+        c2 = signum $ fromMaybe 1 (listToMaybe [c | (c,_) <- LA.terms e])  assertLower :: (PrimMonad m, SolverValue v) => GenericSolverM m v -> Var -> v -> m () assertLower solver x l = assertLB solver x (Just (l, IntSet.empty))

@@ -53,7 +53,7 @@   ) where  import Data.Ord-import Data.List+import Data.List (foldl', intersperse, maximumBy, minimumBy) import qualified Data.IntMap as IM import qualified Data.IntSet as IS import Data.OptDir

@@ -44,8 +44,6 @@  import Prelude hiding (repeat) import Data.Bits-import Data.Map (Map)-import qualified Data.Map as Map import Data.Ord import qualified Data.Semigroup as Semigroup import qualified Data.Vector as V@@ -490,10 +488,10 @@  -- ------------------------------------------------------------------------ -type Model = (V.Vector BV, Map BV BV, Map BV BV)+type Model = V.Vector BV  evalExpr :: Model -> Expr -> BV-evalExpr (env, divTable, remTable) = f+evalExpr env = f   where     f (EConst bv) = bv     f (EVar v) = env VG.! varId v@@ -511,23 +509,11 @@     evalOp2 OpAdd x y = bvadd x y     evalOp2 OpMul x y = bvmul x y     evalOp2 OpUDiv x y-      | y' /= 0 = bvudiv x y-      | otherwise =-          case Map.lookup x divTable of-            Just d -> d-            Nothing -> nat2bv (width x) 0-      where-        y' :: Integer-        y' = bv2nat y+      | bv2nat y /= (0 :: Integer) = bvudiv x y+      | otherwise = fromAscBits (replicate (width x) True)     evalOp2 OpURem x y-      | y' /= 0 = bvurem x y-      | otherwise =-          case Map.lookup x remTable of-            Just r -> r-            Nothing -> nat2bv (width x) 0-      where-        y' :: Integer-        y' = bv2nat y+      | bv2nat y /= (0 :: Integer) = bvurem x y+      | otherwise = x     evalOp2 OpSDiv x y       | width x < 1 || width y < 1 || width x /= width y = error "invalid width"       | not msb_x && not msb_y = evalOp2 OpUDiv x y

@@ -61,7 +61,6 @@   , svSATSolver :: SAT.Solver   , svTseitin :: Tseitin.Encoder IO   , svEncTable :: IORef (Map Expr (VU.Vector SAT.Lit))-  , svDivRemTable :: IORef [(VU.Vector SAT.Lit, VU.Vector SAT.Lit, VU.Vector SAT.Lit, VU.Vector SAT.Lit)]   , svAtomTable :: IORef (Map NormalizedAtom SAT.Lit)   , svContexts :: Vec.Vec (IntMap (Maybe Int))   }@@ -72,7 +71,6 @@   sat <- SAT.newSolver   tseitin <- Tseitin.newEncoder sat   table <- newIORef Map.empty-  divRemTable <- newIORef []   atomTable <- newIORef Map.empty   contexts <- Vec.new   Vec.push contexts IntMap.empty@@ -82,7 +80,6 @@     , svSATSolver = sat     , svTseitin = tseitin     , svEncTable = table-    , svDivRemTable = divRemTable     , svAtomTable = atomTable     , svContexts = contexts     }@@ -156,12 +153,8 @@   m <- SAT.getModel (svSATSolver solver)   vss <- Vec.getElems (svVars solver)   let f = fromAscBits . map (SAT.evalLit m) . VG.toList-      isZero' = not . or . toAscBits       env = VG.fromList [f vs | vs <- vss]-  xs <- readIORef (svDivRemTable solver)-  let divTable = Map.fromList [(f s, f d) | (s,t,d,_r) <- xs, isZero' (f t)]-      remTable = Map.fromList [(f s, f r) | (s,t,_d,r) <- xs, isZero' (f t)]-  return (env, divTable, remTable)+  return env  explain :: Solver -> IO IntSet explain solver = do@@ -387,12 +380,11 @@   c <- do     tmp <- encodeMul (svTseitin solver) False d t     encodeSum (svTseitin solver) w False [tmp, r]-  tbl <- readIORef (svDivRemTable solver)+  -- Semantics of division and remainder operators has been changed in SMT-LIB 2.6.   Tseitin.addFormula (svTseitin solver) $     ite (isZero t)-        (And [(isEQ s s' .&&. isZero t') .=>. (isEQ d d' .&&. isEQ r r') | (s',t',d',r') <- tbl, w == VG.length s'])+        (And [Atom l | l <- VG.toList d] .&&. isEQ s r)         (isEQ s c .&&. isULT r t)-  modifyIORef (svDivRemTable solver) ((s,t,d,r) :)   return (d,r)  encodeSDiv :: Solver -> SBV -> SBV -> IO SBV

@@ -1,4 +1,3 @@-{-# LANGUAGE DeriveDataTypeable #-} {-# OPTIONS_GHC -Wall #-} {-# OPTIONS_HADDOCK show-extensions #-} -----------------------------------------------------------------------------@@ -34,7 +33,6 @@ import qualified Data.IntMap as IntMap import Data.Set (Set) import qualified Data.Set as Set-import Data.Typeable import System.Exit import System.IO import System.IO.Temp@@ -69,7 +67,7 @@     }  data Failure = Failure !Int-  deriving (Show, Typeable)+  deriving (Show)  instance Exception Failure 

@@ -1,4 +1,3 @@-{-# LANGUAGE DeriveDataTypeable #-} {-# OPTIONS_GHC -Wall #-} {-# OPTIONS_HADDOCK show-extensions #-} -----------------------------------------------------------------------------@@ -33,7 +32,6 @@ import qualified Data.IntMap as IntMap import Data.Set (Set) import qualified Data.Set as Set-import Data.Typeable import System.Exit import System.IO import System.IO.Temp@@ -60,7 +58,7 @@     }  data Failure = Failure !Int-  deriving (Show, Typeable)+  deriving (Show)  instance Exception Failure 

@@ -22,10 +22,10 @@  import Control.Monad import Control.Monad.State.Strict-import Data.Function (on) import Data.IntSet (IntSet) import qualified Data.IntSet as IntSet-import Data.List+import Data.List (sortOn)+import Data.Ord  type Weight = Rational type Value  = Rational@@ -41,7 +41,7 @@   )   where     items' :: [(Value, Weight, Int)]-    items' = map fst $ sortBy (flip compare `on` snd) [((v, w, n), (v / w, v)) | (n, (v, w)) <- zip [0..] items, w > 0, v > 0]+    items' = sortOn (\(v, w, _) -> Down ((v / w, v))) [(v, w, n) | (n, (v, w)) <- zip [0..] items, w > 0, v > 0]      sol :: IntSet     sol = IntSet.fromList [n | (n, (v, w)) <- zip [0..] items, w == 0, v > 0] `IntSet.union`

@@ -1,3 +1,4 @@+{-# OPTIONS_GHC -Wall #-} {-# OPTIONS_HADDOCK show-extensions #-} {-# LANGUAGE ScopedTypeVariables #-} -----------------------------------------------------------------------------@@ -24,8 +25,6 @@ import Control.Monad import Control.Monad.ST import Data.Array.ST-import Data.Function (on)-import Data.List  type Weight = Int type Value = Rational@@ -56,5 +55,8 @@       (obj, w, sol) <- readArray table limit       return (obj, w, reverse sol) -test1 = solve [(5,4), (4,5), (3,2)] 9-test2 = solve [(45,5), (48,8), (35,3)] 10+_test1 :: (Value, Weight, [Bool])+_test1 = solve [(5,4), (4,5), (3,2)] 9++_test2 :: (Value, Weight, [Bool])+_test2 = solve [(45,5), (48,8), (35,3)] 10

@@ -22,7 +22,7 @@   , solveGeneric   ) where -import Data.List+import Data.List (foldl', foldl1') import Data.IntMap.Strict (IntMap) import qualified Data.IntMap.Strict as IntMap import Data.Map.Strict (Map)

@@ -1,6 +1,5 @@ {-# OPTIONS_GHC -Wall #-} {-# OPTIONS_HADDOCK show-extensions #-}-{-# LANGUAGE CPP #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -34,6 +33,10 @@   , ip2pb   , IP2PBInfo (..)   , addMIP++  -- * Linearization of the constant term in objective function+  , normalizeMIPObjective+  , NormalizeMIPObjectiveInfo (..)   ) where  import Control.Monad@@ -43,14 +46,12 @@ import Control.Monad.Trans.Except import qualified Data.Aeson as J import qualified Data.Aeson.Types as J-#if MIN_VERSION_aeson(2,0,0) import qualified Data.Aeson.Key as Key-#endif import Data.Aeson ((.=), (.:)) import Data.Array.IArray import Data.Default.Class import qualified Data.IntSet as IntSet-import Data.List (intercalate, foldl', sortBy)+import Data.List (intercalate, foldl', foldl1',  sortBy) import Data.Maybe import Data.Map (Map) import qualified Data.Map as Map@@ -60,11 +61,15 @@ import qualified Data.Set as Set import Data.String import qualified Data.Text as T+import qualified Data.Vector as V+import qualified Data.Vector.Generic as VG import Data.VectorSpace+import Text.Printf  import qualified Data.PseudoBoolean as PBFile import qualified Numeric.Optimization.MIP as MIP +import qualified ToySolver.Combinatorial.SubsetSum as SubsetSum import ToySolver.Converter.Base import ToySolver.Converter.PB import ToySolver.Data.OrdRel@@ -74,7 +79,6 @@ import qualified ToySolver.SAT.Types as SAT import qualified ToySolver.SAT.Encoder.Integer as Integer import ToySolver.SAT.Store.PB-import ToySolver.Internal.Util (revForM)  -- ----------------------------------------------------------------------------- @@ -125,27 +129,30 @@      vs = [convVar v | v <- [1..PBFile.pbNumVars formula]] +    varTable :: Array SAT.Var MIP.Var+    varTable = listArray (1, PBFile.pbNumVars formula) vs+     obj2 =       case PBFile.pbObjectiveFunction formula of-        Just obj' -> def{ MIP.objDir = MIP.OptMin, MIP.objExpr = convExpr obj' }+        Just obj' -> def{ MIP.objDir = MIP.OptMin, MIP.objExpr = convExpr varTable obj' }         Nothing   -> def{ MIP.objDir = MIP.OptMin, MIP.objExpr = 0 }      cs2 = do       (lhs,op,rhs) <- PBFile.pbConstraints formula-      let (lhs2,c) = splitConst $ convExpr lhs+      let (lhs2,c) = splitConst $ convExpr varTable lhs           rhs2 = rhs - c       return $ case op of         PBFile.Ge -> def{ MIP.constrExpr = lhs2, MIP.constrLB = MIP.Finite rhs2 }         PBFile.Eq -> def{ MIP.constrExpr = lhs2, MIP.constrLB = MIP.Finite rhs2, MIP.constrUB = MIP.Finite rhs2 }  -convExpr :: PBFile.Sum -> MIP.Expr Integer-convExpr s = sum [product (fromIntegral w : map f tm) | (w,tm) <- s]+convExpr :: Array SAT.Var MIP.Var -> PBFile.Sum -> MIP.Expr Integer+convExpr varTable s = sum [product (fromIntegral w : map f tm) | (w,tm) <- s]   where     f :: PBFile.Lit -> MIP.Expr Integer     f x-      | x > 0     = MIP.varExpr (convVar x)-      | otherwise = 1 - MIP.varExpr (convVar (abs x))+      | x > 0     = MIP.varExpr (varTable ! x)+      | otherwise = 1 - MIP.varExpr (varTable ! abs x)  convVar :: PBFile.Var -> MIP.Var convVar x = fromString ("x" ++ show x)@@ -184,16 +191,10 @@     [ "type" .= ("WBO2IPInfo" :: J.Value)     , "num_original_variables" .= nv     , "relax_variables" .= J.object-        [ toKey (MIP.varName v) .= jPBConstraint constr+        [ Key.fromText (MIP.varName v) .= jPBConstraint constr         | (v, constr) <- relaxVariables         ]     ]-    where-#if MIN_VERSION_aeson(2,0,0)-      toKey = Key.fromText-#else-      toKey = id-#endif  instance J.FromJSON WBO2IPInfo where   parseJSON =@@ -217,8 +218,13 @@       , MIP.varDomains = Map.fromList [(v, (MIP.IntegerVariable, (0,1))) | v <- vs]       } -    vs = [convVar v | v <- [1..PBFile.wboNumVars formula]] ++ [v | (ts, _) <- cs2, (_, v) <- ts]+    vs1 = [convVar v | v <- [1..PBFile.wboNumVars formula]]+    vs2 = [v | (ts, _) <- cs2, (_, v) <- ts]+    vs = vs1 ++ vs2 +    varTable :: Array SAT.Var MIP.Var+    varTable = listArray (1, PBFile.wboNumVars formula) vs1+     obj2 = def       { MIP.objDir = MIP.OptMin       , MIP.objExpr = MIP.Expr [MIP.Term w [v] | (ts, _) <- cs2, (w, v) <- ts]@@ -237,7 +243,7 @@     cs2 :: [([(Integer, MIP.Var)], MIP.Constraint Integer)]     cs2 = do       (v, (w, (lhs,op,rhs))) <- relaxVariables-      let (lhs2,c) = splitConst $ convExpr lhs+      let (lhs2,c) = splitConst $ convExpr varTable lhs           rhs2 = rhs - c           (ts,ind) =             case w of@@ -318,7 +324,7 @@       formula <- lift $ getPBFormula db       return $ (formula{ PBFile.pbObjectiveFunction = Just obj }, info) -data IP2PBInfo = IP2PBInfo (Map MIP.Var Integer.Expr) (Map MIP.Var SAT.Lit) !Integer+data IP2PBInfo = IP2PBInfo (Map MIP.Var Integer.Expr) (Map MIP.Var SAT.Lit) !Rational   deriving (Eq, Show)  instance Transformer IP2PBInfo where@@ -326,7 +332,7 @@   type Target IP2PBInfo = SAT.Model  instance ForwardTransformer IP2PBInfo where-  transformForward (IP2PBInfo vmap nonZeroTable _d) sol+  transformForward (IP2PBInfo vmap nonZeroTable _s) sol     | Map.keysSet vmap /= Map.keysSet sol = error "variables mismatch"     | otherwise = array (1, x_max) $         [(x, val) | (var, Integer.Expr s) <- Map.toList vmap, (x, val) <- f s (sol Map.! var)] ++@@ -343,60 +349,45 @@       f :: SAT.PBSum -> Rational -> [(SAT.Var, Bool)]       f s val         | denominator val /= 1 = error "value should be integer"-        | otherwise = g (numerator val - sum [c | (c, []) <- s]) (Map.toDescList tmp)+        | otherwise =+            case SubsetSum.subsetSum (V.fromList (map fst s')) d of+              Nothing -> error "failed to reconstruct boolean assignment"+              Just sol -> [if l > 0 then (l, v) else (- l, not v) | (l, v) <- zip (map snd s') (VG.toList sol)]         where-          tmp :: Map Integer SAT.Var-          tmp =-            Map.fromList-            [ if c < 0 then-                error "coefficient should be non-negative"-              else if length ls > 1 then-                error "variable definition should be linear"-              else-                (c, head ls)-            | (c, ls) <- s, not (null ls), c /= 0-            ]--          g :: Integer -> [(Integer, SAT.Var)] -> [(SAT.Var, Bool)]-          g 0 [] = []-          g _ [] = error "no more variables"-          g v ((c,l) : ys)-            | v >= c    = (l, True)  : g (v - c) ys-            | otherwise = (l, False) : g v ys+          s' = [if null ls then (c, l) else error "variable definition should be linear" | (c, l : ls) <- s]+          d = numerator val - sum [c | (c, []) <- s]  instance BackwardTransformer IP2PBInfo where-  transformBackward (IP2PBInfo vmap _nonZeroTable _d) m = fmap (toRational . Integer.eval m) vmap+  transformBackward (IP2PBInfo vmap _nonZeroTable _s) m = fmap (toRational . Integer.eval m) vmap  instance ObjValueTransformer IP2PBInfo where   type SourceObjValue IP2PBInfo = Rational   type TargetObjValue IP2PBInfo = Integer  instance ObjValueForwardTransformer IP2PBInfo where-  transformObjValueForward (IP2PBInfo _vmap _nonZeroTable d) val = asInteger (val * fromIntegral d)+  transformObjValueForward (IP2PBInfo _vmap _nonZeroTable s) val = asInteger (val * s)  instance ObjValueBackwardTransformer IP2PBInfo where-  transformObjValueBackward (IP2PBInfo _vmap _nonZeroTable d) val = fromIntegral val / fromIntegral d+  transformObjValueBackward (IP2PBInfo _vmap _nonZeroTable s) val = fromIntegral val / s  instance J.ToJSON IP2PBInfo where-  toJSON (IP2PBInfo vmap nonZeroTable d) =+  toJSON (IP2PBInfo vmap nonZeroTable s) =     J.object     [ "type" .= ("IP2PBInfo" :: J.Value)     , "substitutions" .= J.object-        [ toKey (MIP.varName v) .= jPBSum s+        [ Key.fromText (MIP.varName v) .= jPBSum s         | (v, Integer.Expr s) <- Map.toList vmap         ]     , "nonzero_indicators" .= J.object-        [ toKey (MIP.varName v) .= (jLitName lit :: J.Value)+        [ Key.fromText (MIP.varName v) .= (jLitName lit :: J.Value)         | (v, lit) <- Map.toList nonZeroTable         ]-    , "objective_function_scale_factor" .= d+    , "objective_function_scale_factor" .=+        J.object+        [ "numerator" .= numerator s+        , "denominator" .= denominator s+        ]     ]-    where-#if MIN_VERSION_aeson(2,0,0)-      toKey = Key.fromText-#else-      toKey = id-#endif  instance J.FromJSON IP2PBInfo where   parseJSON = withTypedObject "IP2PBInfo" $ \obj -> do@@ -408,107 +399,146 @@     nonZeroTable <- liftM Map.fromList $ forM (Map.toList tmp2) $ \(name, s) -> do       lit <- parseLitName s       return (MIP.Var name, lit)-    d <- obj .: "objective_function_scale_factor"-    pure $ IP2PBInfo subst nonZeroTable d+    v <- obj .: "objective_function_scale_factor"+    s <- fmap fromInteger (J.parseJSON v) `mplus` parseRat v+    pure $ IP2PBInfo subst nonZeroTable s+    where+      parseRat = J.withObject "Rational" $ \obj -> (%)+        <$> obj .: "numerator"+        <*> obj .: "denominator"  addMIP :: (SAT.AddPBNL m enc, PrimMonad m) => enc -> MIP.Problem Rational -> m (Either String (Integer.Expr, IP2PBInfo)) addMIP enc mip = runExceptT $ addMIP' enc mip  addMIP' :: forall m enc. (SAT.AddPBNL m enc, PrimMonad m) => enc -> MIP.Problem Rational -> ExceptT String m (Integer.Expr, IP2PBInfo) addMIP' enc mip = do-  if not (Set.null nivs) then do-    throwE $ "cannot handle non-integer variables: " ++ intercalate ", " (map (T.unpack . MIP.varName) (Set.toList nivs))-  else do-    vmap <- liftM Map.fromList $ revForM (Set.toList ivs) $ \v -> do-      case MIP.getBounds mip v of-        (MIP.Finite lb, MIP.Finite ub) -> do-          v2 <- lift $ Integer.newVar enc (ceiling lb) (floor ub)+  let contVars = Map.filter p (MIP.varDomains mip)+        where+          p (MIP.ContinuousVariable, _) = True+          p (MIP.SemiContinuousVariable, _) = True+          p (_, _) = False+  unless (Map.null contVars) $ do+    let n = Map.size contVars+        vars = intercalate ", " (map (T.unpack . MIP.varName) (take 10 (Map.keys contVars)) ++ ["..." | n > 10])+        msg = printf "Unsupported problem: %d (semi-)continuous variables (%s)" n vars+    throwE msg++  let unboundedVars = Map.filter p (MIP.varDomains mip)+        where+          p (_, (MIP.Finite _, MIP.Finite _)) = False+          p (_, _) = True+  unless (Map.null unboundedVars) $ do+    let n = Map.size unboundedVars+        vars = intercalate ", " (map (T.unpack . MIP.varName) (take 10 (Map.keys unboundedVars)) ++ ["..." | n > 10])+        msg = printf "Unsupported problem: %d unbounded variables (%s)" n vars+    throwE msg++  nonZeroTableRef <- lift $ newMutVar Map.empty++  vmap <- fmap Map.fromDistinctAscList $ forM (Map.toAscList (MIP.varDomains mip)) $ \(v, dom) ->+    case dom of+      (vt, (MIP.Finite lb, MIP.Finite ub)) -> do+        let lb' = ceiling lb+            ub' = floor ub+        if vt == MIP.IntegerVariable || lb' <= 0 && 0 <= ub' then do+          v2 <- lift $ Integer.newVar enc lb' ub'           return (v,v2)-        _ -> do-          throwE $ "cannot handle unbounded variable: " ++ T.unpack (MIP.varName v)-    forM_ (MIP.constraints mip) $ \c -> do-      let lhs = MIP.constrExpr c-      let f op rhs = do-            let d = foldl' lcm 1 (map denominator  (rhs:[r | MIP.Term r _ <- MIP.terms lhs]))-                lhs' = sumV [asInteger (r * fromIntegral d) *^ product [vmap Map.! v | v <- vs] | MIP.Term r vs <- MIP.terms lhs]-                rhs' = asInteger (rhs * fromIntegral d)-                c2 = case op of-                       MIP.Le  -> lhs' .<=. fromInteger rhs'-                       MIP.Ge  -> lhs' .>=. fromInteger rhs'-                       MIP.Eql -> lhs' .==. fromInteger rhs'-            case MIP.constrIndicator c of-              Nothing -> lift $ Integer.addConstraint enc c2-              Just (var, val) -> do-                let var' = asBin (vmap Map.! var)-                case val of-                  1 -> lift $ Integer.addConstraintSoft enc var' c2-                  0 -> lift $ Integer.addConstraintSoft enc (SAT.litNot var') c2-                  _ -> return ()-          g = do-            case MIP.constrIndicator c of-              Nothing -> lift $ SAT.addClause enc []-              Just (var, val) -> do-                let var' = asBin (vmap Map.! var)-                case val of-                  1 -> lift $ SAT.addClause enc [- var']-                  0 -> lift $ SAT.addClause enc [var']-                  _ -> return ()-      case (MIP.constrLB c, MIP.constrUB c) of-        (MIP.Finite x1, MIP.Finite x2) | x1==x2 -> f MIP.Eql x2-        (lb, ub) -> do-          case lb of-            MIP.NegInf -> return ()-            MIP.Finite x -> f MIP.Ge x-            MIP.PosInf -> g-          case ub of-            MIP.NegInf -> g-            MIP.Finite x -> f MIP.Le x-            MIP.PosInf -> return ()+        else do+          -- vt == MIP.IntegerVariable && (0 <= lb' || ub' <= 0)+          v2@(Integer.Expr s) <- lift $ Integer.newVar enc (min 0 lb') (max 0 ub')+          lift $ do+            y <- SAT.newVar enc+            SAT.addPBNLAtLeast enc (s ++ [(- lb', [y])]) 0+            SAT.addPBNLAtMost enc (s ++ [(- ub', [y])]) 0+            modifyMutVar nonZeroTableRef (Map.insert v y)+          return (v,v2)+      _ -> error "should not happen" -    nonZeroTableRef <- lift $ newMutVar Map.empty-    let isNonZero :: MIP.Var -> ExceptT String m SAT.Lit-        isNonZero v = do-          tbl <- lift $ readMutVar nonZeroTableRef-          case Map.lookup v tbl of-            Just lit -> pure lit-            Nothing -> do-              let (MIP.Finite lb, MIP.Finite ub) = MIP.getBounds mip v-                  e@(Integer.Expr s) = vmap Map.! v-              lit <--                if lb == 0 && ub == 1 then do-                  return (asBin e)-                else do-                  v <- lift $ SAT.newVar enc-                  -- F(v) → F(s ≠ 0)-                  -- ⇐ s≠0 → v-                  -- ⇔ ¬v → s=0-                  lift $ SAT.addPBNLExactlySoft enc (- v) s 0-                  return v-              lift $ writeMutVar nonZeroTableRef (Map.insert v lit tbl)-              pure lit+  forM_ (MIP.constraints mip) $ \c -> do+    let lhs = MIP.constrExpr c+    let f op rhs = do+          let m = foldl' lcm 1 (map denominator (rhs:[r | MIP.Term r _ <- MIP.terms lhs]))+              d = foldl1' gcd (map (abs . numerator) (rhs:[r | MIP.Term r _ <- MIP.terms lhs]))+              -- For ease of understanding, no scaling is performed if the values were already integers+              s = if m == 1 then 1 else m % d+              lhs' = sumV [asInteger (r * s) *^ product [vmap Map.! v | v <- vs] | MIP.Term r vs <- MIP.terms lhs]+              rhs' = asInteger (rhs * s)+              c2 = case op of+                     MIP.Le  -> lhs' .<=. fromInteger rhs'+                     MIP.Ge  -> lhs' .>=. fromInteger rhs'+                     MIP.Eql -> lhs' .==. fromInteger rhs'+          case MIP.constrIndicator c of+            Nothing -> lift $ Integer.addConstraint enc c2+            Just (var, val) -> do+              let var' = asBin (vmap Map.! var)+              case val of+                1 -> lift $ Integer.addConstraintSoft enc var' c2+                0 -> lift $ Integer.addConstraintSoft enc (SAT.litNot var') c2+                _ -> return ()+        g = do+          case MIP.constrIndicator c of+            Nothing -> lift $ SAT.addClause enc []+            Just (var, val) -> do+              let var' = asBin (vmap Map.! var)+              case val of+                1 -> lift $ SAT.addClause enc [- var']+                0 -> lift $ SAT.addClause enc [var']+                _ -> return ()+    case (MIP.constrLB c, MIP.constrUB c) of+      (MIP.Finite x1, MIP.Finite x2) | x1==x2 -> f MIP.Eql x2+      (lb, ub) -> do+        case lb of+          MIP.NegInf -> return ()+          MIP.Finite x -> f MIP.Ge x+          MIP.PosInf -> g+        case ub of+          MIP.NegInf -> g+          MIP.Finite x -> f MIP.Le x+          MIP.PosInf -> return () -    forM_ (MIP.sosConstraints mip) $ \MIP.SOSConstraint{ MIP.sosType = typ, MIP.sosBody = xs } -> do-      case typ of-        MIP.S1 -> do-          ys <- mapM (isNonZero . fst) xs-          lift $ SAT.addAtMost enc ys 1-        MIP.S2 -> do-          ys <- mapM (isNonZero . fst) $ sortBy (comparing snd) xs-          lift $ SAT.addSOS2 enc ys+  let isNonZero :: MIP.Var -> ExceptT String m SAT.Lit+      isNonZero v = do+        tbl <- lift $ readMutVar nonZeroTableRef+        case Map.lookup v tbl of+          Just lit -> pure lit+          Nothing -> do+            let (MIP.Finite lb, MIP.Finite ub) = MIP.getBounds mip v+                e@(Integer.Expr s) = vmap Map.! v+            lit <-+              if lb == 0 && ub == 1 then do+                return (asBin e)+              else do+                v <- lift $ SAT.newVar enc+                -- F(v) → F(s ≠ 0)+                -- ⇐ s≠0 → v+                -- ⇔ ¬v → s=0+                lift $ SAT.addPBNLExactlySoft enc (- v) s 0+                return v+            lift $ writeMutVar nonZeroTableRef (Map.insert v lit tbl)+            pure lit -    let obj = MIP.objectiveFunction mip-        d = foldl' lcm 1 [denominator r | MIP.Term r _ <- MIP.terms (MIP.objExpr obj)] *-            (if MIP.objDir obj == MIP.OptMin then 1 else -1)-        obj2 = sumV [asInteger (r * fromIntegral d) *^ product [vmap Map.! v | v <- vs] | MIP.Term r vs <- MIP.terms (MIP.objExpr obj)]+  forM_ (MIP.sosConstraints mip) $ \MIP.SOSConstraint{ MIP.sosType = typ, MIP.sosBody = xs } -> do+    case typ of+      MIP.S1 -> do+        ys <- mapM (isNonZero . fst) xs+        lift $ SAT.addAtMost enc ys 1+      MIP.S2 -> do+        ys <- mapM (isNonZero . fst) $ sortBy (comparing snd) xs+        lift $ SAT.addSOS2 enc ys -    nonZeroTable <- readMutVar nonZeroTableRef+  let obj = MIP.objectiveFunction mip+      m = foldl' lcm 1 [denominator r | MIP.Term r _ <- MIP.terms (MIP.objExpr obj)]+      d = if null (MIP.terms (MIP.objExpr obj)) then 1+          else foldl1' gcd [abs (numerator r) | MIP.Term r _ <- MIP.terms (MIP.objExpr obj)]+      -- For ease of understanding, no scaling is performed if the values were already integers+      s = (if MIP.objDir obj == MIP.OptMin then 1 else -1) * (if m == 1 then 1 else m % d)+      obj2 = sumV [asInteger (r * s) *^ product [vmap Map.! v | v <- vs] | MIP.Term r vs <- MIP.terms (MIP.objExpr obj)] -    return (obj2, IP2PBInfo vmap nonZeroTable d)+  nonZeroTable <- readMutVar nonZeroTableRef -  where-    ivs = MIP.integerVariables mip-    nivs = MIP.variables mip `Set.difference` ivs+  return (obj2, IP2PBInfo vmap nonZeroTable s) +  where     asBin :: Integer.Expr -> SAT.Lit     asBin (Integer.Expr [(1,[lit])]) = lit     asBin _ = error "asBin: failure"@@ -517,5 +547,60 @@ asInteger r   | denominator r /= 1 = error (show r ++ " is not integer")   | otherwise = numerator r++-- -----------------------------------------------------------------------------++normalizeMIPObjective :: (Num c, Eq c) => MIP.Problem c -> (MIP.Problem c, NormalizeMIPObjectiveInfo r)+normalizeMIPObjective prob@MIP.Problem{ MIP.objectiveFunction = obj }+  | offset == 0 = (prob{ MIP.objectiveFunction = obj{ MIP.objExpr = e }}, NormalizeMIPObjectiveInfo Nothing)+  | otherwise =+      ( prob+        { MIP.objectiveFunction = obj{ MIP.objExpr = e + MIP.Expr [MIP.Term offset [unit_var]] }+        , MIP.varDomains = Map.insert unit_var (MIP.IntegerVariable, (MIP.Finite 1, MIP.Finite 1)) (MIP.varDomains prob)+        }+      , NormalizeMIPObjectiveInfo (Just unit_var)+      )+  where+    offset = sum [c | MIP.Term c [] <- MIP.terms (MIP.objExpr obj)]+    e = MIP.Expr [t | t@(MIP.Term _ (_:_)) <- MIP.terms (MIP.objExpr obj)]+    used = MIP.variables prob+    candidates = map MIP.Var $ "unit" : [T.pack ("unit" ++ show i) | i <- [(1::Int)..]]+    unit_var = head [name | name <- candidates, name `Set.notMember` used]++newtype NormalizeMIPObjectiveInfo r = NormalizeMIPObjectiveInfo (Maybe MIP.Var)+  deriving (Eq, Show)++instance Transformer (NormalizeMIPObjectiveInfo r) where+  type Source (NormalizeMIPObjectiveInfo r) = Map MIP.Var r+  type Target (NormalizeMIPObjectiveInfo r) = Map MIP.Var r++instance Num r => ForwardTransformer (NormalizeMIPObjectiveInfo r) where+  transformForward (NormalizeMIPObjectiveInfo Nothing) sol = sol+  transformForward (NormalizeMIPObjectiveInfo (Just v)) sol = Map.insert v 1 sol++instance BackwardTransformer (NormalizeMIPObjectiveInfo r) where+  transformBackward (NormalizeMIPObjectiveInfo Nothing) sol = sol+  transformBackward (NormalizeMIPObjectiveInfo (Just v)) sol = Map.delete v sol++instance ObjValueTransformer (NormalizeMIPObjectiveInfo r) where+  type SourceObjValue (NormalizeMIPObjectiveInfo r) = r+  type TargetObjValue (NormalizeMIPObjectiveInfo r) = r++instance ObjValueForwardTransformer (NormalizeMIPObjectiveInfo r) where+  transformObjValueForward (NormalizeMIPObjectiveInfo _) val = val++instance ObjValueBackwardTransformer (NormalizeMIPObjectiveInfo r) where+  transformObjValueBackward (NormalizeMIPObjectiveInfo _) val = val++instance J.ToJSON (NormalizeMIPObjectiveInfo r) where+  toJSON (NormalizeMIPObjectiveInfo m) =+    J.object+    [ "type" .= ("NormalizeMIPObjectiveInfo" :: J.Value)+    , "unit_var" .= fmap MIP.varName m+    ]++instance J.FromJSON (NormalizeMIPObjectiveInfo r) where+  parseJSON = withTypedObject "NormalizeMIPObjectiveInfo" $ \obj -> do+    (NormalizeMIPObjectiveInfo . fmap MIP.Var) <$> obj .: "unit_var"  -- -----------------------------------------------------------------------------

@@ -22,7 +22,7 @@ import Data.Char import Data.Default.Class import Data.Ord-import Data.List+import Data.List (intersperse, sortBy) import Data.Ratio import qualified Data.Set as Set import Data.Map (Map)

@@ -85,7 +85,6 @@ import qualified Data.Aeson as J import Data.Aeson ((.=), (.:)) import Data.Array.IArray-import Data.Bits hiding (And (..)) import Data.ByteString.Builder import Data.Default.Class import qualified Data.Foldable as F@@ -93,7 +92,7 @@ import qualified Data.IntMap.Strict as IntMap import Data.IntSet (IntSet) import qualified Data.IntSet as IntSet-import Data.List+import Data.List (foldl', foldl1', intersperse) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Data.Maybe@@ -102,13 +101,18 @@ import Data.Set (Set) import qualified Data.Set as Set import qualified Data.PseudoBoolean as PBFile+import qualified Data.Vector as V+import qualified Data.Vector.Generic as VG +import ToySolver.Data.Boolean (true) import ToySolver.Converter.Base+import qualified ToySolver.Combinatorial.SubsetSum as SubsetSum import qualified ToySolver.Converter.PB.Internal.Product as Product import ToySolver.Converter.Tseitin import qualified ToySolver.FileFormat.CNF as CNF import ToySolver.Internal.JSON import qualified ToySolver.SAT.Types as SAT+import qualified ToySolver.SAT.Encoder.Integer as Integer import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin import ToySolver.SAT.Encoder.Tseitin (Formula (..)) import qualified ToySolver.SAT.Encoder.PB as PB@@ -119,21 +123,59 @@  -- ----------------------------------------------------------------------------- --- XXX: we do not normalize objective function, because normalization might--- introduce constant terms, but OPB file format does not allow constant terms.+-- | Normalize 'PBFile.Formula' to be suitable for writing as OPB file. ----- Options:--- (1) not normalize objective function (current implementation),--- (2) normalize and simply delete constant terms (in pseudo-boolean package?),--- (3) normalize and introduce dummy variable to make constant terms---     into non-constant terms (in pseudo-boolean package?).-normalizePB :: PBFile.Formula -> PBFile.Formula+-- This may introduce a new variable.+normalizePB :: PBFile.Formula -> (PBFile.Formula, PBTseitinInfo) normalizePB formula =-  formula-  { PBFile.pbConstraints =-      map normalizePBConstraint (PBFile.pbConstraints formula)-  }+  case PBFile.pbObjectiveFunction formula of+    Nothing ->+      ( formula{ PBFile.pbConstraints = cs }+      , PBTseitinInfo (TseitinInfo nv nv IntMap.empty)+      )+    Just obj | (obj', offset) <- normalizePBSum obj ->+      if offset == 0 then+        ( formula+          { PBFile.pbObjectiveFunction = Just obj'+          , PBFile.pbConstraints = cs+          }+        , PBTseitinInfo (TseitinInfo nv nv IntMap.empty)+        )+      else+        case msum [detectTrueVar c | c <- cs] of+          Just v ->+            ( formula+              { PBFile.pbObjectiveFunction = Just (obj' ++ [(offset, [v])])+              , PBFile.pbConstraints = cs+              }+            , PBTseitinInfo (TseitinInfo nv nv IntMap.empty)+            )+          Nothing ->+            let v = nv + 1+             in ( formula+                  { PBFile.pbObjectiveFunction = Just (obj' ++ [(offset, [v])])+                  , PBFile.pbConstraints = cs ++ [([(1, [v])], PBFile.Ge, 1)]+                  , PBFile.pbNumVars = v+                  }+                , PBTseitinInfo (TseitinInfo nv v (IntMap.singleton v true))+                )+  where+    cs = map normalizePBConstraint (PBFile.pbConstraints formula)+    nv = PBFile.pbNumVars formula +detectTrueVar :: PBFile.Constraint -> Maybe SAT.Var+detectTrueVar (lhs, op, rhs) =+  case op of+    PBFile.Ge -> f lhs rhs+    PBFile.Eq -> f lhs rhs `mplus` f [(- c, ls) | (c,ls) <- lhs] (- rhs)+  where+    f [(c, ls)] rhs+      | c > 0 && (rhs + c - 1) `div` c >= 1 =+          -- c L ≥ rhs ↔ L ≥ ⌈rhs / c⌉+          listToMaybe [l | l <- ls, l > 0]+    f _ _ = Nothing++-- | Normalize 'PBFile.SoftFormula' to be suitable for writing as WBO file. normalizeWBO :: PBFile.SoftFormula -> PBFile.SoftFormula normalizeWBO formula =   formula@@ -143,11 +185,18 @@  normalizePBConstraint :: PBFile.Constraint -> PBFile.Constraint normalizePBConstraint (lhs,op,rhs) =-  case mapAccumL h 0 lhs of-    (offset, lhs') -> (lhs', op, rhs - offset)+  case normalizePBSum lhs of+    (lhs', offset) -> (lhs', op, rhs - offset)++normalizePBSum :: PBFile.Sum -> (PBFile.Sum, Integer)+normalizePBSum s =+  case foldl' h ([], 0) s of+    (s', offset) -> (reverse s', offset)   where-    h s (w,[x]) | x < 0 = (s+w, (-w,[-x]))-    h s t = (s,t)+    h (s', offset) (0,_) = (s', offset)+    h (s', offset) (w,[x]) | x < 0 = ((-w,[-x]) : s', offset+w)+    h (s', offset) (w,[]) = (s', offset + w)+    h (s', offset) t = (t : s', offset)  -- ----------------------------------------------------------------------------- @@ -403,7 +452,7 @@  -- ----------------------------------------------------------------------------- --- | Convert inequality constraints into equality constraints by introducing surpass variables.+-- | Convert inequality constraints into equality constraints by introducing surplus variables. inequalitiesToEqualitiesPB :: PBFile.Formula -> (PBFile.Formula, PBInequalitiesToEqualitiesInfo) inequalitiesToEqualitiesPB formula = runST $ do   db <- newPBStore@@ -419,17 +468,20 @@           Just clause -> do             SAT.addPBNLExactly db [(1, [- l | l <- clause])] 0             return Nothing-          Nothing -> do-            let maxSurpass = max (SAT.pbUpperBound lhs - rhs) 0-                maxSurpassNBits = head [i | i <- [0..], maxSurpass < bit i]-            vs <- SAT.newVars db maxSurpassNBits-            SAT.addPBNLExactly db (lhs ++ [(-c,[x]) | (c,x) <- zip (iterate (*2) 1) vs]) rhs-            if maxSurpassNBits > 0 then do-              return $ Just (lhs, rhs, vs)-            else-              return Nothing+          Nothing+            | SAT.pbLowerBound lhs > rhs -> return Nothing+            | otherwise -> do+                let (lhs', rhs') = simplifyPBAtLeast (lhs, rhs)+                    maxSurplus = max (SAT.pbUpperBound lhs' - rhs') 0+                surplus <- Integer.newVarPBLinSum db maxSurplus+                SAT.addPBNLExactly db (lhs' ++ [(-c,[l]) | (c,l) <- surplus]) rhs'+                if maxSurplus > 0 then do+                  return $ Just (lhs', rhs', surplus)+                else+                  return Nothing    formula' <- getPBFormula db+  unless (all (\(_, op, _) -> op == PBFile.Eq) (PBFile.pbConstraints formula')) $ error "should not happen"   return     ( formula'{ PBFile.pbObjectiveFunction = PBFile.pbObjectiveFunction formula }     , PBInequalitiesToEqualitiesInfo (PBFile.pbNumVars formula) (PBFile.pbNumVars formula') defs@@ -452,8 +504,21 @@         (lhs'', 1) | all (\(c,_) -> c == 1) lhs'' -> return (map snd lhs'')         _ -> mzero +    simplifyPBAtLeast :: (SAT.PBSum, Integer) -> (SAT.PBSum, Integer)+    simplifyPBAtLeast (lhs, rhs) =+      case splitConst lhs of+        (lhs', offset) ->+          let rhs' = rhs - offset+              d = case lhs' of+                    [] -> 1+                    _ -> abs $ foldl1' gcd (map fst lhs')+           in ([(c `div` d, ls) | (c,ls) <- lhs'], (rhs' + d - 1) `div` d)++    splitConst :: SAT.PBSum -> (SAT.PBSum, Integer)+    splitConst s = ([t | t@(c, _:_) <- s, c /= 0], sum [c | (c, []) <- s])+ data PBInequalitiesToEqualitiesInfo-  = PBInequalitiesToEqualitiesInfo !Int !Int [(PBFile.Sum, Integer, [SAT.Var])]+  = PBInequalitiesToEqualitiesInfo !Int !Int [(PBFile.Sum, Integer, SAT.PBLinSum)]   deriving (Eq, Show)  instance Transformer PBInequalitiesToEqualitiesInfo where@@ -462,7 +527,16 @@  instance ForwardTransformer PBInequalitiesToEqualitiesInfo where   transformForward (PBInequalitiesToEqualitiesInfo _nv1 nv2 defs) m =-    array (1, nv2) $ assocs m ++ [(v, testBit n i) | (lhs, rhs, vs) <- defs, let n = SAT.evalPBSum m lhs - rhs, (i,v) <- zip [0..] vs]+    array (1, nv2) $ assocs m ++ concat+      [ if lhsVal >= rhs then+          case SubsetSum.subsetSum (V.fromList (map fst surplus)) (lhsVal - rhs) of+            Nothing -> error ("failed to construct surplus assignment")+            Just sol -> [if l > 0 then (l, v) else (- l, not v) | (l, v) <- zip (map snd surplus) (VG.toList sol)]+        else+          [if l > 0 then (l, False) else (-l, True) | (_, l) <- surplus]+      | (lhs, rhs, surplus) <- defs+      , let lhsVal = SAT.evalPBSum m lhs+      ]  instance BackwardTransformer PBInequalitiesToEqualitiesInfo where   transformBackward (PBInequalitiesToEqualitiesInfo nv1 _nv2 _defs) = SAT.restrictModel nv1@@ -483,13 +557,13 @@     [ "type" .= ("PBInequalitiesToEqualitiesInfo" :: J.Value)     , "num_original_variables" .= nv1     , "num_transformed_variables" .= nv2-    , "slack" .=+    , "definitions" .=         [ J.object           [ "lhs" .= jPBSum lhs           , "rhs" .= rhs-          , "slack" .= [jVarName v :: J.Value | v <- vs]+          , "surplus" .= jPBLinSum surplus           ]-        | (lhs, rhs, vs) <- defs+        | (lhs, rhs, surplus) <- defs         ]     ] @@ -498,15 +572,13 @@     PBInequalitiesToEqualitiesInfo       <$> obj .: "num_original_variables"       <*> obj .: "num_transformed_variables"-      <*> (mapM f =<< obj .: "slack")+      <*> (mapM f =<< obj .: "definitions")     where-      f = J.withObject "slack" $ \obj -> do+      f = J.withObject "definition" $ \obj -> do         lhs <- parsePBSum =<< obj .: "lhs"         rhs <- obj .: "rhs"-        vs <- mapM g =<< obj .: "slack"-        return (lhs, rhs, vs)-      g ('x' : rest) = pure $! read rest-      g s = fail ("fail to parse variable: " ++ show s)+        surplus <- parsePBLinSum =<< obj .: "surplus"+        return (lhs, rhs, surplus)  -- ----------------------------------------------------------------------------- @@ -569,14 +641,26 @@     p = obj1ub - obj1lb + 1     obj2 = [(p*c, IntSet.toList ls) | (ls, c) <- Map.toList obj2', c /= 0]     obj2' = Map.unionsWith (+) [sq ((-rhs, []) : lhs) | (lhs, PBFile.Eq, rhs) <- PBFile.pbConstraints formula]-    sq ts = Map.fromListWith (+) $ do-              (c1,ls1) <- ts-              (c2,ls2) <- ts-              let ls3 = IntSet.fromList ls1 `IntSet.union` IntSet.fromList ls2-              guard $ not $ isFalse ls3-              return (ls3, c1*c2)-    isFalse ls = not $ IntSet.null $ ls `IntSet.intersection` IntSet.map negate ls+    sq ts = Map.unionWith (+) sq1 sq2+      where+        ts' = [ (c, ls', neg, pos)+              | (c, ls) <- ts, c /= 0+              , let ls' = IntSet.fromList ls, let (neg, pos) = IntSet.split 0 ls'+              , not (contradict neg pos)+              ]+        sq1 = Map.fromListWith (+) [(ls, c^(2::Int)) | (c, ls, _, _) <- ts']+        sq2 = Map.fromListWith (+) $ do+          ((c1, ls1, neg1, pos1), (c2, ls2, neg2, pos2)) <- pairs ts'+          guard $ not $ contradict neg1 pos2+          guard $ not $ contradict neg2 pos1+          return (ls1 `IntSet.union` ls2, 2*c1*c2)+    contradict ls1 ls2 =+      not $ IntSet.null $ IntSet.fromAscList (map negate (IntSet.toDescList ls1)) `IntSet.intersection` ls2 +pairs :: [a] -> [(a, a)]+pairs [] = []+pairs (x:xs) = [(x,y) | y <- xs] ++ pairs xs+ -- -----------------------------------------------------------------------------  pb2qubo' :: PBFile.Formula -> ((PBFile.Formula, Integer), PB2QUBOInfo')@@ -716,7 +800,6 @@   objRef <- newMutVar []   objOffsetRef <- newMutVar 0   defsRef <- newMutVar []-  trueLitRef <- newMutVar SAT.litUndef    forM_ (PBFile.wboConstraints wbo) $ \(cost, constr@(lhs,op,rhs)) -> do     case cost of@@ -724,11 +807,6 @@         case op of           PBFile.Ge -> SAT.addPBNLAtLeast db lhs rhs           PBFile.Eq -> SAT.addPBNLExactly db lhs rhs-        trueLit <- readMutVar trueLitRef-        when (trueLit == SAT.litUndef) $ do-          case detectTrueLit constr of-            Nothing -> return ()-            Just l -> writeMutVar trueLitRef l       Just w -> do         case op of           PBFile.Ge -> do@@ -767,42 +845,17 @@             modifyMutVar defsRef ((sel,constr) :)    offset <- readMutVar objOffsetRef-  when (offset /= 0) $ do-    l <- readMutVar trueLitRef-    trueLit <--      if l /= SAT.litUndef then-        return l-      else do-        v <- SAT.newVar db-        SAT.addClause db [v]-        modifyMutVar defsRef ((v, ([], PBFile.Ge, 0)) :)-        return v-    modifyMutVar objRef ((offset,[trueLit]) :)+  when (offset /= 0) $ modifyMutVar objRef ((offset,[]) :)    obj <- liftM reverse $ readMutVar objRef   defs <- liftM IntMap.fromList $ readMutVar defsRef    case PBFile.wboTopCost wbo of-    Nothing -> return ()-    Just t -> SAT.addPBNLAtMost db obj (t - 1)+    Just t | t <= sum [w | (Just w, _) <- PBFile.wboConstraints wbo] -> SAT.addPBNLAtMost db obj (t - 1)+    _ -> return ()    return (obj, defs) --detectTrueLit :: PBFile.Constraint -> Maybe SAT.Lit-detectTrueLit (lhs, op, rhs) =-  case op of-    PBFile.Ge -> f lhs rhs-    PBFile.Eq -> f lhs rhs `mplus` f [(- c, ls) | (c,ls) <- lhs] (- rhs)-  where-    f [(c, [l])] rhs-      | c > 0 && (rhs + c - 1) `div` c == 1 =-          -- c l ≥ rhs ↔ l ≥ ⌈rhs / c⌉-          return l-      | c < 0 && rhs `div` c == 0 =-          -- c l ≥ rhs ↔ l ≤ ⌊rhs / c⌋-          return (- l)-    f _ _ = Nothing  -- ----------------------------------------------------------------------------- 

@@ -16,10 +16,9 @@  import Data.IntSet (IntSet) import qualified Data.IntSet as IntSet-import Data.List hiding (insert)+import Data.List (foldl', sortOn) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map-import Data.Ord import Data.Set (Set) import qualified Data.Set as Set @@ -31,7 +30,7 @@ decompose1 :: Set IntSet -> Map IntSet (Maybe (IntSet,IntSet)) decompose1 ss = snd $ foldl' (flip f) (LargestIntersectionFinder.empty, Map.empty) ss'   where-    ss' = map fst $ sortBy (comparing snd) [(s, IntSet.size s) | s <- Set.toList ss]+    ss' = sortOn IntSet.size (Set.toList ss)      f :: IntSet       -> (LargestIntersectionFinder.Table, Map IntSet (Maybe (IntSet,IntSet)))

@@ -38,7 +38,7 @@ import Data.Array.Unboxed import Data.IntMap.Strict (IntMap) import qualified Data.IntMap.Strict as IntMap-import Data.List+import Data.List (foldl') import Data.Maybe import qualified Data.PseudoBoolean as PBFile import Data.Ratio

@@ -102,11 +102,9 @@ instance ForwardTransformer SAT3ToISInfo where   transformForward (SAT3ToISInfo _nv clusters nodeToLit) m = IntSet.fromList $ do     nodes <- clusters-    let xs = [node | node <- nodes, SAT.evalLit m (nodeToLit ! node)]-    if null xs then-      error "not a model"-    else-      return (head xs)+    case [node | node <- nodes, SAT.evalLit m (nodeToLit ! node)] of+      [] -> error "not a model"+      x : _ -> return x  instance BackwardTransformer SAT3ToISInfo where   transformBackward (SAT3ToISInfo nv _clusters nodeToLit) indep_set = runSTUArray $ do

@@ -50,7 +50,7 @@  import Control.Exception (assert) import Control.Monad-import Data.List+import Data.List (delete, elemIndex, sort) import Data.Ratio import qualified Data.Set as Set import qualified Text.PrettyPrint.HughesPJClass as PP

@@ -20,7 +20,7 @@ ----------------------------------------------------------------------------- module ToySolver.Data.AlgebraicNumber.Root where -import Data.List+import Data.List (inits) import Data.Maybe import Data.Map (Map) import qualified Data.Map as Map

@@ -1,7 +1,7 @@ ----------------------------------------------------------------------------- -- | -- Module      :  ToySolver.Data.AlgebraicNumber.Sturm--- Copyright   :  (c) Masahiro Sakai 2012+-- Copyright   :  (c) Masahiro Sakai 2012-2026 -- License     :  BSD-style -- -- Maintainer  :  masahiro.sakai@gmail.com@@ -31,6 +31,8 @@   , narrow'   , approx   , approx'++  , cauchysBounds   ) where  import Data.Maybe@@ -95,14 +97,21 @@       | otherwise = go x2 xs (r+1)  -- | Closed interval that contains all real roots of a given polynomial.--- 根の限界--- <http://aozoragakuen.sakura.ne.jp/taiwa/taiwaNch02/node26.html>+--+-- Currently Cauchy's bounds ('cauchysBounds') is used. bounds :: UPolynomial Rational -> (Rational, Rational) bounds p = (-m, m)   where-    m = if p==0-        then 0-        else max 1 (sum [abs (c/s) | (c,_) <- P.terms p] - 1)+    m = cauchysBounds p++-- | Cauchy's upper bounds for the magnitudes of all roots+--+-- <https://en.wikipedia.org/wiki/Geometrical_properties_of_polynomial_roots>+cauchysBounds :: UPolynomial Rational -> Rational+cauchysBounds p+  | P.deg p == 0 = 0+  | otherwise = 1 + maximum (0 : [abs (c/s) | (c,xs) <- P.terms p, P.deg xs /= P.deg p])+  where     s = P.lc P.nat p  boundInterval :: UPolynomial Rational -> Interval Rational -> Interval Rational

@@ -44,7 +44,7 @@   | Imply (BoolExpr a) (BoolExpr a)   | Equiv (BoolExpr a) (BoolExpr a)   | ITE (BoolExpr a) (BoolExpr a) (BoolExpr a)-  deriving (Eq, Ord, Show, Read, Typeable, Data)+  deriving (Eq, Ord, Show, Read, Data)  instance Functor BoolExpr where   fmap = fmapDefault

@@ -65,7 +65,7 @@  import Control.Monad import Control.DeepSeq-import Data.List+import Data.List (intersperse) import Data.Maybe import Data.IntMap.Strict (IntMap) import qualified Data.IntMap.Strict as IntMap

@@ -20,7 +20,7 @@   , toConstraints   ) where -import Data.List+import Data.List (foldl', transpose) import Data.Ratio import qualified Data.IntSet as IntSet import Data.Map (Map)@@ -52,16 +52,13 @@   vars (Polyhedron m) = IntSet.unions [vars e | e <- Map.keys m]   vars Empty = IntSet.empty -instance JoinSemiLattice Polyhedron where-  join Empty b = b-  join a Empty = a-  join (Polyhedron m1) (Polyhedron m2) =-    normalize $ Polyhedron (Map.intersectionWith Interval.join m1 m2)--instance MeetSemiLattice Polyhedron where-  meet = intersection+instance Lattice Polyhedron where+  Empty \/ b = b+  a \/ Empty = a+  Polyhedron m1 \/ Polyhedron m2 =+    normalize $ Polyhedron (Map.intersectionWith Interval.hull m1 m2) -instance Lattice Polyhedron+  (/\) = intersection  instance BoundedJoinSemiLattice Polyhedron where   bottom = empty@@ -69,8 +66,6 @@ instance BoundedMeetSemiLattice Polyhedron where   top = univ -instance BoundedLattice Polyhedron- normalize :: Polyhedron -> Polyhedron normalize (Polyhedron m) | any Interval.null (Map.elems m) = Empty normalize p = p@@ -96,10 +91,10 @@   map (foldl' intersection univ) $ transpose $ map fromAtom cs  fromAtom :: AtomR  -> [Polyhedron]-fromAtom (Rel lhs NEq rhs) =+fromAtom (OrdRel lhs NEq rhs) =   fromAtom (lhs .<. rhs) ++ fromAtom (lhs .>. rhs)-fromAtom (Rel lhs op rhs) =-  case LA.extract LA.unitVar (lhs .-. rhs) of+fromAtom (OrdRel lhs op rhs) =+  case LA.extract LA.unitVar (lhs ^-^ rhs) of     (c, e1) ->       case toRat e1 of         (lhs1, d) ->@@ -110,10 +105,10 @@                 else (lhs1, op, rhs1)               ival =                 case op of-                  Lt  -> Interval.interval Nothing (Just (False, rhs2))-                  Le  -> Interval.interval Nothing (Just (True, rhs2))-                  Ge  -> Interval.interval (Just (True, rhs2)) Nothing-                  Gt  -> Interval.interval (Just (False, rhs2)) Nothing+                  Lt  -> Interval.NegInf Interval.<..<  Interval.Finite rhs2+                  Le  -> Interval.NegInf Interval.<..<= Interval.Finite rhs2+                  Ge  -> Interval.Finite rhs2 Interval.<=..< Interval.PosInf+                  Gt  -> Interval.Finite rhs2 Interval.<..<  Interval.PosInf                   Eql -> Interval.singleton rhs2                   NEq -> error "should not happen"           in filter (Empty /=) [normalize $ Polyhedron (Map.singleton lhs2 ival)]@@ -124,14 +119,16 @@ toConstraints (Polyhedron m) = do   (e, ival) <- Map.toList m   let e' = LA.mapCoeff fromIntegral e-      xs = case Interval.lowerBound ival of-             Nothing -> []-             Just (True,c)  -> [LA.constant c .<=. e']-             Just (False,c) -> [LA.constant c .<.  e']-      ys = case Interval.upperBound ival of-             Nothing -> []-             Just (True,c)  -> [e' .<=. LA.constant c]-             Just (False,c) -> [e' .<.  LA.constant c]+      xs = case Interval.lowerBound' ival of+             (Interval.NegInf, _) -> []+             (Interval.PosInf, _) -> undefined+             (Interval.Finite c, Interval.Closed) -> [LA.constant c .<=. e']+             (Interval.Finite c, Interval.Open)   -> [LA.constant c .<.  e']+      ys = case Interval.upperBound' ival of+             (Interval.NegInf, _) -> undefined+             (Interval.PosInf, _) -> []+             (Interval.Finite c, Interval.Closed) -> [e' .<=. LA.constant c]+             (Interval.Finite c, Interval.Open)   -> [e' .<.  LA.constant c]   xs ++ ys  p :: ExprZ -> Bool

@@ -139,7 +139,8 @@ import qualified Data.FiniteField as FF import Data.Function import Data.Hashable-import Data.List+import Data.List (foldl', foldl1', intersperse, maximumBy, sortBy)+import qualified Data.List.NonEmpty as NonEmpty import Data.Numbers.Primes (primeFactors) import Data.Ratio import Data.String (IsString (..))@@ -175,7 +176,7 @@  -- | Polynomial over commutative ring r newtype Polynomial r v = Polynomial{ coeffMap :: Map (Monomial v) r }-  deriving (Eq, Ord, Typeable)+  deriving (Eq, Ord)  instance (Eq k, Num k, Ord v) => Num (Polynomial k v) where   (+)      = plus@@ -404,7 +405,7 @@ divModMP   :: forall k v. (Eq k, Fractional k, Ord v)   => MonomialOrder v -> Polynomial k v -> [Polynomial k v] -> ([Polynomial k v], Polynomial k v)-divModMP cmp p fs = go IntMap.empty (terms' p)+divModMP cmp p fs = go IntMap.empty [] (terms' p)   where     terms' :: Polynomial k v -> [Term k v]     terms' g = sortBy (flip cmp `on` snd) (terms g)@@ -421,20 +422,26 @@             0 -> merge xs ys             c -> (c, snd x) : merge xs ys -    ls = zip [0..] [(lt cmp f, terms' f) | f <- fs]+    -- For each divisor: its index, its leading term, and its remaining+    -- (lower) terms in descending order with respect to @cmp@.+    -- Zero divisors have no terms and are simply skipped.+    ls :: [(Int, Term k v, [Term k v])]+    ls = [(i, a, rest) | (i, f) <- zip [0..] fs, (a : rest) <- [terms' f]] -    go :: IntMap (Polynomial k v) -> [Term k v] -> ([Polynomial k v], Polynomial k v)-    go qs g =-      case xs of-        [] -> ([IntMap.findWithDefault 0 i qs | i <- [0 .. length fs - 1]], fromTerms g)-        (i, b, g') : _ -> go (IntMap.insertWith (+) i b qs) g'-      where-        xs = do-          (i,(a,f)) <- ls-          h <- g-          guard $ a `tdivides` h-          let b = tdiv h a-          return (i, fromTerm b, merge g [(tscale (-1) b `tmult` m) | m <- f])+    -- @g@ holds the terms of the dividend not yet processed, kept sorted in+    -- descending order with respect to @cmp@; @rs@ accumulates the terms of+    -- the remainder. At each step we look at the leading term @h@ of @g@ and+    -- either reduce it by a divisor or, if no divisor's leading term divides+    -- it, move it to the remainder.+    go :: IntMap (Polynomial k v) -> [Term k v] -> [Term k v]+       -> ([Polynomial k v], Polynomial k v)+    go qs rs [] = ([IntMap.findWithDefault 0 i qs | i <- [0 .. length fs - 1]], fromTerms rs)+    go qs rs (h : g) =+      case [(i, b, rest) | (i, a, rest) <- ls, a `tdivides` h, let b = tdiv h a] of+        [] -> go qs (h : rs) g+        (i, b, rest) : _ ->+          go (IntMap.insertWith (+) i (fromTerm b) qs) rs+             (merge g [tscale (-1) b `tmult` m | m <- rest])  -- | Multivariate division algorithm --@@ -445,7 +452,10 @@ reduce cmp p fs = go p   where     ls = [(lt cmp f, f) | f <- fs]-    go g = if null xs then g else go (head xs)+    go g =+      case xs of+       [] -> g+       x : _ -> go x       where         ms = sortBy (flip cmp `on` snd) (terms g)         xs = do@@ -486,7 +496,7 @@   | otherwise  = eisensteinsCriterion' (pp p)  eisensteinsCriterion' :: UPolynomial Integer -> Bool-eisensteinsCriterion' p = or [criterion prime | prime <- map head $ group $ primeFactors c]+eisensteinsCriterion' p = or [criterion prime | prime <- map NonEmpty.head $ NonEmpty.group $ primeFactors c]   where     Just ((_,an), ts) = Map.maxViewWithKey (coeffMap p)     a0 = coeff mone p@@ -615,7 +625,7 @@  -- | Variable "x" data X = X-  deriving (Eq, Ord, Bounded, Enum, Show, Read, Typeable, Data)+  deriving (Eq, Ord, Bounded, Enum, Show, Read, Data)  instance NFData X where    rnf a = a `seq` ()@@ -778,7 +788,7 @@  -- | Monic monomials newtype Monomial v = Monomial{ mindicesMap :: Map v Integer }-  deriving (Eq, Ord, Typeable)+  deriving (Eq, Ord)  type UMonomial = Monomial X 

@@ -34,7 +34,7 @@  import Control.Exception (assert) import Data.FiniteField-import Data.List+import Data.List (sortOn) import Data.Ord import Data.Set (Set) import qualified Data.Set as Set

@@ -21,7 +21,7 @@   ( factor   ) where -import Data.List+import Data.List (find) import Data.MultiSet (MultiSet) import qualified Data.MultiSet as MultiSet import Data.Numbers.Primes (primes)

@@ -28,7 +28,7 @@ import Control.Monad import Control.Monad.ST import Control.Exception (assert)-import Data.List+import Data.List ((\\)) import Data.Maybe import Data.Numbers.Primes (primes) import Data.Ratio

@@ -12,7 +12,7 @@ -- -- References: ----- * Lagrange polynomial <https://en.wikipedia.org/wiki/Hermite_interpolation>+-- * Hermite interpolation, <https://en.wikipedia.org/wiki/Hermite_interpolation> -- ----------------------------------------------------------------------------- module ToySolver.Data.Polynomial.Interpolation.Hermite

@@ -63,7 +63,7 @@ import Data.Interned (intern, unintern) import Data.Interned.Text import Data.IORef-import Data.List+import Data.List (intercalate) import Data.Maybe import Data.Map (Map) import qualified Data.Map as Map

@@ -1,7 +1,6 @@ {-# OPTIONS_GHC -Wall #-} {-# OPTIONS_HADDOCK show-extensions #-} {-# LANGUAGE CPP #-}-{-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE OverloadedStrings #-} ----------------------------------------------------------------------------- -- |@@ -22,6 +21,9 @@   , parseFile   , readFile   , writeFile++  -- * Utility functions+  , getBaseExtension   ) where  import Prelude hiding (readFile, writeFile)@@ -29,7 +31,7 @@ import Control.Monad.IO.Class import qualified Data.ByteString.Lazy.Char8 as BS import Data.ByteString.Builder hiding (writeFile)-import Data.Typeable+import Data.Char import System.IO hiding (readFile, writeFile)  #ifdef WITH_ZLIB@@ -48,7 +50,7 @@  -- | 'ParseError' represents a parse error and it wraps a error message. data ParseError = ParseError String-  deriving (Show, Typeable)+  deriving (Show)  instance Exception ParseError @@ -87,3 +89,16 @@ #else     hPutBuilder h (render a) #endif++-- | Get base extension of a filename+--+-- Supported compression format extensions (e.g. @.gz@) are removed, and extensions such as @.cnf@ are returned.+--+-- @since 0.10.0+getBaseExtension :: FilePath -> String+getBaseExtension name | (base, ext) <- splitExtension name =+  case map toLower ext of+#ifdef WITH_ZLIB+    ".gz" -> getBaseExtension base+#endif+    s -> s

@@ -0,0 +1,307 @@+{-# OPTIONS_GHC -Wall #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  ToySolver.Internal.SolutionChecker+-- Copyright   :  (c) Masahiro Sakai 2025+-- License     :  BSD-style+--+-- Maintainer  :  masahiro.sakai@gmail.com+-- Stability   :  unstable+-- Portability :  non-portable+--+-----------------------------------------------------------------------------++module ToySolver.Internal.SolutionChecker+  ( checkSATResult+  , checkMaxSATResult+  , checkPBResult+  , checkWBOResult+  , checkMIPResult+  ) where++import Control.Monad+import Control.Monad.RWS.Lazy+import qualified Data.ByteString.Char8 as BS+import Data.List (intercalate, sortBy)+import qualified Data.Map.Lazy as Map+import Data.Maybe+import Data.Ord+import qualified Data.PseudoBoolean as PBFile+import Data.Scientific+import Data.String+import qualified Data.Text as T+import qualified Numeric.Optimization.MIP as MIP+import Text.Printf++import qualified ToySolver.FileFormat.CNF as CNF+import qualified ToySolver.SAT.Types as SAT++-- ------------------------------------------------------------------------++type M = RWS () [String] Bool++execM :: M () -> (Bool, [String])+execM m = execRWS m () True++addInfo :: String -> M ()+addInfo s = tell [s]++addError :: String -> M ()+addError s = tell [s] >> put False++-- ------------------------------------------------------------------------++checkSATResult :: CNF.CNF -> (BS.ByteString, Maybe SAT.Model) -> (Bool, [String])+checkSATResult cnf (status, m) = execM $ do+  case status of+    "SATISFIABLE" -> do+      when (isNothing m) $ do+        addError "SATISFIABLE, but a model is missing"+    "UNSATISFIABLE" -> do+      when (isJust m) $ do+        addError "UNSATISFIABLE, but a model is provided"+    "UNKNOWN" -> return ()+    _ -> do+      addError $ "unknown status: " ++ BS.unpack status++  case m of+    Nothing -> return ()+    Just model -> do+      forM_ (CNF.cnfClauses cnf) $ \constr ->+        unless (SAT.evalClause model (SAT.unpackClause constr)) $ do+          addError $ printf "violated: %s" (showClause constr :: String)++checkMaxSATResult :: CNF.WCNF -> (BS.ByteString, Maybe Integer, Maybe SAT.Model) -> (Bool, [String])+checkMaxSATResult wcnf (status, o, m) = execM $ do+  case status of+    "OPTIMUM FOUND" -> do+      when (isNothing m) $ do+        addError "OPTIMUM FOUND, but a model is missing"+    "SATISFIABLE" -> do+      when (isNothing m) $ do+        addError "SATISFIABLE, but a model is missing"+    "UNSATISFIABLE" -> do+      when (isJust m) $ do+        addError "UNSATISFIABLE, but a model is provided"+    "UNKNOWN" -> return ()+    _ -> do+      addError $ "unknown status: " ++ BS.unpack status++  case m of+    Nothing -> return ()+    Just model -> do+      cost <- fmap sum $ forM (CNF.wcnfClauses wcnf) $ \(w, constr) ->+        if SAT.evalClause model (SAT.unpackClause constr) then do+          return 0+        else if w == CNF.wcnfTopCost wcnf then do+          addError $ printf "violated hard constraint: %s" (showClause constr :: String)+          return 0+        else do+          return w+      addInfo $ "total cost = " ++ show cost++      case o of+        Just oVal | oVal /= cost -> do+          addError $ printf "o-line value (%d) is inconsistent" oVal+        _ -> return ()++checkPBResult :: PBFile.Formula -> (BS.ByteString, Maybe Integer, Maybe SAT.Model) -> (Bool, [String])+checkPBResult opb (status, o, m) = execM $ do+  case status of+    "SATISFIABLE" -> do+      when (isNothing m) $ do+        addError "SATISFIABLE, but a model is missing"+    "OPTIMUM FOUND" -> do+      when (isNothing m) $ do+        addError "OPTIMUM FOUND, but a model is missing"+    "UNSATISFIABLE" -> do+      when (isJust m) $ do+        addError "UNSATISFIABLE, but a model is provided"+    "UNSUPPORTED" -> return ()+    "UNKNOWN" -> return ()+    _ -> do+      addError $ "unknown status: " ++ BS.unpack status+++  case (PBFile.pbObjectiveFunction opb, o) of+    (Nothing, Just _) -> do+      addInfo $ "o-line(s) exist even though it is a PBS problem. (will be ignored)"+    _ -> pure ()++  case m of+    Nothing -> return ()+    Just model -> do+      case PBFile.pbObjectiveFunction opb of+        Nothing -> return ()+        Just objFunc -> do+          let val = SAT.evalPBSum model objFunc+          addInfo $ "objective function value = " ++ show val+          case o of+            Just oVal | val /= oVal -> do+              addError $ printf "o-line value (%d) is inconsistent" oVal+            _ -> return ()++      forM_ (PBFile.pbConstraints opb) $ \constr -> do+        unless (SAT.evalPBConstraint model constr) $ do+          addError $ printf "violated: %s" (showPBConstraint constr :: String)++checkWBOResult :: PBFile.SoftFormula -> (BS.ByteString, Maybe Integer, Maybe SAT.Model) -> (Bool, [String])+checkWBOResult wbo (status, o, m) = execM $ do+  case status of+    "SATISFIABLE" -> do+      when (isNothing m) $ do+        addError "SATISFIABLE, but a model is missing"+    "OPTIMUM FOUND" -> do+      when (isNothing m) $ do+        addError "OPTIMUM FOUND, but a model is missing"+    "UNSATISFIABLE" -> do+      when (isJust m) $ do+        addError "UNSATISFIABLE, but a model is provided"+    "UNSUPPORTED" -> return ()+    "UNKNOWN" -> return ()+    _ -> do+      addError $ "unknown status: " ++ BS.unpack status++  case m of+    Nothing -> return ()+    Just model -> do+      cost <- fmap sum $ forM (PBFile.wboConstraints wbo) $ \(w, constr) -> do+        if SAT.evalPBConstraint model constr then+          return 0+        else do+          case w of+            Nothing -> do+              addError $ printf "violated hard constraint: %s" (showPBConstraint constr :: String)+              return 0+            Just w' -> do+              return w'+      addInfo $ "total cost = " ++ show cost++      case PBFile.wboTopCost wbo of+        Just top | top <= cost -> do+          addError $ printf "total cost (%d) is greater than or equal to top cost (%d)" cost top+        _ -> return ()++      case o of+        Just oVal | oVal /= cost -> do+          addError $ printf "o-line value (%d) is inconsistent" oVal+        _ -> return ()++checkMIPResult :: MIP.Tol Scientific -> MIP.Problem Scientific -> MIP.Solution Scientific -> (Bool, [String])+checkMIPResult tol mip sol = execM $ do+  let m = MIP.solVariables sol++  let objVal = MIP.eval tol m (MIP.objExpr (MIP.objectiveFunction mip))+  addInfo $ "objective value = " ++ show objVal+  case MIP.solObjectiveValue sol of+    Nothing -> return ()+    Just declaredObjVal -> do+      unless (abs (objVal - declaredObjVal) <= MIP.feasibilityTol tol) $ do+        addError $ printf "declared objective value (%s) does not match to the computed value (%s)"+          (show declaredObjVal) (show objVal)++  forM_ (Map.toList (MIP.varDomains mip)) $ \(v, (vt, bounds@(lb,ub))) -> do+    let val = MIP.eval tol m v+        flag1 =+          case vt of+            MIP.ContinuousVariable -> True+            MIP.SemiContinuousVariable -> True+            MIP.IntegerVariable -> isIntegral tol val+            MIP.SemiIntegerVariable -> isIntegral tol val+        flag2 =+          case vt of+            MIP.ContinuousVariable -> isInBounds tol bounds val+            MIP.IntegerVariable -> isInBounds tol bounds val+            MIP.SemiIntegerVariable -> isInBounds tol (0,0) val || isInBounds tol bounds val+            MIP.SemiContinuousVariable -> isInBounds tol (0,0) val || isInBounds tol bounds val+    unless flag1 $ do+      addError $ printf "variable %s is not integral" (T.unpack (MIP.varName v))+    unless flag2 $ do+      let f MIP.NegInf = "-inf"+          f MIP.PosInf = "+inf"+          f (MIP.Finite x) = show x+      addError $ printf "variable %s is out of bounds lb=%s ub=%s" (T.unpack (MIP.varName v)) (f lb) (f ub)++  forM_ (MIP.constraints mip) $ \constr -> do+    unless (MIP.eval tol m constr) $ do+      addError $ case MIP.constrLabel constr of+        Just name -> printf "violated: %s" (T.unpack name)+        Nothing -> printf "violated: %s" (showMIPConstraint constr)++  forM_ (MIP.sosConstraints mip) $ \constr -> do+    unless (MIP.eval tol m constr) $ do+      addError $ case MIP.sosLabel constr of+        Just name -> printf "violated: %s" (T.unpack name)+        Nothing -> printf "violated: %s" (showMIPSOSConstraint constr)++-- ------------------------------------------------------------------------++showClause :: (Monoid a, IsString a) => SAT.PackedClause -> a+showClause = foldr (\f g -> f <> fromString " " <> g) mempty . map (fromString . show) . SAT.unpackClause++showPBSum :: (Monoid a, IsString a) => PBFile.Sum -> a+showPBSum = mconcat . map showWeightedTerm+  where+    showWeightedTerm :: (Monoid a, IsString a) => PBFile.WeightedTerm -> a+    showWeightedTerm (c, lits) = foldr (\f g -> f <> fromString " " <> g) mempty (x:xs)+      where+        x = if c >= 0 then fromString "+" <> fromString (show c) else fromString (show c)+        xs = map showLit $ sortBy (comparing abs) lits++    showLit :: (Monoid a, IsString a) => PBFile.Lit -> a+    showLit lit = if lit > 0 then v else fromString "~" <> v+      where+        v = fromString "x" <> fromString (show (abs lit))++showPBConstraint :: (Monoid a, IsString a) => PBFile.Constraint -> a+showPBConstraint (lhs, op, rhs) =+  showPBSum lhs <> f op <>  fromString " " <> fromString (show rhs)+  where+    f PBFile.Eq = fromString "="+    f PBFile.Ge = fromString ">="++showMIPConstraint :: MIP.Constraint Scientific -> String+showMIPConstraint constr = concat+  [ case MIP.constrIndicator constr of+      Nothing -> ""+      Just (MIP.Var var, val) ->+        let rhs =+              case floatingOrInteger val of+                Right (i :: Integer) -> show i+                Left (_ :: Double) -> show val  -- should be error?+         in T.unpack var ++ " = " ++ rhs ++ " -> "+  , case MIP.constrLB constr of+      MIP.NegInf -> ""+      MIP.PosInf -> "+inf <= "+      MIP.Finite x -> show x ++ " <= "+  , showMIPExpr (MIP.constrExpr constr)+  , case MIP.constrUB constr of+      MIP.NegInf -> "<= -inf"+      MIP.PosInf -> ""+      MIP.Finite x -> " <= " ++ show x+  ]++showMIPSOSConstraint :: MIP.SOSConstraint Scientific -> String+showMIPSOSConstraint constr = concat $+  [show (MIP.sosType constr), " ::"] ++ [+    " " ++ T.unpack (MIP.varName v) ++ " : " ++ show r+  | (v, r) <- MIP.sosBody constr+  ]++showMIPExpr :: MIP.Expr Scientific -> String+showMIPExpr e = intercalate " "+  [ intercalate "*" (((if c >= 0 then "+" ++ show c else show c) : map (T.unpack . MIP.varName) vs))+  | MIP.Term c vs <- MIP.terms e+  ]++isIntegral :: RealFrac r => MIP.Tol r -> r -> Bool+isIntegral tol x = abs (x - fromIntegral (floor (x + 0.5) :: Integer)) <= MIP.integralityTol tol++isInBounds :: (Num r, Ord r) => MIP.Tol r -> MIP.Bounds r -> r -> Bool+isInBounds tol (lb, ub) x =+  lb - MIP.Finite (MIP.feasibilityTol tol) <= MIP.Finite x &&+  MIP.Finite x <= ub + MIP.Finite (MIP.feasibilityTol tol)++-- ------------------------------------------------------------------------

@@ -41,7 +41,8 @@ import qualified Data.IntMap as IntMap import qualified Data.IntSet as IntSet import Data.Function (on)-import Data.List (groupBy, foldl')+import Data.List (foldl')+import qualified Data.List.NonEmpty as NonEmpty import Data.Maybe  import ToySolver.Data.Boolean@@ -65,9 +66,9 @@ removeEmptyQuantifiers = filter (\(_,xs) -> not (IntSet.null xs))  groupQuantifiers :: Prefix -> Prefix-groupQuantifiers = map f . groupBy ((==) `on` fst)+groupQuantifiers = map f . NonEmpty.groupBy ((==) `on` fst)   where-    f qs = (fst (head qs), IntSet.unions [xs | (_,xs) <- qs])+    f qs = (fst (NonEmpty.head qs), IntSet.unions [xs | (_,xs) <- NonEmpty.toList qs])  quantifyFreeVariables :: Int -> Prefix -> Prefix quantifyFreeVariables nv prefix

@@ -14,6 +14,7 @@ module ToySolver.SAT.Encoder.Integer   ( Expr (..)   , newVar+  , newVarPBLinSum   , linearize   , addConstraint   , addConstraintSoft@@ -24,6 +25,7 @@ import Control.Monad.Primitive import Data.Array.IArray import Data.VectorSpace+import Math.NumberTheory.Logarithms (integerLog2) import Text.Printf  import ToySolver.Data.OrdRel@@ -33,19 +35,41 @@ newtype Expr = Expr SAT.PBSum   deriving (Eq, Show, Read) -newVar :: SAT.AddPBNL m enc => enc -> Integer -> Integer -> m Expr+newVar+  :: SAT.AddPBNL m enc+  => enc+  -> Integer -- ^ lower bound+  -> Integer -- ^ upper bound+  -> m Expr newVar enc lo hi   | lo > hi = do       SAT.addClause enc [] -- assert inconsistency       return 0-  | lo == hi = return $ fromInteger lo   | otherwise = do-      let hi' = hi - lo-          bitWidth = head $ [w | w <- [1..], let mx = 2 ^ w - 1, hi' <= mx]-      vs <- SAT.newVars enc bitWidth-      let xs = zip (iterate (2*) 1) vs-      SAT.addPBAtMost enc xs hi'-      return $ Expr $ [(lo,[]) | lo /= 0] ++ [(c,[x]) | (c,x) <- xs]+      s <- newVarPBLinSum enc (hi - lo)+      return $ Expr $ [(lo,[]) | lo /= 0] ++ [(c, [l]) | (c,l) <- s]++-- | Lower-level version of 'newVar'+--+-- * It takes only upper bound. Lower bound is always 0.+--+-- * Return type is 'SAT.PBLinSum'. It is inconvenient for performing operations,+--   but it is sometimes useful to be guaranteed to be in a linear form.+newVarPBLinSum+  :: SAT.AddPBNL m enc+  => enc+  -> Integer -- ^ upper bound+  -> m SAT.PBLinSum+newVarPBLinSum enc hi+  | hi < 0 = do+      SAT.addClause enc [] -- assert inconsistency+      return []+  | hi == 0 = return []+  | otherwise = do+      let bitWidth = integerLog2 hi + 1+      vs <- SAT.newVars enc (bitWidth - 1)+      v <- SAT.newVar enc+      return $ [(c,x) | (c,x) <- zip (iterate (2*) 1) vs] ++ [(hi - (2 ^ (bitWidth - 1) - 1), v)]  instance AdditiveGroup Expr where   Expr xs1 ^+^ Expr xs2 = Expr (xs1++xs2)

@@ -61,7 +61,7 @@ import Data.Function (on) import Data.List (sortBy) import Data.Maybe (listToMaybe)-import Data.Ord (comparing)+import Data.Ord (comparing, Down (..))  import ToySolver.SAT.Types import qualified ToySolver.SAT.Encoder.Cardinality as Card@@ -165,7 +165,7 @@ preprocess constr = (lhs2, rhs1)   where     (lhs1, rhs1) = normalizePBLinAtLeast constr-    lhs2 = sortBy (flip (comparing fst) <> comparing (abs . snd)) lhs1+    lhs2 = sortBy (comparing (Down . fst) <> comparing (abs . snd)) lhs1  -- | Algorithm 2 in the paper but with a bug fixed encodePrefixSum :: PrefixSum -> Integer -> [[BCLit]]

@@ -26,7 +26,7 @@ import Control.Monad.State.Strict import Control.Monad.Primitive import Data.Ord-import Data.List+import Data.List (sortBy) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import qualified ToySolver.SAT.Types as SAT@@ -39,7 +39,7 @@  encodePBLinAtLeastWithPolarityBDD :: forall m. PrimMonad m => Tseitin.Encoder m -> Tseitin.Polarity -> SAT.PBLinAtLeast -> m SAT.Lit encodePBLinAtLeastWithPolarityBDD enc polarity (lhs,rhs) = do-  let lhs' = sortBy (flip (comparing fst)) lhs+  let lhs' = sortBy (comparing (Down . fst)) lhs   flip evalStateT Map.empty $ do     let f :: SAT.PBLinSum -> Integer -> Integer -> StateT (Map (SAT.PBLinSum, Integer) SAT.Lit) m SAT.Lit         f xs rhs slack

@@ -40,12 +40,13 @@ import Control.Monad.Primitive import Control.Monad.State import Control.Monad.Writer-import Data.List+import Data.List (sortBy) import Data.Maybe import Data.Ord import Data.Vector (Vector, (!)) import qualified Data.Vector as V import qualified Data.Vector.Mutable as MV+import Math.NumberTheory.Logarithms (intLog2) import ToySolver.Data.Boolean import qualified ToySolver.SAT.Types as SAT import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin@@ -85,8 +86,7 @@   | V.length v <= 1 = (v, V.empty)   | otherwise = (V.slice 0 len1 v, V.slice len1 len2 v)       where-        n = head $ dropWhile (< V.length v) $ iterate (*2) 1-        len1 = n `div` 2+        len1 = 2 ^ intLog2 (V.length v - 1)         len2 = V.length v - len1  splitOddEven :: Vector a -> (Vector a, Vector a)

@@ -74,19 +74,25 @@ parseConst = withTypedObject "constant" $ \obj -> obj .: "value"  jPBSum :: SAT.PBSum -> J.Value+jPBSum [t] = jPBWeightedTerm t jPBSum s = J.object   [ "type" .= ("operator" :: J.Value)   , "name" .= ("+" :: J.Value)-  , "operands" .=-      [ J.object-          [ "type" .= ("operator" :: J.Value)-          , "name" .= ("*" :: J.Value)-          , "operands" .= (jConst c : [jLit lit | lit <- lits])-          ]-      | (c, lits) <- s-      ]+  , "operands" .= map jPBWeightedTerm s   ] +jPBWeightedTerm :: PBFile.WeightedTerm -> J.Value+jPBWeightedTerm (c, lits) =+  case [jConst c | c /= 1] ++ [jLit lit | lit <- lits] of+    [] -> jConst (1 :: Int)+    [x] -> x+    xs ->+      J.object+        [ "type" .= ("operator" :: J.Value)+        , "name" .= ("*" :: J.Value)+        , "operands" .= xs+        ]+ parsePBSum :: J.Value -> J.Parser SAT.PBSum parsePBSum x = msum   [ withOperator "+" (fmap concat . mapM parsePBSum) x@@ -99,6 +105,17 @@       , parseLit y >>= \lit -> pure (1, [lit])       , withOperator "*" (fmap ((product *** concat) . unzip) . mapM f) y       ]++jPBLinSum :: SAT.PBLinSum -> J.Value+jPBLinSum s = jPBSum [(c, [l]) | (c,l) <- s]++parsePBLinSum :: J.Value -> J.Parser SAT.PBLinSum+parsePBLinSum x = do+  s <- parsePBSum x+  forM s $ \(c, ls) ->+    case ls of+      [l] -> pure (c, l)+      _ -> fail "non-linear expression (linear expression expected)"  jPBConstraint :: PBFile.Constraint -> J.Value jPBConstraint (lhs, op, rhs) =

@@ -0,0 +1,121 @@+{-# OPTIONS_GHC -Wall #-}+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ViewPatterns #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  ToySolver.SAT.LogParser+-- Copyright   :  (c) Masahiro Sakai 2025+-- License     :  BSD-style+--+-- Maintainer  :  masahiro.sakai@gmail.com+-- Stability   :  provisional+-- Portability :  portable+--+-----------------------------------------------------------------------------+module ToySolver.SAT.LogParser+  ( parseSATLog+  , parseMaxSATLog+  , parsePBLog+  ) where++import Data.Array.IArray+import qualified Data.ByteString.Char8 as BS+import qualified Data.ByteString.Lazy.Char8 as BL+import Data.Char+import Data.Maybe (fromMaybe)+import qualified Data.Vector.Unboxed as VU++import ToySolver.SAT.Types as SAT++parseSATLog :: BL.ByteString -> (BS.ByteString, Maybe SAT.Model)+parseSATLog s = f "UNKNOWN" Nothing (BL.lines s)+  where+    f :: BS.ByteString -> Maybe [BL.ByteString] -> [BL.ByteString] -> (BS.ByteString, Maybe SAT.Model)+    f !status vlines (l : ls) =+      case BL.uncons l of+        Just ('c', _) -> f status vlines ls+        Just ('s', BS.toStrict -> BS.strip -> rest) -> f rest vlines ls+        Just ('v', rest) ->+          let vlines' = Just $ rest : fromMaybe [] vlines+           in f status vlines' ls+        Just (c, _) -> error ("unknown line type: " ++ show c)+        Nothing -> f status vlines ls+    f !status vlines [] =+      ( status+      , case vlines of+          Nothing -> Nothing+          Just lss ->+            let xs = VU.fromList $ map (read . BL.unpack) $ concat $ map BL.words $ reverse lss+                xs' = VU.init xs+                n = maximum $ map abs $ VU.toList xs'+             in if VU.last xs /= 0 then+                  error "vlines are not terminated with zero"+                else if 0 `VU.elem` xs' then+                  error "multiple zeros in vlines"+                else+                  Just $ array (1, n) [if lit > 0 then (lit, True) else (- lit, False) | lit <- VU.toList xs']+      )++parseMaxSATLog :: BL.ByteString -> (BS.ByteString, Maybe Integer, Maybe SAT.Model)+parseMaxSATLog s = f "UNKNOWN" Nothing Nothing (BL.lines s)+  where+    f :: BS.ByteString -> Maybe Integer -> Maybe [BL.ByteString] -> [BL.ByteString] -> (BS.ByteString, Maybe Integer, Maybe SAT.Model)+    f !status obj vlines (l : ls) =+      case BL.uncons l of+        Just ('c', _) -> f status obj vlines ls+        Just ('s', BL.toStrict -> BS.strip -> rest) -> f rest obj vlines ls+        Just ('v', rest) ->+          let vlines' = Just $ rest : fromMaybe [] vlines+           in f status obj vlines' ls+        Just ('o', BL.toStrict -> BS.strip -> rest) ->+          case BS.readInteger rest of+            Just (!val, "") -> f status (Just val) Nothing ls+            _ -> error "failed to parse o-line"+        Just (c, _) -> error ("unknown line type: " ++ show c)+        Nothing -> f status obj vlines ls+    f !status obj vlines [] =+      ( status+      , obj+      , case vlines of+          Nothing -> Nothing+          Just lss ->+            let tmp1 = BL.filter (not . isSpace) $ BL.concat $ reverse lss+                tmp2 = map (read . BL.unpack) $ concat $ map BL.words $ reverse lss+             in if BL.all (\c -> c == '0' || c == '1') tmp1 then+                  Just $ array (1, fromIntegral (BL.length tmp1)) [(v, c=='1') | (v, c) <- zip [1..] (BL.unpack tmp1)]+                else+                  Just $ array (1, maximum (map abs tmp2)) [if lit > 0 then (lit, True) else (- lit, False) | lit <- tmp2]+      )++parsePBLog :: BL.ByteString -> (BS.ByteString, Maybe Integer, Maybe SAT.Model)+parsePBLog s = f "UNKNOWN" Nothing Nothing (BL.lines s)+  where+    f :: BS.ByteString -> Maybe Integer -> Maybe [BL.ByteString] -> [BL.ByteString] -> (BS.ByteString, Maybe Integer, Maybe SAT.Model)+    f !status obj vlines (l : ls) =+      case BL.uncons l of+        Just ('c', _) -> f status obj vlines ls+        Just ('s', BL.toStrict -> BS.strip -> rest) -> f rest obj vlines ls+        Just ('v', rest) ->+          let vlines' = Just $ rest : fromMaybe [] vlines+           in f status obj vlines' ls+        Just ('o', BL.toStrict -> BS.strip -> rest) ->+          case BS.readInteger rest of+            Just (!val, "") -> f status (Just val) Nothing ls+            _ -> error "failed to parse o-line"+        Just (c, _) -> error ("unknown line type: " ++ show c)+        Nothing -> f status obj vlines ls+    f !status obj vlines [] =+      ( status+      , obj+      , case vlines of+          Nothing -> Nothing+          Just lss ->+            let lits = map (parseLit . BL.unpack) $ concat $ map BL.words $ reverse lss+             in Just $ array (1, maximum (map abs lits)) [if lit > 0 then (lit, True) else (- lit, False) | lit <- lits]+      )++    parseLit :: String -> SAT.Lit+    parseLit ('-' : 'x' : rest) | [(v, "")] <- reads rest = - v+    parseLit ('x' : rest) | [(v, "")] <- reads rest = v+    parseLit w = error ("failed to parse a literal: " ++ show w)

@@ -17,7 +17,6 @@  import Control.Monad import Data.Default.Class-import Data.List import qualified Data.IntSet as IS import qualified ToySolver.SAT as SAT import ToySolver.SAT.Types

@@ -18,7 +18,7 @@  import Control.Monad import Data.Default.Class-import Data.List+import Data.List (intercalate) import qualified Data.IntSet as IS import qualified ToySolver.SAT as SAT import ToySolver.SAT.Types

@@ -38,7 +38,6 @@ import Data.Array.IArray import Data.Default.Class import qualified Data.IntSet as IS-import Data.List import Data.IORef import Data.Set (Set) import qualified Data.Set as Set

@@ -22,7 +22,7 @@  import Control.Monad import Data.Default.Class-import Data.List+import Data.List (intercalate) import qualified Data.IntSet as IntSet import qualified ToySolver.SAT as SAT import ToySolver.SAT.Types

@@ -25,7 +25,7 @@  import Control.Monad import Data.Default.Class-import Data.List+import Data.List (intercalate) import qualified Data.IntSet as IS import qualified ToySolver.SAT as SAT import ToySolver.SAT.Types

@@ -32,7 +32,7 @@ import Control.Monad import qualified Data.IntSet as IntSet import qualified Data.IntMap as IntMap-import Data.List+import Data.List (foldl') import qualified ToySolver.SAT as SAT import qualified ToySolver.SAT.Types as SAT import qualified ToySolver.SAT.PBO.Context as C

@@ -1,27 +1,39 @@+{-# OPTIONS_GHC -Wall #-}+{-# OPTIONS_HADDOCK show-extensions #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE OverloadedStrings #-} ----------------------------------------------------------------------------- -- | -- Module      :  ToySolver.SAT.Printer--- Copyright   :  (c) Masahiro Sakai 2012+-- Copyright   :  (c) Masahiro Sakai 2012-2025 -- License     :  BSD-style -- -- Maintainer  :  masahiro.sakai@gmail.com -- Stability   :  provisional--- Portability :  portable+-- Portability :  non-portable -- -- Printing utilities. -- ----------------------------------------------------------------------------- module ToySolver.SAT.Printer-  ( satPrintModel+  (+  -- * Model/Solution printer+    satPrintModel   , maxsatPrintModel   , maxsatPrintModelCompact   , pbPrintModel   , musPrintSol++  -- * Low-level builder functions+  , satModel+  , maxsatModel+  , maxsatModelCompact+  , pbModel+  , musSol   ) where -import Control.Monad import Data.Array.IArray-import Data.List+import qualified Data.ByteString.Builder as Builder import System.IO import ToySolver.SAT.Types @@ -29,64 +41,97 @@ -- See <http://www.satcompetition.org/2011/rules.pdf> for details. satPrintModel :: Handle -> Model -> Int -> IO () satPrintModel h m n = do-  let as = if n > 0-           then takeWhile (\(v,_) -> v <= n) $ assocs m-           else assocs m-  forM_ (split 10 as) $ \xs -> do-    hPutStr h "v"-    forM_ xs $ \(var,val) -> hPutStr h (' ': show (literal var val))-    hPutStrLn h ""-  hPutStrLn h "v 0"+  newline <- getNewline h+  Builder.hPutBuilder h $ satModel m n newline   hFlush h  -- | Print a 'Model' in a way specified for Max-SAT Evaluation. -- See <http://maxsat.ia.udl.cat/requirements/> for details. maxsatPrintModel :: Handle -> Model -> Int -> IO () maxsatPrintModel h m n = do-  let as = if n > 0-           then takeWhile (\(v,_) -> v <= n) $ assocs m-           else assocs m-  forM_ (split 10 as) $ \xs -> do-    hPutStr h "v"-    forM_ xs $ \(var,val) -> hPutStr h (' ' : show (literal var val))-    hPutStrLn h ""-  -- no terminating 0 is necessary+  newline <- getNewline h+  Builder.hPutBuilder h $ maxsatModel m n newline   hFlush h  -- | Print a 'Model' in the new compact way specified for Max-SAT Evaluation >=2020. -- See <https://maxsat-evaluations.github.io/2020/vline.html> for details. maxsatPrintModelCompact :: Handle -> Model -> Int -> IO () maxsatPrintModelCompact h m n = do-  let vs = if n > 0-           then take n $ elems m-           else elems m-  hPutStrLn h $ "v " ++ [if v then '1' else '0' | v <- vs]+  newline <- getNewline h+  Builder.hPutBuilder h $ maxsatModelCompact m n newline   hFlush h  -- | Print a 'Model' in a way specified for Pseudo-Boolean Competition. -- See <http://www.cril.univ-artois.fr/PB12/format.pdf> for details. pbPrintModel :: Handle -> Model -> Int -> IO () pbPrintModel h m n = do-  let as = if n > 0-           then takeWhile (\(v,_) -> v <= n) $ assocs m-           else assocs m-  forM_ (split 10 as) $ \xs -> do-    hPutStr h "v"-    forM_ xs $ \(var,val) -> hPutStr h (" " ++ (if val then "" else "-") ++ "x" ++ show var)-    hPutStrLn h ""+  newline <- getNewline h+  Builder.hPutBuilder h $ pbModel m n newline   hFlush h  musPrintSol :: Handle -> [Int] -> IO () musPrintSol h is = do-  forM_ (split 10 is) $ \xs -> do-    hPutStr h "v"-    forM_ xs $ \i -> hPutStr h (' ': show i)-    hPutStrLn h ""-  hPutStrLn h "v 0"+  newline <- getNewline h+  Builder.hPutBuilder h $ musSol is newline   hFlush h  -- ------------------------------------------------------------------------ +satModel :: Model -> Int -> Newline -> Builder.Builder+satModel m n newline = mconcat+  [ Builder.char7 'v' <> mconcat [Builder.char7 ' ' <> Builder.intDec (literal var val) | (var, val) <- xs] <> nl+  | xs <- split 10 as+  ] <> Builder.string7 "v 0" <> nl+  where+    as = if n > 0+         then takeWhile (\(v,_) -> v <= n) $ assocs m+         else assocs m+    nl = newlineBuilder newline++maxsatModel :: Model -> Int -> Newline -> Builder.Builder+maxsatModel m n newline = mconcat+  [ Builder.char7 'v' <> mconcat [Builder.char7 ' ' <> Builder.intDec (literal var val) | (var, val) <- xs] <> nl+  | xs <- split 10 as+  ] -- no terminating 0 is necessary+  where+    as = if n > 0+         then takeWhile (\(v,_) -> v <= n) $ assocs m+         else assocs m+    nl = newlineBuilder newline++maxsatModelCompact :: Model -> Int -> Newline -> Builder.Builder+maxsatModelCompact m n newline =+  Builder.string7 "v " <> mconcat [Builder.char7 (if v then '1' else '0') | v <- vs] <> nl+  where+    vs = if n > 0+         then take n $ elems m+         else elems m+    nl = newlineBuilder newline++pbModel :: Model -> Int -> Newline -> Builder.Builder+pbModel m n newline = mconcat+  [ Builder.char7 'v' <> mconcat+    [ Builder.char7 ' ' <> (if val then mempty else Builder.char7 '-') <> Builder.char7 'x' <> Builder.intDec var+    | (var, val) <- xs+    ] <> nl+  | xs <- split 10 as+  ]+  where+    as = if n > 0+         then takeWhile (\(v,_) -> v <= n) $ assocs m+         else assocs m+    nl = newlineBuilder newline++musSol :: [Int] -> Newline -> Builder.Builder+musSol is newline = mconcat+  [ Builder.char7 'v' <> mconcat [Builder.char7 ' ' <> Builder.intDec i | i <- xs] <> nl+  | xs <- split 10 is+  ] <> Builder.string7 "v 0" <> nl+  where+    nl = newlineBuilder newline++-- ------------------------------------------------------------------------+ split :: Int -> [a] -> [[a]] split n = go   where@@ -94,3 +139,23 @@     go xs =       case splitAt n xs of         (ys, zs) -> ys : go zs++#ifdef mingw32_HOST_OS++getNewline :: Handle -> IO Newline+getNewline h = do+  m <- hGetEncoding h+  case m of+    Nothing -> return LF+    Just _ -> return CRLF++#else++getNewline :: Handle -> IO Newline+getNewline _ = return LF++#endif++newlineBuilder :: Newline -> Builder.Builder+newlineBuilder LF = Builder.char7 '\n'+newlineBuilder CRLF = Builder.string7 "\r\n"

@@ -2,7 +2,6 @@ {-# OPTIONS_HADDOCK show-extensions #-} {-# LANGUAGE BangPatterns #-} {-# LANGUAGE CPP #-}-{-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE InstanceSigs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RecursiveDo #-}@@ -142,9 +141,6 @@ import Data.Array.IO import Data.Array.Unsafe (unsafeFreeze) import Data.Array.Base (unsafeRead, unsafeWrite)-#if !MIN_VERSION_hashable(1,4,3)-import Data.Bits (xor) -- for defining 'combine' function-#endif import Data.Coerce import Data.Default.Class import Data.Either@@ -154,7 +150,7 @@ import qualified Data.HashSet as HashSet import Data.IORef import Data.Int-import Data.List+import Data.List (delete, find, foldl', maximumBy, partition, sortBy) import Data.Maybe import Data.Ord import qualified Data.IntMap.Strict as IM@@ -163,7 +159,6 @@ import ToySolver.Internal.Data.IOURef import qualified ToySolver.Internal.Data.IndexedPriorityQueue as PQ import qualified ToySolver.Internal.Data.Vec as Vec-import Data.Typeable import System.Clock import qualified System.Random.MWC as Rand import Text.Printf@@ -1173,12 +1168,12 @@       Left m -> m  data BudgetExceeded = BudgetExceeded-  deriving (Show, Typeable)+  deriving (Show)  instance Exception BudgetExceeded  data Canceled = Canceled-  deriving (Show, Typeable)+  deriving (Show)  instance Exception Canceled @@ -1771,7 +1766,7 @@    incrementReasoned solver (IS.toList lits2) -  xs <- liftM (sortBy (flip (comparing snd))) $+  xs <- liftM (sortBy (comparing (Down . snd))) $     forM (IS.toList lits2) $ \l -> do       lv <- litLevel solver l       return (l,lv)@@ -2474,7 +2469,7 @@           watchLit solver liti this           assignBy solver lit0 this -- should always succeed       else do -- CONFLICT-        ls <- liftM (map fst . sortBy (flip (comparing snd))) $ forM [0..size-1] $ \l -> do+        ls <- liftM (map fst . sortBy (comparing (Down . snd))) $ forM [0..size-1] $ \l -> do           lit <- readLitArray (claLits this2) l           lv <- litLevel solver lit           return (l,lv)@@ -2687,7 +2682,7 @@                   else do                     -- CONFLICT                     -- We need to watch unassigned literals or most recently falsified literals.-                    do xs <- liftM (sortBy (flip (comparing snd))) $ forM [i..m-1] $ \l -> do+                    do xs <- liftM (sortBy (comparing (Down . snd))) $ forM [i..m-1] $ \l -> do                          lit <- readLitArray a l                          val <- litValue solver lit                          if val == lFalse then do@@ -2918,7 +2913,7 @@  newPBHandlerCounter :: PBLinSum -> Integer -> Bool -> IO PBHandlerCounter newPBHandlerCounter ts degree learnt = do-  let ts' = sortBy (flip compare `on` fst) ts+  let ts' = sortBy (comparing (Down . fst)) ts       slack = sum (map fst ts) - degree       m = IM.fromList [(l,c) | (c,l) <- ts]   s <- newIORef slack@@ -3063,7 +3058,7 @@  newPBHandlerPueblo :: PBLinSum -> Integer -> Bool -> IO PBHandlerPueblo newPBHandlerPueblo ts degree learnt = do-  let ts' = sortBy (flip compare `on` fst) ts+  let ts' = sortBy (comparing (Down . fst)) ts       slack = sum [c | (c,_) <- ts'] - degree   ws   <- newIORef IS.empty   wsum <- newIORef 0@@ -3321,7 +3316,7 @@             readIORef ref'           assignBy solver (if y then litNot lit0 else lit0) this -- should always succeed       else do-        ls <- liftM (map fst . sortBy (flip (comparing snd))) $ forM [0..size-1] $ \l -> do+        ls <- liftM (map fst . sortBy (comparing (Down . snd))) $ forM [0..size-1] $ \l -> do           lit <- readLitArray a l           lv <- litLevel solver lit           return (l,lv)@@ -3623,16 +3618,6 @@   (x:xs) <- readIORef ref   writeIORef ref xs   return x--#if !MIN_VERSION_hashable(1,4,3)--defaultHashWithSalt :: Hashable a => Int -> a -> Int-defaultHashWithSalt salt x = salt `combine` hash x-  where-    combine :: Int -> Int -> Int-    combine h1 h2 = (h1 * 16777619) `xor` h2--#endif  {--------------------------------------------------------------------   debug