From 04154c08c1af81bb751376ae9379c071a95c5a3f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 1 Jul 2020 08:46:07 -0500 Subject: Inferences and model construction taking into account seq.unit (#4607) Towards theory of sequences. This makes the strings solver handle seq.unit, which requires two new inferences and updates to its model construction. It also fixes a bug in the best content heuristic, which previously failed to update the best score. --- src/theory/strings/infer_info.h | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'src/theory/strings/infer_info.h') diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h index 1e37dc5b0..2a42b9fab 100644 --- a/src/theory/strings/infer_info.h +++ b/src/theory/strings/infer_info.h @@ -59,6 +59,10 @@ enum class Inference : uint32_t // equal after e.g. removing strings that are currently empty. For example: // y = "" ^ z = "" => x ++ y = z ++ x I_NORM, + // injectivity of seq.unit + UNIT_INJ, + // unit constant conflict + UNIT_CONST_CONFLICT, // A split due to cardinality CARD_SP, // The cardinality inference for strings, see Liang et al CAV 2014. -- cgit v1.2.3