<jupyter_start><jupyter_text>Evaluation of ITETo confirm the effectiveness of the presented lightweight approach to constructive disjunction, we compare our ITE implementation to the corresponding standard methods contained in SICStus Prolog.The benchmark is an evaluation on 28 representative expressions containing one or multiple constructive operators.We start by defining a couple of helper functions and settings, especially for allowing Latex compatible plotting.<jupyter_code>def figsize_column(scale, height_ratio=1.0):
    fig_width_pt = 252  # Get this from LaTeX using \the\columnwidth
    inches_per_pt = 1.0 / 72.27  # Convert pt to inch
    golden_mean = (np.sqrt(5.0) - 1.0) / 2.0  # Aesthetic ratio (you could change this)
    fig_width = fig_width_pt * inches_per_pt * scale  # width in inches
    fig_height = fig_width * golden_mean * height_ratio  # height in inches
    fig_size = [fig_width, fig_height]
    return fig_size


def figsize_text(scale, height_ratio=1.0):
    fig_width_pt = 516  # Get this from LaTeX using \the\textwidth
    inches_per_pt = 1.0 / 72.27  # Convert pt to inch
    golden_mean = (np.sqrt(5.0) - 1.0) / 2.0  # Aesthetic ratio (you could change this)
    fig_width = fig_width_pt * inches_per_pt * scale  # width in inches
    fig_height = fig_width * golden_mean * height_ratio  # height in inches
    fig_size = [fig_width, fig_height]
    return fig_size


pgf_with_latex = {  # setup matplotlib to use latex for output
    "pgf.texsystem": "pdflatex",  # change this if using xetex or lautex
    "text.usetex": True,  # use LaTeX to write all text
    "font.family": "serif",
    "font.serif": [],  # blank entries should cause plots to inherit fonts from the document
    "font.sans-serif": [],
    "font.monospace": [],
    "axes.labelsize": 9,
    "font.size": 9,
    "legend.fontsize": 9,
    "xtick.labelsize": 9,
    "ytick.labelsize": 9,
    "figure.figsize": figsize_column(1.0),
    "text.latex.preamble": [
        r"\usepackage[utf8x]{inputenc}",  # use utf8 fonts because your computer can handle it :)
        r"\usepackage[T1]{fontenc}",  # plots will be generated using this preamble
    ]
}

sns.set_style("white", pgf_with_latex)
sns.set_context("paper")
import matplotlib.pyplot as plt

LABELS = {
    "cd/2": "cd/2",
    "cd/3_0.9": "cd/3 (*0.9)",
    "cd/3_1": "cd/3 (*1)",
    "cd/3_1.25": "cd/3 (*1.25)",
    "cd/3_1.5": "cd/3 (*1.5)",
    "cd/3_2": "cd/3 (*2)",
    "cd/3_3": "cd/3 (*3)",
    "cd/3_4": "cd/3 (*4)",
    "cd/3_5": "cd/3 (*5)",
    "native": "clp(FD)",
    "smt": "smt",
    "nb_clauses": "Number of Clauses",
    "time": "Propagation Time"
}<jupyter_output><empty_output><jupyter_text>Experimental functionsNext, we define functions that run the actual experiment.All Prolog logic is wrapped in `benchmark.pl`, including the import of the `ite.pl` and measuring the time taken for propagation.Running the benchmark requires to have the executable `sictus` in the PATH variable. If not, adjust the path to `sicstus` in the function `run`.<jupyter_code>def run(clause, variables, res={}):
    INF = float("inf")
    call_cmd = ['sicstus', '--noinfo', '--nologo', '-l', 'benchmark.pl', '--goal']
    goal_tmpl = "pre(T0, S0),{clause},post({variables},T0,S0),halt."
    goal = goal_tmpl.format(clause=clause, variables=variables)
    out = subprocess.check_output(call_cmd + [goal], universal_newlines=True)
    
    for l in out.splitlines():
        k, v = l.split(":")
        try:        
            if v == 'sup':
                v1 = INF
            elif v == 'inf':
                v1 = -INF
            else:
                v1 = int(v)
                        
            if k == 'domain' and k in res:
                res[k] += v1
            else:
                res[k] = v1
        except ValueError:
            res[k] = v
        
    return res

def run_comparison(cd2_clause, cd3_clause, native_clause=None, properties={}, init="", variables=None):
    if native_clause is None:
        native_clause = transform(cd2_clause)
    
    if variables is None:
        variables = extract_vars(cd2_clause)
    
    cn_count = cd3_clause.count("cn")
    cd_count = cd3_clause.count("cd")
    disj_ops_count = cn_count + cd_count
    
    results = []
    for k in [0.9,1,1.25,1.5,2,3,4,5]:
        r = run(init + cd3_clause.format(k=int(k*disj_ops_count)), variables, {"type": "cd/3_{}".format(k), **properties})
        results.append(r)
    
    r_cd2 = run(init + cd2_clause, variables, {"type": "cd/2", **properties})
    r_native = run(init + native_clause, variables, {"type": "native", **properties})      
    r_smt = run("{}smt({})".format(init, native_clause.replace(",", "#/\\")), variables, {"type": "smt", **properties})
    results.extend([r_cd2, r_native, r_smt])
    return results

def transform(ite_clause):
    return ite_clause.replace("cn", "#\\").replace(" cd ", " #\/ ")

def extract_vars(clause):
    return "[" + ",".join(set((c for c in clause if c.isupper()))) + "]"<jupyter_output><empty_output><jupyter_text>Benchmark ExpressionsIn the cells below, the actual benchmark expressions are defined. Most of these expressions are also found in `test_ite.pl` in the main directory of this repository.  Examples from cn/1 (constructive negation)<jupyter_code>results_cn1 = []
cd2_formulation = "cn(X #= 0 cd X #= 4 cd X #= 1 cd X #= 7)"
cd3_formulation = "init_env(ENV, {k}), cn(cd(X #= 0, X #= 4, ENV) #\/ cd(X #= 1, X #= 7, ENV), ENV),end_env(ENV)"
init = "X in 0..10,"
ex1 = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "example1"}, init=init)
results_cn1.extend(ex1)

cd2_formulation = "cn(X in 1..10)"
cd3_formulation = "init_env(ENV, {k}),cn(X in 1..10, ENV),end_env(ENV)"
init = "X in 4..15, "
ex = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "cn1_example1"}, init=init)
results_cn1.extend(ex)

cd2_formulation = "cn(X #>= Y)"
cd3_formulation = "init_env(ENV, {k}),cn(X #>= Y, ENV),end_env(ENV)"
init = "X in 4..15, Y in 0..10, "
ex = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "cn1_example2"}, init=init)
results_cn1.extend(ex)

cd2_formulation = "cn(cn(X #>= Y))"
cd3_formulation = "init_env(ENV, {k}), cn(cn(X #>= Y, ENV), ENV),end_env(ENV)"
init = "X in 4..15, Y in 0..10, "
ex = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "cn1_example3"}, init=init)
results_cn1.extend(ex)

cd2_formulation = "cn(X #> Y-3 #/\ X #> Y+1)"
cd3_formulation = "init_env(ENV, {k}), cn(X #> Y-3 #/\ X #> Y+1, ENV), end_env(ENV)"
init = "X in 4..15, Y in 0..10, "
ex = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "cn1_example4"}, init=init)
results_cn1.extend(ex)

cd2_formulation = "cn((X #= 0) cd (Y #= 4) cd (X #= 9))"
cd3_formulation = "init_env(ENV, {k}), cn(cd(cd(X #= 0, Y #= 4, ENV), X #= 9, ENV), ENV),end_env(ENV)"
init = "X in 0..10,Y in 0..12,"
ex = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "cn1_example5"}, init=init)
results_cn1.extend(ex)

cd2_formulation = "cn((X #= 0) cd (Y #= 4) cd (X #= 9)), cn((Y #= 9) cd (Y #= 6) cd (Y #= 7))"
cd3_formulation = "init_env(ENV, {k}), cn(cd(cd(X #= 0, Y #= 4, ENV), X #= 9, ENV), ENV), cn(cd(cd(Y #= 9, Y #= 6, ENV), Y #= 7, ENV), ENV), end_env(ENV)"
init = "X in 0..10, Y in 0..10,"
ex = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "cn1_example6"}, init=init)
results_cn1.extend(ex)

cd2_formulation = "cn((X #= 0 cd X #= 4) #\/ (X #= 1 cd X #= 7))"
cd3_formulation = "init_env(ENV, {k}), cn(cd(X #= 0, X #= 4, ENV) #\/ cd(X #= 1, X #= 7, ENV), ENV), end_env(ENV)"
init = "X in 0..10, "
ex = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "cn1_example7"}, init=init)
results_cn1.extend(ex)

cd2_formulation = "cn(X in(2..3)\/(5..6)\/(8..10))"
cd3_formulation = "init_env(ENV, {k}), cn(X in(2..3)\/(5..6)\/(8..10), ENV),end_env(ENV)"
init = "X in 2..10,"
ex = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "cn1_example8"}, init=init)
results_cn1.extend(ex)

cd2_formulation = "cn(X in(2..3)\/(5..6)\/(8..10)), cn(X #>15), cn(X #< 0)"
cd3_formulation = "init_env(ENV, {k}), cn(X in(2..3)\/(5..6)\/(8..10), ENV),cn(X #>15, ENV), cn(X #< 0, ENV), end_env(ENV)"
ex = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "cn1_example9"})
results_cn1.extend(ex)<jupyter_output><empty_output><jupyter_text>Examples from cd/2 (constructive disjunction)<jupyter_code>results_cd2 = []
cd2_formulation = "cn(X #= 0 cd X #= 4 cd X #= 1 cd X #= 7)"
cd3_formulation = "init_env(ENV, {k}), cn(cd(X #= 0, X #= 4, ENV) #\/ cd(X #= 1, X #= 7, ENV), ENV),end_env(ENV)"
init = "X in 0..10,"
ex1 = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "cd2_example1"}, init=init)
results_cd2.extend(ex1)

cd2_formulation = "(X + Y #= Z) cd (X + T #= Z)"
cd3_formulation = "init_env(ENV, {k}),cd(X + Y #= Z, X + T #= Z, ENV),end_env(ENV)"
init = "X in 4..5, Y in 0..1, Z in 2..9, T in 4..5, "
ex2 = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "cd2_example2"}, init=init)
results_cd2.extend(ex2)

cd2_formulation = "(X + Y #= Z) cd (X + T #= 0)"
cd3_formulation = "init_env(ENV, {k}),cd(X + Y #= Z, X + T #= 0, ENV),end_env(ENV)"
init = "X in 4..5, Y in 0..1, Z in 2..9, T in 4..5,"
ex3 = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "cd2_example3"}, init=init)
results_cd2.extend(ex3)

cd2_formulation = "(X #= 0) cd (X #= 4)"
cd3_formulation = "init_env(ENV, {k}),cd(X #= 0, X #= 4, ENV),end_env(ENV)"
ex4 = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "cd2_example4"})
results_cd2.extend(ex4)

cd2_formulation = "(X #= 0) cd (X #= 4) cd (X #= 9)"
cd3_formulation = "init_env(ENV, {k}),cd(cd(X #= 0, X #= 4, ENV), (X #= 9), ENV),end_env(ENV)"
ex5 = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "cd2_example5"})
results_cd2.extend(ex5)

cd2_formulation = "(X #= 0) cd (X #= 4) cd (X #= 9), (X #= 9) cd (X #= 4) cd (X #= 7)"
cd3_formulation = "init_env(ENV, {k}),cd(cd(X #= 0, X #= 4, ENV), (X #= 9), ENV), cd(cd(X #= 9, X #= 4, ENV), (X #= 7), ENV),end_env(ENV)"
ex6 = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "cd2_example6"})
results_cd2.extend(ex6)

cd2_formulation = "(X #= 0) cd (Y #= 4) cd (X #= 9), (X #= 9) cd (Y #= 3) cd (Y #= 7)"
cd3_formulation = "init_env(ENV, {k}),cd(cd(X #= 0, Y #= 4, ENV), (X #= 9), ENV), cd(cd(X #= 9, Y #= 3, ENV), (Y #= 7), ENV),end_env(ENV)"
init = "X in 0..9, Y in 4..7,"
ex7 = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "cd2_example7"}, init=init)
results_cd2.extend(ex7)

cd2_formulation = "(X #= 0) cd (Y #= 4) cd (X #= 9), (Y #= 9) cd (Y #= 6) cd (Y #= 7)"
cd3_formulation = "init_env(ENV, {k}),cd(cd(X #= 0, Y #= 4, ENV), (X #= 9), ENV), cd(cd(Y #= 9, Y #= 6, ENV), (Y #= 7), ENV),end_env(ENV)"
ex8 = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "cd2_example8"})
results_cd2.extend(ex8)

# Ex. "Constructive Disjunction revisited" 1996, <NAME>
cd2_formulation = "(A+7 #=< B) cd (B+7 #=< A)"
cd3_formulation = "init_env(ENV, {k}),cd(A+7 #=< B, B+7 #=< A, ENV),end_env(ENV)"
init = "A in 1..10, B in 1..10,"
ex9 = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "cd2_example9"}, init=init)
results_cd2.extend(ex9)

cd2_formulation = "(A-B #= 4) cd (B-A #= 4)"
cd3_formulation = "init_env(ENV, {k}),cd(A-B #= 4, B-A #= 4, ENV),end_env(ENV)"
init = "A in 1..5, B in 1..5,"
ex10 = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "cd2_example10"}, init=init)
results_cd2.extend(ex10)

cd2_formulation = "(X + 2 #< Y) cd (X #=< 2)"
cd3_formulation = "init_env(ENV, {k}),cd(X + 2 #< Y, X #=< 2, ENV),end_env(ENV)"
init = "X #> 3, Y in 0..9,"
ex11 = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "cd2_example11"}, init=init)
results_cd2.extend(ex11)

cd2_formulation = "(A+7 #=< B) cd (cn(B+7 #> A)), (A #> 1,B #<9) cd (A #> 2, A#<10)"
cd3_formulation = "init_env(ENV, {k}),cd(A+7 #=< B, cn(B+7 #> A, ENV), ENV), cd((A #> 1,B #<9), (A #> 2, A#<10), ENV),end_env(ENV)"
native_formulation = "(A+7 #=< B) #\/ (#\(B+7 #> A)), (A #> 1 #/\B #<9) #\/ (A #> 2 #/\ A#<10)"
init = "A in 1..10, B in 1..10,"
ex12 = run_comparison(cd2_formulation, cd3_formulation, native_formulation, properties={"name": "cd2_example12"}, init=init)
results_cd2.extend(ex12)<jupyter_output><empty_output><jupyter_text>Complex tests<jupyter_code>results_complex = []

cd2_formulation = "(X#=0 cd Y #= 4 cd X #= 9), (Y #= 9 cd Y #= 6 cd Y #= 7)"
cd3_formulation = "init_env(ENV, {k}),cd(cd(X#=0, Y #= 4, ENV), X #= 9,ENV), cd(cd(Y #= 9, Y #= 6, ENV), Y #= 7, ENV),end_env(ENV)"
cex1 = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "complex_example1"})
results_complex.extend(cex1)

cd2_formulation = "Y in 30..40 cd Y#=X cd X*2 #=Y"
cd3_formulation = "init_env(ENV, {k}),cd(cd(Y in 30..40, Y#=X, ENV), X*2 #=Y, ENV), end_env(ENV)"
init = "X in 0..10,"
cex2 = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "complex_example2"}, init=init)
results_complex.extend(cex2)

cd2_formulation = "Y in 1..100 cd Y#=X cd X #=Y"
cd3_formulation = "init_env(ENV, {k}),cd(cd(Y in 1..100, Y#=X, ENV), X #=Y, ENV),end_env(ENV)"
init = "X in 0..10,"
cex3 = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "complex_example3"}, init=init)
results_complex.extend(cex3)

cd2_formulation = "X #= 1 cd X #= 3 cd X*X #= 100"
cd3_formulation = "init_env(ENV, {k}),cd(cd(X #= 1, X #= 3, ENV), X*X #= 100, ENV),end_env(ENV)"
cex4 = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "complex_example4"})
results_complex.extend(cex4)

cd2_formulation = "(X in 0..9 #/\ Y #= X*X) cd (X in 9..90 #/\ Y #= 90 - X) cd (X in 90..100 #/\ Y - 8100 #= X*X)"
cd3_formulation = "init_env(ENV, {k}),cd(cd(X in 0..9 #/\ Y #= X*X, X in 9..90 #/\ Y #= 90 - X, ENV), X in 90..100 #/\ Y - 8100 #= X*X, ENV),end_env(ENV)"
cex5 = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "complex_example5"})
results_complex.extend(cex5)

cd2_formulation = "(X #> Y #/\ Y #= Z) cd (Y #> X #/\ X #= Z) cd (Z #> X #/\ X #=Y) cd (X #= Y #/\ Y #= Z)"
cd3_formulation = "init_env(ENV, {k}),cd(cd(X #> Y #/\ Y #= Z, Y #> X #/\ X #= Z, ENV), cd(Z #> X #/\ X #=Y, X #= Y #/\ Y #= Z, ENV), ENV),end_env(ENV)"
init = "X in 5..100, Y in 3..100, Z in -100..3,"
cex6 = run_comparison(cd2_formulation, cd3_formulation, properties={"name": "complex_example6"}, init=init)
results_complex.extend(cex6)
dfex = pd.DataFrame.from_records(results_complex + results_cd2 + results_cn1)
#dfex
dfex.pivot_table(index='name', columns=['type'], values=['time', 'domain'])
dfex = dfex[(dfex.type != 'cd/3_4') & (dfex.type != 'cd/3_5') & (dfex.type != 'cd/3_3')]  # These factors do not perform, we exclude them before plotting
df_time = dfex.pivot_table(index='name', columns=['type'], values='time')
labels = [LABELS[l] for l in df_time.columns.tolist()]
data_time = df_time.values

df_domain = dfex.pivot_table(index='name', columns=['type'], values='domain')
data_domain = df_domain.values
data_domain[data_domain == np.inf] = np.nan
data_time[np.isnan(data_domain)] = np.nan

fig = plt.figure(figsize=figsize_text(0.85, height_ratio=0.55))

num_scenarios = data_time.shape[0]
y = 100 * np.arange(0, num_scenarios + 1) / num_scenarios

from itertools import cycle
lines = ["-","--","-.",":"]
linecycler = cycle(lines)

for col in range(len(labels)):
    x = np.hstack(([0], np.sort(data_time[:, col])))
    plt.plot(x, y, label=labels[col], linestyle=next(linecycler))

plt.legend(bbox_to_anchor=(1.01, 1), loc=2, borderaxespad=0., frameon=True)
plt.xlim([0, np.nanmax(data_time)])
plt.ylim([0, 100])
plt.xlabel("Time [ms]")
plt.ylabel("Resolved Expressions [%]")
plt.grid(axis='y')
plt.tight_layout()
plt.savefig('time.pgf', dpi=500, bbox_inches='tight')
plt.show()
df_domain = dfex.pivot_table(index='name', columns=['type'], values='domain')
labels = [LABELS[l] for l in df_domain.columns.tolist()]
data_domain = df_domain.values
data_domain = data_domain / np.nanmin(data_domain, axis=1, keepdims=True)
data_domain[data_domain == np.inf] = np.nan
largest_value = np.ceil(np.nanmax(data_domain))
nanval = largest_value+1
data_domain[np.isnan(data_domain)] = nanval

data, bins, _ = plt.hist(data_domain, bins=[1, 1.01, 1.5, 2, largest_value, nanval])
data = np.array(data)
data = 100 * data / np.sum(data, axis=1, keepdims=True)
data = data.round().astype(int)
df = pd.DataFrame(data, columns=["Opt.", "+50\%", "+100\%", "$>100\%$", "No Sol."], index=labels)
df.to_latex(buf='domain.tex', escape=False)
df<jupyter_output><empty_output>
{'fraction_non_alphanumeric': 0.1968390804597701, 'fraction_numerical': 0.04525862068965517, 'mean_word_length': 4.3748391248391245, 'pattern_counts': {'":': 60, '<': 41, '<?xml version=': 0, '>': 49, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '5', 'dir': 'jupyter-structured-clean-dedup', 'id': '383483', 'license': 'MIT', 'n_tokens_mistral': 7266, 'n_tokens_neox': 6869, 'n_words': 1613, 'path': 'evaluation/SampleStatements.ipynb', 'repo_name': 'simula-vias/ite', 'size': '16711'}