msakai / toysolver / 810

Committed 18 Jun 2026 03:18AM UTC coverage: 71.026% (+0.3%) from 70.748%

Build # 810

Build Type

push

github

Committed by

web-flow

Commit Message

Merge f349d3ac5 into 040480525

Coverage Stats

4 of 7 new or added lines in 2 files covered. (57.14%)

42 existing lines in 13 files now uncovered.

11379 of 16021 relevant lines covered (71.03%)

0.71 hits per line

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

86.56

/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))
  , 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
  atomTable <- newIORef Map.empty
  contexts <- Vec.new
  Vec.push contexts IntMap.empty
  return $
    Solver
    { svVars = vars
    , svSATSolver = sat
    , svTseitin = tseitin
    , svEncTable = table
    , 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]
  return env

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

msakai / toysolver / 810

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