Nikolaj Bjorner
e943bee625
apply delcypher's todo
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-04 20:25:14 -08:00
Nikolaj Bjorner
d1fb831030
relevancy overhaul
2022-01-04 16:03:31 -08:00
Nikolaj Bjorner
4a1975053f
cleanup
2022-01-03 17:37:04 -08:00
Nikolaj Bjorner
614c66f1e2
missing relevancy propagation
2022-01-03 17:21:37 -08:00
Nikolaj Bjorner
fc741cf018
rename module
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-03 14:23:22 -08:00
Nikolaj Bjorner
a2a5924e5c
purge more
2022-01-03 14:14:09 -08:00
Nikolaj Bjorner
8e3185ffe3
remove dual solver approach
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-03 14:08:01 -08:00
Nikolaj Bjorner
cf08cdff9c
#5747
2022-01-03 08:54:54 -08:00
Nikolaj Bjorner
a71aa113e0
#5641
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-02 19:36:17 -08:00
Nikolaj Bjorner
9cbec3b0ca
#5641
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-02 19:15:23 -08:00
Nikolaj Bjorner
43e449a805
#5641
2022-01-02 17:53:26 -08:00
Nikolaj Bjorner
d0fb3cba15
#5641 - projection that skips interpreted functions can violate model evaluation.
2022-01-02 17:45:43 -08:00
Nikolaj Bjorner
5cd1fe31fd
propagate parent default not add parent default)
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2022-01-01 20:37:26 -08:00
Nikolaj Bjorner
8245935d41
#5641 add handlers for basic set operations to euf=true
2022-01-01 20:33:17 -08:00
Nikolaj Bjorner
84f514a4f4
throttle ackerman on arrays
2022-01-01 15:33:33 -08:00
Nikolaj Bjorner
a20b577b2f
na
2022-01-01 11:26:38 -08:00
Nikolaj Bjorner
9550321064
missed push lambdas
2021-12-31 16:33:06 -08:00
Nikolaj Bjorner
0ef0ed3b94
redoing arrays
2021-12-31 15:51:52 -08:00
Nikolaj Bjorner
aa901c4e88
axiom solver improvements
2021-12-31 11:53:40 -08:00
Nikolaj Bjorner
e8833f4dac
working on relevancy=3
2021-12-30 17:07:14 -08:00
Nikolaj Bjorner
b87b464e69
set relevancy flag on enode
2021-12-29 17:57:28 -08:00
Nikolaj Bjorner
a90b66134d
make roots uniform for theory lemmas
2021-12-29 13:42:11 -08:00
Nikolaj Bjorner
69b4392210
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-12-29 13:04:31 -08:00
Nikolaj Bjorner
f215b18e0e
change registration mode for relevant_eh
2021-12-29 13:03:43 -08:00
Nikolaj Bjorner
1706f77b9e
optimize propagation to only blocked literals
2021-12-28 18:53:37 -08:00
Nikolaj Bjorner
8ff8252e89
debug relevancy mode
2021-12-28 13:02:09 -08:00
Nikolaj Bjorner
743e56bda3
remove output
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-12-28 12:08:10 -08:00
Nikolaj Bjorner
5ed27a6c38
fix initialization
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-12-28 12:06:56 -08:00
Nikolaj Bjorner
28bce8f09c
working on relevant
2021-12-28 11:00:02 -08:00
Nikolaj Bjorner
9527471967
build
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-12-27 16:03:56 -08:00
Nikolaj Bjorner
6f1be09993
add direct and incremental relevancy propagator
2021-12-27 15:10:33 -08:00
Nikolaj Bjorner
d88f125818
build
2021-12-26 15:24:03 -08:00
Nikolaj Bjorner
0bd6725711
#5641
...
mark all literals duplicated in dual solver as external
2021-12-26 15:10:21 -08:00
Nikolaj Bjorner
fcee2f5aa5
revert relevancy2
2021-12-26 15:10:21 -08:00
Nikolaj Bjorner
7d311ac2ef
use netstandard 2.0 per recommendations
...
seems that now the recommended starting point is 2.0 and not lower.
2021-12-25 13:44:49 -08:00
Nikolaj Bjorner
71b868d7f6
#5722 - internalize unary xnor
2021-12-22 13:32:53 -08:00
Nikolaj Bjorner
4b5ee91b44
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-12-21 20:40:58 -08:00
Nikolaj Bjorner
f0740bdf60
move user propagte declare to context level
...
declaration of user propagate functions are declared at context level instead of at solver scope.
2021-12-18 10:56:42 -08:00
Nikolaj Bjorner
1e95fb44d1
add ability to register expressions during callback
2021-12-07 09:47:05 -08:00
Nikolaj Bjorner
fdc253afdd
update arithmetic contract for unbounded ( #5696 )
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-12-06 08:19:18 -08:00
Nikolaj Bjorner
5857236f2f
introducing base namespace for user propagator
2021-11-29 19:41:30 -08:00
Nikolaj Bjorner
1e9e52a58f
#5641
2021-11-29 08:59:53 -08:00
Nikolaj Bjorner
d50bfc6a50
#5641
2021-11-25 18:01:35 +01:00
Nikolaj Bjorner
c826b64e35
prepare release
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-11-16 09:41:51 -08:00
Nikolaj Bjorner
dd1e0fc561
#5643
2021-11-03 08:53:48 -07:00
Nikolaj Bjorner
87d4ce2659
working on #5614
...
there are some different sources for the performance regression illustrated by the example. The mitigations will be enabled separately:
- m_bv_to_propagate is too expensive
- lp_bound_propagator misses equalities in two different ways:
- it resets row checks after backtracking even though they could still propagate
- it misses equalities for fixed rows when the fixed constant value does not correspond to a fixed variable.
FYI @levnach
2021-11-02 14:55:39 -07:00
Nikolaj Bjorner
a94e2e62af
build warnings
2021-11-02 14:55:38 -07:00
Henrich Lauko
96671cfc73
Add and fix a few general compiler warnings. ( #5628 )
...
* rewriter: fix unused variable warnings
* cmake: make missing non-virtual dtors error
* treewide: add missing virtual destructors
* cmake: add a few more checks
* api: add missing virtual destructor to user_propagator_base
* examples: compile cpp example with compiler warnings
* model: fix unused variable warnings
* rewriter: fix logical-op-parentheses warnings
* sat: fix unused variable warnings
* smt: fix unused variable warnings
2021-10-29 15:42:32 +02:00
Alexander Traud
1d45a33163
fix one typo and two misunderstandings for doxygen ( #5633 )
2021-10-29 15:35:05 +02:00
Nikolaj Bjorner
86147d01ea
#5605
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-10-19 12:24:29 -04:00
