1 /*********************                                                        */
2 /*! \file assertion.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Tim King, Dejan Jovanovic
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 The representation of the assertions sent to theories.
13  **
14  ** The representation of the assertions sent to theories.
15  **/
16 
17 
18 #include "cvc4_private.h"
19 
20 #ifndef __CVC4__THEORY__ASSERTION_H
21 #define __CVC4__THEORY__ASSERTION_H
22 
23 #include "expr/node.h"
24 
25 namespace CVC4 {
26 namespace theory {
27 
28 /** Information about an assertion for the theories. */
29 struct Assertion {
30   /** The assertion expression. */
31   const Node assertion;
32 
33   /** Has this assertion been preregistered with this theory. */
34   const bool isPreregistered;
35 
AssertionAssertion36   Assertion(TNode assertion, bool isPreregistered)
37       : assertion(assertion), isPreregistered(isPreregistered) {}
38 
39   /** Convert the assertion to a TNode. */
TNodeAssertion40   operator TNode() const { return assertion; }
41 
42   /** Convert the assertion to a Node. */
NodeAssertion43   operator Node() const { return assertion; }
44 
45 }; /* struct Assertion */
46 
47 std::ostream& operator<<(std::ostream& out, const Assertion& a);
48 
49 }/* CVC4::theory namespace */
50 }/* CVC4 namespace */
51 
52 #endif /* __CVC4__THEORY__ASSERTION_H */
53