diff options
Diffstat (limited to 'src/smt/smt_engine.h')
| -rw-r--r-- | src/smt/smt_engine.h | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 25800f5b3..234814245 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -389,16 +389,10 @@ public: CVC4::SExpr getAssignment() throw(ModalException, AssertionException); /** - * Add to Model Type. This is used for recording which types should be reported + * Add to Model command. This is used for recording a command that should be reported * during a get-model call. */ - void addToModelType( Type& t ); - - /** - * Add to Model Function. This is used for recording which functions should be reported - * during a get-model call. - */ - void addToModelFunction( Expr& e ); + void addToModelCommand( Command* c, int c_type ); /** * Get the model (only if immediately preceded by a SAT @@ -565,6 +559,12 @@ public: */ void printModel( std::ostream& out, Model* m ); + /** Set user attribute + * This function is called when an attribute is set by a user. In SMT-LIBv2 this is done + * via the syntax (! expr :attr) + */ + void setUserAttribute( std::string& attr, Expr expr ); + };/* class SmtEngine */ }/* CVC4 namespace */ |