1 /*********************                                                        */
2 /*! \file theoryof_mode.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Dejan Jovanovic, Morgan Deters, Tim King
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 Option selection for theoryOf() operation
13  **
14  ** Option selection for theoryOf() operation.
15  **/
16 
17 #include "cvc4_public.h"
18 
19 #pragma once
20 
21 #include <ostream>
22 
23 namespace CVC4 {
24 namespace theory {
25 
26 /** How do we associate theories with the terms */
27 enum TheoryOfMode {
28   /** Equality, variables and constants are associated with the types */
29   THEORY_OF_TYPE_BASED,
30   /** Variables are uninterpreted, constants are with the type, equalities prefer parametric */
31   THEORY_OF_TERM_BASED
32 };/* enum TheoryOfMode */
33 
34 std::ostream& operator<<(std::ostream& out, TheoryOfMode m) CVC4_PUBLIC;
35 
36 }/* CVC4::theory namespace */
37 }/* CVC4 namespace */
38 
39