Nikolaj Bjorner
d74ff29c25
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-12-07 13:55:31 -08:00
Nikolaj Bjorner
9f2b18cac5
add tactic name
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-12-07 13:37:57 -08:00
Nikolaj Bjorner
e3bd5badf2
pass through for unary tactical
2021-12-07 10:45:03 -08:00
Nikolaj Bjorner
1e95fb44d1
add ability to register expressions during callback
2021-12-07 09:47:05 -08:00
Nikolaj Bjorner
50d50cdb48
register forbidden functions with reduce_args for user-propagator
2021-12-07 09:03:19 -08:00
Nikolaj Bjorner
658a334ecf
clear tactic user propagate state on solver destructor
2021-12-07 03:14:50 -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
Lev Nachmanson
9b4f3a7075
start using lar_solver::is_feasible() ( #5697 )
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2021-12-06 08:16:57 -08:00
Lev Nachmanson
7758b519bc
Handle correctly cancelled run ( #5695 )
...
* remove the bound on total iterations in simplex
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* remove unncesseray checks in get_freedom_interval_for_column()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* fix the build of test-z3
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* Revert "remove unncesseray checks in get_freedom_interval_for_column()"
This reverts commit 6770ed85e3
.
* optimize get_freedom_interval_for_column() for feasible case
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* add function lar_solver::status_feasible
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* rename status_is_feasible() to is_feasible()
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
* fix the linux build
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2021-12-05 18:38:37 -08:00
Nikolaj Bjorner
0242566792
remove
2021-12-05 11:54:05 -08:00
Nikolaj Bjorner
f0e9363e78
fix bug in smt_tactic_core for translating user-ids
2021-12-05 11:13:27 -08:00
Nikolaj Bjorner
0d055b83eb
update input for doxygen #5400
2021-12-05 09:04:18 -08:00
Nikolaj Bjorner
c845b22c15
fix translation for equality propagation
2021-12-04 11:55:36 -08:00
Nikolaj Bjorner
1b0ac4940b
prevent stale user-propagators from being used on the same tactic after it was applied.
2021-12-04 11:51:00 -08:00
Nikolaj Bjorner
da765355e8
don't rely on cleanup
2021-12-04 11:48:41 -08:00
Nikolaj Bjorner
3d528c8ef6
typo
2021-12-04 11:19:49 -08:00
Nikolaj Bjorner
eae567ac3d
indirection for user ids
2021-12-04 11:04:32 -08:00
Nikolaj Bjorner
68b072e7f1
only use setup_and_check if there is no user propagator set.
2021-12-04 09:22:25 -08:00
Nikolaj Bjorner
1618c970df
adding checks
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-12-03 13:17:48 -08:00
Nikolaj Bjorner
970347e797
infeas
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-12-03 13:00:52 -08:00
Nikolaj Bjorner
0077ddf33c
try delay init for user propagator in smt_tactic
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-12-03 09:45:07 -08:00
Nikolaj Bjorner
41aa7d7b60
stack
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-12-02 09:00:51 -08:00
Nikolaj Bjorner
bfd61fec00
enable user propagation on tactics
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-12-02 08:28:52 -08:00
Matteo Nicoli
cbdd7b0696
three smt2 examples added and one python example updated ( #5690 )
2021-12-01 16:21:12 -08:00
Nikolaj Bjorner
71cbb160d2
fix regression from today, see #5676
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-12-01 14:29:53 -08:00
Nikolaj Bjorner
87aec8819f
fix #5687
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-12-01 10:08:29 -08:00
Nikolaj Bjorner
c6a5aa0cc4
try th_lemma, update documentation of api functions for creating strings
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-12-01 09:21:02 -08:00
Nikolaj Bjorner
3b4f976118
na
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-11-30 19:15:03 -08:00
Nikolaj Bjorner
4daba290b1
change user propagation to apply scheme similar to theory_recfun
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-11-30 19:12:15 -08:00
Nikolaj Bjorner
3c1aedf219
fixing #5473
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-11-30 17:08:28 -08:00
Nikolaj Bjorner
9e51691285
add virtual destructor
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-11-29 20:02:12 -08:00
Nikolaj Bjorner
b5efb87118
base -> core
2021-11-29 19:55:10 -08:00
Nikolaj Bjorner
959f4c9440
rename files to theory_user_propagator
2021-11-29 19:44:58 -08:00
Nikolaj Bjorner
5857236f2f
introducing base namespace for user propagator
2021-11-29 19:41:30 -08:00
Nikolaj Bjorner
c083aa82ee
add debug information in user-propagate #5687
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-11-29 08:59:53 -08:00
Nikolaj Bjorner
1e9e52a58f
#5641
2021-11-29 08:59:53 -08:00
Lev Nachmanson
d50c4bfcc1
remove an unused var
...
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2021-11-28 09:44:50 -08:00
Nikolaj Bjorner
d50bfc6a50
#5641
2021-11-25 18:01:35 +01:00
Nikolaj Bjorner
833dd62623
fix #5681
2021-11-24 13:24:31 +01:00
Nikolaj Bjorner
e8f5a29c31
fix #5679
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-11-22 19:37:10 +01:00
Nikolaj Bjorner
fee4821106
include thread
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-11-19 21:06:07 +01:00
Nikolaj Bjorner
a7d24788c3
wasm build issue
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-11-19 20:45:36 +01:00
Nikolaj Bjorner
741c5f43f4
Merge branch 'master' of https://github.com/z3prover/z3
2021-11-19 11:03:08 -08:00
Nikolaj Bjorner
ca2c2bb802
ensure smt2log works with multi-threaded consumers, ease scenarios around #5655
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-11-19 11:02:50 -08:00
Nikolaj Bjorner
4928c28e63
fix #5675
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-11-19 08:42:32 -08:00
Nikolaj Bjorner
99d5215956
revert use of f format
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-11-19 00:01:19 -08:00
Nikolaj Bjorner
f83367a11e
mac builds
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-11-18 22:39:30 -08:00
Nikolaj Bjorner
518ef9f916
fix #5674
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-11-18 21:14:50 -08:00
Nikolaj Bjorner
4587575649
if you read this commit message you probably are a programmer who has no life
...
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2021-11-18 20:25:47 -08:00
Nikolaj Bjorner
43a827c931
Update release.yml for Azure Pipelines
2021-11-18 16:05:22 -08:00