mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-26 01:14:36 +00:00
Code Activity
5773 commits 45 branches 52 tags 177 MiB
Commit graph

4667 commits

Author SHA1 Message Date
Andres Nötzli
18b9cd1948 [Z3py] Fix documentation in FPSortRef 2016-03-01 18:56:20 -08:00
Christoph M. Wintersteiger
1e86175c03 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-01 21:21:32 +00:00
Christoph M. Wintersteiger
59e695f2be Bugfixes for FP numerals in Python 
Relates to #464, #470
 2016-03-01 21:21:25 +00:00
Nikolaj Bjorner
9b6963d112 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-01 09:48:53 -08:00
Nikolaj Bjorner
67397bf71e enable logic parameter update to configure SMTLIB logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-01 09:48:24 -08:00
Christoph M. Wintersteiger
0cb8193cdd logic fix 2016-03-01 17:42:33 +00:00
Nikolaj Bjorner
7f51ecab37 enable logic parameter update to configure SMTLIB logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-01 09:26:14 -08:00
Nikolaj Bjorner
31c58b0999 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-01 08:46:51 -08:00
Nikolaj Bjorner
908f09a9df update logic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-01 08:46:43 -08:00
Christoph M. Wintersteiger
c171170bed Fixed FP string input conversions. 
Fixes #464
 2016-03-01 15:31:33 +00:00
Christoph M. Wintersteiger
b6e43b6d7b Merge pull request #468 from 4tXJ7f/fix_fp_neq 
[Z3py] Consistent behavior of eq and ne for FP
 2016-03-01 14:07:28 +00:00
Nuno Lopes
62e46aacd9 bv_bounds: make may_simplify more precise to skip exprs with just 1 bound expr 
speedups up to 3x in selected benchmarks
 2016-03-01 11:31:08 +00:00
Nuno Lopes
33431ef922 fix build with gcc 2016-03-01 10:02:24 +00:00
Nuno Lopes
10ea36bfed fix build with gcc 2016-03-01 10:00:58 +00:00
Andres Notzli
91d6b2cbbb [Z3py] Consistent behavior of eq and ne for FP 
Before, x == y and x != y were returning inconsistent expressions (i.e.
`Not(x == y)` was not the same as `x != y`):

>>> x = FP('x', Float32())
>>> y = FP('y', Float32())
>>> (x == y).sexpr()
'(= x y)'
>>> (x != y).sexpr()
'(not (fp.eq x y))'

`=` does not have the same semantics as `fp.eq` (e.g. `fp.eq` of +0.0
and -0.0 is true while it is false for `=`).
This patch removes the __ne__ method from FPRef, so `x == y` and `x !=
y` use the inherited operations while fpEQ and fpNEQ can be used to
refer to `fp.eq(..)`/`Not(fp.eq(..))`.
 2016-03-01 00:21:10 -08:00
Nikolaj Bjorner
830a99aab4 finish minimization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-01 00:04:03 -08:00
Nikolaj Bjorner
4a15d756d7 uint64_t -> uint64 for cross platform 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-29 22:16:03 -08:00
Nikolaj Bjorner
b90bc4e685 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-29 21:15:44 -08:00
Nikolaj Bjorner
3b6eef05c9 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-29 20:23:29 -08:00
Nikolaj Bjorner
6cf76f2113 remove references to _DEBUG use Z3DEBUG instead 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-29 20:23:20 -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
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