# Reproducing results of Efficient Implementation of Large-Scale Watchlists

All runs have been performed with the E version "devRuhdorfer002" on the data provided here.
You can download a distribution of this version of E on this webpage.
Additionally, you will also find all problem files here and the watchlist that we used.

To run E against one of the problems use:

```
./PROVER/eprover --definitional-cnf=24 --split-aggressive --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(1*ConjectureTermPrefixWeight(PreferProcessed,1,3,0.1,5,0,0.1,1,4),1*ConjectureTermPrefixWeight(PreferWatchlist,1,3,0.5,100,0,0.2,0.2,4),1*Refinedweight(PreferWatchlist,4,300,4,4,0.7),1*RelevanceLevelWeight2(PreferWatchlist,0,1,2,1,1,1,200,200,2.5,9999.9,9999.9),1*StaggeredWeight(PreferWatchlist,1),1*SymbolTypeweight(PreferWatchlist,18,7,-2,5,9999.9,2,1.5),2*Clauseweight(PreferWatchlist,20,9999,4),2*ConjectureSymbolWeight(PreferWatchlist,9999,20,50,-1,50,3,3,0.5),2*StaggeredWeight(PreferWatchlist,2))' --free-numbers --watchlist=path/to/watchlist.mizar40 /path/to/problem_file.p
```

The prover was instructed to stop after 720 seconds or 10.000 generated clauses.
We did this by using an [adapted version](https://github.com/ConstantinRuhdorfer/pyprove) of the pyprove python 3 library for orchestrating the runs.
This library expects a directory `watchlists` and `strats` where it looks for the input for E.
A project using this library might therefore look like this:

```
.
+-- evaluation.py         The evaluations script (see below)
+-- watchlists/           Watchlist you want to test
|   +-- watchlist.mizar40 The watchlist we have used
+-- straty/               Testing commands (see strats_softwatch)
|   +-- mzr02WL10_000FP2L
|   +-- mzr02WL10_000FP4L
|   +-- mzr02WL10_000FP6L
|   +-- ...
```

We have used a script similar to this for actually performing the runs:

```python
import pandas as pd
import numpy as np

import datetime
from pyprove import *
from pprint import pprint

# The same as the names of your command files in ./strats/
# (i.e. ./strats/mzr02WL10_000FP2L, ./strats/mzr02WL10_000FP4L etc.)
PIDS = ["mzr02WL10_000FP2L", "mzr02WL10_000FP4L", "mzr02WL10_000FP6L",
        "mzr02WL10_000FP8L", "mzr02WL10_000FP10L", "mzr02WL10_000FP4LL",
        "mzr02WL10_000FP6LL", "mzr02WL10_000FP8LL", "mzr02WL10_000FP10LL"]

experiment = {
    "bid": "mizar40-tenth",
    "pids": PIDS,
    "limit": "G10000-T720",
    "cores": 64, # Number of cores
    "eargs": "-s --free-numbers --resources-info --print-statistics"
}

def evaluate(fig_name, experiment, ebinary="eprover"):

    experiment["ebinary"] = ebinary

    log.start("Evaluating models", experiment)

    experiment["results"] = expres.benchmarks.eval(**experiment)

    results = experiment["results"]

    pprint(results)

    runtimes = np.empty(len(results))
    processed_clauses = np.empty(len(results))
    generated_clauses = np.empty(len(results))
    status = np.empty(len(results), dtype=object)
    strategy = np.empty(len(results), dtype=object)
    names = np.empty(len(results), dtype=object)
    limitation = np.empty(len(results), dtype=object)
    c_p_c = np.empty(len(results), dtype=object)
    c_p_p_o_c = np.empty(len(results), dtype=object)
    c_p_p_n_o_c = np.empty(len(results), dtype=object)
    c_p_n_uc = np.empty(len(results), dtype=object)
    c_p_non_uc = np.empty(len(results), dtype=object)

    wl_n_u_c = np.empty(len(results), dtype=object)
    wl_u_c = np.empty(len(results), dtype=object)
    wl_checks = np.empty(len(results), dtype=object)
    wl_checks_u = np.empty(len(results), dtype=object)
    process_c_loops = np.empty(len(results), dtype=object)

    i = 0
    for result in results:
        if "RUNTIME" in results[result]:
            runtimes[i] = results[result]["RUNTIME"]
        else:
            runtimes[i] = 720
        if "PROCESSED" in results[result]:
            processed_clauses[i] = results[result]["PROCESSED"]
        else:
            processed_clauses[i] = np.nan
        if "GENERATED" in results[result]:
            generated_clauses[i] = results[result]["GENERATED"]
        else:
            generated_clauses[i] = np.nan
        if "CURR_PROCESSED_CLAUSES" in results[result]:
            c_p_c[i] = results[result]["CURR_PROCESSED_CLAUSES"]
        else:
            c_p_c[i] = np.nan
        if "CURR_PROCESSED_POS_OR_UC" in results[result]:
            c_p_p_o_c[i] = results[result]["CURR_PROCESSED_POS_OR_UC"]
        else:
            c_p_p_o_c[i] = np.nan
        if "CURR_PROCESSED_POS_NOT_OR_UC" in results[result]:
            c_p_p_n_o_c[i] = results[result]["CURR_PROCESSED_POS_NOT_OR_UC"]
        else:
            c_p_p_n_o_c[i] = np.nan
        if "CURR_PROCESSED_NEG_UC" in results[result]:
            c_p_n_uc[i] = results[result]["CURR_PROCESSED_NEG_UC"]
        else:
            c_p_n_uc[i] = np.nan
        if "CURR_PROCESSED_NON_UC" in results[result]:
            c_p_non_uc[i] = results[result]["CURR_PROCESSED_NON_UC"]
        else:
            c_p_non_uc[i] = np.nan
        if "WATCHLIST_NON_UNIT_CLAUSES" in results[result]:
            wl_n_u_c[i] = results[result]["WATCHLIST_NON_UNIT_CLAUSES"]
        else:
            wl_n_u_c[i] = np.nan
        if "WATCHLIST_UNIT_CLAUSES" in results[result]:
            wl_u_c[i] = results[result]["WATCHLIST_UNIT_CLAUSES"]
        else:
            wl_u_c[i] = np.nan
        if "WATCHLIST_CHECKS" in results[result]:
            wl_checks[i] = results[result]["WATCHLIST_CHECKS"]
        else:
            wl_checks[i] = np.nan
        if "WATCHLIST_CHECKS_Unit" in results[result]:
            wl_checks_u[i] = results[result]["WATCHLIST_CHECKS_Unit"]
        else:
            wl_checks_u[i] = np.nan
        if "PROCESS_CLAUSE_LOOPS" in results[result]:
            process_c_loops[i] = results[result]["PROCESS_CLAUSE_LOOPS"]
        else:
            process_c_loops[i] = np.nan
        status[i] = results[result]["STATUS"]
        strategy[i] = result[1]
        names[i] = result[2]
        limitation[i] = result[3]
        i += 1

    presentation_data = {
        "runtimes": runtimes,
        "processed_clauses": processed_clauses,
        "generated_clauses": generated_clauses,
        "status": status,
        "strategy": strategy,
        "names": names,
        "limitation": limitation,
        "CURR_PROCESSED_CLAUSES": c_p_c,
        "CURR_PROCESSED_POS_OR_UC": c_p_p_o_c,
        "CURR_PROCESSED_POS_NOT_OR_UC": c_p_p_n_o_c,
        "CURR_PROCESSED_NEG_UC": c_p_n_uc,
        "CURR_PROCESSED_NON_UC": c_p_non_uc,
        "WATCHLIST_NON_UNIT_CLAUSES": wl_n_u_c,
        "WATCHLIST_UNIT_CLAUSES": wl_u_c,
        "WATCHLIST_CHECKS": wl_checks,
        "WATCHLIST_CHECKS_Unit": wl_checks_u,
        "PROCESS_CLAUSE_LOOPS": process_c_loops
    }

    presentation_df = pd.DataFrame(data=presentation_data)
    presentation_df.to_csv(
        experiment["ebinary"] + "__" + experiment["bid"] +
        str(datetime.datetime.now().isoformat()),
        sep=';',
        encoding='utf-8',
        index=False)

evaluate("MyExperiment", experiment,
         "your/path/to/eprover-devRuhdorfer002")

```