1 /******************************************************************************
2 * Top contributors (to current version):
3 * Tim King, Andrew Reynolds, Mathias Preiner
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 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.
11 * ****************************************************************************
13 * The representation of the assertions sent to theories.
16 #include "cvc5_private.h"
18 #ifndef CVC5__THEORY__ASSERTION_H
19 #define CVC5__THEORY__ASSERTION_H
21 #include "expr/node.h"
26 /** Information about an assertion for the theories. */
28 /** The assertion expression. */
29 const Node d_assertion
;
31 /** Has this assertion been preregistered with this theory. */
32 const bool d_isPreregistered
;
34 Assertion(TNode assertion
, bool isPreregistered
)
35 : d_assertion(assertion
), d_isPreregistered(isPreregistered
)
39 /** Convert the assertion to a TNode. */
40 operator TNode() const { return d_assertion
; }
42 /** Convert the assertion to a Node. */
43 operator Node() const { return d_assertion
; }
45 }; /* struct Assertion */
47 std::ostream
& operator<<(std::ostream
& out
, const Assertion
& a
);
52 #endif /* CVC5__THEORY__ASSERTION_H */