mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity
4932 commits 23 branches 48 tags 156 MiB
Commit graph

4932 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 6f45970b6e Merge pull request #466 from 4tXJ7f/patch-1 
Fix documentation for floating-point comparisons
 2016-02-29 20:22:57 -08:00
Andres Nötzli c9269c1983 Fix documentation for floating-point comparisons 2016-02-29 19:12:14 -08:00
Nikolaj Bjorner 7ac5e67538 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-29 17:04:32 -08:00
Nikolaj Bjorner c6c84dd59a update documentation help to be inline with fpLT. Issue #465 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-29 17:04:26 -08:00
Nuno Lopes 43202572ee bv_bounds: switch from rational to uint64 
this limits the analysis to 64-bit BVs, but gives a speedup of up to one order of magnitude
 2016-02-29 17:23:54 +00:00
Nikolaj Bjorner 9efc7f4aea turn on model completion in validation code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-29 09:06:20 -08:00
Nikolaj Bjorner d89c39cbe2 apply t() 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-29 08:36:25 -08:00
Nuno Lopes 006dc147a8 fix build with gcc 5 2016-02-29 14:34:48 +00:00
Nikolaj Bjorner 7656adc483 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-28 17:05:52 -08:00
Nikolaj Bjorner df2d7e7628 add intersection using symbolic automata facility 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-28 17:05:12 -08:00
Nuno Lopes c1eb1cc3f2 bv_bounds: improve perf of push/pop 2016-02-28 20:07:39 +00:00
Nuno Lopes e7a360ca08 ctx_simplify: remove virtual push() method 2016-02-28 17:57:40 +00:00
Nuno Lopes 51687b2be7 bv_bounds: ensure (bvule x maxuint) is simplified to true 2016-02-28 10:56:48 +00:00
Nikolaj Bjorner 4cf72e23e6 fix python 3 compat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-27 09:58:45 -08:00
Nikolaj Bjorner e659845bc0 tune handling of contains, avoid redundant equalities, merge use of indexof.left/right with contains.left/right adding only least-ness constraints in the context of index 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-27 09:56:11 -08:00
Nikolaj Bjorner 1c630ccc9a Merge branch 'master' of https://github.com/Z3Prover/z3 into HEAD 2016-02-26 18:15:57 -08:00
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