From 160b1f8d35e7bf6441981db3176f18ce077046bd Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 20 Dec 2021 18:30:43 -0600 Subject: [PATCH] Connect sequences array solver to strategy in theory of strings (#7847) Also corrects an issue with model construction, where SEQ_NTH should be assignable in addition to SEQ_NTH_TOTAL. seqArray branch (which has regressions) can be merged to master after this PR. --- src/theory/strings/extf_solver.cpp | 25 ++++++++++++++++++++++--- src/theory/strings/strategy.cpp | 16 ++++++++++++++++ src/theory/strings/strategy.h | 6 ++++++ src/theory/strings/theory_strings.cpp | 3 +++ src/theory/theory_model.cpp | 1 + src/theory/theory_model_builder.cpp | 2 +- 6 files changed, 49 insertions(+), 4 deletions(-) diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 52b0a6907..07105a311 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -16,6 +16,7 @@ #include "theory/strings/extf_solver.h" #include "options/strings_options.h" +#include "theory/strings/array_solver.h" #include "theory/strings/sequences_rewriter.h" #include "theory/strings/theory_strings_preprocess.h" #include "theory/strings/theory_strings_utils.h" @@ -157,10 +158,28 @@ bool ExtfSolver::doReduction(int effort, Node n) // asserted (pol=0). return false; } - else if (effort != 2) + else { - // all other operators reduce at level 2 - return false; + if (options().strings.seqArray != options::SeqArrayMode::NONE) + { + if (k == SEQ_NTH) + { + // don't need to reduce seq.nth when sequence update solver is used + return false; + } + else if ((k == STRING_UPDATE || k == STRING_SUBSTR) + && d_termReg.isHandledUpdate(n)) + { + // don't need to reduce certain seq.update + // don't need to reduce certain seq.extract with length 1 + return false; + } + } + if (effort != 2) + { + // all other operators reduce at level 2 + return false; + } } Node c_n = pol == -1 ? n.negate() : n; Trace("strings-process-debug") diff --git a/src/theory/strings/strategy.cpp b/src/theory/strings/strategy.cpp index 921a676d7..f54722104 100644 --- a/src/theory/strings/strategy.cpp +++ b/src/theory/strings/strategy.cpp @@ -38,6 +38,13 @@ std::ostream& operator<<(std::ostream& out, InferStep s) case CHECK_EXTF_REDUCTION: out << "check_extf_reduction"; break; case CHECK_MEMBERSHIP: out << "check_membership"; break; case CHECK_CARDINALITY: out << "check_cardinality"; break; + case CHECK_SEQUENCES_ARRAY_CONCAT: + out << "check_sequences_update_concat_terms"; + break; + case CHECK_SEQUENCES_ARRAY: out << "check_sequences_array"; break; + case CHECK_SEQUENCES_ARRAY_EAGER: + out << "check_sequences_array_eager"; + break; default: out << "?"; break; } return out; @@ -101,6 +108,10 @@ void Strategy::initializeStrategy() addStrategyStep(CHECK_INIT); addStrategyStep(CHECK_CONST_EQC); addStrategyStep(CHECK_EXTF_EVAL, 0); + if (options().strings.seqArray == options::SeqArrayMode::EAGER) + { + addStrategyStep(CHECK_SEQUENCES_ARRAY_EAGER); + } // we must check cycles before using flat forms addStrategyStep(CHECK_CYCLES); if (options().strings.stringFlatForms) @@ -130,6 +141,11 @@ void Strategy::initializeStrategy() { addStrategyStep(CHECK_LENGTH_EQC); } + if (options().strings.seqArray != options::SeqArrayMode::NONE) + { + addStrategyStep(CHECK_SEQUENCES_ARRAY_CONCAT); + addStrategyStep(CHECK_SEQUENCES_ARRAY); + } if (options().strings.stringExp) { addStrategyStep(CHECK_EXTF_REDUCTION, 2); diff --git a/src/theory/strings/strategy.h b/src/theory/strings/strategy.h index 48253c64a..e87372c0f 100644 --- a/src/theory/strings/strategy.h +++ b/src/theory/strings/strategy.h @@ -65,6 +65,12 @@ enum InferStep CHECK_MEMBERSHIP, // check cardinality CHECK_CARDINALITY, + // check sequence updates wrt concat + CHECK_SEQUENCES_ARRAY_CONCAT, + // check sequence array-like reasoning + CHECK_SEQUENCES_ARRAY, + // check sequence + CHECK_SEQUENCES_ARRAY_EAGER, }; std::ostream& operator<<(std::ostream& out, InferStep i); diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 6f19a5aaf..fdc743915 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1264,6 +1264,9 @@ void TheoryStrings::runInferStep(InferStep s, int effort) case CHECK_NORMAL_FORMS_DEQ: d_csolver.checkNormalFormsDeq(); break; case CHECK_CODES: checkCodes(); break; case CHECK_LENGTH_EQC: d_csolver.checkLengthsEqc(); break; + case CHECK_SEQUENCES_ARRAY_CONCAT: d_asolver.checkArrayConcat(); break; + case CHECK_SEQUENCES_ARRAY: d_asolver.checkArray(); break; + case CHECK_SEQUENCES_ARRAY_EAGER: d_asolver.checkArrayEager(); break; case CHECK_REGISTER_TERMS_NF: checkRegisterTermsNormalForms(); break; case CHECK_EXTF_REDUCTION: d_esolver.checkExtfReductions(effort); break; case CHECK_MEMBERSHIP: d_rsolver.checkMemberships(effort); break; diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 96e86e482..6a083b7e3 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -60,6 +60,7 @@ void TheoryModel::finishInit(eq::EqualityEngine* ee) d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR); d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR_TOTAL); d_equalityEngine->addFunctionKind(kind::APPLY_TESTER); + d_equalityEngine->addFunctionKind(kind::SEQ_NTH); d_equalityEngine->addFunctionKind(kind::SEQ_NTH_TOTAL); // do not interpret APPLY_UF if we are not assigning function values if (!d_enableFuncModels) diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index f80cf5159..06b82afd1 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -133,7 +133,7 @@ bool TheoryEngineModelBuilder::isValue(TNode n) bool TheoryEngineModelBuilder::isAssignable(TNode n) { if (n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL - || n.getKind() == kind::SEQ_NTH_TOTAL) + || n.getKind() == kind::SEQ_NTH_TOTAL || n.getKind() == kind::SEQ_NTH) { // selectors are always assignable (where we guarantee that they are not // evaluatable here) -- 2.30.2