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

getting duality to recover from incompleteness-related failures by restarting

Browse source
This commit is contained in:
Ken McMillan 2014-10-01 18:16:21 -07:00
parent c5f17df310
commit d54d758f45
2 changed files with 28 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/duality/duality_profiling.cpp
View file

@ -125,8 +125,18 @@ namespace Duality {
void timer_stop(const char *name){ void timer_stop(const char *name){
if(current->name != name || !current->parent){ if(current->name != name || !current->parent){
#if 0
std::cerr << "imbalanced timer_start and timer_stop"; std::cerr << "imbalanced timer_start and timer_stop";
exit(1); exit(1);
#endif
// in case we lost a timer stop due to an exception
while(current->name != name && current->parent)
current = current->parent;
if(current->parent){
current->time += (current_time() - current->start_time);
current = current->parent;
}
return;
} }
current->time += (current_time() - current->start_time); current->time += (current_time() - current->start_time);
current = current->parent; current = current->parent;

25
src/duality/duality_solver.cpp
View file

@ -2252,22 +2252,27 @@ namespace Duality {
int update_count = 0; int update_count = 0;
for(unsigned i = 0; i < expansions.size(); i++){ for(unsigned i = 0; i < expansions.size(); i++){
Node *node = expansions[i]; Node *node = expansions[i];
tree->SolveSingleNode(top,node);
#ifdef NO_GENERALIZE
node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
#else
try { try {
tree->SolveSingleNode(top,node);
#ifdef NO_GENERALIZE
node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
#else
if(expansions.size() == 1 && NodeTooComplicated(node)) if(expansions.size() == 1 && NodeTooComplicated(node))
SimplifyNode(node); SimplifyNode(node);
else else
node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify(); node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
Generalize(node); Generalize(node);
#endif
} }
catch(const RPFP::Bad &){ catch(const RPFP::Bad &){
// bad interpolants can get us here // bad interpolants can get us here
throw DoRestart(); throw DoRestart();
} }
#endif catch(char const *msg){
// bad interpolants can get us here
reporter->Message(std::string("interpolation failure:") + msg);
throw DoRestart();
}
if(RecordUpdate(node)){ if(RecordUpdate(node)){
update_count++; update_count++;
total_updates++; total_updates++;
@ -2283,8 +2288,14 @@ namespace Duality {
if(update_count == 0){ if(update_count == 0){
if(was_sat){ if(was_sat){
update_failures++; update_failures++;
if(update_failures > 10) if(update_failures > 10){
throw Incompleteness(); for(unsigned i = 0; i < expansions.size(); i++){
Node *node = expansions[i];
node->map->Annotation.SetFull();
reporter->Message("incompleteness: cleared annotation");
}
throw DoRestart();
}
} }
reporter->Message("backtracked without learning"); reporter->Message("backtracked without learning");
} }