1 /********************* */
2 /*! \file normal_form.cpp
4 ** Top contributors (to current version):
5 ** Andrew Reynolds, Andres Noetzli
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
8 ** in the top-level source directory and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief Implementation of normal form data structure for the theory of
16 #include "theory/strings/normal_form.h"
18 #include "options/strings_options.h"
19 #include "theory/rewriter.h"
20 #include "theory/strings/theory_strings_utils.h"
21 #include "theory/strings/word.h"
24 using namespace CVC4::kind
;
30 void NormalForm::init(Node base
)
32 Assert(base
.getType().isStringLike());
33 Assert(base
.getKind() != STRING_CONCAT
);
41 if (!base
.isConst() || Word::getLength(base
) > 0)
47 void NormalForm::reverse()
49 std::reverse(d_nf
.begin(), d_nf
.end());
53 void NormalForm::splitConstant(unsigned index
, Node c1
, Node c2
)
55 Assert(Rewriter::rewrite(NodeManager::currentNM()->mkNode(
56 STRING_CONCAT
, d_isRev
? c2
: c1
, d_isRev
? c1
: c2
))
58 d_nf
.insert(d_nf
.begin() + index
+ 1, c2
);
60 // update the dependency indices
61 // notice this is not critical for soundness: not doing the below incrementing
62 // will only lead to overapproximating when antecedants are required in
64 for (const std::pair
<const Node
, std::map
<bool, unsigned> >& pe
: d_expDep
)
66 for (const auto& pep
: pe
.second
)
68 // See if this can be incremented: it can if this literal is not relevant
69 // to the current index, and hence it is not relevant for both c1 and c2.
70 Assert(pep
.second
>= 0 && pep
.second
<= d_nf
.size());
71 bool increment
= (pep
.first
== d_isRev
)
73 : (d_nf
.size() - 1 - pep
.second
) < index
;
76 d_expDep
[pe
.first
][pep
.first
] = pep
.second
+ 1;
82 void NormalForm::addToExplanation(Node exp
,
86 Assert(!exp
.isConst());
87 if (std::find(d_exp
.begin(), d_exp
.end(), exp
) == d_exp
.end())
91 for (unsigned k
= 0; k
< 2; k
++)
93 unsigned val
= k
== 0 ? new_val
: new_rev_val
;
94 std::map
<bool, unsigned>::iterator itned
= d_expDep
[exp
].find(k
== 1);
95 if (itned
== d_expDep
[exp
].end())
97 Trace("strings-process-debug")
98 << "Deps : set dependency on " << exp
<< " to " << val
99 << " isRev=" << (k
== 0) << std::endl
;
100 d_expDep
[exp
][k
== 1] = val
;
104 Trace("strings-process-debug")
105 << "Deps : Multiple dependencies on " << exp
<< " : " << itned
->second
106 << " " << val
<< " isRev=" << (k
== 0) << std::endl
;
107 // if we already have a dependency (in the case of non-linear string
108 // equalities), it is min/max
109 bool cmp
= val
> itned
->second
;
112 d_expDep
[exp
][k
== 1] = val
;
118 void NormalForm::getExplanation(int index
, std::vector
<Node
>& curr_exp
)
120 if (index
== -1 || !options::stringMinPrefixExplain())
122 curr_exp
.insert(curr_exp
.end(), d_exp
.begin(), d_exp
.end());
125 for (const Node
& exp
: d_exp
)
127 int dep
= static_cast<int>(d_expDep
[exp
][d_isRev
]);
130 curr_exp
.push_back(exp
);
131 Trace("strings-explain-prefix-debug") << " include : ";
135 Trace("strings-explain-prefix-debug") << " exclude : ";
137 Trace("strings-explain-prefix-debug") << exp
<< std::endl
;
141 Node
NormalForm::collectConstantStringAt(size_t& index
)
144 while (d_nf
.size() > index
&& d_nf
[index
].isConst())
146 c
.push_back(d_nf
[index
]);
153 std::reverse(c
.begin(), c
.end());
155 Node cc
= Rewriter::rewrite(utils::mkConcat(c
, c
[0].getType()));
156 Assert(cc
.isConst());
165 void NormalForm::getExplanationForPrefixEq(NormalForm
& nfi
,
169 std::vector
<Node
>& curr_exp
)
171 Assert(nfi
.d_isRev
== nfj
.d_isRev
);
172 Trace("strings-explain-prefix")
173 << "Get explanation for prefix " << index_i
<< ", " << index_j
174 << ", reverse = " << nfi
.d_isRev
<< std::endl
;
176 nfi
.getExplanation(index_i
, curr_exp
);
177 nfj
.getExplanation(index_j
, curr_exp
);
178 Trace("strings-explain-prefix")
179 << "Included " << curr_exp
.size() << " / "
180 << (nfi
.d_exp
.size() + nfj
.d_exp
.size()) << std::endl
;
181 // add explanation for why they are equal
182 Node eq
= nfi
.d_base
.eqNode(nfj
.d_base
);
183 curr_exp
.push_back(eq
);
186 } // namespace strings
187 } // namespace theory