{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# 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
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.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.SAT.Encoder.Tseitin (Formula (..))

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 <- forall (a :: * -> * -> *) e. MArray a e IO => IO (GenericVec a e)
Vec.new
  Solver
sat <- IO Solver
SAT.newSolver
  Encoder IO
tseitin <- forall (m :: * -> *) a.
(PrimMonad m, AddClause m a) =>
a -> m (Encoder m)
Tseitin.newEncoder Solver
sat
  IORef (Map Expr (Vector Int))
table <- forall a. a -> IO (IORef a)
newIORef forall k a. Map k a
Map.empty
  IORef [(Vector Int, Vector Int, Vector Int, Vector Int)]
divRemTable <- forall a. a -> IO (IORef a)
newIORef []
  IORef (Map NormalizedAtom Int)
atomTable <- forall a. a -> IO (IORef a)
newIORef forall k a. Map k a
Map.empty
  Vec (IntMap (Maybe Int))
contexts <- forall (a :: * -> * -> *) e. MArray a e IO => IO (GenericVec a e)
Vec.new
  forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push Vec (IntMap (Maybe Int))
contexts forall a. IntMap a
IntMap.empty
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    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 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 <- forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. NewVar m a => a -> Int -> m [Int]
SAT.newVars (Solver -> Solver
svSATSolver Solver
solver) Int
w
  Int
v <- forall (a :: * -> * -> *) e. GenericVec a e -> IO Int
Vec.getSize forall a b. (a -> b) -> a -> b
$ Solver -> Vec (Vector Int)
svVars Solver
solver
  forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> Vec (Vector Int)
svVars Solver
solver) Vector Int
bs
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Var{ varWidth :: Int
varWidth = Int
w, varId :: Int
varId = Int
v }

data NormalizedRel = NRSLt | NRULt | NREql
  deriving (NormalizedRel -> NormalizedRel -> Bool
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
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
Ord, Int -> NormalizedRel
NormalizedRel -> Int
NormalizedRel -> [NormalizedRel]
NormalizedRel -> NormalizedRel
NormalizedRel -> NormalizedRel -> [NormalizedRel]
NormalizedRel -> NormalizedRel -> NormalizedRel -> [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
forall a. a -> a -> Bounded a
maxBound :: NormalizedRel
$cmaxBound :: NormalizedRel
minBound :: NormalizedRel
$cminBound :: NormalizedRel
Bounded, Int -> NormalizedRel -> ShowS
[NormalizedRel] -> ShowS
NormalizedRel -> String
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
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
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
Ord, Int -> NormalizedAtom -> ShowS
[NormalizedAtom] -> ShowS
NormalizedAtom -> String
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 <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map NormalizedAtom Int)
svAtomTable Solver
solver)
  Int
l <- (if Bool
polarity then forall a. a -> a
id else forall a. Num a => a -> a
negate) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup NormalizedAtom
atom' Map NormalizedAtom Int
table of
      Just Int
lit -> 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 <- forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Int
Tseitin.encodeFormula (Solver -> Encoder IO
svTseitin Solver
solver) 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
        forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (Map NormalizedAtom Int)
svAtomTable Solver
solver) forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert NormalizedAtom
atom' Int
l Map NormalizedAtom Int
table
        forall (m :: * -> *) a. Monad m => a -> m a
return Int
l
  Int
size <- 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 forall a. Eq a => a -> a -> Bool
== Int
1 -> forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause (Solver -> Encoder IO
svTseitin Solver
solver) [Int
l]
    Maybe Int
_ -> do
      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 forall a. Num a => a -> a -> a
- Int
1) (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 <- forall (a :: * -> * -> *) e. GenericVec a e -> IO Int
Vec.getSize (Solver -> Vec (IntMap (Maybe Int))
svContexts Solver
solver)
  IntMap (Maybe Int)
m <- 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 forall a. Num a => a -> a -> a
- Int
1)
  Bool
b <- Solver -> [Int] -> IO Bool
SAT.solveWith (Solver -> Solver
svSATSolver Solver
solver) (forall a. IntMap a -> [Int]
IntMap.keys IntMap (Maybe Int)
m)
  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 <- 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 = forall a. IsBV a => [Bool] -> a
fromAscBits forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall m. IModel m => m -> Int -> Bool
SAT.evalLit Model
m) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (v :: * -> *) a. Vector v a => v a -> [a]
VG.toList
      isZero' :: BV -> Bool
isZero' = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *). Foldable t => t Bool -> Bool
or forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV -> [Bool]
toAscBits
      env :: Vector BV
env = 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 <- 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 = 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 = 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)]
  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 <- forall (a :: * -> * -> *) e. GenericVec a e -> IO Int
Vec.getSize (Solver -> Vec (IntMap (Maybe Int))
svContexts Solver
solver)
  IntMap (Maybe Int)
m <- 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 forall a. Num a => a -> a -> a
- Int
1)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Int] -> IntSet
IntSet.fromList forall a b. (a -> b) -> a -> b
$ forall a. [Maybe a] -> [a]
catMaybes forall a b. (a -> b) -> a -> b
$ forall a. IntMap a -> [a]
IntMap.elems forall a b. (a -> b) -> a -> b
$ forall a. IntMap a -> IntSet -> IntMap a
IntMap.restrictKeys IntMap (Maybe Int)
m IntSet
xs

pushBacktrackPoint :: Solver -> IO ()
pushBacktrackPoint :: Solver -> IO ()
pushBacktrackPoint Solver
solver = do
  Int
size <- forall (a :: * -> * -> *) e. GenericVec a e -> IO Int
Vec.getSize (Solver -> Vec (IntMap (Maybe Int))
svContexts Solver
solver)
  IntMap (Maybe Int)
m <- 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 forall a. Num a => a -> a -> a
- Int
1)
  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)
_ <- forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO e
Vec.pop (Solver -> Vec (IntMap (Maybe Int))
svContexts Solver
solver)
  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 <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (Map Expr (Vector Int))
svEncTable Solver
solver)
      case 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 -> 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
          forall a. IORef a -> (a -> a) -> IO ()
modifyIORef (Solver -> IORef (Map Expr (Vector Int))
svEncTable Solver
solver) (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Expr
e Vector Int
vs)
          forall (m :: * -> *) a. Monad m => a -> m a
return Vector Int
vs

    enc' :: Expr -> IO (Vector Int)
enc' (EConst BV
bs) =
      forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. Unbox a => [a] -> Vector a
VU.fromList forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (BV -> [Bool]
toAscBits BV
bs) forall a b. (a -> b) -> a -> b
$ \Bool
b ->
        if Bool
b
        then forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeConj (Solver -> Encoder IO
svTseitin Solver
solver) []
        else forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeDisj (Solver -> Encoder IO
svTseitin Solver
solver) []
    enc' (EVar Var
v) = 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
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
arg' forall a. Ord a => a -> a -> Bool
> Int
i Bool -> Bool -> Bool
&& Int
i forall a. Ord a => a -> a -> Bool
>= Int
j Bool -> Bool -> Bool
&& Int
j forall a. Ord a => a -> a -> Bool
>= Int
0) forall a b. (a -> b) -> a -> b
$
            forall a. HasCallStack => String -> a
error (String
"invalid extract " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Int
i,Int
j) forall a. [a] -> [a] -> [a]
++ String
" on bit-vector of length " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
arg') forall a. [a] -> [a] -> [a]
++ String
" : " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Expr
arg)
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (v :: * -> *) a. Vector v a => Int -> Int -> v a -> v a
VG.slice Int
j (Int
i forall a. Num a => a -> a -> a
- Int
j forall a. Num a => a -> a -> a
+ Int
1) Vector Int
arg'
        Op1
OpNot -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (v :: * -> *) a b.
(Vector v a, Vector v b) =>
(a -> b) -> v a -> v b
VG.map 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return (Vector Int
arg2' forall a. Semigroup a => a -> a -> a
<> Vector Int
arg1')
        Op2
OpAnd -> 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 -> 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  -> 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 -> 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 -> 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 (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 -> forall (v :: * -> *) a. Vector v a => a -> v a
VG.singleton forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) (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 -> forall a b. (a, b) -> a
fst 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 -> forall a b. (a, b) -> b
snd 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 = forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
arg1
  Int
b0 <- forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeDisj Encoder IO
enc [] -- False
  [Vector Int]
bss <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] (forall (v :: * -> *) a. Vector v a => v a -> [a]
VG.toList Vector Int
arg2)) forall a b. (a -> b) -> a -> b
$ \(Int
i,Int
b2) -> do
    let arg1' :: Vector Int
arg1' = if Bool
allowOverflow
                then forall (v :: * -> *) a. Vector v a => Int -> v a -> v a
VG.take (Int
w forall a. Num a => a -> a -> a
- Int
i) Vector Int
arg1
                else Vector Int
arg1
    Vector Int
bs <- 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' forall a b. (a -> b) -> a -> b
$ \Int
b1 -> do
            forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeConj Encoder IO
enc [Int
b1,Int
b2]
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall (v :: * -> *) a. Vector v a => Int -> a -> v a
VG.replicate Int
i Int
b0 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))) <- forall a. a -> IO (IORef a)
newIORef forall a. Seq a
Seq.empty
  let insert :: Int -> Int -> IO ()
insert Int
i Int
x = do
        Seq (SeqQueue IO Int)
bs <- forall a. IORef a -> IO a
readIORef IORef (Seq (SeqQueue IO Int))
buckets
        let n :: Int
n = forall a. Seq a -> Int
Seq.length Seq (SeqQueue IO Int)
bs
        SeqQueue IO Int
q <- if Int
i forall a. Ord a => a -> a -> Bool
< Int
n then do
               forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Seq a -> Int -> a
Seq.index Seq (SeqQueue IO Int)
bs Int
i
             else do
               [SeqQueue IO Int]
qs <- forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM (Int
iforall a. Num a => a -> a -> a
+Int
1 forall a. Num a => a -> a -> a
- Int
n) forall q (m :: * -> *). NewFifo q m => m q
SQ.newFifo
               let bs' :: Seq (SeqQueue IO Int)
bs' = Seq (SeqQueue IO Int)
bs forall a. Seq a -> Seq a -> Seq a
Seq.>< forall a. [a] -> Seq a
Seq.fromList [SeqQueue IO Int]
qs
               forall a. IORef a -> a -> IO ()
writeIORef IORef (Seq (SeqQueue IO Int))
buckets Seq (SeqQueue IO Int)
bs'
               forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Seq a -> Int -> a
Seq.index Seq (SeqQueue IO Int)
bs' Int
i
        forall q (m :: * -> *) a. Enqueue q m a => q -> a -> m ()
SQ.enqueue SeqQueue IO Int
q Int
x

  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Vector Int]
xss forall a b. (a -> b) -> a -> b
$ \Vector Int
xs -> do
    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 forall a. Ord a => a -> a -> Bool
>= Int
w = do
            forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
allowOverflow forall a b. (a -> b) -> a -> b
$ do
              Seq (SeqQueue IO Int)
bs <- forall a. IORef a -> IO a
readIORef IORef (Seq (SeqQueue IO Int))
buckets
              forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (SeqQueue IO Int)
bs) forall a b. (a -> b) -> a -> b
$ \SeqQueue IO Int
q -> do
                [Int]
ls <- forall q (m :: * -> *) a. Dequeue q m a => q -> m [a]
SQ.dequeueBatch SeqQueue IO Int
q
                forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int]
ls forall a b. (a -> b) -> a -> b
$ \Int
l -> do
                  forall (m :: * -> *) a. AddClause m a => a -> [Int] -> m ()
SAT.addClause  Encoder IO
enc [-Int
l]
            forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. [a] -> [a]
reverse [Int]
ret)
        | Bool
otherwise = do
            Seq (SeqQueue IO Int)
bs <- forall a. IORef a -> IO a
readIORef IORef (Seq (SeqQueue IO Int))
buckets
            let n :: Int
n = forall a. Seq a -> Int
Seq.length Seq (SeqQueue IO Int)
bs
            if Int
i forall a. Ord a => a -> a -> Bool
>= Int
n then do
              Int
b <- forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeDisj Encoder IO
enc [] -- False
              Int -> [Int] -> IO [Int]
loop (Int
iforall a. Num a => a -> a -> a
+Int
1) (Int
b forall a. a -> [a] -> [a]
: [Int]
ret)
            else do
              let q :: SeqQueue IO Int
q = forall a. Seq a -> Int -> a
Seq.index Seq (SeqQueue IO Int)
bs Int
i
              Int
m <- forall q (m :: * -> *). QueueSize q m => q -> m Int
SQ.queueSize SeqQueue IO Int
q
              case Int
m of
                Int
0 -> do
                  Int
b <- forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeDisj Encoder IO
enc [] -- False
                  Int -> [Int] -> IO [Int]
loop (Int
iforall a. Num a => a -> a -> a
+Int
1) (Int
b forall a. a -> [a] -> [a]
: [Int]
ret)
                Int
1 -> do
                  Just Int
b <- forall q (m :: * -> *) a. Dequeue q m a => q -> m (Maybe a)
SQ.dequeue SeqQueue IO Int
q
                  Int -> [Int] -> IO [Int]
loop (Int
iforall a. Num a => a -> a -> a
+Int
1) (Int
b forall a. a -> [a] -> [a]
: [Int]
ret)
                Int
2 -> do
                  Just Int
b1 <- forall q (m :: * -> *) a. Dequeue q m a => q -> m (Maybe a)
SQ.dequeue SeqQueue IO Int
q
                  Just Int
b2 <- 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
iforall a. Num a => a -> a -> a
+Int
1) Int
c
                  Int -> [Int] -> IO [Int]
loop (Int
iforall a. Num a => a -> a -> a
+Int
1) (Int
s forall a. a -> [a] -> [a]
: [Int]
ret)
                Int
_ -> do
                  Just Int
b1 <- forall q (m :: * -> *) a. Dequeue q m a => q -> m (Maybe a)
SQ.dequeue SeqQueue IO Int
q
                  Just Int
b2 <- forall q (m :: * -> *) a. Dequeue q m a => q -> m (Maybe a)
SQ.dequeue SeqQueue IO Int
q
                  Just Int
b3 <- forall q (m :: * -> *) a. Dequeue q m a => q -> m (Maybe a)
SQ.dequeue SeqQueue IO Int
q
                  Int
s <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Int -> Int -> Int -> m Int
Tseitin.encodeFASum Encoder IO
enc Int
b1 Int
b2 Int
b3
                  Int
c <- 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
iforall a. Num a => a -> a -> a
+Int
1) Int
c
                  Int -> [Int] -> IO [Int]
loop Int
i [Int]
ret
  forall a. Unbox a => [a] -> Vector a
VU.fromList 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 = 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 = 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Unbox a => [a] -> Vector a
VU.fromList forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse [Int]
ret
      f Int
b (Int
x:[Int]
xs) [Int]
ret = do
        Int
y <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Int -> Int -> Int -> m Int
Tseitin.encodeITE Encoder IO
enc Int
b (- Int
x) Int
x
        Int
b' <- 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 forall a. a -> [a] -> [a]
: [Int]
ret)
  Int
b0 <- forall (m :: * -> *). PrimMonad m => Encoder m -> [Int] -> m Int
Tseitin.encodeDisj Encoder IO
enc []
  Int -> [Int] -> [Int] -> IO (Vector Int)
f Int
b0 (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 = forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
s
  if Int
w forall a. Eq a => a -> a -> Bool
== Int
0 then
    forall (m :: * -> *) a. Monad m => a -> m a
return forall (v :: * -> *) a. Vector v a => v a
VG.empty
  else do
    let msb_s :: Int
msb_s = forall (v :: * -> *) a. Vector v a => v a -> a
VG.last Vector Int
s
    Vector Int
r <- forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
    forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula Encoder IO
enc forall a b. (a -> b) -> a -> b
$
      forall b a. IfThenElse b a => b -> a -> a -> a
ite (Int -> Formula
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)
    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 = forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
s
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
w forall a. Eq a => a -> a -> Bool
/= forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
t) forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => String -> a
error String
"invalid width"
  Int
b0 <- 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) =
        forall (m :: * -> *) (v :: * -> *) a.
(Monad m, Vector v a) =>
Int -> (Int -> m a) -> m (v a)
VG.generateM Int
w forall a b. (a -> b) -> a -> b
$ \Int
j -> do
          let k :: Integer
k = forall a. Integral a => a -> Integer
toInteger Int
j forall a. Num a => a -> a -> a
- Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^a
i
              t :: Int
t = if Integer
k forall a. Ord a => a -> a -> Bool
>= Integer
0 then v Int
bs forall (v :: * -> *) a. Vector v a => v a -> Int -> a
VG.! forall a. Num a => Integer -> a
fromInteger Integer
k else Int
b0
              e :: Int
e = v Int
bs forall (v :: * -> *) a. Vector v a => v a -> Int -> a
VG.! Int
j
          forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Int -> Int -> Int -> m Int
Tseitin.encodeITE Encoder IO
enc Int
b Int
t Int
e
  forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM forall {v :: * -> *} {v :: * -> *} {a}.
(Vector v Int, Integral a, Vector v Int) =>
v Int -> (a, Int) -> IO (v Int)
go Vector Int
s (forall a b. [a] -> [b] -> [(a, b)]
zip [(Int
0::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 = forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
s
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
w forall a. Eq a => a -> a -> Bool
/= forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
t) forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => String -> a
error String
"invalid width"
  Int
b0 <- 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) =
        forall (m :: * -> *) (v :: * -> *) a.
(Monad m, Vector v a) =>
Int -> (Int -> m a) -> m (v a)
VG.generateM Int
w forall a b. (a -> b) -> a -> b
$ \Int
j -> do
          let k :: Integer
k = forall a. Integral a => a -> Integer
toInteger Int
j forall a. Num a => a -> a -> a
+ Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^a
i
              t :: Int
t = if Integer
k forall a. Ord a => a -> a -> Bool
< forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length v Int
bs) then v Int
bs forall (v :: * -> *) a. Vector v a => v a -> Int -> a
VG.! forall a. Num a => Integer -> a
fromInteger Integer
k else Int
b0
              e :: Int
e = v Int
bs forall (v :: * -> *) a. Vector v a => v a -> Int -> a
VG.! Int
j
          forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Int -> Int -> Int -> m Int
Tseitin.encodeITE Encoder IO
enc Int
b Int
t Int
e
  forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM forall {v :: * -> *} {v :: * -> *} {a}.
(Vector v Int, Integral a, Vector v Int) =>
v Int -> (a, Int) -> IO (v Int)
go Vector Int
s (forall a b. [a] -> [b] -> [(a, b)]
zip [(Int
0::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 = forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
s
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
w forall a. Eq a => a -> a -> Bool
/= forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
t) forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => String -> a
error String
"invalid width"
  if Int
w forall a. Eq a => a -> a -> Bool
== Int
0 then
    forall (m :: * -> *) a. Monad m => a -> m a
return forall (v :: * -> *) a. Vector v a => v a
VG.empty
  else do
    let msb_s :: Int
msb_s = forall (v :: * -> *) a. Vector v a => v a -> a
VG.last Vector Int
s
    Vector Int
r <- forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 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
    forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula Encoder IO
enc forall a b. (a -> b) -> a -> b
$
      forall b a. IfThenElse b a => b -> a -> a -> a
ite (Int -> Formula
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)
    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 = forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
s
  Vector Int
d <- forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. NewVar m a => a -> Int -> m [Int]
SAT.newVars (Solver -> Solver
svSATSolver Solver
solver) Int
w
  Vector Int
r <- forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 <- forall a. IORef a -> IO a
readIORef (Solver -> IORef [(Vector Int, Vector Int, Vector Int, Vector Int)]
svDivRemTable Solver
solver)
  forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
svTseitin Solver
solver) forall a b. (a -> b) -> a -> b
$
    forall b a. IfThenElse b a => b -> a -> a -> a
ite (Vector Int -> Formula
isZero Vector Int
t)
        ([Formula] -> Formula
And [(Vector Int -> Vector Int -> Formula
isEQ Vector Int
s Vector Int
s' forall a. MonotoneBoolean a => a -> a -> a
.&&. Vector Int -> Formula
isZero Vector Int
t') forall a. Boolean a => a -> a -> a
.=>. (Vector Int -> Vector Int -> Formula
isEQ Vector Int
d Vector Int
d' 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 forall a. Eq a => a -> a -> Bool
== 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 forall a. MonotoneBoolean a => a -> a -> a
.&&. Vector Int -> Vector Int -> Formula
isULT Vector Int
r Vector Int
t)
  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) forall a. a -> [a] -> [a]
:)
  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 = forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
s
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
w forall a. Eq a => a -> a -> Bool
/= forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
t) forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => String -> a
error String
"invalid width"
  if Int
w forall a. Eq a => a -> a -> Bool
== Int
0 then
    forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall (v :: * -> *) a. Vector v a => v a -> a
VG.last Vector Int
s
        msb_t :: Int
msb_t = forall (v :: * -> *) a. Vector v a => v a -> a
VG.last Vector Int
t
    Vector Int
r <- forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall a b. (a, b) -> a
fst 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) 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) 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'
    forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
svTseitin Solver
solver) forall a b. (a -> b) -> a -> b
$
      forall b a. IfThenElse b a => b -> a -> a -> a
ite (Int -> Formula
Atom (-Int
msb_s) forall a. MonotoneBoolean a => a -> a -> a
.&&. Int -> Formula
Atom (-Int
msb_t)) (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
a) forall a b. (a -> b) -> a -> b
$
      forall b a. IfThenElse b a => b -> a -> a -> a
ite (Int -> Formula
Atom Int
msb_s forall a. MonotoneBoolean a => a -> a -> a
.&&. Int -> Formula
Atom (-Int
msb_t)) (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
b) forall a b. (a -> b) -> a -> b
$
      forall b a. IfThenElse b a => b -> a -> a -> a
ite (Int -> Formula
Atom (-Int
msb_s) forall a. MonotoneBoolean a => a -> a -> a
.&&. Int -> Formula
Atom Int
msb_t) (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
c) forall a b. (a -> b) -> a -> b
$
      (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
d)
    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 = forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
s
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
w forall a. Eq a => a -> a -> Bool
/= forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
t) forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => String -> a
error String
"invalid width"
  if Int
w forall a. Eq a => a -> a -> Bool
== Int
0 then
    forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall (v :: * -> *) a. Vector v a => v a -> a
VG.last Vector Int
s
        msb_t :: Int
msb_t = forall (v :: * -> *) a. Vector v a => v a -> a
VG.last Vector Int
t
    Vector Int
r <- forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall a b. (a, b) -> b
snd 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) 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) 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'
    forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
svTseitin Solver
solver) forall a b. (a -> b) -> a -> b
$
      forall b a. IfThenElse b a => b -> a -> a -> a
ite (Int -> Formula
Atom (-Int
msb_s) forall a. MonotoneBoolean a => a -> a -> a
.&&. Int -> Formula
Atom (-Int
msb_t)) (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
a) forall a b. (a -> b) -> a -> b
$
      forall b a. IfThenElse b a => b -> a -> a -> a
ite (Int -> Formula
Atom Int
msb_s forall a. MonotoneBoolean a => a -> a -> a
.&&. Int -> Formula
Atom (-Int
msb_t)) (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
b) forall a b. (a -> b) -> a -> b
$
      forall b a. IfThenElse b a => b -> a -> a -> a
ite (Int -> Formula
Atom (-Int
msb_s) forall a. MonotoneBoolean a => a -> a -> a
.&&. Int -> Formula
Atom Int
msb_t) (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
c) forall a b. (a -> b) -> a -> b
$
      (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
d)
    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 = forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
s
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
w forall a. Eq a => a -> a -> Bool
/= forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
t) forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => String -> a
error String
"invalid width"
  if Int
w forall a. Eq a => a -> a -> Bool
== Int
0 then
    forall (m :: * -> *) a. Monad m => a -> m a
return forall (v :: * -> *) a. Vector v a => v a
VG.empty
  else do
    let msb_s :: Int
msb_s = forall (v :: * -> *) a. Vector v a => v a -> a
VG.last Vector Int
s
        msb_t :: Int
msb_t = forall (v :: * -> *) a. Vector v a => v a -> a
VG.last Vector Int
t
    Vector Int
r <- forall (v :: * -> *) a. Vector v a => [a] -> v a
VG.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 <- forall a b. (a, b) -> b
snd 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]
    forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
Tseitin.addFormula (Solver -> Encoder IO
svTseitin Solver
solver) forall a b. (a -> b) -> a -> b
$
      forall b a. IfThenElse b a => b -> a -> a -> a
ite (Vector Int -> Formula
isZero Vector Int
u forall a. MonotoneBoolean a => a -> a -> a
.||. (Int -> Formula
Atom (-Int
msb_s) forall a. MonotoneBoolean a => a -> a -> a
.&&. Int -> Formula
Atom (-Int
msb_t))) (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
u) forall a b. (a -> b) -> a -> b
$
      forall b a. IfThenElse b a => b -> a -> a -> a
ite (Int -> Formula
Atom Int
msb_s forall a. MonotoneBoolean a => a -> a -> a
.&&. Int -> Formula
Atom (-Int
msb_t)) (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
a) forall a b. (a -> b) -> a -> b
$
      forall b a. IfThenElse b a => b -> a -> a -> a
ite (Int -> Formula
Atom (-Int
msb_s) forall a. MonotoneBoolean a => a -> a -> a
.&&. Int -> Formula
Atom Int
msb_t) (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
b) forall a b. (a -> b) -> a -> b
$
      (Vector Int -> Vector Int -> Formula
isEQ Vector Int
r Vector Int
u')
    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
And [Formula -> Formula
Not (Int -> Formula
Atom Int
b) | Int
b <- 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
  | forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs1 forall a. Eq a => a -> a -> Bool
/= forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs2 = forall a. HasCallStack => String -> a
error (String
"length mismatch: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs1) forall a. [a] -> [a] -> [a]
++ String
" and " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs2))
  | Bool
otherwise = [Formula] -> Formula
And [Formula -> Formula -> Formula
Equiv (Int -> Formula
Atom Int
b1) (Int -> Formula
Atom Int
b2) | (Int
b1,Int
b2) <- forall a b. [a] -> [b] -> [(a, b)]
zip (forall (v :: * -> *) a. Vector v a => v a -> [a]
VG.toList Vector Int
bs1) (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
  | forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs1 forall a. Eq a => a -> a -> Bool
/= forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs2 = forall a. HasCallStack => String -> a
error (String
"length mismatch: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs1) forall a. [a] -> [a] -> [a]
++ String
" and " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs2))
  | Bool
otherwise = [Int] -> [Int] -> Formula
f (forall (v :: * -> *) a. Vector v a => v a -> [a]
VG.toList (forall (v :: * -> *) a. Vector v a => v a -> v a
VG.reverse Vector Int
bs1)) (forall (v :: * -> *) a. Vector v a => v a -> [a]
VG.toList (forall (v :: * -> *) a. Vector v a => v a -> v a
VG.reverse Vector Int
bs2))
  where
    f :: [Int] -> [Int] -> Formula
f [] [] = forall a. MonotoneBoolean a => a
false
    f (Int
b1:[Int]
bs1) (Int
b2:[Int]
bs2) =
      (forall a. Complement a => a -> a
notB (Int -> Formula
Atom Int
b1) forall a. MonotoneBoolean a => a -> a -> a
.&&. Int -> Formula
Atom Int
b2) forall a. MonotoneBoolean a => a -> a -> a
.||. ((Int -> Formula
Atom Int
b1 forall a. Boolean a => a -> a -> a
.=>. Int -> Formula
Atom Int
b2) forall a. MonotoneBoolean a => a -> a -> a
.&&. [Int] -> [Int] -> Formula
f [Int]
bs1 [Int]
bs2)
    f [Int]
_ [Int]
_ = 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
  | forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs1 forall a. Eq a => a -> a -> Bool
/= forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs2 = forall a. HasCallStack => String -> a
error (String
"length mismatch: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs1) forall a. [a] -> [a] -> [a]
++ String
" and " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs2))
  | Int
w forall a. Eq a => a -> a -> Bool
== Int
0 = forall a. MonotoneBoolean a => a
false
  | Bool
otherwise =
      Int -> Formula
Atom Int
bs1_msb forall a. MonotoneBoolean a => a -> a -> a
.&&. Formula -> Formula
Not (Int -> Formula
Atom Int
bs2_msb)
      forall a. MonotoneBoolean a => a -> a -> a
.||. (Int -> Formula
Atom Int
bs1_msb forall a. Boolean a => a -> a -> a
.<=>. Int -> Formula
Atom Int
bs2_msb) forall a. MonotoneBoolean a => a -> a -> a
.&&. Vector Int -> Vector Int -> Formula
isULT Vector Int
bs1 Vector Int
bs2
  where
    w :: Int
w = forall (v :: * -> *) a. Vector v a => v a -> Int
VG.length Vector Int
bs1
    bs1_msb :: Int
bs1_msb = Vector Int
bs1 forall (v :: * -> *) a. Vector v a => v a -> Int -> a
VG.! (Int
wforall a. Num a => a -> a -> a
-Int
1)
    bs2_msb :: Int
bs2_msb = Vector Int
bs2 forall (v :: * -> *) a. Vector v a => v a -> Int -> a
VG.! (Int
wforall 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 forall e r. IsEqRel e r => e -> e -> r
.==. forall a. IsBV a => Int -> Integer -> a
nat2bv Int
8 Integer
6) forall a. Maybe a
Nothing
  forall a. Show a => a -> IO ()
print 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
  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 = 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 forall e r. IsEqRel e r => e -> e -> r
./=. Op2 -> Expr -> Expr -> Expr
EOp2 Op2
OpUDiv Expr
v2 Expr
z) forall a. Maybe a
Nothing
  Solver -> Atom -> Maybe Int -> IO ()
assertAtom Solver
solver (Expr
v1 forall e r. IsEqRel e r => e -> e -> r
.==. Expr
v2) forall a. Maybe a
Nothing
  forall a. Show a => a -> IO ()
print forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Solver -> IO Bool
check Solver
solver -- False