funsat 0.6.1 → 0.6.2
raw patch · 10 files changed
+406/−567 lines, 10 filesdep ~QuickCheckdep ~arraydep ~base
Dependency ranges changed: QuickCheck, array, base, bitset, containers, fgl, mtl, pretty, random, time
Files
- Main.hs +31/−52
- funsat.cabal +22/−44
- src/Funsat/Circuit.hs +1/−7
- src/Funsat/Resolution.hs +1/−1
- src/Funsat/Solver.hs +63/−37
- src/Funsat/Types.hs +35/−39
- src/Funsat/Types/Internal.hs +9/−0
- src/Funsat/Utils.hs +229/−8
- src/Funsat/Utils/Internal.hs +0/−332
- tests/Properties.hs +15/−47
Main.hs view
@@ -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
funsat.cabal view
@@ -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
src/Funsat/Circuit.hs view
@@ -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 -- <http://okmij.org/ftp/Haskell/DSLSharing.hs>. 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
src/Funsat/Resolution.hs view
@@ -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
src/Funsat/Solver.hs view
@@ -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
src/Funsat/Types.hs view
@@ -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 "<STUArray Var Int>" instance Show (STUArray s Var Double) where show = const "<STUArray Var Double>" instance Show (STArray s a b) where show = const "<STArray>"----- * 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)-
src/Funsat/Types/Internal.hs view
@@ -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+
src/Funsat/Utils.hs view
@@ -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++
− src/Funsat/Utils/Internal.hs
@@ -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
tests/Properties.hs view
@@ -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"