mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 00:55:31 +00:00
Code Activity
16124 commits 23 branches 48 tags 157 MiB
Commit graph

3851 commits

Author SHA1 Message Date
Nikolaj Bjorner
af9ae35984 term 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-20 14:43:16 +01:00
Nikolaj Bjorner
c527fda0b6 term 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-20 14:41:27 +01:00
Nikolaj Bjorner
f1a302bba7 term 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-20 14:38:34 +01:00
Nikolaj Bjorner
7a8c969033 ensure b_internalized 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-20 13:27:23 +01:00
Nikolaj Bjorner
c00591daaf finish is-fixed 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-19 16:28:34 +01:00
Nikolaj Bjorner
e5767bf2b8 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-19 15:19:07 +01:00
Nikolaj Bjorner
0f03ef4ab0 for Clemens: ensure fixed values are propagated after registration 
Also allow to register expressions that the rewriter changes to ensure they get picked up.
 2022-01-19 14:38:11 +01:00
Nikolaj Bjorner
d09abdf58e fix #5771 
Missing congruence closure enforcement on auxiliary guard predicates.
It diverges but is sound.
 2022-01-14 15:46:40 -08:00
Nikolaj Bjorner
56d3718cde add simplification with qe-lite as an option #5767 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-12 03:41:21 -08:00
Nikolaj Bjorner
dbd5512d8c ensure enode without recursion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-11 08:35:57 -08:00
Nikolaj Bjorner
055732423c ensure enode without recursion 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-11 08:35:25 -08:00
Nikolaj Bjorner
0bc8518cb5 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-07 11:53:27 -08:00
Nikolaj Bjorner
199daead50 remove Z3_bool_opt #5757 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-07 11:52:10 -08:00
Nikolaj Bjorner
592b1d7f65 #5752 2022-01-06 13:32:50 -08:00
Nikolaj Bjorner
d7c7fbb8f1 setting roots breaks relevancy propagation 2022-01-05 21:16:25 -08:00
Nikolaj Bjorner
9d3c8a6a2f na 2022-01-01 17:59:31 -08:00
Nikolaj Bjorner
fc77345bec breaking change. Enforce append semantics everywhere for parameter updates #5744 
Replace semantics doesn't work with assumptions made elsewhere in code.
The remedy is to apply append (override) semantics for parameter changes.
 2021-12-30 19:11:14 -08:00
Nikolaj Bjorner
d88f125818 build 2021-12-26 15:24:03 -08:00
Nikolaj Bjorner
09ee60ccce update comment 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-21 11:04:07 -08:00
Nikolaj Bjorner
4b813bac1c na 2021-12-19 12:31:47 -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
4856581b68 na 2021-12-17 16:40:19 -08:00
Nikolaj Bjorner
8ca023d541 expose propagate created 2021-12-17 16:12:47 -08:00
Nikolaj Bjorner
9c8800bdde adding a new toy for Clemens 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-17 10:45:59 -08:00
Nikolaj Bjorner
6cc9aa3562 prepare user propagator declared functions for likely Clemens use case 2021-12-16 19:37:30 -08:00
Nikolaj Bjorner
dd6a11b526 fix #5715 2021-12-16 09:35:54 -08:00
Nikolaj Bjorner
3b58f548f7 remove dead code 2021-12-14 13:42:52 -08:00
Nikolaj Bjorner
b1d167de5b fix co-factoring' 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-14 10:12:38 -08:00
Nikolaj Bjorner
5348af3c4c fix co-factoring 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-14 10:05:09 -08:00
Nikolaj Bjorner
f40becf099 remove case for non-emptiness to combine with standard membership 
as part of revising engine for addressing #5693
 2021-12-13 18:17:40 -08:00
Nikolaj Bjorner
b2af7ea68f stdout 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-13 15:19:29 -08:00
Nikolaj Bjorner
9ec0f94ab9 hoisting out blocker for empty 
#5693
 2021-12-13 14:25:05 -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
1e95fb44d1 add ability to register expressions during callback 2021-12-07 09:47:05 -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
f0e9363e78 fix bug in smt_tactic_core for translating user-ids 2021-12-05 11:13:27 -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
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
bfd61fec00 enable user propagation on tactics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-12-02 08:28:52 -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
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