z3 / src / ast / rewriter / dl_rewriter.cpp

/*++
Copyright (c) 2010 Microsoft Corporation

Module Name:

    dl_rewriter.cpp

Abstract:

    <abstract>

Author:

    Nikolaj Bjorner (nbjorner) 2010-08-10

Revision History:

--*/

#include"dl_rewriter.h"
    
    br_status dl_rewriter::mk_app_core(
        func_decl * f, unsigned num_args, expr* const* args, expr_ref& result) {
        ast_manager& m = result.get_manager();
        uint64 v1, v2;
        switch(f->get_decl_kind()) {
		case datalog::OP_DL_LT:
            if (m_util.is_numeral_ext(args[0], v1) &&
                m_util.is_numeral_ext(args[1], v2)) {
                result = (v1 < v2)?m.mk_true():m.mk_false();
                return BR_DONE;
            }
            // x < x <=> false
            if (args[0] == args[1]) {
                result = m.mk_false();
                return BR_DONE;
            }
            // x < 0 <=> false
            if (m_util.is_numeral_ext(args[1], v2) && v2 == 0) {
                result = m.mk_false();
                return BR_DONE;
            }
            // 0 < x <=> 0 != x
            if (m_util.is_numeral_ext(args[1], v1) && v1 == 0) {
                result = m.mk_not(m.mk_eq(args[0], args[1]));
                return BR_DONE;
            }
            break;

        default:
            break;
        }
        return BR_FAILED;
    }
    
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.