mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
13093 commits 49 branches 53 tags 182 MiB
Commit graph

13093 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
ae982c5225 add tc and trc functionals for binary relations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-10 04:12:45 +02:00
Nikolaj Bjorner
d3305aac16
Merge pull request #2224 from maxzinkus/patch-1 
Require verbosity=1 to log parallel tactic progress
 2019-04-10 02:26:29 +02:00
Max Zinkus
45595af665
Require verbosity=1 to log parallel tactic progress 2019-04-09 12:35:04 -04:00
Nils Becker
7ead159b2d comments for log_axiom_definitions 2019-04-09 16:54:54 +02:00
Nikolaj Bjorner
6cc82f0401 enable theory_lra on non-linear reals if configured to use 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-07 07:23:32 -07:00
Nikolaj Bjorner
9e62a7834d Merge branch 'master' of https://github.com/z3prover/z3 2019-04-05 03:06:58 -07:00
Nikolaj Bjorner
f1a2e875b5 fixing #2217 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-05 03:06:41 -07:00
Nikolaj Bjorner
56ac3f86a5 fix justification for implied equalities in special relations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-03 17:08:10 -07:00
Nikolaj Bjorner
dfd327f287 add tuple and disjoint sum shorthands 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-02 18:36:35 -07:00
Nikolaj Bjorner
6360798a53 local 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-02 17:40:38 -07:00
Nikolaj Bjorner
ff6d703c05 add tracing, fix #2214, remove unused variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-02 12:20:55 -07:00
Nikolaj Bjorner
5fdf5b67a4 remove not 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-01 12:17:49 -07:00
Nikolaj Bjorner
7e7cdf3635 update dependencies in legacy build system 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-01 12:13:50 -07:00
Nikolaj Bjorner
a9c20c96ee Merge branch 'master' of https://github.com/z3prover/z3 2019-04-01 12:10:17 -07:00
Nikolaj Bjorner
b18864d4cc
Merge pull request #2204 from Z3Prover/sr 
Special relations
 2019-04-01 12:01:55 -07:00
Nikolaj Bjorner
4fb867a49c na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-04-01 11:57:07 -07:00
Nikolaj Bjorner
3afe081f62 fixup compiled patterns 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-29 11:42:40 -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
1c694fd42f sr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 16:11:16 -07:00
Nikolaj Bjorner
7a6823aef1 add special relations tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 10:07:50 -07:00
Nikolaj Bjorner
ec6cf7950e Merge branch 'sr' of https://github.com/z3prover/z3 into sr 2019-03-28 09:21:37 -07:00
Nikolaj Bjorner
bce1ee6d39 new files 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 09:21:34 -07:00
Nikolaj Bjorner
e4eca577f6 fix po model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:22 -07:00
Nikolaj Bjorner
175008a6c6 adding po evaluator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:22 -07:00
Nikolaj Bjorner
f55e4ccc41 support indexed relations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:22 -07:00
Nikolaj Bjorner
81b1338af6 display methods 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:22 -07:00
Nikolaj Bjorner
87bc4cf693 virtual -> override 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:22 -07:00
Nikolaj Bjorner
57609e57f5 include path 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:22 -07:00
Nikolaj Bjorner
b46cedf647 include path 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner
8d5507008e adding cmd_context 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner
5536834019 add API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner
e3a2168a20 e_id3 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner
6a9cbe1461 l -> eq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner
892be69d51 nits 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner
168b0bcc44 tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner
1e751422e1 remove unused code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner
f8b8d5b870 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner
10ba731697 tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner
c714abbff2 use override 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner
5baef8bcf3 use for pattern 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner
876aa01167 add sr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:04:21 -07:00
Nikolaj Bjorner
4e38e90e2b fix po model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-28 07:03:04 -07:00
Nikolaj Bjorner
c69e911a79 adding po evaluator 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-27 16:59:13 -07:00
Nikolaj Bjorner
deb48bffe1 possible fix for #2182 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-27 10:35:27 -07:00
Christoph M. Wintersteiger
ce8263cf27
Merge branch 'master' of https://github.com/Z3Prover/z3 2019-03-27 17:34:40 +00:00
Christoph M. Wintersteiger
d1d49ef3a9
Fix BV-conversion of fp.roundToIntegral. Fixes #2191. 2019-03-27 17:13:00 +00:00
Nikolaj Bjorner
51a26ceb9e more segfault sources #2205, examining bit2bool internalization for #2282 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-27 09:50:13 -07:00
Nikolaj Bjorner
5478955199 disable cancelation during propagation at base level 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-26 16:19:50 -07:00
Nikolaj Bjorner
fde7283bb9 support indexed relations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-26 08:39:56 -07:00
Nikolaj Bjorner
b89cd9aea6 display methods 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-03-26 08:15:26 -07:00