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

184 commits

Author SHA1 Message Date
Nikolaj Bjorner bee3077640 free memory in egraph 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-30 20:13:46 -07:00
Nikolaj Bjorner a003af494b release nodes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-30 20:09:27 -07:00
Nikolaj Bjorner bbe027f6a1 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-30 15:03:15 -07:00
Nikolaj Bjorner 25106866b5 fix dotnet build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-30 14:46:31 -07:00
Nikolaj Bjorner 727ea43b16 remove lazy push from theory_lra 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-30 12:07:14 -07:00
Nikolaj Bjorner e8826bb20f fix #4651 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-30 09:49:12 -07:00
Nikolaj Bjorner 86310a1a27 updated sat_smt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-29 19:21:51 -07:00
Nikolaj Bjorner e9a4e486ae dbg 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-29 19:21:50 -07:00
Nikolaj Bjorner 79fc3f2375 warnings /errors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-29 09:53:24 -07:00
Nikolaj Bjorner 60f8884dbd sr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-28 15:10:52 -07:00
Nikolaj Bjorner b8fb744935 reset caches 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-28 15:09:12 -07:00
Nikolaj Bjorner 93ee2a68a4 persist fields 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-28 13:41:50 -07:00
Nikolaj Bjorner 4244ce4aad adding ack/model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-28 12:55:47 -07:00
Nikolaj Bjorner 1a36d44450 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-26 10:41:20 -07:00
Nikolaj Bjorner c21a2fcf9f sat solver setup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-26 09:40:42 -07:00
Nikolaj Bjorner ecd3315a74 add sat-euf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-25 12:16:57 -07:00
Nikolaj Bjorner 65e6d942ac euf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-24 01:55:13 -07:00
Nikolaj Bjorner ac39ddb43f flush gmc for sat-preprocessor model bug #4532 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-26 14:30:48 -07:00
Nikolaj Bjorner ec3066c28a #4532 - arithmetic using SAT for interpreted atoms such as (< 0 0) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-08 11:43:32 -07:00
Nikolaj Bjorner c70e9af09d fix #3734 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-04 12:53:24 -07:00
Nikolaj Bjorner 426e4cc75c fix #3557 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-03 16:37:59 -07:00
Nikolaj Bjorner 3d7098ec85 fix #3137 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-09 07:15:06 +01:00
Nikolaj Bjorner bd3024e837 fix #3161 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-05 17:37:38 +01:00
Nikolaj Bjorner dd3e77107e rename aig_simplifier to cut_simplifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-18 18:29:59 -08:00
Nikolaj Bjorner a9d22d7409 fix #2918 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-01 14:09:40 -08:00
Nikolaj Bjorner e0a41a18c3 add validation to aig_simplifier, start BIG-based masking 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-11 20:47:38 -08:00
Nikolaj Bjorner ca243428f8 make cutset maintainance incremental, expose option for goal2sat to populate aig 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-08 16:39:49 -08:00
Nikolaj Bjorner 57846e50fa use variable id as level, separate cut-set updates, add missing reset in pdd 2020-01-08 02:15:45 -08:00
Nikolaj Bjorner 40a4326ad4 add anf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-05 16:46:49 -08:00
Nikolaj Bjorner ca498e20d1 move value factories to model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-16 19:48:35 -07:00
Nikolaj Bjorner 185b01dd35 fix #2416 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-23 19:01:49 -07:00
Nikolaj Bjorner 41ca956012 expose import model converter over Python, document it, add partial order axioms for lex, disable linear order axioms, prepare ground for re-adding clauses from reconstruction stack 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-18 13:45:13 -07:00
Nikolaj Bjorner 333b32b0d2 disable adding redundant ite clauses as lemma. Add as non-redundant 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-21 16:32:45 +02:00
Nikolaj Bjorner cbe52e298b remove tracing, fix doctext 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-21 15:08:26 +02:00
Nikolaj Bjorner e0d8cefde4 remove cooperate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-12 20:15:46 -07:00
Nikolaj Bjorner a74ac93bcc fix #2196 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-22 13:34:31 -07:00
Nikolaj Bjorner 057151c7a8 fix #2188 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-18 07:56:25 -07:00
Nikolaj Bjorner 22783a4bcb import more from csp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-11 13:09:28 -08:00
Nikolaj Bjorner d04e72819a abstract solver API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-02-06 19:42:01 +01:00
Nikolaj Bjorner d3d392da41 adding maxlex, delay mk_true() calls in goal2sat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-24 21:36:40 -08:00
Nikolaj Bjorner 074ed0d874 fix warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-24 17:39:19 -08:00
Nikolaj Bjorner ec36a9c495 fix user push/pop with ba constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-22 12:40:23 -08:00
Nikolaj Bjorner e9d615e309 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-14 15:16:22 -07:00
Bruce Mitchener cdfc19a885 Use nullptr. 2018-10-02 09:11:19 +07:00
Nikolaj Bjorner c8730daea7 fix memory leak, add strengthening 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-03 16:56:07 -07:00
Nikolaj Bjorner 96d3b98a44 fix #1783, wronge clausification of negated pb inequalities. Signs were ignored 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-11 13:33:09 -07:00
Nikolaj Bjorner 84c7df75d6 record statistics setting in config_params so that fp engine can access them, fix serialization bug when check-assumptions returns unsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-06 16:21:27 -07:00
Nuno Lopes cef17c22a1 remove some allocs from exceptions 2018-07-02 17:08:02 +01:00
Nikolaj Bjorner 335d672bf1 fix #1675, regression in core processing in maxres 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-19 23:23:19 -07:00
Nikolaj Bjorner ff0f257102 remove iff 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-06-14 16:08:48 -07:00
Nikolaj Bjorner c513f3ca09 merge with master 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-25 14:57:01 -07:00
Nikolaj Bjorner f04e805fa4 add hiding to auxiliary declarations created in mc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-06 18:02:37 -08:00
Nikolaj Bjorner 718e5a9b6c add unit extraction 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-06 01:08:17 -08:00
Nikolaj Bjorner 4c1379e8c9 bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-19 21:49:03 -08:00
Bruce Mitchener 76eb7b9ede Use nullptr. 2018-02-12 14:05:55 +07:00
Nikolaj Bjorner 8fb7fb9f98 add missing caching of PB/cardinality constraints, increase limit for compiling cardinalities to circuits 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-11 19:27:00 -08:00
Bruce Mitchener 7167fda1dc Use override rather than virtual. 2018-02-10 09:56:33 +07:00
Nikolaj Bjorner 5e482def18 fix local search encoding bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-08 07:27:32 -08:00
Nikolaj Bjorner 61f99b242e xor to xr to avoid clang issue 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-07 15:25:02 -08:00
Nikolaj Bjorner 20fe08d80c fix more bugs with compilation of pb equalities 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-04 09:51:45 -08:00
Nikolaj Bjorner 354c16454a fix bug in translation of pbeq into sat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-03 22:19:25 -08:00
Nikolaj Bjorner 3b1810d893 fix hidden tautology bug on non-learned clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-21 23:18:41 -08:00
Nikolaj Bjorner 7fc1b75cb8 Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2018-01-19 21:36:24 -08:00
Nikolaj Bjorner e4f29a7b8a debugging mc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-19 21:09:52 -08:00
Nikolaj Bjorner 67de30ca4a Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2018-01-19 13:57:25 -08:00
Nikolaj Bjorner d6c49adddb local 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-19 13:57:21 -08:00
Nikolaj Bjorner c7ee532173 fix static 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-18 10:44:40 -08:00
Nikolaj Bjorner 7b8101c502 fix bugs related to model-converter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-17 12:25:24 -08:00
Nikolaj Bjorner 3047d930e1 fix xor processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-13 19:53:50 -08:00
Nikolaj Bjorner d79c33fb21 fix model bugs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-13 16:12:38 -08:00
Nikolaj Bjorner 1c2966f8e9 updates to model generation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-11 11:20:23 -08:00
Nikolaj Bjorner b1724b2f62 fix update to variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-28 14:39:16 -08:00
Nikolaj Bjorner 0b424942ab bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-23 14:42:21 -08:00
Nikolaj Bjorner 8198a8ce7b bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-23 14:41:16 -08:00
Nikolaj Bjorner c199344bbf fix sat model converter to work with incrementality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-18 11:12:27 -08:00
Nikolaj Bjorner 427b5ef002 set eliminated to false on literals used in clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-30 11:20:19 -08:00
Miguel Angelo Da Terra Neves cba0599046 model converter fixes 
Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>
 2017-11-29 17:14:49 -08:00
Nikolaj Bjorner a57628fbcc fix missing conversions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 14:12:05 -08:00
Nikolaj Bjorner 5f0a02b5f7 remove output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-22 09:05:17 -08:00
Nikolaj Bjorner 8230cbef4c fix mc efficiency issues 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-22 08:55:21 -08:00
Nikolaj Bjorner 87a1e2b30e Merge branch 'opt' of https://github.com/nikolajbjorner/z3 into opt 2017-11-21 13:32:44 -08:00
Nikolaj Bjorner ef30868ad7 change lookahead equivalence filter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-21 13:32:40 -08:00
Miguel Angelo Da Terra Neves 773d938925 re-adding simplified constraints based on model converter 
Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>
 2017-11-21 13:24:14 -08:00
Nikolaj Bjorner 4bbece6616 re-organize proof and model converters to be associated with goals instead of external 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-18 16:33:54 -08:00
Nikolaj Bjorner b3bd9b89b5 prepare for inverse model conversion for formulas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-17 19:55:23 -08:00
Nikolaj Bjorner 0d15b6abb7 add stubs for converting assertions, consolidate filter_model_converter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-17 14:51:13 -08:00
Nikolaj Bjorner 7c743b3d16 add direct FromFile method to solvers so that model transformations are loaded along with assertions. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-02 09:25:18 -05:00
Nikolaj Bjorner fd49a0c89c added facility to persist model transformations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-02 00:05:52 -05:00
Nikolaj Bjorner caaf0ba33c model-add/del 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-01 22:32:22 -05:00
Nikolaj Bjorner 3de8c193ea implementing model updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-30 16:11:51 -05:00
Nikolaj Bjorner 829c140087 ensure that bca takes also lemmas into account 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-27 15:40:25 -07:00
Nikolaj Bjorner ac0202630e fix non-termination bug with retained clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 15:40:11 -07:00
Nikolaj Bjorner 32711790e8 bug fixes reported by Miguel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-25 13:36:48 -07:00
Nikolaj Bjorner 4d48811efd updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-13 11:22:47 -07:00
Nikolaj Bjorner 81ad69214c fixing lookahead/ba + parallel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-11 17:06:28 -07:00
Nikolaj Bjorner 79ceaa1d13 fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-11 13:17:57 -07:00
Nikolaj Bjorner 6c4cadd223 tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-09-28 00:33:56 -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 394d54fa8b fix missin clause generation for ad-hoc handling of conjunction #1245 2017-09-05 09:54:52 -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