mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 07:13:41 +00:00
Code Activity

completed process_free_var(), still WIP

Browse source 
working on gen_len_val_options_for_free_var()
This commit is contained in:
Murphy Berzish 2015-11-09 15:33:52 -05:00
parent a9b8707d48
commit 0178872a19
2 changed files with 41 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

40
src/smt/theory_str.cpp
View file

@ -2385,6 +2385,14 @@ void theory_str::set_up_axioms(expr * ex) {
if (is_concat(ap)) { if (is_concat(ap)) {
// if ex is a concat, set up concat axioms later // if ex is a concat, set up concat axioms later
m_concat_axiom_todo.push_back(n); m_concat_axiom_todo.push_back(n);
} else if (is_strlen(ap)) {
// if the argument is a variable,
// keep track of this for later, we'll need it during model gen
expr * var = ap->get_arg(0);
app * aVar = to_app(var);
if (aVar->get_num_args() == 0 && !is_string(aVar)) {
input_var_in_len.insert(var);
}
} else if (ap->get_num_args() == 0 && !is_string(ap)) { } else if (ap->get_num_args() == 0 && !is_string(ap)) {
// if ex is a variable, add it to our list of variables // if ex is a variable, add it to our list of variables
TRACE("t_str_detail", tout << "tracking variable" << std::endl;); TRACE("t_str_detail", tout << "tracking variable" << std::endl;);
@ -3419,6 +3427,20 @@ expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTe
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
} }
void theory_str::get_var_in_eqc(expr * n, std::set<expr*> & varSet) {
context & ctx = get_context();
expr * eqcNode = n;
do {
if (variable_set.find(eqcNode) != variable_set.end()) {
varSet.insert(eqcNode);
}
enode * e_eqc = ctx.get_enode(eqcNode);
eqcNode = e_eqc->get_next()->get_owner();
// eqcNode = Z3_theory_get_eqc_next(t, eqcNode);
} while (eqcNode != n);
}
void theory_str::process_free_var(std::map<expr*, int> & freeVar_map) { void theory_str::process_free_var(std::map<expr*, int> & freeVar_map) {
context & ctx = get_context(); context & ctx = get_context();
ast_manager & m = get_manager(); ast_manager & m = get_manager();
@ -3494,8 +3516,22 @@ void theory_str::process_free_var(std::map<expr*, int> & freeVar_map) {
} }
} }
// TODO the rest // TODO here's a great place for debugging info
NOT_IMPLEMENTED_YET();
for(std::set<expr*>::iterator itor1 = leafVarSet.begin();
itor1 != leafVarSet.end(); ++itor1) {
expr * toAssert = gen_len_val_options_for_free_var(*itor1, NULL, "");
assert_axiom(toAssert);
}
for (std::map<int, std::set<expr*> >::iterator mItor = aloneVars.begin();
mItor != aloneVars.end(); ++mItor) {
std::set<expr*>::iterator itor2 = mItor->second.begin();
for(; itor2 != mItor->second.end(); ++itor2) {
expr * toAssert = gen_len_val_options_for_free_var(*itor2, NULL, "");
assert_axiom(toAssert);
}
}
} }
/* /*

3
src/smt/theory_str.h
View file

@ -82,6 +82,8 @@ namespace smt {
std::set<expr*> variable_set; std::set<expr*> variable_set;
std::set<expr*> internal_variable_set; std::set<expr*> internal_variable_set;
std::set<expr*> input_var_in_len;
protected: protected:
void assert_axiom(expr * e); void assert_axiom(expr * e);
void assert_implication(expr * premise, expr * conclusion); void assert_implication(expr * premise, expr * conclusion);
@ -159,6 +161,7 @@ namespace smt {
expr * get_alias_index_ast(std::map<expr*, expr*> & aliasIndexMap, expr * node); expr * get_alias_index_ast(std::map<expr*, expr*> & aliasIndexMap, expr * node);
expr * getMostLeftNodeInConcat(expr * node); expr * getMostLeftNodeInConcat(expr * node);
expr * getMostRightNodeInConcat(expr * node); expr * getMostRightNodeInConcat(expr * node);
void get_var_in_eqc(expr * n, std::set<expr*> & varSet);
// strRegex // strRegex