cvc4-1.4
predicate.h
Go to the documentation of this file.
1 /********************* */
19 #include "cvc4_public.h"
20 
21 #ifndef __CVC4__PREDICATE_H
22 #define __CVC4__PREDICATE_H
23 
24 #include "util/exception.h"
25 
26 namespace CVC4 {
27 
28 class Predicate;
29 
30 std::ostream& operator<<(std::ostream& out, const Predicate& p) CVC4_PUBLIC;
31 
32 struct CVC4_PUBLIC PredicateHashFunction {
33  size_t operator()(const Predicate& p) const;
34 };/* class PredicateHashFunction */
35 
36 }/* CVC4 namespace */
37 
38 #include "expr/expr.h"
39 
40 namespace CVC4 {
41 
43 
44  Expr d_predicate;
45  Expr d_witness;
46 
47 public:
48 
50 
51  operator Expr() const;
52 
53  bool operator==(const Predicate& p) const;
54 
55  friend std::ostream& CVC4::operator<<(std::ostream& out, const Predicate& p);
56  friend size_t PredicateHashFunction::operator()(const Predicate& p) const;
57 
58 };/* class Predicate */
59 
60 }/* CVC4 namespace */
61 
62 #endif /* __CVC4__PREDICATE_H */
void * Expr
Class encapsulating CVC4 expressions and methods for constructing new expressions.
Definition: expr.h:227
CVC4's exception base class and some associated utilities.
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
std::ostream & operator<<(std::ostream &out, TypeConstant typeConstant)
Definition: kind.h:568
Macros that should be defined everywhere during the building of the libraries and driver binary...
struct CVC4::options::out__option_t out
expr.h
bool operator==(enum Result::Sat s, const Result &r)
size_t operator()(const Predicate &p) const