{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE CPP #-}
{-# 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.BoolExpr
import ToySolver.Data.OrdRel
import qualified ToySolver.Data.LA as LA
import qualified ToySolver.Internal.Data.Vec as Vec
import qualified ToySolver.SAT as SAT
import ToySolver.SAT.TheorySolver
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
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
(Int -> Index -> ShowS)
-> (Index -> String) -> ([Index] -> ShowS) -> Show Index
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
(Index -> Index -> Bool) -> (Index -> Index -> Bool) -> Eq Index
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
Eq Index
-> (Index -> Index -> Ordering)
-> (Index -> Index -> Bool)
-> (Index -> Index -> Bool)
-> (Index -> Index -> Bool)
-> (Index -> Index -> Bool)
-> (Index -> Index -> Index)
-> (Index -> Index -> Index)
-> Ord 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
$cp1Ord :: Eq Index
Ord)

data FSym
  = FSym !InternedText [Index]
  deriving (Int -> FSym -> ShowS
[FSym] -> ShowS
FSym -> String
(Int -> FSym -> ShowS)
-> (FSym -> String) -> ([FSym] -> ShowS) -> Show FSym
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
(FSym -> FSym -> Bool) -> (FSym -> FSym -> Bool) -> Eq FSym
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
Eq FSym
-> (FSym -> FSym -> Ordering)
-> (FSym -> FSym -> Bool)
-> (FSym -> FSym -> Bool)
-> (FSym -> FSym -> Bool)
-> (FSym -> FSym -> Bool)
-> (FSym -> FSym -> FSym)
-> (FSym -> FSym -> FSym)
-> Ord 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
$cp1Ord :: Eq FSym
Ord)

instance IsString FSym where
  fromString :: String -> FSym
fromString String
s = InternedText -> [Index] -> FSym
FSym (String -> InternedText
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
(Int -> SSym -> ShowS)
-> (SSym -> String) -> ([SSym] -> ShowS) -> Show SSym
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
(SSym -> SSym -> Bool) -> (SSym -> SSym -> Bool) -> Eq SSym
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
Eq SSym
-> (SSym -> SSym -> Ordering)
-> (SSym -> SSym -> Bool)
-> (SSym -> SSym -> Bool)
-> (SSym -> SSym -> Bool)
-> (SSym -> SSym -> Bool)
-> (SSym -> SSym -> SSym)
-> (SSym -> SSym -> SSym)
-> Ord 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
$cp1Ord :: Eq SSym
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
(Int -> Sort -> ShowS)
-> (Sort -> String) -> ([Sort] -> ShowS) -> Show Sort
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
(Sort -> Sort -> Bool) -> (Sort -> Sort -> Bool) -> Eq Sort
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
Eq Sort
-> (Sort -> Sort -> Ordering)
-> (Sort -> Sort -> Bool)
-> (Sort -> Sort -> Bool)
-> (Sort -> Sort -> Bool)
-> (Sort -> Sort -> Bool)
-> (Sort -> Sort -> Sort)
-> (Sort -> Sort -> Sort)
-> Ord 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
$cp1Ord :: Eq Sort
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
(Int -> Expr -> ShowS)
-> (Expr -> String) -> ([Expr] -> ShowS) -> Show Expr
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
(Expr -> Expr -> Bool) -> (Expr -> Expr -> Bool) -> Eq Expr
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
Eq Expr
-> (Expr -> Expr -> Ordering)
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Expr)
-> (Expr -> Expr -> Expr)
-> Ord 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
$cp1Ord :: Eq Expr
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 = String -> Expr
forall a. HasCallStack => String -> a
error String
"Num{ToySolver.SMT.Expr}.abs is not implemented"
  signum :: Expr -> Expr
signum Expr
x = String -> Expr
forall a. HasCallStack => String -> a
error String
"Num{ToySolver.SMT.Expr}.signum is not implemented"
  fromInteger :: Integer -> Expr
fromInteger Integer
x = Value -> Expr
EValue (Value -> Expr) -> Value -> Expr
forall a b. (a -> b) -> a -> b
$ Rational -> Value
ValRational (Rational -> Value) -> Rational -> Value
forall a b. (a -> b) -> a -> b
$ Integer -> Rational
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 (Value -> Expr) -> Value -> Expr
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 = Expr -> Expr
forall a. Complement a => a -> a
notB (Expr
a Expr -> Expr -> Expr
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
(Int -> FDef -> ShowS)
-> (FDef -> String) -> ([FDef] -> ShowS) -> Show FDef
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
(Int -> Exception -> ShowS)
-> (Exception -> String)
-> ([Exception] -> ShowS)
-> Show Exception
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
(TheorySolverID -> TheorySolverID -> Bool)
-> (TheorySolverID -> TheorySolverID -> Bool) -> Eq TheorySolverID
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
Eq TheorySolverID
-> (TheorySolverID -> TheorySolverID -> Ordering)
-> (TheorySolverID -> TheorySolverID -> Bool)
-> (TheorySolverID -> TheorySolverID -> Bool)
-> (TheorySolverID -> TheorySolverID -> Bool)
-> (TheorySolverID -> TheorySolverID -> Bool)
-> (TheorySolverID -> TheorySolverID -> TheorySolverID)
-> (TheorySolverID -> TheorySolverID -> TheorySolverID)
-> Ord 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
$cp1Ord :: Eq TheorySolverID
Ord, Int -> TheorySolverID
TheorySolverID -> Int
TheorySolverID -> [TheorySolverID]
TheorySolverID -> TheorySolverID
TheorySolverID -> TheorySolverID -> [TheorySolverID]
TheorySolverID
-> TheorySolverID -> TheorySolverID -> [TheorySolverID]
(TheorySolverID -> TheorySolverID)
-> (TheorySolverID -> TheorySolverID)
-> (Int -> TheorySolverID)
-> (TheorySolverID -> Int)
-> (TheorySolverID -> [TheorySolverID])
-> (TheorySolverID -> TheorySolverID -> [TheorySolverID])
-> (TheorySolverID -> TheorySolverID -> [TheorySolverID])
-> (TheorySolverID
    -> TheorySolverID -> TheorySolverID -> [TheorySolverID])
-> Enum 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
TheorySolverID -> TheorySolverID -> Bounded 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 <- Solver -> IO (Encoder IO)
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 <- IO (GenericSolver (Delta Rational))
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
m (GenericSolverM m v)
Simplex.newSolver
  Solver
bv <- IO Solver
BV.newSolver

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

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

  IORef Bool
globalDeclarationsRef <- Bool -> IO (IORef Bool)
forall a. a -> IO (IORef a)
newIORef Bool
False
  IORef (Map FSym FDef)
fdefs <- Map FSym FDef -> IO (IORef (Map FSym FDef))
forall a. a -> IO (IORef a)
newIORef (Map FSym FDef -> IO (IORef (Map FSym FDef)))
-> Map FSym FDef -> IO (IORef (Map FSym FDef))
forall a b. (a -> b) -> a -> b
$ FSym -> FDef -> Map FSym FDef
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 <- TheorySolverID -> IO (IORef TheorySolverID)
forall a. a -> IO (IORef a)
newIORef TheorySolverID
forall a. HasCallStack => a
undefined

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

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

            (Map BVAtomNormalized Int
_, IntMap BVAtomNormalized
defsBV) <- IO (Map BVAtomNormalized Int, IntMap BVAtomNormalized)
-> ExceptT
     Bool IO (Map BVAtomNormalized Int, IntMap BVAtomNormalized)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Map BVAtomNormalized Int, IntMap BVAtomNormalized)
 -> ExceptT
      Bool IO (Map BVAtomNormalized Int, IntMap BVAtomNormalized))
-> IO (Map BVAtomNormalized Int, IntMap BVAtomNormalized)
-> ExceptT
     Bool IO (Map BVAtomNormalized Int, IntMap BVAtomNormalized)
forall a b. (a -> b) -> a -> b
$ IORef (Map BVAtomNormalized Int, IntMap BVAtomNormalized)
-> IO (Map BVAtomNormalized Int, IntMap BVAtomNormalized)
forall a. IORef a -> IO a
readIORef IORef (Map BVAtomNormalized Int, IntMap BVAtomNormalized)
bvAtomDefs
            case Int -> IntMap BVAtomNormalized -> Maybe BVAtomNormalized
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (Int -> Int
SAT.litVar Int
l) IntMap BVAtomNormalized
defsBV of
              Maybe BVAtomNormalized
Nothing -> () -> ExceptT Bool IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
              Just BVAtomNormalized
atom -> do
                IO () -> ExceptT Bool IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> ExceptT Bool IO ()) -> IO () -> ExceptT Bool IO ()
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)) (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
l)
                Bool -> ExceptT Bool IO ()
forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE Bool
True

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

        , thCheck :: (Int -> IO Bool) -> IO Bool
thCheck = \Int -> IO Bool
callback -> (Either () () -> Bool) -> IO (Either () ()) -> IO Bool
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Either () () -> Bool
forall a b. Either a b -> Bool
isRight (IO (Either () ()) -> IO Bool) -> IO (Either () ()) -> IO Bool
forall a b. (a -> b) -> a -> b
$ ExceptT () IO () -> IO (Either () ())
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT () IO () -> IO (Either () ()))
-> ExceptT () IO () -> IO (Either () ())
forall a b. (a -> b) -> a -> b
$ do
            do Bool
b <- IO Bool -> ExceptT () IO Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO Bool -> ExceptT () IO Bool) -> IO Bool -> ExceptT () IO Bool
forall a b. (a -> b) -> a -> b
$ GenericSolver (Delta Rational) -> IO Bool
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Bool
Simplex.check GenericSolver (Delta Rational)
lra
               Bool -> ExceptT () IO () -> ExceptT () IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
b (ExceptT () IO () -> ExceptT () IO ())
-> ExceptT () IO () -> ExceptT () IO ()
forall a b. (a -> b) -> a -> b
$ do
                 IO () -> ExceptT () IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> ExceptT () IO ()) -> IO () -> ExceptT () IO ()
forall a b. (a -> b) -> a -> b
$ IORef TheorySolverID -> TheorySolverID -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef TheorySolverID
conflictTheory TheorySolverID
TheorySolverSimplex
                 () -> ExceptT () IO ()
forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE ()
            do Bool
b <- IO Bool -> ExceptT () IO Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO Bool -> ExceptT () IO Bool) -> IO Bool -> ExceptT () IO Bool
forall a b. (a -> b) -> a -> b
$ Solver -> IO Bool
EUF.check Solver
euf
               Bool -> ExceptT () IO () -> ExceptT () IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
b (ExceptT () IO () -> ExceptT () IO ())
-> ExceptT () IO () -> ExceptT () IO ()
forall a b. (a -> b) -> a -> b
$ do
                 IO () -> ExceptT () IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> ExceptT () IO ()) -> IO () -> ExceptT () IO ()
forall a b. (a -> b) -> a -> b
$ IORef TheorySolverID -> TheorySolverID -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef TheorySolverID
conflictTheory TheorySolverID
TheorySolverEUF
                 () -> ExceptT () IO ()
forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE ()
               (Map (Term, Term) Int
_, IntMap (Term, Term)
defsEUF) <- IO (Map (Term, Term) Int, IntMap (Term, Term))
-> ExceptT () IO (Map (Term, Term) Int, IntMap (Term, Term))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Map (Term, Term) Int, IntMap (Term, Term))
 -> ExceptT () IO (Map (Term, Term) Int, IntMap (Term, Term)))
-> IO (Map (Term, Term) Int, IntMap (Term, Term))
-> ExceptT () IO (Map (Term, Term) Int, IntMap (Term, Term))
forall a b. (a -> b) -> a -> b
$ IORef (Map (Term, Term) Int, IntMap (Term, Term))
-> IO (Map (Term, Term) Int, IntMap (Term, Term))
forall a. IORef a -> IO a
readIORef IORef (Map (Term, Term) Int, IntMap (Term, Term))
eufAtomDefs
               [(Int, (Term, Term))]
-> ((Int, (Term, Term)) -> ExceptT () IO ()) -> ExceptT () IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntMap (Term, Term) -> [(Int, (Term, Term))]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (Term, Term)
defsEUF) (((Int, (Term, Term)) -> ExceptT () IO ()) -> ExceptT () IO ())
-> ((Int, (Term, Term)) -> ExceptT () IO ()) -> ExceptT () IO ()
forall a b. (a -> b) -> a -> b
$ \(Int
v, (t1, t2)) -> do
                  Bool
b2 <- IO Bool -> ExceptT () IO Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO Bool -> ExceptT () IO Bool) -> IO Bool -> ExceptT () IO Bool
forall a b. (a -> b) -> a -> b
$ Solver -> Term -> Term -> IO Bool
EUF.areEqual Solver
euf Term
t1 Term
t2
                  Bool -> ExceptT () IO () -> ExceptT () IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
b2 (ExceptT () IO () -> ExceptT () IO ())
-> ExceptT () IO () -> ExceptT () IO ()
forall a b. (a -> b) -> a -> b
$ do
                    Bool
b3 <- IO Bool -> ExceptT () IO Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO Bool -> ExceptT () IO Bool) -> IO Bool -> ExceptT () IO Bool
forall a b. (a -> b) -> a -> b
$ Int -> IO Bool
callback Int
v
                    Bool -> ExceptT () IO () -> ExceptT () IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
b3 (ExceptT () IO () -> ExceptT () IO ())
-> ExceptT () IO () -> ExceptT () IO ()
forall a b. (a -> b) -> a -> b
$ () -> ExceptT () IO ()
forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE ()
            do Bool
b <- IO Bool -> ExceptT () IO Bool
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO Bool -> ExceptT () IO Bool) -> IO Bool -> ExceptT () IO Bool
forall a b. (a -> b) -> a -> b
$ Solver -> IO Bool
BV.check Solver
bv
               Bool -> ExceptT () IO () -> ExceptT () IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
b (ExceptT () IO () -> ExceptT () IO ())
-> ExceptT () IO () -> ExceptT () IO ()
forall a b. (a -> b) -> a -> b
$ do
                 IO () -> ExceptT () IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> ExceptT () IO ()) -> IO () -> ExceptT () IO ()
forall a b. (a -> b) -> a -> b
$ IORef TheorySolverID -> TheorySolverID -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef TheorySolverID
conflictTheory TheorySolverID
TheorySolverBV
                 () -> ExceptT () IO ()
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 <- IORef TheorySolverID -> IO TheorySolverID
forall a. IORef a -> IO a
readIORef IORef TheorySolverID
conflictTheory
                case TheorySolverID
t of
                  TheorySolverID
TheorySolverSimplex -> (IntSet -> [Int]) -> IO IntSet -> IO [Int]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM IntSet -> [Int]
IntSet.toList (IO IntSet -> IO [Int]) -> IO IntSet -> IO [Int]
forall a b. (a -> b) -> a -> b
$ GenericSolver (Delta Rational) -> IO IntSet
forall (m :: * -> *) v.
PrimMonad m =>
GenericSolverM m v -> m IntSet
Simplex.explain GenericSolver (Delta Rational)
lra
                  TheorySolverID
TheorySolverBV -> (IntSet -> [Int]) -> IO IntSet -> IO [Int]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM IntSet -> [Int]
IntSet.toList (IO IntSet -> IO [Int]) -> IO IntSet -> IO [Int]
forall a b. (a -> b) -> a -> b
$ Solver -> IO IntSet
BV.explain Solver
bv
                  TheorySolverID
TheorySolverEUF -> (IntSet -> [Int]) -> IO IntSet -> IO [Int]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM IntSet -> [Int]
IntSet.toList (IO IntSet -> IO [Int]) -> IO IntSet -> IO [Int]
forall a b. (a -> b) -> a -> b
$ Solver -> Maybe (Term, Term) -> IO IntSet
EUF.explain Solver
euf Maybe (Term, Term)
forall a. Maybe a
Nothing
              Just Int
v -> do
                (Map (Term, Term) Int
_, IntMap (Term, Term)
defsEUF) <- IORef (Map (Term, Term) Int, IntMap (Term, Term))
-> IO (Map (Term, Term) Int, IntMap (Term, Term))
forall a. IORef a -> IO a
readIORef IORef (Map (Term, Term) Int, IntMap (Term, Term))
eufAtomDefs
                case Int -> IntMap (Term, Term) -> Maybe (Term, Term)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
v IntMap (Term, Term)
defsEUF of
                  Maybe (Term, Term)
Nothing -> String -> IO [Int]
forall a. HasCallStack => String -> a
error String
"should not happen"
                  Just (t1,t2) -> (IntSet -> [Int]) -> IO IntSet -> IO [Int]
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM IntSet -> [Int]
IntSet.toList (IO IntSet -> IO [Int]) -> IO IntSet -> IO [Int]
forall a b. (a -> b) -> a -> b
$ Solver -> Maybe (Term, Term) -> IO IntSet
EUF.explain Solver
euf ((Term, Term) -> Maybe (Term, Term)
forall a. a -> Maybe a
Just (Term
t1,Term
t2))

        , thPushBacktrackPoint :: IO ()
thPushBacktrackPoint = do
            GenericSolver (Delta Rational) -> IO ()
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
            GenericSolver (Delta Rational) -> IO ()
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
            IORef Model -> Model -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Model
eufModelRef (Model -> IO ()) -> IO Model -> IO ()
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.
            IORef Model -> Model -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Model
lraModelRef (Model -> IO ()) -> IO Model -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< GenericSolver (Delta Rational) -> IO Model
forall v (m :: * -> *).
(SolverValue v, PrimMonad m) =>
GenericSolverM m v -> m Model
Simplex.getModel GenericSolver (Delta Rational)
lra
            IORef Model -> Model -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Model
bvModelRef (Model -> IO ()) -> IO Model -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> IO Model
BV.getModel Solver
bv
            () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        }
  Solver -> TheorySolver -> IO ()
SAT.setTheory Solver
sat TheorySolver
tsolver

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

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

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

  Solver -> IO Solver
forall (m :: * -> *) a. Monad m => a -> m a
return (Solver -> IO Solver) -> Solver -> IO Solver
forall a b. (a -> b) -> a -> b
$
    Solver :: Solver
-> Encoder IO
-> Solver
-> GenericSolver (Delta Rational)
-> Solver
-> IORef (Map (Term, Term) Int, IntMap (Term, Term))
-> IORef
     (Map (Int, Rational) (Int, Int, Int), IntMap (Atom Rational))
-> IORef (Map BVAtomNormalized Int, IntMap BVAtomNormalized)
-> IORef (Map Term Int, IntMap Term)
-> IORef (Map (Expr Rational) Int, IntMap (Expr Rational))
-> IORef (Map Expr Int, IntMap (IntMap Expr))
-> Term
-> Term
-> IORef Model
-> IORef Model
-> IORef Model
-> IORef Bool
-> IORef (Map FSym FDef)
-> IORef (Map String Int)
-> Vec AssertionLevel
-> IORef [Expr]
-> IORef [String]
-> Solver
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 = SSym -> IO SSym
forall (m :: * -> *) a. Monad m => a -> m a
return (InternedText -> Int -> SSym
SSymUninterpreted (String -> InternedText
forall a. IsString a => String -> a
fromString String
name) Int
arity)

declareSort :: VASortFun a => Solver -> String -> Int -> IO a
declareSort :: 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 = ([Sort] -> Sort) -> a
forall a. VASortFun a => ([Sort] -> Sort) -> a
withSortVArgs (SSym -> [Sort] -> Sort
Sort SSym
ssym)
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (a -> Int
forall a. VASortFun a => a -> Int
arityVASortFun a
f Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
arity) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    Exception -> IO ()
forall e a. Exception e => e -> IO a
E.throwIO (Exception -> IO ()) -> Exception -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Exception
Error String
"ToySolver.SMT.declareSort: argument number error"
  a -> IO a
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 = ([Sort] -> Sort) -> a
forall a. VASortFun a => ([Sort] -> Sort) -> a
withSortVArgs (\[Sort]
xs -> [Sort] -> Sort
k (Sort
x Sort -> [Sort] -> [Sort]
forall a. a -> [a] -> [a]
: [Sort]
xs))
  arityVASortFun :: (Sort -> a) -> Int
arityVASortFun Sort -> a
f = a -> Int
forall a. VASortFun a => a -> Int
arityVASortFun (Sort -> a
f Sort
forall a. HasCallStack => a
undefined) Int -> Int -> Int
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 (Uninterned InternedText -> InternedText
forall t. Interned t => Uninterned t -> t
intern (String -> Text
T.pack String
f')) []
  Map FSym FDef
fdefs <- IORef (Map FSym FDef) -> IO (Map FSym FDef)
forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map FSym FDef)
smtFDefs Solver
solver)
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FSym
f FSym -> Map FSym FDef -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map FSym FDef
fdefs) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    Exception -> IO ()
forall e a. Exception e => e -> IO a
E.throwIO (Exception -> IO ()) -> Exception -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Exception
Error (String -> Exception) -> String -> Exception
forall a b. (a -> b) -> a -> b
$ String
"function symbol " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
f' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is already used"
  FDef
fdef <-
    case ([Sort]
xs, Sort
y) of
      ([], Sort SSym
SSymBool [Sort]
_) -> do
        Int
v <- Solver -> IO Int
forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar (Solver -> Solver
smtSAT Solver
solver)
        FDef -> IO FDef
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> FDef
FBoolVar Int
v)
      ([], Sort SSym
SSymReal [Sort]
_) -> do
        Int
v <- GenericSolver (Delta Rational) -> IO Int
forall (m :: * -> *) v.
(PrimMonad m, SolverValue v) =>
GenericSolverM m v -> m Int
Simplex.newVar (Solver -> GenericSolver (Delta Rational)
smtLRA Solver
solver)
        FDef -> IO FDef
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
        FDef -> IO FDef
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)
        FDef -> IO FDef
forall (m :: * -> *) a. Monad m => a -> m a
return (FunType -> Int -> FDef
FEUFFun ([Sort]
xs,Sort
y) Int
v)
  IORef (Map FSym FDef) -> Map FSym FDef -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (Map FSym FDef)
smtFDefs Solver
solver) (Map FSym FDef -> IO ()) -> Map FSym FDef -> IO ()
forall a b. (a -> b) -> a -> b
$ FSym -> FDef -> Map FSym FDef -> Map FSym FDef
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert FSym
f FDef
fdef Map FSym FDef
fdefs
  FSym -> IO FSym
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 = ([Expr] -> Expr) -> a
forall a. VAFun a => ([Expr] -> Expr) -> a
withVArgs (\[Expr]
xs -> [Expr] -> Expr
k (Expr
x Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
: [Expr]
xs))
  arityVAFun :: (Expr -> a) -> Int
arityVAFun Expr -> a
f = a -> Int
forall a. VAFun a => a -> Int
arityVAFun (Expr -> a
f Expr
forall a. HasCallStack => a
undefined) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1

declareFun :: VAFun a => Solver -> String -> [Sort] -> Sort -> IO a
declareFun :: 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 = ([Expr] -> Expr) -> a
forall a. VAFun a => ([Expr] -> Expr) -> a
withVArgs (FSym -> [Expr] -> Expr
EAp FSym
fsym)
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (a -> Int
forall a. VAFun a => a -> Int
arityVAFun a
f Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Sort] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Sort]
ps) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    Exception -> IO ()
forall e a. Exception e => e -> IO a
E.throwIO (Exception -> IO ()) -> Exception -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Exception
Error String
"ToySolver.SMT.declareFun: argument number error"
  a -> IO a
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 = Solver -> String -> [Sort] -> Sort -> IO Expr
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 <- Vec AssertionLevel -> IO Int
forall (a :: * -> * -> *) e. GenericVec a e -> IO Int
Vec.getSize (Solver -> Vec AssertionLevel
smtAssertionStack Solver
solver)
  if Int
nInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>Int
0 then do
    AssertionLevel
assertionLevel <- Vec AssertionLevel -> IO AssertionLevel
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO e
Vec.peek (Solver -> Vec AssertionLevel
smtAssertionStack Solver
solver)
    Encoder IO -> Formula -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
smtEnc Solver
solver) (Formula -> IO ()) -> Formula -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> Formula
forall a. a -> BoolExpr a
Atom (AssertionLevel -> Int
alSelector AssertionLevel
assertionLevel) Formula -> Formula -> Formula
forall a. Boolean a => a -> a -> a
.=>. Formula
formula
  else
    Encoder IO -> Formula -> IO ()
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 <- Encoder IO -> Formula -> IO Int
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Int
Tseitin.encodeFormula (Solver -> Encoder IO
smtEnc Solver
solver) (Formula -> IO Int) -> IO Formula -> IO Int
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> Expr -> IO Formula
exprToFormula Solver
solver Expr
e
  IORef (Map String Int)
-> (Map String Int -> Map String Int) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef (Solver -> IORef (Map String Int)
smtNamedAssertions Solver
solver) (String -> Int -> Map String Int -> Map String Int
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 = IORef Bool -> IO Bool
forall a. IORef a -> IO a
readIORef (Solver -> IORef Bool
smtGlobalDeclarationsRef Solver
solver)

setGlobalDeclarations :: Solver -> Bool -> IO ()
setGlobalDeclarations :: Solver -> Bool -> IO ()
setGlobalDeclarations Solver
solver = IORef Bool -> Bool -> IO ()
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 <- IORef (Map FSym FDef) -> IO (Map FSym FDef)
forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map FSym FDef)
smtFDefs Solver
solver)
  Sort -> IO Sort
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> IO Sort) -> Sort -> IO Sort
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 FSym -> Set FSym -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` [FSym] -> Set FSym
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 FSym -> Set FSym -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` [FSym] -> Set FSym
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 FSym -> Set FSym -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` [FSym] -> Set FSym
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 (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer
i Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
j Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1))
  | FSym
f FSym -> FSym -> Bool
forall a. Eq a => a -> a -> Bool
== FSym
"concat" =
      case (Map FSym FDef -> Expr -> Sort
exprSort' Map FSym FDef
fdefs ([Expr]
xs [Expr] -> Int -> Expr
forall a. [a] -> Int -> a
!! Int
0), Map FSym FDef -> Expr -> Sort
exprSort' Map FSym FDef
fdefs ([Expr]
xs [Expr] -> Int -> Expr
forall a. [a] -> Int -> a
!! Int
1)) of
        (Sort (SSymBitVec Int
m) [], Sort (SSymBitVec Int
n) []) -> Int -> Sort
sBitVec (Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
n)
        (Sort, 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 [Expr] -> Int -> Expr
forall a. [a] -> Int -> a
!! Int
0) of
        Sort (SSymBitVec Int
m) [] -> Int -> Sort
sBitVec (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
* Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i)
        Sort
_ -> Sort
forall a. HasCallStack => a
undefined
  | FSym InternedText
name [IndexNumeral Integer
i] <- FSym
f, InternedText
name InternedText -> InternedText -> Bool
forall a. Eq a => a -> a -> Bool
== InternedText
"zero_extend" Bool -> Bool -> Bool
|| InternedText
name InternedText -> InternedText -> Bool
forall a. Eq a => a -> a -> Bool
== InternedText
"sign_extend" =
      case Map FSym FDef -> Expr -> Sort
exprSort' Map FSym FDef
fdefs ([Expr]
xs [Expr] -> Int -> Expr
forall a. [a] -> Int -> a
!! Int
0) of
        Sort (SSymBitVec Int
m) [] -> Int -> Sort
sBitVec (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i)
        Sort
_ -> Sort
forall a. HasCallStack => a
undefined
  | FSym InternedText
name [IndexNumeral Integer
i] <- FSym
f, InternedText
name InternedText -> InternedText -> Bool
forall a. Eq a => a -> a -> Bool
== InternedText
"rotate_left" Bool -> Bool -> Bool
|| InternedText
name InternedText -> InternedText -> Bool
forall a. Eq a => a -> a -> Bool
== InternedText
"rotate_right" =
      Map FSym FDef -> Expr -> Sort
exprSort' Map FSym FDef
fdefs ([Expr]
xs [Expr] -> Int -> Expr
forall a. [a] -> Int -> a
!! Int
0)
  | FSym
f FSym -> FSym -> Bool
forall a. Eq a => a -> a -> Bool
== FSym
"bvnot" Bool -> Bool -> Bool
|| FSym
f FSym -> FSym -> Bool
forall a. Eq a => a -> a -> Bool
== FSym
"bvneg" = Map FSym FDef -> Expr -> Sort
exprSort' Map FSym FDef
fdefs ([Expr]
xs [Expr] -> Int -> Expr
forall a. [a] -> Int -> a
!! Int
0)
  | FSym
f FSym -> FSym -> Bool
forall a. Eq a => a -> a -> Bool
== FSym
"bvcomp" = Int -> Sort
sBitVec Int
1
  | FSym
f FSym -> Set FSym -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` [FSym] -> Set FSym
forall a. Ord a => [a] -> Set a
Set.fromList [FSym
name | (FSym
name, BV -> BV -> BV
_op::BV.BV->BV.BV->BV.BV) <- [(FSym, 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 [Expr] -> Int -> Expr
forall a. [a] -> Int -> a
!! Int
0)
  | FSym
f FSym -> FSym -> Bool
forall a. Eq a => a -> a -> Bool
== FSym
"ite" = Map FSym FDef -> Expr -> Sort
exprSort' Map FSym FDef
fdefs ([Expr]
xs [Expr] -> Int -> Expr
forall a. [a] -> Int -> a
!! Int
1)
  | Bool
otherwise =
      case FSym -> Map FSym FDef -> Maybe FDef
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup FSym
f Map FSym FDef
fdefs of
        Maybe FDef
Nothing -> String -> Sort
forall a. HasCallStack => String -> a
error (String -> Sort) -> String -> Sort
forall a b. (a -> b) -> a -> b
$ FSym -> String
forall a. Show a => a -> String
show FSym
f String -> ShowS
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" [])  = Formula -> IO Formula
forall (m :: * -> *) a. Monad m => a -> m a
return Formula
forall a. MonotoneBoolean a => a
true
exprToFormula Solver
solver (EAp FSym
"false" []) = Formula -> IO Formula
forall (m :: * -> *) a. Monad m => a -> m a
return Formula
forall a. MonotoneBoolean a => a
false
exprToFormula Solver
solver (EAp FSym
"and" [Expr]
xs) =
  ([Formula] -> Formula) -> IO [Formula] -> IO Formula
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [Formula] -> Formula
forall a. MonotoneBoolean a => [a] -> a
andB (IO [Formula] -> IO Formula) -> IO [Formula] -> IO Formula
forall a b. (a -> b) -> a -> b
$ (Expr -> IO Formula) -> [Expr] -> IO [Formula]
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) =
  ([Formula] -> Formula) -> IO [Formula] -> IO Formula
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [Formula] -> Formula
forall a. MonotoneBoolean a => [a] -> a
orB (IO [Formula] -> IO Formula) -> IO [Formula] -> IO Formula
forall a b. (a -> b) -> a -> b
$ (Expr -> IO Formula) -> [Expr] -> IO [Formula]
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 <- (Expr -> IO Formula) -> [Expr] -> IO [Formula]
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
  Formula -> IO Formula
forall (m :: * -> *) a. Monad m => a -> m a
return (Formula -> IO Formula) -> Formula -> IO Formula
forall a b. (a -> b) -> a -> b
$ (Formula -> Formula -> Formula) -> Formula -> [Formula] -> Formula
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Formula
a Formula
b -> Formula -> Formula
forall a. Complement a => a -> a
notB (Formula
a Formula -> Formula -> Formula
forall a. Boolean a => a -> a -> a
.<=>. Formula
b)) Formula
forall a. MonotoneBoolean a => a
false [Formula]
ys
exprToFormula Solver
solver (EAp FSym
"not" [Expr
x]) =
  (Formula -> Formula) -> IO Formula -> IO Formula
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Formula -> Formula
forall a. Complement a => a -> a
notB (IO Formula -> IO Formula) -> IO Formula -> IO Formula
forall a b. (a -> b) -> a -> b
$ Solver -> Expr -> IO Formula
exprToFormula Solver
solver Expr
x
exprToFormula Solver
solver (EAp FSym
"not" [Expr]
_) = IO Formula
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
  Formula -> IO Formula
forall (m :: * -> *) a. Monad m => a -> m a
return (Formula -> IO Formula) -> Formula -> IO Formula
forall a b. (a -> b) -> a -> b
$ Formula
b1 Formula -> Formula -> Formula
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
  Formula -> IO Formula
forall (m :: * -> *) a. Monad m => a -> m a
return (Formula -> IO Formula) -> Formula -> IO Formula
forall a b. (a -> b) -> a -> b
$ Formula -> Formula -> Formula -> Formula
forall b a. IfThenElse b a => b -> a -> a -> a
ite Formula
b1 Formula
b2 Formula
b3
exprToFormula Solver
solver (EAp FSym
"=" []) = Formula -> IO Formula
forall (m :: * -> *) a. Monad m => a -> m a
return Formula
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" []) = Formula -> IO Formula
forall (m :: * -> *) a. Monad m => a -> m a
return Formula
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 -> (Formula -> Formula) -> IO Formula -> IO Formula
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Formula -> Formula
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
        (Int -> Formula) -> IO Int -> IO Formula
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Int -> Formula
forall a. a -> BoolExpr a
Atom (IO Int -> IO Formula) -> IO Int -> IO Formula
forall a b. (a -> b) -> a -> b
$ Solver -> Atom Rational -> IO Int
abstractLRAAtom Solver
solver (Expr Rational
e1' Expr Rational -> Expr Rational -> Atom Rational
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
          (Int -> Formula) -> IO Int -> IO Formula
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Int -> Formula
forall a. a -> BoolExpr a
Atom (IO Int -> IO Formula) -> IO Int -> IO Formula
forall a b. (a -> b) -> a -> b
$ Solver -> Atom Rational -> IO Int
abstractLRAAtom Solver
solver (Expr Rational
e1' Expr Rational -> Expr Rational -> Atom Rational
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
        (Int -> Formula) -> IO Int -> IO Formula
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Int -> Formula
forall a. a -> BoolExpr a
Atom (IO Int -> IO Formula) -> IO Int -> IO Formula
forall a b. (a -> b) -> a -> b
$ Solver -> Atom Rational -> IO Int
abstractLRAAtom Solver
solver (Expr Rational
e1' Expr Rational -> Expr Rational -> Atom Rational
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
        (Int -> Formula) -> IO Int -> IO Formula
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Int -> Formula
forall a. a -> BoolExpr a
Atom (IO Int -> IO Formula) -> IO Int -> IO Formula
forall a b. (a -> b) -> a -> b
$ Solver -> Atom Rational -> IO Int
abstractLRAAtom Solver
solver (Expr Rational
e1' Expr Rational -> Expr Rational -> Atom Rational
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 <- IORef (Map FSym FDef) -> IO (Map FSym FDef)
forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map FSym FDef)
smtFDefs Solver
solver)
  case FSym -> Map FSym FDef -> Maybe FDef
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup FSym
f Map FSym FDef
fdefs of
    Just (FBoolVar Int
v) -> Formula -> IO Formula
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Formula
forall a. a -> BoolExpr a
Atom Int
v)
    Just FDef
_ -> Exception -> IO Formula
forall e a. Exception e => e -> IO a
E.throwIO (Exception -> IO Formula) -> Exception -> IO Formula
forall a b. (a -> b) -> a -> b
$ String -> Exception
Error String
"non Bool constant appears in a boolean context"
    Maybe FDef
Nothing -> Exception -> IO Formula
forall e a. Exception e => e -> IO a
E.throwIO (Exception -> IO Formula) -> Exception -> IO Formula
forall a b. (a -> b) -> a -> b
$ String -> Exception
Error (String -> Exception) -> String -> Exception
forall a b. (a -> b) -> a -> b
$ String
"unknown function symbol: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ FSym -> String
forall a. Show a => a -> String
show FSym
f
exprToFormula Solver
solver (EAp FSym
op [Expr
e1,Expr
e2]) | Just Expr -> Expr -> Atom
f <- FSym
-> Map FSym (Expr -> Expr -> Atom) -> Maybe (Expr -> Expr -> Atom)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup FSym
op Map FSym (Expr -> Expr -> Atom)
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
  (Int -> Formula) -> IO Int -> IO Formula
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Int -> Formula
forall a. a -> BoolExpr a
Atom (IO Int -> IO Formula) -> IO Int -> IO Formula
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 = [(FSym, Expr -> Expr -> ComparisonResult Expr)]
-> Map FSym (Expr -> Expr -> ComparisonResult Expr)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
      [ (FSym
"bvule", Expr -> Expr -> ComparisonResult Expr
forall a. BVComparison a => a -> a -> ComparisonResult a
BV.bvule)
      , (FSym
"bvult", Expr -> Expr -> ComparisonResult Expr
forall a. BVComparison a => a -> a -> ComparisonResult a
BV.bvult)
      , (FSym
"bvuge", Expr -> Expr -> ComparisonResult Expr
forall a. BVComparison a => a -> a -> ComparisonResult a
BV.bvuge)
      , (FSym
"bvugt", Expr -> Expr -> ComparisonResult Expr
forall a. BVComparison a => a -> a -> ComparisonResult a
BV.bvugt)
      , (FSym
"bvsle", Expr -> Expr -> ComparisonResult Expr
forall a. BVComparison a => a -> a -> ComparisonResult a
BV.bvsle)
      , (FSym
"bvslt", Expr -> Expr -> ComparisonResult Expr
forall a. BVComparison a => a -> a -> ComparisonResult a
BV.bvslt)
      , (FSym
"bvsge", Expr -> Expr -> ComparisonResult Expr
forall a. BVComparison a => a -> a -> ComparisonResult a
BV.bvsge)
      , (FSym
"bvsgt", Expr -> Expr -> ComparisonResult Expr
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
_ [] = Formula -> IO Formula
forall (m :: * -> *) a. Monad m => a -> m a
return Formula
forall a. MonotoneBoolean a => a
true
chain Solver
solver Expr -> Expr -> IO Formula
p [Expr]
xs = ([Formula] -> Formula) -> IO [Formula] -> IO Formula
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [Formula] -> Formula
forall a. MonotoneBoolean a => [a] -> a
andB (IO [Formula] -> IO Formula) -> IO [Formula] -> IO Formula
forall a b. (a -> b) -> a -> b
$ ((Expr, Expr) -> IO Formula) -> [(Expr, Expr)] -> IO [Formula]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Expr -> Expr -> IO Formula) -> (Expr, Expr) -> IO Formula
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Expr -> Expr -> IO Formula
p) ([Expr] -> [Expr] -> [(Expr, Expr)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Expr]
xs ([Expr] -> [Expr]
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
_ [] = Formula -> IO Formula
forall (m :: * -> *) a. Monad m => a -> m a
return Formula
forall a. MonotoneBoolean a => a
true
pairwise Solver
solver Expr -> Expr -> IO Formula
p [Expr]
xs = ([Formula] -> Formula) -> IO [Formula] -> IO Formula
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [Formula] -> Formula
forall a. MonotoneBoolean a => [a] -> a
andB (IO [Formula] -> IO Formula) -> IO [Formula] -> IO Formula
forall a b. (a -> b) -> a -> b
$ ((Expr, Expr) -> IO Formula) -> [(Expr, Expr)] -> IO [Formula]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Expr -> Expr -> IO Formula) -> (Expr, Expr) -> IO Formula
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Expr -> Expr -> IO Formula
p) ([Expr] -> [(Expr, Expr)]
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
      Formula -> IO Formula
forall (m :: * -> *) a. Monad m => a -> m a
return (Formula -> IO Formula) -> Formula -> IO Formula
forall a b. (a -> b) -> a -> b
$ Formula
b1 Formula -> Formula -> Formula
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
      (Int -> Formula) -> IO Int -> IO Formula
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Int -> Formula
forall a. a -> BoolExpr a
Atom (IO Int -> IO Formula) -> IO Int -> IO Formula
forall a b. (a -> b) -> a -> b
$ Solver -> Atom Rational -> IO Int
abstractLRAAtom Solver
solver (Expr Rational
e1' Expr Rational -> Expr Rational -> Atom Rational
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
      (Int -> Formula) -> IO Int -> IO Formula
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Int -> Formula
forall a. a -> BoolExpr a
Atom (IO Int -> IO Formula) -> IO Int -> IO Formula
forall a b. (a -> b) -> a -> b
$ Solver -> Atom -> IO Int
abstractBVAtom Solver
solver (Expr
e1' Expr -> Expr -> Atom
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
      (Int -> Formula) -> IO Int -> IO Formula
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Int -> Formula
forall a. a -> BoolExpr a
Atom (IO Int -> IO Formula) -> IO Int -> IO Formula
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)) = Expr Rational -> IO (Expr Rational)
forall (m :: * -> *) a. Monad m => a -> m a
return (Rational -> Expr Rational
forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
r)
exprToLRAExpr Solver
solver (EAp FSym
"-" []) = Exception -> IO (Expr Rational)
forall e a. Exception e => e -> IO a
E.throwIO (Exception -> IO (Expr Rational))
-> Exception -> IO (Expr Rational)
forall a b. (a -> b) -> a -> b
$ String -> Exception
Error String
"ToySolver.SMT: nullary '-' function"
exprToLRAExpr Solver
solver (EAp FSym
"-" [Expr
x]) = (Expr Rational -> Expr Rational)
-> IO (Expr Rational) -> IO (Expr Rational)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Expr Rational -> Expr Rational
forall v. AdditiveGroup v => v -> v
negateV (IO (Expr Rational) -> IO (Expr Rational))
-> IO (Expr Rational) -> IO (Expr Rational)
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' <- (Expr -> IO (Expr Rational)) -> [Expr] -> IO [Expr Rational]
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
  Expr Rational -> IO (Expr Rational)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr Rational -> IO (Expr Rational))
-> Expr Rational -> IO (Expr Rational)
forall a b. (a -> b) -> a -> b
$ (Expr Rational -> Expr Rational -> Expr Rational)
-> Expr Rational -> [Expr Rational] -> Expr Rational
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Expr Rational -> Expr Rational -> Expr Rational
forall v. AdditiveGroup v => v -> v -> v
(^-^) Expr Rational
x' [Expr Rational]
xs'
exprToLRAExpr Solver
solver (EAp FSym
"+" [Expr]
xs) = ([Expr Rational] -> Expr Rational)
-> IO [Expr Rational] -> IO (Expr Rational)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [Expr Rational] -> Expr Rational
forall (f :: * -> *) v. (Foldable f, AdditiveGroup v) => f v -> v
sumV (IO [Expr Rational] -> IO (Expr Rational))
-> IO [Expr Rational] -> IO (Expr Rational)
forall a b. (a -> b) -> a -> b
$ (Expr -> IO (Expr Rational)) -> [Expr] -> IO [Expr Rational]
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) = ([Expr Rational] -> Expr Rational)
-> IO [Expr Rational] -> IO (Expr Rational)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM ((Expr Rational -> Expr Rational -> Expr Rational)
-> Expr Rational -> [Expr Rational] -> Expr Rational
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Expr Rational -> Expr Rational -> Expr Rational
forall r. (Num r, Eq r) => Expr r -> Expr r -> Expr r
mult (Rational -> Expr Rational
forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
1)) (IO [Expr Rational] -> IO (Expr Rational))
-> IO [Expr Rational] -> IO (Expr Rational)
forall a b. (a -> b) -> a -> b
$ (Expr -> IO (Expr Rational)) -> [Expr] -> IO [Expr Rational]
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 <- Expr r -> Maybe r
forall r. Num r => Expr r -> Maybe r
LA.asConst Expr r
e1 = r
Scalar (Expr r)
c Scalar (Expr r) -> Expr r -> Expr r
forall v. VectorSpace v => Scalar v -> v -> v
*^ Expr r
e2
      | Just r
c <- Expr r -> Maybe r
forall r. Num r => Expr r -> Maybe r
LA.asConst Expr r
e2 = r
Scalar (Expr r)
c Scalar (Expr r) -> Expr r -> Expr r
forall v. VectorSpace v => Scalar v -> v -> v
*^ Expr r
e1
      | Bool
otherwise = Exception -> Expr r
forall a e. Exception e => e -> a
E.throw (Exception -> Expr r) -> Exception -> Expr r
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 Expr Rational -> Maybe Rational
forall r. Num r => Expr r -> Maybe r
LA.asConst Expr Rational
y' of
    Maybe Rational
Nothing -> Exception -> IO (Expr Rational)
forall e a. Exception e => e -> IO a
E.throwIO (Exception -> IO (Expr Rational))
-> Exception -> IO (Expr Rational)
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 (Term -> IO (Expr Rational)) -> IO Term -> IO (Expr Rational)
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
      Expr Rational -> IO (Expr Rational)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr Rational -> IO (Expr Rational))
-> Expr Rational -> IO (Expr Rational)
forall a b. (a -> b) -> a -> b
$ (Rational
1Rational -> Rational -> Rational
forall a. Fractional a => a -> a -> a
/Rational
c) Scalar (Expr Rational) -> Expr Rational -> Expr Rational
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 <- (Int -> Expr Rational) -> IO Int -> IO (Expr Rational)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Int -> Expr Rational
forall r. Num r => Int -> Expr r
LA.var (IO Int -> IO (Expr Rational)) -> IO Int -> IO (Expr Rational)
forall a b. (a -> b) -> a -> b
$ GenericSolver (Delta Rational) -> IO Int
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 Expr Rational -> Expr Rational -> Atom Rational
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 Expr Rational -> Expr Rational -> Atom Rational
forall e r. IsEqRel e r => e -> e -> r
.==. Expr Rational
e')
  Encoder IO -> Formula -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
smtEnc Solver
solver) (Formula -> IO ()) -> Formula -> IO ()
forall a b. (a -> b) -> a -> b
$ Formula -> Formula -> Formula -> Formula
forall b a. IfThenElse b a => b -> a -> a -> a
ite Formula
c' (Int -> Formula
forall a. a -> BoolExpr a
Atom Int
c1) (Int -> Formula
forall a. a -> BoolExpr a
Atom Int
c2)
  Expr Rational -> IO (Expr Rational)
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 (Term -> IO (Expr Rational)) -> IO Term -> IO (Expr Rational)
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) <- GenericSolver (Delta Rational)
-> Atom Rational -> IO (Int, RelOp, Rational)
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) <- IORef (Map (Int, Rational) (Int, Int, Int), IntMap (Atom Rational))
-> IO (Map (Int, Rational) (Int, Int, Int), IntMap (Atom Rational))
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 (Int, Rational)
-> Map (Int, Rational) (Int, Int, Int) -> Maybe (Int, Int, Int)
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) -> (Int, Int, Int) -> IO (Int, Int, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
vLt, Int
vEq, Int
vGt)
      Maybe (Int, Int, Int)
Nothing -> do
        Int
vLt <- Solver -> IO Int
forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar (Solver -> Solver
smtSAT Solver
solver)
        Int
vEq <- Solver -> IO Int
forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar (Solver -> Solver
smtSAT Solver
solver)
        Int
vGt <- Solver -> IO Int
forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar (Solver -> Solver
smtSAT Solver
solver)
        Solver -> [Int] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause (Solver -> Solver
smtSAT Solver
solver) [Int
vLt,Int
vEq,Int
vGt]
        Solver -> [Int] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause (Solver -> Solver
smtSAT Solver
solver) [-Int
vLt, -Int
vEq]
        Solver -> [Int] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause (Solver -> Solver
smtSAT Solver
solver) [-Int
vLt, -Int
vGt]
        Solver -> [Int] -> IO ()
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 = [(Int, Atom Rational)] -> IntMap (Atom Rational)
forall a. [(Int, a)] -> IntMap a
IntMap.fromList
                 [ (Int
vEq,  Int -> Expr Rational
forall r. Num r => Int -> Expr r
LA.var Int
v Expr Rational -> Expr Rational -> Atom Rational
forall e r. IsEqRel e r => e -> e -> r
.==. Rational -> Expr Rational
forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
rhs)
                 , (Int
vLt,  Int -> Expr Rational
forall r. Num r => Int -> Expr r
LA.var Int
v Expr Rational -> Expr Rational -> Atom Rational
forall e r. IsOrdRel e r => e -> e -> r
.<.  Rational -> Expr Rational
forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
rhs)
                 , (Int
vGt,  Int -> Expr Rational
forall r. Num r => Int -> Expr r
LA.var Int
v Expr Rational -> Expr Rational -> Atom Rational
forall e r. IsOrdRel e r => e -> e -> r
.>.  Rational -> Expr Rational
forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
rhs)
                 , (-Int
vLt, Int -> Expr Rational
forall r. Num r => Int -> Expr r
LA.var Int
v Expr Rational -> Expr Rational -> Atom Rational
forall e r. IsOrdRel e r => e -> e -> r
.>=. Rational -> Expr Rational
forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
rhs)
                 , (-Int
vGt, Int -> Expr Rational
forall r. Num r => Int -> Expr r
LA.var Int
v Expr Rational -> Expr Rational -> Atom Rational
forall e r. IsOrdRel e r => e -> e -> r
.<=. Rational -> Expr Rational
forall r. (Num r, Eq r) => r -> Expr r
LA.constant Rational
rhs)
                 ]
        IORef (Map (Int, Rational) (Int, Int, Int), IntMap (Atom Rational))
-> (Map (Int, Rational) (Int, Int, Int), IntMap (Atom Rational))
-> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver
-> IORef
     (Map (Int, Rational) (Int, Int, Int), IntMap (Atom Rational))
smtLRAAtomDefs Solver
solver) ((Int, Rational)
-> (Int, Int, Int)
-> Map (Int, Rational) (Int, Int, Int)
-> Map (Int, Rational) (Int, Int, Int)
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, IntMap (Atom Rational)
-> IntMap (Atom Rational) -> IntMap (Atom Rational)
forall a. IntMap a -> IntMap a -> IntMap a
IntMap.union IntMap (Atom Rational)
xs IntMap (Atom Rational)
defs)
        (Int, Int, Int) -> IO (Int, Int, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
vLt, Int
vEq, Int
vGt)
  case RelOp
op of
    RelOp
Lt  -> Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
vLt
    RelOp
Gt  -> Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
vGt
    RelOp
Eql -> Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
vEq
    RelOp
Le  -> Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return (-Int
vGt)
    RelOp
Ge  -> Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return (-Int
vLt)
    RelOp
NEq -> Int -> IO Int
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) <- IORef (Map (Expr Rational) Int, IntMap (Expr Rational))
-> IO (Map (Expr Rational) Int, IntMap (Expr Rational))
forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map (Expr Rational) Int, IntMap (Expr Rational))
smtRealTermDefs Solver
solver)
  case Expr Rational -> Map (Expr Rational) Int -> Maybe Int
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 -> Term -> IO Term
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)
      [(Int, Expr Rational)] -> ((Int, Expr Rational) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntMap (Expr Rational) -> [(Int, Expr Rational)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (Expr Rational)
fsymToReal) (((Int, Expr Rational) -> IO ()) -> IO ())
-> ((Int, Expr Rational) -> IO ()) -> IO ()
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 Expr Rational -> Expr Rational -> Atom Rational
forall e r. IsEqRel e r => e -> e -> r
.==. Expr Rational
d_lra)
        Encoder IO -> Formula -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
smtEnc Solver
solver) (Int -> Formula
forall a. a -> BoolExpr a
Atom Int
b1 Formula -> Formula -> Formula
forall a. Boolean a => a -> a -> a
.<=>. Int -> Formula
forall a. a -> BoolExpr a
Atom Int
b2)
      IORef (Map (Expr Rational) Int, IntMap (Expr Rational))
-> (Map (Expr Rational) Int, IntMap (Expr Rational)) -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (Map (Expr Rational) Int, IntMap (Expr Rational))
smtRealTermDefs Solver
solver) ((Map (Expr Rational) Int, IntMap (Expr Rational)) -> IO ())
-> (Map (Expr Rational) Int, IntMap (Expr Rational)) -> IO ()
forall a b. (a -> b) -> a -> b
$
        ( Expr Rational
-> Int -> Map (Expr Rational) Int -> Map (Expr Rational) Int
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
        , Int
-> Expr Rational
-> IntMap (Expr Rational)
-> IntMap (Expr Rational)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
c Expr Rational
e IntMap (Expr Rational)
fsymToReal
        )
      Term -> IO Term
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) <- IORef (Map (Expr Rational) Int, IntMap (Expr Rational))
-> IO (Map (Expr Rational) Int, IntMap (Expr Rational))
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 Int -> IntMap (Expr Rational) -> Maybe (Expr Rational)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
c IntMap (Expr Rational)
fsymToReal of
    Just Expr Rational
e -> Expr Rational -> IO (Expr Rational)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr Rational
e
    Maybe (Expr Rational)
Nothing -> do
      Int
v <- GenericSolver (Delta Rational) -> IO Int
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 = Int -> Expr Rational
forall r. Num r => Int -> Expr r
LA.var Int
v
      [(Int, Expr Rational)] -> ((Int, Expr Rational) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntMap (Expr Rational) -> [(Int, Expr Rational)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (Expr Rational)
fsymToReal) (((Int, Expr Rational) -> IO ()) -> IO ())
-> ((Int, Expr Rational) -> IO ()) -> IO ()
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 Expr Rational -> Expr Rational -> Atom Rational
forall e r. IsEqRel e r => e -> e -> r
.==. Expr Rational
d_lra)
        Encoder IO -> Formula -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
smtEnc Solver
solver) (Int -> Formula
forall a. a -> BoolExpr a
Atom Int
b1 Formula -> Formula -> Formula
forall a. Boolean a => a -> a -> a
.<=>. Int -> Formula
forall a. a -> BoolExpr a
Atom Int
b2)
      IORef (Map (Expr Rational) Int, IntMap (Expr Rational))
-> (Map (Expr Rational) Int, IntMap (Expr Rational)) -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (Map (Expr Rational) Int, IntMap (Expr Rational))
smtRealTermDefs Solver
solver) ((Map (Expr Rational) Int, IntMap (Expr Rational)) -> IO ())
-> (Map (Expr Rational) Int, IntMap (Expr Rational)) -> IO ()
forall a b. (a -> b) -> a -> b
$
        ( Expr Rational
-> Int -> Map (Expr Rational) Int -> Map (Expr Rational) Int
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
        , Int
-> Expr Rational
-> IntMap (Expr Rational)
-> IntMap (Expr Rational)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
c Expr Rational
e IntMap (Expr Rational)
fsymToReal
        )
      Expr Rational -> IO (Expr Rational)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr Rational
e

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

bvBinOpsSameSize :: (IsString s, BV.IsBV bv) => [(s, bv -> bv -> bv)]
bvBinOpsSameSize :: [(s, bv -> bv -> bv)]
bvBinOpsSameSize =
  [ (s
"bvand", bv -> bv -> bv
forall a. IsBV a => a -> a -> a
BV.bvand)
  , (s
"bvor", bv -> bv -> bv
forall a. IsBV a => a -> a -> a
BV.bvor)
  , (s
"bvxor", bv -> bv -> bv
forall a. IsBV a => a -> a -> a
BV.bvxor)
  , (s
"bvnand", bv -> bv -> bv
forall a. IsBV a => a -> a -> a
BV.bvnand)
  , (s
"bvnor", bv -> bv -> bv
forall a. IsBV a => a -> a -> a
BV.bvnor)
  , (s
"bvxnor", bv -> bv -> bv
forall a. IsBV a => a -> a -> a
BV.bvxnor)
  , (s
"bvadd", bv -> bv -> bv
forall a. IsBV a => a -> a -> a
BV.bvadd)
  , (s
"bvsub", bv -> bv -> bv
forall a. IsBV a => a -> a -> a
BV.bvsub)
  , (s
"bvmul", bv -> bv -> bv
forall a. IsBV a => a -> a -> a
BV.bvmul)
  , (s
"bvudiv", bv -> bv -> bv
forall a. IsBV a => a -> a -> a
BV.bvudiv)
  , (s
"bvurem", bv -> bv -> bv
forall a. IsBV a => a -> a -> a
BV.bvurem)
  , (s
"bvsdiv", bv -> bv -> bv
forall a. IsBV a => a -> a -> a
BV.bvsdiv)
  , (s
"bvsrem", bv -> bv -> bv
forall a. IsBV a => a -> a -> a
BV.bvsrem)
  , (s
"bvsmod", bv -> bv -> bv
forall a. IsBV a => a -> a -> a
BV.bvsmod)
  , (s
"bvshl", bv -> bv -> bv
forall a. IsBV a => a -> a -> a
BV.bvshl)
  , (s
"bvlshr", bv -> bv -> bv
forall a. IsBV a => a -> a -> a
BV.bvlshr)
  , (s
"bvashr", bv -> bv -> bv
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)) = Expr -> IO Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> IO Expr) -> Expr -> IO Expr
forall a b. (a -> b) -> a -> b
$ BV -> Expr
forall a. IsBV a => BV -> a
BV.fromBV BV
bv
exprToBVExpr Solver
solver (EAp FSym
"concat" [Expr
x,Expr
y]) = do
  (Expr -> Expr -> Expr) -> IO Expr -> IO Expr -> IO Expr
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Expr -> Expr -> Expr
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
  Int -> Int -> Expr -> Expr
forall a. IsBV a => Int -> Int -> a -> a
BV.extract (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i) (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
j) (Expr -> Expr) -> IO Expr -> IO Expr
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
  Int -> Expr -> Expr
forall m. Monoid m => Int -> m -> m
BV.repeat (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i) (Expr -> Expr) -> IO Expr -> IO Expr
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
  Int -> Expr -> Expr
forall a. IsBV a => Int -> a -> a
BV.zeroExtend (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i) (Expr -> Expr) -> IO Expr -> IO Expr
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
  Int -> Expr -> Expr
forall a. IsBV a => Int -> a -> a
BV.signExtend (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i) (Expr -> Expr) -> IO Expr -> IO Expr
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
  Expr -> Int -> Expr
forall a. Bits a => a -> Int -> a
rotateL (Expr -> Int -> Expr) -> IO Expr -> IO (Int -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver -> Expr -> IO Expr
exprToBVExpr Solver
solver Expr
x IO (Int -> Expr) -> IO Int -> IO Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> IO Int
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Int
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
  Expr -> Int -> Expr
forall a. Bits a => a -> Int -> a
rotateR (Expr -> Int -> Expr) -> IO Expr -> IO (Int -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver -> Expr -> IO Expr
exprToBVExpr Solver
solver Expr
x IO (Int -> Expr) -> IO Int -> IO Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> IO Int
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Int
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' <- InternedText
-> Map InternedText (Expr -> Expr) -> Maybe (Expr -> Expr)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup InternedText
op1 Map InternedText (Expr -> Expr)
table = Expr -> Expr
op1' (Expr -> Expr) -> IO Expr -> IO Expr
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 =
      [(InternedText, Expr -> Expr)] -> Map InternedText (Expr -> Expr)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
      [ (InternedText
"bvnot", Expr -> Expr
forall a. IsBV a => a -> a
BV.bvnot)
      , (InternedText
"bvneg", Expr -> Expr
forall a. IsBV a => a -> a
BV.bvneg)
      ]
exprToBVExpr Solver
solver (EAp (FSym InternedText
op2 []) [Expr
x,Expr
y])
  | Just Expr -> Expr -> Expr
op2' <- InternedText
-> Map InternedText (Expr -> Expr -> Expr)
-> Maybe (Expr -> Expr -> Expr)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup InternedText
op2 Map InternedText (Expr -> Expr -> Expr)
table = (Expr -> Expr -> Expr) -> IO Expr -> IO Expr -> IO Expr
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 = [(InternedText, Expr -> Expr -> Expr)]
-> Map InternedText (Expr -> Expr -> Expr)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(InternedText, Expr -> Expr -> Expr)]
 -> Map InternedText (Expr -> Expr -> Expr))
-> [(InternedText, Expr -> Expr -> Expr)]
-> Map InternedText (Expr -> Expr -> Expr)
forall a b. (a -> b) -> a -> b
$ [(InternedText
"bvcomp", Expr -> Expr -> Expr
forall a. IsBV a => a -> a -> a
BV.bvcomp)] [(InternedText, Expr -> Expr -> Expr)]
-> [(InternedText, Expr -> Expr -> Expr)]
-> [(InternedText, Expr -> Expr -> Expr)]
forall a. [a] -> [a] -> [a]
++ [(InternedText, Expr -> Expr -> Expr)]
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) (Expr -> Int
forall a. IsBV a => a -> Int
BV.width Expr
t')
  Int
c1 <- Solver -> Atom -> IO Int
abstractBVAtom Solver
solver (Expr
ret Expr -> Expr -> Atom
forall e r. IsEqRel e r => e -> e -> r
.==. Expr
t')
  Int
c2 <- Solver -> Atom -> IO Int
abstractBVAtom Solver
solver (Expr
ret Expr -> Expr -> Atom
forall e r. IsEqRel e r => e -> e -> r
.==. Expr
e')
  Encoder IO -> Formula -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
smtEnc Solver
solver) (Formula -> IO ()) -> Formula -> IO ()
forall a b. (a -> b) -> a -> b
$ Formula -> Formula -> Formula -> Formula
forall b a. IfThenElse b a => b -> a -> a -> a
ite Formula
c' (Int -> Formula
forall a. a -> BoolExpr a
Atom Int
c1) (Int -> Formula
forall a. a -> BoolExpr a
Atom Int
c2)
  Expr -> IO Expr
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
_ -> String -> IO Expr
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
(BVAtomNormalized -> BVAtomNormalized -> Bool)
-> (BVAtomNormalized -> BVAtomNormalized -> Bool)
-> Eq BVAtomNormalized
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
Eq BVAtomNormalized
-> (BVAtomNormalized -> BVAtomNormalized -> Ordering)
-> (BVAtomNormalized -> BVAtomNormalized -> Bool)
-> (BVAtomNormalized -> BVAtomNormalized -> Bool)
-> (BVAtomNormalized -> BVAtomNormalized -> Bool)
-> (BVAtomNormalized -> BVAtomNormalized -> Bool)
-> (BVAtomNormalized -> BVAtomNormalized -> BVAtomNormalized)
-> (BVAtomNormalized -> BVAtomNormalized -> BVAtomNormalized)
-> Ord 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
$cp1Ord :: Eq BVAtomNormalized
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 Atom -> Atom
forall a. a -> a
id else Atom -> Atom
forall a. Complement a => a -> a
notB) (Atom -> Atom) -> Atom -> Atom
forall a b. (a -> b) -> a -> b
$ OrdRel Expr -> Bool -> Atom
BV.Rel (Expr -> RelOp -> Expr -> OrdRel Expr
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 Atom -> Atom
forall a. a -> a
id else Atom -> Atom
forall a. Complement a => a -> a
notB) (Atom -> Atom) -> Atom -> Atom
forall a b. (a -> b) -> a -> b
$ OrdRel Expr -> Bool -> Atom
BV.Rel (Expr -> RelOp -> Expr -> OrdRel Expr
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 Atom -> Atom
forall a. a -> a
id else Atom -> Atom
forall a. Complement a => a -> a
notB) (Atom -> Atom) -> Atom -> Atom
forall a b. (a -> b) -> a -> b
$ OrdRel Expr -> Bool -> Atom
BV.Rel (Expr -> RelOp -> Expr -> OrdRel Expr
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) <- IORef (Map BVAtomNormalized Int, IntMap BVAtomNormalized)
-> IO (Map BVAtomNormalized Int, IntMap BVAtomNormalized)
forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map BVAtomNormalized Int, IntMap BVAtomNormalized)
smtBVAtomDefs Solver
solver)
  Int
v <- case BVAtomNormalized -> Map BVAtomNormalized Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup BVAtomNormalized
atom' Map BVAtomNormalized Int
tbl of
         Just Int
v -> Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
v
         Maybe Int
Nothing -> do
           Int
v <- Solver -> IO Int
forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar (Solver -> Solver
smtSAT Solver
solver)
           IORef (Map BVAtomNormalized Int, IntMap BVAtomNormalized)
-> (Map BVAtomNormalized Int, IntMap BVAtomNormalized) -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (Map BVAtomNormalized Int, IntMap BVAtomNormalized)
smtBVAtomDefs Solver
solver) (BVAtomNormalized
-> Int -> Map BVAtomNormalized Int -> Map BVAtomNormalized Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert BVAtomNormalized
atom' Int
v Map BVAtomNormalized Int
tbl, Int
-> BVAtomNormalized
-> IntMap BVAtomNormalized
-> IntMap BVAtomNormalized
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
v BVAtomNormalized
atom' IntMap BVAtomNormalized
defs)
           Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
v
  Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> IO Int) -> Int -> IO Int
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) <- IORef (Map Expr Int, IntMap (IntMap Expr))
-> IO (Map Expr Int, IntMap (IntMap Expr))
forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map Expr Int, IntMap (IntMap Expr))
smtBVTermDefs Solver
solver)
  case Expr -> Map Expr Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Expr
e Map Expr Int
bvToFSym of
    Just Int
c -> Term -> IO Term
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 = Expr -> Int
forall a. IsBV a => a -> Int
BV.width Expr
e
          m :: IntMap Expr
m = IntMap Expr -> Int -> IntMap (IntMap Expr) -> IntMap Expr
forall a. a -> Int -> IntMap a -> a
IntMap.findWithDefault IntMap Expr
forall a. IntMap a
IntMap.empty Int
w IntMap (IntMap Expr)
fsymToBV
      [(Int, Expr)] -> ((Int, Expr) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntMap Expr -> [(Int, Expr)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap Expr
m) (((Int, Expr) -> IO ()) -> IO ())
-> ((Int, Expr) -> IO ()) -> IO ()
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 Expr -> Expr -> Atom
forall e r. IsEqRel e r => e -> e -> r
.==. Expr
d_bv)
        Encoder IO -> Formula -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
smtEnc Solver
solver) (Int -> Formula
forall a. a -> BoolExpr a
Atom Int
b1 Formula -> Formula -> Formula
forall a. Boolean a => a -> a -> a
.<=>. Int -> Formula
forall a. a -> BoolExpr a
Atom Int
b2)
      IORef (Map Expr Int, IntMap (IntMap Expr))
-> (Map Expr Int, IntMap (IntMap Expr)) -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (Map Expr Int, IntMap (IntMap Expr))
smtBVTermDefs Solver
solver) ((Map Expr Int, IntMap (IntMap Expr)) -> IO ())
-> (Map Expr Int, IntMap (IntMap Expr)) -> IO ()
forall a b. (a -> b) -> a -> b
$
        ( Expr -> Int -> Map Expr Int -> Map Expr Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Expr
e Int
c Map Expr Int
bvToFSym
        , Int -> IntMap Expr -> IntMap (IntMap Expr) -> IntMap (IntMap Expr)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
w (Int -> Expr -> IntMap Expr -> IntMap Expr
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
c Expr
e IntMap Expr
m) IntMap (IntMap Expr)
fsymToBV
        )
      Term -> IO Term
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) <- IORef (Map Expr Int, IntMap (IntMap Expr))
-> IO (Map Expr Int, IntMap (IntMap Expr))
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 = IntMap Expr -> Int -> IntMap (IntMap Expr) -> IntMap Expr
forall a. a -> Int -> IntMap a -> a
IntMap.findWithDefault IntMap Expr
forall a. IntMap a
IntMap.empty Int
w IntMap (IntMap Expr)
fsymToBV
  case Int -> IntMap Expr -> Maybe Expr
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
c IntMap Expr
m of
    Just Expr
e -> Expr -> IO Expr
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
      [(Int, Expr)] -> ((Int, Expr) -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (IntMap Expr -> [(Int, Expr)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap Expr
m) (((Int, Expr) -> IO ()) -> IO ())
-> ((Int, Expr) -> IO ()) -> IO ()
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 Expr -> Expr -> Atom
forall e r. IsEqRel e r => e -> e -> r
.==. Expr
d_bv)
        Encoder IO -> Formula -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
smtEnc Solver
solver) (Int -> Formula
forall a. a -> BoolExpr a
Atom Int
b1 Formula -> Formula -> Formula
forall a. Boolean a => a -> a -> a
.<=>. Int -> Formula
forall a. a -> BoolExpr a
Atom Int
b2)
      IORef (Map Expr Int, IntMap (IntMap Expr))
-> (Map Expr Int, IntMap (IntMap Expr)) -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (Map Expr Int, IntMap (IntMap Expr))
smtBVTermDefs Solver
solver) ((Map Expr Int, IntMap (IntMap Expr)) -> IO ())
-> (Map Expr Int, IntMap (IntMap Expr)) -> IO ()
forall a b. (a -> b) -> a -> b
$
        ( Expr -> Int -> Map Expr Int -> Map Expr Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Expr
e Int
c Map Expr Int
bvToFSym
        , Int -> IntMap Expr -> IntMap (IntMap Expr) -> IntMap (IntMap Expr)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
w (Int -> Expr -> IntMap Expr -> IntMap Expr
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
c Expr
e IntMap Expr
m) IntMap (IntMap Expr)
fsymToBV
        )
      Expr -> IO Expr
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')
  Encoder IO -> Formula -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
smtEnc Solver
solver) (Formula -> IO ()) -> Formula -> IO ()
forall a b. (a -> b) -> a -> b
$ Formula -> Formula -> Formula -> Formula
forall b a. IfThenElse b a => b -> a -> a -> a
ite Formula
c' (Int -> Formula
forall a. a -> BoolExpr a
Atom Int
c1) (Int -> Formula
forall a. a -> BoolExpr a
Atom Int
c2)
  Term -> IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
ret
exprToEUFTerm Solver
solver FSym
f [Expr]
xs = do
  Map FSym FDef
fdefs <- IORef (Map FSym FDef) -> IO (Map FSym FDef)
forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map FSym FDef)
smtFDefs Solver
solver)
  case FSym -> Map FSym FDef -> Maybe FDef
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
forall a. a -> BoolExpr a
Atom Int
v)
    Just (FLRAVar Int
v) -> Solver -> Expr Rational -> IO Term
lraExprToEUFTerm Solver
solver (Int -> Expr Rational
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
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Sort] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Sort]
ps Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Expr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
xs) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
        Exception -> IO ()
forall e a. Exception e => e -> IO a
E.throwIO (Exception -> IO ()) -> Exception -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Exception
Error String
"argument number error"
      ([Term] -> Term) -> IO [Term] -> IO Term
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Int -> [Term] -> Term
EUF.TApp Int
fsym) (IO [Term] -> IO Term) -> IO [Term] -> IO Term
forall a b. (a -> b) -> a -> b
$ (Expr -> IO Term) -> [Expr] -> IO [Term]
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
_ -> Exception -> IO Term
forall a e. Exception e => e -> a
E.throw (Exception -> IO Term) -> Exception -> IO Term
forall a b. (a -> b) -> a -> b
$ String -> Exception
Error (String -> Exception) -> String -> Exception
forall a b. (a -> b) -> a -> b
$ String
"unknown function symbol: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ FSym -> String
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) = Term -> IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> IO Term) -> Term -> IO Term
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 (Rational -> Expr Rational
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 (BV -> Expr
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 (Formula -> IO Term) -> IO Formula -> IO Term
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 (Expr Rational -> IO Term) -> IO (Expr Rational) -> IO Term
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 (Expr -> IO Term) -> IO Expr -> IO Term
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 Term -> Term -> Bool
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) <- IORef (Map (Term, Term) Int, IntMap (Term, Term))
-> IO (Map (Term, Term) Int, IntMap (Term, Term))
forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map (Term, Term) Int, IntMap (Term, Term))
smtEUFAtomDefs Solver
solver)
  case (Term, Term) -> Map (Term, Term) Int -> Maybe Int
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 -> Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
v
    Maybe Int
Nothing -> do
      Int
v <- Solver -> IO Int
forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar (Solver -> Solver
smtSAT Solver
solver)
      IORef (Map (Term, Term) Int, IntMap (Term, Term))
-> (Map (Term, Term) Int, IntMap (Term, Term)) -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (Map (Term, Term) Int, IntMap (Term, Term))
smtEUFAtomDefs Solver
solver) ((Term, Term) -> Int -> Map (Term, Term) Int -> Map (Term, Term) Int
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, Int -> (Term, Term) -> IntMap (Term, Term) -> IntMap (Term, Term)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
v (Term
t1,Term
t2) IntMap (Term, Term)
defs)
      Int -> IO Int
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 <- Encoder IO -> Formula -> IO Int
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) <- IORef (Map Term Int, IntMap Term) -> IO (Map Term Int, IntMap Term)
forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map Term Int, IntMap Term)
smtBoolTermDefs Solver
solver)
  case Int -> IntMap Term -> Maybe Term
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
lit IntMap Term
boolToTerm of
    Just Term
t -> Term -> IO Term
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
      Term -> IO Term
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
_) <- IORef (Map Term Int, IntMap Term) -> IO (Map Term Int, IntMap Term)
forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map Term Int, IntMap Term)
smtBoolTermDefs Solver
solver)
  case Term -> Map Term Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Term
t Map Term Int
termToBool of
    Just Int
lit -> Formula -> IO Formula
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Formula
forall a. a -> BoolExpr a
Atom Int
lit)
    Maybe Int
Nothing -> do
      Int
lit <- Solver -> IO Int
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
      Formula -> IO Formula
forall (m :: * -> *) a. Monad m => a -> m a
return (Formula -> IO Formula) -> Formula -> IO Formula
forall a b. (a -> b) -> a -> b
$ Int -> Formula
forall a. a -> BoolExpr a
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)
  Solver -> [Int] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause (Solver -> Solver
smtSAT Solver
solver) [-Int
lit, Int
lit1]  --  lit  ->  lit1
  Solver -> [Int] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause (Solver -> Solver
smtSAT Solver
solver) [-Int
lit1, Int
lit]  --  lit1 ->  lit
  Solver -> [Int] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause (Solver -> Solver
smtSAT Solver
solver) [Int
lit, Int
lit2]   -- -lit  ->  lit2
  Solver -> [Int] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause (Solver -> Solver
smtSAT Solver
solver) [-Int
lit2, -Int
lit] --  lit2 -> -lit
  IORef (Map Term Int, IntMap Term)
-> ((Map Term Int, IntMap Term) -> (Map Term Int, IntMap Term))
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef (Solver -> IORef (Map Term Int, IntMap Term)
smtBoolTermDefs Solver
solver) (((Map Term Int, IntMap Term) -> (Map Term Int, IntMap Term))
 -> IO ())
-> ((Map Term Int, IntMap Term) -> (Map Term Int, IntMap Term))
-> IO ()
forall a b. (a -> b) -> a -> b
$ \(Map Term Int
termToBool, IntMap Term
boolToTerm) ->
    ( Term -> Int -> Map Term Int -> Map Term Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Term
t Int
lit Map Term Int
termToBool
    , Int -> Term -> IntMap Term -> IntMap Term
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 <- IORef (Map String Int) -> IO (Map String Int)
forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map String Int)
smtNamedAssertions Solver
solver)

  IORef (IntMap Expr)
ref <- IntMap Expr -> IO (IORef (IntMap Expr))
forall a. a -> IO (IORef a)
newIORef IntMap Expr
forall a. IntMap a
IntMap.empty
  [Int]
ls <- [Expr] -> (Expr -> IO Int) -> IO [Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Expr]
xs ((Expr -> IO Int) -> IO [Int]) -> (Expr -> IO Int) -> IO [Int]
forall a b. (a -> b) -> a -> b
$ \Expr
x -> do
    Int
b <- Encoder IO -> Formula -> IO Int
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Int
Tseitin.encodeFormula (Solver -> Encoder IO
smtEnc Solver
solver) (Formula -> IO Int) -> IO Formula -> IO Int
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> Expr -> IO Formula
exprToFormula Solver
solver Expr
x
    IORef (IntMap Expr) -> (IntMap Expr -> IntMap Expr) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef (IntMap Expr)
ref (Int -> Expr -> IntMap Expr -> IntMap Expr
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
b Expr
x)
    Int -> IO Int
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 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
ls [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ Map String Int -> [Int]
forall k a. Map k a -> [a]
Map.elems Map String Int
named)
  if Bool
ret then do
    IORef [Expr] -> [Expr] -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef [Expr]
smtUnsatAssumptions Solver
solver) [Expr]
forall a. HasCallStack => a
undefined
    IORef [String] -> [String] -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef [String]
smtUnsatCore Solver
solver) [String]
forall a. HasCallStack => a
undefined
  else do
    IntMap Expr
m1 <- IORef (IntMap Expr) -> IO (IntMap Expr)
forall a. IORef a -> IO a
readIORef IORef (IntMap Expr)
ref
    let m2 :: IntMap String
m2 = [(Int, String)] -> IntMap String
forall a. [(Int, a)] -> IntMap a
IntMap.fromList [(Int
lit, String
name) | (String
name, Int
lit) <- Map String Int -> [(String, Int)]
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)
    IORef [Expr] -> [Expr] -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef [Expr]
smtUnsatAssumptions Solver
solver) ([Expr] -> IO ()) -> [Expr] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Maybe Expr] -> [Expr]
forall a. [Maybe a] -> [a]
catMaybes [Int -> IntMap Expr -> Maybe Expr
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
l IntMap Expr
m1 | Int
l <- IntSet -> [Int]
IntSet.toList IntSet
failed]
    IORef [String] -> [String] -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef [String]
smtUnsatCore Solver
solver) ([String] -> IO ()) -> [String] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Maybe String] -> [String]
forall a. [Maybe a] -> [a]
catMaybes [Int -> IntMap String -> Maybe String
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
l IntMap String
m2 | Int
l <- IntSet -> [Int]
IntSet.toList IntSet
failed]
  Bool -> IO Bool
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 <- Vec AssertionLevel -> IO Int
forall (a :: * -> * -> *) e. GenericVec a e -> IO Int
Vec.getSize (Solver -> Vec AssertionLevel
smtAssertionStack Solver
solver)
  if Int
nInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>Int
0 then do
    AssertionLevel
assertionLevel <- Vec AssertionLevel -> IO AssertionLevel
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO e
Vec.peek (Solver -> Vec AssertionLevel
smtAssertionStack Solver
solver)
    Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ AssertionLevel -> Int
alSelector AssertionLevel
assertionLevel
  else
    Encoder IO -> [Int] -> IO Int
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 <- Solver -> IO Int
forall (m :: * -> *) a. NewVar m a => a -> m Int
SAT.newVar (Solver -> Solver
smtSAT Solver
solver)
  Solver -> [Int] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause (Solver -> Solver
smtSAT Solver
solver) [-Int
l2, Int
l1] -- l2 → l1
  Bool
globalDeclarations <- IORef Bool -> IO Bool
forall a. IORef a -> IO a
readIORef (Solver -> IORef Bool
smtGlobalDeclarationsRef Solver
solver)
  Map String Int
named <- IORef (Map String Int) -> IO (Map String Int)
forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map String Int)
smtNamedAssertions Solver
solver)
  Map FSym FDef
fdefs <- IORef (Map FSym FDef) -> IO (Map FSym FDef)
forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map FSym FDef)
smtFDefs Solver
solver)
  let newLevel :: AssertionLevel
newLevel =
        AssertionLevel :: Map String Int -> Maybe (Map FSym FDef) -> Int -> AssertionLevel
AssertionLevel
        { alSavedNamedAssertions :: Map String Int
alSavedNamedAssertions = Map String Int
named
        , alSavedFDefs :: Maybe (Map FSym FDef)
alSavedFDefs = if Bool
globalDeclarations then Maybe (Map FSym FDef)
forall a. Maybe a
Nothing else Map FSym FDef -> Maybe (Map FSym FDef)
forall a. a -> Maybe a
Just Map FSym FDef
fdefs
        , alSelector :: Int
alSelector = Int
l2
        }
  Vec AssertionLevel -> AssertionLevel -> IO ()
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 <- Vec AssertionLevel -> IO Int
forall (a :: * -> * -> *) e. GenericVec a e -> IO Int
Vec.getSize (Solver -> Vec AssertionLevel
smtAssertionStack Solver
solver)
  if Int
nInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
0 then
    Exception -> IO ()
forall e a. Exception e => e -> IO a
E.throwIO (Exception -> IO ()) -> Exception -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Exception
Error (String -> Exception) -> String -> Exception
forall a b. (a -> b) -> a -> b
$ String
"cannot pop first assertion level"
  else do
    AssertionLevel
assertionLevel <- Vec AssertionLevel -> IO AssertionLevel
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO e
Vec.unsafePop (Solver -> Vec AssertionLevel
smtAssertionStack Solver
solver)
    Solver -> [Int] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause (Solver -> Solver
smtSAT Solver
solver) [- AssertionLevel -> Int
alSelector AssertionLevel
assertionLevel]
    IORef (Map String Int) -> Map String Int -> IO ()
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 -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      Just Map FSym FDef
fdefs -> IORef (Map FSym FDef) -> Map FSym FDef -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (Map FSym FDef)
smtFDefs Solver
solver) Map FSym FDef
fdefs
    () -> IO ()
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
(Int -> Model -> ShowS)
-> (Model -> String) -> ([Model] -> ShowS) -> Show Model
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
(Value -> Value -> Bool) -> (Value -> Value -> Bool) -> Eq Value
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
Eq Value
-> (Value -> Value -> Ordering)
-> (Value -> Value -> Bool)
-> (Value -> Value -> Bool)
-> (Value -> Value -> Bool)
-> (Value -> Value -> Bool)
-> (Value -> Value -> Value)
-> (Value -> Value -> Value)
-> Ord 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
$cp1Ord :: Eq Value
Ord, Int -> Value -> ShowS
[Value] -> ShowS
Value -> String
(Int -> Value -> ShowS)
-> (Value -> String) -> ([Value] -> ShowS) -> Show Value
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 <- IORef (Map FSym FDef) -> IO (Map FSym FDef)
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 <- IORef Model -> IO Model
forall a. IORef a -> IO a
readIORef (Solver -> IORef Model
smtLRAModel Solver
solver)
  Model
bvModel  <- IORef Model -> IO Model
forall a. IORef a -> IO a
readIORef (Solver -> IORef Model
smtBVModel Solver
solver)
  Model
eufModel <- IORef Model -> IO Model
forall a. IORef a -> IO a
readIORef (Solver -> IORef Model
smtEUFModel Solver
solver)

  (Map (Expr Rational) Int
_, IntMap (Expr Rational)
fsymToReal) <- IORef (Map (Expr Rational) Int, IntMap (Expr Rational))
-> IO (Map (Expr Rational) Int, IntMap (Expr Rational))
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, Model -> Expr Rational -> Rational
forall m e v. Eval m e v => m -> e -> v
LA.eval Model
lraModel Expr Rational
lraExpr) | (Int
fsym, Expr Rational
lraExpr) <- IntMap (Expr Rational) -> [(Int, Expr Rational)]
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Model -> Int
EUF.mUnspecified Model
eufModel]

  (Map Expr Int
_, IntMap (IntMap Expr)
fsymToBV) <- IORef (Map Expr Int, IntMap (IntMap Expr))
-> IO (Map Expr Int, IntMap (IntMap Expr))
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) <- IntMap (IntMap Expr) -> [(Int, IntMap Expr)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (IntMap Expr)
fsymToBV, (Int
fsym, Expr
bvExpr) <- IntMap Expr -> [(Int, Expr)]
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Model -> Int
EUF.mUnspecified Model
eufModel]

  Model -> IO Model
forall (m :: * -> *) a. Monad m => a -> m a
return (Model -> IO Model) -> Model -> IO Model
forall a b. (a -> b) -> a -> b
$
    Model :: Map FSym FDef
-> Model
-> Model
-> Model
-> Model
-> Int
-> Int
-> Model
-> Map Rational Int
-> IntMap BV
-> Map BV Int
-> Model
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 = [(Int, Rational)] -> Model
forall a. [(Int, a)] -> IntMap a
IntMap.fromList [(Int, Rational)]
xs
    , mRationalToEntity :: Map Rational Int
mRationalToEntity = [(Rational, Int)] -> Map Rational Int
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 = [(Int, BV)] -> IntMap BV
forall a. [(Int, a)] -> IntMap a
IntMap.fromList [(Int, BV)]
ys
    , mBitVecToEntity :: Map BV Int
mBitVecToEntity = [(BV, Int)] -> Map BV Int
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 (Bool -> Value) -> Bool -> Value
forall a b. (a -> b) -> a -> b
$ [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (Expr -> Bool) -> [Expr] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Model -> Value -> Bool
valToBool Model
m (Value -> Bool) -> (Expr -> Value) -> Expr -> Bool
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 (Bool -> Value) -> Bool -> Value
forall a b. (a -> b) -> a -> b
$ [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (Expr -> Bool) -> [Expr] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Model -> Value -> Bool
valToBool Model
m (Value -> Bool) -> (Expr -> Value) -> Expr -> Bool
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 (Bool -> Value) -> Bool -> Value
forall a b. (a -> b) -> a -> b
$ (Bool -> Bool -> Bool) -> Bool -> [Bool] -> Bool
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Bool -> Bool -> Bool
forall a. Bits a => a -> a -> a
xor Bool
False ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (Expr -> Bool) -> [Expr] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Model -> Value -> Bool
valToBool Model
m (Value -> Bool) -> (Expr -> Value) -> Expr -> Bool
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 (Bool -> Value) -> Bool -> Value
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Model -> Value -> Bool
valToBool Model
m (Value -> Bool) -> Value -> Bool
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 (Bool -> Value) -> Bool -> Value
forall a b. (a -> b) -> a -> b
$ Model -> Value -> Bool
valToBool Model
m (Model -> Expr -> Value
eval Model
m Expr
x) Bool -> Bool -> Bool
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 (Bool -> Value) -> Bool -> Value
forall a b. (a -> b) -> a -> b
$ Model -> Value -> Rational
valToRational Model
m (Model -> Expr -> Value
eval Model
m Expr
x) Rational -> Rational -> Bool
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 (Bool -> Value) -> Bool -> Value
forall a b. (a -> b) -> a -> b
$ Model -> Value -> Rational
valToRational Model
m (Model -> Expr -> Value
eval Model
m Expr
x) Rational -> Rational -> Bool
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 (Bool -> Value) -> Bool -> Value
forall a b. (a -> b) -> a -> b
$ Model -> Value -> Rational
valToRational Model
m (Model -> Expr -> Value
eval Model
m Expr
x) Rational -> Rational -> Bool
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 (Bool -> Value) -> Bool -> Value
forall a b. (a -> b) -> a -> b
$ Model -> Value -> Rational
valToRational Model
m (Model -> Expr -> Value
eval Model
m Expr
x) Rational -> Rational -> Bool
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 (Rational -> Value) -> Rational -> Value
forall a b. (a -> b) -> a -> b
$ [Rational] -> Rational
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Rational] -> Rational) -> [Rational] -> Rational
forall a b. (a -> b) -> a -> b
$ (Expr -> Rational) -> [Expr] -> [Rational]
forall a b. (a -> b) -> [a] -> [b]
map (Model -> Value -> Rational
valToRational Model
m (Value -> Rational) -> (Expr -> Value) -> Expr -> Rational
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 (Rational -> Value) -> Rational -> Value
forall a b. (a -> b) -> a -> b
$ Rational -> Rational
forall a. Num a => a -> a
negate (Rational -> Rational) -> Rational -> Rational
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 (Rational -> Value) -> Rational -> Value
forall a b. (a -> b) -> a -> b
$ Model -> Value -> Rational
valToRational Model
m (Model -> Expr -> Value
eval Model
m Expr
x) Rational -> Rational -> Rational
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 (Rational -> Value) -> Rational -> Value
forall a b. (a -> b) -> a -> b
$ [Rational] -> Rational
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product ([Rational] -> Rational) -> [Rational] -> Rational
forall a b. (a -> b) -> a -> b
$ (Expr -> Rational) -> [Expr] -> [Rational]
forall a b. (a -> b) -> [a] -> [b]
map (Model -> Value -> Rational
valToRational Model
m (Value -> Rational) -> (Expr -> Value) -> Expr -> Rational
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' Rational -> Rational -> Bool
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 (Rational -> Value) -> Rational -> Value
forall a b. (a -> b) -> a -> b
$ Model -> Value -> Rational
valToRational Model
m (Model -> Expr -> Value
eval Model
m Expr
x) Rational -> Rational -> Rational
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 (Bool -> Value) -> Bool -> Value
forall a b. (a -> b) -> a -> b
$ BV -> BV -> ComparisonResult BV
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 (Bool -> Value) -> Bool -> Value
forall a b. (a -> b) -> a -> b
$ BV -> BV -> ComparisonResult BV
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 (Bool -> Value) -> Bool -> Value
forall a b. (a -> b) -> a -> b
$ BV -> BV -> ComparisonResult BV
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 (Bool -> Value) -> Bool -> Value
forall a b. (a -> b) -> a -> b
$ BV -> BV -> ComparisonResult BV
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 (Bool -> Value) -> Bool -> Value
forall a b. (a -> b) -> a -> b
$ BV -> BV -> ComparisonResult BV
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 (Bool -> Value) -> Bool -> Value
forall a b. (a -> b) -> a -> b
$ BV -> BV -> ComparisonResult BV
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 (Bool -> Value) -> Bool -> Value
forall a b. (a -> b) -> a -> b
$ BV -> BV -> ComparisonResult BV
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 (Bool -> Value) -> Bool -> Value
forall a b. (a -> b) -> a -> b
$ BV -> BV -> ComparisonResult BV
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 (BV -> Value) -> BV -> Value
forall a b. (a -> b) -> a -> b
$ Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
x) BV -> BV -> BV
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 (BV -> Value) -> BV -> Value
forall a b. (a -> b) -> a -> b
$ Int -> Int -> BV -> BV
forall a. IsBV a => Int -> Int -> a -> a
BV.extract (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i) (Integer -> Int
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 (BV -> Value) -> BV -> Value
forall a b. (a -> b) -> a -> b
$ Int -> BV -> BV
forall m. Monoid m => Int -> m -> m
BV.repeat (Integer -> Int
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 (BV -> Value) -> BV -> Value
forall a b. (a -> b) -> a -> b
$ Int -> BV -> BV
forall a. IsBV a => Int -> a -> a
BV.zeroExtend (Integer -> Int
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 (BV -> Value) -> BV -> Value
forall a b. (a -> b) -> a -> b
$ Int -> BV -> BV
forall a. IsBV a => Int -> a -> a
BV.signExtend (Integer -> Int
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 (BV -> Value) -> BV -> Value
forall a b. (a -> b) -> a -> b
$ BV -> Int -> BV
forall a. Bits a => a -> Int -> a
rotateL (Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
x)) (Integer -> Int
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 (BV -> Value) -> BV -> Value
forall a b. (a -> b) -> a -> b
$ BV -> Int -> BV
forall a. Bits a => a -> Int -> a
rotateR (Model -> Value -> BV
valToBitVec Model
m (Model -> Expr -> Value
eval Model
m Expr
x)) (Integer -> Int
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' <- InternedText
-> Map InternedText (Expr -> Expr) -> Maybe (Expr -> Expr)
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 (BV -> Expr) -> BV -> Expr
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 (BV -> Value) -> BV -> Value
forall a b. (a -> b) -> a -> b
$ Model -> Expr -> BV
BV.evalExpr (Model -> Model
mBVModel Model
m) (Expr -> BV) -> Expr -> BV
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
op1' Expr
x'
  where
    table :: Map InternedText (Expr -> Expr)
table =
      [(InternedText, Expr -> Expr)] -> Map InternedText (Expr -> Expr)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
      [ (InternedText
"bvnot", Expr -> Expr
forall a. IsBV a => a -> a
BV.bvnot)
      , (InternedText
"bvneg", Expr -> Expr
forall a. IsBV a => a -> a
BV.bvneg)
      ]
eval Model
m (EAp (FSym InternedText
op2 []) [Expr
x,Expr
y])
  | Just Expr -> Expr -> Expr
op2' <- InternedText
-> Map InternedText (Expr -> Expr -> Expr)
-> Maybe (Expr -> Expr -> Expr)
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 (BV -> Expr) -> BV -> Expr
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 (BV -> Expr) -> BV -> Expr
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 (BV -> Value) -> BV -> Value
forall a b. (a -> b) -> a -> b
$ Model -> Expr -> BV
BV.evalExpr (Model -> Model
mBVModel Model
m) (Expr -> BV) -> Expr -> BV
forall a b. (a -> b) -> a -> b
$ Expr -> Expr -> Expr
op2' Expr
x' Expr
y'
  where
    table :: Map InternedText (Expr -> Expr -> Expr)
table = [(InternedText, Expr -> Expr -> Expr)]
-> Map InternedText (Expr -> Expr -> Expr)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(InternedText, Expr -> Expr -> Expr)]
 -> Map InternedText (Expr -> Expr -> Expr))
-> [(InternedText, Expr -> Expr -> Expr)]
-> Map InternedText (Expr -> Expr -> Expr)
forall a b. (a -> b) -> a -> b
$ [(InternedText
"bvcomp", Expr -> Expr -> Expr
forall a. IsBV a => a -> a -> a
BV.bvcomp)] [(InternedText, Expr -> Expr -> Expr)]
-> [(InternedText, Expr -> Expr -> Expr)]
-> [(InternedText, Expr -> Expr -> Expr)]
forall a. [a] -> [a] -> [a]
++ [(InternedText, Expr -> Expr -> Expr)]
forall s bv. (IsString s, IsBV bv) => [(s, bv -> bv -> bv)]
bvBinOpsSameSize

eval Model
m (EAp FSym
"=" [Expr
x,Expr
y])   = Bool -> Value
ValBool (Bool -> Value) -> Bool -> Value
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 Value -> Value -> Bool
forall a. Eq a => a -> a -> Bool
== Value
v2
eval Model
m expr :: Expr
expr@(EAp FSym
f [Expr]
xs) =
  case FSym -> Map FSym FDef -> Maybe FDef
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 -> Exception -> Value
forall a e. Exception e => e -> a
E.throw (Exception -> Value) -> Exception -> Value
forall a b. (a -> b) -> a -> b
$ String -> Exception
Error (String -> Exception) -> String -> Exception
forall a b. (a -> b) -> a -> b
$ String
"unknown function symbol: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ FSym -> String
forall a. Show a => a -> String
show FSym
f
    Just (FBoolVar Int
v) -> Bool -> Value
ValBool (Bool -> Value) -> Bool -> Value
forall a b. (a -> b) -> a -> b
$ Model -> Int -> Bool
forall m. IModel m => m -> Int -> Bool
SAT.evalLit (Model -> Model
mBoolModel Model
m) Int
v
    Just (FLRAVar Int
v) -> Rational -> Value
ValRational (Rational -> Value) -> Rational -> Value
forall a b. (a -> b) -> a -> b
$ Model -> Model
mLRAModel Model
m Model -> Int -> Rational
forall a. IntMap a -> Int -> a
IntMap.! Int
v
    Just (FBVVar Var
v) -> BV -> Value
ValBitVec (BV -> Value) -> BV -> Value
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 ((Expr -> Int) -> [Expr] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Model -> Value -> Int
valToEntity Model
m (Value -> Int) -> (Expr -> Value) -> Expr -> Int
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Model -> Int
mEUFTrue Model
m)
           SSym
SSymReal ->
             case Int -> Model -> Maybe Rational
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 (Int -> Rational
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
1000000 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
e))
           SSymBitVec Int
w ->
             case Int -> IntMap BV -> Maybe BV
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 (Int -> Integer -> BV
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
_ = Exception -> Bool
forall a e. Exception e => e -> a
E.throw (Exception -> Bool) -> Exception -> Bool
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
_ = Exception -> Rational
forall a e. Exception e => e -> a
E.throw (Exception -> Rational) -> Exception -> Rational
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
_ = Exception -> BV
forall a e. Exception e => e -> a
E.throw (Exception -> BV) -> Exception -> BV
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 Rational -> Map Rational Int -> Maybe Int
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 BV -> Map BV Int -> Maybe Int
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 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Model -> Int
mEUFTrue Model
m)
    Sort SSym
SSymReal [Sort]
_ ->
      case Int -> Model -> Maybe Rational
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 (Int -> Rational
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int
1000000 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
e))
    Sort (SSymBitVec Int
n) [Sort]
_ ->
      case Int -> IntMap BV -> Maybe BV
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 (Int -> Integer -> BV
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 (BV -> Int
forall a. IsBV a => a -> Int
BV.width BV
bv)

data FunDef = FunDef [([Value], Value)] Value
  deriving (FunDef -> FunDef -> Bool
(FunDef -> FunDef -> Bool)
-> (FunDef -> FunDef -> Bool) -> Eq FunDef
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
(Int -> FunDef -> ShowS)
-> (FunDef -> String) -> ([FunDef] -> ShowS) -> Show FunDef
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 FSym -> Map FSym FDef -> Maybe FDef
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) IntMap (Map [Int] Int) -> Int -> Map [Int] Int
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 (Int -> Integer -> BV
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 [ ((Int -> Sort -> Value) -> [Int] -> [Sort] -> [Value]
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) <- Map [Int] Int -> [([Int], Int)]
forall k a. Map k a -> [(k, a)]
Map.toList Map [Int] Int
tbl ]
                Value
defaultVal
    Just FDef
_ -> [([Value], Value)] -> Value -> FunDef
FunDef [] (Value -> FunDef) -> Value -> 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 -> Exception -> FunDef
forall a e. Exception e => e -> a
E.throw (Exception -> FunDef) -> Exception -> FunDef
forall a b. (a -> b) -> a -> b
$ String -> Exception
Error (String -> Exception) -> String -> Exception
forall a b. (a -> b) -> a -> b
$ String
"unknown function symbol: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ FSym -> String
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 Map FSym FDef -> FSym -> FDef
forall k a. Ord k => Map k a -> k -> a
Map.! FSym
"_/0"
  , ([Int
arg], Int
result) <- Map [Int] Int -> [([Int], Int)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map [Int] Int -> [([Int], Int)])
-> Map [Int] Int -> [([Int], Int)]
forall a b. (a -> b) -> a -> b
$ Model -> IntMap (Map [Int] Int)
EUF.mFunctions (Model -> Model
mEUFModel Model
m) IntMap (Map [Int] Int) -> Int -> Map [Int] Int
forall a. IntMap a -> Int -> a
IntMap.! Int
sym
  ]
  [Expr] -> [Expr] -> [Expr]
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 (Int -> Integer -> BV
forall a. IsBV a => Int -> Integer -> a
BV.nat2bv (BV -> Int
forall a. IsBV a => a -> Int
BV.width BV
s) Integer
0))
        ]
      , Value -> Expr
EValue (BV -> Value
ValBitVec BV
t)
      ]
  | (BV
s,BV
t) <- Map BV BV -> [(BV, BV)]
forall k a. Map k a -> [(k, a)]
Map.toList Map BV BV
bvDivTable
  ]
  [Expr] -> [Expr] -> [Expr]
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 (Int -> Integer -> BV
forall a. IsBV a => Int -> Integer -> a
BV.nat2bv (BV -> Int
forall a. IsBV a => a -> Int
BV.width BV
s) Integer
0))
        ]
      , Value -> Expr
EValue (BV -> Value
ValBitVec BV
t)
      ]
  | (BV
s,BV
t) <- Map BV BV -> [(BV, BV)]
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
  IORef [Expr] -> IO [Expr]
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
  IORef [String] -> IO [String]
forall a. IORef a -> IO a
readIORef (Solver -> IORef [String]
smtUnsatCore Solver
solver)

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

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