elsoroka / Satisfiability.jl

Specify satisfiability modulo theories problems in Julia and use the SMT-LIB format to interact with SMT solvers.
https://elsoroka.github.io/Satisfiability.jl/
MIT License
29 stars 4 forks source link

Reals example in README.md doesn't work #32

Closed zygi closed 8 months ago

zygi commented 9 months ago

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
elsoroka commented 8 months ago

Hi, Thanks for finding this bug! PR #33 should fix it. You can get this fix immediately by uninstalling your current version and reinstalling with Pkg.add(url="https://github.com/elsoroka/Satisfiability.jl")