diff options
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/arith_entail.cpp | 1 | ||||
-rw-r--r-- | src/theory/strings/base_solver.cpp | 1 | ||||
-rw-r--r-- | src/theory/strings/core_solver.cpp | 3 | ||||
-rw-r--r-- | src/theory/strings/inference_manager.cpp | 1 | ||||
-rw-r--r-- | src/theory/strings/kinds | 36 | ||||
-rw-r--r-- | src/theory/strings/regexp_elim.cpp | 23 | ||||
-rw-r--r-- | src/theory/strings/regexp_entail.cpp | 2 | ||||
-rw-r--r-- | src/theory/strings/regexp_operation.cpp | 1 | ||||
-rw-r--r-- | src/theory/strings/sequences_rewriter.cpp | 3 | ||||
-rw-r--r-- | src/theory/strings/solver_state.cpp | 1 | ||||
-rw-r--r-- | src/theory/strings/strings_entail.cpp | 2 | ||||
-rw-r--r-- | src/theory/strings/strings_fmf.cpp | 2 | ||||
-rw-r--r-- | src/theory/strings/strings_rewriter.cpp | 1 | ||||
-rw-r--r-- | src/theory/strings/term_registry.cpp | 2 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 2 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_type_rules.cpp | 1 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_utils.cpp | 3 | ||||
-rw-r--r-- | src/theory/strings/type_enumerator.cpp | 1 |
18 files changed, 60 insertions, 26 deletions
diff --git a/src/theory/strings/arith_entail.cpp b/src/theory/strings/arith_entail.cpp index 4c3b2f17e..66e3cf634 100644 --- a/src/theory/strings/arith_entail.cpp +++ b/src/theory/strings/arith_entail.cpp @@ -22,6 +22,7 @@ #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" #include "theory/theory.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 6ee88b298..00491128a 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -21,6 +21,7 @@ #include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" using namespace std; using namespace cvc5::context; diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index a6e4ce698..fb1d086a4 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -16,6 +16,7 @@ #include "theory/strings/core_solver.h" #include "base/configuration.h" +#include "expr/sequence.h" #include "options/strings_options.h" #include "smt/logic_exception.h" #include "theory/rewriter.h" @@ -23,6 +24,8 @@ #include "theory/strings/strings_entail.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" +#include "util/string.h" using namespace std; using namespace cvc5::context; diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 3dbb6b89b..94d99732a 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -20,6 +20,7 @@ #include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" using namespace std; using namespace cvc5::context; diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 30ca92808..743a5c006 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -57,10 +57,11 @@ enumerator STRING_TYPE \ "theory/strings/type_enumerator.h" constant CONST_STRING \ - ::cvc5::String \ - ::cvc5::strings::StringHashFunction \ - "util/string.h" \ - "a string of characters" + class \ + String \ + ::cvc5::strings::StringHashFunction \ + "util/string.h" \ + "a string of characters" # the type operator SEQUENCE_TYPE 1 "seuence type, takes as parameter the type of the elements" @@ -76,10 +77,11 @@ enumerator SEQUENCE_TYPE \ "theory/strings/type_enumerator.h" constant CONST_SEQUENCE \ - ::cvc5::Sequence \ - ::cvc5::SequenceHashFunction \ - "expr/sequence.h" \ - "a sequence of characters" + class \ + Sequence \ + ::cvc5::SequenceHashFunction \ + "expr/sequence.h" \ + "a sequence of characters" operator SEQ_UNIT 1 "a sequence of length one" operator SEQ_NTH 2 "The nth element of a sequence" @@ -101,17 +103,19 @@ operator REGEXP_EMPTY 0 "regexp empty" operator REGEXP_SIGMA 0 "regexp all characters" constant REGEXP_REPEAT_OP \ - ::cvc5::RegExpRepeat \ - ::cvc5::RegExpRepeatHashFunction \ - "util/regexp.h" \ - "operator for regular expression repeat; payload is an instance of the cvc5::RegExpRepeat class" + struct \ + RegExpRepeat \ + ::cvc5::RegExpRepeatHashFunction \ + "util/regexp.h" \ + "operator for regular expression repeat; payload is an instance of the cvc5::RegExpRepeat class" parameterized REGEXP_REPEAT REGEXP_REPEAT_OP 1 "regular expression repeat; first parameter is a REGEXP_REPEAT_OP, second is a regular expression term" constant REGEXP_LOOP_OP \ - ::cvc5::RegExpLoop \ - ::cvc5::RegExpLoopHashFunction \ - "util/regexp.h" \ - "operator for regular expression loop; payload is an instance of the cvc5::RegExpLoop class" + struct \ + RegExpLoop \ + ::cvc5::RegExpLoopHashFunction \ + "util/regexp.h" \ + "operator for regular expression loop; payload is an instance of the cvc5::RegExpLoop class" parameterized REGEXP_LOOP REGEXP_LOOP_OP 1 "regular expression loop; first parameter is a REGEXP_LOOP_OP, second is a regular expression term" #internal diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index c3580d963..ac0e487f9 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -20,6 +20,8 @@ #include "theory/rewriter.h" #include "theory/strings/regexp_entail.h" #include "theory/strings/theory_strings_utils.h" +#include "util/rational.h" +#include "util/string.h" using namespace cvc5::kind; @@ -90,7 +92,8 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) // into fixed length regular expressions are easy to handle. // the index of _* in re unsigned pivotIndex = 0; - size_t numPivotIndex = 0; + bool hasPivotIndex = false; + bool hasFixedLength = true; std::vector<Node> childLengths; std::vector<Node> childLengthsPostPivot; for (unsigned i = 0, size = children.size(); i < size; i++) @@ -99,34 +102,34 @@ Node RegExpElimination::eliminateConcat(Node atom, bool isAgg) Node fl = RegExpEntail::getFixedLengthForRegexp(c); if (fl.isNull()) { - if (numPivotIndex == 0 && c.getKind() == REGEXP_STAR + if (!hasPivotIndex && c.getKind() == REGEXP_STAR && c[0].getKind() == REGEXP_SIGMA) { - numPivotIndex = 1; + hasPivotIndex = true; pivotIndex = i; // zero is used in sum below and is used for concat-fixed-len fl = zero; } else { - numPivotIndex++; + hasFixedLength = false; } } if (!fl.isNull()) { childLengths.push_back(fl); - if (numPivotIndex > 0) + if (hasPivotIndex) { childLengthsPostPivot.push_back(fl); } } } - Node lenSum = childLengths.size() > 1 ? nm->mkNode(PLUS, childLengths) - : childLengths[0]; - // if we have at most one pivot index - if (numPivotIndex <= 1) + Node lenSum = childLengths.size() > 1 + ? nm->mkNode(PLUS, childLengths) + : (childLengths.empty() ? zero : childLengths[0]); + // if we have a fixed length + if (hasFixedLength) { - bool hasPivotIndex = (numPivotIndex == 1); Assert(re.getNumChildren() == children.size()); std::vector<Node> conc; conc.push_back(nm->mkNode(hasPivotIndex ? GEQ : EQUAL, lenx, lenSum)); diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp index b789db6a4..3d4a2d143 100644 --- a/src/theory/strings/regexp_entail.cpp +++ b/src/theory/strings/regexp_entail.cpp @@ -18,6 +18,8 @@ #include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" +#include "util/string.h" using namespace std; using namespace cvc5::kind; diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 96351cda9..106ce09d0 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -23,6 +23,7 @@ #include "theory/strings/regexp_entail.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/regexp.h" using namespace cvc5::kind; diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp index 91cea5fe8..7ef1242c6 100644 --- a/src/theory/strings/sequences_rewriter.cpp +++ b/src/theory/strings/sequences_rewriter.cpp @@ -25,7 +25,10 @@ #include "theory/strings/strings_rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" +#include "util/regexp.h" #include "util/statistics_registry.h" +#include "util/string.h" using namespace std; using namespace cvc5::kind; diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index e5e014f9d..1ddf2af58 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -18,6 +18,7 @@ #include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" using namespace std; using namespace cvc5::context; diff --git a/src/theory/strings/strings_entail.cpp b/src/theory/strings/strings_entail.cpp index a5d01eefd..a527d99dc 100644 --- a/src/theory/strings/strings_entail.cpp +++ b/src/theory/strings/strings_entail.cpp @@ -21,6 +21,8 @@ #include "theory/strings/sequences_rewriter.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" +#include "util/string.h" using namespace cvc5::kind; diff --git a/src/theory/strings/strings_fmf.cpp b/src/theory/strings/strings_fmf.cpp index f5ccc3bef..9bb6a2420 100644 --- a/src/theory/strings/strings_fmf.cpp +++ b/src/theory/strings/strings_fmf.cpp @@ -15,6 +15,8 @@ #include "theory/strings/strings_fmf.h" +#include "util/rational.h" + using namespace std; using namespace cvc5::context; using namespace cvc5::kind; diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp index 41a8ac448..b455d8a9b 100644 --- a/src/theory/strings/strings_rewriter.cpp +++ b/src/theory/strings/strings_rewriter.cpp @@ -19,6 +19,7 @@ #include "expr/node_builder.h" #include "theory/strings/theory_strings_utils.h" #include "util/rational.h" +#include "util/string.h" using namespace cvc5::kind; diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index c6710fb73..c7b3b5300 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -23,6 +23,8 @@ #include "theory/strings/inference_manager.h" #include "theory/strings/theory_strings_utils.h" #include "theory/strings/word.h" +#include "util/rational.h" +#include "util/string.h" using namespace std; using namespace cvc5::context; diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 3da682871..83a4fa04a 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -24,7 +24,9 @@ #include "theory/strings/arith_entail.h" #include "theory/strings/sequences_rewriter.h" #include "theory/strings/word.h" +#include "util/rational.h" #include "util/statistics_registry.h" +#include "util/string.h" using namespace cvc5; using namespace cvc5::kind; diff --git a/src/theory/strings/theory_strings_type_rules.cpp b/src/theory/strings/theory_strings_type_rules.cpp index a7e891d86..183344aa2 100644 --- a/src/theory/strings/theory_strings_type_rules.cpp +++ b/src/theory/strings/theory_strings_type_rules.cpp @@ -19,6 +19,7 @@ #include "expr/node_manager.h" #include "expr/sequence.h" #include "options/strings_options.h" +#include "util/cardinality.h" namespace cvc5 { namespace theory { diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index ed610ca95..c763557ca 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -22,6 +22,9 @@ #include "theory/strings/arith_entail.h" #include "theory/strings/strings_entail.h" #include "theory/strings/word.h" +#include "util/rational.h" +#include "util/regexp.h" +#include "util/string.h" using namespace cvc5::kind; diff --git a/src/theory/strings/type_enumerator.cpp b/src/theory/strings/type_enumerator.cpp index 1f2f31a61..5641312cb 100644 --- a/src/theory/strings/type_enumerator.cpp +++ b/src/theory/strings/type_enumerator.cpp @@ -15,6 +15,7 @@ #include "theory/strings/type_enumerator.h" +#include "expr/sequence.h" #include "theory/strings/theory_strings_utils.h" #include "util/string.h" |