diff options
Diffstat (limited to 'src/smt/command.h')
-rw-r--r-- | src/smt/command.h | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/src/smt/command.h b/src/smt/command.h index f5be9ddfe..a60c85a3c 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -529,13 +529,9 @@ public: };/* class QueryCommand */ class CVC4_PUBLIC CheckSynthCommand : public Command { -protected: - Expr d_expr; - Result d_result; - bool d_inUnsatCore; public: CheckSynthCommand() throw(); - CheckSynthCommand(const Expr& expr, bool inUnsatCore = true) throw(); + CheckSynthCommand(const Expr& expr) throw(); ~CheckSynthCommand() throw() {} Expr getExpr() const throw(); void invoke(SmtEngine* smtEngine); @@ -544,6 +540,14 @@ public: Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; std::string getCommandName() const throw(); + + protected: + /** the assertion of check-synth */ + Expr d_expr; + /** result of the check-synth call */ + Result d_result; + /** string stream that stores the output of the solution */ + std::stringstream d_solution; };/* class CheckSynthCommand */ // this is TRANSFORM in the CVC presentation language |