diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-24 19:00:59 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-24 19:00:59 +0100 |
commit | 73cecf65a750b9ee59486083af5ee55734da0a6a (patch) | |
tree | 43cae0e79c45f2c8204f3f5bc6e3c3f198e6845e /src/theory/quantifiers/term_database.h | |
parent | e1e393dff082ad115ba198c32990235fb991eb13 (diff) |
Add --lte-restrict-inst-closure option. Push dt.size fairness constraints inside splitting lemmas for sygus.
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
-rw-r--r-- | src/theory/quantifiers/term_database.h | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index f841bb2d8..8a20d6b41 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -33,7 +33,7 @@ typedef expr::Attribute< AxiomAttributeId, bool > AxiomAttribute; /** Attribute true for quantifiers that are conjecture */ struct ConjectureAttributeId {}; typedef expr::Attribute< ConjectureAttributeId, bool > ConjectureAttribute; - + /** Attribute true for function definition quantifiers */ struct FunDefAttributeId {}; typedef expr::Attribute< FunDefAttributeId, bool > FunDefAttribute; @@ -183,10 +183,11 @@ public: /** is entailed (incomplete check) */ bool isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol ); /** has term */ - bool hasTermCurrent( Node n ); + bool hasTermCurrent( Node n, bool useMode = true ); /** get has term eqc */ Node getHasTermEqc( Node r ); - + /** is inst closure */ + bool isInstClosure( Node r ); //for model basis private: //map from types to model basis terms @@ -252,8 +253,8 @@ public: public: //get bound variables in n static void getBoundVars( Node n, std::vector< Node >& bvs); - - + + //for skolem private: /** map from universal quantifiers to their skolemized body */ @@ -268,9 +269,9 @@ public: Node getSkolemizedBody( Node f); /** is induction variable */ static bool isInductionTerm( Node n ); - + //for ground term enumeration -private: +private: /** ground terms enumerated for types */ std::map< TypeNode, std::vector< Node > > d_enum_terms; //type enumerators @@ -278,8 +279,8 @@ private: std::vector< TypeEnumerator > d_typ_enum; public: //get nth term for type - Node getEnumerateTerm( TypeNode tn, unsigned index ); - + Node getEnumerateTerm( TypeNode tn, unsigned index ); + //miscellaneous public: /** map from universal quantifiers to the list of variables */ @@ -353,7 +354,7 @@ public: int getQAttrQuantInstLevel( Node q ); /** get rewrite rule priority */ int getQAttrRewriteRulePriority( Node q ); - + };/* class TermDb */ }/* CVC4::theory::quantifiers namespace */ |