mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 09:28:45 +00:00
Code Activity

add get-some-value to seq API, expose quantifier tactics

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-26 08:05:44 -08:00
parent 345f6e87bd
commit 8e378062e2
3 changed files with 29 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/ast/seq_decl_plugin.cpp
View file

@ -744,6 +744,19 @@ bool seq_decl_plugin::is_value(app* e) const {
m_manager->is_value(e->get_arg(0))); 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) { app* seq_util::mk_skolem(symbol const& name, unsigned n, expr* const* args, sort* range) {
SASSERT(range); SASSERT(range);
parameter param(name); parameter param(name);

3
src/ast/seq_decl_plugin.h
View file

@ -177,10 +177,13 @@ public:
virtual bool is_unique_value(app * e) const { return is_value(e); } 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; } bool is_char(ast* a) const { return a == m_char; }
app* mk_string(symbol const& s); app* mk_string(symbol const& s);
app* mk_string(zstring const& s); app* mk_string(zstring const& s);
}; };
class seq_util { class seq_util {

13
src/tactic/smtlogics/quant_tactics.h
View file

@ -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_lia_tactic(ast_manager & m, params_ref const & p);
tactic * mk_lira_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 #endif