{-|
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.
-}

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module What4.Protocol.SMTLib2.Syntax
  ( -- * Commands
    Command(..)
  , setLogic
  , setOption
  , setProduceModels
  , SMTInfoFlag(..)
  , getInfo
  , getVersion
  , getName
  , getErrorBehavior
  , exit
     -- * Declarations
  , declareSort
  , defineSort
  , declareConst
  , declareFun
  , defineFun
  , Symbol
    -- * Assertions and checking
  , checkSat
  , checkSatAssuming
  , checkSatWithAssumptions
  , getModel
  , getValue
  , push
  , pop
  , resetAssertions
  , assert
  , assertNamed
  , getUnsatAssumptions
  , getUnsatCore
    -- * Logic
  , Logic(..)
  , qf_bv
  , allSupported
    -- * Sort
  , Sort(..)
  , boolSort
  , bvSort
  , intSort
  , realSort
  , varSort
    -- * Term
  , Term(..)
  , un_app
  , bin_app
  , term_app
  , pairwise_app
  , namedTerm
  , builder_list
    -- * Core theory
  , true
  , false
  , not
  , implies
  , and
  , or
  , xor
  , eq
  , distinct
  , ite
  , forall
  , exists
  , letBinder
    -- * @Ints@, @Reals@, @Reals_Ints@ theories
  , negate
  , numeral
  , decimal
  , sub
  , add
  , mul
  , div
  , (./)
  , mod
  , abs
  , le
  , lt
  , ge
  , gt
  , toReal
  , toInt
  , isInt
    -- * Bitvector theory and extensions
  , concat
  , extract
  , bvnot
  , bvand
  , bvor
  , bvxor
  , bvneg
  , bvadd
  , bvsub
  , bvmul
  , bvudiv
  , bvurem
  , bvshl
  , bvlshr
  , bvult
    -- ** Extensions provided by QF_BV
  , bit0
  , bit1
  , bvbinary
  , bvdecimal
  , bvhexadecimal
  , bvashr
  , bvslt
  , bvsle
  , bvule
  , bvsgt
  , bvsge
  , bvugt
  , bvuge
  , bvsdiv
  , bvsrem
  , bvsignExtend
  , bvzeroExtend
    -- * Array theory
  , arraySort
  , arrayConst
  , select
  , store
  ) where

import qualified Data.BitVector.Sized as BV
import           Data.Char (intToDigit)
import           Data.Parameterized.NatRepr
import           Data.String
import           Data.Text (Text, cons)
import           Data.Text.Lazy.Builder (Builder)
import qualified Data.Text.Lazy.Builder as Builder
import qualified Data.Text.Lazy.Builder.Int as Builder
import           Numeric.Natural

import           GHC.Generics (Generic)
import           Data.Data (Data)
import           Data.Typeable (Typeable)

import qualified Prelude
import           Prelude hiding (and, or, concat, negate, div, mod, abs, not)

app_list :: Builder -> [Builder] -> Builder
app_list :: Builder -> [Builder] -> Builder
app_list Builder
o [Builder]
args = Builder
"(" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
o Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> [Builder] -> Builder
forall p. (IsString p, Semigroup p) => [p] -> p
go [Builder]
args
  where go :: [p] -> p
go [] = p
")"
        go (p
f:[p]
r) = p
" " p -> p -> p
forall a. Semigroup a => a -> a -> a
<> p
f p -> p -> p
forall a. Semigroup a => a -> a -> a
<> [p] -> p
go [p]
r

app :: Builder -> [Builder] -> Builder
app :: Builder -> [Builder] -> Builder
app Builder
o [] = Builder
o
app Builder
o [Builder]
args = Builder -> [Builder] -> Builder
app_list Builder
o [Builder]
args

builder_list :: [Builder] -> Builder
builder_list :: [Builder] -> Builder
builder_list [] = Builder
"()"
builder_list (Builder
h:[Builder]
l) = Builder -> [Builder] -> Builder
app_list Builder
h [Builder]
l

------------------------------------------------------------------------
-- Logic

-- | Identifies the set of predefined sorts and operators available.
newtype Logic = Logic Builder

-- | Use the QF_BV logic
qf_bv :: Logic
qf_bv :: Logic
qf_bv = Builder -> Logic
Logic Builder
"QF_BV"

-- | Set the logic to all supported logics.
allSupported :: Logic
allSupported :: Logic
allSupported = Builder -> Logic
Logic Builder
"ALL_SUPPORTED"

------------------------------------------------------------------------
-- Symbol

type Symbol = Text

------------------------------------------------------------------------
-- Sort

-- | Sort for SMTLIB expressions
newtype Sort = Sort { Sort -> Builder
unSort :: Builder }

-- | Create a sort from a symbol name
varSort :: Symbol -> Sort
varSort :: Symbol -> Sort
varSort = Builder -> Sort
Sort (Builder -> Sort) -> (Symbol -> Builder) -> Symbol -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Builder
Builder.fromText

-- | Booleans
boolSort :: Sort
boolSort :: Sort
boolSort = Builder -> Sort
Sort Builder
"Bool"

-- | Bitvectors with the given number of bits.
bvSort :: Natural -> Sort
bvSort :: Natural -> Sort
bvSort Natural
w | Natural
w Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
>= Natural
1 = Builder -> Sort
Sort (Builder -> Sort) -> Builder -> Sort
forall a b. (a -> b) -> a -> b
$ Builder
"(_ BitVec " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> String -> Builder
forall a. IsString a => String -> a
fromString (Natural -> String
forall a. Show a => a -> String
show Natural
w) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
         | Bool
otherwise = String -> Sort
forall a. HasCallStack => String -> a
error String
"bvSort expects a positive number."

-- | Integers
intSort :: Sort
intSort :: Sort
intSort = Builder -> Sort
Sort Builder
"Int"

-- | Real numbers
realSort :: Sort
realSort :: Sort
realSort = Builder -> Sort
Sort Builder
"Real"

-- | @arraySort a b@ denotes the set of functions from @a@ to be @b@.
arraySort :: Sort -> Sort -> Sort
arraySort :: Sort -> Sort -> Sort
arraySort (Sort Builder
i) (Sort Builder
v) = Builder -> Sort
Sort (Builder -> Sort) -> Builder -> Sort
forall a b. (a -> b) -> a -> b
$ Builder
"(Array " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
i Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
v Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"

------------------------------------------------------------------------
-- Term

-- | Denotes an expression in the SMT solver
newtype Term = T { Term -> Builder
renderTerm :: Builder }
  deriving (String -> Term
(String -> Term) -> IsString Term
forall a. (String -> a) -> IsString a
fromString :: String -> Term
$cfromString :: String -> Term
IsString, Semigroup Term
Term
Semigroup Term
-> Term
-> (Term -> Term -> Term)
-> ([Term] -> Term)
-> Monoid Term
[Term] -> Term
Term -> Term -> Term
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
mconcat :: [Term] -> Term
$cmconcat :: [Term] -> Term
mappend :: Term -> Term -> Term
$cmappend :: Term -> Term -> Term
mempty :: Term
$cmempty :: Term
$cp1Monoid :: Semigroup Term
Monoid, b -> Term -> Term
NonEmpty Term -> Term
Term -> Term -> Term
(Term -> Term -> Term)
-> (NonEmpty Term -> Term)
-> (forall b. Integral b => b -> Term -> Term)
-> Semigroup Term
forall b. Integral b => b -> Term -> Term
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
stimes :: b -> Term -> Term
$cstimes :: forall b. Integral b => b -> Term -> Term
sconcat :: NonEmpty Term -> Term
$csconcat :: NonEmpty Term -> Term
<> :: Term -> Term -> Term
$c<> :: Term -> Term -> Term
Semigroup)

-- | Construct an expression with the given operator and list of arguments.
term_app :: Builder -> [Term] -> Term
term_app :: Builder -> [Term] -> Term
term_app Builder
o [Term]
args = Builder -> Term
T (Builder -> [Builder] -> Builder
app Builder
o (Term -> Builder
renderTerm (Term -> Builder) -> [Term] -> [Builder]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term]
args))

-- | Construct an expression with the given operator and single argument.
un_app :: Builder -> Term -> Term
un_app :: Builder -> Term -> Term
un_app Builder
o (T Builder
x) = Builder -> Term
T (Builder -> Term) -> Builder -> Term
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat [Builder
"(", Builder
o, Builder
" ", Builder
x, Builder
")"]

-- | Construct an expression with the given operator and two arguments.
bin_app :: Builder -> Term -> Term -> Term
bin_app :: Builder -> Term -> Term -> Term
bin_app Builder
o (T Builder
x) (T Builder
y) = Builder -> Term
T (Builder -> Term) -> Builder -> Term
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat [Builder
"(", Builder
o, Builder
" ", Builder
x, Builder
" ", Builder
y, Builder
")"]

-- | Construct a chainable term with the given relation
--
-- @chain_app p [x1, x2, ..., xn]@ is equivalent to
-- @p x1 x2 /\ p x2 x3 /\ ... /\ p x(n-1) xn@.
chain_app :: Builder -> [Term] -> Term
chain_app :: Builder -> [Term] -> Term
chain_app Builder
f l :: [Term]
l@(Term
_:Term
_:[Term]
_) = Builder -> [Term] -> Term
term_app Builder
f [Term]
l
chain_app Builder
f [Term]
_ = String -> Term
forall a. HasCallStack => String -> a
error (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ Builder -> String
forall a. Show a => a -> String
show Builder
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" expects two or more arguments."

-- | Build a term for a left-associative operator.
assoc_app :: Builder -> Term -> [Term] -> Term
assoc_app :: Builder -> Term -> [Term] -> Term
assoc_app Builder
_ Term
t [] = Term
t
assoc_app Builder
f Term
t [Term]
l = Builder -> [Term] -> Term
term_app Builder
f (Term
tTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[Term]
l)

-- | Append a "name" to a term so that it will be printed when
-- @(get-assignment)@ is called.
namedTerm :: Term -> Text -> Term
namedTerm :: Term -> Symbol -> Term
namedTerm (T Builder
x) Symbol
nm = Builder -> Term
T (Builder -> Term) -> Builder -> Term
forall a b. (a -> b) -> a -> b
$ Builder
"(! " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
x Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" :named " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Symbol -> Builder
Builder.fromText Symbol
nm Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"

------------------------------------------------------------------------
-- Core theory

-- | @true@ Boolean term
true :: Term
true :: Term
true = Builder -> Term
T Builder
"true"

-- | @false@ Boolean term
false :: Term
false :: Term
false = Builder -> Term
T Builder
"false"

-- | Complement a Boolean
not :: Term -> Term
not :: Term -> Term
not = Builder -> Term -> Term
un_app Builder
"not"

-- | @implies c r@ is equivalent to @c1 => c2 => .. cn => r@.
implies :: [Term] -> Term -> Term
implies :: [Term] -> Term -> Term
implies [] Term
t = Term
t
implies [Term]
l Term
t = Builder -> [Term] -> Term
term_app Builder
"=>" ([Term]
l [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term
t])

-- | Conjunction of all terms
and :: [Term] -> Term
and :: [Term] -> Term
and [] = Term
true
and [Term
x] = Term
x
and [Term]
l = Builder -> [Term] -> Term
term_app Builder
"and" [Term]
l

-- | Disjunction of all terms
or :: [Term] -> Term
or :: [Term] -> Term
or [] = Term
true
or [Term
x] = Term
x
or [Term]
l = Builder -> [Term] -> Term
term_app Builder
"or" [Term]
l

-- | Disjunction of all terms
xor :: [Term] -> Term
xor :: [Term] -> Term
xor l :: [Term]
l@(Term
_:Term
_:[Term]
_) = Builder -> [Term] -> Term
term_app Builder
"xor" [Term]
l
xor [Term]
_ = String -> Term
forall a. HasCallStack => String -> a
error String
"xor expects two or more arguments."

-- | Return true if all terms are equal.
eq :: [Term] -> Term
eq :: [Term] -> Term
eq = Builder -> [Term] -> Term
chain_app Builder
"="

-- | Construct a chainable term with the givne relation
--
-- @pairwise_app p [x1, x2, ..., xn]@ is equivalent to
-- \forall_{i,j} p x_i x_j@.
pairwise_app :: Builder -> [Term] -> Term
pairwise_app :: Builder -> [Term] -> Term
pairwise_app Builder
_ [] = Term
true
pairwise_app Builder
_ [Term
_] = Term
true
pairwise_app Builder
f l :: [Term]
l@(Term
_:Term
_:[Term]
_) = Builder -> [Term] -> Term
term_app Builder
f [Term]
l

-- | Asserts that each term in the list is unique.
distinct :: [Term] -> Term
distinct :: [Term] -> Term
distinct = Builder -> [Term] -> Term
pairwise_app Builder
"distinct"

-- | Create an if-then-else expression.
ite :: Term -> Term -> Term -> Term
ite :: Term -> Term -> Term -> Term
ite Term
c Term
x Term
y = Builder -> [Term] -> Term
term_app Builder
"ite" [Term
c, Term
x, Term
y]

varBinding :: (Text,Sort) -> Builder
varBinding :: (Symbol, Sort) -> Builder
varBinding (Symbol
nm, Sort
tp) = Builder
"(" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Symbol -> Builder
Builder.fromText Symbol
nm Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Sort -> Builder
unSort Sort
tp Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"

-- | @forall vars t@ denotes a predicate that holds if @t@ for every valuation of the
-- variables in @vars@.
forall :: [(Text, Sort)] -> Term -> Term
forall :: [(Symbol, Sort)] -> Term -> Term
forall [] Term
r = Term
r
forall [(Symbol, Sort)]
vars Term
r =
  Builder -> Term
T (Builder -> Term) -> Builder -> Term
forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"forall" [[Builder] -> Builder
builder_list ((Symbol, Sort) -> Builder
varBinding ((Symbol, Sort) -> Builder) -> [(Symbol, Sort)] -> [Builder]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
vars), Term -> Builder
renderTerm Term
r]

-- | @exists vars t@ denotes a predicate that holds if @t@ for some valuation of the
-- variables in @vars@.
exists :: [(Text, Sort)] -> Term -> Term
exists :: [(Symbol, Sort)] -> Term -> Term
exists [] Term
r = Term
r
exists [(Symbol, Sort)]
vars Term
r =
  Builder -> Term
T (Builder -> Term) -> Builder -> Term
forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"exists" [[Builder] -> Builder
builder_list ((Symbol, Sort) -> Builder
varBinding ((Symbol, Sort) -> Builder) -> [(Symbol, Sort)] -> [Builder]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
vars), Term -> Builder
renderTerm Term
r]

letBinding :: (Text, Term) -> Builder
letBinding :: (Symbol, Term) -> Builder
letBinding (Symbol
nm, Term
t) = Builder -> [Builder] -> Builder
app_list (Symbol -> Builder
Builder.fromText Symbol
nm) [Term -> Builder
renderTerm Term
t]

-- | 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.
letBinder :: [(Text, Term)] -> Term -> Term
letBinder :: [(Symbol, Term)] -> Term -> Term
letBinder [] Term
r = Term
r
letBinder [(Symbol, Term)]
vars Term
r =
  Builder -> Term
T (Builder -> [Builder] -> Builder
app Builder
"let" [[Builder] -> Builder
builder_list ((Symbol, Term) -> Builder
letBinding ((Symbol, Term) -> Builder) -> [(Symbol, Term)] -> [Builder]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Term)]
vars), Term -> Builder
renderTerm Term
r])

------------------------------------------------------------------------
-- Reals/Int/Real_Ints theories

-- | Negate an integer or real number.
negate :: Term -> Term
negate :: Term -> Term
negate = Builder -> Term -> Term
un_app Builder
"-"

-- | Create a numeral literal from the given integer.
numeral :: Integer -> Term
numeral :: Integer -> Term
numeral Integer
i | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 = Builder -> Term
T (Builder -> Term) -> Builder -> Term
forall a b. (a -> b) -> a -> b
$ Integer -> Builder
forall a. Integral a => a -> Builder
Builder.decimal Integer
i
          | Bool
otherwise = Term -> Term
negate (Builder -> Term
T (Integer -> Builder
forall a. Integral a => a -> Builder
Builder.decimal (Integer -> Integer
forall a. Num a => a -> a
Prelude.negate Integer
i)))

-- | Create a literal as a real from the given integer.
decimal :: Integer -> Term
decimal :: Integer -> Term
decimal Integer
i | Integer
i Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 = Builder -> Term
T (Builder -> Term) -> Builder -> Term
forall a b. (a -> b) -> a -> b
$ Integer -> Builder
forall a. Integral a => a -> Builder
Builder.decimal Integer
i Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
".0"
          | Bool
otherwise = Term -> Term
negate (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Builder -> Term
T (Builder -> Term) -> Builder -> Term
forall a b. (a -> b) -> a -> b
$ Integer -> Builder
forall a. Integral a => a -> Builder
Builder.decimal (Integer -> Integer
forall a. Num a => a -> a
Prelude.negate Integer
i) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
".0"

-- | @sub x1 [x2, ..., xn]@ with n >= 1 returns
-- @x1@ minus @x2 + ... + xn@.
--
-- The terms are expected to have type @Int@ or @Real@.
sub :: Term -> [Term] -> Term
sub :: Term -> [Term] -> Term
sub Term
x [] = Term
x
sub Term
x [Term]
l = Builder -> [Term] -> Term
term_app Builder
"-" (Term
xTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[Term]
l)

-- | @add [x1, x2, ..., xn]@ with n >= 2 returns
-- @x1@ minus @x2 + ... + xn@.
--
-- The terms are expected to have type @Int@ or @Real@.
add :: [Term] -> Term
add :: [Term] -> Term
add [] = Builder -> Term
T Builder
"0"
add [Term
x] = Term
x
add [Term]
l = Builder -> [Term] -> Term
term_app Builder
"+" [Term]
l

-- | @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
mul :: [Term] -> Term
mul [] = Builder -> Term
T Builder
"1"
mul [Term
x] = Term
x
mul [Term]
l = Builder -> [Term] -> Term
term_app Builder
"*" [Term]
l

-- | @div x1 [x2, ..., xn]@ with n >= 1 returns
-- @x1@ div @x2 * ... * xn@.
--
-- The terms are expected to have type @Int@.
div :: Term -> [Term] -> Term
div :: Term -> [Term] -> Term
div Term
x [] = Term
x
div Term
x [Term]
l = Builder -> [Term] -> Term
term_app Builder
"div" (Term
xTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[Term]
l)

-- | @x1 ./ [x2, ..., xn]@ with n >= 1 returns
-- @x1@ / @x2 * ... * xn@.
(./) :: Term -> [Term] -> Term
Term
x ./ :: Term -> [Term] -> Term
./ [] = Term
x
Term
x ./ [Term]
l = Builder -> [Term] -> Term
term_app Builder
"/" (Term
xTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[Term]
l)

-- | @mod x1 x2@ returns x1 - x2 * (x1 `div` [x2])@.
--
-- The terms are expected to have type @Int@.
mod :: Term -> Term -> Term
mod :: Term -> Term -> Term
mod = Builder -> Term -> Term -> Term
bin_app Builder
"mod"

-- | @abs x1@ returns the absolute value of @x1@.
--
-- The term is expected to have type @Int@.
abs :: Term -> Term
abs :: Term -> Term
abs = Builder -> Term -> Term
un_app Builder
"abs"

-- | 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.
le :: [Term] -> Term
le :: [Term] -> Term
le = Builder -> [Term] -> Term
chain_app Builder
"<="

-- | 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.
lt :: [Term] -> Term
lt :: [Term] -> Term
lt = Builder -> [Term] -> Term
chain_app Builder
"<"

-- | 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.
ge :: [Term] -> Term
ge :: [Term] -> Term
ge = Builder -> [Term] -> Term
chain_app Builder
">="

-- | 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.
gt :: [Term] -> Term
gt :: [Term] -> Term
gt = Builder -> [Term] -> Term
chain_app Builder
">"

-- | Maps a term with type @Int@ to @Real@.
toReal :: Term -> Term
toReal :: Term -> Term
toReal = Builder -> Term -> Term
un_app Builder
"to_real"

-- | Returns the largest integer not larger than the given real term.
toInt :: Term -> Term
toInt :: Term -> Term
toInt = Builder -> Term -> Term
un_app Builder
"to_int"

-- | Returns true if this is an integer.
isInt :: Term -> Term
isInt :: Term -> Term
isInt = Builder -> Term -> Term
un_app Builder
"is_int"

------------------------------------------------------------------------
-- Array theory

-- | @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 and Z3
-- (and perhaps others).
arrayConst :: Sort -> Sort -> Term -> Term
arrayConst :: Sort -> Sort -> Term -> Term
arrayConst Sort
itp Sort
rtp Term
c =
  let tp :: Sort
tp = Sort -> Sort -> Sort
arraySort Sort
itp Sort
rtp
      cast_app :: Builder
cast_app = [Builder] -> Builder
builder_list [ Builder
"as" , Builder
"const" , Sort -> Builder
unSort Sort
tp ]
   in Builder -> [Term] -> Term
term_app Builder
cast_app [ Term
c ]

-- | @select a i@ denotes the value of @a@ at @i@.
select :: Term -> Term -> Term
select :: Term -> Term -> Term
select = Builder -> Term -> Term -> Term
bin_app Builder
"select"

-- | @store a i v@ denotes the array whose valuation is @v@ at index @i@ and
-- @select a j@ at every other index @j@.
store :: Term -> Term -> Term -> Term
store :: Term -> Term -> Term -> Term
store Term
a Term
i Term
v = Builder -> [Term] -> Term
term_app Builder
"store" [Term
a,Term
i,Term
v]

------------------------------------------------------------------------
-- Bitvector theory

-- | A 1-bit bitvector representing @0@.
bit0 :: Term
bit0 :: Term
bit0 = Builder -> Term
T Builder
"#b0"

-- | A 1-bit bitvector representing @1@.
bit1 :: Term
bit1 :: Term
bit1 = Builder -> Term
T Builder
"#b1"

-- | @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.
bvbinary :: 1 <= w => NatRepr w -> BV.BV w -> Term
bvbinary :: NatRepr w -> BV w -> Term
bvbinary NatRepr w
w0 BV w
u
    | Bool
otherwise = Builder -> Term
T (Builder -> Term) -> Builder -> Term
forall a b. (a -> b) -> a -> b
$ Builder
"#b" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Natural -> Builder
go (NatRepr w -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr w
w0)
  where go :: Natural -> Builder
        go :: Natural -> Builder
go Natural
0 = Builder
forall a. Monoid a => a
mempty
        go Natural
w =
          let i :: Natural
i = Natural
w Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1
              b :: Builder
              b :: Builder
b = if Natural -> BV w -> Bool
forall (w :: Nat). Natural -> BV w -> Bool
BV.testBit' Natural
i BV w
u then Builder
"1" else Builder
"0"
           in Builder
b Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Natural -> Builder
go Natural
i

-- | @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.
bvdecimal :: 1 <= w => NatRepr w -> BV.BV w -> Term
bvdecimal :: NatRepr w -> BV w -> Term
bvdecimal NatRepr w
w BV w
u = Builder -> Term
T (Builder -> Term) -> Builder -> Term
forall a b. (a -> b) -> a -> b
$ [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat [ Builder
"(_ bv"
                            , Integer -> Builder
forall a. Integral a => a -> Builder
Builder.decimal Integer
d
                            , Builder
" "
                            , Natural -> Builder
forall a. Integral a => a -> Builder
Builder.decimal (NatRepr w -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr w
w)
                            , Builder
")"]
  where d :: Integer
d = BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned BV w
u

-- | @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.
bvhexadecimal :: 1 <= w => NatRepr w -> BV.BV w -> Term
bvhexadecimal :: NatRepr w -> BV w -> Term
bvhexadecimal NatRepr w
w0 BV w
u
    | Bool
otherwise = Builder -> Term
T (Builder -> Term) -> Builder -> Term
forall a b. (a -> b) -> a -> b
$ Builder
"#x" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Natural -> Builder
go (NatRepr w -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue NatRepr w
w0)
  where go :: Natural -> Builder
        go :: Natural -> Builder
go Natural
0 = Builder
forall a. Monoid a => a
mempty
        go Natural
w | Natural
w Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< Natural
4 = String -> Builder
forall a. HasCallStack => String -> a
error String
"bvhexadecimal width must be a multiple of 4."
        go Natural
w =
          let i :: Natural
i = Natural
w Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
4
              charBits :: Integer
charBits = BV 4 -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned (Natural -> NatRepr 4 -> BV w -> BV 4
forall (w' :: Nat) (w :: Nat).
Natural -> NatRepr w' -> BV w -> BV w'
BV.select' Natural
i (KnownNat 4 => NatRepr 4
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @4) BV w
u)
              c :: Char
              c :: Char
c = Int -> Char
intToDigit (Int -> Char) -> Int -> Char
forall a b. (a -> b) -> a -> b
$ Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
charBits
           in Char -> Builder
Builder.singleton Char
c Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Natural -> Builder
go Natural
i

-- | @concat x y@ returns the bitvector with the bits of @x@ followed by the bits of @y@.
concat :: Term -> Term -> Term
concat :: Term -> Term -> Term
concat = Builder -> Term -> Term -> Term
bin_app Builder
"concat"

-- | @extract i j x@ returns the bitvector containing the bits @[j..i]@.
extract :: Natural -> Natural -> Term -> Term
extract :: Natural -> Natural -> Term -> Term
extract Natural
i Natural
j Term
x
  | Natural
i Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< Natural
j = String -> Term
forall a. HasCallStack => String -> a
error (String -> Term) -> String -> Term
forall a b. (a -> b) -> a -> b
$ String
"End of extract (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show Natural
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") less than beginning (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Natural -> String
forall a. Show a => a -> String
show Natural
j String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")."
  | Bool
otherwise = -- We cannot check that j is small enough.
    let e :: Builder
e = Builder
"(_ extract " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Natural -> Builder
forall a. Integral a => a -> Builder
Builder.decimal Natural
i Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Natural -> Builder
forall a. Integral a => a -> Builder
Builder.decimal Natural
j Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
     in Builder -> Term -> Term
un_app Builder
e Term
x

-- | Bitwise negation of term.
bvnot :: Term -> Term
bvnot :: Term -> Term
bvnot = Builder -> Term -> Term
un_app Builder
"bvnot"

-- | Bitwise and of all arguments.
bvand :: Term -> [Term] -> Term
bvand :: Term -> [Term] -> Term
bvand = Builder -> Term -> [Term] -> Term
assoc_app Builder
"bvand"

-- | Bitwise include or of all arguments.
bvor :: Term -> [Term] -> Term
bvor :: Term -> [Term] -> Term
bvor = Builder -> Term -> [Term] -> Term
assoc_app Builder
"bvor"

-- | Bitvector exclusive or of all arguments.
bvxor :: Term -> [Term] -> Term
bvxor :: Term -> [Term] -> Term
bvxor = Builder -> Term -> [Term] -> Term
assoc_app Builder
"bvxor"

-- | Negate the bitvector
bvneg :: Term -> Term
bvneg :: Term -> Term
bvneg = Builder -> Term -> Term
un_app Builder
"bvneg"

-- | Bitvector addition
bvadd :: Term -> [Term] -> Term
bvadd :: Term -> [Term] -> Term
bvadd = Builder -> Term -> [Term] -> Term
assoc_app Builder
"bvadd"

-- | Bitvector subtraction
bvsub :: Term -> Term -> Term
bvsub :: Term -> Term -> Term
bvsub = Builder -> Term -> Term -> Term
bin_app Builder
"bvsub"

-- | Bitvector multiplication
bvmul :: Term -> [Term] -> Term
bvmul :: Term -> [Term] -> Term
bvmul = Builder -> Term -> [Term] -> Term
assoc_app Builder
"bvmul"

-- | @bvudiv x y@ returns @floor (to_nat x / to_nat y)@ when @y != 0@.
--
-- When @y = 0@, this returns @not (from_nat 0)@.
bvudiv :: Term -> Term -> Term
bvudiv :: Term -> Term -> Term
bvudiv = Builder -> Term -> Term -> Term
bin_app Builder
"bvudiv"

-- | @bvurem x y@ returns @x - y * bvudiv x y@ when @y != 0@.
--
-- When @y = 0@, this returns @from_nat 0@.
bvurem :: Term -> Term -> Term
bvurem :: Term -> Term -> Term
bvurem = Builder -> Term -> Term -> Term
bin_app Builder
"bvurem"

-- | @bvshl x y@ shifts the bits in @x@ to the left by @to_nat u@ bits.
--
-- The new bits are zeros (false)
bvshl :: Term -> Term -> Term
bvshl :: Term -> Term -> Term
bvshl = Builder -> Term -> Term -> Term
bin_app Builder
"bvshl"

-- | @bvlshr x y@ shifts the bits in @x@ to the right by @to_nat u@ bits.
--
-- The new bits are zeros (false)
bvlshr :: Term -> Term -> Term
bvlshr :: Term -> Term -> Term
bvlshr = Builder -> Term -> Term -> Term
bin_app Builder
"bvlshr"

-- | @bvult x y@ returns a Boolean term that is true if @to_nat x < to_nat y@.
bvult :: Term -> Term -> Term
bvult :: Term -> Term -> Term
bvult = Builder -> Term -> Term -> Term
bin_app Builder
"bvult"

-- | @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.
bvule :: Term -> Term -> Term
bvule :: Term -> Term -> Term
bvule = Builder -> Term -> Term -> Term
bin_app Builder
"bvule"

-- | @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.
bvsle :: Term -> Term -> Term
bvsle :: Term -> Term -> Term
bvsle = Builder -> Term -> Term -> Term
bin_app Builder
"bvsle"

-- | @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.
bvslt :: Term -> Term -> Term
bvslt :: Term -> Term -> Term
bvslt = Builder -> Term -> Term -> Term
bin_app Builder
"bvslt"

-- | @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.
bvuge :: Term -> Term -> Term
bvuge :: Term -> Term -> Term
bvuge = Builder -> Term -> Term -> Term
bin_app Builder
"bvuge"

-- | @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.
bvugt :: Term -> Term -> Term
bvugt :: Term -> Term -> Term
bvugt = Builder -> Term -> Term -> Term
bin_app Builder
"bvugt"

-- | @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.
bvsge :: Term -> Term -> Term
bvsge :: Term -> Term -> Term
bvsge = Builder -> Term -> Term -> Term
bin_app Builder
"bvsge"

-- | @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.
bvsgt :: Term -> Term -> Term
bvsgt :: Term -> Term -> Term
bvsgt = Builder -> Term -> Term -> Term
bin_app Builder
"bvsgt"

-- | @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.
bvashr :: Term -> Term -> Term
bvashr :: Term -> Term -> Term
bvashr = Builder -> Term -> Term -> Term
bin_app Builder
"bvashr"

-- | @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.
bvsdiv :: Term -> Term -> Term
bvsdiv :: Term -> Term -> Term
bvsdiv = Builder -> Term -> Term -> Term
bin_app Builder
"bvsdiv"

-- | @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.
bvsrem :: Term -> Term -> Term
bvsrem :: Term -> Term -> Term
bvsrem = Builder -> Term -> Term -> Term
bin_app Builder
"bvsrem"

-- | @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.
bvsignExtend :: Integer -> Term -> Term
bvsignExtend :: Integer -> Term -> Term
bvsignExtend Integer
w Term
x =
  let e :: Builder
e = Builder
"(_ sign_extend " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
forall a. Integral a => a -> Builder
Builder.decimal Integer
w Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
   in Builder -> Term -> Term
un_app Builder
e Term
x

-- | @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.
bvzeroExtend :: Integer -> Term -> Term
bvzeroExtend :: Integer -> Term -> Term
bvzeroExtend Integer
w Term
x =
  let e :: Builder
e = Builder
"(_ zero_extend " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
forall a. Integral a => a -> Builder
Builder.decimal Integer
w Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
   in Builder -> Term -> Term
un_app Builder
e Term
x

------------------------------------------------------------------------
-- Command

-- | This represents a command to be sent to the SMT solver.
newtype Command = Cmd Builder

-- | Set the logic of the SMT solver
setLogic :: Logic -> Command
setLogic :: Logic -> Command
setLogic (Logic Builder
nm) = Builder -> Command
Cmd (Builder -> Command) -> Builder -> Command
forall a b. (a -> b) -> a -> b
$ Builder
"(set-logic " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
nm Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"

-- | Set an option in the SMT solver
--
-- The name should not need to be prefixed with a colon."
setOption :: Text -> Text -> Command
setOption :: Symbol -> Symbol -> Command
setOption Symbol
nm Symbol
val = Builder -> Command
Cmd (Builder -> Command) -> Builder -> Command
forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app_list Builder
"set-option" [Builder
":" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Symbol -> Builder
Builder.fromText Symbol
nm, Symbol -> Builder
Builder.fromText Symbol
val]

ppBool :: Bool -> Text
ppBool :: Bool -> Symbol
ppBool Bool
b = if Bool
b then Symbol
"true" else Symbol
"false"

-- | Set option to produce models
--
-- This is a widely used option so, we we have a custom command to
-- make it.
setProduceModels :: Bool -> Command
setProduceModels :: Bool -> Command
setProduceModels Bool
b = Symbol -> Symbol -> Command
setOption Symbol
"produce-models" (Bool -> Symbol
ppBool Bool
b)

-- | Request the SMT solver to exit
exit :: Command
exit :: Command
exit = Builder -> Command
Cmd Builder
"(exit)"

-- | Declare an uninterpreted sort with the given number of sort parameters.
declareSort :: Symbol -> Integer -> Command
declareSort :: Symbol -> Integer -> Command
declareSort Symbol
v Integer
n = Builder -> Command
Cmd (Builder -> Command) -> Builder -> Command
forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"declare-sort" [Symbol -> Builder
Builder.fromText Symbol
v, String -> Builder
forall a. IsString a => String -> a
fromString (Integer -> String
forall a. Show a => a -> String
show Integer
n)]

-- | Define a sort in terms of other sorts
--
defineSort :: Symbol -- ^ Name of new sort
           -> [Symbol] -- ^ Parameters for polymorphic sorts
           -> Sort -- ^ Definition
           -> Command
defineSort :: Symbol -> [Symbol] -> Sort -> Command
defineSort Symbol
v [Symbol]
params Sort
d =
  Builder -> Command
Cmd (Builder -> Command) -> Builder -> Command
forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"define-sort" [ Symbol -> Builder
Builder.fromText Symbol
v
                          , [Builder] -> Builder
builder_list (Symbol -> Builder
Builder.fromText (Symbol -> Builder) -> [Symbol] -> [Builder]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Symbol]
params)
                          , Sort -> Builder
unSort Sort
d
                          ]

-- | Declare a constant with the given name and return types.
declareConst :: Text -> Sort -> Command
declareConst :: Symbol -> Sort -> Command
declareConst Symbol
v Sort
tp = Builder -> Command
Cmd (Builder -> Command) -> Builder -> Command
forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"declare-const" [Symbol -> Builder
Builder.fromText Symbol
v, Sort -> Builder
unSort Sort
tp]

-- | Declare a function with the given name, argument types, and
-- return type.
declareFun :: Text -> [Sort] -> Sort -> Command
declareFun :: Symbol -> [Sort] -> Sort -> Command
declareFun Symbol
v [Sort]
argSorts Sort
retSort = Builder -> Command
Cmd (Builder -> Command) -> Builder -> Command
forall a b. (a -> b) -> a -> b
$
  Builder -> [Builder] -> Builder
app Builder
"declare-fun" [ Symbol -> Builder
Builder.fromText Symbol
v
                    , [Builder] -> Builder
builder_list ([Builder] -> Builder) -> [Builder] -> Builder
forall a b. (a -> b) -> a -> b
$ Sort -> Builder
unSort (Sort -> Builder) -> [Sort] -> [Builder]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Sort]
argSorts
                    , Sort -> Builder
unSort Sort
retSort
                    ]

-- | Declare a function with the given name, argument types, and
-- return type.
defineFun :: Text -> [(Text,Sort)] -> Sort -> Term -> Command
defineFun :: Symbol -> [(Symbol, Sort)] -> Sort -> Term -> Command
defineFun Symbol
f [(Symbol, Sort)]
args Sort
return_type Term
e =
  let resolveArg :: (Symbol, Sort) -> Builder
resolveArg (Symbol
var, Sort
tp) = Builder -> [Builder] -> Builder
app (Symbol -> Builder
Builder.fromText Symbol
var) [Sort -> Builder
unSort Sort
tp]
   in Builder -> Command
Cmd (Builder -> Command) -> Builder -> Command
forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"define-fun" [ Symbol -> Builder
Builder.fromText Symbol
f
                             , [Builder] -> Builder
builder_list ((Symbol, Sort) -> Builder
resolveArg ((Symbol, Sort) -> Builder) -> [(Symbol, Sort)] -> [Builder]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
args)
                             , Sort -> Builder
unSort Sort
return_type
                             , Term -> Builder
renderTerm Term
e
                             ]

-- | Assert the predicate holds in the current context.
assert :: Term -> Command
assert :: Term -> Command
assert Term
p = Builder -> Command
Cmd (Builder -> Command) -> Builder -> Command
forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"assert" [Term -> Builder
renderTerm Term
p]

-- | Assert the predicate holds in the current context, and assign
--   it a name so it can appear in unsatisfiable core results.
assertNamed :: Term -> Text -> Command
assertNamed :: Term -> Symbol -> Command
assertNamed Term
p Symbol
nm =
  Builder -> Command
Cmd (Builder -> Command) -> Builder -> Command
forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"assert"
    [[Builder] -> Builder
builder_list [Symbol -> Builder
Builder.fromText Symbol
"!", Term -> Builder
renderTerm Term
p, Symbol -> Builder
Builder.fromText Symbol
":named", Symbol -> Builder
Builder.fromText Symbol
nm]]

-- | Check the satisfiability of the current assertions
checkSat :: Command
checkSat :: Command
checkSat = Builder -> Command
Cmd Builder
"(check-sat)"

-- | Check the satisfiability of the current assertions and the additional ones in the list.
checkSatAssuming :: [Term] -> Command
checkSatAssuming :: [Term] -> Command
checkSatAssuming [Term]
l = Builder -> Command
Cmd (Builder -> Command) -> Builder -> Command
forall a b. (a -> b) -> a -> b
$ Builder
"(check-sat-assuming " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> [Builder] -> Builder
builder_list (Term -> Builder
renderTerm (Term -> Builder) -> [Term] -> [Builder]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term]
l) Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"

-- | 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.
checkSatWithAssumptions :: [Text] -> Command
checkSatWithAssumptions :: [Symbol] -> Command
checkSatWithAssumptions [Symbol]
nms = Builder -> Command
Cmd (Builder -> Command) -> Builder -> Command
forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"check-sat-assuming" [[Builder] -> Builder
builder_list ((Symbol -> Builder) -> [Symbol] -> [Builder]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> Builder
Builder.fromText [Symbol]
nms)]

-- | Get the model associated with the last call to @check-sat@.
getModel :: Command
getModel :: Command
getModel = Builder -> Command
Cmd Builder
"(get-model)"

getUnsatAssumptions :: Command
getUnsatAssumptions :: Command
getUnsatAssumptions = Builder -> Command
Cmd Builder
"(get-unsat-assumptions)"

getUnsatCore :: Command
getUnsatCore :: Command
getUnsatCore = Builder -> Command
Cmd Builder
"(get-unsat-core)"

-- | Get the values associated with the terms from the last call to @check-sat@.
getValue :: [Term] -> Command
getValue :: [Term] -> Command
getValue [Term]
values = Builder -> Command
Cmd (Builder -> Command) -> Builder -> Command
forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"get-value" [[Builder] -> Builder
builder_list (Term -> Builder
renderTerm (Term -> Builder) -> [Term] -> [Builder]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term]
values)]

-- | Empties the assertion stack and remove all global assertions and declarations.
resetAssertions :: Command
resetAssertions :: Command
resetAssertions = Builder -> Command
Cmd Builder
"(reset-assertions)"

-- | Push the given number of scope frames to the SMT solver.
push :: Integer -> Command
push :: Integer -> Command
push Integer
n =  Builder -> Command
Cmd (Builder -> Command) -> Builder -> Command
forall a b. (a -> b) -> a -> b
$ Builder
"(push " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
forall a. Integral a => a -> Builder
Builder.decimal Integer
n Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"

-- | Pop the given number of scope frames to the SMT solver.
pop :: Integer -> Command
pop :: Integer -> Command
pop Integer
n =  Builder -> Command
Cmd (Builder -> Command) -> Builder -> Command
forall a b. (a -> b) -> a -> b
$ Builder
"(pop " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Integer -> Builder
forall a. Integral a => a -> Builder
Builder.decimal Integer
n Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"

-- | This is a subtype of the type of the same name in Data.SBV.Control.
data SMTInfoFlag =
    Name
  | Version
  | ErrorBehavior
  | InfoKeyword Text
  deriving (Typeable SMTInfoFlag
DataType
Constr
Typeable SMTInfoFlag
-> (forall (c :: Type -> Type).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> SMTInfoFlag -> c SMTInfoFlag)
-> (forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c SMTInfoFlag)
-> (SMTInfoFlag -> Constr)
-> (SMTInfoFlag -> DataType)
-> (forall (t :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c SMTInfoFlag))
-> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c SMTInfoFlag))
-> ((forall b. Data b => b -> b) -> SMTInfoFlag -> SMTInfoFlag)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> SMTInfoFlag -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> SMTInfoFlag -> r)
-> (forall u. (forall d. Data d => d -> u) -> SMTInfoFlag -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> SMTInfoFlag -> u)
-> (forall (m :: Type -> Type).
    Monad m =>
    (forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag)
-> Data SMTInfoFlag
SMTInfoFlag -> DataType
SMTInfoFlag -> Constr
(forall b. Data b => b -> b) -> SMTInfoFlag -> SMTInfoFlag
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SMTInfoFlag -> c SMTInfoFlag
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SMTInfoFlag
forall a.
Typeable a
-> (forall (c :: Type -> Type).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: Type -> Type).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: Type -> Type).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: Type -> Type).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> SMTInfoFlag -> u
forall u. (forall d. Data d => d -> u) -> SMTInfoFlag -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SMTInfoFlag -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SMTInfoFlag -> r
forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag
forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag
forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SMTInfoFlag
forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SMTInfoFlag -> c SMTInfoFlag
forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SMTInfoFlag)
forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SMTInfoFlag)
$cInfoKeyword :: Constr
$cErrorBehavior :: Constr
$cVersion :: Constr
$cName :: Constr
$tSMTInfoFlag :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag
$cgmapMo :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag
gmapMp :: (forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag
$cgmapMp :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag
gmapM :: (forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag
$cgmapM :: forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> SMTInfoFlag -> m SMTInfoFlag
gmapQi :: Int -> (forall d. Data d => d -> u) -> SMTInfoFlag -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SMTInfoFlag -> u
gmapQ :: (forall d. Data d => d -> u) -> SMTInfoFlag -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SMTInfoFlag -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SMTInfoFlag -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> SMTInfoFlag -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SMTInfoFlag -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> SMTInfoFlag -> r
gmapT :: (forall b. Data b => b -> b) -> SMTInfoFlag -> SMTInfoFlag
$cgmapT :: (forall b. Data b => b -> b) -> SMTInfoFlag -> SMTInfoFlag
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SMTInfoFlag)
$cdataCast2 :: forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c SMTInfoFlag)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c SMTInfoFlag)
$cdataCast1 :: forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c SMTInfoFlag)
dataTypeOf :: SMTInfoFlag -> DataType
$cdataTypeOf :: SMTInfoFlag -> DataType
toConstr :: SMTInfoFlag -> Constr
$ctoConstr :: SMTInfoFlag -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SMTInfoFlag
$cgunfold :: forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c SMTInfoFlag
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SMTInfoFlag -> c SMTInfoFlag
$cgfoldl :: forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> SMTInfoFlag -> c SMTInfoFlag
$cp1Data :: Typeable SMTInfoFlag
Data, SMTInfoFlag -> SMTInfoFlag -> Bool
(SMTInfoFlag -> SMTInfoFlag -> Bool)
-> (SMTInfoFlag -> SMTInfoFlag -> Bool) -> Eq SMTInfoFlag
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SMTInfoFlag -> SMTInfoFlag -> Bool
$c/= :: SMTInfoFlag -> SMTInfoFlag -> Bool
== :: SMTInfoFlag -> SMTInfoFlag -> Bool
$c== :: SMTInfoFlag -> SMTInfoFlag -> Bool
Eq, Eq SMTInfoFlag
Eq SMTInfoFlag
-> (SMTInfoFlag -> SMTInfoFlag -> Ordering)
-> (SMTInfoFlag -> SMTInfoFlag -> Bool)
-> (SMTInfoFlag -> SMTInfoFlag -> Bool)
-> (SMTInfoFlag -> SMTInfoFlag -> Bool)
-> (SMTInfoFlag -> SMTInfoFlag -> Bool)
-> (SMTInfoFlag -> SMTInfoFlag -> SMTInfoFlag)
-> (SMTInfoFlag -> SMTInfoFlag -> SMTInfoFlag)
-> Ord SMTInfoFlag
SMTInfoFlag -> SMTInfoFlag -> Bool
SMTInfoFlag -> SMTInfoFlag -> Ordering
SMTInfoFlag -> SMTInfoFlag -> SMTInfoFlag
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SMTInfoFlag -> SMTInfoFlag -> SMTInfoFlag
$cmin :: SMTInfoFlag -> SMTInfoFlag -> SMTInfoFlag
max :: SMTInfoFlag -> SMTInfoFlag -> SMTInfoFlag
$cmax :: SMTInfoFlag -> SMTInfoFlag -> SMTInfoFlag
>= :: SMTInfoFlag -> SMTInfoFlag -> Bool
$c>= :: SMTInfoFlag -> SMTInfoFlag -> Bool
> :: SMTInfoFlag -> SMTInfoFlag -> Bool
$c> :: SMTInfoFlag -> SMTInfoFlag -> Bool
<= :: SMTInfoFlag -> SMTInfoFlag -> Bool
$c<= :: SMTInfoFlag -> SMTInfoFlag -> Bool
< :: SMTInfoFlag -> SMTInfoFlag -> Bool
$c< :: SMTInfoFlag -> SMTInfoFlag -> Bool
compare :: SMTInfoFlag -> SMTInfoFlag -> Ordering
$ccompare :: SMTInfoFlag -> SMTInfoFlag -> Ordering
$cp1Ord :: Eq SMTInfoFlag
Ord, (forall x. SMTInfoFlag -> Rep SMTInfoFlag x)
-> (forall x. Rep SMTInfoFlag x -> SMTInfoFlag)
-> Generic SMTInfoFlag
forall x. Rep SMTInfoFlag x -> SMTInfoFlag
forall x. SMTInfoFlag -> Rep SMTInfoFlag x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SMTInfoFlag x -> SMTInfoFlag
$cfrom :: forall x. SMTInfoFlag -> Rep SMTInfoFlag x
Generic, Int -> SMTInfoFlag -> String -> String
[SMTInfoFlag] -> String -> String
SMTInfoFlag -> String
(Int -> SMTInfoFlag -> String -> String)
-> (SMTInfoFlag -> String)
-> ([SMTInfoFlag] -> String -> String)
-> Show SMTInfoFlag
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [SMTInfoFlag] -> String -> String
$cshowList :: [SMTInfoFlag] -> String -> String
show :: SMTInfoFlag -> String
$cshow :: SMTInfoFlag -> String
showsPrec :: Int -> SMTInfoFlag -> String -> String
$cshowsPrec :: Int -> SMTInfoFlag -> String -> String
Show, Typeable)

flagToSExp :: SMTInfoFlag -> Text
flagToSExp :: SMTInfoFlag -> Symbol
flagToSExp = (Char -> Symbol -> Symbol
cons Char
':') (Symbol -> Symbol)
-> (SMTInfoFlag -> Symbol) -> SMTInfoFlag -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  \case
    SMTInfoFlag
Name -> Symbol
"name"
    SMTInfoFlag
Version -> Symbol
"version"
    SMTInfoFlag
ErrorBehavior -> Symbol
"error-behavior"
    InfoKeyword Symbol
s -> Symbol
s

-- | A @get-info@ command
getInfo :: SMTInfoFlag -> Command
getInfo :: SMTInfoFlag -> Command
getInfo SMTInfoFlag
flag = Builder -> Command
Cmd (Builder -> Command) -> Builder -> Command
forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"get-info" [Symbol -> Builder
Builder.fromText (SMTInfoFlag -> Symbol
flagToSExp SMTInfoFlag
flag)]

getVersion :: Command
getVersion :: Command
getVersion = SMTInfoFlag -> Command
getInfo SMTInfoFlag
Version

getName :: Command
getName :: Command
getName = SMTInfoFlag -> Command
getInfo SMTInfoFlag
Name

getErrorBehavior :: Command
getErrorBehavior :: Command
getErrorBehavior = SMTInfoFlag -> Command
getInfo SMTInfoFlag
ErrorBehavior