diff options
Diffstat (limited to 'src/theory/strings/base_solver.cpp')
| -rw-r--r-- | src/theory/strings/base_solver.cpp | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 1e30b1623..69d50a7d9 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -46,7 +46,7 @@ void BaseSolver::checkInit() // build term index d_eqcInfo.clear(); d_termIndex.clear(); - d_stringsEqc.clear(); + d_stringLikeEqc.clear(); Trace("strings-base") << "BaseSolver::checkInit" << std::endl; // count of congruent, non-congruent per operator (independent of type), @@ -65,7 +65,7 @@ void BaseSolver::checkInit() std::map<Kind, TermIndex>& tti = d_termIndex[tn]; if (tn.isStringLike()) { - d_stringsEqc.push_back(eqc); + d_stringLikeEqc.push_back(eqc); emps = Word::mkEmptyWord(tn); } Node var; @@ -512,7 +512,7 @@ void BaseSolver::checkCardinality() // between lengths of string terms that are disequal (DEQ-LENGTH-SP). std::map<TypeNode, std::vector<std::vector<Node> > > cols; std::map<TypeNode, std::vector<Node> > lts; - d_state.separateByLength(d_stringsEqc, cols, lts); + d_state.separateByLength(d_stringLikeEqc, cols, lts); for (std::pair<const TypeNode, std::vector<std::vector<Node> > >& c : cols) { checkCardinalityType(c.first, c.second, lts[c.first]); @@ -604,7 +604,8 @@ void BaseSolver::checkCardinalityType(TypeNode tn, if (lr.isConst()) { // if constant, compare - Node cmp = nm->mkNode(GEQ, lr, nm->mkConst(Rational(card_need))); + Node cmp = + nm->mkNode(GEQ, lr, nm->mkConst(CONST_RATIONAL, Rational(card_need))); cmp = rewrite(cmp); needsSplit = !cmp.getConst<bool>(); } @@ -618,7 +619,7 @@ void BaseSolver::checkCardinalityType(TypeNode tn, bool success = true; while (r < card_need && success) { - Node rr = nm->mkConst(Rational(r)); + Node rr = nm->mkConst(CONST_RATIONAL, Rational(r)); if (d_state.areDisequal(rr, lr)) { r++; @@ -668,7 +669,7 @@ void BaseSolver::checkCardinalityType(TypeNode tn, << std::endl; if (int_k + 1 > ei->d_cardinalityLemK.get()) { - Node k_node = nm->mkConst(Rational(int_k)); + Node k_node = nm->mkConst(CONST_RATIONAL, Rational(int_k)); // add cardinality lemma Node dist = nm->mkNode(DISTINCT, cols[i]); std::vector<Node> expn; @@ -758,9 +759,9 @@ Node BaseSolver::explainBestContentEqc(Node n, Node eqc, std::vector<Node>& exp) return Node::null(); } -const std::vector<Node>& BaseSolver::getStringEqc() const +const std::vector<Node>& BaseSolver::getStringLikeEqc() const { - return d_stringsEqc; + return d_stringLikeEqc; } Node BaseSolver::TermIndex::add(TNode n, |