mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-27 09:49:23 +00:00
Code Activity
4961 commits 45 branches 52 tags 177 MiB
Commit graph

4961 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nuno Lopes
c1aa33339d bv_bounds: early exit in is_bound in case the expr is not boolean 
~2% speedup
 2016-02-25 09:32:10 +00:00
Nikolaj Bjorner
4c408165ab Merge branch 'master' of https://github.com/Z3Prover/z3 into HEAD 2016-02-24 08:55:28 -08:00
Nikolaj Bjorner
5679fb5d6b experimenting with alternative prefix encodings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-24 08:55:22 -08:00
Nikolaj Bjorner
4e7a867cd9 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-23 18:42:01 -08:00
Nikolaj Bjorner
d5383e2387 fix bug in definition of rewrite rule for replace, tighten constraints for tightest-prefix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-23 18:41:56 -08:00
Nikolaj Bjorner
8c68aed69e Merge branch 'master' of https://github.com/Z3Prover/z3 into HEAD 2016-02-23 08:11:09 -08:00
Nuno Lopes
64888b6b19 ctx_simplify: fix bug in simplification of or exprs 
this triggered when the or covers the whole space -> true
 2016-02-23 10:37:01 +00:00
Nuno Lopes
12458b1a84 remove dead code in qfufbv 2016-02-22 10:22:56 +00:00
Nikolaj Bjorner
63c138c08e add option to enable equality propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-21 11:16:13 -08:00
Nikolaj Bjorner
8c538fd3f0 setting partial equivalence priority lower so that it doesn't intefere with inlining (partial fix to the fact that inlining will remove such implicit relations). Using short-circuit negation in qe to avoid redundant double negations in intermediary results 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-21 10:31:13 -08:00
Nikolaj Bjorner
d4f41c0420 add goal context for simplifier, disable equality creation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-20 10:13:24 -08:00
Nikolaj Bjorner
c7abc11ce0 Merge branch 'master' of https://github.com/Z3Prover/z3 into HEAD 2016-02-19 08:23:32 -08:00
Nikolaj Bjorner
bff10527d1 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-19 08:23:27 -08:00
Nuno Lopes
7d3af70a63 ctx-simplify: fix mem leak of simplifier 2016-02-19 11:08:01 +00:00
Nuno Lopes
c618838ed9 bv_bounds: fix crash in push() when realloc happened 2016-02-19 11:06:22 +00:00
Nuno Lopes
121b3b60f3 bv_bounds/ctx_simplify: improve handling of (ite x a b) where (not x) is proved to be false 2016-02-19 09:42:42 +00:00
Nikolaj Bjorner
73f93dbadb Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-18 18:10:30 -08:00
Nikolaj Bjorner
a073b37ce3 fix bugs in seq solver: add relevancy and axiom 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-18 18:10:16 -08:00
Nikolaj Bjorner
5962ca2a62 seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-18 12:08:35 -08:00
Nuno Lopes
73da4dda07 add a bv rewrite pattern: 
(bvsle (- x (srem x c1)) c2) -> (bvsle x (+ c1 c2 - 1))
 2016-02-18 17:45:55 +00:00
Nuno Lopes
d32b4c71d1 [bv_bounds] introduce a tight bit in intervals to denote they are tight (over and under approx) 
use this to ensure certain transformations remain sound
 2016-02-18 15:53:11 +00:00
Nikolaj Bjorner
67958efed2 add fixed length heuristic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-17 21:20:39 -08:00
Nuno Lopes
8718c1c99f bv_bounds: simplify negated expressions as well 2016-02-17 19:14:02 +00:00
Nikolaj Bjorner
16ced7cda5 Merge pull request #453 from delcypher/fix_clause_allocator_bound_check 
Fix incorrect (off by one) bound check in clause_allocator
 2016-02-17 08:50:51 -08:00
Nuno Lopes
a4cfcd4550 bv_bounds: fix bug in interval intersection for non-wrapping disjoint values 2016-02-17 16:32:43 +00:00
Nuno Lopes
ac20d8bc11 bv_bounds: fix intersection of wrapped intervals 
e.g., [117, 115] /\ [115, 113] -> [115, 113]
 2016-02-17 15:41:12 +00:00
Nuno Lopes
98a92b9255 bv_bounds tactic: change representation to intervals 
Code by myself and Nikolaj Bjorner
 2016-02-17 10:02:40 +00:00
Dan Liew
6c966bba59 Fix incorrect (off by one) bound check. Also assert that we don't 
increment ``m_num_segments`` beyond the maximum value
(``c_max_segments``).

This is related to #436.

When doing an AddressSanitized build and running the ``c_example``
it looks like Z3 tries to create too many segments and index out of
bounds. Fixing the checks here causes them to fail which should help
us narrow down the problem.
 2016-02-16 14:04:21 +00:00
Nuno Lopes
c05a0dfa61 revert my previous attempt to simplify the destructor of ctx-simplify 
there can be assertions at level 0
 2016-02-16 13:10:17 +00:00
Christoph M. Wintersteiger
cb814ec65d Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-16 12:13:04 +00:00
Christoph M. Wintersteiger
3b92128ed8 Fixed old-style C variable declaration problem in interpolation C example. 2016-02-16 12:12:59 +00:00
Nuno Lopes
293566d464 ctx-simplify: simplify destructor 2016-02-16 09:53:04 +00:00
Nuno Lopes
98c5a5c86c move ctx_propagate_assertions class to .cpp file 2016-02-16 09:34:45 +00:00
Nikolaj Bjorner
07953342ac Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-15 17:29:54 -08:00
Nikolaj Bjorner
d3805bbdf6 fix location of level retrieval 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-15 17:29:46 -08:00
Nuno Lopes
96f6bf7028 ctx_simplify: simplify ite if then/else values become equal 2016-02-15 12:06:20 +00:00
Nikolaj Bjorner
8fc58e1ace propagate bounds implementation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-13 02:07:41 +00:00
Nikolaj Bjorner
d7186eede8 bv bounds tactic for Nuno 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-13 00:13:16 +00:00
Nikolaj Bjorner
e484fc365d add outline of bv bounds tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-12 22:57:47 +00:00
Nikolaj Bjorner
94be6fc776 remove passing suffixes into pdr_sym_mux, trying to isolate cause of issue #420 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-12 19:25:52 +00:00
Nikolaj Bjorner
660eff0b9e Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-12 18:59:05 +00:00
Nikolaj Bjorner
45999b254c hoist simplifier functionality out of context loop to allow plugging in other contextual simplification methods 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-12 18:58:37 +00:00
Christoph M. Wintersteiger
6319861e26 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-12 18:32:46 +00:00
Christoph M. Wintersteiger
da502a79dc Merge branch 'cheshire-codesmells' 2016-02-12 18:32:25 +00:00
Christoph M. Wintersteiger
f399fe5e1d resolved conflicts 2016-02-12 18:29:46 +00:00
Christoph M. Wintersteiger
3356f36b8f Merge pull request #446 from msullivan/arm-build 
Fix gcc build failure on ARM caused by including <emmintrin.h>
 2016-02-12 18:27:14 +00:00
Nikolaj Bjorner
e2dc7c6f64 add note that current re.complement is non-standard 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-12 17:12:43 +00:00
Nikolaj Bjorner
94453033b6 add partial support for complementation of regular expressions. Handles case of complementing character ranges 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-12 15:59:33 +00:00
Christoph M. Wintersteiger
9dbb8057ca Merge pull request #449 from kenmcmil/issue243 
fixed logging on return of Z3_compute_interpolant...
 2016-02-12 12:40:01 +00:00
Nikolaj Bjorner
8d61d36c3f add documentation methods to param_descrs, add C++ API and example for param_descrs. Issue #443 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-12 11:45:00 +00:00