126 commits

Author	SHA1	Message	Date
Christoph M. Wintersteiger	2ec51d40ec	Eliminated a number potential memory leaks in fp2bv code. ... Relates to #615	2016-05-25 18:49:22 +01:00
Christoph M. Wintersteiger	617e941015	fp2bv refactoring	2016-05-23 18:10:17 +01:00
Christoph M. Wintersteiger	bf3a5effbc	Fixed and refactored fp.min/fp.max for theory_fpa. ... Fixes #616	2016-05-23 15:38:25 +01:00
Christoph M. Wintersteiger	184aebab59	variable naming	2016-05-23 15:08:27 +01:00
Christoph M. Wintersteiger	d4bc8ebb70	FP to BV translation of UFs refactored.	2016-05-22 18:16:57 +01:00
Christoph M. Wintersteiger	8db17311ae	fpa2bv build fixes	2016-05-22 13:13:32 +01:00
Christoph M. Wintersteiger	fe3f8466b6	Partial support for fpa2bv translation in complex types.	2016-05-21 18:08:48 +01:00
Christoph M. Wintersteiger	1cc8146aba	Bugfixes for FP UFs and arrays.	2016-05-20 19:53:57 +01:00
Christoph M. Wintersteiger	44b0a6ddbc	Tentative fix for #586.	2016-05-14 18:42:10 +01:00
Christoph M. Wintersteiger	bb2c5972c7	Bugfixes for UFs in theory_fpa. ... Fixes #591, but performance issues remain.	2016-05-14 18:21:53 +01:00
Christoph M. Wintersteiger	be424d9cbb	Bugfixes for fp.roundToIntegral and fp.rem. ... Relates to #561	2016-04-24 15:14:16 +01:00
Christoph M. Wintersteiger	6db0a15d29	Fixed potential memory leakage issues in fpa2bv_converfter	2016-04-18 17:17:31 +01:00
Christoph M. Wintersteiger	cdc8e1303a	Bugfix for fp.to_*_unspecified. ... Fixes #507	2016-03-16 16:16:29 +00:00
Christoph M. Wintersteiger	99d7a47f82	Bugfixes for unspecified results from fp.to_* (models are still incomplete). ... Relates to #507	2016-03-15 21:45:54 +00:00
Christoph M. Wintersteiger	3101d281e4	Removed unused variable	2016-03-15 15:12:54 +00:00
Christoph M. Wintersteiger	371573cbff	More implementation of fp.to_ieee_bv for unspecified input/output ... Relates to #507	2016-03-15 15:11:37 +00:00
Christoph M. Wintersteiger	a9df4a208f	More bugfixes for fp.to_ieee_bv for unspecified input/output. ... Relates to #507	2016-03-15 14:58:55 +00:00
Christoph M. Wintersteiger	176782d62b	Bugfix for fp.to_ieee_bv for unspecified input/output.	2016-03-15 14:38:11 +00:00
Christoph M. Wintersteiger	5463167a84	Bugfix for fp.rem (denormal numbers) ... Fixes #508.	2016-03-14 15:52:09 +00:00
Christoph M. Wintersteiger	badf9e6e67	whitespace	2016-03-11 14:05:32 +00:00
Christoph M. Wintersteiger	3e61ee2331	disabled "hardware interpretation" of fp.min/fp.max because the unspecified, standard-compliant behaviour is cheap anyways.	2016-03-11 12:52:00 +00:00
Nikolaj Bjorner	640308b546	make proto-model evaluation use model_evaluator instead of legacy evaluator ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2016-03-05 10:27:19 -08:00
Nikolaj Bjorner	70f13ced33	make proto-model evaluation use model_evaluator instead of legacy evaluator ... Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>	2016-03-05 10:14:15 -08:00
Christoph M. Wintersteiger	f34e15f289	whitespace	2016-03-05 16:47:39 +00:00
Christoph M. Wintersteiger	9dfc2bc61e	Fixed memory leaks in fpa2bv converter. ... Fixes #480	2016-03-05 16:47:08 +00:00
Christoph M. Wintersteiger	92b6a3e134	Fixed exponent cap for fp.add in fpa2bv_converter (was unsound for combinations of many sbits but few ebits). ... Fixes #439.	2016-02-07 17:33:33 +00:00
Christoph M. Wintersteiger	4dba5270ad	Efficiency fix for fp.div.	2016-01-18 18:09:29 +00:00
Christoph M. Wintersteiger	de3cb7e5dc	More FPA exponent/siginficand order consistency	2016-01-05 18:05:21 +00:00
Christoph M. Wintersteiger	677ff221f8	Internal consistency: FP exponents are always passed before significands.	2016-01-04 18:57:15 +00:00
Christoph M. Wintersteiger	8eea6fd775	Bugfix for FPA float to float conversion. ... Fixes #337	2015-11-24 17:21:40 +00:00
Christoph M. Wintersteiger	59c1944f92	Bugfix for FP casts (float to float conversion). ... Fixes #331.	2015-11-22 14:49:04 +00:00
Christoph M. Wintersteiger	4cb96bfe76	Fixed assertion failure in fpa2bv_converter. ... Partially addresses #307	2015-11-13 15:55:01 +00:00
Christoph M. Wintersteiger	92152b16ca	Bugfixes for model verification of unspecified values of fp.min/fp.max	2015-11-02 19:25:44 +00:00
Christoph M. Wintersteiger	89fb5a44fb	Made fresh variable generation in fpa2bv lazy so that it doesn't create unnecessary variables.	2015-10-26 18:10:15 +00:00
Christoph M. Wintersteiger	5b39d8fa0d	bugfix for fpa2bv converter	2015-10-26 15:59:00 +00:00
Christoph M. Wintersteiger	ed94bc2f6b	Bugfix for fpa2bv converter.	2015-10-25 13:10:40 +00:00
Christoph M. Wintersteiger	9b5abcd55a	Improved support for FPA unspecified min/max values, model validation, and proof generation.	2015-10-25 13:10:40 +00:00
Christoph M. Wintersteiger	ca496f20cb	Partial refactoring of fpa2bv conversion to support proofs.	2015-10-25 13:10:40 +00:00
Christoph M. Wintersteiger	099775947e	Partial fix for fp,min/fp.max models	2015-10-25 13:10:40 +00:00
Christoph M. Wintersteiger	a951ff0769	Fix for FP UFs and conversion functions.	2015-10-08 16:04:17 +01:00
Christoph M. Wintersteiger	883514c195	Bugfix for FPA UFs	2015-10-08 14:14:39 +01:00
Christoph M. Wintersteiger	c787ea1a3b	Bugfix for FP UFs.	2015-10-08 12:45:26 +01:00
Christoph M. Wintersteiger	a2503af585	Bugfixes for UFs and conversion functions in theory_fpa	2015-10-08 11:54:35 +01:00
Christoph M. Wintersteiger	de39173f6f	Corrected unspecified behavior of fp.min/fp.max corner cases in fpa2bv_converter and in theory_fpa. ... Fixes #68	2015-10-07 20:44:08 +01:00
Christoph M. Wintersteiger	8a026c355f	Corrected unspecified behavior of corner cases in fp.min/fp.max. ... Partially addresses #68.	2015-10-07 20:39:36 +01:00
Christoph M. Wintersteiger	076e680433	Improved UF suppport in fpa2bv_converter.	2015-09-25 17:28:31 +01:00
Christoph M. Wintersteiger	2744d80642	Fixed reference counting in fpa2bv converter.	2015-09-23 14:22:02 +01:00
Christoph M. Wintersteiger	4d39108808	Bugfix for fp.to_sbv ... Fixes #162	2015-09-17 12:21:59 +01:00
Christoph M. Wintersteiger	52df2224e9	Disabled FP debug variables.	2015-09-16 18:04:26 +01:00
Christoph M. Wintersteiger	27f8ad288c	Bugfix for fp.to_ubv. ... Fixes #162.,	2015-09-16 14:26:53 +01:00