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)37 inline 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