43 observable sharing

[bruderj15]

No description provided.

[fabeulous]

It's nice to see the sharing worked out for SMT and OMT 👍

Unfortunately, the sharing in Pipe doesn't interact well with MonadIncrSMT.

For example:

example :: IO ()
example = do
  z3Inter <- interactiveSolver z3
  res <- debugInteractiveWith @Pipe (z3Inter) $ do
     setLogic "QF_LIA"
     x <- var @IntSort
     let a1 = x + x
         an = a1 === 2
     push
     assert an
     pop
     assert an
     solve
     return ()
  return ()

will produce a runtime error

"(error \"line 1 column 199: unknown constant var_3\")"
lpo-encoding: string
CallStack (from HasCallStack):
  error, called at src/Language/Hasmtlib/Type/Pipe.hs:114:9 in hasmtlib-2.3.2-inplace:Language.Hasmtlib.Type.Pipe

This is down to sharing the expression of an, but only introducing the corresponding variable var_2 after the push. The pop removes the variable and assertion from the stack, but var_2 is reused in the second assert.

(set-logic QF_LIA)
(declare-fun var_1 () Int)
(push 1)
(declare-fun var_2 () Int)
(assert (= var_2 (+ var_1 var_1)))
(declare-fun var_3 () Bool)
(assert (= var_3 (= var_2 2)))
(assert var_3)
(pop 1)
(assert var_3)
(check-sat)
(error "line 1 column 199: unknown constant var_3")

[bruderj15]

Good catch!
Most simple solution seems to be clearing the entire stableMap on a pop. However we may loose out on a lot of possible sharing doing so.
Better: Similar to the Solver, keep track of the assertions on the incremental stack. Then delete corresponding entries in stableMap when popping.
I will add this to the PR.

[bruderj15]

That solution is a little ugly but keeps memory overhead little.
Your example now results in:

(set-logic QF_LIA)
(declare-fun var_1 () Int)
(push 1)
(declare-fun var_2 () Int)
(assert (= var_2 (+ var_1 var_1)))
(declare-fun var_3 () Bool)
(assert (= var_3 (= var_2 2)))
(assert var_3)
(pop 1)
(declare-fun var_4 () Int)
(assert (= var_4 (+ var_1 var_1)))
(declare-fun var_5 () Bool)
(assert (= var_5 (= var_4 2)))
(assert var_5)

[fabeulous]

Nice! The added stack fixes the issue I mentioned 👍

While testing I only noticed two possible issues with performance (see my other comments).

[fabeulous]

Here you likely want to clean up the stack with something like:

stackHeightAuxMap.at (smt^.incrStackHeight) .= Nothing

otherwise, the stack level will not be empty after another push call.
For me adding this reduces the runtime of

example :: IO ()
example = do
  z3Inter <- interactiveSolver z3
  debugInteractiveWith @Pipe (z3Inter) $ do
    setLogic "QF_LIA"
    x <- var @IntSort
    forM_ [1..5000] $ \_ -> do
      let bn = nest 2 x
          an = bn === 2
      push
      assert an
      pop
  return ()
 where 
  nest 0 x = x
  nest n x = nest (n-1) (x + x)

from 7.3s to 0.33s.

Since you only access the stackHeightAuxMap at incrStackHeight, a simpler stack representation like [[StableName ()]] could also be used.

[bruderj15]

Great input once again.
We will clean the stack and replace the IntMap with Seq (Seq (StableName ())).

[fabeulous]

I think grnf reducing the expression to normal form is unnecessary. For makeStableName it should be enough to evaluate to weak head normal form with:

makeStableName' x = x `seq` fmap unsafeCoerce (makeStableName x)

For deeply nested expressions with a lot of sharing grnf could have exponential run-time compared to just seq. For the following example removing grnf reduces the runtime from 29s to 0.01s on my machine, while producing the same SMTLib output.

example :: IO ()
example = do
  z3Inter <- interactiveSolver z3
  debugInteractiveWith @Pipe (z3Inter) $ do
    setLogic "QF_LIA"
    x <- var @IntSort
    let bn = nest 30 x
        an = bn === 2
    push
    assert an
    pop
  return ()
 where 
  nest 0 x = x
  nest n x = nest (n-1) (x + x)

[bruderj15]

Right, overshot here.

[bruderj15]

I highly appreciate your help, many thanks!