mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity
18005 commits 23 branches 48 tags 157 MiB
Commit graph

124 commits

Author SHA1 Message Date
Nikolaj Bjorner 31c91e1674 #6902 
add parse check for identifiers used for datatype declarations.
 2023-09-18 12:52:59 -07:00
Nikolaj Bjorner 5806869ae4 fix #6792, add scaffolding for type variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-07-07 17:22:56 -07:00
Nikolaj Bjorner 58a2a9c79c fix #6680 2023-04-11 14:42:47 -07:00
Nikolaj Bjorner 4aa05b2b57 remove limiting error mode #6600 2023-02-20 12:16:43 -08:00
Facundo Domínguez 91cdc082c4
Optimize calls to Z3_eval_smtlib2_string (#6422) 
* Allow reseting the stream of smt2::scanner

* Put the parser of parse_smt2_commands in the cmd_context

* Move parser streams to cmd_context

* Move parser fields from cmd_context to api::context

* Move forward declarations from cmd_context.h to api_context.h

* Change parse_smt2_commands_with_parser to use *& instead of **

* Add tests for Z3_eval_smtlib2_string

* Don't reuse the streams in Z3_eval_smtlib2_string

* Fix indentation

* Add back unnecessary deleted line

Co-authored-by: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
 2022-10-28 13:57:22 -07:00
Nikolaj Bjorner e5767bf2b8 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-19 15:19:07 +01:00
Nikolaj Bjorner 7de8c72246 cleanups 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-31 11:32:47 -07:00
Nikolaj Bjorner 53ab931626 #5429 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-30 21:35:09 -07:00
Nikolaj Bjorner 20a67e47ca remove symbol -> zstring -> symbol round-trips 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-22 13:12:49 -07:00
Nikolaj Bjorner a10de2e975 #5140 2021-05-22 10:15:06 -07:00
Nikolaj Bjorner ff480d1183 fix #5238 2021-05-02 16:09:01 -07:00
Nikolaj Bjorner 381e502d30 fix #5224 2021-04-29 20:12:20 -07:00
Nikolaj Bjorner 4a6083836a call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
Nikolaj Bjorner cebf83c460 fix #5146 2021-04-02 11:48:44 -07:00
Nikolaj Bjorner 937b61fc88 fix build, refactor 2021-02-02 05:26:57 -08:00
Nikolaj Bjorner 3ae4c6e9de refactor get_sort 2021-02-02 04:45:54 -08:00
Nikolaj Bjorner 520b24aab4 string escaping 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-01-30 04:58:58 -08:00
Nikolaj Bjorner 797f50e699 DRAT debugging updates 2020-11-22 15:38:57 -08:00
Nuno Lopes 23e6adcad3 fix a couple hundred deref-after-free bugs due to .c_str() on a temporary string 2020-07-11 20:24:45 +01:00
Nikolaj Bjorner 85661c415d remove ex-act 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-22 09:08:04 -07:00
Nikolaj Bjorner 274323b818 fix reset order for #4533 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-19 16:07:45 -07:00
Nikolaj Bjorner c92a63690d enable parsing (_ char ..) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-29 17:47:24 -07:00
Nikolaj Bjorner cd64967706 fix #4317 2020-05-16 17:11:47 -07:00
Nikolaj Bjorner 321329d77c fix #2910 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-01 14:31:13 -08:00
Nikolaj Bjorner 78a1736bd2 prepare symbols to be more abstract, update mbi, delay initialize some modules 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-10 12:02:08 -08:00
Nikolaj Bjorner 823bf317c5 fix #2664 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-28 05:11:46 -07:00
Nikolaj Bjorner 3e6080b265 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-02 21:06:41 -07:00
Nikolaj Bjorner 2dd9ea071d fix #2577 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-23 10:41:00 -07:00
Nikolaj Bjorner 0d9cd7bc2b addressing misc. string bugs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-24 15:40:15 +01:00
Nikolaj Bjorner f90db2ba1c add back compression to ensure local functions are inlined #2517 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-23 21:35:45 +03:00
Nikolaj Bjorner 88aa689a70 fix #2387, add ite-hoist rewriting, allow assumptions to be compound expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-09 07:40:29 +01:00
Nikolaj Bjorner b1dbea328a remove unreferenced 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-21 09:17:17 +02:00
Nikolaj Bjorner f3b79087ee add default tactic as option to overwrite the behavior of strategic solver factory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-17 09:27:10 -07:00
Nikolaj Bjorner ebc4b93d52 update documentation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-29 08:41:31 -07:00
Nikolaj Bjorner 7399f78dfd disable model compression for regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 12:40:59 -08:00
Nikolaj Bjorner 3ee5c0e7d9 fix #2164 address some of simplification shortcommings from #2151 #2152 #2153 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-03 11:33:44 -08:00
Nuno Lopes 6a0c409b0f move a few strings instead of copying 2019-02-28 10:53:27 +00:00
Nikolaj Bjorner 0acc042bf7 fix #2120 fix #2122 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-03 17:15:38 +01:00
Nikolaj Bjorner 52910fa465 fix #1937 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-14 11:31:39 -08:00
Nikolaj Bjorner aa6e1badf2 recfun 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-23 08:16:26 -07:00
Nikolaj Bjorner ccca063e54 Merge branch 'master' of https://github.com/Z3Prover/z3 into csp 2018-10-21 12:26:53 -07:00
Nikolaj Bjorner 6e41b853f7 remove case-pred and depth-limit classes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-21 12:25:57 -07:00
Florian Pigorsch 326bf401b9 Fix some spelling errors (mostly in comments). 2018-10-20 17:07:41 +02:00
Nikolaj Bjorner bd53fa801e handle case input format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-17 21:42:18 -07:00
Nikolaj Bjorner c7d0d4e191 add c-cube's recursive function theory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-17 04:56:58 -07:00
Michał Janiszewski cfd0486582 Catch exceptions by const-reference 
Exceptions caught by value incur needless cost in C++, most of them can
be caught by const-reference, especially as nearly none are actually
used. This could allow compiler generate a slightly more efficient code.
 2018-10-16 19:16:07 +02:00
Nikolaj Bjorner e9d615e309 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-14 15:16:22 -07:00
Nikolaj Bjorner 77e4340470 update parser 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-14 13:06:09 -07:00
Bruce Mitchener cdfc19a885 Use nullptr. 2018-10-02 09:11:19 +07:00
Nikolaj Bjorner 3478b8b924 add js-model interfacing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-12 18:14:06 -07:00