ALASCA

.gitmodules

@@ -1,3 +1,6 @@
 [submodule "z3"]
 	path = z3
 	url = https://github.com/Z3Prover/z3
+[submodule "viras"]
+	path = viras
+	url = https://github.com/joe-hauns/viras

CASC/PortfolioMode.cpp

@@ -32,6 +32,7 @@
 #include "Shell/Shuffling.hpp"
 #include "Shell/TheoryFinder.hpp"
 
+#include <limits>
 #include <unistd.h>
 #include <signal.h>
 #include <fstream>
@@ -296,7 +297,14 @@ bool PortfolioMode::prepareScheduleAndPerform(const Shell::Property& prop)
  */
 void PortfolioMode::rescaleScheduleLimits(const Schedule& sOld, Schedule& sNew, float limit_multiplier) 
 {
+  ASS(limit_multiplier >= 0)
   Schedule::BottomFirstIterator it(sOld);
+  auto scale = [&](auto v) {
+    unsigned newV = v * limit_multiplier;
+    return limit_multiplier > 0 && newV < v
+       ? /* overflow */ std::numeric_limits<unsigned>::max()
+       : newV;
+    };
   while(it.hasNext()){
     std::string s = it.next();
 
@@ -310,19 +318,19 @@ void PortfolioMode::rescaleScheduleLimits(const Schedule& sOld, Schedule& sNew,
       size_t eidx = s.find_first_of(":_",bidx); // find the end of the number there
       ASS_NEQ(eidx,std::string::npos);
       std::string instrStr = s.substr(bidx,eidx-bidx);
-      unsigned instr;
-      ALWAYS(Int::stringToUnsignedInt(instrStr,instr));
-      instr *= limit_multiplier;
-      s = s.substr(0,bidx) + Lib::Int::toString(instr) + s.substr(eidx);
+      unsigned oldInstr;
+      ALWAYS(Int::stringToUnsignedInt(instrStr,oldInstr));
+      s = s.substr(0,bidx) + Lib::Int::toString(scale(oldInstr)) + s.substr(eidx);
     }
 
     // do the analogous with the time limit suffix
     std::string ts = s.substr(s.find_last_of("_")+1,std::string::npos);
-    unsigned time;
-    ALWAYS(Lib::Int::stringToUnsignedInt(ts,time));
+    unsigned oldTime;
+    ALWAYS(Lib::Int::stringToUnsignedInt(ts,oldTime));
     std::string prefix = s.substr(0,s.find_last_of("_"));
     // Add a copy with increased time limit ...
-    std::string new_time_suffix = Lib::Int::toString((int)(time*limit_multiplier));
+
+    std::string new_time_suffix = Lib::Int::toString(scale(oldTime));
 
     sNew.push(prefix + "_" + new_time_suffix);
   }
@@ -557,7 +565,11 @@ unsigned PortfolioMode::getSliceTime(const std::string &sliceCode)
     sliceTime = 1 + sliceInstr / 200; // rather round up than down (and never return 0 here)
   }
 
-  return _slowness * sliceTime;
+  ASS(_slowness > 0)
+  unsigned res = _slowness * sliceTime;
+  return _slowness >= 1 && res < sliceTime
+    ? /* overflow */ std::numeric_limits<unsigned>::max()
+    : res;
 } // getSliceTime
 
 /**
@@ -568,7 +580,7 @@ void PortfolioMode::runSlice(std::string sliceCode, int timeLimitInDeciseconds)
   TIME_TRACE("run slice");
 
   int sliceTime = getSliceTime(sliceCode);
-  if (sliceTime > timeLimitInDeciseconds 
+  if (sliceTime > timeLimitInDeciseconds
     || !sliceTime) // no limit set, i.e. "infinity"
   {
     sliceTime = timeLimitInDeciseconds;
@@ -580,7 +592,7 @@ void PortfolioMode::runSlice(std::string sliceCode, int timeLimitInDeciseconds)
     Options opt = *env.options;
 
     // opt.randomSeed() would normally be inherited from the parent
-    // addCommentSignForSZS(cout) << "runSlice - seed before setting: " << opt.randomSeed() << endl;    
+    // addCommentSignForSZS(cout) << "runSlice - seed before setting: " << opt.randomSeed() << endl;
     if (env.options->randomizeSeedForPortfolioWorkers()) {
       // but here we want each worker to have their own seed
       opt.setRandomSeed(std::random_device()());

CMakeLists.txt

@@ -213,6 +213,7 @@ set(VAMPIRE_KERNEL_SOURCES
     Kernel/InterpretedLiteralEvaluator.cpp
     Kernel/Rebalancing.cpp
     Kernel/KBO.cpp
+    Kernel/QKbo.cpp
     Kernel/KBOComparator.cpp
     Kernel/LiteralSelector.cpp
     Kernel/LookaheadLiteralSelector.cpp
@@ -263,6 +264,7 @@ set(VAMPIRE_KERNEL_SOURCES
     Kernel/InterpretedLiteralEvaluator.hpp
     Kernel/Rebalancing.cpp
     Kernel/KBO.hpp
+    Kernel/QKbo.hpp
     Kernel/KBOComparator.hpp
     Kernel/LiteralComparators.hpp
     Kernel/LiteralSelector.hpp
@@ -307,6 +309,18 @@ set(VAMPIRE_KERNEL_SOURCES
     Kernel/ApplicativeHelper.cpp
     Kernel/SKIKBO.hpp
     Kernel/SKIKBO.cpp
+    Kernel/ALASCA.hpp
+    Kernel/ALASCA/Signature.hpp
+    Kernel/ALASCA/Signature.cpp
+    Kernel/ALASCA/SelectionPrimitves.hpp
+    Kernel/ALASCA/SelectionPrimitves.cpp
+    Kernel/ALASCA/Normalization.cpp
+    Kernel/ALASCA/Normalization.hpp
+    Kernel/ALASCA/Preprocessor.hpp
+    Kernel/ALASCA/Ordering.hpp
+    Kernel/ALASCA/State.hpp
+    Kernel/ALASCA/State.cpp
+    Kernel/ALASCA/Index.hpp
     Inferences/CNFOnTheFly.cpp
     Inferences/CNFOnTheFly.hpp
     Inferences/CombinatorDemodISE.cpp
@@ -420,6 +434,28 @@ set(VAMPIRE_INFERENCE_SOURCES
     Kernel/Rebalancing.cpp
     Kernel/Rebalancing/Inverters.cpp
     Inferences/Superposition.cpp
+    Inferences/ALASCA/Normalization.cpp
+    Inferences/ALASCA/Normalization.hpp
+    Inferences/ALASCA/InequalityFactoring.cpp
+    Inferences/ALASCA/InequalityFactoring.hpp
+    Inferences/ALASCA/EqFactoring.cpp
+    Inferences/ALASCA/EqFactoring.hpp
+    Inferences/ALASCA/VariableElimination.cpp
+    Inferences/ALASCA/VariableElimination.hpp
+    Inferences/ALASCA/VIRAS.cpp
+    Inferences/ALASCA/VIRAS.hpp
+    Inferences/ALASCA/Superposition.cpp
+    Inferences/ALASCA/Superposition.hpp
+    Inferences/ALASCA/Demodulation.cpp
+    Inferences/ALASCA/Demodulation.hpp
+    Inferences/ALASCA/FwdDemodulation.cpp
+    Inferences/ALASCA/FwdDemodulation.hpp
+    Inferences/ALASCA/BwdDemodulation.cpp
+    Inferences/ALASCA/BwdDemodulation.hpp
+    Inferences/ALASCA/FourierMotzkin.cpp
+    Inferences/ALASCA/FourierMotzkin.hpp
+    Inferences/ALASCA/TermFactoring.cpp
+    Inferences/ALASCA/TermFactoring.hpp
     Inferences/TautologyDeletionISE.cpp
     Inferences/TermAlgebraReasoning.cpp
     Inferences/URResolution.cpp
@@ -711,6 +747,10 @@ set(VAMPIRE_SAT_SUBSUMPTION_SOURCES
 source_group(smt_subsumption_source_files FILES ${VAMPIRE_SAT_SUBSUMPTION_SOURCES})
 
 set(VAMPIRE_TESTING_SOURCES
+    Test/TermIndexTester.hpp
+    Test/BuilderPattern.hpp
+    Test/SimplificationTester.hpp
+    Test/GenerationTester.hpp
     Test/UnitTesting.cpp
     Test/UnitTesting.hpp
     Test/SyntaxSugar.hpp
@@ -726,6 +766,22 @@ set(UNIT_TESTS
     UnitTests/tUnificationWithAbstraction.cpp
     UnitTests/tTermIndex.cpp
     UnitTests/tGaussianElimination.cpp
+    UnitTests/tALASCA_FourierMotzkin.cpp
+    UnitTests/tALASCA_TautologyDeletion.cpp
+    UnitTests/tALASCA_IntegerFourierMotzkin.cpp
+    UnitTests/tALASCA_InequalityFactoring.cpp
+    UnitTests/tALASCA_Normalization.cpp
+    UnitTests/tALASCA_FloorElimination.cpp
+    UnitTests/tALASCA_CoherenceNormalization.cpp
+    UnitTests/tALASCA_Abstraction.cpp
+    UnitTests/tALASCA_Superposition.cpp
+    UnitTests/tALASCA_Coherence.cpp
+    UnitTests/tALASCA_EqFactoring.cpp
+    UnitTests/tALASCA_VariableElimination.cpp
+    UnitTests/tALASCA_TermFactoring.cpp
+    UnitTests/tALASCA_Demodulation.cpp
+    UnitTests/tALASCA_VIRAS.cpp
+    UnitTests/tALASCA_LaKbo.cpp
     UnitTests/tPushUnaryMinus.cpp
     UnitTests/tArithmeticSubtermGeneralization.cpp
     UnitTests/tInterpretedFunctions.cpp
@@ -741,6 +797,7 @@ set(UNIT_TESTS
     UnitTests/tBinaryHeap.cpp
     UnitTests/tSafeRecursion.cpp
     UnitTests/tKBO.cpp
+    UnitTests/tQKbo.cpp
     UnitTests/tSKIKBO.cpp
     UnitTests/tLPO.cpp
     UnitTests/tRatioKeeper.cpp
@@ -749,7 +806,6 @@ set(UNIT_TESTS
     UnitTests/tList.cpp
     UnitTests/tBottomUpEvaluation.cpp
     UnitTests/tCoproduct.cpp
-    UnitTests/tEqualityResolution.cpp
     UnitTests/tIterator.cpp
     UnitTests/tOption.cpp
     UnitTests/tStack.cpp
@@ -812,11 +868,15 @@ include_directories(${CMAKE_CURRENT_SOURCE_DIR})
 add_compile_definitions(CHECK_LEAKS=0)
 if(CMAKE_BUILD_TYPE STREQUAL Debug)
   add_compile_definitions(VDEBUG=1)
+elseif(CMAKE_BUILD_TYPE STREQUAL RelWithDebInfo)
+  add_compile_definitions(VDEBUG=0)
+  add_compile_definitions(NDEBUG)
 elseif(CMAKE_BUILD_TYPE STREQUAL Release)
   add_compile_definitions(VDEBUG=0)
   add_compile_definitions(NDEBUG)
 endif()
 
+add_compile_definitions(ABSOLUTE_SOURCE_DIR="${CMAKE_SOURCE_DIR}")
 # enable for time profiling
 add_compile_definitions(VTIME_PROFILING=0)
 
@@ -830,8 +890,9 @@ list(APPEND CMAKE_MODULE_PATH "${PROJECT_SOURCE_DIR}/cmake-modules")
 # gmp stuff
 ################################################################
 
-find_package(GMP)
-if (GMP_FOUND)
+option(MINI_GMP "compile an own version of mini-gmp instead of linking with system level gmp" ON)
+if (NOT MINI_GMP)
+  find_package(GMP REQUIRED)
   message(STATUS "Found system level gmp version ${GMP_C_LIBRARIES}.")
   add_compile_definitions(VMINI_GMP=0)
   include_directories(${GMP_INCLUDE_DIRS})
@@ -842,7 +903,6 @@ else()
   include_directories(${CMAKE_CURRENT_SOURCE_DIR}/mini-gmp-6.3.0)
 endif()
 
-
 ################################################################
 # z3 stuff
 ################################################################
@@ -874,6 +934,8 @@ else ()
   set(UNIT_TESTS ${UNIT_TESTS} ${UNIT_TESTS_Z3})
 endif()
 
+# add viras package source
+include_directories(${CMAKE_CURRENT_SOURCE_DIR}/viras/src)
 
 ################################################################
 # build objects

Debug/Tracer.hpp

@@ -31,6 +31,16 @@ namespace Tracer {
   void printStack();
 };
 
+struct DebugConfig {
+  unsigned indent = 0;
+};
+static DebugConfig debugConfig;
+
+struct DebugIndentGuard { 
+   DebugIndentGuard() { debugConfig.indent++; } 
+  ~DebugIndentGuard() { debugConfig.indent--; } 
+};
+
 template<class... As>
 struct _printDbg {
   void operator()(const As&... msg);
@@ -58,6 +68,7 @@ template<class... A> void printDbg(const char* file, int line, const A&... msg)
     std::cout << ' ';
   }
   std::cout <<  "@" << std::setw(5) << line << ":";
+  std::cout << Lib::Output::repeat("  ", debugConfig.indent);
   _printDbg<A...>{}(msg...);
   std::cout << std::endl; 
 }
@@ -73,10 +84,12 @@ template<class... A> void printDbg(const char* file, int line, const A&... msg)
 #endif
 
 #  define DBG(...) { Debug::printDbg(__REL_FILE__, __LINE__, __VA_ARGS__); }
+#  define DBG_INDENT Debug::DebugIndentGuard {};
 #  define WARN(...) { DBG("WARNING: ", __VA_ARGS__); }
 #  define DBGE(x) DBG(#x, " = ", x)
 #else // ! VDEBUG
 #  define WARN(...) {}
+#  define DBG_INDENT {}
 #  define DBG(...) {}
 #  define DBGE(x) {}
 #endif

FMB/DefinitionIntroduction.hpp

@@ -18,6 +18,7 @@
 #include "Kernel/Signature.hpp"
 #include "Kernel/Term.hpp"
 #include "Kernel/TermIterators.hpp"
+#include "Debug/TimeProfiling.hpp"
 #include "Kernel/Clause.hpp"
 
 #include "Lib/Environment.hpp"

Forwards.hpp

@@ -55,6 +55,7 @@ class Signature;
 
 class Term;
 class TermList;
+typedef TermList SortId;
 typedef VirtualIterator<TermList> TermIterator;
 typedef Stack<TermList> TermStack;
 
@@ -173,6 +174,7 @@ namespace SAT
 using namespace Lib;
 
 class SATClause;
+class Z3Interfacing;
 class SATLiteral;
 class SATInference;
 class SATSolver;
@@ -181,6 +183,7 @@ typedef VirtualIterator<SATClause*> SATClauseIterator;
 typedef List<SATClause*> SATClauseList;
 typedef Stack<SATClause*> SATClauseStack;
 typedef Stack<SATLiteral> SATLiteralStack;
+
 }
 
 namespace Shell

Indexing/CodeTree.hpp

@@ -555,7 +555,6 @@ class CodeTree
   unsigned _maxVarCnt;
 
   CodeBlock* _entryPoint;
-
 };
 
 }

Indexing/Index.cpp

@@ -14,6 +14,7 @@
  */
 
 #include "Index.hpp"
+#include "Forwards.hpp"
 
 
 namespace Indexing

Indexing/Index.hpp

@@ -24,6 +24,7 @@
 #include "Lib/Exception.hpp"
 #include "Lib/VirtualIterator.hpp"
 #include "Saturation/ClauseContainer.hpp"
+#include "Kernel/Clause.hpp"
 #include "ResultSubstitution.hpp"
 #include "Kernel/UnificationWithAbstraction.hpp"
 #include "Lib/Allocator.hpp"