Refactoring and Extending Unification with Abstraction

.gitignore

@@ -39,3 +39,6 @@ cmake-build
 
 # vim swap files
 **/.*.swp
+**/.*.swo
+.ccls-cache
+.cache/

CMakeLists.txt

@@ -240,7 +240,7 @@ set(VAMPIRE_KERNEL_SOURCES
     Kernel/Problem.cpp
     Kernel/Renaming.cpp
     Kernel/RobSubstitution.cpp
-    Kernel/MismatchHandler.cpp
+    Kernel/UnificationWithAbstraction.cpp
     Kernel/Signature.cpp
     Kernel/SortHelper.cpp
     Kernel/OperatorType.cpp
@@ -287,7 +287,7 @@ set(VAMPIRE_KERNEL_SOURCES
     Kernel/RCClauseStack.hpp
     Kernel/Renaming.hpp
     Kernel/RobSubstitution.hpp
-    Kernel/MismatchHandler.hpp
+    Kernel/UnificationWithAbstraction.hpp
     Kernel/Signature.hpp
     Kernel/SortHelper.hpp
     Kernel/OperatorType.hpp
@@ -639,8 +639,6 @@ set(VAMPIRE_SHELL_SOURCES
     Shell/Token.hpp
     Shell/TPTPPrinter.hpp
     Shell/TweeGoalTransformation.hpp
-    Shell/UnificationWithAbstractionConfig.hpp
-    Shell/UnificationWithAbstractionConfig.cpp
     Shell/UIHelper.hpp
     Shell/VarManager.hpp
     Shell/Lexer.hpp

DP/SimpleCongruenceClosure.cpp

@@ -75,7 +75,7 @@ vstring SimpleCongruenceClosure::CEq::toString(SimpleCongruenceClosure& parent)
 
 void SimpleCongruenceClosure::ConstInfo::init() {
   sigSymbol = NO_SIG_SYMBOL;
-  term.makeEmpty();
+  term = TermList::empty();
   lit = 0;
   namedPair = CPair(0,0);
   reprConst = 0;
@@ -905,7 +905,7 @@ void SimpleCongruenceClosure::getModel(LiteralStack& model)
 
     cInfo.processed = false;    
     cInfo.half_normalized = false;
-    cInfo.normalForm.makeEmpty();                
+    cInfo.normalForm = TermList::empty();                
 
     if (cInfo.sigSymbol != NO_SIG_SYMBOL) { // either a symbol ...
       // cout << " is sigsym ";

Debug/Output.hpp

@@ -11,17 +11,15 @@
  * @file Forwards.hpp
  * Forward declarations of some classes
  */
-#ifndef __Debug_Output__
-#define __Debug_Output__
+#ifndef __Debug_Output_HPP__
+#define __Debug_Output_HPP__
 
 #include <iostream>
 #include <utility>
+#include <tuple>
 
-namespace Kernel {
 
-template<class A, class B>
-std::ostream& operator<<(std::ostream& out, std::pair<A,B> const& self)
-{ return out << "(" << self.first << ", " << self.second << ")"; }
+namespace Kernel {
 
 /** Newtype in order to nicely output a pointer.
  * Usage: `out << outputPtr(ptr) << std::endl;` 
@@ -36,25 +34,88 @@ struct OutputPtr {
 template<class T>
 OutputPtr<T> outputPtr(T* self) { return { .self = self, }; }
 
+template<class T>
+void repeat(std::ostream& out, T const& c, int times) 
+{ for (int i = 0; i < times; i++) out << c; };
+
+
 /** Newtype for outputting a datatype that implements it in multiline format.
  * Usage: `out << multiline(substitutioTree) << std::endl;` 
  *
  * You can implement this for a `MyType` by implementing 
  * std::ostream& operator<<(std::ostream&, OutputMultiline<MyType>)
  */
 template<class T>
-struct OutputMultiline { T const& self; };
+struct OutputMultiline { 
+  T const& self; 
+  unsigned indent; 
 
-template<class T>
-OutputMultiline<T> multiline(T const& self)
-{ return { self }; }
+  static void outputIndent(std::ostream& out, unsigned indent)
+  { repeat(out, "    ", indent); };
+};
 
 
 template<class T>
-void repeat(std::ostream& out, T const& c, int times) 
-{ for (int i = 0; i < times; i++) out << c; };
+OutputMultiline<T> multiline(T const& self, unsigned indent = 0)
+{ return { self, indent, }; }
 
-static constexpr char const* INDENT = "    ";
+template<class Sep, class Iter>
+struct OutputInterleaved { 
+  Sep const& sep; 
+  Iter iter; 
+};
+
+template<class Sep, class Iter>
+struct OutputInterleaved<Sep,Iter> outputInterleaved(Sep const& s, Iter i)
+{ return OutputInterleaved<Sep, Iter>{s, std::move(i)}; }
+
+
+template<class Iter>
+auto commaSep(Iter i) { return outputInterleaved(", ", std::move(i)); }
+
+template<unsigned i, unsigned sz, class Tup> 
+struct __OutputTuple
+{
+  static void apply(std::ostream& out, Tup const& self)
+  {
+    out << std::get<i>(self) << ", ";
+    __OutputTuple<i + 1, sz, Tup>::apply(out, self);
+  }
+};
+
+template<unsigned i, class Tup> 
+struct __OutputTuple<i, i, Tup>  {
+  static void apply(std::ostream& out, Tup const& self)
+  {
+    out << std::get<i>(self);
+  }
+};
+
+template<class... As> 
+std::ostream& operator<<(std::ostream& out, std::tuple<As...> const& self)
+{ 
+  out << "(";
+  Kernel::__OutputTuple<0, std::tuple_size<std::tuple<As...>>::value - 1, std::tuple<As...>>::apply(out, self);
+  out << ")";
+  return out;
+}
+
+template<class Sep, class Iter>
+std::ostream& operator<<(std::ostream& out, Kernel::OutputInterleaved<Sep, Iter> self)
+{
+  if (self.iter.hasNext()) {
+    out << self.iter.next();
+    while (self.iter.hasNext()) {
+      out << self.sep << self.iter.next();
+    }
+  }
+  return out;
+}
 
 } // namespace Kernel
-#endif // __Debug_Output__
+
+template<class A, class B>
+std::ostream& operator<<(std::ostream& out, std::pair<A,B> const& self)
+{ return out << "(" << self.first << ", " << self.second << ")"; }
+
+#endif // __Debug_Output_HPP__

Debug/TimeProfiling.hpp

@@ -16,7 +16,6 @@
 #include "Lib/Option.hpp"
 #include "Kernel/Ordering.hpp"
 #include "Debug/Assertion.hpp"
-#include "Kernel/Term.hpp"
 #include <chrono>
 #include "Lib/MacroUtils.hpp"
 
@@ -74,6 +73,8 @@ namespace Shell {
 
 #endif // VTIME_PROFILING
 
+#if VTIME_PROFILING
+
 /**
  * A class to trace time for particular blocks. this class shall never be used directly,
  * as it is preprocessed away when the flag VTIME_PROFILING is set to false.
@@ -187,34 +188,7 @@ class TimeTrace
   bool _enabled;
 };
 
-
-template<class Ord>
-class TimeTraceOrdering : public Kernel::Ordering
-{
-  const char* _nameLit;
-  const char* _nameTerm;
-  Ord _ord;
-public:
-  TimeTraceOrdering(const char* nameLit, const char* nameTerm, Ord ord)
-  : _nameLit(nameLit)
-  , _nameTerm(nameTerm)
-  , _ord(std::move(ord))
-  { }
-
-  ~TimeTraceOrdering() override {  }
-
-  Result compare(Kernel::Literal* l1, Kernel::Literal* l2) const final override
-  { TIME_TRACE(_nameLit); return _ord.compare(l1,l2); }
-
-  Result compare(Kernel::TermList l1, Kernel::TermList l2) const final override
-  { TIME_TRACE(_nameTerm); return _ord.compare(l1,l2); }
-
-  void show(std::ostream& out) const final override
-  { _ord.show(out); }
-
-  Ord      & inner()       { return _ord; }
-  Ord const& inner() const { return _ord; }
-};
+#endif // VTIME_PROFILING
 
 } // namespace Shell
 

Debug/Tracer.hpp

@@ -22,6 +22,7 @@
 
 #include <iostream>
 #include <iomanip>
+#include "Debug/Output.hpp"
 
 namespace Debug {
 

FMB/FiniteModelBuilder.cpp

@@ -2375,7 +2375,7 @@ bool FiniteModelBuilder::HackyDSAE::increaseModelSizes(DArray<unsigned>& newSort
 
       // test 2a -- generator constraints
       {
-        Constraint_Generator_Heap::Iterator it(_constraints_generators);
+        auto it = _constraints_generators.iter();
         while (it.hasNext()) {
           if (checkConstriant(newSortSizes,it.next()->_vals)) {
             goto next_candidate;

FMB/FunctionRelationshipInference.cpp

@@ -60,7 +60,7 @@ void FunctionRelationshipInference::findFunctionRelationships(ClauseIterator cla
 
   ClauseList* checkingClauses = getCheckingClauses();
 
-  ClauseIterator cit = pvi(getConcatenatedIterator(clauses,pvi(ClauseList::Iterator(checkingClauses))));
+  ClauseIterator cit = pvi(concatIters(clauses,ClauseList::Iterator(checkingClauses)));
 
   Problem prb(cit,false);
   Options opt; // default saturation algorithm options
@@ -348,7 +348,7 @@ Formula* FunctionRelationshipInference::getName(TermList fromSrt, TermList toSrt
     else
       _labelMap_nonstrict.insert(label,make_pair(fsT,tsT));
 
-    return new AtomicFormula(Literal::create(label,0,true,false,0)); 
+    return new AtomicFormula(Literal::create(label, /* polarity */ true, {})); 
 }
 
 }

FMB/Monotonicity.cpp

@@ -58,9 +58,7 @@ Monotonicity::Monotonicity(ClauseList* clauses, unsigned srt) : _srt(srt)
  ClauseIterator cit = pvi(ClauseList::Iterator(clauses));
  while(cit.hasNext()){
    Clause* c = cit.next();
-   Clause::Iterator lit(*c);
-   while(lit.hasNext()){
-     Literal* l = lit.next();
+   for (auto l : c->iterLits()) {
      monotone(c,l);
    }
  }
@@ -115,9 +113,7 @@ void Monotonicity::safe(Clause* c, Literal* parent, TermList* t,Stack<SATLiteral
     unsigned var = t->var();
     TermList s = SortHelper::getVariableSort(*t,parent);
     if(s.term()->functor()==_srt){
-      Clause::Iterator lit(*c);
-      while(lit.hasNext()){
-        Literal* l = lit.next(); 
+      for (auto l : c->iterLits()) {
         if(guards(l,var,slits)){
           // if guards returns true it means true will be added to the clause
           // so don't bother creating it
@@ -261,7 +257,7 @@ void Monotonicity::addSortPredicates(bool withMon, ClauseList*& clauses, DArray<
      if(!sortedVariables.isEmpty()){
 
        Stack<Literal*> literals; 
-       literals.loadFromIterator(Clause::Iterator(*cl)); 
+       literals.loadFromIterator(cl->iterLits()); 
 
        Stack<std::pair<unsigned,unsigned>>::Iterator vit(sortedVariables);
        while(vit.hasNext()){
@@ -356,10 +352,8 @@ void Monotonicity::addSortFunctions(bool withMon, ClauseList*& clauses)
 
      Stack<Literal*> literals;
 
-     Clause::Iterator lit(*cl);
      bool changed = false;
-     while(lit.hasNext()){
-       Literal* l = lit.next();
+     for (auto l : cl->iterLits()) {
        Literal* lnew = l->arity() == 0 ? l : evaluateLiteralBottomUp(l, SortFunctionTransformer(isMonotonic,sortFunctions));
        if(l!=lnew) {
          changed=true;

Forwards.hpp

@@ -23,7 +23,6 @@ struct EmptyStruct {};
 typedef void (*VoidFunc)();
 
 template<typename T> class VirtualIterator;
-template<typename T, template<class> class ref_t> class ArrayishObjectIterator;
 
 template<typename T> class ScopedPtr;
 template<typename T> class SmartPtr;
@@ -59,8 +58,6 @@ using namespace Lib;
 class Signature;
 
 class Term;
-typedef BiMap<unsigned, Term*> FuncSubtermMap;
-
 class TermList;
 typedef VirtualIterator<TermList> TermIterator;
 typedef Stack<TermList> TermStack;
@@ -69,9 +66,6 @@ typedef List<unsigned> VList; // a list of variables (which are unsigned)
 typedef List<TermList> SList; // a list of sorts (which are now, with polymorphism, TermLists)
 typedef const SharedSet<unsigned> VarSet;
 
-typedef std::pair<std::pair<TermList,unsigned>,std::pair<TermList,unsigned>> UnificationConstraint;
-typedef Stack<UnificationConstraint> UnificationConstraintStack;
-typedef Lib::SmartPtr<UnificationConstraintStack> UnificationConstraintStackSP;
 
 class Literal;
 typedef List<Literal*> LiteralList;
@@ -153,8 +147,6 @@ class TermSharing;
 class ResultSubstitution;
 typedef Lib::SmartPtr<ResultSubstitution> ResultSubstitutionSP;
 
-struct SLQueryResult;
-struct TermQueryResult;
 };
 
 namespace Saturation
@@ -197,5 +189,4 @@ class Options;
 class Property;
 class Statistics;
 }
-
 #endif /* __Forwards__ */

Indexing/AcyclicityIndex.cpp

@@ -379,7 +379,7 @@ namespace Indexing
 
   void AcyclicityIndex::handleClause(Clause* c, bool adding)
   {
-    ArrayishObjectIterator<Clause> it = c->getSelectedLiteralIterator();
+    auto it = c->getSelectedLiteralIterator();
     while (it.hasNext()) {
       if (adding) {
         insert(it.next(), c);

Indexing/ClauseCodeTree.hpp

@@ -97,6 +97,7 @@ class ClauseCodeTree : public CodeTree
   {
     void init(ClauseCodeTree* tree_, Clause* query_, bool sres_);
     void reset();
+    bool keepRecycled() const { return lInfos.keepRecycled(); }
 
     Clause* next(int& resolvedQueryLit);
 

Indexing/ClauseVariantIndex.cpp

@@ -26,6 +26,7 @@
 #include "LiteralSubstitutionTree.hpp"
 
 #include "ClauseVariantIndex.hpp"
+#include "Indexing/IndexManager.hpp"
 
 namespace Indexing
 {
@@ -182,7 +183,7 @@ void SubstitutionTreeClauseVariantIndex::insert(Clause* cl)
   }
 
   if(!_strees[clen]) {
-    _strees[clen]=new LiteralSubstitutionTree();
+    _strees[clen] = new LiteralSubstitutionTree();
   }
   Literal* mainLit=getMainLiteral(cl->literals(), clen);
   _strees[clen]->insert(mainLit, cl);

Indexing/CodeTree.hpp

@@ -392,6 +392,11 @@ class CodeTree
   public:
     bool next();
 
+    bool keepRecycled() const
+    { return bindings.keepRecycled() 
+        || btStack.keepRecycled() 
+        || (firstsInBlocks && firstsInBlocks->keepRecycled()); }
+
   protected:
     void init(CodeOp* entry_, LitInfo* linfos_, size_t linfoCnt_,
 	CodeTree* tree_, Stack<CodeOp*>* firstsInBlocks_);
@@ -488,6 +493,7 @@ class CodeTree
   public:
     /** Variable bindings */
     BindingArray bindings;
+    bool keepRecycled() const { return bindings.keepRecycled(); }
 
   protected:
     /** the matcher object is initialized but no execution of code was done yet */