diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-26 10:17:30 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-26 10:17:30 -0600 |
commit | 9b09505bb2a8ed50622b9442700e7f98d010b955 (patch) | |
tree | cdc9b8fe22178cf96346b068eef3377067f92f59 /src/theory/strings/eqc_info.h | |
parent | abd0048cdb6cf4d2ee0a096c9f7a63a1f7f1d9c8 (diff) |
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.
Diffstat (limited to 'src/theory/strings/eqc_info.h')
-rw-r--r-- | src/theory/strings/eqc_info.h | 81 |
1 files changed, 81 insertions, 0 deletions
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 <map> + +#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<Node> 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<Node> d_codeTerm; + context::CDO<unsigned> d_cardinalityLemK; + context::CDO<Node> 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<Node> d_prefixC; + /** same as above, for suffix. */ + context::CDO<Node> d_suffixC; +}; + +} // namespace strings +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__STRINGS__EQC_INFO_H */ |