mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

fix #2640

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-10-16 20:40:03 -07:00
parent ca498e20d1
commit 4ce6b53d95
7 changed files with 190 additions and 150 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/ast/seq_decl_plugin.cpp
View file

@ -913,6 +913,11 @@ app* seq_decl_plugin::mk_string(zstring const& s) {
}
bool seq_decl_plugin::is_considered_uninterpreted(func_decl * f) {
seq_util util(*m_manager);
return util.str.is_nth_u(f);
}
bool seq_decl_plugin::is_value(app* e) const {
while (true) {
if (is_app_of(e, m_family_id, OP_SEQ_EMPTY)) {

1
src/ast/seq_decl_plugin.h
View file

@ -207,6 +207,7 @@ public:
bool has_re() const { return m_has_re; }
bool is_considered_uninterpreted(func_decl * f) override;
};
class seq_util {

50
src/model/model.cpp
View file

@ -29,6 +29,12 @@ Revision History:
#include "model/model.h"
#include "model/model_params.hpp"
#include "model/model_evaluator.h"
#include "model/array_factory.h"
#include "model/value_factory.h"
#include "model/seq_factory.h"
#include "model/datatype_factory.h"
#include "model/numeral_factory.h"
model::model(ast_manager & m):
model_core(m),
@ -88,40 +94,38 @@ bool model::eval_expr(expr * e, expr_ref & result, bool model_completion) {
}
}
struct model::value_proc : public some_value_proc {
model & m_model;
value_proc(model & m):m_model(m) {}
expr * operator()(sort * s) override {
ptr_vector<expr> * u = nullptr;
if (m_model.m_usort2universe.find(s, u)) {
if (!u->empty())
return u->get(0);
}
return nullptr;
}
};
value_factory* model::get_factory(sort* s) {
if (m_factories.plugins().empty()) {
seq_util su(m);
m_factories.register_plugin(alloc(array_factory, m, *this));
m_factories.register_plugin(alloc(datatype_factory, m, *this));
m_factories.register_plugin(alloc(bv_factory, m));
m_factories.register_plugin(alloc(arith_factory, m));
m_factories.register_plugin(alloc(seq_factory, m, su.get_family_id(), *this));
}
family_id fid = s->get_family_id();
return m_factories.get_plugin(fid);
}
expr * model::get_some_value(sort * s) {
value_proc p(*this);
return m.get_some_value(s, &p);
ptr_vector<expr> * u = nullptr;
if (m_usort2universe.find(s, u)) {
if (!u->empty())
return u->get(0);
}
return m.get_some_value(s);
}
expr * model::get_fresh_value(sort * s) {
value_proc p(*this);
return m.get_some_value(s, &p);
return get_factory(s)->get_fresh_value(s);
}
bool model::get_some_values(sort * s, expr_ref& v1, expr_ref& v2) {
v1 = get_some_value(s);
v2 = get_some_value(s);
return true;
return get_factory(s)->get_some_values(s, v1, v2);
}
ptr_vector<expr> const & model::get_universe(sort * s) const {
ptr_vector<expr> * u = nullptr;
m_usort2universe.find(s, u);
SASSERT(u != nullptr);
return *u;
return *m_usort2universe[s];
}
bool model::has_uninterpreted_sort(sort * s) const {

10
src/model/model.h
View file

@ -19,10 +19,13 @@ Revision History:
#ifndef MODEL_H_
#define MODEL_H_
#include "util/ref.h"
#include "util/vector.h"
#include "ast/ast_translation.h"
#include "util/plugin_manager.h"
#include "model/model_core.h"
#include "model/model_evaluator.h"
#include "util/ref.h"
#include "ast/ast_translation.h"
#include "model/value_factory.h"
class model;
typedef ref<model> model_ref;
@ -37,7 +40,7 @@ protected:
model_evaluator m_mev;
bool m_cleaned;
bool m_inline;
struct value_proc;
plugin_manager<value_factory> m_factories;
struct deps_collector;
struct occs_collector;
@ -52,6 +55,7 @@ protected:
expr_ref cleanup_expr(top_sort& ts, expr* e, unsigned current_partition);
void remove_decls(ptr_vector<func_decl> & decls, func_decl_set const & s);
bool can_inline_def(top_sort& ts, func_decl* f);
value_factory* get_factory(sort* s);
public:
model(ast_manager & m);

149
src/model/seq_factory.h Normal file
View file

@ -0,0 +1,149 @@
/*++
Copyright (c) 2011 Microsoft Corporation
Module Name:
theory_seq_empty.h
Abstract:
<abstract>
Author:
Nikolaj Bjorner (nbjorner) 2011-14-11
Revision History:
--*/
#ifndef SEQ_FACTORY_H_
#define SEQ_FACTORY_H_
#include "ast/seq_decl_plugin.h"
#include "model/model_core.h"
class seq_factory : public value_factory {
typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> symbol_set;
model_core& m_model;
ast_manager& m;
seq_util u;
symbol_set m_strings;
unsigned m_next;
std::string m_unique_delim;
obj_map<sort, expr*> m_unique_sequences;
expr_ref_vector m_trail;
public:
seq_factory(ast_manager & m, family_id fid, model_core& md):
value_factory(m, fid),
m_model(md),
m(m),
u(m),
m_next(0),
m_unique_delim("!"),
m_trail(m)
{
m_strings.insert(symbol(""));
m_strings.insert(symbol("a"));
m_strings.insert(symbol("b"));
}
void add_trail(expr* e) {
m_trail.push_back(e);
}
void set_prefix(char const* p) {
m_unique_delim = p;
}
// generic method for setting unique sequences
void set_prefix(expr* uniq) {
m_trail.push_back(uniq);
m_unique_sequences.insert(m.get_sort(uniq), uniq);
}
expr* get_some_value(sort* s) override {
if (u.is_seq(s)) {
return u.str.mk_empty(s);
}
sort* seq = nullptr;
if (u.is_re(s, seq)) {
return u.re.mk_to_re(u.str.mk_empty(seq));
}
UNREACHABLE();
return nullptr;
}
bool get_some_values(sort* s, expr_ref& v1, expr_ref& v2) override {
if (u.is_string(s)) {
v1 = u.str.mk_string(symbol("a"));
v2 = u.str.mk_string(symbol("b"));
return true;
}
sort* ch;
if (u.is_seq(s, ch)) {
if (m_model.get_some_values(ch, v1, v2)) {
v1 = u.str.mk_unit(v1);
v2 = u.str.mk_unit(v2);
return true;
}
else {
return false;
}
}
NOT_IMPLEMENTED_YET();
return false;
}
expr* get_fresh_value(sort* s) override {
if (u.is_string(s)) {
while (true) {
std::ostringstream strm;
strm << m_unique_delim << std::hex << m_next++ << std::dec << m_unique_delim;
symbol sym(strm.str().c_str());
if (m_strings.contains(sym)) continue;
m_strings.insert(sym);
return u.str.mk_string(sym);
}
}
sort* seq = nullptr, *ch = nullptr;
if (u.is_re(s, seq)) {
expr* v0 = get_fresh_value(seq);
return u.re.mk_to_re(v0);
}
if (u.is_char(s)) {
//char s[2] = { ++m_char, 0 };
//return u.str.mk_char(zstring(s), 0);
return u.str.mk_char(zstring("a"), 0);
}
if (u.is_seq(s, ch)) {
expr* v = m_model.get_fresh_value(ch);
if (!v) return nullptr;
return u.str.mk_unit(v);
}
UNREACHABLE();
return nullptr;
}
void register_value(expr* n) override {
symbol sym;
if (u.str.is_string(n, sym)) {
m_strings.insert(sym);
if (sym.str().find(m_unique_delim) != std::string::npos) {
add_new_delim();
}
}
}
private:
void add_new_delim() {
bool found = true;
while (found) {
found = false;
m_unique_delim += "!";
symbol_set::iterator it = m_strings.begin(), end = m_strings.end();
for (; it != end && !found; ++it) {
found = it->str().find(m_unique_delim) != std::string::npos;
}
}
}
};
#endif

1
src/smt/proto_model/proto_model.h
View file

@ -31,7 +31,6 @@ Revision History:
#include "model/model_core.h"
#include "model/model_evaluator.h"
#include "model/value_factory.h"
#include "util/plugin_manager.h"
#include "ast/arith_decl_plugin.h"
#include "ast/func_decl_dependencies.h"
#include "model/model.h"

124
src/smt/theory_seq_empty.h
View file

@ -21,131 +21,9 @@ Revision History:
#include "smt/smt_theory.h"
#include "ast/seq_decl_plugin.h"
#include "model/seq_factory.h"
namespace smt {
class seq_factory : public value_factory {
typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> symbol_set;
proto_model& m_model;
ast_manager& m;
seq_util u;
symbol_set m_strings;
unsigned m_next;
std::string m_unique_delim;
obj_map<sort, expr*> m_unique_sequences;
expr_ref_vector m_trail;
public:
seq_factory(ast_manager & m, family_id fid, proto_model& md):
value_factory(m, fid),
m_model(md),
m(m),
u(m),
m_next(0),
m_unique_delim("!"),
m_trail(m)
{
m_strings.insert(symbol(""));
m_strings.insert(symbol("a"));
m_strings.insert(symbol("b"));
}
void add_trail(expr* e) {
m_trail.push_back(e);
}
void set_prefix(char const* p) {
m_unique_delim = p;
}
// generic method for setting unique sequences
void set_prefix(expr* uniq) {
m_trail.push_back(uniq);
m_unique_sequences.insert(m.get_sort(uniq), uniq);
}
expr* get_some_value(sort* s) override {
if (u.is_seq(s)) {
return u.str.mk_empty(s);
}
sort* seq = nullptr;
if (u.is_re(s, seq)) {
return u.re.mk_to_re(u.str.mk_empty(seq));
}
UNREACHABLE();
return nullptr;
}
bool get_some_values(sort* s, expr_ref& v1, expr_ref& v2) override {
if (u.is_string(s)) {
v1 = u.str.mk_string(symbol("a"));
v2 = u.str.mk_string(symbol("b"));
return true;
}
sort* ch;
if (u.is_seq(s, ch)) {
if (m_model.get_some_values(ch, v1, v2)) {
v1 = u.str.mk_unit(v1);
v2 = u.str.mk_unit(v2);
return true;
}
else {
return false;
}
}
NOT_IMPLEMENTED_YET();
return false;
}
expr* get_fresh_value(sort* s) override {
if (u.is_string(s)) {
while (true) {
std::ostringstream strm;
strm << m_unique_delim << std::hex << m_next++ << std::dec << m_unique_delim;
symbol sym(strm.str().c_str());
if (m_strings.contains(sym)) continue;
m_strings.insert(sym);
return u.str.mk_string(sym);
}
}
sort* seq = nullptr, *ch = nullptr;
if (u.is_re(s, seq)) {
expr* v0 = get_fresh_value(seq);
return u.re.mk_to_re(v0);
}
if (u.is_char(s)) {
//char s[2] = { ++m_char, 0 };
//return u.str.mk_char(zstring(s), 0);
return u.str.mk_char(zstring("a"), 0);
}
if (u.is_seq(s, ch)) {
expr* v = m_model.get_fresh_value(ch);
if (!v) return nullptr;
return u.str.mk_unit(v);
}
UNREACHABLE();
return nullptr;
}
void register_value(expr* n) override {
symbol sym;
if (u.str.is_string(n, sym)) {
m_strings.insert(sym);
if (sym.str().find(m_unique_delim) != std::string::npos) {
add_new_delim();
}
}
}
private:
void add_new_delim() {
bool found = true;
while (found) {
found = false;
m_unique_delim += "!";
symbol_set::iterator it = m_strings.begin(), end = m_strings.end();
for (; it != end && !found; ++it) {
found = it->str().find(m_unique_delim) != std::string::npos;
}
}
}
};
class theory_seq_empty : public theory {
bool m_used;