1 /********************* */
2 /*! \file relevant_domain.h
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
14 ** \brief relevant domain class
17 #include "cvc4_private.h"
19 #ifndef __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
20 #define __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H
22 #include "theory/quantifiers/first_order_model.h"
26 namespace quantifiers
{
31 FirstOrderModel
* d_model
;
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
);
42 RelevantDomain( FirstOrderModel
* m
);
43 virtual ~RelevantDomain(){}
44 //compute the relevant domain
46 //relevant instantiation domain for each quantifier
47 std::map
< Node
, std::vector
< RepDomain
> > d_quant_inst_domain
;
48 };/* class RelevantDomain */
50 }/* CVC4::theory::quantifiers namespace */
51 }/* CVC4::theory namespace */
54 #endif /* __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */