Commit 22a88ac9 authored by Michael Hanus's avatar Michael Hanus
Browse files

Update to version3

parent 185c2e4a
Pipeline #2296 failed with stages
in 3 seconds
Copyright (c) 2017, Michael Hanus
Copyright (c) 2021, Michael Hanus
All rights reserved.
Redistribution and use in source and binary forms, with or without
......
-- Examples for testing the satisfiability of Boolean formulas.
import Test.Prop
import Dimacs.Build
import Dimacs.Solver
import Dimacs.Types
-- A satisfiable formula.
b1 :: Boolean
b1 = (va 1 .\/ va 2) ./\ no (va 3)
b1 = (va 1 .\/ va 2) ./\ no (va 3) ./\ no (va 1)
solveb1 :: IO [(Int,Bool)]
solveb1 = solveWithDimacs z3Dimacs b1
testb1 :: PropIO
testb1 = solveb1 `returns` [(1,False),(2,True),(3,False)]
-- An unsatisfiable formula.
b2 :: Boolean
b2 = (va 1 .\/ va 2) ./\ (va 1 .\/ no (va 2)) ./\
......@@ -19,3 +24,5 @@ b2 = (va 1 .\/ va 2) ./\ (va 1 .\/ no (va 2)) ./\
solveb2 :: IO [(Int,Bool)]
solveb2 = solveWithDimacs z3Dimacs b2
testb2 :: PropIO
testb2 = solveb2 `returns` []
{
"name": "dimacs",
"version": "0.0.1",
"author": "Sven Hueser, Michael Hanus <mh@informatik.uni-kiel.de>",
"maintainer": "Michael Hanus <mh@informatik.uni-kiel.de>",
"synopsis": "An interface to SAT solvers supporting DIMACS.",
"category": [ "Constraints", "Verification" ],
"license": "BSD-3-Clause",
"licenseFile": "LICENSE",
"dependencies": {
},
"compilerCompatibility": {
"pakcs": ">= 1.14.0, < 2.0.0",
"kics2": ">= 0.5.0, < 2.0.0"
},
"exportedModules": [ "Dimacs.Types", "Dimacs.Build", "Dimacs.Solver" ],
"source": {
"git": "https://git.ps.informatik.uni-kiel.de/curry-packages/dimacs.git",
"tag": "$version"
}
"name": "dimacs",
"version": "3.0.0",
"author": "Sven Hueser, Michael Hanus <mh@informatik.uni-kiel.de>",
"maintainer": "Michael Hanus <mh@informatik.uni-kiel.de>",
"synopsis": "An interface to SAT solvers supporting DIMACS.",
"category": [ "Constraints", "Verification" ],
"license": "BSD-3-Clause",
"licenseFile": "LICENSE",
"dependencies": {
"base" : ">= 3.0.0, < 4.0.0",
"io-extra" : ">= 3.0.0, < 4.0.0",
"wl-pprint": ">= 3.0.0, < 4.0.0"
},
"exportedModules": [ "Dimacs.Types", "Dimacs.Build", "Dimacs.Solver" ],
"testsuite": {
"src-dir": "examples",
"modules": [ "Simple" ]
},
"source": {
"git": "https://git.ps.informatik.uni-kiel.de/curry-packages/dimacs.git",
"tag": "$version"
}
}
......@@ -49,7 +49,7 @@ yield :: a -> Parser token a
yield x ts = Right (ts, x)
--- A parser recognizing a particular terminal symbol.
terminal :: token -> Parser token ()
terminal :: (Eq token, Show token) => token -> Parser token ()
terminal _ [] = eof []
terminal x (t:ts) = case x == t of
True -> Right (ts, ())
......@@ -60,7 +60,7 @@ eof :: Parser token a
eof _ = Left "unexpected end-of-file"
--- Returns parse error about unexpected token `t`
unexpected :: token -> Parser token a
unexpected :: Show token => token -> Parser token a
unexpected t _ = Left $ "unexpected token " ++ show t
--- A star combinator for parsers. The returned parser
......
......@@ -3,12 +3,12 @@
--- of Boolean formulas.
---
--- @author Sven Hueser
--- @version September 2017
--- @version July 2021
------------------------------------------------------------------------------
module Dimacs.Build where
import List (nub)
import Data.List (nub)
import Dimacs.Types
......
......@@ -2,11 +2,13 @@
--- This module defines a simple parser for the output of a DIMACS solver.
---
--- @author Sven Hueser
--- @version September 2017
--- @version July 2021
------------------------------------------------------------------------------
module Dimacs.Parser where
import Prelude hiding ( some, (<*), (*>), (<$>) )
import DetParser
import Dimacs.Types
import Dimacs.Scanner
......
......@@ -2,13 +2,13 @@
--- This module defines operations to show Boolean formulas in DIMACS format.
---
--- @author Michael Hanus, Sven Hueser
--- @version September 2017
--- @version July 2021
------------------------------------------------------------------------------
module Dimacs.Pretty ( showDimacs, prettyDimacs, prettySolution )
where
import Pretty
import Text.Pretty
import Dimacs.Types
import Dimacs.Build
......
......@@ -2,13 +2,13 @@
--- This module defines a simple scanner for the output of a DIMACS solver.
---
--- @author Sven Hueser
--- @version September 2017
--- @version July 2021
------------------------------------------------------------------------------
module Dimacs.Scanner where
import ReadNumeric
import Char (isAlpha, isDigit, toLower)
import Data.Char (isAlpha, isDigit, toLower)
import Numeric
data Token
-- keywords
......@@ -19,6 +19,7 @@ data Token
| VarNot
-- other
| EOF
deriving (Eq, Show)
keywords :: [(String, Token)]
keywords =
......@@ -56,5 +57,5 @@ scanNum :: String -> [Token]
scanNum cs =
let v = readInt cs
in case v of
Just (num, rest) -> VarNum num : scan rest
Nothing -> error "should not be possible"
[(num, rest)] -> VarNum num : scan rest
_ -> error "should not be possible"
......@@ -4,13 +4,13 @@
--- It also defines configuration for various solvers.
---
--- @author Michael Hanus
--- @version September 2017
--- @version July 2021
------------------------------------------------------------------------------
module Dimacs.Solver where
import IO
import IOExts
import System.IO
import System.IOExts ( execCmd )
import Dimacs.Parser ( parse )
import Dimacs.Pretty ( showDimacs )
......
......@@ -3,12 +3,12 @@
--- together with some auxiliary operations.
---
--- @author Michael Hanus, Sven Hueser
--- @version September 2017
--- @version July 2021
------------------------------------------------------------------------------
module Dimacs.Types where
import List ( maximum )
import Data.List ( maximum )
--- The type of Boolean formulas.
--- Not that variables should be numbered from 1.
......@@ -16,6 +16,7 @@ data Boolean = Var Int
| Not Boolean
| And [Boolean]
| Or [Boolean]
deriving (Eq,Show)
--- Returns the maximal variable index in a Boolean formula.
maxVar :: Boolean -> Int
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment