src/theory/quantifiers/quant_conflict_find.h

   1 /*********************                                                        */
   2 /*! \file quant_conflict_find.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-2013  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 quantifiers conflict find class
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef QUANT_CONFLICT_FIND
  18 #define QUANT_CONFLICT_FIND
  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 QcfNode;
  29
  30 class QuantConflictFind;
  31
  32 class QcfNodeIndex {
  33 public:
  34   std::map< Node, QcfNodeIndex > d_children;
  35   void clear() { d_children.clear(); }
  36   //Node existsTerm( QuantConflictFind * qcf, Node n, int index = 0 );
  37   //Node addTerm( QuantConflictFind * qcf, Node n, int index = 0 );
  38   //bool addTermEq( QuantConflictFind * qcf, Node n1, Node n2, int index = 0 );
  39   void debugPrint( const char * c, int t );
  40   //optimized versions
  41   Node existsTerm( Node n, std::vector< Node >& reps, int index = 0 );
  42   Node addTerm( Node n, std::vector< Node >& reps, int index = 0 );
  43   bool addTermEq( Node n1, Node n2, std::vector< Node >& reps1, std::vector< Node >& reps2, int index = 0 );
  44 };
  45
  46 class EqRegistry {
  47   typedef context::CDChunkList<Node> NodeList;
  48   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
  49 public:
  50   EqRegistry( context::Context* c );
  51   //active
  52   context::CDO< bool > d_active;
  53   //NodeIndex describing pairs that meet the criteria of the EqRegistry
  54   QcfNodeIndex d_qni;
  55
  56   //qcf nodes that this helps to 1:satisfy -1:falsify 0:both a quantifier conflict node
  57   //std::map< QcfNode *, int > d_qcf;
  58   //has eqc
  59   //bool hasEqc( Node n ) { return d_t_eqc.find( n )!=d_t_eqc.end() && d_t_eqc[n]; }
  60   //void setEqc( Node n, bool val = true ) { d_t_eqc[n] = val; }
  61   void clear() { d_qni.clear(); }
  62   void debugPrint( const char * c, int t );
  63 };
  64
  65 /*
  66 class QcfNode {
  67 public:
  68   QcfNode( context::Context* c );
  69   QcfNode * d_parent;
  70   std::map< int, QcfNode * > d_child;
  71   Node d_node;
  72   EqRegistry * d_reg[2];
  73 };
  74 */
  75
  76 class QuantConflictFind : public QuantifiersModule
  77 {
  78   friend class QcfNodeIndex;
  79   typedef context::CDChunkList<Node> NodeList;
  80   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
  81 private:
  82   context::Context* d_c;
  83   context::CDO< bool > d_conflict;
  84   bool d_performCheck;
  85   //void registerAssertion( Node n );
  86   void registerNode( Node q, Node n, bool hasPol, bool pol );
  87   void flatten( Node q, Node n );
  88 private:
  89   std::map< TypeNode, Node > d_fv;
  90   Node getFv( TypeNode tn );
  91   std::map< Node, Node > d_op_node;
  92   int getFunctionId( Node f );
  93   bool isLessThan( Node a, Node b );
  94   Node getFunction( Node n, bool isQuant = false );
  95   int d_fid_count;
  96   std::map< Node, int > d_fid;
  97   Node mkEqNode( Node a, Node b );
  98 private:  //for ground terms
  99   Node d_true;
 100   Node d_false;
 101   std::map< Node, std::map< Node, EqRegistry * > > d_eqr[2];
 102   EqRegistry * getEqRegistry( bool polarity, Node lit, bool doCreate = true );
 103   void getEqRegistryApps( Node lit, std::vector< Node >& terms );
 104   int evaluate( Node n );
 105 public:  //for quantifiers
 106   //match generator
 107   class MatchGen {
 108   private:
 109     //current children information
 110     int d_child_counter;
 111     //children of this object
 112     std::vector< int > d_children_order;
 113     unsigned getNumChildren() { return d_children.size(); }
 114     MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; }
 115     //current matching information
 116     std::vector< QcfNodeIndex * > d_qn;
 117     std::vector< std::map< Node, QcfNodeIndex >::iterator > d_qni;
 118     bool doMatching( QuantConflictFind * p, Node q );
 119     //for matching : each index is either a variable or a ground term
 120     unsigned d_qni_size;
 121     std::map< int, int > d_qni_var_num;
 122     std::map< int, Node > d_qni_gterm;
 123     std::map< int, Node > d_qni_gterm_rep;
 124     std::map< int, int > d_qni_bound;
 125     std::map< int, Node > d_qni_bound_cons;
 126   public:
 127     //type of the match generator
 128     enum {
 129       typ_invalid,
 130       typ_ground,
 131       typ_var_eq,
 132       typ_valid_lit,
 133       typ_valid,
 134       typ_var,
 135       typ_top,
 136     };
 137     void debugPrintType( const char * c, short typ, bool isTrace = false );
 138   public:
 139     MatchGen() : d_type( typ_invalid ){}
 140     MatchGen( QuantConflictFind * p, Node q, Node n, bool isTop = false, bool isVar = false );
 141     bool d_tgt;
 142     Node d_n;
 143     std::vector< MatchGen > d_children;
 144     short d_type;
 145     bool d_type_not;
 146     void reset_round( QuantConflictFind * p );
 147     void reset( QuantConflictFind * p, bool tgt, Node q );
 148     bool getNextMatch( QuantConflictFind * p, Node q );
 149     bool isValid() { return d_type!=typ_invalid; }
 150     void setInvalid();
 151   };
 152 private:
 153   //currently asserted quantifiers
 154   NodeList d_qassert;
 155   //info for quantifiers
 156   class QuantInfo {
 157   public:
 158     QuantInfo() : d_mg( NULL ) {}
 159     std::vector< Node > d_vars;
 160     std::map< Node, int > d_var_num;
 161     std::map< EqRegistry *, bool > d_rel_eqr;
 162     std::map< int, std::vector< Node > > d_var_constraint[2];
 163     int getVarNum( Node v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; }
 164     bool isVar( Node v ) { return d_var_num.find( v )!=d_var_num.end(); }
 165     int getNumVars() { return (int)d_vars.size(); }
 166     Node getVar( int i ) { return d_vars[i]; }
 167     MatchGen * d_mg;
 168     std::map< int, MatchGen * > d_var_mg;
 169     void reset_round( QuantConflictFind * p );
 170   public:
 171     //current constraints
 172     std::map< int, Node > d_match;
 173     std::map< int, std::map< Node, int > > d_curr_var_deq;
 174     int getCurrentRepVar( int v );
 175     Node getCurrentValue( Node n );
 176     bool getCurrentCanBeEqual( QuantConflictFind * p, int v, Node n );
 177     int addConstraint( QuantConflictFind * p, int v, Node n, bool polarity );
 178     int addConstraint( QuantConflictFind * p, int v, Node n, int vn, bool polarity, bool doRemove );
 179     bool setMatch( QuantConflictFind * p, int v, Node n );
 180     bool isMatchSpurious( QuantConflictFind * p );
 181     bool completeMatch( QuantConflictFind * p, Node q, std::vector< int >& assigned );
 182     void debugPrintMatch( const char * c );
 183   };
 184   std::map< Node, QuantInfo > d_qinfo;
 185 private:  //for equivalence classes
 186   eq::EqualityEngine * getEqualityEngine();
 187   bool areDisequal( Node n1, Node n2 );
 188   bool areEqual( Node n1, Node n2 );
 189   Node getRepresentative( Node n );
 190   Node getTerm( Node n );
 191
 192   class EqcInfo {
 193   public:
 194     EqcInfo( context::Context* c ) : d_diseq( c ) {}
 195     NodeBoolMap d_diseq;
 196     bool isDisequal( Node n ) { return d_diseq.find( n )!=d_diseq.end() && d_diseq[n]; }
 197     void setDisequal( Node n, bool val = true ) { d_diseq[n] = val; }
 198     //NodeBoolMap& getRelEqr( int index ) { return index==0 ? d_rel_eqr_e : d_rel_eqr_d; }
 199   };
 200   std::map< Node, EqcInfo * > d_eqc_info;
 201   EqcInfo * getEqcInfo( Node n, bool doCreate = true );
 202   // operator -> index(terms)
 203   std::map< Node, QcfNodeIndex > d_uf_terms;
 204   // eqc x operator -> index(terms)
 205   std::map< Node, std::map< Node, QcfNodeIndex > > d_eqc_uf_terms;
 206   // type -> list(eqc)
 207   std::map< TypeNode, std::vector< Node > > d_eqcs;
 208   //mapping from UF terms to representatives of their arguments
 209   std::map< Node, std::vector< Node > > d_arg_reps;
 210   //compute arg reps
 211   void computeArgReps( Node n );
 212 public:
 213   QuantConflictFind( QuantifiersEngine * qe, context::Context* c );
 214
 215   /** register assertions */
 216   //void registerAssertions( std::vector< Node >& assertions );
 217   /** register quantifier */
 218   void registerQuantifier( Node q );
 219
 220 public:
 221   /** assert quantifier */
 222   void assertNode( Node q );
 223   /** new node */
 224   void newEqClass( Node n );
 225   /** merge */
 226   void merge( Node a, Node b );
 227   /** assert disequal */
 228   void assertDisequal( Node a, Node b );
 229   /** check */
 230   void check( Theory::Effort level );
 231   /** needs check */
 232   bool needsCheck( Theory::Effort level );
 233 private:
 234   void computeRelevantEqr();
 235 private:
 236   void debugPrint( const char * c );
 237   //for debugging
 238   std::vector< Node > d_quants;
 239   std::map< Node, int > d_quant_id;
 240   void debugPrintQuant( const char * c, Node q );
 241   void debugPrintQuantBody( const char * c, Node q, Node n, bool doVarNum = true );
 242 public:
 243   /** statistics class */
 244   class Statistics {
 245   public:
 246     IntStat d_inst_rounds;
 247     IntStat d_conflict_inst;
 248     Statistics();
 249     ~Statistics();
 250   };
 251   Statistics d_statistics;
 252 };
 253
 254 }
 255 }
 256 }
 257
 258 #endif