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
Jakob Rath
c78007fd1a
Use mul_ovfl constraint directly instead of approximating it with bounds
2022-06-29 14:28:59 +02:00
Jakob Rath
69a28a7740
fix check against looping
2022-06-29 14:27:11 +02:00
Jakob Rath
0fb8c72f50
print more information
2022-06-29 14:26:25 +02: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
