summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/Makefile.am1
-rw-r--r--src/theory/logic_info.cpp91
-rw-r--r--src/theory/logic_info.i15
-rw-r--r--src/theory/theory.h2
-rw-r--r--src/theory/theory_engine.cpp10
-rw-r--r--src/theory/theory_engine.h4
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback