cvc4-1.4
simplification_mode.h
Go to the documentation of this file.
1 /********************* */
18 #include "cvc4_public.h"
19 
20 #ifndef __CVC4__SMT__SIMPLIFICATION_MODE_H
21 #define __CVC4__SMT__SIMPLIFICATION_MODE_H
22 
23 #include <iostream>
24 
25 namespace CVC4 {
26 
28 typedef enum {
36 
37 std::ostream& operator<<(std::ostream& out, SimplificationMode mode) CVC4_PUBLIC;
38 
39 }/* CVC4 namespace */
40 
41 #endif /* __CVC4__SMT__SIMPLIFICATION_MODE_H */
Definition: options.h:76
Simplify the assertions all together once a check is requested.
SimplificationMode
Enumeration of simplification modes (when to simplify).
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
Don't do simplification.
Macros that should be defined everywhere during the building of the libraries and driver binary...
std::ostream & operator<<(std::ostream &out, ModelFormatMode mode)
struct CVC4::options::out__option_t out
Simplify the assertions as they come in.