dreal/dreal3

Smt2lib parser in C-API

Opened this issue · 0 comments

Dear dReal developers,

is there an SMT2 parser in the dReal project which can be used together with the C-API? I mean somehing similar to the parse_smt2_string() function provided by the z3 python API to convert an SMT2 string into a formula which can be added to a solver. An example of how this function is used in the z3 python API is below.

import z3
example = """
(declare-const x Real)
(assert (> x 0.0))
(assert (< x 2.0))
"""
f = z3.parse_smt2_string(example)
s = z3.Solver()
s.add(f)
s.check()
s.model()

and the output by z3 is:

sat
[x = 1]

If such a parser is not directly available in the C-API, is there some indirect way to access it, perhaps by changing something in the dReal source code?

This may help me very much to make an interactive version of dReal as proposed here

Many thanks for your wonderful work...

PS I have built dReal in a Ubuntu 14.04 64bit machine with clang-3.8.