module ToySolver.SMT
(
Solver
, newSolver
, Exception (..)
, SSym (..)
, ssymArity
, Sort (..)
, sBool
, sReal
, FunType
, Expr (..)
, exprSort
, FSym
, declareSSym
, declareSort
, VASortFun
, declareFSym
, declareFun
, declareConst
, VAFun
, assert
, assertNamed
, getGlobalDeclarations
, setGlobalDeclarations
, checkSAT
, checkSATAssuming
, push
, pop
, Model
, Value (..)
, getModel
, eval
, valSort
, FunDef (..)
, evalFSym
, getUnsatAssumptions
, getUnsatCore
) where
import qualified Control.Exception as E
import Control.Monad
import Control.Monad.Trans
import Control.Monad.Trans.Except
import Data.Either
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import Data.IORef
import Data.List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe (catMaybes)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Typeable
import Data.VectorSpace
import ToySolver.Data.Delta
import ToySolver.Data.Boolean
import ToySolver.Data.BoolExpr
import ToySolver.Data.OrdRel
import qualified ToySolver.Data.LA as LA
import qualified ToySolver.Internal.Data.Vec as Vec
import qualified ToySolver.SAT as SAT
import ToySolver.SAT.TheorySolver
import qualified ToySolver.SAT.TseitinEncoder as Tseitin
import qualified ToySolver.Arith.Simplex2 as Simplex2
import qualified ToySolver.EUF.EUFSolver as EUF
type FSym = String
data SSym
= SSymBool
| SSymReal
| SSymUserDeclared String !Int
deriving (Show, Eq, Ord)
ssymArity :: SSym -> Int
ssymArity SSymBool = 0
ssymArity SSymReal = 0
ssymArity (SSymUserDeclared _ ar) = ar
data Sort = Sort SSym [Sort]
deriving (Show, Eq, Ord)
sBool :: Sort
sBool = Sort SSymBool []
sReal :: Sort
sReal = Sort SSymReal []
type FunType = ([Sort],Sort)
data Expr
= EAp FSym [Expr]
| EFrac Rational
deriving (Show, Eq, Ord)
instance MonotoneBoolean Expr where
true = EAp "true" []
false = EAp "false" []
andB = EAp "and"
orB = EAp "or"
instance Complement Expr where
notB x = EAp "not" [x]
instance IfThenElse Expr Expr where
ite x y z = EAp "ite" [x,y,z]
instance Boolean Expr where
x .=>. y = EAp "=>" [x,y]
x .<=>. y = EAp "=" [x,y]
instance Num Expr where
x + y = EAp "+" [x,y]
x y = EAp "-" [x,y]
x * y = EAp "*" [x,y]
negate x = EAp "-" [x]
abs x = error "Num{ToySolver.SMT.Expr}.abs is not implemented"
signum x = error "Num{ToySolver.SMT.Expr}.signum is not implemented"
fromInteger x = EFrac (fromInteger x)
instance Fractional Expr where
x / y = EAp "/" [x,y]
fromRational x = EFrac x
instance IsEqRel Expr Expr where
a .==. b = EAp "=" [a,b]
a ./=. b = notB (a .==. b)
instance IsOrdRel Expr Expr where
a .<. b = EAp "<" [a,b]
a .>. b = EAp ">" [a,b]
a .<=. b = EAp "<=" [a,b]
a .>=. b = EAp ">=" [a,b]
data FDef
= FBoolVar SAT.Var
| FLRAVar LA.Var
| FEUFFun FunType EUF.FSym
deriving (Show)
data Exception
= Error String
| Unsupported
deriving (Show, Typeable)
instance E.Exception Exception
data Solver
= Solver
{ smtSAT :: !SAT.Solver
, smtEnc :: !Tseitin.Encoder
, smtEUF :: !EUF.Solver
, smtLRA :: !(Simplex2.GenericSolver (Delta Rational))
, smtEUFAtomDefs :: !(IORef (Map (EUF.Term, EUF.Term) SAT.Var, IntMap (EUF.Term, EUF.Term)))
, smtLRAAtomDefs :: !(IORef (Map (LA.Var, Rational) (SAT.Lit, SAT.Lit, SAT.Lit), IntMap (LA.Atom Rational)))
, smtBoolTermDefs :: !(IORef (Map EUF.Term SAT.Lit, IntMap EUF.Term))
, smtRealTermDefs :: !(IORef (Map (LA.Expr Rational) EUF.FSym, IntMap (LA.Expr Rational)))
, smtEUFTrue :: !EUF.Term
, smtEUFFalse :: !EUF.Term
, smtEUFModel :: !(IORef EUF.Model)
, smtLRAModel :: !(IORef Simplex2.Model)
, smtGlobalDeclarationsRef :: !(IORef Bool)
, smtFDefs :: !(IORef (Map FSym FDef))
, smtNamedAssertions :: !(IORef (Map String SAT.Lit))
, smtAssertionStack :: !(Vec.Vec AssertionLevel)
, smtUnsatAssumptions :: !(IORef [Expr])
, smtUnsatCore :: !(IORef [String])
}
data AssertionLevel
= AssertionLevel
{ alSavedNamedAssertions :: Map String SAT.Lit
, alSavedFDefs :: Maybe (Map FSym FDef)
, alSelector :: SAT.Lit
}
newSolver :: IO Solver
newSolver = do
sat <- SAT.newSolver
enc <- Tseitin.newEncoder sat
euf <- EUF.newSolver
lra <- Simplex2.newSolver
litTrue <- Tseitin.encodeConj enc []
let litFalse = litTrue
eufTrue <- EUF.newConst euf
eufFalse <- EUF.newConst euf
EUF.assertNotEqual euf eufTrue eufFalse
divByZero <- EUF.newFSym euf
eufAtomDefs <- newIORef (Map.empty, IntMap.empty)
lraAtomDefs <- newIORef (Map.empty, IntMap.empty)
boolTermDefs <- newIORef $
( Map.fromList [(eufTrue, litTrue), (eufFalse, litFalse)]
, IntMap.fromList [(litTrue, eufTrue), (litFalse, eufFalse)]
)
realTermDefs <- newIORef (Map.empty, IntMap.empty)
eufModelRef <- newIORef (undefined :: EUF.Model)
lraModelRef <- newIORef (undefined :: Simplex2.Model)
globalDeclarationsRef <- newIORef False
fdefs <- newIORef $ Map.singleton "_/0" (FEUFFun ([sReal], sReal) divByZero)
conflictTheory <- newIORef True
let tsolver =
TheorySolver
{ thAssertLit = \_ l -> do
(_, defsLRA) <- readIORef lraAtomDefs
(_, defsEUF) <- readIORef eufAtomDefs
case IntMap.lookup l defsLRA of
Just atom -> do
Simplex2.assertAtomEx' lra atom (Just l)
return True
Nothing ->
case IntMap.lookup (SAT.litVar l) defsEUF of
Just (t1,t2) -> do
if SAT.litPolarity l then do
EUF.assertEqual' euf t1 t2 (Just l)
return True
else do
EUF.assertNotEqual' euf t1 t2 (Just l)
return True
Nothing ->
return True
, thCheck = \callback -> do
b <- Simplex2.check lra
if b then do
b2 <- EUF.check euf
if b2 then do
(_, defsEUF) <- readIORef eufAtomDefs
liftM isRight $ runExceptT $ do
forM_ (IntMap.toList defsEUF) $ \(v, (t1, t2)) -> do
b3 <- lift $ EUF.areEqual euf t1 t2
when b3 $ do
b4 <- lift $ callback v
unless b4 $ throwE ()
else do
writeIORef conflictTheory False
return b2
else do
writeIORef conflictTheory True
return False
, thExplain = \m -> do
case m of
Nothing -> do
b <- readIORef conflictTheory
if b then
liftM IntSet.toList $ Simplex2.explain lra
else
liftM IntSet.toList $ EUF.explain euf Nothing
Just v -> do
(_, defsEUF) <- readIORef eufAtomDefs
case IntMap.lookup v defsEUF of
Nothing -> error "should not happen"
Just (t1,t2) -> liftM IntSet.toList $ EUF.explain euf (Just (t1,t2))
, thPushBacktrackPoint = do
Simplex2.pushBacktrackPoint lra
EUF.pushBacktrackPoint euf
, thPopBacktrackPoint = do
Simplex2.popBacktrackPoint lra
EUF.popBacktrackPoint euf
, thConstructModel = do
writeIORef eufModelRef =<< EUF.getModel euf
writeIORef lraModelRef =<< Simplex2.getModel lra
return ()
}
SAT.setTheory sat tsolver
named <- newIORef Map.empty
stack <- Vec.new
unsatAssumptionsRef <- newIORef undefined
unsatCoreRef <- newIORef undefined
return $
Solver
{ smtSAT = sat
, smtEnc = enc
, smtEUF = euf
, smtLRA = lra
, smtEUFAtomDefs = eufAtomDefs
, smtLRAAtomDefs = lraAtomDefs
, smtBoolTermDefs = boolTermDefs
, smtRealTermDefs = realTermDefs
, smtEUFTrue = eufTrue
, smtEUFFalse = eufFalse
, smtEUFModel = eufModelRef
, smtLRAModel = lraModelRef
, smtGlobalDeclarationsRef = globalDeclarationsRef
, smtFDefs = fdefs
, smtNamedAssertions = named
, smtAssertionStack = stack
, smtUnsatAssumptions = unsatAssumptionsRef
, smtUnsatCore = unsatCoreRef
}
declareSSym :: Solver -> String -> Int -> IO SSym
declareSSym solver name arity = return (SSymUserDeclared name arity)
declareSort :: VASortFun a => Solver -> String -> Int -> IO a
declareSort solver name arity = do
ssym <- declareSSym solver name arity
let f = withSortVArgs (Sort ssym)
unless (arityVASortFun f == arity) $ do
E.throwIO $ Error "ToySolver.SMT.declareSort: argument number error"
return f
class VASortFun a where
withSortVArgs :: ([Sort] -> Sort) -> a
arityVASortFun :: a -> Int
instance VASortFun Sort where
withSortVArgs k = k []
arityVASortFun f = 0
instance VASortFun a => VASortFun (Sort -> a) where
withSortVArgs k x = withSortVArgs (\xs -> k (x : xs))
arityVASortFun f = arityVASortFun (f undefined) + 1
declareFSym :: Solver -> String -> [Sort] -> Sort -> IO FSym
declareFSym solver f xs y = do
fdefs <- readIORef (smtFDefs solver)
when (f `Map.member` fdefs) $ do
E.throwIO $ Error $ "function symbol " ++ f ++ " is already used"
fdef <-
case (xs, y) of
([], Sort SSymBool []) -> do
v <- SAT.newVar (smtSAT solver)
return (FBoolVar v)
([], Sort SSymReal []) -> do
v <- Simplex2.newVar (smtLRA solver)
return (FLRAVar v)
_ -> do
v <- EUF.newFSym (smtEUF solver)
return (FEUFFun (xs,y) v)
writeIORef (smtFDefs solver) $ Map.insert f fdef fdefs
return f
class VAFun a where
withVArgs :: ([Expr] -> Expr) -> a
arityVAFun :: a -> Int
instance VAFun Expr where
withVArgs k = k []
arityVAFun _ = 0
instance VAFun a => VAFun (Expr -> a) where
withVArgs k x = withVArgs (\xs -> k (x : xs))
arityVAFun f = arityVAFun (f undefined) + 1
declareFun :: VAFun a => Solver -> String -> [Sort] -> Sort -> IO a
declareFun solver name ps r = do
fsym <- declareFSym solver name ps r
let f = withVArgs (EAp fsym)
unless (arityVAFun f == length ps) $ do
E.throwIO $ Error "ToySolver.SMT.declareFun: argument number error"
return f
declareConst :: Solver -> String -> Sort -> IO Expr
declareConst solver name s = declareFun solver name [] s
assert :: Solver -> Expr -> IO ()
assert solver e = do
formula <- exprToFormula solver e
n <- Vec.getSize (smtAssertionStack solver)
if n>0 then do
assertionLevel <- Vec.peek (smtAssertionStack solver)
Tseitin.addFormula (smtEnc solver) $ Atom (alSelector assertionLevel) .=>. formula
else
Tseitin.addFormula (smtEnc solver) formula
assertNamed :: Solver -> String -> Expr -> IO ()
assertNamed solver name e = do
lit <- Tseitin.encodeFormula (smtEnc solver) =<< exprToFormula solver e
modifyIORef (smtNamedAssertions solver) (Map.insert name lit)
getGlobalDeclarations :: Solver -> IO Bool
getGlobalDeclarations solver = readIORef (smtGlobalDeclarationsRef solver)
setGlobalDeclarations :: Solver -> Bool -> IO ()
setGlobalDeclarations solver = writeIORef (smtGlobalDeclarationsRef solver)
exprSort :: Solver -> Expr -> IO Sort
exprSort solver e = do
fdefs <- readIORef (smtFDefs solver)
return $! exprSort' fdefs e
exprSort' :: Map FSym FDef -> Expr -> Sort
exprSort' _fdefs (EFrac _) = Sort SSymReal []
exprSort' fdefs (EAp f xs)
| f `Set.member` Set.fromList ["true","false","and","or","not","=>","=",">=","<=",">","<"] = Sort SSymBool []
| f `Set.member` Set.fromList ["+", "-", "*", "/"] = Sort SSymReal []
| f == "ite" = exprSort' fdefs (xs !! 1)
| otherwise =
case fdefs Map.! f of
FBoolVar _ -> Sort SSymBool []
FLRAVar _ -> Sort SSymReal []
FEUFFun (_,s) _ -> s
exprToFormula :: Solver -> Expr -> IO Tseitin.Formula
exprToFormula solver (EAp "true" []) = return true
exprToFormula solver (EAp "false" []) = return false
exprToFormula solver (EAp "and" xs) =
liftM andB $ mapM (exprToFormula solver) xs
exprToFormula solver (EAp "or" xs) =
liftM orB $ mapM (exprToFormula solver) xs
exprToFormula solver (EAp "not" [x]) =
liftM notB $ exprToFormula solver x
exprToFormula solver (EAp "not" _) = undefined
exprToFormula solver (EAp "=>" [e1,e2]) = do
b1 <- exprToFormula solver e1
b2 <- exprToFormula solver e2
return $ b1 .=>. b2
exprToFormula solver (EAp "ite" [e1,e2,e3]) = do
b1 <- exprToFormula solver e1
b2 <- exprToFormula solver e2
b3 <- exprToFormula solver e3
return $ ite b1 b2 b3
exprToFormula solver (EAp "=" []) = return true
exprToFormula solver (EAp "=" xs) =
chain solver (abstractEq solver) xs
exprToFormula solver (EAp "distinct" []) = return true
exprToFormula solver (EAp "distinct" xs) =
pairwise solver (\e1 e2 -> liftM notB (abstractEq solver e1 e2)) xs
exprToFormula solver (EAp ">=" xs) = do
let f e1 e2 = do
e1' <- exprToLRAExpr solver e1
e2' <- exprToLRAExpr solver e2
liftM Atom $ abstractLRAAtom solver (e1' .>=. e2')
chain solver f xs
exprToFormula solver (EAp "<=" xs) = do
let f e1 e2 = do
e1' <- exprToLRAExpr solver e1
e2' <- exprToLRAExpr solver e2
liftM Atom $ abstractLRAAtom solver (e1' .<=. e2')
chain solver f xs
exprToFormula solver (EAp ">" xs) = do
let f e1 e2 = do
e1' <- exprToLRAExpr solver e1
e2' <- exprToLRAExpr solver e2
liftM Atom $ abstractLRAAtom solver (e1' .>. e2')
chain solver f xs
exprToFormula solver (EAp "<" xs) = do
let f e1 e2 = do
e1' <- exprToLRAExpr solver e1
e2' <- exprToLRAExpr solver e2
liftM Atom $ abstractLRAAtom solver (e1' .<. e2')
chain solver f xs
exprToFormula solver (EAp f []) = do
fdefs <- readIORef (smtFDefs solver)
case Map.lookup f fdefs of
Just (FBoolVar v) -> return (Atom v)
Just _ -> E.throwIO $ Error "non Bool constant appears in a boolean context"
Nothing -> E.throwIO $ Error $ "unknown function symbol: " ++ show f
exprToFormula solver (EAp f xs) = do
e' <- exprToEUFTerm solver f xs
formulaFromEUFTerm solver e'
chain :: Solver -> (Expr -> Expr -> IO Tseitin.Formula) -> [Expr] -> IO Tseitin.Formula
chain _ _ [] = return true
chain solver p xs = liftM andB $ mapM (uncurry p) (zip xs (tail xs))
pairwise :: Solver -> (Expr -> Expr -> IO Tseitin.Formula) -> [Expr] -> IO Tseitin.Formula
pairwise _ _ [] = return true
pairwise solver p xs = liftM andB $ mapM (uncurry p) (pairs xs)
abstractEq :: Solver -> Expr -> Expr -> IO Tseitin.Formula
abstractEq solver e1 e2 = do
s <- exprSort solver e1
case s of
(Sort SSymBool _) -> do
b1 <- exprToFormula solver e1
b2 <- exprToFormula solver e2
return $ b1 .<=>. b2
(Sort SSymReal _) -> do
e1' <- exprToLRAExpr solver e1
e2' <- exprToLRAExpr solver e2
liftM Atom $ abstractLRAAtom solver (e1' .==. e2')
(Sort (SSymUserDeclared _ _) _) -> do
e1' <- exprToEUFArg solver e1
e2' <- exprToEUFArg solver e2
liftM Atom $ abstractEUFAtom solver (e1',e2')
exprToLRAExpr :: Solver -> Expr -> IO (LA.Expr Rational)
exprToLRAExpr solver (EFrac r) = return (LA.constant r)
exprToLRAExpr solver (EAp "-" []) = E.throwIO $ Error "ToySolver.SMT: nullary '-' function"
exprToLRAExpr solver (EAp "-" [x]) = liftM negateV $ exprToLRAExpr solver x
exprToLRAExpr solver (EAp "-" (x:xs)) = do
x' <- exprToLRAExpr solver x
xs' <- mapM (exprToLRAExpr solver) xs
return $ foldl' (^-^) x' xs'
exprToLRAExpr solver (EAp "+" xs) = liftM sumV $ mapM (exprToLRAExpr solver) xs
exprToLRAExpr solver (EAp "*" xs) = liftM (foldr mult (LA.constant 1)) $ mapM (exprToLRAExpr solver) xs
where
mult e1 e2
| Just c <- LA.asConst e1 = c *^ e2
| Just c <- LA.asConst e2 = c *^ e1
| otherwise = E.throw $ Error "non-linear multiplication is not supported"
exprToLRAExpr solver (EAp "/" [x,y]) = do
y' <- exprToLRAExpr solver y
case LA.asConst y' of
Nothing -> E.throwIO $ Error "division by non-constant is not supported"
Just 0 -> do
lraExprFromTerm solver =<< exprToEUFTerm solver "_/0" [x]
Just c -> do
x' <- exprToLRAExpr solver x
return $ (1/c) *^ x'
exprToLRAExpr solver (EAp "ite" [c,t,e]) = do
c' <- exprToFormula solver c
ret <- liftM LA.var $ Simplex2.newVar (smtLRA solver)
t' <- exprToLRAExpr solver t
e' <- exprToLRAExpr solver e
c1 <- abstractLRAAtom solver (ret .==. t')
c2 <- abstractLRAAtom solver (ret .==. e')
Tseitin.addFormula (smtEnc solver) $ ite c' (Atom c1) (Atom c2)
return ret
exprToLRAExpr solver (EAp f xs) =
lraExprFromTerm solver =<< exprToEUFTerm solver f xs
abstractLRAAtom :: Solver -> LA.Atom Rational -> IO SAT.Lit
abstractLRAAtom solver atom = do
(v,op,rhs) <- Simplex2.simplifyAtom (smtLRA solver) atom
(tbl,defs) <- readIORef (smtLRAAtomDefs solver)
(vLt, vEq, vGt) <-
case Map.lookup (v,rhs) tbl of
Just (vLt, vEq, vGt) -> return (vLt, vEq, vGt)
Nothing -> do
vLt <- SAT.newVar (smtSAT solver)
vEq <- SAT.newVar (smtSAT solver)
vGt <- SAT.newVar (smtSAT solver)
SAT.addClause (smtSAT solver) [vLt,vEq,vGt]
SAT.addClause (smtSAT solver) [vLt, vEq]
SAT.addClause (smtSAT solver) [vLt, vGt]
SAT.addClause (smtSAT solver) [vEq, vGt]
let xs = IntMap.fromList
[ (vEq, LA.var v .==. LA.constant rhs)
, (vLt, LA.var v .<. LA.constant rhs)
, (vGt, LA.var v .>. LA.constant rhs)
, (vLt, LA.var v .>=. LA.constant rhs)
, (vGt, LA.var v .<=. LA.constant rhs)
]
writeIORef (smtLRAAtomDefs solver) (Map.insert (v,rhs) (vLt, vEq, vGt) tbl, IntMap.union xs defs)
return (vLt, vEq, vGt)
case op of
Lt -> return vLt
Gt -> return vGt
Eql -> return vEq
Le -> return (vGt)
Ge -> return (vLt)
NEq -> return (vEq)
lraExprToEUFTerm :: Solver -> LA.Expr Rational -> IO EUF.Term
lraExprToEUFTerm solver e = do
(realToFSym, fsymToReal) <- readIORef (smtRealTermDefs solver)
case Map.lookup e realToFSym of
Just c -> return (EUF.TApp c [])
Nothing -> do
c <- EUF.newFSym (smtEUF solver)
forM_ (IntMap.toList fsymToReal) $ \(d, d_lra) -> do
b1 <- abstractEUFAtom solver (EUF.TApp c [], EUF.TApp d [])
b2 <- abstractLRAAtom solver (e .==. d_lra)
Tseitin.addFormula (smtEnc solver) (Atom b1 .<=>. Atom b2)
writeIORef (smtRealTermDefs solver) $
( Map.insert e c realToFSym
, IntMap.insert c e fsymToReal
)
return (EUF.TApp c [])
lraExprFromTerm :: Solver -> EUF.Term -> IO (LA.Expr Rational)
lraExprFromTerm solver t = do
(realToFSym, fsymToReal) <- readIORef (smtRealTermDefs solver)
c <- EUF.termToFSym (smtEUF solver) t
case IntMap.lookup c fsymToReal of
Just e -> return e
Nothing -> do
v <- Simplex2.newVar (smtLRA solver)
let e = LA.var v
forM_ (IntMap.toList fsymToReal) $ \(d, d_lra) -> do
b1 <- abstractEUFAtom solver (EUF.TApp c [], EUF.TApp d [])
b2 <- abstractLRAAtom solver (e .==. d_lra)
Tseitin.addFormula (smtEnc solver) (Atom b1 .<=>. Atom b2)
writeIORef (smtRealTermDefs solver) $
( Map.insert e c realToFSym
, IntMap.insert c e fsymToReal
)
return e
exprToEUFTerm :: Solver -> FSym -> [Expr] -> IO EUF.Term
exprToEUFTerm solver "ite" [c,t,e] = do
c' <- exprToFormula solver c
ret <- EUF.newConst (smtEUF solver)
t' <- exprToEUFArg solver t
e' <- exprToEUFArg solver e
c1 <- abstractEUFAtom solver (ret, t')
c2 <- abstractEUFAtom solver (ret, e')
Tseitin.addFormula (smtEnc solver) $ ite c' (Atom c1) (Atom c2)
return ret
exprToEUFTerm solver f xs = do
fdefs <- readIORef (smtFDefs solver)
case Map.lookup f fdefs of
Just (FBoolVar v) -> formulaToEUFTerm solver (Atom v)
Just (FLRAVar v) -> lraExprToEUFTerm solver (LA.var v)
Just (FEUFFun (ps,_) fsym) -> do
unless (length ps == length xs) $ do
E.throwIO $ Error "argument number error"
liftM (EUF.TApp fsym) $ mapM (exprToEUFArg solver) xs
_ -> E.throw $ Error $ "unknown function symbol: " ++ show f
exprToEUFArg :: Solver -> Expr -> IO EUF.Term
exprToEUFArg solver (EFrac r) = lraExprToEUFTerm solver (LA.constant r)
exprToEUFArg solver e@(EAp f xs) = do
Sort s _ <- exprSort solver e
case s of
SSymBool -> formulaToEUFTerm solver =<< exprToFormula solver e
SSymReal -> lraExprToEUFTerm solver =<< exprToLRAExpr solver e
_ -> exprToEUFTerm solver f xs
abstractEUFAtom :: Solver -> (EUF.Term, EUF.Term) -> IO SAT.Lit
abstractEUFAtom solver (t1,t2) | t1 > t2 = abstractEUFAtom solver (t2,t1)
abstractEUFAtom solver (t1,t2) = do
(tbl,defs) <- readIORef (smtEUFAtomDefs solver)
case Map.lookup (t1,t2) tbl of
Just v -> return v
Nothing -> do
v <- SAT.newVar (smtSAT solver)
writeIORef (smtEUFAtomDefs solver) (Map.insert (t1,t2) v tbl, IntMap.insert v (t1,t2) defs)
return v
formulaToEUFTerm :: Solver -> Tseitin.Formula -> IO EUF.Term
formulaToEUFTerm solver formula = do
lit <- Tseitin.encodeFormula (smtEnc solver) formula
(_, boolToTerm) <- readIORef (smtBoolTermDefs solver)
case IntMap.lookup lit boolToTerm of
Just t -> return t
Nothing -> do
t <- EUF.newConst (smtEUF solver)
connectBoolTerm solver lit t
return t
formulaFromEUFTerm :: Solver -> EUF.Term -> IO Tseitin.Formula
formulaFromEUFTerm solver t = do
(termToBool, _) <- readIORef (smtBoolTermDefs solver)
case Map.lookup t termToBool of
Just lit -> return (Atom lit)
Nothing -> do
lit <- SAT.newVar (smtSAT solver)
connectBoolTerm solver lit t
return $ Atom lit
connectBoolTerm :: Solver -> SAT.Lit -> EUF.Term -> IO ()
connectBoolTerm solver lit t = do
lit1 <- abstractEUFAtom solver (t, smtEUFTrue solver)
lit2 <- abstractEUFAtom solver (t, smtEUFFalse solver)
SAT.addClause (smtSAT solver) [lit, lit1]
SAT.addClause (smtSAT solver) [lit1, lit]
SAT.addClause (smtSAT solver) [lit, lit2]
SAT.addClause (smtSAT solver) [lit2, lit]
modifyIORef (smtBoolTermDefs solver) $ \(termToBool, boolToTerm) ->
( Map.insert t lit termToBool
, IntMap.insert lit t boolToTerm
)
checkSAT :: Solver -> IO Bool
checkSAT solver = checkSATAssuming solver []
checkSATAssuming :: Solver -> [Expr] -> IO Bool
checkSATAssuming solver xs = do
l <- getContextLit solver
named <- readIORef (smtNamedAssertions solver)
ref <- newIORef IntMap.empty
ls <- forM xs $ \x -> do
b <- Tseitin.encodeFormula (smtEnc solver) =<< exprToFormula solver x
modifyIORef ref (IntMap.insert b x)
return b
ret <- SAT.solveWith (smtSAT solver) (l : ls ++ Map.elems named)
if ret then do
writeIORef (smtUnsatAssumptions solver) undefined
writeIORef (smtUnsatCore solver) undefined
else do
m1 <- readIORef ref
let m2 = IntMap.fromList [(lit, name) | (name, lit) <- Map.toList named]
failed <- SAT.getFailedAssumptions (smtSAT solver)
writeIORef (smtUnsatAssumptions solver) $ catMaybes [IntMap.lookup l m1 | l <- failed]
writeIORef (smtUnsatCore solver) $ catMaybes [IntMap.lookup l m2 | l <- failed]
return ret
getContextLit :: Solver -> IO SAT.Lit
getContextLit solver = do
n <- Vec.getSize (smtAssertionStack solver)
if n>0 then do
assertionLevel <- Vec.peek (smtAssertionStack solver)
return $ alSelector assertionLevel
else
Tseitin.encodeConj (smtEnc solver) []
push :: Solver -> IO ()
push solver = do
l1 <- getContextLit solver
l2 <- SAT.newVar (smtSAT solver)
SAT.addClause (smtSAT solver) [l2, l1]
globalDeclarations <- readIORef (smtGlobalDeclarationsRef solver)
named <- readIORef (smtNamedAssertions solver)
fdefs <- readIORef (smtFDefs solver)
let newLevel =
AssertionLevel
{ alSavedNamedAssertions = named
, alSavedFDefs = if globalDeclarations then Nothing else Just fdefs
, alSelector = l2
}
Vec.push (smtAssertionStack solver) newLevel
pop :: Solver -> IO ()
pop solver = do
n <- Vec.getSize (smtAssertionStack solver)
if n==0 then
E.throwIO $ Error $ "cannot pop first assertion level"
else do
assertionLevel <- Vec.unsafePop (smtAssertionStack solver)
SAT.addClause (smtSAT solver) [ alSelector assertionLevel]
writeIORef (smtNamedAssertions solver) (alSavedNamedAssertions assertionLevel)
case alSavedFDefs assertionLevel of
Nothing -> return ()
Just fdefs -> writeIORef (smtFDefs solver) fdefs
return ()
data Model
= Model
{ mDefs :: !(Map FSym FDef)
, mBoolModel :: !SAT.Model
, mLRAModel :: !Simplex2.Model
, mEUFModel :: !EUF.Model
, mEUFTrue :: !EUF.Entity
, mEUFFalse :: !EUF.Entity
, mEntityToRational :: !(IntMap Rational)
, mRationalToEntity :: !(Map Rational EUF.Entity)
}
deriving (Show)
data Value
= ValRational !Rational
| ValBool !Bool
| ValUninterpreted !Int !Sort
deriving (Eq, Show)
getModel :: Solver -> IO Model
getModel solver = do
defs <- readIORef (smtFDefs solver)
boolModel <- SAT.getModel (smtSAT solver)
lraModel <- readIORef (smtLRAModel solver)
eufModel <- readIORef (smtEUFModel solver)
(_, fsymToReal) <- readIORef (smtRealTermDefs solver)
let xs = [(e, LA.evalExpr lraModel lraExpr) | (fsym, lraExpr) <- IntMap.toList fsymToReal, let e = EUF.evalAp eufModel fsym [], e /= EUF.mUnspecified eufModel]
return $
Model
{ mDefs = defs
, mBoolModel = boolModel
, mLRAModel = lraModel
, mEUFModel = eufModel
, mEUFTrue = EUF.eval eufModel (smtEUFTrue solver)
, mEUFFalse = EUF.eval eufModel (smtEUFFalse solver)
, mEntityToRational = IntMap.fromList xs
, mRationalToEntity = Map.fromList [(r,e) | (e,r) <- xs]
}
eval :: Model -> Expr -> Value
eval m (EFrac r) = ValRational r
eval m (EAp "true" []) = ValBool True
eval m (EAp "false" []) = ValBool False
eval m (EAp "ite" [a,b,c]) = if valToBool m (eval m a) then eval m b else eval m c
eval m (EAp "and" xs) = ValBool $ and $ map (valToBool m . eval m) xs
eval m (EAp "or" xs) = ValBool $ or $ map (valToBool m . eval m) xs
eval m (EAp "not" [x]) = ValBool $ not $ valToBool m $ eval m x
eval m (EAp "=>" [x,y]) = ValBool $ valToBool m (eval m x) .=>. valToBool m (eval m y)
eval m (EAp "<=" [x,y]) = ValBool $ valToRational m (eval m x) <= valToRational m (eval m y)
eval m (EAp ">=" [x,y]) = ValBool $ valToRational m (eval m x) >= valToRational m (eval m y)
eval m (EAp ">" [x,y]) = ValBool $ valToRational m (eval m x) > valToRational m (eval m y)
eval m (EAp "<" [x,y]) = ValBool $ valToRational m (eval m x) < valToRational m (eval m y)
eval m (EAp "+" xs) = ValRational $ sum $ map (valToRational m . eval m) xs
eval m (EAp "-" [x]) = ValRational $ negate $ valToRational m (eval m x)
eval m (EAp "-" [x,y]) = ValRational $ valToRational m (eval m x) valToRational m (eval m y)
eval m (EAp "*" xs) = ValRational $ product $ map (valToRational m . eval m) xs
eval m (EAp "/" [x,y])
| y' == 0 = eval m (EAp "_/0" [x])
| otherwise = ValRational $ valToRational m (eval m x) / y'
where
y' = valToRational m (eval m y)
eval m (EAp "=" [x,y]) = ValBool $
case (eval m x, eval m y) of
(v1, v2) -> v1 == v2
eval m expr@(EAp f xs) =
case Map.lookup f (mDefs m) of
Nothing -> E.throw $ Error $ "unknown function symbol: " ++ show f
Just (FBoolVar v) -> ValBool $ SAT.evalLit (mBoolModel m) v
Just (FLRAVar v) -> ValRational $ mLRAModel m IntMap.! v
Just (FEUFFun (_, Sort s []) sym) ->
let e = EUF.evalAp (mEUFModel m) sym (map (valToEntity m . eval m) xs)
in case s of
SSymUserDeclared _ _ -> ValUninterpreted e (exprSort' (mDefs m) expr)
SSymBool -> ValBool (e == mEUFTrue m)
SSymReal ->
case IntMap.lookup e (mEntityToRational m) of
Just r -> ValRational r
Nothing -> ValRational (fromIntegral (1000000 + e))
valToBool :: Model -> Value -> Bool
valToBool _ (ValBool b) = b
valToBool _ _ = E.throw $ Error "boolean value is expected"
valToRational :: Model -> Value -> Rational
valToRational _ (ValRational r) = r
valToRational _ _ = E.throw $ Error "rational value is expected"
valToEntity :: Model -> Value -> EUF.Entity
valToEntity _ (ValUninterpreted e _) = e
valToEntity m (ValBool b) = if b then mEUFTrue m else mEUFFalse m
valToEntity m (ValRational r) =
case Map.lookup r (mRationalToEntity m) of
Just e -> e
Nothing -> EUF.mUnspecified (mEUFModel m)
entityToValue :: Model -> EUF.Entity -> Sort -> Value
entityToValue m e s =
case s of
Sort SSymBool _ -> ValBool (e == mEUFTrue m)
Sort SSymReal _ ->
case IntMap.lookup e (mEntityToRational m) of
Just r -> ValRational r
Nothing -> ValRational (fromIntegral (1000000 + e))
Sort (SSymUserDeclared _ _) _ -> ValUninterpreted e s
valSort :: Model -> Value -> Sort
valSort _m (ValUninterpreted _e s) = s
valSort _m (ValBool _b) = sBool
valSort _m (ValRational _r) = sReal
data FunDef = FunDef [([Value], Value)] Value
evalFSym :: Model -> FSym -> FunDef
evalFSym m f =
case Map.lookup f (mDefs m) of
Just (FEUFFun (argsSorts@(_:_), resultSort) sym) ->
let tbl = EUF.mFunctions (mEUFModel m) IntMap.! sym
defaultVal =
case resultSort of
Sort SSymReal [] -> ValRational 555555
Sort SSymBool [] -> ValBool False
Sort (SSymUserDeclared _s _ar) _ss -> ValUninterpreted (EUF.mUnspecified (mEUFModel m)) resultSort
in FunDef [ (zipWith (entityToValue m) args argsSorts, entityToValue m result resultSort)
| (args, result) <- Map.toList tbl ]
defaultVal
Just _ -> FunDef [] $ eval m (EAp f [])
Nothing -> E.throw $ Error $ "unknown function symbol: " ++ show f
getUnsatAssumptions :: Solver -> IO [Expr]
getUnsatAssumptions solver = do
readIORef (smtUnsatAssumptions solver)
getUnsatCore :: Solver -> IO [String]
getUnsatCore solver = do
readIORef (smtUnsatCore solver)
pairs :: [a] -> [(a,a)]
pairs [] = []
pairs (x:xs) = [(x,y) | y <- xs] ++ pairs xs
#if !MIN_VERSION_base(4,7,0)
isRight :: Either a b -> Bool
isRight (Left _) = False
isRight (Right _) = True
#endif