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-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 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 #include "theory/quantifiers/term_database.h"
  24
  25 namespace CVC4 {
  26 namespace theory {
  27 namespace quantifiers {
  28
  29 class QuantConflictFind;
  30 class QuantInfo;
  31
  32 //match generator
  33 class MatchGen {
  34   friend class QuantInfo;
  35 private:
  36   //current children information
  37   int d_child_counter;
  38   //children of this object
  39   std::vector< int > d_children_order;
  40   unsigned getNumChildren() { return d_children.size(); }
  41   MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; }
  42   //MatchGen * getChild( int i ) { return &d_children[i]; }
  43   //current matching information
  44   std::vector< TermArgTrie * > d_qn;
  45   std::vector< std::map< TNode, TermArgTrie >::iterator > d_qni;
  46   bool doMatching( QuantConflictFind * p, QuantInfo * qi );
  47   //for matching : each index is either a variable or a ground term
  48   unsigned d_qni_size;
  49   std::map< int, int > d_qni_var_num;
  50   std::map< int, TNode > d_qni_gterm;
  51   std::map< int, TNode > d_qni_gterm_rep;
  52   std::map< int, int > d_qni_bound;
  53   std::vector< int > d_qni_bound_except;
  54   std::map< int, TNode > d_qni_bound_cons;
  55   std::map< int, int > d_qni_bound_cons_var;
  56   std::map< int, int >::iterator d_binding_it;
  57   //std::vector< int > d_independent;
  58   bool d_matched_basis;
  59   bool d_binding;
  60   //int getVarBindingVar();
  61   std::map< int, Node > d_ground_eval;
  62   //determine variable order
  63   void determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars );
  64   void collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars );
  65 public:
  66   //type of the match generator
  67   enum {
  68     typ_invalid,
  69     typ_ground,
  70     typ_pred,
  71     typ_eq,
  72     typ_formula,
  73     typ_var,
  74     typ_ite_var,
  75     typ_bool_var,
  76     typ_tconstraint,
  77     typ_tsym,
  78   };
  79   void debugPrintType( const char * c, short typ, bool isTrace = false );
  80 public:
  81   MatchGen() : d_type( typ_invalid ){}
  82   MatchGen( QuantInfo * qi, Node n, bool isVar = false );
  83   bool d_tgt;
  84   bool d_tgt_orig;
  85   bool d_wasSet;
  86   Node d_n;
  87   std::vector< MatchGen > d_children;
  88   short d_type;
  89   bool d_type_not;
  90   void reset_round( QuantConflictFind * p );
  91   void reset( QuantConflictFind * p, bool tgt, QuantInfo * qi );
  92   bool getNextMatch( QuantConflictFind * p, QuantInfo * qi );
  93   bool getExplanation( QuantConflictFind * p, QuantInfo * qi, std::vector< Node >& exp );
  94   Node getExplanationTerm( QuantConflictFind * p, QuantInfo * qi, Node t, std::vector< Node >& exp );
  95   bool isValid() { return d_type!=typ_invalid; }
  96   void setInvalid();
  97
  98   // is this term treated as UF application?
  99   static bool isHandledBoolConnective( TNode n );
 100   static bool isHandledUfTerm( TNode n );
 101   static Node getOperator( QuantConflictFind * p, Node n );
 102   //can this node be handled by the algorithm
 103   static bool isHandled( TNode n );
 104 };
 105
 106 //info for quantifiers
 107 class QuantInfo {
 108 private:
 109   void registerNode( Node n, bool hasPol, bool pol, bool beneathQuant = false );
 110   void flatten( Node n, bool beneathQuant );
 111 private: //for completing match
 112   std::vector< int > d_unassigned;
 113   std::vector< TypeNode > d_unassigned_tn;
 114   int d_unassigned_nvar;
 115   int d_una_index;
 116   std::vector< int > d_una_eqc_count;
 117 public:
 118   QuantInfo() : d_mg( NULL ) {}
 119   ~QuantInfo() { delete d_mg; }
 120   std::vector< TNode > d_vars;
 121   std::map< TNode, int > d_var_num;
 122   std::vector< int > d_tsym_vars;
 123   std::map< TNode, bool > d_inMatchConstraint;
 124   std::map< int, std::vector< Node > > d_var_constraint[2];
 125   int getVarNum( TNode v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; }
 126   bool isVar( TNode v ) { return d_var_num.find( v )!=d_var_num.end(); }
 127   int getNumVars() { return (int)d_vars.size(); }
 128   TNode getVar( int i ) { return d_vars[i]; }
 129
 130   MatchGen * d_mg;
 131   Node d_q;
 132   std::map< int, MatchGen * > d_var_mg;
 133   void reset_round( QuantConflictFind * p );
 134 public:
 135   //initialize
 136   void initialize( Node q, Node qn );
 137   //current constraints
 138   std::vector< TNode > d_match;
 139   std::vector< TNode > d_match_term;
 140   std::map< int, std::map< TNode, int > > d_curr_var_deq;
 141   std::map< Node, bool > d_tconstraints;
 142   int getCurrentRepVar( int v );
 143   TNode getCurrentValue( TNode n );
 144   TNode getCurrentExpValue( TNode n );
 145   bool getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq = false );
 146   int addConstraint( QuantConflictFind * p, int v, TNode n, bool polarity );
 147   int addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove );
 148   bool setMatch( QuantConflictFind * p, int v, TNode n );
 149   bool isMatchSpurious( QuantConflictFind * p );
 150   bool isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms );
 151   bool entailmentTest( QuantConflictFind * p, Node lit, bool chEnt = true );
 152   bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue = false );
 153   void revertMatch( std::vector< int >& assigned );
 154   void debugPrintMatch( const char * c );
 155   bool isConstrainedVar( int v );
 156 public:
 157   void getMatch( std::vector< Node >& terms );
 158 };
 159
 160 class QuantConflictFind : public QuantifiersModule
 161 {
 162   friend class MatchGen;
 163   friend class QuantInfo;
 164   typedef context::CDChunkList<Node> NodeList;
 165   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
 166 private:
 167   context::Context* d_c;
 168   context::CDO< bool > d_conflict;
 169   std::vector< Node > d_quant_order;
 170   std::map< Kind, Node > d_zero;
 171   //for storing nodes created during t-constraint solving (prevents memory leaks)
 172   std::vector< Node > d_tempCache;
 173 private:
 174   std::map< Node, Node > d_op_node;
 175   int d_fid_count;
 176   std::map< Node, int > d_fid;
 177   Node mkEqNode( Node a, Node b );
 178 public:  //for ground terms
 179   Node d_true;
 180   Node d_false;
 181   TNode getZero( Kind k );
 182 private:
 183   Node evaluateTerm( Node n );
 184   int evaluate( Node n, bool pref = false, bool hasPref = false );
 185 private:
 186   //currently asserted quantifiers
 187   NodeList d_qassert;
 188   std::map< Node, QuantInfo > d_qinfo;
 189 private:  //for equivalence classes
 190   eq::EqualityEngine * getEqualityEngine();
 191   bool areDisequal( Node n1, Node n2 );
 192   bool areEqual( Node n1, Node n2 );
 193   Node getRepresentative( Node n );
 194   TermDb* getTermDatabase();
 195   // type -> list(eqc)
 196   std::map< TypeNode, std::vector< TNode > > d_eqcs;
 197   std::map< TypeNode, Node > d_model_basis;
 198 public:
 199   enum {
 200     effort_conflict,
 201     effort_prop_eq,
 202     effort_mc,
 203   };
 204   short d_effort;
 205   void setEffort( int e ) { d_effort = e; }
 206   static short getMaxQcfEffort();
 207   bool areMatchEqual( TNode n1, TNode n2 );
 208   bool areMatchDisequal( TNode n1, TNode n2 );
 209 public:
 210   QuantConflictFind( QuantifiersEngine * qe, context::Context* c );
 211   /** register quantifier */
 212   void registerQuantifier( Node q );
 213 public:
 214   /** assert quantifier */
 215   void assertNode( Node q );
 216   /** new node */
 217   void newEqClass( Node n );
 218   /** merge */
 219   void merge( Node a, Node b );
 220   /** assert disequal */
 221   void assertDisequal( Node a, Node b );
 222   /** needs check */
 223   bool needsCheck( Theory::Effort level );
 224   /** reset round */
 225   void reset_round( Theory::Effort level );
 226   /** check */
 227   void check( Theory::Effort level, unsigned quant_e );
 228 private:
 229   bool d_needs_computeRelEqr;
 230 public:
 231   void computeRelevantEqr();
 232 private:
 233   void debugPrint( const char * c );
 234   //for debugging
 235   std::vector< Node > d_quants;
 236   std::map< Node, int > d_quant_id;
 237   void debugPrintQuant( const char * c, Node q );
 238   void debugPrintQuantBody( const char * c, Node q, Node n, bool doVarNum = true );
 239 public:
 240   /** statistics class */
 241   class Statistics {
 242   public:
 243     IntStat d_inst_rounds;
 244     IntStat d_conflict_inst;
 245     IntStat d_prop_inst;
 246     IntStat d_entailment_checks;
 247     Statistics();
 248     ~Statistics();
 249   };
 250   Statistics d_statistics;
 251   /** Identify this module */
 252   std::string identify() const { return "QcfEngine"; }
 253 };
 254
 255 }
 256 }
 257 }
 258
 259 #endif