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

16697 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner b618537322 Merge branch 'master' of https://github.com/z3prover/z3 2022-06-30 19:49:28 -07:00
Nikolaj Bjorner 94a2477fa0 totalizer 2022-06-30 19:49:19 -07:00
Nikolaj Bjorner 959a0ba370 fix #6121 2022-06-30 19:47:26 -07:00
Mark Marron e054f1683c
fixing compiler warn (missing override) (#6125) 2022-06-30 15:39:28 -07:00
Nikolaj Bjorner c3d2120bdd add totalizer version of rc2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-29 23:10:42 -07:00
Nikolaj Bjorner 8ab8b63a4c fix incorrect mod axiomatization #6116 2022-06-29 12:32:04 -07:00
Nikolaj Bjorner f6932f9a75 Merge branch 'master' of https://github.com/z3prover/z3 2022-06-29 11:16:34 -07:00
Nikolaj Bjorner 1a9122663c remove unsound axioms, fix #6115 2022-06-29 11:16:10 -07:00
Joe Hauns 03287d65a4
fixes issue #6119 (#6120) 
Co-authored-by: Johannes Schoisswohl <johannes.schoisswohl@myotis.at>
 2022-06-29 11:10:33 -07:00
Nikolaj Bjorner ff265235c1 adjust trace output 2022-06-29 08:20:01 -07:00
Nikolaj Bjorner 5afcb489e0 adding totalizer 2022-06-29 08:20:01 -07:00
Nikolaj Bjorner fd8ee34564 add logging 2022-06-29 08:20:01 -07:00
Max Levatich 12e7b4c3d6
fix gc'ed callbacks in .NET propagator api (#6118) 
Co-authored-by: Maxwell Levatich <t-mlevatich@microsoft.com>
 2022-06-28 19:22:41 -07:00
Nikolaj Bjorner 79778767b0 add doc string 2022-06-28 14:25:43 -07:00
Nikolaj Bjorner 798a4ee86e use IEnumerator and format 2022-06-28 14:24:05 -07:00
Nikolaj Bjorner 556f0d7b5f use static list to connect managed and unmanaged objects 2022-06-28 14:09:22 -07:00
Nikolaj Bjorner 820c782b5e pinned semantics 2022-06-28 13:03:52 -07:00
Nikolaj Bjorner 9836d5e6fc missing public 2022-06-28 12:46:29 -07:00
Nikolaj Bjorner b43965bf05 make user propagator work with combined solver 
Then users don't have to specify SImpleSolver, but can use "Solver"
 2022-06-28 09:42:28 -07:00
Nikolaj Bjorner 4c8f6b60ce fix #6107 2022-06-27 20:51:30 -07:00
Nikolaj Bjorner 61f5489223 fix #6107 2022-06-27 16:53:18 -07:00
Nikolaj Bjorner 1fcf7cf0b7 add nl div mod axioms 2022-06-27 09:02:53 -07:00
Nikolaj Bjorner 30165ed40a fix #6105 
non-linear division axioms appear incomplete.
Fixed for legacy arithmetic. Fix pending for new arithmetic solver.
 2022-06-26 20:37:18 -07:00
Nikolaj Bjorner 56aa4261b6 fix #6082 2022-06-23 07:43:06 -07:00
Kevin Gibbons 352666b19f
JS api: fix type for from (#6103) 
* JS api: fix type for from

* whitespace
 2022-06-22 14:51:40 -07:00
Kevin Gibbons c15a000d9b
Make high-level JS API more idiomatic/type-safe (#6101) 
* make JS api more idiomatic

* make JS api type-safe by default

* use strings, not symbols, for results

* add toString

* add miracle sudoku example

* ints should be ints

* add error handling

* add missing Cond to Context

* fewer side-effecting getters
 2022-06-22 09:26:44 -07:00
Nikolaj Bjorner 8234eeae40 unbreak 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-22 09:03:32 -07:00
Nikolaj Bjorner 3189544050 next split 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-22 09:03:32 -07:00
Felix Kohlgrüber a7b41c49fe
fix for spurious wakeups in scoped_timer (#6102) 2022-06-22 10:50:19 +01:00
Nuno Lopes 41deed59a3 fix bug in array rewriter introduced in 202ce1e 2022-06-21 22:40:40 +01:00
Nikolaj Bjorner 36a1f758bc mask regression 2022-06-21 14:34:47 -07:00
Nikolaj Bjorner ab9aee189b perf #6100 2022-06-21 13:49:52 -07:00
Nikolaj Bjorner 202ce1edf0 #6100 - two perf fixes 
remaining perf bug is dealing with very large bit-widths. mod 2^n should be computed natively based on n instead of 2^n because we pre-populate an array with all values up to n. Suppose n is 10000, the array has size 10000.
 2022-06-21 12:45:29 -07:00
Nikolaj Bjorner f24c5ca99a #6095 
arrays that are interpreted using as-array should be reflected back to store expressions
 2022-06-21 12:42:44 -07:00
Nikolaj Bjorner 5ba8231d07 make it work with old pythons 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-21 09:10:38 -07:00
Nikolaj Bjorner d792d30e88 Update NativeContext.cs 
TraceToFile does not correspond to the functionality of enable_trace. Z3_enable_trace tags a trace tag as input. It can be invoked multiple times with different tags. The debug tracing then shows logs with the corresponding tags.
 2022-06-21 09:09:42 -07:00
Nikolaj Bjorner b254f4086b Separate out native static content for Java 
Make it easier to add native methods for callbacks (for user propagator) #6097

The Java User propagator wrapper should define a base class with virtual methods that can be invoked from functions defined in NativeStatic.txt
 2022-06-21 09:09:42 -07:00
Nuno Lopes 25e915fe95 fix #5990: deadlock in the scoped_timer 
Thanks to Felix Kohlgrueber for reporting the bug and for the analysis
 2022-06-21 16:29:09 +01:00
Nikolaj Bjorner 911134b3c7 add new heuristic rc2bin (to be tested) to maxsat 
The rc2bin heuristic is a hybrid of rc2 and binary maxres.
It follows the suggestion by Nina to use rc2 on large cores after a single maxres relaxation step; otherwise maxres (binary) on smaller cores. In the design space of possible hybrids, this variant chooses to always apply a single layer of maxres and then rc2 for large cores.
 2022-06-20 11:50:25 -07:00
AndreiL 940d10ae6d
Update coverage CI (#6099) 
Ignore errors withing `gcov` when using `gcovr`, as per
https://github.com/gcovr/gcovr/issues/627.

Co-authored-by: Andrei Lascu <al2510@bencher14.nms.kcl.ac.uk>
 2022-06-20 11:38:38 -07:00
Clemens Eisenhofer 2fa60aa43c
Added function to select the next variable to split on (User-Propagator) (#6096) 
* Added function to select the next variable to split on

* Fixed typo

* Small fixes

* uint -> int
 2022-06-19 10:49:25 -07:00
Nuno Lopes f08e3d70a9 attempt to fix windows build bot 2022-06-17 21:15:54 +01:00
Nuno Lopes f3c00a0a03 attempt to fix windows build bot 2022-06-17 18:05:19 +01:00
Nuno Lopes c3407fc304 fix build of tests 2022-06-17 17:11:18 +01:00
Nuno Lopes fcbbf7ba76 fix build warning+error in c++ example 2022-06-17 16:43:34 +01:00
Nuno Lopes d9fcfdab34 fix debug build 2022-06-17 14:35:33 +01:00
Nuno Lopes 73a24ca0a9 remove '#include <iostream>' from headers and from unneeded places 
It's harmful to have iostream everywhere as it injects functions in the compiled files
 2022-06-17 14:10:19 +01:00
Nuno Lopes 70bcf0b51d reduce sizeof(enode) from 120 to 112 bytes by swapping the order of fields 
Yes, those 8 bytes are yours now, use responsibly.
 2022-06-17 12:07:15 +01:00
Nikolaj Bjorner 08c44bc6f6 remove unused static features 
remove static features that tax solving time on large instances.
 2022-06-16 15:40:01 -07:00
Nikolaj Bjorner 477e9625ef Don't reset the cache between applications of replace 
tactic/lia2card shows a huge slowdown because the same replace function is called on thousands of assertions. Each time the cache gets reset with thousands of entries - they are all the same.
So don't reset the cache just because... Instead reset the cache if m_refs grows large.
 2022-06-16 15:40:01 -07:00