mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 12:51:22 +00:00
Code Activity

expose maxdiff

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-05-04 08:52:42 -07:00
parent 367bfedab0
commit 5a685ba9b5
2 changed files with 1 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/array_decl_plugin.cpp
View file

@ -535,7 +535,7 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
m_manager->raise_exception("min/maxdiff don't take two arrays of same sort and with integer index"); m_manager->raise_exception("min/maxdiff don't take two arrays of same sort and with integer index");
sort* idx = get_array_domain(domain[0], 0); sort* idx = get_array_domain(domain[0], 0);
arith_util arith(*m_manager); arith_util arith(*m_manager);
if (!arith.is_int(domain[0])) if (!arith.is_int(idx))
m_manager->raise_exception("min/maxdiff take integer index domain"); m_manager->raise_exception("min/maxdiff take integer index domain");
return m_manager->mk_func_decl(k == OP_ARRAY_MAXDIFF ? symbol("maxdiff") : symbol("mindiff"), return m_manager->mk_func_decl(k == OP_ARRAY_MAXDIFF ? symbol("maxdiff") : symbol("mindiff"),
arity, domain, arith.mk_int(), func_decl_info(m_family_id, k)); arity, domain, arith.mk_int(), func_decl_info(m_family_id, k));
@ -601,11 +601,8 @@ void array_decl_plugin::get_op_names(svector<builtin_name>& op_names, symbol con
op_names.push_back(builtin_name("as-array", OP_AS_ARRAY)); op_names.push_back(builtin_name("as-array", OP_AS_ARRAY));
op_names.push_back(builtin_name("array-ext", OP_ARRAY_EXT)); op_names.push_back(builtin_name("array-ext", OP_ARRAY_EXT));
#if 0
// not exposed
op_names.push_back(builtin_name("mindiff", OP_ARRAY_MINDIFF)); op_names.push_back(builtin_name("mindiff", OP_ARRAY_MINDIFF));
op_names.push_back(builtin_name("maxdiff", OP_ARRAY_MAXDIFF)); op_names.push_back(builtin_name("maxdiff", OP_ARRAY_MAXDIFF));
#endif
#if 0 #if 0
op_names.push_back(builtin_name("set-has-size", OP_SET_HAS_SIZE)); op_names.push_back(builtin_name("set-has-size", OP_SET_HAS_SIZE));

3
src/ast/seq_decl_plugin.cpp
View file

@ -185,13 +185,10 @@ void seq_decl_plugin::init() {
array_util autil(m); array_util autil(m);
m_init = true; m_init = true;
sort* A = m.mk_uninterpreted_sort(symbol(0u)); sort* A = m.mk_uninterpreted_sort(symbol(0u));
sort* B = m.mk_uninterpreted_sort(symbol(1u));
sort* strT = m_string; sort* strT = m_string;
parameter paramA(A); parameter paramA(A);
parameter paramB(B);
parameter paramS(strT); parameter paramS(strT);
sort* seqA = m.mk_sort(m_family_id, SEQ_SORT, 1, &paramA); sort* seqA = m.mk_sort(m_family_id, SEQ_SORT, 1, &paramA);
sort* seqB = m.mk_sort(m_family_id, SEQ_SORT, 1, &paramB);
parameter paramSA(seqA); parameter paramSA(seqA);
sort* reA = m.mk_sort(m_family_id, RE_SORT, 1, &paramSA); sort* reA = m.mk_sort(m_family_id, RE_SORT, 1, &paramSA);
sort* reT = m.mk_sort(m_family_id, RE_SORT, 1, &paramS); sort* reT = m.mk_sort(m_family_id, RE_SORT, 1, &paramS);