Add some ops missing from aslp generator - #237
Conversation
katrinafyi
left a comment
katrinafyi
left a comment
There was a problem hiding this comment.
LGTM modulo comments. Thanks :)
| let f_gen_replicate_bits : bigint -> bigint -> expr -> expr -> expr = | ||
| fun _ -> failwith "f_gen_replicate_bits" | ||
| fun targ0 targ1 opr nr -> | ||
| try_const_unsigned_value nr |> Z.to_int |> fun repeats -> |
There was a problem hiding this comment.
should be no need for try_const_unsigned_value; it should be in targ1 which should be a bigint equal to nr's value.
There was a problem hiding this comment.
Are you sure its not just the bitwidth of the result?
There was a problem hiding this comment.
Reasonably. Did you find it to not be the case?
There was a problem hiding this comment.
No but I can't tell from this example
There was a problem hiding this comment.
| |> function | ||
| | [] -> Expr.BasilExpr.boolconst true | ||
| | args -> Expr.BasilExpr.applyintrin ~op:`OR args |
There was a problem hiding this comment.
Did this cause a problem somewhere downstream? Generally, it would be nice to handle 0-ary associative operations sensibly.
There was a problem hiding this comment.
Generally I just give them semantics, SMTLib and boogie don't like it tho so the expr simplifier converts them to unit. Replacing them in the constructor would be unexpected I think.
There was a problem hiding this comment.
If it is to be replaced in this one place, you could imagine that it would also need similar replacements in other random places. Regardless of how it's done, it would be nice to centralise this somewhere to avoid needing ad-hoc patches. But not necessarily in this PR, sure.
There was a problem hiding this comment.
It is centralised in Expr_simp :)
2 participants
cvt_bool_bvreplicate_bits\NEQ` in Ops.ml