mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-15 00:46:38 +00:00
Code Activity
16020 commits 42 branches 51 tags 169 MiB
Commit graph

443 commits

Author SHA1 Message Date
Nikolaj Bjorner
9550321064 missed push lambdas 2021-12-31 16:33:06 -08:00
Nikolaj Bjorner
0ef0ed3b94 redoing arrays 2021-12-31 15:51:52 -08:00
Nikolaj Bjorner
aa901c4e88 axiom solver improvements 2021-12-31 11:53:40 -08:00
Nikolaj Bjorner
e8833f4dac working on relevancy=3 2021-12-30 17:07:14 -08:00
Nikolaj Bjorner
b87b464e69 set relevancy flag on enode 2021-12-29 17:57:28 -08:00
Nikolaj Bjorner
a90b66134d make roots uniform for theory lemmas 2021-12-29 13:42:11 -08:00
Nikolaj Bjorner
69b4392210 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-29 13:04:31 -08:00
Nikolaj Bjorner
f215b18e0e change registration mode for relevant_eh 2021-12-29 13:03:43 -08:00
Nikolaj Bjorner
1706f77b9e optimize propagation to only blocked literals 2021-12-28 18:53:37 -08:00
Nikolaj Bjorner
8ff8252e89 debug relevancy mode 2021-12-28 13:02:09 -08:00
Nikolaj Bjorner
743e56bda3 remove output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-28 12:08:10 -08:00
Nikolaj Bjorner
5ed27a6c38 fix initialization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-28 12:06:56 -08:00
Nikolaj Bjorner
28bce8f09c working on relevant 2021-12-28 11:00:02 -08:00
Nikolaj Bjorner
9527471967 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-27 16:03:56 -08:00
Nikolaj Bjorner
6f1be09993 add direct and incremental relevancy propagator 2021-12-27 15:10:33 -08:00
Nikolaj Bjorner
d88f125818 build 2021-12-26 15:24:03 -08:00
Nikolaj Bjorner
0bd6725711 #5641 
mark all literals duplicated in dual solver as external
 2021-12-26 15:10:21 -08:00
Nikolaj Bjorner
fcee2f5aa5 revert relevancy2 2021-12-26 15:10:21 -08:00
Nikolaj Bjorner
7d311ac2ef use netstandard 2.0 per recommendations 
seems that now the recommended starting point is 2.0 and not lower.
 2021-12-25 13:44:49 -08:00
Nikolaj Bjorner
71b868d7f6 #5722 - internalize unary xnor 2021-12-22 13:32:53 -08:00
Nikolaj Bjorner
4b5ee91b44 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-21 20:40:58 -08:00
Nikolaj Bjorner
f0740bdf60 move user propagte declare to context level 
declaration of user propagate functions are declared at context level instead of at solver scope.
 2021-12-18 10:56:42 -08:00
Nikolaj Bjorner
1e95fb44d1 add ability to register expressions during callback 2021-12-07 09:47:05 -08:00
Nikolaj Bjorner
fdc253afdd
update arithmetic contract for unbounded (#5696) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-06 08:19:18 -08:00
Nikolaj Bjorner
5857236f2f introducing base namespace for user propagator 2021-11-29 19:41:30 -08:00
Nikolaj Bjorner
1e9e52a58f #5641 2021-11-29 08:59:53 -08:00
Nikolaj Bjorner
d50bfc6a50 #5641 2021-11-25 18:01:35 +01:00
Nikolaj Bjorner
c826b64e35 prepare release 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-11-16 09:41:51 -08:00
Nikolaj Bjorner
dd1e0fc561 #5643 2021-11-03 08:53:48 -07:00
Nikolaj Bjorner
87d4ce2659 working on #5614 
there are some different sources for the performance regression illustrated by the example. The mitigations will be enabled separately:
- m_bv_to_propagate is too expensive
- lp_bound_propagator misses equalities in two different ways:
   - it resets row checks after backtracking even though they could still propagate
   - it misses equalities for fixed rows when the fixed constant value does not correspond to a fixed variable.

FYI @levnach
 2021-11-02 14:55:39 -07:00
Nikolaj Bjorner
a94e2e62af build warnings 2021-11-02 14:55:38 -07:00
Henrich Lauko
96671cfc73
Add and fix a few general compiler warnings. (#5628) 
* rewriter: fix unused variable warnings

* cmake: make missing non-virtual dtors error

* treewide: add missing virtual destructors

* cmake: add a few more checks

* api: add missing virtual destructor to user_propagator_base

* examples: compile cpp example with compiler warnings

* model: fix unused variable warnings

* rewriter: fix logical-op-parentheses warnings

* sat: fix unused variable warnings

* smt: fix unused variable warnings
 2021-10-29 15:42:32 +02:00
Alexander Traud
1d45a33163
fix one typo and two misunderstandings for doxygen (#5633) 2021-10-29 15:35:05 +02:00
Nikolaj Bjorner
86147d01ea #5605 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-19 12:24:29 -04:00
Nikolaj Bjorner
f9dde2e8a4 #5605 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-19 12:21:54 -04:00
Nikolaj Bjorner
fc3a701888 push-pop 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-18 15:36:48 -07:00
Nikolaj Bjorner
d5e5dcfe45 add nff and auto-relevant 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-18 15:32:55 -07:00
Nikolaj Bjorner
115203e87c fixes to sat.euf ematching #5573 2021-10-16 15:52:37 -07:00
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
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
cbe7dd4a48 missing continue fixes unsound sat result from #5573 2021-09-29 14:26:09 -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
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
6c71baf77b lifting iff to binary 2021-09-27 03:45:54 -07:00