diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-11-17 04:05:17 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-11-17 04:05:17 +0000 |
commit | 44498017455cce207bf9cb0a1ebbf67c4a4d77cf (patch) | |
tree | 18f0bf80ea93cfd1f0e49cf38b7f0baf2d457285 /src/theory/theory_engine.cpp | |
parent | db35c4be8bd37746e1c27e446291c82556df1d05 (diff) |
* Fix for bug 445 agreed to in meeting 11/13/2012: always dump in ALL_SUPPORTED logic
* Java bindings fixes: fixed access to ostreams, iterators
* Make SmtEngine::setUserAttribute() (and others) take a const string&
* Also a few compliance fixes
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 0f9cb5e8e..4b4316db1 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1329,25 +1329,23 @@ void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions) } -void TheoryEngine::setUserAttribute( std::string& attr, Node n ){ +void TheoryEngine::setUserAttribute(const std::string& attr, Node n) { Trace("te-attr") << "set user attribute " << attr << " " << n << std::endl; if( d_attr_handle.find( attr )!=d_attr_handle.end() ){ for( size_t i=0; i<d_attr_handle[attr].size(); i++ ){ - d_attr_handle[attr][i]->setUserAttribute( attr, n ); + d_attr_handle[attr][i]->setUserAttribute(attr, n); } - }else{ + } else { //unhandled exception? } } - -void TheoryEngine::handleUserAttribute( const char* attr, Theory* t ){ +void TheoryEngine::handleUserAttribute(const char* attr, Theory* t) { Trace("te-attr") << "Handle user attribute " << attr << " " << t << std::endl; std::string str( attr ); d_attr_handle[ str ].push_back( t ); } - void TheoryEngine::checkTheoryAssertionsWithModel() { for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { |