mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fix #1534

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-12 13:21:31 -07:00
parent 3d9139f6ef
commit 5651d00751
3 changed files with 23 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/math/polynomial/upolynomial.cpp
View file

@ -781,17 +781,15 @@ namespace upolynomial {
set(q.size(), q.c_ptr(), C);
m().set(bound, p);
}
else if (q.size() < C.size() || m().m().is_even(p) || m().m().is_even(bound)) {
// discard accumulated image, it was affected by unlucky primes
TRACE("mgcd", tout << "discarding image\n";);
set(q.size(), q.c_ptr(), C);
m().set(bound, p);
}
else {
if (q.size() < C.size()) {
// discard accumulated image, it was affected by unlucky primes
TRACE("mgcd", tout << "discarding image\n";);
set(q.size(), q.c_ptr(), C);
m().set(bound, p);
}
else {
CRA_combine_images(q, p, C, bound);
TRACE("mgcd", tout << "new combined:\n"; display_star(tout, C); tout << "\n";);
}
CRA_combine_images(q, p, C, bound);
TRACE("mgcd", tout << "new combined:\n"; display_star(tout, C); tout << "\n";);
}
numeral_vector & candidate = q;
get_primitive(C, candidate);

18
src/smt/theory_str.cpp
View file

@ -5553,7 +5553,8 @@ namespace smt {
return node;
}
void theory_str::get_grounded_concats(expr* node, std::map<expr*, expr*> & varAliasMap,
void theory_str::get_grounded_concats(unsigned depth,
expr* node, std::map<expr*, expr*> & varAliasMap,
std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr*> & varConstMap,
std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap,
std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap) {
@ -5568,6 +5569,9 @@ namespace smt {
if (groundedMap.find(node) != groundedMap.end()) {
return;
}
IF_VERBOSE(100, verbose_stream() << "concats " << depth << "\n";
if (depth > 100) verbose_stream() << mk_pp(node, get_manager()) << "\n";
);
// haven't computed grounded concats for "node" (de-aliased)
// ---------------------------------------------------------
@ -5595,12 +5599,10 @@ namespace smt {
// merge arg0 and arg1
expr * arg0 = to_app(node)->get_arg(0);
expr * arg1 = to_app(node)->get_arg(1);
SASSERT(arg0 != node);
SASSERT(arg1 != node);
expr * arg0DeAlias = dealias_node(arg0, varAliasMap, concatAliasMap);
expr * arg1DeAlias = dealias_node(arg1, varAliasMap, concatAliasMap);
get_grounded_concats(arg0DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
get_grounded_concats(arg1DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
get_grounded_concats(depth + 1, arg0DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
get_grounded_concats(depth + 1, arg1DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
std::map<std::vector<expr*>, std::set<expr*> >::iterator arg0_grdItor = groundedMap[arg0DeAlias].begin();
std::map<std::vector<expr*>, std::set<expr*> >::iterator arg1_grdItor;
@ -5650,7 +5652,7 @@ namespace smt {
else if (varEqConcatMap.find(node) != varEqConcatMap.end()) {
expr * eqConcat = varEqConcatMap[node].begin()->first;
expr * deAliasedEqConcat = dealias_node(eqConcat, varAliasMap, concatAliasMap);
get_grounded_concats(deAliasedEqConcat, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
get_grounded_concats(depth + 1, deAliasedEqConcat, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
std::map<std::vector<expr*>, std::set<expr*> >::iterator grdItor = groundedMap[deAliasedEqConcat].begin();
for (; grdItor != groundedMap[deAliasedEqConcat].end(); grdItor++) {
@ -5859,8 +5861,8 @@ namespace smt {
expr* strDeAlias = dealias_node(str, varAliasMap, concatAliasMap);
expr* subStrDeAlias = dealias_node(subStr, varAliasMap, concatAliasMap);
get_grounded_concats(strDeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
get_grounded_concats(subStrDeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
get_grounded_concats(0, strDeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
get_grounded_concats(0, subStrDeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
// debugging
print_grounded_concat(strDeAlias, groundedMap);

9
src/smt/theory_str.h
View file

@ -495,10 +495,11 @@ protected:
std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr *> & varConstMap,
std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap);
expr * dealias_node(expr * node, std::map<expr*, expr*> & varAliasMap, std::map<expr*, expr*> & concatAliasMap);
void get_grounded_concats(expr* node, std::map<expr*, expr*> & varAliasMap,
std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr*> & varConstMap,
std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap,
std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
void get_grounded_concats(unsigned depth,
expr* node, std::map<expr*, expr*> & varAliasMap,
std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr*> & varConstMap,
std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap,
std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
void print_grounded_concat(expr * node, std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
void check_subsequence(expr* str, expr* strDeAlias, expr* subStr, expr* subStrDeAlias, expr* boolVar,
std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);