mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity
4916 commits 23 branches 48 tags 157 MiB
Commit graph

4916 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner ce8862d415 fix bug in conflict clause generation in seq-branch-variable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-26 18:15:45 -08:00
Nuno Lopes 97d6098d00 bv_bounds: make may_simplify() more aggressive for the common case of a single comparison 
fix expr_has_bounds to handle cases like (bvadd (ite c t e) ...)
 2016-02-25 19:41:01 +00:00
Nuno Lopes 6563e458f0 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-25 16:53:45 +00:00
Nuno Lopes c693c990df bv_bounds: speedup up to 10x in larger formulas 
introduce a may_simplify() function to short-circuit evaluation of expression trees that are guaranteed to not be simplifiable
 2016-02-25 16:53:35 +00:00
Nuno Lopes d642d5fe4c API: add smt.logic parameter to enable setting the logic through the API 
currently only Z3_solver_set_params() is supported
logic has to be set before solver first usage or before solver reset
 2016-02-25 09:47:51 +00:00
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