diff options
author | Clark Barrett <clarkbarrett@google.com> | 2015-04-23 09:43:52 -0700 |
---|---|---|
committer | Clark Barrett <clarkbarrett@google.com> | 2015-04-23 09:43:52 -0700 |
commit | dea679ce032c130d210d54c2e5482f95db1ff04a (patch) | |
tree | 6c36f68150172b20717f7d504274ab0bf82791b0 /src/theory/quantifiers/conjecture_generator.h | |
parent | d95fe7675e20eaee86b8e804469e6db83265a005 (diff) |
A few more minor updates to match google repository with CVC4 repository
(mostly whitespace differences).
Diffstat (limited to 'src/theory/quantifiers/conjecture_generator.h')
-rw-r--r-- | src/theory/quantifiers/conjecture_generator.h | 874 |
1 files changed, 437 insertions, 437 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 48694c99a..6f99777f4 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -1,437 +1,437 @@ -/********************* */
-/*! \file conjecture_generator.h
- ** \verbatim
- ** Original author: Andrew Reynolds
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief conjecture generator class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef CONJECTURE_GENERATOR_H
-#define CONJECTURE_GENERATOR_H
-
-#include "context/cdhashmap.h"
-#include "context/cdchunk_list.h"
-#include "theory/quantifiers_engine.h"
-#include "theory/type_enumerator.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class TermArgTrie;
-
-//algorithm for computing candidate subgoals
-
-class ConjectureGenerator;
-
-// operator independent index of arguments for an EQC
-class OpArgIndex
-{
-public:
- std::map< TNode, OpArgIndex > d_child;
- std::vector< TNode > d_ops;
- std::vector< TNode > d_op_terms;
- void addTerm( ConjectureGenerator * s, TNode n, unsigned index = 0 );
- Node getGroundTerm( ConjectureGenerator * s, std::vector< TNode >& args );
- void getGroundTerms( ConjectureGenerator * s, std::vector< TNode >& terms );
-};
-
-class PatternTypIndex
-{
-public:
- std::vector< TNode > d_terms;
- std::map< TypeNode, std::map< unsigned, PatternTypIndex > > d_children;
- void clear() {
- d_terms.clear();
- d_children.clear();
- }
-};
-
-class SubstitutionIndex
-{
-public:
- //current variable, or ground EQC if d_children.empty()
- TNode d_var;
- std::map< TNode, SubstitutionIndex > d_children;
- //add substitution
- void addSubstitution( TNode eqc, std::vector< TNode >& vars, std::vector< TNode >& terms, unsigned i = 0 );
- //notify substitutions
- bool notifySubstitutions( ConjectureGenerator * s, std::map< TNode, TNode >& subs, TNode rhs, unsigned numVars, unsigned i = 0 );
-};
-
-class TermGenEnv;
-
-class TermGenerator
-{
-private:
- unsigned calculateGeneralizationDepth( TermGenEnv * s, std::map< TypeNode, std::vector< int > >& fvs );
-public:
- TermGenerator(){}
- TypeNode d_typ;
- unsigned d_id;
- //1 : consider as unique variable
- //2 : consider equal to another variable
- //5 : consider a function application
- unsigned d_status;
- int d_status_num;
- //for function applications: the number of children you have built
- int d_status_child_num;
- //children (pointers to TermGenerators)
- std::vector< unsigned > d_children;
-
- //match status
- int d_match_status;
- int d_match_status_child_num;
- //match mode bits
- //0 : different variables must have different matches
- //1 : variables must map to ground terms
- //2 : variables must map to non-ground terms
- unsigned d_match_mode;
- //children
- std::vector< std::map< TNode, TermArgTrie >::iterator > d_match_children;
- std::vector< std::map< TNode, TermArgTrie >::iterator > d_match_children_end;
-
- void reset( TermGenEnv * s, TypeNode tn );
- bool getNextTerm( TermGenEnv * s, unsigned depth );
- void resetMatching( TermGenEnv * s, TNode eqc, unsigned mode );
- bool getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs );
-
- unsigned getDepth( TermGenEnv * s );
- unsigned getGeneralizationDepth( TermGenEnv * s );
- Node getTerm( TermGenEnv * s );
-
- void debugPrint( TermGenEnv * s, const char * c, const char * cd );
-};
-
-
-class TermGenEnv
-{
-public:
- //collect signature information
- void collectSignatureInformation();
- //reset function
- void reset( unsigned gdepth, bool genRelevant, TypeNode tgen );
- //get next term
- bool getNextTerm();
- //reset matching
- void resetMatching( TNode eqc, unsigned mode );
- //get next match
- bool getNextMatch( TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs );
- //get term
- Node getTerm();
- //debug print
- void debugPrint( const char * c, const char * cd );
-
- //conjecture generation
- ConjectureGenerator * d_cg;
- //the current number of enumerated variables per type
- std::map< TypeNode, unsigned > d_var_id;
- //the limit of number of variables per type to enumerate
- 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
- std::vector< TNode > d_relevant_eqc[2];
- //candidate equivalence classes
- std::vector< std::vector< TNode > > d_ccand_eqc[2];
- //the term generation objects
- unsigned d_tg_id;
- std::map< unsigned, TermGenerator > d_tg_alloc;
- unsigned d_tg_gdepth;
- int d_tg_gdepth_limit;
-
- //all functions
- std::vector< TNode > d_funcs;
- //function to kind map
- std::map< TNode, Kind > d_func_kind;
- //type of each argument of the function
- std::map< TNode, std::vector< TypeNode > > d_func_args;
-
- //access functions
- unsigned getNumTgVars( TypeNode tn );
- bool allowVar( TypeNode tn );
- void addVar( TypeNode tn );
- void removeVar( TypeNode tn );
- unsigned getNumTgFuncs( TypeNode tn );
- TNode getTgFunc( TypeNode tn, unsigned i );
- Node getFreeVar( TypeNode tn, unsigned i );
- bool considerCurrentTerm();
- bool considerCurrentTermCanon( unsigned tg_id );
- void changeContext( bool add );
- bool isRelevantFunc( Node f );
- //carry
- TermDb * getTermDatabase();
- Node getGroundEqc( TNode r );
- bool isGroundEqc( TNode r );
- bool isGroundTerm( TNode n );
-};
-
-
-
-class TheoremIndex
-{
-private:
- void addTheorem( std::vector< TNode >& lhs_v, std::vector< unsigned >& lhs_arg, TNode rhs );
- void addTheoremNode( TNode curr, std::vector< TNode >& lhs_v, std::vector< unsigned >& lhs_arg, TNode rhs );
- void getEquivalentTerms( std::vector< TNode >& n_v, std::vector< unsigned >& n_arg,
- std::map< TNode, TNode >& smap, std::vector< TNode >& vars, std::vector< TNode >& subs,
- std::vector< Node >& terms );
- void getEquivalentTermsNode( Node curr, std::vector< TNode >& n_v, std::vector< unsigned >& n_arg,
- std::map< TNode, TNode >& smap, std::vector< TNode >& vars, std::vector< TNode >& subs,
- std::vector< Node >& terms );
-public:
- std::map< TypeNode, TNode > d_var;
- std::map< TNode, TheoremIndex > d_children;
- std::vector< Node > d_terms;
-
- void addTheorem( TNode lhs, TNode rhs ) {
- std::vector< TNode > v;
- std::vector< unsigned > a;
- addTheoremNode( lhs, v, a, rhs );
- }
- void getEquivalentTerms( TNode n, std::vector< Node >& terms ) {
- std::vector< TNode > nv;
- std::vector< unsigned > na;
- std::map< TNode, TNode > smap;
- std::vector< TNode > vars;
- std::vector< TNode > subs;
- getEquivalentTermsNode( n, nv, na, smap, vars, subs, terms );
- }
- void clear(){
- d_var.clear();
- d_children.clear();
- d_terms.clear();
- }
- void debugPrint( const char * c, unsigned ind = 0 );
-};
-
-
-
-class ConjectureGenerator : public QuantifiersModule
-{
- friend class OpArgIndex;
- friend class PatGen;
- friend class PatternGenEqc;
- friend class PatternGen;
- friend class SubsEqcIndex;
- friend class TermGenerator;
- friend class TermGenEnv;
- typedef context::CDChunkList<Node> NodeList;
- typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
- typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
-//this class maintains a congruence closure for *universal* facts
-private:
- //notification class for equality engine
- class NotifyClass : public eq::EqualityEngineNotify {
- ConjectureGenerator& d_sg;
- public:
- NotifyClass(ConjectureGenerator& sg): d_sg(sg) {}
- bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; }
- bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; }
- bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { return true; }
- void eqNotifyConstantTermMerge(TNode t1, TNode t2) { }
- void eqNotifyNewClass(TNode t) { d_sg.eqNotifyNewClass(t); }
- void eqNotifyPreMerge(TNode t1, TNode t2) { d_sg.eqNotifyPreMerge(t1, t2); }
- void eqNotifyPostMerge(TNode t1, TNode t2) { d_sg.eqNotifyPostMerge(t1, t2); }
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {d_sg.eqNotifyDisequal(t1, t2, reason); }
- };/* class ConjectureGenerator::NotifyClass */
- /** The notify class */
- NotifyClass d_notify;
- class EqcInfo{
- public:
- EqcInfo( context::Context* c );
- //representative
- context::CDO< Node > d_rep;
- };
- /** get or make eqc info */
- EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false );
- /** (universal) equaltity engine */
- eq::EqualityEngine d_uequalityEngine;
- /** pending adds */
- std::vector< Node > d_upendingAdds;
- /** relevant terms */
- std::map< Node, bool > d_urelevant_terms;
- /** information necessary for equivalence classes */
- std::map< Node, EqcInfo* > d_eqc_info;
- /** called when a new equivalance class is created */
- void eqNotifyNewClass(TNode t);
- /** called when two equivalance classes will merge */
- void eqNotifyPreMerge(TNode t1, TNode t2);
- /** called when two equivalance classes have merged */
- void eqNotifyPostMerge(TNode t1, TNode t2);
- /** called when two equivalence classes are made disequal */
- void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
- /** are universal equal */
- bool areUniversalEqual( TNode n1, TNode n2 );
- /** are universal disequal */
- bool areUniversalDisequal( TNode n1, TNode n2 );
- /** get universal representative */
- TNode getUniversalRepresentative( TNode n, bool add = false );
- /** set relevant */
- void setUniversalRelevant( TNode n );
- /** ordering for universal terms */
- bool isUniversalLessThan( TNode rt1, TNode rt2 );
-
- /** the nodes we have reported as canonical representative */
- std::vector< TNode > d_ue_canon;
- /** is reported canon */
- bool isReportedCanon( TNode n );
- /** mark that term has been reported as canonical rep */
- void markReportedCanon( TNode n );
-
-private: //information regarding the conjectures
- /** list of all conjectures */
- std::vector< Node > d_conjectures;
- /** list of all waiting conjectures */
- std::vector< Node > d_waiting_conjectures_lhs;
- std::vector< Node > d_waiting_conjectures_rhs;
- std::vector< int > d_waiting_conjectures_score;
- /** map of currently considered equality conjectures */
- std::map< Node, std::vector< Node > > d_waiting_conjectures;
- /** map of equality conjectures */
- std::map< Node, std::vector< Node > > d_eq_conjectures;
- /** currently existing conjectures in equality engine */
- BoolMap d_ee_conjectures;
- /** conjecture index */
- TheoremIndex d_thm_index;
-private: //free variable list
- //free variables
- std::map< TypeNode, std::vector< Node > > d_free_var;
- //map from free variable to FV#
- std::map< TNode, unsigned > d_free_var_num;
- // get canonical free variable #i of type tn
- Node getFreeVar( TypeNode tn, unsigned i );
- // get canonical term, return null if it contains a term apart from handled signature
- Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs );
-private: //information regarding the terms
- //relevant patterns (the LHS's)
- std::map< TypeNode, std::vector< Node > > d_rel_patterns;
- //total number of unique variables
- std::map< TNode, unsigned > d_rel_pattern_var_sum;
- //by types
- PatternTypIndex d_rel_pattern_typ_index;
- // substitution to ground EQC index
- std::map< TNode, SubstitutionIndex > d_rel_pattern_subs_index;
- //patterns (the RHS's)
- std::map< TypeNode, std::vector< Node > > d_patterns;
- //patterns to # variables per type
- std::map< TNode, std::map< TypeNode, unsigned > > d_pattern_var_id;
- // # duplicated variables
- std::map< TNode, unsigned > d_pattern_var_duplicate;
- // is normal pattern? (variables allocated in canonical way left to right)
- std::map< TNode, int > d_pattern_is_normal;
- std::map< TNode, int > d_pattern_is_relevant;
- // patterns to a count of # operators (variables and functions)
- std::map< TNode, std::map< TNode, unsigned > > d_pattern_fun_id;
- // term size
- std::map< TNode, unsigned > d_pattern_fun_sum;
- // collect functions
- unsigned collectFunctions( TNode opat, TNode pat, std::map< TNode, unsigned >& funcs,
- std::map< TypeNode, unsigned >& mnvn, std::map< TypeNode, unsigned >& mxvn );
- // add pattern
- void registerPattern( Node pat, TypeNode tpat );
-private: //for debugging
- std::map< TNode, unsigned > d_em;
- unsigned d_conj_count;
-public:
- //term generation environment
- TermGenEnv d_tge;
- //consider term canon
- bool considerTermCanon( Node ln, bool genRelevant );
-public: //for generalization
- //generalizations
- bool isGeneralization( TNode patg, TNode pat ) {
- std::map< TNode, TNode > subs;
- return isGeneralization( patg, pat, subs );
- }
- bool isGeneralization( TNode patg, TNode pat, std::map< TNode, TNode >& subs );
- // get generalization depth
- int calculateGeneralizationDepth( TNode n, std::vector< TNode >& fv );
-private:
- //predicate for type
- std::map< TypeNode, Node > d_typ_pred;
- //get predicate for type
- Node getPredicateForType( TypeNode tn );
- //
- void getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms );
- //
- void getEnumeratePredUfTerm( Node n, unsigned num, std::vector< Node >& terms );
- // uf operators enumerated
- std::map< Node, bool > d_uf_enum;
-public: //for property enumeration
- //process this candidate conjecture
- void processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth );
- //whether it should be considered, negative : no, positive returns score
- int considerCandidateConjecture( TNode lhs, TNode rhs );
- //notified of a substitution
- bool notifySubstitution( TNode glhs, std::map< TNode, TNode >& subs, TNode rhs );
- //confirmation count
- unsigned d_subs_confirmCount;
- //individual witnesses (for range)
- std::vector< TNode > d_subs_confirmWitnessRange;
- //individual witnesses (for domain)
- std::map< TNode, std::vector< TNode > > d_subs_confirmWitnessDomain;
- //number of ground substitutions whose equality is unknown
- unsigned d_subs_unkCount;
-private: //information about ground equivalence classes
- TNode d_bool_eqc[2];
- std::map< TNode, Node > d_ground_eqc_map;
- std::vector< TNode > d_ground_terms;
- //operator independent term index
- std::map< TNode, OpArgIndex > d_op_arg_index;
- //is handled term
- bool isHandledTerm( TNode n );
- Node getGroundEqc( TNode r );
- bool isGroundEqc( TNode r );
- bool isGroundTerm( TNode n );
- //has enumerated UF
- bool hasEnumeratedUf( Node n );
- // count of full effort checks
- unsigned d_fullEffortCount;
- // has added lemma
- bool d_hasAddedLemma;
- //flush the waiting conjectures
- unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth );
-public:
- ConjectureGenerator( QuantifiersEngine * qe, context::Context* c );
- ~ConjectureGenerator() throw() {}
- /* needs check */
- bool needsCheck( Theory::Effort e );
- /* reset at a round */
- void reset_round( Theory::Effort e );
- /* Call during quantifier engine's check */
- void check( Theory::Effort e, unsigned quant_e );
- /* Called for new quantifiers */
- void registerQuantifier( Node q );
- void assertNode( Node n );
- /** Identify this module (for debugging, dynamic configuration, etc..) */
- std::string identify() const { return "ConjectureGenerator"; }
-//options
-private:
- bool optReqDistinctVarPatterns();
- bool optFilterUnknown();
- int optFilterScoreThreshold();
- unsigned optFullCheckFrequency();
- unsigned optFullCheckConjectures();
-
- bool optStatsOnly();
-};
-
-
-}
-}
-}
-
-#endif
+/********************* */ +/*! \file conjecture_generator.h + ** \verbatim + ** Original author: Andrew Reynolds + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief conjecture generator class + **/ + +#include "cvc4_private.h" + +#ifndef CONJECTURE_GENERATOR_H +#define CONJECTURE_GENERATOR_H + +#include "context/cdhashmap.h" +#include "context/cdchunk_list.h" +#include "theory/quantifiers_engine.h" +#include "theory/type_enumerator.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class TermArgTrie; + +//algorithm for computing candidate subgoals + +class ConjectureGenerator; + +// operator independent index of arguments for an EQC +class OpArgIndex +{ +public: + std::map< TNode, OpArgIndex > d_child; + std::vector< TNode > d_ops; + std::vector< TNode > d_op_terms; + void addTerm( ConjectureGenerator * s, TNode n, unsigned index = 0 ); + Node getGroundTerm( ConjectureGenerator * s, std::vector< TNode >& args ); + void getGroundTerms( ConjectureGenerator * s, std::vector< TNode >& terms ); +}; + +class PatternTypIndex +{ +public: + std::vector< TNode > d_terms; + std::map< TypeNode, std::map< unsigned, PatternTypIndex > > d_children; + void clear() { + d_terms.clear(); + d_children.clear(); + } +}; + +class SubstitutionIndex +{ +public: + //current variable, or ground EQC if d_children.empty() + TNode d_var; + std::map< TNode, SubstitutionIndex > d_children; + //add substitution + void addSubstitution( TNode eqc, std::vector< TNode >& vars, std::vector< TNode >& terms, unsigned i = 0 ); + //notify substitutions + bool notifySubstitutions( ConjectureGenerator * s, std::map< TNode, TNode >& subs, TNode rhs, unsigned numVars, unsigned i = 0 ); +}; + +class TermGenEnv; + +class TermGenerator +{ +private: + unsigned calculateGeneralizationDepth( TermGenEnv * s, std::map< TypeNode, std::vector< int > >& fvs ); +public: + TermGenerator(){} + TypeNode d_typ; + unsigned d_id; + //1 : consider as unique variable + //2 : consider equal to another variable + //5 : consider a function application + unsigned d_status; + int d_status_num; + //for function applications: the number of children you have built + int d_status_child_num; + //children (pointers to TermGenerators) + std::vector< unsigned > d_children; + + //match status + int d_match_status; + int d_match_status_child_num; + //match mode bits + //0 : different variables must have different matches + //1 : variables must map to ground terms + //2 : variables must map to non-ground terms + unsigned d_match_mode; + //children + std::vector< std::map< TNode, TermArgTrie >::iterator > d_match_children; + std::vector< std::map< TNode, TermArgTrie >::iterator > d_match_children_end; + + void reset( TermGenEnv * s, TypeNode tn ); + bool getNextTerm( TermGenEnv * s, unsigned depth ); + void resetMatching( TermGenEnv * s, TNode eqc, unsigned mode ); + bool getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs ); + + unsigned getDepth( TermGenEnv * s ); + unsigned getGeneralizationDepth( TermGenEnv * s ); + Node getTerm( TermGenEnv * s ); + + void debugPrint( TermGenEnv * s, const char * c, const char * cd ); +}; + + +class TermGenEnv +{ +public: + //collect signature information + void collectSignatureInformation(); + //reset function + void reset( unsigned gdepth, bool genRelevant, TypeNode tgen ); + //get next term + bool getNextTerm(); + //reset matching + void resetMatching( TNode eqc, unsigned mode ); + //get next match + bool getNextMatch( TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs ); + //get term + Node getTerm(); + //debug print + void debugPrint( const char * c, const char * cd ); + + //conjecture generation + ConjectureGenerator * d_cg; + //the current number of enumerated variables per type + std::map< TypeNode, unsigned > d_var_id; + //the limit of number of variables per type to enumerate + 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 + std::vector< TNode > d_relevant_eqc[2]; + //candidate equivalence classes + std::vector< std::vector< TNode > > d_ccand_eqc[2]; + //the term generation objects + unsigned d_tg_id; + std::map< unsigned, TermGenerator > d_tg_alloc; + unsigned d_tg_gdepth; + int d_tg_gdepth_limit; + + //all functions + std::vector< TNode > d_funcs; + //function to kind map + std::map< TNode, Kind > d_func_kind; + //type of each argument of the function + std::map< TNode, std::vector< TypeNode > > d_func_args; + + //access functions + unsigned getNumTgVars( TypeNode tn ); + bool allowVar( TypeNode tn ); + void addVar( TypeNode tn ); + void removeVar( TypeNode tn ); + unsigned getNumTgFuncs( TypeNode tn ); + TNode getTgFunc( TypeNode tn, unsigned i ); + Node getFreeVar( TypeNode tn, unsigned i ); + bool considerCurrentTerm(); + bool considerCurrentTermCanon( unsigned tg_id ); + void changeContext( bool add ); + bool isRelevantFunc( Node f ); + //carry + TermDb * getTermDatabase(); + Node getGroundEqc( TNode r ); + bool isGroundEqc( TNode r ); + bool isGroundTerm( TNode n ); +}; + + + +class TheoremIndex +{ +private: + void addTheorem( std::vector< TNode >& lhs_v, std::vector< unsigned >& lhs_arg, TNode rhs ); + void addTheoremNode( TNode curr, std::vector< TNode >& lhs_v, std::vector< unsigned >& lhs_arg, TNode rhs ); + void getEquivalentTerms( std::vector< TNode >& n_v, std::vector< unsigned >& n_arg, + std::map< TNode, TNode >& smap, std::vector< TNode >& vars, std::vector< TNode >& subs, + std::vector< Node >& terms ); + void getEquivalentTermsNode( Node curr, std::vector< TNode >& n_v, std::vector< unsigned >& n_arg, + std::map< TNode, TNode >& smap, std::vector< TNode >& vars, std::vector< TNode >& subs, + std::vector< Node >& terms ); +public: + std::map< TypeNode, TNode > d_var; + std::map< TNode, TheoremIndex > d_children; + std::vector< Node > d_terms; + + void addTheorem( TNode lhs, TNode rhs ) { + std::vector< TNode > v; + std::vector< unsigned > a; + addTheoremNode( lhs, v, a, rhs ); + } + void getEquivalentTerms( TNode n, std::vector< Node >& terms ) { + std::vector< TNode > nv; + std::vector< unsigned > na; + std::map< TNode, TNode > smap; + std::vector< TNode > vars; + std::vector< TNode > subs; + getEquivalentTermsNode( n, nv, na, smap, vars, subs, terms ); + } + void clear(){ + d_var.clear(); + d_children.clear(); + d_terms.clear(); + } + void debugPrint( const char * c, unsigned ind = 0 ); +}; + + + +class ConjectureGenerator : public QuantifiersModule +{ + friend class OpArgIndex; + friend class PatGen; + friend class PatternGenEqc; + friend class PatternGen; + friend class SubsEqcIndex; + friend class TermGenerator; + friend class TermGenEnv; + typedef context::CDChunkList<Node> NodeList; + typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; + typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; +//this class maintains a congruence closure for *universal* facts +private: + //notification class for equality engine + class NotifyClass : public eq::EqualityEngineNotify { + ConjectureGenerator& d_sg; + public: + NotifyClass(ConjectureGenerator& sg): d_sg(sg) {} + bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; } + bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; } + bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { return true; } + void eqNotifyConstantTermMerge(TNode t1, TNode t2) { } + void eqNotifyNewClass(TNode t) { d_sg.eqNotifyNewClass(t); } + void eqNotifyPreMerge(TNode t1, TNode t2) { d_sg.eqNotifyPreMerge(t1, t2); } + void eqNotifyPostMerge(TNode t1, TNode t2) { d_sg.eqNotifyPostMerge(t1, t2); } + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {d_sg.eqNotifyDisequal(t1, t2, reason); } + };/* class ConjectureGenerator::NotifyClass */ + /** The notify class */ + NotifyClass d_notify; + class EqcInfo{ + public: + EqcInfo( context::Context* c ); + //representative + context::CDO< Node > d_rep; + }; + /** get or make eqc info */ + EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false ); + /** (universal) equaltity engine */ + eq::EqualityEngine d_uequalityEngine; + /** pending adds */ + std::vector< Node > d_upendingAdds; + /** relevant terms */ + std::map< Node, bool > d_urelevant_terms; + /** information necessary for equivalence classes */ + std::map< Node, EqcInfo* > d_eqc_info; + /** called when a new equivalance class is created */ + void eqNotifyNewClass(TNode t); + /** called when two equivalance classes will merge */ + void eqNotifyPreMerge(TNode t1, TNode t2); + /** called when two equivalance classes have merged */ + void eqNotifyPostMerge(TNode t1, TNode t2); + /** called when two equivalence classes are made disequal */ + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); + /** are universal equal */ + bool areUniversalEqual( TNode n1, TNode n2 ); + /** are universal disequal */ + bool areUniversalDisequal( TNode n1, TNode n2 ); + /** get universal representative */ + TNode getUniversalRepresentative( TNode n, bool add = false ); + /** set relevant */ + void setUniversalRelevant( TNode n ); + /** ordering for universal terms */ + bool isUniversalLessThan( TNode rt1, TNode rt2 ); + + /** the nodes we have reported as canonical representative */ + std::vector< TNode > d_ue_canon; + /** is reported canon */ + bool isReportedCanon( TNode n ); + /** mark that term has been reported as canonical rep */ + void markReportedCanon( TNode n ); + +private: //information regarding the conjectures + /** list of all conjectures */ + std::vector< Node > d_conjectures; + /** list of all waiting conjectures */ + std::vector< Node > d_waiting_conjectures_lhs; + std::vector< Node > d_waiting_conjectures_rhs; + std::vector< int > d_waiting_conjectures_score; + /** map of currently considered equality conjectures */ + std::map< Node, std::vector< Node > > d_waiting_conjectures; + /** map of equality conjectures */ + std::map< Node, std::vector< Node > > d_eq_conjectures; + /** currently existing conjectures in equality engine */ + BoolMap d_ee_conjectures; + /** conjecture index */ + TheoremIndex d_thm_index; +private: //free variable list + //free variables + std::map< TypeNode, std::vector< Node > > d_free_var; + //map from free variable to FV# + std::map< TNode, unsigned > d_free_var_num; + // get canonical free variable #i of type tn + Node getFreeVar( TypeNode tn, unsigned i ); + // get canonical term, return null if it contains a term apart from handled signature + Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs ); +private: //information regarding the terms + //relevant patterns (the LHS's) + std::map< TypeNode, std::vector< Node > > d_rel_patterns; + //total number of unique variables + std::map< TNode, unsigned > d_rel_pattern_var_sum; + //by types + PatternTypIndex d_rel_pattern_typ_index; + // substitution to ground EQC index + std::map< TNode, SubstitutionIndex > d_rel_pattern_subs_index; + //patterns (the RHS's) + std::map< TypeNode, std::vector< Node > > d_patterns; + //patterns to # variables per type + std::map< TNode, std::map< TypeNode, unsigned > > d_pattern_var_id; + // # duplicated variables + std::map< TNode, unsigned > d_pattern_var_duplicate; + // is normal pattern? (variables allocated in canonical way left to right) + std::map< TNode, int > d_pattern_is_normal; + std::map< TNode, int > d_pattern_is_relevant; + // patterns to a count of # operators (variables and functions) + std::map< TNode, std::map< TNode, unsigned > > d_pattern_fun_id; + // term size + std::map< TNode, unsigned > d_pattern_fun_sum; + // collect functions + unsigned collectFunctions( TNode opat, TNode pat, std::map< TNode, unsigned >& funcs, + std::map< TypeNode, unsigned >& mnvn, std::map< TypeNode, unsigned >& mxvn ); + // add pattern + void registerPattern( Node pat, TypeNode tpat ); +private: //for debugging + std::map< TNode, unsigned > d_em; + unsigned d_conj_count; +public: + //term generation environment + TermGenEnv d_tge; + //consider term canon + bool considerTermCanon( Node ln, bool genRelevant ); +public: //for generalization + //generalizations + bool isGeneralization( TNode patg, TNode pat ) { + std::map< TNode, TNode > subs; + return isGeneralization( patg, pat, subs ); + } + bool isGeneralization( TNode patg, TNode pat, std::map< TNode, TNode >& subs ); + // get generalization depth + int calculateGeneralizationDepth( TNode n, std::vector< TNode >& fv ); +private: + //predicate for type + std::map< TypeNode, Node > d_typ_pred; + //get predicate for type + Node getPredicateForType( TypeNode tn ); + // + void getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms ); + // + void getEnumeratePredUfTerm( Node n, unsigned num, std::vector< Node >& terms ); + // uf operators enumerated + std::map< Node, bool > d_uf_enum; +public: //for property enumeration + //process this candidate conjecture + void processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth ); + //whether it should be considered, negative : no, positive returns score + int considerCandidateConjecture( TNode lhs, TNode rhs ); + //notified of a substitution + bool notifySubstitution( TNode glhs, std::map< TNode, TNode >& subs, TNode rhs ); + //confirmation count + unsigned d_subs_confirmCount; + //individual witnesses (for range) + std::vector< TNode > d_subs_confirmWitnessRange; + //individual witnesses (for domain) + std::map< TNode, std::vector< TNode > > d_subs_confirmWitnessDomain; + //number of ground substitutions whose equality is unknown + unsigned d_subs_unkCount; +private: //information about ground equivalence classes + TNode d_bool_eqc[2]; + std::map< TNode, Node > d_ground_eqc_map; + std::vector< TNode > d_ground_terms; + //operator independent term index + std::map< TNode, OpArgIndex > d_op_arg_index; + //is handled term + bool isHandledTerm( TNode n ); + Node getGroundEqc( TNode r ); + bool isGroundEqc( TNode r ); + bool isGroundTerm( TNode n ); + //has enumerated UF + bool hasEnumeratedUf( Node n ); + // count of full effort checks + unsigned d_fullEffortCount; + // has added lemma + bool d_hasAddedLemma; + //flush the waiting conjectures + unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth ); +public: + ConjectureGenerator( QuantifiersEngine * qe, context::Context* c ); + ~ConjectureGenerator() throw() {} + /* needs check */ + bool needsCheck( Theory::Effort e ); + /* reset at a round */ + void reset_round( Theory::Effort e ); + /* Call during quantifier engine's check */ + void check( Theory::Effort e, unsigned quant_e ); + /* Called for new quantifiers */ + void registerQuantifier( Node q ); + void assertNode( Node n ); + /** Identify this module (for debugging, dynamic configuration, etc..) */ + std::string identify() const { return "ConjectureGenerator"; } +//options +private: + bool optReqDistinctVarPatterns(); + bool optFilterUnknown(); + int optFilterScoreThreshold(); + unsigned optFullCheckFrequency(); + unsigned optFullCheckConjectures(); + + bool optStatsOnly(); +}; + + +} +} +} + +#endif |