mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
9543 commits 49 branches 53 tags 182 MiB
Commit graph

7935 commits

Author SHA1 Message Date
Nuno Lopes
f5c4800eec reduce-args: last fix for may_be_unique to support quantified variables in arbitrary exprs 2016-03-17 15:29:48 +00:00
Nuno Lopes
facb421398 reduce-args: fix unsoundness 2: f(v + 2), where b is quantified 2016-03-17 13:27:07 +00:00
Nuno Lopes
aed4619066 reduce-args: fixed unsoundness introduced in my previous commit 
skip an UF arg if it's quantified
e.g. forall a . f(a, b) -> f(b) (but not f)
 2016-03-17 13:14:43 +00:00
Christoph M. Wintersteiger
c8af48d7ef Bugfix for bvurem0 model evaluation (+1 rewriting step) 2016-03-17 13:09:52 +00:00
Nikolaj Bjorner
22cae143b1 Merge pull request #517 from yaqwsx/expr_values_to_int 
Add methods for obtaining numeral values in C++ API
 2016-03-16 20:43:39 -04:00
Andres Nötzli
34da0a32b9 [Z3py] Fix error in FPRef.__neg__() 
`FPRef.__neg__()` did not work previously because it tried to construct an FPRef from an FPRef (`fpNeg()` already returns an FPRef).
 2016-03-16 17:12:45 -07:00
Christoph M. Wintersteiger
6b2d84b2be Fixed model evaluation/simplification for to_ieee_bv. 2016-03-16 17:46:52 +00:00
Christoph M. Wintersteiger
7ec70c1686 bug fixes for unspecified FP results 2016-03-16 16:57:20 +00:00
Christoph M. Wintersteiger
db6b9faabc Bugfix for FPA rewriter. 2016-03-16 16:35:45 +00:00
Christoph M. Wintersteiger
778c7fcc64 Bugfix for model evaluator and internal, uninterpreted FPA functions. 
Fixes #518
 2016-03-16 16:17:08 +00:00
Christoph M. Wintersteiger
cdc8e1303a Bugfix for fp.to_*_unspecified. 
Fixes #507
 2016-03-16 16:16:29 +00:00
Jan Mrázek
57265f6eb1 Add methods for obtaining numeral values in C++ API 2016-03-16 00:18:49 +01:00
Christoph M. Wintersteiger
99d7a47f82 Bugfixes for unspecified results from fp.to_* (models are still incomplete). 
Relates to #507
 2016-03-15 21:45:54 +00:00
Christoph M. Wintersteiger
3101d281e4 Removed unused variable 2016-03-15 15:12:54 +00:00
Christoph M. Wintersteiger
371573cbff More implementation of fp.to_ieee_bv for unspecified input/output 
Relates to #507
 2016-03-15 15:11:37 +00:00
Christoph M. Wintersteiger
a9df4a208f More bugfixes for fp.to_ieee_bv for unspecified input/output. 
Relates to #507
 2016-03-15 14:58:55 +00:00
Christoph M. Wintersteiger
ce64999ee2 More bugfixes for fp.to_ieee_bv for unspecified input/output 2016-03-15 14:50:59 +00:00
Christoph M. Wintersteiger
176782d62b Bugfix for fp.to_ieee_bv for unspecified input/output. 2016-03-15 14:38:11 +00:00
Christoph M. Wintersteiger
5463167a84 Bugfix for fp.rem (denormal numbers) 
Fixes #508.
 2016-03-14 15:52:09 +00:00
Nikolaj Bjorner
55956df8d8 remove critical sections that are now redundant due to different cancellation model 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-13 12:10:14 -04:00
Nikolaj Bjorner
3dfc0a93f6 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-13 12:09:25 -04:00
Christoph M. Wintersteiger
badf9e6e67 whitespace 2016-03-11 14:05:32 +00:00
Christoph M. Wintersteiger
3e61ee2331 disabled "hardware interpretation" of fp.min/fp.max because the unspecified, standard-compliant behaviour is cheap anyways. 2016-03-11 12:52:00 +00:00
Christoph M. Wintersteiger
b5279d1da8 Bugfix for fp.to_ieee_bv. 
Fixes #507.
 2016-03-11 12:35:41 +00:00
Christoph M. Wintersteiger
9dd53c091a guard on m_preprocess in inc_sat_solver 2016-03-11 12:02:49 +00:00
mikolas
419e2c4899 Inc sat for ackr. 2016-03-10 17:36:06 +00:00
Mikolas Janota
ae9f369574 Fix in lackr_model_constructor. 2016-03-10 17:36:05 +00:00
mikolas
a2140085d6 In lazy ackermannization, collect all conflicting terms in one iteration. 2016-03-10 17:36:03 +00:00
Mikolas Janota
2f8465552c additional logging 2016-03-10 17:36:02 +00:00
Nuno Lopes
d6c3260db7 reduce_args_tactic: make it aware that 'a + const' may be a unique value in bv theory 
it allows us to remove UFs that are of the form f(a + 1), f(a + 2), etc..
 2016-03-10 10:15:09 +00:00
Nuno Lopes
0b1b5a4328 fix VS x64 warning 2016-03-10 09:03:24 +00:00
Nikolaj Bjorner
2354e747bf Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-09 21:33:16 -08:00
Nikolaj Bjorner
3d7eb12117 tracking use of assumptions in tactics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-09 21:33:08 -08:00
Nikolaj Bjorner
6ad6998c57 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-09 15:53:16 -08:00
Nikolaj Bjorner
03a0a6f6a1 refactor occurrence utility for common use (to be used in ctx_simplifier) per Nuno's suggestion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-09 15:53:02 -08:00
Nuno Lopes
8b53628d67 remove a few unused decls 2016-03-09 17:01:06 +00:00
martin-neuhaeusser
c7a7cc74fa Fix bug in ufbv tactic that enabled ackermannization even if unsat core or proof generation are requested 2016-03-09 14:06:39 +01:00
Nikolaj Bjorner
71fff8ffa2 fix boundary case according to analysis #477, e.g., size = 252, PTR_ALIGNMENT=2, slot_id = 64 = NUM_SLOTS 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-09 00:42:50 -08:00
Nikolaj Bjorner
5db84575f6 fix regression in o7.smt2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-08 22:27:47 -08:00
Nikolaj Bjorner
9743c188da add exception handling for making solver-1 discontinuation transparent, thanks to Martin, #497 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-08 17:00:12 -08:00
Nikolaj Bjorner
335a1dba6e guarding bb_rewriter now that it gets reset 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-08 16:50:06 -08:00
Nuno Lopes
d0de8fff62 ensure ast_manager::are_equal returns true if expr ptrs are equal 
found by Nikolaj
 2016-03-08 16:53:09 +00:00
Christoph M. Wintersteiger
cfda8e9e03 Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api 2016-03-08 14:32:30 +00:00
Nikolaj Bjorner
809fc86ac7 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-07 16:42:39 -08:00
Nikolaj Bjorner
5994c5a948 fix partial model tracking over cancellation/exceptions, reported by August Shi. Fix regression test for fp-to-real, reset the pre-processor in inc_sat_solver on exceptions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-07 16:42:29 -08:00
Nikolaj Bjorner
49d0e28621 allow parameters to overwrite logic, fixes bug report by Nuno 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-07 10:44:06 -08:00
Nikolaj Bjorner
8c4d791f01 use std::vector per Nuno's analysis to fix #420 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-03-07 08:08:17 -08:00
Christoph M. Wintersteiger
027331aef2 resolved merge conflicts 2016-03-07 14:20:10 +00:00
Christoph M. Wintersteiger
3a9b4985e4 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-07 13:35:54 +00:00
Nuno Lopes
9c620376c2 simplify ast::are_equal(), since pointer equality is sufficient 2016-03-07 13:15:12 +00:00