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