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

4847 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Christoph M. Wintersteiger
6980fb3035 Bugfix for distinct of floats. 2015-06-12 12:58:19 +01:00
Christoph M. Wintersteiger
f84d6bf5bb Bugfix for QF_FP tactic 2015-06-12 12:58:07 +01:00
Aleksandar Zeljic
f45fcbe282 Added support for patching of models containing toIntegral, max, min. 2015-06-12 11:47:58 +02:00
Nikolaj Bjorner
ca31c979fe re-enable transformations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-11 12:00:21 -07:00
Nikolaj Bjorner
868b430b8b use scoped pointers instead of explicit deallocation (robust under exceptions) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-06-11 10:19:29 -07:00
Nikolaj Bjorner
94f8ecb06d Merge pull request #126 from ahorn/minimum 
Basic infrastructure for minimum aggregation function
 2015-06-11 09:38:39 -07:00
Christoph M. Wintersteiger
2c2a77174c Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-06-11 16:57:46 +01:00
Christoph M. Wintersteiger
31cb81111d Bugfix for fp.roundToIntegral 2015-06-11 16:56:36 +01:00
Alex Horn
4a2eef132d Merge branch 'unstable' of https://github.com/Z3Prover/z3 into minimum 2015-06-11 16:28:44 +01:00
Alex Horn
8c097044e8 Add basic compiler support for min aggregation function 
Signed-off-by: Alex Horn <t-alexh@microsoft.com>
 2015-06-11 16:23:26 +01:00
Alex Horn
c8a123b7dd Disable a few rule transformations 
For this prototype, we need to disable three rule transformations,
namely coi_filter, similarity_compressor, rule_inliner. But
disabling the inliner causes problems with the tracer in the
datalog interpreter. Since a new proprocessor is underway, we
skip the problematic trace outputs for now.

Signed-off-by: Alex Horn <t-alexh@microsoft.com>
 2015-06-11 16:16:47 +01:00
Christoph M. Wintersteiger
d3df473279 Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable 2015-06-11 12:53:31 +01:00