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
smt_core_theoryt::impliest::validate
static void validate(const smt_termt &lhs, const smt_termt &rhs)
Definition: smt_core_theory.cpp:36
smt_core_theoryt::andt
Definition: smt_core_theory.h:28
smt_core_theoryt::xort::validate
static void validate(const smt_termt &lhs, const smt_termt &rhs)
Definition: smt_core_theory.cpp:112
smt_core_theoryt::andt::return_sort
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
Definition: smt_core_theory.cpp:57
smt_core_theoryt::ort
Definition: smt_core_theory.h:36
smt_core_theoryt::nott::return_sort
static smt_sortt return_sort(const smt_termt &operand)
Definition: smt_core_theory.cpp:10
smt_core_theoryt::distinct
static const smt_function_application_termt::factoryt< distinctt > distinct
Definition: smt_core_theory.h:65
smt_core_theoryt::equalt::validate
static void validate(const smt_termt &lhs, const smt_termt &rhs)
Definition: smt_core_theory.cpp:138
smt_core_theoryt::ort::identifier
static const char * identifier()
Definition: smt_core_theory.cpp:77
smt_core_theoryt::impliest
Definition: smt_core_theory.h:20
smt_core_theoryt::nott::validate
static void validate(const smt_termt &operand)
Definition: smt_core_theory.cpp:15
smt_core_theoryt::if_then_elset
Definition: smt_core_theory.h:68
smt_termt
Definition: smt_terms.h:16
smt_core_theoryt::make_or
static const smt_function_application_termt::factoryt< ort > make_or
Definition: smt_core_theory.h:41
smt_core_theoryt::make_xor
static const smt_function_application_termt::factoryt< xort > make_xor
Definition: smt_core_theory.h:49
smt_core_theoryt::make_not
static const smt_function_application_termt::factoryt< nott > make_not
Definition: smt_core_theory.h:17
smt_core_theoryt::equalt
Definition: smt_core_theory.h:52
smt_core_theoryt::xort::identifier
static const char * identifier()
Definition: smt_core_theory.cpp:101
smt_core_theoryt::xort
Definition: smt_core_theory.h:44
smt_core_theoryt::implies
static const smt_function_application_termt::factoryt< impliest > implies
Definition: smt_core_theory.h:25
smt_core_theoryt::impliest::return_sort
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
Definition: smt_core_theory.cpp:31
smt_core_theoryt::distinctt::validate
static void validate(const smt_termt &lhs, const smt_termt &rhs)
Definition: smt_core_theory.cpp:161
smt_core_theoryt
Definition: smt_core_theory.h:9
smt_core_theoryt::if_then_elset::identifier
static const char * identifier()
Definition: smt_core_theory.cpp:173
smt_core_theoryt::distinctt::identifier
static const char * identifier()
Definition: smt_core_theory.cpp:150
smt_sortt
Definition: smt_sorts.h:18
smt_core_theoryt::nott::identifier
static const char * identifier()
Definition: smt_core_theory.cpp:5
smt_core_theoryt::if_then_else
static const smt_function_application_termt::factoryt< if_then_elset > if_then_else
Definition: smt_core_theory.h:80
smt_function_application_termt::factoryt
Definition: smt_terms.h:130
smt_core_theoryt::distinctt::return_sort
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
Definition: smt_core_theory.cpp:156
smt_core_theoryt::equalt::identifier
static const char * identifier()
Definition: smt_core_theory.cpp:127
smt_core_theoryt::make_and
static const smt_function_application_termt::factoryt< andt > make_and
Definition: smt_core_theory.h:33
smt_core_theoryt::andt::validate
static void validate(const smt_termt &lhs, const smt_termt &rhs)
Definition: smt_core_theory.cpp:62
smt_core_theoryt::equalt::return_sort
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
Definition: smt_core_theory.cpp:133
smt_core_theoryt::impliest::identifier
static const char * identifier()
Definition: smt_core_theory.cpp:25
smt_core_theoryt::xort::return_sort
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
Definition: smt_core_theory.cpp:107
smt_core_theoryt::nott
Definition: smt_core_theory.h:12
smt_core_theoryt::if_then_elset::return_sort
static smt_sortt return_sort(const smt_termt &condition, const smt_termt &then_term, const smt_termt &else_term)
Definition: smt_core_theory.cpp:178
smt_core_theoryt::if_then_elset::validate
static void validate(const smt_termt &condition, const smt_termt &then_term, const smt_termt &else_term)
Definition: smt_core_theory.cpp:186
smt_core_theoryt::distinctt
Definition: smt_core_theory.h:60
smt_core_theoryt::equal
static const smt_function_application_termt::factoryt< equalt > equal
Definition: smt_core_theory.h:57
smt_core_theoryt::ort::return_sort
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
Definition: smt_core_theory.cpp:83
smt_terms.h
smt_core_theoryt::ort::validate
static void validate(const smt_termt &lhs, const smt_termt &rhs)
Definition: smt_core_theory.cpp:88
smt_core_theoryt::andt::identifier
static const char * identifier()
Definition: smt_core_theory.cpp:51