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

Safe HaskellNone
LanguageHaskell2010

What4.Protocol.SMTLib2.Parse

Contents

Description

This module defines types and operations for parsing results from SMTLIB2.

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

CheckSatResponse

data CheckSatResponse Source #

Result of check-sat and check-sat-assuming

readCheckSatResponse :: Handle -> IO CheckSatResponse Source #

Read the results of a (check-sat) request.

GetModelResonse

type GetModelResponse = [ModelResponse] Source #

The parsed declarations and definitions returned by "(get-model)"

readGetModelResponse :: Handle -> IO GetModelResponse Source #

This reads the model response from a "(get-model)" request.

data ModelResponse Source #

A line in the model response

data DefineFun Source #

Constructors

DefineFun 

Fields

data Symbol Source #

An SMT symbol

Instances
Eq Symbol Source # 
Instance details

Defined in What4.Protocol.SMTLib2.Parse

Methods

(==) :: Symbol -> Symbol -> Bool #

(/=) :: Symbol -> Symbol -> Bool #

Show Symbol Source # 
Instance details

Defined in What4.Protocol.SMTLib2.Parse

IsString Symbol Source # 
Instance details

Defined in What4.Protocol.SMTLib2.Parse

Methods

fromString :: String -> Symbol #

Sorts

data Sort Source #

An SMT sort.

Constructors

Sort Symbol [Sort]

A named sort with the given arguments.

BitVec !Integer

A bitvector with the given width.

FloatingPoint !Integer !Integer

floating point with exponent bits followed by significand bit.

pattern Bool :: Sort Source #

pattern Int :: Sort Source #

pattern Real :: Sort Source #

pattern Array :: Sort -> Sort -> Sort Source #

Terms

data Term Source #

This denotes an SMTLIB term over a fixed vocabulary.

Constructors

SymbolTerm !Symbol 
AsConst !Sort !Term 
BVTerm !Integer !Integer 
IntTerm !Integer

IntTerm v denotes the SMTLIB expression v if v >= 0 and @(- `(negate v)) otherwise.

RatTerm !Rational

RatTerm r denotes the SMTLIB expression (/ `(numerator r) `(denomator r)).

StoreTerm !Term !Term !Term

StoreTerm a i v denotes the SMTLIB expression (store a i v).

IfEqTerm !Symbol !Term !Term !Term

IfEqTerm v c t f denotes the SMTLIB expression (ite (= v c) t f).