diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-06 17:12:29 -0600 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-11-06 15:12:29 -0800 |
commit | cbd86eb4ed8bafc17f28244b746a376a019462f1 (patch) | |
tree | 69abc6102e61036f9e60c8276f350d68eaecb931 /src/theory/strings/inference_manager.cpp | |
parent | bef9df667e2788cab327b0c8c6590ba833297670 (diff) |
Move more string utility functions (#3398)
This is work towards splitting a "core solver" object from TheoryStrings.
This moves global functions from TheoryStrings to InferenceManager/SolverState, making them accessible in the future by modules that have references to these objects.
It also corrects an issue where we were maintaining two `d_conflict` fields.
Diffstat (limited to 'src/theory/strings/inference_manager.cpp')
-rw-r--r-- | src/theory/strings/inference_manager.cpp | 199 |
1 files changed, 195 insertions, 4 deletions
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 5c08fdee3..c9a2bcd70 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -34,10 +34,14 @@ InferenceManager::InferenceManager(TheoryStrings& p, context::UserContext* u, SolverState& s, OutputChannel& out) - : d_parent(p), d_state(s), d_out(out), d_keep(c) + : d_parent(p), d_state(s), d_out(out), d_keep(c), d_lengthLemmaTermsCache(u) { - d_true = NodeManager::currentNM()->mkConst(true); - d_false = NodeManager::currentNM()->mkConst(false); + NodeManager* nm = NodeManager::currentNM(); + d_zero = nm->mkConst(Rational(0)); + d_one = nm->mkConst(Rational(1)); + d_emptyString = nm->mkConst(::CVC4::String("")); + d_true = nm->mkConst(true); + d_false = nm->mkConst(false); } bool InferenceManager::sendInternalInference(std::vector<Node>& exp, @@ -131,7 +135,7 @@ void InferenceManager::sendInference(const std::vector<Node>& exp, Node eq_exp; if (options::stringRExplainLemmas()) { - eq_exp = d_parent.mkExplain(exp, exp_n); + eq_exp = mkExplain(exp, exp_n); } else { @@ -279,6 +283,95 @@ void InferenceManager::sendPhaseRequirement(Node lit, bool pol) d_pendingReqPhase[lit] = pol; } +void InferenceManager::registerLength(Node n, LengthStatus s) +{ + if (d_lengthLemmaTermsCache.find(n) != d_lengthLemmaTermsCache.end()) + { + return; + } + d_lengthLemmaTermsCache.insert(n); + + if (s == LENGTH_IGNORE) + { + // ignore it + return; + } + + NodeManager* nm = NodeManager::currentNM(); + Node n_len = nm->mkNode(kind::STRING_LENGTH, n); + + if (s == LENGTH_GEQ_ONE) + { + Node neq_empty = n.eqNode(d_emptyString).negate(); + Node len_n_gt_z = nm->mkNode(GT, n_len, d_zero); + Node len_geq_one = nm->mkNode(AND, neq_empty, len_n_gt_z); + Trace("strings-lemma") << "Strings::Lemma SK-GEQ-ONE : " << len_geq_one + << std::endl; + Trace("strings-assert") << "(assert " << len_geq_one << ")" << std::endl; + d_out.lemma(len_geq_one); + return; + } + + if (s == LENGTH_ONE) + { + Node len_one = n_len.eqNode(d_one); + Trace("strings-lemma") << "Strings::Lemma SK-ONE : " << len_one + << std::endl; + Trace("strings-assert") << "(assert " << len_one << ")" << std::endl; + d_out.lemma(len_one); + return; + } + Assert(s == LENGTH_SPLIT); + + if (options::stringSplitEmp() || !options::stringLenGeqZ()) + { + Node n_len_eq_z = n_len.eqNode(d_zero); + Node n_len_eq_z_2 = n.eqNode(d_emptyString); + Node case_empty = nm->mkNode(AND, n_len_eq_z, n_len_eq_z_2); + case_empty = Rewriter::rewrite(case_empty); + Node case_nempty = nm->mkNode(GT, n_len, d_zero); + if (!case_empty.isConst()) + { + Node lem = nm->mkNode(OR, case_empty, case_nempty); + d_out.lemma(lem); + Trace("strings-lemma") + << "Strings::Lemma LENGTH >= 0 : " << lem << std::endl; + // prefer trying the empty case first + // notice that requirePhase must only be called on rewritten literals that + // occur in the CNF stream. + n_len_eq_z = Rewriter::rewrite(n_len_eq_z); + Assert(!n_len_eq_z.isConst()); + d_out.requirePhase(n_len_eq_z, true); + n_len_eq_z_2 = Rewriter::rewrite(n_len_eq_z_2); + Assert(!n_len_eq_z_2.isConst()); + d_out.requirePhase(n_len_eq_z_2, true); + } + else if (!case_empty.getConst<bool>()) + { + // the rewriter knows that n is non-empty + Trace("strings-lemma") + << "Strings::Lemma LENGTH > 0 (non-empty): " << case_nempty + << std::endl; + d_out.lemma(case_nempty); + } + else + { + // If n = "" ---> true or len( n ) = 0 ----> true, then we expect that + // n ---> "". Since this method is only called on non-constants n, it must + // be that n = "" ^ len( n ) = 0 does not rewrite to true. + Assert(false); + } + } + + // additionally add len( x ) >= 0 ? + if (options::stringLenGeqZ()) + { + Node n_len_geq = nm->mkNode(kind::GEQ, n_len, d_zero); + n_len_geq = Rewriter::rewrite(n_len_geq); + d_out.lemma(n_len_geq); + } +} + void InferenceManager::addToExplanation(Node a, Node b, std::vector<Node>& exp) const @@ -435,6 +528,104 @@ void InferenceManager::inferSubstitutionProxyVars( } } +Node InferenceManager::mkExplain(const std::vector<Node>& a) const +{ + std::vector<Node> an; + return mkExplain(a, an); +} + +Node InferenceManager::mkExplain(const std::vector<Node>& a, + const std::vector<Node>& an) const +{ + std::vector<TNode> antec_exp; + // copy to processing vector + std::vector<Node> aconj; + for (const Node& ac : a) + { + utils::flattenOp(AND, ac, aconj); + } + eq::EqualityEngine* ee = d_state.getEqualityEngine(); + for (const Node& apc : aconj) + { + Assert(apc.getKind() != AND); + Debug("strings-explain") << "Add to explanation " << apc << std::endl; + if (apc.getKind() == NOT && apc[0].getKind() == EQUAL) + { + Assert(ee->hasTerm(apc[0][0])); + Assert(ee->hasTerm(apc[0][1])); + // ensure that we are ready to explain the disequality + AlwaysAssert(ee->areDisequal(apc[0][0], apc[0][1], true)); + } + Assert(apc.getKind() != EQUAL || ee->areEqual(apc[0], apc[1])); + // now, explain + explain(apc, antec_exp); + } + for (const Node& anc : an) + { + if (std::find(antec_exp.begin(), antec_exp.end(), anc) == antec_exp.end()) + { + Debug("strings-explain") + << "Add to explanation (new literal) " << anc << std::endl; + antec_exp.push_back(anc); + } + } + Node ant; + if (antec_exp.empty()) + { + ant = d_true; + } + else if (antec_exp.size() == 1) + { + ant = antec_exp[0]; + } + else + { + ant = NodeManager::currentNM()->mkNode(kind::AND, antec_exp); + } + return ant; +} + +void InferenceManager::explain(TNode literal, + std::vector<TNode>& assumptions) const +{ + Debug("strings-explain") << "Explain " << literal << " " + << d_state.isInConflict() << std::endl; + eq::EqualityEngine* ee = d_state.getEqualityEngine(); + bool polarity = literal.getKind() != NOT; + TNode atom = polarity ? literal : literal[0]; + std::vector<TNode> tassumptions; + if (atom.getKind() == EQUAL) + { + if (atom[0] != atom[1]) + { + Assert(ee->hasTerm(atom[0])); + Assert(ee->hasTerm(atom[1])); + ee->explainEquality(atom[0], atom[1], polarity, tassumptions); + } + } + else + { + ee->explainPredicate(atom, polarity, tassumptions); + } + for (const TNode a : tassumptions) + { + if (std::find(assumptions.begin(), assumptions.end(), a) + == assumptions.end()) + { + assumptions.push_back(a); + } + } + if (Debug.isOn("strings-explain-debug")) + { + Debug("strings-explain-debug") + << "Explanation for " << literal << " was " << std::endl; + for (const TNode a : tassumptions) + { + Debug("strings-explain-debug") << " " << a << std::endl; + } + } +} + } // namespace strings } // namespace theory } // namespace CVC4 |