smtcvc4

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.


Solution

  • 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))