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

2486 commits

Author SHA1 Message Date
Nikolaj Bjorner f9b6e4e247 batch length enforcement 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-06 15:25:33 -07:00
Nikolaj Bjorner b53f66bf2f avoid access to invalid m_length 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-06 10:58:25 -07:00
Nikolaj Bjorner 39edf73e78 fix #2613 fix #2612 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-05 16:57:51 -07:00
Nikolaj Bjorner 016732aa59 move some tracing to verbose 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-03 17:21:47 -07:00
Nikolaj Bjorner 5b4cd6dde4 fix #2604 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-02 20:36:49 -07:00
Nikolaj Bjorner 88f0e4a64c fix #2592 #2593 #2597 #2573 - duplicates, also fix #2603 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-01 13:14:12 -07:00
Murphy Berzish fe7a7fe23f z3str3: fail early on non-string sequence terms 2019-09-30 21:05:41 -07:00
Nikolaj Bjorner 292e72ce0c fix #2590 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-28 17:47:15 -07:00
Murphy Berzish f29b033253 z3str3: add is_var() similar to theory_seq's implementation 2019-09-28 17:45:49 -07:00
Murphy Berzish 1c70bcee69 z3str3: setup uninterpreted functions as though they were string variables 2019-09-28 17:45:49 -07:00
Nikolaj Bjorner deb45c09e8 fix #2586 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-26 08:59:52 -07:00
Nikolaj Bjorner 3dcfbb8347 fix #2585 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-25 18:57:51 -07:00
Nikolaj Bjorner d0fc463a0c fix #2581 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-24 15:56:53 -07:00
Nikolaj Bjorner f7cc68aa6a fix #2580 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-24 08:58:36 -07:00
Nikolaj Bjorner a44cf7a9ba unused variable warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-22 10:15:20 -07:00
Nikolaj Bjorner 4b51fe466d fix #2562 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-17 11:49:11 -04:00
Nikolaj Bjorner 0f20175bdd fix #2556, sign of of inequality is not restricted to -1, 0, 1, but can be -2, -3 etc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-14 19:41:01 -04:00
Nikolaj Bjorner 0c972b8bee tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-13 15:45:10 -04:00
Nikolaj Bjorner fffc539b40 fix #2549 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-13 17:42:29 +02:00
Nikolaj Bjorner 098725aa1c fix #2553 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-13 15:03:05 +02:00
Nikolaj Bjorner 67c4777514 fix #2548 fix #2530 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-13 15:03:04 +02:00
Nikolaj Bjorner 63840806d8 fix #2546, retrieve model in optsmt lex before iterating 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-10 11:19:59 +02:00
Nikolaj Bjorner 0481adb87c fix #2547 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-10 06:38:27 +02:00
Nikolaj Bjorner 78a1f53ac9 fix #2544 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-09 18:07:03 +02:00
Nikolaj Bjorner b1cdb3e451 add mbqi to smtfd. For Nuno, of course 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-09 11:28:25 +02:00
Murphy Berzish 18ba14cff8 Z3str3: fix empty-string contradictions (#2538) 
* z3str3: str.indexof second argument can be empty string without causing contradictions

* z3str3: str.indexof second argument can be empty string without causing contradictions

* z3str3: fixups for str.indexof

* z3str3: str.indexof code cleanup
 2019-09-07 16:35:20 +03:00
Nikolaj Bjorner 8ec6219010 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-06 09:42:57 +03:00
Nikolaj Bjorner a92c82d895 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-06 09:42:57 +03:00
Nikolaj Bjorner 68e4ed3c9c fix #2531 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-02 09:59:58 -07:00
Nikolaj Bjorner e816d16724 fix #2527 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-31 10:09:52 -04:00
Nikolaj Bjorner 4c0db00a7b fix push/pop bug for ite-elimination, thanks to Nao Hirokawa for reporting it 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-30 08:31:37 -03:00
Nikolaj Bjorner de43e05102 fix overflow bug exposed by #2476 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-29 22:34:04 -03:00
Nikolaj Bjorner 20dc59e02d fix #2523 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-28 12:28:33 -03:00
Nikolaj Bjorner 2e6908bd9e fix #2509, fix issue with model inheritance exposed by #2483 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-27 10:48:22 -03:00
Nikolaj Bjorner 271cd2ac6b disable expensive model validation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-26 07:26:12 -03:00
Nikolaj Bjorner 75a40d8f8e reorder fields, rename overload name clash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-25 16:01:39 -03:00
Nikolaj Bjorner 64f4c9794d fix regressions during string fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-25 10:00:26 +01: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 a337a51374 fixes for #2513 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-23 23:29:24 +03:00
Nikolaj Bjorner de69b01e92 Lev's fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-23 23:29:24 +03:00
Nikolaj Bjorner 2b2f016f96 python for accessing lambda, switch to theory branching for QF_LRA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-14 15:44:34 -07:00
Nikolaj Bjorner 520ea65f32 move towards theory phase selection, implement getitem on lambda 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-14 15:44:33 -07:00
Nikolaj Bjorner 75962173ff fix #2481 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-12 09:38:45 -07:00
Nikolaj Bjorner 9fa9aa09ff fix #2468, adding assignment phase heuristic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-10 15:25:05 -07:00
Nikolaj Bjorner 8579a004d0 distribute concat over bvxor and bvor, #2470 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-07 15:14:58 -07:00
Nikolaj Bjorner e950453685 force propagation for smt cubing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-06 14:19:16 -07:00
Nikolaj Bjorner 0af249d651 'na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-06 13:44:12 -07:00
Bruce Mitchener 077f518241 Fix -Wreorder warning. 2019-08-04 18:37:31 -07:00
Nikolaj Bjorner bc3b0f6e33 introduce fresh term when none is available in context or model to fix #2456 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-04 12:00:48 -07:00
Nikolaj Bjorner 01920abf46 introduce fresh term when none is available in context or model to fix #2456 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-04 11:57:30 -07:00