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

4278 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nuno Lopes
3104d2954c don't crash in Z3_model_eval API if not given a valid expression 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-06-26 18:33:13 +01:00
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