Formula can not be retrieved from a String using OpenSMT

[gcarpio21]

While trying to parse the String output from the method printResolutionProofSMT2 from the OpenSMT API I could not find a way to recover the formulas from their name used in the String. E.g., the boolean formula q1 appears in the proof but I can not use this to get the Formula instance associated with the term of said name that was used in the query.

I am trying to do this in this method: https://github.com/sosy-lab/java-smt/pull/458/files#diff-01498cb858bbe623fc3598d725d0563234f9fa324c959e113258d8bd84edbb0aR45 for the #458 PR. I knew beforehand the exact way in which I tried wouldn't work but I wanted to test the output.

[daniel-raffler]

Hello Gabriel,
could you post an example for such a proof? The proofs may contain :named terms like these:

(=> (! (> x y) :named p1)
    (! (= x z) :named p2))

OpenSMT does have a way to get the formulas from the name, but the API is not included in our Java bindings. I could add MainSolver.getTermNames() and TermNames.termByName(String name) to the bindings. Would that fix the issue for you? Or do you also need to create new named terms?

[gcarpio21]

Hi,
when trying to parse a proof like the following:

(proof 
(let (cls_13 q1 )
(let (cls_9 (or q2 (not q1) ))
; q2 
(let (cls_16 (res cls_9 cls_13 q1))
(let (cls_19 (not q2) )
; -
(let (cls_4294967295 (res cls_19 cls_16 q2))
cls_0
)))))
:core
( cls_9 cls_13 cls_19 )
)

The problem is that I can not seem to find a way to retrieve the q1 term just from the String "q1".

[daniel-raffler]

If q1 is just a variable that was part of your assertion s, you should be able to recreate it with BooleanFormulaManger.makeVariable. This won't create a new formula, but will simply return the existing term.

More generally you could also use FormulaManager.parse to get the term reference for any of the formulas (f.ex the (or q2 (not q1) ) in your the next line) from the proof.

OpenSMT does have an internal representation for these proofs and only prints them when printResolutionProofSMT2 is called. If parsing the formulas back doesn't work we could probably still ask them to return the proof in some other form.

[gcarpio21]

I tried this and it works somewhat. While testing I noticed while debugging that strings like "(or q2 (not q1))" and "(not q2)" get parsed into true. This is while using FormulaManager.parse.

I also noticed the same problem here: https://github.com/sosy-lab/java-smt/pull/458/files#r2112391976

Also, I am unsure about only using boolean formulas. Some solvers end up with representations from other theories even when continuing the proof with clauses, e.g., SMTInterpol. We should contact the developers to confirm this approach.

[daniel-raffler]

I've just had a look at your last example, and I believe you just have to wrap the formula in an assert command. So, instead of calling FormulaManager.parse with "(or q2 (not q1))", just pass "(assert (or q2 (not q1)))" to it. There still seems to be some issues with the test, but at least the formulas were parsed fine when I tried it in the debugger.

Also, I am unsure about only using boolean formulas. Some solvers end up with representations from other theories even when continuing the proof with clauses, e.g., SMTInterpol. We should contact the developers to confirm this approach.

It should be safe to use FormulaManager.parse to create variables of "unknown" type. They were declared earlier when the original formula was created and the solver should still know their types. However, if it's too much effort to recover those formulas from the String output, feel free to ask the developers if they can do anything about the API.