diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-16 16:44:52 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-09-16 16:44:52 -0500 |
| commit | 9c4d548af9a14c18a6d69b41bba3e36054d37c0c (patch) | |
| tree | 07946cab9a720c75493264d0e114a493b50340d9 /src/theory/quantifiers/fmf/bounded_integers.h | |
| parent | 57301bf1db0febc6bf5b205c0ecbb2e249601bd0 (diff) | |
Move specific attributes out of term util (#3279)
Diffstat (limited to 'src/theory/quantifiers/fmf/bounded_integers.h')
| -rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.h | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index d668c6f02..1333af61c 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -20,14 +20,26 @@ #include "theory/quantifiers/quant_util.h" +#include "context/cdhashmap.h" #include "context/context.h" -#include "context/context_mm.h" +#include "expr/attribute.h" namespace CVC4 { namespace theory { class RepSetIterator; +/** + * Attribute set to 1 for literals that comprise the bounds of a quantified + * formula. For example, for: + * forall x. ( 0 <= x ^ x <= n ) => P( x ) + * the literals 0 <= x and x <= n are marked 1. + */ +struct BoundIntLitAttributeId +{ +}; +typedef expr::Attribute<BoundIntLitAttributeId, uint64_t> BoundIntLitAttribute; + namespace quantifiers { class BoundedIntegers : public QuantifiersModule |