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

6326 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
9746794962 Merge pull request #742 from angr/fix-tests 
Fix z3test for build rearrangement
 2016-09-21 18:41:57 -07:00
Andrew Dutcher
4801a27c2d Fix up z3test to a) exist and b) work 2016-09-21 17:18:10 -07:00
Nikolaj Bjorner
cf56da8482 add z3test to cmakelists.txt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-21 16:33:30 -07:00
Nikolaj Bjorner
ef0dd74c53 try copy instead of cp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-21 16:14:27 -07:00
Nikolaj Bjorner
14668b4d44 Merge pull request #735 from angr/new-build 
New packaging for and ability to distribute python bindings
 2016-09-21 15:55:22 -07:00
Andrew Dutcher
f451363a8f use copy instead of create_symlink when not on unix 2016-09-21 15:15:21 -07:00
Nikolaj Bjorner
516dba52ce Merge branch 'master' of https://github.com/Z3Prover/z3 2016-09-21 12:24:34 -07:00
Nikolaj Bjorner
527c5191a6 Add C++ functions for set operations per stackoverflow post, set relevancy = 2 for quantified maxsmt per example from Aaron Gember, fix conversion of default weights based on bug report from Patrick Trentin on maxsat. Annotating soft constraints with weight=0 caused the weight to be adjusted to 1 and therefore produce wrong results 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-21 12:24:24 -07:00
Nikolaj Bjorner
e8f4dd76c2 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-09-17 17:29:33 -07:00
Nikolaj Bjorner
77b245b3d8 fix proof production to avoid crash. Issue #733 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-17 17:29:19 -07:00
Nikolaj Bjorner
cda967ead2 guard verbose output by verbosity level for datalog command-line tool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-16 15:36:40 -07:00
Nikolaj Bjorner
7f29674842 add option to bypass compression of unbound tails, issue #738 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-16 14:56:10 -07:00
Christoph M. Wintersteiger
7a3308110c Merge pull request #722 from wintersteiger/i715 
x64 clause allocator bug fix
 2016-09-16 19:53:08 +01:00
Christoph M. Wintersteiger
d922ee6a08 Merge pull request #741 from wintersteiger/master 
Adding bv preprocessing techniques (was #729).
 2016-09-16 19:52:46 +01:00
Mikolas Janota
147c0f8152 Removing an unused method from bv_rewriter. 2016-09-16 19:44:37 +01:00
Mikolas Janota
ec47a1df50 Adding bv preprocessing techniques. 2016-09-16 19:44:37 +01:00
Christoph M. Wintersteiger
27ea7d8e9d style/formatting 2016-09-16 19:34:48 +01:00
Christoph M. Wintersteiger
b70cc47a9d x64 clause allocator fix for del_clause 2016-09-16 19:25:41 +01:00
Christoph M. Wintersteiger
5b1cb49973 x64 clause allocator bug fix 2016-09-16 19:25:41 +01:00
Andrew Dutcher
9e498536b6 Fix cmake build to work with the new system 2016-09-15 02:19:20 -07:00
Andrew Dutcher
02217d048b replace all non-portable filepath slashes with os.path.join 2016-09-14 14:19:10 -07:00
Nikolaj Bjorner
5290cd1ff5 Merge pull request #737 from MathieuRoger/patch-1 
Update socrates.py
 2016-09-14 12:42:36 -07:00
Mathieu Roger
9245e61775 Update socrates.py 2016-09-14 21:36:39 +02:00
Nikolaj Bjorner
e7f36a2d35 remove special characters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-14 10:32:17 -07:00
Nikolaj Bjorner
01eafdf68e Merge pull request #736 from MathieuRoger/patch-1 
Create socrates.py
 2016-09-14 10:29:21 -07:00
Mathieu Roger
a7e3a9df5a Create socrates.py 
Classical syllogism in Z3.
Many samples talks about integer, reals. Not much sample available on non integer things.
 2016-09-14 19:10:49 +02:00
Andrew Dutcher
02783d0bfb Minor tweaks to make things more reliable/less obnoxious 2016-09-14 01:49:37 -07:00
Andrew Dutcher
cb83c42100 Make python stuff live in a python directory in the build tree 2016-09-14 01:49:16 -07:00
Andrew Dutcher
704105306c FINISH IT 2016-09-14 01:40:01 -07:00
Andrew Dutcher
0bbd172af3 First steps to a sane python build 2016-09-14 01:37:04 -07:00
Andrew Dutcher
fa6cc19184 Moved python bindings into package 2016-09-14 01:33:07 -07:00
Nikolaj Bjorner
9f77759cd6 ensure that status is displayed in SMT-LIB2 compliant way. Issue #734 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-13 10:34:34 -07:00
Nikolaj Bjorner
5a86815f34 fix regression in seq-replace rewriting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-11 05:43:16 -07:00
Nikolaj Bjorner
1450594fc6 add patch to deal with bug exposed in issue #721 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-10 12:15:49 -07:00
Nikolaj Bjorner
0b57829bdd fix heisenbug, unintialized variable, issue #720 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-10 11:04:29 -07:00
Nikolaj Bjorner
cb140011bc add missing rewrite rule. Issue #731 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-10 09:42:36 -07:00
Nikolaj Bjorner
2f67665c7e ensure stoi axiom even when no value is present for argument. Issue #731 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-10 09:40:21 -07:00
Nikolaj Bjorner
d74e618565 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-09-08 13:59:22 -07:00
Nikolaj Bjorner
e485d1889c update replace semantics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-08 13:59:13 -07:00
Nikolaj Bjorner
76cf28d48b move from uint_set to hashtable over unsigned to save memory overhead in consequence generation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-08 13:34:59 -07:00
Nikolaj Bjorner
94b67412ec Merge branch 'master' of https://github.com/Z3Prover/z3 2016-09-07 11:59:06 -07:00
Nikolaj Bjorner
c5dd441947 fixes to consequence generation and cancellation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-07 11:50:26 -07:00
Nikolaj Bjorner
2d9dced1c7 fix spacing, cast to Bool 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-06 20:18:31 -07:00
Nikolaj Bjorner
520f8fc60e Merge pull request #730 from cttghc/patch-1 
Fix omission of Z3_model_has_interp in z3++.h
 2016-09-07 11:13:24 +08:00
cttghc
758266b952 Fix omission of Z3_model_has_interp in z3++.h 2016-09-06 18:32:41 -05:00
Nikolaj Bjorner
0e9758a211 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-09-06 14:39:19 -07:00
Nikolaj Bjorner
3b70dd6678 tuning by using get_consequences2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-09-06 14:29:40 +08:00
Christoph M. Wintersteiger
e7ae60893c Merge pull request #728 from AlexVonB/patch-1 
Fix VisualStudio 2010 compiler warning C4100
 2016-09-05 10:29:22 -04:00
AlexVonB
c6b0fc444c Fix VisualStudio 2010 compiler warning C4100 
When compiling with Visual Studio 2010 the buildlog warns of the following: `z3++.h: warning C4100: 'e' : unreferenced formal parameter` and `z3++.h: warning C4100: 'c' : unreferenced formal parameter`. This merge request removes this warning.
 2016-09-05 16:22:00 +02:00
Nikolaj Bjorner
424a8c69bd Merge branch 'master' of https://github.com/Z3Prover/z3 2016-09-02 03:05:23 -07:00