module Data.SBV.Provers.ABC(abc) where
import Data.SBV.Core.Data
import Data.SBV.SMT.SMT
abc :: SMTSolver
abc = SMTSolver {
name = ABC
, executable = "abc"
, options = ["-S", "%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000"]
, engine = standardEngine "SBV_ABC" "SBV_ABC_OPTIONS" id addTimeOut standardModel
, capabilities = SolverCapabilities {
capSolverName = "ABC"
, mbDefaultLogic = const Nothing
, supportsDefineFun = True
, supportsProduceModels = True
, supportsQuantifiers = False
, supportsUninterpretedSorts = False
, supportsUnboundedInts = False
, supportsReals = False
, supportsFloats = False
, supportsDoubles = False
, supportsOptimization = False
, supportsPseudoBooleans = False
, supportsUnsatCores = False
}
}
where addTimeOut _ _ = error "ABC: Timeout values are not supported"