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-2019 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/instantiate.h"
  18 #include "theory/quantifiers/quant_util.h"
  19 #include "theory/quantifiers/term_database.h"
  20 #include "theory/quantifiers_engine.h"
  21
  22 namespace CVC4 {
  23 namespace theory {
  24 namespace inst {
  25
  26 InstMatch::InstMatch(TNode q)
  27 {
  28   d_vals.resize(q[0].getNumChildren());
  29   Assert(!d_vals.empty());
  30   // resize must initialize with null nodes
  31   Assert(d_vals[0].isNull());
  32 }
  33
  34 InstMatch::InstMatch( InstMatch* m ) {
  35   d_vals.insert( d_vals.end(), m->d_vals.begin(), m->d_vals.end() );
  36 }
  37
  38 void InstMatch::add(InstMatch& m)
  39 {
  40   for (unsigned i = 0, size = d_vals.size(); i < size; i++)
  41   {
  42     if( d_vals[i].isNull() ){
  43       d_vals[i] = m.d_vals[i];
  44     }
  45   }
  46 }
  47
  48 bool InstMatch::merge( EqualityQuery* q, InstMatch& m ){
  49   Assert(d_vals.size() == m.d_vals.size());
  50   for (unsigned i = 0, size = d_vals.size(); i < size; i++)
  51   {
  52     if( !m.d_vals[i].isNull() ){
  53       if( d_vals[i].isNull() ){
  54         d_vals[i] = m.d_vals[i];
  55       }else{
  56         if( !q->areEqual( d_vals[i], m.d_vals[i]) ){
  57           clear();
  58           return false;
  59         }
  60       }
  61     }
  62   }
  63   return true;
  64 }
  65
  66 void InstMatch::debugPrint( const char* c ){
  67   for (unsigned i = 0, size = d_vals.size(); i < size; i++)
  68   {
  69     if( !d_vals[i].isNull() ){
  70       Debug( c ) << "   " << i << " -> " << d_vals[i] << std::endl;
  71     }
  72   }
  73 }
  74
  75 bool InstMatch::isComplete() {
  76   for (Node& v : d_vals)
  77   {
  78     if (v.isNull())
  79     {
  80       return false;
  81     }
  82   }
  83   return true;
  84 }
  85
  86 bool InstMatch::empty() {
  87   for (Node& v : d_vals)
  88   {
  89     if (!v.isNull())
  90     {
  91       return false;
  92     }
  93   }
  94   return true;
  95 }
  96
  97 void InstMatch::clear() {
  98   for( unsigned i=0; i<d_vals.size(); i++ ){
  99     d_vals[i] = Node::null();
 100   }
 101 }
 102
 103 Node InstMatch::get(size_t i) const
 104 {
 105   Assert(i < d_vals.size());
 106   return d_vals[i];
 107 }
 108
 109 void InstMatch::setValue(size_t i, TNode n)
 110 {
 111   Assert(i < d_vals.size());
 112   d_vals[i] = n;
 113 }
 114 bool InstMatch::set(EqualityQuery* q, size_t i, TNode n)
 115 {
 116   Assert(i < d_vals.size());
 117   if( !d_vals[i].isNull() ){
 118     if (q->areEqual(d_vals[i], n))
 119     {
 120       return true;
 121     }else{
 122       return false;
 123     }
 124   }else{
 125     d_vals[i] = n;
 126     return true;
 127   }
 128 }
 129
 130 }/* CVC4::theory::inst namespace */
 131 }/* CVC4::theory namespace */
 132 }/* CVC4 namespace */