Leonardo de Moura 7e66a65e98 Add blast_distinct_threshold option to rewriter. Enable blast_distinct in the QF_LIA default strategy ... Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>		2012-12-17 10:32:00 -08:00
..
api	fix get_implied equalities and the unit test	2012-12-11 21:39:31 -08:00
ast	Add blast_distinct_threshold option to rewriter. Enable blast_distinct in the QF_LIA default strategy	2012-12-17 10:32:00 -08:00
cmd_context	solver factories, cleanup solver API, simplified strategic solver, added combined solver	2012-12-11 17:47:27 -08:00
math	exposed subresultants aka psc-chain procedure	2012-12-09 16:47:37 -08:00
model	Added is_unique_value. Its semantics is equal to the old is_value method. The contract for is_value changed. See comments at ast.h for more information.	2012-12-07 12:53:51 -08:00
muz_qe	fixed unused variable warning	2012-12-13 14:09:52 -08:00
nlsat	Fixed bug reported by Yan Peng from UBC	2012-12-12 13:04:54 -08:00
parsers	solver factories, cleanup solver API, simplified strategic solver, added combined solver	2012-12-11 17:47:27 -08:00
sat	exposed sat params	2012-12-02 16:38:33 -08:00
shell	solver factories, cleanup solver API, simplified strategic solver, added combined solver	2012-12-11 17:47:27 -08:00
smt	Removed auxiliary constants created by the nnf tactic from Z3 models. Fixed model.compact parameter propagation problem.	2012-12-13 14:03:58 -08:00
solver	Fix memout detected in nightly regressions	2012-12-15 13:26:11 -08:00
tactic	Add blast_distinct_threshold option to rewriter. Enable blast_distinct in the QF_LIA default strategy	2012-12-17 10:32:00 -08:00
test	fix get_implied equalities and the unit test	2012-12-11 21:39:31 -08:00
util	improved unknown parameter error msg	2012-12-10 18:46:02 -08:00