From 1c5f798cbe473b5508ea295356bed7b97c05adbb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 25 Nov 2017 12:03:47 -0800 Subject: [PATCH] expose extra symbols for logic ALL, requested in #1364 Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.cpp | 2 +- src/ast/array_decl_plugin.cpp | 2 +- src/ast/bv_decl_plugin.cpp | 4 ++-- src/ast/datatype_decl_plugin.cpp | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 03ee77458..85c54d1fa 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -539,7 +539,7 @@ void arith_decl_plugin::get_op_names(svector& op_names, symbol con op_names.push_back(builtin_name("to_int",OP_TO_INT)); op_names.push_back(builtin_name("is_int",OP_IS_INT)); op_names.push_back(builtin_name("abs", OP_ABS)); - if (logic == symbol::null) { + if (logic == symbol::null || logic == symbol("ALL")) { op_names.push_back(builtin_name("^", OP_POWER)); op_names.push_back(builtin_name("sin", OP_SIN)); op_names.push_back(builtin_name("cos", OP_COS)); diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index 0cc4f6031..1e789b7e5 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -524,7 +524,7 @@ void array_decl_plugin::get_sort_names(svector& sort_names, symbol void array_decl_plugin::get_op_names(svector& op_names, symbol const & logic) { op_names.push_back(builtin_name("store",OP_STORE)); op_names.push_back(builtin_name("select",OP_SELECT)); - if (logic == symbol::null || logic == symbol("HORN")) { + if (logic == symbol::null || logic == symbol("HORN") || logic == symbol("ALL")) { // none of the SMT2 logics support these extensions op_names.push_back(builtin_name("const",OP_CONST_ARRAY)); op_names.push_back(builtin_name("map",OP_ARRAY_MAP)); diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 093d0f548..28c3d5f5d 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -670,7 +670,7 @@ bool bv_decl_plugin::are_distinct(app * a, app * b) const { } void bv_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { - if (logic == symbol::null) + if (logic == symbol::null || logic == symbol("ALL")) sort_names.push_back(builtin_name("bv", BV_SORT)); sort_names.push_back(builtin_name("BitVec", BV_SORT)); } @@ -717,7 +717,7 @@ void bv_decl_plugin::get_op_names(svector & op_names, symbol const op_names.push_back(builtin_name("rotate_left",OP_ROTATE_LEFT)); op_names.push_back(builtin_name("rotate_right",OP_ROTATE_RIGHT)); - if (logic == symbol::null) { + if (logic == symbol::null || logic == symbol("ALL")) { op_names.push_back(builtin_name("bvumul_noovfl",OP_BUMUL_NO_OVFL)); op_names.push_back(builtin_name("bvsmul_noovfl",OP_BSMUL_NO_OVFL)); op_names.push_back(builtin_name("bvsmul_noudfl",OP_BSMUL_NO_UDFL)); diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 566487e60..91e636ed7 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -458,7 +458,7 @@ namespace datatype { void plugin::get_op_names(svector & op_names, symbol const & logic) { op_names.push_back(builtin_name("is", OP_DT_IS)); - if (logic == symbol::null) { + if (logic == symbol::null || logic == symbol("ALL")) { op_names.push_back(builtin_name("update-field", OP_DT_UPDATE_FIELD)); } }