{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.BitVector.Solver
-- Copyright   :  (c) Masahiro Sakai 2016
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.BitVector.Solver
  (
  -- * BitVector solver
    Solver
  , newSolver
  , newVar
  , newVar'
  , assertAtom
  , check
  , getModel
  , explain
  , pushBacktrackPoint
  , popBacktrackPoint
  ) where

import Prelude hiding (repeat)
import Control.Monad
import qualified Data.Foldable as F
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.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
#if !MIN_VERSION_base(4,11,0)
import Data.Monoid
#endif
import qualified Data.Vector.Generic as VG
import qualified Data.Vector.Unboxed as VU
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import ToySolver.Data.BoolExpr
import ToySolver.Data.Boolean
import ToySolver.Data.OrdRel
import qualified ToySolver.Internal.Data.SeqQueue as SQ
import qualified ToySolver.Internal.Data.Vec as Vec
import qualified ToySolver.SAT as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin

import ToySolver.BitVector.Base

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

data Solver
  = Solver
  { Solver -> Vec (Vector Int)
svVars :: Vec.Vec (VU.Vector SAT.Lit)
  , Solver -> Solver
svSATSolver :: SAT.Solver
  , Solver -> Encoder IO
svTseitin :: Tseitin.Encoder IO
  , Solver -> IORef (Map Expr (Vector Int))
svEncTable :: IORef (Map Expr (VU.Vector SAT.Lit))
  , Solver -> IORef [(Vector Int, Vector Int, Vector Int, Vector Int)]
svDivRemTable :: IORef [(VU.Vector SAT.Lit, VU.Vector SAT.Lit, VU.Vector SAT.Lit, VU.Vector SAT.Lit)]
  , Solver -> IORef (Map NormalizedAtom Int)
svAtomTable :: IORef (Map NormalizedAtom SAT.Lit)
  , Solver -> Vec (IntMap (Maybe Int))
svContexts :: Vec.Vec (IntMap (Maybe Int))
  }

newSolver :: IO Solver
newSolver :: IO Solver
newSolver = do
  Vec (Vector Int)
vars <- IO (Vec (Vector Int))
forall (a :: * -> * -> *) e. MArray a e IO => IO (GenericVec a e)
Vec.new
  Solver
sat <- IO Solver
SAT.newSolver
  Encoder IO
tseitin <- Solver -> IO (Encoder IO)
forall (m :: * -> *) a.
(PrimMonad m, AddClause m a) =>
a -> m (Encoder m)
Tseitin.newEncoder Solver
sat
  IORef (Map Expr (Vector Int))
table <- Map Expr (Vector Int) -> IO (IORef (Map Expr (Vector Int)))
forall a. a -> IO (IORef a)
newIORef Map Expr (Vector Int)
forall k a. Map k a
Map.empty
  IORef [(Vector Int, Vector Int, Vector Int, Vector Int)]
divRemTable <- [(Vector Int, Vector Int, Vector Int, Vector Int)]
-> IO (IORef [(Vector Int, Vector Int, Vector Int, Vector Int)])
forall a. a -> IO (IORef a)
newIORef []
  IORef (Map NormalizedAtom Int)
atomTable <- Map NormalizedAtom Int -> IO (IORef (Map NormalizedAtom Int))
forall a. a -> IO (IORef a)
newIORef Map NormalizedAtom Int
forall k a. Map k a
Map.empty
  Vec (IntMap (Maybe Int))
contexts <- IO (Vec (IntMap (Maybe Int)))
forall (a :: * -> * -> *) e. MArray a e IO => IO (GenericVec a e)
Vec.new
  Vec (IntMap (Maybe Int)) -> IntMap (Maybe Int) -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push Vec (IntMap (Maybe Int))
contexts IntMap (Maybe Int)
forall a. IntMap a
IntMap.empty
  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 :: Vec (Vector Int)
-> Solver
-> Encoder IO
-> IORef (Map Expr (Vector Int))
-> IORef [(Vector Int, Vector Int, Vector Int, Vector Int)]
-> IORef (Map NormalizedAtom Int)
-> Vec (IntMap (Maybe Int))
-> Solver
Solver
    { svVars :: Vec (Vector Int)
svVars = Vec (Vector Int)
vars
    , svSATSolver :: Solver
svSATSolver = Solver
sat
    , svTseitin :: Encoder IO
svTseitin = Encoder IO
tseitin
    , svEncTable :: IORef (Map Expr (Vector Int))
svEncTable = IORef (Map Expr (Vector Int))
table
    , svDivRemTable :: IORef [(Vector Int, Vector Int, Vector Int, Vector Int)]
svDivRemTable = IORef [(Vector Int, Vector Int, Vector Int, Vector Int)]
divRemTable
    , svAtomTable :: IORef (Map NormalizedAtom Int)
svAtomTable = IORef (Map NormalizedAtom Int)
atomTable
    , svContexts :: Vec (IntMap (Maybe Int))
svContexts = Vec (IntMap (Maybe Int))
contexts
    }

newVar :: Solver -> Int -> IO Expr
newVar :: Solver -> Int -> IO Expr
newVar Solver
solver Int
w = Var -> Expr
EVar (Var -> Expr) -> IO Var -> IO Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver -> Int -> IO Var
newVar' Solver
solver Int
w

newVar' :: Solver -> Int -> IO Var
newVar' :: Solver -> Int -> IO Var
newVar' Solver
solver Int
w = do
  Vector Int
bs <- [Int] -> Vector Int
forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList ([Int] -> Vector Int) -> IO [Int] -> IO (Vector Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver -> Int -> IO [Int]
forall (m :: * -> *) a. NewVar m a => a -> Int -> m [Int]
SAT.newVars (Solver -> Solver
svSATSolver Solver
solver) Int
w
  Int
v <- Vec (Vector Int) -> IO Int
forall (a :: * -> * -> *) e. GenericVec a e -> IO Int
Vec.getSize (Vec (Vector Int) -> IO Int) -> Vec (Vector Int) -> IO Int
forall a b. (a -> b) -> a -> b
$ Solver -> Vec (Vector Int)
svVars Solver
solver
  Vec (Vector Int) -> Vector Int -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> Vec (Vector Int)
svVars Solver
solver) Vector Int
bs
  Var -> IO Var
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> IO Var) -> Var -> IO Var
forall a b. (a -> b) -> a -> b
$ Var :: Int -> Int -> Var
Var{ varWidth :: Int
varWidth = Int
w, varId :: Int
varId = Int
v }

data NormalizedRel = NRSLt | NRULt | NREql
  deriving (NormalizedRel -> NormalizedRel -> Bool
(NormalizedRel -> NormalizedRel -> Bool)
-> (NormalizedRel -> NormalizedRel -> Bool) -> Eq NormalizedRel
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NormalizedRel -> NormalizedRel -> Bool
$c/= :: NormalizedRel -> NormalizedRel -> Bool
== :: NormalizedRel -> NormalizedRel -> Bool
$c== :: NormalizedRel -> NormalizedRel -> Bool
Eq, Eq NormalizedRel
Eq NormalizedRel
-> (NormalizedRel -> NormalizedRel -> Ordering)
-> (NormalizedRel -> NormalizedRel -> Bool)
-> (NormalizedRel -> NormalizedRel -> Bool)
-> (NormalizedRel -> NormalizedRel -> Bool)
-> (NormalizedRel -> NormalizedRel -> Bool)
-> (NormalizedRel -> NormalizedRel -> NormalizedRel)
-> (NormalizedRel -> NormalizedRel -> NormalizedRel)
-> Ord NormalizedRel
NormalizedRel -> NormalizedRel -> Bool
NormalizedRel -> NormalizedRel -> Ordering
NormalizedRel -> NormalizedRel -> NormalizedRel
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 :: NormalizedRel -> NormalizedRel -> NormalizedRel
$cmin :: NormalizedRel -> NormalizedRel -> NormalizedRel
max :: NormalizedRel -> NormalizedRel -> NormalizedRel
$cmax :: NormalizedRel -> NormalizedRel -> NormalizedRel
>= :: NormalizedRel -> NormalizedRel -> Bool
$c>= :: NormalizedRel -> NormalizedRel -> Bool
> :: NormalizedRel -> NormalizedRel -> Bool
$c> :: NormalizedRel -> NormalizedRel -> Bool
<= :: NormalizedRel -> NormalizedRel -> Bool
$c<= :: NormalizedRel -> NormalizedRel -> Bool
< :: NormalizedRel -> NormalizedRel -> Bool
$c< :: NormalizedRel -> NormalizedRel -> Bool
compare :: NormalizedRel -> NormalizedRel -> Ordering
$ccompare :: NormalizedRel -> NormalizedRel -> Ordering
$cp1Ord :: Eq NormalizedRel
Ord, Int -> NormalizedRel
NormalizedRel -> Int
NormalizedRel -> [NormalizedRel]
NormalizedRel -> NormalizedRel
NormalizedRel -> NormalizedRel -> [NormalizedRel]
NormalizedRel -> NormalizedRel -> NormalizedRel -> [NormalizedRel]
(NormalizedRel -> NormalizedRel)
-> (NormalizedRel -> NormalizedRel)
-> (Int -> NormalizedRel)
-> (NormalizedRel -> Int)
-> (NormalizedRel -> [NormalizedRel])
-> (NormalizedRel -> NormalizedRel -> [NormalizedRel])
-> (NormalizedRel -> NormalizedRel -> [NormalizedRel])
-> (NormalizedRel
    -> NormalizedRel -> NormalizedRel -> [NormalizedRel])
-> Enum NormalizedRel
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 :: NormalizedRel -> NormalizedRel -> NormalizedRel -> [NormalizedRel]
$cenumFromThenTo :: NormalizedRel -> NormalizedRel -> NormalizedRel -> [NormalizedRel]
enumFromTo :: NormalizedRel -> NormalizedRel -> [NormalizedRel]
$cenumFromTo :: NormalizedRel -> NormalizedRel -> [NormalizedRel]
enumFromThen :: NormalizedRel -> NormalizedRel -> [NormalizedRel]
$cenumFromThen :: NormalizedRel -> NormalizedRel -> [NormalizedRel]
enumFrom :: NormalizedRel -> [NormalizedRel]
$cenumFrom :: NormalizedRel -> [NormalizedRel]
fromEnum :: NormalizedRel -> Int
$cfromEnum :: NormalizedRel -> Int
toEnum :: Int -> NormalizedRel
$ctoEnum :: Int -> NormalizedRel
pred :: NormalizedRel -> NormalizedRel
$cpred :: NormalizedRel -> NormalizedRel
succ :: NormalizedRel -> NormalizedRel
$csucc :: NormalizedRel -> NormalizedRel
Enum, NormalizedRel
NormalizedRel -> NormalizedRel -> Bounded NormalizedRel
forall a. a -> a -> Bounded a
maxBound :: NormalizedRel
$cmaxBound :: NormalizedRel
minBound :: NormalizedRel
$cminBound :: NormalizedRel
Bounded, Int -> NormalizedRel -> ShowS
[NormalizedRel] -> ShowS
NormalizedRel -> String
(Int -> NormalizedRel -> ShowS)
-> (NormalizedRel -> String)
-> ([NormalizedRel] -> ShowS)
-> Show NormalizedRel
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NormalizedRel] -> ShowS
$cshowList :: [NormalizedRel] -> ShowS
show :: NormalizedRel -> String
$cshow :: NormalizedRel -> String
showsPrec :: Int -> NormalizedRel -> ShowS
$cshowsPrec :: Int -> NormalizedRel -> ShowS
Show)

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

normalizeAtom :: Atom -> (NormalizedAtom, Bool)
normalizeAtom :: Atom -> (NormalizedAtom, Bool)
normalizeAtom (Rel (OrdRel Expr
lhs RelOp
op Expr
rhs) Bool
True) =
  case RelOp
op of
    RelOp
Lt -> (NormalizedRel -> Expr -> Expr -> NormalizedAtom
NormalizedAtom NormalizedRel
NRSLt Expr
lhs Expr
rhs, Bool
True)
    RelOp
Gt -> (NormalizedRel -> Expr -> Expr -> NormalizedAtom
NormalizedAtom NormalizedRel
NRSLt Expr
rhs Expr
lhs, Bool
True)
    RelOp
Le -> (NormalizedRel -> Expr -> Expr -> NormalizedAtom
NormalizedAtom NormalizedRel
NRSLt Expr
rhs Expr
lhs, Bool
False)
    RelOp
Ge -> (NormalizedRel -> Expr -> Expr -> NormalizedAtom
NormalizedAtom NormalizedRel
NRSLt Expr
lhs Expr
rhs, Bool
False)
    RelOp
Eql -> (NormalizedRel -> Expr -> Expr -> NormalizedAtom
NormalizedAtom NormalizedRel
NREql Expr
lhs Expr
rhs, Bool
True)
    RelOp
NEq -> (NormalizedRel -> Expr -> Expr -> NormalizedAtom
NormalizedAtom NormalizedRel
NREql Expr
lhs Expr
rhs, Bool
False)
normalizeAtom (Rel (OrdRel Expr
lhs RelOp
op Expr
rhs) Bool
False) =
  case RelOp
op of
    RelOp
Lt -> (NormalizedRel -> Expr -> Expr -> NormalizedAtom
NormalizedAtom NormalizedRel
NRULt Expr
lhs Expr
rhs, Bool
True)
    RelOp
Gt -> (NormalizedRel -> Expr -> Expr -> NormalizedAtom
NormalizedAtom NormalizedRel
NRULt Expr
rhs Expr
lhs, Bool
True)
    RelOp
Le -> (NormalizedRel -> Expr -> Expr -> NormalizedAtom
NormalizedAtom NormalizedRel
NRULt Expr
rhs Expr
lhs, Bool
False)
    RelOp
Ge -> (NormalizedRel -> Expr -> Expr -> NormalizedAtom
NormalizedAtom NormalizedRel
NRULt Expr
lhs Expr
rhs, Bool
False)
    RelOp
Eql -> (NormalizedRel -> Expr -> Expr -> NormalizedAtom
NormalizedAtom NormalizedRel
NREql Expr
lhs Expr
rhs, Bool
True)
    RelOp
NEq -> (NormalizedRel -> Expr -> Expr -> NormalizedAtom
NormalizedAtom NormalizedRel
NREql Expr
lhs Expr
rhs, Bool
False)

assertAtom :: Solver -> Atom -> Maybe Int -> IO ()
assertAtom :: Solver -> Atom -> Maybe Int -> IO ()
assertAtom Solver
solver Atom
atom Maybe Int
label = do
  let (atom' :: NormalizedAtom
atom'@(NormalizedAtom NormalizedRel
op Expr
lhs Expr
rhs), Bool
polarity) = Atom -> (NormalizedAtom, Bool)
normalizeAtom Atom
atom
  Map NormalizedAtom Int
table <- IORef (Map NormalizedAtom Int) -> IO (Map NormalizedAtom Int)
forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map NormalizedAtom Int)
svAtomTable Solver
solver)
  Int
l <- (if Bool
polarity then Int -> Int
forall a. a -> a
id else Int -> Int
forall a. Num a => a -> a
negate) (Int -> Int) -> IO Int -> IO Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    case NormalizedAtom -> Map NormalizedAtom Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup NormalizedAtom
atom' Map NormalizedAtom Int
table of
      Just Int
lit -> Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
lit
      Maybe Int
Nothing -> do
        Vector Int
s <- Solver -> Expr -> IO (Vector Int)
encodeExpr Solver
solver Expr
lhs
        Vector Int
t <- Solver -> Expr -> IO (Vector Int)
encodeExpr Solver
solver Expr
rhs
        Int
l <- Encoder IO -> Formula -> IO Int
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Int
Tseitin.encodeFormula (Solver -> Encoder IO
svTseitin Solver
solver) (Formula -> IO Int) -> Formula -> IO Int
forall a b. (a -> b) -> a -> b
$
          case NormalizedRel
op of
            NormalizedRel
NRULt -> Vector Int -> Vector Int -> Formula
isULT Vector Int
s Vector Int
t
            NormalizedRel
NRSLt -> Vector Int -> Vector Int -> Formula
isSLT Vector Int
s Vector Int
t
            NormalizedRel
NREql -> Vector Int -> Vector Int -> Formula
isEQ Vector Int
s Vector Int
t
        IORef (Map NormalizedAtom Int) -> Map NormalizedAtom Int -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (Map NormalizedAtom Int)
svAtomTable Solver
solver) (Map NormalizedAtom Int -> IO ())
-> Map NormalizedAtom Int -> IO ()
forall a b. (a -> b) -> a -> b
$ NormalizedAtom
-> Int -> Map NormalizedAtom Int -> Map NormalizedAtom Int
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert NormalizedAtom
atom' Int
l Map NormalizedAtom Int
table
        Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
l
  Int
size <- Vec (IntMap (Maybe Int)) -> IO Int
forall (a :: * -> * -> *) e. GenericVec a e -> IO Int
Vec.getSize (Solver -> Vec (IntMap (Maybe Int))
svContexts Solver
solver)
  case Maybe Int
label of
    Maybe Int
Nothing | Int
size Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 -> Encoder IO -> [Int] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause (Solver -> Encoder IO
svTseitin Solver
solver) [Int
l]
    Maybe Int
_ -> do
      Vec (IntMap (Maybe Int))
-> Int -> (IntMap (Maybe Int) -> IntMap (Maybe Int)) -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Int -> (e -> e) -> IO ()
Vec.modify (Solver -> Vec (IntMap (Maybe Int))
svContexts Solver
solver) (Int
size Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Int -> Maybe Int -> IntMap (Maybe Int) -> IntMap (Maybe Int)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
l Maybe Int
label)

check :: Solver -> IO Bool
check :: Solver -> IO Bool
check Solver
solver = do
  Int
size <- Vec (IntMap (Maybe Int)) -> IO Int
forall (a :: * -> * -> *) e. GenericVec a e -> IO Int
Vec.getSize (Solver -> Vec (IntMap (Maybe Int))
svContexts Solver
solver)
  IntMap (Maybe Int)
m <- Vec (IntMap (Maybe Int)) -> Int -> IO (IntMap (Maybe Int))
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Int -> IO e
Vec.read (Solver -> Vec (IntMap (Maybe Int))
svContexts Solver
solver) (Int
size Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
  Bool
b <- Solver -> [Int] -> IO Bool
SAT.solveWith (Solver -> Solver
svSATSolver Solver
solver) (IntMap (Maybe Int) -> [Int]
forall a. IntMap a -> [Int]
IntMap.keys IntMap (Maybe Int)
m)
  Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
b

getModel :: Solver -> IO Model
getModel :: Solver -> IO Model
getModel Solver
solver = do
  Model
m <- Solver -> IO Model
SAT.getModel (Solver -> Solver
svSATSolver Solver
solver)
  [Vector Int]
vss <- Vec (Vector Int) -> IO [Vector Int]
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO [e]
Vec.getElems (Solver -> Vec (Vector Int)
svVars Solver
solver)
  let f :: Vector Int -> BV
f = [Bool] -> BV
forall a. IsBV a => [Bool] -> a
fromAscBits ([Bool] -> BV) -> (Vector Int -> [Bool]) -> Vector Int -> BV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Bool) -> [Int] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Model -> Int -> Bool
forall m. IModel m => m -> Int -> Bool
SAT.evalLit Model
m) ([Int] -> [Bool]) -> (Vector Int -> [Int]) -> Vector Int -> [Bool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector Int -> [Int]
forall (v :: * -> *) a. Vector v a => v a -> [a]
VG.toList
      isZero' :: BV -> Bool
isZero' = Bool -> Bool
not (Bool -> Bool) -> (BV -> Bool) -> BV -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ([Bool] -> Bool) -> (BV -> [Bool]) -> BV -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV -> [Bool]
toAscBits
      env :: Vector BV
env = [BV] -> Vector BV
forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList [Vector Int -> BV
f Vector Int
vs | Vector Int
vs <- [Vector Int]
vss]
  [(Vector Int, Vector Int, Vector Int, Vector Int)]
xs <- IORef [(Vector Int, Vector Int, Vector Int, Vector Int)]
-> IO [(Vector Int, Vector Int, Vector Int, Vector Int)]
forall a. IORef a -> IO a
readIORef (Solver -> IORef [(Vector Int, Vector Int, Vector Int, Vector Int)]
svDivRemTable Solver
solver)
  let divTable :: Map BV BV
divTable = [(BV, BV)] -> Map BV BV
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Vector Int -> BV
f Vector Int
s, Vector Int -> BV
f Vector Int
d) | (Vector Int
s,Vector Int
t,Vector Int
d,Vector Int
_r) <- [(Vector Int, Vector Int, Vector Int, Vector Int)]
xs, BV -> Bool
isZero' (Vector Int -> BV
f Vector Int
t)]
      remTable :: Map BV BV
remTable = [(BV, BV)] -> Map BV BV
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Vector Int -> BV
f Vector Int
s, Vector Int -> BV
f Vector Int
r) | (Vector Int
s,Vector Int
t,Vector Int
_d,Vector Int
r) <- [(Vector Int, Vector Int, Vector Int, Vector Int)]
xs, BV -> Bool
isZero' (Vector Int -> BV
f Vector Int
t)]
  Model -> IO Model
forall (m :: * -> *) a. Monad m => a -> m a
return (Vector BV
env, Map BV BV
divTable, Map BV BV
remTable)

explain :: Solver -> IO IntSet
explain :: Solver -> IO IntSet
explain Solver
solver = do
  IntSet
xs <- Solver -> IO IntSet
SAT.getFailedAssumptions (Solver -> Solver
svSATSolver Solver
solver)
  Int
size <- Vec (IntMap (Maybe Int)) -> IO Int
forall (a :: * -> * -> *) e. GenericVec a e -> IO Int
Vec.getSize (Solver -> Vec (IntMap (Maybe Int))
svContexts Solver
solver)
  IntMap (Maybe Int)
m <- Vec (IntMap (Maybe Int)) -> Int -> IO (IntMap (Maybe Int))
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Int -> IO e
Vec.read (Solver -> Vec (IntMap (Maybe Int))
svContexts Solver
solver) (Int
size Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
  IntSet -> IO IntSet
forall (m :: * -> *) a. Monad m => a -> m a
return (IntSet -> IO IntSet) -> IntSet -> IO IntSet
forall a b. (a -> b) -> a -> b
$ [Int] -> IntSet
IntSet.fromList ([Int] -> IntSet) -> [Int] -> IntSet
forall a b. (a -> b) -> a -> b
$ [Maybe Int] -> [Int]
forall a. [Maybe a] -> [a]
catMaybes [IntMap (Maybe Int)
m IntMap (Maybe Int) -> Int -> Maybe Int
forall a. IntMap a -> Int -> a
IntMap.! Int
x | Int
x <- IntSet -> [Int]
IntSet.toList IntSet
xs]

pushBacktrackPoint :: Solver -> IO ()
pushBacktrackPoint :: Solver -> IO ()
pushBacktrackPoint Solver
solver = do
  Int
size <- Vec (IntMap (Maybe Int)) -> IO Int
forall (a :: * -> * -> *) e. GenericVec a e -> IO Int
Vec.getSize (Solver -> Vec (IntMap (Maybe Int))
svContexts Solver
solver)
  IntMap (Maybe Int)
m <- Vec (IntMap (Maybe Int)) -> Int -> IO (IntMap (Maybe Int))
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Int -> IO e
Vec.read (Solver -> Vec (IntMap (Maybe Int))
svContexts Solver
solver) (Int
size Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
  Vec (IntMap (Maybe Int)) -> IntMap (Maybe Int) -> IO ()
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> Vec (IntMap (Maybe Int))
svContexts Solver
solver) IntMap (Maybe Int)
m

popBacktrackPoint :: Solver -> IO ()
popBacktrackPoint :: Solver -> IO ()
popBacktrackPoint Solver
solver = do
  IntMap (Maybe Int)
_ <- Vec (IntMap (Maybe Int)) -> IO (IntMap (Maybe Int))
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO e
Vec.pop (Solver -> Vec (IntMap (Maybe Int))
svContexts Solver
solver)
  () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

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

type SBV = VU.Vector SAT.Lit

encodeExpr :: Solver -> Expr -> IO SBV
encodeExpr :: Solver -> Expr -> IO (Vector Int)
encodeExpr Solver
solver = Expr -> IO (Vector Int)
enc
  where
    enc :: Expr -> IO (Vector Int)
enc e :: Expr
e@(EConst BV
_) = Expr -> IO (Vector Int)
enc' Expr
e
    enc e :: Expr
e@(EVar Var
_) = Expr -> IO (Vector Int)
enc' Expr
e
    enc Expr
e = do
      Map Expr (Vector Int)
table <- IORef (Map Expr (Vector Int)) -> IO (Map Expr (Vector Int))
forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map Expr (Vector Int))
svEncTable Solver
solver)
      case Expr -> Map Expr (Vector Int) -> Maybe (Vector Int)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Expr
e Map Expr (Vector Int)
table of
        Just Vector Int
vs -> Vector Int -> IO (Vector Int)
forall (m :: * -> *) a. Monad m => a -> m a
return Vector Int
vs
        Maybe (Vector Int)
Nothing -> do
          Vector Int
vs <- Expr -> IO (Vector Int)
enc' Expr
e
          IORef (Map Expr (Vector Int))
-> (Map Expr (Vector Int) -> Map Expr (Vector Int)) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef (Solver -> IORef (Map Expr (Vector Int))
svEncTable Solver
solver) (Expr
-> Vector Int -> Map Expr (Vector Int) -> Map Expr (Vector Int)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Expr
e Vector Int
vs)
          Vector Int -> IO (Vector Int)
forall (m :: * -> *) a. Monad m => a -> m a
return Vector Int
vs

    enc' :: Expr -> IO (Vector Int)
enc' (EConst BV
bs) =
      ([Int] -> Vector Int) -> IO [Int] -> IO (Vector Int)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM [Int] -> Vector Int
forall a. Unbox a => [a] -> Vector a
VU.fromList (IO [Int] -> IO (Vector Int)) -> IO [Int] -> IO (Vector Int)
forall a b. (a -> b) -> a -> b
$ [Bool] -> (Bool -> IO Int) -> IO [Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (BV -> [Bool]
toAscBits BV
bs) ((Bool -> IO Int) -> IO [Int]) -> (Bool -> IO Int) -> IO [Int]
forall a b. (a -> b) -> a -> b
$ \Bool
b ->
        if Bool
b
        then Encoder IO -> [Int] -> IO Int
forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeConj (Solver -> Encoder IO
svTseitin Solver
solver) []
        else Encoder IO -> [Int] -> IO Int
forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeDisj (Solver -> Encoder IO
svTseitin Solver
solver) []
    enc' (EVar Var
v) = Vec (Vector Int) -> Int -> IO (Vector Int)
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Int -> IO e
Vec.read (Solver -> Vec (Vector Int)
svVars Solver
solver) (Var -> Int
varId Var
v)
    enc' (EOp1 Op1
op Expr
arg) = do
      Vector Int
arg' <- Expr -> IO (Vector Int)
enc Expr
arg
      case Op1
op of
        OpExtract Int
i Int
j -> do
          Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
arg' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
i Bool -> Bool -> Bool
&& Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
j Bool -> Bool -> Bool
&& Int
j Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
            String -> IO ()
forall a. HasCallStack => String -> a
error (String
"invalid extract " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall a. Show a => a -> String
show (Int
i,Int
j) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" on bit-vector of length " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
arg') String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Expr -> String
forall a. Show a => a -> String
show Expr
arg)
          Vector Int -> IO (Vector Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Vector Int -> IO (Vector Int)) -> Vector Int -> IO (Vector Int)
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Vector Int -> Vector Int
forall (v :: * -> *) a. Vector v a => Int -> Int -> v a -> v a
VG.slice Int
j (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
j Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Vector Int
arg'
        Op1
OpNot -> Vector Int -> IO (Vector Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Vector Int -> IO (Vector Int)) -> Vector Int -> IO (Vector Int)
forall a b. (a -> b) -> a -> b
$ (Int -> Int) -> Vector Int -> Vector Int
forall (v :: * -> *) a b.
(Vector v a, Vector v b) =>
(a -> b) -> v a -> v b
VG.map Int -> Int
forall a. Num a => a -> a
negate Vector Int
arg'
        Op1
OpNeg -> Encoder IO -> Vector Int -> IO (Vector Int)
encodeNegate (Solver -> Encoder IO
svTseitin Solver
solver) Vector Int
arg'
    enc' (EOp2 Op2
op Expr
arg1 Expr
arg2) = do
      Vector Int
arg1' <- Expr -> IO (Vector Int)
enc Expr
arg1
      Vector Int
arg2' <- Expr -> IO (Vector Int)
enc Expr
arg2
      case Op2
op of
        Op2
OpConcat -> Vector Int -> IO (Vector Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Vector Int
arg2' Vector Int -> Vector Int -> Vector Int
forall a. Semigroup a => a -> a -> a
<> Vector Int
arg1')
        Op2
OpAnd -> (Int -> Int -> IO Int)
-> Vector Int -> Vector Int -> IO (Vector Int)
forall (m :: * -> *) (v :: * -> *) a b c.
(Monad m, Vector v a, Vector v b, Vector v c) =>
(a -> b -> m c) -> v a -> v b -> m (v c)
VG.zipWithM (\Int
l1 Int
l2 -> Encoder IO -> [Int] -> IO Int
forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeConj (Solver -> Encoder IO
svTseitin Solver
solver) [Int
l1,Int
l2]) Vector Int
arg1' Vector Int
arg2'
        Op2
OpOr  -> (Int -> Int -> IO Int)
-> Vector Int -> Vector Int -> IO (Vector Int)
forall (m :: * -> *) (v :: * -> *) a b c.
(Monad m, Vector v a, Vector v b, Vector v c) =>
(a -> b -> m c) -> v a -> v b -> m (v c)
VG.zipWithM (\Int
l1 Int
l2 -> Encoder IO -> [Int] -> IO Int
forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeDisj (Solver -> Encoder IO
svTseitin Solver
solver) [Int
l1,Int
l2]) Vector Int
arg1' Vector Int
arg2'
        Op2
OpXOr -> (Int -> Int -> IO Int)
-> Vector Int -> Vector Int -> IO (Vector Int)
forall (m :: * -> *) (v :: * -> *) a b c.
(Monad m, Vector v a, Vector v b, Vector v c) =>
(a -> b -> m c) -> v a -> v b -> m (v c)
VG.zipWithM (Encoder IO -> Int -> Int -> IO Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Int -> Int -> m Int
Tseitin.encodeXOR (Solver -> Encoder IO
svTseitin Solver
solver)) Vector Int
arg1' Vector Int
arg2'
        Op2
OpComp -> Int -> Vector Int
forall (v :: * -> *) a. Vector v a => a -> v a
VG.singleton (Int -> Vector Int) -> IO Int -> IO (Vector Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Encoder IO -> Formula -> IO Int
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Int
Tseitin.encodeFormula (Solver -> Encoder IO
svTseitin Solver
solver) (Vector Int -> Vector Int -> Formula
isEQ Vector Int
arg1' Vector Int
arg2')
        Op2
OpAdd -> Encoder IO -> Int -> Bool -> [Vector Int] -> IO (Vector Int)
encodeSum (Solver -> Encoder IO
svTseitin Solver
solver) (Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
arg1') Bool
True [Vector Int
arg1', Vector Int
arg2']
        Op2
OpMul -> Encoder IO -> Bool -> Vector Int -> Vector Int -> IO (Vector Int)
encodeMul (Solver -> Encoder IO
svTseitin Solver
solver) Bool
True Vector Int
arg1' Vector Int
arg2'
        Op2
OpUDiv -> (Vector Int, Vector Int) -> Vector Int
forall a b. (a, b) -> a
fst ((Vector Int, Vector Int) -> Vector Int)
-> IO (Vector Int, Vector Int) -> IO (Vector Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver -> Vector Int -> Vector Int -> IO (Vector Int, Vector Int)
encodeDivRem Solver
solver Vector Int
arg1' Vector Int
arg2'
        Op2
OpURem -> (Vector Int, Vector Int) -> Vector Int
forall a b. (a, b) -> b
snd ((Vector Int, Vector Int) -> Vector Int)
-> IO (Vector Int, Vector Int) -> IO (Vector Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver -> Vector Int -> Vector Int -> IO (Vector Int, Vector Int)
encodeDivRem Solver
solver Vector Int
arg1' Vector Int
arg2'
        Op2
OpSDiv -> Solver -> Vector Int -> Vector Int -> IO (Vector Int)
encodeSDiv Solver
solver Vector Int
arg1' Vector Int
arg2'
        Op2
OpSRem -> Solver -> Vector Int -> Vector Int -> IO (Vector Int)
encodeSRem Solver
solver Vector Int
arg1' Vector Int
arg2'
        Op2
OpSMod -> Solver -> Vector Int -> Vector Int -> IO (Vector Int)
encodeSMod Solver
solver Vector Int
arg1' Vector Int
arg2'
        Op2
OpShl  -> Encoder IO -> Vector Int -> Vector Int -> IO (Vector Int)
encodeShl (Solver -> Encoder IO
svTseitin Solver
solver) Vector Int
arg1' Vector Int
arg2'
        Op2
OpLShr -> Encoder IO -> Vector Int -> Vector Int -> IO (Vector Int)
encodeLShr (Solver -> Encoder IO
svTseitin Solver
solver) Vector Int
arg1' Vector Int
arg2'
        Op2
OpAShr -> Encoder IO -> Vector Int -> Vector Int -> IO (Vector Int)
encodeAShr (Solver -> Encoder IO
svTseitin Solver
solver) Vector Int
arg1' Vector Int
arg2'

encodeMul :: Tseitin.Encoder IO -> Bool -> SBV -> SBV -> IO SBV
encodeMul :: Encoder IO -> Bool -> Vector Int -> Vector Int -> IO (Vector Int)
encodeMul Encoder IO
enc Bool
allowOverflow Vector Int
arg1 Vector Int
arg2 = do
  let w :: Int
w = Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
arg1
  Int
b0 <- Encoder IO -> [Int] -> IO Int
forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeDisj Encoder IO
enc [] -- False
  [Vector Int]
bss <- [(Int, Int)] -> ((Int, Int) -> IO (Vector Int)) -> IO [Vector Int]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] (Vector Int -> [Int]
forall (v :: * -> *) a. Vector v a => v a -> [a]
VG.toList Vector Int
arg2)) (((Int, Int) -> IO (Vector Int)) -> IO [Vector Int])
-> ((Int, Int) -> IO (Vector Int)) -> IO [Vector Int]
forall a b. (a -> b) -> a -> b
$ \(Int
i,Int
b2) -> do
    let arg1' :: Vector Int
arg1' = if Bool
allowOverflow
                then Int -> Vector Int -> Vector Int
forall (v :: * -> *) a. Vector v a => Int -> v a -> v a
VG.take (Int
w Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i) Vector Int
arg1
                else Vector Int
arg1
    Vector Int
bs <- Vector Int -> (Int -> IO Int) -> IO (Vector Int)
forall (m :: * -> *) (v :: * -> *) a b.
(Monad m, Vector v a, Vector v b) =>
v a -> (a -> m b) -> m (v b)
VG.forM Vector Int
arg1' ((Int -> IO Int) -> IO (Vector Int))
-> (Int -> IO Int) -> IO (Vector Int)
forall a b. (a -> b) -> a -> b
$ \Int
b1 -> do
            Encoder IO -> [Int] -> IO Int
forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeConj Encoder IO
enc [Int
b1,Int
b2]
    Vector Int -> IO (Vector Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Int -> Vector Int
forall (v :: * -> *) a. Vector v a => Int -> a -> v a
VG.replicate Int
i Int
b0 Vector Int -> Vector Int -> Vector Int
forall a. Semigroup a => a -> a -> a
<> Vector Int
bs)
  Encoder IO -> Int -> Bool -> [Vector Int] -> IO (Vector Int)
encodeSum Encoder IO
enc Int
w Bool
allowOverflow [Vector Int]
bss

encodeSum :: Tseitin.Encoder IO -> Int -> Bool -> [SBV] -> IO SBV
encodeSum :: Encoder IO -> Int -> Bool -> [Vector Int] -> IO (Vector Int)
encodeSum Encoder IO
enc Int
w Bool
allowOverflow [Vector Int]
xss = do
  (IORef (Seq (SeqQueue IO Int))
buckets :: IORef (Seq (SQ.SeqQueue IO SAT.Lit))) <- Seq (SeqQueue IO Int) -> IO (IORef (Seq (SeqQueue IO Int)))
forall a. a -> IO (IORef a)
newIORef Seq (SeqQueue IO Int)
forall a. Seq a
Seq.empty
  let insert :: Int -> Int -> IO ()
insert Int
i Int
x = do
        Seq (SeqQueue IO Int)
bs <- IORef (Seq (SeqQueue IO Int)) -> IO (Seq (SeqQueue IO Int))
forall a. IORef a -> IO a
readIORef IORef (Seq (SeqQueue IO Int))
buckets
        let n :: Int
n = Seq (SeqQueue IO Int) -> Int
forall a. Seq a -> Int
Seq.length Seq (SeqQueue IO Int)
bs
        SeqQueue IO Int
q <- if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n then do
               SeqQueue IO Int -> IO (SeqQueue IO Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqQueue IO Int -> IO (SeqQueue IO Int))
-> SeqQueue IO Int -> IO (SeqQueue IO Int)
forall a b. (a -> b) -> a -> b
$ Seq (SeqQueue IO Int) -> Int -> SeqQueue IO Int
forall a. Seq a -> Int -> a
Seq.index Seq (SeqQueue IO Int)
bs Int
i
             else do
               [SeqQueue IO Int]
qs <- Int -> IO (SeqQueue IO Int) -> IO [SeqQueue IO Int]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n) IO (SeqQueue IO Int)
forall q (m :: * -> *). NewFifo q m => m q
SQ.newFifo
               let bs' :: Seq (SeqQueue IO Int)
bs' = Seq (SeqQueue IO Int)
bs Seq (SeqQueue IO Int)
-> Seq (SeqQueue IO Int) -> Seq (SeqQueue IO Int)
forall a. Seq a -> Seq a -> Seq a
Seq.>< [SeqQueue IO Int] -> Seq (SeqQueue IO Int)
forall a. [a] -> Seq a
Seq.fromList [SeqQueue IO Int]
qs
               IORef (Seq (SeqQueue IO Int)) -> Seq (SeqQueue IO Int) -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (Seq (SeqQueue IO Int))
buckets Seq (SeqQueue IO Int)
bs'
               SeqQueue IO Int -> IO (SeqQueue IO Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (SeqQueue IO Int -> IO (SeqQueue IO Int))
-> SeqQueue IO Int -> IO (SeqQueue IO Int)
forall a b. (a -> b) -> a -> b
$ Seq (SeqQueue IO Int) -> Int -> SeqQueue IO Int
forall a. Seq a -> Int -> a
Seq.index Seq (SeqQueue IO Int)
bs' Int
i
        SeqQueue IO Int -> Int -> IO ()
forall q (m :: * -> *) a. Enqueue q m a => q -> a -> m ()
SQ.enqueue SeqQueue IO Int
q Int
x

  [Vector Int] -> (Vector Int -> IO (Vector ())) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Vector Int]
xss ((Vector Int -> IO (Vector ())) -> IO ())
-> (Vector Int -> IO (Vector ())) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Vector Int
xs -> do
    (Int -> Int -> IO ()) -> Vector Int -> IO (Vector ())
forall (m :: * -> *) (v :: * -> *) a b.
(Monad m, Vector v a, Vector v b) =>
(Int -> a -> m b) -> v a -> m (v b)
VG.imapM Int -> Int -> IO ()
insert Vector Int
xs

  let loop :: Int -> [Int] -> IO [Int]
loop Int
i [Int]
ret
        | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
w = do
            Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
allowOverflow (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
              Seq (SeqQueue IO Int)
bs <- IORef (Seq (SeqQueue IO Int)) -> IO (Seq (SeqQueue IO Int))
forall a. IORef a -> IO a
readIORef IORef (Seq (SeqQueue IO Int))
buckets
              [SeqQueue IO Int] -> (SeqQueue IO Int -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (Seq (SeqQueue IO Int) -> [SeqQueue IO Int]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (SeqQueue IO Int)
bs) ((SeqQueue IO Int -> IO ()) -> IO ())
-> (SeqQueue IO Int -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \SeqQueue IO Int
q -> do
                [Int]
ls <- SeqQueue IO Int -> IO [Int]
forall q (m :: * -> *) a. Dequeue q m a => q -> m [a]
SQ.dequeueBatch SeqQueue IO Int
q
                [Int] -> (Int -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int]
ls ((Int -> IO ()) -> IO ()) -> (Int -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Int
l -> do
                  Encoder IO -> [Int] -> IO ()
forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause  Encoder IO
enc [-Int
l]
            [Int] -> IO [Int]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Int] -> [Int]
forall a. [a] -> [a]
reverse [Int]
ret)
        | Bool
otherwise = do
            Seq (SeqQueue IO Int)
bs <- IORef (Seq (SeqQueue IO Int)) -> IO (Seq (SeqQueue IO Int))
forall a. IORef a -> IO a
readIORef IORef (Seq (SeqQueue IO Int))
buckets
            let n :: Int
n = Seq (SeqQueue IO Int) -> Int
forall a. Seq a -> Int
Seq.length Seq (SeqQueue IO Int)
bs
            if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
n then do
              Int
b <- Encoder IO -> [Int] -> IO Int
forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeDisj Encoder IO
enc [] -- False
              Int -> [Int] -> IO [Int]
loop (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Int
b Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
ret)
            else do
              let q :: SeqQueue IO Int
q = Seq (SeqQueue IO Int) -> Int -> SeqQueue IO Int
forall a. Seq a -> Int -> a
Seq.index Seq (SeqQueue IO Int)
bs Int
i
              Int
m <- SeqQueue IO Int -> IO Int
forall q (m :: * -> *). QueueSize q m => q -> m Int
SQ.queueSize SeqQueue IO Int
q
              case Int
m of
                Int
0 -> do
                  Int
b <- Encoder IO -> [Int] -> IO Int
forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeDisj Encoder IO
enc [] -- False
                  Int -> [Int] -> IO [Int]
loop (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Int
b Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
ret)
                Int
1 -> do
                  Just Int
b <- SeqQueue IO Int -> IO (Maybe Int)
forall q (m :: * -> *) a. Dequeue q m a => q -> m (Maybe a)
SQ.dequeue SeqQueue IO Int
q
                  Int -> [Int] -> IO [Int]
loop (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Int
b Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
ret)
                Int
2 -> do
                  Just Int
b1 <- SeqQueue IO Int -> IO (Maybe Int)
forall q (m :: * -> *) a. Dequeue q m a => q -> m (Maybe a)
SQ.dequeue SeqQueue IO Int
q
                  Just Int
b2 <- SeqQueue IO Int -> IO (Maybe Int)
forall q (m :: * -> *) a. Dequeue q m a => q -> m (Maybe a)
SQ.dequeue SeqQueue IO Int
q
                  Int
s <- Encoder IO -> Int -> Int -> IO Int
encodeHASum Encoder IO
enc Int
b1 Int
b2
                  Int
c <- Encoder IO -> Int -> Int -> IO Int
encodeHACarry Encoder IO
enc Int
b1 Int
b2
                  Int -> Int -> IO ()
insert (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int
c
                  Int -> [Int] -> IO [Int]
loop (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Int
s Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
ret)
                Int
_ -> do
                  Just Int
b1 <- SeqQueue IO Int -> IO (Maybe Int)
forall q (m :: * -> *) a. Dequeue q m a => q -> m (Maybe a)
SQ.dequeue SeqQueue IO Int
q
                  Just Int
b2 <- SeqQueue IO Int -> IO (Maybe Int)
forall q (m :: * -> *) a. Dequeue q m a => q -> m (Maybe a)
SQ.dequeue SeqQueue IO Int
q
                  Just Int
b3 <- SeqQueue IO Int -> IO (Maybe Int)
forall q (m :: * -> *) a. Dequeue q m a => q -> m (Maybe a)
SQ.dequeue SeqQueue IO Int
q
                  Int
s <- Encoder IO -> Int -> Int -> Int -> IO Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Int -> Int -> Int -> m Int
Tseitin.encodeFASum Encoder IO
enc Int
b1 Int
b2 Int
b3
                  Int
c <- Encoder IO -> Int -> Int -> Int -> IO Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Int -> Int -> Int -> m Int
Tseitin.encodeFACarry Encoder IO
enc Int
b1 Int
b2 Int
b3
                  Int -> Int -> IO ()
insert Int
i Int
s
                  Int -> Int -> IO ()
insert (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Int
c
                  Int -> [Int] -> IO [Int]
loop Int
i [Int]
ret
  [Int] -> Vector Int
forall a. Unbox a => [a] -> Vector a
VU.fromList ([Int] -> Vector Int) -> IO [Int] -> IO (Vector Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> [Int] -> IO [Int]
loop Int
0 []

encodeHASum :: Tseitin.Encoder IO -> SAT.Lit -> SAT.Lit -> IO SAT.Lit
encodeHASum :: Encoder IO -> Int -> Int -> IO Int
encodeHASum = Encoder IO -> Int -> Int -> IO Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Int -> Int -> m Int
Tseitin.encodeXOR

encodeHACarry :: Tseitin.Encoder IO -> SAT.Lit -> SAT.Lit -> IO SAT.Lit
encodeHACarry :: Encoder IO -> Int -> Int -> IO Int
encodeHACarry Encoder IO
enc Int
a Int
b = Encoder IO -> [Int] -> IO Int
forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeConj Encoder IO
enc [Int
a,Int
b]

encodeNegate :: Tseitin.Encoder IO -> SBV -> IO SBV
encodeNegate :: Encoder IO -> Vector Int -> IO (Vector Int)
encodeNegate Encoder IO
enc Vector Int
s = do
  let f :: Int -> [Int] -> [Int] -> IO (Vector Int)
f Int
_ [] [Int]
ret = Vector Int -> IO (Vector Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Vector Int -> IO (Vector Int)) -> Vector Int -> IO (Vector Int)
forall a b. (a -> b) -> a -> b
$ [Int] -> Vector Int
forall a. Unbox a => [a] -> Vector a
VU.fromList ([Int] -> Vector Int) -> [Int] -> Vector Int
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int]
forall a. [a] -> [a]
reverse [Int]
ret
      f Int
b (Int
x:[Int]
xs) [Int]
ret = do
        Int
y <- Encoder IO -> Int -> Int -> Int -> IO Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Int -> Int -> Int -> m Int
Tseitin.encodeITE Encoder IO
enc Int
b (- Int
x) Int
x
        Int
b' <- Encoder IO -> [Int] -> IO Int
forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeDisj Encoder IO
enc [Int
b, Int
x]
        Int -> [Int] -> [Int] -> IO (Vector Int)
f Int
b' [Int]
xs (Int
y Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
ret)
  Int
b0 <- Encoder IO -> [Int] -> IO Int
forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeDisj Encoder IO
enc []
  Int -> [Int] -> [Int] -> IO (Vector Int)
f Int
b0 (Vector Int -> [Int]
forall (v :: * -> *) a. Vector v a => v a -> [a]
VG.toList Vector Int
s) []

encodeAbs :: Tseitin.Encoder IO -> SBV -> IO SBV
encodeAbs :: Encoder IO -> Vector Int -> IO (Vector Int)
encodeAbs Encoder IO
enc Vector Int
s = do
  let w :: Int
w = Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
s
  if Int
w Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then
    Vector Int -> IO (Vector Int)
forall (m :: * -> *) a. Monad m => a -> m a
return Vector Int
forall (v :: * -> *) a. Vector v a => v a
VG.empty
  else do
    let msb_s :: Int
msb_s = Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> a
VG.last Vector Int
s
    Vector Int
r <- [Int] -> Vector Int
forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList ([Int] -> Vector Int) -> IO [Int] -> IO (Vector Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Encoder IO -> Int -> IO [Int]
forall (m :: * -> *) a. NewVar m a => a -> Int -> m [Int]
SAT.newVars Encoder IO
enc Int
w
    Vector Int
t <- Encoder IO -> Vector Int -> IO (Vector Int)
encodeNegate Encoder IO
enc Vector Int
s
    Encoder IO -> Formula -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula Encoder IO
enc (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 (Int -> Formula
forall a. a -> BoolExpr a
Atom (-Int
msb_s)) (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
s) (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
t)
    Vector Int -> IO (Vector Int)
forall (m :: * -> *) a. Monad m => a -> m a
return Vector Int
r

encodeShl :: Tseitin.Encoder IO -> SBV -> SBV -> IO SBV
encodeShl :: Encoder IO -> Vector Int -> Vector Int -> IO (Vector Int)
encodeShl Encoder IO
enc Vector Int
s Vector Int
t = do
  let w :: Int
w = Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
s
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
w Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
t) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
forall a. HasCallStack => String -> a
error String
"invalid width"
  Int
b0 <- Encoder IO -> [Int] -> IO Int
forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeDisj Encoder IO
enc [] -- False
  let go :: v Int -> (a, Int) -> IO (v Int)
go v Int
bs (a
i,Int
b) =
        Int -> (Int -> IO Int) -> IO (v Int)
forall (m :: * -> *) (v :: * -> *) a.
(Monad m, Vector v a) =>
Int -> (Int -> m a) -> m (v a)
VG.generateM Int
w ((Int -> IO Int) -> IO (v Int)) -> (Int -> IO Int) -> IO (v Int)
forall a b. (a -> b) -> a -> b
$ \Int
j -> do
          let k :: Integer
k = Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
j Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
2Integer -> a -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^a
i
              t :: Int
t = if Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 then v Int
bs v Int -> Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int -> a
VG.! Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
k else Int
b0
              e :: Int
e = v Int
bs v Int -> Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int -> a
VG.! Int
j
          Encoder IO -> Int -> Int -> Int -> IO Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Int -> Int -> Int -> m Int
Tseitin.encodeITE Encoder IO
enc Int
b Int
t Int
e
  (Vector Int -> (Int, Int) -> IO (Vector Int))
-> Vector Int -> [(Int, Int)] -> IO (Vector Int)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Vector Int -> (Int, Int) -> IO (Vector Int)
forall (v :: * -> *) (v :: * -> *) a.
(Vector v Int, Integral a, Vector v Int) =>
v Int -> (a, Int) -> IO (v Int)
go Vector Int
s ([Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Int
0::Int)..] (Vector Int -> [Int]
forall (v :: * -> *) a. Vector v a => v a -> [a]
VG.toList Vector Int
t))

encodeLShr :: Tseitin.Encoder IO -> SBV -> SBV -> IO SBV
encodeLShr :: Encoder IO -> Vector Int -> Vector Int -> IO (Vector Int)
encodeLShr Encoder IO
enc Vector Int
s Vector Int
t = do
  let w :: Int
w = Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
s
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
w Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
t) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
forall a. HasCallStack => String -> a
error String
"invalid width"
  Int
b0 <- Encoder IO -> [Int] -> IO Int
forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeDisj Encoder IO
enc [] -- False
  let go :: v Int -> (a, Int) -> IO (v Int)
go v Int
bs (a
i,Int
b) =
        Int -> (Int -> IO Int) -> IO (v Int)
forall (m :: * -> *) (v :: * -> *) a.
(Monad m, Vector v a) =>
Int -> (Int -> m a) -> m (v a)
VG.generateM Int
w ((Int -> IO Int) -> IO (v Int)) -> (Int -> IO Int) -> IO (v Int)
forall a b. (a -> b) -> a -> b
$ \Int
j -> do
          let k :: Integer
k = Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
j Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
2Integer -> a -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^a
i
              t :: Int
t = if Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (v Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length v Int
bs) then v Int
bs v Int -> Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int -> a
VG.! Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
k else Int
b0
              e :: Int
e = v Int
bs v Int -> Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int -> a
VG.! Int
j
          Encoder IO -> Int -> Int -> Int -> IO Int
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Int -> Int -> Int -> m Int
Tseitin.encodeITE Encoder IO
enc Int
b Int
t Int
e
  (Vector Int -> (Int, Int) -> IO (Vector Int))
-> Vector Int -> [(Int, Int)] -> IO (Vector Int)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Vector Int -> (Int, Int) -> IO (Vector Int)
forall (v :: * -> *) (v :: * -> *) a.
(Vector v Int, Integral a, Vector v Int) =>
v Int -> (a, Int) -> IO (v Int)
go Vector Int
s ([Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Int
0::Int)..] (Vector Int -> [Int]
forall (v :: * -> *) a. Vector v a => v a -> [a]
VG.toList Vector Int
t))

encodeAShr :: Tseitin.Encoder IO -> SBV -> SBV -> IO SBV
encodeAShr :: Encoder IO -> Vector Int -> Vector Int -> IO (Vector Int)
encodeAShr Encoder IO
enc Vector Int
s Vector Int
t = do
  let w :: Int
w = Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
s
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
w Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
t) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
forall a. HasCallStack => String -> a
error String
"invalid width"
  if Int
w Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then
    Vector Int -> IO (Vector Int)
forall (m :: * -> *) a. Monad m => a -> m a
return Vector Int
forall (v :: * -> *) a. Vector v a => v a
VG.empty
  else do
    let msb_s :: Int
msb_s = Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> a
VG.last Vector Int
s
    Vector Int
r <- [Int] -> Vector Int
forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList ([Int] -> Vector Int) -> IO [Int] -> IO (Vector Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Encoder IO -> Int -> IO [Int]
forall (m :: * -> *) a. NewVar m a => a -> Int -> m [Int]
SAT.newVars Encoder IO
enc Int
w
    Vector Int
s' <- Encoder IO -> Vector Int -> IO (Vector Int)
encodeNegate Encoder IO
enc Vector Int
s
    Vector Int
a <- Encoder IO -> Vector Int -> Vector Int -> IO (Vector Int)
encodeLShr Encoder IO
enc Vector Int
s Vector Int
t
    Vector Int
b <- Encoder IO -> Vector Int -> IO (Vector Int)
encodeNegate Encoder IO
enc (Vector Int -> IO (Vector Int))
-> IO (Vector Int) -> IO (Vector Int)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Encoder IO -> Vector Int -> Vector Int -> IO (Vector Int)
encodeLShr Encoder IO
enc Vector Int
s' Vector Int
t
    Encoder IO -> Formula -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula Encoder IO
enc (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 (Int -> Formula
forall a. a -> BoolExpr a
Atom (-Int
msb_s)) (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
a) (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
b)
    Vector Int -> IO (Vector Int)
forall (m :: * -> *) a. Monad m => a -> m a
return Vector Int
r

encodeDivRem :: Solver -> SBV -> SBV -> IO (SBV, SBV)
encodeDivRem :: Solver -> Vector Int -> Vector Int -> IO (Vector Int, Vector Int)
encodeDivRem Solver
solver Vector Int
s Vector Int
t = do
  let w :: Int
w = Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
s
  Vector Int
d <- [Int] -> Vector Int
forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList ([Int] -> Vector Int) -> IO [Int] -> IO (Vector Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver -> Int -> IO [Int]
forall (m :: * -> *) a. NewVar m a => a -> Int -> m [Int]
SAT.newVars (Solver -> Solver
svSATSolver Solver
solver) Int
w
  Vector Int
r <- [Int] -> Vector Int
forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList ([Int] -> Vector Int) -> IO [Int] -> IO (Vector Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver -> Int -> IO [Int]
forall (m :: * -> *) a. NewVar m a => a -> Int -> m [Int]
SAT.newVars (Solver -> Solver
svSATSolver Solver
solver) Int
w
  Vector Int
c <- do
    Vector Int
tmp <- Encoder IO -> Bool -> Vector Int -> Vector Int -> IO (Vector Int)
encodeMul (Solver -> Encoder IO
svTseitin Solver
solver) Bool
False Vector Int
d Vector Int
t
    Encoder IO -> Int -> Bool -> [Vector Int] -> IO (Vector Int)
encodeSum (Solver -> Encoder IO
svTseitin Solver
solver) Int
w Bool
False [Vector Int
tmp, Vector Int
r]
  [(Vector Int, Vector Int, Vector Int, Vector Int)]
tbl <- IORef [(Vector Int, Vector Int, Vector Int, Vector Int)]
-> IO [(Vector Int, Vector Int, Vector Int, Vector Int)]
forall a. IORef a -> IO a
readIORef (Solver -> IORef [(Vector Int, Vector Int, Vector Int, Vector Int)]
svDivRemTable Solver
solver)
  Encoder IO -> Formula -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
svTseitin 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 (Vector Int -> Formula
isZero Vector Int
t)
        ([Formula] -> Formula
forall a. [BoolExpr a] -> BoolExpr a
And [(Vector Int -> Vector Int -> Formula
isEQ Vector Int
s Vector Int
s' Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. Vector Int -> Formula
isZero Vector Int
t') Formula -> Formula -> Formula
forall a. Boolean a => a -> a -> a
.=>. (Vector Int -> Vector Int -> Formula
isEQ Vector Int
d Vector Int
d' Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
r') | (Vector Int
s',Vector Int
t',Vector Int
d',Vector Int
r') <- [(Vector Int, Vector Int, Vector Int, Vector Int)]
tbl, Int
w Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
s'])
        (Vector Int -> Vector Int -> Formula
isEQ Vector Int
s Vector Int
c Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. Vector Int -> Vector Int -> Formula
isULT Vector Int
r Vector Int
t)
  IORef [(Vector Int, Vector Int, Vector Int, Vector Int)]
-> ([(Vector Int, Vector Int, Vector Int, Vector Int)]
    -> [(Vector Int, Vector Int, Vector Int, Vector Int)])
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef (Solver -> IORef [(Vector Int, Vector Int, Vector Int, Vector Int)]
svDivRemTable Solver
solver) ((Vector Int
s,Vector Int
t,Vector Int
d,Vector Int
r) (Vector Int, Vector Int, Vector Int, Vector Int)
-> [(Vector Int, Vector Int, Vector Int, Vector Int)]
-> [(Vector Int, Vector Int, Vector Int, Vector Int)]
forall a. a -> [a] -> [a]
:)
  (Vector Int, Vector Int) -> IO (Vector Int, Vector Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Vector Int
d,Vector Int
r)

encodeSDiv :: Solver -> SBV -> SBV -> IO SBV
encodeSDiv :: Solver -> Vector Int -> Vector Int -> IO (Vector Int)
encodeSDiv Solver
solver Vector Int
s Vector Int
t = do
  let w :: Int
w = Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
s
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
w Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
t) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
forall a. HasCallStack => String -> a
error String
"invalid width"
  if Int
w Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then
    Vector Int -> IO (Vector Int)
forall (m :: * -> *) a. Monad m => a -> m a
return Vector Int
forall (v :: * -> *) a. Vector v a => v a
VG.empty
  else do
    Vector Int
s' <- Encoder IO -> Vector Int -> IO (Vector Int)
encodeNegate (Solver -> Encoder IO
svTseitin Solver
solver) Vector Int
s
    Vector Int
t' <- Encoder IO -> Vector Int -> IO (Vector Int)
encodeNegate (Solver -> Encoder IO
svTseitin Solver
solver) Vector Int
t
    let msb_s :: Int
msb_s = Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> a
VG.last Vector Int
s
        msb_t :: Int
msb_t = Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> a
VG.last Vector Int
t
    Vector Int
r <- [Int] -> Vector Int
forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList ([Int] -> Vector Int) -> IO [Int] -> IO (Vector Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver -> Int -> IO [Int]
forall (m :: * -> *) a. NewVar m a => a -> Int -> m [Int]
SAT.newVars (Solver -> Solver
svSATSolver Solver
solver) Int
w
    let f :: Vector Int -> Vector Int -> IO (Vector Int)
f Vector Int
x Vector Int
y = (Vector Int, Vector Int) -> Vector Int
forall a b. (a, b) -> a
fst ((Vector Int, Vector Int) -> Vector Int)
-> IO (Vector Int, Vector Int) -> IO (Vector Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver -> Vector Int -> Vector Int -> IO (Vector Int, Vector Int)
encodeDivRem Solver
solver Vector Int
x Vector Int
y
    Vector Int
a <- Vector Int -> Vector Int -> IO (Vector Int)
f Vector Int
s Vector Int
t
    Vector Int
b <- Encoder IO -> Vector Int -> IO (Vector Int)
encodeNegate (Solver -> Encoder IO
svTseitin Solver
solver) (Vector Int -> IO (Vector Int))
-> IO (Vector Int) -> IO (Vector Int)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Vector Int -> Vector Int -> IO (Vector Int)
f Vector Int
s' Vector Int
t
    Vector Int
c <- Encoder IO -> Vector Int -> IO (Vector Int)
encodeNegate (Solver -> Encoder IO
svTseitin Solver
solver) (Vector Int -> IO (Vector Int))
-> IO (Vector Int) -> IO (Vector Int)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Vector Int -> Vector Int -> IO (Vector Int)
f Vector Int
s Vector Int
t'
    Vector Int
d <- Vector Int -> Vector Int -> IO (Vector Int)
f Vector Int
s' Vector Int
t'
    Encoder IO -> Formula -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
svTseitin 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 (Int -> Formula
forall a. a -> BoolExpr a
Atom (-Int
msb_s) Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. Int -> Formula
forall a. a -> BoolExpr a
Atom (-Int
msb_t)) (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
a) (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$
      Formula -> Formula -> Formula -> Formula
forall b a. IfThenElse b a => b -> a -> a -> a
ite (Int -> Formula
forall a. a -> BoolExpr a
Atom Int
msb_s Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. Int -> Formula
forall a. a -> BoolExpr a
Atom (-Int
msb_t)) (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
b) (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$
      Formula -> Formula -> Formula -> Formula
forall b a. IfThenElse b a => b -> a -> a -> a
ite (Int -> Formula
forall a. a -> BoolExpr a
Atom (-Int
msb_s) Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. Int -> Formula
forall a. a -> BoolExpr a
Atom Int
msb_t) (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
c) (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$
      (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
d)
    Vector Int -> IO (Vector Int)
forall (m :: * -> *) a. Monad m => a -> m a
return Vector Int
r

encodeSRem :: Solver -> SBV -> SBV -> IO SBV
encodeSRem :: Solver -> Vector Int -> Vector Int -> IO (Vector Int)
encodeSRem Solver
solver Vector Int
s Vector Int
t = do
  let w :: Int
w = Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
s
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
w Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
t) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
forall a. HasCallStack => String -> a
error String
"invalid width"
  if Int
w Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then
    Vector Int -> IO (Vector Int)
forall (m :: * -> *) a. Monad m => a -> m a
return Vector Int
forall (v :: * -> *) a. Vector v a => v a
VG.empty
  else do
    Vector Int
s' <- Encoder IO -> Vector Int -> IO (Vector Int)
encodeNegate (Solver -> Encoder IO
svTseitin Solver
solver) Vector Int
s
    Vector Int
t' <- Encoder IO -> Vector Int -> IO (Vector Int)
encodeNegate (Solver -> Encoder IO
svTseitin Solver
solver) Vector Int
t
    let msb_s :: Int
msb_s = Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> a
VG.last Vector Int
s
        msb_t :: Int
msb_t = Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> a
VG.last Vector Int
t
    Vector Int
r <- [Int] -> Vector Int
forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList ([Int] -> Vector Int) -> IO [Int] -> IO (Vector Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver -> Int -> IO [Int]
forall (m :: * -> *) a. NewVar m a => a -> Int -> m [Int]
SAT.newVars (Solver -> Solver
svSATSolver Solver
solver) Int
w
    let f :: Vector Int -> Vector Int -> IO (Vector Int)
f Vector Int
x Vector Int
y = (Vector Int, Vector Int) -> Vector Int
forall a b. (a, b) -> b
snd ((Vector Int, Vector Int) -> Vector Int)
-> IO (Vector Int, Vector Int) -> IO (Vector Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver -> Vector Int -> Vector Int -> IO (Vector Int, Vector Int)
encodeDivRem Solver
solver Vector Int
x Vector Int
y
    Vector Int
a <- Vector Int -> Vector Int -> IO (Vector Int)
f Vector Int
s Vector Int
t
    Vector Int
b <- Encoder IO -> Vector Int -> IO (Vector Int)
encodeNegate (Solver -> Encoder IO
svTseitin Solver
solver) (Vector Int -> IO (Vector Int))
-> IO (Vector Int) -> IO (Vector Int)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Vector Int -> Vector Int -> IO (Vector Int)
f Vector Int
s' Vector Int
t
    Vector Int
c <- Vector Int -> Vector Int -> IO (Vector Int)
f Vector Int
s Vector Int
t'
    Vector Int
d <- Encoder IO -> Vector Int -> IO (Vector Int)
encodeNegate (Solver -> Encoder IO
svTseitin Solver
solver) (Vector Int -> IO (Vector Int))
-> IO (Vector Int) -> IO (Vector Int)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Vector Int -> Vector Int -> IO (Vector Int)
f Vector Int
s' Vector Int
t'
    Encoder IO -> Formula -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
svTseitin 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 (Int -> Formula
forall a. a -> BoolExpr a
Atom (-Int
msb_s) Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. Int -> Formula
forall a. a -> BoolExpr a
Atom (-Int
msb_t)) (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
a) (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$
      Formula -> Formula -> Formula -> Formula
forall b a. IfThenElse b a => b -> a -> a -> a
ite (Int -> Formula
forall a. a -> BoolExpr a
Atom Int
msb_s Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. Int -> Formula
forall a. a -> BoolExpr a
Atom (-Int
msb_t)) (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
b) (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$
      Formula -> Formula -> Formula -> Formula
forall b a. IfThenElse b a => b -> a -> a -> a
ite (Int -> Formula
forall a. a -> BoolExpr a
Atom (-Int
msb_s) Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. Int -> Formula
forall a. a -> BoolExpr a
Atom Int
msb_t) (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
c) (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$
      (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
d)
    Vector Int -> IO (Vector Int)
forall (m :: * -> *) a. Monad m => a -> m a
return Vector Int
r

encodeSMod :: Solver -> SBV -> SBV -> IO SBV
encodeSMod :: Solver -> Vector Int -> Vector Int -> IO (Vector Int)
encodeSMod Solver
solver Vector Int
s Vector Int
t = do
  let w :: Int
w = Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
s
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
w Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
t) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
forall a. HasCallStack => String -> a
error String
"invalid width"
  if Int
w Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then
    Vector Int -> IO (Vector Int)
forall (m :: * -> *) a. Monad m => a -> m a
return Vector Int
forall (v :: * -> *) a. Vector v a => v a
VG.empty
  else do
    let msb_s :: Int
msb_s = Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> a
VG.last Vector Int
s
        msb_t :: Int
msb_t = Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> a
VG.last Vector Int
t
    Vector Int
r <- [Int] -> Vector Int
forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList ([Int] -> Vector Int) -> IO [Int] -> IO (Vector Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver -> Int -> IO [Int]
forall (m :: * -> *) a. NewVar m a => a -> Int -> m [Int]
SAT.newVars (Solver -> Solver
svSATSolver Solver
solver) Int
w
    Vector Int
abs_s <- Encoder IO -> Vector Int -> IO (Vector Int)
encodeAbs (Solver -> Encoder IO
svTseitin Solver
solver) Vector Int
s
    Vector Int
abs_t <- Encoder IO -> Vector Int -> IO (Vector Int)
encodeAbs (Solver -> Encoder IO
svTseitin Solver
solver) Vector Int
t
    Vector Int
u <- (Vector Int, Vector Int) -> Vector Int
forall a b. (a, b) -> b
snd ((Vector Int, Vector Int) -> Vector Int)
-> IO (Vector Int, Vector Int) -> IO (Vector Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver -> Vector Int -> Vector Int -> IO (Vector Int, Vector Int)
encodeDivRem Solver
solver Vector Int
abs_s Vector Int
abs_t
    Vector Int
u' <- Encoder IO -> Vector Int -> IO (Vector Int)
encodeNegate (Solver -> Encoder IO
svTseitin Solver
solver) Vector Int
u
    Vector Int
a <- Encoder IO -> Int -> Bool -> [Vector Int] -> IO (Vector Int)
encodeSum (Solver -> Encoder IO
svTseitin Solver
solver) Int
w Bool
True [Vector Int
u', Vector Int
t]
    Vector Int
b <- Encoder IO -> Int -> Bool -> [Vector Int] -> IO (Vector Int)
encodeSum (Solver -> Encoder IO
svTseitin Solver
solver) Int
w Bool
True [Vector Int
u, Vector Int
t]
    Encoder IO -> Formula -> IO ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
svTseitin 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 (Vector Int -> Formula
isZero Vector Int
u Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.||. (Int -> Formula
forall a. a -> BoolExpr a
Atom (-Int
msb_s) Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. Int -> Formula
forall a. a -> BoolExpr a
Atom (-Int
msb_t))) (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
u) (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$
      Formula -> Formula -> Formula -> Formula
forall b a. IfThenElse b a => b -> a -> a -> a
ite (Int -> Formula
forall a. a -> BoolExpr a
Atom Int
msb_s Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. Int -> Formula
forall a. a -> BoolExpr a
Atom (-Int
msb_t)) (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
a) (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$
      Formula -> Formula -> Formula -> Formula
forall b a. IfThenElse b a => b -> a -> a -> a
ite (Int -> Formula
forall a. a -> BoolExpr a
Atom (-Int
msb_s) Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. Int -> Formula
forall a. a -> BoolExpr a
Atom Int
msb_t) (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
b) (Formula -> Formula) -> Formula -> Formula
forall a b. (a -> b) -> a -> b
$
      (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
u')
    Vector Int -> IO (Vector Int)
forall (m :: * -> *) a. Monad m => a -> m a
return Vector Int
r

isZero :: SBV -> Tseitin.Formula
isZero :: Vector Int -> Formula
isZero Vector Int
bs = [Formula] -> Formula
forall a. [BoolExpr a] -> BoolExpr a
And [Formula -> Formula
forall a. BoolExpr a -> BoolExpr a
Not (Int -> Formula
forall a. a -> BoolExpr a
Atom Int
b) | Int
b <- Vector Int -> [Int]
forall (v :: * -> *) a. Vector v a => v a -> [a]
VG.toList Vector Int
bs]

isEQ :: SBV -> SBV -> Tseitin.Formula
isEQ :: Vector Int -> Vector Int -> Formula
isEQ Vector Int
bs1 Vector Int
bs2
  | Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs2 = String -> Formula
forall a. HasCallStack => String -> a
error (String
"length mismatch: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs1) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs2))
  | Bool
otherwise = [Formula] -> Formula
forall a. [BoolExpr a] -> BoolExpr a
And [Formula -> Formula -> Formula
forall a. BoolExpr a -> BoolExpr a -> BoolExpr a
Equiv (Int -> Formula
forall a. a -> BoolExpr a
Atom Int
b1) (Int -> Formula
forall a. a -> BoolExpr a
Atom Int
b2) | (Int
b1,Int
b2) <- [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Vector Int -> [Int]
forall (v :: * -> *) a. Vector v a => v a -> [a]
VG.toList Vector Int
bs1) (Vector Int -> [Int]
forall (v :: * -> *) a. Vector v a => v a -> [a]
VG.toList Vector Int
bs2)]

isULT :: SBV -> SBV -> Tseitin.Formula
isULT :: Vector Int -> Vector Int -> Formula
isULT Vector Int
bs1 Vector Int
bs2
  | Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs2 = String -> Formula
forall a. HasCallStack => String -> a
error (String
"length mismatch: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs1) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs2))
  | Bool
otherwise = [Int] -> [Int] -> Formula
forall a. [a] -> [a] -> BoolExpr a
f (Vector Int -> [Int]
forall (v :: * -> *) a. Vector v a => v a -> [a]
VG.toList (Vector Int -> Vector Int
forall (v :: * -> *) a. Vector v a => v a -> v a
VG.reverse Vector Int
bs1)) (Vector Int -> [Int]
forall (v :: * -> *) a. Vector v a => v a -> [a]
VG.toList (Vector Int -> Vector Int
forall (v :: * -> *) a. Vector v a => v a -> v a
VG.reverse Vector Int
bs2))
  where
    f :: [a] -> [a] -> BoolExpr a
f [] [] = BoolExpr a
forall a. MonotoneBoolean a => a
false
    f (a
b1:[a]
bs1) (a
b2:[a]
bs2) =
      (BoolExpr a -> BoolExpr a
forall a. Complement a => a -> a
notB (a -> BoolExpr a
forall a. a -> BoolExpr a
Atom a
b1) BoolExpr a -> BoolExpr a -> BoolExpr a
forall a. MonotoneBoolean a => a -> a -> a
.&&. a -> BoolExpr a
forall a. a -> BoolExpr a
Atom a
b2) BoolExpr a -> BoolExpr a -> BoolExpr a
forall a. MonotoneBoolean a => a -> a -> a
.||. ((a -> BoolExpr a
forall a. a -> BoolExpr a
Atom a
b1 BoolExpr a -> BoolExpr a -> BoolExpr a
forall a. Boolean a => a -> a -> a
.=>. a -> BoolExpr a
forall a. a -> BoolExpr a
Atom a
b2) BoolExpr a -> BoolExpr a -> BoolExpr a
forall a. MonotoneBoolean a => a -> a -> a
.&&. [a] -> [a] -> BoolExpr a
f [a]
bs1 [a]
bs2)
    f [a]
_ [a]
_ = String -> BoolExpr a
forall a. HasCallStack => String -> a
error String
"should not happen"

isSLT :: SBV -> SBV -> Tseitin.Formula
isSLT :: Vector Int -> Vector Int -> Formula
isSLT Vector Int
bs1 Vector Int
bs2
  | Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs2 = String -> Formula
forall a. HasCallStack => String -> a
error (String
"length mismatch: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs1) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs2))
  | Int
w Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = Formula
forall a. MonotoneBoolean a => a
false
  | Bool
otherwise =
      Int -> Formula
forall a. a -> BoolExpr a
Atom Int
bs1_msb Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. Formula -> Formula
forall a. BoolExpr a -> BoolExpr a
Not (Int -> Formula
forall a. a -> BoolExpr a
Atom Int
bs2_msb)
      Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.||. (Int -> Formula
forall a. a -> BoolExpr a
Atom Int
bs1_msb Formula -> Formula -> Formula
forall a. Boolean a => a -> a -> a
.<=>. Int -> Formula
forall a. a -> BoolExpr a
Atom Int
bs2_msb) Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. Vector Int -> Vector Int -> Formula
isULT Vector Int
bs1 Vector Int
bs2
  where
    w :: Int
w = Vector Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs1
    bs1_msb :: Int
bs1_msb = Vector Int
bs1 Vector Int -> Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int -> a
VG.! (Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)
    bs2_msb :: Int
bs2_msb = Vector Int
bs2 Vector Int -> Int -> Int
forall (v :: * -> *) a. Vector v a => v a -> Int -> a
VG.! (Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)

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

_test1 :: IO ()
_test1 :: IO ()
_test1 = do
  Solver
solver <- IO Solver
newSolver
  Expr
v1 <- Solver -> Int -> IO Expr
newVar Solver
solver Int
8
  Expr
v2 <- Solver -> Int -> IO Expr
newVar Solver
solver Int
8
  Solver -> Atom -> Maybe Int -> IO ()
assertAtom Solver
solver (Op2 -> Expr -> Expr -> Expr
EOp2 Op2
OpMul Expr
v1 Expr
v2 Expr -> Expr -> Atom
forall e r. IsEqRel e r => e -> e -> r
.==. Int -> Integer -> Expr
forall a. IsBV a => Int -> Integer -> a
nat2bv Int
8 Integer
6) Maybe Int
forall a. Maybe a
Nothing
  Bool -> IO ()
forall a. Show a => a -> IO ()
print (Bool -> IO ()) -> IO Bool -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> IO Bool
check Solver
solver
  Model
m <- Solver -> IO Model
getModel Solver
solver
  Model -> IO ()
forall a. Show a => a -> IO ()
print Model
m

_test2 :: IO ()
_test2 :: IO ()
_test2 = do
  Solver
solver <- IO Solver
newSolver
  Expr
v1 <- Solver -> Int -> IO Expr
newVar Solver
solver Int
8
  Expr
v2 <- Solver -> Int -> IO Expr
newVar Solver
solver Int
8
  let z :: Expr
z = Int -> Integer -> Expr
forall a. IsBV a => Int -> Integer -> a
nat2bv Int
8 Integer
0
  Solver -> Atom -> Maybe Int -> IO ()
assertAtom Solver
solver (Op2 -> Expr -> Expr -> Expr
EOp2 Op2
OpUDiv Expr
v1 Expr
z Expr -> Expr -> Atom
forall e r. IsEqRel e r => e -> e -> r
./=. Op2 -> Expr -> Expr -> Expr
EOp2 Op2
OpUDiv Expr
v2 Expr
z) Maybe Int
forall a. Maybe a
Nothing
  Solver -> Atom -> Maybe Int -> IO ()
assertAtom Solver
solver (Expr
v1 Expr -> Expr -> Atom
forall e r. IsEqRel e r => e -> e -> r
.==. Expr
v2) Maybe Int
forall a. Maybe a
Nothing
  Bool -> IO ()
forall a. Show a => a -> IO ()
print (Bool -> IO ()) -> IO Bool -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> IO Bool
check Solver
solver -- False