From 74c45ee43b46d93e72c0b37621bddc13bd166d43 Mon Sep 17 00:00:00 2001 From: Giles <--global> Date: Fri, 20 Oct 2017 09:48:18 +0100 Subject: [PATCH] tidying --- Build_LLVM_and_CLANG.txt | 20 -------------- ClausifierDependencyFix.cpp | 54 ------------------------------------- explanation | 51 ----------------------------------- ltb_mode | 30 --------------------- 4 files changed, 155 deletions(-) delete mode 100644 Build_LLVM_and_CLANG.txt delete mode 100644 ClausifierDependencyFix.cpp delete mode 100644 explanation delete mode 100755 ltb_mode diff --git a/Build_LLVM_and_CLANG.txt b/Build_LLVM_and_CLANG.txt deleted file mode 100644 index 1becbf7fcd..0000000000 --- a/Build_LLVM_and_CLANG.txt +++ /dev/null @@ -1,20 +0,0 @@ -In order to compile and use clang and LLVM you have to perform the following: - -1. download llvm and clang distributions - in order to make sure the code behaves as expected, please use RELEASE_30 (revision 155707). The llvm distribution can be downloaded using svn co http://llvm.org/svn/llvm-project/llvm/trunk . Let's call the directory where you downloaded this distribution $LLVM_ROOT. Now you have to download the clang distribution. -2. Download it into $LLVM_ROOT/tools/clang using svn from: svn co http://llvm.org/svn/llvm-project/cfe/trunk - take care for the revision number. IT IS IMPORTANT TO HAVE THE SAME RELEASE_30 (revision 155707). -Once the download is done, you can start building the sistem - depending on the hardware you have, it might take a while (aprox. 30-40 min). - -3. Create the directory $LLVM_SRC_ROOT/../build (let's call it $LLVM_OBJ_ROOT). -4. cd $LLVM_OBJ_ROOT -5. $LLVM_SRC_ROOT/configure -6. make - -NOTE that the in order to perform all the above steps one needs to have several software packages installed. More details can be found here: http://llvm.org/docs/GettingStarted.html#requirements -Also more details about compilation and installation of llvm and clang can be found here: http://clang.llvm.org/get_started.html - -Now that you have build the llvm+clang system, you still have to install it. For this purpose run make install. - -In order to compile correctly the project, one has to create three symbolic links: -1. RelClang - to the directory where you installed the llvm+clang ( linux default: /usr/local/lib/ ) -2. SrcInclude - should link to the $LLVM_SRC_ROOT/include -3. BuildInclude - should link to $LLVM_OBJ_ROOT/include diff --git a/ClausifierDependencyFix.cpp b/ClausifierDependencyFix.cpp deleted file mode 100644 index cd79f81bbc..0000000000 --- a/ClausifierDependencyFix.cpp +++ /dev/null @@ -1,54 +0,0 @@ -/** - * @file ClausifierDependencyFix.cpp - * - * Provides dummy implementations for some functions - * referenced in code that is used in clausifier. - */ - -#include "Forwards.hpp" - -#include "Lib/Exception.hpp" - -#include "Kernel/LiteralSelector.hpp" - -#include "Saturation/SaturationAlgorithm.hpp" -#include "Shell/AnswerExtractor.hpp" -#include "Shell/InterpolantMinimizer.hpp" - -void LiteralSelector::reversePredicatePolarity(unsigned pred, bool reverse) -{ -} - -void Saturation::SaturationAlgorithm::tryUpdateFinalClauseCount() -{ -} - -Shell::InterpolantMinimizer::InterpolantMinimizer(OptimizationTarget, bool, bool, vstring) -{ -} -Shell::InterpolantMinimizer::~InterpolantMinimizer() -{ -} -Kernel::Formula* Shell::InterpolantMinimizer::getInterpolant(Kernel::Unit*) -{ - INVALID_OPERATION("not supported in clausifier"); -} - -void AnswerExtractor::tryOutputAnswer(Clause* refutation) -{ - INVALID_OPERATION("not supported in clausifier"); -} - -AnswerLiteralManager* AnswerLiteralManager::getInstance() -{ - INVALID_OPERATION("answer literals not supported in clausifier"); -} - -bool AnswerLiteralManager::addAnswerLiterals(UnitList*& units) -{ - INVALID_OPERATION("answer literals not supported in clausifier"); -} -void AnswerLiteralManager::addAnswerLiterals(Problem& prb) -{ - INVALID_OPERATION("answer literals not supported in clausifier"); -} diff --git a/explanation b/explanation deleted file mode 100644 index e07b864f48..0000000000 --- a/explanation +++ /dev/null @@ -1,51 +0,0 @@ -These explanation files are in each directory and should be used to give a *brief* explanation of a file, if not obvious from the file name. - -Build_LLVM_and_CLANG.txt Explanation of how to setup LLVM and clang for LINGVA compilation -ClausifierDependencyFix.cpp Looks like no longer needed, removed from Makefile -compit2.cpp Looks like a framework for running -compit2.hpp benchmarks for unification -compit2_impl.cpp perhaps belongs in a separate benchmarking area -config.doc Configuration for documentation (doxygen) -Config.hpp Part of the compit framework -dummy_main.cpp Dummy main file (not in Makefile) -Forwards.hpp Forward declarations -Global.cpp Global static member initialisation -licence.pl Perl script for adding licence headers -ltb_mode Bash script for running ltb mode (syntax unknown) -Makefile Makefile - Many targets seem to be a mode-restricted version of vampire - Targets are: - -lingva: invariant generation (requiers llvm and clang) - -vampire: standard vampire - -vcompit: unification benchmarks - -vltb: BROKEN - -vclausify: BROKEN - -vtest: BROKEN - -vutil: BROKEN - -vsat: BROKEN - -vapi: BROKEN - -libvapi: BROKEN - -test_libvapi: BROKEN - -tkv: BROKEN - -clausify_src: BROKEN - -api_src: BROKEN - -vground: BROKEN - -clean - -depend -out_summary Bash script for summarising the output of experiments -README.md Currently empty readme -runner.sh Bash script wrapper for running (with spider) -test_libvapi.cpp Main for test_libvapi target -test_vapi.cpp Main for test_vapi target -todo_list.txt -ucompit.cpp Related to compit framework -vampire.cpp Main for vampire (and lingva) target -vclausify.cpp Main for vclausify target -vcompit.cpp Main for vcompit target -version.cpp Automatically generated version file -vground.cpp Main for vground target -vinter Bash script for vinter (uses vutil) -vltb.cpp Main for vltb target -vsat.cpp Main for vsat target -vtest.cpp Main for vtest target -vutil.cpp Main for vutil target diff --git a/ltb_mode b/ltb_mode deleted file mode 100755 index 89cdad6901..0000000000 --- a/ltb_mode +++ /dev/null @@ -1,30 +0,0 @@ -#!/bin/bash - -EXEC=$1 -FNAME=$2 -shift 2 -ARGS="$*" -memcached -s vampire_mc_socket -m 512 -v & - -#high timelimit because if we don't finish the theory loading, we're lost anyway -$EXEC $ARGS --mode ltb_build -t 120 < $FNAME - - - - -JOBS="`grep -v '^#' $FNAME | awk ' - BEGIN { fileSection=0; } - /% SZS start BatchProblems/ { fileSection=1; } - /% SZS end BatchProblems/ { fileSection=0; } - /^[^%]/ { if(fileSection) { print $0 } } -' | tr ' ' ':' |sed 's/:*$//'`" - -for JOB in $JOBS ; do - INP=${JOB%%:*} - OUTP=${JOB#*:} - - echo $INP - $EXEC $ARGS --mode ltb_solve --input_file $INP |tee $OUTP -done - -kill %?memcached \ No newline at end of file