<commit_before>import stl
import traces
from pytest import raises, approx
from lenses import bind
from magnum.solvers import smt
import funcy as fn
import numpy as np

from magnum.solvers.cegis import (solve, MaxRoundsError, encode_refuted_rec,
                                  combined_solver, find_refuted_radius, 
                                  smt_radius_oracle)

def test_feasible_example2_cegis():
    from magnum.examples.feasible_example2 import feasible_example as g
    
    res = solve(g)
    assert not res.feasible
    assert len(res.counter_examples) in (1,2)
    

def test_smt_radius_oracle():
    from magnum.examples.rock_paper_scissors import rps as g

    play = {'u': traces.TimeSeries([(0, 1)])}
    counter = {'w': traces.TimeSeries([(0, 20/60)])}
    oracle = smt_radius_oracle(g=g, play=play, counter=counter)

    assert not oracle(r=9/60)
    assert oracle(r=20/60)
    assert oracle(r=1)

    play = {'u': traces.TimeSeries([(0, 0)])}
    counter = {'w': traces.TimeSeries([(0, 20/60)])}
    
    oracle = smt_radius_oracle(g=g, play=play, counter=counter)
    
    assert not oracle(r=5/60)
    assert not oracle(r=9/60)
    assert oracle(r=11/60)
    assert oracle(r=1)


def test_find_refuted_radius():
    from magnum.examples.rock_paper_scissors import rps as g
    play = {'u': traces.TimeSeries([(0, 1)])}
    counter = {'w': traces.TimeSeries([(0, 20/60)])}

    r = find_refuted_radius(g, play, counter, tol=1e-6)
    assert approx(10/60, abs=1e-5) == r

    play = {'u': traces.TimeSeries([(0, 0)])}
    counter = {'w': traces.TimeSeries([(0, 20/60)])}
    
    r = find_refuted_radius(g, play, counter, tol=1e-6)
    assert approx(10/60, abs=1e-5) == r

    play = {'u': traces.TimeSeries([(0, 20/60)])}
    counter = {'w': traces.TimeSeries([(0, 40/60)])}
    
    r = find_refuted_radius(g, play, counter, tol=1e-6)
    assert approx(10/60, abs=1e-5) == r

    play = {'u': traces.TimeSeries([(0, 40/60)])}
    counter = {'w': traces.TimeSeries([(0, 0)])}

    r = find_refuted_radius(g, play, counter, tol=1e-6)
    assert approx(10/60, abs=1e-5) == r


# TODO
def test_rps():
    from magnum.examples.rock_paper_scissors import rps as g
    
    res = solve(g, use_smt=True)
    assert not res.feasible
    assert len(res.counter_examples) == 3

    with raises(MaxRoundsError):
        solve(g, use_smt=True, max_ce=1, refuted_recs=False)

    # TODO
    res = solve(g)
    assert not res.feasible
    assert len(res.counter_examples) == 3

    res = solve(g, max_ce=1, max_rounds=10)
    assert not res.feasible


def test_rpss():
    from magnum.examples.rock_paper_scissors_spock import rps as g
    
    res = solve(g)
    assert res.feasible
    assert len(res.counter_examples) == 3
    assert approx(res.cost) == 0.5

    res = solve(g, max_ce=1, max_rounds=4)
    assert res.feasible


def test_encode_refuted_rec():
    refuted = {
        'u1': traces.TimeSeries([(0, 0), (1, 1)]),
        'u2': traces.TimeSeries([(0, 0.5)])
    }<commit_msg>tweaking tests for performance<commit_after>import stl
import traces
from pytest import raises, approx
from lenses import bind
from magnum.solvers import smt
import funcy as fn
import numpy as np

from magnum.solvers.cegis import (solve, MaxRoundsError, encode_refuted_rec,
                                  combined_solver, find_refuted_radius, 
                                  smt_radius_oracle)

def test_feasible_example2_cegis():
    from magnum.examples.feasible_example2 import feasible_example as g
    
    res = solve(g)
    assert not res.feasible
    assert len(res.counter_examples) in (1,2)
    

def test_smt_radius_oracle():
    from magnum.examples.rock_paper_scissors import rps as g

    play = {'u': traces.TimeSeries([(0, 1)])}
    counter = {'w': traces.TimeSeries([(0, 20/60)])}
    oracle = smt_radius_oracle(g=g, play=play, counter=counter)

    assert not oracle(r=9/60)
    assert oracle(r=20/60)
    assert oracle(r=1)

    play = {'u': traces.TimeSeries([(0, 0)])}
    counter = {'w': traces.TimeSeries([(0, 20/60)])}
    
    oracle = smt_radius_oracle(g=g, play=play, counter=counter)
    
    assert not oracle(r=5/60)
    assert not oracle(r=9/60)
    assert oracle(r=11/60)
    assert oracle(r=1)


def test_find_refuted_radius():
    from magnum.examples.rock_paper_scissors import rps as g
    play = {'u': traces.TimeSeries([(0, 1)])}
    counter = {'w': traces.TimeSeries([(0, 20/60)])}

    r = find_refuted_radius(g, play, counter, tol=1e-6)
    assert approx(10/60, abs=1e-5) == r

    play = {'u': traces.TimeSeries([(0, 0)])}
    counter = {'w': traces.TimeSeries([(0, 20/60)])}
    
    r = find_refuted_radius(g, play, counter, tol=1e-6)
    assert approx(10/60, abs=1e-5) == r

    play = {'u': traces.TimeSeries([(0, 20/60)])}
    counter = {'w': traces.TimeSeries([(0, 40/60)])}
    
    r = find_refuted_radius(g, play, counter, tol=1e-6)
    assert approx(10/60, abs=1e-5) == r

    play = {'u': traces.TimeSeries([(0, 40/60)])}
    counter = {'w': traces.TimeSeries([(0, 0)])}

    r = find_refuted_radius(g, play, counter, tol=1e-6)
    assert approx(10/60, abs=1e-5) == r


# TODO
def test_rps():
    from magnum.examples.rock_paper_scissors import rps as g
    
    res = solve(g, use_smt=True)
    assert not res.feasible
    assert len(res.counter_examples) == 3

    with raises(MaxRoundsError):
        solve(g, max_ce=1, refuted_recs=False)

    # TODO
    res = solve(g)
    assert not res.feasible
    assert len(res.counter_examples) == 3

    res = solve(g, max_ce=1, max_rounds=10)
    assert not res.feasible


def test_rpss():
    from magnum.examples.rock_paper_scissors_spock import rps as g
    
    res = solve(g)
    assert res.feasible
    assert len(res.counter_examples) == 3
    assert approx(res.cost) == 0.5

    res = solve(g, max_ce=2, max_rounds=7)
    assert res.feasible


def test_encode_refuted_rec():
    refuted = {
        'u1': traces.TimeSeries([(0, 0), (1, 1)]),
        'u2': traces.TimeSeries([(0, 0.5)])
    }
{'fraction_non_alphanumeric': 0.14221482098251456, 'fraction_numerical': 0.03996669442131557, 'mean_word_length': 3.122168840082361, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6691460', 'n_tokens_mistral': 2447, 'n_tokens_neox': 2207, 'n_words': 504}