diff options
Diffstat (limited to 'src/theory/theory_engine.h')
| -rw-r--r-- | src/theory/theory_engine.h | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 91a88274e..179530240 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -855,17 +855,20 @@ private: std::set< std::string > d_theoryAlternatives; std::map< std::string, std::vector< theory::Theory* > > d_attr_handle; -public: - /** - * Set user attribute. - * This function is called when an attribute is set by a user. In SMT-LIBv2 this is done - * via the syntax (! n :attr) + public: + /** Set user attribute. + * + * This function is called when an attribute is set by a user. In SMT-LIBv2 + * this is done via the syntax (! n :attr) */ - void setUserAttribute(const std::string& attr, Node n, std::vector<Node>& node_values, std::string str_value); + void setUserAttribute(const std::string& attr, + Node n, + const std::vector<Node>& node_values, + const std::string& str_value); - /** - * Handle user attribute. + /** Handle user attribute. + * * Associates theory t with the attribute attr. Theory t will be * notified whenever an attribute of name attr is set. */ @@ -877,7 +880,7 @@ public: */ void checkTheoryAssertionsWithModel(bool hardFailure); -private: + private: IntStat d_arithSubstitutionsAdded; };/* class TheoryEngine */ |