Why CVC4 doesn't work out-of-the-box

[elsoroka]

From @computablee's JOSS review thread (issue #50):

Our investigation of why CVC4 doesn't work

First, a command that should work for launching CVC4 is
cvc4 --lang smt2 --interactive --produce-models --no-interactive-prompt -q
This will launch an interactive SMT2 command-line with no input prompt (the CVC4>) and no welcome message.

MWE of something that should work:

using Satisfiability
# really simple problem
@satvariable(a, Bool)
@satvariable(b, Bool)
	
conjecture = iff(a ∧ b, ¬(¬a ∨ ¬b))
print(smt(conjecture)) # just to check

# Define a new Solver object
# https://elsoroka.github.io/Satisfiability.jl/dev/advanced/#Custom-solver-options-and-using-other-solvers
CVC4() = Solver("CVC4", `cvc4 --lang smt2 --interactive --incremental --produce-models --no-interactive-prompt -q`)

# This should work, but it does not.
# Note that the logic is set because CVC4 requires it, while Z3 and CVC5 don't.
sat!(conjecture, solver=CVC4(), logic="ALL")

When we do this, we get the error

Solver error:
 (set-option :print-success false)
(set-option :print-success false)
(set-logic ALL)
(declare-fun a () Bool)
(declare-fun b () Bool)
(assert (= (and a b) (not (or (not b) (not a)))))
(check-sat)
sat

Now, "Solver error" is printing the output Satisfiability.jl got from CVC4. Internally, this is what sat! does:

• If logic is manually set, we issue (set-logic $LOGIC)
• We issue the commands generated by smt(conjecture) to define the variables and assert the problem
• We issue (check-sat). If the response is sat, we issue (get-model) to retrieve the satisfying assignment.

So this almost looks right. But the problem is...

CVC4 echoes the input (stdin) to the output (stdout)

That's why the INPUT lines (set-logic), (declare-fun) etc. appear in the error.

This is really sneaky because to our eyes, this is right. But to the parser, which was expecting either sat or unsat (or an error), this is an error.

Here's a comparison with Z3:

Demonstration: finding our input on CVC4's stdout

# Now we can open an interactive process to inspect what's going on
begin
	isolver = open(CVC4())
	
	send_command(isolver, "(set-logic ALL)", dont_wait=true)
	assert!(isolver, conjecture)
	
	sleep(0.02)
	println("Read from pstdout:")
	__stdout = readavailable(isolver.pstdout)
	print(String(__stdout))
	
	# Instead of waiting for sat, we'll leave the output in the pipe and print it manually
	send_command(isolver, "(check-sat)", dont_wait=true)
	println("\nFinished sending commands.")
	
	println("Now pstdout should read SAT")
	sleep(0.02)
	__stdout = readavailable(isolver.pstdout)
	print(String(__stdout))
	
	close(isolver)
end

Output:

Read from pstdout:
(set-option :print-success false)
(set-logic ALL)
(declare-fun a () Bool)
(declare-fun b () Bool)
(assert (= (and a b) (not (or (not b) (not a)))))

Finished sending commands.
Now pstdout should read SAT
(check-sat)
sat

Demonstration: Z3 doesn't do this

# Now we can open an interactive process
# this will allow us to inspect what's going on
begin
	isolver_2 = open(Z3())
	
	assert!(isolver_2, conjecture)

	# We don't read here because readavailable() will hang
	# there are NO byptes in pstdout because Z3 does not have this behavior
	
	# Instead of waiting for sat, we'll leave the output in the pipe and print it manually
	send_command(isolver_2, "(check-sat)", dont_wait=true)
	println("Finished sending commands.")
	
	println("Now pstdout should read SAT")
	sleep(0.02)
	__stdout2 = readavailable(isolver_2.pstdout)
	print(String(__stdout2))
	
	close(isolver_2)
end

Output:

Finished sending commands.
Now pstdout should read SAT
sat

From comments:

There is a Python API and a C++ API for CVC4,. Also, the Why3 platform can interface with both CVC4 and CVC5... it might be worth checking how they do it.

To make CVC4 work we need to turn off echoing the input to the output. At some point this must have been identified as a problem, because CVC5 doesn't do it.

[mykelk]

I'm 100% okay with just supporting CVC5 over CVC4.