mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

fix markers aliasing bug in Duality::CheckerForEdgeClone

Browse source
This commit is contained in:
Ken McMillan 2014-05-20 15:10:31 -07:00
parent b91cca8db9
commit 01c6fe39ab
1 changed files with 13 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/duality/duality_solver.cpp
View file

@ -738,6 +738,13 @@ namespace Duality {
return ctx.constant(name.c_str(),ctx.bool_sort()); return ctx.constant(name.c_str(),ctx.bool_sort());
} }
/** Make a boolean variable to act as a "marker" for a pair of nodes. */
expr NodeMarker(Node *node1, Node *node2){
std::string name = std::string("@m_") + string_of_int(node1->number);
name += std::string("_") + string_of_int(node2->number);
return ctx.constant(name.c_str(),ctx.bool_sort());
}
/** Union the annotation of dst into src. If with_markers is /** Union the annotation of dst into src. If with_markers is
true, we conjoin the annotation formula of dst with its true, we conjoin the annotation formula of dst with its
marker. This allows us to discover which disjunct is marker. This allows us to discover which disjunct is
@ -1146,19 +1153,19 @@ namespace Duality {
} }
void GenNodeSolutionWithMarkersAux(Node *node, RPFP::Transformer &annot, expr &marker_disjunction){ void GenNodeSolutionWithMarkersAux(Node *node, RPFP::Transformer &annot, expr &marker_disjunction, Node *other_node){
#ifdef BOUNDED #ifdef BOUNDED
if(RecursionBound >= 0 && NodePastRecursionBound(node)) if(RecursionBound >= 0 && NodePastRecursionBound(node))
return; return;
#endif #endif
RPFP::Transformer temp = node->Annotation; RPFP::Transformer temp = node->Annotation;
expr marker = NodeMarker(node); expr marker = (!other_node) ? NodeMarker(node) : NodeMarker(node, other_node);
temp.Formula = (!marker || temp.Formula); temp.Formula = (!marker || temp.Formula);
annot.IntersectWith(temp); annot.IntersectWith(temp);
marker_disjunction = marker_disjunction || marker; marker_disjunction = marker_disjunction || marker;
} }
bool GenNodeSolutionWithMarkers(Node *node, RPFP::Transformer &annot, bool expanded_only = false){ bool GenNodeSolutionWithMarkers(Node *node, RPFP::Transformer &annot, bool expanded_only = false, Node *other_node = 0){
bool res = false; bool res = false;
annot.SetFull(); annot.SetFull();
expr marker_disjunction = ctx.bool_val(false); expr marker_disjunction = ctx.bool_val(false);
@ -1166,7 +1173,7 @@ namespace Duality {
for(unsigned j = 0; j < insts.size(); j++){ for(unsigned j = 0; j < insts.size(); j++){
Node *node = insts[j]; Node *node = insts[j];
if(indset->Contains(insts[j])){ if(indset->Contains(insts[j])){
GenNodeSolutionWithMarkersAux(node, annot, marker_disjunction); res = true; GenNodeSolutionWithMarkersAux(node, annot, marker_disjunction, other_node); res = true;
} }
} }
annot.Formula = annot.Formula && marker_disjunction; annot.Formula = annot.Formula && marker_disjunction;
@ -1263,7 +1270,7 @@ namespace Duality {
Node *inst = insts[k]; Node *inst = insts[k];
if(indset->Contains(inst)){ if(indset->Contains(inst)){
if(checker->Empty(node) || if(checker->Empty(node) ||
eq(lb ? checker->Eval(lb,NodeMarker(inst)) : checker->dualModel.eval(NodeMarker(inst)),ctx.bool_val(true))){ eq(lb ? checker->Eval(lb,NodeMarker(inst)) : checker->dualModel.eval(NodeMarker(inst,node)),ctx.bool_val(true))){
candidate.Children.push_back(inst); candidate.Children.push_back(inst);
goto next_child; goto next_child;
} }
@ -1346,7 +1353,7 @@ namespace Duality {
for(unsigned j = 0; j < edge->Children.size(); j++){ for(unsigned j = 0; j < edge->Children.size(); j++){
Node *oc = edge->Children[j]; Node *oc = edge->Children[j];
Node *nc = gen_cands_edge->Children[j]; Node *nc = gen_cands_edge->Children[j];
GenNodeSolutionWithMarkers(oc,nc->Annotation,true); GenNodeSolutionWithMarkers(oc,nc->Annotation,true,nc);
} }
checker->AssertEdge(gen_cands_edge,1,true); checker->AssertEdge(gen_cands_edge,1,true);
return root; return root;