Merge branch 'master' into z3_datatype_support

.github/workflows/CI.yml

@@ -3,9 +3,6 @@ on:
   workflow_dispatch:
   pull_request:
     types: [opened, reopened, synchronize]
-  schedule:
-    # build at least daily at UTC 00:00 to keep the Z3 build cache warm
-    - cron: '0 0 * * *'
 
 jobs:
   build:
@@ -15,23 +12,20 @@ jobs:
       uses: actions/checkout@v2
       with:
         submodules: true
+    - name: Check Copyright Headers
+      run: checks/headers
     - name: Create Z3 Build Directory
-      run: mkdir ${{runner.workspace}}/vampire/z3/build
-    - name: Cache Z3 Build
-      uses: actions/cache@v2
-      with:
-        path: ${{runner.workspace}}/vampire/z3/build
-        key: ${{runner.os}}-z3-${{hashFiles('.git/modules/z3/HEAD')}}
+      run: mkdir z3/build
     - name: Configure Z3 Build
       working-directory: ${{runner.workspace}}/vampire/z3/build
-      run: test -f libz3.so || cmake .. -DCMAKE_BUILD_TYPE=Debug
+      run: cmake .. -DCMAKE_BUILD_TYPE=Debug
       env:
         CXX: clang++
     - name: Z3 Build
       working-directory: ${{runner.workspace}}/vampire/z3/build
-      run: test -f libz3.so || make -j8
+      run: make -j8
     - name: Create Build Directory
-      run: mkdir ${{runner.workspace}}/vampire/build
+      run: mkdir build
     - name: Configure Build
       working-directory: ${{runner.workspace}}/vampire/build
       run: cmake .. -DCMAKE_BUILD_TYPE=Debug
@@ -43,3 +37,7 @@ jobs:
     - name: Run Unit Tests
       working-directory: ${{runner.workspace}}/vampire/build
       run: ctest --output-on-failure
+    - name: Find Vampire Binary
+      run: cp build/bin/vampire_* vampire
+    - name: Run Sanity Checks
+      run: checks/sanity vampire

.gitignore

@@ -21,6 +21,7 @@ valgrind.supp
 .DS_Store
 .cproject
 .project
+.vscode/
 .settings/
 
 # Problem files

Api/FormulaBuilder.cpp

@@ -1,7 +1,4 @@
-
 /*
- * File FormulaBuilder.cpp.
- *
  * This file is part of the source code of the software program
  * Vampire. It is protected by applicable
  * copyright laws.
@@ -577,7 +574,7 @@ Formula FormulaBuilder::formula(Connective q,const Var& v,const Formula& f)
     throw FormulaBuilderException("formula function called on a Formula object not built by the same FormulaBuilder object");
   }
   if(_aux->_checkBindingBoundVariables) {
-    VarList* boundVars=static_cast<Kernel::Formula*>(f)->boundVariables();
+    VList* boundVars=static_cast<Kernel::Formula*>(f)->boundVariables();
     bool alreadyBound=boundVars->member(v);
     boundVars->destroy();
     if(alreadyBound) {
@@ -598,8 +595,8 @@ Formula FormulaBuilder::formula(Connective q,const Var& v,const Formula& f)
     throw FormulaBuilderException("Invalid quantifier connective");
   }
 
-  Kernel::Formula::VarList* varList=0;
-  Kernel::Formula::VarList::push(v, varList);
+  VList* varList = VList::empty();
+  VList::push(v, varList);
 
   Formula res(new QuantifiedFormula(con, varList, f.form));
   res._aux=_aux; //assign the correct helper object
@@ -662,7 +659,7 @@ Formula FormulaBuilder::substitute(Formula f, Var v, Term t)
 {
   CALL("FormulaBuilder::substitute(Formula)");
 
-  Kernel::Formula::VarList* fBound = f.form->boundVariables();
+  VList* fBound = f.form->boundVariables();
   if(fBound->member(v)) {
     throw ApiException("Variable we substitute for cannot be bound in the formula");
   }
@@ -725,7 +722,7 @@ Formula FormulaBuilder::replaceConstant(Formula f, Term replaced, Term target)
     throw ApiException("The replaced term must be a constant (zero-arity function)");
   }
 
-  Kernel::Formula::VarList* fBound = f.form->boundVariables();
+  VList* fBound = f.form->boundVariables();
   VariableIterator vit(tTgt);
   while(vit.hasNext()) {
     Kernel::TermList tVar = vit.next();
@@ -1085,7 +1082,7 @@ StringIterator Formula::freeVars()
   if(!form) {
     return StringIterator(VirtualIterator<vstring>::getEmpty());
   }
-  VarList* vars=form->freeVariables();
+  VList* vars=form->freeVariables();
   return _aux->getVarNames(vars);
 }
 
@@ -1096,7 +1093,7 @@ StringIterator Formula::boundVars()
   if(!form) {
     return StringIterator(VirtualIterator<vstring>::getEmpty());
   }
-  VarList* vars=form->boundVariables();
+  VList* vars=form->boundVariables();
   return _aux->getVarNames(vars);
 }
 
@@ -1125,9 +1122,9 @@ StringIterator AnnotatedFormula::freeVars()
   if(!unit) {
     return StringIterator(VirtualIterator<vstring>::getEmpty());
   }
-  VarList* vl=0;
+  VList* vl=0;
   if(unit->isClause()) {
-    VarList::pushFromIterator(static_cast<Clause*>(unit)->getVariableIterator(), vl);
+    VList::pushFromIterator(static_cast<Clause*>(unit)->getVariableIterator(), vl);
   }
   else {
     vl=static_cast<FormulaUnit*>(unit)->formula()->freeVariables();
@@ -1142,7 +1139,7 @@ StringIterator AnnotatedFormula::boundVars()
   if(!unit || unit->isClause()) {
     return StringIterator(VirtualIterator<vstring>::getEmpty());
   }
-  VarList* vl=static_cast<FormulaUnit*>(unit)->formula()->boundVariables();
+  VList* vl=static_cast<FormulaUnit*>(unit)->formula()->boundVariables();
   return _aux->getVarNames(vl);
 }
 

Api/FormulaBuilder.hpp

@@ -1,7 +1,4 @@
-
 /*
- * File FormulaBuilder.hpp.
- *
  * This file is part of the source code of the software program
  * Vampire. It is protected by applicable
  * copyright laws.
@@ -21,7 +18,7 @@
 #include <ostream>
 #include <climits>
 
-#include "Helper.hpp"
+//#include "Helper.hpp"
 
 #include "Lib/VString.hpp"
 
@@ -369,7 +366,7 @@ class FormulaBuilder
   Formula replaceConstant(Formula f, Term replaced, Term target);
   AnnotatedFormula replaceConstant(AnnotatedFormula f, Term replaced, Term target);
 private:
-  FBHelper _aux;
+  // FBHelper _aux;
 
   friend class StringIterator;
   friend class Formula;
@@ -527,14 +524,14 @@ class Term
 
   operator Kernel::TermList() const;
   explicit Term(Kernel::TermList t);
-  explicit Term(Kernel::TermList t, ApiHelper aux);
+  // explicit Term(Kernel::TermList t, ApiHelper aux);
 
   bool operator==(const Term& o) const {
     return toString()==o.toString();
   }
 private:
   size_t content;
-  ApiHelper _aux;
+  // ApiHelper _aux;
 
   friend class FormulaBuilder;
   friend class FBHelperCore;
@@ -620,14 +617,14 @@ class Formula
 
   operator Kernel::Formula*() const { return form; }
   explicit Formula(Kernel::Formula* f) : form(f) {}
-  explicit Formula(Kernel::Formula* f, ApiHelper aux) : form(f), _aux(aux) {}
+  // explicit Formula(Kernel::Formula* f, ApiHelper aux) : form(f), _aux(aux) {}
 
   bool operator==(const Formula& o) const {
     return toString()==o.toString();
   }
 private:
   Kernel::Formula* form;
-  ApiHelper _aux;
+  // ApiHelper _aux;
 
   friend class FormulaBuilder;
   friend class FBHelperCore;
@@ -679,7 +676,7 @@ class AnnotatedFormula
 
   operator Kernel::Unit*() const { return unit; }
   explicit AnnotatedFormula(Kernel::Unit* fu) : unit(fu) {}
-  explicit AnnotatedFormula(Kernel::Unit* fu, ApiHelper aux) : unit(fu), _aux(aux) {}
+  // explicit AnnotatedFormula(Kernel::Unit* fu, ApiHelper aux) : unit(fu), _aux(aux) {}
 
   bool operator==(const AnnotatedFormula& o) const {
     return toString()==o.toString();
@@ -688,7 +685,7 @@ class AnnotatedFormula
   static void assignName(AnnotatedFormula& form, Lib::vstring name);
 
   Kernel::Unit* unit;
-  ApiHelper _aux;
+  // ApiHelper _aux;
 
   friend class FormulaBuilder;
   friend class Problem;

Api/Helper.cpp

@@ -1,7 +1,4 @@
-
 /*
- * File Helper.cpp.
- *
  * This file is part of the source code of the software program
  * Vampire. It is protected by applicable
  * copyright laws.
@@ -237,7 +234,7 @@ vstring DefaultHelperCore::toString(const Kernel::Formula* f0) const
   case EXISTS:
   {
     vstring result = vstring("(") + con + "[";
-    Kernel::Formula::VarList::Iterator vit(f->vars());
+    VList::Iterator vit(f->vars());
     ASS(vit.hasNext());
     while (vit.hasNext()) {
       unsigned var = vit.next();
@@ -401,13 +398,13 @@ struct DefaultHelperCore::Var2NameMapper
   DefaultHelperCore& aux;
 };
 
-StringIterator DefaultHelperCore::getVarNames(VarList* l)
+StringIterator DefaultHelperCore::getVarNames(VList* l)
 {
   CALL("DefaultHelperCore::getVarNames");
 
   VirtualIterator<vstring> res=pvi( getPersistentIterator(
       getMappingIterator(
-	  VarList::DestructiveIterator(l),
+	  VList::DestructiveIterator(l),
 	  Var2NameMapper(*this))
   ) );
 

Api/Helper.hpp

@@ -1,7 +1,4 @@
-
 /*
- * File Helper.hpp.
- *
  * This file is part of the source code of the software program
  * Vampire. It is protected by applicable
  * copyright laws.

Api/Helper_Internal.hpp

@@ -1,7 +1,4 @@
-
 /*
- * File Helper_Internal.hpp.
- *
  * This file is part of the source code of the software program
  * Vampire. It is protected by applicable
  * copyright laws.
@@ -43,8 +40,6 @@ namespace Api {
 
 using namespace Shell;
 
-typedef Kernel::Formula::VarList VarList;
-
 class DefaultHelperCore
 {
 public:
@@ -67,7 +62,7 @@ class DefaultHelperCore
 private:
   struct Var2NameMapper;
 public:
-  StringIterator getVarNames(VarList* l);
+  StringIterator getVarNames(VList* l);
 
   static vstring getDummyName(bool pred, unsigned functor);
   static vstring getDummyName(const Kernel::Term* t);

Api/Problem.cpp

@@ -1,7 +1,4 @@
-
 /*
- * File Problem.cpp.
- *
  * This file is part of the source code of the software program
  * Vampire. It is protected by applicable
  * copyright laws.
@@ -482,7 +479,7 @@ void Problem::addFromStream(istream& s, vstring includeDirectory, bool simplifyS
     SimplifyProver simplify;
     units = simplify.units(expr);
   }
-  else {
+  else { 
     units = Parse::TPTP::parse(s);
   }
 

Api/Problem.hpp

@@ -1,7 +1,4 @@
-
 /*
- * File Problem.hpp.
- *
  * This file is part of the source code of the software program
  * Vampire. It is protected by applicable
  * copyright laws.
@@ -364,7 +361,7 @@ class Problem
     friend class Problem;
     void validate() const;
 
-    void prepareOptionsReader(OptionsReader& rdr);
+    // void prepareOptionsReader(OptionsReader& rdr);
     void setDefaults();
 
     struct Atom2LitFn;

Api/ResourceLimits.cpp

@@ -1,7 +1,4 @@
-
 /*
- * File ResourceLimits.cpp.
- *
  * This file is part of the source code of the software program
  * Vampire. It is protected by applicable
  * copyright laws.

Api/ResourceLimits.hpp

@@ -1,7 +1,4 @@
-
 /*
- * File ResourceLimits.hpp.
- *
  * This file is part of the source code of the software program
  * Vampire. It is protected by applicable
  * copyright laws.

Api/Tracing.cpp

@@ -1,7 +1,4 @@
-
 /*
- * File Tracing.cpp.
- *
  * This file is part of the source code of the software program
  * Vampire. It is protected by applicable
  * copyright laws.

Api/Tracing.hpp

@@ -1,7 +1,4 @@
-
 /*
- * File Tracing.hpp.
- *
  * This file is part of the source code of the software program
  * Vampire. It is protected by applicable
  * copyright laws.

CASC/CLTBMode.cpp

@@ -1,7 +1,4 @@
-
 /*
- * File CLTBMode.cpp.
- *
  * This file is part of the source code of the software program
  * Vampire. It is protected by applicable
  * copyright laws.

CASC/CLTBMode.hpp

@@ -1,7 +1,4 @@
-
 /*
- * File CLTBMode.hpp.
- *
  * This file is part of the source code of the software program
  * Vampire. It is protected by applicable
  * copyright laws.

CASC/CLTBModeLearning.cpp

@@ -1,7 +1,4 @@
-
 /*
- * File CLTBModeLearning.cpp.
- *
  * This file is part of the source code of the software program
  * Vampire. It is protected by applicable
  * copyright laws.

CASC/CLTBModeLearning.hpp

@@ -1,7 +1,4 @@
-
 /*
- * File CLTBModeLearning.hpp.
- *
  * This file is part of the source code of the software program
  * Vampire. It is protected by applicable
  * copyright laws.