3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-20 23:56:37 +00:00
Commit graph

54 commits

Author SHA1 Message Date
Nikolaj Bjorner c2b7b58c78 #7468 - add option (get-info :parameters) to display solver parameters that were updated globally and distinct from defaults
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2025-02-10 11:57:14 -08:00
Nikolaj Bjorner 1ace3d0cf3 fix #7372
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2024-09-12 10:37:56 -07:00
Nikolaj Bjorner 0eea021dc3 include global parameters and fixup for HTML meta-characters 2022-08-22 14:25:18 -07:00
Nikolaj Bjorner e83a70f9ad add newlines for description
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-19 06:57:39 -07:00
Nikolaj Bjorner b169292743 add parameter descriptions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-16 08:26:53 -07:00
Nikolaj Bjorner 7da9f12521 expose description of global parameters #6048
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-05-27 08:50:40 -04:00
Nuno Lopes 43f7636826 remove some copies/moves 2022-03-09 12:46:41 +00:00
Nuno Lopes 689e2d41de remove a bunch of unneeded memory allocations 2022-02-25 16:08:23 +00:00
Nikolaj Bjorner ec034679ce #5215
memory leaks
2021-05-19 12:42:38 -07:00
Nikolaj Bjorner ab1f2f2e63 reduce use of symbols in gparams
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-01-10 12:54:26 -08:00
Nuno Lopes 87a96d7bd4 fix mutexes hanging due to access to free'd memory
Thanks to Kevin de Vos for reporting the bug & testing the fix
2019-09-03 20:02:21 +01:00
Nuno Lopes cb75326686 minor code simplification 2019-09-03 15:51:51 +01:00
Nuno Lopes c21f0c2f00 restore most global muxes as heap-allocated to avoid crashes with hard-kills like ctrl-c 2019-06-13 18:42:57 +01:00
Nuno Lopes cf3e649462 fix crash on Mac due to different destruction order of globals
the mutex in memory_manager has to be destroyed after all mem deallocations happen
2019-06-13 11:22:18 +01:00
Nikolaj Bjorner 71c38a08e5 add initialization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-11 19:28:08 -07:00
Nuno Lopes a53ff6f21c turn locks into no-ops when compiled with -DSINGLE_THREAD 2019-06-05 12:11:27 +01:00
Nikolaj Bjorner 9262908ebb mux
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-05 09:06:17 +01:00
Nuno Lopes cd4b53500c avoid a few str copies + symbol hiding 2019-03-08 10:13:46 +00:00
Nuno Lopes 6a0c409b0f move a few strings instead of copying 2019-02-28 10:53:27 +00:00
Nikolaj Bjorner a9e6d83c6e std::cout -> out
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-18 10:40:08 -08:00
Nuno Lopes cef17c22a1 remove some allocs from exceptions 2018-07-02 17:08:02 +01:00
Nikolaj Bjorner 78b9f0686a merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-05-01 07:43:29 -07:00
Nikolaj Bjorner f525f43e43 merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-04-30 09:30:43 -07:00
Nikolaj Bjorner b8193a0ae6 fix #1604
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-04-29 10:04:42 -07:00
Nikolaj Bjorner c513f3ca09 merge with master
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-03-25 14:57:01 -07:00
Bruce Mitchener 76eb7b9ede Use nullptr. 2018-02-12 14:05:55 +07:00
Nikolaj Bjorner 651587ce01 merge with master branch
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-09-19 09:39:22 -07:00
Nikolaj Bjorner b19f94ae5b make include paths uniformly use path relative to src. #534
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-07-31 13:24:11 -07:00
Nikolaj Bjorner 5752830f71 bug fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2017-06-22 15:01:12 -07:00
Nikolaj Bjorner 940fed16e1 enforce stringstream formatting to avoid default format routine. fixes issue #149
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-07-06 09:11:52 -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
Nikolaj Bjorner 301f441801 bypass simplifier if (m_is_clausal) {
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-10-22 09:02:08 -07:00
Nikolaj Bjorner 1059d226e4 add default statement instead of incomplete cases
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-10-21 13:25:19 -07:00
Nikolaj Bjorner d77d6c6648 update parameter checking for doubles, and fix error reporting
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-10-21 13:24:31 -07:00
Nikolaj Bjorner 7f04529080 validate types of parameter values that get set globally
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2014-10-21 09:11:38 -07: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
Nuno Lopes 7ce88d4da9 fix a few compilation warnings
- remove unused variables and class fields
 - add support for gcc 4.5 & clang's __builtin_unreachable
 - fix 2 bugs related to strict aliasing
 - remove a few unused function parameters

Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
2013-04-21 14:36:39 -07:00
Leonardo de Moura 1c96a7d52f Add option smt.bv.enable_int2bv in the new parameter setting framework. This is the new name for the old parameter :bv-enable-int2bv-propagation. This modification addresses an issue reported at http://stackoverflow.com/questions/15798984/bv-enable-int2bv-propagation-option.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2013-04-03 15:51:09 -07:00
Leonardo de Moura 589f2c6bb3 improved unknown parameter error msg
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-10 18:46:02 -08:00
Leonardo de Moura 7f210d55be fixed warnings on Win64
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-10 07:52:33 -08:00
Leonardo de Moura 6f5f1b290e better error message for renamed parameter names
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-04 15:33:21 -08:00
Leonardo de Moura 2eef4cc1e7 forgot synch
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-04 11:59:46 -08:00
Leonardo de Moura 92a29b1e43 added Z3_global_param_reset_all API
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-04 11:55:12 -08:00
Leonardo de Moura 847c5f9691 fixing problems
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-03 11:55:24 -08:00
Leonardo de Moura a99b8fe797 exposed rewriter parameters
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-02 22:03:30 -08:00
Leonardo de Moura 91096b638a better help
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-02 17:18:25 -08:00
Leonardo de Moura fa53b1eb92 added module descriptions
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-02 13:15:56 -08:00
Leonardo de Moura f15de18c4a context params
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-01 22:53:55 -08:00
Leonardo de Moura 02e763bb6b env params
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2012-12-01 20:56:40 -08:00