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 | |
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')
-rw-r--r-- | src/theory/Makefile.am | 1 | ||||
-rw-r--r-- | src/theory/logic_info.cpp | 91 | ||||
-rw-r--r-- | src/theory/logic_info.i | 15 | ||||
-rw-r--r-- | src/theory/theory.h | 2 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 10 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 4 |
6 files changed, 73 insertions, 50 deletions
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 8dcd14995..1f0108581 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -61,6 +61,7 @@ libtheory_la_LIBADD = \ @builddir@/rewriterules/librewriterules.la EXTRA_DIST = \ + logic_info.i \ options_handlers.h \ rewriter_tables_template.h \ instantiator_tables_template.cpp \ diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index d2cf57643..e76e2ace9 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -76,52 +76,61 @@ LogicInfo::LogicInfo(const char* logicString) throw(IllegalArgumentException) : std::string LogicInfo::getLogicString() const { CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); if(d_logicString == "") { - size_t seen = 0; // make sure we support all the active theories + LogicInfo qf_all_supported; + qf_all_supported.disableQuantifiers(); + qf_all_supported.lock(); + if(hasEverything()) { + d_logicString = "ALL_SUPPORTED"; + } else if(*this == qf_all_supported) { + d_logicString = "QF_ALL_SUPPORTED"; + } else { + size_t seen = 0; // make sure we support all the active theories - stringstream ss; - if(!isQuantified()) { - ss << "QF_"; - } - if(d_theories[THEORY_ARRAY]) { - ss << (d_sharingTheories == 1 ? "AX" : "A"); - ++seen; - } - if(d_theories[THEORY_UF]) { - ss << "UF"; - ++seen; - } - if(d_theories[THEORY_BV]) { - ss << "BV"; - ++seen; - } - if(d_theories[THEORY_DATATYPES]) { - ss << "DT"; - ++seen; - } - if(d_theories[THEORY_ARITH]) { - if(isDifferenceLogic()) { - ss << (areIntegersUsed() ? "I" : ""); - ss << (areRealsUsed() ? "R" : ""); - ss << "DL"; - } else { - ss << (isLinear() ? "L" : "N"); - ss << (areIntegersUsed() ? "I" : ""); - ss << (areRealsUsed() ? "R" : ""); - ss << "A"; + stringstream ss; + if(!isQuantified()) { + ss << "QF_"; + } + if(d_theories[THEORY_ARRAY]) { + ss << (d_sharingTheories == 1 ? "AX" : "A"); + ++seen; + } + if(d_theories[THEORY_UF]) { + ss << "UF"; + ++seen; + } + if(d_theories[THEORY_BV]) { + ss << "BV"; + ++seen; + } + if(d_theories[THEORY_DATATYPES]) { + ss << "DT"; + ++seen; + } + if(d_theories[THEORY_ARITH]) { + if(isDifferenceLogic()) { + ss << (areIntegersUsed() ? "I" : ""); + ss << (areRealsUsed() ? "R" : ""); + ss << "DL"; + } else { + ss << (isLinear() ? "L" : "N"); + ss << (areIntegersUsed() ? "I" : ""); + ss << (areRealsUsed() ? "R" : ""); + ss << "A"; + } + ++seen; } - ++seen; - } - if(seen != d_sharingTheories) { - Unhandled("can't extract a logic string from LogicInfo; at least one " - "active theory is unknown to LogicInfo::getLogicString() !"); - } + if(seen != d_sharingTheories) { + Unhandled("can't extract a logic string from LogicInfo; at least one " + "active theory is unknown to LogicInfo::getLogicString() !"); + } - if(seen == 0) { - ss << "SAT"; - } + if(seen == 0) { + ss << "SAT"; + } - d_logicString = ss.str(); + d_logicString = ss.str(); + } } return d_logicString; } diff --git a/src/theory/logic_info.i b/src/theory/logic_info.i new file mode 100644 index 000000000..67eea4e04 --- /dev/null +++ b/src/theory/logic_info.i @@ -0,0 +1,15 @@ +%{ +#include "theory/logic_info.h" +%} + +%ignore CVC4::LogicInfo::LogicInfo(const char*); + +%rename(less) CVC4::LogicInfo::operator<(const LogicInfo&) const; +%rename(lessEqual) CVC4::LogicInfo::operator<=(const LogicInfo&) const; +%rename(greater) CVC4::LogicInfo::operator>(const LogicInfo&) const; +%rename(greaterEqual) CVC4::LogicInfo::operator>=(const LogicInfo&) const; + +%rename(equals) CVC4::LogicInfo::operator==(const LogicInfo&) const; +%ignore CVC4::LogicInfo::operator!=(const LogicInfo&) const; + +%include "theory/logic_info.h" diff --git a/src/theory/theory.h b/src/theory/theory.h index 72206afb8..95fe03c82 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -669,7 +669,7 @@ public: * This function is called when an attribute is set by a user. In SMT-LIBv2 this is done * via the syntax (! n :attr) */ - virtual void setUserAttribute( std::string& attr, Node n ) { + virtual void setUserAttribute(const std::string& attr, Node n) { Unimplemented("Theory %s doesn't support Theory::setUserAttribute interface", identify().c_str()); } 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) { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 67830390c..d6e984f8f 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -703,13 +703,13 @@ public: * 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( std::string& attr, Node n ); + void setUserAttribute(const std::string& attr, Node n); /** Handle user attribute * Associates theory t with the attribute attr. Theory t will be * notifed whenever an attribute of name attr is set. */ - void handleUserAttribute( const char* attr, theory::Theory* t ); + void handleUserAttribute(const char* attr, theory::Theory* t); /** Check that the theory assertions are satisfied in the model * This function is called from the smt engine's checkModel routine |