diff options
Diffstat (limited to 'src/smt/smt_engine.h')
| -rw-r--r-- | src/smt/smt_engine.h | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 223478e5f..5aa2ba987 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -34,7 +34,6 @@ #include "smt/smt_mode.h" #include "theory/logic_info.h" #include "util/hash.h" -#include "util/proof.h" #include "util/result.h" #include "util/sexpr.h" #include "util/statistics.h" @@ -544,16 +543,6 @@ class CVC4_PUBLIC SmtEngine */ std::vector<std::pair<Expr, Expr> > getAssignment(); - /** - * Get the last proof (only if immediately preceded by an UNSAT or ENTAILED - * query). Only permitted if CVC4 was built with proof support and - * produce-proofs is on. - * - * The Proof object is owned by this SmtEngine until the SmtEngine is - * destroyed. - */ - const Proof& getProof(); - /** Print all instantiations made by the quantifiers module. */ void printInstantiations(std::ostream& out); @@ -921,11 +910,6 @@ class CVC4_PUBLIC SmtEngine }; /** - * Check that a generated proof (via getProof()) checks. - */ - void checkProof(); - - /** * Internal method to get an unsatisfiable core (only if immediately preceded * by an UNSAT or ENTAILED query). Only permitted if CVC4 was built with * unsat-core support and produce-unsat-cores is on. Does not dump the |