infer_clone/sledge/nonstdlib/multiset.mli

(*
 * Copyright (c) Facebook, Inc. and its affiliates.
 *
 * This source code is licensed under the MIT license found in the
 * LICENSE file in the root directory of this source tree.
 *)

(** Multiset - Set with (signed) rational multiplicity for each element *)

include module type of Multiset_intf

module Make (Elt : sig
  type t [@@deriving compare, sexp_of]
end) : S with type elt = Elt.t
[sledge] Reimplement arithmetic and congruence closure Summary: - Add nary expressions implemented using a form of multisets which support any integer multiplicity - Reimplement polynomials using new nary expressions - Move the decomposition of exps into "base plus offset" form into Exp, to enforce simplification invariants - Revise expression simplification to cooperate with congruence closure (mainly: simplification should not invent new subexpressions) - Reimplement congruence closure plus integer offsets to + cope with new representation of polynomials using nary expression forms + be diligent about maintaining which expressions are in the relation + add lots of invariant checking for the correlations between the componnents of the congruence closure data structures Reviewed By: jvillard Differential Revision: D14075512 fbshipit-source-id: 2dbaf3d11 6 years ago			`(*`
[copyright] Remove years Reviewed By: jvillard Differential Revision: D15771884 fbshipit-source-id: e2997e3a3 6 years ago			`* Copyright (c) Facebook, Inc. and its affiliates.`
[sledge] Reimplement arithmetic and congruence closure Summary: - Add nary expressions implemented using a form of multisets which support any integer multiplicity - Reimplement polynomials using new nary expressions - Move the decomposition of exps into "base plus offset" form into Exp, to enforce simplification invariants - Revise expression simplification to cooperate with congruence closure (mainly: simplification should not invent new subexpressions) - Reimplement congruence closure plus integer offsets to + cope with new representation of polynomials using nary expression forms + be diligent about maintaining which expressions are in the relation + add lots of invariant checking for the correlations between the componnents of the congruence closure data structures Reviewed By: jvillard Differential Revision: D14075512 fbshipit-source-id: 2dbaf3d11 6 years ago			`*`
			`* This source code is licensed under the MIT license found in the`
			`* LICENSE file in the root directory of this source tree.`
			`*)`

[sledge] Rename Qset to Multiset Summary: In preparation for generalizing the type of multiplicities. Reviewed By: jvillard Differential Revision: D24306052 fbshipit-source-id: ddb71499e 4 years ago			`(** Multiset - Set with (signed) rational multiplicity for each element *)`
[sledge] Reimplement arithmetic and congruence closure Summary: - Add nary expressions implemented using a form of multisets which support any integer multiplicity - Reimplement polynomials using new nary expressions - Move the decomposition of exps into "base plus offset" form into Exp, to enforce simplification invariants - Revise expression simplification to cooperate with congruence closure (mainly: simplification should not invent new subexpressions) - Reimplement congruence closure plus integer offsets to + cope with new representation of polynomials using nary expression forms + be diligent about maintaining which expressions are in the relation + add lots of invariant checking for the correlations between the componnents of the congruence closure data structures Reviewed By: jvillard Differential Revision: D14075512 fbshipit-source-id: 2dbaf3d11 6 years ago
[sledge] Rename Qset to Multiset Summary: In preparation for generalizing the type of multiplicities. Reviewed By: jvillard Differential Revision: D24306052 fbshipit-source-id: ddb71499e 4 years ago			`include module type of Multiset_intf`
[sledge] Implement Qset using Import.Map Reviewed By: ngorogiannis Differential Revision: D20583759 fbshipit-source-id: d39b13508 5 years ago
			`module Make (Elt : sig`
			`type t [@@deriving compare, sexp_of]`
			`end) : S with type elt = Elt.t`