diff options
Diffstat (limited to 'src/proof/unsat_core.cpp')
-rw-r--r-- | src/proof/unsat_core.cpp | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp new file mode 100644 index 000000000..4a4d13977 --- /dev/null +++ b/src/proof/unsat_core.cpp @@ -0,0 +1,54 @@ +/********************* */ +/*! \file unsat_core.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Representation of unsat cores + ** + ** Representation of unsat cores. + **/ + +#include "proof/unsat_core.h" + +#include "printer/printer.h" +#include "smt/smt_engine_scope.h" +#include "smt_util/command.h" + +namespace CVC4 { + +void UnsatCore::initMessage() const { + Debug("core") << "UnsatCore size " << d_core.size() << std::endl; +} + +UnsatCore::const_iterator UnsatCore::begin() const { + return d_core.begin(); +} + +UnsatCore::const_iterator UnsatCore::end() const { + return d_core.end(); +} + +void UnsatCore::toStream(std::ostream& out) const { + smt::SmtScope smts(d_smt); + Expr::dag::Scope scope(out, false); + Printer::getPrinter(options::outputLanguage())->toStream(out, *this); +} + +void UnsatCore::toStream(std::ostream& out, const std::map<Expr, std::string>& names) const { + smt::SmtScope smts(d_smt); + Expr::dag::Scope scope(out, false); + Printer::getPrinter(options::outputLanguage())->toStream(out, *this, names); +} + +std::ostream& operator<<(std::ostream& out, const UnsatCore& core) { + core.toStream(out); + return out; +} + +}/* CVC4 namespace */ |