mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity
6920 commits 23 branches 48 tags 156 MiB
Commit graph

6920 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner e48e7ef7be fix assertion, start addressing #1087 by using size_t 2017-06-20 14:38:58 -07:00
Nikolaj Bjorner 0ef14acf2e fix build break 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-20 14:25:56 -07:00
Nikolaj Bjorner 0fa6274a65 Fix bug #1079, integrality testing seems to have been wrong 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-20 14:18:43 -07:00
Christoph M. Wintersteiger 78e8e8b893 Kick CI 2017-06-20 18:06:18 +01:00
Christoph M. Wintersteiger 237e6dcd3f Kick CI 2017-06-20 17:21:24 +01:00
Christoph M. Wintersteiger ee2fc41626 Kick CI 2017-06-20 15:17:49 +01:00
Christoph M. Wintersteiger a0b25147d9 Fix for the fix for #1062. 2017-06-20 14:48:03 +01:00
Christoph M. Wintersteiger e9258731e4 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-06-20 14:39:26 +01:00
Christoph M. Wintersteiger ab21caf55f Reverted fix for quoted echo strings when smtlib2_compliant=false. Kindly reported by Armael Gueneau. Fixes #1062. 2017-06-20 14:39:22 +01:00
Christoph M. Wintersteiger 054e139c0d Whitespace 2017-06-20 14:37:26 +01:00
Christoph M. Wintersteiger 7b97688302 Whitespace, typo. 2017-06-20 14:36:40 +01:00
Nikolaj Bjorner 907899debe Merge branch 'master' of https://github.com/z3prover/z3 2017-06-19 18:24:45 -05:00
Nikolaj Bjorner f375016a11 disable tweak to seq until there are cycles to test further 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-19 18:23:27 -05:00
Nikolaj Bjorner 894c60bdf9 fix bug in qe-lite reported in #1086: bookkeeping of unconstrained variables only works for quantifier-free formulas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-19 18:22:30 -05:00
Christoph M. Wintersteiger b27a4a3593 Merge pull request #1084 from dennis714/master 
small typo
 2017-06-19 12:00:17 +01:00
Dennis Yurichev 345c0c796b Merge branch 'master' of github.com:dennis714/z3 2017-06-19 13:56:52 +03:00
Dennis Yurichev e547000bcf typo 2017-06-19 13:52:30 +03:00
Nikolaj Bjorner 02161f2ff7 revert internalize logic for re until debugged 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-15 21:13:25 -07:00
Nikolaj Bjorner e67572ffa6 address issues raised in #998 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-15 20:47:59 -07:00
Nikolaj Bjorner 5be3e959ab address issues raised in #998 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-15 20:46:47 -07:00
Nikolaj Bjorner d3320f8b81 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-14 21:48:19 -07:00
Nikolaj Bjorner f4214e1c71 Merge branch 'master' of https://github.com/z3prover/z3 2017-06-14 21:41:31 -07:00
Nikolaj Bjorner 8ac43c981a use less memory #1078 2017-06-14 21:41:24 -07:00
Christoph M. Wintersteiger d8a02bc040 Fixed AST translation functions in .NET and Java APIs. Fixes #1073. 2017-06-14 13:24:54 +01:00
Nikolaj Bjorner 2d1abf2795 Merge pull request #1076 from chaserhkj/default-pp-mode-api 
Fix Z3_PRINT_SMTLIB_FULL not working as expected
 2017-06-14 03:04:22 -07:00
KangJing Huang (Chaserhkj) e3f32ca3a8 Fix Z3_PRINT_SMTLIB_FULL not working as expected 2017-06-14 02:18:21 -04:00
Nikolaj Bjorner c980cfd783 add concat recognizer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-13 20:51:55 -07:00
Nikolaj Bjorner b978f78c21 add sequence recognizers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-13 20:35:35 -07:00
Nikolaj Bjorner 8b12cc0bdf fix build warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-13 19:58:55 -07:00
Nikolaj Bjorner c2acbc2957 port FuncDecl copy to dotnet, continuation of #1073 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-13 19:11:28 -07:00
Nikolaj Bjorner 7023af4528 Merge branch 'master' of https://github.com/z3prover/z3 2017-06-13 19:03:45 -07:00
Nikolaj Bjorner a59ee8032c fix unsoundness bug in axiomatization of str.at. #1067 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-13 19:02:59 -07:00
Nikolaj Bjorner 5066bd01f7 Merge pull request #1070 from delcypher/cmake_file_move 
[CMake] Move CMake files into their intended location
 2017-06-13 13:27:25 -07:00
Nikolaj Bjorner 90a38c9a35 Merge pull request #1073 from chaserhkj/funcdecl-translate-java 
Add translate method for FuncDecl in java api
 2017-06-13 13:27:12 -07:00
KangJing Huang (Chaserhkj) 5799947183 Fix docstrings for FuncDecl.translate 2017-06-13 02:37:41 -04:00
KangJing Huang (Chaserhkj) 3a692fe33c Add translate method for FuncDecl in java api 2017-06-13 00:37:02 -04:00
Nikolaj Bjorner 6bce173248 properly quote symbols #1061 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-12 18:35:02 -07:00
Dan Liew 814fcd6a17 [CMake] Remove documentation on "Bootstrapping". It is no longer 
relevant.
 2017-06-12 11:59:39 +01:00
Dan Liew 5c3b11f034 [CMake] Modify contrib/cmake/bootstrap.py to do nothing except 
print a warning.

Now that the CMake files have been moved into their intended location
it is no longer necessary for this script to exist.

However we do not want to break out-of-tree scripts that build Z3 using
CMake to suddenly break. So the script has been modified to do nothing
except print a warning.

Eventually we should remove this script.
 2017-06-12 11:59:39 +01:00
Dan Liew 5be503798f [CMake] Remove bootstrap check. Now that the CMake files are in 
their correct location we don't need it anymore.
 2017-06-12 11:59:38 +01: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
Nikolaj Bjorner f0fa439c48 escaping names in get-assignment #1061 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-11 17:17:47 -07:00
Nikolaj Bjorner f5b54f042c apply correction by ddcc #1069 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-11 11:40:39 -07:00
Nikolaj Bjorner 0700413f27 Merge pull request #1069 from delcypher/doxygen_z3_mk_solver 
[Doxygen] Rewrite documentation of `Z3_mk_solver()` and `Z3_mk_simple_solver()`
 2017-06-11 11:39:36 -07:00
Dan Liew c629dcc53f [Doxygen] Rewrite documentation of Z3_mk_solver() and 
`Z3_mk_simple_solver()` to try to make it clearer what the differences
are between these APIs.

This an attempt to address issues noted in #1035.
 2017-06-11 14:04:18 +01:00
Nikolaj Bjorner f44a3e1bbc print_core as a function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-10 10:18:07 -07:00
Nikolaj Bjorner 8acb37e734 revert change to 1065 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-06-10 09:45:18 -07:00
Nikolaj Bjorner 582a069c51 Merge branch 'master' of https://github.com/z3prover/z3 2017-06-10 09:31:02 -07:00