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

107 commits

Author SHA1 Message Date
Nikolaj Bjorner ecdfab81a6 fix #7434 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-10-28 17:51:01 -07:00
Nikolaj Bjorner ba5cec7704 additional rewrites for bv2int 2024-09-22 21:29:12 +03:00
Nikolaj Bjorner fa7fc8ef5e Refactor bv_rewriter functions using unified variable assignment and early break logic 2024-09-22 13:04:49 +03:00
Nikolaj Bjorner d66609ea14 fix #7389 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-09-22 02:41:11 +03:00
Nikolaj Bjorner 13be3c3fbb reset model converter between rounds to elim-unconstrained. 2023-12-18 16:57:52 -08:00
Nikolaj Bjorner 0daa05aab2 add ability to log selected bv rewrites 2023-12-18 16:57:52 -08:00
Nikolaj Bjorner e9abdbb7a4 fix #7011 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-29 15:08:08 -08:00
Jakob Rath 57e92b2a59
Fix bvnego (#6750) 2023-06-07 11:24:40 -07:00
Antti Hyvärinen 12e45c9d17
Implement proposed smtlib2 bitvector overflow predicates (#6715) 
* Logical names for function declarations in c++

Currently, for example, the function declaration symbol member for
checking whether multiplication *does not* overflow is called
`m_bv_smul_ovfl`.  Since we are introducing the upcoming smtlib2 symbols
that check that multpliciation *does* overflow, the not overflow check
symbols are renamed to `m_bv_smul_no_ovfl` etc.

* Implement smtlib overflow preds for multiplication

Smtlib2 is being extended to include overflow predicates for bit
vectors (see https://groups.google.com/u/1/g/smt-lib/c/J4D99wT0aKI).
This commit introduces the predicates `bvumulo` and `bvsmulo` that
return `true` if the unsigned multiplication overflows or the signed
multiplication underflows or overflows, respectively.

* Move mul overflow predicates to BV logic

* Add a todo on illogical argument order

* Implement mk_unary_pred for bv

* Implement bvnego

* Implement bvuaddo

* Implement bvsaddo

* Implement bvusubo

* Implement bvssubo

* Implement bvsdivo
 2023-05-09 10:37:46 -07:00
Nikolaj Bjorner c0f80f92ba deal with compiler warnings (unused variables etc) 2023-02-18 17:53:37 -08:00
Nikolaj Bjorner d415f07386 memory leak on proof justifications 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-10 18:58:25 -08:00
Nikolaj Bjorner 61b90e64b2 disable new simplifcation for multiplier until really understood 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-08 14:17:49 -08:00
Nikolaj Bjorner fcea32344e add missing tactic descriptions, add rewrite for tamagochi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-08 13:32:26 -08:00
Nikolaj Bjorner 87095950cb fix #6477 2022-12-04 13:02:45 -08:00
Nikolaj Bjorner 79e6d4e32d tune and debug elim-unconstrained (v2 - for simplifiers infrastructure) 2022-12-04 03:53:31 -08:00
Nikolaj Bjorner cf7bba6288 use ast_manager as an attribute 2022-12-04 03:53:30 -08:00
Nikolaj Bjorner eceeb295fc fix #6457 2022-11-24 14:41:50 +07:00
Nikolaj Bjorner 9845c33236 add shortcuts in rewriter, eliminate redundancies in dependent_expr tactic 2022-11-15 09:13:13 -08:00
Nikolaj Bjorner 3a4b8e2334 add rewrite rules to bv-rewriter 2022-11-08 12:20:51 -08:00
Nikolaj Bjorner fe1b4bf5ce disable ternary, fixes to propagation, make bv_rewrites for multiplier n-ary 2022-10-26 23:44:38 -07:00
Nikolaj Bjorner 5352a0106d fix #6426 2022-10-26 12:20:55 -07:00
Nikolaj Bjorner c62c5e9d23 add opportunistic, missing, bv rewrites 
- x >> x logical = 0
- ~x = -1 -x
- x * (y << z) = (x * y) << z
 2022-10-25 10:29:48 -07:00
Nikolaj Bjorner ab9aee189b perf #6100 2022-06-21 13:49:52 -07:00
Nikolaj Bjorner 6abea2de2c fix nightly, fix regression identified by Nuno 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-28 18:03:15 -07:00
Nikolaj Bjorner 8d980ea704 remove internal configuration 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-28 12:13:18 -07:00
Clemens Eisenhofer 0b20a4ebf4
Added rewriting distinct with bitvectors to false if bit-size is too low (#5956) 
* Fixed problem with registering bitvector functions

* Added rewriting distinct with bitvectors to false if bit-size is too low

* Removed debug output

* Incorporated Nikolaj's comments

* Simplifications
 2022-04-09 21:46:21 +02:00
Nikolaj Bjorner 431c3af409 fix #5929 - add parameter bv_le2extract to allow disabling the disassembly to extract 2022-03-27 18:23:41 -10:00
Nikolaj Bjorner 913b90f7aa fix #5802 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-30 10:42:34 -08:00
Nikolaj Bjorner 2551631957 mul overflow #5797 2022-01-29 09:15:38 -08:00
Nikolaj Bjorner 5e81c1220c #5797 probably still wrong wrt underflow. 2022-01-27 12:48:15 -08:00
Nikolaj Bjorner 4da930b490 #5794 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-27 10:50:48 -08:00
Nikolaj Bjorner 461e71017d fix #5792 again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-26 15:54:44 -08:00
Nikolaj Bjorner 20f9814939 fix #5789 
fix incorrect constant folding
 2022-01-24 09:42:14 +01:00
Nikolaj Bjorner 87aec8819f fix #5687 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-01 10:08:29 -08:00
Nikolaj Bjorner c083aa82ee add debug information in user-propagate #5687 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-29 08:59:53 -08:00
Nikolaj Bjorner 4a6083836a call it data instead of c_ptr for approaching C++11 std::vector convention. 2021-04-13 18:17:35 -07:00
Nikolaj Bjorner 2fef6dc502 more scaffolding 2021-03-21 11:31:14 -07:00
Nikolaj Bjorner 18143d8932 fix #5102 2021-03-15 01:01:33 -07:00
Nikolaj Bjorner 299e1788b8 fix #4808 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-11-21 15:03:17 -08:00
Nikolaj Bjorner d6106f26ff disable gcd test 2020-11-20 12:18:19 -08:00
Nikolaj Bjorner a475e7cf5a Add gcd test to bv-rewriter 2020-11-20 11:12:54 -08:00
Nikolaj Bjorner 367e5fdd52
delay internalize (#4714) 
* adding array solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* use default in model construction

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* debug delay internalization

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* bv

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* arrays

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* get rid of implied values and bounds

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* redo egraph

* remove out

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove files

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-09-28 19:24:16 -07:00
Nikolaj Bjorner 98084d7da7 add depend 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-29 10:49:19 -07:00
Nikolaj Bjorner e2bdf54d5e update include 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-08-29 10:45:26 -07:00
Nikolaj Bjorner 937afbf95b draft rewrite 2020-05-16 12:43:26 -07:00
Nikolaj Bjorner 2822922d36 fix regression with mainintaing signs for monotonicity lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-16 11:17:40 -07:00
Nikolaj Bjorner d352c61e01 fix regression with mainintaing signs for monotonicity lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2020-05-16 11:17:39 -07:00
Nikolaj Bjorner f30d63a8f2 better rewriting for ule 2020-05-02 12:59:12 -07:00
Nikolaj Bjorner f313ab9e4c correct newly introduced rewrite 2020-05-02 10:15:06 -07:00
Nikolaj Bjorner f0d33ddddb some simplifications based on #4178 2020-05-02 06:44:34 -07:00