mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-09 07:33:24 +00:00
Code Activity

status reporting issue

Browse source
This commit is contained in:
Ken McMillan 2013-05-22 13:23:37 -07:00
parent 477754c386
commit 7905f48e88
1 changed files with 5 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/duality/duality_solver.cpp
View file

@ -77,6 +77,7 @@ namespace Duality {
virtual void InductionFailure(RPFP::Edge *edge, const std::vector<RPFP::Node *> &children){} virtual void InductionFailure(RPFP::Edge *edge, const std::vector<RPFP::Node *> &children){}
virtual void UpdateUnderapprox(RPFP::Node *node, const RPFP::Transformer &update){} virtual void UpdateUnderapprox(RPFP::Node *node, const RPFP::Transformer &update){}
virtual void Reject(RPFP::Edge *edge, const std::vector<RPFP::Node *> &Children){} virtual void Reject(RPFP::Edge *edge, const std::vector<RPFP::Node *> &Children){}
virtual void Message(const std::string &msg){}
virtual ~Reporter(){} virtual ~Reporter(){}
}; };
@ -1154,7 +1155,7 @@ namespace Duality {
} }
#endif #endif
if(!full_scan && candidates.empty()){ if(!full_scan && candidates.empty()){
std::cout << "No candidates from updates. Trying full scan.\n"; reporter->Message("No candidates from updates. Trying full scan.");
GenCandidatesFromInductionFailure(true); GenCandidatesFromInductionFailure(true);
} }
} }
@ -2193,6 +2194,9 @@ namespace Duality {
s << " " << children[i]->number; s << " " << children[i]->number;
s << std::endl; s << std::endl;
} }
virtual void Message(const std::string &msg){
ev(); s << "msg " << msg << std::endl;
}
}; };