mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 04:13:38 +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-05 18:02:14 -07:00
commit c57509d795
2 changed files with 19 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/duality/duality_solver.cpp
View file

@ -684,6 +684,7 @@ namespace Duality {
bool CandidateFeasible(const Candidate &cand){ bool CandidateFeasible(const Candidate &cand){
if(!FeasibleEdges) return true; if(!FeasibleEdges) return true;
timer_start("CandidateFeasible");
RPFP *checker = new RPFP(rpfp->ls); RPFP *checker = new RPFP(rpfp->ls);
// std::cout << "Checking feasibility of extension " << cand.edge->Parent->number << std::endl; // std::cout << "Checking feasibility of extension " << cand.edge->Parent->number << std::endl;
checker->Push(); checker->Push();
@ -691,8 +692,10 @@ namespace Duality {
Node *root = checker->CloneNode(cand.edge->Parent); Node *root = checker->CloneNode(cand.edge->Parent);
#ifdef BOUNDED #ifdef BOUNDED
for(unsigned i = 0; i < cand.Children.size(); i++) for(unsigned i = 0; i < cand.Children.size(); i++)
if(NodePastRecursionBound(cand.Children[i])) if(NodePastRecursionBound(cand.Children[i])){
timer_stop("CandidateFeasible");
return false; return false;
}
#endif #endif
#ifdef NEW_CAND_SEL #ifdef NEW_CAND_SEL
GenNodeSolutionFromIndSet(cand.edge->Parent,root->Bound); GenNodeSolutionFromIndSet(cand.edge->Parent,root->Bound);
@ -710,6 +713,7 @@ namespace Duality {
if(!res)reporter->Reject(cand.edge,cand.Children); if(!res)reporter->Reject(cand.edge,cand.Children);
checker->Pop(1); checker->Pop(1);
delete checker; delete checker;
timer_stop("CandidateFeasible");
return res; return res;
} }
@ -749,12 +753,15 @@ namespace Duality {
int StratifiedLeafCount; int StratifiedLeafCount;
bool DoStratifiedInlining(){ bool DoStratifiedInlining(){
timer_start("StratifiedInlining");
DoTopoSort(); DoTopoSort();
for(unsigned i = 0; i < leaves.size(); i++){ for(unsigned i = 0; i < leaves.size(); i++){
Node *node = leaves[i]; Node *node = leaves[i];
bool res = SatisfyUpperBound(node); bool res = SatisfyUpperBound(node);
if(!res) if(!res){
timer_stop("StratifiedInlining");
return false; return false;
}
} }
// don't leave any dangling nodes! // don't leave any dangling nodes!
#ifndef EFFORT_BOUNDED_STRAT #ifndef EFFORT_BOUNDED_STRAT
@ -762,6 +769,7 @@ namespace Duality {
if(!leaves[i]->Outgoing) if(!leaves[i]->Outgoing)
MakeLeaf(leaves[i],true); MakeLeaf(leaves[i],true);
#endif #endif
timer_stop("StratifiedInlining");
return true; return true;
} }
@ -1333,6 +1341,7 @@ namespace Duality {
/** Extend the unwinding, keeping it solved. */ /** Extend the unwinding, keeping it solved. */
bool Extend(Candidate &cand){ bool Extend(Candidate &cand){
timer_start("Extend");
Node *node = CreateNodeInstance(cand.edge->Parent); Node *node = CreateNodeInstance(cand.edge->Parent);
CreateEdgeInstance(cand.edge,node,cand.Children); CreateEdgeInstance(cand.edge,node,cand.Children);
UpdateBackEdges(node); UpdateBackEdges(node);
@ -1344,11 +1353,13 @@ namespace Duality {
ExpandUnderapproxNodes(cex.tree, cex.root); ExpandUnderapproxNodes(cex.tree, cex.root);
#endif #endif
if(UseUnderapprox) BuildFullCex(node); if(UseUnderapprox) BuildFullCex(node);
timer_stop("Extend");
return res; return res;
} }
#ifdef EARLY_EXPAND #ifdef EARLY_EXPAND
TryExpandNode(node); TryExpandNode(node);
#endif #endif
timer_stop("Extend");
return res; return res;
} }

6
src/muz_qe/duality_dl_interface.cpp
View file

@ -41,6 +41,7 @@ Revision History:
#include "duality.h" #include "duality.h"
#include "duality_profiling.h"
// using namespace Duality; // using namespace Duality;
@ -202,6 +203,11 @@ lbool dl_interface::query(::expr * query) {
// Solve! // Solve!
bool ans = rs->Solve(); bool ans = rs->Solve();
// profile!
if(m_ctx.get_params().profile())
print_profile(std::cout);
// save the result and counterexample if there is one // save the result and counterexample if there is one
_d->status = ans ? StatusModel : StatusRefutation; _d->status = ans ? StatusModel : StatusRefutation;
_d->cex = rs->GetCounterexample(); _d->cex = rs->GetCounterexample();