diff --git a/src/duality/duality.h b/src/duality/duality.h index edd89d78f..04527450c 100755 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -778,6 +778,10 @@ protected: struct Bad { }; + // thrown on more serious internal error + struct ReallyBad { + }; + /** Pop a scope (see Push). Note, you cannot pop axioms. */ void Pop(int num_scopes); diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index f2824c9b0..cdc8fb3b2 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -2643,6 +2643,10 @@ namespace Duality { GetGroundLitsUnderQuants(memo,f.body(),res,1); return; } + if(f.is_var()){ + // std::cout << "foo!\n"; + return; + } if(under && f.is_ground()) res.push_back(f); } @@ -3065,10 +3069,14 @@ namespace Duality { node->Annotation.SetEmpty(); hash_set *core = new hash_set; core->insert(node->Outgoing->dual); + expr prev_annot = ctx.bool_val(false); + expr prev_impl = ctx.bool_val(false); + int repeated_case_count = 0; while(1){ by_case_counter++; is.push(); expr annot = !GetAnnotation(node); + Transformer old_annot = node->Annotation; is.add(annot); if(is.check() == unsat){ is.pop(1); @@ -3076,56 +3084,70 @@ namespace Duality { } is.pop(1); Push(); - ConstrainEdgeLocalized(node->Outgoing,is.get_implicant()); + expr the_impl = is.get_implicant(); + if(eq(the_impl,prev_impl)){ + // std::cout << "got old implicant\n"; + repeated_case_count++; + } + prev_impl = the_impl; + ConstrainEdgeLocalized(node->Outgoing,the_impl); ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); //TODO: need this? - check_result foo = Check(root); - if(foo != unsat){ - slvr().print("should_be_unsat.smt2"); - throw "should be unsat"; - } - std::vector assumps, axioms_to_add; - slvr().get_proof().get_assumptions(assumps); - for(unsigned i = 0; i < assumps.size(); i++){ - (*core).insert(assumps[i]); - if(axioms_needed.find(assumps[i]) != axioms_needed.end()){ - axioms_to_add.push_back(assumps[i]); - axioms_needed.erase(assumps[i]); - } - } - // AddToProofCore(*core); - Transformer old_annot = node->Annotation; - SolveSingleNode(root,node); - - { - expr itp = GetAnnotation(node); - dualModel = is.get_model(); // TODO: what does this mean? - std::vector case_lits; - itp = StrengthenFormulaByCaseSplitting(itp, case_lits); - SetAnnotation(node,itp); - node->Annotation.Formula = node->Annotation.Formula.simplify(); - } - - 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; + check_result foo = Check(root); + if(foo != unsat){ Pop(1); is.pop(1); delete core; timer_stop("InterpolateByCases"); - throw Bad(); + throw ReallyBad(); + // slvr().print("should_be_unsat.smt2"); + // throw "should be unsat"; } - bad_count++; - } -#endif + std::vector assumps, axioms_to_add; + slvr().get_proof().get_assumptions(assumps); + for(unsigned i = 0; i < assumps.size(); i++){ + (*core).insert(assumps[i]); + if(axioms_needed.find(assumps[i]) != axioms_needed.end()){ + axioms_to_add.push_back(assumps[i]); + axioms_needed.erase(assumps[i]); + } + } + // AddToProofCore(*core); + SolveSingleNode(root,node); - if(node->Annotation.IsEmpty()){ + { + expr itp = GetAnnotation(node); + dualModel = is.get_model(); // TODO: what does this mean? + std::vector case_lits; + itp = StrengthenFormulaByCaseSplitting(itp, case_lits); + SetAnnotation(node,itp); + node->Annotation.Formula = node->Annotation.Formula.simplify(); + } + + 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() || eq(node->Annotation.Formula,prev_annot) || (repeated_case_count > 0 && !axioms_added) || (repeated_case_count >= 10)){ + looks_bad: if(!axioms_added){ // add the axioms in the off chance they are useful const std::vector &theory = ls->get_axioms(); @@ -3134,6 +3156,7 @@ namespace Duality { axioms_added = true; } else { + //#define KILL_ON_BAD_INTERPOLANT #ifdef KILL_ON_BAD_INTERPOLANT std::cout << "bad in InterpolateByCase -- core:\n"; #if 0 @@ -3175,10 +3198,11 @@ namespace Duality { is.pop(1); delete core; timer_stop("InterpolateByCases"); - throw Bad(); + throw ReallyBad(); } } Pop(1); + prev_annot = node->Annotation.Formula; node->Annotation.UnionWith(old_annot); } if(proof_core) diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 69759f9bb..b40ab9370 100755 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -2279,6 +2279,18 @@ namespace Duality { // bad interpolants can get us here throw DoRestart(); } + catch(const RPFP::ReallyBad &){ + // this could be caused by incompleteness + for(unsigned i = 0; i < expansions.size(); i++){ + Node *node = expansions[i]; + node->map->Annotation.SetFull(); + std::vector &chs = node->map->Outgoing->Children; + for(unsigned j = 0; j < chs.size(); j++) + chs[j]->Annotation.SetFull(); + reporter->Message("incompleteness: cleared annotation and child annotations"); + } + throw DoRestart(); + } catch(char const *msg){ // bad interpolants can get us here reporter->Message(std::string("interpolation failure:") + msg); diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index a39065922..e3ac59dfd 100755 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -778,6 +778,8 @@ int iz3mgr::occurs_in(ast var, ast e){ bool iz3mgr::solve_arith(const ast &v, const ast &x, const ast &y, ast &res){ + if(occurs_in(v,y)) + return false; if(op(x) == Plus){ int n = num_args(x); for(int i = 0; i < n; i++){ @@ -801,8 +803,8 @@ iz3mgr::ast iz3mgr::cont_eq(stl_ext::hash_set &cont_eq_memo, bool truth, as return ast(); cont_eq_memo.insert(e); if(!truth && op(e) == Equal){ - if(arg(e,0) == v) return(arg(e,1)); - if(arg(e,1) == v) return(arg(e,0)); + if(arg(e,0) == v && !occurs_in(v,arg(e,1))) return(arg(e,1)); + if(arg(e,1) == v && !occurs_in(v,arg(e,0))) return(arg(e,0)); ast res; if(solve_arith(v,arg(e,0),arg(e,1),res)) return res; if(solve_arith(v,arg(e,1),arg(e,0),res)) return res; diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 3ec2c42d1..7f66bb2d8 100755 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -278,7 +278,8 @@ class iz3mgr { } symb sym(ast t){ - return to_app(t.raw())->get_decl(); + raw_ast *_ast = t.raw(); + return is_app(_ast) ? to_app(_ast)->get_decl() : 0; } std::string string_of_symbol(symb s){