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

4459 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner
949c21ca08 enable incremental sat for QF_BV 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-21 02:23:56 -07:00
Nikolaj Bjorner
fe7c577d99 isolate inc_sat_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-21 01:54:52 -07:00
Nikolaj Bjorner
18374aa12a deal with unit test failure cases, fixes #132 #133 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-17 17:30:10 -07:00
Nikolaj Bjorner
6a50f10b8b Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-06-17 12:48:28 -07:00
Nikolaj Bjorner
3af545784b add missing copyright 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-17 12:48:16 -07:00
Nikolaj Bjorner
1657cdd8b4 add missing copyright 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-17 12:47:19 -07:00
Nuno Lopes
64e1455512 Merge pull request #130 from mschlaipfer/udoc_join_project_fix 
Fixed a bug in udoc_relation's join project
 2015-06-17 20:02:43 +01:00
Matthias Schlaipfer
32a00a7062 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-17 17:14:23 +01:00
Christoph M. Wintersteiger
d3db21ccde Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-06-14 19:00:36 -07:00
Christoph M. Wintersteiger
3a49223076 Merge branch 'unstable' of https://github.com/wintersteiger/z3 into unstable 2015-06-14 19:00:09 -07:00
Christoph M. Wintersteiger
0caf3bd18c Bugfix for mpf.is_regular 2015-06-14 18:59:46 -07:00
Nikolaj Bjorner
e463d5d899 remove spurious print statement 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-12 18:31:28 -07:00
Nikolaj Bjorner
c5cdc5bd85 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-06-12 18:30:43 -07:00
Nikolaj Bjorner
61ed4e5741 strengthen quantifier check for PDR (and other engines) that don't handle quantified predicates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-12 18:30:33 -07:00
Aleksandar Zeljic
66e585e817 Merge branch 'unstable' of https://github.com/AleksandarZeljic/z3 into smallFloats 2015-06-12 18:35:59 +02:00
Aleksandar Zeljic
421b3af8bd Minor additions and cleanup to the outdated code. 2015-06-12 18:35:32 +02:00
AleksandarZeljic
93fe080b64 Merge pull request #2 from wintersteiger/distinct_fix 
Distinct fix
 2015-06-12 14:18:06 +02:00
Christoph M. Wintersteiger
28fce367b1 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-06-12 13:00:06 +01:00