CODEWITHSUNDEEP
smtcvc4
Orson Baines
Orson Baines

Reputation: 93

Is there a way to parse SMT-LIB2 strings through the CVC4 C++ API?

I have a program that can dynamically generate expressions in SMT-LIB format and I am trying to connect these expressions to CVC4 to test satisfiability and get the models. I am wondering if there is a convenient way to parse these strings through the CVC4 C++ API or if it would be best to just store the generated SMT-LIB code in a file and redirect input to the cvc4 executable.

Upvotes: 0

Views: 504

Answers (4)

Heisenbug
Heisenbug

Reputation: 484

Workaround for parseSMTLIB2String in CVC5 with string input:

You can use this code to simulate parseSMTLIB2String (which is available in Z3) in CVC5.

public static void main(String[] args) {
        String smtlibString = "(set-logic QF_SLIA)\n" +
                              "(set-option :produce-models true)\n" +
                              "(declare-fun x () Int)\n" +
                              "(assert (> x 10))\n" +
                              "(assert (< x 20))\n" +
                              "(check-sat)\n" +
                              "(get-value (x))\n";

        ProcessBuilder processBuilder = new ProcessBuilder("<path to CVC runnable>/home/CVC5/cvc5/build/bin/cvc5", "--lang=smt2");
        processBuilder.redirectErrorStream(true);

        try {
            Process process = processBuilder.start();
            BufferedWriter writer = new BufferedWriter(new OutputStreamWriter(process.getOutputStream()));
            BufferedReader reader = new BufferedReader(new InputStreamReader(process.getInputStream()));

            writer.write(smtlibString);
            writer.flush();
            writer.close();

            String line;
            while ((line = reader.readLine()) != null) {
                System.out.println(line);
            }
            reader.close();
        } catch (IOException e) {
            e.printStackTrace();
        }
    }

Outout for the code above is :

sat
((x 11))

Upvotes: 1

Heisenbug
Heisenbug

Reputation: 484

You can use Z3 SMT solver for the time being because CVC does not support this parsing as of SMT-LIB2 string to Term.

Z3 Context has method : "parseSMTLIB2String" which will help you produce Expr out of SMT-LIB2 string which can be asserted to Z3 Solver to produce result model.

Ref link for 'parseSMTLIB2String': https://z3prover.github.io/api/html/classcom_1_1microsoft_1_1z3_1_1_context.html#ae6a8e05f503789a6737b7014f0521b2a

Upvotes: 0

Heisenbug
Heisenbug

Reputation: 484

Still, CVC5(or older versions of CVC) don't support parsing of SMT-LIB2 strings directly to return Term object.

But as per recent comment by one of CVC5 developer, v1.1 of CVC5 will support this feature. You can find the comment here: https://github.com/cvc5/cvc5/issues/3075#issuecomment-1710155230

Estimated ETA will be 1 month from the comments date.

Upvotes: 0

alias
alias

Reputation: 30525

A cursory look at their API doesn't reveal anything obvious, so I don't think they support this mode of operation. In general, loading such statements "on the fly" is tricky, since an expression by itself doesn't make much sense: You'd have to be in a context that has all the relevant sorts defined, along with all the definitions that your expressions rely on, including the selection of the proper logic. That is, for instance, why the corresponding function in z3 has extra arguments: https://z3prover.github.io/api/html/classz3_1_1context.html#af2b9bef14b4f338c7bdd79a1bb155a0f

Having said that, your best bet might be to ask directly at https://github.com/CVC4/CVC4/issues to see if they've something similar.

Upvotes: 0

Related Questions