src/theory/assertion.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Tim King, Andrew Reynolds, Mathias Preiner
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   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  * ****************************************************************************
  12  *
  13  * The representation of the assertions sent to theories.
  14  */
  15
  16 #include "cvc5_private.h"
  17
  18 #ifndef CVC5__THEORY__ASSERTION_H
  19 #define CVC5__THEORY__ASSERTION_H
  20
  21 #include "expr/node.h"
  22
  23 namespace cvc5 {
  24 namespace theory {
  25
  26 /** Information about an assertion for the theories. */
  27 struct Assertion {
  28   /** The assertion expression. */
  29   const Node d_assertion;
  30
  31   /** Has this assertion been preregistered with this theory. */
  32   const bool d_isPreregistered;
  33
  34   Assertion(TNode assertion, bool isPreregistered)
  35       : d_assertion(assertion), d_isPreregistered(isPreregistered)
  36   {
  37   }
  38
  39   /** Convert the assertion to a TNode. */
  40   operator TNode() const { return d_assertion; }
  41
  42   /** Convert the assertion to a Node. */
  43   operator Node() const { return d_assertion; }
  44
  45 }; /* struct Assertion */
  46
  47 std::ostream& operator<<(std::ostream& out, const Assertion& a);
  48
  49 }  // namespace theory
  50 }  // namespace cvc5
  51
  52 #endif /* CVC5__THEORY__ASSERTION_H */