infer_clone

History

Josh Berdine 9d12f6502f [sledge] Make aggregate sizes explicit when constructing equalities Summary: In an equation such as `x = ⟨n,a⟩`, `x` is implicitly an aggregate of size `n` (or else the equation is ill-typed). Make this explicit by normalizing such equations to e.g. `⟨\|⟨n,a⟩\|,x⟩ = ⟨n,a⟩`. Reviewed By: ngorogiannis Differential Revision: D19358546 fbshipit-source-id: 77f67a0da		5 years ago
..
dune.in	[copyright] Remove years	6 years ago
exp.ml	[sledge] Remove size of Splat exps and terms	5 years ago
exp.mli	[sledge] Remove size of Splat exps and terms	5 years ago
exp_test.ml	[sledge] Simplify type conversions	5 years ago
exp_test.mli	[sledge] Simplify type conversions	5 years ago
frontend.ml	[sledge] Remove size of Splat exps and terms	5 years ago
frontend.mli	[sledge] Add a flag to disable internalization	5 years ago
global.ml	[sledge] Do not store size of globals separately	5 years ago
global.mli	[sledge] Do not store size of globals separately	5 years ago
llair.ml	[sledge] Printing and tracing improvements	5 years ago
llair.mli	[sledge][NFC] Rename Term.call's func arg to callee to match type	5 years ago
loc.ml	[sledge] Printing and tracing improvements	5 years ago
loc.mli	[copyright] Remove years	6 years ago
reg.ml	[sledge] Distinguish program expressions and formula terms	5 years ago
reg.mli	[sledge] Distinguish program expressions and formula terms	5 years ago
term.ml	[sledge] Make aggregate sizes explicit when constructing equalities	5 years ago
term.mli	[sledge] Add Shostak solver for aggregate theory	5 years ago
term_test.ml	[sledge] Sort arguments of Eq terms	5 years ago
term_test.mli	[sledge] Precompute the Term form of each Exp, and add it to Exp.t	5 years ago
typ.ml	[sledge] Keep size in both bits and bytes for each type	5 years ago
typ.mli	[ocamlformat] Upgrade ocamlformat version	5 years ago
var.ml	[sledge] Precompute the Term form of each Exp, and add it to Exp.t	5 years ago
var.mli	[sledge] Precompute the Term form of each Exp, and add it to Exp.t	5 years ago