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

14973 commits

Author SHA1 Message Date
Nikolaj Bjorner 7956cf1201 annotate arith_sls 2023-02-12 20:55:44 -08:00
Nikolaj Bjorner bb81bc5452 fix #6580 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-12 20:21:53 -08:00
Nikolaj Bjorner 102eee77dc patch regressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-12 20:12:01 -08:00
Nikolaj Bjorner cac5052685 fixes related to #6577 
- enforce elim-and in bool-rewriter when invoking hoisting.
- make cnf tactic more resilient to non-normalized input.
- enable eliminate predicates on ground formulas
 2023-02-12 13:43:44 -08:00
Walden Yan ede9e5ffc2
[WIP] More TS Binding Features (#6412) 
* feat: basic quantfier support

* feat: added isQuantifier

* feat: expanded functions

* wip: (lambda broken)

* temp fix to LambdaImpl typing issue

* feat: function type inference

* formatting with prettier

* fix: imported from invalid module

* fix isBool bug and dumping to smtlib

* substitution and model.updateValue

* api to add custom func interps to model

* fix: building

* properly handling uint32 -> number conversion in z3 TS wrapper

* added simplify

* remame Add->Sum and Mul->Product

* formatting
 2023-02-11 15:48:29 -08:00
Nikolaj Bjorner 5e30323b1a wip - bounded local search for arithmetic 2023-02-11 15:46:39 -08:00
Nikolaj Bjorner 4b2c166e8b fixes to build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-11 10:19:24 -08:00
Nikolaj Bjorner 7bef2f3e6f wip - local search for euf/arithmetic 2023-02-11 09:33:43 -08:00
Nikolaj Bjorner 46c8d78ece fixes for #6577 
- the literal false should not appear in clauses
- the literal true forces a tautology
- fix early return in is_cnf check. It should check all clauses for nested Booleans.
 2023-02-11 09:33:42 -08:00
Nikolaj Bjorner d22e4aa525 wip - integrating arithmetic local search 2023-02-11 09:33:42 -08:00
Nikolaj Bjorner 1b0c76e3f0 fixes to mbqi in the new core based on #6575 2023-02-10 16:56:06 -08:00
Julian Parsert d52e893528
Added overloaded versions of context::recfun in the c++ api that allow for the declaration of recursive functions where the domain is given by a z3::sort_vector instead of an arity and sort* (#6576) 
Co-authored-by: Julian Parsert <julian.parsert@uibk.ac.at>
 2023-02-10 10:00:26 -08:00
Nikolaj Bjorner 02d48adae5 fix #6573 2023-02-08 08:24:52 -08:00
Nikolaj Bjorner a8335f2d5e use phase 2023-02-07 19:50:45 -08:00
Nikolaj Bjorner b3ebce3966 fix compilation 2023-02-07 19:30:45 -08:00
Nikolaj Bjorner 96d815b904 adding arith sls 2023-02-07 19:27:19 -08:00
Nikolaj Bjorner 6a2d60a6ba fix #6571 
most solvers don't support background properties
 2023-02-07 11:04:58 -08:00
Nikolaj Bjorner 601e506d54 remove debug out 2023-02-07 10:40:49 -08:00
Nikolaj Bjorner 90a75866fb elaborating on local-search rephase strategy 2023-02-07 03:17:52 -08:00
Nikolaj Bjorner c1c26f0726 restart after sat solution 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-06 09:21:35 -08:00
Nikolaj Bjorner 03a4920f3d fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-05 21:41:07 -08:00
Nikolaj Bjorner 75c573877d updates to ddfw, initial local search phase option 2023-02-05 21:35:22 -08:00
Nikolaj Bjorner 3712cbdbfd fix #6559 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-04 13:33:40 -08:00
Jakob Rath d69155b9e9
Shared features from polysat branch (#6567) 
* Allow setting default debug action

* Fix dlist and add iterator

* Add var_queue iterator

* Add some helpers

* rational: machine_div2k and pseudo_inverse

* Basic support for non-copyable types in map

* tbv helpers

* pdd updates

* Remove duplicate functions

gcc doesn't like having both versions
 2023-02-03 13:08:47 -08:00
Frederick Robinson be44ace995
fix typo (#6569) 2023-02-03 13:08:35 -08:00
Nikolaj Bjorner cb72b962d1 Merge branch 'master' of https://github.com/z3prover/z3 2023-02-02 20:50:58 -08:00
Nikolaj Bjorner 839f87a10c don't apply tactics in parse mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-02 20:50:53 -08:00
Nikolaj Bjorner 39d2818923 compiler warnings/bugs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-02 19:36:22 -08:00
Nikolaj Bjorner 0d05104d8c remove unused field 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-02 19:33:23 -08:00
Nikolaj Bjorner 741634b703 compiler warning fix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-02 19:26:51 -08:00
Nikolaj Bjorner efbecb19b1 compiler warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-02 19:23:30 -08:00
Nikolaj Bjorner ed4a84e5d3 compiler warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-02 19:21:34 -08:00
Nikolaj Bjorner 4143c54257 add simplifier to java API 2023-02-02 19:06:26 -08:00
Nikolaj Bjorner 2e068e3f56 add simplifiers to .net API 2023-02-02 17:41:00 -08:00
Nikolaj Bjorner 72e7a8a481 fix incremental pre-processing to work with consequences/cubes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-01 20:00:38 -08:00
Nikolaj Bjorner 6c7dd4a863 fix incremental pre-processing to work with assumptions/cores and consequences 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-01 19:47:58 -08:00
Nikolaj Bjorner 7767144051 fix test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-01 11:07:47 -08:00
Nikolaj Bjorner 30fa37e393 fix warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-01 10:31:34 -08:00
Nikolaj Bjorner 38d526ee45 fix warning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-01 10:18:14 -08:00
Nikolaj Bjorner 682e868129 initialize field 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-01 10:18:14 -08:00
Nikolaj Bjorner 0f86a00229 use setter method to easier track updates to settings. 2023-02-01 10:18:14 -08:00
Nikolaj Bjorner 19fed09122 protecting add_simplifier API against mis-use 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-02-01 08:35:32 -08:00
Nikolaj Bjorner 63c0f35978 update ml api 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 19:27:17 -08:00
Nikolaj Bjorner d51d518f96 update ml api 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 19:24:45 -08:00
Nikolaj Bjorner 1289937d1a update ml api 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 19:19:41 -08:00
Nikolaj Bjorner 9a94a9aa6f update ml api 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 19:14:24 -08:00
Nikolaj Bjorner 17bae9b4c1 update ml api 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 19:09:37 -08:00
Nikolaj Bjorner 162fa3dc96 disambiguate overloaded with for Julia bindings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 19:06:20 -08:00
Nikolaj Bjorner 4c6d44f974 add ocaml signature for simplifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 18:58:18 -08:00
Nikolaj Bjorner 550619bfcf add API for creating and attaching simplifiers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 17:06:03 -08:00
Nikolaj Bjorner ebc2cd572b fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 14:53:04 -08:00
Nikolaj Bjorner 88bf3c6e51 check if trail is empty to avoid collecting variables 2023-01-31 13:35:43 -08:00
Nikolaj Bjorner 8495be11f9 add shortcut filter to avoid traversing model reconstruction trail if there are no intersections with model 2023-01-31 13:34:52 -08:00
Nikolaj Bjorner e6f8fe359e remove empty file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 12:32:28 -08:00
Nikolaj Bjorner d263b373ed update release notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-31 12:19:33 -08:00
Nikolaj Bjorner 971b9d4081 fix #6564 
fixes to simplifier command front-end
 2023-01-31 09:32:34 -08:00
Nikolaj Bjorner 238d604a10 android 16 byte alignment for stack allocated memory? 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-30 23:00:44 -08:00
Nikolaj Bjorner 6022c17131 Add simplification customization for SMTLIB2 
Add the ability to customize incremental pre-processing simplification for the SMTLIB2 front-end. The main new capability is to use pre-processing tactics in incremental mode that were previously not available. The main new capabilities are
- solve-eqs
- reduce-args
- elim-unconstrained
There are several more. Documentation and exposed simplifiers are populated incrementally. The current set of supported simplifiers can be inspected by using z3 with the --simplifiers flag or referring to https://microsoft.github.io/z3guide/docs/strategies/simplifiers

Some pending features are:
- add the ability to update parameters to simplifiers similar to how tactics can be controlled using parameters.
- expose simplification solvers over the binary API.
 2023-01-30 22:38:51 -08:00
Nikolaj Bjorner dd0decfe5d create simplifier_solver wrapper to supply simplifier layer 
move sat_smt_preprocess to solver
fix bugs in model_reconstruction_trail for dependency replay

This is a preparatory step for exposing pre-processing as tactics.
 2023-01-30 16:12:25 -08:00
Nikolaj Bjorner 304b316314 move bounded division lemmas to nla solver/ nla_divisions. 2023-01-30 11:11:04 -08:00
Nikolaj Bjorner 03ca330926 fix division filter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-30 08:23:17 -08:00
Nikolaj Bjorner 2c4a9c2f5c fix division filter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-30 08:20:26 -08:00
Nikolaj Bjorner 8e37e2f913 handle non-linear division axioms, consolidate backtracking state in nla_core 
this update enables new incremental linear axioms based on division terms.
It also consolidates some of the backtracking state in nla_core / emons to use stack traces instead of custom backtracking state.
 2023-01-29 17:22:57 -08:00
Nikolaj Bjorner 4ffe3fab05 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-28 21:51:51 -08:00
Nikolaj Bjorner 8ea49eed8e convert reduce-args to a simplifier 
- convert reduce-args to a simplifier. Currently exposed as reduce-args2 tactic until the old tactic code gets removed.
- bug fixes in model_reconstruction trail
  - allow multiple defs to be added with same pool of removed formulas
  - fix tracking of function symbols instead of expressions to filter replay
- add nla_divisions to track (cheap) divisibility lemmas.
-
 2023-01-28 20:12:14 -08:00
Nikolaj Bjorner 246d6f7b77 fix #6561 2023-01-28 03:47:18 -08:00
Nikolaj Bjorner fb1f4f3a2c add pragma 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-27 18:03:06 -08:00
Nikolaj Bjorner 91d6082f2f Move modular interval to interval directory 2023-01-27 17:55:36 -08:00
Nikolaj Bjorner 0f3c56213e move dominator simplifier functionality to rewriter and simplifier, move bv_bounds simplifier functionality to simplifier 2023-01-27 17:11:48 -08:00
Nikolaj Bjorner d4ca7e5374 #6555 2023-01-26 21:39:52 -08:00
Nikolaj Bjorner ae24b73b19 bugfixes to incremental linearization for expanding power 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-26 21:19:45 -08:00
Nikolaj Bjorner 8be43ca68b reshuffle pre-conditions for powers 2023-01-25 13:51:19 -08:00
Nikolaj Bjorner e41dd91893 add module for handling axioms for powers 2023-01-25 13:34:13 -08:00
Nikolaj Bjorner 9e2ec9d018 add stubs for proof production in elim_unconstrained 2023-01-25 13:32:51 -08:00
Nikolaj Bjorner b3de7ac595 remove passing proof parameter to expr-inverter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-25 11:15:09 -08:00
Nikolaj Bjorner f100d2f4de add contextual simplification to bv-bounds-tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-24 17:49:55 -08:00
Nikolaj Bjorner 6a7343aab4 update julia bindings to use 64-bit mk_real (real_val) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-24 13:06:41 -08:00
Nikolaj Bjorner fa72ec5405 switch to expose fresh function instead of changing legacy function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-24 13:05:34 -08:00
Nikolaj Bjorner eac7d7576f force to_fp to disambiguate +zero and -zero, #6548, filter unsupported on relevancy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-24 12:29:42 -08:00
Nikolaj Bjorner 47c7ed3b17 update ml example to 64 bit 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-24 04:33:52 -08:00
Nikolaj Bjorner 15d853dc04 add trail to avoid stale references in expr2var 2023-01-24 04:15:52 -08:00
Nikolaj Bjorner 3f1b7866ca convert caml mk_real to int64 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-24 03:53:42 -08:00
Nikolaj Bjorner 4601d1d664 fix #6550 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-24 03:37:09 -08:00
Nikolaj Bjorner 2ae476416c initial outline of exponentiation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-23 17:38:34 -08:00
Nikolaj Bjorner 3032c9315d handle to-real in variable mapping 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-23 14:31:24 -08:00
Nikolaj Bjorner d9f9cceea4 use intervals for tracking bounds on arithmetic variables 
leverage interval propagation for bounds.
merge functionality with propagate-ineqs tactic
remove the new propagate-bounds tactic and instead use propagate-ineqs
 2023-01-23 14:13:03 -08:00
Nikolaj Bjorner eb751bec4c fix riscv/aarch/powerpc build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-22 23:57:59 -08:00
Nikolaj Bjorner 3b5ae285d9 add outline for interval reasoning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-22 23:28:36 -08:00
Nikolaj Bjorner 273aff5ed6 remove debug out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-22 22:21:23 -08:00
Nikolaj Bjorner db79346ef7 Add new tactic bound-simplifier for integer-based bit-vector reasoning. 2023-01-22 22:07:28 -08:00
Nikolaj Bjorner 83662701b6
Update theory_lra.cpp 
remove spurious output
 2023-01-22 16:27:48 -08:00
Nikolaj Bjorner dbc299efbb revise bv-bounds-tactic 
- share common functionality
- rename propagate-bv-bounds-new to propagate-bv-bound2 for now
- expose configuration options in bounds propagation
 2023-01-22 14:41:53 -08:00
Nikolaj Bjorner e2a6376ddf detect bounds from mod 2023-01-22 14:40:36 -08:00
Nikolaj Bjorner 021ef699af detect bounds from mod 2023-01-22 14:40:19 -08:00
Nikolaj Bjorner 7d364bf786 Allow building AC functions without requiring arity check from API 2023-01-22 14:39:58 -08:00
Nikolaj Bjorner 806a4772bc revert effect of filtering unsupported 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-20 17:28:24 -08:00
Nikolaj Bjorner 4e6d498a60 adding placeholder for refining power of 2 2023-01-20 14:37:05 -08:00
Nikolaj Bjorner 0f4f32c5d0 apply relevancy filtering on unsupported ops, fix term construction bug in bv2fpa_converter fix #6548 2023-01-20 13:05:01 -08:00
Nuno Lopes 37652e7e17 fix tactic name in docs 2023-01-20 17:30:40 +00:00
Nikolaj Bjorner f3d6856736 remove msf example, add option to make model converter not reduce models 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-19 20:24:31 -08:00
Nikolaj Bjorner d11e5c8ca6 address compiler warnings, and user question #6544 2023-01-19 19:02:43 -08:00
Nikolaj Bjorner 523a3f34b0 change to manylinux2014 in setup.py 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-19 17:27:07 -08:00
Nikolaj Bjorner 9290de8223 make euf-egraph resilient to when there are no consumers to literal propagation. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-18 07:57:19 -08:00
Nikolaj Bjorner 7368f9f7d3 increase build version, better propagation in euf-egraph, handle assumptions in sat.smt 
- increase build version to 4.12.1. This prepares updated release for MacOs-11 build on x86
- move literal propagation mode in euf-egraph to a callback and traversal of equivalence class. Track antecedent by newest equality instead of root. This makes equality propagation to literals have similar behavior as in legacy solver and appears to result in a speedup (10% fewer conflicts on QF_UF/QG-classification/qg5/iso_icl478.smt2 in preliminary testing)
- fix interaction of pre-processing and assumptions. Pre-processing has to freeze assumption literals so they don't get eliminated. This is similar to dependencies that are already frozen.
 2023-01-17 14:07:07 -08:00
Nikolaj Bjorner dde5218b29 fix mbqi value caching issue raised by Clemens and Martin 2023-01-15 22:47:34 -05:00
Nikolaj Bjorner d5fde2e578 #6538 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-15 15:58:29 -05:00
Nikolaj Bjorner 4f7f4376b8 fix bug in new core not detecting conflict, fix #6525, add tactic doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-14 17:20:43 -05:00
Nikolaj Bjorner f1805138e7 missing code signing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-13 16:13:20 -08:00
Nikolaj Bjorner 60fef928cc missing code signing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-13 16:12:48 -08:00
Nikolaj Bjorner d289434b65 fix #6535 2023-01-12 19:06:30 -08:00
Nikolaj Bjorner 25b0b1430c move bound_manager to simplifiers, add bound manager to extract_eqs for solve-eqs #6532 2023-01-12 12:42:28 -08:00
Jerry James e5e16268cc
Initialize m_istamp_id in lookahead::init (#6533) 2023-01-12 11:20:28 -08:00
Nikolaj Bjorner 8970a54eaa expose parameters to control behavior for #5660 2023-01-10 22:06:19 -08:00
Nikolaj Bjorner 1c7ff72ae2 add tactic doc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-10 18:58:25 -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 b700dbffce fix #6528 2023-01-10 14:42:23 -08:00
Brecht Sanders 2bd933d87f
Fix hwf.cpp for MinGW-w64 32-bit clang (#6529) 
Fix src/util/hwf.cpp for building with MinGW-w64 clang targetting Windows 32-bit.
Without this fix there is an arror about `__control87_2` not being defined.
 2023-01-10 13:44:11 -08:00
Nikolaj Bjorner c3e31149a5 fix #6530 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-10 13:43:17 -08:00
Nikolaj Bjorner a4d4e2e483 track assertions 2023-01-09 15:18:33 -08:00
Nikolaj Bjorner 64ec8acd30 fix model reconstruction ordering for elim_unconstrained 2023-01-09 15:18:19 -08:00
Nikolaj Bjorner 30e0f78c16 remove exit 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-09 10:00:36 -08:00
dependabot[bot] a4f2a1bb2e
Bump json5 from 2.2.1 to 2.2.3 in /src/api/js (#6527) 
Bumps [json5](https://github.com/json5/json5) from 2.2.1 to 2.2.3.
- [Release notes](https://github.com/json5/json5/releases)
- [Changelog](https://github.com/json5/json5/blob/main/CHANGELOG.md)
- [Commits](https://github.com/json5/json5/compare/v2.2.1...v2.2.3)

---
updated-dependencies:
- dependency-name: json5
  dependency-type: indirect
...

Signed-off-by: dependabot[bot] <support@github.com>
 2023-01-09 09:16:55 +00:00
Nikolaj Bjorner 49ee570b09 split into separate function 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-08 19:16:46 -08:00
Nuno Lopes 5899fe3cea
Add rewrite for array selects of chain of stores of a same value (#6526) 
* Add rewrite for array selects of chain of stores of a same value

Example:
```smt
(declare-fun mem () (Array (_ BitVec 4) (_ BitVec 4)))
(declare-const x (_ BitVec 4))
(declare-const y (_ BitVec 4))
; simplifies to #x1
(simplify (select (store (store (store mem #x1 #x1) y #x1) x #x1) #x1))
```

* Update array_rewriter.cpp

* Update array_rewriter.cpp
 2023-01-08 19:09:01 -08:00
Nikolaj Bjorner 1ddef117a2 several fixes to proof logging in legacy solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-08 16:11:31 -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 95cb06d8cf add quasi macro detection 2023-01-06 19:53:55 -08:00
Nikolaj Bjorner 25112e47b4 bugfix to flatten-clases simplifier 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-05 20:59:28 -08:00
Nikolaj Bjorner c07b6ab38f more tactic descriptions 2023-01-05 20:23:01 -08:00
Nikolaj Bjorner 0d8a472aac pass sign into literal definition for pbge 2023-01-04 16:55:44 -08:00
Nikolaj Bjorner 81ce57b5a8 #6429 2023-01-04 15:38:13 -08:00
Nikolaj Bjorner e0099150ca #6429 2023-01-04 15:28:57 -08:00
Nikolaj Bjorner 380c701cbe restore debug clang/gcc build 2023-01-04 15:01:40 -08:00
Nikolaj Bjorner 21362c0b98 make case-def and recfun-num-rounds re-parsable for logging 2023-01-04 15:00:25 -08:00
Nikolaj Bjorner ef10119005 #6429 fixes 2023-01-04 13:05:45 -08:00
Nikolaj Bjorner aa080a6b19 update ignore-int handling #6429 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-04 12:22:38 -08:00
Nikolaj Bjorner 8d0d6d8f04 Merge branch 'master' of https://github.com/z3prover/z3 2023-01-04 11:56:38 -08:00
Nikolaj Bjorner 6f95c77023 fix bugs in flatten_clauses simplifier, switch proof/fml 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-04 11:56:28 -08:00
Nuno Lopes e448191212 array rewriter: expand select of store with const array into an ite 
This:
(simplify (select (store ((as const (Array (_ BitVec 4) (_ BitVec 4))) #x0) x #x1) y))
=>
(ite (= x y) #x1 #x0)
 2023-01-03 11:08:57 +00:00
Nuno Lopes e508ef17f6 fix Alive bug #875: bit blaster not respecting soft memory limit 2023-01-03 10:39:28 +00:00
Nuno Lopes a2cc504d4a remove a couple more std::endl 2023-01-03 09:49:58 +00:00
Nuno Lopes d30cb55bae don't flush stream when printing param vals 2023-01-03 09:35:17 +00:00
Nikolaj Bjorner d4490738bc Merge branch 'master' of https://github.com/z3prover/z3 2023-01-02 16:49:43 -08:00
Nikolaj Bjorner ea0d09b6c8 add pointer to build parameters to README #6518 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-01-02 16:49:31 -08:00
Walden Yan dbf93c5fbd
Fixing array select for lambda expressions in Python API (#6516) 
* fix: making array select work for lambda expressions

* more elegant solution
 2023-01-01 15:27:54 -08:00
Nikolaj Bjorner f6d411d54b experimental feature to access congruence closure of SimpleSolver 
This update includes an experimental feature to access a congruence closure data-structure after search.
It comes with several caveats as pre-processing is free to eliminate terms. It is therefore necessary to use a solver that does not eliminate the terms you want to track for congruence of. This is partially addressed by using SimpleSolver or incremental mode solving.

```python
from z3 import *
s = SimpleSolver()
x, y, z = Ints('x y z')
s.add(x == y)
s.add(y == z)
s.check()
print(s.root(x), s.root(y), s.root(z))
print(s.next(x), s.next(y), s.next(z))
```
 2022-12-30 21:41:27 -08:00
Nikolaj Bjorner c0f1f33898 dampen second setup of theory_bv 2022-12-30 18:47:32 -08:00
Nikolaj Bjorner 5f6f2fc758 rename bit_blaster class to bit_blaster_simplifier to avoid name clash 2022-12-30 18:39:02 -08:00
Nikolaj Bjorner 0d05e0649b initialization order 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-12-30 18:16:24 -08:00