mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

completing user print experience with seq/re #2200

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-03-24 11:46:36 -07:00
parent fca8ffd948
commit dc0e9c1919
9 changed files with 115 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/api_ast.cpp
View file

@ -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;

26
src/api/api_seq.cpp
View file

@ -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);

30
src/api/python/z3/z3.py
View file

@ -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"))

40
src/api/python/z3/z3printer.py
View file

@ -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:

14
src/api/z3_api.h
View file

@ -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.

6
src/sat/sat_model_converter.cpp
View file

@ -75,7 +75,7 @@ namespace sat {
void model_converter::operator()(model & m) const {
vector<entry>::const_iterator begin = m_entries.begin();
vector<entry>::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;

1
src/sat/sat_solver.cpp
View file

@ -1608,6 +1608,7 @@ namespace sat {
if (inconsistent()) break;
assign_scoped(lit);
}
propagate(false);
TRACE("sat",
for (literal a : m_assumptions) {
index_set s;

3
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -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););

2
src/sat/tactic/goal2sat.h
View file

@ -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;