mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Merge branch 'interp' of https://git01.codeplex.com/z3 into interp

Browse source
This commit is contained in:
Ken McMillan 2013-06-07 11:51:33 -07:00
commit b78752ef04
1 changed files with 14 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/duality/duality_solver.cpp
View file

@ -42,7 +42,7 @@ Revision History:
#define NEW_EXPAND
#define EARLY_EXPAND
// #define TOP_DOWN
#define EFFORT_BOUNDED_STRAT
// #define EFFORT_BOUNDED_STRAT
#define SKIP_UNDERAPPROX_NODES
@ -793,6 +793,18 @@ namespace Duality {
#endif
Edge *edge = node->map->Outgoing;
std::vector<Node *> &chs = edge->Children;
// make sure we don't create a covered node in this process!
for(unsigned i = 0; i < chs.size(); i++){
Node *child = chs[i];
if(TopoSort[child] < TopoSort[node->map]){
Node *leaf = LeafMap[child];
if(!indset->Contains(leaf))
return node->Outgoing;
}
}
std::vector<Node *> nchs(chs.size());
for(unsigned i = 0; i < chs.size(); i++){
Node *child = chs[i];
@ -808,6 +820,7 @@ namespace Duality {
if(StratifiedLeafMap.find(child) == StratifiedLeafMap.end()){
RPFP::Node *nchild = CreateNodeInstance(child,StratifiedLeafCount--);
MakeLeaf(nchild);
nchild->Annotation.SetEmpty();
StratifiedLeafMap[child] = nchild;
indset->SetDominated(nchild);
}