diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-04 10:41:49 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-04 10:42:01 +0100 |
| commit | f9e109b0ac12ffbfd167a19dcd60f16241a0542c (patch) | |
| tree | 07547a834d60cbbbd75c91e1695c5518774c813e /src/theory/quantifiers/term_database.h | |
| parent | 5fae5ff49bfc9c96c03c52f5e2a5caa52ac40d03 (diff) | |
Better combination of UF with cbqi, refactor quantifiers intialization.
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
| -rw-r--r-- | src/theory/quantifiers/term_database.h | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 3e38897d1..bc8851195 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -147,13 +147,13 @@ public: /** constants */ Node d_zero; Node d_one; - + /** map from operators to ground terms for that operator */ std::map< Node, std::vector< Node > > d_op_map; /** map from type nodes to terms of that type */ std::map< TypeNode, std::vector< Node > > d_type_map; - - + + /** count number of non-redundant ground terms per operator */ std::map< Node, int > d_op_nonred_count; /**mapping from UF terms to representatives of their arguments */ @@ -165,7 +165,7 @@ public: std::map< Node, bool > d_has_map; /** map from reps to a term in eqc in d_has_map */ std::map< Node, Node > d_term_elig_eqc; - + public: /** ground terms for operator */ unsigned getNumGroundTerms( Node f ); @@ -204,7 +204,7 @@ public: Node getEligibleTermInEqc( TNode r ); /** is inst closure */ bool isInstClosure( Node r ); - + //for model basis private: //map from types to model basis terms @@ -301,7 +301,7 @@ public: bool isClosedEnumerableType( TypeNode tn ); // may complete bool mayComplete( TypeNode tn ); - + //for triggers private: /** helper function for compute var contains */ @@ -414,6 +414,8 @@ public: //general queries concerning quantified formulas wrt modules static Node getRewriteRule( Node q ); /** is fun def */ static bool isFunDef( Node q ); + /** is fun def */ + static bool isFunDefAnnotation( Node ipl ); /** is sygus conjecture */ static bool isSygusConjecture( Node q ); /** is sygus conjecture */ |