z3 / src / ast / rewriter / rewriter_types.h

Copyright (c) 2007 Microsoft Corporation

Module Name:



    Lean and mean rewriter


    Leonardo (leonardo) 2011-04-10




   \brief Builtin rewrite result status
enum br_status {
    BR_REWRITE1,               // rewrite the result (bounded by depth 1)
    BR_REWRITE2,               // rewrite the result (bounded by depth 2)
    BR_REWRITE3,               // rewrite the result (bounded by depth 3)
    BR_REWRITE_FULL,           // rewrite the result unbounded
    BR_DONE,                   // done, the result is simplified
    BR_FAILED                  // no builtin rewrite is available

inline br_status unsigned2br_status(unsigned u) {
    br_status r = u >= RW_UNBOUNDED_DEPTH ? BR_REWRITE_FULL : static_cast<br_status>(u);
    SASSERT((u == 0) == (r == BR_REWRITE1));
    SASSERT((u == 1) == (r == BR_REWRITE2));
    SASSERT((u == 2) == (r == BR_REWRITE3));
    SASSERT((u >= 3) == (r == BR_REWRITE_FULL));
    return r;

class rewriter_exception : public default_exception {
    rewriter_exception(char const * msg):default_exception(msg) {}

Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.