mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 20:03:38 +00:00
Code Activity

use is_uninterp

Browse source
This commit is contained in:
Doug Woos 2017-02-01 16:20:40 -08:00
parent d9e43f0e6d
commit a147e2bc35
1 changed files with 4 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/tactic/sine_filter.cpp
View file

@ -77,11 +77,6 @@ public:
private: private:
// is this a user-defined symbol name?
bool is_name(func_decl * f) {
return f->get_family_id() < 0;
}
typedef std::pair<expr*,expr*> t_work_item; typedef std::pair<expr*,expr*> t_work_item;
t_work_item work_item(expr *e, expr *root) { t_work_item work_item(expr *e, expr *root) {
@ -97,8 +92,8 @@ private:
stack.pop_back(); stack.pop_back();
if (is_app(curr)) { if (is_app(curr)) {
app *a = to_app(curr); app *a = to_app(curr);
func_decl *f = a->get_decl(); if (is_uninterp(a)) {
if (is_name(f)) { func_decl *f = a->get_decl();
consts.insert_if_not_there(f); consts.insert_if_not_there(f);
} }
} }
@ -159,8 +154,8 @@ private:
stack.pop_back(); stack.pop_back();
if (is_app(curr.first)) { if (is_app(curr.first)) {
app *a = to_app(curr.first); app *a = to_app(curr.first);
func_decl *f = a->get_decl(); if (is_uninterp(a)) {
if (is_name(f)) { func_decl *f = a->get_decl();
if (!consts.contains(f)) { if (!consts.contains(f)) {
consts.insert(f); consts.insert(f);
if (const2quantifier.contains(f)) { if (const2quantifier.contains(f)) {