mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-17 01:46:39 +00:00
Code Activity
10362 commits 43 branches 51 tags 169 MiB
Commit graph

318 commits

Author SHA1 Message Date
Nikolaj Bjorner
5328454c77 const 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-15 08:37:23 -08:00
Nikolaj Bjorner
161c83795f remember inconsistent states when cloning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-15 08:34:55 -08:00
Nikolaj Bjorner
f238460597 neatify statistics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 16:45:04 -08:00
Nikolaj Bjorner
ed7cac8cc0 neatify logging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-14 16:42:13 -08:00
Nikolaj Bjorner
f835a3c2b2 revert assumption tracking choice in unit literals inferred from binary clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-12 11:08:35 -08:00
Nikolaj Bjorner
e4d6aa07dc use vectors instead of hash-tables in dimacs serialization to avoid hash-table contention 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-12 11:05:00 -08:00
Nikolaj Bjorner
3c96b51e97 lvl -> _lvl 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-12 00:40:36 -08:00
Nikolaj Bjorner
0b8dbf2854 fixing drat proofs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-12 00:30:21 -08:00
Nikolaj Bjorner
836f156d54 fix drat for units learned from binary clause resolution 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-12 00:12:20 -08:00
Nikolaj Bjorner
6e60926cc3 fix drat output for elim_eqs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-01-10 15:25:10 -08:00
Bruce Mitchener
44bc00f13d Fix typos. 2018-12-23 21:58:57 -05:00
Nikolaj Bjorner
b0b6394c6c fixing #1971 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-12-21 17:10:37 -08:00
Nikolaj Bjorner
ec36a9c495 fix user push/pop with ba constraints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-22 12:40:23 -08:00
Nikolaj Bjorner
4d0bc8c8b3 ignore propagation on units 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-11 15:10:44 -08:00
Nikolaj Bjorner
719bc5cd5d merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-30 17:23:31 -05:00
Nikolaj Bjorner
3c1c3d5987 fix #1908 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-30 14:15:29 -05:00
Nikolaj Bjorner
ccca063e54 Merge branch 'master' of https://github.com/Z3Prover/z3 into csp 2018-10-21 12:26:53 -07:00
Michał Janiszewski
cfd0486582 Catch exceptions by const-reference 
Exceptions caught by value incur needless cost in C++, most of them can
be caught by const-reference, especially as nearly none are actually
used. This could allow compiler generate a slightly more efficient code.
 2018-10-16 19:16:07 +02:00
Nikolaj Bjorner
5b51e69137 fix #1874 by removing nnf.skolemize option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-14 18:17:34 -07:00
Nikolaj Bjorner
e9d615e309 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-14 15:16:22 -07:00
Nikolaj Bjorner
f5fea8ae30 add parameter to force sat-cleaning on initialization and on simplification phases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-11 22:05:04 -07:00
Nikolaj Bjorner
46cdefac4d fix memory leak when cuber isn't run to completion. Found by Daniel Selsam 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-03 10:57:02 -07:00
Nikolaj Bjorner
9d0aa4d02d update empty cube case for sat/undef cases 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-01 20:22:02 -07:00
Bruce Mitchener
cdfc19a885 Use nullptr. 2018-10-02 09:11:19 +07:00
Nikolaj Bjorner
08c58ae614 make the unsat/sat verdicts from cubing produce empty clause and models respectively 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-10-01 15:52:22 -07:00
Nikolaj Bjorner
13abf5c6a6 n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-09-06 17:49:52 -07:00
Nikolaj Bjorner
fed977b492 fix #1782 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-08-02 10:08:16 -07:00
Nikolaj Bjorner
1918395f0e fix bug in sat-solver where frozen clauses get re-attached 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-07-05 12:19:03 -07:00
Nikolaj Bjorner
2e4fb8d356 work around VS2012 compiler bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-23 16:33:27 -07:00
Nikolaj Bjorner
278fd03f19 GLU -> GNU fix #1643 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-23 13:31:55 -07:00
Nikolaj Bjorner
87ae679db6 delay dereferencing justification 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-22 17:03:35 -07:00
Nikolaj Bjorner
dfeb4b5235 updated sat state 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-17 16:45:12 -07:00
Nikolaj Bjorner
2aedaf315a fix removal bug, tune all-interval usage 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-09 16:32:38 +01:00
Nikolaj Bjorner
75ae58f49e fix parenthesis 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-09 09:25:01 +01:00
Nikolaj Bjorner
41072e3125 use __builtin_prefetch for clang/gcc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-08 19:09:59 +01:00
Nikolaj Bjorner
13b54f379c fix ema 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-05 13:58:47 +02:00
Nikolaj Bjorner
43403fafcd adding ema 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-03 13:23:59 -07:00
Nikolaj Bjorner
fa93bc419d fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-01 10:53:36 -07:00
Nikolaj Bjorner
3de2feb84a fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-01 09:46:54 -07:00
Nikolaj Bjorner
e4d24fd2c3 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-05-01 09:39:19 -07:00
Nikolaj Bjorner
f525f43e43 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-30 09:30:43 -07:00
Nikolaj Bjorner
859c68c2ac merge with opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-30 08:27:54 -07:00
Nikolaj Bjorner
e940f53e9c n/a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-30 07:57:33 -07:00
Nikolaj Bjorner
2f025f52c0 fix local search initialization of units, encode offset in clauses 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-28 22:26:01 +02:00
Nikolaj Bjorner
563f337997 testing memory defragmentation, prefetch, delay ate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-27 17:59:03 +02:00
Nikolaj Bjorner
252fb4af6e add backtracking conquer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-14 15:34:33 -07:00
Nikolaj Bjorner
a954ab7d8d flip literals in ATEs produced using RI 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-04-06 08:38:01 -07:00
Nikolaj Bjorner
528dc8a3f8 disable bdd variable elimination 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-31 17:05:22 -07:00
Nikolaj Bjorner
55eb11d91b fix bug in blocked clause elimination: it was ignoring unit literals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-31 13:26:20 -07:00
Nikolaj Bjorner
aa2721517b model conversion and acce tracking 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-03-30 16:24:22 -07:00