From f9e109b0ac12ffbfd167a19dcd60f16241a0542c Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 4 Nov 2015 10:41:49 +0100 Subject: Better combination of UF with cbqi, refactor quantifiers intialization. --- src/theory/quantifiers/term_database.h | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) (limited to 'src/theory/quantifiers/term_database.h') 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 */ -- cgit v1.2.3