Closed doyougnu closed 3 years ago
Hi Jeff,
Refactoring along these lines would be good indeed.
The following doesn't seem correct to me:
type UserInps = Map.Map Quantifier (S.Seq NamedSymVar)
In general, the user can alternate quantifiers; so the order of declaration is important. This should better be:
type UserInps = S.Seq (Quantifier. NamedSymVar)
I'm not sure if this change would fix the issue you're running into, but that'd be the first thing to do.
Regarding your specific questions:
I think the easiest would be to compile after changing the following line: https://github.com/LeventErkok/sbv/blob/master/Data/SBV/Provers/Prover.hs#L80 so it sets the verbose
to True
. This is a bit clumsy, but should work I suppose. (Of course, now you'll get a lot more other failures since the verbose is turned on and the gold files won't match. But perhaps you can deal with that one at a time, the make test TGT=blah
should help in the Makefile.
Ordering matters because that's how the lazy semantic of Haskell gets serialized. If we only wait until someone "depends" on a value, it might be too late. (The error you're getting is an indication of this.) There's an internal invariant that variables are declared before used and the order of generation must be according to the index. (Also see the calls forceSVArg
, which handles this for uninterpreted functions.)
I haven't use HashMap
before but obviously the faster the access the better. Ordering is absolutely essential, so this might be the way to go.
SBV was never designed with tens-of-thousands of models in mind. I'm guessing this is some sort of an allSat
like scenario? I'd expect the solver time to dominate SBV time in any case, but of course use of better data structures is always better. Best of luck!
Hey Levent,
Your response was very helpful and I did another refactor last night after I realized I optimized the data structure for the wrong thing. Here is my thinking; we want to order the variables by NodeId
to enforce the internal constraint that you mention, so instead of using a HashMap
on user names or the previous Map
I had on quantifiers we just use an IntMap
on NodeId
's themselves which ensures that a toList
call produces a list of variables with NodeId
's from [-2,-1,0...]
(-2 for false, -1 for true, and so on).
Here is what the data structures look like:
type UserInps = IMap.IntMap (Quantifier, NamedSymVar)
type InternInps = Set.Set NamedSymVar
type AllInps = Set.Set UserName
-- | Inputs as a record of maps and sets
data Inputs = Inputs { userInps :: !UserInps
, internInps :: !InternInps
, allInps :: !AllInps
} deriving (Eq,Ord,Show)
and an example insertion helper function which unpacks the SV
to insert to the IntMap
addUserInput :: Quantifier -> SV -> UserName -> Inputs -> Inputs
addUserInput q sv nm = goAll . goUser
where !new = toNamedSV sv nm
(NodeId nid) = swNodeId sv
goUser = onUserInps (nid `IMap.insert` (q, new))
goAll = onAllInps (Set.insert nm)
So we pay a little for the redundancy in SV
, i.e., SV
holds the NodeId
s and now so does UserInps
, but I think this is a low cost to pay for much faster operations, and avoiding reverse
's brought on by cons
ing. The problem now is that this no longer allows for duplicates because variables will be overwritten in the quantifier changes. I'm not sure if that is a viable use case however because it seems like a programmer error, i.e., variable x
is existentially quantified and then the same x
is universally quantified.
In any case the majority of tests pass with this setup:
1298 out of 375511 tests failed (873.87s)
I'm digging into a few of the left overs (this is just a matter of finding a call to reverse
and removing it). Once I get the tests to pass I'll have to run and change the gold tests many of which are failing because of show instances. For example they are expecting modelAssocs = [...
and not modelAssocs = fromList [...
or something similar.
Do we have a set of tests such that if the branch passes them we can be confident in the correctness of sbv? Or in other words, I want to be extremely confident the branch is sound before issuing a PR; so what is the best way to do that given I'm changing the internals here.
Edit: Added pass/fail numbers
Ah, yes. That refactoring seems to be on the spot. With an ascending conversion to lists from IntMap
that should be equivalent to what we currently have, and hopefully faster.
I don't have a set of tests separated out for this purpose. But feel free to send a PR if you're confident enough that whatever else failing is just cosmetic and I'll merge it to master after running the entire test-suite (including doctests). I'm in favor of this change regardless, so we can "fix" whatever bugs it introduces (if any) before making the 8.9 release on hackage.
@doyougnu
Hi Jeff. What's the status of this? I'm planning to do a release and I can hold off on it if you just need a few more days before a PR is available. If not, that's perfectly fine too; we can always make another release when it's ready.
Hi Levent,
The current status is that we have around ~1k failures on my branch (with gold tests being accepted) compared to only 21 on master. Nothing is stopping this from being merged but I want to get that number down before issuing a PR to eliminate future bug reports as much as possible.
Unfortunately, I haven't had a whole lot of time recently to make progress on this although that'll change after my next paper deadline (Nov 6th). You may have noticed that my contributions to sbv come in waves which reflects these deadlines.
So I think you should go ahead with the release and we can issue another release sometime in mid to late November.
Yeah, that sounds like a good plan. I'll make a release over the weekend. Thanks!
Hey Levent,
I've reduced the failing tests on my branch to just 4. 99% of them where caused by this change I made when exploring the space leak.
the remaining errors come from Basics
, for example quantified_sat_forallexists_satisfiable_p
produces:
SBVTest: Test platform: TestEnvCI CILinux
Remote
SBVTests
Basics.Quantifiers
quantified_sat_forallexists_satisfiable_p: FAIL (0.03s)
*** Data.SBV: Unexpected response from the solver, context: getModel:
***
*** Sent : (get-value (s0))
*** Expected : a value binding for kind: SWord8
*** Received : (error "line 15 column 12: unknown constant s0")
***
*** Executable: z3
*** Options : -nw -in -smt2
***
*** Reason : Solver returned an error: "line 15 column 12: unknown constant s0"
I've tracked this error down to this line, which I'll just reproduce here to save you a click:
Data.SBV.Control.Query.getModelAtIndex
from my branch:
let
wasSat,wasNotSat,allModelInputs :: M.Map Quantifier [NamedSymVar]
-- !wasSat = takeWhile ((/= ALL) . fst) qinps
-- !wasNotSat = dropWhile ((/= ALL) . fst) qinps -- takeWhile ((== ALL) . fst) qinps
(!wasSat, !wasNotSat) = M.partitionWithKey (\k _ -> k /= ALL) qinps
!allModelInputs = if isSAT
then wasSat
else wasNotSat
notice that allModelInputs
is a map instead of a list of quantifiers and NamedSymVar
s
compared to Data.SBV.Control.Query.getModelAtIndex
on master:
-- for "sat", display the prefix existentials. for "proof", display the prefix universals
let allModelInputs = if isSAT then takeWhile ((/= ALL) . fst) qinps
else takeWhile ((== ALL) . fst) qinps
The bug occurs because of differences in behavior between takeWhile
and partitionWithKey
. On master qinps
will look like this: qinps: [(Forall,(s0,"x")),(Exists,(s1,"y"))]
which means that takeWhile ((/= ALL) . fst) qinps = []
because takeWhile
will stop at the head element of this list which contains a ALL
. However, on my branch the corresponding code (wasSat
), will be a map that contains the existential, i.e., qinps = qinps: fromList [(Forall,[NamedSymVar s0 "x"]),(Exists,[NamedSymVar s1 "y"])]
and wasSat = fromList [(Exists,[NamedSymVar s1 "y"])]
.
Furthermore I verified this by running just the failing tests with:
allModelInputs = if isSAT
then mempty -- wasSat
else wasNotSat
which would mimic the behavior of the takeWhile
because the then
branch will return an empty map, as in the case on master
and not a singleton map, as in the case on my branch. With this hack all the previously failing tests passed so I know this is the right line of code to change but I'm not sure how to change it.
It seems that the original implementation was wrong in that it was taking any existential
s until it found a forall
then stopped once it found a forall
, but this is throwing away information which seems wrong...so I don't really understand what to do here. Any guidance on the appropriate semantics would be greatly appreciated.
Hi Jeff,
It's possible that I misunderstand your question. But if you're wondering why we have the following code in master:
-- for "sat", display the prefix existentials. for "proof", display the prefix universals
let allModelInputs = if isSAT then takeWhile ((/= ALL) . fst) qinps
else takeWhile ((== ALL) . fst) qinps
then I can explain that. This code is not buggy, it's written that way on purpose. We have to keep track of the exact alternation of quantifiers, because otherwise, we cannot present the model correctly. Here's an example to illustrate:
Prelude Data.SBV> prove $ forAll ["x"] $ \x -> forSome ["y"] (\y -> x .> (y :: SWord8))
Falsifiable. Counter-example:
x = 0 :: Word8
In the above, we have to display all the "prefix" univerals, i.e., the value of x
, but we cannot display the value of y
. This is because the solver is telling us that if x
is 0
, then this theorem is false; i.e., there is no y
to display. That's why we do takeWhile (== ALL)
in the prove
case. That is, we stop at the first existential, because the counter-example is true regardless of the choice for those variables, i.e., there's no canonical value.
Alternatively, consider:
Prelude Data.SBV> sat $ forSome ["x"] $ \x -> forAll ["y"] (\y -> x .<= (y :: SWord8))
Satisfiable. Model:
x = 0 :: Word8
This is a sat
call, and the solver is telling us if we pick x
to be 0
, then all y
's satisfy it. There's really no point in displaying a particular value of y
, because the formula holds for all y
. That's why we do takeWhile (/= ALL)
in the sat
case. That is we stop at the first occurrence of a universal, because the remaining variables will depend on that choice and it's true for all those variables.
I hope this makes it clear. Let me know if I misunderstood your point.
As far as the solution goes, regardless of how you represent the inputs you have to know in which order the user wrote them, as alternating quantifiers have different meanings. (That is, you cannot swap a universal with an existential in their order, or vice versa. It has to be kept as is.) So, you'll have to track the order as they come in. Perhaps associate each with an order number before you put them in the map, and respect that as you determine the model variables? Alternatively, you can keep that part as a good old list as it exists in the master, if the remaining code can be decoupled from that decision.
Hey Levent,
Yup that answered my question and did the trick. I know have all the tests passing. I have to clean up some of the code (removing some SCC
annotations) and I want to run some benchmarking but I'll issue the PR today for sure.
Fantastic! Looking forward to the PR, though of course there's no hurry. Do take your time.
Hi Jeff. I'm a bit confused as to where all the commits for performance updates are..
Can you fork off of https://github.com/LeventErkok/sbv/commits/perfUpdate rebase and push everything on to that branch? I'll take it from there.
Hey Levent,
This is done.
I finished the IntMap
refactor for the quantified inputs over the weekend. Unfortunately the mystery deepens, both Euler185
and U2Bridge
still have the same erroneous behavior you identified last week. Just as a sanity check I made sure the these doctests were correct on master and they were, so one of my changes is inducing these bugs.
I'm also confused particularly about Euler185
. I'm not familiar with the problem but If the hypothesis is that the ordering in a model is inducing the bug then I would expect the solution must be sensitive to the order (e.g., it can't be a simple sum or anything that is a commutative monoid), but I'm not sure if this is the case with this particular problem. So I wonder if there is some other change that is orthogonal to the IntMap
stuff that causing this bug...
Note: I originally pushed with a merge
but have finished the rebase and cleaned up the history. Now the commits are correct. It was pretty complicated so I double checked the commits and ran tests, everything looks fine.
@doyougnu
I pulled in the changes to my own perfUpdate
branch and indeed the doctests are still failing.
In which commit did you try to maintain the order of variables as the user wrote them? (Instead of reconstructing in the sorted name order?) I can take a look at that commit to see if I can spot anything.
@LeventErkok I think the commit you're after is 27e85844adc1b71a89c900eb8d3039fee6f6a6ee, which changes this line to use the semigroup operation on IntMap
which should do an order preserving merge.
This specific statement:
try to maintain the order of variables as the user wrote them
Hits the limit of my understanding of the core code base. My working understanding is that mkSymVar
is the function to create the user defined variables, and the ordering of them. So my working hypothesis of these bugs is that the internal ordering is sound due to the hard constraint on IntMap
but during model retrieval I'm breaking this ordering somewhere. Then for these doctests the results are used in some subsequent computation which also relies on the ordering, which is now broken, hence the bug.
After reviewing our previous conversation in the PR, I suspect that this line is problematic for the same reasons that the previous one was which you pointed out.
Great! Yes, please push to LeventErkok/sbv:perfUpdate
and I'll merge it after taking a look through to familiarize myself with the changes.
Pushed. I've also narrowed down the bug to this line in this commit: https://github.com/doyougnu/sbv/commit/33e1545c496af1b695d954003620ffcd285ba317#diff-e529dc5fa1e2311a5c79a67b82a089ddbf72f100668999e20cd26d020197304e
It's exactly what we were suspecting, the ordering is broken by a fromList
call, it was just in a different area of the code base and that's probably why it only showed up in a few doctests.
For the record I tested it by changing that line to , modelAssocs = Map.toList . Map.fromList . F.toList $ nameAssocs
and running the doctest on Euler185
.
I'm having compilation issues. Did you leave out some files from the commit?
[ 1 of 105] Compiling Utils.SBVTestFramework ( SBVTestSuite/Utils/SBVTestFramework.hs, interpreted )
SBVTestSuite/Utils/SBVTestFramework.hs:203:96: error:
• Couldn't match expected type ‘[(String,
sbv-8.9.5:Data.SBV.Core.Concrete.CV)]’
with actual type ‘M.Map [Char] sbv-8.9.5:Data.SBV.Core.Concrete.CV’
• In the third argument of ‘SMTModel’, namely
‘(vals <> M.fromList [getCV "Result" (literal v)])’
In the second argument of ‘showModel’, namely
‘(SMTModel
[] Nothing (vals <> M.fromList [getCV "Result" (literal v)]) [])’
In the expression:
showModel
defaultSMTCfg
(SMTModel
[] Nothing (vals <> M.fromList [getCV "Result" (literal v)]) [])
|
203 | Right v -> showModel defaultSMTCfg (SMTModel [] Nothing (vals <> M.fromList [getCV "Result" (literal v)]) [])
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
SBVTestSuite/Utils/SBVTestFramework.hs:204:95: error:
• Couldn't match expected type ‘[(String,
sbv-8.9.5:Data.SBV.Core.Concrete.CV)]’
with actual type ‘M.Map [Char] sbv-8.9.5:Data.SBV.Core.Concrete.CV’
• In the third argument of ‘SMTModel’, namely ‘vals’
In the second argument of ‘showModel’, namely
‘(SMTModel [] Nothing vals [])’
In the first argument of ‘(++)’, namely
‘showModel defaultSMTCfg (SMTModel [] Nothing vals [])’
|
204 | Left e -> showModel defaultSMTCfg (SMTModel [] Nothing vals []) ++ "\n" ++ e
| ^^^^
SBVTestSuite/Utils/SBVTestFramework.hs:262:96: error:
• Couldn't match expected type ‘[(String,
sbv-8.9.5:Data.SBV.Core.Concrete.CV)]’
with actual type ‘M.Map [Char] sbv-8.9.5:Data.SBV.Core.Concrete.CV’
• In the third argument of ‘SMTModel’, namely
‘(vals <> M.fromList [getCV "Result" (literal v)])’
In the second argument of ‘showModel’, namely
‘(SMTModel
[] Nothing (vals <> M.fromList [getCV "Result" (literal v)]) [])’
In the expression:
showModel
defaultSMTCfg
(SMTModel
[] Nothing (vals <> M.fromList [getCV "Result" (literal v)]) [])
|
262 | Right v -> showModel defaultSMTCfg (SMTModel [] Nothing (vals <> M.fromList [getCV "Result" (literal v)]) [])
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
SBVTestSuite/Utils/SBVTestFramework.hs:263:95: error:
• Couldn't match expected type ‘[(String,
sbv-8.9.5:Data.SBV.Core.Concrete.CV)]’
with actual type ‘M.Map [Char] sbv-8.9.5:Data.SBV.Core.Concrete.CV’
• In the third argument of ‘SMTModel’, namely ‘vals’
In the second argument of ‘showModel’, namely
‘(SMTModel [] Nothing vals [])’
In the first argument of ‘(++)’, namely
‘showModel defaultSMTCfg (SMTModel [] Nothing vals [])’
|
263 | Left e -> showModel defaultSMTCfg (SMTModel [] Nothing vals []) ++ "\n" ++ e
| ^^^^
Failed, no modules loaded.
I didn't build the test suite after changing the modelAssocs
type back to [(String, CV)]
. I'll be pushing shortly with the fix.
Pushed the fix. Just had to remove some M.fromList
's
Great. I'm still getting a few doctest failures, but looks like these are simply a matter of how the printing changed slightly, as opposed to "correctness."
I'll review those and most likely merge the branch sometime tomorrow.
@doyougnu
I've looked through the changes and pushed a few commits to the perfUpdate
branch to clean up a few things.
Unfortunately, the code isn't matching the master quite yet. The problem is with the getQuantifiedInps
function.
Here's the new code:
getQuantifiedInputs :: (MonadIO m, MonadQuery m) => m UserInps
getQuantifiedInputs = do State{rinps} <- queryState
(rQinps, rTrackers) <- liftIO $ getInputs <$> readIORef rinps
-- we rely on the nodeId ordering in UserInps to ensure
-- the order of quantifiers
let trackers :: UserInps
trackers = inpsFromListWith (const EX) $ F.toList rTrackers
return $ rQinps <> trackers
And here's the old:
getQuantifiedInputs :: (MonadIO m, MonadQuery m) => m [(Quantifier, NamedSymVar)]
getQuantifiedInputs = do State{rinps} <- queryState
((rQinps, rTrackers), _) <- liftIO $ readIORef rinps
let qinps = reverse rQinps
trackers = map (EX,) $ reverse rTrackers
-- separate the existential prefix, which will go first
(preQs, postQs) = span (\(q, _) -> q == EX) qinps
return $ preQs ++ trackers ++ postQs
Unfortunately the new code isn't preserving the semantics here. The idea is to make sure the "tracker" variables (which are always existential) are spliced in after all the existentials but before the universals. The new code isn't doing this, which causes downstream problems. (The semigroup merge operation isn't doing the right thing here.)
Perhaps one way to fix is to change getQuantifiedInputs
to simply return the list (i.e., keep the old signature.) But I'll leave it to you to see how you might want to address this change.
Good catch. I'll sync with the perfUpdate
branch on master and play around with some implementations. I think the easiest course of action is to use a list, but this is probably some technical debt although it could be worth it given how large this branch has gotten already. I'll leave this decision up to you and probably won't have time to tinker until Saturday.
Ideally the tracker's nodeId's would always have the constraint forall e \in existentials t \in trackers u \in universals. max (nodeID e) < nodeID t < nodeID u)
, and thus any time a tracker is made it would uphold this constraint, and then the semigroup operator would merge appropriately.
I'm also pretty surprised that this got through all the tests and doctests without throwing an error. This seems like a good candidate to add as a unit test.
There's a test for it, but looks like the gold-files got fumbled. I found this after looking at the output of:
git diff master -- '*.gold'
There are legitimate changes to gold files, but there's a few that are missing variables in the output models. optQuant2
being one example.)
Looking at your commit histories, looks like there was a commit that "erased" a bunch of output in model values; you then had a separate commit that fixed a bunch of these, but not all. Looking very carefully at the commit-diffs really pays off.
@LeventErkok
I think I've settled on a workable solution for quantified inputs.
This requirement:
The idea is to make sure the "tracker" variables (which are always existential) are spliced in after all the existentials but before the universals
Isn't workable because this ordering will almost certainly differ from than the order of variable creation, which the IntMap
enforces, and thus my previous comment about trying to enforce constraints on NodeId
s also isn't workable (and would probably be a way more complex implementation). So my working hypothesis was that the requirement that trackers are placed after existential and before universals was only important because the trackers would then be picked up by this line in getModelAtIndex
:
-- for "sat", display the prefix existentials. for "proof", display the prefix universals
let allModelInputs = if isSAT then takeWhile ((/= ALL) . fst) qinps
else takeWhile ((== ALL) . fst) qinps
thus when I changed to the IntMap
implementation, the trackers were not included in allModelInputs
because prefixExistentials
may not include them now that they are in creation-order. Thus if I simply made sure the trackers were added, even if they were interspersed with the existentials then the semantics would be preserved. Furthermore, this would explain why some variables like goal
in optQuant2
were missing.
So I changed the internal variables type to:
-- | Internally declared, always existential
type InternInps = IMap.IntMap NamedSymVar
and then tested the hypothesis by ensuring the trackers were added after prefixExistentials
:
getModelAtIndex :: (MonadIO m, MonadQuery m) => Maybe Int -> m SMTModel
getModelAtIndex mbi = do
State{runMode,rinps} <- queryState
rm <- io $ readIORef runMode
inputs <- io $ readIORef rinps
...
let allModelInputs = if isSAT
then ((EX,) <$> internInps inputs) <> prefixExistentials qinps
else prefixUniversals qinps
and sure enough optQuant2
produced a model that matches the gold on master
(Recall that this fails on the perfUpdate
branch because I accidentally nuked the gold tests, sorry!):
Remote
SBVTests
Optimization.Reals
optQuant2: FAIL (0.02s)
Test output was different from 'SBVTestSuite/GoldFiles/optQuant2.gold'. It was:
Optimal model:
a = 0 :: Integer
b1 = 1 :: Integer
b2 = 1 :: Integer
goal = 0 :: Integer
Does this seem like the right direction to you? getQuantifiedInputs
is awkward to use with this change because we add the trackers in that function, and then add them again in allModelInputs
. Looking through the code base I only see calls to prefixExistential
in getModelAtIndex
and getAllSatResult
so maybe it is fine? If this is right then maybe changing prefixExistential
to always include the trackers is the way to go. I've pushed the changes to doyougnu/perfUpdate
if you wanted to look at them in more detail.
I'm a little concerned that as innocuous as the original idea was, it revealed a whole bunch of internal invariants that I couldn't even remember. I'm worried that there might be other pieces of code that rely on this order, where the test-suite is rather weak and thus we don't see the breakage.
Here's an alternative idea. While IntMap
is cool, we hardly ever access these SVs out-of-order. So, instead of IntMap
, why not use something like Data.Sequence
. (https://hackage.haskell.org/package/containers-0.6.4.1/docs/Data-Sequence.html) This change would keep the code close to the original, almost all list-like operations will continue to work, and it'll bring in efficiency without much work at all.
I'm curious what sort of performance upgrade we'd get by simply converting []
to Data.Sequence
, and String
to Text
. My hunch is that it'll bring all the performance without the added complexity. Experimenting with that design might be well worth the time.
I agree.
The original decision for IntMap
was to ensure the ordering and avoid subsequent sortByNodeId
s. But most of the performance issues came from [(,)]
begin overly lazy. Just from seeing downstream effects of the change I'm also concerned about the soundness of the perfUpdate
branch.
I think a Sequence
would be a nice middle ground: it would allow us to build the Sequence
's in the correct order instead of reverse
'ing. We can use a spine-struct variant to avoid thunks, and as you mention keep the code closer to master. I do still want to de-tangle the rinps :: [((Quantifier, NamedSymVar), [NamedSymVar])]
data type because it doesn't convey much meaning to the type system.
What would you like to do with the perfUpdate
branch? I have time this week to implement the Sequence
design but I think its best to start over from master
just in case there are any lingering changes.
Agreed.
Let's just abandon the perfUpdate
branch. Simply make a new branch, call it perfSequence
for instance, and let's build it out of that.
Update on this.
I've implemented the performance updates with a Sequence
:
-- | User defined, with proper quantifiers
type UserInputs = S.Seq (Quantifier, NamedSymVar)
-- | Internally declared, always existential
type InternInps = S.Seq NamedSymVar
the key function is lookupInput
:
lookupInput :: Eq a => (a -> SV) -> SV -> S.Seq a -> Maybe a
lookupInput f sv ns = res
where
i = getId (swNodeId sv)
svs = fmap f ns
res = case S.lookup i ns of -- Nothing on negative Int or Int > length seq
Nothing -> secondLookup
x@(Just e) -> if sv == f e then x else secondLookup
-- we try the fast lookup first, if the node ids don't match then
-- we use the more expensive O (n) to find the index and the elem
secondLookup = S.elemIndexL sv svs >>= flip S.lookup ns
which tries to lookup by node id first, if it finds the right symbol (i.e., the node ids match) then it returns it, if not then it searches for the element with an O (n)
linear search (just like Data.List.lookup
).
I tried as much as possible to keep the code base as similar to master
, for example getQuantifiedInputs
is:
getQuantifiedInputs :: (MonadIO m, MonadQuery m) => m UserInputs
getQuantifiedInputs = do State{rinps} <- queryState
(rQinps, rTrackers) <- liftIO $ getInputs <$> readIORef rinps
let trackers = (EX,) <$> rTrackers
-- separate the existential prefix, which will go first
(preQs, postQs) = S.spanl (\(q, _) -> q == EX) rQinps
return $ preQs <> trackers <> postQs
which is very close to the list implementation. A few things to note:
><
but I figured the semigroup is more general and easier to maintain if the types change againnodeId :: SV -> Int
I replaced them with the identical function from Symbolic
namely swNodeId :: SV -> NodeId
and then composed with NodeId
's new type for: getId . swNodeId
con
sing and reverse
-ing. I chose not to do this yet because it would complicate the integration. For example, recordObservable
now looks like:
recordObservable :: State -> String -> (CV -> Bool) -> SV -> IO ()
-- notice that we cons like a list, we should build at the end of the seq, but cons to preserve semantics for now
recordObservable st (T.pack -> nm) chk sv = modifyState st rObservables ((nm, chk, sv) S.<|) (return ())
which still adds at the head position rather than the end position.
scanr
is scanl
but beginning at the end cell rather than the head cell. There are similar cases for takeWhile
and the list combinators. It could be worth looking into these for some minor optimizations.There are 17 failing gold tests. I've seen these errors before but don't really know how to dig into them. Some of them are legitimate and reflect the change others I'm not sure about, here are a few samples of the failures I think are true failures:
Basics.ModelValidate
validate_1: FAIL (0.01s)
--- SBVTestSuite/GoldFiles/validate_1.gold 2020-11-30 18:08:55.012511796 -0800
+++ SBVTestSuite/GoldFiles/validate_1.gold_temp 2020-11-30 19:11:31.364310376 -0800
@@ -25,11 +25,11 @@
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
-[RECV] ((s0 (_ +zero 8 24)))
+[RECV] ((s0 (fp #b1 #xfe #b11111111111111111111111)))
*** Solver : Z3
*** Exit code: ExitSuccess
[VALIDATE] Validating the model. Assignment:
-[VALIDATE] x = 0.0 :: Float
+[VALIDATE] x = -3.4028235e38 :: Float
[VALIDATE] There are no constraints to check.
[VALIDATE] Validating outputs.
uiSat_test3: FAIL (0.42s)
--- SBVTestSuite/GoldFiles/uiSat_test3.gold 2020-11-30 18:08:55.011511767 -0800
+++ SBVTestSuite/GoldFiles/uiSat_test3.gold_temp 2020-11-30 19:11:36.350370863 -0800
@@ -29,9 +29,9 @@
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
-[RECV] ((q1 ((as const Array) false)))
+[RECV] ((q1 (_ as-array q1)))
[SEND] (get-value (q2))
-[RECV] ((q2 ((as const Array) false)))
+[RECV] ((q2 (_ as-array q2)))
[GOOD] (define-fun q1_model1 ((x!0 Bool)) Bool
false
)
@@ -57,7 +57,7 @@
[SEND] (get-value (q1))
[RECV] ((q1 ((as const Array) true)))
[SEND] (get-value (q2))
-[RECV] ((q2 ((as const Array) false)))
+[RECV] ((q2 (_ as-array q2)))
[GOOD] (define-fun q1_model2 ((x!0 Bool)) Bool
true
)
@@ -164,7 +164,7 @@
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
[SEND] (get-value (q2))
-[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not x!1) (not x!2)))))
+[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not x!2) (not x!1)))))
[SEND]<truncated>
Use --accept or increase --size-cutoff to see full output.
Basics.Set
set_uninterp1: FAIL (0.02s)
--- SBVTestSuite/GoldFiles/set_uninterp1.gold 2020-11-30 18:08:55.010511738 -0800
+++ SBVTestSuite/GoldFiles/set_uninterp1.gold_temp 2020-11-30 19:11:33.620337760 -0800
@@ -57,8 +57,8 @@
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
-[RECV] ((s0 (store (store ((as const (Array E Bool)) false) C true) A true)))
-[GOOD] (define-fun s10 () (Array E Bool) (store (store ((as const (Array E Bool)) false) C true) A true))
+[RECV] ((s0 (store (store (store ((as const (Array E Bool)) false) C true) B true) A true)))
+[GOOD] (define-fun s10 () (Array E Bool) (store (store (store ((as const (Array E Bool)) false) C true) B true) A true))
[GOOD] (define-fun s11 () Bool (= s0 s10))
[GOOD] (define-fun s12 () Bool (not s11))
[GOOD] (assert s12)
Both Euler185
and the optQuant
s pass. I just spot checked these and didn't run the full doctest
and I've pushed the branch to sbv/perfSequence
Great!
I can get a clean test-suite with this. (You need a freshly compiled z3 from their master github. I suppose your version of z3 is probably a bit old.)
I pushed in a few changes; mostly to make sure getObservables
have the same type both in regular (i.e., Query
) and Trans
modes. That's an invariant we keep: The type of those functions should differ only in one being specialized to the Query
monad, and the other being parameterized over the monad itself.
I'm happy to merge this back to master. But let's see if it did the trick. Can you run your benchmarks and let's see if it indeed brings in performance? After we get some positive feedback from that, I'll merge it to master. Great work!
I can get a clean test-suite with this. (You need a freshly compiled z3 from their master github. I suppose your version of z3 is probably a bit old.)
Ah yea it is by that standard. I'm using the z3
on nixos stable (4.8.8)
I'll run the benchmarks today to get a read on performance.
Benchmark results, more negative is faster, more positive is slower, tested with z3 4.8.8
:
*Main> compareBenchmarks "SBVBenchSuite/BenchResults/master.csv" "SBVBenchSuite/BenchResults/perfSequence.csv"
(Mean)
Benchmark default(0)(μs) default(1) - default(0)(%)
---------------------------------------------------------- -------------- --------------------------
Uninterpreted//r2 10629.59 -6.36
WeakestPreconditions/Correctness.Length 12272.40 -5.48
Miscellaneous//SubsetChar.Union 10781.96 -5.39
Uninterpreted//genLs 12453.07 -5.16
WeakestPreconditions//Correctness.Basics y+1 10363.61 -5.11
Uninterpreted//univOk 2831.77 -4.86
Miscellaneous//SubsetEquality 10923.01 -4.56
Optimizations/VM.allocate 9630.36 -4.54
Optimizations/Production.production 8128.62 -4.38
WeakestPreconditions/Correctness.IntDiv 13463.93 -4.29
ProofTools//Strengthen.ex2 50446.83 -4.16
Miscellaneous//JoinMeet.5 10563.93 -4.14
Miscellaneous//JoinMeet.3 9801.79 -3.88
WeakestPreconditions//Correctness.Sum.correctInvariant 14280.30 -3.76
Miscellaneous//SubsetEquality.Transitivity 10635.04 -3.76
Miscellaneous//RelativeComplements.Union 10481.61 -3.54
WeakestPreconditions//ImperativeGCD 101.80 -3.27
WeakestPreconditions/Correctness.IntSqrt 15161.24 -3.25
WeakestPreconditions//Correctness.Sum.alwaysFalseInvariant 10325.80 -3.25
Miscellaneous//RelativeComplements.ComplementIdentity 10202.97 -3.11
Uninterpreted//shannon 3329.61 -3.06
Miscellaneous//JoinMeet.1 10424.99 -2.97
Uninterpreted//t1 10211.74 -2.96
Uninterpreted//synthMul22 13526.63 -2.95
WeakestPreconditions//Correctness.Sum.loopInvariant 14492.36 -2.95
Miscellaneous//RelativeComplements.CompFull 10293.06 -2.89
Puzzles//NQueens.NQueens 1 2969.80 -2.89
Miscellaneous//DeMorgans.Cap 10296.68 -2.76
Miscellaneous//Associativity.Union 10268.20 -2.73
WeakestPreconditions//Correctness.Basics skip 9817.75 -2.50
WeakestPreconditions//Correctness.Fib 14395.67 -2.49
Puzzles//NQueens.NQueens 6 18534.40 -2.36
Uninterpreted//SFunArray 3204.72 -2.35
Miscellaneous//RelativeComplements.UnitRight 10025.05 -2.16
Uninterpreted//thmGood 2893.93 -2.10
Miscellaneous//SubsetChar.Implication 9889.23 -2.06
Miscellaneous//RelativeComplements.Identity 9752.85 -2.01
Uninterpreted//existsOk 2741.89 -1.96
Miscellaneous//RelativeComplements.UnionUnion 10439.56 -1.92
WeakestPreconditions//Correctness.Sum.alwaysTrueInvariant 11074.91 -1.88
Puzzles//LadyAndTigers 11427.06 -1.79
Uninterpreted//shannon2 3306.00 -1.67
Miscellaneous//Identity.Intersection 10075.94 -1.51
Miscellaneous//Complement.Complement 9617.45 -1.48
Miscellaneous//RelativeComplements.UnitLeft 10164.49 -1.40
Miscellaneous//RelativeComplements.CompComp 10086.30 -1.35
Puzzles//Birthday 13033.96 -1.35
Lists//GenFibs 2104068.73 -1.35
Uninterpreted//noWiggle 2943.85 -1.32
Miscellaneous//Intersection.Difference 9620.64 -1.30
Miscellaneous//InclusionIsPO 9703.25 -1.30
Miscellaneous//JoinMeet.4 9676.70 -1.29
Miscellaneous//RelativeComplements.InterInters.2 10323.73 -1.28
Miscellaneous//Absorption.Cap 10009.25 -1.26
Optimizations//Enumerate.firstWeekend 9923.90 -1.24
Miscellaneous//DistributionSubset.Union 10950.43 -1.24
Miscellaneous//Commutivity.Intersection 10120.87 -1.24
Puzzles//NQueens.NQueens 8 184294.51 -1.21
Miscellaneous//RelativeComplements.ComplementUnion 10172.22 -1.19
Miscellaneous//DeMorgans.Cup 10352.04 -1.17
Puzzles//NQueens.NQueens 3 4235.81 -1.13
WeakestPreconditions//Correctness.Sum.badMeasure1 14569.85 -1.12
Puzzles//NQueens.NQueens 5 15879.27 -1.05
ProofTools//BMC.ex1 8231.46 -1.04
Miscellaneous//Identity.Union 10042.82 -1.03
ProofTools//Strengthen.ex3 19864.42 -1.00
Miscellaneous//Distributivity.Union 10223.81 -0.99
Optimizations//Enumerate.WeekendJustOver 9649.48 -0.99
Puzzles//Puzzles.SendMoreMoney 21614.76 -0.96
Miscellaneous//RelativeComplements.Intersection 10428.69 -0.93
Miscellaneous//RelativeComplements.UnionInters 10283.19 -0.92
Miscellaneous//SubsetChar.Intersection 10365.84 -0.83
Uninterpreted//SArray 3263.14 -0.79
Miscellaneous//Absorption.Cup 9995.29 -0.76
Miscellaneous//Commutivity.Union 10050.87 -0.73
Miscellaneous//SoftConstrain 13361.83 -0.73
Miscellaneous//Distributivity.Intersection 10287.84 -0.70
Puzzles//Garden 121714.73 -0.61
Miscellaneous//Complement.Intersection 9582.74 -0.58
WeakestPreconditions//Correctness.Sum.badMeasure2 13944.01 -0.55
BitPrecise//Fast-min 5631.68 -0.53
ProofTools//Strengthen.ex5 29785.52 -0.50
Miscellaneous//RelativeComplements.InterInters.1 10217.07 -0.43
Miscellaneous/genVals 119800.35 -0.39
Miscellaneous//DistributionSubset.Intersection 10867.96 -0.35
Strings//puzzle1 21640.44 -0.25
Miscellaneous//Complement.Union 9661.13 -0.22
Miscellaneous//SubsetChar.Complement 10167.47 -0.17
ProofTools/Fibonacci.Correctness 35680.72 -0.15
Lists//CheckMutex.5 121389.82 -0.14
Lists//NotFair.3 21227.04 -0.12
Miscellaneous//Tuple 74405.11 -0.10
Puzzles//Coins 121797.49 -0.03
Lists//NotFair.5 82702.13 -0.02
BitPrecise//MultMask 64778.00 +0.02
Miscellaneous//Complement.Empty 2163.98 +0.02
Miscellaneous//Complement.Unique 10455.03 +0.03
ProofTools/Sum.Correctness 34423.91 +0.20
Puzzles//sudoku 5 43498.25 +0.27
WeakestPreconditions//Correctness.Basics x>-5 9725.71 +0.27
Puzzles//sudoku 2 44028.80 +0.29
Puzzles//sudoku 0 71399.18 +0.32
Miscellaneous//Associativity.Intersection 10211.70 +0.32
Strings//FindInjection 7444303.42 +0.33
Uninterpreted//Correctness 3426.89 +0.33
Puzzles//MagicSquare.magic 2 3422.73 +0.33
Puzzles//sudoku 1 31370.04 +0.36
Miscellaneous//JoinMeet.2 10167.99 +0.38
Lists//CheckMutex.3 24159.47 +0.38
Puzzles//sudoku 6 70519.35 +0.38
Puzzles//sudoku 4 57918.89 +0.39
ProofTools//BMC.ex2 19145.45 +0.39
ProofTools//Strengthen.ex1 19725.50 +0.41
ProofTools//Strengthen.ex4 29140.26 +0.43
Puzzles//MagicSquare.magic 3 30923.57 +0.48
Miscellaneous//Complement.Full 2164.39 +0.49
Puzzles//sudoku 3 44485.06 +0.53
Miscellaneous//MaxE 11582.14 +0.55
Puzzles//NQueens.NQueens 4 8099.57 +0.55
Strings//puzzle3 65664.36 +0.63
Miscellaneous//MinE 11035.72 +0.69
WeakestPreconditions//Correctness.Basics x>0 9846.59 +0.81
Miscellaneous//test.2 2946.63 +0.82
Lists//NotFair.1 12356.44 +0.84
Puzzles//DogCatMouse 11728.74 +0.86
Transformers//Example.1 10036.90 +0.95
Miscellaneous//Idempotency.Cup 9381.04 +0.95
Optimizations//ExtField.problem 7613.39 +0.99
Puzzles//NQueens.NQueens 2 3283.18 +1.07
WeakestPreconditions/Correctness.Append 14045.27 +1.08
Uninterpreted//test 11302.03 +1.10
Transformers//Example.2 9825.43 +1.12
ProofTools//Strengthen.ex6 48770.63 +1.30
Puzzles//NQueens.NQueens 7 60300.37 +1.36
Miscellaneous//Idempotency.Cap 9438.48 +1.44
Optimizations//Enumerate.AlmostWeekend 9659.31 +1.54
Miscellaneous//Four 10106.07 +1.56
Miscellaneous/Birthday 11390.14 +1.62
Lists//CheckMutex.1 11019.93 +1.85
Miscellaneous//Domination.Cap 9883.81 +1.89
WeakestPreconditions//Correctness.GCD 14677.98 +2.07
WeakestPreconditions//Correctness.Basics skip-assign 10387.55 +2.08
Optimizations/LinearOpt.problem 7804.04 +2.54
WeakestPreconditions//Correctness.Basics y > x 9537.83 +2.66
Strings//puzzle2 23291.55 +2.69
Miscellaneous//test.1 3115.55 +2.85
WeakestPreconditions//Correctness.Basics y is even 11005.52 +2.97
WeakestPreconditions//ImperativeFib 81.66 +3.47
Miscellaneous//Domination.Cup 9881.55 +3.47
BitPrecise//Fast-max 5412.08 +3.55
Miscellaneous/Problem 10605.33 +4.45
Miscellaneous//Elts 10145.72 +4.49
Transformers//Example.3 16.16 +5.84
This probably won't exercise the space leak which from my observation only occurs when several models (>10 and over 1000 variables) are being requested, but it is a good data point regardless. In order to test the original use case I'll have to update my library which depends on sbv and profile it, which I won't get to until tomorrow most likely.
I bet these numbers will approach the IntMap
results (which were likely incorrect anyways) as we migrate more of the code to Sequence
and therefore remove reverse
's. But I think this is a good point to merge based on these results.
I think these results show that the changes are equivalent for the documentation examples. One might be able to make a case that it is slightly more performant (more -
than +
but the majority of these are probably within noise, e.g., Miscellaneous//Tuple
0.10
is percent better), but the real win, at least for me, is that profiling is easier because the types now have names and thus space leaks are easier to track down.
Let's give it a day or two and see if the original concern with large models/variables benefit from the changes. I suspect you might want to make a few more tweaks depending on what you find out there. I'll merge once the dust settles.
@doyougnu Any progress on this? Should we merge to master?
Hey Levent,
I haven't had a chance to rerun the original dataset to check the original issue. I will have time this weekend because my preliminary exam is Friday and so my work load will clear up and I can finally get back to programming :)
Good luck with the exams! No hurry on the merge, it'll eventually go in I'm sure.
Looks like a decent improvement, this used to take 158MB now is down to ~35MB.
Great! All merged to master and good to go. Thanks for the contributions.
I was talking with @doyougnu this last week and it sounded like there was some further work to be done in this direction. But I can’t seem to find an active ticket around what he mentioned to me.
I’m not aware of any other tickets. It’s likely there are other leaks, so would be good to dig deeper if anyone has the motivation and the resources.
Hey Levent,
I have an application written around sbv that generates then parses lots of models (thousands to tens-of-thousands) in query mode. As I was testing it I noticed it began to really slow down towards the higher end of this range. So I limited the input to only boolean formulas, did some profiling, and found a massive heap leak around in
getModelAtIndex
specifically this line. I doubt this line is the actual source of the leak because if you trace the logic back, it gets torinps
inState
which is a wrappedIORef
, and I believe the profiler can't see past theIORef
but I am not sure.So I tinkered with adding strictness for a few days to no avail, and then just decided this was a good opportunity to swap out the
rinps
data structure inState
for a Map of Sequences like this:where
Inputs
is:and then
NamedSymVar
's are changed to be strict:I also searched and changed every instance of
foldr
foldl
walk
sofar
go
and the like to have strict accumulators.There are numerous benefits besides plugging the heap leak and you can check my branch here. The thinking is that instead of doing list operations like
filter
we build data structures that create the right logic while the solver works. So instead of building a list then filtering, we build a map and never have to filter based onQuantifier
, rather, filtering becomes anO (log n)
lookup. From my testing (through my own application) I saw a huge speedup ~10x - 100x for problems of the same size that I tested before and was able to finish a computation that didn't finish after several hours.So I wanted to submit the PR today (given the magnitude of the changes I think this should be in the 8.9 release) but I am stuck getting the test suite to pass the tests, and they keep failing with:
So it looks like I've broken the link between the names somewhere even though almost all of my changes were merely syntactic with respect to the new data structures and not logical. So I wanted to ask the following:
Is there a good way in the test suite to run the tests with
verbose=True
so I can check the solver output. Right now I'm only testing with1%
of cases and I don't want to issue a PR until all checks pass of course.I noticed a lot of
reverse
's and sorting by node id's in the code base. Why does ordering matter? I've changed the code such that when a new symbolic is created we append to the sequence (which is still O(1)) instead of cons'ing onto a list and then reversing, thus I've removed the reversals that touched the refactored code.If an ordering is important I'd like to use a
Map
and exploit theOrd
instance on keys to perform the ordering instead of sorting. I'm not sure if that is possible right now as sorting by node id would require aHashMap
on user given names and internal names, its not impossible but I think would require a much larger change. Thus, If this is something that is desirable we should change these data structures, and then do the ordering/HashMap change.