diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-26 19:26:21 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-26 19:26:21 +0200 |
| commit | f07e8a3f06feb789692ede8ad9d25a2e049af769 (patch) | |
| tree | bdeb79262056c70c6b5125ed11a392a4fa1864f7 /src/theory/rep_set.h | |
| parent | 349deb0522c4602b740d96f6a688b644dd84c64f (diff) | |
Bug fixes and improvements for mbqi with theory symbols, TheoryModel fullModel=false assigns values to eqc. Bug fix for fmf-fun. Minor change to resource limiting for quantifiers. Add fmf regressions.
Diffstat (limited to 'src/theory/rep_set.h')
| -rw-r--r-- | src/theory/rep_set.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index 19bb6d3d3..4aab230e6 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -33,6 +33,8 @@ public: std::map< TypeNode, std::vector< Node > > d_type_reps; std::map< TypeNode, bool > d_type_complete; std::map< Node, int > d_tmap; + // map from values to terms they were assigned for + std::map< Node, Node > d_values_to_terms; /** clear the set */ void clear(); /** has type */ |