src/theory/quantifiers/inst_match.h

   1 /*********************                                                        */
   2 /*! \file inst_match.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Francois Bobot
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 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 inst match class
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
  18 #define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H
  19
  20 #include <vector>
  21
  22 #include "expr/node.h"
  23
  24 namespace CVC4 {
  25 namespace theory {
  26
  27 class EqualityQuery;
  28
  29 namespace inst {
  30
  31 /** Inst match
  32  *
  33  * This is the basic class specifying an instantiation. Its domain size (the
  34  * size of d_vals) is the number of bound variables of the quantified formula
  35  * that is passed to its constructor.
  36  *
  37  * The values of d_vals may be null, which indicate that the field has
  38  * yet to be initialized.
  39  */
  40 class InstMatch {
  41 public:
  42   InstMatch(){}
  43   explicit InstMatch(TNode q);
  44   InstMatch( InstMatch* m );
  45   /* map from variable to ground terms */
  46   std::vector<Node> d_vals;
  47   /** add match m
  48    *
  49    * This adds the initialized fields of m to this match for each field that is
  50    * not already initialized in this match.
  51    */
  52   void add(InstMatch& m);
  53   /** merge with match m
  54    *
  55    * This method returns true if the merge was successful, that is, all jointly
  56    * initialized fields of this class and m are equivalent modulo the equalities
  57    * given by q.
  58    */
  59   bool merge( EqualityQuery* q, InstMatch& m );
  60   /** is this complete, i.e. are all fields non-null? */
  61   bool isComplete();
  62   /** is this empty, i.e. are all fields the null node? */
  63   bool empty();
  64   /** clear the instantiation, i.e. set all fields to the null node */
  65   void clear();
  66   /** debug print method */
  67   void debugPrint(const char* c);
  68   /** to stream */
  69   inline void toStream(std::ostream& out) const {
  70     out << "INST_MATCH( ";
  71     bool printed = false;
  72     for( unsigned i=0; i<d_vals.size(); i++ ){
  73       if( !d_vals[i].isNull() ){
  74         if( printed ){ out << ", "; }
  75         out << i << " -> " << d_vals[i];
  76         printed = true;
  77       }
  78     }
  79     out << " )";
  80   }
  81   /** get the i^th term in the instantiation */
  82   Node get(int i) const;
  83   /** append the terms of this instantiation to inst */
  84   void getInst(std::vector<Node>& inst) const;
  85   /** set/overwrites the i^th field in the instantiation with n */
  86   void setValue( int i, TNode n );
  87   /** set the i^th term in the instantiation to n
  88    *
  89    * This method returns true if the i^th field was previously uninitialized,
  90    * or is equivalent to n modulo the equalities given by q.
  91    */
  92   bool set(EqualityQuery* q, int i, TNode n);
  93 };
  94
  95 inline std::ostream& operator<<(std::ostream& out, const InstMatch& m) {
  96   m.toStream(out);
  97   return out;
  98 }
  99
 100 }/* CVC4::theory::inst namespace */
 101
 102 typedef CVC4::theory::inst::InstMatch InstMatch;
 103
 104 }/* CVC4::theory namespace */
 105 }/* CVC4 namespace */
 106
 107 #endif /* __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */