From 4875741a3708009fd54519e2afaa5c45a8dcda0c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 2 Sep 2016 17:04:01 -0700 Subject: [PATCH] feat(library/app_builder): add mk_ite --- src/library/app_builder.cpp | 6 ++++++ src/library/app_builder.h | 3 +++ 2 files changed, 9 insertions(+) diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index b0602706ab..5b8e5c92d9 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -951,6 +951,12 @@ expr mk_false_rec(type_context & ctx, expr const & c, expr const & H) { return app_builder(ctx).mk_false_rec(c, H); } +expr mk_ite(type_context & ctx, expr const & c, expr const & t, expr const & e) { + bool mask[5] = {true, false, false, true, true}; + expr args[3] = {c, t, e}; + return mk_app(ctx, get_ite_name(), 5, mask, args); +} + void initialize_app_builder() { register_trace_class("app_builder"); } diff --git a/src/library/app_builder.h b/src/library/app_builder.h index 700d576c2e..486f80cea9 100644 --- a/src/library/app_builder.h +++ b/src/library/app_builder.h @@ -155,6 +155,9 @@ expr mk_ss_elim(type_context & ctx, expr const & A, expr const & ss_inst, expr c /** \brief False elimination */ expr mk_false_rec(type_context & ctx, expr const & c, expr const & H); +/* (if c then t else e) */ +expr mk_ite(type_context & ctx, expr const & c, expr const & t, expr const & e); + level get_level(type_context & ctx, expr const & A); void initialize_app_builder();