Updates to Clark's commit r4540:

* ALL_SUPPORTED/QF_ALL_SUPPORTED don't include nonlinear
* Change "Notice" to "Warning" when produce-models turned off due to non-linear

(this commit was certified error- and warning-free by the test-and-commit script.)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 761fe3b8ccfadcc9239a29882d718d0dfa5920fa..e308db2696f872feb404b61479afa1ca3498c01f 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -892,11 +892,11 @@ void SmtEngine::setLogicInternal() throw() {
   if (d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
       !d_logic.isLinear()) {
     if (options::produceModels()) {
-      Notice() << "SmtEngine: turning off produce-models because unsupported for nonlinear arith" << std::endl;
+      Warning() << "SmtEngine: turning off produce-models because unsupported for nonlinear arith" << std::endl;
       setOption("produce-models", SExpr("false"));
     }
     if (options::checkModels()) {
-      Notice() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << std::endl;
+      Warning() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << std::endl;
       setOption("check-models", SExpr("false"));
     }    
   }

diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index d721d089e4c806b91a751999e2b00b300abdb39d..d2cf576438583cb44f3ff280ead6fe1fcc2cd105 100644 (file)
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -35,7 +35,7 @@ LogicInfo::LogicInfo() :
   d_sharingTheories(0),
   d_integers(true),
   d_reals(true),
-  d_linear(false),
+  d_linear(true),// for now, "everything enabled" doesn't include non-linear arith
   d_differenceLogic(false),
   d_locked(false) {
 

diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h
index ba498c0322cc942ca5cd600f056250f0fa3ca8c5..430a2a164f00b9290dd2f9926dacc641a9df5d52 100644 (file)
--- a/test/unit/theory/logic_info_white.h
+++ b/test/unit/theory/logic_info_white.h
@@ -418,7 +418,7 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
-    TS_ASSERT( !info.isLinear() );
+    TS_ASSERT( info.isLinear() );// for now, nonlinear not included in ALL_SUPPORTED
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areRealsUsed() );
@@ -436,7 +436,7 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
-    TS_ASSERT( !info.isLinear() );
+    TS_ASSERT( info.isLinear() );// for now, nonlinear not included in ALL_SUPPORTED
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areRealsUsed() );
@@ -470,11 +470,11 @@ public:
     TS_ASSERT_THROWS( info.isQuantified(), CVC4::IllegalArgumentException );
     TS_ASSERT_THROWS( info.areIntegersUsed(), CVC4::IllegalArgumentException );
     TS_ASSERT_THROWS( info.areRealsUsed(), CVC4::IllegalArgumentException );
-    TS_ASSERT_THROWS( ! info.isLinear(), CVC4::IllegalArgumentException );
+    TS_ASSERT_THROWS( info.isLinear(), CVC4::IllegalArgumentException );// for now, nonlinear not included in ALL_SUPPORTED
 
     info.lock();
     TS_ASSERT( info.isLocked() );
-    TS_ASSERT_EQUALS( info.getLogicString(), "AUFBVDTNIRA" );
+    TS_ASSERT_EQUALS( info.getLogicString(), "AUFBVDTLIRA" );// for now, nonlinear not included in ALL_SUPPORTED
     TS_ASSERT( info.isSharingEnabled() );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BUILTIN ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
@@ -497,7 +497,7 @@ public:
     TS_ASSERT( info.isQuantified() );
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( info.areRealsUsed() );
-    TS_ASSERT( ! info.isLinear() );
+    TS_ASSERT( info.isLinear() );// for now, nonlinear not included in ALL_SUPPORTED
 
     TS_ASSERT_THROWS( info.arithOnlyLinear(), CVC4::IllegalArgumentException );
     TS_ASSERT_THROWS( info.disableIntegers(), CVC4::IllegalArgumentException );
@@ -594,7 +594,7 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
-    TS_ASSERT( !info.isLinear() );
+    TS_ASSERT( info.isLinear() );// for now, nonlinear not included in ALL_SUPPORTED
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areRealsUsed() );
@@ -613,7 +613,7 @@ public:
     TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) );
     TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) );
-    TS_ASSERT( !info.isLinear() );
+    TS_ASSERT( info.isLinear() );// for now, nonlinear not included in ALL_SUPPORTED
     TS_ASSERT( info.areIntegersUsed() );
     TS_ASSERT( !info.isDifferenceLogic() );
     TS_ASSERT( info.areRealsUsed() );