what4-1.6.3: Solver-agnostic symbolic values support for issuing queries

Safe Haskell | None
Language | Haskell2010

What4.Protocol.SMTLib2.Syntax

Contents

- Commands
- Declarations
- Assertions and checking
- SyGuS
- Logic
- Sort
- Term
- Core theory
- `Ints`, `Reals`, `Reals_Ints` theories
- Bitvector theory and extensions
  - Extensions provided by QF_BV
- Array theory

Description

This module defines types and operations for generating SMTLIB2 files.

It does not depend on the rest of What4 so that it can be used directly by clients interested in generating SMTLIB without depending on the What4 formula interface. All the type constructors are exposed so that clients can generate new values that are not exposed through this interface.

Synopsis

- newtype Command = Cmd Builder
- setLogic :: Logic -> Command
- setOption :: Text -> Text -> Command
- setProduceModels :: Bool -> Command
- data SMTInfoFlag
  - = Name
  - | Version
  - | ErrorBehavior
  - | InfoKeyword Text
- getInfo :: SMTInfoFlag -> Command
- getVersion :: Command
- getName :: Command
- getErrorBehavior :: Command
- exit :: Command
- declareSort :: Symbol -> Integer -> Command
- defineSort :: Symbol -> [Symbol] -> Sort -> Command
- declareConst :: Text -> Sort -> Command
- declareFun :: Text -> [Sort] -> Sort -> Command
- defineFun :: Text -> [(Text, Sort)] -> Sort -> Term -> Command
- type Symbol = Text
- checkSat :: Command
- checkSatAssuming :: [Term] -> Command
- checkSatWithAssumptions :: [Text] -> Command
- getModel :: Command
- getValue :: [Term] -> Command
- push :: Integer -> Command
- pop :: Integer -> Command
- resetAssertions :: Command
- assert :: Term -> Command
- assertNamed :: Term -> Text -> Command
- getUnsatAssumptions :: Command
- getUnsatCore :: Command
- getAbduct :: Text -> Term -> Command
- getAbductNext :: Command
- synthFun :: Text -> [(Text, Sort)] -> Sort -> Command
- declareVar :: Text -> Sort -> Command
- constraint :: Term -> Command
- checkSynth :: Command
- newtype Logic = Logic Builder
- qf_bv :: Logic
- allSupported :: Logic
- allLogic :: Logic
- hornLogic :: Logic
- newtype Sort = Sort {
  - unSort :: Builder
  }
- boolSort :: Sort
- bvSort :: Natural -> Sort
- intSort :: Sort
- realSort :: Sort
- varSort :: Symbol -> Sort
- newtype Term = T {
  - renderTerm :: Builder
  }
- un_app :: Builder -> Term -> Term
- bin_app :: Builder -> Term -> Term -> Term
- term_app :: Builder -> [Term] -> Term
- pairwise_app :: Builder -> [Term] -> Term
- namedTerm :: Term -> Text -> Term
- builder_list :: [Builder] -> Builder
- true :: Term
- false :: Term
- not :: Term -> Term
- implies :: [Term] -> Term -> Term
- and :: [Term] -> Term
- or :: [Term] -> Term
- xor :: [Term] -> Term
- eq :: [Term] -> Term
- distinct :: [Term] -> Term
- ite :: Term -> Term -> Term -> Term
- forall_ :: [(Text, Sort)] -> Term -> Term
- exists_ :: [(Text, Sort)] -> Term -> Term
- letBinder :: [(Text, Term)] -> Term -> Term
- negate :: Term -> Term
- numeral :: Integer -> Term
- decimal :: Integer -> Term
- sub :: Term -> [Term] -> Term
- add :: [Term] -> Term
- mul :: [Term] -> Term
- div :: Term -> [Term] -> Term
- (./) :: Term -> [Term] -> Term
- mod :: Term -> Term -> Term
- abs :: Term -> Term
- le :: [Term] -> Term
- lt :: [Term] -> Term
- ge :: [Term] -> Term
- gt :: [Term] -> Term
- toReal :: Term -> Term
- toInt :: Term -> Term
- isInt :: Term -> Term
- concat :: Term -> Term -> Term
- extract :: Natural -> Natural -> Term -> Term
- bvnot :: Term -> Term
- bvand :: Term -> [Term] -> Term
- bvor :: Term -> [Term] -> Term
- bvxor :: Term -> [Term] -> Term
- bvneg :: Term -> Term
- bvadd :: Term -> [Term] -> Term
- bvsub :: Term -> Term -> Term
- bvmul :: Term -> [Term] -> Term
- bvudiv :: Term -> Term -> Term
- bvurem :: Term -> Term -> Term
- bvshl :: Term -> Term -> Term
- bvlshr :: Term -> Term -> Term
- bvult :: Term -> Term -> Term
- bit0 :: Term
- bit1 :: Term
- bvbinary :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> Term
- bvdecimal :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> Term
- bvhexadecimal :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> Term
- bvashr :: Term -> Term -> Term
- bvslt :: Term -> Term -> Term
- bvsle :: Term -> Term -> Term
- bvule :: Term -> Term -> Term
- bvsgt :: Term -> Term -> Term
- bvsge :: Term -> Term -> Term
- bvugt :: Term -> Term -> Term
- bvuge :: Term -> Term -> Term
- bvsdiv :: Term -> Term -> Term
- bvsrem :: Term -> Term -> Term
- bvsignExtend :: Integer -> Term -> Term
- bvzeroExtend :: Integer -> Term -> Term
- arraySort :: Sort -> Sort -> Sort
- arrayConst :: Sort -> Sort -> Term -> Term
- select :: Term -> Term -> Term
- store :: Term -> Term -> Term -> Term

# Commands

newtype Command Source #

This represents a command to be sent to the SMT solver.

Constructors

Cmd Builder |

setLogic :: Logic -> Command Source #

Set the logic of the SMT solver

setOption :: Text -> Text -> Command Source #

Set an option in the SMT solver

The name should not need to be prefixed with a colon."

setProduceModels :: Bool -> Command Source #

Set option to produce models

This is a widely used option so, we we have a custom command to make it.

data SMTInfoFlag Source #

This is a subtype of the type of the same name in Data.SBV.Control.

Constructors

Name |
Version |
ErrorBehavior |
InfoKeyword Text |

#### Instances

Instances details

Data SMTInfoFlag Source # |

Instance details

Defined in What4.Protocol.SMTLib2.Syntax

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SMTInfoFlag -> c SMTInfoFlag Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c SMTInfoFlag Source #

toConstr :: SMTInfoFlag -> Constr Source #

dataTypeOf :: SMTInfoFlag -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c SMTInfoFlag) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c SMTInfoFlag) Source #

gmapT :: (forall b. Data b => b -> b) -> SMTInfoFlag -> SMTInfoFlag Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SMTInfoFlag -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SMTInfoFlag -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> SMTInfoFlag -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> SMTInfoFlag -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag Source #

Generic SMTInfoFlag Source # |

Instance details

Defined in What4.Protocol.SMTLib2.Syntax

Associated Types

type Rep SMTInfoFlag |

Instance details

Defined in What4.Protocol.SMTLib2.Syntax

type Rep SMTInfoFlag = D1 ('MetaData "SMTInfoFlag" "What4.Protocol.SMTLib2.Syntax" "what4-1.6.3-9uBVkRxr1Ru1evGDxWAmM9" 'False) ((C1 ('MetaCons "Name" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Version" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ErrorBehavior" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InfoKeyword" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text))))

Methods

from :: SMTInfoFlag -> Rep SMTInfoFlag x Source #

to :: Rep SMTInfoFlag x -> SMTInfoFlag Source #

Show SMTInfoFlag Source # |
Instance details Defined in What4.Protocol.SMTLib2.Syntax Methods showsPrec :: Int -> SMTInfoFlag -> ShowS Source # show :: SMTInfoFlag -> String Source # showList :: [SMTInfoFlag] -> ShowS Source #
Eq SMTInfoFlag Source # |
Instance details Defined in What4.Protocol.SMTLib2.Syntax Methods (==) :: SMTInfoFlag -> SMTInfoFlag -> Bool Source # (/=) :: SMTInfoFlag -> SMTInfoFlag -> Bool Source #
Ord SMTInfoFlag Source # |

Instance details

Defined in What4.Protocol.SMTLib2.Syntax

Methods

compare :: SMTInfoFlag -> SMTInfoFlag -> Ordering Source #

(<) :: SMTInfoFlag -> SMTInfoFlag -> Bool Source #

(<=) :: SMTInfoFlag -> SMTInfoFlag -> Bool Source #

(>) :: SMTInfoFlag -> SMTInfoFlag -> Bool Source #

(>=) :: SMTInfoFlag -> SMTInfoFlag -> Bool Source #

max :: SMTInfoFlag -> SMTInfoFlag -> SMTInfoFlag Source #

min :: SMTInfoFlag -> SMTInfoFlag -> SMTInfoFlag Source #

type Rep SMTInfoFlag Source # |

Instance details

Defined in What4.Protocol.SMTLib2.Syntax

type Rep SMTInfoFlag = D1 ('MetaData "SMTInfoFlag" "What4.Protocol.SMTLib2.Syntax" "what4-1.6.3-9uBVkRxr1Ru1evGDxWAmM9" 'False) ((C1 ('MetaCons "Name" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Version" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ErrorBehavior" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InfoKeyword" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Text))))

getInfo :: SMTInfoFlag -> Command Source #

A `get-info` command

getVersion :: Command Source #

getName :: Command Source #

getErrorBehavior :: Command Source #

exit :: Command Source #

Request the SMT solver to exit

# Declarations

declareSort :: Symbol -> Integer -> Command Source #

Declare an uninterpreted sort with the given number of sort parameters.

defineSort Source #

Arguments

:: Symbol | Name of new sort
-> [Symbol] | Parameters for polymorphic sorts
-> Sort | Definition
-> Command |

Define a sort in terms of other sorts

declareConst :: Text -> Sort -> Command Source #

Declare a constant with the given name and return types.

declareFun :: Text -> [Sort] -> Sort -> Command Source #

Declare a function with the given name, argument types, and return type.

defineFun :: Text -> [(Text, Sort)] -> Sort -> Term -> Command Source #

Declare a function with the given name, argument types, and return type.

type Symbol = Text Source #

# Assertions and checking

checkSat :: Command Source #

Check the satisfiability of the current assertions

checkSatAssuming :: [Term] -> Command Source #

Check the satisfiability of the current assertions and the additional ones in the list.

checkSatWithAssumptions :: [Text] -> Command Source #

Check satisfiability of the given atomic assumptions in the current context.

NOTE! The names of variables passed to this function MUST be generated using a `declare-fun` statement, and NOT a `define-fun` statement. Thus, if you want to bind an arbitrary term, you must declare a new term and assert that it is equal to it's definition. Yes, this is quite irritating.

getModel :: Command Source #

Get the model associated with the last call to `check-sat`.

getValue :: [Term] -> Command Source #

Get the values associated with the terms from the last call to `check-sat`.

push :: Integer -> Command Source #

Push the given number of scope frames to the SMT solver.

pop :: Integer -> Command Source #

Pop the given number of scope frames to the SMT solver.

resetAssertions :: Command Source #

Empties the assertion stack and remove all global assertions and declarations.

assert :: Term -> Command Source #

Assert the predicate holds in the current context.

assertNamed :: Term -> Text -> Command Source #

Assert the predicate holds in the current context, and assign it a name so it can appear in unsatisfiable core results.

getUnsatAssumptions :: Command Source #

getUnsatCore :: Command Source #

getAbduct :: Text -> Term -> Command Source #

Get an abduct that entails the formula, and bind it to the name

getAbductNext :: Command Source #

Get the next command, called after a get-abduct command

# SyGuS

synthFun :: Text -> [(Text, Sort)] -> Sort -> Command Source #

Declare a SyGuS function to synthesize with the given name, arguments, and return type.

declareVar :: Text -> Sort -> Command Source #

Declare a SyGuS variable with the given name and type.

constraint :: Term -> Command Source #

Add the SyGuS constraint to the current synthesis problem.

checkSynth :: Command Source #

Ask the SyGuS solver to find a solution for the synthesis problem corresponding to the current functions-to-synthesize, variables and constraints.

# Logic

newtype Logic Source #

Identifies the set of predefined sorts and operators available.

Constructors

Logic Builder |

qf_bv :: Logic Source #

Use the QF_BV logic

allSupported :: Logic Source #

Deprecated: Use allLogic instead

Set the logic to all supported logics.

allLogic :: Logic Source #

Set the logic to all supported logics.

hornLogic :: Logic Source #

Use the Horn logic

# Sort

newtype Sort Source #

Sort for SMTLIB expressions

Constructors

Sort |

Fields

- unSort :: Builder

boolSort :: Sort Source #

Booleans

bvSort :: Natural -> Sort Source #

Bitvectors with the given number of bits.

intSort :: Sort Source #

Integers

realSort :: Sort Source #

Real numbers

varSort :: Symbol -> Sort Source #

Create a sort from a symbol name

# Term

newtype Term Source #

Denotes an expression in the SMT solver

Constructors

T |

Fields

- renderTerm :: Builder

#### Instances

Instances details

Monoid Term Source # |
Instance details Defined in What4.Protocol.SMTLib2.Syntax Methods mempty :: Term Source # mappend :: Term -> Term -> Term Source # mconcat :: [Term] -> Term Source #
Semigroup Term Source # |
Instance details Defined in What4.Protocol.SMTLib2.Syntax Methods (<>) :: Term -> Term -> Term Source # sconcat :: NonEmpty Term -> Term Source # stimes :: Integral b => b -> Term -> Term Source #
IsString Term Source # |
Instance details Defined in What4.Protocol.SMTLib2.Syntax Methods fromString :: String -> Term Source #
Num Term Source # |
Instance details Defined in What4.Protocol.SMTLib2 Methods (+) :: Term -> Term -> Term Source # (-) :: Term -> Term -> Term Source # (*) :: Term -> Term -> Term Source # negate :: Term -> Term Source # abs :: Term -> Term Source # signum :: Term -> Term Source # fromInteger :: Integer -> Term Source #
SupportTermOps Term Source # |

Instance details

Defined in What4.Protocol.SMTLib2

Methods

boolExpr :: Bool -> Term Source #

notExpr :: Term -> Term Source #

andAll :: [Term] -> Term Source #

orAll :: [Term] -> Term Source #

(.&&) :: Term -> Term -> Term Source #

(.||) :: Term -> Term -> Term Source #

(.==) :: Term -> Term -> Term Source #

(./=) :: Term -> Term -> Term Source #

impliesExpr :: Term -> Term -> Term Source #

letExpr :: [(Text, Term)] -> Term -> Term Source #

ite :: Term -> Term -> Term -> Term Source #

sumExpr :: [Term] -> Term Source #

termIntegerToReal :: Term -> Term Source #

termRealToInteger :: Term -> Term Source #

integerTerm :: Integer -> Term Source #

rationalTerm :: Rational -> Term Source #

(.<=) :: Term -> Term -> Term Source #

(.<) :: Term -> Term -> Term Source #

(.>) :: Term -> Term -> Term Source #

(.>=) :: Term -> Term -> Term Source #

intAbs :: Term -> Term Source #

intDiv :: Term -> Term -> Term Source #

intMod :: Term -> Term -> Term Source #

intDivisible :: Term -> Natural -> Term Source #

bvTerm :: forall (w :: Nat). NatRepr w -> BV w -> Term Source #

bvNeg :: Term -> Term Source #

bvAdd :: Term -> Term -> Term Source #

bvSub :: Term -> Term -> Term Source #

bvMul :: Term -> Term -> Term Source #

bvSLe :: Term -> Term -> Term Source #

bvULe :: Term -> Term -> Term Source #

bvSLt :: Term -> Term -> Term Source #

bvULt :: Term -> Term -> Term Source #

bvUDiv :: Term -> Term -> Term Source #

bvURem :: Term -> Term -> Term Source #

bvSDiv :: Term -> Term -> Term Source #

bvSRem :: Term -> Term -> Term Source #

bvAnd :: Term -> Term -> Term Source #

bvOr :: Term -> Term -> Term Source #

bvXor :: Term -> Term -> Term Source #

bvNot :: Term -> Term Source #

bvShl :: Term -> Term -> Term Source #

bvLshr :: Term -> Term -> Term Source #

bvAshr :: Term -> Term -> Term Source #

bvConcat :: Term -> Term -> Term Source #

bvExtract :: forall (w :: Nat). NatRepr w -> Natural -> Natural -> Term -> Term Source #

bvTestBit :: forall (w :: Nat). NatRepr w -> Natural -> Term -> Term Source #

bvSumExpr :: forall (w :: Nat). NatRepr w -> [Term] -> Term Source #

floatTerm :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> BigFloat -> Term Source #

floatNeg :: Term -> Term Source #

floatAbs :: Term -> Term Source #

floatSqrt :: RoundingMode -> Term -> Term Source #

floatAdd :: RoundingMode -> Term -> Term -> Term Source #

floatSub :: RoundingMode -> Term -> Term -> Term Source #

floatMul :: RoundingMode -> Term -> Term -> Term Source #

floatDiv :: RoundingMode -> Term -> Term -> Term Source #

floatRem :: Term -> Term -> Term Source #

floatFMA :: RoundingMode -> Term -> Term -> Term -> Term Source #

floatEq :: Term -> Term -> Term Source #

floatFpEq :: Term -> Term -> Term Source #

floatLe :: Term -> Term -> Term Source #

floatLt :: Term -> Term -> Term Source #

floatIsNaN :: Term -> Term Source #

floatIsInf :: Term -> Term Source #

floatIsZero :: Term -> Term Source #

floatIsPos :: Term -> Term Source #

floatIsNeg :: Term -> Term Source #

floatIsSubnorm :: Term -> Term Source #

floatIsNorm :: Term -> Term Source #

floatCast :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

floatRound :: RoundingMode -> Term -> Term Source #

floatFromBinary :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> Term -> Term Source #

bvToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

sbvToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

realToFloat :: forall (fpp :: FloatPrecision). FloatPrecisionRepr fpp -> RoundingMode -> Term -> Term Source #

floatToBV :: Natural -> RoundingMode -> Term -> Term Source #

floatToSBV :: Natural -> RoundingMode -> Term -> Term Source #

floatToReal :: Term -> Term Source #

realIsInteger :: Term -> Term Source #

realDiv :: Term -> Term -> Term Source #

realSin :: Term -> Term Source #

realCos :: Term -> Term Source #

realTan :: Term -> Term Source #

realATan2 :: Term -> Term -> Term Source #

realSinh :: Term -> Term Source #

realCosh :: Term -> Term Source #

realTanh :: Term -> Term Source #

realExp :: Term -> Term Source #

realLog :: Term -> Term Source #

smtFnApp :: Term -> [Term] -> Term Source #

smtFnUpdate :: Maybe (Term -> [Term] -> Term -> Term) Source #

lambdaTerm :: Maybe ([(Text, Some TypeMap)] -> Term -> Term) Source #

fromText :: Text -> Term Source #

un_app :: Builder -> Term -> Term Source #

Construct an expression with the given operator and single argument.

bin_app :: Builder -> Term -> Term -> Term Source #

Construct an expression with the given operator and two arguments.

term_app :: Builder -> [Term] -> Term Source #

Construct an expression with the given operator and list of arguments.

pairwise_app :: Builder -> [Term] -> Term Source #

Construct a chainable term with the given relation

`pairwise_app p [x1, x2, ..., xn]` is equivalent to forall_{i,j} p x_i x_j@.

namedTerm :: Term -> Text -> Term Source #

Append a "name" to a term so that it will be printed when `(get-assignment)` is called.

builder_list :: [Builder] -> Builder Source #

# Core theory

true :: Term Source #

`true` Boolean term

false :: Term Source #

`false` Boolean term

not :: Term -> Term Source #

Complement a Boolean

implies :: [Term] -> Term -> Term Source #

`implies c r` is equivalent to `c1 => c2 => .. cn => r`.

and :: [Term] -> Term Source #

Conjunction of all terms

or :: [Term] -> Term Source #

Disjunction of all terms

xor :: [Term] -> Term Source #

Xor of all terms

eq :: [Term] -> Term Source #

Return true if all terms are equal.

distinct :: [Term] -> Term Source #

Asserts that each term in the list is unique.

ite :: Term -> Term -> Term -> Term Source #

Create an if-then-else expression.

forall_ :: [(Text, Sort)] -> Term -> Term Source #

`forall_ vars t` denotes a predicate that holds if `t` for every valuation of the variables in `vars`.

exists_ :: [(Text, Sort)] -> Term -> Term Source #

`exists_ vars t` denotes a predicate that holds if `t` for some valuation of the variables in `vars`.

letBinder :: [(Text, Term)] -> Term -> Term Source #

Create a let binding. NOTE: SMTLib2 defines this to be a "parallel" let, which means that the bound variables are NOT in scope in the right-hand sides of other bindings, even syntactically-later ones.

# `Ints`, `Reals`, `Reals_Ints` theories

negate :: Term -> Term Source #

Negate an integer or real number.

numeral :: Integer -> Term Source #

Create a numeral literal from the given integer.

decimal :: Integer -> Term Source #

Create a literal as a real from the given integer.

sub :: Term -> [Term] -> Term Source #

`sub x1 [x2, ..., xn]` with n >= 1 returns `x1` minus `x2 + ... + xn`.

The terms are expected to have type `Int` or `Real`.

add :: [Term] -> Term Source #

`add [x1, x2, ..., xn]` with n >= 2 returns `x1` minus `x2 + ... + xn`.

The terms are expected to have type `Int` or `Real`.

mul :: [Term] -> Term Source #

`add [x1, x2, ..., xn]` with n >= 2 returns `x1` minus `x2 + ... + xn`.

The terms are expected to have type `Int` or `Real`.

div :: Term -> [Term] -> Term Source #

`div x1 [x2, ..., xn]` with n >= 1 returns `x1` div `x2 * ... * xn`.

The terms are expected to have type `Int`.

(./) :: Term -> [Term] -> Term Source #

`x1 ./ [x2, ..., xn]` with n >= 1 returns `x1` / `x2 * ... * xn`.

mod :: Term -> Term -> Term Source #

`mod x1 x2` returns x1 - x2 * (x1 `div` [x2])@.

The terms are expected to have type `Int`.

abs :: Term -> Term Source #

`abs x1` returns the absolute value of `x1`.

The term is expected to have type `Int`.

le :: [Term] -> Term Source #

Less than or equal over a chained list of terms.

`le [x1, x2, ..., xn]` is equivalent to `x1 <= x2 x2 <= x3 ... / x(n-1) <= xn`.

This is defined in the Reals, Ints, and Reals_Ints theories, and the number of elements must be at least 2.

With a strict interpretation of the SMTLIB standard, the terms should be all of the same type (i.e. Int or Real"), but existing solvers appear to implicitly all mixed terms.

lt :: [Term] -> Term Source #

Less than over a chained list of terms.

`lt [x1, x2, ..., xn]` is equivalent to `x1 < x2 x2 < x3 ... / x(n-1) < xn`.

With a strict interpretation of the SMTLIB standard, the terms should be all of the same type (i.e. Int or Real"), but existing solvers appear to implicitly all mixed terms.

ge :: [Term] -> Term Source #

Greater than or equal over a chained list of terms.

`ge [x1, x2, ..., xn]` is equivalent to `x1 >= x2 x2 >= x3 ... / x(n-1) >= xn`.

With a strict interpretation of the SMTLIB standard, the terms should be all of the same type (i.e. Int or Real"), but existing solvers appear to implicitly all mixed terms.

gt :: [Term] -> Term Source #

Greater than over a chained list of terms.

`gt [x1, x2, ..., xn]` is equivalent to `x1 > x2 x2 > x3 ... / x(n-1) > xn`.

With a strict interpretation of the SMTLIB standard, the terms should be all of the same type (i.e. Int or Real"), but existing solvers appear to implicitly all mixed terms.

toReal :: Term -> Term Source #

Maps a term with type `Int` to `Real`.

toInt :: Term -> Term Source #

Returns the largest integer not larger than the given real term.

isInt :: Term -> Term Source #

Returns true if this is an integer.

# Bitvector theory and extensions

concat :: Term -> Term -> Term Source #

`concat x y` returns the bitvector with the bits of `x` followed by the bits of `y`.

extract :: Natural -> Natural -> Term -> Term Source #

`extract i j x` returns the bitvector containing the bits `[j..i]`.

bvnot :: Term -> Term Source #

Bitwise negation of term.

bvand :: Term -> [Term] -> Term Source #

Bitwise and of all arguments.

bvor :: Term -> [Term] -> Term Source #

Bitwise include or of all arguments.

bvxor :: Term -> [Term] -> Term Source #

Bitvector exclusive or of all arguments.

bvneg :: Term -> Term Source #

Negate the bitvector

bvadd :: Term -> [Term] -> Term Source #

Bitvector addition

bvsub :: Term -> Term -> Term Source #

Bitvector subtraction

bvmul :: Term -> [Term] -> Term Source #

Bitvector multiplication

bvudiv :: Term -> Term -> Term Source #

`bvudiv x y` returns `floor (to_nat x / to_nat y)` when `y != 0`.

When `y = 0`, this returns `not (from_nat 0)`.

bvurem :: Term -> Term -> Term Source #

`bvurem x y` returns `x - y * bvudiv x y` when `y != 0`.

When `y = 0`, this returns `from_nat 0`.

bvshl :: Term -> Term -> Term Source #

`bvshl x y` shifts the bits in `x` to the left by `to_nat u` bits.

The new bits are zeros (false)

bvlshr :: Term -> Term -> Term Source #

`bvlshr x y` shifts the bits in `x` to the right by `to_nat u` bits.

The new bits are zeros (false)

bvult :: Term -> Term -> Term Source #

`bvult x y` returns a Boolean term that is true if `to_nat x < to_nat y`.

## Extensions provided by QF_BV

bit0 :: Term Source #

A 1-bit bitvector representing `0`.

bit1 :: Term Source #

A 1-bit bitvector representing `1`.

bvbinary :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> Term Source #

`bvbinary w x` constructs a bitvector term with width `w` equal to `x `mod` 2^w`.

The width `w` must be positive.

The literal uses a binary notation.

bvdecimal :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> Term Source #

`bvdecimal x w` constructs a bitvector term with width `w` equal to `x `mod` 2^w`.

The width `w` must be positive.

The literal uses a decimal notation.

bvhexadecimal :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> Term Source #

`bvhexadecimal x w` constructs a bitvector term with width `w` equal to `x `mod` 2^w`.

The width `w` must be a positive multiple of 4.

The literal uses hex notation.

bvashr :: Term -> Term -> Term Source #

`bvashr x y` shifts the bits in `x` to the right by `to_nat u` bits.

The new bits are the same as the most-significant bit of `x`.

Note. This is in `QF_BV`, but not the bitvector theory.

bvslt :: Term -> Term -> Term Source #

`bvslt x y` returns a Boolean term that is true if `to_int x < to_int y`.

Note. This is in `QF_BV`, but not the bitvector theory.

bvsle :: Term -> Term -> Term Source #

`bvsle x y` returns a Boolean term that is true if `to_int x <= to_int y`.

Note. This is in `QF_BV`, but not the bitvector theory.

bvule :: Term -> Term -> Term Source #

`bvule x y` returns a Boolean term that is true if `to_nat x <= to_nat y`.

Note. This is in `QF_BV`, but not the bitvector theory.

bvsgt :: Term -> Term -> Term Source #

`bvsgt x y` returns a Boolean term that is true if `to_int x < to_int y`.

Note. This is in `QF_BV`, but not the bitvector theory.

bvsge :: Term -> Term -> Term Source #

`bvsge x y` returns a Boolean term that is true if `to_int x <= to_int y`.

Note. This is in `QF_BV`, but not the bitvector theory.

bvugt :: Term -> Term -> Term Source #

`bvugt x y` returns a Boolean term that is true if `to_nat x < to_nat y`.

Note. This is in `QF_BV`, but not the bitvector theory.

bvuge :: Term -> Term -> Term Source #

`bvuge x y` returns a Boolean term that is true if `to_nat x <= to_nat y`.

Note. This is in `QF_BV`, but not the bitvector theory.

bvsdiv :: Term -> Term -> Term Source #

`bvsdiv x y` returns `round_to_zero (to_int x / to_int y)` when `y != 0`.

When `y = 0`, this returns `not (from_nat 0)`.

Note. This is in `QF_BV`, but not the bitvector theory.

bvsrem :: Term -> Term -> Term Source #

`bvsrem x y` returns `x - y * bvsdiv x y` when `y != 0`.

When `y = 0`, this returns `from_nat 0`.

Note. This is in `QF_BV`, but not the bitvector theory.

bvsignExtend :: Integer -> Term -> Term Source #

`bvsignExtend w x` adds an additional `w` bits to the most significant bits of `x` by sign extending `x`.

Note. This is in `QF_BV`, but not the bitvector theory.

bvzeroExtend :: Integer -> Term -> Term Source #

`bvzeroExtend w x` adds an additional `w` zero bits to the most significant bits of `x`.

Note. This is in `QF_BV`, but not the bitvector theory.

# Array theory

arraySort :: Sort -> Sort -> Sort Source #

`arraySort a b` denotes the set of functions from `a` to be `b`.

arrayConst :: Sort -> Sort -> Term -> Term Source #

`arrayConst t1 t2 c` generates an array with index type `t1` and value type `t2` that always returns `c`.

This uses the non-standard SMTLIB2 syntax `((as const (Array t1 t2)) c)` which is supported by CVC4, CVC5, and Z3 (and perhaps others).

select :: Term -> Term -> Term Source #

`select a i` denotes the value of `a` at `i`.

store :: Term -> Term -> Term -> Term Source #

`store a i v` denotes the array whose valuation is `v` at index `i` and `select a j` at every other index `j`.