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

Satisfying assignment found when using SArray, not with SFunArray #541

Closed
gergoerdi opened this issue Jul 9, 2020 · 37 comments
Closed

Satisfying assignment found when using SArray, not with SFunArray #541

gergoerdi opened this issue Jul 9, 2020 · 37 comments

Comments

@gergoerdi
Copy link

gergoerdi commented Jul 9, 2020

The code at https://github.com/gergoerdi/scottcheck/tree/sbv-sfunarray-bug uses an SFunArray in src/ScottCheck/Engine.hs, line 59. The program can be run with stack run without any external dependencies. With that SFunArray version, the search gets to depth 8 and then starts slowing down.

However, if I replace that SFunArray with SArray, the search correctly finds a solution at just depth 6:

Searching at depth: 1
Searching at depth: 2
Searching at depth: 3
Searching at depth: 4
Searching at depth: 5
Searching at depth: 6
(1,2)
(1,2)
(10,7)
(1,1)
(1,1)
(18,7)
@LeventErkok
Copy link
Owner

LeventErkok commented Jul 9, 2020

SFunArray and SArray should be interchangeable for most practical purposes. (The latter can be compared for equality but the former cannot. But you'd get a type error for that.) Assuming both variants compile but they behave differently, then this is most likely a bug in SBV. I'll take a look.

@LeventErkok LeventErkok self-assigned this Jul 9, 2020
@LeventErkok LeventErkok added the Bug label Jul 9, 2020
LeventErkok added a commit that referenced this issue Jul 9, 2020
@LeventErkok
Copy link
Owner

LeventErkok commented Jul 9, 2020

@gergoerdi

I pushed in a fix that should address the issue. When I run your program, I now get:

Searching at depth: 1
Searching at depth: 2
(0,0)
(18,7)

Note that this is a different output from what you get with an SArray. I haven't looked into the details on what you're encoding, so I'm wondering if this is OK, or if we do still have a problem and the solution found is actually not valid. Do let me know.

@gergoerdi
Copy link
Author

gergoerdi commented Jul 10, 2020

Well the problem with reducing the repro code is that I have absolutely no idea what the output means anymore, I need to go back to the full program for that.

@gergoerdi
Copy link
Author

gergoerdi commented Jul 10, 2020

Note that this is a different output from what you get with an SArray. I haven't looked into the details on what you're encoding, so I'm wondering if this is OK

In the abstract, this doesn't sound OK: just like the Hex example you have pointed me towards, my code keeps feeding more and more input to the stateful computation only if the input so far doesn't yield a satisfying end state. So if SArray stops at depth 6 and SFunArray stops at depth 2, then that means either the SArray based one didn't correctly find a satisfying input of length 2, or the SFunArray one found a bogus one.

@gergoerdi
Copy link
Author

gergoerdi commented Jul 10, 2020

Well the problem with reducing the repro code is that I have absolutely no idea what the output means anymore, I need to go back to the full program for that.

OK so going back to my original program, I get two different solutions for SArray vs SFunArray (so I guess I managed to cut down my program without affecting its behaviour for this particular game data, which is good). The SFunArray solution isn't correct.

I tried to "prove" this, and the best I could come up with was to change main to this:

    let cmds1 = [(0, 0), (2, 0)] -- from SFunArray
        cmds2 = [(1, 2), (1, 2), (10, 7), (1, 1), (1, 1), (18, 7)] -- from SArray

    runSMT $ do
        arr <- newArray "items" Nothing
        query $ do
            let s0 = initState theGame arr
                (result, output) = flip evalState s0 $ runGame theGame $ do
                    mapM_ (\cmd -> stepWorld >> stepPlayer cmd) cmds1
                    finished
            constrain $ SBV.fromMaybe sFalse result
            sat <- checkSat
            liftIO $ print sat

If cmds1 and cmds2 would both be valid solutions, then I'd expect both to result in a satisfying end state for both SArray and SFunArray implementation. However, using either SArray or SFunArray, only cmds2 results in a satisfying end result (which is consistent with my eyeballing of them).

Would it be helpful if I ported this "checker" to the minimized version as well?

@LeventErkok
Copy link
Owner

LeventErkok commented Jul 10, 2020

I believe the SFunArray output was [(0, 0), (18, 7)], not [(0, 0), (2, 0)] as you wrote in cmds1 above. That both solutions end in the same value is interesting, though indeed I'd expect them to have the same "depth" if you're basically encoding a depth-first-search. If you are not coding a depth-first search, then there's no reason to expect them to have the same answer.

But you've the right idea: Whatever solution you get from whichever array representation, it'd be good to add code that walks through it concretely and makes sure it indeed satisfies all your constraints. If you find otherwise, that'd be a bug. (Either in the end-user code or in SBV.)

Do you still get a failure when you change cmds1 to be [(0, 0), (18. 7)]? That'd be the test.

Let me know what you find out!

@gergoerdi
Copy link
Author

gergoerdi commented Jul 11, 2020

I believe the SFunArray output was [(0, 0), (18, 7)], not [(0, 0), (2, 0)] as you wrote in cmds1 above.

Yeah but that's because I went back to the original program, not the cut-down one, and that one gave me [(0, 0), (2, 0)] as a "solution". I'll implement the "checker" for the cut-down version as you suggest.

@gergoerdi
Copy link
Author

gergoerdi commented Jul 11, 2020

OK so here's a full standalone program that demonstrates the problem. In line 21, I define the type synonym SArr as SArray; please change that to SFunArray to trigger the bug.

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE DeriveGeneric, DeriveAnyClass #-}
module Main where

import Control.Monad.Identity
import Control.Monad.Reader
import Control.Monad.State

import Control.Lens
import Data.Int
import Data.Array as A

import GHC.Generics (Generic)
import Data.SBV
import Data.SBV.Control
import qualified Data.SBV.Maybe as SBV
import Data.SBV.Maybe (sJust, sNothing)
import qualified Data.SBV.Tuple as SBV

type SArr = SArray

data Game = Game
    { gameStartRoom :: Int16
    , gameMaxScore :: Int16
    , gameItems :: Array Int16 Item
    , gameRooms :: Array Int16 Room
    }
    deriving (Show)

data Room = Room [Int16] deriving (Show)

data Item = Item Bool (Maybe Int16) Int16 deriving (Show)

theGame = Game
    { gameStartRoom = 1
    , gameMaxScore = 1
    , gameItems = A.listArray (0,0)
        [ Item True (Just 7) 2 ]
    , gameRooms = A.listArray (0,2)
        [ Room [0,0,0,0,0,0]
        , Room [0,2,0,0,0,0]
        , Room [1,0,0,0,0,0]
        ]
    }

type SInput = (SInt16, SInt16)

data S = S
    { _currentRoom :: SInt16
    , _itemLocations :: SArr Int16 Int16
    } deriving (Show, Generic, Mergeable)
makeLenses ''S

type Engine = ReaderT Game (State S)


instance (Mergeable a, forall a. Mergeable a => Mergeable (m a)) => Mergeable (ReaderT r m a) where
    symbolicMerge force cond thn els = ReaderT $ symbolicMerge force cond (runReaderT thn) (runReaderT els)

instance (Mergeable s, Mergeable a, forall a. Mergeable a => Mergeable (m a)) => Mergeable (StateT s m a) where
    symbolicMerge force cond thn els = StateT $
        symbolicMerge force cond (runStateT thn) (runStateT els)

instance forall a. Mergeable a => Mergeable (Identity a) where
    symbolicMerge force cond thn els = Identity $ symbolicMerge force cond (runIdentity thn) (runIdentity els)

main :: IO ()
main = do
    putStrLn "Solving"

    let genWord = do
            word <- freshVar_
            constrain $ 0 .<= word .&& word .< 19
            return word
        genInput i = curry SBV.tuple <$> genWord <*> genWord

    cmds <- runSMT $ do
        arr <- newArray "items" Nothing
        query $ loopState genInput (initState arr) $ \cmd -> do
            let (verb, noun) = SBV.untuple cmd
            runGame $ stepPlayer (verb, noun)

    mapM_ print cmds

    putStrLn "Checking"
    let cmds' = [(literal v, literal n) | (v, n) <- cmds]

    r <- runSMT $ do
        arr <- newArray "items" Nothing
        let r = flip evalState (initState arr) $ runGame $ last <$> mapM stepPlayer cmds'
        query $ do
            constrain r
            c <- checkSat
            liftIO $ print c
            getValue r
    print r

carried :: Int16
carried = 255

fillArray :: (Ix a, SymArray sarr, SymVal a, SymVal b) => Array a b -> sarr a b -> sarr a b
fillArray arr sarr = foldr write sarr (A.assocs arr)
  where
    write (i, x) sarr = writeArray sarr (literal i) (literal x)

initState :: SArr Int16 Int16 -> S
initState itemsArr = S
    { _currentRoom = literal $ gameStartRoom theGame
    , _itemLocations = fillArray (fmap (\(Item _ _ loc) -> loc) $ gameItems theGame) itemsArr
    }

runGame :: Engine a -> State S a
runGame act = runReaderT act theGame

stepPlayer :: SInput -> Engine SBool
stepPlayer (v, n) = do
    builtin (v, n)
    finished

data SRoom = SRoom [SInt16] deriving (Show, Generic, Mergeable)

sRoom :: Room -> SRoom
sRoom (Room exits) = SRoom (map literal exits)

finished :: Engine SBool
finished = do
    maxScore <- asks gameMaxScore
    items <- asks gameItems
    itemLocs <- use itemLocations
    let treasureLocs = [ readArray itemLocs (literal item) | (item, Item True _ _) <- A.assocs items ]
    let haveAllTreasure = map (.== literal carried) treasureLocs `pbAtLeast` fromIntegral maxScore
    return haveAllTreasure

sWhen :: SBool -> Engine () -> Engine ()
sWhen b = ite (sNot b) (return ())

builtin :: SInput -> Engine ()
builtin (verb, noun) = sCase verb (return ())
    [ (1, builtin_go)
    , (10, builtin_get)
    ]
  where
    builtin_go = sWhen (1 .<= noun .&& noun .<= 6) $ do
        let dir = noun - 1
        here <- use currentRoom
        SRoom exits <- asks $ (.! here) . fmap sRoom . gameRooms
        let newRoom = select exits 0 dir
        sWhen (newRoom ./= 0) $ currentRoom .= newRoom

    builtin_get = do
        locs <- use itemLocations
        here <- use currentRoom
        item <- parseItem
        sWhen (readArray locs item .== here) $ move item (literal carried)

    parseItem = do
        items <- asks gameItems
        return $ SBV.fromMaybe (-1) $ sFindIndex (\(Item _ name _) -> maybe sFalse ((noun .==) . literal) name) $ A.elems items


move :: SInt16 -> SInt16 -> Engine ()
move item loc = itemLocations %= \arr -> writeArray arr item loc

(.!) :: (Mergeable a) => Array Int16 a -> SInt16 -> a
xs .! i = case A.elems xs of
    [] -> error "(.!) : empty array"
    xs@(x:_) -> select xs x i

sCase :: (Mergeable a) => SInt16 -> a -> [(Int16, a)] -> a
sCase x def = go
  where
    go [] = def
    go ((k,v):kvs) = ite (x .== literal k) v (go kvs)

sFindIndex :: (a -> SBool) -> [a] -> SMaybe Int16
sFindIndex p = go 0
  where
    go i [] = sNothing
    go i (x:xs) = ite (p x) (sJust i) (go (i + 1) xs)


loopState :: (SymVal i) => (Int -> Query (SBV i)) -> s -> (SBV i -> State s SBool) -> Query [i]
loopState genCmd s0 step = go 1 s0 []
  where
    go i s cmds = do
        io $ putStrLn $ "Searching at depth: " ++ show i

        cmd <- genCmd i
        let cmds' = cmds ++ [cmd]

        push 1
        let (finished, s') = runState (step cmd) s
        constrain finished
        cs <- checkSat

        case cs of
            Unk -> error $ "Solver said Unknown, depth: " ++ show i
            Unsat -> do
                pop 1
                go (i+1) s' cmds'
            Sat -> mapM getValue cmds'

Output with SArr = SArray:

Solving
Searching at depth: 1
Searching at depth: 2
(1,2)
(10,7)
Checking
Sat
True

Output with SArr = SFunArray:

Solving
Searching at depth: 1
Searching at depth: 2
(0,4)
(10,7)
Checking
Unsat
scott-check: 
*** Data.SBV: Unexpected response from the solver, context: getModel:
***
***    Sent      : (get-value (s8))
***    Expected  : a value binding for kind: SBool
***    Received  : (error "line 18 column 15: model is not available")
***
***    Executable: z3
***    Options   : -nw -in -smt2
***
***    Reason    : Solver returned an error: "line 18 column 15: model is not available"

And from the "outside POV", the proposed solution [(0, 4), (10, 7)] really shouldn't be correct.

@LeventErkok
Copy link
Owner

LeventErkok commented Jul 11, 2020

Thanks for the report. Looking at this in some detail; I'm noticing that the caching mechanism used by SFunArray is not sound in the presence of pop, and resetAssertions.

I'm not sure if this is something I can work around easily. I'm inclined to put in the code to check if SFunArray is present if a pop or resetAssertions is issued and throw an error. I'll think some more about this before deciding.

@LeventErkok
Copy link
Owner

LeventErkok commented Jul 11, 2020

Thinking more about this, I'm no longer sure if it's pop (or resetAssertions in general) that's to blame here. Something else is going on, but it's really hard to debug your program.

Is there any chance you can simplify it? Say, get rid of all the state-constructions, and mergeable instances? That'd make it simpler to continue debugging this issue.

@LeventErkok
Copy link
Owner

LeventErkok commented Jul 11, 2020

@gergoerdi

Actually, I just noticed that the program you posted in this ticket behaves differently on my machine. Regardless SFunArray or SArray, I get the following output:

*Main> main
Solving
Searching at depth: 1
Searching at depth: 2
(1,2)
(10,7)
Checking
Sat
True

I'm curious why you're getting different output. Can you download SBV from github master and try again, maybe you're referring to a stale version somehow?

@gergoerdi
Copy link
Author

gergoerdi commented Jul 12, 2020

I went through various commits trying to reproduce this:

  • It fails with 211d6c2 as in my original report

  • It is rejected with e3f4f8a with:

    Data.SBV: pop and resetAssertions commands are not supported in the presence of SFunArrays.

    Instead of an SFunArray, use an SArray for problems that require pop or resetAssetions.

  • With 375ae01 it works with SFunArray:

    Searching at depth: 1
    Searching at depth: 2
    (1,2)
    (10,7)
    Checking
    Sat
    True
    

@gergoerdi
Copy link
Author

gergoerdi commented Jul 12, 2020

But I thought 375ae01 was supposed to just be a revert of e3f4f8a? Looking at the diff between 375ae01 and e3f4f8a^, the combined effect of the two commits is only in restoreTablesAndArrays, in that these lines are removed:

-- We have to also clean-out the caches for all functional arrays, as a pop would
-- invalidate the cache. See: https://github.com/LeventErkok/sbv/issues/541
io $ do faMap <- readIORef (rFArrayMap st)
        mapM_ (\(_, c) -> writeIORef c IM.empty) (IM.elems faMap)

@LeventErkok
Copy link
Owner

LeventErkok commented Jul 12, 2020

Yes, I'm a bit confused as well. The above change was bogus, which I now reverted.

Bottom line, the latest master in github is the one to put to test.

@gergoerdi
Copy link
Author

gergoerdi commented Jul 12, 2020

Well like I said, with 375ae01 which I see as the latest, it works.

@LeventErkok
Copy link
Owner

LeventErkok commented Jul 12, 2020

Right..

Does it work for your full repo as well?

@gergoerdi
Copy link
Author

gergoerdi commented Jul 12, 2020

OK just checked, and... no :/

@LeventErkok
Copy link
Owner

LeventErkok commented Jul 12, 2020

That's what I expected.. If you can create a new repro, I'd like to take a look.

It might indeed end up being a bug in SBV, but so far I'm not seeing why. I'd like to get to the bottom of it.

@gergoerdi
Copy link
Author

gergoerdi commented Jul 12, 2020

While I am working on minimizing it, here's the full code for reference: https://github.com/gergoerdi/scottcheck/tree/sbv-issue-541

You can run it with stack run -- games/t0.sao. The SArray to replace with SFunArray is in src/ScottCheck/Engine.hs.

@LeventErkok
Copy link
Owner

LeventErkok commented Jul 12, 2020

Thanks. Would be really great to get rid of all those Mergeable's, lenses, and anything higher-order, if you can. The simpler, the better. (When we get to the bottom of this, I'm sure it'll be demonstrable with a 10 line program.)

@gergoerdi
Copy link
Author

gergoerdi commented Jul 12, 2020

You can track my progress in simplifying it at that branch:)

@LeventErkok
Copy link
Owner

LeventErkok commented Jul 12, 2020

Waiting eagerly to see with what you come! Thanks for helping debug this.

@gergoerdi
Copy link
Author

gergoerdi commented Jul 12, 2020

OK so I managed to remove all uses of Lens, MTL, and Transformers. Let me know if it's good enough for debugging now.

@LeventErkok
Copy link
Owner

LeventErkok commented Jul 12, 2020

Great.. The simpler the better, but I'll take a look at this version.

@gergoerdi
Copy link
Author

gergoerdi commented Jul 12, 2020

I've found something that could potentially be interesting: a simplification step that makes the SFunArray version work, i.e. one that "breaks the breakage":

On top of fcead9ea91e86e34c14e357e79804e75c3ce584e, if I just change the definition of finished from

finished Game{..} (_, itemLocs) = readArray itemLocs (literal 0) .== literal gameTreasury

to

finished Game{..} (_, itemLocs) = readArray itemLocs (literal 0) .== literal carried

(which means we will not need to take the 18 branch of builtin for a solution), then SFunArray works the same as SArray!

So maybe you could look at the generated constraints with and without this one-liner change.

@gergoerdi
Copy link
Author

gergoerdi commented Jul 12, 2020

Here's the smallest version I have so far: <50 lines, single module:

module Main where

import Data.Int
import Data.SBV
import Data.SBV.Control
import qualified Data.SBV.Maybe as SBV

type SArr = SFunArray

type S = SArr Int16 Int16

initState :: SArr Int16 Int16 -> S
initState itemsArr = writeArray itemsArr 0 255

step :: [Maybe Int16] -> (SInt16, SInt16) -> S -> SBool
step items (verb, noun) locs = finished
  where
    finished = readArray locs' (literal 0) .== 1

    locs' = ite (verb .== 0) builtin_get $
            ite (verb .== 1) builtin_drop $
            locs

    builtin_get = ite (readArray locs item .== 1) (writeArray locs item 255) locs
    builtin_drop = ite (readArray locs item .== 255) (writeArray locs item 1) locs

    item = SBV.fromMaybe (-1) $ sFindIndex (\name -> maybe sFalse ((noun .==) . literal) name) $ items

sFindIndex :: (a -> SBool) -> [a] -> SMaybe Int16
sFindIndex p = go 0
  where
    go i [] = SBV.sNothing
    go i (x:xs) = ite (p x) (SBV.sJust i) (go (i + 1) xs)

main :: IO ()
main = do
    let theGame = [Just 7]
    cmds <- runSMT $ do
        arr <- newArray "items" Nothing
        query $ do
            verb <- freshVar "verb"
            noun <- freshVar "noun"
            constrain $ step theGame (verb, noun) (initState arr)
            ensureSat
            mapM getValue [verb, noun]
    mapM_ print cmds

@gergoerdi
Copy link
Author

gergoerdi commented Jul 12, 2020

We can even get rid of sFindIndex:

module Main where

import Data.Int
import Data.SBV
import Data.SBV.Control

type SArr = SFunArray

type S = SArr Int16 Int16

initState :: SArr Int16 Int16 -> S
initState itemsArr = writeArray itemsArr 0 255

step :: [Maybe Int16] -> (SInt16, SInt16) -> S -> SBool
step items (verb, noun) locs = finished
  where
    finished = readArray locs' (literal 0) .== 1

    locs' = ite (verb .== 0) builtin_get $
            ite (verb .== 1) builtin_drop $
            locs

    builtin_get = ite (readArray locs item .== 1) (writeArray locs item 255) locs
    builtin_drop = ite (readArray locs item .== 255) (writeArray locs item 1) locs

    item = ite (noun .== 7) 0 (-1)

main :: IO ()
main = do
    let theGame = [Just 7]
    cmds <- runSMT $ do
        arr <- newArray "items" Nothing
        query $ do
            verb <- freshVar "verb"
            noun <- freshVar "noun"
            constrain $ step theGame (verb, noun) (initState arr)
            ensureSat
            mapM getValue [verb, noun]
    mapM_ print cmds

@gergoerdi
Copy link
Author

gergoerdi commented Jul 12, 2020

I think this is the smallest I can do myself:

{-# LANGUAGE TypeApplications #-}
module Main where

import Data.Int
import Data.SBV
import Data.SBV.Control

type SArr = SFunArray

main :: IO ()
main = runSMT $ do
    arr <- newArray @SArr @Int16 @Int16 "items" Nothing
    query $ do
        x <- freshVar_ @Int16
        let ys = writeArray arr 0 255
        constrain $
          let ys' = ite (x .== 0) ys1 $ ite (x .== 1) ys2 ys

              ys1 = writeArray ys idx $ ite (y .== 1) 255 y
              ys2 = writeArray ys idx $ ite (y .== 255) 1 y

              idx = ite (x .== 1) 0 (-1)
              y = readArray ys idx
          in readArray ys' 0 .== 1
        ensureSat

@LeventErkok
Copy link
Owner

LeventErkok commented Jul 12, 2020

Fantastic! Great progress, and most importantly there are no push/pop calls which was the most confusing part for me. I was able to reduce it a little further, getting rid of query completely and streamline the testing:

import Data.SBV

test a = sat $ do
    arr <- newArray "items" (Just 0)
    x   <- sInteger "x"
    let ys = writeArray (arr `asTypeOf` a) 0 255

        idx = ite (x .== 1) 0 1
        y   = readArray ys idx

        ys1 = writeArray ys idx $ ite (y .== 1) 255 y
        ys2 = writeArray ys idx $ ite (y .== 255) 1 y

        ys' = ite (x .== 0) ys1 $ ite (x .== 1) ys2 ys

    constrain $ readArray ys' 0 .== 1

main = do print =<< test (undefined :: SArray    Integer Integer)
          print =<< test (undefined :: SFunArray Integer Integer)

I get:

Main> main
Satisfiable. Model:
  x = 1 :: Integer
Unsatisfiable

This is clearly a bug! And hopefully small enough to figure out what's going on.

@LeventErkok
Copy link
Owner

LeventErkok commented Jul 12, 2020

@gergoerdi @doyougnu

Update: I've spent some time on this, and I'm still stumped on what's going on. Even though the failing program is rather small now, it's really intricate how the SFunArray caching works to sort out what's going on here. But rest assured it's something we'll get to the bottom of, eventually.

Jeff: If you find yourself with free time and want to lend a pair of fresh eyes, do take a look. The functions to worry about are readSFunArr and writeSFunArr. (Perhaps mergeSFunArr plays a role too, but I suspect the issue is in one of the former two.) Any insights you might share would be most appreciated.

@doyougnu
Copy link
Collaborator

doyougnu commented Jul 13, 2020

@LeventErkok Will do but I won't have any time until later this week unfortunately.

@LeventErkok
Copy link
Owner

LeventErkok commented Jul 14, 2020

Here's another program that produces a bad result, I believe it's caused by the very same issue:

import Data.SBV

test :: Bool -> IO SatResult
test swap = satWith z3{verbose=False} $ do
    arr :: SFunArray Integer Integer <- newArray "items" (Just 0)
    x   <- sInteger "x"

    let ys = writeArray arr 0 2

        idx = x + 1

        ys1 = writeArray ys 0   (readArray ys idx)
        ys2 = writeArray ys idx 1

        v = if swap
               then ite (x .== 0) (readArray ys1 0) (readArray ys2 0)
               else ite (x ./= 0) (readArray ys2 0) (readArray ys1 0)

    constrain $ v .== 1

run :: IO ()
run = do print =<< test False
         putStrLn $ replicate 40 '-'
         print =<< test True

When I run it, I get:

*Test> run
Satisfiable. Model:
  x = -1 :: Integer
----------------------------------------
Unsatisfiable

Note that the only difference is the swapping of the ite condition, negated and branches are switched.

Obviously, caching isn't working correctly here: It appears to produce different results depending on evaluation order. The caches for the array will surely be different depending on the order of evaluation, but I'm not sure why the latter is producing an unsat result. In my mind, they should be equivalent.

LeventErkok added a commit that referenced this issue Jul 22, 2020
…rther accesses can use this entry symbolically

Addresses #541
LeventErkok added a commit that referenced this issue Jul 22, 2020
@LeventErkok
Copy link
Owner

LeventErkok commented Jul 22, 2020

@gergoerdi

I just pushed a few commits that I believe should fix this issue. Can you give it a try and see if it works for your original program?

@gergoerdi
Copy link
Author

gergoerdi commented Jul 22, 2020

Thanks, I can confirm it works now on my full program: using SArray and SFunArray finds the same (correct) solution.

@LeventErkok
Copy link
Owner

LeventErkok commented Jul 22, 2020

@gergoerdi

Great!

Out of curiosity: What's the performance of SArray vs SFunArray for your original problem? I'm noticing that for http://hackage.haskell.org/package/sbv-8.6/docs/Documentation-SBV-Examples-Puzzles-HexPuzzle.html, SFunArray is significantly faster than SArray. Do you observe similar?

@gergoerdi
Copy link
Author

gergoerdi commented Aug 3, 2020

OK so I finally got around to testing this, with 34d836a. And the results are... inconclusive.

I have two input files, a smaller one and a larger one; the smaller one is a simpler problem that requires less stateful steps to solve. For the small one, SArray still beats SFunArray by quite a large margin:

SArray, small input

00:00 Searching at depth: 1
00:00 Searching at depth: 2
00:00 Searching at depth: 3
00:00 Searching at depth: 4
00:00 Searching at depth: 5
00:00 Searching at depth: 6
00:00 Searching at depth: 7
00:01 Solution found:
00:01   1. GO SOU
00:01   2. GO SOU
00:01   3. GET COI
00:01   4. GO NOR
00:01   5. GO NOR
00:01   6. DRO COI
00:01   7. SCO ANY
	Command being timed: "scott-check games/t0.sao"
	User time (seconds): 0.53
	System time (seconds): 0.01
	Percent of CPU this job got: 100%
	Elapsed (wall clock) time (h:mm:ss or m:ss): 0:00.54

SFunArray, small input

00:00 Searching at depth: 1
00:00 Searching at depth: 2
00:00 Searching at depth: 3
00:00 Searching at depth: 4
00:00 Searching at depth: 5
00:00 Searching at depth: 6
00:00 Searching at depth: 7
00:02 Solution found:
00:02   1. GO SOU
00:02   2. GO SOU
00:02   3. GET COI
00:02   4. GO NOR
00:02   5. GO NOR
00:02   6. DRO COI
00:02   7. SCO ANY
	Command being timed: "scott-check games/t0.sao"
	User time (seconds): 2.42
	System time (seconds): 0.06
	Percent of CPU this job got: 100%
	Elapsed (wall clock) time (h:mm:ss or m:ss): 0:02.48

However, for the large one, SFunArray is so much slower that I gave up on waiting for it:

SArray, large input

00:00 Searching at depth: 1
00:00 Searching at depth: 2
00:00 Searching at depth: 3
00:00 Searching at depth: 4
00:01 Searching at depth: 5
00:01 Searching at depth: 6
00:03 Searching at depth: 7
00:06 Searching at depth: 8
00:16 Searching at depth: 9
00:51 Searching at depth: 10
01:23 Searching at depth: 11
01:44 Searching at depth: 12
03:23 Searching at depth: 13
04:13 Searching at depth: 14
05:58 Solution found:
05:58   1. GO WES
05:58   2. GET CRO
05:58   3. GO EAS
05:58   4. GO NOR
05:58   5. GET KEY
05:58   6. GO SOU
05:58   7. OPE DOO
05:58   8. GO DOO
05:58   9. GET COI
05:58  10. GO NOR
05:58  11. GO WES
05:58  12. GO NOR
05:58  13. DRO COI
05:58  14. SCO ANY
	Command being timed: "scott-check games/t4.sao"
	User time (seconds): 357.78
	System time (seconds): 0.53
	Percent of CPU this job got: 100%
	Elapsed (wall clock) time (h:mm:ss or m:ss): 5:57.91

SFunArray, large input

00:01 Searching at depth: 1
00:01 Searching at depth: 2
00:01 Searching at depth: 3
00:02 Searching at depth: 4

and then nothing for at least 12 minutes, with memory usage slowly climbing to 4 Gb.

@LeventErkok
Copy link
Owner

LeventErkok commented Aug 3, 2020

Thanks for the report. I've observed similar over the years, where it's really hard to predict how the array-solvers in SMT-land will behave. In theory, SArray should always beat SFunArray: There's a custom solver behind it. And I'd expect this to hold in general as the solvers get better over time. But giving SFunArray a try occasionally helps too.

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

No branches or pull requests

3 participants