From df9df50a7127db37d5ced3ff08283f4bf65e2e87 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 13 Mar 2026 10:00:23 -0700 Subject: [PATCH] update generation of empty sequence to take sort argument, fix mk_concat substitution Signed-off-by: Nikolaj Bjorner --- spec/perf-results.csv | 108 ++++++++++++++--------------- src/ast/euf/euf_sgraph.cpp | 18 ++--- src/ast/euf/euf_sgraph.h | 2 +- src/ast/euf/euf_snode.h | 4 ++ src/smt/seq/seq_nielsen.cpp | 132 +++++++++++++++++++++--------------- src/smt/theory_nseq.cpp | 3 - 6 files changed, 146 insertions(+), 121 deletions(-) diff --git a/spec/perf-results.csv b/spec/perf-results.csv index acfa15a33..c1e2a105d 100644 --- a/spec/perf-results.csv +++ b/spec/perf-results.csv @@ -1,55 +1,55 @@ benchmark,full_path,seq_status,seq_time,nseq_status,nseq_time,zipt_status,zipt_time -20230329-automatark-lu/instance00000.smt2,C:\c3\tests\non-incremental\QF_S\20230329-automatark-lu\instance00000.smt2,sat,0.492,timeout,10.099,sat,0.46 -20230329-automatark-lu/instance05331.smt2,C:\c3\tests\non-incremental\QF_S\20230329-automatark-lu\instance05331.smt2,sat,0.469,timeout,10.083,sat,0.496 -20230329-automatark-lu/instance10662.smt2,C:\c3\tests\non-incremental\QF_S\20230329-automatark-lu\instance10662.smt2,unsat,0.511,timeout,10.087,unsat,0.489 -20240318-omark/cloud-service-query-1.smt2,C:\c3\tests\non-incremental\QF_S\20240318-omark\cloud-service-query-1.smt2,sat,7.603,Result: SAT,0.53,sat,1.092 -20240318-omark/lyndon-schuetzenberg-3.smt2,C:\c3\tests\non-incremental\QF_S\20240318-omark\lyndon-schuetzenberg-3.smt2,timeout,10.065,timeout,10.49,timeout,10.41 -20240318-omark/noodles-unsat-5.smt2,C:\c3\tests\non-incremental\QF_S\20240318-omark\noodles-unsat-5.smt2,timeout,10.445,unknown,0.436,sat,0.939 -20250410-matching/sub-matching-sat-1.smt2,C:\c3\tests\non-incremental\QF_S\20250410-matching\sub-matching-sat-1.smt2,timeout,10.074,timeout,10.448,crash,0.781 -20250410-matching/sub-matching-unsat-16.smt2,C:\c3\tests\non-incremental\QF_S\20250410-matching\sub-matching-unsat-16.smt2,timeout,10.472,timeout,10.443,crash,0.808 -20250410-matching/wildcard-matching-regex-104.smt2,C:\c3\tests\non-incremental\QF_S\20250410-matching\wildcard-matching-regex-104.smt2,sat,0.531,unknown,0.085,unknown,0.404 -20250410-matching/wildcard-matching-regex-41.smt2,C:\c3\tests\non-incremental\QF_S\20250410-matching\wildcard-matching-regex-41.smt2,crash,0.389,unknown,0.341,crash,0.699 -20250411-hornstr-equiv/Burns_lstar_non_incre_equiv_bad_0_0.smt2,C:\c3\tests\non-incremental\QF_S\20250411-hornstr-equiv\Burns_lstar_non_incre_equiv_bad_0_0.smt2,sat,0.123,unknown,0.093,sat,0.503 -20250411-hornstr-equiv/dining-cryptographers_sat_non_incre_equiv_init_0_3.smt2,C:\c3\tests\non-incremental\QF_S\20250411-hornstr-equiv\dining-cryptographers_sat_non_incre_equiv_init_0_3.smt2,sat,0.1,Result: UNSAT,0.107,sat,0.488 -20250411-hornstr-equiv/muzzle_sat_non_incre_equiv_bad_0_13.smt2,C:\c3\tests\non-incremental\QF_S\20250411-hornstr-equiv\muzzle_sat_non_incre_equiv_bad_0_13.smt2,unsat,0.059,unsat,0.097,unsat,0.419 -20250411-negated-predicates/diseq-1-3-5-0.smt2,C:\c3\tests\non-incremental\QF_S\20250411-negated-predicates\diseq-1-3-5-0.smt2,timeout,10.067,Result: SAT,0.461,timeout,10 -20250411-negated-predicates/diseq-None-4-5-107.smt2,C:\c3\tests\non-incremental\QF_S\20250411-negated-predicates\diseq-None-4-5-107.smt2,timeout,10.411,Result: SAT,0.437,timeout,10 -20250411-negated-predicates/not-contains-1-4-5-112.smt2,C:\c3\tests\non-incremental\QF_S\20250411-negated-predicates\not-contains-1-4-5-112.smt2,timeout,10.445,unknown,0.43,sat,0.404 -pcp-3-3-random/pcp_instance_0.smt2,C:\c3\tests\non-incremental\QF_S\20250403-pcp-string\pcp-3-3-random\pcp_instance_0.smt2,unknown,0.098,timeout,10.077,unknown,0.321 -pcp-3-3-random/pcp_instance_248.smt2,C:\c3\tests\non-incremental\QF_S\20250403-pcp-string\pcp-3-3-random\pcp_instance_248.smt2,unknown,0.462,timeout,10.077,unknown,0.289 -pcp-3-3-random/pcp_instance_398.smt2,C:\c3\tests\non-incremental\QF_S\20250403-pcp-string\pcp-3-3-random\pcp_instance_398.smt2,unknown,0.456,timeout,10.074,unknown,0.316 -pcp-3-4-hard/unsolved_pcp_instance_0.smt2,C:\c3\tests\non-incremental\QF_S\20250403-pcp-string\pcp-3-4-hard\unsolved_pcp_instance_0.smt2,unknown,0.467,timeout,10.074,unknown,0.335 -pcp-3-4-hard/unsolved_pcp_instance_248.smt2,C:\c3\tests\non-incremental\QF_S\20250403-pcp-string\pcp-3-4-hard\unsolved_pcp_instance_248.smt2,unknown,0.458,timeout,10.061,unknown,0.316 -pcp-3-4-hard/unsolved_pcp_instance_398.smt2,C:\c3\tests\non-incremental\QF_S\20250403-pcp-string\pcp-3-4-hard\unsolved_pcp_instance_398.smt2,unknown,0.468,timeout,10.072,unknown,0.305 -queries/query2885.smt2,C:\c3\tests\non-incremental\QF_S\2020-sygus-qgen\queries\query2885.smt2,sat,0.886,unknown,0.093,sat,0.386 -queries/query3358.smt2,C:\c3\tests\non-incremental\QF_S\2020-sygus-qgen\queries\query3358.smt2,sat,0.519,unknown,0.068,sat,0.448 -queries/query3664.smt2,C:\c3\tests\non-incremental\QF_S\2020-sygus-qgen\queries\query3664.smt2,sat,0.271,unknown,0.072,sat,0.424 -queries/query6481.smt2,C:\c3\tests\non-incremental\QF_S\2020-sygus-qgen\queries\query6481.smt2,sat,0.218,unknown,0.069,sat,0.433 -queries-no-ree/query10041.smt2,C:\c3\tests\non-incremental\QF_S\2020-sygus-qgen\queries-no-ree\query10041.smt2,sat,0.798,unknown,0.075,sat,0.448 -queries-no-ree/query3231.smt2,C:\c3\tests\non-incremental\QF_S\2020-sygus-qgen\queries-no-ree\query3231.smt2,sat,0.444,unknown,0.474,sat,0.422 -queries-no-ree/query3723.smt2,C:\c3\tests\non-incremental\QF_S\2020-sygus-qgen\queries-no-ree\query3723.smt2,sat,0.422,unknown,0.082,sat,0.451 -queries-no-ree/query5519.smt2,C:\c3\tests\non-incremental\QF_S\2020-sygus-qgen\queries-no-ree\query5519.smt2,sat,0.222,unknown,0.09,sat,0.418 -rna-sat/benchmark_0001.smt2,C:\c3\tests\non-incremental\QF_S\20250403-rna\rna-sat\benchmark_0001.smt2,unknown,0.079,unknown,0.06,unknown,0.275 -rna-sat/benchmark_0167.smt2,C:\c3\tests\non-incremental\QF_S\20250403-rna\rna-sat\benchmark_0167.smt2,unknown,0.074,unknown,0.08,unknown,0.276 -rna-sat/benchmark_0333.smt2,C:\c3\tests\non-incremental\QF_S\20250403-rna\rna-sat\benchmark_0333.smt2,unknown,0.109,unknown,0.09,unknown,0.269 -rna-unsat/benchmark_0001.smt2,C:\c3\tests\non-incremental\QF_S\20250403-rna\rna-unsat\benchmark_0001.smt2,unknown,0.08,unknown,0.097,unknown,0.246 -rna-unsat/benchmark_0167.smt2,C:\c3\tests\non-incremental\QF_S\20250403-rna\rna-unsat\benchmark_0167.smt2,unknown,0.091,unknown,0.088,unknown,0.269 -rna-unsat/benchmark_0333.smt2,C:\c3\tests\non-incremental\QF_S\20250403-rna\rna-unsat\benchmark_0333.smt2,unknown,0.099,unknown,0.094,unknown,0.293 -slog/slog_stranger_1001_sink.smt2,C:\c3\tests\non-incremental\QF_S\2019-Jiang\slog\slog_stranger_1001_sink.smt2,unsat,0.092,unsat,0.084,unsat,0.416 -slog/slog_stranger_2251_sink.smt2,C:\c3\tests\non-incremental\QF_S\2019-Jiang\slog\slog_stranger_2251_sink.smt2,unsat,0.433,unsat,0.077,unsat,0.352 -slog/slog_stranger_3947_sink.smt2,C:\c3\tests\non-incremental\QF_S\2019-Jiang\slog\slog_stranger_3947_sink.smt2,sat,0.218,unknown,0.094,sat,0.575 -track01/01_track_1.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track01\01_track_1.smt2,sat,0.084,sat,0.082,sat,0.404 -track01/01_track_144.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track01\01_track_144.smt2,sat,0.06,sat,0.094,sat,0.503 -track01/01_track_19.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track01\01_track_19.smt2,sat,0.073,sat,0.061,sat,0.434 -track01/01_track_54.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track01\01_track_54.smt2,sat,0.101,Result: SAT,0.093,sat,1.142 -track02/02_track_1.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track02\02_track_1.smt2,timeout,10.075,Result: SAT,0.523,sat,0.594 -track02/02_track_4.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track02\02_track_4.smt2,timeout,10.072,Result: SAT,0.723,sat,6.008 -track02/02_track_7.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track02\02_track_7.smt2,timeout,10.428,Result: SAT,0.644,sat,2.855 -track03/03_track_1.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track03\03_track_1.smt2,unsat,0.065,unsat,0.08,unsat,0.472 -track03/03_track_144.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track03\03_track_144.smt2,sat,0.086,Result: SAT,0.075,sat,0.832 -track03/03_track_19.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track03\03_track_19.smt2,unsat,0.094,unsat,0.077,unsat,0.388 -track03/03_track_54.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track03\03_track_54.smt2,timeout,10.448,Result: UNSAT,0.482,unsat,0.508 -track04/04_track_1.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track04\04_track_1.smt2,sat,0.067,sat,0.062,sat,0.367 -track04/04_track_144.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track04\04_track_144.smt2,unsat,0.088,unsat,0.072,unsat,0.515 -track04/04_track_19.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track04\04_track_19.smt2,unsat,0.084,unsat,0.068,unsat,0.467 -track04/04_track_54.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track04\04_track_54.smt2,sat,0.085,sat,0.084,sat,0.462 +20230329-automatark-lu/instance00000.smt2,C:\c3\tests\non-incremental\QF_S\20230329-automatark-lu\instance00000.smt2,sat,5.549,timeout,10.069,sat,0.449 +20230329-automatark-lu/instance05331.smt2,C:\c3\tests\non-incremental\QF_S\20230329-automatark-lu\instance05331.smt2,sat,0.489,timeout,10.078,sat,0.511 +20230329-automatark-lu/instance10662.smt2,C:\c3\tests\non-incremental\QF_S\20230329-automatark-lu\instance10662.smt2,unsat,0.554,timeout,10.095,unsat,0.509 +20240318-omark/cloud-service-query-1.smt2,C:\c3\tests\non-incremental\QF_S\20240318-omark\cloud-service-query-1.smt2,sat,8.002,sat,0.527,sat,1.155 +20240318-omark/lyndon-schuetzenberg-3.smt2,C:\c3\tests\non-incremental\QF_S\20240318-omark\lyndon-schuetzenberg-3.smt2,timeout,10.087,timeout,10.493,timeout,10.425 +20240318-omark/noodles-unsat-5.smt2,C:\c3\tests\non-incremental\QF_S\20240318-omark\noodles-unsat-5.smt2,timeout,10.463,unknown,0.472,sat,0.882 +20250410-matching/sub-matching-sat-1.smt2,C:\c3\tests\non-incremental\QF_S\20250410-matching\sub-matching-sat-1.smt2,timeout,10.072,timeout,10.452,crash,0.879 +20250410-matching/sub-matching-unsat-16.smt2,C:\c3\tests\non-incremental\QF_S\20250410-matching\sub-matching-unsat-16.smt2,timeout,10.439,timeout,10.601,crash,0.871 +20250410-matching/wildcard-matching-regex-104.smt2,C:\c3\tests\non-incremental\QF_S\20250410-matching\wildcard-matching-regex-104.smt2,sat,0.588,unknown,0.096,unknown,0.429 +20250410-matching/wildcard-matching-regex-41.smt2,C:\c3\tests\non-incremental\QF_S\20250410-matching\wildcard-matching-regex-41.smt2,crash,0.415,unknown,0.339,crash,0.718 +20250411-hornstr-equiv/Burns_lstar_non_incre_equiv_bad_0_0.smt2,C:\c3\tests\non-incremental\QF_S\20250411-hornstr-equiv\Burns_lstar_non_incre_equiv_bad_0_0.smt2,sat,0.139,timeout,10.094,sat,0.592 +20250411-hornstr-equiv/dining-cryptographers_sat_non_incre_equiv_init_0_3.smt2,C:\c3\tests\non-incremental\QF_S\20250411-hornstr-equiv\dining-cryptographers_sat_non_incre_equiv_init_0_3.smt2,sat,0.519,unsat,0.139,sat,0.509 +20250411-hornstr-equiv/muzzle_sat_non_incre_equiv_bad_0_13.smt2,C:\c3\tests\non-incremental\QF_S\20250411-hornstr-equiv\muzzle_sat_non_incre_equiv_bad_0_13.smt2,unsat,0.096,unsat,0.07,unsat,0.46 +20250411-negated-predicates/diseq-1-3-5-0.smt2,C:\c3\tests\non-incremental\QF_S\20250411-negated-predicates\diseq-1-3-5-0.smt2,timeout,10.063,unknown,0.476,timeout,10 +20250411-negated-predicates/diseq-None-4-5-107.smt2,C:\c3\tests\non-incremental\QF_S\20250411-negated-predicates\diseq-None-4-5-107.smt2,timeout,10.463,unknown,0.491,timeout,10 +20250411-negated-predicates/not-contains-1-4-5-112.smt2,C:\c3\tests\non-incremental\QF_S\20250411-negated-predicates\not-contains-1-4-5-112.smt2,timeout,10.46,unknown,0.434,sat,0.407 +pcp-3-3-random/pcp_instance_0.smt2,C:\c3\tests\non-incremental\QF_S\20250403-pcp-string\pcp-3-3-random\pcp_instance_0.smt2,unknown,0.1,timeout,10.079,unknown,0.296 +pcp-3-3-random/pcp_instance_248.smt2,C:\c3\tests\non-incremental\QF_S\20250403-pcp-string\pcp-3-3-random\pcp_instance_248.smt2,unknown,0.467,timeout,10.082,unknown,0.345 +pcp-3-3-random/pcp_instance_398.smt2,C:\c3\tests\non-incremental\QF_S\20250403-pcp-string\pcp-3-3-random\pcp_instance_398.smt2,unknown,0.471,timeout,10.066,unknown,0.347 +pcp-3-4-hard/unsolved_pcp_instance_0.smt2,C:\c3\tests\non-incremental\QF_S\20250403-pcp-string\pcp-3-4-hard\unsolved_pcp_instance_0.smt2,unknown,0.494,timeout,10.073,unknown,0.304 +pcp-3-4-hard/unsolved_pcp_instance_248.smt2,C:\c3\tests\non-incremental\QF_S\20250403-pcp-string\pcp-3-4-hard\unsolved_pcp_instance_248.smt2,unknown,0.482,timeout,10.079,unknown,0.332 +pcp-3-4-hard/unsolved_pcp_instance_398.smt2,C:\c3\tests\non-incremental\QF_S\20250403-pcp-string\pcp-3-4-hard\unsolved_pcp_instance_398.smt2,unknown,0.461,timeout,10.076,unknown,0.305 +queries/query2885.smt2,C:\c3\tests\non-incremental\QF_S\2020-sygus-qgen\queries\query2885.smt2,sat,0.878,timeout,10.093,sat,0.468 +queries/query3358.smt2,C:\c3\tests\non-incremental\QF_S\2020-sygus-qgen\queries\query3358.smt2,sat,0.94,timeout,10.103,sat,0.484 +queries/query3664.smt2,C:\c3\tests\non-incremental\QF_S\2020-sygus-qgen\queries\query3664.smt2,sat,0.691,timeout,10.131,sat,0.573 +queries/query6481.smt2,C:\c3\tests\non-incremental\QF_S\2020-sygus-qgen\queries\query6481.smt2,sat,0.611,timeout,10.092,sat,0.491 +queries-no-ree/query10041.smt2,C:\c3\tests\non-incremental\QF_S\2020-sygus-qgen\queries-no-ree\query10041.smt2,sat,1.176,timeout,10.119,sat,0.484 +queries-no-ree/query3231.smt2,C:\c3\tests\non-incremental\QF_S\2020-sygus-qgen\queries-no-ree\query3231.smt2,sat,0.84,timeout,10.105,sat,0.476 +queries-no-ree/query3723.smt2,C:\c3\tests\non-incremental\QF_S\2020-sygus-qgen\queries-no-ree\query3723.smt2,sat,0.836,timeout,10.11,sat,0.469 +queries-no-ree/query5519.smt2,C:\c3\tests\non-incremental\QF_S\2020-sygus-qgen\queries-no-ree\query5519.smt2,sat,0.633,timeout,10.1,sat,0.458 +rna-sat/benchmark_0001.smt2,C:\c3\tests\non-incremental\QF_S\20250403-rna\rna-sat\benchmark_0001.smt2,unknown,0.495,unknown,0.09,unknown,0.286 +rna-sat/benchmark_0167.smt2,C:\c3\tests\non-incremental\QF_S\20250403-rna\rna-sat\benchmark_0167.smt2,unknown,0.091,unknown,0.102,unknown,0.265 +rna-sat/benchmark_0333.smt2,C:\c3\tests\non-incremental\QF_S\20250403-rna\rna-sat\benchmark_0333.smt2,unknown,0.098,unknown,0.076,unknown,0.254 +rna-unsat/benchmark_0001.smt2,C:\c3\tests\non-incremental\QF_S\20250403-rna\rna-unsat\benchmark_0001.smt2,unknown,0.092,unknown,0.093,unknown,0.293 +rna-unsat/benchmark_0167.smt2,C:\c3\tests\non-incremental\QF_S\20250403-rna\rna-unsat\benchmark_0167.smt2,unknown,0.098,unknown,0.077,unknown,0.33 +rna-unsat/benchmark_0333.smt2,C:\c3\tests\non-incremental\QF_S\20250403-rna\rna-unsat\benchmark_0333.smt2,unknown,0.104,unknown,0.093,unknown,0.304 +slog/slog_stranger_1001_sink.smt2,C:\c3\tests\non-incremental\QF_S\2019-Jiang\slog\slog_stranger_1001_sink.smt2,unsat,0.073,unsat,0.085,unsat,0.443 +slog/slog_stranger_2251_sink.smt2,C:\c3\tests\non-incremental\QF_S\2019-Jiang\slog\slog_stranger_2251_sink.smt2,unsat,0.082,unsat,0.086,unsat,0.386 +slog/slog_stranger_3947_sink.smt2,C:\c3\tests\non-incremental\QF_S\2019-Jiang\slog\slog_stranger_3947_sink.smt2,sat,0.221,sat,3.478,sat,0.646 +track01/01_track_1.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track01\01_track_1.smt2,sat,0.483,sat,0.092,sat,0.466 +track01/01_track_144.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track01\01_track_144.smt2,sat,0.064,sat,0.072,sat,0.434 +track01/01_track_19.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track01\01_track_19.smt2,sat,0.089,sat,0.083,sat,0.444 +track01/01_track_54.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track01\01_track_54.smt2,sat,0.114,sat,0.099,sat,1.016 +track02/02_track_1.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track02\02_track_1.smt2,timeout,10.081,sat,0.521,sat,0.566 +track02/02_track_4.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track02\02_track_4.smt2,timeout,10.078,sat,0.737,sat,6.142 +track02/02_track_7.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track02\02_track_7.smt2,timeout,10.451,sat,0.64,sat,2.842 +track03/03_track_1.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track03\03_track_1.smt2,unsat,0.061,unsat,0.081,unsat,0.378 +track03/03_track_144.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track03\03_track_144.smt2,sat,0.088,sat,0.095,sat,0.865 +track03/03_track_19.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track03\03_track_19.smt2,unsat,0.096,unsat,0.066,unsat,0.376 +track03/03_track_54.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track03\03_track_54.smt2,timeout,10.449,unsat,0.492,unsat,0.586 +track04/04_track_1.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track04\04_track_1.smt2,sat,0.091,sat,0.074,sat,0.346 +track04/04_track_144.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track04\04_track_144.smt2,unsat,0.069,unsat,0.071,unsat,0.516 +track04/04_track_19.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track04\04_track_19.smt2,unsat,0.094,unsat,0.07,unsat,0.476 +track04/04_track_54.smt2,C:\c3\tests\non-incremental\QF_S\20230329-woorpje-lu\track04\04_track_54.smt2,sat,0.082,sat,0.066,sat,0.519 diff --git a/src/ast/euf/euf_sgraph.cpp b/src/ast/euf/euf_sgraph.cpp index 6e8827a79..03f5603cf 100644 --- a/src/ast/euf/euf_sgraph.cpp +++ b/src/ast/euf/euf_sgraph.cpp @@ -461,21 +461,23 @@ namespace euf { return mk(u); } - snode* sgraph::mk_empty() { - expr_ref e(m_seq.str.mk_empty(m_str_sort), m); + snode* sgraph::mk_empty_seq(sort* s) { + expr_ref e(m_seq.str.mk_empty(s), m); return mk(e); } snode* sgraph::mk_concat(snode* a, snode* b) { if (a->is_empty()) return b; if (b->is_empty()) return a; - expr_ref e(m_seq.str.mk_concat(a->get_expr(), b->get_expr()), m); - return mk(e); + if (m_seq.is_re(a->get_expr())) + return mk(expr_ref(m_seq.re.mk_concat(a->get_expr(), b->get_expr()), m)); + else + return mk(expr_ref(m_seq.str.mk_concat(a->get_expr(), b->get_expr()), m)); } snode* sgraph::drop_first(snode* n) { if (n->is_empty() || n->is_token()) - return mk_empty(); + return mk_empty_seq(n->get_sort()); SASSERT(n->is_concat()); snode* l = n->arg(0); snode* r = n->arg(1); @@ -486,7 +488,7 @@ namespace euf { snode* sgraph::drop_last(snode* n) { if (n->is_empty() || n->is_token()) - return mk_empty(); + return mk_empty_seq(n->get_sort()); SASSERT(n->is_concat()); snode* l = n->arg(0); snode* r = n->arg(1); @@ -497,7 +499,7 @@ namespace euf { snode* sgraph::drop_left(snode* n, unsigned count) { if (count == 0 || n->is_empty()) return n; - if (count >= n->length()) return mk_empty(); + if (count >= n->length()) return mk_empty_seq(n->get_sort()); for (unsigned i = 0; i < count; ++i) n = drop_first(n); return n; @@ -505,7 +507,7 @@ namespace euf { snode* sgraph::drop_right(snode* n, unsigned count) { if (count == 0 || n->is_empty()) return n; - if (count >= n->length()) return mk_empty(); + if (count >= n->length()) return mk_empty_seq(n->get_sort()); for (unsigned i = 0; i < count; ++i) n = drop_last(n); return n; diff --git a/src/ast/euf/euf_sgraph.h b/src/ast/euf/euf_sgraph.h index 545f21c38..950fc8c06 100644 --- a/src/ast/euf/euf_sgraph.h +++ b/src/ast/euf/euf_sgraph.h @@ -128,7 +128,7 @@ namespace euf { // factory methods for creating snodes with corresponding expressions snode* mk_var(symbol const& name); snode* mk_char(unsigned ch); - snode* mk_empty(); + snode *mk_empty_seq(sort *s); snode* mk_concat(snode* a, snode* b); // drop operations: remove tokens from the front/back of a concat tree diff --git a/src/ast/euf/euf_snode.h b/src/ast/euf/euf_snode.h index 95bf1f64e..1028cdfa1 100644 --- a/src/ast/euf/euf_snode.h +++ b/src/ast/euf/euf_snode.h @@ -143,6 +143,10 @@ namespace euf { } } + sort *get_sort() const { + return m_expr ? m_expr->get_sort() : nullptr; + } + // analogous to ZIPT's Str.First / Str.Last snode const* first() const { snode const* s = this; diff --git a/src/smt/seq/seq_nielsen.cpp b/src/smt/seq/seq_nielsen.cpp index f3c763ba2..ac8676274 100644 --- a/src/smt/seq/seq_nielsen.cpp +++ b/src/smt/seq/seq_nielsen.cpp @@ -544,7 +544,7 @@ namespace seq { m_root = mk_node(); dep_tracker dep; dep.insert(m_root->str_eqs().size() + m_root->str_mems().size()); - euf::snode* history = m_sg.mk_empty(); + euf::snode* history = m_sg.mk_empty_seq(str->get_sort()); unsigned id = next_mem_id(); m_root->add_str_mem(str_mem(str, regex, history, id, dep)); ++m_num_input_mems; @@ -1055,7 +1055,7 @@ namespace seq { arith_util arith(m); for (euf::snode* t : tokens) { if (t->is_var()) { - nielsen_subst s(t, sg.mk_empty(), dep); + nielsen_subst s(t, sg.mk_empty_seq(t->get_sort()), dep); apply_subst(sg, s); changed = true; } @@ -1069,7 +1069,7 @@ namespace seq { m_int_constraints.push_back( int_constraint(pow_exp, zero, int_constraint_kind::eq, dep, m)); } - nielsen_subst s(t, sg.mk_empty(), dep); + nielsen_subst s(t, sg.mk_empty_seq(t->get_sort()), dep); apply_subst(sg, s); changed = true; } @@ -1234,7 +1234,7 @@ namespace seq { if (!merged) return nullptr; // Rebuild snode from merged token list - euf::snode* rebuilt = sg.mk_empty(); + euf::snode* rebuilt = sg.mk_empty_seq(side->get_sort()); for (unsigned k = 0; k < result.size(); ++k) { rebuilt = (k == 0) ? result[k] : sg.mk_concat(rebuilt, result[k]); } @@ -1281,7 +1281,7 @@ namespace seq { if (!simplified) return nullptr; - if (result.empty()) return sg.mk_empty(); + if (result.empty()) return sg.mk_empty_seq(side->get_sort()); euf::snode* rebuilt = result[0]; for (unsigned k = 1; k < result.size(); ++k) rebuilt = sg.mk_concat(rebuilt, result[k]); @@ -2230,24 +2230,51 @@ namespace seq { return true; } - if (rhead->is_char() && lhead->is_var()) { - { - nielsen_node* child = mk_child(node); - nielsen_edge* e = mk_edge(node, child, true); - nielsen_subst s(lhead, m_sg.mk_empty(), eq.m_dep); - e->add_subst(s); - child->apply_subst(m_sg, s); - } - { - euf::snode* replacement = dir_concat(m_sg, rhead, lhead, fwd); - nielsen_node* child = mk_child(node); - nielsen_edge* e = mk_edge(node, child, false); - nielsen_subst s(lhead, replacement, eq.m_dep); - e->add_subst(s); - child->apply_subst(m_sg, s); - } - return true; + euf::snode* lhead = lhs_toks[0]; + euf::snode* rhead = rhs_toks[0]; + + // char·A = y·B → branch 1: y→ε, branch 2: y→char·y + if (lhead->is_char() && rhead->is_var()) { + // branch 1: y → ε (progress) + { + nielsen_node* child = mk_child(node); + nielsen_edge* e = mk_edge(node, child, true); + nielsen_subst s(rhead, m_sg.mk_empty_seq(rhead->get_sort()), eq.m_dep); + e->add_subst(s); + child->apply_subst(m_sg, s); } + // branch 2: y → char·y (no progress) + { + euf::snode* replacement = m_sg.mk_concat(lhead, rhead); + nielsen_node* child = mk_child(node); + nielsen_edge* e = mk_edge(node, child, false); + nielsen_subst s(rhead, replacement, eq.m_dep); + e->add_subst(s); + child->apply_subst(m_sg, s); + } + return true; + } + + // x·A = char·B → branch 1: x→ε, branch 2: x→char·x + if (rhead->is_char() && lhead->is_var()) { + // branch 1: x → ε (progress) + { + nielsen_node* child = mk_child(node); + nielsen_edge* e = mk_edge(node, child, true); + nielsen_subst s(lhead, m_sg.mk_empty_seq(lhead->get_sort()), eq.m_dep); + e->add_subst(s); + child->apply_subst(m_sg, s); + } + // branch 2: x → char·x (no progress) + { + euf::snode* replacement = m_sg.mk_concat(rhead, lhead); + nielsen_node* child = mk_child(node); + nielsen_edge* e = mk_edge(node, child, false); + nielsen_subst s(lhead, replacement, eq.m_dep); + e->add_subst(s); + child->apply_subst(m_sg, s); + } + return true; } } return false; @@ -2270,33 +2297,28 @@ namespace seq { if (lhead->id() == rhead->id()) continue; - // child 1: x -> ε (progress) - { - nielsen_node* child = mk_child(node); - nielsen_edge* e = mk_edge(node, child, true); - nielsen_subst s(lhead, m_sg.mk_empty(), eq.m_dep); - e->add_subst(s); - child->apply_subst(m_sg, s); - } - // child 2: x -> y·x (forward) or x·y (backward) - { - euf::snode* replacement = dir_concat(m_sg, rhead, lhead, fwd); - nielsen_node* child = mk_child(node); - nielsen_edge* e = mk_edge(node, child, false); - nielsen_subst s(lhead, replacement, eq.m_dep); - e->add_subst(s); - child->apply_subst(m_sg, s); - } - // child 3: y -> x·y (forward) or y·x (backward) - { - euf::snode* replacement = dir_concat(m_sg, lhead, rhead, fwd); - nielsen_node* child = mk_child(node); - nielsen_edge* e = mk_edge(node, child, false); - nielsen_subst s(rhead, replacement, eq.m_dep); - e->add_subst(s); - child->apply_subst(m_sg, s); - } - return true; + euf::snode_vector lhs_toks, rhs_toks; + eq.m_lhs->collect_tokens(lhs_toks); + eq.m_rhs->collect_tokens(rhs_toks); + if (lhs_toks.empty() || rhs_toks.empty()) + continue; + + euf::snode* lhead = lhs_toks[0]; + euf::snode* rhead = rhs_toks[0]; + + if (!lhead->is_var() || !rhead->is_var()) + continue; + if (lhead->id() == rhead->id()) + continue; + + // x·A = y·B where x,y are distinct variables (classic Nielsen) + // child 1: x → ε (progress) + { + nielsen_node* child = mk_child(node); + nielsen_edge* e = mk_edge(node, child, true); + nielsen_subst s(lhead, m_sg.mk_empty_seq(lhead->get_sort()), eq.m_dep); + e->add_subst(s); + child->apply_subst(m_sg, s); } } return false; @@ -2703,7 +2725,7 @@ namespace seq { { nielsen_node* child = mk_child(node); nielsen_edge* e = mk_edge(node, child, true); - nielsen_subst s(first, m_sg.mk_empty(), mem.m_dep); + nielsen_subst s(first, m_sg.mk_empty_seq(first->get_sort()), mem.m_dep); e->add_subst(s); child->apply_subst(m_sg, s); created = true; @@ -2921,7 +2943,7 @@ namespace seq { if (base->is_var()) { child = mk_child(node); e = mk_edge(node, child, true); - nielsen_subst s1(base, m_sg.mk_empty(), dep); + nielsen_subst s1(base, m_sg.mk_empty_seq(base->get_sort()), dep); e->add_subst(s1); child->apply_subst(m_sg, s1); } @@ -2929,7 +2951,7 @@ namespace seq { // Branch 2: replace the power token itself with ε (n = 0 semantics) child = mk_child(node); e = mk_edge(node, child, true); - nielsen_subst s2(power, m_sg.mk_empty(), dep); + nielsen_subst s2(power, m_sg.mk_empty_seq(power->get_sort()), dep); e->add_subst(s2); child->apply_subst(m_sg, s2); @@ -3096,7 +3118,7 @@ namespace seq { // Side constraint: n = 0 nielsen_node *child = mk_child(node); nielsen_edge *e = mk_edge(node, child, true); - nielsen_subst s1(power, m_sg.mk_empty(), eq->m_dep); + nielsen_subst s1(power, m_sg.mk_empty_seq(power->get_sort()), eq->m_dep); e->add_subst(s1); child->apply_subst(m_sg, s1); if (exp_n) @@ -3413,7 +3435,7 @@ namespace seq { { nielsen_node* child = mk_child(node); nielsen_edge* e = mk_edge(node, child, true); - nielsen_subst s(first, m_sg.mk_empty(), mem.m_dep); + nielsen_subst s(first, m_sg.mk_empty_seq(first->get_sort()), mem.m_dep); e->add_subst(s); child->apply_subst(m_sg, s); created = true; @@ -3600,7 +3622,7 @@ namespace seq { { nielsen_node* child = mk_child(node); nielsen_edge* e = mk_edge(node, child, true); - nielsen_subst s(power, m_sg.mk_empty(), eq->m_dep); + nielsen_subst s(power, m_sg.mk_empty_seq(power->get_sort()), eq->m_dep); e->add_subst(s); child->apply_subst(m_sg, s); if (exp_n) diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index f75436e57..fdda483cd 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -421,9 +421,6 @@ namespace smt { // here the actual Nielsen solving happens auto result = m_nielsen.solve(); - std::cout << "Result: " << (result == seq::nielsen_graph::search_result::sat ? "SAT" : result == seq::nielsen_graph::search_result::unsat ? "UNSAT" : "UNKNOWN") << "\n"; - // m_nielsen.to_dot(std::cout); - // std::cout << std::endl; if (result == seq::nielsen_graph::search_result::sat) { IF_VERBOSE(1, verbose_stream() << "nseq final_check: solve SAT, sat_node="