From 6cf68bee80461a88048146cdc02dd7123e38d6f2 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Mon, 7 Aug 2017 11:47:57 +0200
Subject: [PATCH] app ordering that puts special skolem constants first

---
 src/muz/spacer/spacer_manager.cpp | 22 ++++++++++++++++++++++
 src/muz/spacer/spacer_manager.h   |  4 ++++
 2 files changed, 26 insertions(+)

diff --git a/src/muz/spacer/spacer_manager.cpp b/src/muz/spacer/spacer_manager.cpp
index ba4ca0da7..d583813a8 100644
--- a/src/muz/spacer/spacer_manager.cpp
+++ b/src/muz/spacer/spacer_manager.cpp
@@ -384,4 +384,26 @@ bool has_zk_const(expr *e){
     return false;
 }
 
+bool is_zk_const (const app *a, int &n) {
+    if (!is_uninterp_const(a)) return false;
+
+    const symbol &name = a->get_decl()->get_name();
+    if (name.str().compare (0, 3, "sk!") != 0) {
+        return false;
+    }
+
+    n = std::stoi(name.str().substr(3));
+    return true;
+}
+bool sk_lt_proc::operator()(const app *a1, const app *a2) {
+    if (a1 == a2) return false;
+    int n1, n2;
+    bool z1, z2;
+    z1 = is_zk_const(a1, n1);
+    z2 = is_zk_const(a2, n2);
+    if (z1 && z2) return n1 < n2;
+    if (z1 != z2) return z1;
+    return ast_lt_proc()(a1, a2);
+}
+
 }
diff --git a/src/muz/spacer/spacer_manager.h b/src/muz/spacer/spacer_manager.h
index f2382c15d..f49aa63fc 100644
--- a/src/muz/spacer/spacer_manager.h
+++ b/src/muz/spacer/spacer_manager.h
@@ -341,6 +341,10 @@ public:
 app* mk_zk_const (ast_manager &m, unsigned idx, sort *s);
 void find_zk_const(expr* e, app_ref_vector &out);
 bool has_zk_const(expr* e);
+
+struct sk_lt_proc {
+    bool operator()(const app* a1, const app* a2);
+};
 }
 
 #endif