module Language.SMTLib2 (
SMT(),Embed(),
B.Backend(SMTMonad),
withBackend,
withBackendExitCleanly,
setOption,B.SMTOption(..),
getInfo,B.SMTInfo(..),
B.Expr(),
declareVar,declareVarNamed,
defineVar,defineVarNamed,
declareFun,declareFunNamed,
defineFun,defineFunNamed,
constant,Value(..),
pattern ConstBool,cbool,true,false,
pattern ConstInt,cint,
pattern ConstReal,creal,
BitWidth(),bw,pattern ConstBV,cbv,cbvUntyped,
cdt,
exists, forall,
pattern Fun,app,fun,
pattern EqLst,pattern Eq,pattern (:==:),
eq,(.==.),
pattern DistinctLst,pattern Distinct,pattern (:/=:),
distinct,(./=.),
map',
pattern Ord,pattern (:>=:),pattern (:>:),pattern (:<=:),pattern (:<:),
ord,(.>=.),(.>.),(.<=.),(.<.),
pattern ArithLst,pattern Arith,arith,
pattern PlusLst,pattern Plus,pattern (:+:),plus,(.+.),
pattern MultLst,pattern Mult,pattern (:*:),mult,(.*.),
pattern MinusLst,pattern Minus,pattern (:-:),pattern Neg,minus,(.-.),neg,
pattern Div,pattern Mod,pattern Rem,div',mod',rem',
pattern (:/:),(./.),
pattern Abs,abs',
pattern Not,not',
pattern LogicLst,pattern Logic,logic,
pattern AndLst,pattern And,pattern (:&:),and',(.&.),
pattern OrLst,pattern Or,pattern (:|:),or',(.|.),
pattern XOrLst,pattern XOr,xor',
pattern ImpliesLst,pattern Implies,pattern (:=>:),implies,(.=>.),
pattern ToReal,pattern ToInt,toReal,toInt,
pattern ITE,ite,
pattern BVComp,pattern BVULE,pattern BVULT,pattern BVUGE,pattern BVUGT,pattern BVSLE,pattern BVSLT,pattern BVSGE,pattern BVSGT,bvcomp,bvule,bvult,bvuge,bvugt,bvsle,bvslt,bvsge,bvsgt,
pattern BVBin,pattern BVAdd,pattern BVSub,pattern BVMul,pattern BVURem,pattern BVSRem,pattern BVUDiv,pattern BVSDiv,pattern BVSHL,pattern BVLSHR,pattern BVASHR,pattern BVXor,pattern BVAnd,pattern BVOr,bvbin,bvadd,bvsub,bvmul,bvurem,bvsrem,bvudiv,bvsdiv,bvshl,bvlshr,bvashr,bvxor,bvand,bvor,
pattern BVUn,pattern BVNot,pattern BVNeg,
bvun,bvnot,bvneg,
pattern Concat,pattern Extract,concat',extract',extractChecked,extractUntypedStart,extractUntyped,
pattern Select,pattern Store,pattern ConstArray,select,select1,store,store1,constArray,
pattern Mk,mk,pattern Is,is,(.#.),
pattern Divisible,divisible,
getExpr,
assert,checkSat,checkSatWith,
B.CheckSatResult(..),
B.CheckSatLimits(..),noLimits,
assertId,getUnsatCore,B.ClauseId(),
assertPartition,B.Partition(..),
getInterpolant,
getProof,analyzeProof,
push,pop,stack,
getValue,
getModel,
B.Model(),
modelEvaluate,
registerDatatype,
Type(..),Repr(..),GetType(..),bool,int,real,bitvec,array,dt,dt',
Nat(..),Natural(..),nat,natT,reifyNat,
List(..),reifyList,(.:.),nil,
comment,simplify
) where
import Language.SMTLib2.Internals.Type
import Language.SMTLib2.Internals.Type.Nat
import Language.SMTLib2.Internals.Type.List hiding (nil)
import qualified Language.SMTLib2.Internals.Type.List as List
import Language.SMTLib2.Internals.Monad
import qualified Language.SMTLib2.Internals.Expression as E
import qualified Language.SMTLib2.Internals.Proof as P
import qualified Language.SMTLib2.Internals.Backend as B
import Language.SMTLib2.Internals.Interface
import Language.SMTLib2.Internals.Embed
import Language.SMTLib2.Strategy
import Control.Monad.State.Strict
setOption :: B.Backend b => B.SMTOption -> SMT b ()
setOption opt = embedSMT $ B.setOption opt
getInfo :: B.Backend b => B.SMTInfo i -> SMT b i
getInfo info = embedSMT $ B.getInfo info
assert :: (B.Backend b,HasMonad expr,MatchMonad expr (SMT b),MonadResult expr ~ B.Expr b BoolType)
=> expr -> SMT b ()
assert e = embedM e >>= embedSMT . B.assert
assertId :: (B.Backend b,HasMonad expr,MatchMonad expr (SMT b),MonadResult expr ~ B.Expr b BoolType)
=> expr -> SMT b (B.ClauseId b)
assertId e = embedM e >>= embedSMT . B.assertId
assertPartition :: (B.Backend b,HasMonad expr,MatchMonad expr (SMT b),
MonadResult expr ~ B.Expr b BoolType)
=> expr -> B.Partition -> SMT b ()
assertPartition e p = do
e' <- embedM e
embedSMT (B.assertPartition e' p)
checkSat :: B.Backend b => SMT b B.CheckSatResult
checkSat = embedSMT (B.checkSat Nothing noLimits)
checkSatWith :: B.Backend b => Maybe Tactic -> B.CheckSatLimits -> SMT b B.CheckSatResult
checkSatWith tactic limits = embedSMT (B.checkSat tactic limits)
noLimits :: B.CheckSatLimits
noLimits = B.CheckSatLimits Nothing Nothing
getValue :: (B.Backend b,HasMonad expr,MatchMonad expr (SMT b),
MonadResult expr ~ B.Expr b t)
=> expr -> SMT b (Value t)
getValue e = embedM e >>= embedSMT . B.getValue
getModel :: B.Backend b => SMT b (B.Model b)
getModel = embedSMT B.getModel
modelEvaluate :: (B.Backend b,HasMonad expr,MatchMonad expr (SMT b),
MonadResult expr ~ B.Expr b t)
=> B.Model b -> expr -> SMT b (Value t)
modelEvaluate mdl e = embedM e >>= embedSMT . B.modelEvaluate mdl
push :: B.Backend b => SMT b ()
push = embedSMT B.push
pop :: B.Backend b => SMT b ()
pop = embedSMT B.pop
stack :: B.Backend b => SMT b a -> SMT b a
stack act = do
push
res <- act
pop
return res
declareVar :: B.Backend b => Repr t
-> SMT b (B.Expr b t)
declareVar tp = declareVar' tp >>= embedSMT . B.toBackend . E.Var
declareVarNamed :: B.Backend b => Repr t
-> String
-> SMT b (B.Expr b t)
declareVarNamed tp name = declareVarNamed' tp name >>= embedSMT . B.toBackend . E.Var
defineVar :: (B.Backend b,HasMonad expr,MatchMonad expr (SMT b),
MonadResult expr ~ B.Expr b t)
=> expr
-> SMT b (B.Expr b t)
defineVar e = embedM e >>= defineVar' >>= embedSMT . B.toBackend . E.Var
defineVarNamed :: (B.Backend b,HasMonad expr,MatchMonad expr (SMT b),
MonadResult expr ~ B.Expr b t)
=> String
-> expr
-> SMT b (B.Expr b t)
defineVarNamed name e = embedM e >>= defineVarNamed' name >>= embedSMT . B.toBackend . E.Var
declareFun :: B.Backend b
=> List Repr args
-> Repr res
-> SMT b (B.Fun b '(args,res))
declareFun args res = embedSMT $ B.declareFun args res Nothing
declareFunNamed :: B.Backend b => List Repr args
-> Repr res
-> String
-> SMT b (B.Fun b '(args,res))
declareFunNamed args res name = embedSMT $ B.declareFun args res (Just name)
defineFun :: (B.Backend b,HasMonad def,MatchMonad def (SMT b),
MonadResult def ~ B.Expr b res)
=> List Repr args
-> (List (B.Expr b) args -> def)
-> SMT b (B.Fun b '(args,res))
defineFun tps f = do
args <- List.mapM (\tp -> embedSMT $ B.createFunArg tp Nothing) tps
args' <- List.mapM (embedSMT . B.toBackend . E.FVar) args
res <- embedM $ f args'
embedSMT $ B.defineFun Nothing args res
defineFunNamed :: (B.Backend b,HasMonad def,MatchMonad def (SMT b),
MonadResult def ~ B.Expr b res)
=> String
-> List Repr args
-> (List (B.Expr b) args -> def)
-> SMT b (B.Fun b '(args,res))
defineFunNamed name tps f = do
args <- List.mapM (\tp -> embedSMT $ B.createFunArg tp Nothing) tps
args' <- List.mapM (embedSMT . B.toBackend . E.FVar) args
res <- embedM $ f args'
embedSMT $ B.defineFun (Just name) args res
getUnsatCore :: B.Backend b => SMT b [B.ClauseId b]
getUnsatCore = embedSMT B.getUnsatCore
getInterpolant :: B.Backend b => SMT b (B.Expr b BoolType)
getInterpolant = embedSMT B.interpolate
getExpr :: (B.Backend b) => B.Expr b tp
-> SMT b (E.Expression
(B.Var b)
(B.QVar b)
(B.Fun b)
(B.FunArg b)
(B.LVar b)
(B.Expr b) tp)
getExpr e = do
st <- get
return $ B.fromBackend (backend st) e
comment :: (B.Backend b) => String -> SMT b ()
comment msg = embedSMT $ B.comment msg
simplify :: B.Backend b => B.Expr b tp -> SMT b (B.Expr b tp)
simplify e = embedSMT $ B.simplify e
getProof :: B.Backend b => SMT b (B.Proof b)
getProof = embedSMT B.getProof
analyzeProof :: B.Backend b => B.Proof b -> SMT b (P.Proof String (B.Expr b) (B.Proof b))
analyzeProof pr = do
st <- get
return $ B.analyzeProof (backend st) pr