You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

Josh Berdine b16e85d10d [sledge] Eliminate redundant existential quantifiers ... Summary: This diff changes `Sh.simplify` from a logically-weakening syntactic simplification to an equivalence-preserving rewrite. The implementation is based on `Equality.solve_for_vars` which is also used by `Solver` to witness existential variables. Reviewed By: jvillard Differential Revision: D20120274 fbshipit-source-id: 5e11659ea		5 years ago
..
dune.in	[copyright] Remove years	6 years ago
import.ml	[sledge] Eliminate redundant existential quantifiers	5 years ago
import.mli	[sledge] Eliminate redundant existential quantifiers	5 years ago
qset.ml	[sledge] Replace solution substitution trimming with partitioning	5 years ago
qset.mli	[sledge] Replace solution substitution trimming with partitioning	5 years ago
vector.ml	[sledge] Add Shostak canonizer for aggregate theory	5 years ago
vector.mli	[sledge] Add Shostak canonizer for aggregate theory	5 years ago