Language.SMTLib2.Strategy

Documentation

data Tactic

Constructors

Skip

AndThen [Tactic]

OrElse [Tactic]

ParOr [Tactic]

ParThen Tactic Tactic

TryFor Tactic Integer

If (Probe Bool) Tactic Tactic

FailIf (Probe Bool)

forall p . Show p => UsingParams (BuiltInTactic p) [p]

Instances

Show Tactic

data Probe a where

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

ProbeGt :: Probe Integer -> Probe Integer -> Probe Bool

ProbeGe :: Probe Integer -> Probe Integer -> Probe Bool

ProbeLt :: Probe Integer -> Probe Integer -> Probe Bool

ProbeLe :: 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)

data AnyPar

Constructors

ParBool Bool

ParInt Integer

ParDouble Double

Instances

Show AnyPar

data BuiltInTactic p where

Constructors

QFLRATactic :: BuiltInTactic QFLRATacticP

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

Instances

Show (BuiltInTactic p)

data QFLRATacticP

Constructors

ArithBranchCutRatio Integer

Instances

Show QFLRATacticP