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