From: Andrew Reynolds Date: Tue, 8 Dec 2020 07:50:10 +0000 (-0600) Subject: Make term indices in the strings base solver aware of types (#5589) X-Git-Tag: cvc5-1.0.0~2482 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=384ab75e8637e872b568b6f493612d308f3f15ee;p=cvc5.git Make term indices in the strings base solver aware of types (#5589) This is required for handling inputs that combine strings and sequences. Fixes #5542. --- diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 451c01f8c..93803ea02 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -44,8 +44,10 @@ void BaseSolver::checkInit() d_termIndex.clear(); d_stringsEqc.clear(); - std::map ncongruent; - std::map congruent; + Trace("strings-base") << "BaseSolver::checkInit" << std::endl; + // count of congruent, non-congruent per operator (independent of type), + // for debugging. + std::map> congruentCount; eq::EqualityEngine* ee = d_state.getEqualityEngine(); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee); while (!eqcs_i.isFinished()) @@ -55,6 +57,8 @@ void BaseSolver::checkInit() if (!tn.isRegExp()) { Node emps; + // get the term index for type tn + std::map& tti = d_termIndex[tn]; if (tn.isStringLike()) { d_stringsEqc.push_back(eqc); @@ -66,6 +70,7 @@ void BaseSolver::checkInit() { Node n = *eqc_i; Kind k = n.getKind(); + Trace("strings-base") << "initialize term: " << n << std::endl; // process constant-like terms if (utils::isConstantLike(n)) { @@ -136,14 +141,17 @@ void BaseSolver::checkInit() if (d_congruent.find(n) == d_congruent.end()) { std::vector c; - Node nc = d_termIndex[k].add(n, 0, d_state, emps, c); + Node nc = tti[k].add(n, 0, d_state, emps, c); if (nc != n) { + Trace("strings-base-debug") + << "...found congruent term " << nc << std::endl; // check if we have inferred a new equality by removal of empty // components if (k == STRING_CONCAT && !d_state.areEqual(nc, n)) { std::vector exp; + // the number of empty components of n, nc size_t count[2] = {0, 0}; while (count[0] < nc.getNumChildren() || count[1] < n.getNumChildren()) @@ -163,6 +171,9 @@ void BaseSolver::checkInit() count[t]++; } } + Trace("strings-base-debug") + << " counts = " << count[0] << ", " << count[1] + << std::endl; // explain equal components if (count[0] < nc.getNumChildren()) { @@ -190,15 +201,15 @@ void BaseSolver::checkInit() // assuming that the reduction of f(a) depends on itself. } // this node is congruent to another one, we can ignore it - Trace("strings-process-debug") + Trace("strings-base-debug") << " congruent term : " << n << " (via " << nc << ")" << std::endl; d_congruent.insert(n); - congruent[k]++; + congruentCount[k].first++; } else if (k == STRING_CONCAT && c.size() == 1) { - Trace("strings-process-debug") + Trace("strings-base-debug") << " congruent term by singular : " << n << " " << c[0] << std::endl; // singular case @@ -229,16 +240,16 @@ void BaseSolver::checkInit() d_im.sendInference(exp, n.eqNode(ns), Inference::I_NORM_S); } d_congruent.insert(n); - congruent[k]++; + congruentCount[k].first++; } else { - ncongruent[k]++; + congruentCount[k].second++; } } else { - congruent[k]++; + congruentCount[k].first++; } } } @@ -254,14 +265,14 @@ void BaseSolver::checkInit() } else if (var > n) { - Trace("strings-process-debug") + Trace("strings-base-debug") << " congruent variable : " << var << std::endl; d_congruent.insert(var); var = n; } else { - Trace("strings-process-debug") + Trace("strings-base-debug") << " congruent variable : " << n << std::endl; d_congruent.insert(n); } @@ -272,17 +283,17 @@ void BaseSolver::checkInit() } ++eqcs_i; } - if (Trace.isOn("strings-process")) + if (Trace.isOn("strings-base")) { - for (std::map::iterator it = d_termIndex.begin(); - it != d_termIndex.end(); - ++it) + for (const std::pair>& cc : + congruentCount) { - Trace("strings-process") - << " Terms[" << it->first << "] = " << ncongruent[it->first] << "/" - << (congruent[it->first] + ncongruent[it->first]) << std::endl; + Trace("strings-base") + << " Terms[" << cc.first << "] = " << cc.second.second << "/" + << (cc.second.first + cc.second.second) << std::endl; } } + Trace("strings-base") << "BaseSolver::checkInit finished" << std::endl; } void BaseSolver::checkConstantEquivalenceClasses() @@ -293,17 +304,27 @@ void BaseSolver::checkConstantEquivalenceClasses() do { vecc.clear(); - Trace("strings-process-debug") + Trace("strings-base-debug") << "Check constant equivalence classes..." << std::endl; prevSize = d_eqcInfo.size(); - checkConstantEquivalenceClasses(&d_termIndex[STRING_CONCAT], vecc, true); + for (std::pair>& tindex : + d_termIndex) + { + checkConstantEquivalenceClasses( + &tindex.second[STRING_CONCAT], vecc, true); + } } while (!d_im.hasProcessed() && d_eqcInfo.size() > prevSize); if (!d_im.hasProcessed()) { // now, go back and set "most content" terms vecc.clear(); - checkConstantEquivalenceClasses(&d_termIndex[STRING_CONCAT], vecc, false); + for (std::pair>& tindex : + d_termIndex) + { + checkConstantEquivalenceClasses( + &tindex.second[STRING_CONCAT], vecc, false); + } } } diff --git a/src/theory/strings/base_solver.h b/src/theory/strings/base_solver.h index 87f136dd0..929034e42 100644 --- a/src/theory/strings/base_solver.h +++ b/src/theory/strings/base_solver.h @@ -235,8 +235,8 @@ class BaseSolver std::map d_eqcInfo; /** The list of equivalence classes of type string */ std::vector d_stringsEqc; - /** A term index for each function kind */ - std::map d_termIndex; + /** A term index for each type, function kind pair */ + std::map > d_termIndex; /** the cardinality of the alphabet */ uint32_t d_cardSize; }; /* class BaseSolver */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 062478075..7b3f94c1a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1029,6 +1029,7 @@ set(regress_0_tests regress0/strings/issue5090.smt2 regress0/strings/issue5384-double-conflict.smt2 regress0/strings/issue5428-re-diff-assoc.smt2 + regress0/strings/issue5542-strings-seq-mix.smt2 regress0/strings/itos-entail.smt2 regress0/strings/large-model.smt2 regress0/strings/leadingzero001.smt2 diff --git a/test/regress/regress0/strings/issue5542-strings-seq-mix.smt2 b/test/regress/regress0/strings/issue5542-strings-seq-mix.smt2 new file mode 100644 index 000000000..56d1ddfb4 --- /dev/null +++ b/test/regress/regress0/strings/issue5542-strings-seq-mix.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) +(declare-fun a () String) +(declare-fun b () String) +(declare-fun c () (Seq Int)) +(assert (distinct b (str.++ a a))) +(assert (distinct (seq.unit 0) (seq.extract c 1 1))) +(assert (= (seq.len c) 1)) +(check-sat)