diff options
Diffstat (limited to 'src/theory/strings/solver_state.h')
-rw-r--r-- | src/theory/strings/solver_state.h | 52 |
1 files changed, 2 insertions, 50 deletions
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,66 +19,18 @@ #include <map> -#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<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; -}; - -/** * Solver state for strings. * * The purpose of this class is track and provide query functions for the state @@ -224,4 +176,4 @@ class SolverState } // namespace theory } // namespace CVC4 -#endif /* CVC4__THEORY__STRINGS__THEORY_STRINGS_H */ +#endif /* CVC4__THEORY__STRINGS__SOLVER_STATE_H */ |