src/theory/quantifiers/inst_match.cpp

   1 /*********************                                                        */
   2 /*! \file inst_match.cpp
   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-2021 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 Implementation of inst match class
  13  **/
  14
  15 #include "theory/quantifiers/inst_match.h"
  16
  17 #include "theory/quantifiers/quantifiers_state.h"
  18
  19 namespace CVC5 {
  20 namespace theory {
  21 namespace quantifiers {
  22
  23 InstMatch::InstMatch(TNode q)
  24 {
  25   d_vals.resize(q[0].getNumChildren());
  26   Assert(!d_vals.empty());
  27   // resize must initialize with null nodes
  28   Assert(d_vals[0].isNull());
  29 }
  30
  31 InstMatch::InstMatch( InstMatch* m ) {
  32   d_vals.insert( d_vals.end(), m->d_vals.begin(), m->d_vals.end() );
  33 }
  34
  35 void InstMatch::add(InstMatch& m)
  36 {
  37   for (unsigned i = 0, size = d_vals.size(); i < size; i++)
  38   {
  39     if( d_vals[i].isNull() ){
  40       d_vals[i] = m.d_vals[i];
  41     }
  42   }
  43 }
  44
  45 void InstMatch::debugPrint( const char* c ){
  46   for (unsigned i = 0, size = d_vals.size(); i < size; i++)
  47   {
  48     if( !d_vals[i].isNull() ){
  49       Debug( c ) << "   " << i << " -> " << d_vals[i] << std::endl;
  50     }
  51   }
  52 }
  53
  54 bool InstMatch::isComplete() {
  55   for (Node& v : d_vals)
  56   {
  57     if (v.isNull())
  58     {
  59       return false;
  60     }
  61   }
  62   return true;
  63 }
  64
  65 bool InstMatch::empty() {
  66   for (Node& v : d_vals)
  67   {
  68     if (!v.isNull())
  69     {
  70       return false;
  71     }
  72   }
  73   return true;
  74 }
  75
  76 void InstMatch::clear() {
  77   for( unsigned i=0; i<d_vals.size(); i++ ){
  78     d_vals[i] = Node::null();
  79   }
  80 }
  81
  82 Node InstMatch::get(size_t i) const
  83 {
  84   Assert(i < d_vals.size());
  85   return d_vals[i];
  86 }
  87
  88 void InstMatch::setValue(size_t i, TNode n)
  89 {
  90   Assert(i < d_vals.size());
  91   d_vals[i] = n;
  92 }
  93 bool InstMatch::set(QuantifiersState& qs, size_t i, TNode n)
  94 {
  95   Assert(i < d_vals.size());
  96   if( !d_vals[i].isNull() ){
  97     return qs.areEqual(d_vals[i], n);
  98   }
  99   d_vals[i] = n;
 100   return true;
 101 }
 102
 103 }  // namespace quantifiers
 104 }  // namespace theory
 105 }  // namespace CVC5