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

797 commits

Author SHA1 Message Date
Nikolaj Bjorner
9ca5b3f304 fix #4449 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-06-03 21:10:07 -07:00
Nuno Lopes
e844aef896 remove a few more copy constructors, though still not enough to enable the assertion in vector 
I give up for now; there are too many copies left for little return..
 2020-06-03 20:32:13 +01:00
Nikolaj Bjorner
becf423c77
remove level of indirection for context and ast_manager in smt_theory (#4253) 
* remove level of indirection for context and ast_manager in smt_theory

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

* add request by #4252

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

* move to def

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

* int

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-08 16:46:03 -07:00
Nikolaj Bjorner
54f38d004b fix #4235 2020-05-07 10:50:56 -07:00
Nikolaj Bjorner
6a61e8dd5b fix #4234 2020-05-07 10:47:46 -07:00
Nikolaj Bjorner
da9b037f2a fix #4233 2020-05-07 10:40:41 -07:00
Nikolaj Bjorner
fc6bdb9708 fix #4232 2020-05-07 10:36:53 -07:00
Nikolaj Bjorner
236edad8dc fix #4111 2020-04-26 14:44:50 -07:00
Nikolaj Bjorner
40b4ca7f86 fix #3950 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-15 15:07:53 -07:00
Nikolaj Bjorner
b889b110ee bool_vector, some spacer tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-05 12:59:04 -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
b3c863fb15 fix #3660 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-04-01 11:05:03 -07:00
Nikolaj Bjorner
e2a247a64a fix #3601 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-31 13:48:44 -07:00
Nikolaj Bjorner
0b10cb3312 fix #3528 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-30 11:00:02 -07:00
Nikolaj Bjorner
1155db383e fix #3540 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-29 10:55:47 -07:00
Nikolaj Bjorner
5da2169a0e fix #3524 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 10:38:13 -07:00
Nikolaj Bjorner
868a6b3594 fix #3521 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-26 09:44:00 -07:00
Nikolaj Bjorner
f92050c7e5 fix #3515 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 13:21:02 -07:00
Nikolaj Bjorner
e5e6f481f9 update bounds and assert values during initialization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 04:05:58 -07:00
Nikolaj Bjorner
477fd3fba0 remove model initialization all-together because assumption literals are not connected with model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 04:00:21 -07:00
Nikolaj Bjorner
a7495876fd fix #3506 fix #3505 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 03:06:02 -07:00
Nikolaj Bjorner
504a7550b3 fix #3509 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-25 02:42:30 -07:00
Nikolaj Bjorner
044d6316ca fix #3417 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-19 09:39:21 -07:00
Nikolaj Bjorner
b3e1e302f7 fix #3320 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-18 13:22:17 -07:00
Nikolaj Bjorner
daadc1dd8c fix #3391 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-18 13:04:30 -07:00
Nikolaj Bjorner
19cdf08818 fix #3396 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-18 12:45:37 -07:00
Nikolaj Bjorner
752b498254 fix #3384 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-17 18:02:30 -07:00
Nikolaj Bjorner
6ad261e24c fix #3330 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-15 09:49:44 -07:00
Nikolaj Bjorner
4d30e9b411 fix #3332 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-03-15 09:16:44 -07:00
Nikolaj Bjorner
11199619a5 prepare for throttling gcd test and patching based on cost/success ratio 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-26 19:02:56 -08:00
Nikolaj Bjorner
82273da630 fix #2945 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-09 15:43:21 -08:00
Nikolaj Bjorner
5d772c1eb1 retrieve model before push 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-06 01:38:59 -08:00
Nikolaj Bjorner
d418467089 can't validate when benchmarks use strict bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-02-03 08:26:13 -08:00
Nikolaj Bjorner
773b27296f translate optimize from c++ API #2859 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-15 04:24:51 -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
ebc9b7fb4e fix #2841 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-01-06 11:05:00 -08:00
Nikolaj Bjorner
918846a97e fix #2814 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-12-20 16:35:38 -08: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
85fb6f59de disable ackermannize on goal 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-07 17:56:21 +03:00
Nikolaj Bjorner
228d68f165 enhance ackermannize for constant arguments 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-07 16:36:09 +03:00
Nikolaj Bjorner
000e485794 add array selects to basic ackerman reduction improves performance significantly for #2525 as it now uses the SAT solver core instead of SMT core 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-09-01 12:17:19 -07:00
Nikolaj Bjorner
35fa24a82a initialize best model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-08-28 12:31:13 -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
53aded3198 fix #2416 exposed bugs: unsat-core extraction in combination with chronological backracking, equivalence elimination in combination with PB constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-25 18:55:44 -07:00
Nikolaj Bjorner
8a0d79251e make sorting of soft constraints the same across implementations of std::sort 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-25 11:32:49 -07:00
Nikolaj Bjorner
c2264c73f2 debug mutex 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-23 19:01:49 -07:00
Nikolaj Bjorner
1fca76b0a1 relax restriction on infinitesimal for rdl, #2410 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-18 08:26:23 -07:00
Nikolaj Bjorner
5820b16800 mark assumption literals to be skolem to hide them from models #2406 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-07-18 08:25:42 -07:00
Nikolaj Bjorner
8893913c98 remove internal referenes to set_activity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 16:06:05 -07:00
Nikolaj Bjorner
c012f6ea5b fix #2210 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-07 03:09:48 +02:00