mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-24 16:34:36 +00:00
Code Activity
16823 commits 43 branches 52 tags 176 MiB
Commit graph

16823 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Kartik Singhal
1dcbd2d86c
Correct capitalization of package (#5569) 
See https://stackoverflow.com/a/50004273/1167061
 2021-09-25 09:04:06 -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
Duncan Ogilvie
91fb646f55
Fix Z3Config.cmake.in when generating a static library (#5555) 2021-09-17 18:03:10 +01: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