cprover
solvers/module.md
Go to the documentation of this file.
1 \ingroup module_hidden
2 \defgroup module_solvers SAT/SMT Encoding and Decision Procedure
3 
4 \author Kareem Khazem
5 
6 \section sat-smt-encoding SAT/SMT Encoding
7 
8 In the \ref solvers directory.
9 
10 **Key classes:**
11 * \ref literalt
12 * \ref boolbvt
13 * \ref propt
14 
15 \dot
16 digraph G {
17  node [shape=box];
18  rankdir="LR";
19  1 [shape=none, label=""];
20  2 [label="goto conversion"];
21  3 [shape=none, label=""];
22  1 -> 2 [label="equations"];
23  2 -> 3 [label="propositional variables as bitvectors, constraints"];
24 }
25 \enddot
26 
27 
28 ---
29 
30 \section decision-procedure Decision Procedure
31 
32 In the \ref solvers directory.
33 
34 **Key classes:**
35 * symex_target_equationt
36 * \ref propt
37 * \ref bmct
38 
39 \dot
40 digraph G {
41  node [shape=box];
42  rankdir="LR";
43  1 [shape=none, label=""];
44  2 [label="goto conversion"];
45  3 [shape=none, label=""];
46  1 -> 2 [label="propositional variables as bitvectors, constraints"];
47  2 -> 3 [label="solutions"];
48 }
49 \enddot