3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

duality: added restarts

This commit is contained in:
Ken McMillan 2014-03-16 15:37:19 -07:00
parent 663d110b72
commit 2417b75d8d
3 changed files with 120 additions and 27 deletions

View file

@ -746,6 +746,10 @@ protected:
struct bad_format {
};
// thrown on internal error
struct Bad {
};
/** Pop a scope (see Push). Note, you cannot pop axioms. */
void Pop(int num_scopes);

View file

@ -2954,6 +2954,8 @@ namespace Duality {
}
}
static int by_case_counter = 0;
void RPFP::InterpolateByCases(Node *root, Node *node){
timer_start("InterpolateByCases");
bool axioms_added = false;
@ -2968,6 +2970,7 @@ namespace Duality {
hash_set<ast> *core = new hash_set<ast>;
core->insert(node->Outgoing->dual);
while(1){
by_case_counter++;
is.push();
expr annot = !GetAnnotation(node);
is.add(annot);
@ -3009,6 +3012,23 @@ namespace Duality {
for(unsigned i = 0; i < axioms_to_add.size(); i++)
is.add(axioms_to_add[i]);
#define TEST_BAD
#ifdef TEST_BAD
{
static int bad_count = 0, num_bads = 1;
if(bad_count >= num_bads){
bad_count = 0;
num_bads = num_bads * 2;
Pop(1);
is.pop(1);
delete core;
timer_stop("InterpolateByCases");
throw Bad();
}
bad_count++;
}
#endif
if(node->Annotation.IsEmpty()){
if(!axioms_added){
// add the axioms in the off chance they are useful
@ -3018,12 +3038,48 @@ namespace Duality {
axioms_added = true;
}
else {
#ifdef KILL_ON_BAD_INTERPOLANT
std::cout << "bad in InterpolateByCase -- core:\n";
#if 0
std::vector<expr> assumps;
slvr().get_proof().get_assumptions(assumps);
for(unsigned i = 0; i < assumps.size(); i++)
assumps[i].show();
#endif
std::cout << "checking for inconsistency\n";
std::cout << "model:\n";
is.get_model().show();
expr impl = is.get_implicant();
std::vector<expr> conjuncts;
CollectConjuncts(impl,conjuncts,true);
std::cout << "impl:\n";
for(unsigned i = 0; i < conjuncts.size(); i++)
conjuncts[i].show();
std::cout << "annot:\n";
annot.show();
is.add(annot);
for(unsigned i = 0; i < conjuncts.size(); i++)
is.add(conjuncts[i]);
if(is.check() == unsat){
std::cout << "inconsistent!\n";
std::vector<expr> is_assumps;
is.aux_solver.get_proof().get_assumptions(is_assumps);
std::cout << "core:\n";
for(unsigned i = 0; i < is_assumps.size(); i++)
is_assumps[i].show();
}
else {
std::cout << "consistent!\n";
is.aux_solver.print("should_be_inconsistent.smt2");
}
std::cout << "by_case_counter = " << by_case_counter << "\n";
throw "ack!";
#endif
Pop(1);
is.pop(1);
delete core;
timer_stop("InterpolateByCases");
throw Bad();
}
}
Pop(1);

View file

@ -2078,7 +2078,24 @@ namespace Duality {
stack.push_back(stack_entry());
}
struct DoRestart {};
virtual bool Build(){
while (true) {
try {
return BuildMain();
}
catch (const DoRestart &) {
// clear the statck and try again
updated_nodes.clear();
while(stack.size() > 1)
PopLevel();
reporter->Message("restarted");
}
}
}
bool BuildMain(){
stack.back().level = tree->slvr().get_scope_level();
bool was_sat = true;
@ -2110,11 +2127,17 @@ namespace Duality {
#ifdef NO_GENERALIZE
node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
#else
if(expansions.size() == 1 && NodeTooComplicated(node))
SimplifyNode(node);
else
node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
Generalize(node);
try {
if(expansions.size() == 1 && NodeTooComplicated(node))
SimplifyNode(node);
else
node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify();
Generalize(node);
}
catch(const RPFP::Bad &){
// bad interpolants can get us here
throw DoRestart();
}
#endif
if(RecordUpdate(node))
update_count++;
@ -2134,28 +2157,8 @@ namespace Duality {
tree->ComputeProofCore(); // need to compute the proof core before popping solver
bool propagated = false;
while(1) {
std::vector<Node *> &expansions = stack.back().expansions;
bool prev_level_used = LevelUsedInProof(stack.size()-2); // need to compute this before pop
tree->Pop(1);
hash_set<Node *> leaves_to_remove;
for(unsigned i = 0; i < expansions.size(); i++){
Node *node = expansions[i];
// if(node != top)
// tree->ConstrainParent(node->Incoming[0],node);
std::vector<Node *> &cs = node->Outgoing->Children;
for(unsigned i = 0; i < cs.size(); i++){
leaves_to_remove.insert(cs[i]);
UnmapNode(cs[i]);
if(std::find(updated_nodes.begin(),updated_nodes.end(),cs[i]) != updated_nodes.end())
throw "help!";
}
}
RemoveLeaves(leaves_to_remove); // have to do this before actually deleting the children
for(unsigned i = 0; i < expansions.size(); i++){
Node *node = expansions[i];
RemoveExpansion(node);
}
stack.pop_back();
PopLevel();
if(stack.size() == 1)break;
if(prev_level_used){
Node *node = stack.back().expansions[0];
@ -2213,6 +2216,30 @@ namespace Duality {
}
}
void PopLevel(){
std::vector<Node *> &expansions = stack.back().expansions;
tree->Pop(1);
hash_set<Node *> leaves_to_remove;
for(unsigned i = 0; i < expansions.size(); i++){
Node *node = expansions[i];
// if(node != top)
// tree->ConstrainParent(node->Incoming[0],node);
std::vector<Node *> &cs = node->Outgoing->Children;
for(unsigned i = 0; i < cs.size(); i++){
leaves_to_remove.insert(cs[i]);
UnmapNode(cs[i]);
if(std::find(updated_nodes.begin(),updated_nodes.end(),cs[i]) != updated_nodes.end())
throw "help!";
}
}
RemoveLeaves(leaves_to_remove); // have to do this before actually deleting the children
for(unsigned i = 0; i < expansions.size(); i++){
Node *node = expansions[i];
RemoveExpansion(node);
}
stack.pop_back();
}
bool NodeTooComplicated(Node *node){
int ops = tree->CountOperators(node->Annotation.Formula);
if(ops > 10) return true;
@ -2224,7 +2251,13 @@ namespace Duality {
// have to destroy the old proof to get a new interpolant
timer_start("SimplifyNode");
tree->PopPush();
tree->InterpolateByCases(top,node);
try {
tree->InterpolateByCases(top,node);
}
catch(const RPFP::Bad&){
timer_stop("SimplifyNode");
throw RPFP::Bad();
}
timer_stop("SimplifyNode");
}