diff --git a/Main.hs b/Main.hs --- a/Main.hs +++ b/Main.hs @@ -14,7 +14,7 @@ import Control.Monad( when, forM_ ) import Data.Array.Unboxed( elems ) -import Data.List( intersperse ) +import Data.Int( Int64 ) import Data.Version( showVersion ) import Funsat.Solver ( solve @@ -22,7 +22,8 @@ , defaultConfig , ShowWrapped(..) , statTable ) -import Funsat.Types( CNF(..), FunsatConfig(..), ConflictCut(..) ) +import Funsat.Types( CNF(..) ) +import Funsat.Types.Internal( FunsatConfig(..) ) import Paths_funsat( version ) import Prelude hiding ( elem ) import System.Console.GetOpt @@ -34,45 +35,31 @@ import qualified Language.CNF.Parse.ParseDIMACS as ParseDIMACS import qualified Text.Tabular as Tabular +#ifdef TESTING import qualified Properties +#endif options :: [OptDescr (Options -> Options)] options = [ Option [] ["restart-at"] - (ReqArg (\i o -> - let c = optFunsatConfig o - in o{ optFunsatConfig = c{configRestart = read i} }) "INT") - (withDefault (configRestart . optFunsatConfig) + (ReqArg (\i o -> o{ optRestartAt = read i }) "INT") + (withDefault optRestartAt "Restart after INT conflicts.") , Option [] ["restart-bump"] - (ReqArg (\d o -> - let c = optFunsatConfig o - in o{ optFunsatConfig = c{configRestartBump = read d} }) "FLOAT") - (withDefault (configRestartBump . optFunsatConfig) + (ReqArg (\d o -> o{ optRestartBump = read d }) "FLOAT") + (withDefault optRestartBump "Alter the number of conflicts required to restart by multiplying by FLOAT.") - , Option [] ["no-vsids"] (NoArg $ \o -> - let c = optFunsatConfig o - in o{ optFunsatConfig = c{configUseVSIDS = False} }) + , Option [] ["no-vsids"] (NoArg $ \o -> o{ optUseVsids = False }) "Use static variable ordering." - , Option [] ["no-restarts"] (NoArg $ \o -> - let c = optFunsatConfig o - in o{ optFunsatConfig = c{configUseRestarts = False} }) + , Option [] ["no-restarts"] (NoArg $ \o -> o{ optUseRestarts = False }) "Never restart." - - , Option [] ["conflict-cut"] - (ReqArg (\cut o -> - let c = optFunsatConfig o - in o{ optFunsatConfig = c{configCut = readCutOption cut} }) "1|d") - "Which cut of the conflict graph to use for learning. 1=first UIP; d=decision lit" - +#ifdef TESTING , Option [] ["verify"] (NoArg $ \o -> o{ optVerify = True }) "Run quickcheck properties and unit tests." - - , Option [] ["profile"] (NoArg $ \o -> o{ optProfile = True }) - "Run solver. (assumes profiling build)" +#endif , Option [] ["print-features"] (NoArg $ \o -> o{ optPrintFeatures = True }) "Print the optimisations the SAT solver supports and exit." @@ -82,27 +69,23 @@ ] data Options = Options - { optVerify :: Bool - , optProfile :: Bool + { optRestartAt :: Int64 + , optRestartBump :: Double + , optUseVsids :: Bool + , optUseRestarts :: Bool + , optVerify :: Bool , optPrintFeatures :: Bool - , optFunsatConfig :: FunsatConfig , optVersion :: Bool } deriving (Show) defaultOptions :: Options defaultOptions = Options - { optVerify = False - , optProfile = False - , optVersion = False + { optRestartAt = configRestart defaultConfig + , optRestartBump = configRestartBump defaultConfig + , optUseVsids = True + , optUseRestarts = True + , optVerify = False , optPrintFeatures = False - , optFunsatConfig = defaultConfig } - -optUseVsids, optUseRestarts :: Options -> Bool -optUseVsids = configUseVSIDS . optFunsatConfig -optUseRestarts = configUseRestarts . optFunsatConfig - -readCutOption ('1':_) = FirstUipCut -readCutOption ('d':_) = DecisionLitCut -readCutOption _ = error "error parsing cut option" + , optVersion = False } -- | Show default value of option at the end of the given string. withDefault :: (Show v) => (Options -> v) -> String -> String @@ -120,14 +103,11 @@ main :: IO () main = do (opts, files) <- getArgs >>= validateArgv +#ifdef TESTING when (optVerify opts) $ do Properties.main exitWith ExitSuccess - - when (optProfile opts) $ do - putStrLn "Solving ..." - Properties.profile - exitWith ExitSuccess +#endif when (optVersion opts) $ do putStr "funsat " @@ -135,11 +115,8 @@ exitWith ExitSuccess putStr "Feature config: " - putStr . concat $ intersperse ", " - [ if (optUseVsids opts) then "vsids" else "no vsids" - , if (optUseRestarts opts) then "restarts" else "no restarts" - , "unsat checking" - ] + putStr $ if (optUseVsids opts) then "vsids" else "no vsids" + putStr $ if (optUseRestarts opts) then ", restarts" else ", no restarts" putStr "\n" when (optPrintFeatures opts) $ exitWith ExitSuccess @@ -158,7 +135,9 @@ parseEnd <- getCurrentTime startingTime <- getCurrentTime - let cfg = optFunsatConfig opts + let cfg = defaultConfig + { configUseVSIDS = optUseVsids opts + , configUseRestarts = optUseRestarts opts } (solution, stats, rt) = solve cfg cnf endingTime <- solution `seq` getCurrentTime print solution diff --git a/funsat.cabal b/funsat.cabal --- a/funsat.cabal +++ b/funsat.cabal @@ -1,5 +1,5 @@ Name: funsat -Version: 0.6.1 +Version: 0.6.2 Cabal-Version: >= 1.2 Description: @@ -13,7 +13,7 @@ Currently along this theme we provide unsatisfiable core generation (see "Funsat.Resolution") and a logical circuit interface (see "Funsat.Circuit"). - New in 0.6: circuits and BSD3 license. + New in 0.6.2: works with ghc-6.12 and fixed some space leaks. =/ Synopsis: A modern DPLL-style SAT solver Homepage: http://github.com/dbueno/funsat @@ -30,20 +30,10 @@ Executable funsat Main-is: Main.hs Ghc-options: -funbox-strict-fields - -Wall - -fwarn-tabs + -Wall -fwarn-tabs -fno-warn-name-shadowing -fno-warn-orphans - Extensions: CPP, - BangPatterns, - ScopedTypeVariables, - TypeSynonymInstances, - MultiParamTypeClasses, - FunctionalDependencies, - FlexibleInstances, - FlexibleContexts - - + Extensions: CPP, ScopedTypeVariables CPP-options: -DTESTING Hs-source-dirs: . src tests Other-modules: @@ -55,32 +45,23 @@ Funsat.Types Funsat.Types.Internal Funsat.Utils - Funsat.Utils.Internal Text.Tabular Properties - Build-Depends: base >= 3 && < 5, - random < 2, - containers >= 0.2 && < 0.3, - pretty < 2, - mtl >= 1 && < 2, - array >= 0.2 && < 0.3, - QuickCheck < 2, + Build-Depends: base < 4, + random, + containers, + pretty, + mtl, + array, + QuickCheck >= 2 && < 3, parse-dimacs >= 1.2 && < 2, - bitset < 1, + bitset >= 1 && < 2, bimap >= 0.2 && < 0.3, - fgl >= 5 && <= 5.4.2.2, - time < 1.2 + fgl, + time Library - Extensions: CPP, - BangPatterns, - ScopedTypeVariables, - TypeSynonymInstances, - MultiParamTypeClasses, - FunctionalDependencies, - FlexibleInstances, - FlexibleContexts Exposed-modules: Control.Monad.MonadST Funsat.Circuit Funsat.Monad @@ -89,22 +70,19 @@ Funsat.Types Funsat.Types.Internal Text.Tabular - Funsat.Utils - Funsat.Utils.Internal - Other-modules: Funsat.FastDom + Other-modules: Funsat.FastDom Funsat.Utils Ghc-options: -funbox-strict-fields -Wall -fwarn-tabs -fno-warn-name-shadowing -fno-warn-orphans Extensions: CPP, ScopedTypeVariables Hs-source-dirs: src - Build-Depends: base >= 3 && < 5, - containers >= 0.2 && < 0.3, - pretty < 2, - mtl >= 1 && < 2, - array >= 0.2 && < 0.3, - QuickCheck < 2, + Build-Depends: base, + containers, + pretty, + mtl, + array, parse-dimacs >= 1.2 && < 2, - bitset < 1, + bitset >= 1 && < 2, bimap >= 0.2 && < 0.3, - fgl >= 5 && <= 5.4.2.2 + fgl diff --git a/src/Funsat/Circuit.hs b/src/Funsat/Circuit.hs --- a/src/Funsat/Circuit.hs +++ b/src/Funsat/Circuit.hs @@ -5,11 +5,6 @@ -- class and various representations that admit efficient conversion to funsat -- CNF. -- --- The types in this class are more capable than simply being able to go from --- (for example) an equality constraint to the CNF representation. In --- particular, the `Shared' circuit type efficiently shares subterms, --- potentially drastically reducing the memory require for the circuit. --- -- The implementation for this module was adapted from -- . module Funsat.Circuit @@ -83,8 +78,7 @@ import Data.Maybe() import Data.Ord() import Data.Set( Set ) -import Funsat.Types( CNF(..), Lit(..), Var(..), var, lit, Solution(..), litSign ) -import Funsat.Utils( litAssignment ) +import Funsat.Types( CNF(..), Lit(..), Var(..), var, lit, Solution(..), litSign, litAssignment ) import Prelude hiding( not, and, or ) import qualified Data.Bimap as Bimap diff --git a/src/Funsat/Resolution.hs b/src/Funsat/Resolution.hs --- a/src/Funsat/Resolution.hs +++ b/src/Funsat/Resolution.hs @@ -43,7 +43,7 @@ import qualified Data.IntSet as IntSet import qualified Data.Map as Map import Funsat.Types -import Funsat.Utils.Internal( isSingle, getUnit, isFalseUnder ) +import Funsat.Utils( isSingle, getUnit, isFalseUnder ) -- IDs = Ints diff --git a/src/Funsat/Solver.hs b/src/Funsat/Solver.hs --- a/src/Funsat/Solver.hs +++ b/src/Funsat/Solver.hs @@ -1,5 +1,20 @@ +{-# LANGUAGE MultiParamTypeClasses + ,FunctionalDependencies + ,FlexibleInstances + ,FlexibleContexts + ,GeneralizedNewtypeDeriving + ,TypeSynonymInstances + ,TypeOperators + ,ParallelListComp + ,BangPatterns + #-} +{-# OPTIONS -cpp #-} + + + + {-| Funsat aims to be a reasonably efficient modern SAT solver that is easy to @@ -78,7 +93,6 @@ import Data.Array.ST import Data.Array.Unboxed import Data.Foldable hiding ( sequence_ ) -import Data.Graph.Inductive.Tree import Data.Int( Int64 ) import Data.List( nub, tails, sortBy, sort ) import Data.Maybe @@ -88,7 +102,6 @@ -- import Debug.Trace (trace) import Funsat.Monad import Funsat.Utils -import Funsat.Utils.Internal import Funsat.Resolution( ResolutionTrace(..), initResolutionTrace ) import Funsat.Types import Funsat.Types.Internal @@ -144,14 +157,14 @@ -- Watch each clause, making sure to bork if we find a contradiction. (`catchError` - (const $ funFreeze m >>= \a -> return (a,True))) $ do + (const $ liftST (unsafeFreezeAss m) >>= \a -> return (a,True))) $ do forM_ (clauses f) (\c -> do cid <- nextTraceId isConsistent <- watchClause m (c, cid) False when (not isConsistent) -- conflict data is ignored here, so safe to fake (do traceClauseId cid ; throwError (L 0, [], 0))) - a <- funFreeze m + a <- liftST (unsafeFreezeAss m) return (a, False) @@ -184,12 +197,12 @@ s{ dpllConfig = c{ configRestart = ceiling (configRestartBump c * fromIntegral (configRestart c)) } } - lvl <- gets level >>= funFreeze + lvl :: FrozenLevelArray <- gets level >>= liftST . unsafeFreeze undoneLits <- takeWhile (\l -> lvl ! (var l) > 0) `liftM` gets trail forM_ undoneLits $ const (undoOne m) modify $ \s -> s{ dl = [], propQ = Seq.empty } compactDB - funFreeze m >>= simplifyDB + unsafeFreezeAss m >>= simplifyDB reportSolution :: Solution -> FunMonad s (Solution, Stats, Maybe ResolutionTrace) reportSolution s = do @@ -212,10 +225,9 @@ -- * restarts to be enabled defaultConfig :: FunsatConfig defaultConfig = Cfg { configRestart = 100 -- fromIntegral $ max (numVars f `div` 10) 100 - , configRestartBump = 1.5 - , configUseVSIDS = True - , configUseRestarts = True - , configCut = FirstUipCut } + , configRestartBump = 1.5 + , configUseVSIDS = True + , configUseRestarts = True } -- * Preprocessing @@ -254,13 +266,13 @@ -- new state. solveStep :: MAssignment s -> FunMonad s (Either (MAssignment s) Solution) solveStep m = do - funFreeze m >>= solveStepInvariants + unsafeFreezeAss m >>= solveStepInvariants conf <- gets dpllConfig let selector = if configUseVSIDS conf then select else selectStatic maybeConfl <- bcp m - mFr <- funFreeze m + mFr <- unsafeFreezeAss m voArr <- gets (varOrderArr . varOrder) - voFr <- FrozenVarOrder `liftM` funFreeze voArr + voFr <- FrozenVarOrder `liftM` liftST (unsafeFreeze voArr) s <- get stepForward $ -- Check if unsat. @@ -271,11 +283,11 @@ >< selector mFr voFr >=> decide m where -- Take the step chosen by the transition guards above. - stepForward Nothing = (Right . Sat) `liftM` funFreeze m + stepForward Nothing = (Right . Sat) `liftM` unsafeFreezeAss m stepForward (Just step) = do r <- step case r of - Nothing -> (Right . Unsat) `liftM` funFreeze m + Nothing -> (Right . Unsat) `liftM` liftST (unsafeFreezeAss m) Just m -> return . Left $ m -- | /Precondition:/ problem determined to be unsat. @@ -344,7 +356,7 @@ {-# INLINE updateWatches #-} updateWatches _ [] = return () updateWatches alter (annCl@(watchRef, c, cid) : restClauses) = do - mFr :: IAssignment <- funFreeze m + mFr <- unsafeFreezeAss m q <- liftST $ do (x, y) <- readSTRef watchRef return $ if x == l then y else x -- l,q are the (negated) literals being watched for clause c. @@ -410,8 +422,8 @@ -- *** Backtracking --- | The current returns the learned clause implied by the first unique --- implication point cut of the conflict graph. +-- | Non-chronological backtracking. The current returns the learned clause +-- implied by the first unique implication point cut of the conflict graph. backJump :: MAssignment s -> (Lit, Clause, ClauseId) -- ^ @(l, c)@, where attempting to assign @l@ conflicted with @@ -425,42 +437,55 @@ -- ++ "reason: " ++ Map.showTree _reason -- ) ( incNumConfl ; incNumConflTotal - levelArr <- do s <- get - funFreeze (level s) - (learntCl, learntClId, newLevel) <- analyse m levelArr dl c + levelArr :: FrozenLevelArray <- do s <- get + liftST $ unsafeFreeze (level s) + (learntCl, learntClId, newLevel) <- + do mFr <- unsafeFreezeAss m + analyse mFr levelArr dl c s <- get let numDecisionsToUndo = length dl - newLevel dl' = drop numDecisionsToUndo dl undoneLits = takeWhile (\lit -> levelArr ! (var lit) > newLevel) (trail s) forM_ undoneLits $ const (undoOne m) -- backtrack - mFr <- funFreeze m + mFr <- unsafeFreezeAss m assert (numDecisionsToUndo > 0) $ assert (not (null learntCl)) $ assert (learntCl `isUnitUnder` mFr) $ modify $ \s -> s{ dl = dl' } -- undo decisions + mFr <- unsafeFreezeAss m -- trace ("new mFr: " ++ showAssignment mFr) $ return () -- TODO once I'm sure this works I don't need getUnit, I can just use the -- uip of the cut. watchClause m (learntCl, learntClId) True - mFr <- funFreeze m enqueue m (getUnit learntCl mFr) (Just (learntCl, learntClId)) -- learntCl is asserting return $ Just m + +-- | @doWhile cmd test@ first runs @cmd@, then loops testing @test@ and +-- executing @cmd@. The traditional @do-while@ semantics, in other words. +doWhile :: (Monad m) => m () -> m Bool -> m () +doWhile body test = do + body + shouldContinue <- test + when shouldContinue $ doWhile body test + -- | Analyse a the conflict graph and produce a learned clause. We use the -- First UIP cut of the conflict graph. -- -- May undo part of the trail, but not past the current decision level. -analyse :: MAssignment s -> FrozenLevelArray -> [Lit] -> (Lit, Clause, ClauseId) +analyse :: IAssignment -> FrozenLevelArray -> [Lit] -> (Lit, Clause, ClauseId) -> FunMonad s (Clause, ClauseId, Int) -- ^ learned clause and new decision level -analyse m levelArr dlits (cLit, cClause, cCid) = do - conf <- gets dpllConfig - mFr <- funFreeze m - st <- get - -- let conflGraph = mkConflGraph mFr levelArr (reason st) dlits (cLit, cClause) - -- :: ConflictGraph Gr +analyse mFr levelArr dlits (cLit, cClause, cCid) = do + st <- get +-- trace ("mFr: " ++ showAssignment mFr) $ assert True (return ()) +-- let (learntCl, newLevel) = cutLearn mFr levelArr firstUIPCut +-- firstUIPCut = uipCut dlits levelArr conflGraph (unLit cLit) +-- (firstUIP conflGraph) +-- conflGraph = mkConflGraph mFr levelArr (reason st) dlits c +-- :: Gr CGNodeAnnot () -- trace ("graphviz graph:\n" ++ graphviz' conflGraph) $ return () -- trace ("cut: " ++ show firstUIPCut) $ return () -- trace ("topSort: " ++ show topSortNodes) $ return () @@ -468,11 +493,9 @@ -- trace ("learnt: " ++ show (map (\l -> (l, levelArr!(var l))) learntCl, newLevel)) $ return () -- outputConflict "conflict.dot" (graphviz' conflGraph) $ return () -- return $ (learntCl, newLevel) - a <- case configCut conf of - FirstUipCut -> firstUIPBFS m (numVars . cnf $ st) (reason st) - DecisionLitCut -> error "decisionlitcut unimplemented" - -- let lastDecision = fromMaybe $ find (\ --- trace ("learned: " ++ show a) $ return () + m <- liftST $ unsafeThawAss mFr + a <- firstUIPBFS m (numVars . cnf $ st) (reason st) +-- trace ("firstUIPBFS learned: " ++ show a) $ return () return a where -- BFS by undoing the trail backward. From Minisat paper. Returns @@ -670,7 +693,7 @@ {-# INLINE enqueue #-} -- enqueue _m l _r | trace ("enqueue " ++ show l) $ False = undefined enqueue m l r = do - mFr <- funFreeze m + mFr <- unsafeFreezeAss m case l `statusUnder` mFr of Right b -> return b -- conflict/already assigned Left () -> do @@ -882,7 +905,7 @@ extractStats :: FunMonad s Stats extractStats = do s <- gets stats - learntArr <- get >>= funFreeze . learnt + learntArr <- get >>= liftST . unsafeFreezeWatchArray . learnt let learnts = (nub . Fl.concat) [ map (sort . (\(_,c,_) -> c)) (learntArr!i) | i <- (range . bounds) learntArr ] :: [Clause] @@ -896,6 +919,9 @@ , statsNumDecisions = numDecisions s , statsNumImpl = numImpl s } return stats + +unsafeFreezeWatchArray :: WatchArray s -> ST s (Array Lit [WatchedPair s]) +unsafeFreezeWatchArray = freeze constructResTrace :: Solution -> FunMonad s ResolutionTrace diff --git a/src/Funsat/Types.hs b/src/Funsat/Types.hs --- a/src/Funsat/Types.hs +++ b/src/Funsat/Types.hs @@ -25,15 +25,17 @@ module Funsat.Types where +import Control.Monad.MonadST( MonadST(..) ) +import Control.Monad.ST.Strict import Data.Array.ST import Data.Array.Unboxed import Data.BitSet ( BitSet ) import Data.Foldable hiding ( sequence_ ) -import Data.Int( Int64 ) import Data.List( intercalate ) import Data.Map ( Map ) import Data.Set ( Set ) import Data.STRef +import Funsat.Monad import Prelude hiding ( sum, concatMap, elem, foldr, foldl, any, maximum ) import qualified Data.BitSet as BitSet import qualified Data.Foldable as Fl @@ -154,20 +156,11 @@ without m (k,_) = Map.delete k m contains = error "no contains for Setlike (Map k a) (k, a)" -instance (Ord a, BitSet.Hash a) => Setlike (BitSet a) a where +instance (Ord a, Enum a) => Setlike (BitSet a) a where with = flip BitSet.insert without = flip BitSet.delete contains = flip BitSet.member - -instance (BitSet.Hash Lit) where - hash l = if li > 0 then 2 * vi else (2 * vi) + 1 - where li = unLit l - vi = abs li - -instance (BitSet.Hash Var) where - hash = unVar - -- * Assignments @@ -191,6 +184,37 @@ -- | Mutable array corresponding to the `IAssignment' representation. type MAssignment s = STUArray s Var Int +-- | Same as @freeze@, but at the right type so GHC doesn't yell at me. +freezeAss :: MAssignment s -> ST s IAssignment +{-# INLINE freezeAss #-} +freezeAss = freeze +-- | See `freezeAss'. +unsafeFreezeAss :: (MonadST s m) => MAssignment s -> m IAssignment +{-# INLINE unsafeFreezeAss #-} +unsafeFreezeAss = liftST . unsafeFreeze + +thawAss :: IAssignment -> ST s (MAssignment s) +{-# INLINE thawAss #-} +thawAss = thaw +unsafeThawAss :: IAssignment -> ST s (MAssignment s) +{-# INLINE unsafeThawAss #-} +unsafeThawAss = unsafeThaw + +-- | Destructively update the assignment with the given literal. +assign :: MAssignment s -> Lit -> ST s (MAssignment s) +assign a l = writeArray a (var l) (unLit l) >> return a + +-- | Destructively undo the assignment to the given literal. +unassign :: MAssignment s -> Lit -> ST s (MAssignment s) +unassign a l = writeArray a (var l) 0 >> return a + +-- | The assignment as a list of signed literals. +litAssignment :: IAssignment -> [Lit] +litAssignment mFr = foldr (\i ass -> if mFr!i == 0 then ass + else (L . (mFr!) $ i) : ass) + [] + (range . bounds $ mFr) + -- | The union of the reason side and the conflict side are all the nodes in -- the `cutGraph' (excepting, perhaps, the nodes on the reason side at -- decision level 0, which should never be present in a learned clause). @@ -209,14 +233,6 @@ -- assignment) and decision level. The only reason we make a new datatype for -- this is for its `Show' instance. data CGNodeAnnot = CGNA Lit Int - --- | Just a graph with special node annotations. -type ConflictGraph g = g CGNodeAnnot () - --- | The lambda node is connected exactly to the two nodes causing the conflict. -cgLambda :: CGNodeAnnot -cgLambda = CGNA (L 0) (-1) - instance Show CGNodeAnnot where show (CGNA (L 0) _) = "lambda" show (CGNA l lev) = show l ++ " (" ++ show lev ++ ")" @@ -306,23 +322,3 @@ instance Show (STUArray s Var Int) where show = const "" instance Show (STUArray s Var Double) where show = const "" instance Show (STArray s a b) where show = const "" - - --- * Configuration - --- | A choice of conflict graph cut for learning clauses. -data ConflictCut = FirstUipCut - | DecisionLitCut - deriving (Show) - --- | Configuration parameters for the solver. -data FunsatConfig = Cfg - { configRestart :: !Int64 -- ^ Number of conflicts before a restart. - , configRestartBump :: !Double -- ^ `configRestart' is altered after each - -- restart by multiplying it by this value. - , configUseVSIDS :: !Bool -- ^ If true, use dynamic variable ordering. - , configUseRestarts :: !Bool - , configCut :: !ConflictCut - } - deriving (Show) - diff --git a/src/Funsat/Types/Internal.hs b/src/Funsat/Types/Internal.hs --- a/src/Funsat/Types/Internal.hs +++ b/src/Funsat/Types/Internal.hs @@ -93,3 +93,12 @@ -- `FunsatState' and is not mutable. type FunMonad s = SSTErrMonad (Lit, Clause, ClauseId) (FunsatState s) s +-- | Configuration parameters for the solver. +data FunsatConfig = Cfg + { configRestart :: !Int64 -- ^ Number of conflicts before a restart. + , configRestartBump :: !Double -- ^ `configRestart' is altered after each + -- restart by multiplying it by this value. + , configUseVSIDS :: !Bool -- ^ If true, use dynamic variable ordering. + , configUseRestarts :: !Bool } + deriving Show + diff --git a/src/Funsat/Utils.hs b/src/Funsat/Utils.hs --- a/src/Funsat/Utils.hs +++ b/src/Funsat/Utils.hs @@ -16,7 +16,7 @@ {-| -Utilities. +Generic utilities that happen to be used in the SAT solver. -} module Funsat.Utils where @@ -28,7 +28,8 @@ import Data.Foldable hiding ( sequence_ ) import Data.Graph.Inductive.Graph( DynGraph, Graph ) import Data.List( foldl1' ) -import Data.Set( Set ) +import Data.Map (Map) +import Data.Set (Set) import Debug.Trace( trace ) import Funsat.Types import Prelude hiding ( sum, concatMap, elem, foldr, foldl, any, maximum ) @@ -43,9 +44,229 @@ --- | The assignment as a list of signed literals. -litAssignment :: IAssignment -> [Lit] -litAssignment mFr = foldr (\i ass -> if mFr!i == 0 then ass - else (L . (mFr!) $ i) : ass) - [] - (range . bounds $ mFr) +-- | `True' if and only if the object is undefined in the model. +isUndefUnder :: Model a m => a -> m -> Bool +isUndefUnder x m = isUndef $ x `statusUnder` m + where isUndef (Left ()) = True + isUndef _ = False + +-- | `True' if and only if the object is true in the model. +isTrueUnder :: Model a m => a -> m -> Bool +isTrueUnder x m = isTrue $ x `statusUnder` m + where isTrue (Right True) = True + isTrue _ = False + +-- | `True' if and only if the object is false in the model. +isFalseUnder :: Model a m => a -> m -> Bool +isFalseUnder x m = isFalse $ x `statusUnder` m + where isFalse (Right False) = True + isFalse _ = False + +-- * Helpers + + +-- isUnitUnder c m | trace ("isUnitUnder " ++ show c ++ " " ++ showAssignment m) $ False = undefined + +-- | Whether all the elements of the model in the list are false but one, and +-- none is true, under the model. +isUnitUnder :: (Model a m) => [a] -> m -> Bool +{-# SPECIALISE INLINE isUnitUnder :: Clause -> IAssignment -> Bool #-} +isUnitUnder c m = isSingle (filter (not . (`isFalseUnder` m)) c) + && not (Fl.any (`isTrueUnder` m) c) + +-- Precondition: clause is unit. +-- getUnit :: (Model a m, Show a, Show m) => [a] -> m -> a +-- getUnit c m | trace ("getUnit " ++ show c ++ " " ++ showAssignment m) $ False = undefined + +-- | Get the element of the list which is not false under the model. If no +-- such element, throws an error. +getUnit :: (Model a m, Show a) => [a] -> m -> a +{-# SPECIALISE INLINE getUnit :: Clause -> IAssignment -> Lit #-} +getUnit c m = case filter (not . (`isFalseUnder` m)) c of + [u] -> u + xs -> error $ "getUnit: not unit: " ++ show xs + + +{-# INLINE mytrace #-} +mytrace :: String -> a -> a +mytrace msg expr = unsafePerformIO $ do + hPutStr stderr msg + return expr + +outputConflict :: FilePath -> String -> a -> a +outputConflict fn g x = unsafePerformIO $ do writeFile fn g + return x + + +-- | /O(1)/ Whether a list contains a single element. +isSingle :: [a] -> Bool +{-# INLINE isSingle #-} +isSingle [_] = True +isSingle _ = False + +-- | Modify a value inside the state. +modifySlot :: (MonadState s m) => (s -> a) -> (s -> a -> s) -> m () +{-# INLINE modifySlot #-} +modifySlot slot f = modify $ \s -> f s (slot s) + +-- | @modifyArray arr i f@ applies the function @f@ to the index @i@ and the +-- current value of the array at index @i@, then writes the result into @i@ in +-- the array. +modifyArray :: (Monad m, MArray a e m, Ix i) => a i e -> i -> (i -> e -> e) -> m () +{-# INLINE modifyArray #-} +modifyArray arr i f = readArray arr i >>= writeArray arr i . (f i) + +-- | Same as @newArray@, but helping along the type checker. +newSTUArray :: (MArray (STUArray s) e (ST s), Ix i) + => (i, i) -> e -> ST s (STUArray s i e) +newSTUArray = newArray + +newSTArray :: (MArray (STArray s) e (ST s), Ix i) + => (i, i) -> e -> ST s (STArray s i e) +newSTArray = newArray + + +-- | Count the number of elements in the list that satisfy the predicate. +count :: (a -> Bool) -> [a] -> Int +count p = foldl' f 0 + where f x y | p y = x + 1 + | otherwise = x + +-- | /O(1)/ @argmin f x y@ is the argument whose image is least under @f@; if +-- the images are equal, returns the first. +argmin :: Ord b => (a -> b) -> a -> a -> a +argmin f x y = if f x <= f y then x else y + +-- | /O(length xs)/ @argminimum f xs@ returns the value in @xs@ whose image +-- is least under @f@; if @xs@ is empty, throws an error. +argminimum :: Ord b => (a -> b) -> [a] -> a +argminimum f = foldl1' (argmin f) + + +-- | Show the value with trace, then return it. Useful because you can wrap +-- it around any subexpression to print it when it is forced. +tracing :: (Show a) => a -> a +tracing x = trace (show x) x + +-- | Returns a predicate which holds exactly when both of the given predicates +-- hold. +(.&&.) :: (a -> Bool) -> (a -> Bool) -> (a -> Bool) +p .&&. q = \x -> p x && q x + + +-- | Generate a cut using the given UIP node. The cut generated contains +-- exactly the (transitively) implied nodes starting with (but not including) +-- the UIP on the conflict side, with the rest of the nodes on the reason +-- side. +uipCut :: (Graph gr) => + [Lit] -- ^ decision literals + -> FrozenLevelArray + -> gr a b -- ^ conflict graph + -> Graph.Node -- ^ unassigned, implied conflicting node + -> Graph.Node -- ^ a UIP in the conflict graph + -> Cut Set gr a b +uipCut dlits levelArr conflGraph conflNode uip = + Cut { reasonSide = Set.filter (\i -> levelArr!(V $ abs i) > 0) $ + allNodes Set.\\ impliedByUIP + , conflictSide = impliedByUIP + , cutUIP = uip + , cutGraph = conflGraph } + where + -- Transitively implied, and not including the UIP. + impliedByUIP = Set.insert extraNode $ + Set.fromList $ tail $ DFS.reachable uip conflGraph + -- The UIP may not imply the assigned conflict variable which needs to + -- be on the conflict side, unless it's a decision variable or the UIP + -- itself. + extraNode = if L (negate conflNode) `elem` dlits || negate conflNode == uip + then conflNode -- idempotent addition + else negate conflNode + allNodes = Set.fromList $ Graph.nodes conflGraph + + +-- | Generate a learned clause from a cut of the graph. Returns a pair of the +-- learned clause and the decision level to which to backtrack. +cutLearn :: (Graph gr, Foldable f) => IAssignment -> FrozenLevelArray + -> Cut f gr a b -> (Clause, Int) +cutLearn a levelArr cut = + ( clause + -- The new decision level is the max level of all variables in the + -- clause, excluding the uip (which is always at the current decision + -- level). + , maximum0 (map (levelArr!) . (`without` V (abs $ cutUIP cut)) . map var $ clause) ) + where + -- The clause is composed of the variables on the reason side which have + -- at least one successor on the conflict side. The value of the variable + -- is the negation of its value under the current assignment. + clause = + foldl' (\ls i -> + if any (`elem` conflictSide cut) (Graph.suc (cutGraph cut) i) + then L (negate $ a!(V $ abs i)):ls + else ls) + [] (reasonSide cut) + maximum0 [] = 0 -- maximum0 has 0 as its max for the empty list + maximum0 xs = maximum xs + + +-- | Creates the conflict graph, where each node is labeled by its literal and +-- level. +-- +-- Useful for getting pretty graphviz output of a conflict. +mkConflGraph :: DynGraph gr => + IAssignment + -> FrozenLevelArray + -> Map Var Clause + -> [Lit] -- ^ decision lits, in rev. chron. order + -> (Lit, Clause) -- ^ conflict info + -> gr CGNodeAnnot () +mkConflGraph mFr lev reasonMap _dlits (cLit, confl) = + Graph.mkGraph nodes' edges' + where + -- we pick out all the variables from the conflict graph, specially adding + -- both literals of the conflict variable, so that that variable has two + -- nodes in the graph. + nodes' = + ((0, CGNA (L 0) (-1)) :) $ -- lambda node + ((unLit cLit, CGNA cLit (-1)) :) $ + ((negate (unLit cLit), CGNA (negate cLit) (lev!(var cLit))) :) $ + -- annotate each node with its literal and level + map (\v -> (unVar v, CGNA (varToLit v) (lev!v))) $ + filter (\v -> v /= var cLit) $ + toList nodeSet' + + -- node set includes all variables reachable from conflict. This node set + -- construction needs a `seen' set because it might infinite loop + -- otherwise. + (nodeSet', edges') = + mkGr Set.empty (Set.empty, [ (unLit cLit, 0, ()) + , ((negate . unLit) cLit, 0, ()) ]) + [negate cLit, cLit] + varToLit v = (if v `isTrueUnder` mFr then id else negate) $ L (unVar v) + + -- seed with both conflicting literals + mkGr _ ne [] = ne + mkGr (seen :: Set Graph.Node) ne@(nodes, edges) (lit:lits) = + if haveSeen + then mkGr seen ne lits + else newNodes `seq` newEdges `seq` + mkGr seen' (newNodes, newEdges) (lits ++ pred) + where + haveSeen = seen `contains` litNode lit + newNodes = var lit `Set.insert` nodes + newEdges = [ ( litNode (negate x) -- unimplied lits from reasons are + -- complemented + , litNode lit, () ) + | x <- pred ] ++ edges + pred = filterReason $ + if lit == cLit then confl else + Map.findWithDefault [] (var lit) reasonMap `without` lit + filterReason = filter ( ((var lit /=) . var) .&&. + ((<= litLevel lit) . litLevel) ) + seen' = seen `with` litNode lit + litLevel l = if l == cLit then length _dlits else lev!(var l) + litNode l = -- lit to node + if var l == var cLit -- preserve sign of conflicting lit + then unLit l + else (abs . unLit) l + + diff --git a/src/Funsat/Utils/Internal.hs b/src/Funsat/Utils/Internal.hs deleted file mode 100644 --- a/src/Funsat/Utils/Internal.hs +++ /dev/null @@ -1,332 +0,0 @@ -{-# LANGUAGE MultiParamTypeClasses #-} - -{- - This file is part of funsat. - - funsat is free software: it is released under the BSD3 open source license. - You can find details of this license in the file LICENSE at the root of the - source tree. - - Copyright 2008 Denis Bueno --} - - -{-| - -Generic utilities that happen to be used in the SAT solver. - --} -module Funsat.Utils.Internal where - -import Control.Monad.MonadST( MonadST, liftST ) -import Control.Monad.ST.Strict -import Control.Monad.State.Lazy hiding ( (>=>), forM_ ) -import Data.Array.ST -import Data.Array.Unboxed -import Data.Foldable hiding ( sequence_ ) -import Data.Graph.Inductive.Graph( DynGraph, Graph ) -import Data.List( foldl1' ) -import Data.Set( Set ) -import Debug.Trace( trace ) -import Funsat.Types -import Funsat.Types.Internal( FunMonad ) -import Prelude hiding ( sum, concatMap, elem, foldr, foldl, any, maximum ) -import System.IO.Unsafe( unsafePerformIO ) -import System.IO( hPutStr, stderr ) -import qualified Data.Foldable as Fl -import qualified Data.Graph.Inductive.Graph as Graph -import qualified Data.Graph.Inductive.Query.DFS as DFS -import qualified Data.List as List -import qualified Data.Map as Map -import qualified Data.Set as Set - - -class FunFreeze t e f | t -> f where - funFreeze :: (MArray t e (ST s), Ix i, IArray f e) => - t i e -> FunMonad s (f i e) - funThaw :: (MArray t e (ST s), Ix i, IArray f e) => - f i e -> FunMonad s (t i e) -instance FunFreeze (STUArray s) Int UArray where - {-# INLINE funFreeze #-} - funFreeze = liftST . unsafeFreeze - {-# INLINE funThaw #-} - funThaw = liftST . unsafeThaw - -instance FunFreeze (STUArray s) Double UArray where - {-# INLINE funFreeze #-} - funFreeze = liftST . unsafeFreeze - {-# INLINE funThaw #-} - funThaw = liftST . unsafeThaw - -instance FunFreeze (STArray s) [WatchedPair s] Array where - {-# INLINE funFreeze #-} - funFreeze = liftST . freeze - {-# INLINE funThaw #-} - funThaw = liftST . thaw - -{- --- | Same as @freeze@, but at the right type so GHC doesn't yell at me. -freezeAss :: MAssignment s -> ST s IAssignment -{-# INLINE freezeAss #-} -freezeAss = freeze --- | See `freezeAss'. -unsafeFreezeAss :: (MonadST s m) => MAssignment s -> m IAssignment -{-# INLINE unsafeFreezeAss #-} -unsafeFreezeAss = liftST . unsafeFreeze - -thawAss :: IAssignment -> ST s (MAssignment s) -{-# INLINE thawAss #-} -thawAss = thaw -unsafeThawAss :: IAssignment -> ST s (MAssignment s) -{-# INLINE unsafeThawAss #-} -unsafeThawAss = unsafeThaw --} - --- | Destructively update the assignment with the given literal. -assign :: MAssignment s -> Lit -> ST s (MAssignment s) -assign a l = writeArray a (var l) (unLit l) >> return a - --- | Destructively undo the assignment to the given literal. -unassign :: MAssignment s -> Lit -> ST s (MAssignment s) -unassign a l = writeArray a (var l) 0 >> return a - - --- | `True' if and only if the object is undefined in the model. -isUndefUnder :: Model a m => a -> m -> Bool -isUndefUnder x m = isUndef $ x `statusUnder` m - where isUndef (Left ()) = True - isUndef _ = False - --- | `True' if and only if the object is true in the model. -isTrueUnder :: Model a m => a -> m -> Bool -isTrueUnder x m = isTrue $ x `statusUnder` m - where isTrue (Right True) = True - isTrue _ = False - --- | `True' if and only if the object is false in the model. -isFalseUnder :: Model a m => a -> m -> Bool -isFalseUnder x m = isFalse $ x `statusUnder` m - where isFalse (Right False) = True - isFalse _ = False - --- * Helpers - - --- isUnitUnder c m | trace ("isUnitUnder " ++ show c ++ " " ++ showAssignment m) $ False = undefined - --- | Whether all the elements of the model in the list are false but one, and --- none is true, under the model. -isUnitUnder :: (Model a m) => [a] -> m -> Bool -{-# SPECIALISE INLINE isUnitUnder :: Clause -> IAssignment -> Bool #-} -isUnitUnder c m = isSingle (filter (not . (`isFalseUnder` m)) c) - && not (Fl.any (`isTrueUnder` m) c) - --- Precondition: clause is unit. --- getUnit :: (Model a m, Show a, Show m) => [a] -> m -> a --- getUnit c m | trace ("getUnit " ++ show c ++ " " ++ showAssignment m) $ False = undefined - --- | Get the element of the list which is not false under the model. If no --- such element, throws an error. -getUnit :: (Model a m, Show a) => [a] -> m -> a -{-# SPECIALISE INLINE getUnit :: Clause -> IAssignment -> Lit #-} -getUnit c m = case filter (not . (`isFalseUnder` m)) c of - [u] -> u - xs -> error $ "getUnit: not unit: " ++ show xs - - -{-# INLINE mytrace #-} -mytrace :: String -> a -> a -mytrace msg expr = unsafePerformIO $ do - hPutStr stderr msg - return expr - -outputConflict :: FilePath -> String -> a -> a -outputConflict fn g x = unsafePerformIO $ do writeFile fn g - return x - - --- | /O(1)/ Whether a list contains a single element. -isSingle :: [a] -> Bool -{-# INLINE isSingle #-} -isSingle [_] = True -isSingle _ = False - --- | Modify a value inside the state. -modifySlot :: (MonadState s m) => (s -> a) -> (s -> a -> s) -> m () -{-# INLINE modifySlot #-} -modifySlot slot f = modify $ \s -> f s (slot s) - --- | @modifyArray arr i f@ applies the function @f@ to the index @i@ and the --- current value of the array at index @i@, then writes the result into @i@ in --- the array. -modifyArray :: (Monad m, MArray a e m, Ix i) => a i e -> i -> (i -> e -> e) -> m () -{-# INLINE modifyArray #-} -modifyArray arr i f = readArray arr i >>= writeArray arr i . (f i) - --- | Same as @newArray@, but helping along the type checker. -newSTUArray :: (MArray (STUArray s) e (ST s), Ix i) - => (i, i) -> e -> ST s (STUArray s i e) -newSTUArray = newArray - -newSTArray :: (MArray (STArray s) e (ST s), Ix i) - => (i, i) -> e -> ST s (STArray s i e) -newSTArray = newArray - - --- | Count the number of elements in the list that satisfy the predicate. -count :: (a -> Bool) -> [a] -> Int -count p = foldl' f 0 - where f x y | p y = x + 1 - | otherwise = x - --- | /O(1)/ @argmin f x y@ is the argument whose image is least under @f@; if --- the images are equal, returns the first. -argmin :: Ord b => (a -> b) -> a -> a -> a -argmin f x y = if f x <= f y then x else y - --- | /O(length xs)/ @argminimum f xs@ returns the value in @xs@ whose image --- is least under @f@; if @xs@ is empty, throws an error. -argminimum :: Ord b => (a -> b) -> [a] -> a -argminimum f = foldl1' (argmin f) - - --- | Show the value with trace, then return it. Useful because you can wrap --- it around any subexpression to print it when it is forced. -tracing :: (Show a) => a -> a -tracing x = trace (show x) x - --- | Returns a predicate which holds exactly when both of the given predicates --- hold. -(.&&.) :: (a -> Bool) -> (a -> Bool) -> (a -> Bool) -p .&&. q = \x -> p x && q x - - --- | Generate a cut using the given UIP node. The cut generated contains --- exactly the (transitively) implied nodes starting with (but not including) --- the UIP on the conflict side, with the rest of the nodes on the reason --- side. -uipCut :: (Graph gr) => - [Lit] -- ^ decision literals - -> FrozenLevelArray - -> gr a b -- ^ conflict graph - -> Graph.Node -- ^ unassigned, implied conflicting node - -> Graph.Node -- ^ a UIP in the conflict graph - -> Cut Set gr a b -uipCut dlits levelArr conflGraph conflNode uip = - Cut { reasonSide = Set.filter (\i -> levelArr!(V $ abs i) > 0) $ - allNodes Set.\\ impliedByUIP - , conflictSide = impliedByUIP - , cutUIP = uip - , cutGraph = conflGraph } - where - -- Transitively implied, and not including the UIP. - impliedByUIP = Set.insert extraNode - . Set.fromList - . tail - $ DFS.reachable uip conflGraph - -- The UIP may not imply the assigned conflict variable which needs to - -- be on the conflict side, unless it's a decision variable or the UIP - -- itself. - extraNode = if L (negate conflNode) `elem` dlits || negate conflNode == uip - then conflNode -- idempotent addition - else negate conflNode - allNodes = Set.fromList $ Graph.nodes conflGraph - - --- | Generate a learned clause from a cut of the graph. Returns a pair of the --- learned clause and the decision level to which to backtrack. -cutLearn :: (Graph gr, Foldable f) => IAssignment -> FrozenLevelArray - -> Cut f gr a b -> (Clause, Int) -cutLearn a levelArr cut = - ( clause - -- The new decision level is the max level of all variables in the - -- clause, excluding the uip (which is always at the current decision - -- level). - , maximum0 (map (levelArr!) . (`without` V (abs $ cutUIP cut)) . map var $ clause) ) - where - -- The clause is composed of the variables on the reason side which have - -- at least one successor on the conflict side. The value of the variable - -- is the negation of its value under the current assignment. - clause = - foldl' (\ls i -> - if any (`elem` conflictSide cut) (Graph.suc (cutGraph cut) i) - then L (negate $ a!(V $ abs i)):ls - else ls) - [] (reasonSide cut) - maximum0 [] = 0 -- maximum0 has 0 as its max for the empty list - maximum0 xs = maximum xs - --- | Creates the conflict graph, where each node is labeled by its literal and --- level. There is also a distinguished /lambda/ node, as used by Sabharwal --- when he explains conflict graphs. --- --- Useful for getting pretty graphviz output of a conflict. -mkConflGraph :: DynGraph g => - IAssignment - -> FrozenLevelArray - -> ReasonMap - -> [Lit] -- ^ the trail (decision lits, in rev. chron. order) - -> (Lit, Clause) -- ^ conflicting literal and reason clause - -> ConflictGraph g -mkConflGraph mFr lev reasonMap _dlits (cLit, confl) = - Graph.mkGraph nodes' edges' - where - -- we pick out all the variables from the conflict graph, specially adding - -- both literals of the conflict variable, so that that variable has two - -- nodes in the graph. - nodes' = - ((0, cgLambda) :) $ - ((unLit cLit, CGNA cLit (-1)) :) $ - ((negate (unLit cLit), CGNA (negate cLit) (lev!(var cLit))) :) $ - -- annotate each node with its literal and level - map (\v -> (unVar v, CGNA (varToLit v) (lev!v))) $ - filter (\v -> v /= var cLit) $ - toList nodeSet' - - -- node set includes all variables reachable from conflict. This node set - -- construction needs a `seen' set because it might infinite loop - -- otherwise. - (nodeSet', edges') = - mkGr Set.empty (Set.empty, [ (unLit cLit, 0, ()) - , ((negate . unLit) cLit, 0, ()) ]) - [negate cLit, cLit] - varToLit v = (if v `isTrueUnder` mFr then id else negate) $ L (unVar v) - - -- seed with both conflicting literals - mkGr _ ne [] = ne - mkGr (seen :: Set Graph.Node) ne@(nodes, edges) (lit:lits) = - if haveSeen - then mkGr seen ne lits - else newNodes `seq` newEdges `seq` - mkGr seen' (newNodes, newEdges) (lits ++ pred) - where - haveSeen = seen `contains` litNode lit - newNodes = var lit `Set.insert` nodes - newEdges = [ ( litNode (negate x) -- unimplied lits from reasons are - -- complemented - , litNode lit, () ) - | x <- pred ] ++ edges - pred = filterReason $ - if lit == cLit then confl else - fst (Map.findWithDefault ([],undefined) (var lit) reasonMap) - `without` lit - filterReason = filter ( ((var lit /=) . var) .&&. - ((<= litLevel lit) . litLevel) ) - seen' = seen `with` litNode lit - litLevel l = if l == cLit then numDlits else lev!(var l) - numDlits = length _dlits - litNode l = -- lit to node - if var l == var cLit -- preserve sign of conflicting lit - then unLit l - else (abs . unLit) l - - - - --- | @doWhile cmd test@ first runs @cmd@, then loops testing @test@ and --- executing @cmd@. The traditional @do-while@ semantics, in other words. -doWhile :: (Monad m) => m () -> m Bool -> m () -doWhile body test = do - body - shouldContinue <- test - when shouldContinue $ doWhile body test diff --git a/tests/Properties.hs b/tests/Properties.hs --- a/tests/Properties.hs +++ b/tests/Properties.hs @@ -16,7 +16,6 @@ import Control.Exception( assert ) import Control.Monad import Data.Array.Unboxed -import Data.BitSet (hash) import Data.Bits hiding( xor ) import Data.Foldable hiding (sequence_) import Data.List (nub, splitAt) @@ -26,13 +25,14 @@ import Funsat.Circuit hiding( Circuit(..) ) import Funsat.Circuit( Circuit(input,true,false,ite,xor,onlyif) ) import Funsat.Types -import Funsat.Utils.Internal +import Funsat.Utils import Language.CNF.Parse.ParseDIMACS( parseFile ) import Prelude hiding ( or, and, all, any, elem, minimum, foldr, splitAt, concatMap, sum, concat ) import Funsat.Resolution( ResolutionTrace(..) ) import System.IO import System.Random -import Test.QuickCheck hiding (defaultConfig) +import Test.QuickCheck +import Test.QuickCheck.Gen( unGen ) import qualified Data.Foldable as Foldable import qualified Data.List as List @@ -58,10 +58,8 @@ hPutStr stderr "prop_clauseStatusUnderA: " >> check config prop_clauseStatusUnderA hPutStr stderr "prop_negDefNotUndefUnder: " >> check config prop_negDefNotUndefUnder hPutStr stderr "prop_undefUnderImpliesNegUndef: " >> check config prop_undefUnderImpliesNegUndef - hPutStr stderr "prop_litHash: " >> check config prop_litHash - hPutStr stderr "prop_varHash: " >> check config prop_varHash hPutStr stderr "prop_count: " >> check config prop_count - hPutStr stderr "prop_circuitToCnf: " >> check config prop_circuitToCnf + hPutStr stderr "prop_circuitToCnf: " >> check config{ maxSize = 10000} prop_circuitToCnf hPutStr stderr "prop_circuitSimplify: " >> check config prop_circuitSimplify -- Add more tests above here. Setting the rng keeps the SAT instances the @@ -86,42 +84,21 @@ hPutStr stderr "prop_resolutionChecker (rand): " check resChkConfig prop_resolutionChecker - -profile :: IO () -profile = do - -- hPutStr stderr "prop_circuitToCnf: " >> check config prop_circuitToCnf - - -- Add more tests above here. Setting the rng keeps the SAT instances the - -- same even if more tests are added above. I want this because if I make - -- a change that makes the solver dramatically faster or slower, I know - -- this wasn't due to the test distribution. - gen <- getStdGen - setStdGen (mkStdGen 42) - hPutStr stderr "prop_solveCorrect: " - check solveConfig prop_solveCorrect - - setStdGen gen - hPutStr stderr "prop_solveCorrect (rand): " - check solveConfig prop_solveCorrect - gen <- getStdGen - - setStdGen (mkStdGen 42) - hPutStr stderr "prop_resolutionChecker: " - check resChkConfig prop_resolutionChecker - - setStdGen gen - hPutStr stderr "prop_resolutionChecker (rand): " - check resChkConfig prop_resolutionChecker - - -config = QC.defaultConfig { configMaxTest = 1000 } +check :: Testable prop => Args -> prop -> IO () +check = QC.quickCheckWith +config = QC.stdArgs{ maxSuccess = 1400 + , maxSize = 800 + , maxDiscard = 1000 } -- Special configuration for the "solve this random instance" tests. -solveConfig = QC.defaultConfig { configMaxTest = 2000 } -resChkConfig = QC.defaultConfig{ configMaxTest = 1200 } +solveConfig = config{ maxSuccess = 2000 } +resChkConfig = config{ maxSuccess = 1200, maxSize = 600 } myConfigEvery testnum args = show testnum ++ ": " ++ show args ++ "\n\n" +trivial :: Testable p => Bool -> p -> Property +trivial t = classify t "trivial" + -- * Tests prop_solveCorrect (cnf :: CNF) = trivial (numClauses cnf < 2 || numVars cnf < 2) $ @@ -213,15 +190,7 @@ -- Nothing -> label "no propagation" True -- Just m' -> label "propagated" $ all (\l -> elem l m') m --- Make sure the bit set will work. -prop_litHash (k :: Lit) (l :: Lit) = - hash k == hash l <==> k == l - -prop_varHash (k :: Var) l = - hash k == hash l <==> k == l - - (<==>) = iff infixl 3 <==> @@ -366,7 +335,6 @@ newtype ArbBEnv = ArbBEnv (BEnv Var) deriving (Show) instance Arbitrary ArbBEnv where - coarbitrary = undefined arbitrary = sized $ \n -> do bools <- vector (n+1) :: Gen [Bool] return . ArbBEnv $ Map.fromList (zip [V 1 .. V (n+1)] bools) @@ -446,7 +414,7 @@ getCNF :: Int -> IO CNF getCNF maxVars = do g <- newStdGen - return (generate (maxVars * 3) g arbitrary) + return (unGen arbitrary g (maxVars * 3)) prob :: IO ParseCNF.CNF prob = do cnfOrError <- parseFile "./tests/problems/uf20/uf20-0119.cnf"