mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-30 05:09:02 +00:00
Code Activity

implement str_decl_plugin::is_value() and ::is_unique_value()

Browse source 
we can now prove that (= "abc" "def") is unsatisfiable
This commit is contained in:
Murphy Berzish 2015-09-27 23:57:41 -04:00
parent 02cb329ca5
commit 0d54e4e4ae
2 changed files with 15 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/str_decl_plugin.cpp
View file

@ -115,6 +115,18 @@ void str_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol
sort_names.push_back(builtin_name("String", STRING_SORT)); sort_names.push_back(builtin_name("String", STRING_SORT));
} }
bool str_decl_plugin::is_value(app * e) const {
if (e->get_family_id() != m_family_id) {
return false;
}
switch (e->get_decl_kind()) {
case OP_STR:
return true;
default:
return false;
}
}
bool str_recognizers::is_string(expr const * n, const char ** val) const { bool str_recognizers::is_string(expr const * n, const char ** val) const {
if (!is_app_of(n, m_afid, OP_STR)) if (!is_app_of(n, m_afid, OP_STR))
return false; return false;

4
src/ast/str_decl_plugin.h
View file

@ -60,8 +60,10 @@ public:
app * mk_string(const char * val); app * mk_string(const char * val);
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic); virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic); virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
virtual bool is_value(app * e) const;
virtual bool is_unique_value(app * e) const { return is_value(e); }
// TODO // TODO
}; };