cvc4-1.3
type.h
Go to the documentation of this file.
1 /********************* */
17 #include "cvc4_public.h"
18 
19 #ifndef __CVC4__TYPE_H
20 #define __CVC4__TYPE_H
21 
22 #include <string>
23 #include <vector>
24 #include <limits.h>
25 #include <stdint.h>
26 
27 #include "util/cardinality.h"
28 #include "util/subrange_bound.h"
29 
30 namespace CVC4 {
31 
32 class NodeManager;
34 class CVC4_PUBLIC Expr;
35 class TypeNode;
36 struct CVC4_PUBLIC ExprManagerMapCollection;
37 
38 class CVC4_PUBLIC SmtEngine;
39 
40 class CVC4_PUBLIC Datatype;
41 class CVC4_PUBLIC Record;
42 
43 template <bool ref_count>
44 class NodeTemplate;
45 
46 class BooleanType;
47 class IntegerType;
48 class RealType;
49 class StringType;
50 class BitVectorType;
51 class ArrayType;
52 class DatatypeType;
53 class ConstructorType;
54 class SelectorType;
55 class TesterType;
56 class FunctionType;
57 class TupleType;
58 class RecordType;
59 class SExprType;
60 class SortType;
61 class SortConstructorType;
62 // not in release 1.0
63 //class PredicateSubtype;
64 class SubrangeType;
65 class Type;
66 
70  size_t operator()(const CVC4::Type& t) const;
71 };/* struct TypeHashFunction */
72 
79 std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC;
80 
81 namespace expr {
82  TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* nm, ExprManagerMapCollection& vmap);
83 }/* CVC4::expr namespace */
84 
89 
90  friend class SmtEngine;
91  friend class ExprManager;
92  friend class NodeManager;
93  friend class TypeNode;
94  friend std::ostream& CVC4::operator<<(std::ostream& out, const Type& t);
95  friend TypeNode expr::exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* nm, ExprManagerMapCollection& vmap);
96 
97 protected:
98 
100  TypeNode* d_typeNode;
101 
103  NodeManager* d_nodeManager;
104 
110  Type makeType(const TypeNode& typeNode) const;
111 
117  Type(NodeManager* em, TypeNode* typeNode);
118 
120  static TypeNode* getTypeNode(const Type& t) throw() { return t.d_typeNode; }
121 
122 public:
123 
125  virtual ~Type();
126 
128  Type();
129 
134  Type(const Type& t);
135 
140  bool isNull() const;
141 
145  Cardinality getCardinality() const;
146 
150  bool isWellFounded() const;
151 
156  Expr mkGroundTerm() const;
157 
161  bool isSubtypeOf(Type t) const;
162 
167  bool isComparableTo(Type t) const;
168 
172  Type getBaseType() const;
173 
177  Type substitute(const Type& type, const Type& replacement) const;
178 
182  Type substitute(const std::vector<Type>& types,
183  const std::vector<Type>& replacements) const;
184 
188  ExprManager* getExprManager() const;
189 
193  Type exportTo(ExprManager* exprManager, ExprManagerMapCollection& vmap) const;
194 
200  Type& operator=(const Type& t);
201 
207  bool operator==(const Type& t) const;
208 
214  bool operator!=(const Type& t) const;
215 
219  bool operator<(const Type& t) const;
220 
224  bool operator<=(const Type& t) const;
225 
229  bool operator>(const Type& t) const;
230 
234  bool operator>=(const Type& t) const;
235 
240  bool isBoolean() const;
241 
246  bool isInteger() const;
247 
252  bool isReal() const;
253 
258  bool isString() const;
259 
264  bool isBitVector() const;
265 
270  bool isFunction() const;
271 
277  bool isPredicate() const;
278 
283  bool isTuple() const;
284 
289  bool isRecord() const;
290 
295  bool isSExpr() const;
296 
301  bool isArray() const;
302 
307  bool isDatatype() const;
308 
313  bool isConstructor() const;
314 
319  bool isSelector() const;
320 
325  bool isTester() const;
326 
331  bool isSort() const;
332 
337  bool isSortConstructor() const;
338 
343  // not in release 1.0
344  //bool isPredicateSubtype() const;
345 
350  bool isSubrange() const;
351 
356  void toStream(std::ostream& out) const;
357 
361  std::string toString() const;
362 };/* class Type */
363 
367 class CVC4_PUBLIC BooleanType : public Type {
368 
369 public:
370 
372  BooleanType(const Type& type = Type()) throw(IllegalArgumentException);
373 };/* class BooleanType */
374 
378 class CVC4_PUBLIC IntegerType : public Type {
379 
380 public:
381 
383  IntegerType(const Type& type = Type()) throw(IllegalArgumentException);
384 };/* class IntegerType */
385 
389 class CVC4_PUBLIC RealType : public Type {
390 
391 public:
392 
394  RealType(const Type& type = Type()) throw(IllegalArgumentException);
395 };/* class RealType */
396 
400 class CVC4_PUBLIC StringType : public Type {
401 
402 public:
403 
405  StringType(const Type& type) throw(IllegalArgumentException);
406 };/* class StringType */
407 
411 class CVC4_PUBLIC FunctionType : public Type {
412 
413 public:
414 
416  FunctionType(const Type& type = Type()) throw(IllegalArgumentException);
417 
419  size_t getArity() const;
420 
422  std::vector<Type> getArgTypes() const;
423 
425  Type getRangeType() const;
426 };/* class FunctionType */
427 
431 class CVC4_PUBLIC TupleType : public Type {
432 
433 public:
434 
436  TupleType(const Type& type = Type()) throw(IllegalArgumentException);
437 
439  size_t getLength() const;
440 
442  std::vector<Type> getTypes() const;
443 
444 };/* class TupleType */
445 
449 class CVC4_PUBLIC RecordType : public Type {
450 
451 public:
452 
454  RecordType(const Type& type = Type()) throw(IllegalArgumentException);
455 
457  const Record& getRecord() const;
458 };/* class RecordType */
459 
463 class CVC4_PUBLIC SExprType : public Type {
464 
465 public:
466 
468  SExprType(const Type& type = Type()) throw(IllegalArgumentException);
469 
471  std::vector<Type> getTypes() const;
472 };/* class SExprType */
473 
477 class CVC4_PUBLIC ArrayType : public Type {
478 
479 public:
480 
482  ArrayType(const Type& type = Type()) throw(IllegalArgumentException);
483 
485  Type getIndexType() const;
486 
488  Type getConstituentType() const;
489 };/* class ArrayType */
490 
494 class CVC4_PUBLIC SortType : public Type {
495 
496 public:
497 
499  SortType(const Type& type = Type()) throw(IllegalArgumentException);
500 
502  std::string getName() const;
503 
505  bool isParameterized() const;
506 
508  std::vector<Type> getParamTypes() const;
509 
510 };/* class SortType */
511 
516 
517 public:
518 
520  SortConstructorType(const Type& type = Type()) throw(IllegalArgumentException);
521 
523  std::string getName() const;
524 
526  size_t getArity() const;
527 
529  SortType instantiate(const std::vector<Type>& params) const;
530 
531 };/* class SortConstructorType */
532 
533 // not in release 1.0
534 #if 0
535 
538 class CVC4_PUBLIC PredicateSubtype : public Type {
539 
540 public:
541 
543  PredicateSubtype(const Type& type = Type()) throw(IllegalArgumentException);
544 
546  Expr getPredicate() const;
547 
552  Type getParentType() const;
553 
554 };/* class PredicateSubtype */
555 #endif /* 0 */
556 
560 class CVC4_PUBLIC SubrangeType : public Type {
561 
562 public:
563 
565  SubrangeType(const Type& type = Type()) throw(IllegalArgumentException);
566 
568  SubrangeBounds getSubrangeBounds() const;
569 
570 };/* class SubrangeType */
571 
576 
577 public:
578 
580  BitVectorType(const Type& type = Type()) throw(IllegalArgumentException);
581 
586  unsigned getSize() const;
587 
588 };/* class BitVectorType */
589 
590 
594 class CVC4_PUBLIC DatatypeType : public Type {
595 
596 public:
597 
599  DatatypeType(const Type& type = Type()) throw(IllegalArgumentException);
600 
602  const Datatype& getDatatype() const;
603 
605  bool isParametric() const;
606 
611  Expr getConstructor(std::string name) const;
612 
619  bool isInstantiated() const;
620 
624  bool isParameterInstantiated(unsigned n) const;
625 
627  std::vector<Type> getParamTypes() const;
628 
630  size_t getArity() const;
631 
633  DatatypeType instantiate(const std::vector<Type>& params) const;
634 
635 };/* class DatatypeType */
636 
641 
642 public:
643 
645  ConstructorType(const Type& type = Type()) throw(IllegalArgumentException);
646 
648  DatatypeType getRangeType() const;
649 
651  std::vector<Type> getArgTypes() const;
652 
654  size_t getArity() const;
655 
656 };/* class ConstructorType */
657 
658 
662 class CVC4_PUBLIC SelectorType : public Type {
663 
664 public:
665 
667  SelectorType(const Type& type = Type()) throw(IllegalArgumentException);
668 
670  DatatypeType getDomain() const;
671 
673  Type getRangeType() const;
674 
675 };/* class SelectorType */
676 
680 class CVC4_PUBLIC TesterType : public Type {
681 
682 public:
683 
685  TesterType(const Type& type = Type()) throw(IllegalArgumentException);
686 
688  DatatypeType getDomain() const;
689 
694  BooleanType getRangeType() const;
695 
696 };/* class TesterType */
697 
698 }/* CVC4 namespace */
699 
700 #endif /* __CVC4__TYPE_H */
Singleton class encapsulating the real type.
Definition: type.h:389
Class encapsulating the Selector type.
Definition: type.h:662
void * Expr
Class encapsulating CVC4 expressions and methods for constructing new expressions.
Definition: expr.h:226
Singleton class encapsulating the integer type.
Definition: type.h:378
Class encapsulating a user-defined sort.
Definition: type.h:494
std::ostream & operator<<(std::ostream &os, const Integer &n)
void * ExprManager
Hash function for Types.
Definition: type.h:68
Class encapsulating a tuple type.
Definition: type.h:463
The representation of an inductive datatype.
Definition: datatype.h:382
A simple representation of a cardinality.
Definition: cardinality.h:65
Class encapsulating CVC4 expression types.
Definition: type.h:88
static TypeNode * getTypeNode(const Type &t)
Accessor for derived classes.
Definition: type.h:120
TypeNode * d_typeNode
The internal expression representation.
Definition: type.h:100
Class encapsulating the Tester type.
Definition: type.h:680
Singleton class encapsulating the Boolean type.
Definition: type.h:367
This is CVC4 release version For build and installation please see the INSTALL file included with this distribution This first official release of CVC4 is the result of more than three years of efforts by researchers at New York University and The University of Iowa The project leaders are Clark please refer to the AUTHORS file in the source distribution CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order CVC CVC3 but does not directly incorporate code from any previous version CVC4 is intended to be an open and extensible SMT engine It can be used as a stand alone tool or as a library It has been designed to increase the performance and reduce the memory overhead of its predecessors It is written entirely in C and is released under a free software see the INSTALL file that comes with this distribution We recommend that you visit our CVC4 tutorials online please write to the cvc users cs nyu edu mailing list *if you need to report a bug with CVC4
Definition: README:39
Representation of subrange bounds.
Representation of cardinality.
Class encapsulating an array type.
Definition: type.h:477
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
Class encapsulating a function type.
Definition: type.h:411
Class encapsulating a user-defined sort constructor.
Definition: type.h:515
Class encapsulating the datatype type.
Definition: type.h:594
Macros that should be defined everywhere during the building of the libraries and driver binary...
Class encapsulating a record type.
Definition: type.h:449
NodeManager * d_nodeManager
The responsible expression manager.
Definition: type.h:103
TypeNode exportTypeInternal(TypeNode n, NodeManager *from, NodeManager *nm, ExprManagerMapCollection &vmap)
Class encapsulating a tuple type.
Definition: type.h:431
Singleton class encapsulating the string type.
Definition: type.h:400
struct CVC4::options::out__option_t out
Class encapsulating an integer subrange type.
Definition: type.h:560
void * Type
Class encapsulating the constructor type.
Definition: type.h:640
Class encapsulating the bit-vector type.
Definition: type.h:575
bool operator!=(enum Result::Sat s, const Result &r)
bool operator==(enum Result::Sat s, const Result &r)