smtlib2-0.3.1: A type-safe interface to communicate with an SMT solver.

Safe HaskellSafe
LanguageHaskell98

Language.SMTLib2.Strategy

Documentation

data Tactic Source #

Constructors

Skip 
AndThen [Tactic] 
OrElse [Tactic] 
ParOr [Tactic] 
ParThen Tactic Tactic 
TryFor Tactic Integer 
If (Probe Bool) Tactic Tactic 
FailIf (Probe Bool) 
Show p => UsingParams (BuiltInTactic p) [p] 

Instances

data Probe a where Source #

Constructors

ProbeBoolConst :: Bool -> Probe Bool 
ProbeIntConst :: Integer -> Probe Integer 
ProbeAnd :: [Probe Bool] -> Probe Bool 
ProbeOr :: [Probe Bool] -> Probe Bool 
ProbeNot :: Probe Bool -> Probe Bool 
ProbeEq :: Show a => Probe a -> Probe a -> Probe Bool 
ProbeCompare :: SMTOrdOp -> Probe Integer -> Probe Integer -> Probe Bool 
IsPB :: Probe Bool 
ArithMaxDeg :: Probe Integer 
ArithAvgDeg :: Probe Integer 
ArithMaxBW :: Probe Integer 
ArithAvgBW :: Probe Integer 
IsQFLIA :: Probe Bool 
IsQFLRA :: Probe Bool 
IsQFLIRA :: Probe Bool 
IsILP :: Probe Bool 
IsQFNIA :: Probe Bool 
IsQFNRA :: Probe Bool 
IsNIA :: Probe Bool 
IsNRA :: Probe Bool 
IsUnbounded :: Probe Bool 
Memory :: Probe Integer 
Depth :: Probe Integer 
Size :: Probe Integer 
NumExprs :: Probe Integer 
NumConsts :: Probe Integer 
NumBoolConsts :: Probe Integer 
NumArithConsts :: Probe Integer 
NumBVConsts :: Probe Integer 
ProduceProofs :: Probe Bool 
ProduceModel :: Probe Bool 
ProduceUnsatCores :: Probe Bool 
HasPatterns :: Probe Bool 
IsPropositional :: Probe Bool 
IsQFBV :: Probe Bool 
IsQFBVEQ :: Probe Bool 

Instances

Show a => Show (Probe a) Source # 

Methods

showsPrec :: Int -> Probe a -> ShowS #

show :: Probe a -> String #

showList :: [Probe a] -> ShowS #

data AnyPar Source #

Constructors

ParBool Bool 
ParInt Integer 
ParDouble Double 

Instances

data BuiltInTactic p where Source #

Constructors

QFLRATactic :: BuiltInTactic QFLRATacticP 
CustomTactic :: String -> BuiltInTactic (String, AnyPar) 

Instances

data QFLRATacticP Source #

Constructors

ArithBranchCutRatio Integer 

Instances