summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/conjecture_generator.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.h')
-rwxr-xr-xsrc/theory/quantifiers/conjecture_generator.h2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 462fadfce..2d8e8e403 100755
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -138,6 +138,8 @@ public:
std::map< TypeNode, unsigned > d_var_limit;
//the functions we can currently generate
std::map< TypeNode, std::vector< TNode > > d_typ_tg_funcs;
+ // whether functions must add operators
+ std::map< TNode, bool > d_tg_func_param;
//the equivalence classes (if applicable) that match the currently generated term
bool d_gen_relevant_terms;
//relevant equivalence classes
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback