Nikolaj Bjorner
6e1ac19c44
new name
2021-04-07 17:43:32 -07:00
Nikolaj Bjorner
90995b63c3
fix nightly
2021-04-07 15:43:39 -07:00
Nikolaj Bjorner
d9af8ea9fb
fix #5113
2021-04-07 12:20:12 -07:00
Nikolaj Bjorner
a99e75f58f
fix #5154
2021-04-07 11:28:51 -07:00
Nikolaj Bjorner
46831e7ebb
provisionary fix for #5127
2021-04-06 22:32:22 -07:00
Nikolaj Bjorner
dcfd9c859d
fix build
2021-04-06 21:30:13 -07:00
Nikolaj Bjorner
1b503b8887
na
2021-04-06 20:09:51 -07:00
Nikolaj Bjorner
0b0efa83ca
debugging #5127
2021-04-06 20:09:50 -07:00
Nikolaj Bjorner
e5e663e874
fix for #5153
2021-04-06 20:09:50 -07:00
Nikolaj Bjorner
a832ada3d1
fix #5152
2021-04-06 20:09:50 -07:00
Nikolaj Bjorner
6099b84ff6
fix #5149
2021-04-06 20:09:49 -07:00
Nuno Lopes
a6ef99d56e
constify ids of builtin AST families + remove some dead code
2021-04-04 18:13:52 +01:00
Nuno Lopes
c47ab023e5
remove a few trivial destructors so they get inlined
2021-04-04 17:13:59 +01:00
Nikolaj Bjorner
c0e74f946b
patch to fix #5145
...
underlying issue is that model updates for multi-objective and single objective solving are too brittle to serve its use cases among different plugins.
For maxlex, the last model is always the best and it doesn't use multiple objectives.
2021-04-02 12:23:01 -07:00
Nikolaj Bjorner
cebf83c460
fix #5146
2021-04-02 11:48:44 -07:00
Nikolaj Bjorner
1fc9a7ba84
fix regression, fix #5115
2021-03-30 17:43:12 -07:00
Nikolaj Bjorner
1fcd537d81
fix #5117
2021-03-30 14:23:30 -07:00
Nikolaj Bjorner
c71bbb6391
fix #5136 , regression when removing variable registration for mod/div operations
2021-03-30 13:45:54 -07:00
Nikolaj Bjorner
c629f09f21
fix #5139
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-03-29 15:46:47 -07:00
Nikolaj Bjorner
94b4d1b442
fix travis build for python doc
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-03-29 15:30:31 -07:00
Nikolaj Bjorner
2fdb703865
remove redundant assertion
2021-03-29 15:17:01 -07:00
Nikolaj Bjorner
5cc29bec14
simplify ""* to ""
2021-03-29 14:18:57 -07:00
Nikolaj Bjorner
6d28b1a858
fix #5134
2021-03-29 14:11:49 -07:00
Nikolaj Bjorner
6bdf377e11
remove unneeded assertion fix #5131
2021-03-28 21:20:05 -07:00
Nikolaj Bjorner
dfb696becf
fix #5119
2021-03-28 16:47:56 -07:00
Nikolaj Bjorner
974ef3c147
port equality propagation changes to new core
2021-03-28 16:15:04 -07:00
Nikolaj Bjorner
0432311b11
fix #5121
2021-03-28 16:14:37 -07:00
Nikolaj Bjorner
6aa766a544
fix perf regression for new arithmetic solver, missing equality propagation #5106
2021-03-28 14:17:50 -07:00
Nikolaj Bjorner
d6691830c7
fix perf regression for new solver, missing equality propagations #5106
2021-03-28 14:17:50 -07:00
Nikolaj Bjorner
bb2c40072e
skip div 1
2021-03-28 14:17:49 -07:00
Nikolaj Bjorner
22d66f57f1
pp
2021-03-28 14:17:49 -07:00
Zachary Wimer
531a828c57
Update setup.py to use cmake build system ( #5128 )
2021-03-28 14:17:33 -07:00
Nikolaj Bjorner
0c25d2560d
improve diagnosability
2021-03-26 14:58:25 -07:00
Nikolaj Bjorner
e89071d366
#5125
2021-03-26 14:58:24 -07:00
Nikolaj Bjorner
c2b353ba72
adding factorization
2021-03-26 14:58:24 -07:00
Nikolaj Bjorner
a352a6638a
fix #5126
2021-03-26 14:58:24 -07:00
Nikolaj Bjorner
7fab0f5923
updated experiment
2021-03-26 14:58:23 -07:00
Luca Bruno
b918f121ef
zstring: fix encode rountrip for '\' as printable ASCII ( #5120 )
...
This fixes encode roundtripping for all printable ASCII characters.
In particular, this now leaves a plain '\' untouched by the
encoding logic, instead of converting it to escaped hex-digits.
It also adds unit testing covering this specific zstring encoding
property, in order to avoid future regressions.
2021-03-23 11:25:59 -07:00
Luca Bruno
119c5a995b
cmake/git: tweak submodule detection logic ( #5118 )
...
This removes an incomplete check in cmake git-submodule detection
logic, directly using filepath probing instead. As a direct usecase,
it fixes submodule building for https://github.com/prove-rs/z3.rs .
2021-03-22 16:10:17 -07:00
Nikolaj Bjorner
67e419d20d
yada yada
2021-03-21 19:57:17 -07:00
Nikolaj Bjorner
2ee971ef68
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-03-21 12:32:01 -07:00
Nikolaj Bjorner
2fef6dc502
more scaffolding
2021-03-21 11:31:14 -07:00
Nikolaj Bjorner
a1f484fa35
na
2021-03-19 16:42:45 -07:00
Nikolaj Bjorner
731cf9b885
ensure compilation
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-03-19 15:37:05 -07:00
Nikolaj Bjorner
560f072786
elaborate on header
2021-03-19 14:26:52 -07:00
Lev Nachmanson
3b67dd8288
add a trace statement
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2021-03-19 13:17:27 -07:00
Nikolaj Bjorner
1971ee60e1
Create polysat.h
2021-03-19 11:15:06 -07:00
Nikolaj Bjorner
15a7621e27
remove template dependency for trail objects
2021-03-19 11:15:05 -07:00
Nikolaj Bjorner
c05c5caab5
fix #5111
2021-03-19 11:15:04 -07:00
Murphy Berzish
064b1f0721
z3str3: address code reviews and remove some dead code ( #5116 )
2021-03-19 10:37:16 -07:00