src/theory/quantifiers/quant_conflict_find.h

   1 /*********************                                                        */
   2 /*! \file quant_conflict_find.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Tim King, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing 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 <ostream>
  21 #include <vector>
  22
  23 #include "context/cdhashmap.h"
  24 #include "context/cdlist.h"
  25 #include "expr/node_trie.h"
  26 #include "theory/quantifiers/quant_util.h"
  27
  28 namespace CVC4 {
  29 namespace theory {
  30 namespace quantifiers {
  31
  32 class QuantConflictFind;
  33 class QuantInfo;
  34
  35 //match generator
  36 class MatchGen {
  37   friend class QuantInfo;
  38 private:
  39   //current children information
  40   int d_child_counter;
  41   bool d_use_children;
  42   //children of this object
  43   std::vector< int > d_children_order;
  44   unsigned getNumChildren() { return d_children.size(); }
  45   MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; }
  46   //MatchGen * getChild( int i ) { return &d_children[i]; }
  47   //current matching information
  48   std::vector<TNodeTrie*> d_qn;
  49   std::vector<std::map<TNode, TNodeTrie>::iterator> d_qni;
  50   bool doMatching( QuantConflictFind * p, QuantInfo * qi );
  51   //for matching : each index is either a variable or a ground term
  52   unsigned d_qni_size;
  53   std::map< int, int > d_qni_var_num;
  54   std::map< int, TNode > d_qni_gterm;
  55   std::map< int, int > d_qni_bound;
  56   std::vector< int > d_qni_bound_except;
  57   std::map< int, TNode > d_qni_bound_cons;
  58   std::map< int, int > d_qni_bound_cons_var;
  59   std::map< int, int >::iterator d_binding_it;
  60   //std::vector< int > d_independent;
  61   bool d_matched_basis;
  62   bool d_binding;
  63   //int getVarBindingVar();
  64   std::map< int, Node > d_ground_eval;
  65   //determine variable order
  66   void determineVariableOrder( QuantInfo * qi, std::vector< int >& bvars );
  67   void collectBoundVar( QuantInfo * qi, Node n, std::vector< int >& cbvars, std::map< Node, bool >& visited, bool& hasNested );
  68 public:
  69   //type of the match generator
  70   enum {
  71     typ_invalid,
  72     typ_ground,
  73     typ_pred,
  74     typ_eq,
  75     typ_formula,
  76     typ_var,
  77     typ_bool_var,
  78     typ_tconstraint,
  79     typ_tsym,
  80   };
  81   void debugPrintType( const char * c, short typ, bool isTrace = false );
  82 public:
  83   MatchGen();
  84   MatchGen( QuantInfo * qi, Node n, bool isVar = false );
  85   bool d_tgt;
  86   bool d_tgt_orig;
  87   bool d_wasSet;
  88   Node d_n;
  89   std::vector< MatchGen > d_children;
  90   short d_type;
  91   bool d_type_not;
  92   /** reset round
  93    *
  94    * Called once at the beginning of each full/last-call effort, prior to
  95    * processing this match generator. This method returns false if the reset
  96    * failed, e.g. if a conflict was encountered during term indexing.
  97    */
  98   bool reset_round(QuantConflictFind* p);
  99   void reset( QuantConflictFind * p, bool tgt, QuantInfo * qi );
 100   bool getNextMatch( QuantConflictFind * p, QuantInfo * qi );
 101   bool isValid() { return d_type!=typ_invalid; }
 102   void setInvalid();
 103
 104   // is this term treated as UF application?
 105   static bool isHandledBoolConnective( TNode n );
 106   static bool isHandledUfTerm( TNode n );
 107   static Node getMatchOperator( QuantConflictFind * p, Node n );
 108   //can this node be handled by the algorithm
 109   static bool isHandled( TNode n );
 110 };
 111
 112 //info for quantifiers
 113 class QuantInfo {
 114 private:
 115   void registerNode( Node n, bool hasPol, bool pol, bool beneathQuant = false );
 116   void flatten( Node n, bool beneathQuant );
 117 private: //for completing match
 118   std::vector< int > d_unassigned;
 119   std::vector< TypeNode > d_unassigned_tn;
 120   int d_unassigned_nvar;
 121   int d_una_index;
 122   std::vector< int > d_una_eqc_count;
 123   //optimization: track which arguments variables appear under UF terms in
 124   std::map< int, std::map< TNode, std::vector< unsigned > > > d_var_rel_dom;
 125   void getPropagateVars( QuantConflictFind * p, std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited );
 126   //optimization: number of variables set, to track when we can stop
 127   std::map< int, bool > d_vars_set;
 128   std::vector< Node > d_extra_var;
 129 public:
 130   bool isBaseMatchComplete();
 131 public:
 132   QuantInfo();
 133   ~QuantInfo();
 134   std::vector< TNode > d_vars;
 135   std::vector< TypeNode > d_var_types;
 136   std::map< TNode, int > d_var_num;
 137   std::vector< int > d_tsym_vars;
 138   std::map< TNode, bool > d_inMatchConstraint;
 139   int getVarNum( TNode v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; }
 140   bool isVar( TNode v ) { return d_var_num.find( v )!=d_var_num.end(); }
 141   int getNumVars() { return (int)d_vars.size(); }
 142   TNode getVar( int i ) { return d_vars[i]; }
 143
 144   typedef std::map< int, MatchGen * > VarMgMap;
 145  private:
 146   MatchGen * d_mg;
 147   VarMgMap d_var_mg;
 148  public:
 149   VarMgMap::const_iterator var_mg_find(int i) const { return d_var_mg.find(i); }
 150   VarMgMap::const_iterator var_mg_end() const { return d_var_mg.end(); }
 151   bool containsVarMg(int i) const { return var_mg_find(i) != var_mg_end(); }
 152
 153   bool matchGeneratorIsValid() const { return d_mg->isValid(); }
 154   bool getNextMatch( QuantConflictFind * p ) {
 155     return d_mg->getNextMatch(p, this);
 156   }
 157
 158   Node d_q;
 159   bool reset_round( QuantConflictFind * p );
 160 public:
 161   //initialize
 162   void initialize( QuantConflictFind * p, Node q, Node qn );
 163   //current constraints
 164   std::vector< TNode > d_match;
 165   std::vector< TNode > d_match_term;
 166   std::map< int, std::map< TNode, int > > d_curr_var_deq;
 167   std::map< Node, bool > d_tconstraints;
 168   int getCurrentRepVar( int v );
 169   TNode getCurrentValue( TNode n );
 170   TNode getCurrentExpValue( TNode n );
 171   bool getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, bool chDiseq = false );
 172   int addConstraint( QuantConflictFind * p, int v, TNode n, bool polarity );
 173   int addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove );
 174   bool setMatch( QuantConflictFind * p, int v, TNode n, bool isGroundRep, bool isGround );
 175   void unsetMatch( QuantConflictFind * p, int v );
 176   bool isMatchSpurious( QuantConflictFind * p );
 177   bool isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms );
 178   bool entailmentTest( QuantConflictFind * p, Node lit, bool chEnt = true );
 179   bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue = false );
 180   void revertMatch( QuantConflictFind * p, std::vector< int >& assigned );
 181   void debugPrintMatch( const char * c );
 182   bool isConstrainedVar( int v );
 183 public:
 184   void getMatch( std::vector< Node >& terms );
 185 };
 186
 187 class QuantConflictFind : public QuantifiersModule
 188 {
 189   friend class MatchGen;
 190   friend class QuantInfo;
 191   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
 192 private:
 193   context::CDO< bool > d_conflict;
 194   std::map< Kind, Node > d_zero;
 195   //for storing nodes created during t-constraint solving (prevents memory leaks)
 196   std::vector< Node > d_tempCache;
 197   //optimization: list of quantifiers that depend on ground function applications
 198   std::map< TNode, std::vector< Node > > d_func_rel_dom;
 199   std::map< TNode, bool > d_irr_func;
 200   std::map< Node, bool > d_irr_quant;
 201   void setIrrelevantFunction( TNode f );
 202 private:
 203   std::map< Node, Node > d_op_node;
 204   std::map< Node, int > d_fid;
 205 public:  //for ground terms
 206   Node d_true;
 207   Node d_false;
 208   TNode getZero( Kind k );
 209 private:
 210   std::map< Node, QuantInfo > d_qinfo;
 211 private:  //for equivalence classes
 212   // type -> list(eqc)
 213   std::map< TypeNode, std::vector< TNode > > d_eqcs;
 214
 215  public:
 216   enum Effort : unsigned {
 217     EFFORT_CONFLICT,
 218     EFFORT_PROP_EQ,
 219     EFFORT_INVALID,
 220   };
 221   void setEffort(Effort e) { d_effort = e; }
 222
 223   inline bool atConflictEffort() const {
 224     return d_effort == QuantConflictFind::EFFORT_CONFLICT;
 225   }
 226
 227  private:
 228   Effort d_effort;
 229
 230  public:
 231   bool areMatchEqual( TNode n1, TNode n2 );
 232   bool areMatchDisequal( TNode n1, TNode n2 );
 233
 234  public:
 235   QuantConflictFind(QuantifiersEngine* qe,
 236                     QuantifiersState& qs,
 237                     QuantifiersInferenceManager& qim,
 238                     QuantifiersRegistry& qr);
 239
 240   /** register quantifier */
 241   void registerQuantifier(Node q) override;
 242
 243  public:
 244   /** needs check */
 245   bool needsCheck(Theory::Effort level) override;
 246   /** reset round */
 247   void reset_round(Theory::Effort level) override;
 248   /** check
 249    *
 250    * This method attempts to construct a conflicting or propagating instance.
 251    * If such an instance exists, then it makes a call to
 252    * Instantiation::addInstantiation.
 253    */
 254   void check(Theory::Effort level, QEffort quant_e) override;
 255
 256  private:
 257   /** check quantified formula
 258    *
 259    * This method is called by the above check method for each quantified
 260    * formula q. It attempts to find a conflicting or propagating instance for
 261    * q, depending on the effort level (d_effort).
 262    *
 263    * isConflict: this is set to true if we discovered a conflicting instance.
 264    * This flag may be set instead of d_conflict if --qcf-all-conflict is true,
 265    * in which we continuing adding all conflicts.
 266    * addedLemmas: tracks the total number of lemmas added, and is incremented by
 267    * this method when applicable.
 268    */
 269   void checkQuantifiedFormula(Node q, bool& isConflict, unsigned& addedLemmas);
 270
 271  private:
 272   void debugPrint( const char * c );
 273   //for debugging
 274   std::vector< Node > d_quants;
 275   std::map< Node, int > d_quant_id;
 276   void debugPrintQuant( const char * c, Node q );
 277   void debugPrintQuantBody( const char * c, Node q, Node n, bool doVarNum = true );
 278 public:
 279   /** statistics class */
 280   class Statistics {
 281   public:
 282     IntStat d_inst_rounds;
 283     IntStat d_entailment_checks;
 284     Statistics();
 285     ~Statistics();
 286   };
 287   Statistics d_statistics;
 288   /** Identify this module */
 289   std::string identify() const override { return "QcfEngine"; }
 290   /** is n a propagating instance?
 291    *
 292    * A propagating instance is any formula that consists of Boolean connectives,
 293    * equality, quantified formulas, and terms that exist in the current
 294    * context (those in the master equality engine).
 295    *
 296    * Notice the distinction that quantified formulas that do not appear in the
 297    * current context are considered to be legal in propagating instances. This
 298    * choice is significant for TPTP, where a net of ~200 benchmarks are gained
 299    * due to this decision.
 300    *
 301    * Propagating instances are the second most useful kind of instantiation
 302    * after conflicting instances and are used as a second effort in the
 303    * algorithm performed by this class.
 304    */
 305   bool isPropagatingInstance(Node n) const;
 306 };
 307
 308 std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e);
 309
 310 } /* namespace CVC4::theory::quantifiers */
 311 } /* namespace CVC4::theory */
 312 } /* namespace CVC4 */
 313
 314 #endif