From: Andrew Reynolds Date: Wed, 26 Feb 2020 16:17:30 +0000 (-0600) Subject: Move equivalence class info to its own file in strings (#3799) X-Git-Tag: cvc5-1.0.0~3600 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9b09505bb2a8ed50622b9442700e7f98d010b955;p=cvc5.git Move equivalence class info to its own file in strings (#3799) Code move only, no updates to behavior or content of code in this PR. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index e8c38f39d..30cdf15b7 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -672,6 +672,8 @@ libcvc4_add_sources( theory/strings/core_solver.h theory/strings/extf_solver.cpp theory/strings/extf_solver.h + theory/strings/eqc_info.cpp + theory/strings/eqc_info.h theory/strings/infer_info.cpp theory/strings/infer_info.h theory/strings/inference_manager.cpp diff --git a/src/theory/strings/eqc_info.cpp b/src/theory/strings/eqc_info.cpp new file mode 100644 index 000000000..ab6d473bd --- /dev/null +++ b/src/theory/strings/eqc_info.cpp @@ -0,0 +1,143 @@ +/********************* */ +/*! \file eqc_info.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 equivalence class info for the theory of strings + **/ + +#include "theory/strings/eqc_info.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(); + const String& cs = c.getConst(); + 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 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(); +} + +} // namespace strings +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/strings/eqc_info.h b/src/theory/strings/eqc_info.h new file mode 100644 index 000000000..241b7d523 --- /dev/null +++ b/src/theory/strings/eqc_info.h @@ -0,0 +1,81 @@ +/********************* */ +/*! \file eqc_info.h + ** \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 Equivalence class info for the theory of strings + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__STRINGS__EQC_INFO_H +#define CVC4__THEORY__STRINGS__EQC_INFO_H + +#include + +#include "context/cdo.h" +#include "context/context.h" +#include "expr/node.h" + +namespace CVC4 { +namespace theory { +namespace strings { + +/** + * SAT-context-dependent information about an equivalence class. This + * information is updated eagerly as assertions are processed by the theory of + * strings at standard effort. + */ +class EqcInfo +{ + public: + EqcInfo(context::Context* c); + ~EqcInfo() {} + /** add prefix constant + * + * This informs this equivalence class info that a term t in its + * equivalence class has a constant prefix (if isSuf=true) or suffix + * (if isSuf=false). The constant c (if non-null) is the value of that + * constant, if it has been computed already. + * + * If this method returns a non-null node ret, then ret is a conjunction + * corresponding to a conflict that holds in the current context. + */ + Node addEndpointConst(Node t, Node c, bool isSuf); + /** + * If non-null, this is a term x from this eq class such that str.len( x ) + * occurs as a term in this SAT context. + */ + context::CDO d_lengthTerm; + /** + * If non-null, this is a term x from this eq class such that str.code( x ) + * occurs as a term in this SAT context. + */ + context::CDO d_codeTerm; + context::CDO d_cardinalityLemK; + context::CDO d_normalizedLength; + /** + * A node that explains the longest constant prefix known of this + * equivalence class. This can either be: + * (1) A term from this equivalence class, including a constant "ABC" or + * concatenation term (str.++ "ABC" ...), or + * (2) A membership of the form (str.in.re x R) where x is in this + * equivalence class and R is a regular expression of the form + * (str.to.re "ABC") or (re.++ (str.to.re "ABC") ...). + */ + context::CDO d_prefixC; + /** same as above, for suffix. */ + context::CDO d_suffixC; +}; + +} // namespace strings +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__STRINGS__EQC_INFO_H */ diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp index 5eb0818b7..422c9e58b 100644 --- a/src/theory/strings/solver_state.cpp +++ b/src/theory/strings/solver_state.cpp @@ -24,120 +24,6 @@ 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(); - const String& cs = c.getConst(); - 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 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, Valuation& v) diff --git a/src/theory/strings/solver_state.h b/src/theory/strings/solver_state.h index b295ba12d..e3fe432d3 100644 --- a/src/theory/strings/solver_state.h +++ b/src/theory/strings/solver_state.h @@ -19,65 +19,17 @@ #include -#include "context/cdo.h" #include "context/context.h" #include "expr/node.h" -#include "options/theory_options.h" #include "theory/theory_model.h" #include "theory/uf/equality_engine.h" #include "theory/valuation.h" +#include "theory/strings/eqc_info.h" namespace CVC4 { namespace theory { namespace strings { -/** - * SAT-context-dependent information about an equivalence class. This - * information is updated eagerly as assertions are processed by the theory of - * strings at standard effort. - */ -class EqcInfo -{ - public: - EqcInfo(context::Context* c); - ~EqcInfo() {} - /** add prefix constant - * - * This informs this equivalence class info that a term t in its - * equivalence class has a constant prefix (if isSuf=true) or suffix - * (if isSuf=false). The constant c (if non-null) is the value of that - * constant, if it has been computed already. - * - * If this method returns a non-null node ret, then ret is a conjunction - * corresponding to a conflict that holds in the current context. - */ - Node addEndpointConst(Node t, Node c, bool isSuf); - /** - * If non-null, this is a term x from this eq class such that str.len( x ) - * occurs as a term in this SAT context. - */ - context::CDO d_lengthTerm; - /** - * If non-null, this is a term x from this eq class such that str.code( x ) - * occurs as a term in this SAT context. - */ - context::CDO d_codeTerm; - context::CDO d_cardinalityLemK; - context::CDO d_normalizedLength; - /** - * A node that explains the longest constant prefix known of this - * equivalence class. This can either be: - * (1) A term from this equivalence class, including a constant "ABC" or - * concatenation term (str.++ "ABC" ...), or - * (2) A membership of the form (str.in.re x R) where x is in this - * equivalence class and R is a regular expression of the form - * (str.to.re "ABC") or (re.++ (str.to.re "ABC") ...). - */ - context::CDO d_prefixC; - /** same as above, for suffix. */ - context::CDO d_suffixC; -}; - /** * Solver state for strings. * @@ -224,4 +176,4 @@ class SolverState } // namespace theory } // namespace CVC4 -#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_H */ +#endif /* CVC4__THEORY__STRINGS__SOLVER_STATE_H */