Skip to content

Smt2lib parser in C-API #344

@AndreaCallia

Description

@AndreaCallia

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions