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 Joss revisions, final push #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 (Joss revisions, final push #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.