satplus (empty) → 0.1.0.0
raw patch · 15 files changed
+2394/−0 lines, 15 filesdep +basedep +minisatsetup-changed
Dependencies added: base, minisat
Files
- LICENSE +30/−0
- README.md +182/−0
- SAT.hs +224/−0
- SAT/Binary.hs +215/−0
- SAT/Bool.hs +152/−0
- SAT/Equal.hs +122/−0
- SAT/Optimize.hs +120/−0
- SAT/Order.hs +205/−0
- SAT/Term.hs +449/−0
- SAT/Unary.hs +321/−0
- SAT/Util.hs +46/−0
- SAT/Val.hs +149/−0
- SAT/Value.hs +107/−0
- Setup.hs +2/−0
- satplus.cabal +70/−0
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2015, Koen Claessen++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Koen Claessen nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,182 @@+# SAT+++This is a Haskell library for constraint programming using a SAT-solver,+in particular MiniSAT.++The names and types of these functions may change at any moment!++## Basic MiniSAT++The basic MiniSAT functions are:++```haskell+newSolver :: IO Solver+newLit :: Solver -> IO Lit+addClause :: Solver -> [Lit] -> IO ()+solve :: Solver -> [Lit] -> IO Bool+modelValue :: Solver -> Lit -> IO Bool+conflict :: Solver -> IO [Lit]++valueMaybe :: Solver -> Lit -> IO (Maybe Bool)+modelValueMaybe :: Solver -> Lit -> IO (Maybe Bool)+```++## Boolean functions++This library also supports boolean operators:++```haskell+andl, orl, xorl :: Solver -> [Lit] -> IO Lit+```+And binary operators:++```haskell+implies :: Solver -> Lit -> Lit -> IO Lit+equiv :: Solver -> Lit -> Lit -> IO Lit+```++## Values++We also have implemented a convenient type that links Haskell values+with the SAT-solver:++```haskell+type Val a++newVal :: Ord a => Solver -> [a] -> IO (Val a)+val :: a -> Val a+(.=) :: Ord a => Val a -> a -> Lit+domain :: Val a -> [a]+```++We also provide:++```haskell+modelValue :: Solver -> Val a -> IO a+```++## Equality++We often want to add constraints that say that two things are equal,+or not equal, to each other.++```haskell+class Equal a where+ equal :: Solver -> a -> a -> IO ()+ notEqual :: Solver -> a -> a -> IO ()+ ...+```++Instances of this class are:++```haskell+instance Equal ()+instance Equal Lit+instance (Equal a, Equal b) => Equal (a,b)+instance (Equal a, Equal b) => Equal (Either a b)+instance Equal a => Equal [a]+instance Equal a => Equal (Maybe a)+instance Ord a => Equal (Val a)+instance Equal Unary+instance Equal Binary+```++## Order++We often want to add constraints that say that one thing is smaller than+another.++```haskell+class Order a where+ lessThan :: Solver -> a -> a -> IO ()+ lessThanEqual :: Solver -> a -> a -> IO ()+ greaterThan :: Solver -> a -> a -> IO ()+ greaterThanEqual :: Solver -> a -> a -> IO ()+ ...+```++Instances of this class are:++```haskell+instance Order ()+instance Order Lit+instance (Order a, Order b) => Equal (a,b)+instance (Order a, Order b) => Equal (Either a b)+instance Order a => Order [a]+instance Order a => Order (Maybe a)+instance Ord a => Order (Val a)+instance Order Unary+instance Order Binary+```++## Unary numbers++We have support for unary numbers (represented as sorted lists of Lits).+These are handy when you want to count number of literals in a set being+true, for example.++```haskell+type Unary++zero :: Unary+digit :: Lit -> Unary+number :: Int -> Unary++count :: Solver -> [Lit] -> IO Unary+countMax :: Solver -> Int -> [Lit] -> IO Unary++add :: Solver -> Unary -> Unary -> IO Unary+addList :: Solver -> [Unary] -> IO Unary++(.<=), (.<), (.>=), (.>) :: Unary -> Int -> Lit+```++We also provide:++```haskell+modelValue :: Solver -> Unary -> IO Int+```++## Binary numbers++We have support for binary numbers (represented as lists of Lits).+These are handy when you want to represent numbers that are large.++```haskell+type Binary++zero :: Binary+digit :: Lit -> Binary+number :: Integer -> Binary++count :: Solver -> [Lit] -> IO Binary+countMax :: Solver -> Int -> [Lit] -> IO Binary++add :: Solver -> Binary -> Binary -> IO Binary+addList :: Solver -> [Binary] -> IO Binary+```++We also provide:++```haskell+modelValue :: Solver -> Binary -> IO Integer+```++## Terms++We also support linear arithmetic terms over a base type of variables+(for example Lit, Unary, or Binary).++(not done yet)++## Minimization / Maximization++We also support finding solutions that are minimized or maximized w.r.t.+a particular argument.++```haskell+solveMinimize :: Order a => Solver -> [Lit] -> Unary -> IO Bool+solveMaximize :: Order a => Solver -> [Lit] -> Unary -> IO Bool+```++TODO: add optimization over binary numbers.
+ SAT.hs view
@@ -0,0 +1,224 @@+{-|+Module : SAT+Description : Basic SAT operations++This module provides basic functions for working with Solver objects. A simple+example of typical use is:++@+main :: IO ()+main = do s <- newSolver+ x <- newLit s+ y <- newLit s+ addClause s [neg x, neg y]+ addClause s [x, y]+ b <- solve s []+ if b then+ do putStrLn \"Found model!\"+ a <- modelValue s x+ b <- modelValue s y+ putStrLn (\"x=\" ++ show a ++ \", y=\" ++ show b)+ else+ do putStrLn \"No model found.\"+ deleteSolver s+@+-}+module SAT(+ -- * The Solver object+ Solver+ , newSolver+ , deleteSolver+ , withNewSolver+ , numAssigns+ , numClauses+ , numLearnts+ , numVars+ , numFreeVars+ , numConflicts++ -- * Literals+ , Lit+ , newLit+ , false, true+ , bool+ , neg+ , pos++ -- * Clauses+ , addClause++ -- * Solving+ , solve+ , modelValue+ , modelValueMaybe+ , conflict++ -- * Implied constants+ , valueMaybe+ )+ where++import qualified MiniSat as M+import Data.IORef+import Data.Maybe( fromMaybe )++------------------------------------------------------------------------------+-- The Solver object++-- | The type of a Solver object+data Solver = Solver M.Solver (IORef (Maybe Lit))++-- | Create a Solver object.+newSolver :: IO Solver+newSolver =+ do s <- M.newSolver+ ref <- newIORef Nothing+ return (Solver s ref)++-- | Delete a Solver object. Use only once!+deleteSolver :: Solver -> IO ()+deleteSolver (Solver s _) =+ do M.deleteSolver s++-- | Create a Solver object, and delete when done.+withNewSolver :: (Solver -> IO a) -> IO a+withNewSolver h =+ M.withNewSolver $ \s ->+ do ref <- newIORef Nothing+ h (Solver s ref)++-- | The current number of assigned literals.+numAssigns :: Solver -> IO Int+numAssigns (Solver m _) = M.minisat_num_assigns m++-- | The current number of original clauses.+numClauses :: Solver -> IO Int+numClauses (Solver m _) = M.minisat_num_clauses m++-- | The current number of learnt clauses.+numLearnts :: Solver -> IO Int+numLearnts (Solver m _) = M.minisat_num_learnts m++-- | The current number of variables.+numVars :: Solver -> IO Int+numVars (Solver m _) = M.minisat_num_vars m++numFreeVars :: Solver -> IO Int+numFreeVars (Solver m _) = M.minisat_num_freeVars m++numConflicts :: Solver -> IO Int+numConflicts (Solver m _) = M.minisat_num_conflicts m++------------------------------------------------------------------------------+-- Literals++-- | The type of a literal+data Lit = Bool Bool | Lit M.Lit+ deriving ( Eq, Ord )++instance Show Lit where+ show (Bool b) = show b+ show (Lit x) = show x++-- | Create a fresh literal in a given Solver.+newLit :: Solver -> IO Lit+newLit (Solver s _) = Lit `fmap` M.newLit s++-- | Constant literal.+true, false :: Lit+true = Bool True+false = Bool False++-- | Create a constant literal based on a Bool.+bool :: Bool -> Lit+bool = Bool++-- | Negate a literal.+neg :: Lit -> Lit+neg (Bool b) = Bool (not b)+neg (Lit x) = Lit (M.neg x)++-- | Return the sign of a literal. The sign flips when a literal is negated.+pos :: Lit -> Bool+pos x = x < neg x++------------------------------------------------------------------------------+-- Clauses++-- | Add a clause in a given Solver. (The argument list is thus /disjunctive/.)+addClause :: Solver -> [Lit] -> IO ()+addClause (Solver s _) xs+ | true `elem` xs = do return ()+ | otherwise = do M.addClause s [ x | Lit x <- xs ]; return ()++------------------------------------------------------------------------------+-- Solving++-- | Try to find a model of all clauses in the given Solver, under the+-- assumptions of the given arguments. (The argument list is thus /conjunctive/.)+-- Returns True if a model was found, False if no model was found.+solve :: Solver -> [Lit] -> IO Bool+solve (Solver s ref) xs+ | false `elem` xs =+ do writeIORef ref (Just true)+ return False++ | otherwise =+ do writeIORef ref Nothing+ M.solve s [ x | Lit x <- xs ]++-- | If the last call to 'solve' returned False: Return the conflict clause+-- that was the reason for the fact that no model was found under the+-- specified assumptions. The conflict clause only contains literals that+-- are negations of the assumptions given to 'solve'. The conflict+-- clause is always logically implied by the current set of clauses.+--+-- For example, if the returned clause is empty, there is a contradiction even+-- without any assumptions.+--+-- This function can be used to implement so-called \'unsatisfiable cores\'.+--+-- There are no guarantees about minimality of the returned clause.+-- (/Only use when 'solve' has previously returned False!/)+conflict :: Solver -> IO [Lit]+conflict (Solver s ref) =+ do mx <- readIORef ref+ case mx of+ Nothing -> do xs <- M.conflict s+ return (map Lit xs)+ Just x -> do return [x]++------------------------------------------------------------------------------++-- | If the last call to 'solve' returned True, return the value of+-- the specified literal in the found model.+-- (/Only use when 'solve' has previously returned True!/)+modelValue :: Solver -> Lit -> IO Bool+modelValue s x =+ do mb <- modelValueMaybe s x+ return (fromMaybe (not (pos x)) mb)++-- | If the last call to 'solve' returned True, return the value of+-- the specified literal in the found model, or Nothing if there is a model+-- regardless of the value of this literal.+-- There are no guarantees about when Nothing is returned.+-- (/Only use when 'solve' has previously returned True!/)+modelValueMaybe :: Solver -> Lit -> IO (Maybe Bool)+modelValueMaybe _ (Bool b) =+ do return (Just b)++modelValueMaybe (Solver s _) (Lit x) =+ do M.modelValue s x++------------------------------------------------------------------------------+-- Implied constants++-- | Check whether or not a given literal has received a top-level value+-- in the given Solver. This can happen when the literal is implied to be+-- False or True by the current set of clauses. There are no guarantees about+-- when this actually happens.+valueMaybe :: Solver -> Lit -> IO (Maybe Bool)+valueMaybe _ (Bool b) = return (Just b)+valueMaybe (Solver s _) (Lit x) = M.value s x++------------------------------------------------------------------------------
+ SAT/Binary.hs view
@@ -0,0 +1,215 @@+{-|+Module : SAT.Binary+Description : Functions for working with natural numbers represented as+ binary numbers.+ + WARNING: completely untested so far.+-}+module SAT.Binary(+ -- * The Binary type+ Binary+ , newBinary+ , zero+ , number+ , digit+ , maxValue++ -- * Counting+ , count+ , add+ , addList+ , addBits+ , mul1+ , mul++ -- * Operations+ , invert++ -- * Conversion+ , fromList+ , toList++ -- * Models+ , modelValue+ )+ where++------------------------------------------------------------------------------++import SAT hiding ( modelValue )+import qualified SAT+import SAT.Bool+import SAT.Equal+import SAT.Order+import Data.List( insert, sort )++------------------------------------------------------------------------------++-- | The type Binary, for natural numbers represented in binary+newtype Binary = Binary [Lit] -- least significant bit first+ deriving ( Eq, Ord )++instance Show Binary where+ show (Binary xs) = show xs++-- | Creates a binary number from a list of digits (least significant bit first).+fromList :: [Lit] -> Binary+fromList xs = Binary xs++-- | Returns the list of digits (least significant bit first).+toList :: Binary -> [Lit]+toList (Binary xs) = xs++-- | Creates a fresh binary number, with the specified number of bits.+newBinary :: Solver -> Int -> IO Binary+newBinary s k =+ do xs <- sequence [ newLit s | i <- [1..k] ]+ return (Binary xs)++-- | Creates 0 as a binary number.+zero :: Binary+zero = Binary []++-- | Creates n>=0 as a binary number.+number :: Int -> Binary+number n = Binary (bin n)+ where+ bin 0 = []+ bin n = (if odd n then true else false) : bin (n `div` 2)++-- | Creates a 1-digit binary number, specified by the given literal.+digit :: Lit -> Binary+digit x = fromList [x]++-- | Inverts a binary number; computes /maxValue n - n/. Can be used to maximize+-- instead of minimize.+invert :: Binary -> Binary+invert (Binary xs) = Binary (map neg xs)++-- | Returns a binary number that represents the number of true literals in+-- the given list.+count :: Solver -> [Lit] -> IO Binary+count s xs = addList s (map digit xs)++-- | Adds up two binary numbers.+add :: Solver -> Binary -> Binary -> IO Binary+add s a b = addList s [a,b]++-- | Adds up a list of binary numbers. When adding more than 2 numbers, this+-- function is preferred over linearly folding the function 'add' over a list,+-- because a balanced tree (based on the sizes of the numbers involved) is+-- constructed by this function, which creates a lot less clauses than doing+-- it the naive way.+addList :: Solver -> [Binary] -> IO Binary+addList s bs = addBits s [ (k,x) | Binary xs <- bs, (k,x) <- [0..] `zip` xs ]++-- | Adds up a list of digits, annotated with their weight, which is the+-- placement of the binary digit. This function is used in the functions @addList@+-- and @mul@, but may be useful to users in its own right.+addBits :: Solver -> [(Int,Lit)] -> IO Binary+addBits s ixs = Binary `fmap` go 0 (sort ixs)+ where+ go _ [] =+ do return []++ go i xs@((i0,x):_) | i < i0 =+ do ys <- go (i+1) xs+ return (false : ys)++ go _ ((i0,x):(i1,y):(i2,z):xs) | i0 == i1 && i0 == i2 =+ do (v,c) <- full x y z+ go i0 ((i0,v):insert (i0+1,c) xs)++ go _ ((i0,x):(i1,y):xs) | i0 == i1 =+ do (v,c) <- full x y false+ ys <- go (i0+1) ((i0+1,c):xs)+ return (v:ys)++ go _ ((i0,x):xs) =+ do ys <- go (i0+1) xs+ return (x:ys)++ full x y z =+ do v <- xorl s [x,y,z]+ c <- atLeast2 x y z+ return (v,c)+ + -- desparately tries to avoid creating extra literals+ atLeast2 x y z+ | x == true = orl s [y,z] + | y == true = orl s [x,z] + | z == true = orl s [x,y] ++ | x == false = andl s [y,z] + | y == false = andl s [x,z] + | z == false = andl s [x,y] ++ | x == y = return x + | y == z = return y + | x == z = return z+ + | x == neg y = return z + | y == neg z = return x + | x == neg z = return y+ + | otherwise =+ do v <- newLit s+ addClause s [neg x, neg y, v]+ addClause s [neg x, neg z, v]+ addClause s [neg y, neg z, v]+ addClause s [x, y, neg v]+ addClause s [x, z, neg v]+ addClause s [y, z, neg v]+ return v++-- | Returns the maximum value a given binary number can have.+maxValue :: Num a => Binary -> a+maxValue (Binary xs) = (2^length xs) - 1++-- | Multiplies a digit and a binary number.+mul1 :: Solver -> Lit -> Binary -> IO Binary+mul1 s x (Binary ys) =+ do ys' <- sequence [ andl s [x,y] | y <- ys ]+ return (Binary ys')++-- | Multiplies two binary numbers.+mul :: Solver -> Binary -> Binary -> IO Binary+mul s (Binary xs) (Binary ys) =+ do izs <- sequence+ [ do z <- andl s [x,y]+ return (i+j,z)+ | (i,x) <- [0..] `zip` xs+ , (j,y) <- [0..] `zip` ys+ ]+ addBits s izs++-- | Return the numeric value of a binary number in the current model.+-- (/Use only when 'solve' has returned True!/)+modelValue :: Num a => Solver -> Binary -> IO a+modelValue s (Binary xs) = go xs+ where+ go [] = do return 0+ go (x:xs) = do b <- SAT.modelValue s x+ n <- go xs+ return (2*n + if b then 1 else 0)++------------------------------------------------------------------------------++instance Equal Binary where+ equalOr s pre (Binary xs) (Binary ys) =+ equalOr s pre (pad xs ys) (pad ys xs)++ notEqualOr s pre (Binary xs) (Binary ys) =+ notEqualOr s pre (pad xs ys) (pad ys xs)++instance Order Binary where+ lessOr s pre b (Binary xsLSBF) (Binary ysLSBF) =+ do lessOr s pre b xs ys+ where xs = reverse (pad xsLSBF ysLSBF)+ ys = reverse (pad ysLSBF xsLSBF)+++pad xs ys = xs ++ replicate (length ys - length xs) false++------------------------------------------------------------------------------+
+ SAT/Bool.hs view
@@ -0,0 +1,152 @@+{-|+Module : SAT.Bool+Description : Basic boolean functions and constraints+-}+module SAT.Bool where++import SAT+import SAT.Util( unconditionally, usort )+import Data.List( partition, sort )++------------------------------------------------------------------------------+-- * Boolean functions++-- | Return a literal representing the conjunction (''big-and'') of the+-- literals in the argument list. This function may create new literals and+-- add constraints, but tries to avoid doing this when possible.+andl :: Solver -> [Lit] -> IO Lit+andl s xs+ | false `elem` xs = return false+ | xAndNegX = return false+ | otherwise = case filter (/= true) xs' of+ [] -> do return true+ [x] -> do return x+ xs'' -> do y <- newLit s+ sequence_ [ addClause s [neg y, x]+ | x <- xs''+ ]+ addClause s (y : map neg xs'')+ return y+ where+ xs' = usort xs+ (xs0,xs1) = partition pos xs'+ xAndNegX = xs0 `overlap` sort (map neg xs1)++ [] `overlap` _ = False+ _ `overlap` [] = False+ (x:xs) `overlap` (y:ys) =+ case x `compare` y of+ LT -> xs `overlap` (y:ys)+ EQ -> True+ GT -> (x:xs) `overlap` ys++-- | Return a literal representing the disjunction (''big-or'') of the+-- literals in the argument list. This function may create new literals and+-- add constraints, but tries to avoid doing this when possible.+orl :: Solver -> [Lit] -> IO Lit+orl s = fmap neg . andl s . map neg++-- | Return a literal representing the parity (''big-xor'') of the literals+-- in the argument list. This function may create new literals and add+-- constraints, but tries to avoid doing this when possible.+xorl :: Solver -> [Lit] -> IO Lit+xorl s xs =+ case xs'' of+ [] -> do return (bool p)+ [x] -> do return (if p then neg x else x)+ _ -> do y <- newLit s+ parity s (y : xs'') p+ return y+ where+ xs' = filter (/= false) (sort xs)+ (xs0,xs1) = partition pos (filter (/= true) xs')+ (p,xs'') = go (odd (length (filter (== true) xs'))) [] xs0 (sort (map neg xs1))++ go p ys [] [] = (p, ys)+ go p ys (x:y:xs0) xs1 | x == y = go p ys xs0 xs1+ go p ys xs0 (x:y:xs1) | x == y = go p ys xs0 xs1+ go p ys [] (x1:xs1) = go p (neg x1:ys) [] xs1+ go p ys (x0:xs0) [] = go p (x0:ys) xs0 []+ go p ys (x0:xs0) (x1:xs1) =+ case x0 `compare` x1 of+ LT -> go p (x0:ys) xs0 (x1:xs1)+ EQ -> go (not p) ys xs0 xs1+ GT -> go p (neg x1:ys) (x0:xs0) xs1++-- | Return a literal representing the implication @a ==> b@ between two+-- literals @a@ and @b@.+implies :: Solver -> Lit -> Lit -> IO Lit+implies s x y = orl s [neg x, y]++-- | Return a literal representing the equivalence @a \<=\> b@ of two+-- literals @a@ and @b@.+equiv :: Solver -> Lit -> Lit -> IO Lit+equiv s x y = xorl s [neg x, y]++------------------------------------------------------------------------------+-- * Boolean constraints++-- | Add clauses that constrain the list of literals to have at most one+-- element to be True. See also 'atMostOneOr'.+atMostOne :: Solver -> [Lit] -> IO ()+atMostOne = unconditionally atMostOneOr++-- | Add clauses that constrain the list of literals to have the specified+-- parity, as a Bool. The parity of a list says whether the number of True+-- literals is even (False) or odd (True). See also 'parityOr'.+parity :: Solver -> [Lit] -> Bool -> IO ()+parity = unconditionally parityOr++------------------------------------------------------------------------------+-- * Boolean constraints with prefix++-- | Add clauses that constrain the list of literals to have at most one+-- element to be True, under the presence of a /disjunctive prefix/.+-- (See 'SAT.Util.unconditionally' for what /prefix/ means. This function+-- without prefix is called 'atMostOne'.)+atMostOneOr :: Solver -> [Lit] {- ^ prefix -}+ -> [Lit] {- ^ literal set -}+ -> IO ()+atMostOneOr s pre xs = go (length xs) xs+ where+ go n xs | n <= 5 =+ do sequence_ [ addClause s (pre ++ [neg x, neg y]) | (x,y) <- pairs xs ]+ where+ pairs (x:xs) = [ (x,y) | y <- xs ] ++ pairs xs+ pairs [] = []++ go n xs =+ do x <- newLit s+ go (k+1) (x : take k xs)+ go (n-k+1) (neg x : drop k xs)+ where+ k = n `div` 2++-- | Add clauses that constrain the list of literals to have the specified+-- parity, as a Bool, under the presence of a /disjunctive prefix/.+-- (See 'SAT.Util.unconditionally' for what /prefix/ means. This function+-- without prefix is called 'parity'.)+parityOr :: Solver -> [Lit] {- ^ prefix -}+ -> [Lit] {- ^ literal set -}+ -> Bool {- ^ parity -}+ -> IO ()+parityOr s pre xs p = go pre (length xs) xs p+ where+ go pre _ [] False =+ do return ()++ go pre _ [] True =+ do addClause s pre++ go pre n (x:xs) p | n <= 5 =+ do go (neg x : pre) (n-1) xs (not p)+ go (x : pre) (n-1) xs p++ go pre n xs p =+ do x <- newLit s+ go pre (k+1) (x : take k xs) p+ go pre (n-k+1) ((if p then neg x else x) : drop k xs) p+ where+ k = n `div` 2++------------------------------------------------------------------------------
+ SAT/Equal.hs view
@@ -0,0 +1,122 @@+{-|+Module : SAT.Equal+Description : Equality functions on things that live in the SAT-solver++This module provides a type class with functions for asserting the equality+or inequality of two objects, as well as functions that compute whether or+not two objects are equal or not.+-}+module SAT.Equal(+ -- * Constraints+ equal+ , notEqual++ -- * Type class Equal+ , Equal(..)+ )+ where++import SAT+import SAT.Bool+import SAT.Util( unconditionally )++------------------------------------------------------------------------------++-- | Type class for SAT-things that can be equal or not.+class Equal a where+ -- | Add constraints to the Solver that state that the arguments are equal,+ -- under the presence of a /disjunctive prefix/.+ -- (See 'SAT.Util.unconditionally' for what /prefix/ means. This function+ -- without prefix is called 'equal'.)+ equalOr :: Solver -> [Lit] {- ^ prefix -} -> a -> a -> IO ()++ -- | Add constraints to the Solver that state that the arguments are not+ -- equal, under the presence of a /disjunctive prefix/.+ -- (See 'SAT.Util.unconditionally' for what /prefix/ means.+ -- This function without prefix is called 'notEqual'.)+ notEqualOr :: Solver -> [Lit] {- ^ prefix -} -> a -> a -> IO ()++ -- | Return a literal that represents the arguments being equal or not.+ isEqual :: Solver -> a -> a -> IO Lit+ isEqual s x y =+ do q <- newLit s+ equalOr s [neg q] x y+ notEqualOr s [q] x y+ return q++------------------------------------------------------------------------------++-- | Add constraints to the Solver that state that the arguments are equal.+-- See also 'equalOr'.+equal :: Equal a => Solver -> a -> a -> IO ()+equal = unconditionally equalOr++-- | Add constraints to the Solver that state that the arguments are not equal.+-- See also 'notEqualOr'.+notEqual :: Equal a => Solver -> a -> a -> IO ()+notEqual = unconditionally notEqualOr++------------------------------------------------------------------------------++instance Equal () where+ equalOr s pre _ _ = return ()+ notEqualOr s pre _ _ = addClause s pre+ isEqual _ _ _ = return true++instance Equal Bool where+ equalOr s pre x y = if x == y then return () else addClause s pre+ notEqualOr s pre x y = if x /= y then return () else addClause s pre+ isEqual _ x y = return (bool (x==y))++instance Equal Lit where+ equalOr s pre x y =+ do addClause s (pre ++ [neg x, y])+ addClause s (pre ++ [x, neg y])++ notEqualOr s pre x y =+ do equalOr s pre x (neg y)++ isEqual s x y = xorl s [x, neg y]++instance (Equal a, Equal b) => Equal (a,b) where+ equalOr s pre (x1,x2) (y1,y2) =+ do equalOr s pre x1 y1+ equalOr s pre x2 y2++ notEqualOr s pre (x1,x2) (y1,y2) =+ do q <- newLit s+ notEqualOr s (q:pre) x1 y1+ notEqualOr s [neg q] x2 y2++instance (Equal a, Equal b) => Equal (Either a b) where+ equalOr s pre (Left x) (Left y) = equalOr s pre x y+ equalOr s pre (Right x) (Right y) = equalOr s pre x y+ equalOr s pre _ _ = addClause s pre++ notEqualOr s pre (Left x) (Left y) = notEqualOr s pre x y+ notEqualOr s pre (Right x) (Right y) = notEqualOr s pre x y+ notEqualOr s pre _ _ = return ()++------------------------------------------------------------------------------++instance (Equal a, Equal b, Equal c) => Equal (a,b,c) where+ equalOr s pre x y = equalOr s pre (encTriple x) (encTriple y)+ notEqualOr s pre x y = notEqualOr s pre (encTriple x) (encTriple y)++encTriple (x,y,z) = ((x,y),z)++instance Equal a => Equal (Maybe a) where+ equalOr s pre mx my = equalOr s pre (encMaybe mx) (encMaybe my)+ notEqualOr s pre mx my = notEqualOr s pre (encMaybe mx) (encMaybe my)++encMaybe Nothing = Left ()+encMaybe (Just x) = Right x++instance Equal a => Equal [a] where+ equalOr s pre xs ys = equalOr s pre (encList xs) (encList ys)+ notEqualOr s pre xs ys = notEqualOr s pre (encList xs) (encList ys)++encList [] = Nothing+encList (x:xs) = Just (x,xs)++------------------------------------------------------------------------------
+ SAT/Optimize.hs view
@@ -0,0 +1,120 @@+{-|+Module : SAT.Optimize+Description : Finding the optimal solution, according to a specified objective+-}+module SAT.Optimize where++import SAT as S+import SAT.Unary as U+import Data.Maybe( fromJust )+import System.IO( hFlush, stdout )++------------------------------------------------------------------------------+-- * Simple optimization++-- | Like 'solve', but finds the minimum solution, where the objective is a+-- specified unary number. This function does not /commit/ to a+-- solution. If committing is the desired behavior, the user should manually+-- add a clause with @obj .<= k@ afterwards.+solveMinimize :: Solver -> [Lit] -> Unary -> IO Bool+solveMinimize s ass obj =+ fromJust `fmap` solveOptimize s ass obj (\_ -> return True)++-- | Like 'solve', but finds the maximum solution, where the objective is a+-- specified unary number. This function does not /commit/ to a+-- solution. If committing is the desired behavior, the user should manually+-- add a clause with @obj .>= k@ afterwards.+solveMaximize :: Solver -> [Lit] -> Unary -> IO Bool+solveMaximize s ass obj =+ fromJust `fmap` solveOptimize s ass (invert obj) (\_ -> return True)++------------------------------------------------------------------------------+-- * Verbose optimization++-- | A type to specify what to print during optimization+data Verbosity+ = None -- ^ Print nothing+ | Compact -- ^ Print a compact state, erase afterwards+ | Line -- ^ Print every output on a separate line+ deriving ( Eq, Ord, Show, Read )++-- | Like 'solveMinimum', but also prints information during optimization.+solveMinimizeVerbose :: Solver -> [Lit] -> Unary -> Verbosity -> IO Bool+solveMinimizeVerbose s ass obj v =+ fromJust `fmap` solveOptimize s ass obj (printOpti v)++-- | Like 'solveMaximum', but also prints information during optimization.+solveMaximizeVerbose :: Solver -> [Lit] -> Unary -> Verbosity -> IO Bool+solveMaximizeVerbose s ass obj v =+ fromJust `fmap` solveOptimize s ass (invert obj) (printOpti' v)+ where+ m = maxValue obj+ printOpti' v (x,y) = printOpti v (m-y,m-x)++printOpti :: Verbosity -> (Int,Int) -> IO Bool+printOpti v (x,y) =+ do case v of+ None -> do return ()+ Line -> do putStrLn s+ Compact -> do putStr (s ++ back)+ hFlush stdout+ putStr (wipe ++ back)+ return True+ where+ s = "(" ++ show x ++ "-" ++ show y ++ ")"+ n = length s+ back = replicate n '\b'+ wipe = replicate n ' '++------------------------------------------------------------------------------+-- * General optimization++-- | The most general optimization function. It supports a callback that at+-- each optimization step can decide whether or not to continue. If the+-- callback says not to continue (by returning False),+-- the result of 'solveOptimize' will be Nothing. It is still possible to+-- read off the best solution found using functions such as 'modelValue'.+--+-- The optimization performs a binary search. The callback function gets the+-- current optimization interval @(minTry,minReached)@ as argument;+-- which are the values of the best value still considered possible+-- (@minTry@) and the best value found so far (@minReached@), respectively.+--+-- This function minimizes. For maximization, use the function 'invert' on+-- the objective first.+solveOptimize :: Solver -> [Lit] {- ^ assumptions -}+ -> Unary {- ^ objective (for minimization) -}+ -> ((Int,Int) -> IO Bool) {- ^ callback -}+ -> IO (Maybe Bool)+solveOptimize s ass obj callback =+ do b <- solve s ass+ if b then+ -- there is a solution; let's optimize!+ let opti minTry minReached | minReached > minTry =+ do cont <- callback (minTry,minReached)+ if cont then+ do b <- solve s ([ obj .<= i | i <- [minReached-1,minReached-2..k] ] ++ ass)+ if b then+ do n <- U.modelValue s obj+ opti minTry n+ else+ do cfl <- conflict s+ let ass' = [i | i <- [k..minReached-1], neg (obj .<= i) `elem` cfl]+ opti (if null ass' then k+1 else minimum ass'+1) minReached+ else+ -- callback says: give up+ do return Nothing+ where+ k = (minTry+minReached) `div` 2++ opti _ _ =+ -- optimum reached+ do return (Just True)++ in do n <- U.modelValue s obj+ opti 0 n++ else+ -- no solution+ do return (Just False)+
+ SAT/Order.hs view
@@ -0,0 +1,205 @@+{-|+Module : SAT.Order+Description : Comparison functions on things that live in the SAT-solver++This module provides a type class with functions for asserting the ordering+of two objects, as well as functions that compute whether or+not an object compares to another object.+-}+module SAT.Order(+ -- * Functions+ isGreaterThan+ , isLessThan+ , isGreaterThanEqual+ , isLessThanEqual++ -- * Constraints+ , greaterThan+ , lessThan+ , greaterThanEqual+ , lessThanEqual++ , greaterThanOr+ , lessThanOr+ , greaterThanEqualOr+ , lessThanEqualOr++ -- * Type class+ , Order(..)+ )+ where++import SAT+import SAT.Equal+import SAT.Util++import Prelude+import Control.Monad ( when )++------------------------------------------------------------------------------++-- | Type class for things that can be compared.+--+-- New instances only need to define the 'lessTupleOr' function. However, if+-- there is no natural way to implement lexicographic ordering with the+-- instance type, it is possible to only define 'lessOr', in which case+-- the default definition of 'lessTupleOr' is less efficient.+--+-- For types where it is easy to see statically if the answer is going to+-- be True or False, a special definition of 'newLessLit' can be made. For+-- most types, the default definition should be enough.+class Order a where+ -- | Add constraints to the Solver that state that the first argument is+ -- less than the second, under the presence of a /disjunctive prefix/.+ -- The extra argument specifies if the comparison should be strict (False)+ -- or inclusive (True).+ -- (See 'SAT.Util.unconditionally' for what /prefix/ means.)+ lessOr :: Solver -> [Lit] -> Bool -> a -> a -> IO ()+ lessOr s pre incl x y = lessTupleOr s pre incl (x,()) (y,())++ -- | Create a literal that implies the specified relationship between+ -- the arguments.+ newLessLit :: Solver -> Bool -> a -> a -> IO Lit+ newLessLit s incl x y =+ do q <- newLit s+ lessOr s [neg q] incl x y+ return q++ -- | Add constraints to the Solver that state that the first argument is+ -- less than the second, under the presence of a /disjunctive prefix/.+ -- The extra argument specifies if the comparison should be strict (False)+ -- or inclusive (True).+ -- (See 'SAT.Util.unconditionally' for what /prefix/ means.) This function+ -- is typically not going to be used directly by a user of this library;+ -- use 'compareOr' instead.+ lessTupleOr :: Order b => Solver -> [Lit] -> Bool -> (a,b) -> (a,b) -> IO ()+ lessTupleOr s pre incl (x,p) (y,q) =+ do w <- newLessLit s incl p q+ if w == false || w == true then+ do lessOr s pre (w == true) x y+ else+ do lessOr s pre True x y -- x <= y+ lessOr s (w:pre) False x y -- x < y | p <~ q++------------------------------------------------------------------------------++-- | Add constraints to the Solver that state that the arguments have the+-- specified relationship.+greaterThan, greaterThanEqual, lessThan, lessThanEqual ::+ Order a => Solver -> a -> a -> IO ()+greaterThan = unconditionally greaterThanOr+greaterThanEqual = unconditionally greaterThanEqualOr+lessThan = unconditionally lessThanOr+lessThanEqual = unconditionally lessThanEqualOr++-- | Add constraints to the Solver that state that the arguments have the+-- specified relationship, under the presence of a /disjunctive prefix/.+-- (See 'SAT.Util.unconditionally' for what /prefix/ means.)+greaterThanOr, greaterThanEqualOr, lessThanOr, lessThanEqualOr ::+ Order a => Solver -> [Lit] -> a -> a -> IO ()+greaterThanOr s pre x y = lessThanOr s pre y x+greaterThanEqualOr s pre x y = lessThanEqualOr s pre y x+lessThanOr s pre x y = lessOr s pre False x y+lessThanEqualOr s pre x y = lessOr s pre True x y++-- | Return a literal that indicates whether or not the arguments have+-- the specified relationship.+isGreaterThan, isGreaterThanEqual, isLessThan, isLessThanEqual ::+ Order a => Solver -> a -> a -> IO Lit+isGreaterThan s x y = isLessThan s y x+isGreaterThanEqual s x y = isLessThanEqual s y x+isLessThan s x y = neg `fmap` isGreaterThanEqual s x y+isLessThanEqual s x y =+ do q <- newLessLit s True x y+ when (q /= false && q /= true) $+ greaterThanOr s [q] x y+ return q++------------------------------------------------------------------------------++instance Order () where+ lessOr s pre True _ _ = return ()+ lessOr s pre False _ _ = addClause s pre++ newLessLit s True _ _ = return true+ newLessLit s False _ _ = return false++ lessTupleOr s pre incl (_,p) (_,q) =+ lessOr s pre incl p q++instance Order Bool where+ lessTupleOr s pre incl (x,p) (y,q) =+ case x `compare` y of+ LT -> return ()+ EQ -> lessOr s pre incl p q+ GT -> addClause s pre++ newLessLit s incl x y =+ case x `compare` y of+ LT -> return true+ EQ -> return (bool incl)+ GT -> return false++instance Order Lit where+ lessTupleOr s pre incl (x,p) (y,q)+ | x == y = lessOr s pre incl p q+ | otherwise =+ do w <- newLessLit s incl p q+ addClause s ([y, w] ++ pre)+ addClause s ([neg x, w] ++ pre)+ addClause s ([neg x, y] ++ pre)++ newLessLit s incl x y+ | x == y = return (bool incl)+ | x == neg y = return y+ | x == false = return (if incl then true else y)+ | x == true = return (if incl then y else false)+ | y == false = return (if incl then neg x else false)+ | y == true = return (if incl then true else neg x)+ | otherwise = do q <- newLit s+ lessOr s [neg q] incl x y+ return q++instance (Order a, Order b) => Order (a,b) where+ lessOr s pre incl t1 t2 =+ lessTupleOr s pre incl t1 t2++ lessTupleOr s pre incl t1 t2 =+ lessTupleOr s pre incl (encTuple t1) (encTuple t2)++encTuple ((x,y),r) = (x,(y,r))++instance (Order a, Order b) => Order (Either a b) where+ lessTupleOr s pre incl (Left x1,z1) (Left x2,z2) =+ lessTupleOr s pre incl (x1,z1) (x2,z2)++ lessTupleOr s pre incl (Right y1,z1) (Right y2,z2) =+ lessTupleOr s pre incl (y1,z1) (y2,z2)++ lessTupleOr s pre incl (Left _,z1) (Right _,z2) =+ return ()++ lessTupleOr s pre incl (Right _,z1) (Left _,z2) =+ addClause s pre++------------------------------------------------------------------------------++instance (Order a, Order b, Order c) => Order (a,b,c) where+ lessTupleOr s pre incl t1 t2 =+ lessTupleOr s pre incl (encTriple t1) (encTriple t2)++encTriple ((x,y,z),r) = (x,(y,(z,r)))++instance Order a => Order (Maybe a) where+ lessTupleOr s pre incl m1 m2 =+ lessTupleOr s pre incl (encMaybe m1) (encMaybe m2)++encMaybe (Nothing, r) = (Left (), r)+encMaybe (Just x, r) = (Right x, r)++instance Order a => Order [a] where+ lessTupleOr s pre incl l1 l2 =+ lessTupleOr s pre incl (encList l1) (encList l2)++encList ([], r) = (Left (), r)+encList ((x:xs), r) = (Right (x,xs), r)
+ SAT/Term.hs view
@@ -0,0 +1,449 @@+{-|+Module : SAT.Term+Description : Representing sums of products of literals++This module can be used to implement so-called pseudo-boolean constraints.+These are constraints of the form:++@+a1 * x1 + ... + ak * xk <= c+@++where @a1@..@an@ and @c@ are integer constants, and @x1@..@xk@ are SAT literals.++To add such a constraint, simply create two terms:++@+lhs = fromList [(a1,x1),..,(ak,xk)]+rhs = number c+@++and use any of the comparison constraints in the 'Order' type class, for+example:++@+lessThanEqual s lhs rhs+@++When adding a constraint, terms are normalized as much as possible (so the+user does not have to worry about this). When creating terms, almost no+normalization happens.+-}+module SAT.Term(+ -- * Terms+ Term+ , SAT.Term.number+ , newTerm+ , newTermFrom+ , fromList+ , fromBinary+ , dumbFromUnary+ , fromUnary+ , toList+ , (.+.)+ , (.-.)+ , (.*)+ , minus+ , multiply+ , minValue+ , SAT.Term.maxValue+ , SAT.Term.modelValue+ )+ where++import SAT as S+import SAT.Bool+import SAT.Equal+import SAT.Order+import qualified SAT.Binary as B+import qualified SAT.Unary as U++import Data.List( sort, group, sortBy, groupBy, minimumBy )+import Data.Ord( comparing )++------------------------------------------------------------------------------++-- | A type to represent sums of products of literals.+data Term = Term{ toList :: [(Integer,Lit)] {- ^ Look inside a term. -} }+ deriving ( Eq, Ord )++instance Show Term where+ show (Term axs) =+ combine [ if x == true then show a else+ (if a == 1 then ""+ else if a == -1 then "-"+ else show a ++ "*")+ ++ show x+ | (a,x) <- axs+ , a /= 0+ ]+ where+ combine [] = "0"+ combine [x] = x+ combine (x:y:xs)+ | take 1 y == "-" = x ++ combine (y:xs)+ | otherwise = x ++ "+" ++ combine (y:xs)++-- | Create a fresh term, between 0 and n.+newTerm :: Solver -> Integer -> IO Term+newTerm s n = go [] 1 n+ where+ go axs _ 0 =+ do return (Term axs)++ go axs k n | k <= n =+ do x <- newLit s+ go ((k,x):axs) (2*k) (n-k)++ go axs k n =+ do x <- newLit s+ sequence_ [ addClause s (neg x : c) | c <- atLeast (k-n) (sum (map fst axs)) axs ]+ return (Term ((n,x):axs))+ where+ atLeast b s _ | b <= 0 =+ []++ atLeast b s _ | s < b =+ [ [] ]++ atLeast b s ((a,x):axs) =+ [ xs | xs <- atLeast (b-a) (s-a) axs ] +++ [ x : xs | xs <- atLeast b (s-a) axs ]++-- | Create a fresh term that can represent all numbers in the given list.+-- (Possibly more numbers, but never numbers smaller than the minimum or larger+-- than the maximum in the list.) +newTermFrom :: Solver -> [Integer] -> IO Term+newTermFrom s [] = return (number 0)+newTermFrom s ns = do t <- go (map (subtract n0) ns')+ return (t .+. number n0)+ where+ ns' = map head . group . sort $ ns+ n0 = minimum ns'+ + go [n] =+ do return (number n) -- n should be 0 here...++ go ns =+ do x <- newLit s+ t <- go ([ n | n <- ns, n < k ] `merge` [ n-k | n <- ns, n >= k ])+ return (fromList [(k,x)] .+. t)+ where+ k = compressor ns+ + compressor ns = go ns+ where+ m = last ns+ + go (x:y:xs) | 2*y > m = m-x+ go (_:xs) = go xs+ + [] `merge` ys = ys+ xs `merge` [] = xs+ (x:xs) `merge` (y:ys) =+ case x `compare` y of+ LT -> x : (xs `merge` (y:ys))+ EQ -> x : (xs `merge` ys)+ GT -> y : ((x:xs) `merge` ys)++-- | Create a constant term.+number :: Integer -> Term+number 0 = Term []+number n = Term [(n,true)]++-- | Create a term from a list of products.+fromList :: [(Integer,Lit)] -> Term+fromList axs = Term axs++-- | Create a term from a binary number.+fromBinary :: B.Binary -> Term+fromBinary b = Term [ (2^i,x) | (i,x) <- [0..] `zip` B.toList b ]++-- | Create a term from a unary number, the dumb way. This ignores the invariant+-- that unary numbers obey, but avoids creating new literals and clauses. Works OK+-- for unary numbers with few digits. The number of literals in the resulting term+-- is linear in the size of the unary number.+dumbFromUnary :: U.Unary -> Term+dumbFromUnary u = Term [ (1,x) | x <- U.toList u ]++-- | Create a term from a unary number, making use of the invariant+-- that unary numbers obey. This may create extra literals and clauses. The number+-- of literals in the resulting term is logarithmic in the size of the unary number.+fromUnary :: Solver -> U.Unary -> IO Term+fromUnary s u = Term `fmap` go (length xs) xs+ where+ xs = U.toList u++ go k xs | k <= 2 =+ do return [(1,x)|x<-xs]+ + go k xs =+ do ys <- sequence+ [ do y <- newLit s+ addClause s [ neg x1, y]+ addClause s [neg x, x1, neg y]+ addClause s [ x, neg x0, y]+ addClause s [ x0, neg y]+ return y+ | (x0,x1) <- xs0 `zipp` xs1+ ]+ zs <- go (k-i) ys+ return ((fromIntegral i,x):zs)+ where+ i = (k+1) `div` 2+ xs0 = take (i-1) xs+ x = xs!!(i-1)+ xs1 = drop i xs+ + [] `zipp` [] = []+ xs `zipp` [] = xs `zipp` [false]+ [] `zipp` ys = [false] `zipp` ys+ (x:xs) `zipp` (y:ys) = (x,y):zipp xs ys++-- | Add two terms.+(.+.) :: Term -> Term -> Term+Term axs .+. Term bys = Term (axs ++ bys)++-- | Subtract two terms.+(.-.) :: Term -> Term -> Term+t1 .-. t2 = t1 .+. minus t2++-- | Multiply a term by a constant.+(.*) :: Integer -> Term -> Term+c .* Term axs = Term [ (c*a,x) | c /= 0, (a,x) <- axs, a /= 0 ]++-- | Negate a term.+minus :: Term -> Term+minus t = (-1) .* t++-- | Multiply a term by another term (creates extra clauses and literals).+multiply :: Solver -> Term -> Term -> IO Term+multiply s (Term axs) (Term bys) =+ do cxs <- sequence+ [ do z <- andl s [x,y]+ return (a*b,z)+ | (a,x) <- norm axs+ , a /= 0+ , (b,y) <- norm bys+ , b /= 0+ ]+ return (Term cxs)+ where+ -- TODO: could also merge positive/negative literals here+ norm = filter ((/=0) . fst)+ . map (\(xas@((x,_):_)) -> (sum (map snd xas),x))+ . groupBy (\(x,_) (y,_) -> x == y)+ . sort+ . map swap+ . filter ((/=false) . snd)++ swap (a,x) = (x,a)++-- | Compute the minimum value of a term.+minValue :: Term -> Integer+minValue (Term axs) = sum [ a | (a,x) <- axs, x == true || (a < 0 && x /= false) ]++-- | Compute the maximum value of a term.+maxValue :: Term -> Integer+maxValue (Term axs) = sum [ a | (a,x) <- axs, x == true || (a > 0 && x /= false) ]++-- | Look at the value of a term.+modelValue :: Solver -> Term -> IO Integer+modelValue s (Term axs) =+ do ns <- sequence [ val a `fmap` S.modelValue s x | (a,x) <- axs ]+ return (sum ns)+ where+ val a False = 0+ val a True = a++------------------------------------------------------------------------------++instance Equal Term where+ equalOr s pre t1 t2 =+ do lessThanEqualOr s pre t1 t2+ lessThanEqualOr s pre t2 t1++ notEqualOr s pre t1 t2 =+ do q <- newLit s+ lessThanOr s (q :pre) t1 t2+ lessThanOr s (neg q:pre) t2 t1++instance Order Term where+ lessOr s pre incl t1 t2 =+ addNormedConstrOr s pre (norm ((t1 .-. t2) :<=: (if incl then 0 else (-1))))++------------------------------------------------------------------------------++data Constr = Term :<=: Integer++-- | Normalizes an LEQ-constraint.+-- After normalization:+-- 1. Constant literals do not occur+-- 2. Every literal only occurs at most once; either positively or negatively+-- 3. All factors are strictly positive+-- 4. We have divided by appropriate constants as much as we can+-- (..still an open problem for now..)+norm :: Constr -> Constr+norm = normFactorize+ . normPositive+ . normLiterals++normLiterals :: Constr -> Constr+normLiterals (Term axs :<=: k) =+ Term [ ax | ax@(a,x) <- axs1, a /= 0, x /= true ]+ :<=:+ (k - sum [ a | (a,x) <- axs1, x == true ])+ where+ keep x | x == true = True+ | x == false = False+ | otherwise = pos x++ axs0 = [ ax | ax@(_,x) <- axs+ , keep x+ ]+ ++ [ by | (a,x) <- axs+ , not (keep x)+ , by <- [ (-a, neg x), (a, true) ]+ ]++ axs1 = map (\(axs@((_,x):_)) -> (sum (map fst axs), x))+ $ groupBy eqLit+ $ sortBy cmpLit axs0++ (_,x) `eqLit` (_,y) = x == y+ (_,x) `cmpLit` (_,y) = x `compare` y++normPositive :: Constr -> Constr+normPositive (Term axs :<=: k) =+ Term [ if a > 0 then (a, x) else (-a, neg x) | (a,x) <- axs, a /= 0 ]+ :<=:+ (k + sum [ -a | (a,x) <- axs, a < 0 ])++normFactorize :: Constr -> Constr+normFactorize constr@(Term axs :<=: k) =+ Term [ (a `div` n, x) | (a,x) <- axs ] :<=: (k `div` n)+ where+ n | null axs = 1+ | otherwise = foldr1 gcd [ a | (a,_) <- axs ]++------------------------------------------------------------------------------++-- | Adds a normalized LEQ-constraint.+addNormedConstrOr :: Solver -> [Lit] -> Constr -> IO ()+addNormedConstrOr s pre (Term axs :<=: k) =+ do --putStrLn (show axs ++ " <= " ++ show k)+ go pre (reverse (sort axs)) k+ where+ -- all 1+ --go pre axs k | all (==1) (map fst axs) =+ -- do putStrLn (show pre ++ " | ALL 1: " ++ show (Term axs) ++ " <= " ++ show k)++ -- expand whenever possible+ go pre axs k | k <= 0 || n <= 8 || cs `lengthLeq` 64 =+ do --if not (null cs)+ -- then putStrLn (show pre ++ " | " ++ show axs ++ " <= " ++ show k)+ -- else return ()+ sequence_ [ do addClause s (pre ++ c) {- ; print (pre ++ c) -} | c <- cs ]+ where+ n = length axs+ cs = expand axs (sum [ a | (a,_) <- axs ]) k+ + expand _ m k | k < 0 = [[]]+ expand _ m k | m <= k = []+ expand ((a,x):axs) m k =+ [ neg x : c | c <- expand axs m' (k-a) ] +++ expand axs m' k+ where+ m' = m-a++ (_:_) `lengthLeq` 0 = False+ [] `lengthLeq` _ = True+ (_:xs) `lengthLeq` n = xs `lengthLeq` (n-1)++ -- case split on largest coefficient whenever possible+ go pre ((a,x):axs) k | a >= k || a >= sum [ a | (a,_) <- axs ] =+ do go (neg x : pre) axs (k-a)+ go pre axs k++ -- split according to p*A + B <= k --> A <= t & p*t + B <= k+ go pre axs@((a,_):_) k =+ do i <- newTerm s (maxI-minI)+ let t = number minI .+. i+ --putStrLn ("t = " ++ show t)+ --putStrLn (show minI ++ " <= t <= " ++ show maxI)+ --putStrLn (show (Term axs') ++ " <= t")+ --putStrLn (show p ++ " * t + " ++ show (Term bxs) ++ " <= " ++ show k)+ if p > 1 && myc <= c then error "cost!" else return ()+ lessThanEqualOr s pre (Term axs') t+ lessThanEqualOr s pre (p .* t .+. Term bxs) (number k)+ where+ n = length axs+ n2 = n `div` 2++ (p, axs', bxs, minI, maxI) =+ minimumOn cost possibilities++ myc = cost (1, axs, [], 0, 0)+ c = cost (p, axs', bxs, minI, maxI)++ cost (p, axs', bxs, minI, maxI) =+ if p == 1+ then (ca,va) `max` (cb,vb)+ else (cb, vb)+ where+ r = maxI - minI+ v = log2 r+ va = length axs' + v+ vb = length bxs + v+ ca = sum [ a | (a,_) <- axs' ] + r+ cb = sum [ abs b | (b,_) <- bxs ] + p*r++ log2 0 = 0+ log2 n = 1 + log2 (n `div` 2)++ addRange (p, axs', bxs) = (p, axs', bxs, minI, maxI)+ where+ minL = 0 -- = minValue (Term axs')+ maxL = maxValue (Term axs')+ minR = (k - maxValue (Term bxs)) `div` p+ maxR = (k - minValue (Term bxs)) `div` p+ minI = minL `max` minR+ maxI = maxL `min` maxR++ possibilities =+ map addRange $+ [ (1, axs', take n2 axs)+ | let axs' = reverse (drop n2 axs)+ -- , tight 1 axs'+ ] +++ [ (p, axs', bxs)+ | p <- ps+ , let dmxs = [ (a `aDivMod` p,x) | (a,x) <- axs ]+ axs' = [ (d,x) | ((d,_),x) <- dmxs, d /= 0 ]+ bxs = [ (m,x) | ((_,m),x) <- dmxs, m /= 0 ]+ ]++ tight s [] = True+ tight s ((a,_):axs) = a <= s && tight (s+a) axs++ a `aDivMod` p+ | abs m2 < m1 = (d2,m2)+ | otherwise = (d1,m1)+ where+ (d1,m1) = (a `div` p, a `mod` p)+ (d2,m2) = (d1+1,m1-p)++ ps = map head . group . sort $+ takeWhile (<=a) [2,3,5,7] +++ as ++ gcds as+ where+ as = [ a | (a,_) <- axs, a /= 1 ]++ gcds [] = []+ gcds [_] = []+ gcds xs = zipWith gcd xs (tail xs ++ [head xs])++minimumOn :: Ord b => (a -> b) -> [a] -> a+minimumOn f xs = snd . minimumBy (comparing fst) $ [ (f x, x) | x <- xs ]++------------------------------------------------------------------------------
+ SAT/Unary.hs view
@@ -0,0 +1,321 @@+{-|+Module : SAT.Unary+Description : Functions for working with natural numbers represented as+ unary numbers.+-}+module SAT.Unary(+ -- * The Unary type+ Unary+ , newUnary+ , zero+ , number+ , digit+ , maxValue++ -- * Comparison against constants+ , (.<=), (.<), (.>), (.>=)++ -- * Counting+ , count+ , countUpTo+ , add+ , addList+ , mul1+ , mul++ -- * Operations+ , invert+ , succ+ , pred+ , (**)+ , (//)+ , modulo+ + -- * Conversion+ , unsafeFromList+ , toList++ -- * Models+ , modelValue+ )+ where++import SAT hiding ( modelValue )+import qualified SAT+import SAT.Bool+import SAT.Equal+import SAT.Order+import Data.List( sort, insert, transpose )++import Prelude hiding ( Enum(succ,pred), (**) )++------------------------------------------------------------------------------++-- | The type Unary, for natural numbers represented in unary+data Unary = Unary Int [Lit] -- sorted 11..1100..00+ deriving ( Eq, Ord )++instance Show Unary where+ show (Unary _ xs) = show xs++-- | Creates a unary number from a list of digits. WARNING ("unsafe"): this +-- function assumes that the list of digits is sorted 11..1100..00.+unsafeFromList :: [Lit] -> Unary+unsafeFromList xs = Unary (length xs) xs++-- | Returns the list of digits of a unary number.+toList :: Unary -> [Lit]+toList (Unary _ xs) = xs++-- | Creates a fresh unary number, with the specified maximum value.+newUnary :: Solver -> Int -> IO Unary+newUnary s n =+ do xs <- sequence [ newLit s | i <- [1..n] ]+ sequence_ [ addClause s [neg y, x] | (x,y) <- xs `zip` tail xs ]+ return (Unary n xs)++-- | Creates 0 as a unary number.+zero :: Unary+zero = Unary 0 []++-- | Creates n as a unary number.+number :: Int -> Unary+number n = Unary n (replicate n true)++-- | Successor.+succ :: Unary -> Unary+succ (Unary n xs) = Unary (n+1) (true : xs)++-- | Predecessor (but 0 goes to 0).+pred :: Unary -> Unary+pred (Unary _ []) = Unary 0 []+pred (Unary n (_:xs)) = Unary (n-1) xs++-- | Creates a 1-digit unary number, specified by the given literal.+digit :: Lit -> Unary+digit x = Unary 1 [x]++-- | Inverts a unary number; computes /maxValue n - n/. Can be used to maximize+-- instead of minimize.+invert :: Unary -> Unary+invert (Unary n xs) = Unary n (reverse (map neg xs))++-- | Compares a unary number with a constant.+(.<=), (.<), (.>=), (.>) :: Unary -> Int -> Lit+--u .> k = u .>= (k+1)+u .< k = neg (u .>= k)+u .<= k = u .< (k+1)+u .>= k = u .> (k-1)++Unary n xs .> k+-- | length xs /= n = error ("unary: length " ++ show xs ++ " /= " ++ show n)+ | k < 0 = true+ | k >= n = false+ | otherwise = xs !! k++-- | Integer multiplication by a (non-negative) constant.+(**) :: Unary -> Int -> Unary+Unary n xs ** k =+ -- Idea: expand every literal k times.+ Unary (n * k) (concat [ replicate k x | x <- xs ])++-- | Integer division by a (strictly positive) constant.+(//) :: Unary -> Int -> Unary+Unary n xs // k =+ -- Idea: take every k-th literal.+ Unary (n `div` k)+ [ x | (x,True) <- xs `zip` cycle (replicate (k-1) False ++ [True]) ]++-- | Integer modulo a (strictly positive) constant.+modulo :: Solver -> Unary -> Int -> IO Unary+modulo s (Unary n xs) k =+ -- Idea: We start with a unary number, say+ -- 1 1 1 1 1 1 1 0 0 0 0 0 0+ -- and we take modulo, say 3. First, we divide in groups of 3:+ -- [1 1 1] [1 1 1] [1 0 0] [0 0 0] [0]+ -- and pad:+ -- [1 1 1] [1 1 1] [1 0 0] [0 0 0] [0 0 0]+ -- We know there will only be at most one group that contains+ -- both 1's and 0's. That group is the answer (minus the last element+ -- because we know it will be 0).+ -- (If there is no such group, the answer is simply [0 0].)+ -- First, we "neutralize" every group [1 1 1], by taking away the+ -- last literal in each group, negating it, and and-ing it with the rest:+ -- [0 0] [0 0] [1 0] [0 0] [0 0]+ -- Then, we transpose:+ -- [0 0 1 0 0]+ -- [0 0 0 0 0]+ -- and we take the or of each row:+ -- [1 0]+ -- which is the right answer.+ do xss1 <- sequence [ sequence [ andl s [neg a, x] | x <- init as ]+ | as <- xss+ , let a = last as+ ]+ ys <- sequence [ orl s bs | bs <- transpose xss1 ]+ return (Unary (if null ys then 0 else k-1) ys)+ where+ xss = map pad . takeWhile (not . null) . map (take k) . iterate (drop k) $ xs+ pad = take k . (++ repeat false)++-- | Returns a unary number that represents the number of true literals in+-- the given list.+count :: Solver -> [Lit] -> IO Unary+count s xs = addList s (map digit xs)++-- | Like 'count', but chops the result off at k.+countUpTo :: Solver -> Int -> [Lit] -> IO Unary+countUpTo s k xs = addListUpTo s k (map digit xs)++-- | Adds up two unary numbers.+add :: Solver -> Unary -> Unary -> IO Unary+add s (Unary n xs) (Unary m ys) =+ do zs <- merge s (n+m) xs ys+ return (Unary (n+m) zs)++-- | Like 'add', but chops the result off at k.+addUpTo :: Solver -> Int -> Unary -> Unary -> IO Unary+addUpTo s k (Unary n xs) (Unary m ys) =+ do zs <- merge s k xs ys+ return (Unary (k `min` (n+m)) zs)++merge :: Solver -> Int -> [Lit] -> [Lit] -> IO [Lit]+merge s k [] ys = return (take k ys)+merge s k xs [] = return (take k xs)++merge s 0 [x] [y] =+ do return []++merge s 1 [x] [y] =+ do b <- orl s [x,y]+ return [b]++merge s k [x] [y] =+ do a <- andl s [x,y]+ b <- orl s [x,y]+ return [b,a]++merge s k xs ys =+ do zs0 <- merge s k xs0 ys0+ zs1 <- merge s k xs1 ys1+ let zs = zs0 `ilv` zs1+ zss <- sequence [ merge s 2 [v] [w] | (v,w) <- pairs (tail zs) ]+ return (take k ([head zs] ++ concat zss ++ [last zs]))+ where+ a = length xs+ b = length ys+ n' = a `max` b+ n = if even n' then n' else n'+1 -- apparently not needed?+ xs' = xs ++ replicate (n-a) false+ ys' = ys ++ replicate (n-b) false+ xs0 = evens xs'+ xs1 = odds xs'+ ys0 = evens ys'+ ys1 = odds ys'++ evens (x:xs) = x : odds xs+ evens [] = []++ odds (x:xs) = evens xs+ odds [] = []++ pairs (x:y:xs) = (x,y) : pairs xs+ pairs _ = []++ (x:xs) `ilv` ys = x : (ys `ilv` xs)+ [] `ilv` ys = ys++-- | Returns the maximum value a given unary number can have.+maxValue :: Unary -> Int+maxValue (Unary n _) = n++-- | Adds up a list of unary numbers. When adding more than 2 numbers, this+-- function is preferred over linearly folding the function 'add' over a list,+-- because a balanced tree (based on the sizes of the numbers involved) is+-- constructed by this function, which creates a lot less clauses than doing+-- it the naive way.+addList :: Solver -> [Unary] -> IO Unary+addList s us = go (sort us)+ where+ go [] =+ do return zero++ go [u] =+ do return u++ go (u1:u2:us) =+ do u <- add s u1 u2+ go (insert u us)++-- | Like 'addList', but chops the result off at k.+addListUpTo :: Solver -> Int -> [Unary] -> IO Unary+addListUpTo s 0 us = return zero+addListUpTo s k us = go (sort us)+ where+ go [] =+ do return zero++ go [u] =+ do return u++ go (u1:u2:us) =+ do u <- addUpTo s k u1 u2+ go (insert u us)++-- | Multiplies a digit and a unary number.+mul1 :: Solver -> Lit -> Unary -> IO Unary+mul1 s x (Unary m ys) =+ do ys' <- sequence [ andl s [x,y] | y <- ys ]+ return (Unary m ys')++-- | Multiplies two unary numbers.+mul :: Solver -> Unary -> Unary -> IO Unary+mul s (Unary n xs) b@(Unary m ys) | n <= m =+ do bs <- sequence [ mul1 s x b | x <- xs ]+ addList s bs+mul s x y = mul s y x++-- | Return the numeric value of a unary number in the current model.+-- (/Use only when 'solve' has returned True!/)+modelValue :: Solver -> Unary -> IO Int+modelValue s (Unary _ xs) = go xs+ where+ go [] = do return 0+ go (x:xs) = do b <- SAT.modelValue s x+ if b then+ (+1) `fmap` go xs+ else+ return 0++------------------------------------------------------------------------------++instance Equal Unary where+ equalOr s pre u1 u2 =+ -- this generates precisely all bi-implications+ do lessThanEqualOr s pre u1 u2+ lessThanEqualOr s pre u2 u1++ notEqualOr s pre u1 u2 =+ -- this only needs one helper variable+ do q <- newLit s+ lessThanOr s (q :pre) u1 u2+ lessThanOr s (neg q:pre) u2 u1++instance Order Unary where+ lessOr s pre False u v =+ do lessOr s pre True (succ u) v++ lessOr s pre True (Unary _ xs) (Unary _ ys) = leq xs ys+ where+ leq [] _ =+ do return ()++ leq (x:xs) [] =+ do addClause s (neg x : pre)+ -- do not need to recurse here++ leq (x:xs) (y:ys) =+ do addClause s (neg x : y : pre)+ leq xs ys++------------------------------------------------------------------------------
+ SAT/Util.hs view
@@ -0,0 +1,46 @@+module SAT.Util where++import SAT+import Data.List( sort, group )++------------------------------------------------------------------------------++-- | Turn a Solver-function with prefix into a Solver-function without prefix.+--+-- All constraint-generating functions in this library have two versions: One+-- that unconditionally adds the constraint, and one that makes use of a+-- /disjunctive prefix/.+-- When the prefix is used, the actual constraint that is added is the+-- disjunction between the prefix and the constraint the function generates.+--+-- The naming scheme works as follows. If the unconditional function is:+--+-- @someConstraint :: Solver -> ... -> IO ()@+--+-- then the prefixed version is:+--+-- @someConstraintOr :: Solver -> [Lit] -> ... -> IO ()@+--+-- It is always the case that:+--+-- @someConstraint = unconditionally someConstraintOr@+--+-- The disjunctive prefix is typically used to conditionally add the+-- constraint. For example, if we say:+--+-- @someConstraintOr s [neg x] ...@+-- +-- (i.e. the prefix is @[neg x]@), then the someConstraint is only asserted+-- when @x@ is True.+--+-- If the prefix is empty, it degenerates to the function without prefix.+unconditionally :: (Solver -> [Lit] -> abc) -> (Solver -> abc)+unconditionally f = \s -> f s []++------------------------------------------------------------------------------++-- | Sort and remove duplicates.+usort :: Ord a => [a] -> [a]+usort = map head . group . sort++------------------------------------------------------------------------------
+ SAT/Val.hs view
@@ -0,0 +1,149 @@+{-|+Module : SAT.Val+Description : Functions for working with symbolic values+-}+module SAT.Val(+ -- * The Val type+ Val+ , newVal+ , val++ -- * Inspection+ , (.=)+ , domain++ -- * Models+ , modelValue+ )+ where++import qualified SAT+import SAT hiding ( modelValue )+import SAT.Util( usort )+import SAT.Bool( atMostOne )+import SAT.Equal+import SAT.Order++import Data.List( tails )+import Control.Monad( when )++------------------------------------------------------------------------------++-- | The Val type, for representing symbolic values.+newtype Val a = Val [(Lit,a)]+ deriving ( Eq, Ord, Show )++-- | Creates a symbolic value, with concrete values all elements of the+-- specified list. The list has to be non-empty.+newVal :: Ord a => Solver -> [a] -> IO (Val a)+newVal s xs =+ case xs' of+ [] -> do error "SAT.Val.newVal: empty list"+ [x] -> do return (val x)+ [x,y] -> do q <- newLit s+ return (Val [(q,x),(neg q,y)])+ _ -> do qs <- sequence [ newLit s | x <- xs' ]+ addClause s qs+ atMostOne s qs+ return (Val (qs `zip` xs'))+ where+ xs' = usort xs++-- | Creates a symbolic value with only one concrete element.+val :: a -> Val a+val x = Val [(true,x)]++-- | Returns all possible concrete values for a symbolic value.+domain :: Val a -> [a]+domain (Val qxs) = map snd qxs++-- | Returns the literal representing the symbolic value having the concrete+-- specified value.+(.=) :: Ord a => Val a -> a -> Lit+Val qxs .= x = go qxs+ where+ go [] = false+ go ((q,y):qxs) =+ case x `compare` y of+ LT -> false+ EQ -> q+ GT -> go qxs++------------------------------------------------------------------------------++instance Ord a => Equal (Val a) where+ equalOr s pre p q =+ sequence_+ [ case pqx of+ (Just p, Nothing, _) -> addClause s (neg p : pre)+ (Nothing, Just q, _) -> addClause s (neg q : pre)+ (Just p, Just q, _) -> addClause s (neg p : q : pre)+ | pqx <- stitch p q+ ]++ notEqualOr s pre p q =+ sequence_+ [ case pqx of+ (Just p, Just q, _) -> addClause s (neg p : neg q : pre)+ _ -> return ()+ | pqx <- stitch p q+ ]++instance Ord a => Order (Val a) where+ lessTupleOr s pre incl (x,p) (y,q) =+ do w <- newLessLit s incl p q+ when (w /= true) $+ notEqualOr s (w:pre) x y+ sandwich false true n xys+ where+ xys = [ (lit a,lit b) | (a,b,_) <- stitch x y ]+ n = length xys++ lit Nothing = false+ lit (Just x) = x++ sandwich lft rgt _ [] =+ do return ()++ sandwich lft rgt n xys | n <= 2 =+ do sequence_ [ addClause s (neg lft : neg x : pre) | (x,_) <- xys ]+ sequence_ [ addClause s (rgt : neg y : pre) | (_,y) <- xys ]+ sequence_ [ addClause s (neg y : neg x : pre)+ | (_,y):xys' <- tails xys+ , (x,_) <- xys'+ ]++ sandwich lft rgt n xys =+ do lft' <- newLit s+ rgt' <- newLit s+ addClause s [neg lft, lft']+ addClause s [neg rgt', lft']+ addClause s [neg rgt', rgt]+ sandwich lft rgt' k (take k xys)+ sandwich lft' rgt (n-k) (drop k xys)+ where+ k = n `div` 2++stitch :: Ord a => Val a -> Val a -> [(Maybe Lit, Maybe Lit, a)]+stitch (Val pxs) (Val qys) = go pxs qys+ where+ go [] qys = [ (Nothing, Just q, y) | (q,y) <- qys ]+ go pxs [] = [ (Just p, Nothing, x) | (p,x) <- pxs ]+ go ((p,x):pxs) ((q,y):qys) =+ case x `compare` y of+ LT -> (Just p, Nothing, x) : go pxs ((q,y):qys)+ EQ -> (Just p, Just q, x) : go pxs qys+ GT -> (Nothing, Just q, y) : go ((p,x):pxs) qys++------------------------------------------------------------------------------++-- | Returns the concrete value of the symbolic value in the found model.+-- (/Only use when 'solve' has returned True!/)+modelValue :: Solver -> Val a -> IO a+modelValue s (Val qxs) = go qxs+ where+ go [] = error "SAT.Val.modelValue: no trues in list"+ go ((q,x):qxs) = do b <- SAT.modelValue s q+ if b then return x else go qxs++------------------------------------------------------------------------------
+ SAT/Value.hs view
@@ -0,0 +1,107 @@+{-|+Module : SAT.Value+Description : Reading off the value of things in models+-}+{-# LANGUAGE TypeFamilies #-}+module SAT.Value where++import SAT ( Solver )+import qualified SAT as S+import qualified SAT.Val as V+import qualified SAT.Unary as U+import qualified SAT.Term as T+import qualified SAT.Binary as B++import Control.Monad ( liftM2, liftM3 )++------------------------------------------------------------------------------++-- | A class for symbolic objects that have Haskell values in models.+class Value a where+ -- | The Haskell type for the symbolic object a.+ type Type a++ -- | Return the value of the object in the current model.+ -- /Only use if 'solve' has returned True!/+ getValue :: Solver -> a -> IO (Type a)++------------------------------------------------------------------------------++instance Value () where+ type Type () = ()++ getValue _ _ = return ()++instance Value S.Lit where+ type Type S.Lit = Bool++ getValue = S.modelValue++instance Value Bool where+ type Type Bool = Bool++ getValue _ = return++instance Value Int where+ type Type Int = Int++ getValue _ = return++instance Value Integer where+ type Type Integer = Integer++ getValue _ = return++------------------------------------------------------------------------------++instance (Value a, Value b) => Value (a,b) where+ type Type (a,b) = (Type a, Type b)++ getValue s (x,y) = liftM2 (,) (getValue s x) (getValue s y)++instance (Value a, Value b, Value c) => Value (a,b,c) where+ type Type (a,b,c) = (Type a, Type b, Type c)++ getValue s (x,y,z) = liftM3 (,,) (getValue s x) (getValue s y) (getValue s z)++instance (Value a, Value b) => Value (Either a b) where+ type Type (Either a b) = Either (Type a) (Type b)++ getValue s (Left x) = Left `fmap` getValue s x+ getValue s (Right y) = Right `fmap` getValue s y++instance Value a => Value [a] where+ type Type [a] = [Type a]++ getValue s xs = sequence [ getValue s x | x <- xs ]++instance Value a => Value (Maybe a) where+ type Type (Maybe a) = Maybe (Type a)++ getValue s Nothing = return Nothing+ getValue s (Just x) = Just `fmap` getValue s x++------------------------------------------------------------------------------++instance Value (V.Val a) where+ type Type (V.Val a) = a++ getValue = V.modelValue++instance Value U.Unary where+ type Type U.Unary = Int++ getValue = U.modelValue++instance Value T.Term where+ type Type T.Term = Integer++ getValue = T.modelValue++instance Value B.Binary where+ type Type B.Binary = Integer++ getValue = B.modelValue++------------------------------------------------------------------------------+
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ satplus.cabal view
@@ -0,0 +1,70 @@+-- Initial satplus.cabal generated by cabal init. For further+-- documentation, see http://haskell.org/cabal/users-guide/++-- The name of the package.+name: satplus++-- The package version. See the Haskell package versioning policy (PVP)+-- for standards guiding when and how versions should be incremented.+-- http://www.haskell.org/haskellwiki/Package_versioning_policy+-- PVP summary: +-+------- breaking API changes+-- | | +----- non-breaking API additions+-- | | | +--- code changes with no API change+version: 0.1.0.0++-- A short (one-line) description of the package.+synopsis: Useful functions when programming with a SAT-solver++-- A longer description of the package.+-- description:++-- URL for the project homepage or repository.+homepage: https://github.com/koengit/satplus/++-- The license under which the package is released.+license: BSD3++-- The file containing the license text.+license-file: LICENSE++-- The package author(s).+author: Koen Claessen++-- An email address to which users can send suggestions, bug reports, and+-- patches.+maintainer: koen@chalmers.se++-- A copyright notice.+-- copyright:++category: Logic++build-type: Simple++-- Extra files to be distributed with the package, such as examples or a+-- README.+extra-source-files: README.md++-- Constraint on the version of Cabal needed to build this package.+cabal-version: >=1.10+++library+ -- Modules exported by the library.+ exposed-modules: SAT, SAT.Optimize, SAT.Unary, SAT.Util, SAT.Term, SAT.Value, SAT.Order, SAT.Binary, SAT.Val, SAT.Bool, SAT.Equal++ -- Modules included in this library but not exported.+ -- other-modules: SAT.Test++ -- LANGUAGE extensions used by modules in this package.+ -- other-extensions:++ -- Other library packages from which modules are imported.+ build-depends: base >=4 && < 5, minisat >=0.1++ -- Directories containing source files.+ -- hs-source-dirs:++ -- Base language which the package is written in.+ default-language: Haskell2010+