cvc4-1.4
Main Page
Related Pages
Namespaces
Data Structures
Files
File List
Globals
arith_unate_lemma_mode.h
Go to the documentation of this file.
1
/********************* */
18
#include "
cvc4_public.h
"
19
20
#ifndef __CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H
21
#define __CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H
22
23
#include <iostream>
24
25
namespace
CVC4
{
26
27
typedef
enum
{
28
NO_PRESOLVE_LEMMAS
,
29
INEQUALITY_PRESOLVE_LEMMAS
,
30
EQUALITY_PRESOLVE_LEMMAS
,
31
ALL_PRESOLVE_LEMMAS
32
}
ArithUnateLemmaMode
;
33
34
std::ostream&
operator<<
(std::ostream&
out
, ArithUnateLemmaMode rule)
CVC4_PUBLIC
;
35
36
}
/* CVC4 namespace */
37
38
#endif
/* __CVC4__THEORY__ARITH__ARITH_UNATE_LEMMA_MODE_H */
CVC4
Definition:
expr_manager.h:100
CVC4::ArithUnateLemmaMode
ArithUnateLemmaMode
Definition:
arith_unate_lemma_mode.h:27
CVC4::INEQUALITY_PRESOLVE_LEMMAS
Definition:
arith_unate_lemma_mode.h:29
CVC4::EQUALITY_PRESOLVE_LEMMAS
Definition:
arith_unate_lemma_mode.h:30
CVC4_PUBLIC
#define CVC4_PUBLIC
Definition:
cvc4_public.h:30
CVC4::operator<<
std::ostream & operator<<(std::ostream &out, TypeConstant typeConstant)
Definition:
kind.h:568
cvc4_public.h
Macros that should be defined everywhere during the building of the libraries and driver binary...
CVC4::NO_PRESOLVE_LEMMAS
Definition:
arith_unate_lemma_mode.h:28
CVC4::options::out
struct CVC4::options::out__option_t out
CVC4::ALL_PRESOLVE_LEMMAS
Definition:
arith_unate_lemma_mode.h:31
src
theory
arith
arith_unate_lemma_mode.h
Generated by
1.8.11