mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

add recognizer for distinct

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-03-06 10:18:29 -08:00
parent f00697cf95
commit 5a02edc8cd
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/api/c++/z3++.h
View file

@ -996,6 +996,7 @@ namespace z3 {
bool is_implies() const { return is_app() && Z3_OP_IMPLIES == decl().decl_kind(); }
bool is_eq() const { return is_app() && Z3_OP_EQ == decl().decl_kind(); }
bool is_ite() const { return is_app() && Z3_OP_ITE == decl().decl_kind(); }
bool is_distinct() const { return is_app() && Z3_OP_DISTINCT == decl().decl_kind(); }
friend expr distinct(expr_vector const& args);
friend expr concat(expr const& a, expr const& b);