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

5089 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
701f32471e hardening model checker code against cancellations' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-21 15:04:20 -07:00
Nikolaj Bjorner
3dc2028925 adding min/max 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-21 09:20:57 -07:00
Nikolaj Bjorner
680c28d083 remove nnf conversion which breaks NRA property 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-20 16:34:04 -07:00
Nikolaj Bjorner
1a5449c3d4 enable new NRA solver for nra benchmarks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-20 12:35:29 -07:00
Nikolaj Bjorner
73e29c6ee6 fix regression warning on invalid case split strategy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-20 10:20:43 -07:00
Nikolaj Bjorner
92b5aac12a adjusting new tactics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-20 10:13:23 -07:00
Nikolaj Bjorner
b66fc4e355 Merge pull request #523 from delcypher/fix_no_kind_namespace 
Fix gcc build broken by f175f864ec.
 2016-03-20 10:12:14 -07:00
Dan Liew
971fd59fbb Fix gcc build broken by f175f864ec. 
C++ enums (unless they are class enums) don't define their own
namespace.
 2016-03-20 10:18:59 +00:00
Nikolaj Bjorner
f0bdcbb3db expose qsat tactic to default tactics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 18:40:59 -07:00
Christoph M. Wintersteiger
fe201013e0 Merge pull request #521 from delcypher/cmake_python_custom_install_location 
[CMake] Add CMAKE_INSTALL_PYTHON_PKG_DIR option to control where python
 2016-03-20 00:57:31 +00:00
Nikolaj Bjorner
67dc5ce2b5 fix cmake issues 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 15:51:31 -07:00
Nikolaj Bjorner
20bbdfe31a moving remaining qsat functionality over 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 15:35:26 -07:00
Nikolaj Bjorner
296addf246 add new files to cmakelists 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 12:44:44 -07:00
Nikolaj Bjorner
d614fedde2 more merges with qsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 12:41:41 -07:00
Nikolaj Bjorner
76d637626a include more qsat features 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 12:30:24 -07:00
Nikolaj Bjorner
c4472ce717 include more qsat features 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 12:29:23 -07:00
Nikolaj Bjorner
f175f864ec merge useful utilities from qsat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-19 12:01:44 -07:00
Dan Liew
8746cc4a14 [CMake] Add CMAKE_INSTALL_PYTHON_PKG_DIR option to control where python 
bindings are installed.
 2016-03-18 22:18:51 +00:00
Nikolaj Bjorner
f951372f03 fix regression in internalizing bit-vectors, reported by Mikolas Janota 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-18 13:54:42 -07:00
Nikolaj Bjorner
b0f65335ab update copyright year 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-17 13:07:40 -07:00
Nikolaj Bjorner
ab82fee398 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-17 13:06:21 -07:00
Christoph M. Wintersteiger
94054593a4 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-17 17:52:32 +00:00
Christoph M. Wintersteiger
cc04fdbd70 Added eager ackermannization to QF_FP, so that small numbers of unspecified operators are eliminated upfront. 2016-03-17 17:52:26 +00:00
Nuno Lopes
f5c4800eec reduce-args: last fix for may_be_unique to support quantified variables in arbitrary exprs 2016-03-17 15:29:48 +00:00
Nuno Lopes
facb421398 reduce-args: fix unsoundness 2: f(v + 2), where b is quantified 2016-03-17 13:27:07 +00:00
Nuno Lopes
aed4619066 reduce-args: fixed unsoundness introduced in my previous commit 
skip an UF arg if it's quantified
e.g. forall a . f(a, b) -> f(b) (but not f)
 2016-03-17 13:14:43 +00:00
Christoph M. Wintersteiger
c8af48d7ef Bugfix for bvurem0 model evaluation (+1 rewriting step) 2016-03-17 13:09:52 +00:00
Nikolaj Bjorner
22cae143b1 Merge pull request #517 from yaqwsx/expr_values_to_int 
Add methods for obtaining numeral values in C++ API
 2016-03-16 20:43:39 -04:00
Nikolaj Bjorner
3755035d65 Merge pull request #519 from 4tXJ7f/patch-1 
[Z3py] Fix error in FPRef.__neg__()
 2016-03-16 20:41:36 -04:00
Andres Nötzli
34da0a32b9 [Z3py] Fix error in FPRef.__neg__() 
`FPRef.__neg__()` did not work previously because it tried to construct an FPRef from an FPRef (`fpNeg()` already returns an FPRef).
 2016-03-16 17:12:45 -07:00
Christoph M. Wintersteiger
6b2d84b2be Fixed model evaluation/simplification for to_ieee_bv. 2016-03-16 17:46:52 +00:00
Christoph M. Wintersteiger
7ec70c1686 bug fixes for unspecified FP results 2016-03-16 16:57:20 +00:00
Christoph M. Wintersteiger
db6b9faabc Bugfix for FPA rewriter. 2016-03-16 16:35:45 +00:00
Christoph M. Wintersteiger
778c7fcc64 Bugfix for model evaluator and internal, uninterpreted FPA functions. 
Fixes #518
 2016-03-16 16:17:08 +00:00
Christoph M. Wintersteiger
cdc8e1303a Bugfix for fp.to_*_unspecified. 
Fixes #507
 2016-03-16 16:16:29 +00:00
Jan Mrázek
57265f6eb1 Add methods for obtaining numeral values in C++ API 2016-03-16 00:18:49 +01:00
Christoph M. Wintersteiger
99d7a47f82 Bugfixes for unspecified results from fp.to_* (models are still incomplete). 
Relates to #507
 2016-03-15 21:45:54 +00:00
Christoph M. Wintersteiger
3101d281e4 Removed unused variable 2016-03-15 15:12:54 +00:00
Christoph M. Wintersteiger
371573cbff More implementation of fp.to_ieee_bv for unspecified input/output 
Relates to #507
 2016-03-15 15:11:37 +00:00
Christoph M. Wintersteiger
a9df4a208f More bugfixes for fp.to_ieee_bv for unspecified input/output. 
Relates to #507
 2016-03-15 14:58:55 +00:00
Christoph M. Wintersteiger
ce64999ee2 More bugfixes for fp.to_ieee_bv for unspecified input/output 2016-03-15 14:50:59 +00:00
Christoph M. Wintersteiger
176782d62b Bugfix for fp.to_ieee_bv for unspecified input/output. 2016-03-15 14:38:11 +00:00
Christoph M. Wintersteiger
5463167a84 Bugfix for fp.rem (denormal numbers) 
Fixes #508.
 2016-03-14 15:52:09 +00:00
Christoph M. Wintersteiger
45b868e90b Merge pull request #513 from delcypher/fix_exec 
Fix #510
 2016-03-14 12:49:16 +00:00
Christoph M. Wintersteiger
139920e68d Merge pull request #516 from delcypher/readme_tweak 
Fix omission of CMake build in README.md
 2016-03-14 12:48:41 +00:00
Dan Liew
474ce6645a Fix omission of CMake build in README.md 2016-03-14 08:27:46 +00:00
Dan Liew
4814555c46 Fix inconsistent emission of `gparams_register_modules.cpp`, 
``install_tactics.cpp`` and ``mem_initialiszer.cpp`` files between
the CMake and Python build systems.

The problem was that the generated files were

* Senstive to the order component directories were traversed
* For CMake there are two directories (a source and build directory)
  for every component rather than a single directory like the
  Python build system has.

To fix this a new function ``sorted_headers_by_component()`` has been
added which defines a order that is consistent between both build
systems. This function is then used on lists of paths to discovered
header files.
 2016-03-13 23:00:40 +00:00
Nikolaj Bjorner
55956df8d8 remove critical sections that are now redundant due to different cancellation model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-13 12:10:14 -04:00
Nikolaj Bjorner
3dfc0a93f6 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-13 12:09:25 -04:00
Dan Liew
75af362b25 Fix inconsistent emission of `z3consts.py`. The ordering of emitted 
enum values is not consistent between python 2 or 3. The root cause
of the problem was a dictionary's keys being iterated over which has
no defined order.

This has been fixed by iterating over the dictionary's items and
ordering by values.  We could order by key rather than the values but
seeing as these represent an enum, ordering by value makes more sense.
 2016-03-12 23:27:26 +00:00