{-|
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
  , getAbduct
  , getAbductNext
    -- * SyGuS
  , synthFun
  , declareVar
  , constraint
  , checkSynth
    -- * Logic
  , Logic(..)
  , qf_bv
  , allSupported
  , allLogic
  , hornLogic
    -- * 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
"(" forall a. Semigroup a => a -> a -> a
<> Builder
o forall a. Semigroup a => a -> a -> a
<> forall {a}. (IsString a, Semigroup a) => [a] -> a
go [Builder]
args
  where go :: [a] -> a
go [] = a
")"
        go (a
f:[a]
r) = a
" " forall a. Semigroup a => a -> a -> a
<> a
f forall a. Semigroup a => a -> a -> a
<> [a] -> a
go [a]
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"
{-# DEPRECATED allSupported "Use allLogic instead" #-}

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

-- | Use the Horn logic
hornLogic :: Logic
hornLogic :: Logic
hornLogic = Builder -> Logic
Logic Builder
"HORN"

------------------------------------------------------------------------
-- 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 :: Text -> Sort
varSort = Builder -> Sort
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> 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 forall a. Ord a => a -> a -> Bool
>= Natural
1 = Builder -> Sort
Sort forall a b. (a -> b) -> a -> b
$ Builder
"(_ BitVec " forall a. Semigroup a => a -> a -> a
<> forall a. IsString a => [Char] -> a
fromString (forall a. Show a => a -> [Char]
show Natural
w) forall a. Semigroup a => a -> a -> a
<> Builder
")"
         | Bool
otherwise = forall a. HasCallStack => [Char] -> a
error [Char]
"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 forall a b. (a -> b) -> a -> b
$ Builder
"(Array " forall a. Semigroup a => a -> a -> a
<> Builder
i forall a. Semigroup a => a -> a -> a
<> Builder
" " forall a. Semigroup a => a -> a -> a
<> Builder
v forall a. Semigroup a => a -> a -> a
<> Builder
")"

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

-- | Denotes an expression in the SMT solver
newtype Term = T { Term -> Builder
renderTerm :: Builder }
  deriving ([Char] -> Term
forall a. ([Char] -> a) -> IsString a
fromString :: [Char] -> Term
$cfromString :: [Char] -> Term
IsString, Semigroup Term
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
Monoid, NonEmpty Term -> Term
Term -> Term -> 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 :: forall b. Integral b => 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 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 forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ 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]
_ = forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> [Char]
show Builder
f forall a. [a] -> [a] -> [a]
++ [Char]
" 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
tforall 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 -> Text -> Term
namedTerm (T Builder
x) Text
nm = Builder -> Term
T forall a b. (a -> b) -> a -> b
$ Builder
"(! " forall a. Semigroup a => a -> a -> a
<> Builder
x forall a. Semigroup a => a -> a -> a
<> Builder
" :named " forall a. Semigroup a => a -> a -> a
<> Text -> Builder
Builder.fromText Text
nm 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 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

-- | Xor 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]
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"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 given 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 :: (Text, Sort) -> Builder
varBinding (Text
nm, Sort
tp) = Builder
"(" forall a. Semigroup a => a -> a -> a
<> Text -> Builder
Builder.fromText Text
nm forall a. Semigroup a => a -> a -> a
<> Builder
" " forall a. Semigroup a => a -> a -> a
<> Sort -> Builder
unSort Sort
tp 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_ :: [(Text, Sort)] -> Term -> Term
forall_ [] Term
r = Term
r
forall_ [(Text, Sort)]
vars Term
r =
  Builder -> Term
T forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"forall" [[Builder] -> Builder
builder_list ((Text, Sort) -> Builder
varBinding forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, 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_ :: [(Text, Sort)] -> Term -> Term
exists_ [] Term
r = Term
r
exists_ [(Text, Sort)]
vars Term
r =
  Builder -> Term
T forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"exists" [[Builder] -> Builder
builder_list ((Text, Sort) -> Builder
varBinding forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, Sort)]
vars), Term -> Builder
renderTerm Term
r]

letBinding :: (Text, Term) -> Builder
letBinding :: (Text, Term) -> Builder
letBinding (Text
nm, Term
t) = Builder -> [Builder] -> Builder
app_list (Text -> Builder
Builder.fromText Text
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 :: [(Text, Term)] -> Term -> Term
letBinder [] Term
r = Term
r
letBinder [(Text, Term)]
vars Term
r =
  Builder -> Term
T (Builder -> [Builder] -> Builder
app Builder
"let" [[Builder] -> Builder
builder_list ((Text, Term) -> Builder
letBinding forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, 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 forall a. Ord a => a -> a -> Bool
>= Integer
0 = Builder -> Term
T forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> Builder
Builder.decimal Integer
i
          | Bool
otherwise = Term -> Term
negate (Builder -> Term
T (forall a. Integral a => a -> Builder
Builder.decimal (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 forall a. Ord a => a -> a -> Bool
>= Integer
0 = Builder -> Term
T forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> Builder
Builder.decimal Integer
i forall a. Semigroup a => a -> a -> a
<> Builder
".0"
          | Bool
otherwise = Term -> Term
negate forall a b. (a -> b) -> a -> b
$ Builder -> Term
T forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> Builder
Builder.decimal (forall a. Num a => a -> a
Prelude.negate Integer
i) 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
xforall 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
xforall 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
xforall 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, CVC5, 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 :: forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Term
bvbinary NatRepr w
w0 BV w
u
    | Bool
otherwise = Builder -> Term
T forall a b. (a -> b) -> a -> b
$ Builder
"#b" forall a. Semigroup a => a -> a -> a
<> Natural -> Builder
go (forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr w
w0)
  where go :: Natural -> Builder
        go :: Natural -> Builder
go Natural
0 = forall a. Monoid a => a
mempty
        go Natural
w =
          let i :: Natural
i = Natural
w forall a. Num a => a -> a -> a
- Natural
1
              b :: Builder
              b :: Builder
b = if forall (w :: Natural). Natural -> BV w -> Bool
BV.testBit' Natural
i BV w
u then Builder
"1" else Builder
"0"
           in Builder
b 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 :: forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Term
bvdecimal NatRepr w
w BV w
u = Builder -> Term
T forall a b. (a -> b) -> a -> b
$ forall a. Monoid a => [a] -> a
mconcat [ Builder
"(_ bv"
                            , forall a. Integral a => a -> Builder
Builder.decimal Integer
d
                            , Builder
" "
                            , forall a. Integral a => a -> Builder
Builder.decimal (forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr w
w)
                            , Builder
")"]
  where d :: Integer
d = forall (w :: Natural). 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 :: forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Term
bvhexadecimal NatRepr w
w0 BV w
u
    | Bool
otherwise = Builder -> Term
T forall a b. (a -> b) -> a -> b
$ Builder
"#x" forall a. Semigroup a => a -> a -> a
<> Natural -> Builder
go (forall (n :: Natural). NatRepr n -> Natural
natValue NatRepr w
w0)
  where go :: Natural -> Builder
        go :: Natural -> Builder
go Natural
0 = forall a. Monoid a => a
mempty
        go Natural
w | Natural
w forall a. Ord a => a -> a -> Bool
< Natural
4 = forall a. HasCallStack => [Char] -> a
error [Char]
"bvhexadecimal width must be a multiple of 4."
        go Natural
w =
          let i :: Natural
i = Natural
w forall a. Num a => a -> a -> a
- Natural
4
              charBits :: Integer
charBits = forall (w :: Natural). BV w -> Integer
BV.asUnsigned (forall (w' :: Natural) (w :: Natural).
Natural -> NatRepr w' -> BV w -> BV w'
BV.select' Natural
i (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @4) BV w
u)
              c :: Char
              c :: Char
c = Int -> Char
intToDigit forall a b. (a -> b) -> a -> b
$ forall a. Num a => Integer -> a
fromInteger Integer
charBits
           in Char -> Builder
Builder.singleton Char
c 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 forall a. Ord a => a -> a -> Bool
< Natural
j = forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$ [Char]
"End of extract (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Natural
i forall a. [a] -> [a] -> [a]
++ [Char]
") less than beginning (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Natural
j forall a. [a] -> [a] -> [a]
++ [Char]
")."
  | Bool
otherwise = -- We cannot check that j is small enough.
    let e :: Builder
e = Builder
"(_ extract " forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Builder
Builder.decimal Natural
i forall a. Semigroup a => a -> a -> a
<> Builder
" " forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Builder
Builder.decimal Natural
j 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 " forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Builder
Builder.decimal Integer
w 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 " forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Builder
Builder.decimal Integer
w 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 forall a b. (a -> b) -> a -> b
$ Builder
"(set-logic " forall a. Semigroup a => a -> a -> a
<> Builder
nm 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 :: Text -> Text -> Command
setOption Text
nm Text
val = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app_list Builder
"set-option" [Builder
":" forall a. Semigroup a => a -> a -> a
<> Text -> Builder
Builder.fromText Text
nm, Text -> Builder
Builder.fromText Text
val]

ppBool :: Bool -> Text
ppBool :: Bool -> Text
ppBool Bool
b = if Bool
b then Text
"true" else Text
"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 = Text -> Text -> Command
setOption Text
"produce-models" (Bool -> Text
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 :: Text -> Integer -> Command
declareSort Text
v Integer
n = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"declare-sort" [Text -> Builder
Builder.fromText Text
v, forall a. IsString a => [Char] -> a
fromString (forall a. Show a => a -> [Char]
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 :: Text -> [Text] -> Sort -> Command
defineSort Text
v [Text]
params Sort
d =
  Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"define-sort" [ Text -> Builder
Builder.fromText Text
v
                          , [Builder] -> Builder
builder_list (Text -> Builder
Builder.fromText forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Text]
params)
                          , Sort -> Builder
unSort Sort
d
                          ]

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

-- | Declare a function with the given name, argument types, and
-- return type.
declareFun :: Text -> [Sort] -> Sort -> Command
declareFun :: Text -> [Sort] -> Sort -> Command
declareFun Text
v [Sort]
argSorts Sort
retSort = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$
  Builder -> [Builder] -> Builder
app Builder
"declare-fun" [ Text -> Builder
Builder.fromText Text
v
                    , [Builder] -> Builder
builder_list forall a b. (a -> b) -> a -> b
$ Sort -> Builder
unSort 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 :: Text -> [(Text, Sort)] -> Sort -> Term -> Command
defineFun Text
f [(Text, Sort)]
args Sort
return_type Term
e =
  let resolveArg :: (Text, Sort) -> Builder
resolveArg (Text
var, Sort
tp) = Builder -> [Builder] -> Builder
app (Text -> Builder
Builder.fromText Text
var) [Sort -> Builder
unSort Sort
tp]
   in Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"define-fun" [ Text -> Builder
Builder.fromText Text
f
                             , [Builder] -> Builder
builder_list ((Text, Sort) -> Builder
resolveArg forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Text, 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 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 -> Text -> Command
assertNamed Term
p Text
nm =
  Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"assert"
    [[Builder] -> Builder
builder_list [Text -> Builder
Builder.fromText Text
"!", Term -> Builder
renderTerm Term
p, Text -> Builder
Builder.fromText Text
":named", Text -> Builder
Builder.fromText Text
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 forall a b. (a -> b) -> a -> b
$ Builder
"(check-sat-assuming " forall a. Semigroup a => a -> a -> a
<> [Builder] -> Builder
builder_list (Term -> Builder
renderTerm forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term]
l) 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 :: [Text] -> Command
checkSatWithAssumptions [Text]
nms = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"check-sat-assuming" [[Builder] -> Builder
builder_list (forall a b. (a -> b) -> [a] -> [b]
map Text -> Builder
Builder.fromText [Text]
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 an abduct that entails the formula, and bind it to the name
getAbduct :: Text -> Term -> Command
getAbduct :: Text -> Term -> Command
getAbduct Text
nm Term
p = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder
"(get-abduct " forall a. Semigroup a => a -> a -> a
<> Text -> Builder
Builder.fromText Text
nm forall a. Semigroup a => a -> a -> a
<> Builder
" " forall a. Semigroup a => a -> a -> a
<> Term -> Builder
renderTerm Term
p forall a. Semigroup a => a -> a -> a
<> Builder
")"

-- | Get the next command, called after a get-abduct command
getAbductNext :: Command
getAbductNext :: Command
getAbductNext = Builder -> Command
Cmd Builder
"(get-abduct-next)"

-- | Declare a SyGuS function to synthesize with the given name, arguments, and
-- return type.
synthFun :: Text -> [(Text, Sort)] -> Sort -> Command
synthFun :: Text -> [(Text, Sort)] -> Sort -> Command
synthFun Text
f [(Text, Sort)]
args Sort
ret_tp = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"synth-fun"
  [ Text -> Builder
Builder.fromText Text
f
  , [Builder] -> Builder
builder_list forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (\(Text
var, Sort
tp) -> Builder -> [Builder] -> Builder
app (Text -> Builder
Builder.fromText Text
var) [Sort -> Builder
unSort Sort
tp]) [(Text, Sort)]
args
  , Sort -> Builder
unSort Sort
ret_tp
  ]

-- | Declare a SyGuS variable with the given name and type.
declareVar :: Text -> Sort -> Command
declareVar :: Text -> Sort -> Command
declareVar Text
v Sort
tp = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"declare-var" [Text -> Builder
Builder.fromText Text
v, Sort -> Builder
unSort Sort
tp]

-- | Add the SyGuS constraint to the current synthesis problem.
constraint :: Term -> Command
constraint :: Term -> Command
constraint Term
p = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"constraint" [Term -> Builder
renderTerm Term
p]

-- | Ask the SyGuS solver to find a solution for the synthesis problem
-- corresponding to the current functions-to-synthesize, variables and
-- constraints.
checkSynth :: Command
checkSynth :: Command
checkSynth = Builder -> Command
Cmd Builder
"(check-synth)\n"

-- | 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 forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"get-value" [[Builder] -> Builder
builder_list (Term -> Builder
renderTerm 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 forall a b. (a -> b) -> a -> b
$ Builder
"(push " forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Builder
Builder.decimal Integer
n 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 forall a b. (a -> b) -> a -> b
$ Builder
"(pop " forall a. Semigroup a => a -> a -> a
<> forall a. Integral a => a -> Builder
Builder.decimal Integer
n 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
SMTInfoFlag -> DataType
SMTInfoFlag -> Constr
(forall b. Data b => b -> b) -> SMTInfoFlag -> 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)
gmapMo :: forall (m :: Type -> Type).
MonadPlus m =>
(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 (m :: Type -> Type).
MonadPlus m =>
(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 (m :: Type -> Type).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> SMTInfoFlag -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> SMTInfoFlag -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> SMTInfoFlag -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> SMTInfoFlag -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(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 (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(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 (c :: Type -> Type).
(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 (c :: Type -> Type).
(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
Data, SMTInfoFlag -> SMTInfoFlag -> Bool
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
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
Ord, 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 -> ShowS
[SMTInfoFlag] -> ShowS
SMTInfoFlag -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [SMTInfoFlag] -> ShowS
$cshowList :: [SMTInfoFlag] -> ShowS
show :: SMTInfoFlag -> [Char]
$cshow :: SMTInfoFlag -> [Char]
showsPrec :: Int -> SMTInfoFlag -> ShowS
$cshowsPrec :: Int -> SMTInfoFlag -> ShowS
Show, Typeable)

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

-- | A @get-info@ command
getInfo :: SMTInfoFlag -> Command
getInfo :: SMTInfoFlag -> Command
getInfo SMTInfoFlag
flag = Builder -> Command
Cmd forall a b. (a -> b) -> a -> b
$ Builder -> [Builder] -> Builder
app Builder
"get-info" [Text -> Builder
Builder.fromText (SMTInfoFlag -> Text
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