mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-08 00:41:56 +00:00
Code Activity
7885 commits 29 branches 52 tags 172 MiB
Commit graph

1208 commits

Author SHA1 Message Date
Nikolaj Bjorner
7b47b0380e update Ackerman reduction for division to make Andre and Nathan happy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-10 23:43:21 +02:00
Nikolaj Bjorner
082936bca6 enable overloading resolution on define-fun declarations, fix #1199 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-08 09:21:06 +02:00
Nikolaj Bjorner
2f466b6585 Merge branch 'master' of https://github.com/z3prover/z3 2017-08-03 13:56:04 -07:00
Nikolaj Bjorner
91ee52e549 fix #1195 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-03 13:53:38 -07:00
Nikolaj Bjorner
ffaaa1ff34 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-08-03 08:50:17 -07:00
Nikolaj Bjorner
8844112418 update header include generation to use relative paths #534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-03 08:50:04 -07:00
Nikolaj Bjorner
ce3fd22f3b use common idioms for factor-equivalence code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 21:07:20 -07:00
Arie Gurfinkel
88a35119b9 moved obj_equiv_class to ast 2017-08-01 19:24:50 -04:00
Nikolaj Bjorner
2b82fd5d0c updated include directives 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-08-01 10:51:47 -07:00
Christoph M. Wintersteiger
e8cdc34219 Debug fix in fpa2bv converter. Relates to #872. 2017-07-31 22:34:58 +01:00
Christoph M. Wintersteiger
6a2fa91818 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-31 22:12:37 +01:00
Christoph M. Wintersteiger
9601761a6f Added missing float conversion in fpa2bv converter. Relates to #1178. 2017-07-31 22:12:15 +01:00
Nikolaj Bjorner
013127e947 fix build break based on ambiguous path resolution 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 14:01:39 -07:00
Nikolaj Bjorner
063b6e9ea5 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-31 13:24:57 -07:00
Nikolaj Bjorner
b19f94ae5b make include paths uniformly use path relative to src. #534 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-31 13:24:11 -07:00
Christoph M. Wintersteiger
bbf0ebcb74 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-31 20:18:53 +01:00
Christoph M. Wintersteiger
507356c7bf Fixed bug in fpa2bv converter. Fixes #1178. 2017-07-31 20:18:39 +01:00
Christoph M. Wintersteiger
52cf80d637 Simplified bit-vector bounds in fp.rem. Relates to #872. 2017-07-31 19:53:55 +01:00
Christoph M. Wintersteiger
ecfd241e19 Injected 3 missing bits of precision into fp.rem. Relates to #872. 2017-07-31 19:53:44 +01:00
Arie Gurfinkel
7670b49ada mark mk_true() and mk_false() const 2017-07-31 14:14:35 -04:00
Arie Gurfinkel
15451ae858 extra flags to control quant_hoist 2017-07-31 14:13:45 -04:00
Arie Gurfinkel
be1df279ec make proof_checker less verbose 2017-07-31 14:11:07 -04:00
Christoph M. Wintersteiger
a59907170d Fixed renormalization in fp.mul. Relates to #872. 2017-07-31 18:34:46 +01:00
Christoph M. Wintersteiger
175f042db8 Fixed renormalization in fp.fma. Relates to #872. 2017-07-28 23:01:01 +01:00
Christoph M. Wintersteiger
a30c343d7a Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-28 20:24:35 +01:00
Christoph M. Wintersteiger
0610392a05 Bugfix for fp.fma. Fixes #872. 2017-07-28 20:16:13 +01:00
Nikolaj Bjorner
31d6abcfe8 remove arity check 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-28 08:55:41 -07:00
Nikolaj Bjorner
e9b9a29339 revert first fix for #1173, replace by handling single arity chainables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-28 08:44:19 -07:00
Nikolaj Bjorner
64233034cc fix #1173 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-28 08:26:52 -07:00
Christoph M. Wintersteiger
33ebdc8adc Cleaned up mpf rounder. Rewrote mpf fma. Relates to #872. 2017-07-27 23:08:35 +01:00
Christoph M. Wintersteiger
f1c0ac72e7 Fix for fp.fma encoding. Relates to #872. 2017-07-25 20:29:10 +01:00
Nikolaj Bjorner
9d6be286d0 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-07-25 10:18:43 -07:00
Nikolaj Bjorner
70f6280bf1 fix regression reported in #1159 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-25 10:18:21 -07:00
Nikolaj Bjorner
741f940119 Merge pull request #1158 from facanferff/master 
pretty printer: fix typo with ReSort sort name
 2017-07-24 21:19:18 -07:00
Nikolaj Bjorner
ae5e39a8b8 Merge branch 'master' of https://github.com/z3prover/z3 2017-07-24 09:18:27 -07:00
Nikolaj Bjorner
a0a8bc2a62 fixes to #1155 and partial introduction of SMTLIB 2.6 datatype format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-24 09:12:43 -07:00
Fábio Ferreira
2e2782577b pretty printer: fix typo with ReSort sort name 2017-07-23 02:32:35 +01:00
Christoph M. Wintersteiger
0f1583309d Bugfix for fp.fma. One piece of puzzle #872. 2017-07-21 21:12:45 +01:00
Dan Liew
89c8f1722f Fix typo that prevented uses of bvsmod_i being parsed. 2017-07-12 12:53:10 +01:00
Nikolaj Bjorner
2af08a378d avoid complaining about division by 0 as unhandled in theory-lra 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-08 18:21:47 -07:00
Nikolaj Bjorner
d66db280a8 fix compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-04 13:43:32 -07:00
Nikolaj Bjorner
08524a2d90 cleanup for warning message 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-07-01 11:47:17 -07:00
Nikolaj Bjorner
244cbc2638 ensure that auxiliary PB booleans are recognized during rewriting. Fixes segementation fault #1113, but does not address performance issues with quantifiers and optimization combinations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-26 10:04:50 -07:00
Arie Gurfinkel
9874db7458 [CMake] typos in cmake 2017-06-23 09:37:49 -04:00
Nikolaj Bjorner
1fee5fd94e Merge pull request #1094 from delcypher/cmake_fix_generated_cpp_deps 
[WIP][CMake] Fix broken regeneration of some .cpp files
 2017-06-21 17:47:41 -07:00
Dan Liew
6f48a145aa [CMake] Fix dependencies for generating gparams_register_modules.cpp. 
Previously CMake was not aware of which headers files the generation
of `gparams_register_modules.cpp` depended on. Consequently this could result
in broken incremental builds if

* Existing headers that declared module description/parameters change.
* New headers are added that declare module description/parameters.
* `.pyg` files that generate header files that declare module
  description/parameters change

Now the `z3_add_component()` CMake function has been modifed so that

* All header files that are generated from `.pyg` files are added as
dependencies and are scanned from module description/parameter
declarations. This implicit dependency of `gparams_register_modules.cpp`
depending on other generated header files seems unnecessary complex. We
should revisit this design decision once the Python/Makefile build
system is deprecated.

* The function now takes an optional `EXTRA_REGISTER_MODULE_HEADERS`
argument which allows the headers that declare module
description/paramters to be explicitly listed.

With this information CMake will now regenerate `gparams_register_modules.cpp`
correctly.

This required the `mk_gparams_register_modules_internal()` function to be
changed to take a list of header files rather than a list of component
source directories. The two consumers (CMake and Python/Makefile build
systems) of this function have been modified to work with this change.

This partially fixes #1030.
 2017-06-21 23:56:46 +01:00
Nikolaj Bjorner
b516f22549 refine test for non-fd to be more inclusive while addressing #1092 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-21 08:01:03 -07:00
Arie Gurfinkel
6eced8836d expose iterators in expr_map 2017-06-20 21:07:38 -04:00
Arie Gurfinkel
e9100854b9 ensure that variable names are properly quoted 2017-06-20 21:07:38 -04:00
Arie Gurfinkel
69a3e984aa add is_hypothesis() method 2017-06-20 21:07:38 -04:00