mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
18165 commits 49 branches 53 tags 182 MiB
Commit graph

18165 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
a3d4e9a4e8 adding created to sat/smt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-20 11:48:27 +01:00
Jakob Rath
c9b9b5f531 remove obsolete test case 2022-01-19 19:10:10 +01:00
Jakob Rath
fa75a9109e Test forbidden intervals, disequal case 2022-01-19 19:06:35 +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
5b0389615b #5780 2022-01-19 10:10:36 +01:00
Nikolaj Bjorner
06feb71eb1 fix bug in root setting exposed by incremental mode pb_solver 2022-01-18 10:55:27 +01:00
Jakob Rath
175b348948 Update quot_rem axioms 2022-01-18 10:43:12 +01:00
Jakob Rath
e005838129 clause_builder should not fail on always-true literals 
Otherwise, e.g. when adding axioms, the caller would have to check each literal before adding it.
 2022-01-18 10:32:33 +01:00
Nikolaj Bjorner
36cfb88f5f add preliminary stub to handle closure types 2022-01-17 22:01:31 -08:00
Nikolaj Bjorner
d777306bb6 #5778 2022-01-17 10:43:15 -08:00
Jakob Rath
ebc4df1ece remove branch_bool 2022-01-17 15:57:05 +01:00
Nikolaj Bjorner
fcc9f379e7 #5778 2022-01-16 19:36:00 -08:00
Nikolaj Bjorner
a15da8f9ba #5778 2022-01-16 19:11:55 -08:00
Nikolaj Bjorner
637ddf9397 fix #5777 
latest issue
 2022-01-16 18:09:38 -08:00
Nikolaj Bjorner
0dd5a5e576 #5777 2022-01-16 17:46:08 -08:00
Nikolaj Bjorner
a48d3fdbb1 #5777 2022-01-16 14:01:49 -08:00
Nikolaj Bjorner
ea93345b75 #5777 2022-01-16 10:52:25 -08:00
Nikolaj Bjorner
cd56d55e34 #5753 2022-01-16 09:31:16 -08:00
Nikolaj Bjorner
bc9c6ad93d #5753 2022-01-15 18:01:31 -08:00
Nikolaj Bjorner
1b5f7cd9e5 na 2022-01-15 10:05:26 -08:00
Nikolaj Bjorner
17cfc1d034 #5753 2022-01-15 10:03:03 -08:00
Nikolaj Bjorner
74824ac901 #5753 
get_antecedent has to be well-founded. It got broken when using eval during propagation and egraph explain during conflict resolution.
 2022-01-15 09:35:25 -08: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
d5cc162fa7 bug in bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-13 15:42:23 -08:00
Nikolaj Bjorner
2363bfc132 internalize arithmetic sub-terms #5753 2022-01-13 15:34:04 -08:00
Nikolaj Bjorner
e816946ddc handling unsimplified input 2022-01-13 14:40:46 -08:00
Nikolaj Bjorner
b259f46f85 dependencies 2022-01-13 12:34:58 -08:00
Nikolaj Bjorner
4b6679e8e0 #5753 2022-01-13 12:19:54 -08:00
Nikolaj Bjorner
366cd9b16d missing pb cases 2022-01-12 14:50:40 -08:00
Nikolaj Bjorner
dfe2b27f9a #5773 2022-01-12 13:28:15 -08:00
Nikolaj Bjorner
0720998bac #5753 2022-01-12 13:12:10 -08:00
Nikolaj Bjorner
10dc8d7313 #5753 2022-01-12 12:49:06 -08:00
Jakob Rath
3a34995b03 Add eval_and 2022-01-12 13:47:05 +01:00
Jakob Rath
3895d8d6bb quot_rem needs additional constraint: quot <= a 2022-01-12 13:44:30 +01:00
Jakob Rath
e0e03b3fc5 Wrap polysat tests in class 2022-01-12 13:42:04 +01: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
08294d62e5 separate dependencies for qe_lite 2022-01-12 03:26:22 -08:00
Nikolaj Bjorner
2bcc814031 add macro to track closures declared in z3_api 
This is to ease integration with external API wrappers that rely on accessing
information about type names that are used.
#5762
 2022-01-12 02:47:39 -08:00
Nikolaj Bjorner
e5eaea46aa ensure m_true is assigned #5753 2022-01-11 10:42:05 -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
571a74c061 counting function applications #5766 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-10 14:51:25 -08:00
Nikolaj Bjorner
4cd818b578 #5766 2022-01-10 14:40:27 -08:00
Nikolaj Bjorner
d3bc11dd3a bvs have to be expressions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-10 12:38:25 -08:00
Nikolaj Bjorner
21feefeac5 Add character access functions #5764 2022-01-10 12:33:58 -08:00