diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-11-03 15:36:38 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-03 15:36:38 -0500 |
commit | 5cafed748989602263b8ad1a27ac6b9bd159a441 (patch) | |
tree | b0e474f47251d480dce48637e73f663aba0dd179 /src/smt/command.h | |
parent | 3f2c2c745ae2f13441c1cabd363e6539c9bdaeb9 (diff) |
Sygus clean main (#1297)
* Remove front end hack for sygus.
* Remove other hack, add sygus solution output mode.
* Clang format
* Minor
* Fix
* Minor
* Remove unused field.
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 |