1 /********************* */
4 ** Top contributors (to current version):
5 ** Morgan Deters, Andrew Reynolds, Liana Hadarean
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "cvc4_public.h"
20 #ifndef __CVC4__UNSAT_CORE_H
21 #define __CVC4__UNSAT_CORE_H
26 #include "expr/expr.h"
33 std::ostream
& operator<<(std::ostream
& out
, const UnsatCore
& core
) CVC4_PUBLIC
;
35 class CVC4_PUBLIC UnsatCore
{
36 friend std::ostream
& operator<<(std::ostream
&, const UnsatCore
&);
38 /** The SmtEngine we're associated with */
41 std::vector
<Expr
> d_core
;
43 void initMessage() const;
46 UnsatCore() : d_smt(NULL
) {}
48 UnsatCore(SmtEngine
* smt
, std::vector
<Expr
> core
) : d_smt(smt
), d_core(core
) {
54 /** get the smt engine that this unsat core is hooked up to */
55 SmtEngine
* getSmtEngine() const { return d_smt
; }
57 size_t size() const { return d_core
.size(); }
59 typedef std::vector
<Expr
>::const_iterator iterator
;
60 typedef std::vector
<Expr
>::const_iterator const_iterator
;
62 const_iterator
begin() const;
63 const_iterator
end() const;
65 /** prints this UnsatCore object to the stream out.
66 * We use the expression names stored in the SmtEngine d_smt
68 void toStream(std::ostream
& out
) const;
70 };/* class UnsatCore */
74 #endif /* __CVC4__UNSAT_CORE_H */