Nikolaj Bjorner
458f417f44
move drat functionality into euf
2022-08-25 19:19:13 -07:00
Nikolaj Bjorner
1ffbe23ee3
add virtual destructor to fix build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-25 18:37:24 -07:00
Nikolaj Bjorner
1894c86ee0
virtual
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-25 18:27:30 -07:00
Nikolaj Bjorner
ca0a82952f
add function pointer to class to see how MacOs build reacts
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-25 16:15:34 -07:00
Nikolaj Bjorner
0d7b7a417a
selectively re-add solver_params
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-25 13:29:42 -07:00
Nikolaj Bjorner
5f2387b3be
revert some changes that coincide with breaking macos build
2022-08-25 11:22:35 -07:00
Nikolaj Bjorner
a628e4c4e5
updates to printer to get instantiations, take 1
2022-08-25 11:22:35 -07:00
Nikolaj Bjorner
f0eee41ab9
include depenency
2022-08-25 09:09:04 -07:00
Jakob Rath
f819c2bad8
conflict2 stub
2022-08-25 17:04:07 +02:00
Jakob Rath
b31931bb9f
disable assertions for now; some notes
2022-08-25 16:40:38 +02:00
Jakob Rath
41b74ab215
newline is implicit
2022-08-25 16:37:38 +02:00
Jakob Rath
e39e1dcc49
Extract inference_logger
2022-08-25 16:03:17 +02:00
Nikolaj Bjorner
6c165e89dc
#6299
2022-08-24 20:25:01 -07:00
Nikolaj Bjorner
f6e151a49c
assert
2022-08-24 17:16:47 -07:00
Nikolaj Bjorner
d975886cdc
fix #6300
...
several boundary cases with repeated rows being retired twice and non-termination for K = 1 where decomposition is just identity.
2022-08-24 17:16:47 -07:00
Nikolaj Bjorner
fb8532bf55
succinct logging
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-23 21:06:04 -07:00
Nikolaj Bjorner
74c61f49b4
move std::function to header of sat-drat - alignment?
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-23 20:20:51 -07:00
Nikolaj Bjorner
c6263587c3
fix validator bug returning true for unprocessed case, bug reported in #6116
2022-08-23 20:17:32 -07:00
Nikolaj Bjorner
ce1f3987d9
fix unsoundness in quantifier propagation #6116 and add initial lemma logging
2022-08-23 19:10:01 -07:00
Nikolaj Bjorner
912b284602
disable validate_hint too permissive
2022-08-23 19:07:55 -07:00
Nikolaj Bjorner
2f8b13368d
add redirect for warnings
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-23 15:55:55 -07:00
Nikolaj Bjorner
fbf9e3004f
ack
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-23 10:16:13 -07:00
Nikolaj Bjorner
fbfb28eba9
update release notes
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-23 10:15:41 -07:00
Nikolaj Bjorner
437e83f6de
fixmul negative case
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-23 08:20:32 -07:00
Nuno Lopes
916d1dbb13
fix default parameter regression
...
bug introduced in commit 63f48f8fd4
2022-08-23 15:26:29 +01:00
Nuno Lopes
7ab904bfc6
remove spurious file
2022-08-23 14:39:44 +01:00
Nikolaj Bjorner
0eea021dc3
include global parameters and fixup for HTML meta-characters
2022-08-22 14:25:18 -07:00
Nikolaj Bjorner
8128ae8109
generalize subsumption to non-univariate
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-22 10:46:49 -07:00
Jakob Rath
058c5771b9
univariate solver: add_bit
2022-08-22 15:09:11 +02:00
Jakob Rath
d9a63ce786
fix
2022-08-22 15:05:29 +02:00
Jakob Rath
9fcea37625
remove constructor
2022-08-22 15:00:35 +02:00
Jakob Rath
28ddd4ad56
Implement unilinear subsumption as clause simplification
2022-08-22 14:55:02 +02:00
Jakob Rath
c1e2ea80f5
make explicit that we compare the concrete values
2022-08-22 14:17:47 +02:00
Jakob Rath
3a759c1a28
move fi_record
2022-08-22 14:14:30 +02:00
Jakob Rath
26fcfc6ecd
Add default constructor to fi_entry
2022-08-22 14:03:43 +02:00
Jakob Rath
3c093e03cf
log
2022-08-22 12:46:47 +02:00
Jakob Rath
53f276d225
apply
2022-08-22 12:44:56 +02:00
Jakob Rath
bf1a7914cd
Add clause simplification stub
2022-08-22 12:36:05 +02:00
Nikolaj Bjorner
f6e4a45f4b
Merge branch 'master' of https://github.com/z3prover/z3
2022-08-21 18:28:19 -07:00
Nikolaj Bjorner
64e0e785e7
#5953
2022-08-21 18:28:07 -07:00
Nikolaj Bjorner
09ab575d29
parens
2022-08-21 18:27:14 -07:00
Nikolaj Bjorner
daa24ef4ce
add missing error check
2022-08-21 18:26:53 -07:00
Nikolaj Bjorner
9eb4237dfe
fix #6292
...
this patches a case where macro-finder is used with arrays. It doesn't work so macro quantifiers have to be re-instated to ensure correctness
2022-08-21 16:32:01 -07:00
Nikolaj Bjorner
a38308792e
#6288
...
floating points may also track bit-literals.
Since the legacy solver doesn't handle dual tracking of literals we just let the floating point solver track.
2022-08-21 15:47:19 -07:00
Nikolaj Bjorner
4092302590
use interface for creating unary equalities
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-08-21 15:37:43 -07:00
Nikolaj Bjorner
17fc438476
don't have bv-ackerman influence simplification
...
previous scheme has Ackmerman module instrument main solver to backjump and simplify when reaching a threshold.
This destroys overall performance: simplification does many more things than invoking Ackerman axioms.
Having a dependency between simplification (in-processing) and depleting a priority queue of auxiliary axioms therefore hurts overall performance. It has to be decoupled. The current approach is now to empty the axiom queue on occasion.
It is still not ideal - it should be coupled with the search level - axioms don't survive higher levels where redundant clauses get garbage collected as they don't have a chance of being used.
2022-08-21 15:25:18 -07:00
Nikolaj Bjorner
be0cd74c71
#6289
2022-08-21 15:25:17 -07:00
Nikolaj Bjorner
2181a0ff74
#6289
2022-08-21 15:25:17 -07:00
Clemens Eisenhofer
56fb161532
ADT-constructor generation crashed in .NET/Java when no (= default) fields are given ( #6287 )
2022-08-21 12:40:38 -07:00
Bruce Mitchener
6ba9ada1e2
Fix typos. ( #6291 )
2022-08-21 12:40:07 -07:00
