cprover
smt_core_theory.h
Go to the documentation of this file.
1 // Author: Diffblue Ltd.
2 
3 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_CORE_THEORY_H
4 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_CORE_THEORY_H
5 
7 
9 {
10 public:
11  struct nott final
12  {
13  static const char *identifier();
14  static smt_sortt return_sort(const smt_termt &operand);
15  static void validate(const smt_termt &operand);
16  };
18 
19  struct impliest final
20  {
21  static const char *identifier();
22  static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
23  static void validate(const smt_termt &lhs, const smt_termt &rhs);
24  };
26 
27  struct andt final
28  {
29  static const char *identifier();
30  static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
31  static void validate(const smt_termt &lhs, const smt_termt &rhs);
32  };
34 
35  struct ort final
36  {
37  static const char *identifier();
38  static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
39  static void validate(const smt_termt &lhs, const smt_termt &rhs);
40  };
42 
43  struct xort final
44  {
45  static const char *identifier();
46  static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
47  static void validate(const smt_termt &lhs, const smt_termt &rhs);
48  };
50 
51  struct equalt final
52  {
53  static const char *identifier();
54  static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
55  static void validate(const smt_termt &lhs, const smt_termt &rhs);
56  };
58 
59  struct distinctt final
60  {
61  static const char *identifier();
62  static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
63  static void validate(const smt_termt &lhs, const smt_termt &rhs);
64  };
66 
67  struct if_then_elset final
68  {
69  static const char *identifier();
70  static smt_sortt return_sort(
71  const smt_termt &condition,
72  const smt_termt &then_term,
73  const smt_termt &else_term);
74  static void validate(
75  const smt_termt &condition,
76  const smt_termt &then_term,
77  const smt_termt &else_term);
78  };
81 };
82 
83 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_CORE_THEORY_H
static const smt_function_application_termt::factoryt< distinctt > distinct
static const smt_function_application_termt::factoryt< if_then_elset > if_then_else
static const smt_function_application_termt::factoryt< impliest > implies
static const smt_function_application_termt::factoryt< ort > make_or
static const smt_function_application_termt::factoryt< equalt > equal
static const smt_function_application_termt::factoryt< andt > make_and
static const smt_function_application_termt::factoryt< xort > make_xor
static const smt_function_application_termt::factoryt< nott > make_not
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static const char * identifier()
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static const char * identifier()
static const char * identifier()
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &condition, const smt_termt &then_term, const smt_termt &else_term)
static const char * identifier()
static smt_sortt return_sort(const smt_termt &condition, const smt_termt &then_term, const smt_termt &else_term)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static const char * identifier()
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &operand)
static void validate(const smt_termt &operand)
static const char * identifier()
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static const char * identifier()
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static const char * identifier()
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)