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