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 169ee34371 [sledge] Drop fresh variables that do not appear in the solution ... Summary: In the process of computing `Context.solve`, fresh variables can be generated. Not all of these end up in the final solution substitution. Currently all of the freshly generated variables are returned to the client, which leads to extraneous existentials. This diff trims the returned fresh variables to only those that appear in the final solution. Reviewed By: ngorogiannis Differential Revision: D24746241 fbshipit-source-id: 59a2f221b		4 years ago
..
arithmetic.ml	[sledge] Reorganize first-order logic support into separate library	4 years ago
arithmetic.mli	[sledge] Reorganize first-order logic support into separate library	4 years ago
arithmetic_intf.ml	[sledge] Reorganize first-order logic support into separate library	4 years ago
context.ml	[sledge] Drop fresh variables that do not appear in the solution	4 years ago
context.mli	[sledge] Change Context API to use Term instead of Trm	4 years ago
exp.ml	[sledge] Make API of Term constant destructors uniform	4 years ago
exp.mli	[sledge] Make API of Term constant destructors uniform	4 years ago
fml.ml	[sledge] Reorganize first-order logic support into separate library	4 years ago
fml.mli	[sledge] Reorganize first-order logic support into separate library	4 years ago
fol.ml	[sledge] Change Context API to use Term instead of Trm	4 years ago
fol.mli	[sledge] Change Context API to use Term instead of Trm	4 years ago
funsym.ml	[sledge] Reorganize first-order logic support into separate library	4 years ago
funsym.mli	[sledge] Reorganize first-order logic support into separate library	4 years ago
predsym.ml	[sledge] Reorganize first-order logic support into separate library	4 years ago
predsym.mli	[sledge] Reorganize first-order logic support into separate library	4 years ago
propositional.ml	[sledge] Strengthen normalization by flattening nested And and Or formulas	4 years ago
propositional.mli	[sledge] Reorganize first-order logic support into separate library	4 years ago
propositional_intf.ml	[sledge] Reorganize first-order logic support into separate library	4 years ago
trm.ml	[sledge] Minor exception optimizations	4 years ago
trm.mli	[sledge] Make API of Term constant destructors uniform	4 years ago
var.ml	[sledge] Reorganize first-order logic support into separate library	4 years ago
var.mli	[sledge] Reorganize first-order logic support into separate library	4 years ago
var0.ml	[sledge] Reorganize first-order logic support into separate library	4 years ago
var0.mli	[sledge] Reorganize first-order logic support into separate library	4 years ago
var_intf.ml	[sledge] Reorganize first-order logic support into separate library	4 years ago