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

13411 commits

Author SHA1 Message Date
Andrew V. Jones f1b8376739
Rename 'user' to 'user_solver' #5586 (#5587) 
Issue #5586 reported that Android builds (targetting, e.g., x86) failed
to compile due to a conflict between:

* `struct user` in `sys/user.h`; and
* `namespace user` in z3's `user_solver.h`

This issue is resolved by renaming `namespace user` to `namespace
user_solver` (matching the header name) to avoid this conflict.

Reported-by: Jamie Collinson <jamiecollinson@gmail.com>

Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
 2021-10-09 15:07:37 -07:00
Nikolaj Bjorner bfa960c2ce fix internalize regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-08 14:48:17 -07:00
Margus Veanes 146f4621c5
Updated regex derivative engine (#5567) 
* updated derivative engine

* some edit

* further improvements in derivative code

* more deriv code edits and re::to_str update

* optimized mk_deriv_accept

* fixed PR comments

* small syntax fix

* updated some simplifications

* bugfix:forgot to_re before reverse

* fixed PR comments

* more PR comment fixes

* more PR comment fixes

* forgot to delete

* deleting unused definition

* fixes

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

* fixes

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

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-08 13:04:49 -07:00
Nikolaj Bjorner c0c3e685e7 disable all propagation until ematch incompleteness is fixed 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-05 11:25:35 -07:00
Nikolaj Bjorner 94cc4ead72 remove arith_lhs simplification from preamble tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-05 10:55:38 -07:00
Nikolaj Bjorner 33f4e65fa9 redo bindings/fingerprints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-05 10:15:56 -07:00
Nikolaj Bjorner 281fb67d88 unit propagate with fingerprints 2021-10-04 20:01:46 -07:00
Nikolaj Bjorner 8a85cfdb12 fix #5579 - 
It is only possible to reach this case when new assertions are created.
 2021-09-30 09:32:34 -07:00
Nikolaj Bjorner cbe7dd4a48 missing continue fixes unsound sat result from #5573 2021-09-29 14:26:09 -07:00
Nikolaj Bjorner ff723f15ff Update z3++.h 2021-09-29 12:19:02 -07:00
Nikolaj Bjorner 62fd22f555 disable macro finder tactic if there are recursive functions fix #5574 2021-09-29 09:33:52 -07:00
Nikolaj Bjorner 137e5c5263 fix tmp_eq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-28 14:28:41 -07:00
Nikolaj Bjorner 67ae75bac7 fix tmp_eq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-28 14:27:46 -07:00
Nikolaj Bjorner da124e4275 tune q-eval and q-ematch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-28 13:41:37 -07:00
Nikolaj Bjorner 92c1b600c3 tuning eval 2021-09-28 09:56:00 -07:00
Nikolaj Bjorner 2e176a0e02 count lazy bindings 2021-09-28 08:27:46 -07:00
Nikolaj Bjorner 3abecc3428 add extra commands to API parser 2021-09-27 14:19:43 -07:00
Nikolaj Bjorner 6c71baf77b lifting iff to binary 2021-09-27 03:45:54 -07:00
Nikolaj Bjorner d174f87c5e #5532 2021-09-21 20:21:23 -07:00
Nikolaj Bjorner 18d1b368d1 #5532 2021-09-21 20:12:32 -07:00
Nikolaj Bjorner cabd5b10fa #5532 2021-09-21 18:56:55 -07:00
Nikolaj Bjorner de20bffafe import goodies from ps 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-21 11:13:03 -07:00
Nikolaj Bjorner 708602dfbb fix #5560 - add a throttle on maximal size of bignums created for propagate-value lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-21 08:56:13 -07:00
Nikolaj Bjorner 2e96557827 fix #5560 - add a throttle on maximal size of bignums created for propagate-value lemmas 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-21 08:55:28 -07:00
Nikolaj Bjorner 2c266a96c8 #5545 2021-09-20 13:57:34 -07:00
Nikolaj Bjorner 1352aa06f3 #5532 2021-09-20 12:08:04 -07:00
Nikolaj Bjorner 0170f1f461 #5532 2021-09-20 11:39:16 -07:00
Nikolaj Bjorner fd799089b7 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-20 11:19:26 -07:00
Nikolaj Bjorner 6f31d83633 fix #5541 2021-09-20 10:10:28 -07:00
Jamey Sharp 426306376f
CNF conversion refactoring (#5547) 
* split sat2goal out of goal2sat

These two classes need different things out of the sat::solver class,
and separating them makes it easier to fiddle with their dependencies
independently.

I also fiddled with some headers to make it possible to include
sat_solver_core.h instead of sat_solver.h.

* limit solver_core methods to those needed by goal2sat

And switch sat2goal and sat_tactic over to relying on the derived
sat::solver class instead. There were no other uses of solver_core.

I'm hoping this makes it feasible to reuse goal2sat's CNF conversion
from places like the tseitin-cnf tactic, so they can be unified into a
single implementation.
 2021-09-20 08:53:10 -07:00
Nikolaj Bjorner d36c3faf76 #4880 add interpreted versions of to_bv functions for MBQI quantifier models 2021-09-17 14:23:14 +01:00
Nikolaj Bjorner 1fc7b63a80 ... 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-16 21:59:54 +01:00
Nikolaj Bjorner cef964fda3 fixes for model converter default case 2021-09-16 17:31:26 +01:00
Nikolaj Bjorner fe3f139eb2 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-16 16:25:43 +01:00
Nikolaj Bjorner c3c5c14ead prepare for min/max i 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-16 16:23:10 +01:00
Nikolaj Bjorner 50375df8dc enforce idempotency 
bug reported by Clemens
 2021-09-15 15:36:20 +01:00
CEisenhofer c58b2f4a9c
Added character functions to API (#5549) 
* Added character functions to API

* Changed names of c++ functions
 2021-09-15 13:34:58 +01:00
Nikolaj Bjorner 9aad331699 #5546 
try dampening
 2021-09-14 10:32:53 +02:00
Nikolaj Bjorner f13ccf8969 bv2char and char2bv with Clemens 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-13 16:09:03 +02:00
Nikolaj Bjorner 34f878fb97 make it easier to debug parallel 2021-09-10 07:09:22 +02:00
Nikolaj Bjorner 3e6ff768a5 fix regression bug in mam reported by Aseem 2021-09-10 07:09:22 +02:00
CEisenhofer 47fdd6c060
Added 16 bit string-encoding (#5540) 2021-09-09 11:35:16 +02:00
Nikolaj Bjorner e70f501932 handle potential extra nodes from q_solver 2021-09-09 09:17:11 +02:00
Nikolaj Bjorner c4d0ded7b7 #5532 2021-09-08 06:19:49 +02:00
Nikolaj Bjorner 8c406c161e #5532 add blocking condition for recursion. 2021-09-07 12:28:18 +02:00
Nikolaj Bjorner 93415740b6 left over bugs #5532 
disabling complete const rewriting (temporarily) as it can loop
 2021-09-07 07:00:41 +02:00
Nikolaj Bjorner be4df46f6f #5532 remove unsound rewrite rule that was recently added 2021-09-07 06:42:24 +02:00
Nikolaj Bjorner 72f6271d82 #5532 
bugs in:
- rewriting of 0-ary expressions was incomplete
- sharing annotations when a node has two theories attached it is shared
- sharing of const of an array

Remove unreadable part of pretty printer for lp solver.
 2021-09-06 19:14:03 +02:00
Nikolaj Bjorner 3764eb1959 #5532 
ensure re-internalization for predicates that are replayed.
Theory internalization is currently not considered in depth.
 2021-09-05 00:24:34 -07:00
Nikolaj Bjorner 3021da87cf #5532 2021-09-04 21:10:26 -07:00
Nikolaj Bjorner 9c91698201 #5532 2021-09-04 18:03:15 -07:00
Nikolaj Bjorner 976c0a391c revisit as-array evaluation 2021-09-04 18:00:36 -07:00
Nikolaj Bjorner 38b82fa742 const rewriting revisited 2021-09-04 17:59:08 -07:00
Nikolaj Bjorner 051ede64e7 #5532 2021-09-04 09:48:46 -07:00
Nikolaj Bjorner 3de9162c7e handle null more gracefully 2021-09-04 09:42:45 -07:00
Nikolaj Bjorner 9c5ef79701 #5532 2021-09-04 09:05:49 -07:00
Nikolaj Bjorner 18e4546404 modernize parameter defaults 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-03 17:42:36 -07:00
Nikolaj Bjorner cdcfbeb6d8 #5532 
remove "reflect" parameter from exposed options. It should be internal only.
 2021-09-03 16:01:59 -07:00
Nikolaj Bjorner 0ddbbe9bd2 #5532 2021-09-03 15:41:52 -07:00
Nikolaj Bjorner 5633af76cc #5532 2021-09-03 15:25:50 -07:00
Nikolaj Bjorner a566c7307d #5532 2021-09-03 12:33:04 -07:00
Nikolaj Bjorner 87f5b9282f #5532 2021-09-03 12:20:23 -07:00
Nikolaj Bjorner c4158ebc33 #5532 2021-09-03 12:02:57 -07:00
Nikolaj Bjorner 20a259cfaa throw less #5519 2021-09-03 10:40:08 -07:00
Nikolaj Bjorner af5c6e43b9 #5528 2021-09-02 11:21:57 -07:00
Nikolaj Bjorner 55285b2193 make it easier to iterate over arguments of an application 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-02 09:51:59 -07:00
Nikolaj Bjorner e9a4a9a390 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-02 09:23:59 -07:00
Nikolaj Bjorner edb26e7be7 Merge branch 'master' of https://github.com/z3prover/z3 2021-09-02 08:53:56 -07:00
Nikolaj Bjorner 02acc38c28 add extra checks that user-supplied assumptions are asserted 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-02 08:53:47 -07:00
Nikolaj Bjorner e05ef8ece9 account for updating scoped state by goal2sat #5528 2021-09-02 04:20:19 -07:00
Nikolaj Bjorner f4abe3db02 #5528 2021-09-02 03:13:46 -07:00
Nikolaj Bjorner 9e306e3b6e more useful diagnostics 2021-09-01 20:50:35 -07:00
Nikolaj Bjorner 968717a532 follow on fix from #5528 
the same bug is also undetected in the main solver
 2021-09-01 20:49:39 -07:00
Nikolaj Bjorner 6907d30717 #5528 2021-09-01 20:44:00 -07:00
Nikolaj Bjorner a74c01c8b9 #5528 2021-09-01 20:39:54 -07:00
Nikolaj Bjorner cf9e55fa96 #5516 
expose ability to expand select/store and select/ite (lambdas are always expanded) during pre-processing for N.P. Lopes.
 2021-09-01 17:44:17 -07:00
Nikolaj Bjorner ba68fba419 build 2021-09-01 17:10:23 -07:00
Nikolaj Bjorner 0c53c139da add to_string method to make it easier to use without << 2021-09-01 15:37:58 -07:00
Nikolaj Bjorner 7ce4be8455 #5528 2021-09-01 14:01:15 -07:00
Nikolaj Bjorner a7bc4719c0 fix #5526 
when propagation claims progress, but is a no-op.
 2021-09-01 11:45:21 -07:00
Nikolaj Bjorner 8bdc8d0e1a Update solver_subsumption_tactic.h 
use naming convention with - instead of _ for tactics
 2021-09-01 11:35:06 -07:00
Nikolaj Bjorner a3ba4e1366 #5528 2021-09-01 11:34:44 -07:00
Nikolaj Bjorner f91c3d9fd6 round-tripping escapes, again #5519 2021-08-31 20:36:38 -07:00
Nikolaj Bjorner 90f98d5791 fix part of #5519 
generation of escape sequences for output was not handling non-printable character ranges correctly and also not offsetting hexadecimal characters right.
 2021-08-31 20:06:06 -07:00
Nikolaj Bjorner 7c782a7ef8 #5518 
patch a gaping hole in recfun
 2021-08-31 19:49:18 -07:00
Nikolaj Bjorner 1426390aec #5518 2021-08-31 16:38:27 -07:00
Nikolaj Bjorner ab2baa764c #5518 
@wintersteiger
This example exposes a bug in is_unique_value
```
(assert (= (fp.to_real ((_ to_fp 8 24) (_ bv4286579200 32))) (fp.to_real ((_ to_fp 8 24) (_ bv4286578944 32)))))
(check-sat)
```
It returns true for fp representations that map to NaN. It can only return true for fp values that are unique relative to having no other bit-vector representation so not corresponding to an equivalence class of values such as NaN.
I am having it return false. If there is a way to refine the test it will catch some earlier inferences.
 2021-08-31 14:52:45 -07:00
Nikolaj Bjorner 34c8f598a5 #5518 2021-08-31 14:21:10 -07:00
Nikolaj Bjorner 07bbd026ac #5518 2021-08-31 13:02:54 -07:00
Nikolaj Bjorner 0b063f7903 #5518 2021-08-31 12:50:24 -07:00
Nikolaj Bjorner 535f442655 #5518 
regression from adding lambdas in model
 2021-08-31 12:13:27 -07:00
pcarbonn cd2701da0c
fix the use of ctx in Q() (#5521) 
* fix #4956

* fix: use ctx in Q()
 2021-08-31 10:01:47 -07:00
Nikolaj Bjorner 148cb83b0d #5482 fix default case for model construction 
port mg_merge functionality from theory_array_base that ensures default values in arrays congruent modulo stores are the same
 2021-08-29 17:30:39 -07:00
Nuno Lopes 9b5ec6d004 logging cleanup 
move everything out-of-line as common path doesn't log
fix some race conditions on file ptr vs enable_logging vars
 2021-08-29 12:24:19 +01:00
Nuno Lopes 9a172939e0 fix logging in Z3_fpa_get_[es]bits 2021-08-29 10:58:54 +01:00
Nikolaj Bjorner b1bc890992 fix #5515 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-28 18:05:51 -07:00
Nikolaj Bjorner e7fcbd9563 bail on first model validation failure 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-28 17:08:34 -07:00
Nikolaj Bjorner 4f064ee5d6 simplify based on comment from Jamie Sharp #5512 2021-08-28 17:08:34 -07:00
Nuno Lopes e5a2f08cc9 fix logging of Z3_mk_lambda and Z3_mk_lambda_const 
In preparation of a bug report just for you @NikolajBjorner
 2021-08-29 00:37:45 +01:00
Nikolaj Bjorner e3a83dd0dd Integrate fixes from #5512 
Pull request #5512 identifies a in line 1139 where the const-case-multiplier constructor returns false and does useless work.
In this update we also remove mk_const_multiplier because code path is subsumed by mk_const_case_multiplier.
 2021-08-28 10:46:45 -07:00