diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-10 16:38:37 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-10 16:45:56 -0400 |
| commit | 65128efc1d0a4c2007ebb7b47712888481c07843 (patch) | |
| tree | e4cd01c8712c1a05fcd4bb660c921e83d7e82830 /src/smt/boolean_terms.h | |
| parent | 06f26f17c9a2fb0fbf56143cd4c06a19586ca0c8 (diff) | |
Boolean terms conversion fix for datatypes, fixes a problem Andy discovered on his branch.
Diffstat (limited to 'src/smt/boolean_terms.h')
| -rw-r--r-- | src/smt/boolean_terms.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h index b289e3469..bdd9ff839 100644 --- a/src/smt/boolean_terms.h +++ b/src/smt/boolean_terms.h @@ -69,6 +69,8 @@ class BooleanTermConverter { BooleanTermTypeCache d_typeCache; /** The cache used during Boolean term datatype conversion */ BooleanTermDatatypeCache d_datatypeCache; + /** A (reverse) cache for Boolean term datatype conversion */ + BooleanTermDatatypeCache d_datatypeReverseCache; Node rewriteAs(TNode in, TypeNode as) throw(); |