From 8e378062e249d902a78652b02d1bccae3e9530a4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 26 Jan 2016 08:05:44 -0800
Subject: [PATCH] add get-some-value to seq API, expose quantifier tactics

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/seq_decl_plugin.cpp          | 13 +++++++++++++
 src/ast/seq_decl_plugin.h            |  3 +++
 src/tactic/smtlogics/quant_tactics.h | 13 +++++++++++++
 3 files changed, 29 insertions(+)

diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 5cd3526d9..f15e83381 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -744,6 +744,19 @@ bool seq_decl_plugin::is_value(app* e) const {
          m_manager->is_value(e->get_arg(0)));
 }
 
+expr* seq_decl_plugin::get_some_value(sort* s) {
+    seq_util util(*m_manager);
+    if (util.is_seq(s)) {
+        return util.str.mk_empty(s);
+    }
+    sort* seq;
+    if (util.is_re(s, seq)) {
+        return util.re.mk_to_re(util.str.mk_empty(seq));
+    }
+    UNREACHABLE();
+    return 0;
+}
+
 app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range) {
     SASSERT(range);
     parameter param(name);
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index 29ec98b07..a83878b0e 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -177,10 +177,13 @@ public:
 
     virtual bool is_unique_value(app * e) const { return is_value(e); }
 
+    virtual expr * get_some_value(sort * s);
+
     bool is_char(ast* a) const { return a == m_char; }
 
     app* mk_string(symbol const& s);  
     app* mk_string(zstring const& s);  
+
 };
 
 class seq_util {
diff --git a/src/tactic/smtlogics/quant_tactics.h b/src/tactic/smtlogics/quant_tactics.h
index 3da05a0f2..b78730236 100644
--- a/src/tactic/smtlogics/quant_tactics.h
+++ b/src/tactic/smtlogics/quant_tactics.h
@@ -32,4 +32,17 @@ tactic * mk_lra_tactic(ast_manager & m, params_ref const & p);
 tactic * mk_lia_tactic(ast_manager & m, params_ref const & p);
 tactic * mk_lira_tactic(ast_manager & m, params_ref const & p);
 
+/*
+  ADD_TACTIC("ufnia", "builtin strategy for solving UFNIA problems.", "mk_ufnia_tactic(m, p)")
+  ADD_TACTIC("uflra", "builtin strategy for solving UFLRA problems.", "mk_uflra_tactic(m, p)")
+  ADD_TACTIC("auflia", "builtin strategy for solving AUFLIA problems.", "mk_auflia_tactic(m, p)")
+  ADD_TACTIC("auflira", "builtin strategy for solving AUFLIRA problems.", "mk_auflira_tactic(m, p)")
+  ADD_TACTIC("aufnira", "builtin strategy for solving AUFNIRA problems.", "mk_aufnira_tactic(m, p)")
+  ADD_TACTIC("lra", "builtin strategy for solving LRA problems.", "mk_lra_tactic(m, p)")
+  ADD_TACTIC("lia", "builtin strategy for solving LIA problems.", "mk_lia_tactic(m, p)")
+  ADD_TACTIC("lira", "builtin strategy for solving LIRA problems.", "mk_lira_tactic(m, p)")
+
+*/
+
+
 #endif