Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fix bugs in simplifyDB and analyze in 1.5.0 #52

Merged
merged 16 commits into from
Nov 11, 2017
Merged

Fix bugs in simplifyDB and analyze in 1.5.0 #52

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
9f9e179
update version ids
Oct 31, 2017
ca95e05
simplifyDB: fix bugs
Oct 31, 2017
32a2d6a
seems the best heuristics on lastDL
Nov 1, 2017
c7a77b3
Revert "seems the best heuristics on lastDL"
Nov 2, 2017
f977ca0
commit for 'an effect of definition of LBD'
Nov 2, 2017
61a06a7
WIP: increment double smaller clauses in terms of size or LBD
Nov 2, 2017
c5864ba
just Glucose heuristics + update LBDs
Nov 5, 2017
71945ee
Revert "just Glucose heuristics + update LBDs"
Nov 5, 2017
7dac37d
Revert "WIP: increment double smaller clauses in terms of size or LBD"
Nov 5, 2017
7ec94f7
Revert "commit for 'an effect of definition of LBD'"
Nov 6, 2017
37b5125
Util/*; add signatures
Nov 8, 2017
1110253
moos.cabal: refactored
Nov 8, 2017
cb705d0
a tiny change for hlint
Nov 8, 2017
14742c1
EXP: reactivate the case: 'resolvent LBD < LBD'
Nov 9, 2017
45c8a6a
UPDATEVARACTIVITY EXP: re-implement C: size < resolvent size
Nov 10, 2017
c069430
UPDATEVARACTIVITY: mios uses 'learnt size < size' heuristics
Nov 11, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
167 changes: 40 additions & 127 deletions mios.cabal
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,10 +29,6 @@ Flag llvm
Description: Compile with llvm
Default: False

Flag lib
Description: Build the solver library
Default: False

Flag prof
Description: Build the profiler
Default: False
Expand All @@ -46,11 +42,7 @@ Flag utils
Default: False

library
hs-source-dirs: .
if flag(lib)
buildable: True
else
buildable: False
hs-source-dirs: src
default-language: Haskell2010
default-extensions: Strict
other-extensions: BangPatterns
Expand All @@ -71,10 +63,11 @@ library
SAT.Mios.Clause
SAT.Mios.ClauseManager
SAT.Mios.ClausePool
SAT.Mios.Vec
SAT.Mios.Glucose
SAT.Mios.Main
SAT.Mios.OptionParser
SAT.Mios.Solver
SAT.Mios.Vec
SAT.Mios.Types
SAT.Mios.Validator
SAT.Mios.Util.DIMACS.MinisatReader
Expand All @@ -85,87 +78,51 @@ library
SAT.Mios
build-depends: base >=4.10, vector >=0.12, ghc-prim >=0.5, bytestring >=0.10, primitive >=0.6
if flag(llvm)
ghc-options: -O2 -ignore-asserts -funbox-strict-fields -fllvm -optlo-O2 -optlc-O2
ghc-options: -O2 -funbox-strict-fields -fllvm -optlo-O3 -optlc-O3 -fwarn-missing-signatures
else
ghc-options: -O2 -ignore-asserts -funbox-strict-fields
ghc-options: -O2 -funbox-strict-fields -msse2 -fwarn-missing-signatures

executable mios-WIP
hs-source-dirs: src app
executable mios-52
hs-source-dirs: app
main-is: mios.hs
if flag(prof)
buildable: False
else
buildable: True
default-language: Haskell2010
default-extensions: Strict
build-depends: base >=4.10, vector >=0.12, ghc-prim >=0.5, bytestring >=0.10, primitive >=0.6
default-extensions: Strict
build-depends: base, mios
if flag(llvm)
ghc-options: -O2 -funbox-strict-fields -fllvm -optlo-O3 -optlc-O3 -rtsopts -fwarn-missing-signatures
else
ghc-options: -O2 -funbox-strict-fields -msse2 -rtsopts -fwarn-missing-signatures
other-modules:
SAT.Mios.Clause
SAT.Mios.ClauseManager
SAT.Mios.ClausePool
SAT.Mios.Glucose
SAT.Mios.Main
SAT.Mios.OptionParser
SAT.Mios.Solver
SAT.Mios.Types
SAT.Mios.Validator
SAT.Mios.Vec
SAT.Mios

executable mios-WIP-prof
hs-source-dirs: src app
executable mios-52-prof
hs-source-dirs: app
main-is: mios.hs
if flag(prof)
buildable: True
else
buildable: False
default-language: Haskell2010
default-extensions: Strict
build-depends: base >=4.10, vector >=0.12, ghc-prim >=0.5, bytestring >=0.10, primitive >=0.6
default-extensions: Strict
build-depends: base, mios
if flag(llvm)
ghc-options: -O2 -funbox-strict-fields -fllvm -optlo-O3 -prof -fprof-auto -rtsopts -ddump-simpl
else
ghc-options: -O2 -funbox-strict-fields -prof -fprof-auto -rtsopts -ddump-simpl
other-modules:
SAT.Mios.Clause
SAT.Mios.ClauseManager
SAT.Mios.ClausePool
SAT.Mios.Glucose
SAT.Mios.Main
SAT.Mios.OptionParser
SAT.Mios.Solver
SAT.Mios.Types
SAT.Mios.Validator
SAT.Mios.Vec
SAT.Mios

executable cnf-stat
hs-source-dirs: src utils
hs-source-dirs: utils
main-is: cnf-stat.hs
if flag(utils)
buildable: True
else
buildable: False
default-language: Haskell2010
default-extensions: Strict
build-depends: base >=4.10, vector >=0.12, ghc-prim >=0.5, bytestring >=0.10, primitive >=0.6
ghc-options: -O1 -ignore-asserts -funbox-strict-fields
other-modules:
SAT.Mios.Clause
SAT.Mios.ClauseManager
SAT.Mios.ClausePool
SAT.Mios.Glucose
SAT.Mios.Main
SAT.Mios.OptionParser
SAT.Mios.Solver
SAT.Mios.Types
SAT.Mios.Validator
SAT.Mios.Vec
SAT.Mios
default-extensions: Strict
build-depends: base, mios, bytestring >=0.10
ghc-options: -O1 -ignore-asserts -funbox-strict-fields

executable mios-mc
hs-source-dirs: MultiConflict app
Expand All @@ -175,22 +132,12 @@ executable mios-mc
else
buildable: False
default-language: Haskell2010
default-extensions: Strict
build-depends: base >=4.10, vector >=0.12, ghc-prim >=0.5, bytestring >=0.10, primitive >=0.6
default-extensions: Strict
build-depends: base, mios, bytestring >=0.10
if flag(llvm)
ghc-options: -O2 -ignore-asserts -funbox-strict-fields -fllvm -optlo-O2 -optlc-O2
else
ghc-options: -O2 -ignore-asserts -funbox-strict-fields
other-modules:
SAT.Mios.Clause
SAT.Mios.ClauseManager
SAT.Mios.Main
SAT.Mios.OptionParser
SAT.Mios.Solver
SAT.Mios.Types
SAT.Mios.Validator
SAT.Mios.Vec
SAT.Mios

executable mios-mc-prof
hs-source-dirs: MultiConflict app
Expand All @@ -200,19 +147,9 @@ executable mios-mc-prof
else
buildable: False
default-language: Haskell2010
default-extensions: Strict
build-depends: base >=4.10, vector >=0.12, ghc-prim >=0.5, bytestring >=0.10, primitive >=0.6
ghc-options: -O2 -ignore-asserts -funbox-strict-fields -prof -fprof-auto
other-modules:
SAT.Mios.Clause
SAT.Mios.ClauseManager
SAT.Mios.Main
SAT.Mios.OptionParser
SAT.Mios.Solver
SAT.Mios.Types
SAT.Mios.Validator
SAT.Mios.Vec
SAT.Mios
default-extensions: Strict
build-depends: base, mios, bytestring >=0.10
ghc-options: -O2 -ignore-asserts -funbox-strict-fields -prof -fprof-auto

executable mc-dump2csv
hs-source-dirs: MultiConflict
Expand All @@ -222,13 +159,9 @@ executable mc-dump2csv
else
buildable: False
default-language: Haskell2010
default-extensions: Strict
build-depends: base >=4.10, vector >= 0.12, bytestring >=0.10, primitive >=0.6
ghc-options: -O1 -ignore-asserts -funbox-strict-fields
other-modules:
SAT.Mios.Types
SAT.Mios.Util.Stat
SAT.Mios.Vec
default-extensions: Strict
build-depends: base, mios, bytestring >=0.10
ghc-options: -O1 -ignore-asserts -funbox-strict-fields

executable mc-averagecsv
hs-source-dirs: MultiConflict
Expand All @@ -238,13 +171,9 @@ executable mc-averagecsv
else
buildable: False
default-language: Haskell2010
default-extensions: Strict
build-depends: base >=4.10, vector >= 0.12, bytestring >=0.10, primitive >=0.6
ghc-options: -O1 -ignore-asserts -funbox-strict-fields
other-modules:
SAT.Mios.Types
SAT.Mios.Util.Stat
SAT.Mios.Vec
default-extensions: Strict
build-depends: base, mios, bytestring >=0.10
ghc-options: -O1 -ignore-asserts -funbox-strict-fields

executable mc-summary
hs-source-dirs: MultiConflict
Expand All @@ -254,13 +183,9 @@ executable mc-summary
else
buildable: False
default-language: Haskell2010
default-extensions: Strict
build-depends: base >=4.10, vector >= 0.12, bytestring >=0.10, primitive >=0.6
ghc-options: -O1 -ignore-asserts -funbox-strict-fields
other-modules:
SAT.Mios.Types
SAT.Mios.Util.Stat
SAT.Mios.Vec
default-extensions: Strict
build-depends: base, mios, bytestring >=0.10
ghc-options: -O1 -ignore-asserts -funbox-strict-fields

executable mc-stat2csv
hs-source-dirs: MultiConflict
Expand All @@ -270,13 +195,9 @@ executable mc-stat2csv
else
buildable: False
default-language: Haskell2010
default-extensions: Strict
build-depends: base >=4.10, vector >= 0.11, bytestring >=0.10, primitive >=0.6
ghc-options: -O1 -ignore-asserts -funbox-strict-fields
other-modules:
SAT.Mios.Types
SAT.Mios.Util.Stat
SAT.Mios.Vec
default-extensions: Strict
build-depends: base, mios, bytestring >=0.10
ghc-options: -O1 -ignore-asserts -funbox-strict-fields

executable mc-pickup
hs-source-dirs: MultiConflict
Expand All @@ -286,13 +207,9 @@ executable mc-pickup
else
buildable: False
default-language: Haskell2010
default-extensions: Strict
build-depends: base >=4.10, vector >= 0.12, bytestring >=0.10, primitive >=0.6
ghc-options: -O1 -ignore-asserts -funbox-strict-fields
other-modules:
SAT.Mios.Types
SAT.Mios.Util.Stat
SAT.Mios.Vec
default-extensions: Strict
build-depends: base, mios, bytestring >=0.10
ghc-options: -O1 -ignore-asserts -funbox-strict-fields

executable mc-numbers
hs-source-dirs: MultiConflict
Expand All @@ -302,10 +219,6 @@ executable mc-numbers
else
buildable: False
default-language: Haskell2010
default-extensions: Strict
build-depends: base >=4.10, vector >= 0.12, bytestring >=0.10, primitive >=0.6
ghc-options: -O1 -ignore-asserts -funbox-strict-fields
other-modules:
SAT.Mios.Types
SAT.Mios.Util.Stat
SAT.Mios.Vec
default-extensions: Strict
build-depends: base, mios, bytestring >=0.10
ghc-options: -O1 -ignore-asserts -funbox-strict-fields
2 changes: 1 addition & 1 deletion src/SAT/Mios.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ import SAT.Mios.Validator

-- | version name
versionId :: String
versionId = "mios-1.5.0WIP"
versionId = "mios-1.5.0WIP #52fix-bugs"

reportElapsedTime :: Bool -> String -> Integer -> IO Integer
reportElapsedTime False _ _ = return 0
Expand Down
39 changes: 15 additions & 24 deletions src/SAT/Mios/Main.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -163,7 +163,7 @@ analyze s@Solver{..} confl = do
setNth an'seen v 1
if dl <= l -- cancelUntil doesn't clear level of cancelled literals
then do
-- glucose heuristics
-- UPDATEVARACTIVITY: glucose heuristics
r <- getNth reason v
when (r /= NullClause) $ do
ra <- get' (rank r)
Expand Down Expand Up @@ -216,7 +216,7 @@ analyze s@Solver{..} confl = do
then setNth litsLearnt j l >> loopOnLits (i + 1) (j + 1)
else loopOnLits (i + 1) j
loopOnLits 2 2 -- the first literal is specail
-- glucose heuristics
-- UPDATEVARACTIVITY: glucose heuristics
nld <- get' an'lastDL
r <- get' litsLearnt -- this is an estimated LBD value based on the clause size
let loopOnLastDL :: Int -> IO ()
Expand Down Expand Up @@ -586,36 +586,27 @@ simplifyDB s@Solver{..} = do
if p /= NullClause
then set' ok False >> return False
else do
-- Clear watcher lists:
n <- get' trail
let loopOnLit ((< n) -> False) = return ()
loopOnLit i = do l <- getNth trail i
reset . getNthWatcher watches $ l
reset . getNthWatcher watches $ negateLit l
loopOnLit $ i + 1
loopOnLit 1
-- Remove satisfied clauses:
-- Remove satisfied clauses and their watcher lists:
let
for :: Int -> IO Bool
for ((< 2) -> False) = return True
for t = do
let ptr = if t == 0 then learnts else clauses
vec' <- getClauseVector ptr
n' <- get' ptr
for :: ClauseExtManager -> IO ()
for mgr = do
vec' <- getClauseVector mgr
n' <- get' mgr
let
loopOnVector :: Int -> Int -> IO Bool
loopOnVector ((< n') -> False) j = shrinkBy ptr (n' - j) >> return True
loopOnVector :: Int -> Int -> IO ()
loopOnVector ((< n') -> False) j = shrinkBy mgr (n' - j)
loopOnVector i j = do
c <- getNth vec' i
l <- locked s c
r <- simplify s c
if not l && r
r <- if l then return False else simplify s c
if r
then removeWatch s c >> loopOnVector (i + 1) j
else setNth vec' j c >> loopOnVector (i + 1) (j + 1)
else unless (i == j) (setNth vec' j c) >> loopOnVector (i + 1) (j + 1)
loopOnVector 0 0
ret <- for 0
for clauses
for learnts
reset watches
return ret
return True
else return False

-- | #M22
Expand Down
5 changes: 5 additions & 0 deletions src/SAT/Mios/Util/BoolExp.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,10 @@ numberOfVariables (Cnf (a, b) _) = a + b - tseitinBase
numberOfClauses :: BoolForm -> Int
numberOfClauses (Cnf _ l) = length l

boolFormTrue :: BoolForm
boolFormTrue = Cnf (-1, 1) []

boolFormFalse :: BoolForm
boolFormFalse = Cnf (-1, -1) []

instance BoolComponent Bool where
Expand Down Expand Up @@ -186,6 +189,7 @@ disjunctionOf [] = boolFormFalse
disjunctionOf (x:l) = foldl' (-|-) x l

-- | an alias of 'disjunctionOf'
(-|||-) :: [BoolForm] -> BoolForm
(-|||-) = disjunctionOf

-- | merge [BoolForm] by '(-&-)'
Expand All @@ -194,6 +198,7 @@ conjunctionOf [] = boolFormTrue
conjunctionOf (x:l) = foldl' (-&-) x l

-- | an alias of 'conjunctionOf'
(-&&&-) :: [BoolForm] -> BoolForm
(-&&&-) = conjunctionOf

-- | converts a BoolForm to "[[Int]]"
Expand Down
Loading