SmtEngine smt(&exprMgr, &options);
// If no file supplied we read from standard input
- bool inputFromStdin =
+ bool inputFromStdin =
firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]);
// Auto-detect input language by filename extension
const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
+ ReferenceStat< const char* > s_statFilename("filename",filename);
+ StatisticsRegistry::registerStat(&s_statFilename);
+
if(options.lang == parser::LANG_AUTO) {
if( inputFromStdin ) {
// We can't do any fancy detection on stdin
ParserBuilder(exprMgr, filename)
.withInputLanguage(options.lang)
.withMmap(options.memoryMap)
- .withChecks(options.semanticChecks &&
+ .withChecks(options.semanticChecks &&
!Configuration::isMuzzledBuild() )
.withStrictMode( options.strictParsing );
// Remove the parser
delete parser;
+ Result asSatResult = lastResult.asSatisfiabilityResult();
+ ReferenceStat< Result > s_statSatResult("sat/unsat", asSatResult);
+ StatisticsRegistry::registerStat(&s_statSatResult);
+
if(options.statistics){
StatisticsRegistry::flushStatistics(cerr);
}
Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
- if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){
+ if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){ // \upperbound(x_i) <= c_i
return false; //sat
}
- if(d_partialModel.belowLowerBound(x_i, c_i, true)){
+ if(d_partialModel.belowLowerBound(x_i, c_i, true)){// \lowerbound(x_i) > c_i
Node lbc = d_partialModel.getLowerConstraint(x_i);
Node conflict = NodeManager::currentNM()->mkNode(AND, lbc, original);
Debug("arith") << "AssertUpper conflict " << conflict << endl;
AlwaysAssert(d_name.find(s_delim) == std::string::npos);
}
}
+ virtual ~Stat() {}
virtual void flushInformation(std::ostream& out) const = 0;
}
+
+/**
+ * class T must have stream insertion operation defined.
+ * std::ostream& operator<<(std::ostream&, const T&);
+ */
template<class T>
class DataStat : public Stat{
public:
}
};
+/** T must have an assignment operator=(). */
template <class T>
class ReferenceStat: public DataStat<T>{
private:
const T* d_data;
public:
- ReferenceStat(const std::string& s): DataStat<T>(s), d_data(NULL){}
+ ReferenceStat(const std::string& s):
+ DataStat<T>(s), d_data(NULL)
+ {}
- ReferenceStat(const std::string& s, const T& data):ReferenceStat<T>(s){
+ ReferenceStat(const std::string& s, const T& data):
+ DataStat<T>(s),d_data(NULL)
+ {
setData(data);
}