Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Missing implementation of writeAigerWithLatches in class instance #14

Open
brianhuffman opened this issue Mar 4, 2020 · 1 comment
Open

Comments

@brianhuffman
Copy link

Here's the compiler warning message:

abcBridge            > /Users/huffman/Work/saw-script/deps/abcBridge/src/Data/ABC/AIG.hs:242:10: error: [-Wmissing-methods, -Werror=missing-methods]
abcBridge            >     • No explicit implementation for
abcBridge            >         ‘AIG.writeAigerWithLatches’
abcBridge            >     • In the instance declaration for ‘AIG.IsAIG Lit AIG’
abcBridge            >     |
abcBridge            > 242 | instance AIG.IsAIG Lit AIG where
abcBridge            >     |          ^^^^^^^^^^^^^^^^^
abcBridge            >

And here's the instance in question:

instance AIG.IsAIG Lit AIG where
newGraph _ = newAIG
aigerNetwork _ = readAiger
trueLit = true
falseLit = false
newInput a =
withAIGPtr a $ \p -> do
Lit <$> abcNtkCreateObj p AbcObjPi
and a x y = do
withAIGPtr a $ \p -> do
manFunc <- castPtr <$> abcNtkManFunc p
Lit <$> abcAigAnd manFunc (unLit x) (unLit y)
xor a x y = do
withAIGPtr a $ \p -> do
manFunc <- castPtr <$> abcNtkManFunc p
Lit <$> abcAigXor manFunc (unLit x) (unLit y)
mux a c t f = do
withAIGPtr a $ \p -> do
manFunc <- castPtr <$> abcNtkManFunc p
Lit <$> abcAigMux manFunc (unLit c) (unLit t) (unLit f)
inputCount a = withAIGPtr a (vecPtrSize <=< abcNtkPis)
getInput a i = do
withAIGPtr a $ \p -> do
v <- abcNtkPis p
sz <- vecPtrSize v
assert (0 <= i && i < sz) $
Lit . castPtr <$> vecPtrEntry v i
writeAiger path a = do
withNetworkPtr a $ \p -> do
ioWriteAiger p path True False False
writeCNF aig l path =
withNetworkPtr (AIG.Network aig [l]) $ \pNtk -> do
withAbcNtkToDar pNtk False False $ \pMan -> do
vars <- writeAIGManToCNFWithMapping pMan path
ciCount <- aigManCiNum pMan
forM [0..(ciCount - 1)] $ \i -> do
ci <- aigManCi pMan (fromIntegral i)
((vars V.!) . fromIntegral) `fmap` (aigObjId ci)
checkSat g l = do
withNetworkPtr (AIG.Network g [l]) $ \p ->
alloca $ \pp ->
bracket_
(poke pp =<< abcNtkDup p)
(abcNtkDelete =<< peek pp)
(checkSat' pp)
litView g l = withAIGPtr g $ \_ -> litViewInner l
abstractEvaluateAIG = memoFoldAIG
cec x y = do
ix <- networkInputCount x
iy <- networkInputCount y
assert (ix == iy) $ do
assert (outputCount x == outputCount y) $ do
withNetworkPtr x $ \xp -> do
withNetworkPtr y $ \yp -> do
alloca $ \pp -> do
bracket_
(poke pp =<< abcNtkMiter xp yp False 0 False False)
(abcNtkDelete =<< peek pp)
(AIG.toVerifyResult <$> checkSat' pp)
evaluator g inputs_l = do
withAIGPtr g $ \ntk -> do
-- Get vector with objects.
objs <- abcNtkObjs ntk
-- Get number of objects
var_count <- vecPtrSize objs
v <- VM.new var_count
-- Initialize constant literal value.
VM.write v 0 True
-- Initialize primary input.
pis <- abcNtkPis ntk
pi_count <- vecPtrSize pis
let inputs = V.fromList inputs_l
when (V.length inputs /= pi_count) $
fail "evaluate given unexpected number of inputs."
forI_ pi_count $ \pi_idx -> do
o <- vecPtrEntry pis pi_idx
idx <- fromIntegral <$> abcObjId o
VM.write v idx (inputs V.! pi_idx)
-- Initialize and nodes.
forI_ var_count $ \i -> do
o <- vecPtrEntry objs i
-- skip deleted vars!
unless (o == nullPtr) $ do
is_and <- abcObjIsAnd o
when is_and $ do
r0 <- evaluateFn v . Lit =<< abcObjLit0 o
r1 <- evaluateFn v . Lit =<< abcObjLit1 o
VM.write v i (r0 && r1)
-- Return evaluation function.
pureEvaluateFn g <$> V.freeze v

And the declaration of writeAigerWithLatches in the IsAIG class definition: https://github.com/GaloisInc/aig/blob/f5cf71da841187c726b8511c79476ddfeb8ea3aa/src/Data/AIG/Interface.hs#L201-L202

@robdockins
Copy link
Contributor

This whole module is deprecated, and has been since issue #4. We should probably just remove it.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants