summaryrefslogtreecommitdiff
path: root/src/theory/strings
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings')
-rw-r--r--src/theory/strings/arith_entail.cpp1
-rw-r--r--src/theory/strings/base_solver.cpp1
-rw-r--r--src/theory/strings/core_solver.cpp3
-rw-r--r--src/theory/strings/inference_manager.cpp1
-rw-r--r--src/theory/strings/kinds36
-rw-r--r--src/theory/strings/regexp_elim.cpp23
-rw-r--r--src/theory/strings/regexp_entail.cpp2
-rw-r--r--src/theory/strings/regexp_operation.cpp1
-rw-r--r--src/theory/strings/sequences_rewriter.cpp3
-rw-r--r--src/theory/strings/solver_state.cpp1
-rw-r--r--src/theory/strings/strings_entail.cpp2
-rw-r--r--src/theory/strings/strings_fmf.cpp2
-rw-r--r--src/theory/strings/strings_rewriter.cpp1
-rw-r--r--src/theory/strings/term_registry.cpp2
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp2
-rw-r--r--src/theory/strings/theory_strings_type_rules.cpp1
-rw-r--r--src/theory/strings/theory_strings_utils.cpp3
-rw-r--r--src/theory/strings/type_enumerator.cpp1
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"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback