msakai / toysolver / 814

Committed 18 Jun 2026 04:19PM UTC coverage: 70.999% (+0.6%) from 70.362%

Build # 814

Build Type

push

github

Committed by

web-flow

Commit Message

update CHANGELOG

Coverage Stats

11374 of 16020 relevant lines covered (71.0%)

0.71 hits per line

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

86.25

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

msakai / toysolver / 814

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