diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-25 12:18:05 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-25 12:18:14 -0500 |
| commit | d8de492163b90974709a16918cb615515a536afc (patch) | |
| tree | 8241c94be9a610149b40af0fc0932ee05094b2aa /src/theory/quantifiers/term_database.h | |
| parent | a9bf7fc500daba46ed86ca744c1346059880e6f4 (diff) | |
Refactoring of model engine to separate individual implementations of model builder. Begin work on interval models for integers. Other minor cleanup.
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
| -rw-r--r-- | src/theory/quantifiers/term_database.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index fb5964554..1688479f3 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -68,6 +68,10 @@ typedef expr::Attribute<HasBoundVarComputedAttributeId, bool> HasBoundVarCompute struct QRewriteRuleAttributeId {}; typedef expr::Attribute<QRewriteRuleAttributeId, Node> QRewriteRuleAttribute; +//for bounded integers +struct BoundIntLitAttributeId {}; +typedef expr::Attribute<BoundIntLitAttributeId, uint64_t> BoundIntLitAttribute; + class QuantifiersEngine; |