msakai / toysolver / 724

Committed 01 May 2025 12:26AM UTC coverage: 71.64% (-0.2%) from 71.828%

Build # 724

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #183 from msakai/feature/get-base-extension

Rename getBaseExt to getBaseExtension

Run Details

0 of 2 new or added lines in 1 file covered. (0.0%)

58 existing lines in 12 files now uncovered.

11049 of 15423 relevant lines covered (71.64%)

0.72 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

86.84

/src/ToySolver/BitVector/Solver.hs

{-# 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
  { svVars :: Vec.Vec (VU.Vector SAT.Lit)
  , svSATSolver :: SAT.Solver
  , svTseitin :: Tseitin.Encoder IO
  , svEncTable :: IORef (Map Expr (VU.Vector SAT.Lit))
  , svDivRemTable :: IORef [(VU.Vector SAT.Lit, VU.Vector SAT.Lit, VU.Vector SAT.Lit, VU.Vector SAT.Lit)]
  , svAtomTable :: IORef (Map NormalizedAtom SAT.Lit)
  , svContexts :: Vec.Vec (IntMap (Maybe Int))
  }

newSolver :: IO Solver
newSolver = do
  vars <- Vec.new
  sat <- SAT.newSolver
  tseitin <- Tseitin.newEncoder sat
  table <- newIORef Map.empty
  divRemTable <- newIORef []
  atomTable <- newIORef Map.empty
  contexts <- Vec.new
  Vec.push contexts IntMap.empty
  return $
    Solver
    { svVars = vars
    , svSATSolver = sat
    , svTseitin = tseitin
    , svEncTable = table
    , svDivRemTable = divRemTable
    , svAtomTable = atomTable
    , svContexts = contexts
    }

newVar :: Solver -> Int -> IO Expr
newVar solver w = EVar <$> newVar' solver w

newVar' :: Solver -> Int -> IO Var
newVar' solver w = do
  bs <- VG.fromList <$> SAT.newVars (svSATSolver solver) w
  v <- Vec.getSize $ svVars solver
  Vec.push (svVars solver) bs
  return $ Var{ varWidth = w, varId = v }

data NormalizedRel = NRSLt | NRULt | NREql
  deriving (Eq, Ord, Enum, Bounded, Show)

data NormalizedAtom = NormalizedAtom NormalizedRel Expr Expr
  deriving (Eq, Ord, Show)

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

assertAtom :: Solver -> Atom -> Maybe Int -> IO ()
assertAtom solver atom label = do
  let (atom'@(NormalizedAtom op lhs rhs), polarity) = normalizeAtom atom
  table <- readIORef (svAtomTable solver)
  l <- (if polarity then id else negate) <$>
    case Map.lookup atom' table of
      Just lit -> return lit
      Nothing -> do
        s <- encodeExpr solver lhs
        t <- encodeExpr solver rhs
        l <- Tseitin.encodeFormula (svTseitin solver) $
          case op of
            NRULt -> isULT s t
            NRSLt -> isSLT s t
            NREql -> isEQ s t
        writeIORef (svAtomTable solver) $ Map.insert atom' l table
        return l
  size <- Vec.getSize (svContexts solver)
  case label of
    Nothing | size == 1 -> SAT.addClause (svTseitin solver) [l]
    _ -> do
      Vec.modify (svContexts solver) (size - 1) (IntMap.insert l label)

check :: Solver -> IO Bool
check solver = do
  size <- Vec.getSize (svContexts solver)
  m <- Vec.read (svContexts solver) (size - 1)
  b <- SAT.solveWith (svSATSolver solver) (IntMap.keys m)
  return b

getModel :: Solver -> IO Model
getModel solver = do
  m <- SAT.getModel (svSATSolver solver)
  vss <- Vec.getElems (svVars solver)
  let f = fromAscBits . map (SAT.evalLit m) . VG.toList
      isZero' = not . or . toAscBits
      env = VG.fromList [f vs | vs <- vss]
  xs <- readIORef (svDivRemTable solver)
  let divTable = Map.fromList [(f s, f d) | (s,t,d,_r) <- xs, isZero' (f t)]
      remTable = Map.fromList [(f s, f r) | (s,t,_d,r) <- xs, isZero' (f t)]
  return (env, divTable, remTable)

explain :: Solver -> IO IntSet
explain solver = do
  xs <- SAT.getFailedAssumptions (svSATSolver solver)
  size <- Vec.getSize (svContexts solver)
  m <- Vec.read (svContexts solver) (size - 1)
  return $ IntSet.fromList $ catMaybes $ IntMap.elems $ IntMap.restrictKeys m xs

pushBacktrackPoint :: Solver -> IO ()
pushBacktrackPoint solver = do
  size <- Vec.getSize (svContexts solver)
  m <- Vec.read (svContexts solver) (size - 1)
  Vec.push (svContexts solver) m

popBacktrackPoint :: Solver -> IO ()
popBacktrackPoint solver = do
  _ <- Vec.pop (svContexts solver)
  return ()

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

type SBV = VU.Vector SAT.Lit

encodeExpr :: Solver -> Expr -> IO SBV
encodeExpr solver = enc
  where
    enc e@(EConst _) = enc' e
    enc e@(EVar _) = enc' e
    enc e = do
      table <- readIORef (svEncTable solver)
      case Map.lookup e table of
        Just vs -> return vs
        Nothing -> do
          vs <- enc' e
          modifyIORef (svEncTable solver) (Map.insert e vs)
          return vs

    enc' (EConst bs) =
      liftM VU.fromList $ forM (toAscBits bs) $ \b ->
        if b
        then Tseitin.encodeConj (svTseitin solver) []
        else Tseitin.encodeDisj (svTseitin solver) []
    enc' (EVar v) = Vec.read (svVars solver) (varId v)
    enc' (EOp1 op arg) = do
      arg' <- enc arg
      case op of
        OpExtract i j -> do
          unless (VG.length arg' > i && i >= j && j >= 0) $
            error ("invalid extract " ++ show (i,j) ++ " on bit-vector of length " ++ show (VG.length arg') ++ " : " ++ show arg)
          return $ VG.slice j (i - j + 1) arg'
        OpNot -> return $ VG.map negate arg'
        OpNeg -> encodeNegate (svTseitin solver) arg'
    enc' (EOp2 op arg1 arg2) = do
      arg1' <- enc arg1
      arg2' <- enc arg2
      case op of
        OpConcat -> return (arg2' <> arg1')
        OpAnd -> VG.zipWithM (\l1 l2 -> Tseitin.encodeConj (svTseitin solver) [l1,l2]) arg1' arg2'
        OpOr  -> VG.zipWithM (\l1 l2 -> Tseitin.encodeDisj (svTseitin solver) [l1,l2]) arg1' arg2'
        OpXOr -> VG.zipWithM (Tseitin.encodeXOR (svTseitin solver)) arg1' arg2'
        OpComp -> VG.singleton <$> Tseitin.encodeFormula (svTseitin solver) (isEQ arg1' arg2')
        OpAdd -> encodeSum (svTseitin solver) (VG.length arg1') True [arg1', arg2']
        OpMul -> encodeMul (svTseitin solver) True arg1' arg2'
        OpUDiv -> fst <$> encodeDivRem solver arg1' arg2'
        OpURem -> snd <$> encodeDivRem solver arg1' arg2'
        OpSDiv -> encodeSDiv solver arg1' arg2'
        OpSRem -> encodeSRem solver arg1' arg2'
        OpSMod -> encodeSMod solver arg1' arg2'
        OpShl  -> encodeShl (svTseitin solver) arg1' arg2'
        OpLShr -> encodeLShr (svTseitin solver) arg1' arg2'
        OpAShr -> encodeAShr (svTseitin solver) arg1' arg2'

encodeMul :: Tseitin.Encoder IO -> Bool -> SBV -> SBV -> IO SBV
encodeMul enc allowOverflow arg1 arg2 = do
  let w = VG.length arg1
  b0 <- Tseitin.encodeDisj enc [] -- False
  bss <- forM (zip [0..] (VG.toList arg2)) $ \(i,b2) -> do
    let arg1' = if allowOverflow
                then VG.take (w - i) arg1
                else arg1
    bs <- VG.forM arg1' $ \b1 -> do
            Tseitin.encodeConj enc [b1,b2]
    return (VG.replicate i b0 <> bs)
  encodeSum enc w allowOverflow bss

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

  forM_ xss $ \xs -> do
    VG.imapM insert xs

  let loop i ret
        | i >= w = do
            unless allowOverflow $ do
              bs <- readIORef buckets
              forM_ (F.toList bs) $ \q -> do
                ls <- SQ.dequeueBatch q
                forM_ ls $ \l -> do
                  SAT.addClause  enc [-l]
            return (reverse ret)
        | otherwise = do
            bs <- readIORef buckets
            let n = Seq.length bs
            if i >= n then do
              b <- Tseitin.encodeDisj enc [] -- False
              loop (i+1) (b : ret)
            else do
              let q = Seq.index bs i
              m <- SQ.queueSize q
              case m of
                0 -> do
                  b <- Tseitin.encodeDisj enc [] -- False
                  loop (i+1) (b : ret)
                1 -> do
                  Just b <- SQ.dequeue q
                  loop (i+1) (b : ret)
                2 -> do
                  Just b1 <- SQ.dequeue q
                  Just b2 <- SQ.dequeue q
                  s <- encodeHASum enc b1 b2
                  c <- encodeHACarry enc b1 b2
                  insert (i+1) c
                  loop (i+1) (s : ret)
                _ -> do
                  Just b1 <- SQ.dequeue q
                  Just b2 <- SQ.dequeue q
                  Just b3 <- SQ.dequeue q
                  s <- Tseitin.encodeFASum enc b1 b2 b3
                  c <- Tseitin.encodeFACarry enc b1 b2 b3
                  insert i s
                  insert (i+1) c
                  loop i ret
  VU.fromList <$> loop 0 []

encodeHASum :: Tseitin.Encoder IO -> SAT.Lit -> SAT.Lit -> IO SAT.Lit
encodeHASum = Tseitin.encodeXOR

encodeHACarry :: Tseitin.Encoder IO -> SAT.Lit -> SAT.Lit -> IO SAT.Lit
encodeHACarry enc a b = Tseitin.encodeConj enc [a,b]

encodeNegate :: Tseitin.Encoder IO -> SBV -> IO SBV
encodeNegate enc s = do
  let f _ [] ret = return $ VU.fromList $ reverse ret
      f b (x:xs) ret = do
        y <- Tseitin.encodeITE enc b (- x) x
        b' <- Tseitin.encodeDisj enc [b, x]
        f b' xs (y : ret)
  b0 <- Tseitin.encodeDisj enc []
  f b0 (VG.toList s) []

encodeAbs :: Tseitin.Encoder IO -> SBV -> IO SBV
encodeAbs enc s = do
  let w = VG.length s
  if w == 0 then
    return VG.empty
  else do
    let msb_s = VG.last s
    r <- VG.fromList <$> SAT.newVars enc w
    t <- encodeNegate enc s
    Tseitin.addFormula enc $
      ite (Atom (-msb_s)) (isEQ r s) (isEQ r t)
    return r

encodeShl :: Tseitin.Encoder IO -> SBV -> SBV -> IO SBV
encodeShl enc s t = do
  let w = VG.length s
  when (w /= VG.length t) $ error "invalid width"
  b0 <- Tseitin.encodeDisj enc [] -- False
  let go bs (i,b) =
        VG.generateM w $ \j -> do
          let k = toInteger j - 2^i
              t = if k >= 0 then bs VG.! fromInteger k else b0
              e = bs VG.! j
          Tseitin.encodeITE enc b t e
  foldM go s (zip [(0::Int)..] (VG.toList t))

encodeLShr :: Tseitin.Encoder IO -> SBV -> SBV -> IO SBV
encodeLShr enc s t = do
  let w = VG.length s
  when (w /= VG.length t) $ error "invalid width"
  b0 <- Tseitin.encodeDisj enc [] -- False
  let go bs (i,b) =
        VG.generateM w $ \j -> do
          let k = toInteger j + 2^i
              t = if k < fromIntegral (VG.length bs) then bs VG.! fromInteger k else b0
              e = bs VG.! j
          Tseitin.encodeITE enc b t e
  foldM go s (zip [(0::Int)..] (VG.toList t))

encodeAShr :: Tseitin.Encoder IO -> SBV -> SBV -> IO SBV
encodeAShr enc s t = do
  let w = VG.length s
  when (w /= VG.length t) $ error "invalid width"
  if w == 0 then
    return VG.empty
  else do
    let msb_s = VG.last s
    r <- VG.fromList <$> SAT.newVars enc w
    s' <- encodeNegate enc s
    a <- encodeLShr enc s t
    b <- encodeNegate enc =<< encodeLShr enc s' t
    Tseitin.addFormula enc $
      ite (Atom (-msb_s)) (isEQ r a) (isEQ r b)
    return r

encodeDivRem :: Solver -> SBV -> SBV -> IO (SBV, SBV)
encodeDivRem solver s t = do
  let w = VG.length s
  d <- VG.fromList <$> SAT.newVars (svSATSolver solver) w
  r <- VG.fromList <$> SAT.newVars (svSATSolver solver) w
  c <- do
    tmp <- encodeMul (svTseitin solver) False d t
    encodeSum (svTseitin solver) w False [tmp, r]
  tbl <- readIORef (svDivRemTable solver)
  Tseitin.addFormula (svTseitin solver) $
    ite (isZero t)
        (And [(isEQ s s' .&&. isZero t') .=>. (isEQ d d' .&&. isEQ r r') | (s',t',d',r') <- tbl, w == VG.length s'])
        (isEQ s c .&&. isULT r t)
  modifyIORef (svDivRemTable solver) ((s,t,d,r) :)
  return (d,r)

encodeSDiv :: Solver -> SBV -> SBV -> IO SBV
encodeSDiv solver s t = do
  let w = VG.length s
  when (w /= VG.length t) $ error "invalid width"
  if w == 0 then
    return VG.empty
  else do
    s' <- encodeNegate (svTseitin solver) s
    t' <- encodeNegate (svTseitin solver) t
    let msb_s = VG.last s
        msb_t = VG.last t
    r <- VG.fromList <$> SAT.newVars (svSATSolver solver) w
    let f x y = fst <$> encodeDivRem solver x y
    a <- f s t
    b <- encodeNegate (svTseitin solver) =<< f s' t
    c <- encodeNegate (svTseitin solver) =<< f s t'
    d <- f s' t'
    Tseitin.addFormula (svTseitin solver) $
      ite (Atom (-msb_s) .&&. Atom (-msb_t)) (isEQ r a) $
      ite (Atom msb_s .&&. Atom (-msb_t)) (isEQ r b) $
      ite (Atom (-msb_s) .&&. Atom msb_t) (isEQ r c) $
      (isEQ r d)
    return r

encodeSRem :: Solver -> SBV -> SBV -> IO SBV
encodeSRem solver s t = do
  let w = VG.length s
  when (w /= VG.length t) $ error "invalid width"
  if w == 0 then
    return VG.empty
  else do
    s' <- encodeNegate (svTseitin solver) s
    t' <- encodeNegate (svTseitin solver) t
    let msb_s = VG.last s
        msb_t = VG.last t
    r <- VG.fromList <$> SAT.newVars (svSATSolver solver) w
    let f x y = snd <$> encodeDivRem solver x y
    a <- f s t
    b <- encodeNegate (svTseitin solver) =<< f s' t
    c <- f s t'
    d <- encodeNegate (svTseitin solver) =<< f s' t'
    Tseitin.addFormula (svTseitin solver) $
      ite (Atom (-msb_s) .&&. Atom (-msb_t)) (isEQ r a) $
      ite (Atom msb_s .&&. Atom (-msb_t)) (isEQ r b) $
      ite (Atom (-msb_s) .&&. Atom msb_t) (isEQ r c) $
      (isEQ r d)
    return r

encodeSMod :: Solver -> SBV -> SBV -> IO SBV
encodeSMod solver s t = do
  let w = VG.length s
  when (w /= VG.length t) $ error "invalid width"
  if w == 0 then
    return VG.empty
  else do
    let msb_s = VG.last s
        msb_t = VG.last t
    r <- VG.fromList <$> SAT.newVars (svSATSolver solver) w
    abs_s <- encodeAbs (svTseitin solver) s
    abs_t <- encodeAbs (svTseitin solver) t
    u <- snd <$> encodeDivRem solver abs_s abs_t
    u' <- encodeNegate (svTseitin solver) u
    a <- encodeSum (svTseitin solver) w True [u', t]
    b <- encodeSum (svTseitin solver) w True [u, t]
    Tseitin.addFormula (svTseitin solver) $
      ite (isZero u .||. (Atom (-msb_s) .&&. Atom (-msb_t))) (isEQ r u) $
      ite (Atom msb_s .&&. Atom (-msb_t)) (isEQ r a) $
      ite (Atom (-msb_s) .&&. Atom msb_t) (isEQ r b) $
      (isEQ r u')
    return r

isZero :: SBV -> Tseitin.Formula
isZero bs = And [Not (Atom b) | b <- VG.toList bs]

isEQ :: SBV -> SBV -> Tseitin.Formula
isEQ bs1 bs2
  | VG.length bs1 /= VG.length bs2 = error ("length mismatch: " ++ show (VG.length bs1) ++ " and " ++ show (VG.length bs2))
  | otherwise = And [Equiv (Atom b1) (Atom b2) | (b1,b2) <- zip (VG.toList bs1) (VG.toList bs2)]

isULT :: SBV -> SBV -> Tseitin.Formula
isULT bs1 bs2
  | VG.length bs1 /= VG.length bs2 = error ("length mismatch: " ++ show (VG.length bs1) ++ " and " ++ show (VG.length bs2))
  | otherwise = f (VG.toList (VG.reverse bs1)) (VG.toList (VG.reverse bs2))
  where
    f [] [] = false
    f (b1:bs1) (b2:bs2) =
      (notB (Atom b1) .&&. Atom b2) .||. ((Atom b1 .=>. Atom b2) .&&. f bs1 bs2)
    f _ _ = error "should not happen"

isSLT :: SBV -> SBV -> Tseitin.Formula
isSLT bs1 bs2
  | VG.length bs1 /= VG.length bs2 = error ("length mismatch: " ++ show (VG.length bs1) ++ " and " ++ show (VG.length bs2))
  | w == 0 = false
  | otherwise =
      Atom bs1_msb .&&. Not (Atom bs2_msb)
      .||. (Atom bs1_msb .<=>. Atom bs2_msb) .&&. isULT bs1 bs2
  where
    w = VG.length bs1
    bs1_msb = bs1 VG.! (w-1)
    bs2_msb = bs2 VG.! (w-1)

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

_test1 :: IO ()
_test1 = do
  solver <- newSolver
  v1 <- newVar solver 8
  v2 <- newVar solver 8
  assertAtom solver (EOp2 OpMul v1 v2 .==. nat2bv 8 6) Nothing
  print =<< check solver
  m <- getModel solver
  print m

_test2 :: IO ()
_test2 = do
  solver <- newSolver
  v1 <- newVar solver 8
  v2 <- newVar solver 8
  let z = nat2bv 8 0
  assertAtom solver (EOp2 OpUDiv v1 z ./=. EOp2 OpUDiv v2 z) Nothing
  assertAtom solver (v1 .==. v2) Nothing
  print =<< check solver -- False

1	{-# OPTIONS_GHC -Wall #-}
2	{-# OPTIONS_HADDOCK show-extensions #-}
3	{-# LANGUAGE FlexibleContexts #-}
4	{-# LANGUAGE ScopedTypeVariables #-}
5	-----------------------------------------------------------------------------
6	-- \|
7	-- Module : ToySolver.BitVector.Solver
8	-- Copyright : (c) Masahiro Sakai 2016
9	-- License : BSD-style
10	--
11	-- Maintainer : masahiro.sakai@gmail.com
12	-- Stability : experimental
13	-- Portability : non-portable
14	--
15	-----------------------------------------------------------------------------
16	module ToySolver.BitVector.Solver
17	(
18	-- * BitVector solver
19	Solver
20	, newSolver
21	, newVar
22	, newVar'
23	, assertAtom
24	, check
25	, getModel
26	, explain
27	, pushBacktrackPoint
28	, popBacktrackPoint
29	) where
30
31	import Prelude hiding (repeat)
32	import Control.Monad
33	import qualified Data.Foldable as F
34	import Data.IntMap (IntMap)
35	import qualified Data.IntMap as IntMap
36	import Data.IntSet (IntSet)
37	import qualified Data.IntSet as IntSet
38	import Data.IORef
39	import Data.Map (Map)
40	import qualified Data.Map as Map
41	import Data.Maybe
42	import qualified Data.Vector.Generic as VG
43	import qualified Data.Vector.Unboxed as VU
44	import Data.Sequence (Seq)
45	import qualified Data.Sequence as Seq
46	import ToySolver.Data.Boolean
47	import ToySolver.Data.OrdRel
48	import qualified ToySolver.Internal.Data.SeqQueue as SQ
49	import qualified ToySolver.Internal.Data.Vec as Vec
50	import qualified ToySolver.SAT as SAT
51	import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
52	import ToySolver.SAT.Encoder.Tseitin (Formula (..))
53
54	import ToySolver.BitVector.Base
55
56	-- ------------------------------------------------------------------------
57
58	data Solver
59	= Solver
60	{ svVars :: Vec.Vec (VU.Vector SAT.Lit)	1✔
61	, svSATSolver :: SAT.Solver	1✔
62	, svTseitin :: Tseitin.Encoder IO	1✔
63	, svEncTable :: IORef (Map Expr (VU.Vector SAT.Lit))	1✔
64	, svDivRemTable :: IORef [(VU.Vector SAT.Lit, VU.Vector SAT.Lit, VU.Vector SAT.Lit, VU.Vector SAT.Lit)]	1✔
65	, svAtomTable :: IORef (Map NormalizedAtom SAT.Lit)	1✔
66	, svContexts :: Vec.Vec (IntMap (Maybe Int))	1✔
67	}
68
69	newSolver :: IO Solver
70	newSolver = do	1✔
71	vars <- Vec.new	1✔
72	sat <- SAT.newSolver	1✔
73	tseitin <- Tseitin.newEncoder sat	1✔
74	table <- newIORef Map.empty	1✔
75	divRemTable <- newIORef []	1✔
76	atomTable <- newIORef Map.empty	1✔
77	contexts <- Vec.new	1✔
78	Vec.push contexts IntMap.empty	1✔
79	return $	1✔
80	Solver	1✔
81	{ svVars = vars	1✔
82	, svSATSolver = sat	1✔
83	, svTseitin = tseitin	1✔
84	, svEncTable = table	1✔
85	, svDivRemTable = divRemTable	1✔
86	, svAtomTable = atomTable	1✔
87	, svContexts = contexts	1✔
88	}
89
90	newVar :: Solver -> Int -> IO Expr
91	newVar solver w = EVar <$> newVar' solver w	1✔
92
93	newVar' :: Solver -> Int -> IO Var
94	newVar' solver w = do	1✔
95	bs <- VG.fromList <$> SAT.newVars (svSATSolver solver) w	1✔
96	v <- Vec.getSize $ svVars solver	1✔
97	Vec.push (svVars solver) bs	1✔
98	return $ Var{ varWidth = w, varId = v }	1✔
99
100	data NormalizedRel = NRSLt \| NRULt \| NREql
101	deriving (Eq, Ord, Enum, Bounded, Show)	×
102
103	data NormalizedAtom = NormalizedAtom NormalizedRel Expr Expr
104	deriving (Eq, Ord, Show)	×
105
106	normalizeAtom :: Atom -> (NormalizedAtom, Bool)
107	normalizeAtom (Rel (OrdRel lhs op rhs) True) =	1✔
108	case op of	1✔
109	Lt -> (NormalizedAtom NRSLt lhs rhs, True)	1✔
110	Gt -> (NormalizedAtom NRSLt rhs lhs, True)	1✔
111	Le -> (NormalizedAtom NRSLt rhs lhs, False)	1✔
112	Ge -> (NormalizedAtom NRSLt lhs rhs, False)	1✔
113	Eql -> (NormalizedAtom NREql lhs rhs, True)	1✔
114	NEq -> (NormalizedAtom NREql lhs rhs, False)	1✔
115	normalizeAtom (Rel (OrdRel lhs op rhs) False) =
116	case op of	1✔
117	Lt -> (NormalizedAtom NRULt lhs rhs, True)	1✔
118	Gt -> (NormalizedAtom NRULt rhs lhs, True)	1✔
119	Le -> (NormalizedAtom NRULt rhs lhs, False)	1✔
120	Ge -> (NormalizedAtom NRULt lhs rhs, False)	1✔
121	Eql -> (NormalizedAtom NREql lhs rhs, True)	1✔
122	NEq -> (NormalizedAtom NREql lhs rhs, False)	1✔
123
124	assertAtom :: Solver -> Atom -> Maybe Int -> IO ()
125	assertAtom solver atom label = do	1✔
126	let (atom'@(NormalizedAtom op lhs rhs), polarity) = normalizeAtom atom	1✔
127	table <- readIORef (svAtomTable solver)	1✔
128	l <- (if polarity then id else negate) <$>	1✔
129	case Map.lookup atom' table of	1✔
130	Just lit -> return lit	1✔
131	Nothing -> do	1✔
132	s <- encodeExpr solver lhs	1✔
133	t <- encodeExpr solver rhs	1✔
134	l <- Tseitin.encodeFormula (svTseitin solver) $	1✔
135	case op of	1✔
136	NRULt -> isULT s t	1✔
137	NRSLt -> isSLT s t	1✔
138	NREql -> isEQ s t	1✔
139	writeIORef (svAtomTable solver) $ Map.insert atom' l table	1✔
140	return l	1✔
141	size <- Vec.getSize (svContexts solver)	1✔
142	case label of	1✔
143	Nothing \| size == 1 -> SAT.addClause (svTseitin solver) [l]	×
144	_ -> do	1✔
145	Vec.modify (svContexts solver) (size - 1) (IntMap.insert l label)	1✔
146
147	check :: Solver -> IO Bool
148	check solver = do	1✔
149	size <- Vec.getSize (svContexts solver)	1✔
150	m <- Vec.read (svContexts solver) (size - 1)	1✔
151	b <- SAT.solveWith (svSATSolver solver) (IntMap.keys m)	1✔
152	return b	1✔
153
154	getModel :: Solver -> IO Model
155	getModel solver = do	1✔
156	m <- SAT.getModel (svSATSolver solver)	1✔
157	vss <- Vec.getElems (svVars solver)	1✔
158	let f = fromAscBits . map (SAT.evalLit m) . VG.toList	1✔
159	isZero' = not . or . toAscBits	1✔
160	env = VG.fromList [f vs \| vs <- vss]	1✔
161	xs <- readIORef (svDivRemTable solver)	1✔
UNCOV 162	let divTable = Map.fromList [(f s, f d) \| (s,t,d,_r) <- xs, isZero' (f t)]	×
163	remTable = Map.fromList [(f s, f r) \| (s,t,_d,r) <- xs, isZero' (f t)]	1✔
164	return (env, divTable, remTable)	1✔
165
166	explain :: Solver -> IO IntSet
167	explain solver = do	1✔
168	xs <- SAT.getFailedAssumptions (svSATSolver solver)	1✔
169	size <- Vec.getSize (svContexts solver)	1✔
170	m <- Vec.read (svContexts solver) (size - 1)	1✔
171	return $ IntSet.fromList $ catMaybes $ IntMap.elems $ IntMap.restrictKeys m xs	1✔
172
173	pushBacktrackPoint :: Solver -> IO ()
174	pushBacktrackPoint solver = do	1✔
175	size <- Vec.getSize (svContexts solver)	1✔
176	m <- Vec.read (svContexts solver) (size - 1)	1✔
177	Vec.push (svContexts solver) m	1✔
178
179	popBacktrackPoint :: Solver -> IO ()
180	popBacktrackPoint solver = do	1✔
181	_ <- Vec.pop (svContexts solver)	1✔
182	return ()	×
183
184	-- ------------------------------------------------------------------------
185
186	type SBV = VU.Vector SAT.Lit
187
188	encodeExpr :: Solver -> Expr -> IO SBV
189	encodeExpr solver = enc	1✔
190	where
191	enc e@(EConst _) = enc' e	1✔
192	enc e@(EVar _) = enc' e	1✔
193	enc e = do	1✔
194	table <- readIORef (svEncTable solver)	1✔
195	case Map.lookup e table of	1✔
196	Just vs -> return vs	1✔
197	Nothing -> do	1✔
198	vs <- enc' e	1✔
199	modifyIORef (svEncTable solver) (Map.insert e vs)	1✔
200	return vs	1✔
201
202	enc' (EConst bs) =	1✔
203	liftM VU.fromList $ forM (toAscBits bs) $ \b ->	1✔
204	if b	1✔
205	then Tseitin.encodeConj (svTseitin solver) []	1✔
206	else Tseitin.encodeDisj (svTseitin solver) []	1✔
207	enc' (EVar v) = Vec.read (svVars solver) (varId v)	1✔
208	enc' (EOp1 op arg) = do	1✔
209	arg' <- enc arg	1✔
210	case op of	1✔
211	OpExtract i j -> do	1✔
212	unless (VG.length arg' > i && i >= j && j >= 0) $	1✔
213	error ("invalid extract " ++ show (i,j) ++ " on bit-vector of length " ++ show (VG.length arg') ++ " : " ++ show arg)	×
214	return $ VG.slice j (i - j + 1) arg'	1✔
215	OpNot -> return $ VG.map negate arg'	1✔
216	OpNeg -> encodeNegate (svTseitin solver) arg'	1✔
217	enc' (EOp2 op arg1 arg2) = do	1✔
218	arg1' <- enc arg1	1✔
219	arg2' <- enc arg2	1✔
220	case op of	1✔
221	OpConcat -> return (arg2' <> arg1')	1✔
222	OpAnd -> VG.zipWithM (\l1 l2 -> Tseitin.encodeConj (svTseitin solver) [l1,l2]) arg1' arg2'	1✔
223	OpOr -> VG.zipWithM (\l1 l2 -> Tseitin.encodeDisj (svTseitin solver) [l1,l2]) arg1' arg2'	1✔
224	OpXOr -> VG.zipWithM (Tseitin.encodeXOR (svTseitin solver)) arg1' arg2'	1✔
225	OpComp -> VG.singleton <$> Tseitin.encodeFormula (svTseitin solver) (isEQ arg1' arg2')	1✔
226	OpAdd -> encodeSum (svTseitin solver) (VG.length arg1') True [arg1', arg2']	1✔
227	OpMul -> encodeMul (svTseitin solver) True arg1' arg2'	1✔
228	OpUDiv -> fst <$> encodeDivRem solver arg1' arg2'	1✔
229	OpURem -> snd <$> encodeDivRem solver arg1' arg2'	1✔
230	OpSDiv -> encodeSDiv solver arg1' arg2'	1✔
231	OpSRem -> encodeSRem solver arg1' arg2'	1✔
232	OpSMod -> encodeSMod solver arg1' arg2'	1✔
233	OpShl -> encodeShl (svTseitin solver) arg1' arg2'	1✔
234	OpLShr -> encodeLShr (svTseitin solver) arg1' arg2'	1✔
235	OpAShr -> encodeAShr (svTseitin solver) arg1' arg2'	1✔
236
237	encodeMul :: Tseitin.Encoder IO -> Bool -> SBV -> SBV -> IO SBV
238	encodeMul enc allowOverflow arg1 arg2 = do	1✔
239	let w = VG.length arg1	1✔
240	b0 <- Tseitin.encodeDisj enc [] -- False	1✔
241	bss <- forM (zip [0..] (VG.toList arg2)) $ \(i,b2) -> do	1✔
242	let arg1' = if allowOverflow	1✔
243	then VG.take (w - i) arg1	1✔
244	else arg1	1✔
245	bs <- VG.forM arg1' $ \b1 -> do	1✔
246	Tseitin.encodeConj enc [b1,b2]	1✔
247	return (VG.replicate i b0 <> bs)	1✔
248	encodeSum enc w allowOverflow bss	1✔
249
250	encodeSum :: Tseitin.Encoder IO -> Int -> Bool -> [SBV] -> IO SBV
251	encodeSum enc w allowOverflow xss = do	1✔
252	(buckets :: IORef (Seq (SQ.SeqQueue IO SAT.Lit))) <- newIORef Seq.empty	1✔
253	let insert i x = do	1✔
254	bs <- readIORef buckets	1✔
255	let n = Seq.length bs	1✔
256	q <- if i < n then do	1✔
257	return $ Seq.index bs i	1✔
258	else do	1✔
259	qs <- replicateM (i+1 - n) SQ.newFifo	1✔
260	let bs' = bs Seq.>< Seq.fromList qs	1✔
261	writeIORef buckets bs'	1✔
262	return $ Seq.index bs' i	1✔
263	SQ.enqueue q x	1✔
264
265	forM_ xss $ \xs -> do	1✔
266	VG.imapM insert xs	1✔
267
268	let loop i ret	1✔
269	\| i >= w = do	1✔
270	unless allowOverflow $ do	1✔
271	bs <- readIORef buckets	1✔
272	forM_ (F.toList bs) $ \q -> do	1✔
273	ls <- SQ.dequeueBatch q	1✔
274	forM_ ls $ \l -> do	1✔
275	SAT.addClause enc [-l]	1✔
276	return (reverse ret)	1✔
277	\| otherwise = do	×
278	bs <- readIORef buckets	1✔
279	let n = Seq.length bs	1✔
280	if i >= n then do	×
281	b <- Tseitin.encodeDisj enc [] -- False	×
282	loop (i+1) (b : ret)	×
283	else do	1✔
284	let q = Seq.index bs i	1✔
285	m <- SQ.queueSize q	1✔
286	case m of	1✔
287	0 -> do	×
288	b <- Tseitin.encodeDisj enc [] -- False	×
289	loop (i+1) (b : ret)	×
290	1 -> do	1✔
291	Just b <- SQ.dequeue q	1✔
292	loop (i+1) (b : ret)	1✔
293	2 -> do	1✔
294	Just b1 <- SQ.dequeue q	1✔
295	Just b2 <- SQ.dequeue q	1✔
296	s <- encodeHASum enc b1 b2	1✔
297	c <- encodeHACarry enc b1 b2	1✔
298	insert (i+1) c	1✔
299	loop (i+1) (s : ret)	1✔
300	_ -> do	1✔
301	Just b1 <- SQ.dequeue q	1✔
302	Just b2 <- SQ.dequeue q	1✔
303	Just b3 <- SQ.dequeue q	1✔
304	s <- Tseitin.encodeFASum enc b1 b2 b3	1✔
305	c <- Tseitin.encodeFACarry enc b1 b2 b3	1✔
306	insert i s	1✔
307	insert (i+1) c	1✔
308	loop i ret	1✔
309	VU.fromList <$> loop 0 []	1✔
310
311	encodeHASum :: Tseitin.Encoder IO -> SAT.Lit -> SAT.Lit -> IO SAT.Lit
312	encodeHASum = Tseitin.encodeXOR	1✔
313
314	encodeHACarry :: Tseitin.Encoder IO -> SAT.Lit -> SAT.Lit -> IO SAT.Lit
315	encodeHACarry enc a b = Tseitin.encodeConj enc [a,b]	1✔
316
317	encodeNegate :: Tseitin.Encoder IO -> SBV -> IO SBV
318	encodeNegate enc s = do	1✔
319	let f _ [] ret = return $ VU.fromList $ reverse ret	1✔
320	f b (x:xs) ret = do	1✔
321	y <- Tseitin.encodeITE enc b (- x) x	1✔
322	b' <- Tseitin.encodeDisj enc [b, x]	1✔
323	f b' xs (y : ret)	1✔
324	b0 <- Tseitin.encodeDisj enc []	1✔
325	f b0 (VG.toList s) []	1✔
326
327	encodeAbs :: Tseitin.Encoder IO -> SBV -> IO SBV
328	encodeAbs enc s = do	1✔
329	let w = VG.length s	1✔
330	if w == 0 then	×
331	return VG.empty	×
332	else do	1✔
333	let msb_s = VG.last s	1✔
334	r <- VG.fromList <$> SAT.newVars enc w	1✔
335	t <- encodeNegate enc s	1✔
336	Tseitin.addFormula enc $	1✔
337	ite (Atom (-msb_s)) (isEQ r s) (isEQ r t)	1✔
338	return r	1✔
339
340	encodeShl :: Tseitin.Encoder IO -> SBV -> SBV -> IO SBV
341	encodeShl enc s t = do	1✔
342	let w = VG.length s	1✔
343	when (w /= VG.length t) $ error "invalid width"	×
344	b0 <- Tseitin.encodeDisj enc [] -- False	1✔
345	let go bs (i,b) =	1✔
346	VG.generateM w $ \j -> do	1✔
347	let k = toInteger j - 2^i	1✔
348	t = if k >= 0 then bs VG.! fromInteger k else b0	1✔
349	e = bs VG.! j	1✔
350	Tseitin.encodeITE enc b t e	1✔
351	foldM go s (zip [(0::Int)..] (VG.toList t))	1✔
352
353	encodeLShr :: Tseitin.Encoder IO -> SBV -> SBV -> IO SBV
354	encodeLShr enc s t = do	1✔
355	let w = VG.length s	1✔
356	when (w /= VG.length t) $ error "invalid width"	×
357	b0 <- Tseitin.encodeDisj enc [] -- False	1✔
358	let go bs (i,b) =	1✔
359	VG.generateM w $ \j -> do	1✔
360	let k = toInteger j + 2^i	1✔
361	t = if k < fromIntegral (VG.length bs) then bs VG.! fromInteger k else b0	1✔
362	e = bs VG.! j	1✔
363	Tseitin.encodeITE enc b t e	1✔
364	foldM go s (zip [(0::Int)..] (VG.toList t))	1✔
365
366	encodeAShr :: Tseitin.Encoder IO -> SBV -> SBV -> IO SBV
367	encodeAShr enc s t = do	1✔
368	let w = VG.length s	1✔
369	when (w /= VG.length t) $ error "invalid width"	×
370	if w == 0 then	1✔
371	return VG.empty	1✔
372	else do	1✔
373	let msb_s = VG.last s	1✔
374	r <- VG.fromList <$> SAT.newVars enc w	1✔
375	s' <- encodeNegate enc s	1✔
376	a <- encodeLShr enc s t	1✔
377	b <- encodeNegate enc =<< encodeLShr enc s' t	1✔
378	Tseitin.addFormula enc $	1✔
379	ite (Atom (-msb_s)) (isEQ r a) (isEQ r b)	1✔
380	return r	1✔
381
382	encodeDivRem :: Solver -> SBV -> SBV -> IO (SBV, SBV)
383	encodeDivRem solver s t = do	1✔
384	let w = VG.length s	1✔
385	d <- VG.fromList <$> SAT.newVars (svSATSolver solver) w	1✔
386	r <- VG.fromList <$> SAT.newVars (svSATSolver solver) w	1✔
387	c <- do	1✔
388	tmp <- encodeMul (svTseitin solver) False d t	1✔
389	encodeSum (svTseitin solver) w False [tmp, r]	1✔
390	tbl <- readIORef (svDivRemTable solver)	1✔
391	Tseitin.addFormula (svTseitin solver) $	1✔
392	ite (isZero t)	1✔
393	(And [(isEQ s s' .&&. isZero t') .=>. (isEQ d d' .&&. isEQ r r') \| (s',t',d',r') <- tbl, w == VG.length s'])	1✔
394	(isEQ s c .&&. isULT r t)	1✔
395	modifyIORef (svDivRemTable solver) ((s,t,d,r) :)	1✔
396	return (d,r)	1✔
397
398	encodeSDiv :: Solver -> SBV -> SBV -> IO SBV
399	encodeSDiv solver s t = do	1✔
400	let w = VG.length s	1✔
401	when (w /= VG.length t) $ error "invalid width"	×
402	if w == 0 then	×
403	return VG.empty	×
404	else do	1✔
405	s' <- encodeNegate (svTseitin solver) s	1✔
406	t' <- encodeNegate (svTseitin solver) t	1✔
407	let msb_s = VG.last s	1✔
408	msb_t = VG.last t	1✔
409	r <- VG.fromList <$> SAT.newVars (svSATSolver solver) w	1✔
410	let f x y = fst <$> encodeDivRem solver x y	1✔
411	a <- f s t	1✔
412	b <- encodeNegate (svTseitin solver) =<< f s' t	1✔
413	c <- encodeNegate (svTseitin solver) =<< f s t'	1✔
414	d <- f s' t'	1✔
415	Tseitin.addFormula (svTseitin solver) $	1✔
416	ite (Atom (-msb_s) .&&. Atom (-msb_t)) (isEQ r a) $	1✔
417	ite (Atom msb_s .&&. Atom (-msb_t)) (isEQ r b) $	1✔
418	ite (Atom (-msb_s) .&&. Atom msb_t) (isEQ r c) $	1✔
419	(isEQ r d)	1✔
420	return r	1✔
421
422	encodeSRem :: Solver -> SBV -> SBV -> IO SBV
423	encodeSRem solver s t = do	1✔
424	let w = VG.length s	1✔
425	when (w /= VG.length t) $ error "invalid width"	×
426	if w == 0 then	×
427	return VG.empty	×
428	else do	1✔
429	s' <- encodeNegate (svTseitin solver) s	1✔
430	t' <- encodeNegate (svTseitin solver) t	1✔
431	let msb_s = VG.last s	1✔
432	msb_t = VG.last t	1✔
433	r <- VG.fromList <$> SAT.newVars (svSATSolver solver) w	1✔
434	let f x y = snd <$> encodeDivRem solver x y	1✔
435	a <- f s t	1✔
436	b <- encodeNegate (svTseitin solver) =<< f s' t	1✔
437	c <- f s t'	1✔
438	d <- encodeNegate (svTseitin solver) =<< f s' t'	1✔
439	Tseitin.addFormula (svTseitin solver) $	1✔
440	ite (Atom (-msb_s) .&&. Atom (-msb_t)) (isEQ r a) $	1✔
441	ite (Atom msb_s .&&. Atom (-msb_t)) (isEQ r b) $	1✔
442	ite (Atom (-msb_s) .&&. Atom msb_t) (isEQ r c) $	1✔
443	(isEQ r d)	1✔
444	return r	1✔
445
446	encodeSMod :: Solver -> SBV -> SBV -> IO SBV
447	encodeSMod solver s t = do	1✔
448	let w = VG.length s	1✔
449	when (w /= VG.length t) $ error "invalid width"	×
450	if w == 0 then	×
451	return VG.empty	×
452	else do	1✔
453	let msb_s = VG.last s	1✔
454	msb_t = VG.last t	1✔
455	r <- VG.fromList <$> SAT.newVars (svSATSolver solver) w	1✔
456	abs_s <- encodeAbs (svTseitin solver) s	1✔
457	abs_t <- encodeAbs (svTseitin solver) t	1✔
458	u <- snd <$> encodeDivRem solver abs_s abs_t	1✔
459	u' <- encodeNegate (svTseitin solver) u	1✔
460	a <- encodeSum (svTseitin solver) w True [u', t]	1✔
461	b <- encodeSum (svTseitin solver) w True [u, t]	1✔
462	Tseitin.addFormula (svTseitin solver) $	1✔
463	ite (isZero u .\|\|. (Atom (-msb_s) .&&. Atom (-msb_t))) (isEQ r u) $	1✔
464	ite (Atom msb_s .&&. Atom (-msb_t)) (isEQ r a) $	1✔
465	ite (Atom (-msb_s) .&&. Atom msb_t) (isEQ r b) $	1✔
466	(isEQ r u')	1✔
467	return r	1✔
468
469	isZero :: SBV -> Tseitin.Formula
470	isZero bs = And [Not (Atom b) \| b <- VG.toList bs]	1✔
471
472	isEQ :: SBV -> SBV -> Tseitin.Formula
473	isEQ bs1 bs2	1✔
474	\| VG.length bs1 /= VG.length bs2 = error ("length mismatch: " ++ show (VG.length bs1) ++ " and " ++ show (VG.length bs2))	×
475	\| otherwise = And [Equiv (Atom b1) (Atom b2) \| (b1,b2) <- zip (VG.toList bs1) (VG.toList bs2)]	×
476
477	isULT :: SBV -> SBV -> Tseitin.Formula
478	isULT bs1 bs2	1✔
479	\| VG.length bs1 /= VG.length bs2 = error ("length mismatch: " ++ show (VG.length bs1) ++ " and " ++ show (VG.length bs2))	×
480	\| otherwise = f (VG.toList (VG.reverse bs1)) (VG.toList (VG.reverse bs2))	×
481	where
482	f [] [] = false	1✔
483	f (b1:bs1) (b2:bs2) =
484	(notB (Atom b1) .&&. Atom b2) .\|\|. ((Atom b1 .=>. Atom b2) .&&. f bs1 bs2)	1✔
485	f _ _ = error "should not happen"	×
486
487	isSLT :: SBV -> SBV -> Tseitin.Formula
488	isSLT bs1 bs2	1✔
489	\| VG.length bs1 /= VG.length bs2 = error ("length mismatch: " ++ show (VG.length bs1) ++ " and " ++ show (VG.length bs2))	×
490	\| w == 0 = false	1✔
491	\| otherwise =	×
492	Atom bs1_msb .&&. Not (Atom bs2_msb)	1✔
493	.\|\|. (Atom bs1_msb .<=>. Atom bs2_msb) .&&. isULT bs1 bs2	1✔
494	where
495	w = VG.length bs1	1✔
496	bs1_msb = bs1 VG.! (w-1)	1✔
497	bs2_msb = bs2 VG.! (w-1)	1✔
498
499	-- ------------------------------------------------------------------------
500
501	_test1 :: IO ()
502	_test1 = do	×
503	solver <- newSolver	×
504	v1 <- newVar solver 8	×
505	v2 <- newVar solver 8	×
506	assertAtom solver (EOp2 OpMul v1 v2 .==. nat2bv 8 6) Nothing	×
507	print =<< check solver	×
508	m <- getModel solver	×
509	print m	×
510
511	_test2 :: IO ()
512	_test2 = do	×
513	solver <- newSolver	×
514	v1 <- newVar solver 8	×
515	v2 <- newVar solver 8	×
516	let z = nat2bv 8 0	×
517	assertAtom solver (EOp2 OpUDiv v1 z ./=. EOp2 OpUDiv v2 z) Nothing	×
518	assertAtom solver (v1 .==. v2) Nothing	×
519	print =<< check solver -- False	×

msakai / toysolver / 724

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous