3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Commit graph

967 commits

Author SHA1 Message Date
Nikolaj Bjorner 3d01246f71 Skip propagation on bits that have not (yet) been fixed by the SAT core: congruence closure for bits has not necessarily propagated to all bit positions when a bit in a congruence class gets fixed.
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-08 08:17:18 -08:00
Nikolaj Bjorner 0e6aaf0211 Issue #407 build break
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-07 20:05:49 -08:00
Nikolaj Bjorner ad778f87c7 change data-structures to concanetation decomposition normal form
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-07 16:03:37 -08:00
Nikolaj Bjorner 0c2334417c fix build warnigs with && vs ||, tuning seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-07 06:53:00 -08:00
Nikolaj Bjorner 643999860d fix memory leak in SAT solver exposed by regression tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-06 17:32:54 -08:00
Nikolaj Bjorner 00f3a1fe81 fix memory leak in SAT solver exposed by regression tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-06 11:47:45 -08:00
Nikolaj Bjorner aec5a38b14 fix memory leak in SAT solver exposed by regression tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-06 11:44:55 -08:00
Christoph M. Wintersteiger d176c8714a Merge branch 'master' of https://github.com/Z3Prover/z3 into jan4 2016-01-05 16:38:12 +00:00
Nikolaj Bjorner af758dea4a tuning for seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-05 08:23:44 -08:00
Christoph M. Wintersteiger 8b47a84598 Merge branch 'master' of https://github.com/Z3Prover/z3 into jan4 2016-01-05 11:34:35 +00:00
Nikolaj Bjorner 2c1d2aad44 seq, API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-04 22:06:32 -08:00
Nikolaj Bjorner c1ebf6b4fc seq + API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-04 18:01:48 -08:00
Christoph M. Wintersteiger 677ff221f8 Internal consistency: FP exponents are always passed before significands. 2016-01-04 18:57:15 +00:00
Nikolaj Bjorner 68a532d066 seq, API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-03 20:53:06 -08:00
Nikolaj Bjorner a3c4972c85 seq API, tuning
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-03 17:16:13 -08:00
Nikolaj Bjorner e10ecad5dc seq API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-02 22:52:28 -08:00
Nikolaj Bjorner 5e553a4dc1 seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-02 13:32:44 -08:00
Nikolaj Bjorner 876fd1f7ba seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-01-01 09:00:21 -08:00
Nikolaj Bjorner 6c6d1d92c4 seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-31 16:10:41 -08:00
Nikolaj Bjorner 78550ec816 seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-31 07:48:14 -08:00
Nikolaj Bjorner 746d26e744 seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-29 21:14:52 -08:00
Nikolaj Bjorner bd9b5b5735 seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-29 10:13:19 -08:00
Nikolaj Bjorner e2fab0a555 seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-28 18:15:48 -08:00
Nikolaj Bjorner 739043e273 seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-28 10:28:43 -08:00
Nikolaj Bjorner 071a654a9a seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-27 04:41:25 -08:00
Nikolaj Bjorner 31302ec851 automata
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-25 15:22:26 -08:00
Nikolaj Bjorner 4a5b645d88 automata
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-25 05:37:24 -08:00
Nikolaj Bjorner 659a7ede84 automata
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-25 04:25:23 -08:00
Nikolaj Bjorner 65d147106e automata
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-24 12:01:59 -08:00
Nikolaj Bjorner 1bbf7813b0 automata
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-24 03:30:02 -08:00
Nikolaj Bjorner f414869456 add symbolic automaton
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-23 19:46:10 -08:00
Nikolaj Bjorner 386399472d seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-23 11:02:34 -08:00
Nikolaj Bjorner 9c6271dded add debugging facilities for github issues #384 #367
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-22 10:43:18 -08:00
Nikolaj Bjorner 65da0f9f3a updated seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-21 06:07:50 -08:00
Nikolaj Bjorner 8e26c97782 tuning bit-vector operations
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-21 13:09:03 +02:00
Nikolaj Bjorner 284fcc2c04 seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-20 09:43:56 +02:00
Nuno Lopes dbc1a84d6a fix warning with MSVC++ 64 2015-12-15 18:36:01 +00:00
Nikolaj Bjorner b1459f4fa3 fix build warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-15 04:57:32 +02:00
Nikolaj Bjorner 43bc6caa55 fix warning messages
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-15 04:11:11 +02:00
Nikolaj Bjorner f3d94db889 bild on gcc #376
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-13 23:47:45 -08:00
Nikolaj Bjorner 72883df134 fix build, add seq features
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-13 16:02:17 -08:00
Nikolaj Bjorner 3c50508762 use ADT for strings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-12 20:46:28 -08:00
Nikolaj Bjorner a7e2fb31e3 updates to resource exceptions, update master possibly handle pull request issue
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-12 11:36:49 -08:00
Nikolaj Bjorner 2a051719d8 cleanup deprecated critical sections, fix cancellation for par_or_else tactic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-12 09:43:00 -08:00
Nikolaj Bjorner 9c597e9eea Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-11 17:47:03 -08:00
Nikolaj Bjorner baee4225a7 reworking cancellation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-11 16:21:24 -08:00
Nikolaj Bjorner 61dbb6168e cleanup cancelation logic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-11 12:35:35 -08:00
Nuno Lopes 39ca5480d7 ensure that formula is skolemized in the smt solver when using MBQI
Reviewed by Nikolaj

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
2015-12-11 18:18:09 +00:00
Nuno Lopes ef06da8c2c fix build with gcc 2015-12-11 18:14:14 +00:00
Nikolaj Bjorner 4e155887b2 consolidate cancellation to context check_cancel_flag instead of calling in set_cancel()
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-11 09:51:43 -08:00
Nikolaj Bjorner ee4ed1749a add cancel checks in model finder, patch by Sarah Winkler
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-11 09:09:25 -08:00
Nikolaj Bjorner 85b9bb3cc6 seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-11 08:37:47 -08:00
Nikolaj Bjorner 58411f64e8 seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-10 20:25:12 -08:00
Nikolaj Bjorner 5eb23e1e7a seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-10 19:20:16 -08:00
Nikolaj Bjorner 30580a012a seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-10 02:38:56 -08:00
Nikolaj Bjorner d81186eaca seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-10 01:36:17 -08:00
Nikolaj Bjorner f9ca66d90b seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-09 23:19:16 -08:00
Nikolaj Bjorner d58c219b54 seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-09 22:18:02 -08:00
Nikolaj Bjorner c5a9d81d93 seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-09 20:17:00 -08:00
Nikolaj Bjorner fe1039d12f seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-09 14:48:50 -08:00
Nikolaj Bjorner 0e701138e1 disable restart code in seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-09 09:53:18 -08:00
Nikolaj Bjorner b9302e6caf seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-09 00:38:03 -08:00
Nikolaj Bjorner 94bd2fdbe4 seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-08 21:03:28 -08:00
Nikolaj Bjorner 24de0a9b90 seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-08 16:37:08 -08:00
Nikolaj Bjorner 6c2e7e7675 seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-08 16:03:24 -08:00
Nikolaj Bjorner 932a3a8387 seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-08 13:27:17 -08:00
Nikolaj Bjorner 895d032996 seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-08 10:33:09 -08:00
Nikolaj Bjorner 5aabc64312 seq
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-08 08:11:00 -08:00
Nikolaj Bjorner ca96fea2c0 add seq methods
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-07 16:28:20 -08:00
Nikolaj Bjorner 34a0d7dfed remove python_install target from all
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-07 09:59:46 -08:00
Nikolaj Bjorner 8bb73c8eae merge seq and string operators
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-06 23:34:28 -08:00
Nikolaj Bjorner 08bfd08412 merging seq and string
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-06 22:15:56 -08:00
Nikolaj Bjorner a8e366aa24 add basic string factory
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-04 15:24:29 -08:00
Nuno Lopes 5d289a8da5 fix leak in asserted_formulas::propagate_values() for proof generation mode
continuation of issue #342

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
2015-11-29 10:49:52 +00:00
Nuno Lopes d175c99542 fix ast leak in asserted_formulas::propagate_values()
Fixes issue #342

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
2015-11-27 20:09:17 +00:00
Nikolaj Bjorner 665af3d8b9 remove deprecated user-theory plugins and other unused functionality from API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-20 08:43:27 -08:00
Nikolaj Bjorner fd8fd40669 fix tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-20 08:00:01 -08:00
Nikolaj Bjorner 04b0e3c2f7 add checks for cancellation inside mam to agilely not ignore Rustan's soft requests for a timeout #326
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-17 18:48:52 -08:00
Nikolaj Bjorner 66fc873613 Fix for #322: PDR engine cannot falls back on fixed size arithmetic for difference logic. It would eventually overflow and cause incorrect model construction. Enable only fixed-size arithmetic when configuration allows it
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-17 09:00:16 -08:00
Nikolaj Bjorner 315dc80eb0 toggle default for bv2int decision procedure support to avoid confusing users. Issue #301
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-10 15:09:52 -05:00
Christoph M. Wintersteiger 5995c753d3 Bugfix for theory_fpa construction and destruction. 2015-11-09 13:54:28 +00:00
Christoph M. Wintersteiger 4e05e93ecb Bugfix for FPA model generation/conversion.
Addresses #300
2015-11-09 11:52:44 +00:00
Nikolaj Bjorner 4685a5f8ba add array-ext to externally exposed functions to enable interpolants with arrays to be usable in feedback loops with Z3. Addresses one issue raised in #292
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-07 16:42:13 -08:00
Nikolaj Bjorner 8d1fa3ae50 move mk_fresh to inside files that include smt_context.h directly to address build problem reported in #297
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-07 11:50:06 -08:00
Nikolaj Bjorner c1adffb6ab Merge branch 'master' of https://github.com/Z3Prover/z3 into nsb/master 2015-11-07 10:00:43 -08:00
Nikolaj Bjorner 1758799ef4 add translate facility to inc_sat_solver. Limit lemma copying to unit lemmas
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-07 10:00:14 -08:00
Nikolaj Bjorner 396875bedf fix compilation problem, issue #297
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-06 22:56:53 -08:00
Nikolaj Bjorner 3d993a4ee1 Merge branch 'master' of https://github.com/Z3Prover/z3 into nsb/master 2015-11-06 17:29:53 -08:00
Nikolaj Bjorner b4cb51cdb3 working on Forking/Serializing a z3 Solver #209
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-06 17:29:24 -08:00
Nikolaj Bjorner 5ea2c22153 fix build break - by renaming tout to out
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-06 10:21:02 -08:00
Nikolaj Bjorner aeedb931f3 fix build break
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-06 10:20:21 -08:00
Christoph M. Wintersteiger a6b3fba038 Build fix, hide debug code in release mode. 2015-11-06 18:06:23 +00:00
Nikolaj Bjorner 7b72486644 Merge branch 'master' of https://github.com/Z3Prover/z3 into nsb/master 2015-11-05 17:32:35 -08:00
Nikolaj Bjorner fc592fc856 fix for #291. The root issue is that the set of antecedents is recycled as a fixed object between routines. Antecedents that were already allocated for a Gomory cut got reset by the internalizer. This causes unsound bounds axioms to be created
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-05 15:08:42 -08:00
Nikolaj Bjorner 2efd5bf9d1 Fix bug exposed in #281
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-02 14:18:49 -08:00
Nikolaj Bjorner f78c769b3b Merge branch 'master' of https://github.com/Z3Prover/z3 2015-11-02 13:49:48 -08:00
Christoph M. Wintersteiger 14d2356a32 Code simplification 2015-11-02 19:25:11 +00:00
Christoph M. Wintersteiger ba70ab9ad2 Bugfix for theory_fpa 2015-11-02 19:08:52 +00:00
Nikolaj Bjorner feba64b739 Enable model construction and evaluation for theory functions that may be uninterpreted. To fix issue #237
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-11-02 10:18:25 -08:00
Nikolaj Bjorner 7169fc469e Merge branch 'master' of https://github.com/NikolajBjorner/z3 2015-11-02 08:19:35 -08:00
Nikolaj Bjorner 32f3bd17fb adding translation routine to context to address enhancement request #209
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-10-31 14:30:54 -07:00
Nikolaj Bjorner 9acaa49a05 adding translation routine to context to address enhancement request #209
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-10-31 14:28:21 -07:00
Nikolaj Bjorner 4b1a730f46 API method for translating context
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-10-31 12:47:16 -07:00
Nikolaj Bjorner fb624780d5 add checks in internalizer for issues of the form #227
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-10-31 12:41:57 -07:00
Christoph M. Wintersteiger 88064fc172 minor theory_fpa refactoring 2015-10-31 19:16:09 +00:00
Christoph M. Wintersteiger 1d7aa9ba2f Fixed rewriter bug in theory_fpa. 2015-10-31 18:53:40 +00:00
Christoph M. Wintersteiger 8491b3bebe Revert "Fixed use of mk_th_axiom in theory_fpa."
This reverts commit 89e99c7b4b.
2015-10-31 18:51:32 +00:00
Nikolaj Bjorner 4fd1f4a65c add handler for abuse of OP_IMPLIES
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-10-31 11:34:55 -07:00
Christoph M. Wintersteiger 89e99c7b4b Fixed use of mk_th_axiom in theory_fpa.
Relates to #227
2015-10-31 13:57:17 +00:00
Nikolaj Bjorner ac3edbbaaa add line/position information to unsupported command reports per zeph pull request
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-10-30 19:23:31 -07:00
Nikolaj Bjorner b19fbe4429 make sure to bring constraints into clausal form before using the th_axiom assertion. Old version should not have been used as a template for copying, as in issue #227
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-10-30 15:55:18 -07:00
Christoph M. Wintersteiger 8fffa9f188 Removed trailing whitespace. 2015-10-30 12:20:41 +00:00
Nikolaj Bjorner 6b82b949cf Make Groebner basis computation interruptable. Exponsed in issue #269
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-10-28 11:39:59 -07:00
Nikolaj Bjorner 2a95a77706 fix issues #240, #250
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-10-28 09:47:17 -07:00
Nikolaj Bjorner b197e590a4 fix coercion regression. Issue #263
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-10-27 19:25:38 -07:00
Nikolaj Bjorner 47cb1058b2 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-10-27 18:11:35 -07:00
Nikolaj Bjorner 357a92dfef n/a
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-10-27 18:11:31 -07: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 e3ed0159a8 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-10-25 13:09:59 +00:00
Christoph M. Wintersteiger 21ad1fb623 Bugfix for proof production in asserted_formulas::propagate_values()
Fixes #259
2015-10-25 13:09:18 +00:00
Nikolaj Bjorner 05c6ed1698 fixing issue #254
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-10-22 09:54:05 -07:00
Nikolaj Bjorner ac902dad1a fix another regression and missing detection of bounds, Issue #254
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-10-22 08:53:12 -07:00
Nikolaj Bjorner ffa78b95ab fix unbounded, issue #252
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-10-21 14:38:47 -07:00
Christoph M. Wintersteiger 6749c19ab1 Merge branch 'static_analysis' of https://github.com/daniel-j-h/z3
# Conflicts:
#	src/ast/ast.h
#	src/interp/iz3foci.cpp
#	src/muz/duality/duality_dl_interface.cpp
#	src/util/hwf.h
2015-10-19 15:14:45 +01:00
Nikolaj Bjorner f4954e9d7f fix for fixed size rational difference logic
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-10-13 09:24:02 -07:00
Nuno Lopes 0e387b2abe use Z3_fallthrough instead of __falthrough directly to avoid messing with reserved identifiers
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
2015-10-09 18:06:49 +01:00
Christoph M. Wintersteiger a951ff0769 Fix for FP UFs and conversion functions. 2015-10-08 16:04:17 +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
Nikolaj Bjorner 6e852762ba patch for issue #232
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-10-06 19:07:47 -07:00
Nikolaj Bjorner 5d71190468 add catch for cancellation intermixed with return value l_true. To address regressions in QF_LIA tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-09-29 16:50:59 -07:00
Nikolaj Bjorner 77c423b9aa annotate enode hash as signed character to address issue #210
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-09-29 14:14:29 -07:00
Nikolaj Bjorner 9b3e242990 adding rlimit resource limit facility to provide platform and architecture independent method for canceling activities
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-09-28 13:37:59 -07:00
Christoph M. Wintersteiger ac7e8b352f Improved support for UFs in FPA theory 2015-09-28 18:20:45 +01:00
Christoph M. Wintersteiger 076e680433 Improved UF suppport in fpa2bv_converter. 2015-09-25 17:28:31 +01:00
Christoph M. Wintersteiger 05d9e188f8 Reactivated smt.max_conflicts option.
Partially fixes #216.
2015-09-17 14:08:04 +01:00
Christoph M. Wintersteiger f3441c6a9b tabs and indentation 2015-09-17 13:25:22 +01:00
Nuno Lopes 45cfb80d14 tentatively fix another issue with char signedness as reported in issue #210
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
2015-09-10 09:01:44 +01:00
Nikolaj Bjorner d7da64f946 fix crash with incorrect bound computation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-09-08 16:27:57 -07:00
Nikolaj Bjorner 73a8f9960f fix regressions exposed in Internal
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-09-07 20:17:46 -07:00
Nikolaj Bjorner 963981b3a6 fix memory alias bug and non-termination bug exposed by issue #184
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-08-31 14:45:10 -07:00
Nikolaj Bjorner 0ed38ed59b add option for using corr set and use partial cores
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-08-30 14:48:24 -07:00
Nikolaj Bjorner 7f219e84de check cancellation flag in min/max. Fixes issue #206
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-08-29 15:51:58 -07:00
Christoph M. Wintersteiger f4c8463619 Bugfix for FP theory
Fixes #207
2015-08-28 15:41:03 +01:00
Christoph M. Wintersteiger 81eecafa66 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-08-27 18:17:38 +01:00
Christoph M. Wintersteiger 081ba9093a Bugfix for FP theory; handling of UFs and interpreted functions from other theories. 2015-08-27 18:17:26 +01:00
Nikolaj Bjorner d00d6a3506 enable Boolean propagation in AUFBV to fix inefficiency (bit-blasting destroys simplifications that are possible by simple Boolean propagation). Fixes issue #194
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-08-25 13:21:33 -07:00
Nikolaj Bjorner 68b441770e Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-08-25 11:09:35 -07:00
Nikolaj Bjorner 7639eff29b retain default configuration between calls to SMT tactic so that values are not overwritten between calls to smt-setup. Fixes bug #196
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-08-25 11:09:10 -07:00
Nikolaj Bjorner ee5f1ad6b6 fix issue #203: domain range was one too large
Signed-off-by: unknown <nbjorner@nikolaj-z.redmond.corp.microsoft.com>
2015-08-24 15:55:40 -07:00
Christoph M. Wintersteiger 8c11299be6 Bugfix for theory_fpa, when datatypes contain floats.
Fixes #201.
2015-08-24 15:09:02 +01:00
Nikolaj Bjorner 655b44c07b make :weight understand both decimal and integral values, remove dweight, remove deprecated commands for optimization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-08-15 00:48:22 +02:00
Nikolaj Bjorner cd838e5cf4 fix bug reported in issue #193: MBQI needs to avoid instantiating data-types that contain model values in nested positions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-08-13 14:29:48 +02:00
Nikolaj Bjorner 702af71a2d Check more frequently for cancelation flags to address grep0095.stp.smt2 in issue #178. Z3 spends time in pre-processing simplification, which indicates there is some opportunity to tune this portion of the code
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-08-11 23:14:34 +02:00
Nikolaj Bjorner 424f34d3d9 enable smt tactic to be used even if cores are enabled, as long as no cores are tracked, fixes issue #189
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-08-11 11:16:41 +02:00
Nikolaj Bjorner e532657d77 .. adding core validation debug option to ease diagnose issue #158
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-08-10 11:01:46 +02:00
Nikolaj Bjorner db24cb8087 add core validation option to directly validate cores using the context
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-08-10 10:56:07 +02:00
Nikolaj Bjorner 6780784bcf filter instantiations for model values to fix issue #183
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-08-06 14:43:08 +02:00
Nikolaj Bjorner f96c0b6963 fixes #186, remove ite-lifting from opt_context to detect weighted maxsat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-08-06 11:52:59 +02:00
Christoph M. Wintersteiger 0cd406ca0b Fixed initialization order and unused variable warnings.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-07-30 09:09:13 +01:00
Christoph M. Wintersteiger 7c282d3719 bugfix for smt::model_finder::set_cancel
follow-up to fixed #178
2015-07-29 17:18:15 +01:00
Christoph M. Wintersteiger b9e273800c Made quantifier-related parts of smt::model_finder and smt::model_checker interruptable.
Fixes #178
2015-07-29 16:55:45 +01:00
Nikolaj Bjorner d7b3aaffbd Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-07-14 13:18:16 -07:00
Nikolaj Bjorner 96c8b1e7ff fixup model construction on undef results for arithmetic. Fixes issue #161
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-07-13 12:44:07 -07:00
Nikolaj Bjorner 6fbc8fa06c break stack abuse in relevancy propagation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-07-12 14:52:43 -07:00
Nikolaj Bjorner 4bc044c982 update header guards to be C++ style. Fixes issue #9
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-07-08 23:18:40 -07:00
Nikolaj Bjorner d815cf9b7b fix bug in optimization where a variable is updated twice
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-07-07 16:01:48 -07:00
Nikolaj Bjorner e81dc5a0a0 fixes issue #143 and memory leak on theory plugin setup
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-06-26 09:03:56 +02:00
Nikolaj Bjorner 108d76270e set undo trail after set-watches to avoid crash during exception handling (the relevancy trail is scoped so ends up traversing the trail if allocating the watch throws an exception). Fixes crash.smt in issue #56
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-06-23 19:18:03 +02:00
Nikolaj Bjorner d9522cfd07 fix mixed integer/real bugs for maximization exposed by non-termination in slow.smt. partially fixes issue #56
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-06-23 12:05:19 +02:00
Nikolaj Bjorner d32e4a9476 exposing facility to extract dependent clauses
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-06-22 23:36:52 +02:00
Nikolaj Bjorner b08ccc7816 added missing Copyright forms
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-06-10 11:54:02 -07:00
Nikolaj Bjorner 9734407cde disable throttle on unbounded objectives in shared theories. It may violate an interface equality, to fix issue #120
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
2015-06-02 11:14:59 -07:00
Nikolaj Bjorner 2d409c6042 revert bug introduced to avoid stack overflow in arrays
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
2015-05-29 14:32:24 -07:00
Nikolaj Bjorner f8e2fa0337 fixes issue #93
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-05-29 11:11:13 -07:00
Nikolaj Bjorner 5acefceada Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-05-29 08:58:31 -07:00
Christoph M. Wintersteiger f2f6fc1994 Added QF_BVFP logic alias for QF_FPBV 2015-05-29 13:58:23 +01:00
Nikolaj Bjorner ed7e0e11a8 n/a
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-05-28 20:55:13 -07:00
Nikolaj Bjorner 534271db08 adding parameters to gomory cut axioms
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
2015-05-27 14:48:51 -07:00
Nikolaj Bjorner e483efd3f4 fixes to Euclidean solver, fixes #100
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
2015-05-27 09:21:20 -07:00
Nikolaj Bjorner cb00555635 local changes
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
2015-05-27 09:18:52 -07:00
Christoph M. Wintersteiger 9912b2cd67 Re-enabled the smt.arith.greatest_error_pivot parameter. 2015-05-23 18:01:00 +01:00
Nuno Lopes c577ab361b fix assorted undefined behaviors caught by clang
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
2015-05-23 11:45:12 +01:00
Ken McMillan 4546c3e7bb merge 2015-05-22 11:01:55 -07:00
Ken McMillan 13a3bdd7a3 fix proof for extended GCD rule 2015-05-22 10:28:19 -07:00
Nikolaj Bjorner c969d78042 throw exception instead of debug mode assertion in ast_manager on malformed input
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
2015-05-21 15:07:01 -07:00
Nikolaj Bjorner 9d0e3abd24 use static features to set hidden configuration parameters on small integers and int vs. real
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
2015-05-20 10:41:41 -07:00
Nikolaj Bjorner 92cfc242d2 cast variables to avoid compiler warning on signed/unsigned comparison
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
2015-05-19 08:15:59 -07:00
Nikolaj Bjorner 203c5015c8 fix debian amd64 warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-05-18 15:17:21 -07:00
Nikolaj Bjorner e8811748d3 fix regressions in nl/smt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-05-16 19:08:37 +01:00
Nikolaj Bjorner 64bd62b17e fix gcc compiler warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-05-16 11:56:04 +01:00
Nikolaj Bjorner 839e3fbb7c add ddnf tests, add facility to solve QF_NRA + QF_UF(and other theories) in joint solver to allow broader use of QF_NRA core
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-05-09 19:40:34 -07:00
Nikolaj Bjorner a0f0b53686 fixes to #52, #53
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-04-28 14:48:59 -07:00
Nikolaj Bjorner ffc3a36dcb checked ite-expressions as shared for bounds detection
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-04-23 19:59:33 +02:00
Nikolaj Bjorner 3ba2e712b2 merge with unstable branch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-04-12 15:54:52 -07:00
Daniel J. Hofmann 88f6e74a27 Wnewline-eof 2015-04-03 19:31:09 +02:00
Daniel J. Hofmann 4e59ba922b Wc++11-extensions 2015-04-03 19:13:52 +02:00
Nikolaj Bjorner 26c53d055a Merge branch 'opt' of https://github.com/Z3Prover/z3 into opt 2015-04-02 15:22:41 -07:00
Nikolaj Bjorner dca0fb77c2 use same defaults as unstable branch for difference logic configuration
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
2015-04-02 15:22:32 -07:00
Nikolaj Bjorner d01c3491a6 simplify with caching, but without expanding number of asserted formulas. Bug reported by Heizmann, codeplex issue 197
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
2015-04-02 10:28:30 -07:00
Nikolaj Bjorner 6b995c4077 disable wrong fix for simplification
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-04-02 02:56:40 -07:00
Nikolaj Bjorner 52619b9dbb pull unstable
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
2015-04-01 14:57:11 -07:00
Nikolaj Bjorner 10cdbb881f enable canceling simplex on interrupt, investigating PDR inconsistency
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-03-25 12:13:57 -07:00
Christoph M. Wintersteiger b76d588c28 Renamed the soft_timeout option to just timeout.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-03-21 16:10:30 +00:00
Nikolaj Bjorner 4145b92136 use of regions for AUX lemmas from pb solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-03-11 11:52:07 -07:00
Nikolaj Bjorner f47cc70236 use of regions for AUX lemmas from pb solver
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-03-11 11:48:52 -07:00
Nikolaj Bjorner 51267f3aba take into account that bound from optimization may create atom that clashes with inequality bound from term
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-03-11 00:26:49 -07:00
nikolajbjorner fe6af38d97 debugging assertion violation
Signed-off-by: nikolajbjorner <nbjorner@microsoft.com>
2015-03-10 20:57:01 -07:00
Christoph M. Wintersteiger 55ca6ce44b Resurrected the dack* options.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-03-04 19:15:22 +00:00
Nuno Lopes 71d31c1267 minor optimization to reset() methods in smt::ketnel and smt::quantifier_manager
Signed-off-by: Nuno Lopes <a-nlopes@MSRC-4051274.europe.corp.microsoft.com>
2015-02-27 11:48:14 +00:00
Christoph M. Wintersteiger a51aed0133 Fixed bug in constant propagation
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-02-24 21:26:25 +00:00
Nuno Lopes 5676fbbc9e compiler love: make a few symbols static and avoid unneeded relocations
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
2015-02-22 11:13:51 +00:00
Nikolaj Bjorner 49483fdc28 take conflicts during restart into account. reported by Arie Gurfinkel
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-02-21 02:08:00 -08:00
Nikolaj Bjorner 911ffc370a separate MaxSMT functionality to enable using this independently (and incrementally) of overall context
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-02-16 09:11:28 +01:00
Nuno Lopes d3fb5f2a4c fix misc compiler warnings
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
2015-02-15 11:53:24 +00:00
Christoph M. Wintersteiger 3a8a62fc4c Added array index/element sort detection to static_features 2015-02-09 13:41:45 +00:00
Christoph M. Wintersteiger d7a37f246c More bugfixes for smt setup
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-02-08 16:59:46 +00:00
Christoph M. Wintersteiger 4792c5fb7c Fixed bugs in static features and smt setup
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-02-08 16:53:08 +00:00
Nikolaj Bjorner 8141dadc89 break on small cores
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-02-08 10:22:06 +01:00
Christoph M. Wintersteiger 3478cdb756 Added smt kernel setup for QF_FP(BV). Thanks to codeplex user smccamant for reporting this performance problem.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-02-03 12:30:42 +00:00
unknown f020b7c7b8 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2015-01-28 17:54:26 -08:00
Christoph M. Wintersteiger bcfefdd8ee Bugfix for the FPA theory. Thanks to codeplex user smccamant for reporting this one.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-28 15:38:08 -06:00
Christoph M. Wintersteiger 560fa79d1f eliminated unused variable 2015-01-21 19:36:41 +00:00
Christoph M. Wintersteiger 25011bc034 eliminated unused variables 2015-01-21 19:35:29 +00:00
Christoph M. Wintersteiger 826d295981 build fixes and removed unused variables 2015-01-21 19:29:31 +00:00
Christoph M. Wintersteiger d56d63e3e8 Merge branch 'fpa-api' of https://git01.codeplex.com/z3 into unstable
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>

Conflicts:
	src/tactic/portfolio/default_tactic.cpp
2015-01-21 14:25:31 +00:00
Christoph M. Wintersteiger ae792f1891 avoid spurious warning message
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-21 13:47:32 +00:00
Christoph M. Wintersteiger e20dc9f9a4 typo
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-21 13:35:25 +00:00
Nikolaj Bjorner e50e02e656 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2015-01-20 16:38:55 -08:00
Nikolaj Bjorner e24db56650 integrating new integer primal loop
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-01-20 16:38:45 -08:00
Christoph M. Wintersteiger d8f90802c0 Added FPA setup to default kernel setup
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-19 18:14:22 +00:00
Nikolaj Bjorner 82f1e81ac2 fix build errors on gcc
Signed-off-by: Nikolaj Bjorner <nbjorner@z3-mac.local>
2015-01-19 00:50:08 +00:00
Nikolaj Bjorner 4bb5302def template args
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-01-18 15:54:18 -08:00
Nikolaj Bjorner d45c7ce082 prepare revised primal phase
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-01-18 04:11:40 +05:30
Christoph M. Wintersteiger 88aa349eb7 Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 2015-01-16 12:30:28 +00:00
Nikolaj Bjorner b9bbfbdbb7 fix interval dependencies bug. Codeplex issue 163
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-01-16 12:05:12 +05:30
Nikolaj Bjorner 41ad1d50f9 fix java compilation bug
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-01-16 08:08:51 +05:30
Christoph M. Wintersteiger 5344d6f3c0 various bugfixes and extensions for FPA
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-15 19:25:49 +00:00
Nikolaj Bjorner 05b7aa3ebb flush cache when proof mode changes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-01-15 14:32:18 +05:30
Nikolaj Bjorner e28701a64c add assertions to simplifier
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-01-14 22:09:48 +05:30
Christoph M. Wintersteiger c0bc2518b0 Renaming for consistency mk_value -> mk_numeral
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-08 14:22:44 +00:00
Christoph M. Wintersteiger 0cedd32ea2 More renaming floats -> fpa
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-08 13:47:26 +00:00
Christoph M. Wintersteiger 5e5758bb25 More float -> fpa renaming
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-08 13:37:18 +00:00
Christoph M. Wintersteiger dd17f3c7d6 Renaming floats, float, Floats, Float -> FPA, fpa
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-08 13:18:56 +00:00
Nikolaj Bjorner 52c6f7c3b1 refine the safety check for leaving basis. As long as all base variables are unbounded in compatible directions as the non-basic variable we can detect unbounded variables. This partial check fixes integer divergence in a case exposed by Karpenov. Establishing or converting this to a check that always identifies unbounded integer variables is left for further analysis.
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-01-06 15:22:40 -08:00
Nikolaj Bjorner 129e048a1b Adding field update feature
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-01-03 01:27:52 -08:00
Christoph M. Wintersteiger 076c709453 cosmetics
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-01 19:00:06 +00:00
Christoph M. Wintersteiger 09247d2e29 FPA theory and API overhaul
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2015-01-01 18:44:41 +00:00
Christoph M. Wintersteiger 7d61223a3a Improved FP theory
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-12-31 18:34:42 +00:00
Christoph M. Wintersteiger afae49b9ed More renaming QF_FPA -> QF_FP
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-12-31 16:15:40 +00:00
Nikolaj Bjorner a296023823 incorrect offset calculation in diff logic optimization. codeplex issue 156
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-12-29 16:15:19 -08:00
Nikolaj Bjorner c54a19b084 generate proof justifications in theory_pb: codeplex issue 157
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-12-29 12:57:02 -08:00
Christoph M. Wintersteiger 05121e25d4 FPA theory support for conversion functions
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-12-28 19:28:48 +00:00
Christoph M. Wintersteiger 12aaa0610b FPA: added get_some_value/s for FP models
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-12-28 15:27:40 +00:00
Christoph M. Wintersteiger 23aa614d55 FPA: New theory implementation with support for "hidden" variables, relevancy, and eq/diseq.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-12-28 13:44:29 +00:00
Nikolaj Bjorner f373996f09 Merge branch 'opt' of https://git01.codeplex.com/z3 into opt 2014-12-22 09:27:48 -08:00
Nikolaj Bjorner c61e9f27db local changes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-12-22 09:27:33 -08:00
Christoph M. Wintersteiger 0ceb67ae33 Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api 2014-12-21 18:47:02 +00:00
Christoph M. Wintersteiger cf4b7219e1 new theory_fpa. plenty of bugs remain.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-12-21 18:45:36 +00:00
Christoph M. Wintersteiger 47325c5fd3 FPA: bugfixes, naming convention, core theory additions
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-12-16 23:59:27 +00:00
Nikolaj Bjorner f4d256ef30 fix issue 153: assert rem/mod axiom no matter what is status of second argument
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-12-16 11:20:34 -08:00
Nikolaj Bjorner ae3d16bc50 fix overflow and integrality bugs reported by Phan
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-12-15 16:18:09 -08:00
Christoph M. Wintersteiger f11ee40c38 FPA: bug and leak fixes
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-12-14 19:09:17 +00:00
Christoph M. Wintersteiger 4e913bb18c FPA bugfixes
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-12-14 17:34:18 +00:00
Christoph M. Wintersteiger b30e61e528 FPA: bugfixes, leakfixes, added fp.to_real
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-12-13 19:34:55 +00:00
Christoph M. Wintersteiger d6ac98a494 FPA API: reintroduced to_ieee_bv
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-12-11 12:05:52 +00:00
Christoph M. Wintersteiger 657595818e FPA API: Renaming for consistency with final SMT standard.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-12-10 18:45:44 +00:00
Nikolaj Bjorner 08cb8b8de8 address divergence in the case of shared theory symbols. Codeplex issue 147, thanks to George Karpenkov
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-12-09 16:04:25 +01:00
Christoph M. Wintersteiger b7c5a29570 FPA theory bug fixes
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-11-11 18:36:18 +00:00
Christoph M. Wintersteiger 8d3ef92383 Merge branch 'unstable' of https://git01.codeplex.com/z3 into fpa-api
Conflicts:
	scripts/mk_project.py
	src/api/z3.h
	src/ast/float_decl_plugin.cpp
	src/ast/float_decl_plugin.h
	src/ast/fpa/fpa2bv_converter.cpp
	src/ast/fpa/fpa2bv_rewriter.h
	src/ast/rewriter/float_rewriter.cpp
	src/ast/rewriter/float_rewriter.h

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-11-11 11:53:39 +00:00
Nikolaj Bjorner cf8ad072d0 remove unused variable
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-11-07 16:03:27 +01:00
Nikolaj Bjorner 444879db5f fix bug reported on stackoverflow on crash for unconstrained variables
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-11-05 13:51:27 +01:00
Christoph M. Wintersteiger 6a496a1bfb Merge branch 'pure' of https://git01.codeplex.com/z3 into contrib 2014-10-24 21:17:57 +01:00
Ken McMillan d815af9f0f merge duality changes with unstable 2014-10-22 10:14:05 -07:00
Nikolaj Bjorner 0e83a2b1af merge with latest unstable
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-10-22 09:45:04 -07:00
Christoph M. Wintersteiger 7af410e6d6 FPA updates and bugfixes
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
2014-10-18 13:42:28 +01:00
Nikolaj Bjorner 7767a23626 improve error messages on incorrect parameter passing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-10-15 21:37:37 -07:00
Nikolaj Bjorner 9d75babcda add more information to error messages
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-10-15 21:33:29 -07:00
Nikolaj Bjorner ce18421a7a fix box
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-10-15 14:29:39 -07:00
Nikolaj Bjorner 69a5634e7e adding symba designated strategy (back?) to optsmt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-10-14 16:33:55 -07:00
Nikolaj Bjorner 1bb4d52cb8 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-07 15:38:57 -07:00
Nikolaj Bjorner d6964226c7 indentation
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-10-07 15:38:44 -07:00
Nikolaj Bjorner 4ea3ed7e27 ensure parameters are updated and ensure that global use of auto-config is not obscured by smt.auto-config scoping
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-10-07 11:00:45 -07:00
Nikolaj Bjorner 8438ac6e21 fix internalization bug when bit2bool is applied to numeral
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-10-06 15:43:24 -07:00
Nikolaj Bjorner c706e91019 merge with unstable
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-10-05 10:37:55 -07:00
Nikolaj Bjorner 47b81d2ec0 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-10-02 14:33:55 -07:00
Nikolaj Bjorner d03a4bc306 check cancel flag after bcp. BCP returns in incomplete state after it check's the cancel flag. Propagate returns 'true' in this case so that the main loop exits
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-10-02 14:33:42 -07:00
Ken McMillan c5f17df310 fixing an assert caused by previous change in theory_array_base.cpp 2014-10-01 18:15:33 -07:00
Nikolaj Bjorner cce287eed1 fix bug in Shannon decomposition for translating PB constraints into formulas
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-10-01 12:51:40 -07:00
Ken McMillan 4763532501 adding compile-time option to replace arrays with maps in smt (define SPARSE_MAP) 2014-09-30 11:25:47 -07:00
Ken McMillan 4c71e9479d optimizing array final check 2014-09-30 11:21:34 -07:00
Nikolaj Bjorner 989569b154 add bceq experiment
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-29 10:57:31 -07:00
Nuno Lopes 97a5e6d326 assorted compiler warnings fixes
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
2014-09-28 12:21:56 +01:00
Nikolaj Bjorner 9412890c63 trace reason for undef in arithmetic, enable model generation on THEORY incompleteness, but retain undef result
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-26 12:58:55 -07:00
Nikolaj Bjorner e6725b2344 merge unstable into opt
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-26 12:12:24 -07:00
Nuno Lopes aaa931e0d5 fix build with gcc
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
2014-09-25 15:56:01 +01:00
Nikolaj Bjorner 45bfcda16c remove typename
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-17 16:37:53 -07:00
Nikolaj Bjorner e8b9c251d5 Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable 2014-09-16 17:13:20 -07:00
Nikolaj Bjorner d01ca11001 reduce asymptotic overhead of asserting bounds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-09-16 17:13:09 -07:00