1 /*++ 2 Copyright (c) 2007 Microsoft Corporation 3 4 Module Name: 5 6 rewriter_types.h 7 8 Abstract: 9 10 Lean and mean rewriter 11 12 Author: 13 14 Leonardo (leonardo) 2011-04-10 15 16 Notes: 17 18 --*/ 19 #pragma once 20 21 #include "util/z3_exception.h" 22 #include "util/common_msgs.h" 23 24 /** 25 \brief Builtin rewrite result status 26 */ 27 enum br_status { 28 BR_REWRITE1, // rewrite the result (bounded by depth 1) 29 BR_REWRITE2, // rewrite the result (bounded by depth 2) 30 BR_REWRITE3, // rewrite the result (bounded by depth 3) 31 BR_REWRITE_FULL, // rewrite the result unbounded 32 BR_DONE, // done, the result is simplified 33 BR_FAILED // no builtin rewrite is available 34 }; 35 36 #define RW_UNBOUNDED_DEPTH 3 unsigned2br_status(unsigned u)37inline br_status unsigned2br_status(unsigned u) { 38 br_status r = u >= RW_UNBOUNDED_DEPTH ? BR_REWRITE_FULL : static_cast<br_status>(u); 39 SASSERT((u == 0) == (r == BR_REWRITE1)); 40 SASSERT((u == 1) == (r == BR_REWRITE2)); 41 SASSERT((u == 2) == (r == BR_REWRITE3)); 42 SASSERT((u >= 3) == (r == BR_REWRITE_FULL)); 43 return r; 44 } 45 46 class rewriter_exception : public default_exception { 47 public: rewriter_exception(std::string && msg)48 rewriter_exception(std::string && msg) : default_exception(std::move(msg)) {} 49 }; 50 51