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