Conversation
samysweb
left a comment
samysweb
left a comment
There was a problem hiding this comment.
Overall this looks good, I left a few small minor comments. I'll look into rational support for Satisfiability.jl
| # this avoids numbers ≥ 1000000 in the expression | ||
| # which avoids unknown Symbol error in the Solver | ||
| # the zero_var is introduced to avoid simplification by Satisfiability | ||
| function secure_int(val::Integer, zero_var) |
There was a problem hiding this comment.
Maybe we can turn LIMIT into a global, configurable constant
There was a problem hiding this comment.
I gave this some more thought: While I like the idea, it's unfortunate that we end up needing division of expressions where it's not necessary. I am looking into adding Rational{BigInt} support for Satisfiability.jl right now, I think there's a good chance that's feasible...
| return smt_cache[n] | ||
| end | ||
| # same value as the Z3 implementation | ||
| x_rat = rationalize(Int32,Float32(n.value)) |
There was a problem hiding this comment.
I think with secure_int in place, we could get rid of this, right?
There was a problem hiding this comment.
Related to Rational support -> I'll look into this
| #print_msg("[SMT] ", constraints[conflict_clauses[string(c)]]) | ||
| push!(conflicts,conflict_clauses[string(c)]) | ||
| end | ||
| # TODO |
There was a problem hiding this comment.
I want to have another look at whether I can get the cores to work. If not, we should throw an error here until we have a fix.
| @satvariable(C[1:n], Bool) # conflict bools | ||
| additional = [] | ||
|
|
||
| cons_trans = map(con -> ast2smt(con, variables, additional, Dict()), constraints) |
There was a problem hiding this comment.
Here and also in lin_feasible: Ideally, we would translate the constraints with a for loop. This will allow us to reuse the smt_cache across constraints...
| cons_trans = map(con -> ast2smt(con, variables, additional, Dict()), constraints) | ||
| expr = Sat.and(cons_trans...) | ||
|
|
||
| !isempty(additional) && (expr = expr ∧ Sat.and(additional...)) |
There was a problem hiding this comment.
Here and also in lin_feasible: Please use an if statement
| expr = Satisfiability.__wrap_const(expr) | ||
| end | ||
| # needs qf_nra since ast2smt(TermNumber) uses fractions with variables in the denominator | ||
| res = sat!(expr, solver=Z3(), logic="QF_NRA") |
There was a problem hiding this comment.
QF_LRA should be sufficient here?
There was a problem hiding this comment.
This is an issue with our current number representation, right?
|
Also, I believe we can remove the "old" SMT folders then? |
|
Caveat: Only reviewed code so far, I still want to test it on my machine |
2 participants
@JanGontscharow we will be merging with
devfirst -- hence a new pull request