Example #3 in README.md is broken.
Closed this issue · 2 comments
rafaelbailo commented
Running
using Satisfiability
@satvariable(x, Bool)
@satvariable(y, Bool)
@uninterpreted(f, Bool, Bool)
# Yices requires setting the logic manually. Here we set it to "QF_UFLIA" - "Quantifier free uninterpreted functions, linear integer arithmetic".
status = sat!(distinct(x, y), f(x) == y, f(f(x)) == x, solver=Yices(), logic="QF_UFLIA")
println("status = \$status")
yields the error
ERROR: IOError: could not spawn `yices-smt2 --interactive --smt2-model-format`: no such file or directory (ENOENT)
Stacktrace:
[1] _spawn_primitive(file::String, cmd::Cmd, stdio::Vector{Union{RawFD, IO}})
@ Base ./process.jl:128
[2] #784
@ ./process.jl:139 [inlined]
[3] setup_stdios(f::Base.var"#784#785"{Cmd}, stdios::Vector{Union{RawFD, IO}})
@ Base ./process.jl:223
[4] _spawn
@ ./process.jl:138 [inlined]
[5] _spawn(::Base.CmdRedirect, ::Vector{Union{RawFD, IO}}) (repeats 3 times)
@ Base ./process.jl:166
[6] run(::Base.CmdRedirect; wait::Bool)
@ Base ./process.jl:483
[7] run
@ ./process.jl:477 [inlined]
[8] open(s::Solver)
@ Satisfiability ~/rfs/rev/rev101_JOSS_Satisfiability/Satisfiability/src/call_solver.jl:134
[9] talk_to_solver(input::String, s::Solver)
@ Satisfiability ~/rfs/rev/rev101_JOSS_Satisfiability/Satisfiability/src/call_solver.jl:162
[10] sat!(::BoolExpr, ::Vararg{…}; solver::Solver, logic::String, clear_values_if_unsat::Bool, line_ending::String, start_commands::String, end_commands::String)
@ Satisfiability ~/rfs/rev/rev101_JOSS_Satisfiability/Satisfiability/src/sat.jl:50
[11] top-level scope
@ REPL[7]:1
Some type information was truncated. Use `show(err)` to see complete types.
elsoroka commented
I can't reproduce this issue...It might happen from not having Yices installed. Does the underlying command
yices-smt2 --interactive --smt2-model-format
work in the terminal?
This was in the README to show that different solvers can be used. So I think a fix is to mention how to call the example with different solvers.
rafaelbailo commented
Does the underlying command
yices-smt2 --interactive --smt2-model-format
work in the terminal?
Indeed, it does not; I mistakenly assumed that because Z3 was installed automatically, the same would be true of Yices. Closing this.