mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity
12735 commits 49 branches 53 tags 182 MiB
Commit graph

12735 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
cc26d49060 preparations for dealing with #2596 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-12 17:44:52 -07:00
Nikolaj Bjorner
5bdcc737ec remove function name 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-12 11:58:30 -07:00
Nikolaj Bjorner
ce06cd0d7a replace iterators by for, looking at @2596 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-12 10:08:30 -07:00
Nikolaj Bjorner
8d942ed26c sudo the install 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-12 04:13:27 -07:00
Nikolaj Bjorner
d0cf1458e3 fix #2630 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-12 04:12:06 -07:00
Nikolaj Bjorner
a1b690032a fix #2629 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-12 04:05:03 -07:00
Nikolaj Bjorner
a90529e3dc add path to python 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-11 13:44:28 -07:00
Nikolaj Bjorner
8c8a8cee7a add build step to generate doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-11 13:12:14 -07:00
Xiao Liang
a1814bf384 doc.fix(ast/rewriter/poly_rewriter_params.pyg): typo som-of-monomials -> sum-of-monomials 2019-10-11 13:06:46 -07:00
Nikolaj Bjorner
31a6788859 comment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-11 12:39:57 -07:00
Nikolaj Bjorner
a990e7f02e add visitor example, fix double conversion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-11 12:37:26 -07:00
Murphy Berzish
4fc64ab578 z3str3: check for and re-internalize str.in.re terms 2019-10-11 09:25:30 -07:00
Nikolaj Bjorner
58bc2bff0b fix typo introducing unsoundness 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-11 09:20:56 -07:00
Nikolaj Bjorner
ca7d066c4e fix #2624 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-10 19:20:02 -07:00
Nikolaj Bjorner
ecba7b3cde fix #1006 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-09 21:47:43 -07:00
Nikolaj Bjorner
fd1974845b fix assert-and-track semantics for smt2 logging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-09 21:16:41 -07:00
Nikolaj Bjorner
908254752b simplify 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-09 15:28:28 -07:00
Nikolaj Bjorner
26c34c9193 fix #2623 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-09 15:22:31 -07:00
Nikolaj Bjorner
6b7c0ce334 add feature description to RELEASE_NOTES 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-09 09:44:45 -07:00
Nikolaj Bjorner
d25c7e67eb increase timeout for LTO 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-09 09:29:54 -07:00
Nikolaj Bjorner
7a5ca96095 remove separate API for setting solver log, use parameter setting instead 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-09 09:01:17 -07:00
Nuno Lopes
bc50b6bea2 fix a few warnings 2019-10-09 14:09:33 +01:00
Nikolaj Bjorner
4192c81fae Merge branch 'master' of https://github.com/z3prover/z3 2019-10-08 19:56:27 -07:00
Nikolaj Bjorner
9eea5cb91a make smt2 log scope aware 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-08 18:15:59 -07:00
Nikolaj Bjorner
8bb2442a3f make smt2 log scope aware 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-08 18:14:32 -07:00
Nuno Lopes
4643fdaa4e remove a few str copies when throwing exceptions 2019-10-08 22:29:17 +01:00
Nikolaj Bjorner
01f085ab53 build C++ API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-08 14:19:54 -07:00
Nikolaj Bjorner
ce1f2e10c5 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-08 13:50:36 -07:00
Nikolaj Bjorner
16dc2788a7 compiler warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-08 12:43:17 -07:00
Nikolaj Bjorner
d716771541 unsafe pointer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-08 12:41:09 -07:00
Nikolaj Bjorner
228b952a50 add also get-consequences 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-08 12:28:45 -07:00
Nikolaj Bjorner
be33bb7b48 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-08 12:19:54 -07:00
Nikolaj Bjorner
6ddce9d5be adding SMT2 log file for solver interaction #867 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-08 11:46:26 -07:00
Nikolaj Bjorner
f6f3ca1507 adding SMT2 log file for solver interaction #867 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-08 11:44:47 -07:00
Nikolaj Bjorner
b6c13340bd bit-vector overflow/underflow operators exposed over C++ API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-08 10:12:18 -07:00
Nikolaj Bjorner
27765ee0f4 add stub for #2522 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-08 09:54:07 -07:00
Nikolaj Bjorner
7e174f50c1 use Z3_char_ptr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-08 09:14:10 -07:00
Nikolaj Bjorner
f4b803de95 expose mk_divides over API. Corresponds to a = b (mod m), #723 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-08 08:46:49 -07:00
Nikolaj Bjorner
f8469b65d1 enable default 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-07 20:53:44 -07:00
Nikolaj Bjorner
66b38eac9f add back dotnet after adding ;*.cs to path 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-07 20:07:55 -07:00
Nikolaj Bjorner
5fa177a650 remove --dotnet from Ubuntu due to 3.0 .Net core issues 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-07 17:41:39 -07:00
Nikolaj Bjorner
02e71c7d23 fix #2650, use datatype constructor producing smallest possible tree whenever possible 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-07 16:23:44 -07:00
Murphy Berzish
b0bf2f1792 z3str3: recognize two-argument re.loop 2019-10-07 15:07:10 -07:00
Nikolaj Bjorner
82c39f81a3 fix str.at rewrite 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-06 20:43:48 -07:00
Nikolaj Bjorner
9a516e5e41 fix str.at rewrite 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-06 20:43:02 -07:00
Nikolaj Bjorner
a8e7074ddd fix #2618 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-06 19:44:33 -07:00
Nikolaj Bjorner
7c10fb83a0 fix #2615 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-06 19:00:14 -07:00
Nikolaj Bjorner
f9b6e4e247 batch length enforcement 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-06 15:25:33 -07:00
Nikolaj Bjorner
b53f66bf2f avoid access to invalid m_length 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-06 10:58:25 -07:00
Nikolaj Bjorner
a1cb3a21f6 fix test build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-10-06 07:46:40 -07:00