JOSS Review Comments

[computablee]

Hello! First, I want to mention that it has been a pleasure to see some SMT work being submitted to JOSS. I have checked almost all of the boxes on my review, but there are just a couple of things that I think could be improved. I'll go over each major section of my checklist and explain why I've checked what I did, and why I haven't checked what I didn't.

From the JOSS submission.

Functionality

• The software seems functional to me. I didn't run every single example given, but I did run several from the site, and all seemed to work as expected.
• Installation worked as expected with no problems.
• There are no performance claims, so that is a non-issue.

Documentation

• I see an adequate statement of need, so that's fine.
• I do not see a list of dependencies anywhere. That list would be great to see somewhere in the documentation. If I've missed it, please point me to where it is.
• There are examples and decent-looking documentation of all of the supported functions, so those are good.
• The tests run, but I encountered one error and several warnings based on the main branch I pulled tonight (commit dd89b1b). The tests that ran did pass, but I don't know if there were tests that didn't run due to errors, or if the warnings are something I should worry about.
• I do not see a CONTRIBUTING.md for contributing to the repository. I also don't see a CODE_OF_CONDUCT.md or issue templates. Please consider adding these.

Software Paper

• The summary looked good to me, and provided a good overview of SMT and Satisfiability.jl
• You may want to consider emphasizing that the use of SMT-LIB is important because this ensures (mostly) compatibility between different SMT solver backends.
• State of the field adequately describes other SMT solver interfaces in other languages, and emphasizes that Satisfiability.jl is the first of its kind for Julia.
• The writing quality looked okay to me.
• References looked good
• I think code examples in the paper would be a good addition.

Nitpicks

• I don't see a full list of supported SMT solvers. I see Z3 and CVC5 listed, but I've been unable to find a way to run with other solvers like Alt-Ergo or CVC4.
• Some parts of the tutorial on the site are poorly written. For example, you write "Suppose you have Boolean variables p, q and r. A common mistake made by students in discrete math classes is to think that if p implies q and q implies r ((p ⟹ q) ∧ (q ⟹ r)) then p must imply r (p ⟹ r)." This is not a mistake, and is in fact a valid deduction. The statement the tutorial attempts to debunk with SMT is whether (p ⟹ q) ∧ (q ⟹ r) is true if and only if (p ⟹ r), not whether the former implies the latter as referenced by the text. Changing the code we verify that the example given does indeed hold:

using Satisfiability

@satvariable(p, Bool)
@satvariable(q, Bool)
@satvariable(r, Bool)

conjecture = ((p ⟹ q) ∧ (q ⟹ r)) ⟹ (p ⟹ r)
status = sat!(!conjecture, solver=Z3())

UNSAT

• In addition, there are some typos and grammatical errors throughout the site. such as "langugages" instead of "languages".
• On the GitHub releases page, there is a v0.1.2 out, but this is not reflected in other parts of the documentation like the site.

Conclusion

Overall, I think a lot of the things here are minor and easily fixable. I don't think there's any glaring issues with the submission, so I cast my review as an acceptance with minor revisions. Thank you again for your submission!

[diehlpk]

Hi @elsoroka could you please have a look.

[elsoroka]

Hi! yes, so sorry this has been delayed. I am working at an internship over the summer and have limited time -- we get a couple days off for the holiday this week so I'm targeting end of the week to address these comments.

[elsoroka]

Addressing comments:

Documentation

• The tests run, but I encountered one error and several warnings based on the main branch I pulled tonight (commit dd89b1b). The tests that ran did pass, but I don't know if there were tests that didn't run due to errors, or if the warnings are something I should worry about.
  PR #55 should suppress warnings in the tests.

• I do not see a CONTRIBUTING.md for contributing to the repository. I also don't see a CODE_OF_CONDUCT.md or issue templates. Please consider adding these.
  Thank you for the suggestion! They are added: contributing.md is in the documentation and linked in the README. The code of conduct issue, I resolved by linking the Julia community standards.

Paper

• I made some edits to address this and am figuring out how to commit them in the right place.

Nitpicks

• Some parts of the tutorial on the site are poorly written.
  Thanks for catching it; I couldn't figure out how to put the iff statement in words clearly, so I just changed the code to the lines you suggested (#55).

• I don't see a full list of supported SMT solvers. I see Z3 and CVC5 listed, but I've been unable to find a way to run with other solvers like Alt-Ergo or CVC4.
  This is interesting: what did you try? I want to see what's going wrong @computablee

[computablee]

@elsoroka I tried the following for CVC4 and similar for Alt-Ergo:

using Satisfiability

@satvariable(p, Bool)
@satvariable(q, Bool)
@satvariable(r, Bool)

conjecture = ((p ⟹ q) ∧ (q ⟹ r)) ⟹ (p ⟹ r)
status = sat!(!conjecture, solver=CVC4())
println(status)

Receiving:

ERROR: LoadError: UndefVarError: `CVC4` not defined
Stacktrace:
 [1] top-level scope
   @ ~/prop.jl:8

As for everything else, the only thing remaining that I haven't seen is a clear list of dependencies. Once that is resolved and I hear a response from this comment, I think I'll be satisfied with the submission. Almost everything is checked on my checklist.

[elsoroka]

Not a fix yet: I tested this for CVC4 and I can see two things:
There isn't a Solver object defined for CVC4 in Satisfiability.jl But we can make our own using a command like
CVC4 = Solver("CVC4", cvc4 --lang smt2 --interactive --produce-models --qqq)
Then sat!(expr, solver=CVC4) should work, but doesn't return...I think something is wrong with how the output of CVC4 is being parsed by my code.
see: https://elsoroka.github.io/Satisfiability.jl/dev/advanced/#Custom-solver-options-and-using-other-solvers

I'm looking into why this is and will respond with an update.

[elsoroka]

Explanation: CVC4 prints input on its output!

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

@computablee what are your thoughts on this? Are you aware of a command-line option for cvc4 that will stop the input from being echoed to the output? If so, that would fix the problem.
Another fix I am going to make today is explaining in the documentation that using another solver is sort of experimental, and issues like this may come up/users are encouraged to open issues about them.

[computablee]

@elsoroka I'm not aware of such an option. There is a Python API and a C++ API for CVC4, but I realize implementing either of those is asking a lot when CVC5 is already supported and better in almost all ways in my experience. I know the Why3 platform can interface with both CVC4 and CVC5... it might be worth checking how they do it.

In my opinion, just knowing that CVC4 is not supported is sufficient. I wasn't aware of the Solver() call to load in a new SMT solver, so I'm fine on my end to mark that as solved.

[elsoroka]

Does Alt-Ergo work

I'm actually not sure how to test this. The reason is Satisfiability.jl relies on opening an interactive session, so we can do things like decide whether to say (get-model) after (check-sat) (because (get-model) isn't a valid command if (check-sat) is invalid).
I read the documentation and I am not sure whether this is a thing. I only see examples of file input. https://ocamlpro.github.io/alt-ergo/latest/Usage/index.html

This has overall been helpful because now we have more examples to discuss in the documentation. And I will make a Git issue about CVC4 and your suggestions for other packages that work with it @computablee.

Dependencies

They are in the Project.toml file https://github.com/elsoroka/Satisfiability.jl/blob/main/Project.toml

[elsoroka]

@computablee are you ready to mark this thread solved?

[diehlpk]

@computablee could you please have a look?

[computablee]

So sorry about the late response! Work has been busy. Yes, I think my issues have been solved. I'll mark it on the review thread. Would you like me to close this issue?

[elsoroka]

I think since the review thread is solved @computablee, this one can be closed. Thank you!

[computablee]

Sounds good! Closing @elsoroka