Run z3 from java using ProcessBuilder

106 views Asked by At

I want to run a SMT solver from java in an interactive manner, send a sequence of command using stdin. The idea is, depending on the result more commands will be set via stdin.

running the code

public class SmtProcess {
SmtProcess() {
    String[] command = { "z3", "-in" , "-smt2"};

    ProcessBuilder process_builder = new ProcessBuilder(command);
    //process_builder.redirectErrorStream(true);
    Process process;
    try {
        process = process_builder.start();

        // Read out dir output
        InputStream is = process.getInputStream();
        InputStream iserr = process.getErrorStream();
        InputStreamReader isr = new InputStreamReader(is);
        InputStreamReader isrerr = new InputStreamReader(iserr);
        BufferedReader br = new BufferedReader(isr);
        BufferedReader brerr = new BufferedReader(isrerr);
        String line = new String();

        OutputStream os = process.getOutputStream();

        os.write(
                "(set-option :print-success false)(set-logic QF_UF)(declare-const p Bool)(assert (and p (not p)))(check-sat)(exit)"
                        .getBytes());

        System.out.printf("Output of running %s is:\n", Arrays.toString(command));
        do {
            while ((line = br.readLine()) != null) {
                System.out.println(line);

            }
            while ((line = brerr.readLine()) != null) {
                System.out.println(line);

            }
            process.wait(1000);
        } while (process.isAlive());

        // Wait to get exit value
        try {
            int exitValue = process.waitFor();
            System.out.println("\n\nExit Value is " + exitValue);
        } catch (InterruptedException e) {
            // TODO Auto-generated catch block
            e.printStackTrace();
        }
    } catch (IOException | InterruptedException e1) {
        // TODO Auto-generated catch block
        e1.printStackTrace();
    }
    }

public static void main(String[] args) {
        SmtProcess v = new SmtProcess();
    }
}

running the code there is not output.

Running on the command line

echo "(set-option :print-success false)(set-logic QF_UF)
      (declare-const p Bool)(assert (and p (not p)))(check-sat)(exit)" 
         | z3 -in -smt2

do give the result wanted.

How can the java code be changed to get the same results as when the command is run on the command line?

in the current case z3 was selected as the solver, a different solver may be used at a different time.

Update 1

Using apache.commons.exec

    PumpStreamHandler stream_handle = new PumpStreamHandler();
    String str = "(set-option :print-success false)(set-logic QF_UF)(declare-const p Bool)(assert (and p (not p)))(check-sat)(exit)";
    DataOutputStream cin;
    try {
        File yourFile = new File("score.txt");
        yourFile.createNewFile();
        cin = new DataOutputStream(new FileOutputStream(yourFile, false));      
        stream_handle.setProcessInputStream(cin);

        String line = " z3 -in -smt2 ";
        CommandLine cmdLine = CommandLine.parse(line);
        DefaultExecutor executor = new DefaultExecutor();
        executor.setStreamHandler(stream_handle);


        cin.writeBytes(str);
        int exitValue = executor.execute(cmdLine);

        System.out.println(exitValue);
    } catch (FileNotFoundException e1) {
        // TODO Auto-generated catch block
        e1.printStackTrace();
    } catch (IOException e1) {
        // TODO Auto-generated catch block
        e1.printStackTrace();
    }

When cin.writeBytes(str); is called a Stream Closed exception is thrown.

0

There are 0 answers