From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 10 Nov 2012 16:41:01 +0000 (+0000)
Subject: Updates to Clark's commit r4540:
X-Git-Tag: cvc5-1.0.0~7626
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3169a068f1a0a6b1f8cc902847d106664d6c0bd9;p=cvc5.git

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 761fe3b8c..e308db269 100644
--- 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 d721d089e..d2cf57643 100644
--- 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 ba498c032..430a2a164 100644
--- 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() );