mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

use skolem function to avoid exposing temporary variables in models

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-07 14:03:24 -07:00
parent 82bdd26817
commit e02392c0e3
2 changed files with 10 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/smt/theory_str.cpp
View file

@ -440,6 +440,11 @@ namespace smt {
return mk_int_var("$$_xor"); return mk_int_var("$$_xor");
} }
app * theory_str::mk_fresh_const(char const* name, sort* s) {
return u.mk_skolem(symbol(name), 0, 0, s);
}
app * theory_str::mk_int_var(std::string name) { app * theory_str::mk_int_var(std::string name) {
context & ctx = get_context(); context & ctx = get_context();
ast_manager & m = get_manager(); ast_manager & m = get_manager();
@ -447,7 +452,7 @@ namespace smt {
TRACE("str", tout << "creating integer variable " << name << " at scope level " << sLevel << std::endl;); TRACE("str", tout << "creating integer variable " << name << " at scope level " << sLevel << std::endl;);
sort * int_sort = m.mk_sort(m_autil.get_family_id(), INT_SORT); sort * int_sort = m.mk_sort(m_autil.get_family_id(), INT_SORT);
app * a = m.mk_fresh_const(name.c_str(), int_sort); app * a = mk_fresh_const(name.c_str(), int_sort);
ctx.internalize(a, false); ctx.internalize(a, false);
SASSERT(ctx.get_enode(a) != NULL); SASSERT(ctx.get_enode(a) != NULL);
@ -482,7 +487,7 @@ namespace smt {
TRACE("str", tout << "creating string variable " << name << " at scope level " << sLevel << std::endl;); TRACE("str", tout << "creating string variable " << name << " at scope level " << sLevel << std::endl;);
sort * string_sort = u.str.mk_string_sort(); sort * string_sort = u.str.mk_string_sort();
app * a = m.mk_fresh_const(name.c_str(), string_sort); app * a = mk_fresh_const(name.c_str(), string_sort);
TRACE("str", tout << "a->get_family_id() = " << a->get_family_id() << std::endl TRACE("str", tout << "a->get_family_id() = " << a->get_family_id() << std::endl
<< "this->get_family_id() = " << this->get_family_id() << std::endl;); << "this->get_family_id() = " << this->get_family_id() << std::endl;);
@ -509,7 +514,7 @@ namespace smt {
ast_manager & m = get_manager(); ast_manager & m = get_manager();
sort * string_sort = u.str.mk_string_sort(); sort * string_sort = u.str.mk_string_sort();
app * a = m.mk_fresh_const("regex", string_sort); app * a = mk_fresh_const("regex", string_sort);
ctx.internalize(a, false); ctx.internalize(a, false);
SASSERT(ctx.get_enode(a) != NULL); SASSERT(ctx.get_enode(a) != NULL);
@ -561,7 +566,7 @@ namespace smt {
TRACE("str", tout << "creating nonempty string variable " << name << " at scope level " << sLevel << std::endl;); TRACE("str", tout << "creating nonempty string variable " << name << " at scope level " << sLevel << std::endl;);
sort * string_sort = u.str.mk_string_sort(); sort * string_sort = u.str.mk_string_sort();
app * a = m.mk_fresh_const(name.c_str(), string_sort); app * a = mk_fresh_const(name.c_str(), string_sort);
ctx.internalize(a, false); ctx.internalize(a, false);
SASSERT(ctx.get_enode(a) != NULL); SASSERT(ctx.get_enode(a) != NULL);

1
src/smt/theory_str.h
View file

@ -403,6 +403,7 @@ protected:
expr * mk_concat_const_str(expr * n1, expr * n2); expr * mk_concat_const_str(expr * n1, expr * n2);
app * mk_contains(expr * haystack, expr * needle); app * mk_contains(expr * haystack, expr * needle);
app * mk_indexof(expr * haystack, expr * needle); app * mk_indexof(expr * haystack, expr * needle);
app * mk_fresh_const(char const* name, sort* s);
literal mk_literal(expr* _e); literal mk_literal(expr* _e);
app * mk_int(int n); app * mk_int(int n);