mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
14570 commits 49 branches 53 tags 182 MiB
Commit graph

210 commits

Author SHA1 Message Date
Nikolaj Bjorner
1ee2ba2a9b mbqi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-26 11:06:40 -07:00
Nikolaj Bjorner
72d407a49f
mbp (#4741) 
* adding dt-solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* dt

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* move mbp to self-contained module

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* files

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Create CMakeLists.txt

* dt

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* rename to bool_var2expr to indicate type class

* mbp

* na

* add projection

* na

* na

* na

* na

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* deps

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* testing arith/q

* na

* newline for model printing

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-21 15:48:40 -07:00
Nikolaj Bjorner
fa58a36b9f
model refactor (#4723) 
* refactor model fixing

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* missing cond macro

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* file

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* file

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add macros dependency

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* deps and debug

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add dependency to normal forms

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* build issues

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* compile

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix leal regression

* complete model fixer

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fold back private functionality to model_finder

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* avoid duplicate fixed callbacks

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-05 14:13:05 -07:00
Nikolaj Bjorner
08a87b102c more fpa 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-10-01 17:47:50 -07:00
Nikolaj Bjorner
4cb07a539b more fpa 2020-09-30 19:06:07 -07:00
Nikolaj Bjorner
414db51d5a stubs for model finder 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-30 08:57:18 -07:00
Nikolaj Bjorner
c0a07f9229 tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-14 04:26:59 -07:00
Nikolaj Bjorner
c4a03dcf7c remove temporary comment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-14 04:13:30 -07:00
Nikolaj Bjorner
9729db16a2 always reduce macro expansions in model evaluation #4588 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-13 17:39:15 -07:00
Nikolaj Bjorner
094e41d21d build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-13 16:40:41 -07:00
Nikolaj Bjorner
780346c7ca address model generation bugs raised in #4518 and #4324 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-24 13:22:19 -07:00
Nikolaj Bjorner
71a32f5bb2 remove unused 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-22 11:38:27 -07: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
d0e20e44ff booyah 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-04 15:56:30 -07:00
Nikolaj Bjorner
655166b867 randomize generation of 'some value' for user sorts. #4557 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-07-01 16:34:09 -07:00
Nikolaj Bjorner
1be22a80f6 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-11 17:20:18 -07:00
Nikolaj Bjorner
884a68251b fix #4266 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-11 16:53:59 -07:00
Nikolaj Bjorner
39fb44fe09 fix #4200 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-03 18:10:54 -07:00
Nikolaj Bjorner
2a93ac3d81 fix #4200 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-03 18:10:26 -07:00
Nikolaj Bjorner
a884201d62 remove using insert_if_not_there2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-25 15:08:51 -07:00
Nikolaj Bjorner
9ea1cf3c5c na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-25 13:13:25 -07:00
Nikolaj Bjorner
ad8eb8fdcb #4024 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-19 22:44:02 -07:00
Arie Gurfinkel
2b27aa1ce6 fix #3908 2020-04-11 13:58:10 -04:00
Nikolaj Bjorner
56358a6b94 fix #3867 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-08 18:06:37 -07:00
Nikolaj Bjorner
8e6bb30c82 cleanup bit2bool from models #3847 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-08 03:06:01 -07:00
Nikolaj Bjorner
35f184a6b9 fix #3826 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-07 14:39:54 -07:00
Nikolaj Bjorner
4c69f9e31b invalid model regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 15:27:06 -07:00
Nikolaj Bjorner
f0a6837c67 invalid model regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 15:17:09 -07:00
Nikolaj Bjorner
ea08fcf65c invalid model regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 15:15:48 -07:00
Nikolaj Bjorner
be1109e80f turn on model evaluation for as-array, #2420 #3646 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 12:25:12 -07:00
Nikolaj Bjorner
cc394f0fe9 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 03:42:13 -07:00
Nikolaj Bjorner
c142f99127 fix #3532 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 11:00:02 -07:00
Nikolaj Bjorner
0a97f37be5 fix #3284 (and other recent regressions) 2020-03-12 08:37:43 -07:00
Nikolaj Bjorner
bdd66e1fa0 fix #3180 fix #3181 #3184 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-07 12:13:43 +01:00
Nikolaj Bjorner
153d0661fe fix #3141 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-05 07:57:21 +01:00
Nikolaj Bjorner
2882a6708e fix #2957 - arrays are treated as values 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-18 16:35:13 -08:00
Nikolaj Bjorner
8428970a1f fix #3006 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-16 23:46:58 -10:00
Nikolaj Bjorner
806ee85759 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-11 14:25:25 -08:00
Nikolaj Bjorner
fe0b3d6648 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-18 12:03:59 -08:00
Nikolaj Bjorner
3c6dceae7c fix #2717 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-18 12:03:59 -08:00
Nikolaj Bjorner
cb600a9329 consolidate model.compact and model_compress #2704 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-15 11:07:08 -08:00
Nikolaj Bjorner
1e0c1cefd6 add definitions for under-specified cases of arithmetic operators #2663 #2676 #2679 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-06 18:24:22 +01:00
Nikolaj Bjorner
6cf7d8e523 adding div0 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-11-06 11:23:19 +01:00
Christoph M. Wintersteiger
2308d8af09
Fix for partially interpreted floating-point functions. Relates to #2596, #2631. 2019-10-28 14:15:29 +00:00
Nikolaj Bjorner
203ba12abc moving to context reset model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-18 19:22:46 -07:00
Nikolaj Bjorner
4ce6b53d95 fix #2640 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-16 20:40:03 -07: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
39edf73e78 fix #2613 fix #2612 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-05 16:57:51 -07:00
Nikolaj Bjorner
feff1f7f96 fix #2609 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-02 14:40:11 -07:00
Nikolaj Bjorner
a635049e23 fill in ad-hoc interpretation for division by 0. #2561 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-01 20:07:31 -07:00