From dc0e9c1919295cb0ad9cb0798741de6e536d5eb1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 24 Mar 2019 11:46:36 -0700 Subject: [PATCH] completing user print experience with seq/re #2200 Signed-off-by: Nikolaj Bjorner --- src/api/api_ast.cpp | 4 +-- src/api/api_seq.cpp | 26 +++++++++++++++++ src/api/python/z3/z3.py | 30 ++++++++++++++++++-- src/api/python/z3/z3printer.py | 40 +++++++++++++++++++++++++-- src/api/z3_api.h | 14 ++++++++++ src/sat/sat_model_converter.cpp | 6 +++- src/sat/sat_solver.cpp | 1 + src/sat/sat_solver/inc_sat_solver.cpp | 3 +- src/sat/tactic/goal2sat.h | 2 +- 9 files changed, 115 insertions(+), 11 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 4893cbe10..cabfdb101 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1192,8 +1192,8 @@ extern "C" { case OP_RE_UNION: return Z3_OP_RE_UNION; case OP_RE_INTERSECT: return Z3_OP_RE_INTERSECT; case OP_RE_LOOP: return Z3_OP_RE_LOOP; - // case OP_RE_FULL_SEQ_SET: return Z3_OP_RE_FULL_SET; - case OP_RE_FULL_CHAR_SET: return Z3_OP_RE_FULL_SET; + case OP_RE_FULL_SEQ_SET: return Z3_OP_RE_FULL_SET; + //case OP_RE_FULL_CHAR_SET: return Z3_OP_RE_FULL_SET; case OP_RE_EMPTY_SET: return Z3_OP_RE_EMPTY_SET; default: return Z3_OP_INTERNAL; diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index b621dcebe..7554fff8a 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -95,6 +95,32 @@ extern "C" { Z3_CATCH_RETURN(false); } + Z3_sort Z3_API Z3_get_seq_sort_basis(Z3_context c, Z3_sort s) { + Z3_TRY; + LOG_Z3_get_seq_sort_basis(c, s); + RESET_ERROR_CODE(); + sort* r = nullptr; + if (!mk_c(c)->sutil().is_seq(to_sort(s), r)) { + SET_ERROR_CODE(Z3_INVALID_ARG, "expected sequence sort"); + RETURN_Z3(nullptr); + } + RETURN_Z3(of_sort(r)); + Z3_CATCH_RETURN(nullptr); + } + + Z3_sort Z3_API Z3_get_re_sort_basis(Z3_context c, Z3_sort s) { + Z3_TRY; + LOG_Z3_get_re_sort_basis(c, s); + RESET_ERROR_CODE(); + sort* r = nullptr; + if (!mk_c(c)->sutil().is_re(to_sort(s), r)) { + SET_ERROR_CODE(Z3_INVALID_ARG, "expected regex sort"); + RETURN_Z3(nullptr); + } + RETURN_Z3(of_sort(r)); + Z3_CATCH_RETURN(nullptr); + } + bool Z3_API Z3_is_string_sort(Z3_context c, Z3_sort s) { Z3_TRY; LOG_Z3_is_string_sort(c, s); diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index e5ab83187..8a7053deb 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -609,6 +609,10 @@ def _to_sort_ref(s, ctx): return FPSortRef(s, ctx) elif k == Z3_ROUNDING_MODE_SORT: return FPRMSortRef(s, ctx) + elif k == Z3_RE_SORT: + return ReSortRef(s, ctx) + elif k == Z3_SEQ_SORT: + return SeqSortRef(s, ctx) return SortRef(s, ctx) def _sort(ctx, a): @@ -9908,6 +9912,9 @@ class SeqSortRef(SortRef): False """ return Z3_is_string_sort(self.ctx_ref(), self.ast) + + def basis(self): + return _to_sort_ref(Z3_get_seq_sort_basis(self.ctx_ref(), self.ast), self.ctx) def StringSort(ctx=None): @@ -10062,7 +10069,7 @@ def Full(s): re.all >>> e1 = Full(ReSort(StringSort())) >>> print(e1) - re.all + rel.all """ if isinstance(s, ReSortRef): return ReRef(Z3_mk_re_full(s.ctx_ref(), s.ast), s.ctx) @@ -10212,6 +10219,8 @@ def Re(s, ctx=None): class ReSortRef(SortRef): """Regular expression sort.""" + def basis(self): + return _to_sort_ref(Z3_get_re_sort_basis(self.ctx_ref(), self.ast), self.ctx) def ReSort(s): if is_ast(s): @@ -10228,7 +10237,6 @@ class ReRef(ExprRef): def __add__(self, other): return Union(self, other) - def is_re(s): return isinstance(s, ReRef) @@ -10265,6 +10273,24 @@ def Union(*args): v[i] = args[i].as_ast() return ReRef(Z3_mk_re_union(ctx.ref(), sz, v), ctx) +def Intersect(*args): + """Create intersection of regular expressions. + >>> re = Intersect(Re("a"), Re("b"), Re("c")) + Intersect(Re("a"), Re("b"), Re("c")) + """ + args = _get_args(args) + sz = len(args) + if __debug__: + _z3_assert(sz > 0, "At least one argument expected.") + _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.") + if sz == 1: + return args[0] + ctx = args[0].ctx + v = (Ast * sz)() + for i in range(sz): + v[i] = args[i].as_ast() + return ReRef(Z3_mk_re_intersect(ctx.ref(), sz, v), ctx) + def Plus(re): """Create the regular expression accepting one or more repetitions of argument. >>> re = Plus(Re("a")) diff --git a/src/api/python/z3/z3printer.py b/src/api/python/z3/z3printer.py index 76614910f..5640ebcac 100644 --- a/src/api/python/z3/z3printer.py +++ b/src/api/python/z3/z3printer.py @@ -36,7 +36,15 @@ _z3_op_to_str = { Z3_OP_CONCAT : 'Concat', Z3_OP_EXTRACT : 'Extract', Z3_OP_BV2INT : 'BV2Int', Z3_OP_ARRAY_MAP : 'Map', Z3_OP_SELECT : 'Select', Z3_OP_STORE : 'Store', Z3_OP_CONST_ARRAY : 'K', Z3_OP_ARRAY_EXT : 'Ext', - Z3_OP_PB_AT_MOST : 'AtMost', Z3_OP_PB_LE : 'PbLe', Z3_OP_PB_GE : 'PbGe', Z3_OP_PB_EQ : 'PbEq' + Z3_OP_PB_AT_MOST : 'AtMost', Z3_OP_PB_LE : 'PbLe', Z3_OP_PB_GE : 'PbGe', Z3_OP_PB_EQ : 'PbEq', + Z3_OP_SEQ_CONCAT : 'Concat', Z3_OP_SEQ_PREFIX : 'PrefixOf', Z3_OP_SEQ_SUFFIX : 'SuffixOf', + Z3_OP_SEQ_UNIT : 'Unit', Z3_OP_SEQ_CONTAINS : 'Contains' , Z3_OP_SEQ_REPLACE : 'Replace', + Z3_OP_SEQ_AT : 'At', Z3_OP_SEQ_NTH : 'Nth', Z3_OP_SEQ_INDEX : 'IndexOf', + Z3_OP_SEQ_LAST_INDEX : 'LastIndexOf', Z3_OP_SEQ_LENGTH : 'Length', Z3_OP_STR_TO_INT : 'StrToInt', Z3_OP_INT_TO_STR : 'IntToStr', + Z3_OP_SEQ_IN_RE : 'InRe', Z3_OP_SEQ_TO_RE : 'Re', + Z3_OP_RE_PLUS : 'Plus', Z3_OP_RE_STAR : 'Star', Z3_OP_RE_OPTION : 'Option', Z3_OP_RE_UNION : 'Union', Z3_OP_RE_RANGE : 'Range', + Z3_OP_RE_INTERSECT : 'Intersect', Z3_OP_RE_COMPLEMENT : 'Complement', + } # List of infix operators @@ -486,7 +494,7 @@ class PP: def pp(self, f, indent): if isinstance(f, str): - sef.pp_string(f, indent) + self.pp_string(f, indent) elif f.is_string(): self.pp_string(f, indent) elif f.is_indent(): @@ -558,10 +566,23 @@ class Formatter: return seq1('BitVec', (to_format(s.size()), )) elif isinstance(s, z3.FPSortRef): return seq1('FPSort', (to_format(s.ebits()), to_format(s.sbits()))) + elif isinstance(s, z3.ReSortRef): + return seq1('ReSort', (self.pp_sort(s.basis()), )) + elif isinstance(s, z3.SeqSortRef): + if s.is_string(): + return to_format("String") + return seq1('Seq', (self.pp_sort(s.basis()), )) else: return to_format(s.name()) def pp_const(self, a): + k = a.decl().kind() + if k == Z3_OP_RE_EMPTY_SET: + return self.pp_set("Empty", a) + elif k == Z3_OP_SEQ_EMPTY: + return self.pp_set("Empty", a) + elif k == Z3_OP_RE_FULL_SET: + return self.pp_set("Full", a) return self.pp_name(a) def pp_int(self, a): @@ -577,7 +598,7 @@ class Formatter: return to_format(a.as_decimal(self.precision)) def pp_string(self, a): - return to_format(a.as_string()) + return to_format("\"" + a.as_string() + "\"") def pp_bv(self, a): return to_format(a.as_string()) @@ -842,6 +863,17 @@ class Formatter: arg = self.pp_expr(a.arg(0), d+1, xs) return seq1(self.pp_name(a), [ to_format(h), to_format(l), arg ]) + def pp_loop(self, a, d, xs): + l = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0) + arg = self.pp_expr(a.arg(0), d+1, xs) + if Z3_get_decl_num_parameters(a.ctx_ref(), a.decl().ast) > 1: + h = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 1) + return seq1("Loop", [ arg, to_format(l), to_format(h) ]) + return seq1("Loop", [ arg, to_format(l) ]) + + def pp_set(self, id, a): + return seq1(id, [self.pp_sort(a.sort())]) + def pp_pattern(self, a, d, xs): if a.num_args() == 1: return self.pp_expr(a.arg(0), d, xs) @@ -918,6 +950,8 @@ class Formatter: return self.pp_unary_param(a, d, xs) elif k == Z3_OP_EXTRACT: return self.pp_extract(a, d, xs) + elif k == Z3_OP_RE_LOOP: + return self.pp_loop(a, d, xs) elif k == Z3_OP_DT_IS: return self.pp_is(a, d, xs) elif k == Z3_OP_ARRAY_MAP: diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 7f1a1c70c..e17378d94 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -3292,6 +3292,13 @@ extern "C" { */ bool Z3_API Z3_is_seq_sort(Z3_context c, Z3_sort s); + /** + \brief Retrieve basis sort for sequence sort. + + def_API('Z3_get_seq_sort_basis', SORT, (_in(CONTEXT), _in(SORT))) + */ + Z3_sort Z3_API Z3_get_seq_sort_basis(Z3_context c, Z3_sort s); + /** \brief Create a regular expression sort out of a sequence sort. @@ -3306,6 +3313,13 @@ extern "C" { */ bool Z3_API Z3_is_re_sort(Z3_context c, Z3_sort s); + /** + \brief Retrieve basis sort for regex sort. + + def_API('Z3_get_re_sort_basis', SORT, (_in(CONTEXT), _in(SORT))) + */ + Z3_sort Z3_API Z3_get_re_sort_basis(Z3_context c, Z3_sort s); + /** \brief Create a sort for 8 bit strings. diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index fb8c48866..fab3be418 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -75,7 +75,7 @@ namespace sat { void model_converter::operator()(model & m) const { vector::const_iterator begin = m_entries.begin(); vector::const_iterator it = m_entries.end(); - bool first = false; // true; // false; // // true; + bool first = false; //SASSERT(!m_solver || m_solver->check_clauses(m)); while (it != begin) { --it; @@ -146,6 +146,10 @@ namespace sat { bool sat = false; for (literal l : it->m_clauses) { if (l == null_literal) { + CTRACE("sat", !sat, + display(tout); + for (unsigned v = 0; v < m.size(); ++v) tout << v << ": " << m[v] << "\n"; + ); SASSERT(sat); sat = false; continue; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 427077804..a0bd94303 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1608,6 +1608,7 @@ namespace sat { if (inconsistent()) break; assign_scoped(lit); } + propagate(false); TRACE("sat", for (literal a : m_assumptions) { index_set s; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 0cc829379..bd8a19044 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -879,6 +879,7 @@ private: mdl = nullptr; return; } + TRACE("sat", m_solver.display_model(tout);); sat::model const & ll_m = m_solver.get_model(); mdl = alloc(model, m); for (sat::bool_var v = 0; v < ll_m.size(); ++v) { @@ -899,11 +900,9 @@ private: } if (m_sat_mc) { - // IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "satmc\n");); (*m_sat_mc)(mdl); } if (m_mcs.back()) { - //IF_VERBOSE(0, m_mc0->display(verbose_stream() << "mc0\n");); (*m_mcs.back())(mdl); } TRACE("sat", model_smt2_pp(tout, m, *mdl, 0);); diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h index 78884051e..2177ca34d 100644 --- a/src/sat/tactic/goal2sat.h +++ b/src/sat/tactic/goal2sat.h @@ -88,7 +88,7 @@ public: mc(ast_manager& m); ~mc() override {} // flush model converter from SAT solver to this structure. - void flush_smc(sat::solver_core& s, atom2bool_var const& map); + void flush_smc(sat::solver_core& s, atom2bool_var const& map); void operator()(model_ref& md) override; void operator()(expr_ref& fml) override; model_converter* translate(ast_translation& translator) override;