src/theory/quantifiers/relevant_domain.h

   1 /*********************                                                        */
   2 /*! \file relevant_domain.h
   3  ** \verbatim
   4  ** Original author: ajreynol
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief relevant domain class
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
  20 #define __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
  21
  22 #include "theory/quantifiers/first_order_model.h"
  23
  24 namespace CVC4 {
  25 namespace theory {
  26 namespace quantifiers {
  27
  28 class RelevantDomain
  29 {
  30 private:
  31   FirstOrderModel* d_model;
  32
  33   //the domain of the arguments for each operator
  34   std::map< Node, std::map< int, RepDomain > > d_active_domain;
  35   //the range for each operator
  36   std::map< Node, RepDomain > d_active_range;
  37   //for computing relevant instantiation domain, return true if changed
  38   bool computeRelevantInstantiationDomain( Node n, Node parent, int arg, std::vector< RepDomain >& rd );
  39   //for computing extended
  40   bool extendFunctionDomains( Node n, RepDomain& range );
  41 public:
  42   RelevantDomain( FirstOrderModel* m );
  43   virtual ~RelevantDomain(){}
  44   //compute the relevant domain
  45   void compute();
  46   //relevant instantiation domain for each quantifier
  47   std::map< Node, std::vector< RepDomain > > d_quant_inst_domain;
  48 };/* class RelevantDomain */
  49
  50 }/* CVC4::theory::quantifiers namespace */
  51 }/* CVC4::theory namespace */
  52 }/* CVC4 namespace */
  53
  54 #endif /* __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */