summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2021-12-17 15:19:46 -0800
committerGitHub <noreply@github.com>2021-12-17 23:19:46 +0000
commitd4f887d72b2bd48b2935838e2e0cf98ba049b96c (patch)
tree7aebad5efbac15c3391df86cf00c7694946866f4
parentc67bbf88a0da5c7c066de5ba9e31b58f00594b9b (diff)
[Strings] Minor fixes/improvements (#7837)
This is a quick follow-up for PR #7815. My comments didn't make it in before the PR was merged, so this commit fixes some of the minor issues I found.
-rw-r--r--src/theory/strings/core_solver.cpp23
-rw-r--r--src/theory/strings/theory_strings.cpp3
2 files changed, 3 insertions, 23 deletions
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index eb3c70a83..84fd3af71 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -102,27 +102,6 @@ void CoreSolver::debugPrintFlatForms( const char * tc ){
Trace( tc ) << std::endl;
}
-struct sortConstLength {
- std::map< Node, unsigned > d_const_length;
- bool operator() (Node i, Node j) {
- std::map< Node, unsigned >::iterator it_i = d_const_length.find( i );
- std::map< Node, unsigned >::iterator it_j = d_const_length.find( j );
- if( it_i==d_const_length.end() ){
- if( it_j==d_const_length.end() ){
- return i<j;
- }else{
- return false;
- }
- }else{
- if( it_j==d_const_length.end() ){
- return true;
- }else{
- return it_i->second<it_j->second;
- }
- }
- }
-};
-
void CoreSolver::checkCycles()
{
// first check for cycles, while building ordering of equivalence classes
@@ -1988,7 +1967,7 @@ void CoreSolver::processDeq(Node ni, Node nj)
{
// If using the sequence update solver, we always apply extensionality.
// This is required for model soundness currently, although we could
- // investigate determine cases where the disequality is already
+ // investigate determining cases where the disequality is already
// satisfied (for optimization).
if (options().strings.seqArray != options::SeqArrayMode::NONE)
{
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 4c60b5141..6f19a5aaf 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -268,7 +268,8 @@ struct SortSeqIndex
{
SortSeqIndex() {}
/** the comparison */
- bool operator()(std::pair<Node, Node> i, std::pair<Node, Node> j)
+ bool operator()(const std::pair<Node, Node>& i,
+ const std::pair<Node, Node>& j)
{
Assert(i.first.isConst() && i.first.getType().isInteger()
&& j.first.isConst() && j.first.getType().isInteger());
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback