mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
11010 commits 49 branches 53 tags 182 MiB
Commit graph

11010 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
da95fd7d83 fixing get-arith-vars and extraction of private variables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-28 11:23:52 +08:00
Nikolaj Bjorner
2cc3918027 Merge branch 'master' of https://github.com/z3prover/z3 2018-12-28 09:38:31 +08:00
Nikolaj Bjorner
8829fa96de change projection function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-28 09:38:17 +08:00
Nikolaj Bjorner
d879e2732a
Merge pull request #2050 from waywardmonkeys/allow-disabling-invoking-debugger 
If NO_Z3_DEBUGGER, also drop defining invoke_gdb.
 2018-12-27 17:23:31 -08:00
Bruce Mitchener
947687d350 Allow emscripten builds. 2018-12-27 09:24:12 -05:00
Bruce Mitchener
877df0f1cc If NO_Z3_DEBUGGER, also drop defining invoke_gdb. 2018-12-27 09:21:45 -05:00
Nikolaj Bjorner
8b3abe120c Merge branch 'master' of https://github.com/z3prover/z3 2018-12-26 21:04:44 +08:00
Nikolaj Bjorner
076cfa5813 working on revising project0 to project 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-26 21:04:35 +08:00
Nikolaj Bjorner
04fb8a45eb
Merge pull request #2049 from waywardmonkeys/fix-typos 
Fix typos.
 2018-12-24 16:31:58 -08:00
Bruce Mitchener
44bc00f13d Fix typos. 2018-12-23 21:58:57 -05:00
Nikolaj Bjorner
9379ec3a68 add back pre_visit, which does get called from rewriter_def/rewriter.h 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-21 18:52:09 -08:00
Nikolaj Bjorner
99cc4747c5 fixing #1971 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-21 17:21:04 -08:00
Nikolaj Bjorner
95db37d105 Merge branch 'master' of https://github.com/z3prover/z3 2018-12-21 17:10:41 -08:00
Nikolaj Bjorner
b0b6394c6c fixing #1971 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-21 17:10:37 -08:00
Nuno Lopes
3104291b80 spread a few anonymous namespaces and remove some m_imp idioms 2018-12-21 23:02:15 +00:00
Nuno Lopes
178e5b31e8 spread a few anonymous namespaces and remove some m_imp idioms 2018-12-21 22:49:06 +00:00
Nuno Lopes
52f960a7c8 elim_uncnstr_tactic: remove m_imp idiom to reduce mem alloc 2018-12-21 19:48:18 +00:00
Nikolaj Bjorner
e1dc553228 inc version 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-20 13:15:50 -08:00
Nikolaj Bjorner
d6df51951f release notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-20 10:32:36 -08:00
Nikolaj Bjorner
a63d1b1848 update doctest 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-18 11:57:20 -08:00
Nikolaj Bjorner
35e8decdb1 for #2039 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-18 11:27:04 -08:00
Nikolaj Bjorner
b6bf299b8b update upolynmial test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-17 17:41:50 -08:00
Nikolaj Bjorner
360d6f963e reduce output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-17 17:05:48 -08:00
Nikolaj Bjorner
bd96eaff47 axiomatize pb-eq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-17 08:26:59 -08:00
Nikolaj Bjorner
f4d03edf22 remove unreachable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-16 15:54:30 -08:00
Nikolaj Bjorner
2dcf36e96c fix #2044 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-16 15:32:38 -08:00
Nikolaj Bjorner
82a89120b0 fix #2042 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-16 15:26:40 -08:00
Nikolaj Bjorner
f56749a241 fix #2041, fix #2043 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-16 15:18:49 -08:00
Nikolaj Bjorner
58b9fc437d add sin/cos axiom regardless of whether sin/cos can be eliminated. fix #2037 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-13 16:09:08 -06:00
Nikolaj Bjorner
c5ada288c2 updated script 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-12 12:46:28 -08:00
Nikolaj Bjorner
8d23ad2f7e fix generation of assembly-sign-input to take escape sequences and absolute paths 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-12 10:14:38 -08:00
Nikolaj Bjorner
db3e5ce070
Merge pull request #1997 from waywardmonkeys/change-64-bit-configuration-strategy 
Change how 64 bit builds are detected.
 2018-12-12 09:55:13 -08:00
Nikolaj Bjorner
83f64ad604 Merge branch 'master' of https://github.com/z3prover/z3 2018-12-11 20:27:37 -08:00
Nikolaj Bjorner
b3d0ed6143 fix #2035 regression. correct axiom is |extract(s,i,l)| <= l or l < 0, but it is subsumed by encoding of extract, so new axiom is not useful 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-11 20:27:28 -08:00
Nikolaj Bjorner
02f01fcef1 adding esrp feature 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-11 17:31:09 -08:00
Nikolaj Bjorner
93c59ffbd9 update script to sign assembly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-11 15:48:33 -08:00
Nikolaj Bjorner
c1b03e8ca6 Merge branch 'master' of https://github.com/z3prover/z3 2018-12-11 09:38:44 -08:00
Nikolaj Bjorner
bfcea7a819 perf improvements by reordering variable branching #1676 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-11 09:38:36 -08:00
Nikolaj Bjorner
271e86020a Merge branch 'master' of https://github.com/z3prover/z3 2018-12-11 09:35:34 -08:00
Nikolaj Bjorner
045fef35ed fix build break 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-11 09:35:27 -08:00
Nikolaj Bjorner
021c5315a7
Merge pull request #2034 from Bronsa/patch-1 
Change error message from "internal failure" to "Object allocation failed"
 2018-12-11 09:32:32 -08:00
Nikolaj Bjorner
a3f9e3168d simplify ~context #1948 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-11 09:29:59 -08:00
Nikolaj Bjorner
796689f708 #1948 remove memory allocation in nlsat::solver::~solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-11 09:08:53 -08:00
Nicola Mometto
06fc94818f
Change error message from "internal failure" to "Object allocation failed" 
For consistency with ad49c3269a and Java/dotNet APIs
 2018-12-11 12:09:22 +00:00
Nikolaj Bjorner
da5486563d Merge branch 'master' of https://github.com/z3prover/z3 2018-12-10 18:38:15 -08:00
Nikolaj Bjorner
092c25d596 fix #2007 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-10 18:37:30 -08:00
Nikolaj Bjorner
b40c2b2926 fix #876 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-10 14:11:00 -08:00
nilsbecker
6d2cf4f464 smt-like logging of theory specific meaning of constants 2018-12-10 22:49:08 +01:00
Nikolaj Bjorner
68ace83893 remove enable trace 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-10 07:34:56 -08:00
Nikolaj Bjorner
f2a7bcaf5d remove prints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-09 14:38:45 -08:00