diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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. diff --git a/SAT.hs b/SAT.hs new file mode 100644 --- /dev/null +++ b/SAT.hs @@ -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 + +------------------------------------------------------------------------------ diff --git a/SAT/Binary.hs b/SAT/Binary.hs new file mode 100644 --- /dev/null +++ b/SAT/Binary.hs @@ -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 + +------------------------------------------------------------------------------ + diff --git a/SAT/Bool.hs b/SAT/Bool.hs new file mode 100644 --- /dev/null +++ b/SAT/Bool.hs @@ -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 + +------------------------------------------------------------------------------ diff --git a/SAT/Equal.hs b/SAT/Equal.hs new file mode 100644 --- /dev/null +++ b/SAT/Equal.hs @@ -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) + +------------------------------------------------------------------------------ diff --git a/SAT/Optimize.hs b/SAT/Optimize.hs new file mode 100644 --- /dev/null +++ b/SAT/Optimize.hs @@ -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) + diff --git a/SAT/Order.hs b/SAT/Order.hs new file mode 100644 --- /dev/null +++ b/SAT/Order.hs @@ -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) diff --git a/SAT/Term.hs b/SAT/Term.hs new file mode 100644 --- /dev/null +++ b/SAT/Term.hs @@ -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 ] + +------------------------------------------------------------------------------ diff --git a/SAT/Unary.hs b/SAT/Unary.hs new file mode 100644 --- /dev/null +++ b/SAT/Unary.hs @@ -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 + +------------------------------------------------------------------------------ diff --git a/SAT/Util.hs b/SAT/Util.hs new file mode 100644 --- /dev/null +++ b/SAT/Util.hs @@ -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 + +------------------------------------------------------------------------------ diff --git a/SAT/Val.hs b/SAT/Val.hs new file mode 100644 --- /dev/null +++ b/SAT/Val.hs @@ -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 + +------------------------------------------------------------------------------ diff --git a/SAT/Value.hs b/SAT/Value.hs new file mode 100644 --- /dev/null +++ b/SAT/Value.hs @@ -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 + +------------------------------------------------------------------------------ + diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/satplus.cabal b/satplus.cabal new file mode 100644 --- /dev/null +++ b/satplus.cabal @@ -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 +