Source

z3 / src / ast / rewriter / rewriter_types.h

/*++
Copyright (c) 2007 Microsoft Corporation

Module Name:

    rewriter_types.h

Abstract:

    Lean and mean rewriter

Author:

    Leonardo (leonardo) 2011-04-10

Notes:

--*/
#ifndef _REWRITER_TYPES_H_
#define _REWRITER_TYPES_H_

#include"z3_exception.h"
#include"common_msgs.h"

/**
   \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
};

#define RW_UNBOUNDED_DEPTH 3
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 {
public:                                                
    rewriter_exception(char const * msg):default_exception(msg) {}
};

#endif
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 ProjectModifiedEvent.java.
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.