1 /*********************                                                        */
2 /*! \file bv_bitblast_mode.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Liana Hadarean, Alex Ozdemir, Mathias Preiner
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
8  ** in the top-level source directory) and their institutional affiliations.
9  ** All rights reserved.  See the file COPYING in the top-level source
10  ** directory for licensing information.\endverbatim
11  **
12  ** \brief Bitblasting modes for bit-vector solver.
13  **
14  ** Bitblasting modes for bit-vector solver.
15  **/
16 
17 #include "cvc4_private.h"
18 
19 #ifndef __CVC4__THEORY__BV__BITBLAST_MODE_H
20 #define __CVC4__THEORY__BV__BITBLAST_MODE_H
21 
22 #include <iosfwd>
23 
24 namespace CVC4 {
25 namespace theory {
26 namespace bv {
27 
28 /** Enumeration of bit-blasting modes */
29 enum BitblastMode {
30 
31   /**
32    * Lazy bit-blasting that separates boolean reasoning
33    * from term reasoning.
34    */
35   BITBLAST_MODE_LAZY,
36 
37   /**
38    * Bit-blast eagerly to the bit-vector SAT solver.
39    */
40   BITBLAST_MODE_EAGER
41 };/* enum BitblastMode */
42 
43 /** Enumeration of bit-vector equality slicer mode */
44 enum BvSlicerMode {
45 
46   /**
47    * Force the slicer on.
48    */
49   BITVECTOR_SLICER_ON,
50 
51   /**
52    * Slicer off.
53    */
54   BITVECTOR_SLICER_OFF,
55 
56   /**
57    * Auto enable slicer if problem has only equalities.
58    */
59   BITVECTOR_SLICER_AUTO
60 
61 };/* enum BvSlicerMode */
62 
63 /** Enumeration of sat solvers that can be used. */
64 enum SatSolverMode
65 {
66   SAT_SOLVER_MINISAT,
67   SAT_SOLVER_CRYPTOMINISAT,
68   SAT_SOLVER_CADICAL,
69 }; /* enum SatSolver */
70 
71 /**
72  * When the BV solver does eager bitblasting backed by CryptoMiniSat, proofs
73  * can be written in a variety of formats.
74  */
75 enum BvProofFormat
76 {
77   /**
78    * Write extended resolution proofs.
79    */
80   BITVECTOR_PROOF_ER,
81   /**
82    * Write DRAT proofs.
83    */
84   BITVECTOR_PROOF_DRAT,
85   /**
86    * Write LRAT proofs.
87    */
88   BITVECTOR_PROOF_LRAT,
89 };
90 
91 }/* CVC4::theory::bv namespace */
92 }/* CVC4::theory namespace */
93 
94 std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode);
95 std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode);
96 std::ostream& operator<<(std::ostream& out, theory::bv::SatSolverMode mode);
97 std::ostream& operator<<(std::ostream& out, theory::bv::BvProofFormat format);
98 
99 }/* CVC4 namespace */
100 
101 #endif /* __CVC4__THEORY__BV__BITBLAST_MODE_H */
102