msakai / toysolver / 513

Committed 24 Nov 2024 08:49AM UTC coverage: 68.675% (-1.0%) from 69.681%

Build # 513

Build Type

push

github

Committed by

web-flow

Commit Message

Merge 496ed4263 into 46e1509c4

Run Details

5 of 121 new or added lines in 7 files covered. (4.13%)

105 existing lines in 14 files now uncovered.

9745 of 14190 relevant lines covered (68.68%)

0.69 hits per line

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

28.57

/src/ToySolver/Converter/Tseitin.hs

{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeFamilies #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Converter.Tseitin
-- Copyright   :  (c) Masahiro Sakai 2018
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.Converter.Tseitin
  ( TseitinInfo (..)
  ) where

import qualified Data.Aeson as J
import Data.Aeson ((.=))
import Data.Array.IArray
import Data.String
import ToySolver.Converter.Base
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin

data TseitinInfo = TseitinInfo !Int !Int [(SAT.Var, Tseitin.Formula)]
  deriving (Eq, Show, Read)

instance Transformer TseitinInfo where
  type Source TseitinInfo = SAT.Model
  type Target TseitinInfo = SAT.Model

instance ForwardTransformer TseitinInfo where
  transformForward (TseitinInfo _nv1 nv2 defs) m = array (1, nv2) (assocs a)
    where
      -- Use BOXED array to tie the knot
      a :: Array SAT.Var Bool
      a = array (1, nv2) $
            assocs m ++ [(v, Tseitin.evalFormula a phi) | (v, phi) <- defs]

instance BackwardTransformer TseitinInfo where
  transformBackward (TseitinInfo nv1 _nv2 _defs) = SAT.restrictModel nv1

instance J.ToJSON TseitinInfo where
  toJSON (TseitinInfo nv1 nv2 defs) =
    J.object
    [ "type" .= J.String "TseitinInfo"
    , "num_original_variables" .= nv1
    , "num_transformed_variables" .= nv2
    , "definitions" .= J.object
        [ fromString ("x" ++ show v) .= J.toJSON formula
        | (v, formula) <- defs
        ]
    ]

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

1	{-# OPTIONS_GHC -Wall #-}
2	{-# OPTIONS_HADDOCK show-extensions #-}
3	{-# LANGUAGE OverloadedStrings #-}
4	{-# LANGUAGE TypeFamilies #-}
5	-----------------------------------------------------------------------------
6	-- \|
7	-- Module : ToySolver.Converter.Tseitin
8	-- Copyright : (c) Masahiro Sakai 2018
9	-- License : BSD-style
10	--
11	-- Maintainer : masahiro.sakai@gmail.com
12	-- Stability : experimental
13	-- Portability : non-portable
14	--
15	-----------------------------------------------------------------------------
16	module ToySolver.Converter.Tseitin
17	( TseitinInfo (..)
18	) where
19
20	import qualified Data.Aeson as J
21	import Data.Aeson ((.=))
22	import Data.Array.IArray
23	import Data.String
24	import ToySolver.Converter.Base
25	import qualified ToySolver.SAT.Types as SAT
26	import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
27
28	data TseitinInfo = TseitinInfo !Int !Int [(SAT.Var, Tseitin.Formula)]
29	deriving (Eq, Show, Read)	×
30
31	instance Transformer TseitinInfo where
32	type Source TseitinInfo = SAT.Model
33	type Target TseitinInfo = SAT.Model
34
35	instance ForwardTransformer TseitinInfo where
36	transformForward (TseitinInfo _nv1 nv2 defs) m = array (1, nv2) (assocs a)	1✔
37	where
38	-- Use BOXED array to tie the knot
39	a :: Array SAT.Var Bool
40	a = array (1, nv2) $	1✔
41	assocs m ++ [(v, Tseitin.evalFormula a phi) \| (v, phi) <- defs]	1✔
42
43	instance BackwardTransformer TseitinInfo where
44	transformBackward (TseitinInfo nv1 _nv2 _defs) = SAT.restrictModel nv1	1✔
45
NEW 46	instance J.ToJSON TseitinInfo where	×
NEW 47	toJSON (TseitinInfo nv1 nv2 defs) =	×
NEW 48	J.object	×
NEW 49	[ "type" .= J.String "TseitinInfo"	×
NEW 50	, "num_original_variables" .= nv1	×
NEW 51	, "num_transformed_variables" .= nv2	×
NEW 52	, "definitions" .= J.object	×
NEW 53	[ fromString ("x" ++ show v) .= J.toJSON formula	×
NEW 54	\| (v, formula) <- defs	×
55	]
56	]
57
58	-- -----------------------------------------------------------------------------

msakai / toysolver / 513

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