10 Commits (867131e964d5e6d98d05278ffd52bf762f8f57fe)

Author	SHA1	Message	Date
Josh Berdine	0568f2ee2d	[sledge] Refactor: Distinguish Fol term and formula types ... Reviewed By: ngorogiannis Differential Revision: D22170516 fbshipit-source-id: e593123ce	4 years ago
Josh Berdine	0aed6eeab6	[sledge] Refactor: Rename to use "first-order logical context" terminology ... Summary: instead of "congruence relation". Reviewed By: ngorogiannis Differential Revision: D22170512 fbshipit-source-id: 2382248da	4 years ago
Josh Berdine	a629486c9f	[sledge] Refactor: Rename Fol.Equality to Fol.Context ... Reviewed By: ngorogiannis Differential Revision: D22170521 fbshipit-source-id: e791739b7	4 years ago
Josh Berdine	dd2e7b4782	[sledge] Refactor: Add Fol module to be used for external interface of solver ... Reviewed By: ngorogiannis Differential Revision: D22170509 fbshipit-source-id: f4ed2bfee	4 years ago
Josh Berdine	eca73cf39b	[sledge] Build: Move sledge equality solver to separate lib ... Reviewed By: ngorogiannis Differential Revision: D22170508 fbshipit-source-id: 1e9cf4a79	4 years ago
Josh Berdine	89f60156a9	[sledge] Change: Use conjunction instead of list of terms for Sh.pure ... Summary: The list interpreted as a conjunction of individual terms in `Sh.pure` is now redundant with `Term.And`. This patch removes the redundant list. Reviewed By: jvillard Differential Revision: D22035852 fbshipit-source-id: 49c01a078	5 years ago
Josh Berdine	fe42fc912d	[sledge] Change: Minor improvement of Sh.extend_us and Sh.freshen ... Summary: Minor code simplification and optimization of `extend_us` in no-op case. Reviewed By: jvillard Differential Revision: D21974021 fbshipit-source-id: a8b12b564	5 years ago
Josh Berdine	1214ab71b7	[sledge] Refactor: Rename to use terminology for "sized sequences" ... Summary: Logically there is nothing specific to memory contents (as byte-arrays) or aggregate (struct/array) values, the theory is for sequences of non-fixed sized elements. Reviewed By: jvillard Differential Revision: D21721019 fbshipit-source-id: b2b730a50	5 years ago
Josh Berdine	dd3645820f	[sledge] Remove Sh.var_strength, no longer used by Solver ... Summary: Now only used internally for printing. Reviewed By: jvillard Differential Revision: D21441534 fbshipit-source-id: 1e6e484c8	5 years ago
Josh Berdine	de20da4fb6	[sledge] Rename lib to src ... Reviewed By: jvillard Differential Revision: D21107643 fbshipit-source-id: 862a2d8c1	5 years ago