src/theory/quantifiers/conjecture_generator.h

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