Skip to content

Commit

Permalink
Merge 9ab1b85 into f113b9e
Browse files Browse the repository at this point in the history
  • Loading branch information
@msakai
msakai committed Oct 7, 2021
2 parents f113b9e + 9ab1b85 commit de00f45
Show file tree
Hide file tree
Showing 12 changed files with 249 additions and 50 deletions.
3 changes: 1 addition & 2 deletions app/toyqbf.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,6 @@ import System.Exit
import System.IO

import ToySolver.Data.Boolean
import qualified ToySolver.Data.BoolExpr as BoolExpr
import qualified ToySolver.FileFormat.CNF as CNF
import qualified ToySolver.QBF as QBF
import ToySolver.Internal.Util (setEncodingChar8)
Expand Down Expand Up @@ -79,7 +78,7 @@ main = do
let nv = CNF.qdimacsNumVars qdimacs
nc = CNF.qdimacsNumClauses qdimacs
prefix' = QBF.quantifyFreeVariables nv [(q, IntSet.fromList xs) | (q,xs) <- CNF.qdimacsPrefix qdimacs]
matrix' = andB [orB [if lit > 0 then BoolExpr.Atom lit else notB (BoolExpr.Atom (abs lit)) | lit <- CNF.unpackClause clause] | clause <- CNF.qdimacsMatrix qdimacs]
matrix' = andB [orB [if lit > 0 then QBF.litToMatrix lit else notB (QBF.litToMatrix (abs lit)) | lit <- CNF.unpackClause clause] | clause <- CNF.qdimacsMatrix qdimacs]
(ans, certificate) <-
case map toLower (optAlgorithm opt) of
"naive" -> QBF.solveNaive nv prefix' matrix'
Expand Down
2 changes: 1 addition & 1 deletion src/ToySolver/BitVector/Solver.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,13 +43,13 @@ import qualified Data.Vector.Generic as VG
import qualified Data.Vector.Unboxed as VU
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import ToySolver.Data.BoolExpr
import ToySolver.Data.Boolean
import ToySolver.Data.OrdRel
import qualified ToySolver.Internal.Data.SeqQueue as SQ
import qualified ToySolver.Internal.Data.Vec as Vec
import qualified ToySolver.SAT as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import ToySolver.SAT.Encoder.Tseitin (Formula (..))

import ToySolver.BitVector.Base

Expand Down
2 changes: 1 addition & 1 deletion src/ToySolver/Converter/PB.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -86,10 +86,10 @@ import qualified Data.PseudoBoolean as PBFile
import ToySolver.Converter.Base
import qualified ToySolver.Converter.PB.Internal.Product as Product
import ToySolver.Converter.Tseitin
import ToySolver.Data.BoolExpr
import qualified ToySolver.FileFormat.CNF as CNF
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import ToySolver.SAT.Encoder.Tseitin (Formula (..))
import qualified ToySolver.SAT.Encoder.PB as PB
import qualified ToySolver.SAT.Encoder.PBNLC as PBNLC
import ToySolver.SAT.Store.CNF
Expand Down
62 changes: 33 additions & 29 deletions src/ToySolver/QBF.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ module ToySolver.QBF
, normalizePrefix
, quantifyFreeVariables
, Matrix
, litToMatrix
, solve
, solveNaive
, solveCEGAR
Expand All @@ -44,8 +45,6 @@ import Data.List (groupBy, foldl')
import Data.Maybe

import ToySolver.Data.Boolean
import ToySolver.Data.BoolExpr (BoolExpr)
import qualified ToySolver.Data.BoolExpr as BoolExpr
import ToySolver.FileFormat.CNF (Quantifier (..))
import qualified ToySolver.FileFormat.CNF as CNF
import qualified ToySolver.SAT as SAT
Expand Down Expand Up @@ -87,58 +86,63 @@ prefixStartWithE _ = False

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

type Matrix = BoolExpr SAT.Lit
type Matrix = Tseitin.Formula

litToMatrix :: SAT.Lit -> Matrix
litToMatrix = Tseitin.Atom

reduct :: Matrix -> LitSet -> Matrix
reduct m ls = BoolExpr.simplify $ m >>= s
reduct m ls = Tseitin.simplify $ Tseitin.fold s m
where
s l
| l `IntSet.member` ls = true
| (-l) `IntSet.member` ls = false
| otherwise = BoolExpr.Atom l
| otherwise = litToMatrix l

substVarMap :: Matrix -> VarMap Matrix -> Matrix
substVarMap m s = BoolExpr.simplify $ m >>= \l -> do
let v = abs l
(if l > 0 then id else notB) $ IntMap.findWithDefault (BoolExpr.Atom v) v s
substVarMap m s = Tseitin.simplify $ Tseitin.fold f m
where
f l = do
let v = abs l
(if l > 0 then id else notB) $ IntMap.findWithDefault (litToMatrix v) v s

-- XXX
prenexAnd :: (Int, Prefix, Matrix) -> (Int, Prefix, Matrix) -> (Int, Prefix, Matrix)
prenexAnd (nv1, prefix1, matrix1) (nv2, prefix2, matrix2) =
evalState (f [] IntSet.empty IntMap.empty IntMap.empty prefix1 prefix2) (nv1 `max` nv2)
where
f :: Prefix -> VarSet
-> VarMap (BoolExpr SAT.Lit) -> VarMap (BoolExpr SAT.Lit)
-> VarMap Tseitin.Formula -> VarMap Tseitin.Formula
-> Prefix -> Prefix
-> State Int (Int, Prefix, Matrix)
f prefix _bvs subst1 subst2 [] [] = do
nv <- get
return (nv, prefix, BoolExpr.simplify (substVarMap matrix1 subst1 .&&. substVarMap matrix2 subst2))
return (nv, prefix, Tseitin.simplify (substVarMap matrix1 subst1 .&&. substVarMap matrix2 subst2))
f prefix bvs subst1 subst2 ((A,xs1) : prefix1') ((A,xs2) : prefix2') = do
let xs = IntSet.union xs1 xs2
ys = IntSet.intersection bvs xs
nv <- get
put (nv + IntSet.size ys)
let s = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]
xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)
subst1' = fmap BoolExpr.Atom (IntMap.filterWithKey (\x _ -> x `IntSet.member` xs1) s) `IntMap.union` subst1
subst2' = fmap BoolExpr.Atom (IntMap.filterWithKey (\x _ -> x `IntSet.member` xs2) s) `IntMap.union` subst2
subst1' = fmap litToMatrix (IntMap.filterWithKey (\x _ -> x `IntSet.member` xs1) s) `IntMap.union` subst1
subst2' = fmap litToMatrix (IntMap.filterWithKey (\x _ -> x `IntSet.member` xs2) s) `IntMap.union` subst2
f (prefix ++ [(A, xs')]) (bvs `IntSet.union` xs') subst1' subst2' prefix1' prefix2'
f prefix bvs subst1 subst2 ((q,xs) : prefix1') prefix2 | q==E || not (prefixStartWithE prefix2) = do
let ys = IntSet.intersection bvs xs
nv <- get
put (nv + IntSet.size ys)
let s = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]
xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)
subst1' = fmap BoolExpr.Atom s `IntMap.union` subst1
subst1' = fmap litToMatrix s `IntMap.union` subst1
f (prefix ++ [(q, xs')]) (bvs `IntSet.union` xs') subst1' subst2 prefix1' prefix2
f prefix bvs subst1 subst2 prefix1 ((q,xs) : prefix2') = do
let ys = IntSet.intersection bvs xs
nv <- get
put (nv + IntSet.size ys)
let s = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]
xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)
subst2' = fmap BoolExpr.Atom s `IntMap.union` subst2
subst2' = fmap litToMatrix s `IntMap.union` subst2
f (prefix ++ [(q, xs')]) (bvs `IntSet.union` xs') subst1 subst2' prefix1 prefix2'

-- XXX
Expand All @@ -147,37 +151,37 @@ prenexOr (nv1, prefix1, matrix1) (nv2, prefix2, matrix2) =
evalState (f [] IntSet.empty IntMap.empty IntMap.empty prefix1 prefix2) (nv1 `max` nv2)
where
f :: Prefix -> VarSet
-> VarMap (BoolExpr SAT.Lit) -> VarMap (BoolExpr SAT.Lit)
-> VarMap Tseitin.Formula -> VarMap Tseitin.Formula
-> Prefix -> Prefix
-> State Int (Int, Prefix, Matrix)
f prefix _bvs subst1 subst2 [] [] = do
nv <- get
return (nv, prefix, BoolExpr.simplify (substVarMap matrix1 subst1 .||. substVarMap matrix2 subst2))
return (nv, prefix, Tseitin.simplify (substVarMap matrix1 subst1 .||. substVarMap matrix2 subst2))
f prefix bvs subst1 subst2 ((E,xs1) : prefix1') ((E,xs2) : prefix2') = do
let xs = IntSet.union xs1 xs2
ys = IntSet.intersection bvs xs
nv <- get
put (nv + IntSet.size ys)
let s = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]
xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)
subst1' = fmap BoolExpr.Atom (IntMap.filterWithKey (\x _ -> x `IntSet.member` xs1) s) `IntMap.union` subst1
subst2' = fmap BoolExpr.Atom (IntMap.filterWithKey (\x _ -> x `IntSet.member` xs2) s) `IntMap.union` subst2
subst1' = fmap litToMatrix (IntMap.filterWithKey (\x _ -> x `IntSet.member` xs1) s) `IntMap.union` subst1
subst2' = fmap litToMatrix (IntMap.filterWithKey (\x _ -> x `IntSet.member` xs2) s) `IntMap.union` subst2
f (prefix ++ [(A, xs')]) (bvs `IntSet.union` xs') subst1' subst2' prefix1' prefix2'
f prefix bvs subst1 subst2 ((q,xs) : prefix1') prefix2 | q==A || not (prefixStartWithA prefix2)= do
let ys = IntSet.intersection bvs xs
nv <- get
put (nv + IntSet.size ys)
let s = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]
xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)
subst1' = fmap BoolExpr.Atom s `IntMap.union` subst1
subst1' = fmap litToMatrix s `IntMap.union` subst1
f (prefix ++ [(q, xs')]) (bvs `IntSet.union` xs') subst1' subst2 prefix1' prefix2
f prefix bvs subst1 subst2 prefix1 ((q,xs) : prefix2') = do
let ys = IntSet.intersection bvs xs
nv <- get
put (nv + IntSet.size ys)
let s = IntMap.fromList $ zip (IntSet.toList ys) [(nv+1) ..]
xs' = (xs `IntSet.difference` bvs) `IntSet.union` IntSet.fromList (IntMap.elems s)
subst2' = fmap BoolExpr.Atom s `IntMap.union` subst2
subst2' = fmap litToMatrix s `IntMap.union` subst2
f (prefix ++ [(q, xs')]) (bvs `IntSet.union` xs') subst1 subst2' prefix1 prefix2'

-- ----------------------------------------------------------------------------
Expand All @@ -191,7 +195,7 @@ solve = solveCEGARIncremental
solveNaive :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveNaive nv prefix matrix =
case prefix' of
[] -> if BoolExpr.fold undefined matrix
[] -> if Tseitin.fold undefined matrix
then return (True, Just IntSet.empty)
else return (False, Nothing)
(E,_) : _ -> do
Expand Down Expand Up @@ -254,7 +258,7 @@ solveNaive nv prefix matrix =
solveCEGAR :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveCEGAR nv prefix matrix =
case prefix' of
[] -> if BoolExpr.fold undefined matrix
[] -> if Tseitin.fold undefined matrix
then return (True, Just IntSet.empty)
else return (False, Nothing)
(E,_) : _ -> do
Expand Down Expand Up @@ -322,7 +326,7 @@ solveCEGAR nv prefix matrix =
solveCEGARIncremental :: Int -> Prefix -> Matrix -> IO (Bool, Maybe LitSet)
solveCEGARIncremental nv prefix matrix =
case prefix' of
[] -> if BoolExpr.fold undefined matrix
[] -> if Tseitin.fold undefined matrix
then return (True, Just IntSet.empty)
else return (False, Nothing)
(E,_) : _ -> do
Expand Down Expand Up @@ -477,17 +481,17 @@ solveQE_CNF nv prefix matrix = g (normalizePrefix prefix) matrix
_test :: IO (Bool, Maybe LitSet)
_test = solveNaive 2 [(A, IntSet.singleton 2), (E, IntSet.singleton 1)] (x .&&. (y .||. notB x))
where
x = BoolExpr.Atom 1
y = BoolExpr.Atom 2
x = litToMatrix 1
y = litToMatrix 2

_test' :: IO (Bool, Maybe LitSet)
_test' = solveCEGAR 2 [(A, IntSet.singleton 2), (E, IntSet.singleton 1)] (x .&&. (y .||. notB x))
where
x = BoolExpr.Atom 1
y = BoolExpr.Atom 2
x = litToMatrix 1
y = litToMatrix 2

_test1 :: (Int, Prefix, Matrix)
_test1 = prenexAnd (1, [(A, IntSet.singleton 1)], BoolExpr.Atom 1) (1, [(A, IntSet.singleton 1)], notB (BoolExpr.Atom 1))
_test1 = prenexAnd (1, [(A, IntSet.singleton 1)], litToMatrix 1) (1, [(A, IntSet.singleton 1)], notB (litToMatrix 1))

_test2 :: (Int, Prefix, Matrix)
_test2 = prenexOr (1, [(A, IntSet.singleton 1)], BoolExpr.Atom 1) (1, [(A, IntSet.singleton 1)], BoolExpr.Atom 1)
_test2 = prenexOr (1, [(A, IntSet.singleton 1)], litToMatrix 1) (1, [(A, IntSet.singleton 1)], litToMatrix 1)
2 changes: 1 addition & 1 deletion src/ToySolver/SAT/Encoder/PB/Internal/Adder.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,10 +32,10 @@ import Data.Primitive.MutVar
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import ToySolver.Data.Boolean
import ToySolver.Data.BoolExpr
import qualified ToySolver.Internal.Data.SeqQueue as SQ
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import ToySolver.SAT.Encoder.Tseitin (Formula (..))

addPBLinAtLeastAdder :: forall m. PrimMonad m => Tseitin.Encoder m -> SAT.PBLinAtLeast -> m ()
addPBLinAtLeastAdder enc constr = do
Expand Down
2 changes: 1 addition & 1 deletion src/ToySolver/SAT/Encoder/PB/Internal/Sorter.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,10 +45,10 @@ import Data.Ord
import Data.Vector (Vector, (!))
import qualified Data.Vector as V
import qualified Data.Vector.Mutable as MV
import ToySolver.Data.BoolExpr
import ToySolver.Data.Boolean
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import ToySolver.SAT.Encoder.Tseitin (Formula (..))

-- ------------------------------------------------------------------------
-- Circuit-like implementation of Batcher's odd-even mergesort
Expand Down

0 comments on commit de00f45

Please sign in to comment.