vampire.cpp

/*
 * This file is part of the source code of the software program
 * Vampire. It is protected by applicable
 * copyright laws.
 *
 * This source code is distributed under the licence found here
 * https://vprover.github.io/license.html
 * and in the source directory
 */
/**
 * @file vampire.cpp. Implements the top-level procedures of Vampire.
 */

#include <iostream>
#include <ostream>

#if VZ3
#include "z3++.h"
#endif

#include "Debug/TimeProfiling.hpp"
#include "Lib/Exception.hpp"
#include "Lib/Environment.hpp"
#include "Lib/Random.hpp"
#include "Lib/Timer.hpp"
#include "Lib/List.hpp"
#include "Lib/System.hpp"
#include "Lib/StringUtils.hpp"
#include "Lib/Sys/Multiprocessing.hpp"
#include "Lib/Int.hpp"

#include "Kernel/Clause.hpp"
#include "Kernel/Formula.hpp"
#include "Kernel/FormulaUnit.hpp"
#include "Kernel/Problem.hpp"
#include "Kernel/Signature.hpp"
#include "Kernel/Term.hpp"

#include "Inferences/InferenceEngine.hpp"
#include "Inferences/TautologyDeletionISE.hpp"

#include "CASC/PortfolioMode.hpp"
#include "Shell/CommandLine.hpp"

#include "Shell/Normalisation.hpp"
#include "Shell/Options.hpp"
#include "Shell/Property.hpp"
#include "Saturation/ProvingHelper.hpp"
#include "Shell/Preprocess.hpp"
#include "Shell/TheoryFinder.hpp"
#include "Shell/TPTPPrinter.hpp"
#include "Parse/TPTP.hpp"
#include "Shell/Statistics.hpp"
#include "Shell/UIHelper.hpp"

#include "Saturation/SaturationAlgorithm.hpp"

#include "FMB/ModelCheck.hpp"

using namespace std;

/**
 * Return value is non-zero unless we were successful.
 *
 * Being successful for modes that involve proving means that we have
 * either found refutation or established satisfiability.
 *
 *
 * If Vampire was interrupted (e.g. SIGINT, SIGHUP), value VAMP_RESULT_STATUS_INTERRUPTED is returned,
 * and in case of other signal we return VAMP_RESULT_STATUS_OTHER_SIGNAL. For implementation
 * of these return values see Lib/System.hpp.
 *
 * In case of an unhandled exception or user error, we return value
 * VAMP_RESULT_STATUS_UNHANDLED_EXCEPTION.
 *
 * In case Vampire was terminated by the timer, return value is
 * uncertain (but definitely not zero), probably it will be 134
 * (we terminate by a call to the @b abort() function in this case).
 */
int vampireReturnValue = VAMP_RESULT_STATUS_UNKNOWN;

/**
 * Preprocess the given problem (in dependence of env.options).
 *
 * The problem is modified destructively.
 */
[[nodiscard]]
Problem* preprocessProblem(Problem* prb)
{
  // Here officially starts preprocessing of vampireMode
  // and that's the moment we want to set the random seed (no randomness in parsing, for the peace of mind)
  // the main reason being that we want to stay in sync with what portfolio mode will do
  // cf ProvingHelper::runVampire
  if (env.options->randomSeed() != 0) {
    Lib::Random::setSeed(env.options->randomSeed());
  } else {
    Lib::Random::resetSeed();
  }

  TIME_TRACE(TimeTrace::PREPROCESSING);

  // this will provide warning if options don't make sense for problem
  if (env.options->mode() != Options::Mode::SPIDER) {
    env.options->checkProblemOptionConstraints(prb->getProperty(), /*before_preprocessing = */ true);
  }

  Shell::Preprocess prepro(*env.options);
  //phases for preprocessing are being set inside the preprocess method
  prepro.preprocess(*prb);

  return prb;
} // getPreprocessedProblem

void explainException(Exception& exception)
{
  exception.cry(std::cout);
} // explainException

[[nodiscard]]
Problem *doProving(Problem* problem)
{
  if (env.options->showPropDict()) {
    cout << "% Prop: " << problem->getProperty()->toDict() << endl;
  }

  // a new strategy randomization mechanism
  if (!env.options->strategySamplerFilename().empty()) {
    env.options->sampleStrategy(env.options->strategySamplerFilename(),
      problem->getProperty()->toDict());
  }

  env.options->setForcedOptionValues();
  env.options->checkGlobalOptionConstraints();

  Problem *prb = preprocessProblem(problem);

  // this will provide warning if options don't make sense for problem
  if (env.options->mode() != Options::Mode::SPIDER) {
    env.options->checkProblemOptionConstraints(prb->getProperty(), /*before_preprocessing = */ false);
  }

  ProvingHelper::runVampireSaturation(*prb, *env.options);
  return prb;
}

/**
 * Read a problem and output profiling information about it.
 * @since 03/08/2008 Torrevieja
 */
void profileMode(Problem* problem)
{
  ScopedPtr<Problem> prb(problem);

  /* CAREFUL: Make sure that the order
   * 1) getProperty, 2) normalise, 3) TheoryFinder::search
   * is the same as in PortfolioMode::searchForProof
   * also, cf. the beginning of Preprocessing::preprocess*/
  Property* property = prb->getProperty();
  Normalisation().normalise(*prb);
  TheoryFinder(prb->units(), property).search();

  std::cout << property->categoryString() << ' ' << property->props() << ' '
	  << property->atoms() << "\n";

  //we have succeeded with the profile mode, so we'll terminate with zero return value
  vampireReturnValue = VAMP_RESULT_STATUS_SUCCESS;
} // profileMode

/**
 * This mode only preprocesses the input using the current preprocessing
 * options and outputs it to stdout. It is useful for either preprocessing
 * per se or also for converting one syntax to another. For the latter, the input
 * and the output syntaxes must be set to different values. Note that for
 * simply translating one syntax to another, output mode is the right one.
 *
 * @author Andrei Voronkov
 * @since 02/07/2013 Manchester
 */
void preprocessMode(Problem* problem, bool theory)
{
  ScopedPtr<Problem> prb(problem);

  TIME_TRACE(TimeTrace::PREPROCESSING);

  // preprocess without clausification
  Shell::Preprocess prepro(*env.options);
  prepro.turnClausifierOff();
  if(env.options->mode() == Options::Mode::PREPROCESS2){
    prepro.keepSimplifyStep();
  }
  prepro.preprocess(*prb);

  const auto language = TPTPPrinter::outputLanguage(!theory && !prb->hasFormulas());
  const auto declarationLanguage = language == TPTPOutput::Language::CNF || language == TPTPOutput::Language::FOF
      ? TPTPOutput::Language::TFF : language;
  std::cout << TPTPPrinter::symbolDeclarations(declarationLanguage);
  UnitList::Iterator units(prb->units());
  while (units.hasNext()) {
    Unit* u = units.next();
    if (!env.options->showFOOL()) {
      if (u->inference().rule() == InferenceRule::FOOL_AXIOM_TRUE_NEQ_FALSE || u->inference().rule() == InferenceRule::FOOL_AXIOM_ALL_IS_TRUE_OR_FALSE) {
        continue;
      }
    }

    if (theory) {
      Formula* f = u->getFormula();
      FormulaUnit* fu = new FormulaUnit(f,u->inference()); // we are stealing u's inference which is not nice
      std::cout << TPTPPrinter::unit(fu, language, UIHelper::outputRole(fu)) << "\n";
    } else {
      std::cout << TPTPPrinter::unit(u, language, UIHelper::outputRole(u)) << "\n";
    }
  }

  //we have successfully output all clauses, so we'll terminate with zero return value
  vampireReturnValue = VAMP_RESULT_STATUS_SUCCESS;
} // preprocessMode

/**
 *
 * @author Giles
 * @since 6/10/2015
 */
void modelCheckMode(Problem* problem)
{
  ScopedPtr<Problem> prb(problem);

  // model definitions are recorded by the TPTP parser
  if (env.options->inputSyntax() == Options::InputSyntax::SMTLIB2) {
    USER_ERROR("Mode model_check only supports TPTP input");
  }
  if(env.getMainProblem()->hasPolymorphicSym() || env.getMainProblem()->isHigherOrder()){
    USER_ERROR("Polymorphic Vampire is not yet compatible with theory reasoning");
  }

  FMB::ModelCheck::doCheck(prb->units());
} // modelCheckMode


/**
 * This mode only outputs the input problem. It is useful for converting
 * one syntax to another.
 * @author Laura Kovacs and Andrei Voronkov
 * @since 02/07/2013 Gothenburg and Manchester
 */
void outputMode(Problem* problem)
{
  ScopedPtr<Problem> prb(problem);

  const auto language = TPTPPrinter::outputLanguage(!prb->hasFormulas());
  const auto declarationLanguage = language == TPTPOutput::Language::CNF || language == TPTPOutput::Language::FOF
      ? TPTPOutput::Language::TFF : language;
  std::cout << TPTPPrinter::symbolDeclarations(declarationLanguage);
  UnitList::Iterator units(prb->units());

  while (units.hasNext()) {
    Unit* u = units.next();
    if (u->inference().rule() == InferenceRule::CONJECTURE_NEGATION) {
      // the parsers negate a conjecture right away; output the one that was stated
      UnitIterator parents = u->getParents();
      ALWAYS(parents.hasNext());
      u = parents.next();
      ASS(!parents.hasNext());
      ASS(u->inference().rule() == InferenceRule::INPUT);
    }
    std::cout << TPTPPrinter::unit(u, language, UIHelper::outputRole(u)) << "\n";
  }

  //we have successfully output all clauses, so we'll terminate with zero return value
  vampireReturnValue = VAMP_RESULT_STATUS_SUCCESS;
} // outputMode

void vampireMode(Problem* problem)
{
  if (env.options->mode() == Options::Mode::CONSEQUENCE_ELIMINATION) {
    env.options->setUnusedPredicateDefinitionRemoval(false);
  }

  ScopedPtr<Problem> prb(doProving(problem));

  UIHelper::outputResult(std::cout);

  if (env.statistics->terminationReason == TerminationReason::REFUTATION
      || env.statistics->terminationReason == TerminationReason::SATISFIABLE) {
      vampireReturnValue = VAMP_RESULT_STATUS_SUCCESS;
  }
} // vampireMode

void spiderMode(Problem* problem)
{
  env.options->setBadOptionChoice(Options::BadOption::HARD);
  env.options->setOutputMode(Options::Output::SPIDER);
  env.options->setNormalize(true);

  Exception* exception = 0;
#if VZ3
  z3::exception* z3_exception = 0;
#endif

  bool exceptionRaised = false;
  ScopedPtr<Problem> prb;
  try {
    prb = doProving(problem);
  } catch (Exception& e) {
    exception = &e;
    exceptionRaised = true;
#if VZ3
  } catch(z3::exception& e){
    z3_exception = &e;
    exceptionRaised = true;
#endif
  } catch (...) {
    exceptionRaised = true;
  }

  if (!exceptionRaised) {
    switch (env.statistics->terminationReason) {
    case TerminationReason::REFUTATION:
      reportSpiderStatus('+');
      vampireReturnValue = VAMP_RESULT_STATUS_SUCCESS;
      break;
    case TerminationReason::TIME_LIMIT:
      reportSpiderStatus('t');
      break;
    case TerminationReason::MEMORY_LIMIT:
      reportSpiderStatus('m');
      break;
    case TerminationReason::UNKNOWN:
    case TerminationReason::INAPPROPRIATE:
      reportSpiderStatus('u');
      break;
    case TerminationReason::REFUTATION_NOT_FOUND:
      if (env.statistics->discardedNonRedundantClauses > 0) {
        reportSpiderStatus('n');
      }
      else{
        reportSpiderStatus('i');
      }
      break;
    case TerminationReason::SATISFIABLE:
      reportSpiderStatus('-');
      vampireReturnValue = VAMP_RESULT_STATUS_SUCCESS;
      break;
    default:
      ASSERTION_VIOLATION;
    }
    return;
  }

  // exception
  vampireReturnValue = VAMP_RESULT_STATUS_UNHANDLED_EXCEPTION;

#if VZ3
  if (z3_exception) {
    if (strcmp(z3_exception->msg(),"out of memory\n")) {
      reportSpiderStatus('m');
    }
    else {
      reportSpiderFail();
    }

    return;
  }
#endif

  reportSpiderFail();

  ASS(exception);
  explainException(*exception);
} // spiderMode

void clausifyMode(Problem* problem, bool theory)
{
  CompositeISE simplifier;
  simplifier.addFront(new TrivialInequalitiesRemovalISE());
  simplifier.addFront(new TautologyDeletionISE());
  simplifier.addFront(new DuplicateLiteralRemovalISE());

  if (!env.options->strategySamplerFilename().empty()) {
    env.options->sampleStrategy(env.options->strategySamplerFilename(),
      problem->getProperty()->toDict());
  }

  ScopedPtr<Problem> prb(preprocessProblem(problem));

  // with theory, we print tcf(), i.e. the clause quantified with its variables' sorts
  TPTPOutput::Language clauseLanguage = TPTPOutput::Language::CNF;
  if (theory) {
    clauseLanguage = TPTPOutput::Language::TCF;
  }
  const auto declarationLanguage = theory ? TPTPOutput::Language::TCF
      : env.higherOrder() ? TPTPOutput::Language::THF : TPTPOutput::Language::TFF;
  std::cout << TPTPPrinter::symbolDeclarations(declarationLanguage);

  ClauseIterator cit = prb->clauseIterator();
  bool printed_conjecture = false;
  while (cit.hasNext()) {
    Clause* cl = cit.next();
    cl = simplifier.simplify(cl);
    if (!cl) {
      continue;
    }
    printed_conjecture |= cl->inputType() == UnitInputType::CONJECTURE || cl->inputType() == UnitInputType::NEGATED_CONJECTURE;
    std::cout << TPTPPrinter::unit(cl, clauseLanguage, UIHelper::outputRole(cl)) << "\n";
  }
  if(!printed_conjecture && UIHelper::haveConjecture()){
    // print a fake tautology conjecture for Kostya and friends
    // (otherwise they can't tell whether the input contained a conjecture or not
    //  which is important for reporting the SZS status)
    unsigned p = env.signature->addFreshPredicate(0,"p")->number();
    auto c = Clause::fromLiterals({
        Literal::create(p, /* polarity */ true , {}),
        Literal::create(p, /* polarity */ false, {})
      },
      FromInput(UnitInputType::NEGATED_CONJECTURE));
    std::cout << TPTPPrinter::unit(c, clauseLanguage, UIHelper::outputRole(c)) << "\n";
  }

  //we have successfully output all clauses, so we'll terminate with zero return value
  vampireReturnValue = VAMP_RESULT_STATUS_SUCCESS;
} // clausifyMode

void dispatchByMode(Problem* problem)
{
  switch (env.options->mode())
  {
  case Options::Mode::SPIDER:
    spiderMode(problem);
    break;
  case Options::Mode::CONSEQUENCE_ELIMINATION:
  case Options::Mode::VAMPIRE:
    vampireMode(problem);
    break;

  case Options::Mode::CASC:
    env.options->setIgnoreMissing(Options::IgnoreMissing::WARN);
    if (env.options->intent() == Options::Intent::UNSAT) {
      env.options->setSchedule(Options::Schedule::CASC);
    } else {
      env.options->setSchedule(Options::Schedule::CASC_SAT);
    }
    // unfortunatelly, setting these here make not difference (the need to be before during parsing)
    // env.options->setInputSyntax(Options::InputSyntax::TPTP);
    // env.options->setOutputAxiomNames(true);
    env.options->setOutputMode(Options::Output::SZS);
    env.options->setProof(Options::Proof::TPTP);

    // env.options->setNormalize(true);
    // env.options->setRandomizeSeedForPortfolioWorkers(false);

    if (CASC::PortfolioMode::perform(problem)) {
      vampireReturnValue = VAMP_RESULT_STATUS_SUCCESS;
    }
    break;

  case Options::Mode::SMTCOMP:
    env.options->setIgnoreMissing(Options::IgnoreMissing::OFF);
    // env.options->setInputSyntax(Options::InputSyntax::SMTLIB2);
    if(env.options->outputMode() != Options::Output::UCORE){
      env.options->setOutputMode(Options::Output::SMTCOMP);
    }
    env.options->setSchedule(Options::Schedule::SMTCOMP);
    env.options->setProof(Options::Proof::OFF);
    env.options->setNormalize(true);
    env.options->setRandomizeSeedForPortfolioWorkers(false);

    env.options->setMulticore(0); // use all available cores
    env.options->setTimeLimitInSeconds(1800);
    env.options->setStatistics(Options::Statistics::NONE);

    //TODO needed?
    // to prevent from terminating by time limit
    env.options->setTimeLimitInSeconds(100000);

    if (CASC::PortfolioMode::perform(problem)){
      vampireReturnValue = VAMP_RESULT_STATUS_SUCCESS;
    }
    else {
      cout << "unknown" << endl;
    }
    break;

  case Options::Mode::PORTFOLIO:
    env.options->setIgnoreMissing(Options::IgnoreMissing::WARN);

    if (CASC::PortfolioMode::perform(problem)) {
      vampireReturnValue = VAMP_RESULT_STATUS_SUCCESS;
    }
    break;
  case Options::Mode::MODEL_CHECK:
    modelCheckMode(problem);
    break;

  case Options::Mode::CLAUSIFY:
    clausifyMode(problem,false);
    break;

  case Options::Mode::TCLAUSIFY:
    clausifyMode(problem,true);
    break;

  case Options::Mode::OUTPUT:
    outputMode(problem);
    break;

  case Options::Mode::PROFILE:
    profileMode(problem);
    break;

  case Options::Mode::PREPROCESS:
  case Options::Mode::PREPROCESS2:
    preprocessMode(problem,false);
    break;

  case Options::Mode::TPREPROCESS:
    preprocessMode(problem,true);
    break;
  }
}

void interactiveMetamode()
{
  Options& opts = *env.options;
  opts.setInteractive(false); // so that we don't pass the interactivity on to the workers

  ScopedPtr<Problem> prb;
  if (!opts.inputFile().empty()) {
    UIHelper::parseFile(opts.inputFile(),opts.inputSyntax(),true);
    opts.resetInputFile();
  } // no parsing of the whole cin in interactiveMetamode
  prb = UIHelper::getInputProblem();

  while (true) {
    std::string line;
    if (!getline(cin, line) || line.rfind("exit",0) == 0) {
      cout << "Bye." << endl;
      break;
    } else if (line.rfind("run",0) == 0) {
      // the whole running happens in a child (don't modify our options, don't crash here when parsing option rubbish, etc.)
      pid_t process = Sys::fork();
      ASS_NEQ(process, -1);
      if(process == 0) {
        UIHelper::unsetExpecting(); // probably garbage at this point

        Stack<std::string> pieces;
        StringUtils::splitStr(line.c_str(),' ',pieces);
        StringUtils::dropEmpty(pieces);
        Stack<const char*> argv(pieces.size());
        for(auto it = pieces.iterFifo(); it.hasNext();) {
          argv.push(it.next().c_str());
        }
        Shell::CommandLine cl(argv.size(), argv.begin());
        cl.interpret(opts);

        Timer::reinitialise(); // start our timer (in the child)

        if (!opts.inputFile().empty()) {
          UIHelper::parseFile(opts.inputFile(),opts.inputSyntax(),true);
          prb = UIHelper::getInputProblem();
        }
        dispatchByMode(prb.ptr());
        exit(vampireReturnValue);
      }
    } else if (line.rfind("load",0) == 0) {
      Stack<std::string> pieces;
      StringUtils::splitStr(line.c_str(),' ',pieces);
      StringUtils::dropEmpty(pieces);
      auto it = pieces.iterFifo();
      ALWAYS(it.next() == "load");
      while (it.hasNext()) {
        UIHelper::parseFile(it.next(),opts.inputSyntax(),true);
      }
      prb = UIHelper::getInputProblem();
    } else if (line.rfind("tptp ",0) == 0) {
      try {
        UIHelper::parseSingleLine(line.substr(5),Options::InputSyntax::TPTP);
        prb = UIHelper::getInputProblem();
      } catch (ParsingRelatedException& exception) {
        explainException(exception);
      }
    } else if (line.rfind("smt2 ",0) == 0) {
      try {
        UIHelper::parseSingleLine(line.substr(5),Options::InputSyntax::SMTLIB2);
        prb = UIHelper::getInputProblem();
      } catch (ParsingRelatedException& exception) {
        explainException(exception);
      }
    } else if (line.rfind("list",0) == 0) {
      UIHelper::listLoadedPieces(cout);
    } else if (line.rfind("pop",0) == 0) {
      Stack<std::string> pieces;
      StringUtils::splitStr(line.c_str(),' ',pieces);
      StringUtils::dropEmpty(pieces);
      int numPops = 1;
      if (pieces.size() > 1) {
        Int::stringToInt(pieces[1],numPops);
      }
      UIHelper::popLoadedPiece(numPops);
      prb = UIHelper::getInputProblem();
    } else {
      cout << "Unreconginzed command! Try 'run [options] [filename_to_load]', 'load <filenames>', 'tptp <one_line_input_in_tptp>',\n"
              "'smt2 <one_line_input_in_smt2>' 'pop [how_many_levels] (one is default)', 'list', or 'exit'." << endl;
    }
  }
}

/**
 * The main function.
 * @since 03/12/2003 many changes related to logging
 *        and exception handling.
 * @since 10/09/2004, Manchester changed to use knowledge bases
 */
int main(int argc, char* argv[])
{
  System::setSignalHandlers();

  try {
    Options& opts = *env.options;

    // read the command line and interpret it
    Shell::CommandLine cl(argc, argv);
    cl.interpret(opts);

#if VDEBUG
    std::cerr << "% WARNING: debug build, do not use in anger\n";
#endif

    if(opts.encodeStrategy()){
      cout << opts.generateEncodedOptions() << "\n";
    }

#if VTIME_PROFILING
    TimeTrace::instance().setEnabled(opts.timeStatistics());
#endif

    // If any of these options are set then we just need to output and exit
    if (opts.showHelp() || opts.showOptions() || opts.showExperimentalOptions() ||
       !opts.explainOption().empty() || opts.printAllTheoryAxioms()) {
      opts.output(std::cout);
      exit(0);
    }

    Lib::setMemoryLimit(env.options->memoryLimit() * 1048576ul);

    if (opts.interactive()) {
      interactiveMetamode();
    } else {
      // can only happen after reading options as it relies on `env.options`
      // start our timer, so that we also limit parsing
#if VAMPIRE_PERF_EXISTS
      // (with parsing_does_not_count, the instruction limit starts after parsing, see below)
      Timer::reinitialise(true, !env.options->parsingDoesNotCount());
#else
      Timer::reinitialise();
#endif

      if (opts.inputFile().empty()) {
        UIHelper::parseStandardInput(opts.inputSyntax());
      } else {
        UIHelper::parseFile(opts.inputFile(),opts.inputSyntax(),
                            opts.mode() != Options::Mode::SPIDER && opts.mode() != Options::Mode::PROFILE);
      }

#if VAMPIRE_PERF_EXISTS
      if (env.options->parsingDoesNotCount()) {
        Timer::updateInstructionCount();
        unsigned burnedParsing = Timer::elapsedMegaInstructions();

        addCommentSignForSZS(std::cout);
        std::cout << "Instructions burned parsing: " << burnedParsing << " (million)" << endl;

        // 0 means no limit, also after parsing
        unsigned instrLimit = env.options->instructionLimit();
        if (instrLimit) {
          instrLimit += burnedParsing;
          env.options->setInstructionLimit(instrLimit);
        }
        Timer::setInstructionLimit(instrLimit);
      }
#endif

      dispatchByMode(UIHelper::getInputProblem());
    }

#if CHECK_LEAKS
    delete env.signature;
    env.signature = 0;
#endif
  }
#if VZ3
  catch (z3::exception& exception) {
    vampireReturnValue = VAMP_RESULT_STATUS_UNHANDLED_EXCEPTION;
    if (outputAllowed()) {
      cout << "Z3 exception:\n" << exception.msg() << endl;
    }
    reportSpiderFail();
  }
#endif
  catch (UserErrorException& exception) {
    vampireReturnValue = VAMP_RESULT_STATUS_UNHANDLED_EXCEPTION;
    reportSpiderFail();
    explainException(exception);
  }
catch (Parse::TPTP::ParseErrorException& exception) {
    vampireReturnValue = VAMP_RESULT_STATUS_UNHANDLED_EXCEPTION;
    reportSpiderFail();
    explainException(exception);
  }
  catch (Exception& exception) {
    vampireReturnValue = VAMP_RESULT_STATUS_UNHANDLED_EXCEPTION;
    reportSpiderFail();
    explainException(exception);
  } catch (std::bad_alloc& _) {
    vampireReturnValue = VAMP_RESULT_STATUS_UNHANDLED_EXCEPTION;
    reportSpiderFail();
    std::cout << "Insufficient system memory" << '\n';
  }

  return vampireReturnValue;
} // main