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