mirror of
https://github.com/GaloisInc/what4.git
synced 2024-11-25 07:13:59 +03:00
Adapt what4-{abc,blt} to SolverEndSATQuery changes (#120)
This updates `what4-{abc,blt}` to use the new `SolverStartSATQueryRec` and `SolverEndSATQueryRec` data types introduced in #111. Fixes #119.
This commit is contained in:
parent
2989668fda
commit
af466fc8ba
@ -79,7 +79,8 @@ import What4.BaseTypes
|
||||
import What4.Concrete
|
||||
import What4.Config
|
||||
import What4.Interface
|
||||
(getConfiguration, IsExprBuilder, logSolverEvent, SolverEvent(..), andAllOf)
|
||||
( getConfiguration, IsExprBuilder, logSolverEvent
|
||||
, SolverEvent(..), SolverStartSATQuery(..), SolverEndSATQuery(..), andAllOf )
|
||||
import What4.Expr
|
||||
import What4.Expr.Builder
|
||||
import qualified What4.Expr.BoolMap as BM
|
||||
@ -743,10 +744,10 @@ checkSat sym logData e = do
|
||||
checkSupportedByAbc vars
|
||||
checkNoLatches vars
|
||||
logSolverEvent sym
|
||||
SolverStartSATQuery
|
||||
(SolverStartSATQuery $ SolverStartSATQueryRec
|
||||
{ satQuerySolverName = "ABC"
|
||||
, satQueryReason = logReason logData
|
||||
}
|
||||
})
|
||||
withNetwork $ \ntk -> do
|
||||
-- Get network
|
||||
let g = gia ntk
|
||||
@ -790,10 +791,10 @@ checkSat sym logData e = do
|
||||
logCallbackVerbose logData 2 "Calling ABC's QBF solver"
|
||||
runQBF ntk exist_cnt p max_qbf_iter
|
||||
logSolverEvent sym
|
||||
SolverEndSATQuery
|
||||
(SolverEndSATQuery $ SolverEndSATQueryRec
|
||||
{ satQueryResult = forgetModelAndCore res
|
||||
, satQueryError = Nothing
|
||||
}
|
||||
})
|
||||
return res
|
||||
|
||||
-- | Associate an element in a binding with the term.
|
||||
|
@ -132,18 +132,18 @@ runBLTInOverride sym logData ps contFn = do
|
||||
epar <- parseBLTParams . T.unpack <$> (getOpt =<< getOptionSetting bltParams cfg)
|
||||
par <- either fail return epar
|
||||
logSolverEvent sym
|
||||
SolverStartSATQuery
|
||||
(SolverStartSATQuery $ SolverStartSATQueryRec
|
||||
{ satQuerySolverName = "BLT"
|
||||
, satQueryReason = logReason logData
|
||||
}
|
||||
})
|
||||
withHandle par $ \h -> do
|
||||
forM_ ps (assume h)
|
||||
result <- checkSat h
|
||||
logSolverEvent sym
|
||||
SolverEndSATQuery
|
||||
(SolverEndSATQuery $ SolverEndSATQueryRec
|
||||
{ satQueryResult = forgetModelAndCore result
|
||||
, satQueryError = Nothing
|
||||
}
|
||||
})
|
||||
contFn result
|
||||
|
||||
------------------------------------------------------------------------
|
||||
|
Loading…
Reference in New Issue
Block a user