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

1713 commits

Author SHA1 Message Date
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
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
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
3e6ff768a5 fix regression bug in mam reported by Aseem 2021-09-10 07:09:22 +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
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
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
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
af5c6e43b9 #5528 2021-09-02 11:21:57 -07:00
Nikolaj Bjorner
e9a4a9a390 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-02 09:23:59 -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
6907d30717 #5528 2021-09-01 20:44:00 -07:00
Nikolaj Bjorner
a74c01c8b9 #5528 2021-09-01 20:39:54 -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
a3ba4e1366 #5528 2021-09-01 11:34:44 -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