Additional SMTLib2 support

[robdockins]

Would it be easy to add support for the :global-declarations option and the get-info operation? They are convenient for certain kinds of interactive use cases. Cf http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf

$ stp
(set-option :global-declarations true)
unsupported

$ stp
(get-info :version)
(error "syntax error: line 1 syntax error  token: get-info")

$ stp
(get-info :error-behavior)
(error "syntax error: line 1 syntax error  token: get-info")

[aytey]

I might be able to take a look at global-declarations -- do you have a small, self-contained example of where this makes sense/is necessary?

This is where the SMTLIB2 front-end handles pop: https://github.com/stp/stp/blob/master/lib/Interface/cpp_interface.cpp#L356

So, I think, it is just a case of ensuring that we don't remove the symbols that you don't want popped.

It seems those get-info commands you've listed are required to claim SMTLIB2.6 support (see 4.1.8 of the SMTLIB reference), but I don't actually know if STP claims this.

[aytey]

If you care about global-declarations, do you also care about reset-assertions?

[robdockins]

Sure, I can come up with a test case.

However, the larger context is quite a bit less self-contained. What I'm doing involves symbolic execution of programs and I use interactive solving with lots of push/pops to keep track of the control-flow conditions that lead to assertions in the program. We don't know in advance which parts of the potential problem space will be relevant to a solver query, so terms are streamed to the solver on-demand. These terms can get quite large, so it's a shame to have to stream them again if they are forgotten on a pop (and the bookeeping on my end is much trickier to keep track of which terms need to be streamed again).

And, yes, good catch: reset-assertions is also relevant to this use case.

[aytey]

Baby-steps: if you can provide an easy/minimal/self-contained example, I can take look at getting that working (but no promises).

Then, once the easy bit is done, we can take a look at some larger examples :)

If you can give an example with and without reset-assertions that would also help!

[robdockins]

I was working on a small example to demonstrated the desired behavior. Somewhat to my surprise, STP already behaves as though global-declarations is set.

STP-online-quickstart.txt

[aytey]

If you don't have global-declarations and you pop a previous symbol, do you expect to able to have the ability to create a symbol with a different type?

I would imagine that this works by luck, rather than by design.

With STP, the end of the run looks like this:

success
success
success
success
success
success
success
success
success
unsat
success

but for Boolector:

boolector: blah.smt2:48:14: undefined symbol 'x!2'

and CVC4:

(error "Parse Error: blah.smt2:48.16: Symbol x!2 is not declared.

  (assert (not x!2))
               ^
")

[robdockins]

If you don't have global-declarations and you pop a previous symbol, do you expect to able to have the ability to create a symbol with a different type?

That is my understanding of the behavior specified by the standard. I think it's kind of crazy, which is why I prefer to work with the global-declarations mode.

The relevant language from the standard is:

Popping a level from the assertion stack has the effect of undoing all assertions in it,
including symbol declarations and definitions. An input option, :global-declarations,
allows the user to make all symbol declarations and definitions global to the assertion stack.
In other words, when that option is enabled, declarations and definitions become permanent,
as opposed to being added to the assertion stack.

[aytey]

Okay, so that's what I expected (without reading it).

Think about this:

(set-option :global-declarations false)
(push 1)
(declare-fun x!0 () Bool)
(assert (not x!0))
(check-sat)
(get-model)
(pop 1)
(push 1)
(declare-fun x!0 () (_ BitVec 32))
(assert (= x!0 (_ bv0 32)))
(check-sat)
(get-model)

This works for STP, irrespective of the value you give you :global-declarations; Boolector rightly complains if you give a value of true.

[robdockins]

Here is a similar example using (reset-assertions), which is accepted, e.g., by Z3 but fails for STP.

quickstart-alt.txt

[TrevorHansen]

As we all acknowledge, the default behaviour of STP should be to treat global-declaration as false.

For symbols, there's a vector created(in the cpp_interface.h file) at each push level that stores the symbols created at that level. When the level is popped away, the references to the symbols in the relevant vector are removed. What's supposed to happen is that no other references to that symbol exist - so it's reference count drops to zero and the symbol is deleted.

Although there should be, there's no similar mechanism for functions. They're put in a map and kept around forever.

Cutting back the longer example @robdockins provided:

(push 1)
(declare-fun x!1 () Bool)
(define-fun x!2 () Bool (not  x!1))
(pop 1)
(assert (not x!1))
; x!1 should have been popped so should error.
(assert (not x!2))
; x!2 should have been popped so should error.

Shows what goes wrong.

So the first step is to fix function handling (on pop) in STP. Is this something you want to work on @andrewvaughanj otherwise I can fix it?

[aytey]

I’m happy to take a look/give it ago, and I should be able to take a look this week.

That being said, I was offering more as way to learn more about STP and support its community, rather than already knowing the solution.

On some other issue trackers, Rob has suggested he is in no rush for this — @TrevorHansen if you’re happy to wait and then review a PR by me, then I’m happy to try!

[aytey]

Weirdly, this "works" (when we don't want it to):

(push 1)
(declare-fun x!1 () Bool)
(define-fun x!2 () Bool (not x!1))
(pop 1)
(assert (not x!1))

but this is has the correct behaviour (w.r.t. :global-declarations being implicitly false):

(push 1)
(declare-fun x!1 () Bool)
(pop 1)
(assert (not x!1))

What I mean here is that the use of an uninterpreted function symbol inside of a function declaration somehow makes the uninterpreted function symbol "escape" the pop.

Indeed, this has the correct behaviour (giving a parse error):

(push 1)
(declare-fun x!1 () Bool)
(declare-fun x!2 () Bool)
(define-fun x!3 () Bool (not x!2))
(pop 1)
(assert (not x!1))

[aytey]

Ah! I think when you use x!2 in a function declaration (like with x!3) then the reference count of x!2 is two (once for itself and once for its use in x!3).

When you do the pop, we remove x!2 itself, so the ref count goes to 1, but this isn't enough for x!2 to be removed from the symbol table, which is why it can still be resolved later on.

This particular problem will be resolved if functions are treated like symbols in cpp_interface.cpp.