Shell::Option demolition

CASC/PortfolioMode.cpp

@@ -93,14 +93,14 @@ bool PortfolioMode::perform(Problem* problem)
       cout<<"Proof not found in time "<<Timer::msToSecondsString(Timer::elapsedMilliseconds())<<endl;
       if (env.remainingTime()/100>0) {
         addCommentSignForSZS(cout);
-        cout<<"SZS status GaveUp for "<<env.options->problemName()<<endl;
+        cout<<"SZS status GaveUp for "<<env.options->problemName<<endl;
       }
       else {
         //From time to time we may also be terminating in the timeLimitReached()
         //function in Lib/Timer.cpp in case the time runs out. We, however, output
         //the same string there as well.
         addCommentSignForSZS(cout);
-        cout<<"SZS status Timeout for "<<env.options->problemName()<<endl;
+        cout<<"SZS status Timeout for "<<env.options->problemName<<endl;
       }
     }
 #if VTIME_PROFILING
@@ -625,7 +625,7 @@ void PortfolioMode::runSlice(Options& opt)
   opt.checkGlobalOptionConstraints();
 
   if (outputAllowed()) {
-    addCommentSignForSZS(cout) << opt.generateEncodedOptions() << " on " << opt.problemName() <<
+    addCommentSignForSZS(cout) << opt.generateEncodedOptions() << " on " << opt.problemName <<
       " for (" << opt.timeLimitInDeciseconds() << "ds"<<
 #if VAMPIRE_PERF_EXISTS
       "/" << opt.instructionLimit() << "Mi" <<

FMB/FiniteModelBuilder.cpp

@@ -36,6 +36,7 @@
 #include "Lib/DHSet.hpp"
 #include "Lib/ArrayMap.hpp"
 
+#include "Shell/Property.hpp"
 #include "Shell/UIHelper.hpp"
 #include "Shell/Statistics.hpp"
 #include "Shell/GeneralSplitting.hpp"
@@ -1877,7 +1878,7 @@ void FiniteModelBuilder::onModelFound()
   //we need to print this early because model generating can take some time
   if(szsOutputMode()) {
     std::cout << "% SZS status "<<( UIHelper::haveConjecture() ? "CounterSatisfiable" : "Satisfiable" )
-        << " for " << _opt.problemName() << endl << flush;
+        << " for " << _opt.problemName << endl << flush;
     UIHelper::satisfiableStatusWasAlreadyOutput = true;
   }
 

FMB/FiniteModelBuilder.hpp

@@ -27,6 +27,7 @@
 #include "Lib/ScopedPtr.hpp"
 #include "SortInference.hpp"
 #include "Lib/BinaryHeap.hpp"
+#include "Lib/DArray.hpp"
 
 namespace FMB {
 using namespace Lib;

FMB/Monotonicity.cpp

@@ -16,6 +16,7 @@
 #include "Forwards.hpp"
 
 #include "Lib/Stack.hpp"
+#include "Lib/DArray.hpp"
 #include "Lib/DHMap.hpp"
 #include "Lib/Environment.hpp"
 #include "Lib/List.hpp"
@@ -31,6 +32,8 @@
 #include "SAT/SATClause.hpp"
 #include "SAT/MinisatInterfacing.hpp"
 
+#include "Shell/Property.hpp"
+
 #include "Monotonicity.hpp"
 
 namespace FMB

FMB/SortInference.cpp

@@ -17,6 +17,7 @@
  */
 
 #include "Shell/Options.hpp"
+#include "Shell/Property.hpp"
 
 #include "Kernel/Term.hpp"
 #include "Kernel/Clause.hpp"

FMB/SortInference.hpp

@@ -22,6 +22,7 @@
 
 #include "Forwards.hpp"
 
+#include "Lib/DArray.hpp"
 #include "Lib/DHMap.hpp"
 
 namespace FMB {

Kernel/FormulaTransformer.cpp

@@ -21,6 +21,7 @@
 #include "Problem.hpp"
 #include "SortHelper.hpp"
 #include "TermTransformer.hpp"
+#include "Lib/DArray.hpp"
 #include "Lib/DHMap.hpp"
 
 #include "FormulaTransformer.hpp"

Kernel/MainLoop.cpp

@@ -22,6 +22,7 @@
 #include "SAT/Z3MainLoop.hpp"
 
 #include "Shell/Options.hpp"
+#include "Shell/Property.hpp"
 #include "Shell/UIHelper.hpp"
 
 #include "Clause.hpp"

Kernel/Theory.cpp

@@ -16,6 +16,7 @@
 #include "Debug/Assertion.hpp"
 
 #include "Kernel/TermIterators.hpp"
+#include "Lib/DArray.hpp"
 #include "Lib/Environment.hpp"
 #include "Lib/Int.hpp"
 

Lib/Hash.hpp

@@ -19,6 +19,7 @@
 #include <functional>
 #include <type_traits>
 #include <cstdint>
+#include <cstring>
 
 #include "Forwards.hpp"
 #include "Kernel/Unit.hpp"
@@ -141,6 +142,10 @@ struct FnvHash
     static_assert(
       !std::is_base_of<Kernel::Unit, T>::value,
       "Units are hashed by their number: use UnitHash or UnitNumberHash");
+    static_assert(
+      !std::is_same<const char, T>::value,
+      "careful - this will use pointer equality in DHMap, are you sure?"
+    );
     return hashBytes(
       reinterpret_cast<const unsigned char*>(&ptr),
       sizeof(ptr),
@@ -151,6 +156,8 @@ struct FnvHash
   // strings hash the underlying C-style string
   static unsigned hash(const std::string& str)
   { return hashNulTerminated(str.c_str()); }
+  static unsigned hash(const std::string_view str)
+  { return hashNulTerminated(str.data()); }
 };
 
 // hash a Unit (or descendant, e.g. Clause) by FNV-1a of its unique incrementing number
@@ -330,6 +337,8 @@ class DefaultHash
   // strings hash the underlying C-style string
   static unsigned hash(const std::string& str)
   { return FnvHash::hash(str); }
+  static unsigned hash(std::string_view str)
+  { return FnvHash::hash(str); }
 
   // dispatch to VectorHash<DefaultHash>
   template<typename T>
@@ -428,6 +437,8 @@ class DefaultHash2 {
   // strings use their length
   static unsigned hash(const std::string &str)
   { return LengthHash::hash(str); }
+  static unsigned hash(std::string_view str)
+  { return LengthHash::hash(str); }
 
   // containers use their length
   template<typename T> static unsigned hash(const Stack<T> &stack)

Lib/StringUtils.cpp

@@ -207,7 +207,7 @@ bool StringUtils::readEqualities(const char* str, char delimiter, char eqChar, D
  *
  * @author Giles
  */
-size_t StringUtils::distance(const std::string &s1, const std::string &s2)
+size_t StringUtils::distance(std::string_view s1, std::string_view s2)
 {
   const size_t m(s1.size());
   const size_t n(s2.size());
@@ -220,13 +220,13 @@ size_t StringUtils::distance(const std::string &s1, const std::string &s2)
   for( size_t k=0; k<=n; k++ ) costs[k] = k;
 
   size_t i = 0;
-  for ( std::string::const_iterator it1 = s1.begin(); it1 != s1.end(); ++it1, ++i )
+  for (auto it1 = s1.begin(); it1 != s1.end(); ++it1, ++i )
   {
     costs[0] = i+1;
     size_t corner = i;
 
     size_t j = 0;
-    for ( std::string::const_iterator it2 = s2.begin(); it2 != s2.end(); ++it2, ++j )
+    for (auto it2 = s2.begin(); it2 != s2.end(); ++it2, ++j )
     {
       size_t upper = costs[j+1];
       if( *it1 == *it2 ){costs[j+1] = corner;}

Lib/StringUtils.hpp

@@ -45,7 +45,7 @@ class StringUtils {
   static A parse(std::string const& str)
   { return StringParser<A>{}(str); }
 
-  static size_t distance(const std::string &s1, const std::string &s2);
+  static size_t distance(std::string_view s1, std::string_view s2);
 };
 
 template<> struct StringParser<int>

Lib/Timer.cpp

@@ -101,7 +101,7 @@ static std::recursive_mutex EXIT_LOCK;
       std::cout << std::endl;
 
       if (szsOutputMode()) {
-        std::cout << STATUS[whichLimit] << (env.options ? env.options->problemName().c_str() : "unknown") << std::endl;
+        std::cout << STATUS[whichLimit] << (env.options ? env.options->problemName.c_str() : "unknown") << std::endl;
       }
     } else // the actual child
       if (env.statistics) {

SAT/Z3MainLoop.cpp

@@ -16,6 +16,7 @@
 
 #include "Forwards.hpp"
 #include "Kernel/Clause.hpp"
+#include "Shell/Property.hpp"
 
 #include "Z3Interfacing.hpp"
 

Saturation/PredicateSplitPassiveClauseContainers.cpp

@@ -14,11 +14,13 @@
 #include <algorithm>
 #include <iterator>
 #include <limits>
+#include <numeric>
 
 #include "Shell/Options.hpp"
 #include "Kernel/Clause.hpp"
 #include "Kernel/HOL/HOL.hpp"
 #include "Kernel/Inference.hpp"
+#include "Lib/Random.hpp"
 #include "Lib/SharedSet.hpp"
 #include "Lib/Int.hpp"
 

Saturation/ProvingHelper.cpp

@@ -14,6 +14,7 @@
 
 #include "Lib/Environment.hpp"
 #include "Debug/TimeProfiling.hpp"
+#include "Lib/Random.hpp"
 #include "Lib/Timer.hpp"
 
 #include "Kernel/Problem.hpp"

Shell/AnswerLiteralManager.cpp

@@ -272,7 +272,7 @@ void AnswerLiteralManager::tryOutputAnswer(Clause* refutation, std::ostream& out
     vss << ")";
   }
   out << postprocessAnswerString(vss.str());
-  out << "|_] for " << env.options->problemName() << endl;
+  out << "|_] for " << env.options->problemName << endl;
 
   // recall what the skolems mean:
   DHSet<unsigned, FnvHash, IdentityHash>::Iterator it(seenSkolems);

Shell/Flattening.cpp

@@ -18,6 +18,7 @@
 #include "Kernel/FormulaUnit.hpp"
 #include "Kernel/Problem.hpp"
 
+#include "Lib/DArray.hpp"
 #include "Lib/Environment.hpp"
 #include "Shell/Options.hpp"
 

Shell/FunctionDefinition.cpp

@@ -17,6 +17,7 @@
 
 #include "Debug/Assertion.hpp"
 #include "Lib/Allocator.hpp"
+#include "Lib/DArray.hpp"
 #include "Lib/Environment.hpp"
 #include "Lib/Random.hpp"
 #include "Lib/ScopedLet.hpp"

Shell/InterpretedNormalizer.cpp

@@ -12,6 +12,7 @@
  * Implements class InterpretedNormalizer.
  */
 
+#include "Lib/DArray.hpp"
 #include "Lib/Environment.hpp"
 #include "Lib/ScopedPtr.hpp"
 

Shell/NNF.cpp

@@ -13,6 +13,7 @@
  * @since 28/12/2003 Manchester
  */
 
+#include "Lib/DArray.hpp"
 #include "Lib/Environment.hpp"
 
 #include "Kernel/Inference.hpp"