summaryrefslogtreecommitdiff
path: root/src/options/bv_bitblast_mode.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/options/bv_bitblast_mode.h')
-rw-r--r--src/options/bv_bitblast_mode.h7
1 files changed, 7 insertions, 0 deletions
diff --git a/src/options/bv_bitblast_mode.h b/src/options/bv_bitblast_mode.h
index 4c8c4f626..3a6474104 100644
--- a/src/options/bv_bitblast_mode.h
+++ b/src/options/bv_bitblast_mode.h
@@ -60,12 +60,19 @@ enum BvSlicerMode {
};/* enum BvSlicerMode */
+/** Enumeration of sat solvers that can be used. */
+enum SatSolverMode {
+ SAT_SOLVER_MINISAT,
+ SAT_SOLVER_CRYPTOMINISAT,
+};/* enum SatSolver */
+
}/* CVC4::theory::bv namespace */
}/* CVC4::theory namespace */
std::ostream& operator<<(std::ostream& out, theory::bv::BitblastMode mode);
std::ostream& operator<<(std::ostream& out, theory::bv::BvSlicerMode mode);
+std::ostream& operator<<(std::ostream& out, theory::bv::SatSolverMode mode);
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback