0

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.

3
  • "Convenient". Probably not by a reasonable person's definition. This can be done at the SMT-LIB command level in an ok fashion (see SMT-LIB 2.6 section 3.9 for command). (FWIW just term parsing is harder than it sounds as terms can generates implicit commands.) The interactive shell is doing this and is not supposed to use private APIs. (These might have creeped in.) I'd start trying to understand that code if this feature is really important. Maybe something better has been added recently?
    – Tim
    Commented Jun 5, 2020 at 16:53
  • @Tim So if I understand you correctly, you can parse the smt-lib commands individually using the parser api with a string input and then invoke the commands on an smt-engine with command.invoke() method. This is much more inconvenient than in z3, but it's good to know that it can be done. Commented Jun 5, 2020 at 23:26
  • "commands individually". What is available is a sequence of commands. The parser tries to handle a stream of text. That can contain multiple commands. Also a command in text can also turn into multiple Command objects as syntactic sugar gets removed, e.g. [ :named ](github.com/CVC4/CVC4/blob/master/src/parser/smt2/Smt2.g#L2244).
    – Tim
    Commented Jun 9, 2020 at 17:10

4 Answers 4

1

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))
1
  • In the end I decided to go with an approach very similar to this and it did work well for my use case. Commented Mar 25 at 0:13
0

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.

0

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.

0

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.