mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

add model construction for disequations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-01-11 16:53:29 -08:00
parent 79a5b133d7
commit e22ac712b0
3 changed files with 25 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/smt/theory_seq.cpp
View file

@ -551,9 +551,6 @@ bool theory_seq::is_solved() {
IF_VERBOSE(10, verbose_stream() << "(seq.giveup " << m_eqs[0].ls() << " = " << m_eqs[0].rs() << " is unsolved)\n";);
return false;
}
if (!m_nqs.empty()) {
return false;
}
for (unsigned i = 0; i < m_automata.size(); ++i) {
if (!m_automata[i]) {
IF_VERBOSE(10, verbose_stream() << "(seq.giveup regular expression did not compile to automaton)\n";);
@ -1252,9 +1249,28 @@ void theory_seq::collect_statistics(::statistics & st) const {
st.update("seq add axiom", m_stats.m_add_axiom);
}
void theory_seq::init_model(expr_ref_vector const& es) {
expr_ref new_s(m);
for (unsigned i = 0; i < es.size(); ++i) {
dependency* eqs = 0;
expr_ref s = canonize(es[i], eqs);
if (is_var(s)) {
new_s = m_factory->get_fresh_value(m.get_sort(s));
m_rep.update(s, new_s, eqs);
}
}
}
void theory_seq::init_model(model_generator & mg) {
m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model());
mg.register_factory(m_factory);
for (unsigned j = 0; j < m_nqs.size(); ++j) {
ne const& n = m_nqs[j];
for (unsigned i = 0; i < n.ls().size(); ++i) {
init_model(n.ls(i));
init_model(n.rs(i));
}
}
}
@ -2182,7 +2198,7 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
m_rewrite(eq);
if (!m.is_false(eq)) {
literal lit = ~mk_eq(e1, e2, false);
SASSERT(get_context().get_assignment(lit) == l_true);
//SASSERT(get_context().get_assignment(lit) == l_true);
dependency* dep = m_dm.mk_leaf(assumption(lit));
m_nqs.push_back(ne(e1, e2, dep));
solve_nqs(m_nqs.size() - 1);

1
src/smt/theory_seq.h
View file

@ -301,6 +301,7 @@ namespace smt {
virtual model_value_proc * mk_value(enode * n, model_generator & mg);
virtual void init_model(model_generator & mg);
void init_model(expr_ref_vector const& es);
// final check
bool simplify_and_solve_eqs(); // solve unitary equalities
bool branch_variable(); // branch on a variable

8
src/smt/theory_seq_empty.h
View file

@ -31,7 +31,7 @@ namespace smt {
symbol_set m_strings;
unsigned m_next;
char m_char;
std::string m_unique_prefix;
std::string m_unique_delim;
obj_map<sort, expr*> m_unique_sequences;
expr_ref_vector m_trail;
public:
@ -43,7 +43,7 @@ namespace smt {
u(m),
m_next(0),
m_char(0),
m_unique_prefix("#B"),
m_unique_delim("!"),
m_trail(m)
{
m_strings.insert(symbol(""));
@ -56,7 +56,7 @@ namespace smt {
}
void set_prefix(char const* p) {
m_unique_prefix = p;
m_unique_delim = p;
}
// generic method for setting unique sequences
@ -89,7 +89,7 @@ namespace smt {
if (u.is_string(s)) {
while (true) {
std::ostringstream strm;
strm << m_unique_prefix << m_next++;
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);