mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-11 00:23:25 +00:00
Code Activity

type check distinct operator. fixes #62

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@hotmail.com>
This commit is contained in:
Nikolaj Bjorner 2015-04-27 11:10:37 -07:00
parent f7d9438e7b
commit 620c11932b
3 changed files with 14 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/ast/ast.cpp
View file

@ -1043,6 +1043,13 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
case OP_DISTINCT: {
func_decl_info info(m_family_id, OP_DISTINCT);
info.set_pairwise();
for (unsigned i = 1; i < arity; i++) {
if (domain[i] != domain[0]) {
std::ostringstream buffer;
buffer << "Sort mismatch between first argument and argument " << (i+1);
throw ast_exception(buffer.str().c_str());
}
}
return m_manager->mk_func_decl(symbol("distinct"), arity, domain, m_bool_sort, info);
}
default:
@ -2338,6 +2345,10 @@ quantifier * ast_manager::update_quantifier(quantifier * q, bool is_forall, unsi
num_patterns == 0 ? q->get_no_patterns() : 0);
}
app * ast_manager::mk_distinct(unsigned num_args, expr * const * args) {
return mk_app(m_basic_family_id, OP_DISTINCT, num_args, args);
}
app * ast_manager::mk_distinct_expanded(unsigned num_args, expr * const * args) {
if (num_args < 2)
return mk_true();