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   //the equivalence classes (if applicable) that match the currently generated term
 142   bool d_gen_relevant_terms;
 143   //relevant equivalence classes
 144   std::vector< TNode > d_relevant_eqc[2];
 145   //candidate equivalence classes
 146   std::vector< std::vector< TNode > > d_ccand_eqc[2];
 147   //the term generation objects
 148   unsigned d_tg_id;
 149   std::map< unsigned, TermGenerator > d_tg_alloc;
 150   unsigned d_tg_gdepth;
 151   int d_tg_gdepth_limit;
 152
 153   //all functions
 154   std::vector< TNode > d_funcs;
 155   //function to kind map
 156   std::map< TNode, Kind > d_func_kind;
 157   //type of each argument of the function
 158   std::map< TNode, std::vector< TypeNode > > d_func_args;
 159
 160   //access functions
 161   unsigned getNumTgVars( TypeNode tn );
 162   bool allowVar( TypeNode tn );
 163   void addVar( TypeNode tn );
 164   void removeVar( TypeNode tn );
 165   unsigned getNumTgFuncs( TypeNode tn );
 166   TNode getTgFunc( TypeNode tn, unsigned i );
 167   Node getFreeVar( TypeNode tn, unsigned i );
 168   bool considerCurrentTerm();
 169   bool considerCurrentTermCanon( unsigned tg_id );
 170   void changeContext( bool add );
 171   bool isRelevantFunc( Node f );
 172   //carry
 173   TermDb * getTermDatabase();
 174   Node getGroundEqc( TNode r );
 175   bool isGroundEqc( TNode r );
 176   bool isGroundTerm( TNode n );
 177 };
 178
 179
 180
 181 class TheoremIndex
 182 {
 183 private:
 184   void addTheorem( std::vector< TNode >& lhs_v, std::vector< unsigned >& lhs_arg, TNode rhs );
 185   void addTheoremNode( TNode curr, std::vector< TNode >& lhs_v, std::vector< unsigned >& lhs_arg, TNode rhs );
 186   void getEquivalentTerms( std::vector< TNode >& n_v, std::vector< unsigned >& n_arg,
 187                            std::map< TNode, TNode >& smap, std::vector< TNode >& vars, std::vector< TNode >& subs,
 188                            std::vector< Node >& terms );
 189   void getEquivalentTermsNode( Node curr, 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 public:
 193   std::map< TypeNode, TNode > d_var;
 194   std::map< TNode, TheoremIndex > d_children;
 195   std::vector< Node > d_terms;
 196
 197   void addTheorem( TNode lhs, TNode rhs ) {
 198     std::vector< TNode > v;
 199     std::vector< unsigned > a;
 200     addTheoremNode( lhs, v, a, rhs );
 201   }
 202   void getEquivalentTerms( TNode n, std::vector< Node >& terms ) {
 203     std::vector< TNode > nv;
 204     std::vector< unsigned > na;
 205     std::map< TNode, TNode > smap;
 206     std::vector< TNode > vars;
 207     std::vector< TNode > subs;
 208     getEquivalentTermsNode( n, nv, na, smap, vars, subs, terms );
 209   }
 210   void clear(){
 211     d_var.clear();
 212     d_children.clear();
 213     d_terms.clear();
 214   }
 215   void debugPrint( const char * c, unsigned ind = 0 );
 216 };
 217
 218
 219
 220 class ConjectureGenerator : public QuantifiersModule
 221 {
 222   friend class OpArgIndex;
 223   friend class PatGen;
 224   friend class PatternGenEqc;
 225   friend class PatternGen;
 226   friend class SubsEqcIndex;
 227   friend class TermGenerator;
 228   friend class TermGenEnv;
 229   typedef context::CDChunkList<Node> NodeList;
 230   typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
 231   typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
 232 //this class maintains a congruence closure for *universal* facts
 233 private:
 234   //notification class for equality engine
 235   class NotifyClass : public eq::EqualityEngineNotify {
 236     ConjectureGenerator& d_sg;
 237   public:
 238     NotifyClass(ConjectureGenerator& sg): d_sg(sg) {}
 239     bool eqNotifyTriggerEquality(TNode equality, bool value) { return true; }
 240     bool eqNotifyTriggerPredicate(TNode predicate, bool value) { return true; }
 241     bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { return true; }
 242     void eqNotifyConstantTermMerge(TNode t1, TNode t2) { }
 243     void eqNotifyNewClass(TNode t) { d_sg.eqNotifyNewClass(t); }
 244     void eqNotifyPreMerge(TNode t1, TNode t2) { d_sg.eqNotifyPreMerge(t1, t2); }
 245     void eqNotifyPostMerge(TNode t1, TNode t2) { d_sg.eqNotifyPostMerge(t1, t2); }
 246     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {d_sg.eqNotifyDisequal(t1, t2, reason); }
 247   };/* class ConjectureGenerator::NotifyClass */
 248   /** The notify class */
 249   NotifyClass d_notify;
 250   class EqcInfo{
 251   public:
 252     EqcInfo( context::Context* c );
 253     //representative
 254     context::CDO< Node > d_rep;
 255   };
 256   /** get or make eqc info */
 257   EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false );
 258   /** (universal) equaltity engine */
 259   eq::EqualityEngine d_uequalityEngine;
 260   /** pending adds */
 261   std::vector< Node > d_upendingAdds;
 262   /** relevant terms */
 263   std::map< Node, bool > d_urelevant_terms;
 264   /** information necessary for equivalence classes */
 265   std::map< Node, EqcInfo* > d_eqc_info;
 266   /** called when a new equivalance class is created */
 267   void eqNotifyNewClass(TNode t);
 268   /** called when two equivalance classes will merge */
 269   void eqNotifyPreMerge(TNode t1, TNode t2);
 270   /** called when two equivalance classes have merged */
 271   void eqNotifyPostMerge(TNode t1, TNode t2);
 272   /** called when two equivalence classes are made disequal */
 273   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
 274   /** are universal equal */
 275   bool areUniversalEqual( TNode n1, TNode n2 );
 276   /** are universal disequal */
 277   bool areUniversalDisequal( TNode n1, TNode n2 );
 278   /** get universal representative */
 279   TNode getUniversalRepresentative( TNode n, bool add = false );
 280   /** set relevant */
 281   void setUniversalRelevant( TNode n );
 282   /** ordering for universal terms */
 283   bool isUniversalLessThan( TNode rt1, TNode rt2 );
 284
 285   /** the nodes we have reported as canonical representative */
 286   std::vector< TNode > d_ue_canon;
 287   /** is reported canon */
 288   bool isReportedCanon( TNode n );
 289   /** mark that term has been reported as canonical rep */
 290   void markReportedCanon( TNode n );
 291
 292 private:  //information regarding the conjectures
 293   /** list of all conjectures */
 294   std::vector< Node > d_conjectures;
 295   /** list of all waiting conjectures */
 296   std::vector< Node > d_waiting_conjectures_lhs;
 297   std::vector< Node > d_waiting_conjectures_rhs;
 298   std::vector< int > d_waiting_conjectures_score;
 299   /** map of currently considered equality conjectures */
 300   std::map< Node, std::vector< Node > > d_waiting_conjectures;
 301   /** map of equality conjectures */
 302   std::map< Node, std::vector< Node > > d_eq_conjectures;
 303   /** currently existing conjectures in equality engine */
 304   BoolMap d_ee_conjectures;
 305   /** conjecture index */
 306   TheoremIndex d_thm_index;
 307 private:  //free variable list
 308   //free variables
 309   std::map< TypeNode, std::vector< Node > > d_free_var;
 310   //map from free variable to FV#
 311   std::map< TNode, unsigned > d_free_var_num;
 312   // get canonical free variable #i of type tn
 313   Node getFreeVar( TypeNode tn, unsigned i );
 314   // get canonical term, return null if it contains a term apart from handled signature
 315   Node getCanonicalTerm( TNode n, std::map< TypeNode, unsigned >& var_count, std::map< TNode, TNode >& subs );
 316 private:  //information regarding the terms
 317   //relevant patterns (the LHS's)
 318   std::map< TypeNode, std::vector< Node > > d_rel_patterns;
 319   //total number of unique variables
 320   std::map< TNode, unsigned > d_rel_pattern_var_sum;
 321   //by types
 322   PatternTypIndex d_rel_pattern_typ_index;
 323   // substitution to ground EQC index
 324   std::map< TNode, SubstitutionIndex > d_rel_pattern_subs_index;
 325   //patterns (the RHS's)
 326   std::map< TypeNode, std::vector< Node > > d_patterns;
 327   //patterns to # variables per type
 328   std::map< TNode, std::map< TypeNode, unsigned > > d_pattern_var_id;
 329   // # duplicated variables
 330   std::map< TNode, unsigned > d_pattern_var_duplicate;
 331   // is normal pattern?  (variables allocated in canonical way left to right)
 332   std::map< TNode, int > d_pattern_is_normal;
 333   std::map< TNode, int > d_pattern_is_relevant;
 334   // patterns to a count of # operators (variables and functions)
 335   std::map< TNode, std::map< TNode, unsigned > > d_pattern_fun_id;
 336   // term size
 337   std::map< TNode, unsigned > d_pattern_fun_sum;
 338   // collect functions
 339   unsigned collectFunctions( TNode opat, TNode pat, std::map< TNode, unsigned >& funcs,
 340                              std::map< TypeNode, unsigned >& mnvn, std::map< TypeNode, unsigned >& mxvn );
 341   // add pattern
 342   void registerPattern( Node pat, TypeNode tpat );
 343 private: //for debugging
 344   std::map< TNode, unsigned > d_em;
 345   unsigned d_conj_count;
 346 public:
 347   //term generation environment
 348   TermGenEnv d_tge;
 349   //consider term canon
 350   bool considerTermCanon( Node ln, bool genRelevant );
 351 public:  //for generalization
 352   //generalizations
 353   bool isGeneralization( TNode patg, TNode pat ) {
 354     std::map< TNode, TNode > subs;
 355     return isGeneralization( patg, pat, subs );
 356   }
 357   bool isGeneralization( TNode patg, TNode pat, std::map< TNode, TNode >& subs );
 358   // get generalization depth
 359   int calculateGeneralizationDepth( TNode n, std::vector< TNode >& fv );
 360 private:
 361   //predicate for type
 362   std::map< TypeNode, Node > d_typ_pred;
 363   //get predicate for type
 364   Node getPredicateForType( TypeNode tn );
 365   //
 366   void getEnumerateUfTerm( Node n, unsigned num, std::vector< Node >& terms );
 367   //
 368   void getEnumeratePredUfTerm( Node n, unsigned num, std::vector< Node >& terms );
 369   // uf operators enumerated
 370   std::map< Node, bool > d_uf_enum;
 371 public:  //for property enumeration
 372   //process this candidate conjecture
 373   void processCandidateConjecture( TNode lhs, TNode rhs, unsigned lhs_depth, unsigned rhs_depth );
 374   //whether it should be considered, negative : no, positive returns score
 375   int considerCandidateConjecture( TNode lhs, TNode rhs );
 376   //notified of a substitution
 377   bool notifySubstitution( TNode glhs, std::map< TNode, TNode >& subs, TNode rhs );
 378   //confirmation count
 379   unsigned d_subs_confirmCount;
 380   //individual witnesses (for range)
 381   std::vector< TNode > d_subs_confirmWitnessRange;
 382   //individual witnesses (for domain)
 383   std::map< TNode, std::vector< TNode > > d_subs_confirmWitnessDomain;
 384   //number of ground substitutions whose equality is unknown
 385   unsigned d_subs_unkCount;
 386 private:  //information about ground equivalence classes
 387   TNode d_bool_eqc[2];
 388   std::map< TNode, Node > d_ground_eqc_map;
 389   std::vector< TNode > d_ground_terms;
 390   //operator independent term index
 391   std::map< TNode, OpArgIndex > d_op_arg_index;
 392   //is handled term
 393   bool isHandledTerm( TNode n );
 394   Node getGroundEqc( TNode r );
 395   bool isGroundEqc( TNode r );
 396   bool isGroundTerm( TNode n );
 397   //has enumerated UF
 398   bool hasEnumeratedUf( Node n );
 399   // count of full effort checks
 400   unsigned d_fullEffortCount;
 401   // has added lemma
 402   bool d_hasAddedLemma;
 403   //flush the waiting conjectures
 404   unsigned flushWaitingConjectures( unsigned& addedLemmas, int ldepth, int rdepth );
 405 public:
 406   ConjectureGenerator( QuantifiersEngine * qe, context::Context* c );
 407   /* needs check */
 408   bool needsCheck( Theory::Effort e );
 409   /* reset at a round */
 410   void reset_round( Theory::Effort e );
 411   /* Call during quantifier engine's check */
 412   void check( Theory::Effort e, unsigned quant_e );
 413   /* Called for new quantifiers */
 414   void registerQuantifier( Node q );
 415   void assertNode( Node n );
 416   /** Identify this module (for debugging, dynamic configuration, etc..) */
 417   std::string identify() const { return "ConjectureGenerator"; }
 418 //options
 419 private:
 420   bool optReqDistinctVarPatterns();
 421   bool optFilterUnknown();
 422   int optFilterScoreThreshold();
 423   unsigned optFullCheckFrequency();
 424   unsigned optFullCheckConjectures();
 425
 426   bool optStatsOnly();
 427 };
 428
 429
 430 }
 431 }
 432 }
 433
 434 #endif