Reals example in README.md doesn't work
Closed this issue · 1 comments
zygi commented
repro.jl:
using Satisfiability
@satvariable(xR, Real)
@satvariable(yR, Real)
@satvariable(x, Int) # x represents a rounded version of xR
@satvariable(y, Int) # y represents a rounded version of yR
@satvariable(a, Int)
exprs = [xR + yR < a,
x + y > a,
or(x == xR, ((x < xR) ∧ (xR < x+1)), ((x-1 < xR) ∧ (xR < x))),
or(y == yR, ((y < yR) ∧ (yR < y+1)), ((y-1 < yR) ∧ (yR < y))),
]
status = sat!(exprs)
println("status = $status, xR=$(value(xR)), yR=$(value(yR))")Running it produces an error:
ERROR: LoadError: MethodError: no method matching to_real(::Int64)
Closest candidates are:
to_real(::IntExpr)
@ Satisfiability ~/.julia/packages/Satisfiability/HQRyl/src/IntExpr.jl:465
Stacktrace:
[1] __propagate_value!(z::RealExpr)
@ Satisfiability ~/.julia/packages/Satisfiability/HQRyl/src/sat.jl:288
[2] assign!(z::RealExpr, assignment::Dict{Any, Any})
@ Satisfiability ~/.julia/packages/Satisfiability/HQRyl/src/sat.jl:334
[3] (::Satisfiability.var"#195#196"{Dict{Any, Any}})(z::RealExpr)
@ Satisfiability ~/.julia/packages/Satisfiability/HQRyl/src/sat.jl:331
[4] iterate
@ ./generator.jl:47 [inlined]
[5] collect_to!(dest::Vector{Float64}, itr::Base.Generator{Vector{AbstractExpr}, Satisfiability.var"#195#196"{Dict{Any, Any}}}, offs::Int64, st::Int64)
@ Base ./array.jl:892
[6] collect_to_with_first!(dest::Vector{Float64}, v1::Float64, itr::Base.Generator{Vector{AbstractExpr}, Satisfiability.var"#195#196"{Dict{Any, Any}}}, st::Int64)
@ Base ./array.jl:870
[7] _collect(c::Vector{AbstractExpr}, itr::Base.Generator{Vector{AbstractExpr}, Satisfiability.var"#195#196"{Dict{Any, Any}}}, ::Base.EltypeUnknown, isz::Base.HasShape{1})
@ Base ./array.jl:864
[8] collect_similar(cont::Vector{AbstractExpr}, itr::Base.Generator{Vector{AbstractExpr}, Satisfiability.var"#195#196"{Dict{Any, Any}}})
@ Base ./array.jl:763
[9] map(f::Function, A::Vector{AbstractExpr})
@ Base ./abstractarray.jl:3282
[10] assign!(z::BoolExpr, assignment::Dict{Any, Any})
@ Satisfiability ~/.julia/packages/Satisfiability/HQRyl/src/sat.jl:331
[11] #154
@ ~/.julia/packages/Satisfiability/HQRyl/src/sat.jl:56 [inlined]
[12] iterate
@ ./generator.jl:47 [inlined]
[13] _collect(c::Vector{BoolExpr}, itr::Base.Generator{Vector{BoolExpr}, Satisfiability.var"#154#157"{Dict{Any, Any}}}, ::Base.EltypeUnknown, isz::Base.HasShape{1})
@ Base ./array.jl:854
[14] collect_similar(cont::Vector{BoolExpr}, itr::Base.Generator{Vector{BoolExpr}, Satisfiability.var"#154#157"{Dict{Any, Any}}})
@ Base ./array.jl:763
[15] map(f::Function, A::Vector{BoolExpr})
@ Base ./abstractarray.jl:3282
[16] #153
@ ~/.julia/packages/Satisfiability/HQRyl/src/sat.jl:55 [inlined]
[17] map
@ ./tuple.jl:291 [inlined]
[18] sat!(prob::Vector{BoolExpr}; solver::Solver, logic::Nothing, clear_values_if_unsat::Bool, line_ending::String, start_commands::String, end_commands::String)
@ Satisfiability ~/.julia/packages/Satisfiability/HQRyl/src/sat.jl:55
[19] sat!(prob::Vector{BoolExpr})
@ Satisfiability ~/.julia/packages/Satisfiability/HQRyl/src/sat.jl:34
[20] top-level scope
@ ~/tsp_qap_lp_solver_v3-Extd/repro.jl:14
in expression starting at /home/nonagon/tsp_qap_lp_solver_v3-Extd/repro.jl:14