module Language.SMTLib2.Internals.Interface where
import Language.SMTLib2.Internals
import Language.SMTLib2.Internals.Instances (extractAnnotation,dtList,conNil,conInsert,withSort)
import Language.SMTLib2.Internals.Optimize
import Language.SMTLib2.Internals.Operators
import Language.SMTLib2.Strategy
import Data.Typeable
import Data.Array
import Data.Unit
import Data.List (genericReplicate)
import Data.Proxy
checkSat :: Monad m => SMT' m Bool
checkSat = checkSat' Nothing noLimits >>= return.isSat
checkSatUsing :: Monad m => Tactic -> SMT' m Bool
checkSatUsing t = checkSat' (Just t) noLimits >>= return.isSat
checkSat' :: Monad m => Maybe Tactic -> CheckSatLimits -> SMT' m CheckSatResult
checkSat' tactic limits = smtBackend $ \b -> smtHandle b (SMTCheckSat tactic limits)
isSat :: CheckSatResult -> Bool
isSat Sat = True
isSat Unsat = False
isSat Unknown = error "smtlib2: checkSat query return 'unknown' (To catch this, use checkSat' function)"
apply :: Monad m => Tactic -> SMT' m [SMTExpr Bool]
apply t = smtBackend $ \backend -> smtHandle backend (SMTApply t)
push :: Monad m => SMT' m ()
push = smtBackend $ \b -> smtHandle b SMTPush
pop :: Monad m => SMT' m ()
pop = smtBackend $ \b -> smtHandle b SMTPop
stack :: Monad m => SMT' m a -> SMT' m a
stack act = do
push
res <- act
pop
return res
comment :: Monad m => String -> SMT' m ()
comment msg = smtBackend $ \b -> smtHandle b (SMTComment msg)
varNamed :: (SMTType t,Typeable t,Unit (SMTAnnotation t),Monad m) => String -> SMT' m (SMTExpr t)
varNamed name = varNamedAnn name unit
varNamedAnn :: (SMTType t,Typeable t,Monad m) => String -> SMTAnnotation t -> SMT' m (SMTExpr t)
varNamedAnn = argVarsAnnNamed
varAnn :: (SMTType t,Typeable t,Monad m) => SMTAnnotation t -> SMT' m (SMTExpr t)
varAnn ann = argVarsAnn ann
var :: (SMTType t,Typeable t,Unit (SMTAnnotation t),Monad m) => SMT' m (SMTExpr t)
var = argVarsAnn unit
untypedNamedVar :: Monad m => String -> Sort -> SMT' m (SMTExpr Untyped)
untypedNamedVar name sort = do
dts <- smtBackend $ \b -> smtHandle b SMTDeclaredDataTypes
withSort dts sort $
\(_::t) ann -> do
v <- varNamedAnn name ann
return $ UntypedExpr (v::SMTExpr t)
untypedVar :: Monad m => Sort -> SMT' m (SMTExpr Untyped)
untypedVar sort = do
dts <- smtBackend $ \b -> smtHandle b SMTDeclaredDataTypes
withSort dts sort $
\(_::t) ann -> do
v <- varAnn ann
return $ UntypedExpr (v::SMTExpr t)
argVarsAnn :: (Args a,Monad m) => ArgAnnotation a -> SMT' m a
argVarsAnn = argVarsAnnNamed' Nothing
argVarsAnnNamed :: (Args a,Monad m) => String -> ArgAnnotation a -> SMT' m a
argVarsAnnNamed name = argVarsAnnNamed' (Just name)
argVarsAnnNamed' :: (Args a,Monad m) => Maybe String -> ArgAnnotation a -> SMT' m a
argVarsAnnNamed' name ann = do
(_,arg) <- foldExprs (\_ (_::SMTExpr t) ann' -> do
declareType (undefined::t) ann'
let info = FunInfo { funInfoProxy = Proxy::Proxy ((),t)
, funInfoArgAnn = ()
, funInfoResAnn = ann'
, funInfoName = name }
res <- smtBackend $ \b -> smtHandle b (SMTDeclareFun info)
let expr = Var res ann'
case additionalConstraints (undefined::t) ann' of
Nothing -> return ()
Just constr -> mapM_ assert $ constr expr
return ((),expr)
) () undefined ann
return arg
argVars :: (Args a,Unit (ArgAnnotation a),Monad m) => SMT' m a
argVars = argVarsAnn unit
constant :: (SMTValue t,Unit (SMTAnnotation t)) => t -> SMTExpr t
constant x = Const x unit
constantAnn :: SMTValue t => t -> SMTAnnotation t -> SMTExpr t
constantAnn x ann = Const x ann
getValue :: (SMTValue t,Monad m) => SMTExpr t -> SMT' m t
getValue expr = smtBackend $ \b -> smtHandle b (SMTGetValue expr)
getValues :: (LiftArgs arg,Monad m) => arg -> SMT' m (Unpacked arg)
getValues args = unliftArgs args getValue
getModel :: Monad m => SMT' m SMTModel
getModel = smtBackend $ \b -> smtHandle b SMTGetModel
unmangleArray :: (Liftable i,LiftArgs i,Ix (Unpacked i),SMTValue v,
Unit (ArgAnnotation i),Monad m)
=> (Unpacked i,Unpacked i)
-> SMTExpr (SMTArray i v)
-> SMT' m (Array (Unpacked i) v)
unmangleArray b expr = mapM (\i -> do
v <- getValue (App SMTSelect (expr,liftArgs i unit))
return (i,v)
) (range b) >>= return.array b
defFun :: (Args a,SMTType r,Unit (ArgAnnotation a),Monad m)
=> (a -> SMTExpr r) -> SMT' m (SMTFunction a r)
defFun = defFunAnn unit
defConst :: (SMTType r,Monad m) => SMTExpr r -> SMT' m (SMTExpr r)
defConst = defConstNamed "constvar"
defConstNamed :: (SMTType r,Monad m) => String -> SMTExpr r -> SMT' m (SMTExpr r)
defConstNamed name = defConstNamed' (Just name)
defConstNamed' :: (SMTType r,Monad m) => Maybe String -> SMTExpr r -> SMT' m (SMTExpr r)
defConstNamed' name e = do
i <- smtBackend $ \b -> smtHandle b (SMTDefineFun name (Proxy::Proxy ()) () e)
return (Var i (extractAnnotation e))
defFunAnnNamed :: (Args a,SMTType r,Monad m)
=> String -> ArgAnnotation a -> (a -> SMTExpr r) -> SMT' m (SMTFunction a r)
defFunAnnNamed name = defFunAnnNamed' (Just name)
defFunAnnNamed' :: (Args a,SMTType r,Monad m)
=> Maybe String -> ArgAnnotation a -> (a -> SMTExpr r)
-> SMT' m (SMTFunction a r)
defFunAnnNamed' name ann_arg (f::a -> SMTExpr r) = do
let (_,rargs) = foldExprsId (\i _ ann -> (i+1,FunArg i ann)) 0 (undefined::a) ann_arg
body = f rargs
i <- smtBackend $ \b -> smtHandle b (SMTDefineFun name (Proxy::Proxy a) ann_arg body)
return (SMTFun i (extractAnnotation body))
defFunAnn :: (Args a,SMTType r,Monad m)
=> ArgAnnotation a -> (a -> SMTExpr r) -> SMT' m (SMTFunction a r)
defFunAnn = defFunAnnNamed' Nothing
and' :: SMTFunction [SMTExpr Bool] Bool
and' = SMTLogic And
(.&&.) :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool
(.&&.) x y = App (SMTLogic And) [x,y]
or' :: SMTFunction [SMTExpr Bool] Bool
or' = SMTLogic Or
(.||.) :: SMTExpr Bool -> SMTExpr Bool -> SMTExpr Bool
(.||.) x y = App (SMTLogic Or) [x,y]
arrayEquals :: (LiftArgs i,Liftable i,SMTValue v,Ix (Unpacked i),Unit (ArgAnnotation i),Unit (SMTAnnotation v))
=> SMTExpr (SMTArray i v) -> Array (Unpacked i) v -> SMTExpr Bool
arrayEquals expr arr
= case [(select expr (liftArgs i unit)) .==. (constant v)
| (i,v) <- assocs arr ] of
[] -> constant True
xs -> foldl1 (.&&.) xs
assert :: Monad m => SMTExpr Bool -> SMT' m ()
assert expr = smtBackend $ \b -> smtHandle b (SMTAssert expr Nothing Nothing)
interpolationGroup :: Monad m => SMT' m InterpolationGroup
interpolationGroup = smtBackend $ \b -> smtHandle b SMTNewInterpolationGroup
assertId :: Monad m => SMTExpr Bool -> SMT' m ClauseId
assertId expr = smtBackend $ \b -> do
(cid,b1) <- smtHandle b SMTNewClauseId
((),b2) <- smtHandle b1 (SMTAssert expr Nothing (Just cid))
return (cid,b2)
assertInterp :: Monad m => SMTExpr Bool -> InterpolationGroup -> SMT' m ()
assertInterp expr interp = smtBackend $ \b -> smtHandle b (SMTAssert expr (Just interp) Nothing)
getInterpolant :: Monad m => [InterpolationGroup] -> SMT' m (SMTExpr Bool)
getInterpolant grps = smtBackend $ \b -> smtHandle b (SMTGetInterpolant grps)
interpolate :: Monad m => [SMTExpr Bool] -> SMT' m [SMTExpr Bool]
interpolate exprs = smtBackend $ \b -> smtHandle b (SMTInterpolate exprs)
setOption :: Monad m => SMTOption -> SMT' m ()
setOption opt = smtBackend $ \b -> smtHandle b (SMTSetOption opt)
getInfo :: (Monad m,Typeable i) => SMTInfo i -> SMT' m i
getInfo inf = smtBackend $ \b -> smtHandle b (SMTGetInfo inf)
funAnn :: (Liftable a,SMTType r,Monad m) => ArgAnnotation a -> SMTAnnotation r -> SMT' m (SMTFunction a r)
funAnn = funAnnNamed' Nothing
funAnnNamed :: (Liftable a, SMTType r,Monad m) => String -> ArgAnnotation a -> SMTAnnotation r -> SMT' m (SMTFunction a r)
funAnnNamed name = funAnnNamed' (Just name)
funAnnNamed' :: (Liftable a, SMTType r,Monad m) => Maybe String -> ArgAnnotation a -> SMTAnnotation r -> SMT' m (SMTFunction a r)
funAnnNamed' name annArg annRet
= withUndef $ \(_::a) (_::r) -> do
let finfo = FunInfo { funInfoProxy = Proxy::Proxy (a,r)
, funInfoArgAnn = annArg
, funInfoResAnn = annRet
, funInfoName = name
}
i <- smtBackend $ \b -> smtHandle b (SMTDeclareFun finfo)
let fun = SMTFun i annRet
case additionalConstraints (undefined::t) annRet of
Nothing -> return ()
Just constr -> assert $ forAllAnn annArg
(\x -> case constr (fun `app` x) of
[] -> constant True
[x] -> x
xs -> and' `app` xs)
return fun
where
withUndef :: (a -> r -> SMT' m (SMTFunction a r)) -> SMT' m (SMTFunction a r)
withUndef f = f undefined undefined
funAnnRet :: (Liftable a,SMTType r,Unit (ArgAnnotation a),Monad m)
=> SMTAnnotation r -> SMT' m (SMTFunction a r)
funAnnRet = funAnn unit
fun :: (Liftable a,SMTType r,SMTAnnotation r ~ (),Unit (ArgAnnotation a),Monad m)
=> SMT' m (SMTFunction a r)
fun = funAnn unit unit
app :: (Args arg,SMTType res) => SMTFunction arg res -> arg -> SMTExpr res
app = App
map' :: (Liftable arg,Args i,SMTType res)
=> SMTFunction arg res -> SMTFunction (Lifted arg i) (SMTArray i res)
map' f = SMTMap f
(.==.) :: SMTType a => SMTExpr a -> SMTExpr a -> SMTExpr Bool
(.==.) x y = App SMTEq [x,y]
infix 4 .==.
argEq :: Args a => a -> a -> SMTExpr Bool
argEq xs ys = app and' res
where
(res,_,_) = foldsExprsId
(\s [(arg1,_),(arg2,_)] _ -> ((arg1 .==. arg2):s,[arg1,arg2],undefined))
[]
[(xs,()),(ys,())] (extractArgAnnotation xs)
distinct :: SMTType a => [SMTExpr a] -> SMTExpr Bool
distinct = App SMTDistinct
plus :: (SMTArith a) => SMTFunction [SMTExpr a] a
plus = SMTArith Plus
mult :: (SMTArith a) => SMTFunction [SMTExpr a] a
mult = SMTArith Mult
minus :: (SMTArith a) => SMTFunction (SMTExpr a,SMTExpr a) a
minus = SMTMinus
div' :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Integer
div' x y = App (SMTIntArith Div) (x,y)
div'' :: SMTFunction (SMTExpr Integer,SMTExpr Integer) Integer
div'' = SMTIntArith Div
mod' :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Integer
mod' x y = App (SMTIntArith Mod) (x,y)
mod'' :: SMTFunction (SMTExpr Integer,SMTExpr Integer) Integer
mod'' = SMTIntArith Mod
rem' :: SMTExpr Integer -> SMTExpr Integer -> SMTExpr Integer
rem' x y = App (SMTIntArith Rem) (x,y)
rem'' :: SMTFunction (SMTExpr Integer,SMTExpr Integer) Integer
rem'' = SMTIntArith Rem
divide :: SMTExpr Rational -> SMTExpr Rational -> SMTExpr Rational
divide x y = App SMTDivide (x,y)
divide' :: SMTFunction (SMTExpr Rational,SMTExpr Rational) Rational
divide' = SMTDivide
neg :: SMTArith a => SMTFunction (SMTExpr a) a
neg = SMTNeg
toReal :: SMTExpr Integer -> SMTExpr Rational
toReal = App SMTToReal
toInt :: SMTExpr Rational -> SMTExpr Integer
toInt = App SMTToInt
ite :: (SMTType a) => SMTExpr Bool
-> SMTExpr a
-> SMTExpr a
-> SMTExpr a
ite c l r = App SMTITE (c,l,r)
xor :: SMTFunction [SMTExpr Bool] Bool
xor = SMTLogic XOr
(.=>.) :: SMTExpr Bool
-> SMTExpr Bool
-> SMTExpr Bool
(.=>.) x y = App (SMTLogic Implies) [x,y]
not' :: SMTExpr Bool -> SMTExpr Bool
not' = App SMTNot
not'' :: SMTFunction (SMTExpr Bool) Bool
not'' = SMTNot
select :: (Liftable i,SMTType v) => SMTExpr (SMTArray i v) -> i -> SMTExpr v
select arr i = App SMTSelect (arr,i)
store :: (Liftable i,SMTType v) => SMTExpr (SMTArray i v) -> i -> SMTExpr v -> SMTExpr (SMTArray i v)
store arr i v = App SMTStore (arr,i,v)
asArray :: (Args arg,Unit (ArgAnnotation arg),SMTType res)
=> SMTFunction arg res -> SMTExpr (SMTArray arg res)
asArray f = AsArray f unit
constArray :: (Args i,SMTType v) => SMTExpr v
-> ArgAnnotation i
-> SMTExpr (SMTArray i v)
constArray e i_ann = App (SMTConstArray i_ann) e
bvand :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)
bvand e1 e2 = App (SMTBVBin BVAnd) (e1,e2)
bvor :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)
bvor e1 e2 = App (SMTBVBin BVOr) (e1,e2)
bvxor :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)
bvxor e1 e2 = App (SMTBVBin BVXor) (e1,e2)
bvnot :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t)
bvnot e = App (SMTBVUn BVNot) e
bvneg :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t)
bvneg e = App (SMTBVUn BVNeg) e
bvadd :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)
bvadd e1 e2 = App (SMTBVBin BVAdd) (e1,e2)
bvsub :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)
bvsub e1 e2 = App (SMTBVBin BVSub) (e1,e2)
bvmul :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)
bvmul e1 e2 = App (SMTBVBin BVMul) (e1,e2)
bvurem :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)
bvurem e1 e2 = App (SMTBVBin BVURem) (e1,e2)
bvsrem :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)
bvsrem e1 e2 = App (SMTBVBin BVSRem) (e1,e2)
bvudiv :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)
bvudiv e1 e2 = App (SMTBVBin BVUDiv) (e1,e2)
bvsdiv :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)
bvsdiv e1 e2 = App (SMTBVBin BVSDiv) (e1,e2)
bvule :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool
bvule e1 e2 = App (SMTBVComp BVULE) (e1,e2)
bvult :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool
bvult e1 e2 = App (SMTBVComp BVULT) (e1,e2)
bvuge :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool
bvuge e1 e2 = App (SMTBVComp BVUGE) (e1,e2)
bvugt :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool
bvugt e1 e2 = App (SMTBVComp BVUGT) (e1,e2)
bvsle :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool
bvsle e1 e2 = App (SMTBVComp BVSLE) (e1,e2)
bvslt :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool
bvslt e1 e2 = App (SMTBVComp BVSLT) (e1,e2)
bvsge :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool
bvsge e1 e2 = App (SMTBVComp BVSGE) (e1,e2)
bvsgt :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr Bool
bvsgt e1 e2 = App (SMTBVComp BVSGT) (e1,e2)
bvshl :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)
bvshl e1 e2 = App (SMTBVBin BVSHL) (e1,e2)
bvlshr :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)
bvlshr e1 e2 = App (SMTBVBin BVLSHR) (e1,e2)
bvashr :: (IsBitVector t) => SMTExpr (BitVector t) -> SMTExpr (BitVector t) -> SMTExpr (BitVector t)
bvashr e1 e2 = App (SMTBVBin BVASHR) (e1,e2)
bvconcat :: (Concatable t1 t2) => SMTExpr (BitVector t1) -> SMTExpr (BitVector t2) -> SMTExpr (BitVector (ConcatResult t1 t2))
bvconcat e1 e2 = App SMTConcat (e1,e2)
bvextract :: (TypeableNat start,TypeableNat len,Extractable tp len')
=> Proxy start
-> Proxy len
-> SMTExpr (BitVector tp)
-> SMTExpr (BitVector len')
bvextract start len (e::SMTExpr (BitVector tp))
= App (SMTExtract start len) e
bvextract' :: Integer -> Integer -> SMTExpr (BitVector BVUntyped) -> SMTExpr (BitVector BVUntyped)
bvextract' start len = reifyNat start $
\start' -> reifyNat len $ \len' -> bvextract start' len'
bvsplitu16to8 :: SMTExpr BV16 -> (SMTExpr BV8,SMTExpr BV8)
bvsplitu16to8 e = (App (SMTExtract (Proxy::Proxy N8) (Proxy::Proxy N8)) e,
App (SMTExtract (Proxy::Proxy N0) (Proxy::Proxy N8)) e)
bvsplitu32to16 :: SMTExpr BV32 -> (SMTExpr BV16,SMTExpr BV16)
bvsplitu32to16 e = (App (SMTExtract (Proxy::Proxy N16) (Proxy::Proxy N16)) e,
App (SMTExtract (Proxy::Proxy N0) (Proxy::Proxy N16)) e)
bvsplitu32to8 :: SMTExpr BV32 -> (SMTExpr BV8,SMTExpr BV8,SMTExpr BV8,SMTExpr BV8)
bvsplitu32to8 e = (App (SMTExtract (Proxy::Proxy N24) (Proxy::Proxy N8)) e,
App (SMTExtract (Proxy::Proxy N16) (Proxy::Proxy N8)) e,
App (SMTExtract (Proxy::Proxy N8) (Proxy::Proxy N8)) e,
App (SMTExtract (Proxy::Proxy N0) (Proxy::Proxy N8)) e)
bvsplitu64to32 :: SMTExpr BV64 -> (SMTExpr BV32,SMTExpr BV32)
bvsplitu64to32 e = (App (SMTExtract (Proxy::Proxy N32) (Proxy::Proxy N32)) e,
App (SMTExtract (Proxy::Proxy N0) (Proxy::Proxy N32)) e)
bvsplitu64to16 :: SMTExpr BV64 -> (SMTExpr BV16,SMTExpr BV16,SMTExpr BV16,SMTExpr BV16)
bvsplitu64to16 e = (App (SMTExtract (Proxy::Proxy N48) (Proxy::Proxy N16)) e,
App (SMTExtract (Proxy::Proxy N32) (Proxy::Proxy N16)) e,
App (SMTExtract (Proxy::Proxy N16) (Proxy::Proxy N16)) e,
App (SMTExtract (Proxy::Proxy N0) (Proxy::Proxy N16)) e)
bvsplitu64to8 :: SMTExpr BV64 -> (SMTExpr BV8,SMTExpr BV8,SMTExpr BV8,SMTExpr BV8,SMTExpr BV8,SMTExpr BV8,SMTExpr BV8,SMTExpr BV8)
bvsplitu64to8 e = (App (SMTExtract (Proxy::Proxy N56) (Proxy::Proxy N8)) e,
App (SMTExtract (Proxy::Proxy N48) (Proxy::Proxy N8)) e,
App (SMTExtract (Proxy::Proxy N40) (Proxy::Proxy N8)) e,
App (SMTExtract (Proxy::Proxy N32) (Proxy::Proxy N8)) e,
App (SMTExtract (Proxy::Proxy N24) (Proxy::Proxy N8)) e,
App (SMTExtract (Proxy::Proxy N16) (Proxy::Proxy N8)) e,
App (SMTExtract (Proxy::Proxy N8) (Proxy::Proxy N8)) e,
App (SMTExtract (Proxy::Proxy N0) (Proxy::Proxy N8)) e)
mkQuantified :: (Args a,SMTType b) => (Integer -> [ProxyArg] -> SMTExpr b -> SMTExpr b)
-> ArgAnnotation a -> (a -> SMTExpr b)
-> SMTExpr b
mkQuantified constr ann f = constr lvl sorts body
where
undef :: (a -> SMTExpr b) -> a
undef _ = undefined
sorts = getTypes (undef f) ann
Just (arg0,[]) = toArgs ann [InternalObj () prx
| prx <- sorts ]
body' = f arg0
lvl = quantificationLevel body'
Just (arg1,[]) = toArgs ann [QVar lvl i prx
| (i,prx) <- Prelude.zip [0..] sorts ]
body = f arg1
forAll :: (Args a,Unit (ArgAnnotation a)) => (a -> SMTExpr Bool) -> SMTExpr Bool
forAll = forAllAnn unit
forAllAnn :: Args a => ArgAnnotation a -> (a -> SMTExpr Bool) -> SMTExpr Bool
forAllAnn = mkQuantified Forall
exists :: (Args a,Unit (ArgAnnotation a)) => (a -> SMTExpr Bool) -> SMTExpr Bool
exists = existsAnn unit
existsAnn :: Args a => ArgAnnotation a -> (a -> SMTExpr Bool) -> SMTExpr Bool
existsAnn = mkQuantified Exists
let' :: (Args a,Unit (ArgAnnotation a),SMTType b) => a -> (a -> SMTExpr b) -> SMTExpr b
let' = letAnn unit
letAnn :: (Args a,SMTType b) => ArgAnnotation a -> a -> (a -> SMTExpr b) -> SMTExpr b
letAnn ann arg = mkQuantified (\lvl _ body -> Let lvl args body) ann
where
args = fromArgs arg
lets :: (Args a,Unit (ArgAnnotation a),SMTType b) => [a] -> ([a] -> SMTExpr b) -> SMTExpr b
lets xs = letAnn (fmap (const unit) xs) xs
forAllList :: (Args a,Unit (ArgAnnotation a)) => Integer
-> ([a] -> SMTExpr Bool)
-> SMTExpr Bool
forAllList l = forAllAnn (genericReplicate l unit)
existsList :: (Args a,Unit (ArgAnnotation a)) => Integer
-> ([a] -> SMTExpr Bool)
-> SMTExpr Bool
existsList l = existsAnn (genericReplicate l unit)
is :: (Args arg,SMTType dt) => SMTExpr dt -> Constructor arg dt -> SMTExpr Bool
is e con = App (SMTConTest con) e
(.#) :: (SMTType a,SMTType f) => SMTExpr a -> Field a f -> SMTExpr f
(.#) e f = App (SMTFieldSel f) e
head' :: (SMTType a,Unit (SMTAnnotation a)) => SMTExpr [a] -> SMTExpr a
head' = App (SMTBuiltIn "head" unit)
tail' :: (SMTType a,Unit (SMTAnnotation a)) => SMTExpr [a] -> SMTExpr [a]
tail' = App (SMTBuiltIn "tail" unit)
isNil :: (SMTType a) => SMTExpr [a] -> SMTExpr Bool
isNil (e::SMTExpr [a]) = is e (Constructor [ProxyArg (undefined::[a]) (extractAnnotation e)] dtList conNil:: Constructor () [a])
isInsert :: (SMTType a,Unit (SMTAnnotation a)) => SMTExpr [a] -> SMTExpr Bool
isInsert (e::SMTExpr [a]) = is e (Constructor [ProxyArg (undefined::[a]) (extractAnnotation e)] dtList conInsert :: Constructor (SMTExpr a,SMTExpr [a]) [a])
setLogic :: Monad m => String -> SMT' m ()
setLogic name = smtBackend $ \b -> smtHandle b (SMTSetLogic name)
named :: (SMTType a,SMTAnnotation a ~ (),Monad m)
=> String -> SMTExpr a -> SMT' m (SMTExpr a,SMTExpr a)
named name expr = do
i <- smtBackend $ \b -> smtHandle b (SMTNameExpr name expr)
return (Named expr i,Var i (extractAnnotation expr))
named' :: (SMTType a,SMTAnnotation a ~ (),Monad m)
=> SMTExpr a -> SMT' m (SMTExpr a,SMTExpr a)
named' = named "named"
getProof :: Monad m => SMT' m (SMTExpr Bool)
getProof = smtBackend $ \b -> smtHandle b SMTGetProof
simplify :: (SMTType t,Monad m) => SMTExpr t -> SMT' m (SMTExpr t)
simplify expr = smtBackend $ \b -> smtHandle b (SMTSimplify expr)
getUnsatCore :: Monad m => SMT' m [ClauseId]
getUnsatCore = smtBackend $ \b -> smtHandle b SMTGetUnsatCore
optimizeExpr' :: SMTExpr a -> SMTExpr a
optimizeExpr' e = case optimizeExpr e of
Nothing -> e
Just e' -> e'