summaryrefslogtreecommitdiff
path: root/src/smt/command.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/command.h')
-rw-r--r--src/smt/command.h8
1 files changed, 0 insertions, 8 deletions
diff --git a/src/smt/command.h b/src/smt/command.h
index a0e591269..9fbd1bf73 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -33,7 +33,6 @@
#include "expr/type.h"
#include "expr/variable_type_map.h"
#include "proof/unsat_core.h"
-#include "util/proof.h"
#include "util/result.h"
#include "util/sexpr.h"
@@ -1131,9 +1130,7 @@ class CVC4_PUBLIC GetProofCommand : public Command
public:
GetProofCommand();
- const Proof& getResult() const;
void invoke(SmtEngine* smtEngine) override;
- void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
Command* exportTo(ExprManager* exprManager,
ExprManagerMapCollection& variableMap) override;
Command* clone() const override;
@@ -1144,11 +1141,6 @@ class CVC4_PUBLIC GetProofCommand : public Command
bool types = false,
size_t dag = 1,
OutputLanguage language = language::output::LANG_AUTO) const override;
-
- protected:
- SmtEngine* d_smtEngine;
- // d_result is owned by d_smtEngine.
- const Proof* d_result;
}; /* class GetProofCommand */
class CVC4_PUBLIC GetInstantiationsCommand : public Command
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback