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