{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SMT
-- Copyright   :  (c) Masahiro Sakai 2015
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  unstable
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.SMT
  (
  -- * The Solver type
    Solver
  , newSolver
  , Exception (..)

  -- * Problem Specification
  , SSym (..)
  , ssymArity
  , Sort (..)
  , sBool
  , sReal
  , sBitVec
  , FunType
  , Expr (..)
  , exprSort
  , Index (..)
  , FSym (..)
  , declareSSym
  , declareSort
  , VASortFun
  , declareFSym
  , declareFun
  , declareConst
  , VAFun
  , assert
  , assertNamed
  , getGlobalDeclarations
  , setGlobalDeclarations

  -- * Solving
  , checkSAT
  , checkSATAssuming
  , push
  , pop

  -- * Inspecting models
  , Model
  , Value (..)
  , getModel
  , eval
  , valSort
  , FunDef (..)
  , evalFSym
  , modelGetAssertions

  -- * Inspecting proofs
  , getUnsatAssumptions
  , getUnsatCore
  ) where

import Control.Applicative
import qualified Control.Exception as E
import Control.Monad
import Control.Monad.Trans
import Control.Monad.Trans.Except
import Data.Bits
import Data.Either
import Data.Interned (intern, unintern)
import Data.Interned.Text
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.Monoid
import Data.Set (Set)
import qualified Data.Set as Set
import Data.String
import qualified Data.Text as T
import Data.Typeable
import Data.VectorSpace

import ToySolver.Data.Delta
import ToySolver.Data.Boolean
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.Encoder.Tseitin as Tseitin
import ToySolver.SAT.Encoder.Tseitin (Formula (..))
import qualified ToySolver.Arith.Simplex as Simplex
import qualified ToySolver.BitVector as BV
import qualified ToySolver.EUF.EUFSolver as EUF

data Index
  = IndexNumeral !Integer
  | IndexSymbol !InternedText
  deriving (Int -> Index -> ShowS
[Index] -> ShowS
Index -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Index] -> ShowS
$cshowList :: [Index] -> ShowS
show :: Index -> String
$cshow :: Index -> String
showsPrec :: Int -> Index -> ShowS
$cshowsPrec :: Int -> Index -> ShowS
Show,Index -> Index -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Index -> Index -> Bool
$c/= :: Index -> Index -> Bool
== :: Index -> Index -> Bool
$c== :: Index -> Index -> Bool
Eq, Eq Index
Index -> Index -> Bool
Index -> Index -> Ordering
Index -> Index -> Index
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 :: Index -> Index -> Index
$cmin :: Index -> Index -> Index
max :: Index -> Index -> Index
$cmax :: Index -> Index -> Index
>= :: Index -> Index -> Bool
$c>= :: Index -> Index -> Bool
> :: Index -> Index -> Bool
$c> :: Index -> Index -> Bool
<= :: Index -> Index -> Bool
$c<= :: Index -> Index -> Bool
< :: Index -> Index -> Bool
$c< :: Index -> Index -> Bool
compare :: Index -> Index -> Ordering
$ccompare :: Index -> Index -> Ordering
Ord)

data FSym
  = FSym !InternedText [Index]
  deriving (Int -> FSym -> ShowS
[FSym] -> ShowS
FSym -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FSym] -> ShowS
$cshowList :: [FSym] -> ShowS
show :: FSym -> String
$cshow :: FSym -> String
showsPrec :: Int -> FSym -> ShowS
$cshowsPrec :: Int -> FSym -> ShowS
Show,FSym -> FSym -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FSym -> FSym -> Bool
$c/= :: FSym -> FSym -> Bool
== :: FSym -> FSym -> Bool
$c== :: FSym -> FSym -> Bool
Eq,Eq FSym
FSym -> FSym -> Bool
FSym -> FSym -> Ordering
FSym -> FSym -> FSym
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 :: FSym -> FSym -> FSym
$cmin :: FSym -> FSym -> FSym
max :: FSym -> FSym -> FSym
$cmax :: FSym -> FSym -> FSym
>= :: FSym -> FSym -> Bool
$c>= :: FSym -> FSym -> Bool
> :: FSym -> FSym -> Bool
$c> :: FSym -> FSym -> Bool
<= :: FSym -> FSym -> Bool
$c<= :: FSym -> FSym -> Bool
< :: FSym -> FSym -> Bool
$c< :: FSym -> FSym -> Bool
compare :: FSym -> FSym -> Ordering
$ccompare :: FSym -> FSym -> Ordering
Ord)

instance IsString FSym where
  fromString :: String -> FSym
fromString String
s = InternedText -> [Index] -> FSym
FSym (forall a. IsString a => String -> a
fromString String
s) []

-- | Sort symbols
data SSym
  = SSymBool
  | SSymReal
  | SSymBitVec !Int
  | SSymUninterpreted !InternedText !Int
  deriving (Int -> SSym -> ShowS
[SSym] -> ShowS
SSym -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SSym] -> ShowS
$cshowList :: [SSym] -> ShowS
show :: SSym -> String
$cshow :: SSym -> String
showsPrec :: Int -> SSym -> ShowS
$cshowsPrec :: Int -> SSym -> ShowS
Show, SSym -> SSym -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SSym -> SSym -> Bool
$c/= :: SSym -> SSym -> Bool
== :: SSym -> SSym -> Bool
$c== :: SSym -> SSym -> Bool
Eq, Eq SSym
SSym -> SSym -> Bool
SSym -> SSym -> Ordering
SSym -> SSym -> SSym
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 :: SSym -> SSym -> SSym
$cmin :: SSym -> SSym -> SSym
max :: SSym -> SSym -> SSym
$cmax :: SSym -> SSym -> SSym
>= :: SSym -> SSym -> Bool
$c>= :: SSym -> SSym -> Bool
> :: SSym -> SSym -> Bool
$c> :: SSym -> SSym -> Bool
<= :: SSym -> SSym -> Bool
$c<= :: SSym -> SSym -> Bool
< :: SSym -> SSym -> Bool
$c< :: SSym -> SSym -> Bool
compare :: SSym -> SSym -> Ordering
$ccompare :: SSym -> SSym -> Ordering
Ord)

ssymArity :: SSym -> Int
ssymArity :: SSym -> Int
ssymArity SSym
SSymBool = Int
0
ssymArity SSym
SSymReal = Int
0
ssymArity (SSymBitVec Int
_) = Int
0
ssymArity (SSymUninterpreted InternedText
_ Int
ar) = Int
ar

data Sort = Sort SSym [Sort]
  deriving (Int -> Sort -> ShowS
[Sort] -> ShowS
Sort -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sort] -> ShowS
$cshowList :: [Sort] -> ShowS
show :: Sort -> String
$cshow :: Sort -> String
showsPrec :: Int -> Sort -> ShowS
$cshowsPrec :: Int -> Sort -> ShowS
Show, Sort -> Sort -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sort -> Sort -> Bool
$c/= :: Sort -> Sort -> Bool
== :: Sort -> Sort -> Bool
$c== :: Sort -> Sort -> Bool
Eq, Eq Sort
Sort -> Sort -> Bool
Sort -> Sort -> Ordering
Sort -> Sort -> Sort
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 :: Sort -> Sort -> Sort
$cmin :: Sort -> Sort -> Sort
max :: Sort -> Sort -> Sort
$cmax :: Sort -> Sort -> Sort
>= :: Sort -> Sort -> Bool
$c>= :: Sort -> Sort -> Bool
> :: Sort -> Sort -> Bool
$c> :: Sort -> Sort -> Bool
<= :: Sort -> Sort -> Bool
$c<= :: Sort -> Sort -> Bool
< :: Sort -> Sort -> Bool
$c< :: Sort -> Sort -> Bool
compare :: Sort -> Sort -> Ordering
$ccompare :: Sort -> Sort -> Ordering
Ord)

sBool :: Sort
sBool :: Sort
sBool = SSym -> [Sort] -> Sort
Sort SSym
SSymBool []

sReal :: Sort
sReal :: Sort
sReal = SSym -> [Sort] -> Sort
Sort SSym
SSymReal []

sBitVec :: Int -> Sort
sBitVec :: Int -> Sort
sBitVec Int
n = SSym -> [Sort] -> Sort
Sort (Int -> SSym
SSymBitVec Int
n) []

type FunType = ([Sort],Sort)

data Expr
  = EAp FSym [Expr]
  | EValue !Value
  deriving (Int -> Expr -> ShowS
[Expr] -> ShowS
Expr -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Expr] -> ShowS
$cshowList :: [Expr] -> ShowS
show :: Expr -> String
$cshow :: Expr -> String
showsPrec :: Int -> Expr -> ShowS
$cshowsPrec :: Int -> Expr -> ShowS
Show, Expr -> Expr -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Expr -> Expr -> Bool
$c/= :: Expr -> Expr -> Bool
== :: Expr -> Expr -> Bool
$c== :: Expr -> Expr -> Bool
Eq, Eq Expr
Expr -> Expr -> Bool
Expr -> Expr -> Ordering
Expr -> Expr -> Expr
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 :: Expr -> Expr -> Expr
$cmin :: Expr -> Expr -> Expr
max :: Expr -> Expr -> Expr
$cmax :: Expr -> Expr -> Expr
>= :: Expr -> Expr -> Bool
$c>= :: Expr -> Expr -> Bool
> :: Expr -> Expr -> Bool
$c> :: Expr -> Expr -> Bool
<= :: Expr -> Expr -> Bool
$c<= :: Expr -> Expr -> Bool
< :: Expr -> Expr -> Bool
$c< :: Expr -> Expr -> Bool
compare :: Expr -> Expr -> Ordering
$ccompare :: Expr -> Expr -> Ordering
Ord)

instance MonotoneBoolean Expr where
  true :: Expr
true  = FSym -> [Expr] -> Expr
EAp FSym
"true" []
  false :: Expr
false = FSym -> [Expr] -> Expr
EAp FSym
"false" []
  andB :: [Expr] -> Expr
andB = FSym -> [Expr] -> Expr
EAp FSym
"and"
  orB :: [Expr] -> Expr
orB  = FSym -> [Expr] -> Expr
EAp FSym
"or"

instance Complement Expr where
  notB :: Expr -> Expr
notB Expr
x = FSym -> [Expr] -> Expr
EAp FSym
"not" [Expr
x]

instance IfThenElse Expr Expr where
  ite :: Expr -> Expr -> Expr -> Expr
ite Expr
x Expr
y Expr
z = FSym -> [Expr] -> Expr
EAp FSym
"ite" [Expr
x,Expr
y,Expr
z]

instance Boolean Expr where
  Expr
x .=>. :: Expr -> Expr -> Expr
.=>. Expr
y  = FSym -> [Expr] -> Expr
EAp FSym
"=>" [Expr
x,Expr
y]
  Expr
x .<=>. :: Expr -> Expr -> Expr
.<=>. Expr
y = FSym -> [Expr] -> Expr
EAp FSym
"=" [Expr
x,Expr
y]

instance Num Expr where
  Expr
x + :: Expr -> Expr -> Expr
+ Expr
y = FSym -> [Expr] -> Expr
EAp FSym
"+" [Expr
x,Expr
y]
  Expr
x - :: Expr -> Expr -> Expr
- Expr
y = FSym -> [Expr] -> Expr
EAp FSym
"-" [Expr
x,Expr
y]
  Expr
x * :: Expr -> Expr -> Expr
* Expr
y = FSym -> [Expr] -> Expr
EAp FSym
"*" [Expr
x,Expr
y]
  negate :: Expr -> Expr
negate Expr
x = FSym -> [Expr] -> Expr
EAp FSym
"-" [Expr
x]
  abs :: Expr -> Expr
abs Expr
x = forall a. HasCallStack => String -> a
error String
"Num{ToySolver.SMT.Expr}.abs is not implemented"
  signum :: Expr -> Expr
signum Expr
x = forall a. HasCallStack => String -> a
error String
"Num{ToySolver.SMT.Expr}.signum is not implemented"
  fromInteger :: Integer -> Expr
fromInteger Integer
x = Value -> Expr
EValue forall a b. (a -> b) -> a -> b
$ Rational -> Value
ValRational forall a b. (a -> b) -> a -> b
$ forall a. Num a => Integer -> a
fromInteger Integer
x

instance Fractional Expr where
  Expr
x / :: Expr -> Expr -> Expr
/ Expr
y = FSym -> [Expr] -> Expr
EAp FSym
"/" [Expr
x,Expr
y]
  fromRational :: Rational -> Expr
fromRational Rational
x = Value -> Expr
EValue forall a b. (a -> b) -> a -> b
$ Rational -> Value
ValRational Rational
x

instance IsEqRel Expr Expr where
  Expr
a .==. :: Expr -> Expr -> Expr
.==. Expr
b = FSym -> [Expr] -> Expr
EAp FSym
"=" [Expr
a,Expr
b]
  Expr
a ./=. :: Expr -> Expr -> Expr
./=. Expr
b = forall a. Complement a => a -> a
notB (Expr
a forall e r. IsEqRel e r => e -> e -> r
.==. Expr
b)

instance IsOrdRel Expr Expr where
  Expr
a .<. :: Expr -> Expr -> Expr
.<. Expr
b = FSym -> [Expr] -> Expr
EAp FSym
"<" [Expr
a,Expr
b]
  Expr
a .>. :: Expr -> Expr -> Expr
.>. Expr
b = FSym -> [Expr] -> Expr
EAp FSym
">" [Expr
a,Expr
b]
  Expr
a .<=. :: Expr -> Expr -> Expr
.<=. Expr
b = FSym -> [Expr] -> Expr
EAp FSym
"<=" [Expr
a,Expr
b]
  Expr
a .>=. :: Expr -> Expr -> Expr
.>=. Expr
b = FSym -> [Expr] -> Expr
EAp FSym
">=" [Expr
a,Expr
b]

data FDef
  = FBoolVar SAT.Var
  | FLRAVar LA.Var
  | FBVVar BV.Var
  | FEUFFun FunType EUF.FSym
  deriving (Int -> FDef -> ShowS
[FDef] -> ShowS
FDef -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FDef] -> ShowS
$cshowList :: [FDef] -> ShowS
show :: FDef -> String
$cshow :: FDef -> String
showsPrec :: Int -> FDef -> ShowS
$cshowsPrec :: Int -> FDef -> ShowS
Show)

data Exception
  = Error String
  | Unsupported
  deriving (Int -> Exception -> ShowS
[Exception] -> ShowS
Exception -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Exception] -> ShowS
$cshowList :: [Exception] -> ShowS
show :: Exception -> String
$cshow :: Exception -> String
showsPrec :: Int -> Exception -> ShowS
$cshowsPrec :: Int -> Exception -> ShowS
Show, Typeable)

instance E.Exception Exception

data Solver
  = Solver
  { Solver -> Solver
smtSAT :: !SAT.Solver
  , Solver -> Encoder IO
smtEnc :: !(Tseitin.Encoder IO)
  , Solver -> Solver
smtEUF :: !EUF.Solver
  , Solver -> GenericSolver (Delta Rational)
smtLRA :: !(Simplex.GenericSolver (Delta Rational))
  , Solver -> Solver
smtBV :: !BV.Solver

  , Solver -> IORef (Map (Term, Term) Int, IntMap (Term, Term))
smtEUFAtomDefs  :: !(IORef (Map (EUF.Term, EUF.Term) SAT.Var, IntMap (EUF.Term, EUF.Term)))
  , Solver
-> IORef
     (Map (Int, Rational) (Int, Int, Int), IntMap (Atom Rational))
smtLRAAtomDefs  :: !(IORef (Map (LA.Var, Rational) (SAT.Lit, SAT.Lit, SAT.Lit), IntMap (LA.Atom Rational)))
  , Solver -> IORef (Map BVAtomNormalized Int, IntMap BVAtomNormalized)
smtBVAtomDefs   :: !(IORef (Map BVAtomNormalized SAT.Var, IntMap BVAtomNormalized))
  , Solver -> IORef (Map Term Int, IntMap Term)
smtBoolTermDefs :: !(IORef (Map EUF.Term SAT.Lit, IntMap EUF.Term))
  , Solver -> IORef (Map (Expr Rational) Int, IntMap (Expr Rational))
smtRealTermDefs :: !(IORef (Map (LA.Expr Rational) EUF.FSym, IntMap (LA.Expr Rational)))
  , Solver -> IORef (Map Expr Int, IntMap (IntMap Expr))
smtBVTermDefs :: !(IORef (Map BV.Expr EUF.FSym, IntMap (IntMap BV.Expr)))
  , Solver -> Term
smtEUFTrue  :: !EUF.Term
  , Solver -> Term
smtEUFFalse :: !EUF.Term

  , Solver -> IORef Model
smtEUFModel :: !(IORef EUF.Model)
  , Solver -> IORef Model
smtLRAModel :: !(IORef Simplex.Model)
  , Solver -> IORef Model
smtBVModel :: !(IORef BV.Model)

  , Solver -> IORef Bool
smtGlobalDeclarationsRef :: !(IORef Bool)
  , Solver -> IORef (Map FSym FDef)
smtFDefs :: !(IORef (Map FSym FDef))
  , Solver -> IORef (Map String Int)
smtNamedAssertions :: !(IORef (Map String SAT.Lit))
  , Solver -> Vec AssertionLevel
smtAssertionStack :: !(Vec.Vec AssertionLevel)

  , Solver -> IORef [Expr]
smtUnsatAssumptions :: !(IORef [Expr])
  , Solver -> IORef [String]
smtUnsatCore :: !(IORef [String])
  }

data AssertionLevel
  = AssertionLevel
  { AssertionLevel -> Map String Int
alSavedNamedAssertions :: Map String SAT.Lit
  , AssertionLevel -> Maybe (Map FSym FDef)
alSavedFDefs :: Maybe (Map FSym FDef)
  , AssertionLevel -> Int
alSelector :: SAT.Lit
  }

data TheorySolverID
  = TheorySolverEUF
  | TheorySolverSimplex
  | TheorySolverBV
  deriving (TheorySolverID -> TheorySolverID -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TheorySolverID -> TheorySolverID -> Bool
$c/= :: TheorySolverID -> TheorySolverID -> Bool
== :: TheorySolverID -> TheorySolverID -> Bool
$c== :: TheorySolverID -> TheorySolverID -> Bool
Eq, Eq TheorySolverID
TheorySolverID -> TheorySolverID -> Bool
TheorySolverID -> TheorySolverID -> Ordering
TheorySolverID -> TheorySolverID -> TheorySolverID
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 :: TheorySolverID -> TheorySolverID -> TheorySolverID
$cmin :: TheorySolverID -> TheorySolverID -> TheorySolverID
max :: TheorySolverID -> TheorySolverID -> TheorySolverID
$cmax :: TheorySolverID -> TheorySolverID -> TheorySolverID
>= :: TheorySolverID -> TheorySolverID -> Bool
$c>= :: TheorySolverID -> TheorySolverID -> Bool
> :: TheorySolverID -> TheorySolverID -> Bool
$c> :: TheorySolverID -> TheorySolverID -> Bool
<= :: TheorySolverID -> TheorySolverID -> Bool
$c<= :: TheorySolverID -> TheorySolverID -> Bool
< :: TheorySolverID -> TheorySolverID -> Bool
$c< :: TheorySolverID -> TheorySolverID -> Bool
compare :: TheorySolverID -> TheorySolverID -> Ordering
$ccompare :: TheorySolverID -> TheorySolverID -> Ordering
Ord, Int -> TheorySolverID
TheorySolverID -> Int
TheorySolverID -> [TheorySolverID]
TheorySolverID -> TheorySolverID
TheorySolverID -> TheorySolverID -> [TheorySolverID]
TheorySolverID
-> TheorySolverID -> TheorySolverID -> [TheorySolverID]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: TheorySolverID
-> TheorySolverID -> TheorySolverID -> [TheorySolverID]
$cenumFromThenTo :: TheorySolverID
-> TheorySolverID -> TheorySolverID -> [TheorySolverID]
enumFromTo :: TheorySolverID -> TheorySolverID -> [TheorySolverID]
$cenumFromTo :: TheorySolverID -> TheorySolverID -> [TheorySolverID]
enumFromThen :: TheorySolverID -> TheorySolverID -> [TheorySolverID]
$cenumFromThen :: TheorySolverID -> TheorySolverID -> [TheorySolverID]
enumFrom :: TheorySolverID -> [TheorySolverID]
$cenumFrom :: TheorySolverID -> [TheorySolverID]
fromEnum :: TheorySolverID -> Int
$cfromEnum :: TheorySolverID -> Int
toEnum :: Int -> TheorySolverID
$ctoEnum :: Int -> TheorySolverID
pred :: TheorySolverID -> TheorySolverID
$cpred :: TheorySolverID -> TheorySolverID
succ :: TheorySolverID -> TheorySolverID
$csucc :: TheorySolverID -> TheorySolverID
Enum, TheorySolverID
forall a. a -> a -> Bounded a
maxBound :: TheorySolverID
$cmaxBound :: TheorySolverID
minBound :: TheorySolverID
$cminBound :: TheorySolverID
Bounded)

newSolver :: IO Solver
newSolver :: IO Solver
newSolver = do
  Solver
sat <- IO Solver
SAT.newSolver
  Encoder IO
enc <- forall (m :: * -> *) a.
(PrimMonad m, AddClause m a) =>
a -> m (Encoder m)
Tseitin.newEncoder Solver
sat
  Solver
euf <- IO Solver
EUF.newSolver
  GenericSolver (Delta Rational)
lra <- forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
m (GenericSolverM m v)
Simplex.newSolver
  Solver
bv <- IO Solver
BV.newSolver

  Int
litTrue <- forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeConj Encoder IO
enc []
  let litFalse :: Int
litFalse = -Int
litTrue

  Term
eufTrue  <- Solver -> IO Term
EUF.newConst Solver
euf
  Term
eufFalse <- Solver -> IO Term
EUF.newConst Solver
euf
  Solver -> Term -> Term -> IO ()
EUF.assertNotEqual Solver
euf Term
eufTrue Term
eufFalse
  Int
divByZero <- Solver -> IO Int
EUF.newFSym Solver
euf

  IORef (Map (Term, Term) Int, IntMap (Term, Term))
eufAtomDefs <- forall a. a -> IO (IORef a)
newIORef (forall k a. Map k a
Map.empty, forall a. IntMap a
IntMap.empty)
  IORef (Map (Int, Rational) (Int, Int, Int), IntMap (Atom Rational))
lraAtomDefs <- forall a. a -> IO (IORef a)
newIORef (forall k a. Map k a
Map.empty, forall a. IntMap a
IntMap.empty)
  IORef (Map BVAtomNormalized Int, IntMap BVAtomNormalized)
bvAtomDefs <- forall a. a -> IO (IORef a)
newIORef (forall k a. Map k a
Map.empty, forall a. IntMap a
IntMap.empty)
  IORef (Map Term Int, IntMap Term)
boolTermDefs <- forall a. a -> IO (IORef a)
newIORef forall a b. (a -> b) -> a -> b
$
    ( forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Term
eufTrue, Int
litTrue), (Term
eufFalse, Int
litFalse)]
    , forall a. [(Int, a)] -> IntMap a
IntMap.fromList [(Int
litTrue, Term
eufTrue), (Int
litFalse, Term
eufFalse)]
    )
  IORef (Map (Expr Rational) Int, IntMap (Expr Rational))
realTermDefs <- forall a. a -> IO (IORef a)
newIORef (forall k a. Map k a
Map.empty, forall a. IntMap a
IntMap.empty)
  IORef (Map Expr Int, IntMap (IntMap Expr))
bvTermDefs <- forall a. a -> IO (IORef a)
newIORef (forall k a. Map k a
Map.empty, forall a. IntMap a
IntMap.empty)

  IORef Model
eufModelRef <- forall a. a -> IO (IORef a)
newIORef (forall a. HasCallStack => a
undefined :: EUF.Model)
  IORef Model
lraModelRef <- forall a. a -> IO (IORef a)
newIORef (forall a. HasCallStack => a
undefined :: Simplex.Model)
  IORef Model
bvModelRef <- forall a. a -> IO (IORef a)
newIORef (forall a. HasCallStack => a
undefined :: BV.Model)

  IORef Bool
globalDeclarationsRef <- forall a. a -> IO (IORef a)
newIORef Bool
False
  IORef (Map FSym FDef)
fdefs <- forall a. a -> IO (IORef a)
newIORef forall a b. (a -> b) -> a -> b
$ forall k a. k -> a -> Map k a
Map.singleton FSym
"_/0" (FunType -> Int -> FDef
FEUFFun ([Sort
sReal], Sort
sReal) Int
divByZero)

  IORef TheorySolverID
conflictTheory <- forall a. a -> IO (IORef a)
newIORef forall a. HasCallStack => a
undefined

  let tsolver :: TheorySolver
tsolver =
        TheorySolver
        { thAssertLit :: (Int -> IO Bool) -> Int -> IO Bool
thAssertLit = \Int -> IO Bool
_ Int
l -> forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a. a -> a
id forall a. a -> a
id) forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ do
            (Map (Int, Rational) (Int, Int, Int)
_, IntMap (Atom Rational)
defsLRA) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef IORef (Map (Int, Rational) (Int, Int, Int), IntMap (Atom Rational))
lraAtomDefs
            case forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
l IntMap (Atom Rational)
defsLRA of
              Maybe (Atom Rational)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
              Just Atom Rational
atom -> do
                forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
PrimMonad m =>
GenericSolverM m (Delta Rational)
-> Atom Rational -> Maybe Int -> m ()
Simplex.assertAtomEx' GenericSolver (Delta Rational)
lra Atom Rational
atom (forall a. a -> Maybe a
Just Int
l)
                forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE Bool
True

            (Map (Term, Term) Int
_, IntMap (Term, Term)
defsEUF) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef IORef (Map (Term, Term) Int, IntMap (Term, Term))
eufAtomDefs
            case forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (Int -> Int
SAT.litVar Int
l) IntMap (Term, Term)
defsEUF of
              Maybe (Term, Term)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
              Just (Term
t1,Term
t2) -> do
                if Int -> Bool
SAT.litPolarity Int
l then do
                  forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Solver -> Term -> Term -> Maybe Int -> IO ()
EUF.assertEqual' Solver
euf Term
t1 Term
t2 (forall a. a -> Maybe a
Just Int
l)
                else do
                  forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Solver -> Term -> Term -> Maybe Int -> IO ()
EUF.assertNotEqual' Solver
euf Term
t1 Term
t2 (forall a. a -> Maybe a
Just Int
l)
                forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE Bool
True

            (Map BVAtomNormalized Int
_, IntMap BVAtomNormalized
defsBV) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef IORef (Map BVAtomNormalized Int, IntMap BVAtomNormalized)
bvAtomDefs
            case forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (Int -> Int
SAT.litVar Int
l) IntMap BVAtomNormalized
defsBV of
              Maybe BVAtomNormalized
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
              Just BVAtomNormalized
atom -> do
                forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Solver -> Atom -> Maybe Int -> IO ()
BV.assertAtom Solver
bv ((BVAtomNormalized, Bool) -> Atom
unnormalizeBVAtom (BVAtomNormalized
atom, Int -> Bool
SAT.litPolarity Int
l)) (forall a. a -> Maybe a
Just Int
l)
                forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE Bool
True

            forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True

        , thCheck :: (Int -> IO Bool) -> IO Bool
thCheck = \Int -> IO Bool
callback -> forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a b. Either a b -> Bool
isRight forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ do
            do Bool
b <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Bool
Simplex.check GenericSolver (Delta Rational)
lra
               forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
b forall a b. (a -> b) -> a -> b
$ do
                 forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> a -> IO ()
writeIORef IORef TheorySolverID
conflictTheory TheorySolverID
TheorySolverSimplex
                 forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE ()
            do Bool
b <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Solver -> IO Bool
EUF.check Solver
euf
               forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
b forall a b. (a -> b) -> a -> b
$ do
                 forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> a -> IO ()
writeIORef IORef TheorySolverID
conflictTheory TheorySolverID
TheorySolverEUF
                 forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE ()
               (Map (Term, Term) Int
_, IntMap (Term, Term)
defsEUF) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef IORef (Map (Term, Term) Int, IntMap (Term, Term))
eufAtomDefs
               forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (Term, Term)
defsEUF) forall a b. (a -> b) -> a -> b
$ \(Int
v, (Term
t1, Term
t2)) -> do
                  Bool
b2 <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Solver -> Term -> Term -> IO Bool
EUF.areEqual Solver
euf Term
t1 Term
t2
                  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
b2 forall a b. (a -> b) -> a -> b
$ do
                    Bool
b3 <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Int -> IO Bool
callback Int
v
                    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
b3 forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE ()
            do Bool
b <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Solver -> IO Bool
BV.check Solver
bv
               forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
b forall a b. (a -> b) -> a -> b
$ do
                 forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> a -> IO ()
writeIORef IORef TheorySolverID
conflictTheory TheorySolverID
TheorySolverBV
                 forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE ()

        , thExplain :: Maybe Int -> IO [Int]
thExplain = \Maybe Int
m -> do
            case Maybe Int
m of
              Maybe Int
Nothing -> do
                TheorySolverID
t <- forall a. IORef a -> IO a
readIORef IORef TheorySolverID
conflictTheory
                case TheorySolverID
t of
                  TheorySolverID
TheorySolverSimplex -> forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM IntSet -> [Int]
IntSet.toList forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m IntSet
Simplex.explain GenericSolver (Delta Rational)
lra
                  TheorySolverID
TheorySolverBV -> forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM IntSet -> [Int]
IntSet.toList forall a b. (a -> b) -> a -> b
$ Solver -> IO IntSet
BV.explain Solver
bv
                  TheorySolverID
TheorySolverEUF -> forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM IntSet -> [Int]
IntSet.toList forall a b. (a -> b) -> a -> b
$ Solver -> Maybe (Term, Term) -> IO IntSet
EUF.explain Solver
euf forall a. Maybe a
Nothing
              Just Int
v -> do
                (Map (Term, Term) Int
_, IntMap (Term, Term)
defsEUF) <- forall a. IORef a -> IO a
readIORef IORef (Map (Term, Term) Int, IntMap (Term, Term))
eufAtomDefs
                case forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
v IntMap (Term, Term)
defsEUF of
                  Maybe (Term, Term)
Nothing -> forall a. HasCallStack => String -> a
error String
"should not happen"
                  Just (Term
t1,Term
t2) -> forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM IntSet -> [Int]
IntSet.toList forall a b. (a -> b) -> a -> b
$ Solver -> Maybe (Term, Term) -> IO IntSet
EUF.explain Solver
euf (forall a. a -> Maybe a
Just (Term
t1,Term
t2))

        , thPushBacktrackPoint :: IO ()
thPushBacktrackPoint = do
            forall (m :: * -> *) v. PrimMonad m => GenericSolverM m v -> m ()
Simplex.pushBacktrackPoint GenericSolver (Delta Rational)
lra
            Solver -> IO ()
EUF.pushBacktrackPoint Solver
euf
            Solver -> IO ()
BV.pushBacktrackPoint Solver
bv
        , thPopBacktrackPoint :: IO ()
thPopBacktrackPoint = do
            forall (m :: * -> *) v. PrimMonad m => GenericSolverM m v -> m ()
Simplex.popBacktrackPoint GenericSolver (Delta Rational)
lra
            Solver -> IO ()
EUF.popBacktrackPoint Solver
euf
            Solver -> IO ()
BV.popBacktrackPoint Solver
bv
        , thConstructModel :: IO ()
thConstructModel = do
            forall a. IORef a -> a -> IO ()
writeIORef IORef Model
eufModelRef forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> IO Model
EUF.getModel Solver
euf
            -- We need to call Simplex.getModel here.
            -- Because backtracking removes constraints that are necessary
            -- for computing the value of delta.
            forall a. IORef a -> a -> IO ()
writeIORef IORef Model
lraModelRef forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall v (m :: * -> *).
(SolverValue v, PrimMonad m) =>
GenericSolverM m v -> m Model
Simplex.getModel GenericSolver (Delta Rational)
lra
            forall a. IORef a -> a -> IO ()
writeIORef IORef Model
bvModelRef forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> IO Model
BV.getModel Solver
bv
            forall (m :: * -> *) a. Monad m => a -> m a
return ()
        }
  Solver -> TheorySolver -> IO ()
SAT.setTheory Solver
sat TheorySolver
tsolver

  IORef (Map String Int)
named <- forall a. a -> IO (IORef a)
newIORef forall k a. Map k a
Map.empty

  Vec AssertionLevel
stack <- forall (a :: * -> * -> *) e. MArray a e IO => IO (GenericVec a e)
Vec.new

  IORef [Expr]
unsatAssumptionsRef <- forall a. a -> IO (IORef a)
newIORef forall a. HasCallStack => a
undefined
  IORef [String]
unsatCoreRef <- forall a. a -> IO (IORef a)
newIORef forall a. HasCallStack => a
undefined

  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    Solver
    { smtSAT :: Solver
smtSAT = Solver
sat
    , smtEnc :: Encoder IO
smtEnc = Encoder IO
enc
    , smtEUF :: Solver
smtEUF = Solver
euf
    , smtLRA :: GenericSolver (Delta Rational)
smtLRA = GenericSolver (Delta Rational)
lra
    , smtBV :: Solver
smtBV  = Solver
bv

    , smtEUFAtomDefs :: IORef (Map (Term, Term) Int, IntMap (Term, Term))
smtEUFAtomDefs = IORef (Map (Term, Term) Int, IntMap (Term, Term))
eufAtomDefs
    , smtLRAAtomDefs :: IORef (Map (Int, Rational) (Int, Int, Int), IntMap (Atom Rational))
smtLRAAtomDefs = IORef (Map (Int, Rational) (Int, Int, Int), IntMap (Atom Rational))
lraAtomDefs
    , smtBVAtomDefs :: IORef (Map BVAtomNormalized Int, IntMap BVAtomNormalized)
smtBVAtomDefs = IORef (Map BVAtomNormalized Int, IntMap BVAtomNormalized)
bvAtomDefs
    , smtBoolTermDefs :: IORef (Map Term Int, IntMap Term)
smtBoolTermDefs = IORef (Map Term Int, IntMap Term)
boolTermDefs
    , smtRealTermDefs :: IORef (Map (Expr Rational) Int, IntMap (Expr Rational))
smtRealTermDefs = IORef (Map (Expr Rational) Int, IntMap (Expr Rational))
realTermDefs
    , smtBVTermDefs :: IORef (Map Expr Int, IntMap (IntMap Expr))
smtBVTermDefs = IORef (Map Expr Int, IntMap (IntMap Expr))
bvTermDefs
    , smtEUFTrue :: Term
smtEUFTrue  = Term
eufTrue
    , smtEUFFalse :: Term
smtEUFFalse = Term
eufFalse

    , smtEUFModel :: IORef Model
smtEUFModel = IORef Model
eufModelRef
    , smtLRAModel :: IORef Model
smtLRAModel = IORef Model
lraModelRef
    , smtBVModel :: IORef Model
smtBVModel = IORef Model
bvModelRef

    , smtGlobalDeclarationsRef :: IORef Bool
smtGlobalDeclarationsRef = IORef Bool
globalDeclarationsRef
    , smtFDefs :: IORef (Map FSym FDef)
smtFDefs = IORef (Map FSym FDef)
fdefs
    , smtNamedAssertions :: IORef (Map String Int)
smtNamedAssertions = IORef (Map String Int)
named
    , smtAssertionStack :: Vec AssertionLevel
smtAssertionStack = Vec AssertionLevel
stack

    , smtUnsatAssumptions :: IORef [Expr]
smtUnsatAssumptions = IORef [Expr]
unsatAssumptionsRef
    , smtUnsatCore :: IORef [String]
smtUnsatCore = IORef [String]
unsatCoreRef
    }

declareSSym :: Solver -> String -> Int -> IO SSym
declareSSym :: Solver -> String -> Int -> IO SSym
declareSSym Solver
solver String
name Int
arity = forall (m :: * -> *) a. Monad m => a -> m a
return (InternedText -> Int -> SSym
SSymUninterpreted (forall a. IsString a => String -> a
fromString String
name) Int
arity)

declareSort :: VASortFun a => Solver -> String -> Int -> IO a
declareSort :: forall a. VASortFun a => Solver -> String -> Int -> IO a
declareSort Solver
solver String
name Int
arity = do
  SSym
ssym <- Solver -> String -> Int -> IO SSym
declareSSym Solver
solver String
name Int
arity
  let f :: a
f = forall a. VASortFun a => ([Sort] -> Sort) -> a
withSortVArgs (SSym -> [Sort] -> Sort
Sort SSym
ssym)
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. VASortFun a => a -> Int
arityVASortFun a
f forall a. Eq a => a -> a -> Bool
== Int
arity) forall a b. (a -> b) -> a -> b
$ do
    forall e a. Exception e => e -> IO a
E.throwIO forall a b. (a -> b) -> a -> b
$ String -> Exception
Error String
"ToySolver.SMT.declareSort: argument number error"
  forall (m :: * -> *) a. Monad m => a -> m a
return a
f

class VASortFun a where
  withSortVArgs :: ([Sort] -> Sort) -> a
  arityVASortFun :: a -> Int

instance VASortFun Sort where
  withSortVArgs :: ([Sort] -> Sort) -> Sort
withSortVArgs [Sort] -> Sort
k = [Sort] -> Sort
k []
  arityVASortFun :: Sort -> Int
arityVASortFun Sort
f = Int
0

instance VASortFun a => VASortFun (Sort -> a) where
  withSortVArgs :: ([Sort] -> Sort) -> Sort -> a
withSortVArgs [Sort] -> Sort
k Sort
x = forall a. VASortFun a => ([Sort] -> Sort) -> a
withSortVArgs (\[Sort]
xs -> [Sort] -> Sort
k (Sort
x forall a. a -> [a] -> [a]
: [Sort]
xs))
  arityVASortFun :: (Sort -> a) -> Int
arityVASortFun Sort -> a
f = forall a. VASortFun a => a -> Int
arityVASortFun (Sort -> a
f forall a. HasCallStack => a
undefined) forall a. Num a => a -> a -> a
+ Int
1

declareFSym :: Solver -> String -> [Sort] -> Sort -> IO FSym
declareFSym :: Solver -> String -> [Sort] -> Sort -> IO FSym
declareFSym Solver
solver String
f' [Sort]
xs Sort
y = do
  let f :: FSym
f = InternedText -> [Index] -> FSym
FSym (forall t. Interned t => Uninterned t -> t
intern (String -> Text
T.pack String
f')) []
  Map FSym FDef
fdefs <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map FSym FDef)
smtFDefs Solver
solver)
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FSym
f forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map FSym FDef
fdefs) forall a b. (a -> b) -> a -> b
$ do
    forall e a. Exception e => e -> IO a
E.throwIO forall a b. (a -> b) -> a -> b
$ String -> Exception
Error forall a b. (a -> b) -> a -> b
$ String
"function symbol " forall a. [a] -> [a] -> [a]
++ String
f' forall a. [a] -> [a] -> [a]
++ String
" is already used"
  FDef
fdef <-
    case ([Sort]
xs, Sort
y) of
      ([], Sort SSym
SSymBool [Sort]
_) -> do
        Int
v <- forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar (Solver -> Solver
smtSAT Solver
solver)
        forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> FDef
FBoolVar Int
v)
      ([], Sort SSym
SSymReal [Sort]
_) -> do
        Int
v <- forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Int
Simplex.newVar (Solver -> GenericSolver (Delta Rational)
smtLRA Solver
solver)
        forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> FDef
FLRAVar Int
v)
      ([], Sort (SSymBitVec Int
n) [Sort]
_) -> do
        Var
v <- Solver -> Int -> IO Var
BV.newVar' (Solver -> Solver
smtBV Solver
solver) Int
n
        forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> FDef
FBVVar Var
v)
      FunType
_ -> do
        Int
v <- Solver -> IO Int
EUF.newFSym (Solver -> Solver
smtEUF Solver
solver)
        forall (m :: * -> *) a. Monad m => a -> m a
return (FunType -> Int -> FDef
FEUFFun ([Sort]
xs,Sort
y) Int
v)
  forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (Map FSym FDef)
smtFDefs Solver
solver) forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert FSym
f FDef
fdef Map FSym FDef
fdefs
  forall (m :: * -> *) a. Monad m => a -> m a
return FSym
f

class VAFun a where
  withVArgs :: ([Expr] -> Expr) -> a
  arityVAFun :: a -> Int

instance VAFun Expr where
  withVArgs :: ([Expr] -> Expr) -> Expr
withVArgs [Expr] -> Expr
k = [Expr] -> Expr
k []
  arityVAFun :: Expr -> Int
arityVAFun Expr
_ = Int
0

instance VAFun a => VAFun (Expr -> a) where
  withVArgs :: ([Expr] -> Expr) -> Expr -> a
withVArgs [Expr] -> Expr
k Expr
x = forall a. VAFun a => ([Expr] -> Expr) -> a
withVArgs (\[Expr]
xs -> [Expr] -> Expr
k (Expr
x forall a. a -> [a] -> [a]
: [Expr]
xs))
  arityVAFun :: (Expr -> a) -> Int
arityVAFun Expr -> a
f = forall a. VAFun a => a -> Int
arityVAFun (Expr -> a
f forall a. HasCallStack => a
undefined) forall a. Num a => a -> a -> a
+ Int
1

declareFun :: VAFun a => Solver -> String -> [Sort] -> Sort -> IO a
declareFun :: forall a. VAFun a => Solver -> String -> [Sort] -> Sort -> IO a
declareFun Solver
solver String
name [Sort]
ps Sort
r = do
  FSym
fsym <- Solver -> String -> [Sort] -> Sort -> IO FSym
declareFSym Solver
solver String
name [Sort]
ps Sort
r
  let f :: a
f = forall a. VAFun a => ([Expr] -> Expr) -> a
withVArgs (FSym -> [Expr] -> Expr
EAp FSym
fsym)
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. VAFun a => a -> Int
arityVAFun a
f forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [Sort]
ps) forall a b. (a -> b) -> a -> b
$ do
    forall e a. Exception e => e -> IO a
E.throwIO forall a b. (a -> b) -> a -> b
$ String -> Exception
Error String
"ToySolver.SMT.declareFun: argument number error"
  forall (m :: * -> *) a. Monad m => a -> m a
return a
f

declareConst :: Solver -> String -> Sort -> IO Expr
declareConst :: Solver -> String -> Sort -> IO Expr
declareConst Solver
solver String
name Sort
s = forall a. VAFun a => Solver -> String -> [Sort] -> Sort -> IO a
declareFun Solver
solver String
name [] Sort
s

assert :: Solver -> Expr -> IO ()
assert :: Solver -> Expr -> IO ()
assert Solver
solver Expr
e = do
  Formula
formula <- Solver -> Expr -> IO Formula
exprToFormula Solver
solver Expr
e
  Int
n <- forall (a :: * -> * -> *) e. GenericVec a e -> IO Int
Vec.getSize (Solver -> Vec AssertionLevel
smtAssertionStack Solver
solver)
  if Int
nforall a. Ord a => a -> a -> Bool
>Int
0 then do
    AssertionLevel
assertionLevel <- forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO e
Vec.peek (Solver -> Vec AssertionLevel
smtAssertionStack Solver
solver)
    forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
smtEnc Solver
solver) forall a b. (a -> b) -> a -> b
$ Int -> Formula
Atom (AssertionLevel -> Int
alSelector AssertionLevel
assertionLevel) forall a. Boolean a => a -> a -> a
.=>. Formula
formula
  else
    forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
smtEnc Solver
solver) Formula
formula

assertNamed :: Solver -> String -> Expr -> IO ()
assertNamed :: Solver -> String -> Expr -> IO ()
assertNamed Solver
solver String
name Expr
e = do
  Int
lit <- forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Int
Tseitin.encodeFormula (Solver -> Encoder IO
smtEnc Solver
solver) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> Expr -> IO Formula
exprToFormula Solver
solver Expr
e
  forall a. IORef a -> (a -> a) -> IO ()
modifyIORef (Solver -> IORef (Map String Int)
smtNamedAssertions Solver
solver) (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
name Int
lit)

getGlobalDeclarations :: Solver -> IO Bool
getGlobalDeclarations :: Solver -> IO Bool
getGlobalDeclarations Solver
solver = forall a. IORef a -> IO a
readIORef (Solver -> IORef Bool
smtGlobalDeclarationsRef Solver
solver)

setGlobalDeclarations :: Solver -> Bool -> IO ()
setGlobalDeclarations :: Solver -> Bool -> IO ()
setGlobalDeclarations Solver
solver = forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef Bool
smtGlobalDeclarationsRef Solver
solver)

exprSort :: Solver -> Expr -> IO Sort
exprSort :: Solver -> Expr -> IO Sort
exprSort Solver
solver Expr
e = do
  Map FSym FDef
fdefs <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map FSym FDef)
smtFDefs Solver
solver)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! Map FSym FDef -> Expr -> Sort
exprSort' Map FSym FDef
fdefs Expr
e

exprSort' :: Map FSym FDef -> Expr -> Sort
exprSort' :: Map FSym FDef -> Expr -> Sort
exprSort' Map FSym FDef
_fdefs (EValue Value
v) = Value -> Sort
valSort Value
v
exprSort' Map FSym FDef
fdefs (EAp FSym
f [Expr]
xs)
  | FSym
f forall a. Ord a => a -> Set a -> Bool
`Set.member` forall a. Ord a => [a] -> Set a
Set.fromList [FSym
"true",FSym
"false",FSym
"and",FSym
"or",FSym
"xor",FSym
"not",FSym
"=>",FSym
"=",FSym
">=",FSym
"<=",FSym
">",FSym
"<"] = Sort
sBool
  | FSym
f forall a. Ord a => a -> Set a -> Bool
`Set.member` forall a. Ord a => [a] -> Set a
Set.fromList [FSym
"bvule", FSym
"bvult", FSym
"bvuge", FSym
"bvugt", FSym
"bvsle", FSym
"bvslt", FSym
"bvsge", FSym
"bvsgt"] = Sort
sBool
  | FSym
f forall a. Ord a => a -> Set a -> Bool
`Set.member` forall a. Ord a => [a] -> Set a
Set.fromList [FSym
"+", FSym
"-", FSym
"*", FSym
"/"] = Sort
sReal
  | FSym InternedText
"extract" [IndexNumeral Integer
i, IndexNumeral Integer
j] <- FSym
f = Int -> Sort
sBitVec (forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer
i forall a. Num a => a -> a -> a
- Integer
j forall a. Num a => a -> a -> a
+ Integer
1))
  | FSym
f forall a. Eq a => a -> a -> Bool
== FSym
"concat" =
      case (Map FSym FDef -> Expr -> Sort
exprSort' Map FSym FDef
fdefs ([Expr]
xs forall a. [a] -> Int -> a
!! Int
0), Map FSym FDef -> Expr -> Sort
exprSort' Map FSym FDef
fdefs ([Expr]
xs forall a. [a] -> Int -> a
!! Int
1)) of
        (Sort (SSymBitVec Int
m) [], Sort (SSymBitVec Int
n) []) -> Int -> Sort
sBitVec (Int
mforall a. Num a => a -> a -> a
+Int
n)
        (Sort, Sort)
_ -> forall a. HasCallStack => a
undefined
  | FSym InternedText
"repeat" [IndexNumeral Integer
i] <- FSym
f =
      case Map FSym FDef -> Expr -> Sort
exprSort' Map FSym FDef
fdefs ([Expr]
xs forall a. [a] -> Int -> a
!! Int
0) of
        Sort (SSymBitVec Int
m) [] -> Int -> Sort
sBitVec (Int
m forall a. Num a => a -> a -> a
* forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i)
        Sort
_ -> forall a. HasCallStack => a
undefined
  | FSym InternedText
name [IndexNumeral Integer
i] <- FSym
f, InternedText
name forall a. Eq a => a -> a -> Bool
== InternedText
"zero_extend" Bool -> Bool -> Bool
|| InternedText
name forall a. Eq a => a -> a -> Bool
== InternedText
"sign_extend" =
      case Map FSym FDef -> Expr -> Sort
exprSort' Map FSym FDef
fdefs ([Expr]
xs forall a. [a] -> Int -> a
!! Int
0) of
        Sort (SSymBitVec Int
m) [] -> Int -> Sort
sBitVec (Int
m forall a. Num a => a -> a -> a
+ forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i)
        Sort
_ -> forall a. HasCallStack => a
undefined
  | FSym InternedText
name [IndexNumeral Integer
i] <- FSym
f, InternedText
name forall a. Eq a => a -> a -> Bool
== InternedText
"rotate_left" Bool -> Bool -> Bool
|| InternedText
name forall a. Eq a => a -> a -> Bool
== InternedText
"rotate_right" =
      Map FSym FDef -> Expr -> Sort
exprSort' Map FSym FDef
fdefs ([Expr]
xs forall a. [a] -> Int -> a
!! Int
0)
  | FSym
f forall a. Eq a => a -> a -> Bool
== FSym
"bvnot" Bool -> Bool -> Bool
|| FSym
f forall a. Eq a => a -> a -> Bool
== FSym
"bvneg" = Map FSym FDef -> Expr -> Sort
exprSort' Map FSym FDef
fdefs ([Expr]
xs forall a. [a] -> Int -> a
!! Int
0)
  | FSym
f forall a. Eq a => a -> a -> Bool
== FSym
"bvcomp" = Int -> Sort
sBitVec Int
1
  | FSym
f forall a. Ord a => a -> Set a -> Bool
`Set.member` forall a. Ord a => [a] -> Set a
Set.fromList [FSym
name | (FSym
name, BV -> BV -> BV
_op::BV.BV->BV.BV->BV.BV) <- forall s bv. (IsString s, IsBV bv) => [(s, bv -> bv -> bv)]
bvBinOpsSameSize] =
      Map FSym FDef -> Expr -> Sort
exprSort' Map FSym FDef
fdefs ([Expr]
xs forall a. [a] -> Int -> a
!! Int
0)
  | FSym
f forall a. Eq a => a -> a -> Bool
== FSym
"ite" = Map FSym FDef -> Expr -> Sort
exprSort' Map FSym FDef
fdefs ([Expr]
xs forall a. [a] -> Int -> a
!! Int
1)
  | Bool
otherwise =
      case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup FSym
f Map FSym FDef
fdefs of
        Maybe FDef
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show FSym
f forall a. [a] -> [a] -> [a]
++ String
" was not found"
        Just FDef
fdef ->
          case FDef
fdef of
            FBoolVar Int
_ -> Sort
sBool
            FLRAVar Int
_ -> Sort
sReal
            FBVVar Var
v -> Int -> Sort
sBitVec (Var -> Int
BV.varWidth Var
v)
            FEUFFun ([Sort]
_,Sort
s) Int
_ -> Sort
s

-- -------------------------------------------------------------------

exprToFormula :: Solver -> Expr -> IO Tseitin.Formula
exprToFormula :: Solver -> Expr -> IO Formula
exprToFormula Solver
solver (EAp FSym
"true" [])  = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. MonotoneBoolean a => a
true
exprToFormula Solver
solver (EAp FSym
"false" []) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. MonotoneBoolean a => a
false
exprToFormula Solver
solver (EAp FSym
"and" [Expr]
xs) =
  forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. MonotoneBoolean a => [a] -> a
andB forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Solver -> Expr -> IO Formula
exprToFormula Solver
solver) [Expr]
xs
exprToFormula Solver
solver (EAp FSym
"or" [Expr]
xs) =
  forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. MonotoneBoolean a => [a] -> a
orB forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Solver -> Expr -> IO Formula
exprToFormula Solver
solver) [Expr]
xs
exprToFormula Solver
solver (EAp FSym
"xor" [Expr]
xs) = do
  [Formula]
ys <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Solver -> Expr -> IO Formula
exprToFormula Solver
solver) [Expr]
xs
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Formula
a Formula
b -> forall a. Complement a => a -> a
notB (Formula
a forall a. Boolean a => a -> a -> a
.<=>. Formula
b)) forall a. MonotoneBoolean a => a
false [Formula]
ys
exprToFormula Solver
solver (EAp FSym
"not" [Expr
x]) =
  forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. Complement a => a -> a
notB forall a b. (a -> b) -> a -> b
$ Solver -> Expr -> IO Formula
exprToFormula Solver
solver Expr
x
exprToFormula Solver
solver (EAp FSym
"not" [Expr]
_) = forall a. HasCallStack => a
undefined
exprToFormula Solver
solver (EAp FSym
"=>" [Expr
e1,Expr
e2]) = do
  Formula
b1 <- Solver -> Expr -> IO Formula
exprToFormula Solver
solver Expr
e1
  Formula
b2 <- Solver -> Expr -> IO Formula
exprToFormula Solver
solver Expr
e2
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Formula
b1 forall a. Boolean a => a -> a -> a
.=>. Formula
b2
exprToFormula Solver
solver (EAp FSym
"ite" [Expr
e1,Expr
e2,Expr
e3]) = do
  Formula
b1 <- Solver -> Expr -> IO Formula
exprToFormula Solver
solver Expr
e1
  Formula
b2 <- Solver -> Expr -> IO Formula
exprToFormula Solver
solver Expr
e2
  Formula
b3 <- Solver -> Expr -> IO Formula
exprToFormula Solver
solver Expr
e3
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall b a. IfThenElse b a => b -> a -> a -> a
ite Formula
b1 Formula
b2 Formula
b3
exprToFormula Solver
solver (EAp FSym
"=" []) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. MonotoneBoolean a => a
true -- ???
exprToFormula Solver
solver (EAp FSym
"=" [Expr]
xs) =
  Solver -> (Expr -> Expr -> IO Formula) -> [Expr] -> IO Formula
chain Solver
solver (Solver -> Expr -> Expr -> IO Formula
abstractEq Solver
solver) [Expr]
xs
exprToFormula Solver
solver (EAp FSym
"distinct" []) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. MonotoneBoolean a => a
true -- ???
exprToFormula Solver
solver (EAp FSym
"distinct" [Expr]
xs) =
  Solver -> (Expr -> Expr -> IO Formula) -> [Expr] -> IO Formula
pairwise Solver
solver (\Expr
e1 Expr
e2 -> forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. Complement a => a -> a
notB (Solver -> Expr -> Expr -> IO Formula
abstractEq Solver
solver Expr
e1 Expr
e2)) [Expr]
xs
exprToFormula Solver
solver (EAp FSym
">=" [Expr]
xs) = do
  let f :: Expr -> Expr -> IO Formula
f Expr
e1 Expr
e2 = do
        Expr Rational
e1' <- Solver -> Expr -> IO (Expr Rational)
exprToLRAExpr Solver
solver Expr
e1
        Expr Rational
e2' <- Solver -> Expr -> IO (Expr Rational)
exprToLRAExpr Solver
solver Expr
e2
        forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Int -> Formula
Atom forall a b. (a -> b) -> a -> b
$ Solver -> Atom Rational -> IO Int
abstractLRAAtom Solver
solver (Expr Rational
e1' forall e r. IsOrdRel e r => e -> e -> r
.>=. Expr Rational
e2')
  Solver -> (Expr -> Expr -> IO Formula) -> [Expr] -> IO Formula
chain Solver
solver Expr -> Expr -> IO Formula
f [Expr]
xs
exprToFormula Solver
solver (EAp FSym
"<=" [Expr]
xs) = do
    let f :: Expr -> Expr -> IO Formula
f Expr
e1 Expr
e2 = do
          Expr Rational
e1' <- Solver -> Expr -> IO (Expr Rational)
exprToLRAExpr Solver
solver Expr
e1
          Expr Rational
e2' <- Solver -> Expr -> IO (Expr Rational)
exprToLRAExpr Solver
solver Expr
e2
          forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Int -> Formula
Atom forall a b. (a -> b) -> a -> b
$ Solver -> Atom Rational -> IO Int
abstractLRAAtom Solver
solver (Expr Rational
e1' forall e r. IsOrdRel e r => e -> e -> r
.<=. Expr Rational
e2')
    Solver -> (Expr -> Expr -> IO Formula) -> [Expr] -> IO Formula
chain Solver
solver Expr -> Expr -> IO Formula
f [Expr]
xs
exprToFormula Solver
solver (EAp FSym
">" [Expr]
xs) = do
  let f :: Expr -> Expr -> IO Formula
f Expr
e1 Expr
e2 = do
        Expr Rational
e1' <- Solver -> Expr -> IO (Expr Rational)
exprToLRAExpr Solver
solver Expr
e1
        Expr Rational
e2' <- Solver -> Expr -> IO (Expr Rational)
exprToLRAExpr Solver
solver Expr
e2
        forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Int -> Formula
Atom forall a b. (a -> b) -> a -> b
$ Solver -> Atom Rational -> IO Int
abstractLRAAtom Solver
solver (Expr Rational
e1' forall e r. IsOrdRel e r => e -> e -> r
.>. Expr Rational
e2')
  Solver -> (Expr -> Expr -> IO Formula) -> [Expr] -> IO Formula
chain Solver
solver Expr -> Expr -> IO Formula
f [Expr]
xs
exprToFormula Solver
solver (EAp FSym
"<" [Expr]
xs) = do
  let f :: Expr -> Expr -> IO Formula
f Expr
e1 Expr
e2 = do
        Expr Rational
e1' <- Solver -> Expr -> IO (Expr Rational)
exprToLRAExpr Solver
solver Expr
e1
        Expr Rational
e2' <- Solver -> Expr -> IO (Expr Rational)
exprToLRAExpr Solver
solver Expr
e2
        forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Int -> Formula
Atom forall a b. (a -> b) -> a -> b
$ Solver -> Atom Rational -> IO Int
abstractLRAAtom Solver
solver (Expr Rational
e1' forall e r. IsOrdRel e r => e -> e -> r
.<. Expr Rational
e2')
  Solver -> (Expr -> Expr -> IO Formula) -> [Expr] -> IO Formula
chain Solver
solver Expr -> Expr -> IO Formula
f [Expr]
xs
exprToFormula Solver
solver (EAp FSym
f []) = do
  Map FSym FDef
fdefs <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map FSym FDef)
smtFDefs Solver
solver)
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup FSym
f Map FSym FDef
fdefs of
    Just (FBoolVar Int
v) -> forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Formula
Atom Int
v)
    Just FDef
_ -> forall e a. Exception e => e -> IO a
E.throwIO forall a b. (a -> b) -> a -> b
$ String -> Exception
Error String
"non Bool constant appears in a boolean context"
    Maybe FDef
Nothing -> forall e a. Exception e => e -> IO a
E.throwIO forall a b. (a -> b) -> a -> b
$ String -> Exception
Error forall a b. (a -> b) -> a -> b
$ String
"unknown function symbol: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show FSym
f
exprToFormula Solver
solver (EAp FSym
op [Expr
e1,Expr
e2]) | Just Expr -> Expr -> Atom
f <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup FSym
op Map FSym (Expr -> Expr -> ComparisonResult Expr)
table = do
  Expr
e1' <- Solver -> Expr -> IO Expr
exprToBVExpr Solver
solver Expr
e1
  Expr
e2' <- Solver -> Expr -> IO Expr
exprToBVExpr Solver
solver Expr
e2
  forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Int -> Formula
Atom forall a b. (a -> b) -> a -> b
$ Solver -> Atom -> IO Int
abstractBVAtom Solver
solver (Expr -> Expr -> Atom
f Expr
e1' Expr
e2')
  where
    table :: Map FSym (Expr -> Expr -> ComparisonResult Expr)
table = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
      [ (FSym
"bvule", forall a. BVComparison a => a -> a -> ComparisonResult a
BV.bvule)
      , (FSym
"bvult", forall a. BVComparison a => a -> a -> ComparisonResult a
BV.bvult)
      , (FSym
"bvuge", forall a. BVComparison a => a -> a -> ComparisonResult a
BV.bvuge)
      , (FSym
"bvugt", forall a. BVComparison a => a -> a -> ComparisonResult a
BV.bvugt)
      , (FSym
"bvsle", forall a. BVComparison a => a -> a -> ComparisonResult a
BV.bvsle)
      , (FSym
"bvslt", forall a. BVComparison a => a -> a -> ComparisonResult a
BV.bvslt)
      , (FSym
"bvsge", forall a. BVComparison a => a -> a -> ComparisonResult a
BV.bvsge)
      , (FSym
"bvsgt", forall a. BVComparison a => a -> a -> ComparisonResult a
BV.bvsgt)
      ]
exprToFormula Solver
solver (EAp FSym
f [Expr]
xs) = do
  Term
e' <- Solver -> FSym -> [Expr] -> IO Term
exprToEUFTerm Solver
solver FSym
f [Expr]
xs
  Solver -> Term -> IO Formula
formulaFromEUFTerm Solver
solver Term
e'

chain :: Solver -> (Expr -> Expr -> IO Tseitin.Formula) -> [Expr] -> IO Tseitin.Formula
chain :: Solver -> (Expr -> Expr -> IO Formula) -> [Expr] -> IO Formula
chain Solver
_ Expr -> Expr -> IO Formula
_ [] = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. MonotoneBoolean a => a
true
chain Solver
solver Expr -> Expr -> IO Formula
p [Expr]
xs = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. MonotoneBoolean a => [a] -> a
andB forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Expr -> Expr -> IO Formula
p) (forall a b. [a] -> [b] -> [(a, b)]
zip [Expr]
xs (forall a. [a] -> [a]
tail [Expr]
xs))

pairwise :: Solver -> (Expr -> Expr -> IO Tseitin.Formula) -> [Expr] -> IO Tseitin.Formula
pairwise :: Solver -> (Expr -> Expr -> IO Formula) -> [Expr] -> IO Formula
pairwise Solver
_ Expr -> Expr -> IO Formula
_ [] = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. MonotoneBoolean a => a
true
pairwise Solver
solver Expr -> Expr -> IO Formula
p [Expr]
xs = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. MonotoneBoolean a => [a] -> a
andB forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Expr -> Expr -> IO Formula
p) (forall a. [a] -> [(a, a)]
pairs [Expr]
xs)

abstractEq :: Solver -> Expr -> Expr -> IO Tseitin.Formula
abstractEq :: Solver -> Expr -> Expr -> IO Formula
abstractEq Solver
solver Expr
e1 Expr
e2 = do
  Sort
s <- Solver -> Expr -> IO Sort
exprSort Solver
solver Expr
e1
  case Sort
s of
    (Sort SSym
SSymBool [Sort]
_) -> do
      Formula
b1 <- Solver -> Expr -> IO Formula
exprToFormula Solver
solver Expr
e1
      Formula
b2 <- Solver -> Expr -> IO Formula
exprToFormula Solver
solver Expr
e2
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Formula
b1 forall a. Boolean a => a -> a -> a
.<=>. Formula
b2
    (Sort SSym
SSymReal [Sort]
_) -> do
      Expr Rational
e1' <- Solver -> Expr -> IO (Expr Rational)
exprToLRAExpr Solver
solver Expr
e1
      Expr Rational
e2' <- Solver -> Expr -> IO (Expr Rational)
exprToLRAExpr Solver
solver Expr
e2
      forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Int -> Formula
Atom forall a b. (a -> b) -> a -> b
$ Solver -> Atom Rational -> IO Int
abstractLRAAtom Solver
solver (Expr Rational
e1' forall e r. IsEqRel e r => e -> e -> r
.==. Expr Rational
e2')
    (Sort (SSymBitVec Int
_) [Sort]
_) -> do
      Expr
e1' <- Solver -> Expr -> IO Expr
exprToBVExpr Solver
solver Expr
e1
      Expr
e2' <- Solver -> Expr -> IO Expr
exprToBVExpr Solver
solver Expr
e2
      forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Int -> Formula
Atom forall a b. (a -> b) -> a -> b
$ Solver -> Atom -> IO Int
abstractBVAtom Solver
solver (Expr
e1' forall e r. IsEqRel e r => e -> e -> r
.==. Expr
e2')
    (Sort (SSymUninterpreted InternedText
_ Int
_) [Sort]
_) -> do
      Term
e1' <- Solver -> Expr -> IO Term
exprToEUFArg Solver
solver Expr
e1
      Term
e2' <- Solver -> Expr -> IO Term
exprToEUFArg Solver
solver Expr
e2
      forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Int -> Formula
Atom forall a b. (a -> b) -> a -> b
$ Solver -> (Term, Term) -> IO Int
abstractEUFAtom Solver
solver (Term
e1',Term
e2')

-- -------------------------------------------------------------------

exprToLRAExpr :: Solver -> Expr -> IO (LA.Expr Rational)
exprToLRAExpr :: Solver -> Expr -> IO (Expr Rational)
exprToLRAExpr Solver
solver (EValue (ValRational Rational
r)) = forall (m :: * -> *) a. Monad m => a -> m a
return (forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
r)
exprToLRAExpr Solver
solver (EAp FSym
"-" []) = forall e a. Exception e => e -> IO a
E.throwIO forall a b. (a -> b) -> a -> b
$ String -> Exception
Error String
"ToySolver.SMT: nullary '-' function"
exprToLRAExpr Solver
solver (EAp FSym
"-" [Expr
x]) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall v. AdditiveGroup v => v -> v
negateV forall a b. (a -> b) -> a -> b
$ Solver -> Expr -> IO (Expr Rational)
exprToLRAExpr Solver
solver Expr
x
exprToLRAExpr Solver
solver (EAp FSym
"-" (Expr
x:[Expr]
xs)) = do
  Expr Rational
x' <- Solver -> Expr -> IO (Expr Rational)
exprToLRAExpr Solver
solver Expr
x
  [Expr Rational]
xs' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Solver -> Expr -> IO (Expr Rational)
exprToLRAExpr Solver
solver) [Expr]
xs
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall v. AdditiveGroup v => v -> v -> v
(^-^) Expr Rational
x' [Expr Rational]
xs'
exprToLRAExpr Solver
solver (EAp FSym
"+" [Expr]
xs) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall (f :: * -> *) v. (Foldable f, AdditiveGroup v) => f v -> v
sumV forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Solver -> Expr -> IO (Expr Rational)
exprToLRAExpr Solver
solver) [Expr]
xs
exprToLRAExpr Solver
solver (EAp FSym
"*" [Expr]
xs) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall {r}. (Num r, Eq r) => Expr r -> Expr r -> Expr r
mult (forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
1)) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Solver -> Expr -> IO (Expr Rational)
exprToLRAExpr Solver
solver) [Expr]
xs
  where
    mult :: Expr r -> Expr r -> Expr r
mult Expr r
e1 Expr r
e2
      | Just r
c <- forall r. Num r => Expr r -> Maybe r
LA.asConst Expr r
e1 = r
c forall v. VectorSpace v => Scalar v -> v -> v
*^ Expr r
e2
      | Just r
c <- forall r. Num r => Expr r -> Maybe r
LA.asConst Expr r
e2 = r
c forall v. VectorSpace v => Scalar v -> v -> v
*^ Expr r
e1
      | Bool
otherwise = forall a e. Exception e => e -> a
E.throw forall a b. (a -> b) -> a -> b
$ String -> Exception
Error String
"non-linear multiplication is not supported"
exprToLRAExpr Solver
solver (EAp FSym
"/" [Expr
x,Expr
y]) = do
  Expr Rational
y' <- Solver -> Expr -> IO (Expr Rational)
exprToLRAExpr Solver
solver Expr
y
  case forall r. Num r => Expr r -> Maybe r
LA.asConst Expr Rational
y' of
    Maybe Rational
Nothing -> forall e a. Exception e => e -> IO a
E.throwIO forall a b. (a -> b) -> a -> b
$ String -> Exception
Error String
"division by non-constant is not supported"
    Just Rational
0 -> do
      Solver -> Term -> IO (Expr Rational)
lraExprFromTerm Solver
solver forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> FSym -> [Expr] -> IO Term
exprToEUFTerm Solver
solver FSym
"_/0" [Expr
x]
    Just Rational
c -> do
      Expr Rational
x' <- Solver -> Expr -> IO (Expr Rational)
exprToLRAExpr Solver
solver Expr
x
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Rational
1forall a. Fractional a => a -> a -> a
/Rational
c) forall v. VectorSpace v => Scalar v -> v -> v
*^ Expr Rational
x'
exprToLRAExpr Solver
solver (EAp FSym
"ite" [Expr
c,Expr
t,Expr
e]) = do
  Formula
c' <- Solver -> Expr -> IO Formula
exprToFormula Solver
solver Expr
c
  Expr Rational
ret <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall r. Num r => Int -> Expr r
LA.var forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Int
Simplex.newVar (Solver -> GenericSolver (Delta Rational)
smtLRA Solver
solver)
  Expr Rational
t' <- Solver -> Expr -> IO (Expr Rational)
exprToLRAExpr Solver
solver Expr
t
  Expr Rational
e' <- Solver -> Expr -> IO (Expr Rational)
exprToLRAExpr Solver
solver Expr
e
  Int
c1 <- Solver -> Atom Rational -> IO Int
abstractLRAAtom Solver
solver (Expr Rational
ret forall e r. IsEqRel e r => e -> e -> r
.==. Expr Rational
t')
  Int
c2 <- Solver -> Atom Rational -> IO Int
abstractLRAAtom Solver
solver (Expr Rational
ret forall e r. IsEqRel e r => e -> e -> r
.==. Expr Rational
e')
  forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
smtEnc Solver
solver) forall a b. (a -> b) -> a -> b
$ forall b a. IfThenElse b a => b -> a -> a -> a
ite Formula
c' (Int -> Formula
Atom Int
c1) (Int -> Formula
Atom Int
c2)
  forall (m :: * -> *) a. Monad m => a -> m a
return Expr Rational
ret
exprToLRAExpr Solver
solver (EAp FSym
f [Expr]
xs) =
  Solver -> Term -> IO (Expr Rational)
lraExprFromTerm Solver
solver forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> FSym -> [Expr] -> IO Term
exprToEUFTerm Solver
solver FSym
f [Expr]
xs

abstractLRAAtom :: Solver -> LA.Atom Rational -> IO SAT.Lit
abstractLRAAtom :: Solver -> Atom Rational -> IO Int
abstractLRAAtom Solver
solver Atom Rational
atom = do
  (Int
v,RelOp
op,Rational
rhs) <- forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> Atom Rational -> m (Int, RelOp, Rational)
Simplex.simplifyAtom (Solver -> GenericSolver (Delta Rational)
smtLRA Solver
solver) Atom Rational
atom
  (Map (Int, Rational) (Int, Int, Int)
tbl,IntMap (Atom Rational)
defs) <- forall a. IORef a -> IO a
readIORef (Solver
-> IORef
     (Map (Int, Rational) (Int, Int, Int), IntMap (Atom Rational))
smtLRAAtomDefs Solver
solver)
  (Int
vLt, Int
vEq, Int
vGt) <-
    case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Int
v,Rational
rhs) Map (Int, Rational) (Int, Int, Int)
tbl of
      Just (Int
vLt, Int
vEq, Int
vGt) -> forall (m :: * -> *) a. Monad m => a -> m a
return (Int
vLt, Int
vEq, Int
vGt)
      Maybe (Int, Int, Int)
Nothing -> do
        Int
vLt <- forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar (Solver -> Solver
smtSAT Solver
solver)
        Int
vEq <- forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar (Solver -> Solver
smtSAT Solver
solver)
        Int
vGt <- forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar (Solver -> Solver
smtSAT Solver
solver)
        forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause (Solver -> Solver
smtSAT Solver
solver) [Int
vLt,Int
vEq,Int
vGt]
        forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause (Solver -> Solver
smtSAT Solver
solver) [-Int
vLt, -Int
vEq]
        forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause (Solver -> Solver
smtSAT Solver
solver) [-Int
vLt, -Int
vGt]
        forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause (Solver -> Solver
smtSAT Solver
solver) [-Int
vEq, -Int
vGt]
        let xs :: IntMap (Atom Rational)
xs = forall a. [(Int, a)] -> IntMap a
IntMap.fromList
                 [ (Int
vEq,  forall r. Num r => Int -> Expr r
LA.var Int
v forall e r. IsEqRel e r => e -> e -> r
.==. forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
rhs)
                 , (Int
vLt,  forall r. Num r => Int -> Expr r
LA.var Int
v forall e r. IsOrdRel e r => e -> e -> r
.<.  forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
rhs)
                 , (Int
vGt,  forall r. Num r => Int -> Expr r
LA.var Int
v forall e r. IsOrdRel e r => e -> e -> r
.>.  forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
rhs)
                 , (-Int
vLt, forall r. Num r => Int -> Expr r
LA.var Int
v forall e r. IsOrdRel e r => e -> e -> r
.>=. forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
rhs)
                 , (-Int
vGt, forall r. Num r => Int -> Expr r
LA.var Int
v forall e r. IsOrdRel e r => e -> e -> r
.<=. forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
rhs)
                 ]
        forall a. IORef a -> a -> IO ()
writeIORef (Solver
-> IORef
     (Map (Int, Rational) (Int, Int, Int), IntMap (Atom Rational))
smtLRAAtomDefs Solver
solver) (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Int
v,Rational
rhs) (Int
vLt, Int
vEq, Int
vGt) Map (Int, Rational) (Int, Int, Int)
tbl, forall a. IntMap a -> IntMap a -> IntMap a
IntMap.union IntMap (Atom Rational)
xs IntMap (Atom Rational)
defs)
        forall (m :: * -> *) a. Monad m => a -> m a
return (Int
vLt, Int
vEq, Int
vGt)
  case RelOp
op of
    RelOp
Lt  -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
vLt
    RelOp
Gt  -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
vGt
    RelOp
Eql -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
vEq
    RelOp
Le  -> forall (m :: * -> *) a. Monad m => a -> m a
return (-Int
vGt)
    RelOp
Ge  -> forall (m :: * -> *) a. Monad m => a -> m a
return (-Int
vLt)
    RelOp
NEq -> forall (m :: * -> *) a. Monad m => a -> m a
return (-Int
vEq)


lraExprToEUFTerm :: Solver -> LA.Expr Rational -> IO EUF.Term
lraExprToEUFTerm :: Solver -> Expr Rational -> IO Term
lraExprToEUFTerm Solver
solver Expr Rational
e = do
  (Map (Expr Rational) Int
realToFSym, IntMap (Expr Rational)
fsymToReal) <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map (Expr Rational) Int, IntMap (Expr Rational))
smtRealTermDefs Solver
solver)
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Expr Rational
e Map (Expr Rational) Int
realToFSym of
    Just Int
c -> forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [Term] -> Term
EUF.TApp Int
c [])
    Maybe Int
Nothing -> do
      Int
c <- Solver -> IO Int
EUF.newFSym (Solver -> Solver
smtEUF Solver
solver)
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (Expr Rational)
fsymToReal) forall a b. (a -> b) -> a -> b
$ \(Int
d, Expr Rational
d_lra) -> do
        -- allocate interface equalities
        Int
b1 <- Solver -> (Term, Term) -> IO Int
abstractEUFAtom Solver
solver (Int -> [Term] -> Term
EUF.TApp Int
c [], Int -> [Term] -> Term
EUF.TApp Int
d [])
        Int
b2 <- Solver -> Atom Rational -> IO Int
abstractLRAAtom Solver
solver (Expr Rational
e forall e r. IsEqRel e r => e -> e -> r
.==. Expr Rational
d_lra)
        forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
smtEnc Solver
solver) (Int -> Formula
Atom Int
b1 forall a. Boolean a => a -> a -> a
.<=>. Int -> Formula
Atom Int
b2)
      forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (Map (Expr Rational) Int, IntMap (Expr Rational))
smtRealTermDefs Solver
solver) forall a b. (a -> b) -> a -> b
$
        ( forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Expr Rational
e Int
c Map (Expr Rational) Int
realToFSym
        , forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
c Expr Rational
e IntMap (Expr Rational)
fsymToReal
        )
      forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [Term] -> Term
EUF.TApp Int
c [])

lraExprFromTerm :: Solver -> EUF.Term -> IO (LA.Expr Rational)
lraExprFromTerm :: Solver -> Term -> IO (Expr Rational)
lraExprFromTerm Solver
solver Term
t = do
  (Map (Expr Rational) Int
realToFSym, IntMap (Expr Rational)
fsymToReal) <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map (Expr Rational) Int, IntMap (Expr Rational))
smtRealTermDefs Solver
solver)
  Int
c <- Solver -> Term -> IO Int
EUF.termToFSym (Solver -> Solver
smtEUF Solver
solver) Term
t
  case forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
c IntMap (Expr Rational)
fsymToReal of
    Just Expr Rational
e -> forall (m :: * -> *) a. Monad m => a -> m a
return Expr Rational
e
    Maybe (Expr Rational)
Nothing -> do
      Int
v <- forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Int
Simplex.newVar (Solver -> GenericSolver (Delta Rational)
smtLRA Solver
solver)
      let e :: Expr Rational
e = forall r. Num r => Int -> Expr r
LA.var Int
v
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (Expr Rational)
fsymToReal) forall a b. (a -> b) -> a -> b
$ \(Int
d, Expr Rational
d_lra) -> do
        -- allocate interface equalities
        Int
b1 <- Solver -> (Term, Term) -> IO Int
abstractEUFAtom Solver
solver (Int -> [Term] -> Term
EUF.TApp Int
c [], Int -> [Term] -> Term
EUF.TApp Int
d [])
        Int
b2 <- Solver -> Atom Rational -> IO Int
abstractLRAAtom Solver
solver (Expr Rational
e forall e r. IsEqRel e r => e -> e -> r
.==. Expr Rational
d_lra)
        forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
smtEnc Solver
solver) (Int -> Formula
Atom Int
b1 forall a. Boolean a => a -> a -> a
.<=>. Int -> Formula
Atom Int
b2)
      forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (Map (Expr Rational) Int, IntMap (Expr Rational))
smtRealTermDefs Solver
solver) forall a b. (a -> b) -> a -> b
$
        ( forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Expr Rational
e Int
c Map (Expr Rational) Int
realToFSym
        , forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
c Expr Rational
e IntMap (Expr Rational)
fsymToReal
        )
      forall (m :: * -> *) a. Monad m => a -> m a
return Expr Rational
e

-- -------------------------------------------------------------------

bvBinOpsSameSize :: (IsString s, BV.IsBV bv) => [(s, bv -> bv -> bv)]
bvBinOpsSameSize :: forall s bv. (IsString s, IsBV bv) => [(s, bv -> bv -> bv)]
bvBinOpsSameSize =
  [ (s
"bvand", forall a. IsBV a => a -> a -> a
BV.bvand)
  , (s
"bvor", forall a. IsBV a => a -> a -> a
BV.bvor)
  , (s
"bvxor", forall a. IsBV a => a -> a -> a
BV.bvxor)
  , (s
"bvnand", forall a. IsBV a => a -> a -> a
BV.bvnand)
  , (s
"bvnor", forall a. IsBV a => a -> a -> a
BV.bvnor)
  , (s
"bvxnor", forall a. IsBV a => a -> a -> a
BV.bvxnor)
  , (s
"bvadd", forall a. IsBV a => a -> a -> a
BV.bvadd)
  , (s
"bvsub", forall a. IsBV a => a -> a -> a
BV.bvsub)
  , (s
"bvmul", forall a. IsBV a => a -> a -> a
BV.bvmul)
  , (s
"bvudiv", forall a. IsBV a => a -> a -> a
BV.bvudiv)
  , (s
"bvurem", forall a. IsBV a => a -> a -> a
BV.bvurem)
  , (s
"bvsdiv", forall a. IsBV a => a -> a -> a
BV.bvsdiv)
  , (s
"bvsrem", forall a. IsBV a => a -> a -> a
BV.bvsrem)
  , (s
"bvsmod", forall a. IsBV a => a -> a -> a
BV.bvsmod)
  , (s
"bvshl", forall a. IsBV a => a -> a -> a
BV.bvshl)
  , (s
"bvlshr", forall a. IsBV a => a -> a -> a
BV.bvlshr)
  , (s
"bvashr", forall a. IsBV a => a -> a -> a
BV.bvashr)
  ]

exprToBVExpr :: Solver -> Expr -> IO BV.Expr
exprToBVExpr :: Solver -> Expr -> IO Expr
exprToBVExpr Solver
solver (EValue (ValBitVec BV
bv)) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. IsBV a => BV -> a
BV.fromBV BV
bv
exprToBVExpr Solver
solver (EAp FSym
"concat" [Expr
x,Expr
y]) = do
  forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall a. Semigroup a => a -> a -> a
(<>) (Solver -> Expr -> IO Expr
exprToBVExpr Solver
solver Expr
x) (Solver -> Expr -> IO Expr
exprToBVExpr Solver
solver Expr
y)
exprToBVExpr Solver
solver (EAp (FSym InternedText
"extract" [IndexNumeral Integer
i, IndexNumeral Integer
j]) [Expr
x]) = do
  forall a. IsBV a => Int -> Int -> a -> a
BV.extract (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i) (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
j) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver -> Expr -> IO Expr
exprToBVExpr Solver
solver Expr
x
exprToBVExpr Solver
solver (EAp (FSym InternedText
"repeat" [IndexNumeral Integer
i]) [Expr
x]) = do
  forall m. Monoid m => Int -> m -> m
BV.repeat (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver -> Expr -> IO Expr
exprToBVExpr Solver
solver Expr
x
exprToBVExpr Solver
solver (EAp (FSym InternedText
"zero_extend" [IndexNumeral Integer
i]) [Expr
x]) = do
  forall a. IsBV a => Int -> a -> a
BV.zeroExtend (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver -> Expr -> IO Expr
exprToBVExpr Solver
solver Expr
x
exprToBVExpr Solver
solver (EAp (FSym InternedText
"sign_extend" [IndexNumeral Integer
i]) [Expr
x]) = do
  forall a. IsBV a => Int -> a -> a
BV.signExtend (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver -> Expr -> IO Expr
exprToBVExpr Solver
solver Expr
x
exprToBVExpr Solver
solver (EAp (FSym InternedText
"rotate_left" [IndexNumeral Integer
i]) [Expr
x]) = do
  forall a. Bits a => a -> Int -> a
rotateL forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver -> Expr -> IO Expr
exprToBVExpr Solver
solver Expr
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i)
exprToBVExpr Solver
solver (EAp (FSym InternedText
"rotate_right" [IndexNumeral Integer
i]) [Expr
x]) = do
  forall a. Bits a => a -> Int -> a
rotateR forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver -> Expr -> IO Expr
exprToBVExpr Solver
solver Expr
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i)
exprToBVExpr Solver
solver (EAp (FSym InternedText
op1 []) [Expr
x])
  | Just Expr -> Expr
op1' <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup InternedText
op1 Map InternedText (Expr -> Expr)
table = Expr -> Expr
op1' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver -> Expr -> IO Expr
exprToBVExpr Solver
solver Expr
x
  where
    table :: Map InternedText (Expr -> Expr)
table =
      forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
      [ (InternedText
"bvnot", forall a. IsBV a => a -> a
BV.bvnot)
      , (InternedText
"bvneg", forall a. IsBV a => a -> a
BV.bvneg)
      ]
exprToBVExpr Solver
solver (EAp (FSym InternedText
op2 []) [Expr
x,Expr
y])
  | Just Expr -> Expr -> Expr
op2' <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup InternedText
op2 Map InternedText (Expr -> Expr -> Expr)
table = forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Expr -> Expr -> Expr
op2' (Solver -> Expr -> IO Expr
exprToBVExpr Solver
solver Expr
x) (Solver -> Expr -> IO Expr
exprToBVExpr Solver
solver Expr
y)
  where
    table :: Map InternedText (Expr -> Expr -> Expr)
table = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ [(InternedText
"bvcomp", forall a. IsBV a => a -> a -> a
BV.bvcomp)] forall a. [a] -> [a] -> [a]
++ forall s bv. (IsString s, IsBV bv) => [(s, bv -> bv -> bv)]
bvBinOpsSameSize
exprToBVExpr Solver
solver (EAp FSym
"ite" [Expr
c,Expr
t,Expr
e]) = do
  Formula
c' <- Solver -> Expr -> IO Formula
exprToFormula Solver
solver Expr
c
  Expr
t' <- Solver -> Expr -> IO Expr
exprToBVExpr Solver
solver Expr
t
  Expr
e' <- Solver -> Expr -> IO Expr
exprToBVExpr Solver
solver Expr
e
  Expr
ret <- Solver -> Int -> IO Expr
BV.newVar (Solver -> Solver
smtBV Solver
solver) (forall a. IsBV a => a -> Int
BV.width Expr
t')
  Int
c1 <- Solver -> Atom -> IO Int
abstractBVAtom Solver
solver (Expr
ret forall e r. IsEqRel e r => e -> e -> r
.==. Expr
t')
  Int
c2 <- Solver -> Atom -> IO Int
abstractBVAtom Solver
solver (Expr
ret forall e r. IsEqRel e r => e -> e -> r
.==. Expr
e')
  forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
smtEnc Solver
solver) forall a b. (a -> b) -> a -> b
$ forall b a. IfThenElse b a => b -> a -> a -> a
ite Formula
c' (Int -> Formula
Atom Int
c1) (Int -> Formula
Atom Int
c2)
  forall (m :: * -> *) a. Monad m => a -> m a
return Expr
ret
exprToBVExpr Solver
solver e :: Expr
e@(EAp FSym
f [Expr]
xs) = do
  Sort
s <- Solver -> Expr -> IO Sort
exprSort Solver
solver Expr
e
  case Sort
s of
    Sort (SSymBitVec Int
w) [] -> do
      Term
t <- Solver -> FSym -> [Expr] -> IO Term
exprToEUFTerm Solver
solver FSym
f [Expr]
xs
      Solver -> Term -> Int -> IO Expr
bvExprFromTerm Solver
solver Term
t Int
w
    Sort
_ -> forall a. HasCallStack => String -> a
error String
"should not happen"

data BVAtomNormalized
  = BVEql BV.Expr BV.Expr
  | BVULt BV.Expr BV.Expr
  | BVSLt BV.Expr BV.Expr
  deriving (BVAtomNormalized -> BVAtomNormalized -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BVAtomNormalized -> BVAtomNormalized -> Bool
$c/= :: BVAtomNormalized -> BVAtomNormalized -> Bool
== :: BVAtomNormalized -> BVAtomNormalized -> Bool
$c== :: BVAtomNormalized -> BVAtomNormalized -> Bool
Eq, Eq BVAtomNormalized
BVAtomNormalized -> BVAtomNormalized -> Bool
BVAtomNormalized -> BVAtomNormalized -> Ordering
BVAtomNormalized -> BVAtomNormalized -> BVAtomNormalized
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 :: BVAtomNormalized -> BVAtomNormalized -> BVAtomNormalized
$cmin :: BVAtomNormalized -> BVAtomNormalized -> BVAtomNormalized
max :: BVAtomNormalized -> BVAtomNormalized -> BVAtomNormalized
$cmax :: BVAtomNormalized -> BVAtomNormalized -> BVAtomNormalized
>= :: BVAtomNormalized -> BVAtomNormalized -> Bool
$c>= :: BVAtomNormalized -> BVAtomNormalized -> Bool
> :: BVAtomNormalized -> BVAtomNormalized -> Bool
$c> :: BVAtomNormalized -> BVAtomNormalized -> Bool
<= :: BVAtomNormalized -> BVAtomNormalized -> Bool
$c<= :: BVAtomNormalized -> BVAtomNormalized -> Bool
< :: BVAtomNormalized -> BVAtomNormalized -> Bool
$c< :: BVAtomNormalized -> BVAtomNormalized -> Bool
compare :: BVAtomNormalized -> BVAtomNormalized -> Ordering
$ccompare :: BVAtomNormalized -> BVAtomNormalized -> Ordering
Ord)

normalizeBVAtom :: BV.Atom -> (BVAtomNormalized, Bool)
normalizeBVAtom :: Atom -> (BVAtomNormalized, Bool)
normalizeBVAtom (BV.Rel (OrdRel Expr
lhs RelOp
op Expr
rhs) Bool
False) =
  case RelOp
op of
    RelOp
Lt  -> (Expr -> Expr -> BVAtomNormalized
BVULt Expr
lhs Expr
rhs, Bool
True)
    RelOp
Gt  -> (Expr -> Expr -> BVAtomNormalized
BVULt Expr
rhs Expr
lhs, Bool
True)
    RelOp
Eql -> (Expr -> Expr -> BVAtomNormalized
BVEql Expr
lhs Expr
rhs, Bool
True)
    RelOp
NEq -> (Expr -> Expr -> BVAtomNormalized
BVEql Expr
lhs Expr
rhs, Bool
False)
    RelOp
Le  -> (Expr -> Expr -> BVAtomNormalized
BVULt Expr
rhs Expr
lhs, Bool
False)
    RelOp
Ge  -> (Expr -> Expr -> BVAtomNormalized
BVULt Expr
lhs Expr
rhs, Bool
False)
normalizeBVAtom (BV.Rel (OrdRel Expr
lhs RelOp
op Expr
rhs) Bool
True) =
  case RelOp
op of
    RelOp
Lt  -> (Expr -> Expr -> BVAtomNormalized
BVSLt Expr
lhs Expr
rhs, Bool
True)
    RelOp
Gt  -> (Expr -> Expr -> BVAtomNormalized
BVSLt Expr
rhs Expr
lhs, Bool
True)
    RelOp
Eql -> (Expr -> Expr -> BVAtomNormalized
BVEql Expr
lhs Expr
rhs, Bool
True)
    RelOp
NEq -> (Expr -> Expr -> BVAtomNormalized
BVEql Expr
lhs Expr
rhs, Bool
False)
    RelOp
Le  -> (Expr -> Expr -> BVAtomNormalized
BVSLt Expr
rhs Expr
lhs, Bool
False)
    RelOp
Ge  -> (Expr -> Expr -> BVAtomNormalized
BVSLt Expr
lhs Expr
rhs, Bool
False)

unnormalizeBVAtom :: (BVAtomNormalized, Bool) -> BV.Atom
unnormalizeBVAtom :: (BVAtomNormalized, Bool) -> Atom
unnormalizeBVAtom (BVEql Expr
lhs Expr
rhs, Bool
p) = (if Bool
p then forall a. a -> a
id else forall a. Complement a => a -> a
notB) forall a b. (a -> b) -> a -> b
$ OrdRel Expr -> Bool -> Atom
BV.Rel (forall e. e -> RelOp -> e -> OrdRel e
OrdRel Expr
lhs RelOp
Eql Expr
rhs) Bool
False
unnormalizeBVAtom (BVULt Expr
lhs Expr
rhs, Bool
p) = (if Bool
p then forall a. a -> a
id else forall a. Complement a => a -> a
notB) forall a b. (a -> b) -> a -> b
$ OrdRel Expr -> Bool -> Atom
BV.Rel (forall e. e -> RelOp -> e -> OrdRel e
OrdRel Expr
lhs RelOp
Lt Expr
rhs) Bool
False
unnormalizeBVAtom (BVSLt Expr
lhs Expr
rhs, Bool
p) = (if Bool
p then forall a. a -> a
id else forall a. Complement a => a -> a
notB) forall a b. (a -> b) -> a -> b
$ OrdRel Expr -> Bool -> Atom
BV.Rel (forall e. e -> RelOp -> e -> OrdRel e
OrdRel Expr
lhs RelOp
Lt Expr
rhs) Bool
True

abstractBVAtom :: Solver -> BV.Atom -> IO SAT.Lit
abstractBVAtom :: Solver -> Atom -> IO Int
abstractBVAtom Solver
solver Atom
atom = do
  let (BVAtomNormalized
atom', Bool
s) = Atom -> (BVAtomNormalized, Bool)
normalizeBVAtom Atom
atom
  (Map BVAtomNormalized Int
tbl,IntMap BVAtomNormalized
defs) <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map BVAtomNormalized Int, IntMap BVAtomNormalized)
smtBVAtomDefs Solver
solver)
  Int
v <- case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup BVAtomNormalized
atom' Map BVAtomNormalized Int
tbl of
         Just Int
v -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
v
         Maybe Int
Nothing -> do
           Int
v <- forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar (Solver -> Solver
smtSAT Solver
solver)
           forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (Map BVAtomNormalized Int, IntMap BVAtomNormalized)
smtBVAtomDefs Solver
solver) (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert BVAtomNormalized
atom' Int
v Map BVAtomNormalized Int
tbl, forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
v BVAtomNormalized
atom' IntMap BVAtomNormalized
defs)
           forall (m :: * -> *) a. Monad m => a -> m a
return Int
v
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if Bool
s then Int
v else -Int
v

bvExprToEUFTerm :: Solver -> BV.Expr -> IO EUF.Term
bvExprToEUFTerm :: Solver -> Expr -> IO Term
bvExprToEUFTerm Solver
solver Expr
e = do
  (Map Expr Int
bvToFSym, IntMap (IntMap Expr)
fsymToBV) <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map Expr Int, IntMap (IntMap Expr))
smtBVTermDefs Solver
solver)
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Expr
e Map Expr Int
bvToFSym of
    Just Int
c -> forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [Term] -> Term
EUF.TApp Int
c [])
    Maybe Int
Nothing -> do
      Int
c <- Solver -> IO Int
EUF.newFSym (Solver -> Solver
smtEUF Solver
solver)
      let w :: Int
w = forall a. IsBV a => a -> Int
BV.width Expr
e
          m :: IntMap Expr
m = forall a. a -> Int -> IntMap a -> a
IntMap.findWithDefault forall a. IntMap a
IntMap.empty Int
w IntMap (IntMap Expr)
fsymToBV
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap Expr
m) forall a b. (a -> b) -> a -> b
$ \(Int
d, Expr
d_bv) -> do
        -- allocate interface equalities
        Int
b1 <- Solver -> (Term, Term) -> IO Int
abstractEUFAtom Solver
solver (Int -> [Term] -> Term
EUF.TApp Int
c [], Int -> [Term] -> Term
EUF.TApp Int
d [])
        Int
b2 <- Solver -> Atom -> IO Int
abstractBVAtom Solver
solver (Expr
e forall e r. IsEqRel e r => e -> e -> r
.==. Expr
d_bv)
        forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
smtEnc Solver
solver) (Int -> Formula
Atom Int
b1 forall a. Boolean a => a -> a -> a
.<=>. Int -> Formula
Atom Int
b2)
      forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (Map Expr Int, IntMap (IntMap Expr))
smtBVTermDefs Solver
solver) forall a b. (a -> b) -> a -> b
$
        ( forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Expr
e Int
c Map Expr Int
bvToFSym
        , forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
w (forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
c Expr
e IntMap Expr
m) IntMap (IntMap Expr)
fsymToBV
        )
      forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [Term] -> Term
EUF.TApp Int
c [])

bvExprFromTerm :: Solver -> EUF.Term -> Int -> IO BV.Expr
bvExprFromTerm :: Solver -> Term -> Int -> IO Expr
bvExprFromTerm Solver
solver Term
t Int
w = do
  (Map Expr Int
bvToFSym, IntMap (IntMap Expr)
fsymToBV) <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map Expr Int, IntMap (IntMap Expr))
smtBVTermDefs Solver
solver)
  Int
c <- Solver -> Term -> IO Int
EUF.termToFSym (Solver -> Solver
smtEUF Solver
solver) Term
t
  let m :: IntMap Expr
m = forall a. a -> Int -> IntMap a -> a
IntMap.findWithDefault forall a. IntMap a
IntMap.empty Int
w IntMap (IntMap Expr)
fsymToBV
  case forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
c IntMap Expr
m of
    Just Expr
e -> forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
    Maybe Expr
Nothing -> do
      Expr
e <- Solver -> Int -> IO Expr
BV.newVar (Solver -> Solver
smtBV Solver
solver) Int
w
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap Expr
m) forall a b. (a -> b) -> a -> b
$ \(Int
d, Expr
d_bv) -> do
        -- allocate interface equalities
        Int
b1 <- Solver -> (Term, Term) -> IO Int
abstractEUFAtom Solver
solver (Int -> [Term] -> Term
EUF.TApp Int
c [], Int -> [Term] -> Term
EUF.TApp Int
d [])
        Int
b2 <- Solver -> Atom -> IO Int
abstractBVAtom Solver
solver (Expr
e forall e r. IsEqRel e r => e -> e -> r
.==. Expr
d_bv)
        forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
smtEnc Solver
solver) (Int -> Formula
Atom Int
b1 forall a. Boolean a => a -> a -> a
.<=>. Int -> Formula
Atom Int
b2)
      forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (Map Expr Int, IntMap (IntMap Expr))
smtBVTermDefs Solver
solver) forall a b. (a -> b) -> a -> b
$
        ( forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Expr
e Int
c Map Expr Int
bvToFSym
        , forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
w (forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
c Expr
e IntMap Expr
m) IntMap (IntMap Expr)
fsymToBV
        )
      forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e

-- -------------------------------------------------------------------

exprToEUFTerm :: Solver -> FSym -> [Expr] -> IO EUF.Term
exprToEUFTerm :: Solver -> FSym -> [Expr] -> IO Term
exprToEUFTerm Solver
solver FSym
"ite" [Expr
c,Expr
t,Expr
e] = do
  Formula
c' <- Solver -> Expr -> IO Formula
exprToFormula Solver
solver Expr
c
  Term
ret <- Solver -> IO Term
EUF.newConst (Solver -> Solver
smtEUF Solver
solver)
  Term
t' <- Solver -> Expr -> IO Term
exprToEUFArg Solver
solver Expr
t
  Term
e' <- Solver -> Expr -> IO Term
exprToEUFArg Solver
solver Expr
e
  Int
c1 <- Solver -> (Term, Term) -> IO Int
abstractEUFAtom Solver
solver (Term
ret, Term
t')
  Int
c2 <- Solver -> (Term, Term) -> IO Int
abstractEUFAtom Solver
solver (Term
ret, Term
e')
  forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
smtEnc Solver
solver) forall a b. (a -> b) -> a -> b
$ forall b a. IfThenElse b a => b -> a -> a -> a
ite Formula
c' (Int -> Formula
Atom Int
c1) (Int -> Formula
Atom Int
c2)
  forall (m :: * -> *) a. Monad m => a -> m a
return Term
ret
exprToEUFTerm Solver
solver FSym
f [Expr]
xs = do
  Map FSym FDef
fdefs <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map FSym FDef)
smtFDefs Solver
solver)
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup FSym
f Map FSym FDef
fdefs of
    Just (FBoolVar Int
v) -> Solver -> Formula -> IO Term
formulaToEUFTerm Solver
solver (Int -> Formula
Atom Int
v)
    Just (FLRAVar Int
v) -> Solver -> Expr Rational -> IO Term
lraExprToEUFTerm Solver
solver (forall r. Num r => Int -> Expr r
LA.var Int
v)
    Just (FBVVar Var
v) -> Solver -> Expr -> IO Term
bvExprToEUFTerm Solver
solver (Var -> Expr
BV.EVar Var
v)
    Just (FEUFFun ([Sort]
ps,Sort
_) Int
fsym) -> do
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Sort]
ps forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
xs) forall a b. (a -> b) -> a -> b
$ do
        forall e a. Exception e => e -> IO a
E.throwIO forall a b. (a -> b) -> a -> b
$ String -> Exception
Error String
"argument number error"
      forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> [Term] -> Term
EUF.TApp Int
fsym) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Solver -> Expr -> IO Term
exprToEUFArg Solver
solver) [Expr]
xs
    Maybe FDef
_ -> forall a e. Exception e => e -> a
E.throw forall a b. (a -> b) -> a -> b
$ String -> Exception
Error forall a b. (a -> b) -> a -> b
$ String
"unknown function symbol: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show FSym
f

valToEUFArg :: Solver -> Value -> IO EUF.Term
valToEUFArg :: Solver -> Value -> IO Term
valToEUFArg Solver
solver (ValBool Bool
b) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! if Bool
b then Solver -> Term
smtEUFTrue Solver
solver else Solver -> Term
smtEUFFalse Solver
solver
valToEUFArg Solver
solver (ValRational Rational
r) = Solver -> Expr Rational -> IO Term
lraExprToEUFTerm Solver
solver (forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
r)
valToEUFArg Solver
solver (ValBitVec BV
bv) = Solver -> Expr -> IO Term
bvExprToEUFTerm Solver
solver (forall a. IsBV a => BV -> a
BV.fromBV BV
bv)

exprToEUFArg :: Solver -> Expr -> IO EUF.Term
exprToEUFArg :: Solver -> Expr -> IO Term
exprToEUFArg Solver
solver (EValue Value
v) = Solver -> Value -> IO Term
valToEUFArg Solver
solver Value
v
exprToEUFArg Solver
solver e :: Expr
e@(EAp FSym
f [Expr]
xs) = do
  Sort SSym
s [Sort]
_ <- Solver -> Expr -> IO Sort
exprSort Solver
solver Expr
e
  case SSym
s of
    SSym
SSymBool -> Solver -> Formula -> IO Term
formulaToEUFTerm Solver
solver forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> Expr -> IO Formula
exprToFormula Solver
solver Expr
e
    SSym
SSymReal -> Solver -> Expr Rational -> IO Term
lraExprToEUFTerm Solver
solver forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> Expr -> IO (Expr Rational)
exprToLRAExpr Solver
solver Expr
e
    SSymBitVec Int
_ -> Solver -> Expr -> IO Term
bvExprToEUFTerm Solver
solver forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> Expr -> IO Expr
exprToBVExpr Solver
solver Expr
e
    SSym
_ -> Solver -> FSym -> [Expr] -> IO Term
exprToEUFTerm Solver
solver FSym
f [Expr]
xs

abstractEUFAtom :: Solver -> (EUF.Term, EUF.Term) -> IO SAT.Lit
abstractEUFAtom :: Solver -> (Term, Term) -> IO Int
abstractEUFAtom Solver
solver (Term
t1,Term
t2) | Term
t1 forall a. Ord a => a -> a -> Bool
> Term
t2 = Solver -> (Term, Term) -> IO Int
abstractEUFAtom Solver
solver (Term
t2,Term
t1)
abstractEUFAtom Solver
solver (Term
t1,Term
t2) = do
  (Map (Term, Term) Int
tbl,IntMap (Term, Term)
defs) <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map (Term, Term) Int, IntMap (Term, Term))
smtEUFAtomDefs Solver
solver)
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Term
t1,Term
t2) Map (Term, Term) Int
tbl of
    Just Int
v -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
v
    Maybe Int
Nothing -> do
      Int
v <- forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar (Solver -> Solver
smtSAT Solver
solver)
      forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (Map (Term, Term) Int, IntMap (Term, Term))
smtEUFAtomDefs Solver
solver) (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Term
t1,Term
t2) Int
v Map (Term, Term) Int
tbl, forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
v (Term
t1,Term
t2) IntMap (Term, Term)
defs)
      forall (m :: * -> *) a. Monad m => a -> m a
return Int
v

formulaToEUFTerm :: Solver -> Tseitin.Formula -> IO EUF.Term
formulaToEUFTerm :: Solver -> Formula -> IO Term
formulaToEUFTerm Solver
solver Formula
formula = do
  Int
lit <- forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Int
Tseitin.encodeFormula (Solver -> Encoder IO
smtEnc Solver
solver) Formula
formula
  (Map Term Int
_, IntMap Term
boolToTerm) <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map Term Int, IntMap Term)
smtBoolTermDefs Solver
solver)
  case forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
lit IntMap Term
boolToTerm of
    Just Term
t -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
t
    Maybe Term
Nothing -> do
      Term
t <- Solver -> IO Term
EUF.newConst (Solver -> Solver
smtEUF Solver
solver)
      Solver -> Int -> Term -> IO ()
connectBoolTerm Solver
solver Int
lit Term
t
      forall (m :: * -> *) a. Monad m => a -> m a
return Term
t

formulaFromEUFTerm :: Solver -> EUF.Term -> IO Tseitin.Formula
formulaFromEUFTerm :: Solver -> Term -> IO Formula
formulaFromEUFTerm Solver
solver Term
t = do
  (Map Term Int
termToBool, IntMap Term
_) <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map Term Int, IntMap Term)
smtBoolTermDefs Solver
solver)
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Term
t Map Term Int
termToBool of
    Just Int
lit -> forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Formula
Atom Int
lit)
    Maybe Int
Nothing -> do
      Int
lit <- forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar (Solver -> Solver
smtSAT Solver
solver)
      Solver -> Int -> Term -> IO ()
connectBoolTerm Solver
solver Int
lit Term
t
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Formula
Atom Int
lit

connectBoolTerm :: Solver -> SAT.Lit -> EUF.Term -> IO ()
connectBoolTerm :: Solver -> Int -> Term -> IO ()
connectBoolTerm Solver
solver Int
lit Term
t = do
  Int
lit1 <- Solver -> (Term, Term) -> IO Int
abstractEUFAtom Solver
solver (Term
t, Solver -> Term
smtEUFTrue Solver
solver)
  Int
lit2 <- Solver -> (Term, Term) -> IO Int
abstractEUFAtom Solver
solver (Term
t, Solver -> Term
smtEUFFalse Solver
solver)
  forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause (Solver -> Solver
smtSAT Solver
solver) [-Int
lit, Int
lit1]  --  lit  ->  lit1
  forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause (Solver -> Solver
smtSAT Solver
solver) [-Int
lit1, Int
lit]  --  lit1 ->  lit
  forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause (Solver -> Solver
smtSAT Solver
solver) [Int
lit, Int
lit2]   -- -lit  ->  lit2
  forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause (Solver -> Solver
smtSAT Solver
solver) [-Int
lit2, -Int
lit] --  lit2 -> -lit
  forall a. IORef a -> (a -> a) -> IO ()
modifyIORef (Solver -> IORef (Map Term Int, IntMap Term)
smtBoolTermDefs Solver
solver) forall a b. (a -> b) -> a -> b
$ \(Map Term Int
termToBool, IntMap Term
boolToTerm) ->
    ( forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Term
t Int
lit Map Term Int
termToBool
    , forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
lit Term
t IntMap Term
boolToTerm
    )

-- -------------------------------------------------------------------

checkSAT :: Solver -> IO Bool
checkSAT :: Solver -> IO Bool
checkSAT Solver
solver = Solver -> [Expr] -> IO Bool
checkSATAssuming Solver
solver []

checkSATAssuming :: Solver -> [Expr] -> IO Bool
checkSATAssuming :: Solver -> [Expr] -> IO Bool
checkSATAssuming Solver
solver [Expr]
xs = do
  Int
l <- Solver -> IO Int
getContextLit Solver
solver
  Map String Int
named <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map String Int)
smtNamedAssertions Solver
solver)

  IORef (IntMap Expr)
ref <- forall a. a -> IO (IORef a)
newIORef forall a. IntMap a
IntMap.empty
  [Int]
ls <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Expr]
xs forall a b. (a -> b) -> a -> b
$ \Expr
x -> do
    Int
b <- forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Int
Tseitin.encodeFormula (Solver -> Encoder IO
smtEnc Solver
solver) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> Expr -> IO Formula
exprToFormula Solver
solver Expr
x
    forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef (IntMap Expr)
ref (forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
b Expr
x)
    forall (m :: * -> *) a. Monad m => a -> m a
return Int
b

  Bool
ret <- Solver -> [Int] -> IO Bool
SAT.solveWith (Solver -> Solver
smtSAT Solver
solver) (Int
l forall a. a -> [a] -> [a]
: [Int]
ls forall a. [a] -> [a] -> [a]
++ forall k a. Map k a -> [a]
Map.elems Map String Int
named)
  if Bool
ret then do
    forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef [Expr]
smtUnsatAssumptions Solver
solver) forall a. HasCallStack => a
undefined
    forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef [String]
smtUnsatCore Solver
solver) forall a. HasCallStack => a
undefined
  else do
    IntMap Expr
m1 <- forall a. IORef a -> IO a
readIORef IORef (IntMap Expr)
ref
    let m2 :: IntMap String
m2 = forall a. [(Int, a)] -> IntMap a
IntMap.fromList [(Int
lit, String
name) | (String
name, Int
lit) <- forall k a. Map k a -> [(k, a)]
Map.toList Map String Int
named]
    IntSet
failed <- Solver -> IO IntSet
SAT.getFailedAssumptions (Solver -> Solver
smtSAT Solver
solver)
    forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef [Expr]
smtUnsatAssumptions Solver
solver) forall a b. (a -> b) -> a -> b
$ forall a. IntMap a -> [a]
IntMap.elems forall a b. (a -> b) -> a -> b
$ forall a. IntMap a -> IntSet -> IntMap a
IntMap.restrictKeys IntMap Expr
m1 IntSet
failed
    forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef [String]
smtUnsatCore Solver
solver) forall a b. (a -> b) -> a -> b
$ forall a. IntMap a -> [a]
IntMap.elems forall a b. (a -> b) -> a -> b
$ forall a. IntMap a -> IntSet -> IntMap a
IntMap.restrictKeys IntMap String
m2 IntSet
failed
  forall (m :: * -> *) a. Monad m => a -> m a
return Bool
ret

getContextLit :: Solver -> IO SAT.Lit
getContextLit :: Solver -> IO Int
getContextLit Solver
solver = do
  Int
n <- forall (a :: * -> * -> *) e. GenericVec a e -> IO Int
Vec.getSize (Solver -> Vec AssertionLevel
smtAssertionStack Solver
solver)
  if Int
nforall a. Ord a => a -> a -> Bool
>Int
0 then do
    AssertionLevel
assertionLevel <- forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO e
Vec.peek (Solver -> Vec AssertionLevel
smtAssertionStack Solver
solver)
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ AssertionLevel -> Int
alSelector AssertionLevel
assertionLevel
  else
    forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeConj (Solver -> Encoder IO
smtEnc Solver
solver) [] -- true

push :: Solver -> IO ()
push :: Solver -> IO ()
push Solver
solver = do
  Int
l1 <- Solver -> IO Int
getContextLit Solver
solver
  Int
l2 <- forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar (Solver -> Solver
smtSAT Solver
solver)
  forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause (Solver -> Solver
smtSAT Solver
solver) [-Int
l2, Int
l1] -- l2 → l1
  Bool
globalDeclarations <- forall a. IORef a -> IO a
readIORef (Solver -> IORef Bool
smtGlobalDeclarationsRef Solver
solver)
  Map String Int
named <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map String Int)
smtNamedAssertions Solver
solver)
  Map FSym FDef
fdefs <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map FSym FDef)
smtFDefs Solver
solver)
  let newLevel :: AssertionLevel
newLevel =
        AssertionLevel
        { alSavedNamedAssertions :: Map String Int
alSavedNamedAssertions = Map String Int
named
        , alSavedFDefs :: Maybe (Map FSym FDef)
alSavedFDefs = if Bool
globalDeclarations then forall a. Maybe a
Nothing else forall a. a -> Maybe a
Just Map FSym FDef
fdefs
        , alSelector :: Int
alSelector = Int
l2
        }
  forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> Vec AssertionLevel
smtAssertionStack Solver
solver) AssertionLevel
newLevel

pop :: Solver -> IO ()
pop :: Solver -> IO ()
pop Solver
solver = do
  Int
n <- forall (a :: * -> * -> *) e. GenericVec a e -> IO Int
Vec.getSize (Solver -> Vec AssertionLevel
smtAssertionStack Solver
solver)
  if Int
nforall a. Eq a => a -> a -> Bool
==Int
0 then
    forall e a. Exception e => e -> IO a
E.throwIO forall a b. (a -> b) -> a -> b
$ String -> Exception
Error forall a b. (a -> b) -> a -> b
$ String
"cannot pop first assertion level"
  else do
    AssertionLevel
assertionLevel <- forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO e
Vec.unsafePop (Solver -> Vec AssertionLevel
smtAssertionStack Solver
solver)
    forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause (Solver -> Solver
smtSAT Solver
solver) [- AssertionLevel -> Int
alSelector AssertionLevel
assertionLevel]
    forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (Map String Int)
smtNamedAssertions Solver
solver) (AssertionLevel -> Map String Int
alSavedNamedAssertions AssertionLevel
assertionLevel)
    case AssertionLevel -> Maybe (Map FSym FDef)
alSavedFDefs AssertionLevel
assertionLevel of
      Maybe (Map FSym FDef)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Just Map FSym FDef
fdefs -> forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (Map FSym FDef)
smtFDefs Solver
solver) Map FSym FDef
fdefs
    forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- -------------------------------------------------------------------

data Model
  = Model
  { Model -> Map FSym FDef
mDefs      :: !(Map FSym FDef)
  , Model -> Model
mBoolModel :: !SAT.Model
  , Model -> Model
mLRAModel  :: !Simplex.Model
  , Model -> Model
mBVModel   :: !BV.Model
  , Model -> Model
mEUFModel  :: !EUF.Model
  , Model -> Int
mEUFTrue   :: !EUF.Entity
  , Model -> Int
mEUFFalse  :: !EUF.Entity
  , Model -> Model
mEntityToRational :: !(IntMap Rational)
  , Model -> Map Rational Int
mRationalToEntity :: !(Map Rational EUF.Entity)
  , Model -> IntMap BV
mEntityToBitVec :: !(IntMap BV.BV)
  , Model -> Map BV Int
mBitVecToEntity :: !(Map BV.BV EUF.Entity)
  }
  deriving (Int -> Model -> ShowS
[Model] -> ShowS
Model -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Model] -> ShowS
$cshowList :: [Model] -> ShowS
show :: Model -> String
$cshow :: Model -> String
showsPrec :: Int -> Model -> ShowS
$cshowsPrec :: Int -> Model -> ShowS
Show)

data Value
  = ValRational !Rational
  | ValBitVec !BV.BV
  | ValBool !Bool
  | ValUninterpreted !Int !Sort
  deriving (Value -> Value -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Value -> Value -> Bool
$c/= :: Value -> Value -> Bool
== :: Value -> Value -> Bool
$c== :: Value -> Value -> Bool
Eq, Eq Value
Value -> Value -> Bool
Value -> Value -> Ordering
Value -> Value -> Value
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 :: Value -> Value -> Value
$cmin :: Value -> Value -> Value
max :: Value -> Value -> Value
$cmax :: Value -> Value -> Value
>= :: Value -> Value -> Bool
$c>= :: Value -> Value -> Bool
> :: Value -> Value -> Bool
$c> :: Value -> Value -> Bool
<= :: Value -> Value -> Bool
$c<= :: Value -> Value -> Bool
< :: Value -> Value -> Bool
$c< :: Value -> Value -> Bool
compare :: Value -> Value -> Ordering
$ccompare :: Value -> Value -> Ordering
Ord, Int -> Value -> ShowS
[Value] -> ShowS
Value -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Value] -> ShowS
$cshowList :: [Value] -> ShowS
show :: Value -> String
$cshow :: Value -> String
showsPrec :: Int -> Value -> ShowS
$cshowsPrec :: Int -> Value -> ShowS
Show)

getModel :: Solver -> IO Model
getModel :: Solver -> IO Model
getModel Solver
solver = do
  Map FSym FDef
defs <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map FSym FDef)
smtFDefs Solver
solver)
  Model
boolModel <- Solver -> IO Model
SAT.getModel (Solver -> Solver
smtSAT Solver
solver)
  Model
lraModel <- forall a. IORef a -> IO a
readIORef (Solver -> IORef Model
smtLRAModel Solver
solver)
  Model
bvModel  <- forall a. IORef a -> IO a
readIORef (Solver -> IORef Model
smtBVModel Solver
solver)
  Model
eufModel <- forall a. IORef a -> IO a
readIORef (Solver -> IORef Model
smtEUFModel Solver
solver)

  (Map (Expr Rational) Int
_, IntMap (Expr Rational)
fsymToReal) <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map (Expr Rational) Int, IntMap (Expr Rational))
smtRealTermDefs Solver
solver)
  let xs :: [(Int, Rational)]
xs = [(Int
e, forall m e v. Eval m e v => m -> e -> v
LA.eval Model
lraModel Expr Rational
lraExpr) | (Int
fsym, Expr Rational
lraExpr) <- forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (Expr Rational)
fsymToReal, let e :: Int
e = Model -> Int -> [Int] -> Int
EUF.evalAp Model
eufModel Int
fsym [], Int
e forall a. Eq a => a -> a -> Bool
/= Model -> Int
EUF.mUnspecified Model
eufModel]

  (Map Expr Int
_, IntMap (IntMap Expr)
fsymToBV) <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map Expr Int, IntMap (IntMap Expr))
smtBVTermDefs Solver
solver)
  let ys :: [(Int, BV)]
ys = [(Int
e, Model -> Expr -> BV
BV.evalExpr Model
bvModel Expr
bvExpr) | (Int
w,IntMap Expr
m) <- forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (IntMap Expr)
fsymToBV, (Int
fsym, Expr
bvExpr) <- forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap Expr
m, let e :: Int
e = Model -> Int -> [Int] -> Int
EUF.evalAp Model
eufModel Int
fsym [], Int
e forall a. Eq a => a -> a -> Bool
/= Model -> Int
EUF.mUnspecified Model
eufModel]

  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    Model
    { mDefs :: Map FSym FDef
mDefs = Map FSym FDef
defs
    , mBoolModel :: Model
mBoolModel = Model
boolModel
    , mLRAModel :: Model
mLRAModel = Model
lraModel
    , mBVModel :: Model
mBVModel  = Model
bvModel
    , mEUFModel :: Model
mEUFModel = Model
eufModel
    , mEUFTrue :: Int
mEUFTrue  = Model -> Term -> Int
EUF.eval Model
eufModel (Solver -> Term
smtEUFTrue Solver
solver)
    , mEUFFalse :: Int
mEUFFalse = Model -> Term -> Int
EUF.eval Model
eufModel (Solver -> Term
smtEUFFalse Solver
solver)
    , mEntityToRational :: Model
mEntityToRational = forall a. [(Int, a)] -> IntMap a
IntMap.fromList [(Int, Rational)]
xs
    , mRationalToEntity :: Map Rational Int
mRationalToEntity = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Rational
r,Int
e) | (Int
e,Rational
r) <- [(Int, Rational)]
xs]

    , mEntityToBitVec :: IntMap BV
mEntityToBitVec = forall a. [(Int, a)] -> IntMap a
IntMap.fromList [(Int, BV)]
ys
    , mBitVecToEntity :: Map BV Int
mBitVecToEntity = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(BV
bv,Int
e) | (Int
e,BV
bv) <- [(Int, BV)]
ys]
    }

eval :: Model -> Expr -> Value
eval :: Model -> Expr -> Value
eval Model
m (EValue Value
v) = Value
v
eval Model
m (EAp FSym
"true" [])   = Bool -> Value
ValBool Bool
True
eval Model
m (EAp FSym
"false" [])  = Bool -> Value
ValBool Bool
False
eval Model
m (EAp FSym
"ite" [Expr
a,Expr
b,Expr
c]) = if Model -> Value -> Bool
valToBool Model
m (Model -> Expr -> Value
eval Model
m Expr
a) then Model -> Expr -> Value
eval Model
m Expr
b else Model -> Expr -> Value
eval Model
m Expr
c
eval Model
m (EAp FSym
"and" [Expr]
xs)    = Bool -> Value
ValBool forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Model -> Value -> Bool
valToBool Model
m forall b c a. (b -> c) -> (a -> b) -> a -> c
. Model -> Expr -> Value
eval Model
m) [Expr]
xs
eval Model
m (EAp FSym
"or" [Expr]
xs)     = Bool -> Value
ValBool forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *). Foldable t => t Bool -> Bool
or forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Model -> Value -> Bool
valToBool Model
m forall b c a. (b -> c) -> (a -> b) -> a -> c
. Model -> Expr -> Value
eval Model
m) [Expr]
xs
eval Model
m (EAp FSym
"xor" [Expr]
xs)    = Bool -> Value
ValBool forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a. Bits a => a -> a -> a
xor Bool
False forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Model -> Value -> Bool
valToBool Model
m forall b c a. (b -> c) -> (a -> b) -> a -> c
. Model -> Expr -> Value
eval Model
m) [Expr]
xs
eval Model
m (EAp FSym
"not" [Expr
x])   = Bool -> Value
ValBool forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Model -> Value -> Bool
valToBool Model
m forall a b. (a -> b) -> a -> b
$ Model -> Expr -> Value
eval Model
m Expr
x
eval Model
m (EAp FSym
"=>" [Expr
x,Expr
y])  = Bool -> Value
ValBool forall a b. (a -> b) -> a -> b
$ Model -> Value -> Bool
valToBool Model
m (Model -> Expr -> Value
eval Model
m Expr
x) forall a. Boolean a => a -> a -> a
.=>. Model -> Value -> Bool
valToBool Model
m (Model -> Expr -> Value
eval Model
m Expr
y)
eval Model
m (EAp FSym
"<=" [Expr
x,Expr
y])  = Bool -> Value
ValBool forall a b. (a -> b) -> a -> b
$ Model -> Value -> Rational
valToRational Model
m (Model -> Expr -> Value
eval Model
m Expr
x) forall a. Ord a => a -> a -> Bool
<= Model -> Value -> Rational
valToRational Model
m (Model -> Expr -> Value
eval Model
m Expr
y)
eval Model
m (EAp FSym
">=" [Expr
x,Expr
y])  = Bool -> Value
ValBool forall a b. (a -> b) -> a -> b
$ Model -> Value -> Rational
valToRational Model
m (Model -> Expr -> Value
eval Model
m Expr
x) forall a. Ord a => a -> a -> Bool
>= Model -> Value -> Rational
valToRational Model
m (Model -> Expr -> Value
eval Model
m Expr
y)
eval Model
m (EAp FSym
">" [Expr
x,Expr
y])   = Bool -> Value
ValBool forall a b. (a -> b) -> a -> b
$ Model -> Value -> Rational
valToRational Model
m (Model -> Expr -> Value
eval Model
m Expr
x) forall a. Ord a => a -> a -> Bool
>  Model -> Value -> Rational
valToRational Model
m (Model -> Expr -> Value
eval Model
m Expr
y)
eval Model
m (EAp FSym
"<" [Expr
x,Expr
y])   = Bool -> Value
ValBool forall a b. (a -> b) -> a -> b
$ Model -> Value -> Rational
valToRational Model
m (Model -> Expr -> Value
eval Model
m Expr
x) forall a. Ord a => a -> a -> Bool
<  Model -> Value -> Rational
valToRational Model
m (Model -> Expr -> Value
eval Model
m Expr
y)
eval Model
m (EAp FSym
"+" [Expr]
xs)      = Rational -> Value
ValRational forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Model -> Value -> Rational
valToRational Model
m forall b c a. (b -> c) -> (a -> b) -> a -> c
. Model -> Expr -> Value
eval Model
m) [Expr]
xs
eval Model
m (EAp FSym
"-" [Expr
x])     = Rational -> Value
ValRational forall a b. (a -> b) -> a -> b
$ forall a. Num a => a -> a
negate forall a b. (a -> b) -> a -> b
$ Model -> Value -> Rational
valToRational Model
m (Model -> Expr -> Value
eval Model
m Expr
x)
eval Model
m (EAp FSym
"-" [Expr
x,Expr
y])   = Rational -> Value
ValRational forall a b. (a -> b) -> a -> b
$ Model -> Value -> Rational
valToRational Model
m (Model -> Expr -> Value
eval Model
m Expr
x) forall a. Num a => a -> a -> a
- Model -> Value -> Rational
valToRational Model
m (Model -> Expr -> Value
eval Model
m Expr
y)
eval Model
m (EAp FSym
"*" [Expr]
xs)      = Rational -> Value
ValRational forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Model -> Value -> Rational
valToRational Model
m forall b c a. (b -> c) -> (a -> b) -> a -> c
. Model -> Expr -> Value
eval Model
m) [Expr]
xs
eval Model
m (EAp FSym
"/" [Expr
x,Expr
y])
  | Rational
y' forall a. Eq a => a -> a -> Bool
== Rational
0   = Model -> Expr -> Value
eval Model
m (FSym -> [Expr] -> Expr
EAp FSym
"_/0" [Expr
x])
  | Bool
otherwise = Rational -> Value
ValRational forall a b. (a -> b) -> a -> b
$ Model -> Value -> Rational
valToRational Model
m (Model -> Expr -> Value
eval Model
m Expr
x) forall a. Fractional a => a -> a -> a
/ Rational
y'
  where
    y' :: Rational
y' = Model -> Value -> Rational
valToRational Model
m (Model -> Expr -> Value
eval Model
m Expr
y)

eval Model
m (EAp FSym
"bvule" [Expr
x,Expr
y]) = Bool -> Value
ValBool forall a b. (a -> b) -> a -> b
$ forall a. BVComparison a => a -> a -> ComparisonResult a
BV.bvule (Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
x)) (Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
y))
eval Model
m (EAp FSym
"bvult" [Expr
x,Expr
y]) = Bool -> Value
ValBool forall a b. (a -> b) -> a -> b
$ forall a. BVComparison a => a -> a -> ComparisonResult a
BV.bvult (Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
x)) (Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
y))
eval Model
m (EAp FSym
"bvuge" [Expr
x,Expr
y]) = Bool -> Value
ValBool forall a b. (a -> b) -> a -> b
$ forall a. BVComparison a => a -> a -> ComparisonResult a
BV.bvuge (Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
x)) (Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
y))
eval Model
m (EAp FSym
"bvugt" [Expr
x,Expr
y]) = Bool -> Value
ValBool forall a b. (a -> b) -> a -> b
$ forall a. BVComparison a => a -> a -> ComparisonResult a
BV.bvugt (Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
x)) (Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
y))
eval Model
m (EAp FSym
"bvsle" [Expr
x,Expr
y]) = Bool -> Value
ValBool forall a b. (a -> b) -> a -> b
$ forall a. BVComparison a => a -> a -> ComparisonResult a
BV.bvsle (Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
x)) (Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
y))
eval Model
m (EAp FSym
"bvslt" [Expr
x,Expr
y]) = Bool -> Value
ValBool forall a b. (a -> b) -> a -> b
$ forall a. BVComparison a => a -> a -> ComparisonResult a
BV.bvslt (Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
x)) (Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
y))
eval Model
m (EAp FSym
"bvsge" [Expr
x,Expr
y]) = Bool -> Value
ValBool forall a b. (a -> b) -> a -> b
$ forall a. BVComparison a => a -> a -> ComparisonResult a
BV.bvsge (Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
x)) (Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
y))
eval Model
m (EAp FSym
"bvsgt" [Expr
x,Expr
y]) = Bool -> Value
ValBool forall a b. (a -> b) -> a -> b
$ forall a. BVComparison a => a -> a -> ComparisonResult a
BV.bvsgt (Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
x)) (Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
y))
eval Model
m (EAp FSym
"concat" [Expr
x,Expr
y]) =
  BV -> Value
ValBitVec forall a b. (a -> b) -> a -> b
$ Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
x) forall a. Semigroup a => a -> a -> a
<> Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
y)
eval Model
m (EAp (FSym InternedText
"extract" [IndexNumeral Integer
i, IndexNumeral Integer
j]) [Expr
x]) =
  BV -> Value
ValBitVec forall a b. (a -> b) -> a -> b
$ forall a. IsBV a => Int -> Int -> a -> a
BV.extract (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i) (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
j) (Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
x))
eval Model
m (EAp (FSym InternedText
"repeat" [IndexNumeral Integer
i]) [Expr
x]) =
  BV -> Value
ValBitVec forall a b. (a -> b) -> a -> b
$ forall m. Monoid m => Int -> m -> m
BV.repeat (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i) (Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
x))
eval Model
m (EAp (FSym InternedText
"zero_extend" [IndexNumeral Integer
i]) [Expr
x]) =
  BV -> Value
ValBitVec forall a b. (a -> b) -> a -> b
$ forall a. IsBV a => Int -> a -> a
BV.zeroExtend (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i) (Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
x))
eval Model
m (EAp (FSym InternedText
"sign_extend" [IndexNumeral Integer
i]) [Expr
x]) =
  BV -> Value
ValBitVec forall a b. (a -> b) -> a -> b
$ forall a. IsBV a => Int -> a -> a
BV.signExtend (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i) (Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
x))
eval Model
m (EAp (FSym InternedText
"rotate_left" [IndexNumeral Integer
i]) [Expr
x]) =
  BV -> Value
ValBitVec forall a b. (a -> b) -> a -> b
$ forall a. Bits a => a -> Int -> a
rotateL (Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
x)) (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i)
eval Model
m (EAp (FSym InternedText
"rotate_right" [IndexNumeral Integer
i]) [Expr
x]) =
  BV -> Value
ValBitVec forall a b. (a -> b) -> a -> b
$ forall a. Bits a => a -> Int -> a
rotateR (Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
x)) (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i)
eval Model
m (EAp (FSym InternedText
op1 []) [Expr
x])
  | Just Expr -> Expr
op1' <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup InternedText
op1 Map InternedText (Expr -> Expr)
table =
      let x' :: Expr
x' = BV -> Expr
BV.EConst forall a b. (a -> b) -> a -> b
$ Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
x)
      in BV -> Value
ValBitVec forall a b. (a -> b) -> a -> b
$ Model -> Expr -> BV
BV.evalExpr (Model -> Model
mBVModel Model
m) forall a b. (a -> b) -> a -> b
$ Expr -> Expr
op1' Expr
x'
  where
    table :: Map InternedText (Expr -> Expr)
table =
      forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
      [ (InternedText
"bvnot", forall a. IsBV a => a -> a
BV.bvnot)
      , (InternedText
"bvneg", forall a. IsBV a => a -> a
BV.bvneg)
      ]
eval Model
m (EAp (FSym InternedText
op2 []) [Expr
x,Expr
y])
  | Just Expr -> Expr -> Expr
op2' <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup InternedText
op2 Map InternedText (Expr -> Expr -> Expr)
table =
      let x' :: Expr
x' = BV -> Expr
BV.EConst forall a b. (a -> b) -> a -> b
$ Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
x)
          y' :: Expr
y' = BV -> Expr
BV.EConst forall a b. (a -> b) -> a -> b
$ Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
y)
      in BV -> Value
ValBitVec forall a b. (a -> b) -> a -> b
$ Model -> Expr -> BV
BV.evalExpr (Model -> Model
mBVModel Model
m) forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
op2' Expr
x' Expr
y'
  where
    table :: Map InternedText (Expr -> Expr -> Expr)
table = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$ [(InternedText
"bvcomp", forall a. IsBV a => a -> a -> a
BV.bvcomp)] forall a. [a] -> [a] -> [a]
++ forall s bv. (IsString s, IsBV bv) => [(s, bv -> bv -> bv)]
bvBinOpsSameSize

eval Model
m (EAp FSym
"=" [Expr
x,Expr
y])   = Bool -> Value
ValBool forall a b. (a -> b) -> a -> b
$
  case (Model -> Expr -> Value
eval Model
m Expr
x, Model -> Expr -> Value
eval Model
m Expr
y) of
    (Value
v1, Value
v2) -> Value
v1 forall a. Eq a => a -> a -> Bool
== Value
v2
eval Model
m expr :: Expr
expr@(EAp FSym
f [Expr]
xs) =
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup FSym
f (Model -> Map FSym FDef
mDefs Model
m) of
    Maybe FDef
Nothing -> forall a e. Exception e => e -> a
E.throw forall a b. (a -> b) -> a -> b
$ String -> Exception
Error forall a b. (a -> b) -> a -> b
$ String
"unknown function symbol: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show FSym
f
    Just (FBoolVar Int
v) -> Bool -> Value
ValBool forall a b. (a -> b) -> a -> b
$ forall m. IModel m => m -> Int -> Bool
SAT.evalLit (Model -> Model
mBoolModel Model
m) Int
v
    Just (FLRAVar Int
v) -> Rational -> Value
ValRational forall a b. (a -> b) -> a -> b
$ Model -> Model
mLRAModel Model
m forall a. IntMap a -> Int -> a
IntMap.! Int
v
    Just (FBVVar Var
v) -> BV -> Value
ValBitVec forall a b. (a -> b) -> a -> b
$ Model -> Expr -> BV
BV.evalExpr (Model -> Model
mBVModel Model
m) (Var -> Expr
BV.EVar Var
v)
    Just (FEUFFun ([Sort]
_, Sort SSym
s [Sort]
_) Int
sym) ->
      let e :: Int
e = Model -> Int -> [Int] -> Int
EUF.evalAp (Model -> Model
mEUFModel Model
m) Int
sym (forall a b. (a -> b) -> [a] -> [b]
map (Model -> Value -> Int
valToEntity Model
m forall b c a. (b -> c) -> (a -> b) -> a -> c
. Model -> Expr -> Value
eval Model
m) [Expr]
xs)
      in case SSym
s of
           SSymUninterpreted InternedText
_ Int
_ -> Int -> Sort -> Value
ValUninterpreted Int
e (Map FSym FDef -> Expr -> Sort
exprSort' (Model -> Map FSym FDef
mDefs Model
m) Expr
expr)
           SSym
SSymBool -> Bool -> Value
ValBool (Int
e forall a. Eq a => a -> a -> Bool
== Model -> Int
mEUFTrue Model
m)
           SSym
SSymReal ->
             case forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
e (Model -> Model
mEntityToRational Model
m) of
               Just Rational
r -> Rational -> Value
ValRational Rational
r
               Maybe Rational
Nothing -> Rational -> Value
ValRational (forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
1000000 forall a. Num a => a -> a -> a
+ Int
e))
           SSymBitVec Int
w ->
             case forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
e (Model -> IntMap BV
mEntityToBitVec Model
m) of
               Just BV
bv -> BV -> Value
ValBitVec BV
bv
               Maybe BV
Nothing -> BV -> Value
ValBitVec (forall a. IsBV a => Int -> Integer -> a
BV.nat2bv Int
w Integer
0)

valToBool :: Model -> Value -> Bool
valToBool :: Model -> Value -> Bool
valToBool Model
_ (ValBool Bool
b) = Bool
b
valToBool Model
_ Value
_ = forall a e. Exception e => e -> a
E.throw forall a b. (a -> b) -> a -> b
$ String -> Exception
Error String
"boolean value is expected"

valToRational :: Model -> Value -> Rational
valToRational :: Model -> Value -> Rational
valToRational Model
_ (ValRational Rational
r) = Rational
r
valToRational Model
_ Value
_ = forall a e. Exception e => e -> a
E.throw forall a b. (a -> b) -> a -> b
$ String -> Exception
Error String
"rational value is expected"

valToBitVec :: Model -> Value -> BV.BV
valToBitVec :: Model -> Value -> BV
valToBitVec Model
_ (ValBitVec BV
bv) = BV
bv
valToBitVec Model
_ Value
_ = forall a e. Exception e => e -> a
E.throw forall a b. (a -> b) -> a -> b
$ String -> Exception
Error String
"bitvector value is expected"

valToEntity :: Model -> Value -> EUF.Entity
valToEntity :: Model -> Value -> Int
valToEntity Model
_ (ValUninterpreted Int
e Sort
_) = Int
e
valToEntity Model
m (ValBool Bool
b)     = if Bool
b then Model -> Int
mEUFTrue Model
m else Model -> Int
mEUFFalse Model
m
valToEntity Model
m (ValRational Rational
r) =
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Rational
r (Model -> Map Rational Int
mRationalToEntity Model
m) of
    Just Int
e -> Int
e
    Maybe Int
Nothing -> Model -> Int
EUF.mUnspecified (Model -> Model
mEUFModel Model
m)
valToEntity Model
m (ValBitVec BV
bv) =
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup BV
bv (Model -> Map BV Int
mBitVecToEntity Model
m) of
    Just Int
e -> Int
e
    Maybe Int
Nothing -> Model -> Int
EUF.mUnspecified (Model -> Model
mEUFModel Model
m)

entityToValue :: Model -> EUF.Entity -> Sort -> Value
entityToValue :: Model -> Int -> Sort -> Value
entityToValue Model
m Int
e Sort
s =
  case Sort
s of
    Sort SSym
SSymBool [Sort]
_ -> Bool -> Value
ValBool (Int
e forall a. Eq a => a -> a -> Bool
== Model -> Int
mEUFTrue Model
m)
    Sort SSym
SSymReal [Sort]
_ ->
      case forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
e (Model -> Model
mEntityToRational Model
m) of
        Just Rational
r -> Rational -> Value
ValRational Rational
r
        Maybe Rational
Nothing -> Rational -> Value
ValRational (forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
1000000 forall a. Num a => a -> a -> a
+ Int
e))
    Sort (SSymBitVec Int
n) [Sort]
_ ->
      case forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
e (Model -> IntMap BV
mEntityToBitVec Model
m) of
        Just BV
bv -> BV -> Value
ValBitVec BV
bv
        Maybe BV
Nothing -> BV -> Value
ValBitVec (forall a. IsBV a => Int -> Integer -> a
BV.nat2bv Int
n Integer
0)
    Sort (SSymUninterpreted InternedText
_ Int
_) [Sort]
_ -> Int -> Sort -> Value
ValUninterpreted Int
e Sort
s

valSort :: Value -> Sort
valSort :: Value -> Sort
valSort (ValUninterpreted Int
_e Sort
s) = Sort
s
valSort (ValBool Bool
_b)     = Sort
sBool
valSort (ValRational Rational
_r) = Sort
sReal
valSort (ValBitVec BV
bv) = Int -> Sort
sBitVec (forall a. IsBV a => a -> Int
BV.width BV
bv)

data FunDef = FunDef [([Value], Value)] Value
  deriving (FunDef -> FunDef -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FunDef -> FunDef -> Bool
$c/= :: FunDef -> FunDef -> Bool
== :: FunDef -> FunDef -> Bool
$c== :: FunDef -> FunDef -> Bool
Eq, Int -> FunDef -> ShowS
[FunDef] -> ShowS
FunDef -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FunDef] -> ShowS
$cshowList :: [FunDef] -> ShowS
show :: FunDef -> String
$cshow :: FunDef -> String
showsPrec :: Int -> FunDef -> ShowS
$cshowsPrec :: Int -> FunDef -> ShowS
Show)

evalFSym :: Model -> FSym -> FunDef
evalFSym :: Model -> FSym -> FunDef
evalFSym Model
m FSym
f =
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup FSym
f (Model -> Map FSym FDef
mDefs Model
m) of
    Just (FEUFFun (argsSorts :: [Sort]
argsSorts@(Sort
_:[Sort]
_), Sort
resultSort) Int
sym) -> -- proper function symbol
      let tbl :: Map [Int] Int
tbl = Model -> IntMap (Map [Int] Int)
EUF.mFunctions (Model -> Model
mEUFModel Model
m) forall a. IntMap a -> Int -> a
IntMap.! Int
sym
          defaultVal :: Value
defaultVal =
            case Sort
resultSort of
              Sort SSym
SSymReal [Sort]
_ -> Rational -> Value
ValRational Rational
555555
              Sort SSym
SSymBool [Sort]
_ -> Bool -> Value
ValBool Bool
False
              Sort (SSymBitVec Int
w) [Sort]
_ -> BV -> Value
ValBitVec (forall a. IsBV a => Int -> Integer -> a
BV.nat2bv Int
w Integer
0)
              Sort (SSymUninterpreted InternedText
_s Int
_ar) [Sort]
_ -> Int -> Sort -> Value
ValUninterpreted (Model -> Int
EUF.mUnspecified (Model -> Model
mEUFModel Model
m)) Sort
resultSort
      in [([Value], Value)] -> Value -> FunDef
FunDef [ (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Model -> Int -> Sort -> Value
entityToValue Model
m) [Int]
args [Sort]
argsSorts, Model -> Int -> Sort -> Value
entityToValue Model
m Int
result Sort
resultSort)
                | ([Int]
args, Int
result) <- forall k a. Map k a -> [(k, a)]
Map.toList Map [Int] Int
tbl ]
                Value
defaultVal
    Just FDef
_ -> [([Value], Value)] -> Value -> FunDef
FunDef [] forall a b. (a -> b) -> a -> b
$ Model -> Expr -> Value
eval Model
m (FSym -> [Expr] -> Expr
EAp FSym
f []) -- constant symbol
    Maybe FDef
Nothing -> forall a e. Exception e => e -> a
E.throw forall a b. (a -> b) -> a -> b
$ String -> Exception
Error forall a b. (a -> b) -> a -> b
$ String
"unknown function symbol: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show FSym
f

-- | Constraints that cannot represented as function definitions.
--
-- For example, zero-division result values cannot be specified by
-- function definition, because division is interpreted function.
modelGetAssertions :: Model -> [Expr]
modelGetAssertions :: Model -> [Expr]
modelGetAssertions Model
m =
  [ FSym -> [Expr] -> Expr
EAp FSym
"="
      [ FSym -> [Expr] -> Expr
EAp FSym
"/"
        [ Value -> Expr
EValue (Model -> Int -> Sort -> Value
entityToValue Model
m Int
arg Sort
sReal)
        , Value -> Expr
EValue (Rational -> Value
ValRational Rational
0)
        ]
      , Value -> Expr
EValue (Model -> Int -> Sort -> Value
entityToValue Model
m Int
result Sort
sReal)
      ]
  | let FEUFFun FunType
_ Int
sym = Model -> Map FSym FDef
mDefs Model
m forall k a. Ord k => Map k a -> k -> a
Map.! FSym
"_/0"
  , ([Int
arg], Int
result) <- forall k a. Map k a -> [(k, a)]
Map.toList forall a b. (a -> b) -> a -> b
$ Model -> IntMap (Map [Int] Int)
EUF.mFunctions (Model -> Model
mEUFModel Model
m) forall a. IntMap a -> Int -> a
IntMap.! Int
sym
  ]
  forall a. [a] -> [a] -> [a]
++
  [ FSym -> [Expr] -> Expr
EAp FSym
"="
      [ FSym -> [Expr] -> Expr
EAp FSym
"bvudiv"
        [ Value -> Expr
EValue (BV -> Value
ValBitVec BV
s)
        , Value -> Expr
EValue (BV -> Value
ValBitVec (forall a. IsBV a => Int -> Integer -> a
BV.nat2bv (forall a. IsBV a => a -> Int
BV.width BV
s) Integer
0))
        ]
      , Value -> Expr
EValue (BV -> Value
ValBitVec BV
t)
      ]
  | (BV
s,BV
t) <- forall k a. Map k a -> [(k, a)]
Map.toList Map BV BV
bvDivTable
  ]
  forall a. [a] -> [a] -> [a]
++
  [ FSym -> [Expr] -> Expr
EAp FSym
"="
      [ FSym -> [Expr] -> Expr
EAp FSym
"bvurem"
        [ Value -> Expr
EValue (BV -> Value
ValBitVec BV
s)
        , Value -> Expr
EValue (BV -> Value
ValBitVec (forall a. IsBV a => Int -> Integer -> a
BV.nat2bv (forall a. IsBV a => a -> Int
BV.width BV
s) Integer
0))
        ]
      , Value -> Expr
EValue (BV -> Value
ValBitVec BV
t)
      ]
  | (BV
s,BV
t) <- forall k a. Map k a -> [(k, a)]
Map.toList Map BV BV
bvRemTable
  ]
  where
    (Vector BV
_, Map BV BV
bvDivTable, Map BV BV
bvRemTable) = Model -> Model
mBVModel Model
m

-- -------------------------------------------------------------------

getUnsatAssumptions :: Solver -> IO [Expr]
getUnsatAssumptions :: Solver -> IO [Expr]
getUnsatAssumptions Solver
solver = do
  forall a. IORef a -> IO a
readIORef (Solver -> IORef [Expr]
smtUnsatAssumptions Solver
solver)

getUnsatCore :: Solver -> IO [String]
getUnsatCore :: Solver -> IO [String]
getUnsatCore Solver
solver = do
  forall a. IORef a -> IO a
readIORef (Solver -> IORef [String]
smtUnsatCore Solver
solver)

-- -------------------------------------------------------------------

pairs :: [a] -> [(a,a)]
pairs :: forall a. [a] -> [(a, a)]
pairs [] = []
pairs (a
x:[a]
xs) = [(a
x,a
y) | a
y <- [a]
xs] forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [(a, a)]
pairs [a]
xs