diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-10-16 18:44:17 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-16 16:44:17 -0700 |
commit | 207245fef36ccad1281fefe9d3f3403cd4f6d15b (patch) | |
tree | aa364b8701f01cb9e30afb8b85c615fae0ee6f40 /src/theory/strings/solver_state.cpp | |
parent | 80b14c0965678fb91467de287b00a9a1d8a39be5 (diff) |
Solver state for theory of strings (#3181)
This refactors the theory of strings to use a solver state object, which manages state information regarding assertions.
It also deletes some unused/undefined functions in theory_strings.h.
There are no major changes to the behavior of the code or its documentation in this PR.
This is work towards #1881.
Diffstat (limited to 'src/theory/strings/solver_state.cpp')
-rw-r--r-- | src/theory/strings/solver_state.cpp | 283 |
1 files changed, 283 insertions, 0 deletions
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp new file mode 100644 index 000000000..c370558b5 --- /dev/null +++ b/src/theory/strings/solver_state.cpp @@ -0,0 +1,283 @@ +/********************* */ +/*! \file solver_state.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of the solver state of the theory of strings. + **/ + +#include "theory/strings/solver_state.h" + +#include "theory/strings/theory_strings_utils.h" + +using namespace std; +using namespace CVC4::context; +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace strings { + +EqcInfo::EqcInfo(context::Context* c) + : d_lengthTerm(c), + d_codeTerm(c), + d_cardinalityLemK(c), + d_normalizedLength(c), + d_prefixC(c), + d_suffixC(c) +{ +} + +Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf) +{ + // check conflict + Node prev = isSuf ? d_suffixC : d_prefixC; + if (!prev.isNull()) + { + Trace("strings-eager-pconf-debug") << "Check conflict " << prev << ", " << t + << " post=" << isSuf << std::endl; + Node prevC = utils::getConstantEndpoint(prev, isSuf); + Assert(!prevC.isNull()); + Assert(prevC.getKind() == CONST_STRING); + if (c.isNull()) + { + c = utils::getConstantEndpoint(t, isSuf); + Assert(!c.isNull()); + } + Assert(c.getKind() == CONST_STRING); + bool conflict = false; + // if the constant prefixes are different + if (c != prevC) + { + // conflicts between constants should be handled by equality engine + Assert(!t.isConst() || !prev.isConst()); + Trace("strings-eager-pconf-debug") + << "Check conflict constants " << prevC << ", " << c << std::endl; + const String& ps = prevC.getConst<String>(); + const String& cs = c.getConst<String>(); + unsigned pvs = ps.size(); + unsigned cvs = cs.size(); + if (pvs == cvs || (pvs > cvs && t.isConst()) + || (cvs > pvs && prev.isConst())) + { + // If equal length, cannot be equal due to node check above. + // If one is fully constant and has less length than the other, then the + // other will not fit and we are in conflict. + conflict = true; + } + else + { + const String& larges = pvs > cvs ? ps : cs; + const String& smalls = pvs > cvs ? cs : ps; + if (isSuf) + { + conflict = !larges.hasSuffix(smalls); + } + else + { + conflict = !larges.hasPrefix(smalls); + } + } + if (!conflict && (pvs > cvs || prev.isConst())) + { + // current is subsumed, either shorter prefix or the other is a full + // constant + return Node::null(); + } + } + else if (!t.isConst()) + { + // current is subsumed since the other may be a full constant + return Node::null(); + } + if (conflict) + { + Trace("strings-eager-pconf") + << "Conflict for " << prevC << ", " << c << std::endl; + std::vector<Node> ccs; + Node r[2]; + for (unsigned i = 0; i < 2; i++) + { + Node tp = i == 0 ? t : prev; + if (tp.getKind() == STRING_IN_REGEXP) + { + ccs.push_back(tp); + r[i] = tp[0]; + } + else + { + r[i] = tp; + } + } + if (r[0] != r[1]) + { + ccs.push_back(r[0].eqNode(r[1])); + } + Assert(!ccs.empty()); + Node ret = + ccs.size() == 1 ? ccs[0] : NodeManager::currentNM()->mkNode(AND, ccs); + Trace("strings-eager-pconf") + << "String: eager prefix conflict: " << ret << std::endl; + return ret; + } + } + if (isSuf) + { + d_suffixC = t; + } + else + { + d_prefixC = t; + } + return Node::null(); +} + +SolverState::SolverState(context::Context* c, eq::EqualityEngine& ee) + : d_context(c), d_ee(ee), d_conflict(c, false), d_pendingConflict(c) +{ +} +SolverState::~SolverState() +{ + for (std::pair<const Node, EqcInfo*>& it : d_eqcInfo) + { + delete it.second; + } +} + +Node SolverState::getRepresentative(Node t) const +{ + if (d_ee.hasTerm(t)) + { + return d_ee.getRepresentative(t); + } + return t; +} + +bool SolverState::hasTerm(Node a) const { return d_ee.hasTerm(a); } + +bool SolverState::areEqual(Node a, Node b) const +{ + if (a == b) + { + return true; + } + else if (hasTerm(a) && hasTerm(b)) + { + return d_ee.areEqual(a, b); + } + return false; +} + +bool SolverState::areDisequal(Node a, Node b) const +{ + if (a == b) + { + return false; + } + else if (hasTerm(a) && hasTerm(b)) + { + Node ar = d_ee.getRepresentative(a); + Node br = d_ee.getRepresentative(b); + return (ar != br && ar.isConst() && br.isConst()) + || d_ee.areDisequal(ar, br, false); + } + Node ar = getRepresentative(a); + Node br = getRepresentative(b); + return ar != br && ar.isConst() && br.isConst(); +} + +eq::EqualityEngine* SolverState::getEqualityEngine() const { return &d_ee; } + +EqcInfo* SolverState::getOrMakeEqcInfo(Node eqc, bool doMake) +{ + std::map<Node, EqcInfo*>::iterator eqc_i = d_eqcInfo.find(eqc); + if (eqc_i != d_eqcInfo.end()) + { + return eqc_i->second; + } + if (doMake) + { + EqcInfo* ei = new EqcInfo(d_context); + d_eqcInfo[eqc] = ei; + return ei; + } + return nullptr; +} + +void SolverState::addEndpointsToEqcInfo(Node t, Node concat, Node eqc) +{ + Assert(concat.getKind() == STRING_CONCAT + || concat.getKind() == REGEXP_CONCAT); + EqcInfo* ei = nullptr; + // check each side + for (unsigned r = 0; r < 2; r++) + { + unsigned index = r == 0 ? 0 : concat.getNumChildren() - 1; + Node c = utils::getConstantComponent(concat[index]); + if (!c.isNull()) + { + if (ei == nullptr) + { + ei = getOrMakeEqcInfo(eqc); + } + Trace("strings-eager-pconf-debug") + << "New term: " << concat << " for " << t << " with prefix " << c + << " (" << (r == 1) << ")" << std::endl; + setPendingConflictWhen(ei->addEndpointConst(t, c, r == 1)); + } + } +} + +Node SolverState::getLengthExp(Node t, std::vector<Node>& exp, Node te) +{ + Assert(areEqual(t, te)); + Node lt = utils::mkNLength(te); + if (hasTerm(lt)) + { + // use own length if it exists, leads to shorter explanation + return lt; + } + EqcInfo* ei = getOrMakeEqcInfo(t, false); + Node lengthTerm = ei ? ei->d_lengthTerm : Node::null(); + if (lengthTerm.isNull()) + { + // typically shouldnt be necessary + lengthTerm = t; + } + Debug("strings") << "SolverState::getLengthTerm " << t << " is " << lengthTerm + << std::endl; + if (te != lengthTerm) + { + exp.push_back(te.eqNode(lengthTerm)); + } + return Rewriter::rewrite( + NodeManager::currentNM()->mkNode(STRING_LENGTH, lengthTerm)); +} + +Node SolverState::getLength(Node t, std::vector<Node>& exp) +{ + return getLengthExp(t, exp, t); +} + +void SolverState::setConflict() { d_conflict = true; } +bool SolverState::isInConflict() const { return d_conflict; } + +void SolverState::setPendingConflictWhen(Node conf) +{ + if (!conf.isNull() && d_pendingConflict.get().isNull()) + { + d_pendingConflict = conf; + } +} + +Node SolverState::getPendingConflict() const { return d_pendingConflict; } + +} // namespace strings +} // namespace theory +} // namespace CVC4 |