mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-17 14:25:35 +00:00
Code Activity
7076 commits 23 branches 48 tags 157 MiB
Commit graph

985 commits

Author SHA1 Message Date
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
Dan Liew 4b517b96df [CMake] Move CMake files into their intended location so the 
`contrib/cmake/bootstrap.py` script no longer needs to be executed.

The previous location of the CMake files was a compromise proposed
by @agurfinkel in #461. While this has served us well (allowing progress
to be made) over time limitations of this approach have appeared.

The main problem is that doing many git operations (e.g. pull, rebase)
means the CMake files don't get updated unless the user remembers to
run the script. This can lead to broken and confusing build system
behaviour.

This commit only does the file moving and necessary changes to
`.gitignore`. Other changes will be done in subsequent commits.
 2017-06-12 11:59:00 +01:00
Christoph M. Wintersteiger 596652ed36 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-05-31 18:35:52 +01:00
Christoph M. Wintersteiger a7d5bb7b36 Tabs 2017-05-31 12:18:00 +01:00
Nikolaj Bjorner 2de80b5ce9 add pb built in ops for logic ALL #1045 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-29 10:08:50 -07:00
Nikolaj Bjorner edb164587f get rid of a simplifier dependency 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-23 10:12:32 -07:00
Nikolaj Bjorner 622d8c951c remove redundant data-type function declarations from pretty-printed output. #1034 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-22 14:40:42 -07:00
Nikolaj Bjorner 79a8e9aab0 fix build break #1029 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-18 12:09:51 -07:00
Nikolaj Bjorner ceec81de0b simplify code, issue #1028 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-16 08:32:08 -07:00
Nikolaj Bjorner 7fab670719 fix regression, issue #1028 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-16 08:21:32 -07:00
Nikolaj Bjorner d1cfc53495 fix for #1015 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-10 19:40:00 -07:00
Nikolaj Bjorner 911b24784a merge LRA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-09 10:46:11 -07:00
Murphy Berzish 8029b6b889 Merge branch 'upstream-master' into develop 2017-05-05 14:44:29 -04:00
Nikolaj Bjorner 7e1fae418a fix #1005, disable expansion of regular expression range to union as it degrades performance significantly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-05 10:59:47 -04:00
Murphy Berzish ab4fbe40b6 cleanup 2017-05-03 17:45:56 -04:00
Murphy Berzish 0862949e66 Merge branch 'upstream-master' into develop 
Conflicts:
	src/smt/params/smt_params.cpp
	src/smt/params/smt_params.h
	src/smt/smt_context.cpp
	src/smt/smt_context.h
 2017-05-01 21:33:23 -04:00
Nikolaj Bjorner d14f2af5ae deal with subtraction that manages to sneak in. Issue #996 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-05-01 15:22:06 -07:00
Murphy Berzish 88147f7047 theory_str static features and cmd_context 2017-04-28 14:14:28 -04:00
Murphy Berzish d51ebac10a remove references to str_fid 2017-04-28 14:01:44 -04:00
Murphy Berzish f1cee803e8 fixup 2017-04-28 13:44:48 -04:00
Murphy Berzish d2ae94935e Merge branch 'upstream-master' into develop 
Conflicts:
	src/ast/rewriter/seq_rewriter.cpp
	src/ast/seq_decl_plugin.h
 2017-04-28 13:43:14 -04:00
Murphy Berzish 05958193ab revert change to String sort declaration 2017-04-27 22:30:02 -04:00
Murphy Berzish 12dd6d786b remove redundant is_seq() check 2017-04-27 21:24:40 -04:00
Murphy Berzish 7811a91bad fix is_string_term() 2017-04-27 13:59:02 -04:00