diff options
| -rw-r--r-- | src/theory/strings/core_solver.cpp | 178 | ||||
| -rw-r--r-- | src/theory/strings/core_solver.h | 54 | ||||
| -rw-r--r-- | src/theory/strings/infer_info.cpp | 36 | ||||
| -rw-r--r-- | src/theory/strings/infer_info.h | 51 | ||||
| -rw-r--r-- | src/theory/strings/inference_manager.cpp | 279 | ||||
| -rw-r--r-- | src/theory/strings/inference_manager.h | 60 |
6 files changed, 362 insertions, 296 deletions
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index e574e4fa9..21b406ff3 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -30,13 +30,15 @@ namespace CVC4 { namespace theory { namespace strings { +CoreInferInfo::CoreInferInfo() : d_index(0), d_rev(false) {} + CoreSolver::CoreSolver(context::Context* c, context::UserContext* u, SolverState& s, InferenceManager& im, TermRegistry& tr, BaseSolver& bs) - : d_state(s), d_im(im), d_termReg(tr), d_bsolver(bs), d_nf_pairs(c) + : d_state(s), d_im(im), d_termReg(tr), d_bsolver(bs), d_nfPairs(c) { d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); @@ -914,7 +916,7 @@ void CoreSolver::processNEqc(std::vector<NormalForm>& normal_forms, TypeNode stype) { //the possible inferences - std::vector< InferInfo > pinfer; + std::vector<CoreInferInfo> pinfer; // loop over all pairs for(unsigned i=0; i<normal_forms.size()-1; i++) { //unify each normalform[j] with normal_forms[i] @@ -961,24 +963,28 @@ void CoreSolver::processNEqc(std::vector<NormalForm>& normal_forms, << ") : " << std::endl; Inference min_id = Inference::NONE; unsigned max_index = 0; - for (unsigned i = 0, size = pinfer.size(); i < size; i++) + for (unsigned i = 0, psize = pinfer.size(); i < psize; i++) { - Trace("strings-solve") << "#" << i << ": From " << pinfer[i].d_i << " / " - << pinfer[i].d_j << " (rev=" << pinfer[i].d_rev - << ") : "; - Trace("strings-solve") << pinfer[i].d_conc << " by " << pinfer[i].d_id - << std::endl; - if (!set_use_index || pinfer[i].d_id < min_id - || (pinfer[i].d_id == min_id && pinfer[i].d_index > max_index)) + CoreInferInfo& ipii = pinfer[i]; + InferInfo& ii = ipii.d_infer; + Trace("strings-solve") << "#" << i << ": From " << ipii.d_i << " / " + << ipii.d_j << " (rev=" << ipii.d_rev << ") : "; + Trace("strings-solve") << ii.d_conc << " by " << ii.d_id << std::endl; + if (!set_use_index || ii.d_id < min_id + || (ii.d_id == min_id && ipii.d_index > max_index)) { - min_id = pinfer[i].d_id; - max_index = pinfer[i].d_index; + min_id = ii.d_id; + max_index = ipii.d_index; use_index = i; set_use_index = true; } } Trace("strings-solve") << "...choose #" << use_index << std::endl; - doInferInfo(pinfer[use_index]); + if (!processInferInfo(pinfer[use_index])) + { + Unhandled() << "Failed to process infer info " << pinfer[use_index].d_infer + << std::endl; + } } void CoreSolver::processSimpleNEq(NormalForm& nfi, @@ -986,7 +992,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, unsigned& index, bool isRev, unsigned rproc, - std::vector<InferInfo>& pinfer, + std::vector<CoreInferInfo>& pinfer, TypeNode stype) { NodeManager* nm = NodeManager::currentNM(); @@ -1168,7 +1174,8 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, } // The candidate inference "info" - InferInfo info; + CoreInferInfo info; + InferInfo& iinfo = info.d_infer; info.d_index = index; // for debugging info.d_i = nfi.d_base; @@ -1189,9 +1196,9 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, << std::endl; Node lenEq = nm->mkNode(EQUAL, xLenTerm, yLenTerm); lenEq = Rewriter::rewrite(lenEq); - info.d_conc = nm->mkNode(OR, lenEq, lenEq.negate()); - info.d_pending_phase[lenEq] = true; - info.d_id = Inference::LEN_SPLIT; + iinfo.d_conc = nm->mkNode(OR, lenEq, lenEq.negate()); + iinfo.d_id = Inference::LEN_SPLIT; + info.d_pendingPhase[lenEq] = true; pinfer.push_back(info); break; } @@ -1205,7 +1212,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, // We are dealing with a looping word equation. if (!isRev) { // FIXME - NormalForm::getExplanationForPrefixEq(nfi, nfj, -1, -1, info.d_ant); + NormalForm::getExplanationForPrefixEq(nfi, nfj, -1, -1, iinfo.d_ant); ProcessLoopResult plr = processLoop(lhsLoopIdx != -1 ? nfi : nfj, lhsLoopIdx != -1 ? nfj : nfi, @@ -1263,14 +1270,14 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, // infer the purification equality, and the (dis)equality // with the empty string in the direction that the rewriter // inferred - info.d_conc = nm->mkNode( + iinfo.d_conc = nm->mkNode( AND, p.eqNode(nc), !eq.getConst<bool>() ? pEq.negate() : pEq); - info.d_id = Inference::INFER_EMP; + iinfo.d_id = Inference::INFER_EMP; } else { - info.d_conc = nm->mkNode(OR, eq, eq.negate()); - info.d_id = Inference::LEN_SPLIT_EMP; + iinfo.d_conc = nm->mkNode(OR, eq, eq.negate()); + iinfo.d_id = Inference::LEN_SPLIT_EMP; } pinfer.push_back(info); break; @@ -1278,7 +1285,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, // At this point, we know that `nc` is non-empty, so we add that to our // explanation. - info.d_ant.push_back(expNonEmpty); + iinfo.d_ant.push_back(expNonEmpty); size_t ncIndex = index + 1; Node nextConstStr = nfnc.collectConstantStringAt(ncIndex); @@ -1326,7 +1333,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, if (p > 1) { NormalForm::getExplanationForPrefixEq( - nfc, nfnc, cIndex, ncIndex, info.d_ant); + nfc, nfnc, cIndex, ncIndex, iinfo.d_ant); Node prea = p == straLen ? stra : (isRev ? Word::suffix(stra, p) : Word::prefix(stra, p)); @@ -1339,10 +1346,10 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, Trace("strings-csp") << "Const Split: " << prea << " is removed from " << stra << " due to " << strb << ", p=" << p << std::endl; - info.d_conc = nc.eqNode(isRev ? utils::mkNConcat(sk, prea) - : utils::mkNConcat(prea, sk)); - info.d_new_skolem[LENGTH_SPLIT].push_back(sk); - info.d_id = Inference::SSPLIT_CST_PROP; + iinfo.d_conc = nc.eqNode(isRev ? utils::mkNConcat(sk, prea) + : utils::mkNConcat(prea, sk)); + iinfo.d_new_skolem[LENGTH_SPLIT].push_back(sk); + iinfo.d_id = Inference::SSPLIT_CST_PROP; pinfer.push_back(info); break; } @@ -1365,11 +1372,12 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, Trace("strings-csp") << "Const Split: " << firstChar << " is removed from " << stra << " (serial) " << std::endl; - NormalForm::getExplanationForPrefixEq(nfi, nfj, index, index, info.d_ant); - info.d_conc = nc.eqNode(isRev ? utils::mkNConcat(sk, firstChar) - : utils::mkNConcat(firstChar, sk)); - info.d_new_skolem[LENGTH_SPLIT].push_back(sk); - info.d_id = Inference::SSPLIT_CST; + NormalForm::getExplanationForPrefixEq( + nfi, nfj, index, index, iinfo.d_ant); + iinfo.d_conc = nc.eqNode(isRev ? utils::mkNConcat(sk, firstChar) + : utils::mkNConcat(firstChar, sk)); + iinfo.d_new_skolem[LENGTH_SPLIT].push_back(sk); + iinfo.d_id = Inference::SSPLIT_CST; pinfer.push_back(info); break; } @@ -1415,7 +1423,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, } } - NormalForm::getExplanationForPrefixEq(nfi, nfj, index, index, info.d_ant); + NormalForm::getExplanationForPrefixEq(nfi, nfj, index, index, iinfo.d_ant); // Add premises for x != "" ^ y != "" for (unsigned xory = 0; xory < 2; xory++) { @@ -1423,12 +1431,12 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, Node tnz = d_state.explainNonEmpty(x); if (!tnz.isNull()) { - info.d_ant.push_back(tnz); + iinfo.d_ant.push_back(tnz); } else { tnz = x.eqNode(emp).negate(); - info.d_antn.push_back(tnz); + iinfo.d_antn.push_back(tnz); } } SkolemCache* skc = d_termReg.getSkolemCache(); @@ -1437,7 +1445,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, y, isRev ? SkolemCache::SK_ID_V_SPT_REV : SkolemCache::SK_ID_V_SPT, "v_spt"); - info.d_new_skolem[LENGTH_GEQ_ONE].push_back(sk); + iinfo.d_new_skolem[LENGTH_GEQ_ONE].push_back(sk); Node eq1 = x.eqNode(isRev ? utils::mkNConcat(sk, y) : utils::mkNConcat(y, sk)); Node eq2 = @@ -1445,16 +1453,16 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, if (lentTestSuccess != -1) { - info.d_antn.push_back(lentTestExp); - info.d_conc = lentTestSuccess == 0 ? eq1 : eq2; - info.d_id = Inference::SSPLIT_VAR_PROP; + iinfo.d_antn.push_back(lentTestExp); + iinfo.d_conc = lentTestSuccess == 0 ? eq1 : eq2; + iinfo.d_id = Inference::SSPLIT_VAR_PROP; } else { Node ldeq = nm->mkNode(EQUAL, xLenTerm, yLenTerm).negate(); - info.d_ant.push_back(ldeq); - info.d_conc = nm->mkNode(OR, eq1, eq2); - info.d_id = Inference::SSPLIT_VAR; + iinfo.d_ant.push_back(ldeq); + iinfo.d_conc = nm->mkNode(OR, eq1, eq2); + iinfo.d_id = Inference::SSPLIT_VAR; } pinfer.push_back(info); break; @@ -1500,10 +1508,10 @@ bool CoreSolver::detectLoop(NormalForm& nfi, //xs(zy)=t(yz)xr CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, - NormalForm& nfj, - int loop_index, - int index, - InferInfo& info) + NormalForm& nfj, + int loop_index, + int index, + CoreInferInfo& info) { if (options::stringProcessLoopMode() == options::ProcessLoopMode::ABORT) { @@ -1540,6 +1548,7 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, Node emp = Word::mkEmptyWord(stype); + InferInfo& iinfo = info.d_infer; if (s_zy.isConst() && r.isConst() && r != emp) { int c; @@ -1560,7 +1569,7 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, { Trace("strings-loop") << "Strings::Loop: tails are different." << std::endl; - d_im.sendInference(info.d_ant, conc, Inference::FLOOP_CONFLICT, true); + d_im.sendInference(iinfo.d_ant, conc, Inference::FLOOP_CONFLICT, true); return ProcessLoopResult::CONFLICT; } } @@ -1578,13 +1587,13 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, if (expNonEmpty.isNull()) { // try to make t equal to empty to avoid loop - info.d_conc = nm->mkNode(kind::OR, split_eq, split_eq.negate()); - info.d_id = Inference::LEN_SPLIT_EMP; + iinfo.d_conc = nm->mkNode(kind::OR, split_eq, split_eq.negate()); + iinfo.d_id = Inference::LEN_SPLIT_EMP; return ProcessLoopResult::INFERENCE; } else { - info.d_ant.push_back(expNonEmpty); + iinfo.d_ant.push_back(expNonEmpty); } } else @@ -1593,9 +1602,9 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, } } - Node ant = d_im.mkExplain(info.d_ant); - info.d_ant.clear(); - info.d_antn.push_back(ant); + Node ant = d_im.mkExplain(iinfo.d_ant); + iinfo.d_ant.clear(); + iinfo.d_antn.push_back(ant); Node str_in_re; if (s_zy == t_yz && r == emp && s_zy.isConst() @@ -1699,10 +1708,10 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi, } // normal case // we will be done - info.d_conc = conc; - info.d_id = Inference::FLOOP; - info.d_nf_pair[0] = nfi.d_base; - info.d_nf_pair[1] = nfj.d_base; + iinfo.d_conc = conc; + iinfo.d_id = Inference::FLOOP; + info.d_nfPair[0] = nfi.d_base; + info.d_nfPair[1] = nfj.d_base; return ProcessLoopResult::INFERENCE; } @@ -2116,11 +2125,12 @@ void CoreSolver::addNormalFormPair( Node n1, Node n2 ){ } if( !isNormalFormPair( n1, n2 ) ){ int index = 0; - NodeIntMap::const_iterator it = d_nf_pairs.find( n1 ); - if( it!=d_nf_pairs.end() ){ + NodeIntMap::const_iterator it = d_nfPairs.find(n1); + if (it != d_nfPairs.end()) + { index = (*it).second; } - d_nf_pairs[n1] = index + 1; + d_nfPairs[n1] = index + 1; if( index<(int)d_nf_pairs_data[n1].size() ){ d_nf_pairs_data[n1][index] = n2; }else{ @@ -2138,8 +2148,9 @@ bool CoreSolver::isNormalFormPair( Node n1, Node n2 ) { return isNormalFormPair(n2,n1); } //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl; - NodeIntMap::const_iterator it = d_nf_pairs.find( n1 ); - if( it!=d_nf_pairs.end() ){ + NodeIntMap::const_iterator it = d_nfPairs.find(n1); + if (it != d_nfPairs.end()) + { Assert(d_nf_pairs_data.find(n1) != d_nf_pairs_data.end()); for( int i=0; i<(*it).second; i++ ){ Assert(i < (int)d_nf_pairs_data[n1].size()); @@ -2286,29 +2297,34 @@ void CoreSolver::checkLengthsEqc() { } } -void CoreSolver::doInferInfo(const InferInfo& ii) +bool CoreSolver::processInferInfo(CoreInferInfo& cii) { - // send the inference - if (!ii.d_nf_pair[0].isNull()) + InferInfo& ii = cii.d_infer; + // rewrite the conclusion, ensure non-trivial + ii.d_conc = Rewriter::rewrite(ii.d_conc); + + if (ii.isTrivial()) { - Assert(!ii.d_nf_pair[1].isNull()); - addNormalFormPair(ii.d_nf_pair[0], ii.d_nf_pair[1]); + // conclusion rewrote to true + return false; } - // send the inference - d_im.sendInference(ii); - // Register the new skolems from this inference. We register them here - // (lazily), since the code above has now decided to use the inference - // at use_index that involves them. - for (const std::pair<const LengthStatus, std::vector<Node> >& sks : - ii.d_new_skolem) + // process the state change to this solver + if (!cii.d_nfPair[0].isNull()) { - for (const Node& n : sks.second) - { - d_termReg.registerTermAtomic(n, sks.first); - } + Assert(!cii.d_nfPair[1].isNull()); + addNormalFormPair(cii.d_nfPair[0], cii.d_nfPair[1]); } -} + // send phase requirements + for (const std::pair<const Node, bool> pp : cii.d_pendingPhase) + { + d_im.sendPhaseRequirement(pp.first, pp.second); + } + + // send the inference, which is a lemma + d_im.sendInference(ii, true); + return true; +} }/* CVC4::theory::strings namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/strings/core_solver.h b/src/theory/strings/core_solver.h index cef5bd3be..4328b8462 100644 --- a/src/theory/strings/core_solver.h +++ b/src/theory/strings/core_solver.h @@ -31,6 +31,45 @@ namespace CVC4 { namespace theory { namespace strings { +/** + * This data structure encapsulates an inference for the core solver of the + * theory of strings. This includes the form of the inference to be processed + * by the inference manager, the side effects it generates for the core solver, + * and information used for heuristics and debugging. + */ +class CoreInferInfo +{ + public: + CoreInferInfo(); + ~CoreInferInfo() {} + /** The infer info of this class */ + InferInfo d_infer; + /** + * The pending phase requirements, see InferenceManager::sendPhaseRequirement. + */ + std::map<Node, bool> d_pendingPhase; + /** + * The index in the normal forms under which this inference is addressing. + * For example, if the inference is inferring x = y from |x|=|y| and + * w ++ x ++ ... = w ++ y ++ ... + * then d_index is 1, since x and y are at index 1 in these concat terms. + */ + unsigned d_index; + /** + * The normal form pair that is cached as a result of this inference. + */ + Node d_nfPair[2]; + /** for debugging + * + * The base pair of strings d_i/d_j that led to the inference, and whether + * (d_rev) we were processing the normal forms of these strings in reverse + * direction. + */ + Node d_i; + Node d_j; + bool d_rev; +}; + /** The core solver for the theory of strings * * This implements techniques for handling (dis)equalities involving @@ -183,10 +222,11 @@ class CoreSolver private: /** * This processes the infer info ii as an inference. In more detail, it calls - * the inference manager to process the inference, it introduces Skolems, and - * updates the set of normal form pairs. + * the inference manager to process the inference, and updates the set of + * normal form pairs. Returns true if the conclusion of ii was not true + * after rewriting. If the conclusion is true, this method does nothing. */ - void doInferInfo(const InferInfo& ii); + bool processInferInfo(CoreInferInfo& ii); /** Add that (n1,n2) is a normal form pair in the current context. */ void addNormalFormPair(Node n1, Node n2); /** Is (n1,n2) a normal form pair in the current context? */ @@ -253,7 +293,7 @@ class CoreSolver * * This method is called when two equal terms have normal forms nfi and nfj. * It adds (typically at most one) possible inference to the vector pinfer. - * This inference is in the form of an InferInfo object, which stores the + * This inference is in the form of an CoreInferInfo object, which stores the * necessary information regarding how to process the inference. * * index: The index in the normal form vectors (nfi.d_nf and nfj.d_nf) that @@ -280,7 +320,7 @@ class CoreSolver unsigned& index, bool isRev, unsigned rproc, - std::vector<InferInfo>& pinfer, + std::vector<CoreInferInfo>& pinfer, TypeNode stype); //--------------------------end for checkNormalFormsEq @@ -309,7 +349,7 @@ class CoreSolver NormalForm& nfj, int loop_index, int index, - InferInfo& info); + CoreInferInfo& info); //--------------------------end for checkNormalFormsEq with loops //--------------------------for checkNormalFormsDeq @@ -402,7 +442,7 @@ class CoreSolver * indepedent map from nodes to lists of nodes to model this, given by * the two data members below. */ - NodeIntMap d_nf_pairs; + NodeIntMap d_nfPairs; std::map<Node, std::vector<Node> > d_nf_pairs_data; /** list of non-congruent concat terms in each equivalence class */ std::map<Node, std::vector<Node> > d_eqc; diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp index 6881970ef..9c4ebafa1 100644 --- a/src/theory/strings/infer_info.cpp +++ b/src/theory/strings/infer_info.cpp @@ -92,7 +92,41 @@ std::ostream& operator<<(std::ostream& out, Inference i) return out; } -InferInfo::InferInfo() : d_id(Inference::NONE), d_index(0), d_rev(false) {} +InferInfo::InferInfo() : d_id(Inference::NONE) {} + +bool InferInfo::isTrivial() const +{ + Assert(!d_conc.isNull()); + return d_conc.isConst() && d_conc.getConst<bool>(); +} + +bool InferInfo::isConflict() const +{ + Assert(!d_conc.isNull()); + return d_conc.isConst() && !d_conc.getConst<bool>() && d_antn.empty(); +} + +bool InferInfo::isFact() const +{ + Assert(!d_conc.isNull()); + TNode atom = d_conc.getKind() == kind::NOT ? d_conc[0] : d_conc; + return !atom.isConst() && atom.getKind() != kind::OR && d_antn.empty(); +} + +std::ostream& operator<<(std::ostream& out, const InferInfo& ii) +{ + out << "(infer " << ii.d_id << " " << ii.d_conc; + if (!ii.d_ant.empty()) + { + out << " :ant (" << ii.d_ant << ")"; + } + if (!ii.d_antn.empty()) + { + out << " :antn (" << ii.d_antn << ")"; + } + out << ")"; + return out; +} } // namespace strings } // namespace theory diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h index 7fce2eaf2..fca528d1b 100644 --- a/src/theory/strings/infer_info.h +++ b/src/theory/strings/infer_info.h @@ -328,19 +328,18 @@ enum LengthStatus }; /** - * This data structure encapsulates an inference for strings. This includes - * the form of the inference, as well as the side effects it generates. + * An inference. This is a class to track an unprocessed call to either + * send a fact, lemma, or conflict that is waiting to be asserted to the + * equality engine or sent on the output channel. */ class InferInfo { public: InferInfo(); - /** - * The identifier for the inference, indicating the kind of reasoning used - * for this conclusion. - */ + ~InferInfo() {} + /** The inference identifier */ Inference d_id; - /** The conclusion of the inference */ + /** The conclusion */ Node d_conc; /** * The antecedant(s) of the inference, interpreted conjunctively. These are @@ -359,32 +358,30 @@ class InferInfo * can be assumed for them. */ std::map<LengthStatus, std::vector<Node> > d_new_skolem; + /** Is this infer info trivial? True if d_conc is true. */ + bool isTrivial() const; /** - * The pending phase requirements, see InferenceManager::sendPhaseRequirement. - */ - std::map<Node, bool> d_pending_phase; - /** - * The index in the normal forms under which this inference is addressing. - * For example, if the inference is inferring x = y from |x|=|y| and - * w ++ x ++ ... = w ++ y ++ ... - * then d_index is 1, since x and y are at index 1 in these concat terms. + * Does this infer info correspond to a conflict? True if d_conc is false + * and it has no new antecedants (d_antn). */ - unsigned d_index; + bool isConflict() const; /** - * The normal form pair that is cached as a result of this inference. - */ - Node d_nf_pair[2]; - /** for debugging - * - * The base pair of strings d_i/d_j that led to the inference, and whether - * (d_rev) we were processing the normal forms of these strings in reverse - * direction. + * Does this infer info correspond to a "fact". A fact is an inference whose + * conclusion should be added as an equality or predicate to the equality + * engine with no new external antecedants (d_antn). */ - Node d_i; - Node d_j; - bool d_rev; + bool isFact() const; }; +/** + * Writes an inference info to a stream. + * + * @param out The stream to write to + * @param ii The inference info to write to the stream + * @return The stream + */ +std::ostream& operator<<(std::ostream& out, const InferInfo& ii); + } // namespace strings } // namespace theory } // namespace CVC4 diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 2a559faac..8e68913ac 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -117,83 +117,86 @@ bool InferenceManager::sendInternalInference(std::vector<Node>& exp, } void InferenceManager::sendInference(const std::vector<Node>& exp, - const std::vector<Node>& exp_n, + const std::vector<Node>& expn, Node eq, Inference infer, bool asLemma) { eq = eq.isNull() ? d_false : Rewriter::rewrite(eq); - if (Trace.isOn("strings-infer-debug")) - { - Trace("strings-infer-debug") - << "By " << infer << ", infer : " << eq << " from: " << std::endl; - for (unsigned i = 0; i < exp.size(); i++) - { - Trace("strings-infer-debug") << " " << exp[i] << std::endl; - } - for (unsigned i = 0; i < exp_n.size(); i++) - { - Trace("strings-infer-debug") << " N:" << exp_n[i] << std::endl; - } - } if (eq == d_true) { return; } - // only keep stats if not trivial conclusion - d_statistics.d_inferences << infer; - Node atom = eq.getKind() == NOT ? eq[0] : eq; - // check if we should send a lemma or an inference - if (asLemma || atom == d_false || atom.getKind() == OR || !exp_n.empty() - || options::stringInferAsLemmas()) + // wrap in infer info and send below + InferInfo ii; + ii.d_id = infer; + ii.d_conc = eq; + ii.d_ant = exp; + ii.d_antn = expn; + sendInference(ii, asLemma); +} + +void InferenceManager::sendInference(const std::vector<Node>& exp, + Node eq, + Inference infer, + bool asLemma) +{ + std::vector<Node> expn; + sendInference(exp, expn, eq, infer, asLemma); +} + +void InferenceManager::sendInference(const InferInfo& ii, bool asLemma) +{ + Assert(!ii.isTrivial()); + Trace("strings-infer-debug") + << "sendInference: " << ii << ", asLemma = " << asLemma << std::endl; + // check if we should send a conflict, lemma or a fact + if (asLemma || options::stringInferAsLemmas() || !ii.isFact()) { - Node eq_exp; - if (options::stringRExplainLemmas()) + if (ii.isConflict()) { - eq_exp = mkExplain(exp, exp_n); - } - else - { - if (exp.empty()) - { - eq_exp = utils::mkAnd(exp_n); - } - else if (exp_n.empty()) - { - eq_exp = utils::mkAnd(exp); - } - else - { - std::vector<Node> ev; - ev.insert(ev.end(), exp.begin(), exp.end()); - ev.insert(ev.end(), exp_n.begin(), exp_n.end()); - eq_exp = NodeManager::currentNM()->mkNode(AND, ev); - } - } - // if we have unexplained literals, this lemma is not a conflict - if (eq == d_false && !exp_n.empty()) - { - eq = eq_exp.negate(); - eq_exp = d_true; + Trace("strings-infer-debug") << "...as conflict" << std::endl; + Trace("strings-lemma") << "Strings::Conflict: " << ii.d_ant << " by " + << ii.d_id << std::endl; + Trace("strings-conflict") << "CONFLICT: inference conflict " << ii.d_ant + << " by " << ii.d_id << std::endl; + // we must fully explain it + Node conf = mkExplain(ii.d_ant); + Trace("strings-assert") << "(assert (not " << conf << ")) ; conflict " + << ii.d_id << std::endl; + ++(d_statistics.d_conflictsInfer); + // only keep stats if we process it here + d_statistics.d_inferences << ii.d_id; + d_out.conflict(conf); + d_state.setConflict(); + return; } - sendLemma(eq_exp, eq, infer); + Trace("strings-infer-debug") << "...as lemma" << std::endl; + d_pendingLem.push_back(ii); return; } - Node eqExp = utils::mkAnd(exp); if (options::stringInferSym()) { std::vector<Node> vars; std::vector<Node> subs; std::vector<Node> unproc; - d_termReg.inferSubstitutionProxyVars(eqExp, vars, subs, unproc); + for (const Node& ac : ii.d_ant) + { + d_termReg.inferSubstitutionProxyVars(ac, vars, subs, unproc); + } if (unproc.empty()) { - Node eqs = - eq.substitute(vars.begin(), vars.end(), subs.begin(), subs.end()); + Node eqs = ii.d_conc.substitute( + vars.begin(), vars.end(), subs.begin(), subs.end()); + InferInfo iiSubsLem; + // keep the same id for now, since we are transforming the form of the + // inference, not the root reason. + iiSubsLem.d_id = ii.d_id; + iiSubsLem.d_conc = eqs; if (Trace.isOn("strings-lemma-debug")) { - Trace("strings-lemma-debug") << "Strings::Infer " << eq << " from " - << eqExp << " by " << infer << std::endl; + Trace("strings-lemma-debug") + << "Strings::Infer " << iiSubsLem << std::endl; Trace("strings-lemma-debug") << "Strings::Infer Alternate : " << eqs << std::endl; for (unsigned i = 0, nvars = vars.size(); i < nvars; i++) @@ -202,7 +205,8 @@ void InferenceManager::sendInference(const std::vector<Node>& exp, << " " << vars[i] << " -> " << subs[i] << std::endl; } } - sendLemma(d_true, eqs, infer); + Trace("strings-infer-debug") << "...as symbolic lemma" << std::endl; + d_pendingLem.push_back(iiSubsLem); return; } if (Trace.isOn("strings-lemma-debug")) @@ -214,59 +218,11 @@ void InferenceManager::sendInference(const std::vector<Node>& exp, } } } - Trace("strings-lemma") << "Strings::Infer " << eq << " from " << eqExp - << " by " << infer << std::endl; - Trace("strings-assert") << "(assert (=> " << eqExp << " " << eq - << ")) ; infer " << infer << std::endl; - d_pending.push_back(PendingInfer(infer, eq, eqExp)); -} - -void InferenceManager::sendInference(const std::vector<Node>& exp, - Node eq, - Inference infer, - bool asLemma) -{ - std::vector<Node> exp_n; - sendInference(exp, exp_n, eq, infer, asLemma); -} - -void InferenceManager::sendInference(const InferInfo& i) -{ - sendInference(i.d_ant, i.d_antn, i.d_conc, i.d_id, true); -} - -void InferenceManager::sendLemma(Node ant, Node conc, Inference infer) -{ - if (conc.isNull() || conc == d_false) - { - Trace("strings-conflict") - << "Strings::Conflict : " << infer << " : " << ant << std::endl; - Trace("strings-lemma") << "Strings::Conflict : " << infer << " : " << ant - << std::endl; - Trace("strings-assert") - << "(assert (not " << ant << ")) ; conflict " << infer << std::endl; - ++(d_statistics.d_conflictsInfer); - d_out.conflict(ant); - d_state.setConflict(); - return; - } - Node lem; - if (ant == d_true) - { - lem = conc; - } - else - { - lem = NodeManager::currentNM()->mkNode(IMPLIES, ant, conc); - } - Trace("strings-lemma") << "Strings::Lemma " << infer << " : " << lem - << std::endl; - Trace("strings-assert") << "(assert " << lem << ") ; lemma " << infer - << std::endl; - d_pendingLem.push_back(lem); + Trace("strings-infer-debug") << "...as fact" << std::endl; + // add to pending, to be processed as a fact + d_pending.push_back(ii); } - bool InferenceManager::sendSplit(Node a, Node b, Inference infer, bool preq) { Node eq = a.eqNode(b); @@ -275,14 +231,12 @@ bool InferenceManager::sendSplit(Node a, Node b, Inference infer, bool preq) { return false; } - // update statistics - d_statistics.d_inferences << infer; NodeManager* nm = NodeManager::currentNM(); - Node lemma_or = nm->mkNode(OR, eq, nm->mkNode(NOT, eq)); - Trace("strings-lemma") << "Strings::Lemma " << infer - << " SPLIT : " << lemma_or << std::endl; - d_pendingLem.push_back(lemma_or); + InferInfo iiSplit; + iiSplit.d_id = infer; + iiSplit.d_conc = nm->mkNode(OR, eq, nm->mkNode(NOT, eq)); sendPhaseRequirement(eq, preq); + d_pendingLem.push_back(iiSplit); return true; } @@ -320,23 +274,25 @@ void InferenceManager::doPendingFacts() size_t i = 0; while (!d_state.isInConflict() && i < d_pending.size()) { - Node fact = d_pending[i].d_fact; - Node exp = d_pending[i].d_exp; - if (fact.getKind() == AND) - { - for (const Node& lit : fact) - { - bool polarity = lit.getKind() != NOT; - TNode atom = polarity ? lit : lit[0]; - assertPendingFact(atom, polarity, exp); - } - } - else - { - bool polarity = fact.getKind() != NOT; - TNode atom = polarity ? fact : fact[0]; - assertPendingFact(atom, polarity, exp); - } + InferInfo& ii = d_pending[i]; + // At this point, ii should be a "fact", i.e. something whose conclusion + // should be added as a normal equality or predicate to the equality engine + // with no new external assumptions (ii.d_antn). + Assert(ii.isFact()); + Node fact = ii.d_conc; + Node exp = utils::mkAnd(ii.d_ant); + Trace("strings-assert") << "(assert (=> " << exp << " " << fact + << ")) ; fact " << ii.d_id << std::endl; + // only keep stats if we process it here + Trace("strings-lemma") << "Strings::Fact: " << fact << " from " << exp + << " by " << ii.d_id << std::endl; + d_statistics.d_inferences << ii.d_id; + // assert it as a pending fact + bool polarity = fact.getKind() != NOT; + TNode atom = polarity ? fact : fact[0]; + // no double negation or double (conjunctive) conclusions + Assert(atom.getKind() != NOT && atom.getKind() != AND); + assertPendingFact(atom, polarity, exp); // Must reference count the equality and its explanation, which is not done // by the equality engine. Notice that we do not need to do this for // external assertions, which enter as facts through sendAssumption. @@ -349,21 +305,68 @@ void InferenceManager::doPendingFacts() void InferenceManager::doPendingLemmas() { - if (!d_state.isInConflict()) + if (d_state.isInConflict()) + { + // just clear the pending vectors, nothing else to do + d_pendingLem.clear(); + d_pendingReqPhase.clear(); + return; + } + NodeManager* nm = NodeManager::currentNM(); + for (unsigned i = 0, psize = d_pendingLem.size(); i < psize; i++) { - for (const Node& lc : d_pendingLem) + InferInfo& ii = d_pendingLem[i]; + Assert(!ii.isTrivial()); + Assert(!ii.isConflict()); + // get the explanation + Node eqExp; + if (options::stringRExplainLemmas()) + { + eqExp = mkExplain(ii.d_ant, ii.d_antn); + } + else + { + std::vector<Node> ev; + ev.insert(ev.end(), ii.d_ant.begin(), ii.d_ant.end()); + ev.insert(ev.end(), ii.d_antn.begin(), ii.d_antn.end()); + eqExp = utils::mkAnd(ev); + } + // make the lemma node + Node lem = ii.d_conc; + if (eqExp != d_true) { - Trace("strings-pending") << "Process pending lemma : " << lc << std::endl; - ++(d_statistics.d_lemmasInfer); - d_out.lemma(lc); + lem = nm->mkNode(IMPLIES, eqExp, lem); } - for (const std::pair<const Node, bool>& prp : d_pendingReqPhase) + Trace("strings-pending") << "Process pending lemma : " << lem << std::endl; + Trace("strings-assert") + << "(assert " << lem << ") ; lemma " << ii.d_id << std::endl; + Trace("strings-lemma") << "Strings::Lemma: " << lem << " by " << ii.d_id + << std::endl; + // only keep stats if we process it here + d_statistics.d_inferences << ii.d_id; + ++(d_statistics.d_lemmasInfer); + d_out.lemma(lem); + + // Process the side effects of the inference info. + // Register the new skolems from this inference. We register them here + // (lazily), since this is the moment when we have decided to process the + // inference. + for (const std::pair<const LengthStatus, std::vector<Node> >& sks : + ii.d_new_skolem) { - Trace("strings-pending") << "Require phase : " << prp.first - << ", polarity = " << prp.second << std::endl; - d_out.requirePhase(prp.first, prp.second); + for (const Node& n : sks.second) + { + d_termReg.registerTermAtomic(n, sks.first); + } } } + // process the pending require phase calls + for (const std::pair<const Node, bool>& prp : d_pendingReqPhase) + { + Trace("strings-pending") << "Require phase : " << prp.first + << ", polarity = " << prp.second << std::endl; + d_out.requirePhase(prp.first, prp.second); + } d_pendingLem.clear(); d_pendingReqPhase.clear(); } diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h index 6e11bf85e..cebd88a7f 100644 --- a/src/theory/strings/inference_manager.h +++ b/src/theory/strings/inference_manager.h @@ -35,29 +35,6 @@ namespace CVC4 { namespace theory { namespace strings { -/** - * A pending inference. This is a helper class to track an unprocessed call to - * InferenceManager::sendInference that is waiting to be asserted as a fact to - * the equality engine. - */ -struct PendingInfer -{ - PendingInfer(Inference i, Node fact, Node exp) - : d_infer(i), d_fact(fact), d_exp(exp) - { - } - ~PendingInfer() {} - /** The inference identifier */ - Inference d_infer; - /** The conclusion */ - Node d_fact; - /** - * Its explanation. This is a conjunction of literals that hold in the - * equality engine in the current context. - */ - Node d_exp; -}; - /** Inference Manager * * The purpose of this class is to process inference steps for strategies @@ -139,7 +116,7 @@ class InferenceManager * equality engine of the theory of strings. On the other hand, the set * exp_n ("explanations new") contain nodes that are not explainable by the * theory of strings. This method may call sendLemma or otherwise add a - * PendingInfer to d_pending, indicating a fact should be asserted to the + * InferInfo to d_pending, indicating a fact should be asserted to the * equality engine. Overall, the result of this method is one of the * following: * @@ -167,7 +144,7 @@ class InferenceManager * of each type. * * If the flag asLemma is true, then this method will send a lemma instead - * of an inference whenever applicable. + * of a fact whenever applicable. */ void sendInference(const std::vector<Node>& exp, const std::vector<Node>& exp_n, @@ -182,10 +159,17 @@ class InferenceManager /** Send inference * - * Makes the appropriate call to send inference based on the infer info - * data structure (see sendInference documentation above). + * This implements the above methods for the InferInfo object. It is called + * by the methods above. + * + * The inference info ii should have a rewritten conclusion and should not be + * trivial (InferInfo::isTrivial). It is the responsibility of the caller to + * ensure this. + * + * If the flag asLemma is true, then this method will send a lemma instead + * of a fact whenever applicable. */ - void sendInference(const InferInfo& i); + void sendInference(const InferInfo& ii, bool asLemma = false); /** Send split * * This requests that ( a = b V a != b ) is sent on the output channel as a @@ -205,7 +189,10 @@ class InferenceManager * * This method is called to indicate this class should send a phase * requirement request to the output channel for literal lit to be - * decided with polarity pol. + * decided with polarity pol. This requirement is processed at the same time + * lemmas are sent on the output channel of this class during this call to + * check. This means if the current lemmas of this class are abandoned (due + * to a conflict), the phase requirement is not processed. */ void sendPhaseRequirement(Node lit, bool pol); /** @@ -304,17 +291,6 @@ class InferenceManager * of atom, including calls to registerTerm. */ void assertPendingFact(Node atom, bool polarity, Node exp); - /** - * Indicates that ant => conc should be sent on the output channel of this - * class. This will either trigger an immediate call to the conflict - * method of the output channel of this class of conc is false, or adds the - * above lemma to the lemma cache d_pending_lem, which may be flushed - * later within the current call to TheoryStrings::check. - * - * The argument infer identifies the reason for inference, used for - * debugging. - */ - void sendLemma(Node ant, Node conc, Inference infer); /** Reference to the solver state of the theory of strings. */ SolverState& d_state; /** Reference to the term registry of theory of strings */ @@ -335,11 +311,11 @@ class InferenceManager * The list of pending literals to assert to the equality engine along with * their explanation. */ - std::vector<PendingInfer> d_pending; + std::vector<InferInfo> d_pending; /** A map from literals to their pending phase requirement */ std::map<Node, bool> d_pendingReqPhase; /** A list of pending lemmas to be sent on the output channel. */ - std::vector<Node> d_pendingLem; + std::vector<InferInfo> d_pendingLem; /** * The keep set of this class. This set is maintained to ensure that * facts and their explanations are ref-counted. Since facts and their |