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

3796 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
e81dc5a0a0 fixes issue #143 and memory leak on theory plugin setup 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-26 09:03:56 +02:00
Nikolaj Bjorner
47da717947 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-06-26 08:24:58 +02:00
Nuno Lopes
f29d82858f make check_relation::check_equiv() exit only when solver return SAT (ie, avoid false-positives with unknowns) 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-24 17:13:24 +01:00
Nuno Lopes
30eb461e01 disable debug output from check_relation 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-24 17:06:22 +01:00
Nuno Lopes
5cc8c8bde6 udoc: micro optimization for compiler_guard 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-24 17:06:21 +01:00
Nikolaj Bjorner
6bf87083ef fix build break 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:20 +01:00
Nikolaj Bjorner
1544105bd5 set undo trail after set-watches to avoid crash during exception handling (the relevancy trail is scoped so ends up traversing the trail if allocating the watch throws an exception). Fixes crash.smt in issue #56 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:20 +01:00
Nikolaj Bjorner
03034e7b33 disable bottom-up COI on rules with negated predicates. Fixes issue #140 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:19 +01:00
Nuno Lopes
44ef4074e2 build system: fix typo in OS_DEFINES for linux 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-24 17:06:18 +01:00
Nikolaj Bjorner
cd05edf833 add model on unknown, to address issue #139 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:18 +01:00
Nikolaj Bjorner
3de2a70a48 move functionality from qe_util to ast_util 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:17 +01:00
Nikolaj Bjorner
7b918e83c3 fix distribute forall, fixes issue #138 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:16 +01:00
Nikolaj Bjorner
020620aadd disable qf-ufnra tactic from default for testing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:16 +01:00
Nikolaj Bjorner
8df919b6bb fix mixed integer/real bugs for maximization exposed by non-termination in slow.smt. partially fixes issue #56 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:15 +01:00
Nikolaj Bjorner
aa4b9e68d7 exposing facility to extract dependent clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:14 +01:00
Nuno Lopes
949f3f9201 Run link-time optimization on windows only when configured with --optimize 
This should probably be revisited for VS 2015

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-24 17:06:14 +01:00
Nikolaj Bjorner
38113e8434 include statistics from sub-modules for QF_UFNRA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:13 +01:00
Nikolaj Bjorner
238e38eaa2 update unit tests for num allocs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:12 +01:00
Nikolaj Bjorner
158a5dd2db add count of memory allocations and way to limit allocations globally. Fix purification in nlsat_smt to fix regressions on QF_UFNRA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:12 +01:00
Nikolaj Bjorner
e7385d60fb fixes to githup issue #133 and stackoverflow reported bug on assertion violation in poly_simplifier_plugin 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:11 +01:00
Nikolaj Bjorner
45d2ffa38c hide new behavior until tested 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:10 +01:00
Nikolaj Bjorner
5aee077d55 enable incremental sat for QF_BV 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:10 +01:00
Nikolaj Bjorner
0518e69d2a isolate inc_sat_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:09 +01:00
Nikolaj Bjorner
22c0a593e7 deal with unit test failure cases, fixes #132 #133 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:08 +01:00
Nikolaj Bjorner
1bdedec920 add missing copyright 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:08 +01:00
Nikolaj Bjorner
baf95ce4e8 add missing copyright 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:07 +01:00
Matthias Schlaipfer
37cb5b9597 Fixed a bug in udoc_relation's join project 
An optimization was applied in too many cases and led to wrong results.

Signed-off-by: Matthias Schlaipfer <t-matsch@microsoft.com>
 2015-06-24 17:06:06 +01:00
Nikolaj Bjorner
8fc6789955 remove spurious print statement 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:06 +01:00
Nikolaj Bjorner
1a5327e427 strengthen quantifier check for PDR (and other engines) that don't handle quantified predicates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 17:06:05 +01:00
Christoph M. Wintersteiger
9a62d989e6 Revert "Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable" 
This reverts commit d3db21ccde, reversing
changes made to e463d5d899.
 2015-06-24 17:06:04 +01:00
Nikolaj Bjorner
c3e666bc44 fix build break 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-24 07:40:23 +02:00
Nikolaj Bjorner
108d76270e set undo trail after set-watches to avoid crash during exception handling (the relevancy trail is scoped so ends up traversing the trail if allocating the watch throws an exception). Fixes crash.smt in issue #56 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-23 19:18:03 +02:00
Nikolaj Bjorner
0eaaafc79d Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-06-23 18:57:35 +02:00
Nikolaj Bjorner
46ca7e17e0 disable bottom-up COI on rules with negated predicates. Fixes issue #140 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-23 18:57:16 +02:00
Nuno Lopes
e441db5bc4 build system: fix typo in OS_DEFINES for linux 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-23 13:59:36 +01:00
Nikolaj Bjorner
77c8e5b0a0 add model on unknown, to address issue #139 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-23 14:45:52 +02:00
Nikolaj Bjorner
bf5419d44a move functionality from qe_util to ast_util 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-23 14:33:45 +02:00
Nikolaj Bjorner
5f484c069b fix distribute forall, fixes issue #138 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-23 14:15:14 +02:00
Nikolaj Bjorner
f3f85b5e0f disable qf-ufnra tactic from default for testing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-23 14:05:49 +02:00
Nikolaj Bjorner
d9522cfd07 fix mixed integer/real bugs for maximization exposed by non-termination in slow.smt. partially fixes issue #56 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-23 12:05:19 +02:00
Nikolaj Bjorner
d32e4a9476 exposing facility to extract dependent clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-22 23:36:52 +02:00
Nikolaj Bjorner
7005027fde Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-06-22 23:36:28 +02:00
Nuno Lopes
2771862583 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-06-22 14:49:02 +01:00
Nuno Lopes
4346966f00 Run link-time optimization on windows only when configured with --optimize 
This should probably be revisited for VS 2015

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-22 14:48:50 +01:00
Nikolaj Bjorner
ad0bdd7508 include statistics from sub-modules for QF_UFNRA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-22 14:01:36 +02:00
Nikolaj Bjorner
ed806b67fb update unit tests for num allocs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-22 13:20:59 +02:00
Nikolaj Bjorner
564da787fb add count of memory allocations and way to limit allocations globally. Fix purification in nlsat_smt to fix regressions on QF_UFNRA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-22 07:45:40 +02:00
Nikolaj Bjorner
4675643271 fixes to githup issue #133 and stackoverflow reported bug on assertion violation in poly_simplifier_plugin 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-21 13:49:15 -07:00
Nikolaj Bjorner
6f0d76a62e Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-06-21 09:39:32 -07:00
Nikolaj Bjorner
3a9f8276fe hide new behavior until tested 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-21 02:25:02 -07:00