diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-11 06:11:46 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-11 06:11:46 -0500 |
commit | 3153e2d94d1b12562557d60305bcac52d3128b83 (patch) | |
tree | ef4740a54d489b61d92163024a8c516f38aae050 /src/smt/command.h | |
parent | 5e2c7c3a25d334c0068b423225f8ff7793260069 (diff) |
Move unsat core names to smt engine (#1192)
* Move unsat core names to SmtEnginePrivate. Adds a SetExpressionNameCommand to do this. Removes the names field from GetUnsatCoreCommand.
* Comment
* Pass expression names by reference.
* Update throw specifiers.
* Minor
* Switch expression names to CDMap, simplify interface for printing unsat core names.
* Revert throw specifier change.
* Minor simplifcations
Diffstat (limited to 'src/smt/command.h')
-rw-r--r-- | src/smt/command.h | 29 |
1 files changed, 25 insertions, 4 deletions
diff --git a/src/smt/command.h b/src/smt/command.h index 0e07583b2..839927fc1 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -687,12 +687,8 @@ public: };/* class GetQuantifierEliminationCommand */ class CVC4_PUBLIC GetUnsatCoreCommand : public Command { -protected: - UnsatCore d_result; - std::map<Expr, std::string> d_names; public: GetUnsatCoreCommand() throw(); - GetUnsatCoreCommand(const std::map<Expr, std::string>& names) throw(); ~GetUnsatCoreCommand() throw() {} void invoke(SmtEngine* smtEngine); void printResult(std::ostream& out, uint32_t verbosity = 2) const; @@ -700,6 +696,10 @@ public: Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); Command* clone() const; std::string getCommandName() const throw(); + +protected: + // the result of the unsat core call + UnsatCore d_result; };/* class GetUnsatCoreCommand */ class CVC4_PUBLIC GetAssertionsCommand : public Command { @@ -804,6 +804,27 @@ public: std::string getCommandName() const throw(); };/* class GetOptionCommand */ +// Set expression name command +// Note this is not an official smt2 command +// Conceptually: +// (assert (! expr :named name)) +// is converted to +// (assert expr) +// (set-expr-name expr name) +class CVC4_PUBLIC SetExpressionNameCommand : public Command { +protected: + Expr d_expr; + std::string d_name; +public: + SetExpressionNameCommand(Expr expr, std::string name) throw(); + ~SetExpressionNameCommand() throw() {} + void invoke(SmtEngine* smtEngine); + Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap); + Command* clone() const; + std::string getCommandName() const throw(); +};/* class SetExpressionNameCommand */ + + class CVC4_PUBLIC DatatypeDeclarationCommand : public Command { private: std::vector<DatatypeType> d_datatypes; |