3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-10 07:10:30 +00:00
Commit graph

10 commits

Author SHA1 Message Date
Nikolaj Bjorner
65464f5944 include order 2020-11-22 15:39:09 -08:00
Nikolaj Bjorner
367e5fdd52
delay internalize (#4714)
* adding array solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* use default in model construction

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* debug delay internalization

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* bv

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* arrays

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* get rid of implied values and bounds

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* redo egraph

* remove out

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove files

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-28 19:24:16 -07:00
Nikolaj Bjorner
629e981e01 fix regression in get-consequence on QF_FD
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-09-08 12:43:18 -07:00
Nikolaj Bjorner
59d8895d15 add accessors for implied values to API
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2020-07-28 19:46:39 -07:00
Nikolaj Bjorner
8893913c98 remove internal referenes to set_activity
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-05-30 16:06:05 -07:00
Nikolaj Bjorner
89bf2d4368 add API for setting variable activity
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-02-15 12:05:24 -08:00
Nikolaj Bjorner
8d20310758 adding trail/levels
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-29 14:45:51 -08:00
Nikolaj Bjorner
498864c582 adding dump facility for cancelation #2095, easing dimacs in/out
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-01-24 12:21:23 -08:00
Bruce Mitchener
cdfc19a885 Use nullptr. 2018-10-02 09:11:19 +07:00
Nikolaj Bjorner
e041ebbe80 bmc improvements, move fd_solver to self-contained directory
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-08-05 10:00:49 -07:00
Renamed from src/tactic/portfolio/enum2bv_solver.cpp (Browse further)