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

Safe HaskellNone
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) 
forall p . 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 
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) Source 

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