Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Qf eq bv arith #444

Merged
merged 39 commits into from
Sep 28, 2023
Merged

Qf eq bv arith #444

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
39 commits
Select commit Hold shift + click to select a range
22f5067
minor typo
ahmed-irfan May 18, 2023
c427088
add qf_ufbvlia logic
ahmed-irfan May 19, 2023
ee9b94c
add qf_aufbvlia and qf_aufbvnia
ahmed-irfan May 19, 2023
90326b9
test qf_aufbvnia
ahmed-irfan May 19, 2023
01ac83a
move mcsat tests
ahmed-irfan May 19, 2023
418ce21
Merge branch 'master' into qf-eq-bv-arith
ahmed-irfan Jun 13, 2023
a1f6a55
add test
ahmed-irfan Jun 13, 2023
7bdddbe
Update NOTES -- fix typo
ahmed-irfan Jul 13, 2023
7f0ebab
install guide for kissat
ahmed-irfan Jul 8, 2023
b6e27f3
add missing EF errors
ahmed-irfan Jul 9, 2023
504851e
interpolats in the context doc
ahmed-irfan Jul 11, 2023
dc3c6c7
rm push/pop comment about mcsat
ahmed-irfan Jul 13, 2023
3379f6e
add comment about mcsat unsat cores
ahmed-irfan Jul 17, 2023
77b2a3d
fix typo
ahmed-irfan Jul 17, 2023
378b830
fix typo
ahmed-irfan Jul 17, 2023
49dd02c
Update yices.h
disteph Aug 8, 2023
ecd4b6c
fix assertion violation in uf_plugin model (#446)
ahmed-irfan Sep 5, 2023
c34e047
Correct debug code.
Sep 21, 2023
ebb3a1f
Avoid deadlocks in MC-SAT.
Sep 22, 2023
ed5211f
Destroy in reverse order of creation.
Sep 22, 2023
ba8283d
Allocate large arrays on the heap.
Sep 22, 2023
a87d54d
Use lock-free API.
Sep 22, 2023
0b5474b
Add option to run individual tests.
Sep 22, 2023
73ce57b
Add fatal error utilities.
Sep 22, 2023
a67e465
Fix typo.
Sep 22, 2023
12ab29a
Use ptrhead condition variables to communicate with the timer thread.
Sep 23, 2023
c6d3564
Simplify thread API checks.
Sep 23, 2023
e2bd36f
Update COMPILING
ahmed-irfan Sep 22, 2023
ccf823d
Update COMPILING
ahmed-irfan Sep 23, 2023
62ee73e
Revert "Update COMPILING"
ahmed-irfan Sep 23, 2023
fe6a8fd
Fix typo in non-THREAD_SAFE code.
Sep 23, 2023
4189740
Undo unnecessary changes.
Sep 23, 2023
b8aa85b
Undo unncessary change.
Sep 23, 2023
4b39bd1
Fix typo.
Sep 23, 2023
de43c66
Fix typo.
Sep 23, 2023
e5d498a
Remove extra factor of 4. (#458)
markpmitchell Sep 26, 2023
9e52bcc
mcsat-arrays-weq-graph: fix in filtering select terms
ahmed-irfan Sep 27, 2023
7aeba75
regress test
ahmed-irfan Sep 27, 2023
9d2dc3f
Merge branch 'master' into qf-eq-bv-arith
ahmed-irfan Sep 27, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 7 additions & 0 deletions src/api/context_config.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -158,6 +158,7 @@ static const int32_t logic2arch[NUM_SMT_LOGICS] = {
-1, // ANIRA
-1, // AUF
-1, // UFBV
-1, // UFBVLIA
-1, // UFIDL
-1, // UFLIA
-1, // UFLRA
Expand All @@ -167,6 +168,8 @@ static const int32_t logic2arch[NUM_SMT_LOGICS] = {
-1, // UFNIRA
-1, // UFRDL
-1, // AUFBV
-1, // AUFBVLIA
-1, // AUFBVNIA
-1, // AUFLIA
-1, // AUFLRA
-1, // AUFLIRA
Expand Down Expand Up @@ -194,6 +197,8 @@ static const int32_t logic2arch[NUM_SMT_LOGICS] = {
CTX_ARCH_MCSAT, // QF_ANIRA
CTX_ARCH_EGFUN, // QF_AUF
CTX_ARCH_EGBV, // QF_UFBV
CTX_ARCH_EGSPLXBV, // QF_UFBVLIA

CTX_ARCH_EGSPLX, // QF_UFIDL
CTX_ARCH_EGSPLX, // QF_UFLIA
CTX_ARCH_EGSPLX, // QF_UFLRA
Expand All @@ -203,6 +208,8 @@ static const int32_t logic2arch[NUM_SMT_LOGICS] = {
CTX_ARCH_MCSAT, // QF_UFNIRA
CTX_ARCH_EGSPLX, // QF_UFRDL
CTX_ARCH_EGFUNBV, // QF_AUFBV
CTX_ARCH_EGFUNSPLXBV, // QF_AUFBVLIA
CTX_ARCH_MCSAT, // QF_AUFBVNIA
CTX_ARCH_EGFUNSPLX, // QF_AUFLIA
CTX_ARCH_EGFUNSPLX, // QF_AUFLRA
CTX_ARCH_EGFUNSPLX, // QF_AUFLIRA
Expand Down
72 changes: 64 additions & 8 deletions src/api/smt_logic_codes.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,8 @@ static const char * const smt_logic_names[NUM_SMT_LOGIC_NAMES] = {
"ANRA",
"AUF",
"AUFBV",
"AUFBVLIA",
"AUFBVNIA",
"AUFLIA",
"AUFLIRA",
"AUFLRA",
Expand All @@ -68,6 +70,8 @@ static const char * const smt_logic_names[NUM_SMT_LOGIC_NAMES] = {
"QF_ANRA",
"QF_AUF",
"QF_AUFBV",
"QF_AUFBVLIA",
"QF_AUFBVNIA",
"QF_AUFLIA",
"QF_AUFLIRA",
"QF_AUFLRA",
Expand All @@ -86,6 +90,7 @@ static const char * const smt_logic_names[NUM_SMT_LOGIC_NAMES] = {
"QF_RDL",
"QF_UF",
"QF_UFBV",
"QF_UFBVLIA",
"QF_UFIDL",
"QF_UFLIA",
"QF_UFLIRA",
Expand All @@ -97,6 +102,7 @@ static const char * const smt_logic_names[NUM_SMT_LOGIC_NAMES] = {
"RDL",
"UF",
"UFBV",
"UFBVLIA",
"UFIDL",
"UFLIA",
"UFLIRA",
Expand Down Expand Up @@ -124,6 +130,8 @@ static const smt_logic_t smt_code[NUM_SMT_LOGIC_NAMES] = {
ANRA,
AUF,
AUFBV,
AUFBVLIA,
AUFBVNIA,
AUFLIA,
AUFLIRA,
AUFLRA,
Expand All @@ -149,6 +157,8 @@ static const smt_logic_t smt_code[NUM_SMT_LOGIC_NAMES] = {
QF_ANRA,
QF_AUF,
QF_AUFBV,
QF_AUFBVLIA,
QF_AUFBVNIA,
QF_AUFLIA,
QF_AUFLIRA,
QF_AUFLRA,
Expand All @@ -167,6 +177,7 @@ static const smt_logic_t smt_code[NUM_SMT_LOGIC_NAMES] = {
QF_RDL,
QF_UF,
QF_UFBV,
QF_UFBVLIA,
QF_UFIDL,
QF_UFLIA,
QF_UFLIRA,
Expand All @@ -178,6 +189,7 @@ static const smt_logic_t smt_code[NUM_SMT_LOGIC_NAMES] = {
RDL,
UF,
UFBV,
UFBVLIA,
UFIDL,
UFLIA,
UFLIRA,
Expand Down Expand Up @@ -292,6 +304,7 @@ static const uint8_t has_arrays[NUM_SMT_LOGICS] = {
true, // ANIRA
true, // AUF
false, // UFBV
false, // UFBVLIA
false, // UFIDL
false, // UFLIA
false, // UFLRA
Expand All @@ -301,6 +314,8 @@ static const uint8_t has_arrays[NUM_SMT_LOGICS] = {
false, // UFNIRA
false, // UFRDL
true, // AUFBV
true, // AUFBVLIA
true, // AUFBVNIA
true, // AUFLIA
true, // AUFLRA
true, // AUFLIRA
Expand Down Expand Up @@ -328,6 +343,7 @@ static const uint8_t has_arrays[NUM_SMT_LOGICS] = {
true, // QF_ANIRA
true, // QF_AUF
false, // QF_UFBV
false, // QF_UFBVLIA
false, // QF_UFIDL
false, // QF_UFLIA
false, // QF_UFLRA
Expand All @@ -337,6 +353,8 @@ static const uint8_t has_arrays[NUM_SMT_LOGICS] = {
false, // QF_UFNIRA
false, // QF_UFRDL
true, // QF_AUFBV
true, // QF_AUFBVLIA
true, // QF_AUFBVNIA
true, // QF_AUFLIA
true, // QF_AUFLRA
true, // QF_AUFLIRA
Expand Down Expand Up @@ -370,6 +388,7 @@ static const uint8_t has_bv[NUM_SMT_LOGICS] = {
false, // ANIRA
false, // AUF
true, // UFBV
true, // UFBVLIA
false, // UFIDL
false, // UFLIA
false, // UFLRA
Expand All @@ -379,6 +398,8 @@ static const uint8_t has_bv[NUM_SMT_LOGICS] = {
false, // UFNIRA
false, // UFRDL
true, // AUFBV
true, // AUFBVLIA
true, // AUFBVNIA
false, // AUFLIA
false, // AUFLRA
false, // AUFLIRA
Expand Down Expand Up @@ -406,6 +427,7 @@ static const uint8_t has_bv[NUM_SMT_LOGICS] = {
false, // QF_ANIRA
false, // QF_AUF
true, // QF_UFBV
true, // QF_UFBVLIA
false, // QF_UFIDL
false, // QF_UFLIA
false, // QF_UFLRA
Expand All @@ -415,6 +437,8 @@ static const uint8_t has_bv[NUM_SMT_LOGICS] = {
false, // QF_UFNIRA
false, // QF_UFRDL
true, // QF_AUFBV
true, // QF_AUFBVLIA
true, // QF_AUFBVNIA
false, // QF_AUFLIA
false, // QF_AUFLRA
false, // QF_AUFLIRA
Expand Down Expand Up @@ -448,6 +472,7 @@ static const uint8_t has_quantifiers[NUM_SMT_LOGICS] = {
true, // ANIRA
true, // AUF
true, // UFBV
true, // UFBVLIA
true, // UFIDL
true, // UFLIA
true, // UFLRA
Expand All @@ -457,6 +482,8 @@ static const uint8_t has_quantifiers[NUM_SMT_LOGICS] = {
true, // UFNIRA
true, // UFRDL
true, // AUFBV
true, // AUFBVLIA
true, // AUFBVNIA
true, // AUFLIA
true, // AUFLRA
true, // AUFLIRA
Expand Down Expand Up @@ -484,6 +511,7 @@ static const uint8_t has_quantifiers[NUM_SMT_LOGICS] = {
false, // QF_ANIRA
false, // QF_AUF
false, // QF_UFBV
false, // QF_UFBVLIA
false, // QF_UFIDL
false, // QF_UFLIA
false, // QF_UFLRA
Expand All @@ -493,6 +521,8 @@ static const uint8_t has_quantifiers[NUM_SMT_LOGICS] = {
false, // QF_UFNIRA
false, // QF_UFRDL
false, // QF_AUFBV
false, // QF_AUFBVLIA
false, // QF_AUFBVNIA
false, // QF_AUFLIA
false, // QF_AUFLRA
false, // QF_AUFLIRA
Expand Down Expand Up @@ -526,6 +556,7 @@ static const uint8_t has_uf[NUM_SMT_LOGICS] = {
false, // ANIRA
true, // AUF
true, // UFBV
true, // UFBVLIA
true, // UFIDL
true, // UFLIA
true, // UFLRA
Expand All @@ -535,6 +566,8 @@ static const uint8_t has_uf[NUM_SMT_LOGICS] = {
true, // UFNIRA
true, // UFRDL
true, // AUFBV
true, // AUFBVLIA
true, // AUFBVNIA
true, // AUFLIA
true, // AUFLRA
true, // AUFLIRA
Expand Down Expand Up @@ -562,6 +595,7 @@ static const uint8_t has_uf[NUM_SMT_LOGICS] = {
false, // QF_ANIRA
true, // QF_AUF
true, // QF_UFBV
true, // QF_UFBVLIA
true, // QF_UFIDL
true, // QF_UFLIA
true, // QF_UFLRA
Expand All @@ -571,6 +605,8 @@ static const uint8_t has_uf[NUM_SMT_LOGICS] = {
true, // QF_UFNIRA
true, // QF_UFRDL
true, // QF_AUFBV
true, // QF_AUFBVLIA
true, // QF_AUFBVNIA
true, // QF_AUFLIA
true, // QF_AUFLRA
true, // QF_AUFLIRA
Expand Down Expand Up @@ -604,6 +640,7 @@ static const uint8_t arith_frag[NUM_SMT_LOGICS] = {
ARITH_NIRA, // ANIRA
ARITH_NONE, // AUF
ARITH_NONE, // UFBV
ARITH_LIA, // UFBVLIA
ARITH_IDL, // UFIDL
ARITH_LIA, // UFLIA
ARITH_LRA, // UFLRA
Expand All @@ -613,6 +650,8 @@ static const uint8_t arith_frag[NUM_SMT_LOGICS] = {
ARITH_NIRA, // UFNIRA
ARITH_RDL, // UFRDL
ARITH_NONE, // AUFBV
ARITH_LIA, // AUFBVLIA
ARITH_NIA, // AUFBVNIA
ARITH_LIA, // AUFLIA
ARITH_LRA, // AUFLRA
ARITH_LIRA, // AUFLIRA
Expand Down Expand Up @@ -640,6 +679,7 @@ static const uint8_t arith_frag[NUM_SMT_LOGICS] = {
ARITH_NIRA, // QF_ANIRA
ARITH_NONE, // QF_AUF
ARITH_NONE, // QF_UFBV
ARITH_LIA, // QF_UFBVLIA
ARITH_IDL, // QF_UFIDL
ARITH_LIA, // QF_UFLIA
ARITH_LRA, // QF_UFLRA
Expand All @@ -649,6 +689,8 @@ static const uint8_t arith_frag[NUM_SMT_LOGICS] = {
ARITH_NIRA, // QF_UFNIRA
ARITH_RDL, // QF_UFRDL
ARITH_NONE, // QF_AUFBV
ARITH_LIA, // QF_AUFBVLIA
ARITH_NIA, // QF_AUFBVNIA
ARITH_LIA, // QF_AUFLIA
ARITH_LRA, // QF_AUFLRA
ARITH_LIRA, // QF_AUFLIRA
Expand Down Expand Up @@ -723,6 +765,7 @@ static const smt_logic_t logic2qf[NUM_SMT_LOGICS] = {
QF_ANIRA,
QF_AUF,
QF_UFBV,
QF_UFBVLIA,
QF_UFIDL,
QF_UFLIA,
QF_UFLRA,
Expand All @@ -732,6 +775,8 @@ static const smt_logic_t logic2qf[NUM_SMT_LOGICS] = {
QF_UFNIRA,
QF_UFRDL,
QF_AUFBV,
QF_AUFBVLIA,
QF_AUFBVNIA,
QF_AUFLIA,
QF_AUFLRA,
QF_AUFLIRA,
Expand Down Expand Up @@ -762,6 +807,7 @@ static const smt_logic_t logic2qf[NUM_SMT_LOGICS] = {
QF_ANIRA,
QF_AUF,
QF_UFBV,
QF_UFBVLIA,
QF_UFIDL,
QF_UFLIA,
QF_UFLRA,
Expand All @@ -771,6 +817,8 @@ static const smt_logic_t logic2qf[NUM_SMT_LOGICS] = {
QF_UFNIRA,
QF_UFRDL,
QF_AUFBV,
QF_AUFBVLIA,
QF_AUFBVNIA,
QF_AUFLIA,
QF_AUFLRA,
QF_AUFLIRA,
Expand All @@ -791,6 +839,8 @@ smt_logic_t qf_fragment(smt_logic_t code) {
* Which of these are officially recognized by our masters.
*
* - 2014/06/19: marked as 'official' everything in SMT-COMP 2014
*
* - 2023/05/18: updated according to SMT-COMP 2022
*/
static const bool is_official[NUM_SMT_LOGICS] = {
false, // NONE
Expand All @@ -806,28 +856,31 @@ static const bool is_official[NUM_SMT_LOGICS] = {
false, // NIRA
false, // RDL
true, // UF
false, // ABV
true, // ABV
true, // ALIA
false, // ALRA
false, // ALIRA
false, // ANIA
true, // ANIA
false, // ANRA
false, // ANIRA
false, // AUF
true, // UFBV
true, // UFBVLIA
true, // UFIDL
true, // UFLIA
true, // UFLRA
false, // UFLIRA
true, // UFNIA
false, // UFNRA
true, // UFNRA
false, // UFNIRA
false, // UFRDL
false, // AUFBV
true, // AUFBV
false, // AUFBVLIA
false, // AUFBVNIA
true, // AUFLIA
false, // AUFLRA
true, // AUFLIRA
false, // AUFNIA
true, // AUFNIA
false, // AUFNRA
true, // AUFNIRA

Expand All @@ -836,21 +889,22 @@ static const bool is_official[NUM_SMT_LOGICS] = {
true, // QF_IDL
true, // QF_LIA
true, // QF_LRA
false, // QF_LIRA
true, // QF_LIRA
true, // QF_NIA
true, // QF_NRA
false, // QF_NIRA
true, // QF_NIRA
true, // QF_RDL
true, // QF_UF
true, // QF_ABV
true, // QF_ALIA
false, // QF_ALRA
false, // QF_ALIRA
false, // QF_ANIA
true, // QF_ANIA
false, // QF_ANRA
false, // QF_ANIRA
false, // QF_AUF
true, // QF_UFBV
true, // QF_UFBVLIA
true, // QF_UFIDL
true, // QF_UFLIA
true, // QF_UFLRA
Expand All @@ -860,6 +914,8 @@ static const bool is_official[NUM_SMT_LOGICS] = {
false, // QF_UFNIRA
false, // QF_UFRDL
true, // QF_AUFBV
true, // QF_AUFBVLIA
true, // QF_AUFBVNIA
true, // QF_AUFLIA
false, // QF_AUFLRA
true, // QF_AUFLIRA
Expand Down
Loading