diff options
Diffstat (limited to 'src/theory/bv/bitblast_mode.h')
-rw-r--r-- | src/theory/bv/bitblast_mode.h | 72 |
1 files changed, 72 insertions, 0 deletions
diff --git a/src/theory/bv/bitblast_mode.h b/src/theory/bv/bitblast_mode.h new file mode 100644 index 000000000..318e17467 --- /dev/null +++ b/src/theory/bv/bitblast_mode.h @@ -0,0 +1,72 @@ +/********************* */ +/*! \file bitblast_mode.h + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Bitblasting modes for bit-vector solver. + ** + ** Bitblasting modes for bit-vector solver. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__BV__BITBLAST_MODE_H +#define __CVC4__THEORY__BV__BITBLAST_MODE_H + +#include <iostream> + +namespace CVC4 { +namespace theory { +namespace bv { + +/** Enumeration of bit-blasting modes */ +enum BitblastMode { + + /** + * Lazy bit-blasting that separates boolean reasoning + * from term reasoning. + */ + BITBLAST_MODE_LAZY, + + /** + * Bit-blast eagerly to the bit-vector SAT solver. + */ + BITBLAST_MODE_EAGER +};/* enum BitblastMode */ + +/** Enumeration of bit-vector equality slicer mode */ +enum BvSlicerMode { + + /** + * Force the slicer on. + */ + BITVECTOR_SLICER_ON, + + /** + * Slicer off. + */ + BITVECTOR_SLICER_OFF, + + /** + * Auto enable slicer if problem has only equalities. + */ + BITVECTOR_SLICER_AUTO + +};/* enum BvSlicerMode */ + + +}/* CVC4::theory::bv namespace */ +}/* CVC4::theory namespace */ + +std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode) CVC4_PUBLIC; + +}/* CVC4 namespace */ + +#endif /* __CVC4__THEORY__BV__BITBLAST_MODE_H */ |