src/theory/quantifiers/conjecture_generator.h

   1 /*********************                                                        */
   2 /*! \file conjecture_generator.h
   3  ** \verbatim
   4  ** Original author: Andrew Reynolds
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief conjecture generator class
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CONJECTURE_GENERATOR_H
  18 #define CONJECTURE_GENERATOR_H
  19
  20 #include "context/cdhashmap.h"
  21 #include "context/cdchunk_list.h"
  22 #include "theory/quantifiers_engine.h"
  23 #include "theory/type_enumerator.h"
  24
  25 namespace CVC4 {
  26 namespace theory {
  27 namespace quantifiers {
  28
  29 class TermArgTrie;
  30
  31 //algorithm for computing candidate subgoals
  32
  33 class ConjectureGenerator;
  34
  35 // operator independent index of arguments for an EQC
  36 class OpArgIndex
  37 {
  38 public:
  39   std::map< TNode, OpArgIndex > d_child;
  40   std::vector< TNode > d_ops;
  41   std::vector< TNode > d_op_terms;
  42   void addTerm( ConjectureGenerator * s, TNode n, unsigned index = 0 );
  43   Node getGroundTerm( ConjectureGenerator * s, std::vector< TNode >& args );
  44   void getGroundTerms( ConjectureGenerator * s, std::vector< TNode >& terms );
  45 };
  46
  47 class PatternTypIndex
  48 {
  49 public:
  50   std::vector< TNode > d_terms;
  51   std::map< TypeNode, std::map< unsigned, PatternTypIndex > > d_children;
  52   void clear() {
  53     d_terms.clear();
  54     d_children.clear();
  55   }
  56 };
  57
  58 class SubstitutionIndex
  59 {
  60 public:
  61   //current variable, or ground EQC if d_children.empty()
  62   TNode d_var;
  63   std::map< TNode, SubstitutionIndex > d_children;
  64   //add substitution
  65   void addSubstitution( TNode eqc, std::vector< TNode >& vars, std::vector< TNode >& terms, unsigned i = 0 );
  66   //notify substitutions
  67   bool notifySubstitutions( ConjectureGenerator * s, std::map< TNode, TNode >& subs, TNode rhs, unsigned numVars, unsigned i = 0 );
  68 };
  69
  70 class TermGenEnv;
  71
  72 class TermGenerator
  73 {
  74 private:
  75   unsigned calculateGeneralizationDepth( TermGenEnv * s, std::map< TypeNode, std::vector< int > >& fvs );
  76 public:
  77   TermGenerator(){}
  78   TypeNode d_typ;
  79   unsigned d_id;
  80   //1 : consider as unique variable
  81   //2 : consider equal to another variable
  82   //5 : consider a function application
  83   unsigned d_status;
  84   int d_status_num;
  85   //for function applications: the number of children you have built
  86   int d_status_child_num;
  87   //children (pointers to TermGenerators)
  88   std::vector< unsigned > d_children;
  89
  90   //match status
  91   int d_match_status;
  92   int d_match_status_child_num;
  93   //match mode bits
  94   //0 : different variables must have different matches
  95   //1 : variables must map to ground terms
  96   //2 : variables must map to non-ground terms
  97   unsigned d_match_mode;
  98   //children
  99   std::vector< std::map< TNode, TermArgTrie >::iterator > d_match_children;
 100   std::vector< std::map< TNode, TermArgTrie >::iterator > d_match_children_end;
 101
 102   void reset( TermGenEnv * s, TypeNode tn );
 103   bool getNextTerm( TermGenEnv * s, unsigned depth );
 104   void resetMatching( TermGenEnv * s, TNode eqc, unsigned mode );
 105   bool getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs );
 106
 107   unsigned getDepth( TermGenEnv * s );
 108   unsigned getGeneralizationDepth( TermGenEnv * s );
 109   Node getTerm( TermGenEnv * s );
 110
 111   void debugPrint( TermGenEnv * s, const char * c, const char * cd );
 112 };
 113
 114
 115 class TermGenEnv
 116 {
 117 public:
 118   //collect signature information
 119   void collectSignatureInformation();
 120   //reset function
 121   void reset( unsigned gdepth, bool genRelevant, TypeNode tgen );
 122   //get next term
 123   bool getNextTerm();
 124   //reset matching
 125   void resetMatching( TNode eqc, unsigned mode );
 126   //get next match
 127   bool getNextMatch( TNode eqc, std::map< TypeNode, std::map< unsigned, TNode > >& subs, std::map< TNode, bool >& rev_subs );
 128   //get term
 129   Node getTerm();
 130   //debug print
 131   void debugPrint( const char * c, const char * cd );
 132
 133   //conjecture generation
 134   ConjectureGenerator * d_cg;
 135   //the current number of enumerated variables per type
 136   std::map< TypeNode, unsigned > d_var_id;
 137   //the limit of number of variables per type to enumerate
 138   std::map< TypeNode, unsigned > d_var_limit;
 139   //the functions we can currently generate
 140   std::map< TypeNode, std::vector< TNode > > d_typ_tg_funcs;
 141   // whether functions must add operators
 142   std::map< TNode, bool > d_tg_func_param;
 143   //the equivalence classes (if applicable) that match the currently generated term
 144   bool d_gen_relevant_terms;
 145   //relevant equivalence classes
 146   std::vector< TNode > d_relevant_eqc[2];
 147   //candidate equivalence classes
 148   std::vector< std::vector< TNode > > d_ccand_eqc[2];
 149   //the term generation objects
 150   unsigned d_tg_id;
 151   std::map< unsigned, TermGenerator > d_tg_alloc;
 152   unsigned d_tg_gdepth;
 153   int d_tg_gdepth_limit;
 154
 155   //all functions
 156   std::vector< TNode > d_funcs;
 157   //function to kind map
 158   std::map< TNode, Kind > d_func_kind;
 159   //type of each argument of the function
 160   std::map< TNode, std::vector< TypeNode > > d_func_args;
 161
 162   //access functions
 163   unsigned getNumTgVars( TypeNode tn );
 164   bool allowVar( TypeNode tn );
 165   void addVar( TypeNode tn );
 166   void removeVar( TypeNode tn );
 167   unsigned getNumTgFuncs( TypeNode tn );
 168   TNode getTgFunc( TypeNode tn, unsigned i );
 169   Node getFreeVar( TypeNode tn, unsigned i );
 170   bool considerCurrentTerm();
 171   bool considerCurrentTermCanon( unsigned tg_id );
 172   void changeContext( bool add );
 173   bool isRelevantFunc( Node f );
 174   bool isRelevantTerm( Node t );
 175   //carry
 176   TermDb * getTermDatabase();
 177   Node getGroundEqc( TNode r );
 178   bool isGroundEqc( TNode r );
 179   bool isGroundTerm( TNode n );
 180 };
 181
 182
 183
 184 class TheoremIndex
 185 {
 186 private:
 187   void addTheorem( std::vector< TNode >& lhs_v, std::vector< unsigned >& lhs_arg, TNode rhs );
 188   void addTheoremNode( TNode curr, std::vector< TNode >& lhs_v, std::vector< unsigned >& lhs_arg, TNode rhs );
 189   void getEquivalentTerms( std::vector< TNode >& n_v, std::vector< unsigned >& n_arg,
 190                            std::map< TNode, TNode >& smap, std::vector< TNode >& vars, std::vector< TNode >& subs,
 191                            std::vector< Node >& terms );
 192   void getEquivalentTermsNode( Node curr, std::vector< TNode >& n_v, std::vector< unsigned >& n_arg,
 193                                std::map< TNode, TNode >& smap, std::vector< TNode >& vars, std::vector< TNode >& subs,
 194                                std::vector< Node >& terms );
 195 public:
 196   std::map< TypeNode, TNode > d_var;
 197   std::map< TNode, TheoremIndex > d_children;
 198   std::vector< Node > d_terms;
 199
 200   void addTheorem( TNode lhs, TNode rhs ) {
 201     std::vector< TNode > v;
 202     std::vector< unsigned > a;
 203     addTheoremNode( lhs, v, a, rhs );
 204   }
 205   void getEquivalentTerms( TNode n, std::vector< Node >& terms ) {
 206     std::vector< TNode > nv;
 207     std::vector< unsigned > na;
 208     std::map< TNode, TNode > smap;
 209     std::vector< TNode > vars;
 210     std::vector< TNode > subs;
 211     getEquivalentTermsNode( n, nv, na, smap, vars, subs, terms );
 212   }
 213   void clear(){
 214     d_var.clear();
 215     d_children.clear();
 216     d_terms.clear();
 217   }
 218   void debugPrint( const char * c, unsigned ind = 0 );
 219 };
 220
 221
 222
 223 class ConjectureGenerator : public QuantifiersModule
 224 {
 225   friend class OpArgIndex;
 226   friend class PatGen;
 227   friend class PatternGenEqc;
 228   friend class PatternGen;
 229   friend class SubsEqcIndex;
 230   friend class TermGenerator;
 231   friend class TermGenEnv;
 232   typedef context::CDChunkList<Node> NodeList;
 233   typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
 234   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
 235 //this class maintains a congruence closure for *universal* facts
 236 private:
 237   //notification class for equality engine
 238   class NotifyClass : public eq::EqualityEngineNotify {
 239     ConjectureGenerator& d_sg;
 240   public:
 241     NotifyClass(ConjectureGenerator& sg): d_sg(sg) {}
 242     bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; }
 243     bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; }
 244     bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { return true; }
 245     void eqNotifyConstantTermMerge(TNode t1, TNode t2) { }
 246     void eqNotifyNewClass(TNode t) { d_sg.eqNotifyNewClass(t); }
 247     void eqNotifyPreMerge(TNode t1, TNode t2) { d_sg.eqNotifyPreMerge(t1, t2); }
 248     void eqNotifyPostMerge(TNode t1, TNode t2) { d_sg.eqNotifyPostMerge(t1, t2); }
 249     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {d_sg.eqNotifyDisequal(t1, t2, reason); }
 250   };/* class ConjectureGenerator::NotifyClass */
 251   /** The notify class */
 252   NotifyClass d_notify;
 253   class EqcInfo{
 254   public:
 255     EqcInfo( context::Context* c );
 256     //representative
 257     context::CDO< Node > d_rep;
 258   };
 259   /** get or make eqc info */
 260   EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false );
 261   /** (universal) equaltity engine */
 262   eq::EqualityEngine d_uequalityEngine;
 263   /** pending adds */
 264   std::vector< Node > d_upendingAdds;
 265   /** relevant terms */
 266   std::map< Node, bool > d_urelevant_terms;
 267   /** information necessary for equivalence classes */
 268   std::map< Node, EqcInfo* > d_eqc_info;
 269   /** called when a new equivalance class is created */
 270   void eqNotifyNewClass(TNode t);
 271   /** called when two equivalance classes will merge */
 272   void eqNotifyPreMerge(TNode t1, TNode t2);
 273   /** called when two equivalance classes have merged */
 274   void eqNotifyPostMerge(TNode t1, TNode t2);
 275   /** called when two equivalence classes are made disequal */
 276   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
 277   /** are universal equal */
 278   bool areUniversalEqual( TNode n1, TNode n2 );
 279   /** are universal disequal */
 280   bool areUniversalDisequal( TNode n1, TNode n2 );
 281   /** get universal representative */
 282   TNode getUniversalRepresentative( TNode n, bool add = false );
 283   /** set relevant */
 284   void setUniversalRelevant( TNode n );
 285   /** ordering for universal terms */
 286   bool isUniversalLessThan( TNode rt1, TNode rt2 );
 287
 288   /** the nodes we have reported as canonical representative */
 289   std::vector< TNode > d_ue_canon;
 290   /** is reported canon */
 291   bool isReportedCanon( TNode n );
 292   /** mark that term has been reported as canonical rep */
 293   void markReportedCanon( TNode n );
 294
 295 private:  //information regarding the conjectures
 296   /** list of all conjectures */
 297   std::vector< Node > d_conjectures;
 298   /** list of all waiting conjectures */
 299   std::vector< Node > d_waiting_conjectures_lhs;
 300   std::vector< Node > d_waiting_conjectures_rhs;
 301   std::vector< int > d_waiting_conjectures_score;
 302   /** map of currently considered equality conjectures */
 303   std::map< Node, std::vector< Node > > d_waiting_conjectures;
 304   /** map of equality conjectures */
 305   std::map< Node, std::vector< Node > > d_eq_conjectures;
 306   /** currently existing conjectures in equality engine */
 307   BoolMap d_ee_conjectures;
 308   /** conjecture index */
 309   TheoremIndex d_thm_index;
 310 private:  //free variable list
 311   // get canonical free variable #i of type tn
 312   Node getFreeVar( TypeNode tn, unsigned i );
 313 private:  //information regarding the terms
 314   //relevant patterns (the LHS's)
 315   std::map< TypeNode, std::vector< Node > > d_rel_patterns;
 316   //total number of unique variables
 317   std::map< TNode, unsigned > d_rel_pattern_var_sum;
 318   //by types
 319   PatternTypIndex d_rel_pattern_typ_index;
 320   // substitution to ground EQC index
 321   std::map< TNode, SubstitutionIndex > d_rel_pattern_subs_index;
 322   //patterns (the RHS's)
 323   std::map< TypeNode, std::vector< Node > > d_patterns;
 324   //patterns to # variables per type
 325   std::map< TNode, std::map< TypeNode, unsigned > > d_pattern_var_id;
 326   // # duplicated variables
 327   std::map< TNode, unsigned > d_pattern_var_duplicate;
 328   // is normal pattern?  (variables allocated in canonical way left to right)
 329   std::map< TNode, int > d_pattern_is_normal;
 330   std::map< TNode, int > d_pattern_is_relevant;
 331   // patterns to a count of # operators (variables and functions)
 332   std::map< TNode, std::map< TNode, unsigned > > d_pattern_fun_id;
 333   // term size
 334   std::map< TNode, unsigned > d_pattern_fun_sum;
 335   // collect functions
 336   unsigned collectFunctions( TNode opat, TNode pat, std::map< TNode, unsigned >& funcs,
 337                              std::map< TypeNode, unsigned >& mnvn, std::map< TypeNode, unsigned >& mxvn );
 338   // add pattern
 339   void registerPattern( Node pat, TypeNode tpat );
 340 private: //for debugging
 341   std::map< TNode, unsigned > d_em;
 342   unsigned d_conj_count;
 343 public:
 344   //term generation environment
 345   TermGenEnv d_tge;
 346   //consider term canon
 347   bool considerTermCanon( Node ln, bool genRelevant );
 348 public:  //for generalization
 349   //generalizations
 350   bool isGeneralization( TNode patg, TNode pat ) {
 351     std::map< TNode, TNode > subs;
 352     return isGeneralization( patg, pat, subs );
 353   }
 354   bool isGeneralization( TNode patg, TNode pat, std::map< TNode, TNode >& subs );
 355   // get generalization depth
 356   int calculateGeneralizationDepth( TNode n, std::vector< TNode >& fv );
 357 private:
 358   //predicate for type
 359   std::map< TypeNode, Node > d_typ_pred;
 360   //get predicate for type
 361   Node getPredicateForType( TypeNode tn );
 362   //
 363   void getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms );
 364   //
 365   void getEnumeratePredUfTerm( Node n, unsigned num, std::vector< Node >& terms );
 366   // uf operators enumerated
 367   std::map< Node, bool > d_uf_enum;
 368 public:  //for property enumeration
 369   //process this candidate conjecture
 370   void processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth );
 371   //whether it should be considered, negative : no, positive returns score
 372   int considerCandidateConjecture( TNode lhs, TNode rhs );
 373   //notified of a substitution
 374   bool notifySubstitution( TNode glhs, std::map< TNode, TNode >& subs, TNode rhs );
 375   //confirmation count
 376   unsigned d_subs_confirmCount;
 377   //individual witnesses (for range)
 378   std::vector< TNode > d_subs_confirmWitnessRange;
 379   //individual witnesses (for domain)
 380   std::map< TNode, std::vector< TNode > > d_subs_confirmWitnessDomain;
 381   //number of ground substitutions whose equality is unknown
 382   unsigned d_subs_unkCount;
 383 private:  //information about ground equivalence classes
 384   TNode d_bool_eqc[2];
 385   std::map< TNode, Node > d_ground_eqc_map;
 386   std::vector< TNode > d_ground_terms;
 387   //operator independent term index
 388   std::map< TNode, OpArgIndex > d_op_arg_index;
 389   //is handled term
 390   bool isHandledTerm( TNode n );
 391   Node getGroundEqc( TNode r );
 392   bool isGroundEqc( TNode r );
 393   bool isGroundTerm( TNode n );
 394   //has enumerated UF
 395   bool hasEnumeratedUf( Node n );
 396   // count of full effort checks
 397   unsigned d_fullEffortCount;
 398   // has added lemma
 399   bool d_hasAddedLemma;
 400   //flush the waiting conjectures
 401   unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth );
 402 public:
 403   ConjectureGenerator( QuantifiersEngine * qe, context::Context* c );
 404   ~ConjectureGenerator() throw() {}
 405   /* needs check */
 406   bool needsCheck( Theory::Effort e );
 407   /* reset at a round */
 408   void reset_round( Theory::Effort e );
 409   /* Call during quantifier engine's check */
 410   void check( Theory::Effort e, unsigned quant_e );
 411   /* Called for new quantifiers */
 412   void registerQuantifier( Node q );
 413   void assertNode( Node n );
 414   /** Identify this module (for debugging, dynamic configuration, etc..) */
 415   std::string identify() const { return "ConjectureGenerator"; }
 416 //options
 417 private:
 418   bool optReqDistinctVarPatterns();
 419   bool optFilterUnknown();
 420   int optFilterScoreThreshold();
 421   unsigned optFullCheckFrequency();
 422   unsigned optFullCheckConjectures();
 423
 424   bool optStatsOnly();
 425 };
 426
 427
 428 }
 429 }
 430 }
 431
 432 #endif