diff options
Diffstat (limited to 'src/theory/strings/infer_info.h')
| -rw-r--r-- | src/theory/strings/infer_info.h | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h index 7d41dca98..31a74784e 100644 --- a/src/theory/strings/infer_info.h +++ b/src/theory/strings/infer_info.h @@ -38,6 +38,7 @@ namespace strings { */ enum class Inference : uint32_t { + BEGIN, //-------------------------------------- base solver // initial normalize singular // x1 = "" ^ ... ^ x_{i-1} = "" ^ x_{i+1} = "" ^ ... ^ xn = "" => @@ -295,6 +296,10 @@ enum class Inference : uint32_t // (see theory_strings_preprocess). REDUCTION, //-------------------------------------- end extended function solver + //-------------------------------------- prefix conflict + // prefix conflict (coarse-grained) + PREFIX_CONFLICT, + //-------------------------------------- end prefix conflict NONE, }; @@ -359,9 +364,11 @@ class InferInfo /** * The "new literal" antecedant(s) of the inference, interpreted * conjunctively. These are literals that were needed to show the conclusion - * but do not currently hold in the equality engine. + * but do not currently hold in the equality engine. These should be a subset + * of d_ant. In other words, antecedants that are not explained are stored + * in *both* d_ant and d_noExplain. */ - std::vector<Node> d_antn; + std::vector<Node> d_noExplain; /** * A list of new skolems introduced as a result of this inference. They * are mapped to by a length status, indicating the length constraint that @@ -372,15 +379,17 @@ class InferInfo bool isTrivial() const; /** * Does this infer info correspond to a conflict? True if d_conc is false - * and it has no new antecedants (d_antn). + * and it has no new antecedants (d_noExplain). */ bool isConflict() const; /** * 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). + * engine with no new external antecedants (d_noExplain). */ bool isFact() const; + /** Get antecedant */ + Node getAntecedant() const; }; /** |