summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/term_database.h
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2014-11-13 10:43:57 +0100
committerajreynol <andrew.j.reynolds@gmail.com>2014-11-13 10:44:11 +0100
commit0e761324a33a993ae9a268bc2d2ed46f7e86b42d (patch)
treed27052ba5aa4520436d8cb6ce059229f2df76ec2 /src/theory/quantifiers/term_database.h
parent270a5577f9a34c92ee991bff1d047d78a8f6d5ab (diff)
More preparation for filtering relevant terms in TermDb.
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
-rw-r--r--src/theory/quantifiers/term_database.h2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 3d419ed5c..4dca6b36c 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -128,6 +128,8 @@ private:
std::map< Node, std::map< TypeNode, Node > > d_par_op_map;
/** count number of ground terms per operator (user-context dependent) */
NodeIntMap d_op_ccount;
+ /** set has term */
+ void setHasTerm( Node n );
public:
TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe );
~TermDb(){}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback