mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

prevent creating some useless solvers in duality

Browse source
This commit is contained in:
Ken McMillan 2014-10-08 13:56:46 -07:00
parent e8985ff33d
commit bbdc8b33e0
2 changed files with 21 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/duality/duality_solver.cpp
View file

@ -802,6 +802,15 @@ namespace Duality {
annot.Simplify();
}
bool NodeSolutionFromIndSetFull(Node *node){
std::vector<Node *> &insts = insts_of_node[node];
for(unsigned j = 0; j < insts.size(); j++)
if(indset->Contains(insts[j]))
if(insts[j]->Annotation.IsFull())
return true;
return false;
}
bool recursionBounded;
/** See if the solution might be bounded. */
@ -1453,16 +1462,18 @@ namespace Duality {
slvr.pop(1);
delete checker;
#else
RPFP_caching::scoped_solver_for_edge ssfe(gen_cands_rpfp,edge,true /* models */, true /*axioms*/);
gen_cands_rpfp->Push();
Node *root = CheckerForEdgeClone(edge,gen_cands_rpfp);
if(gen_cands_rpfp->Check(root) != unsat){
Candidate candidate;
ExtractCandidateFromCex(edge,gen_cands_rpfp,root,candidate);
reporter->InductionFailure(edge,candidate.Children);
candidates.push_back(candidate);
if(!NodeSolutionFromIndSetFull(edge->Parent)){
RPFP_caching::scoped_solver_for_edge ssfe(gen_cands_rpfp,edge,true /* models */, true /*axioms*/);
gen_cands_rpfp->Push();
Node *root = CheckerForEdgeClone(edge,gen_cands_rpfp);
if(gen_cands_rpfp->Check(root) != unsat){
Candidate candidate;
ExtractCandidateFromCex(edge,gen_cands_rpfp,root,candidate);
reporter->InductionFailure(edge,candidate.Children);
candidates.push_back(candidate);
}
gen_cands_rpfp->Pop(1);
}
gen_cands_rpfp->Pop(1);
#endif
}
updated_nodes.clear();

21
src/muz/duality/duality_dl_interface.cpp
View file

@ -158,26 +158,7 @@ lbool dl_interface::query(::expr * query) {
vector<unsigned> bounds;
// m_ctx.get_rules_as_formulas(rules, names);
expr_ref query_ref(m_ctx.get_manager());
if(****){
m_ctx.flush_add_rules();
datalog::rule_manager& rm = m_ctx.get_rule_manager();
rm.mk_query(query, m_ctx.get_rules());
apply_default_transformation(m_ctx);
rule_set &rs = m_ctx.get_rules();
if(m_ctx.get_rules().get_output_predicates().empty())
query_ref = m_ctx.get_manager().mk_true();
else {
query_pred = m_ctx.get_rules().get_output_predicate();
func_decl_ref query_pred(m_ctx.get_manager());
query_pred = m_ctx.get_rules().get_output_predicate();
ptr_vector<sort> sorts;
unsi
}
}
else
m_ctx.get_raw_rule_formulas(rules, names, bounds);
m_ctx.get_raw_rule_formulas(rules, names, bounds);
// get all the rules as clauses
std::vector<expr> &clauses = _d->clauses;