load("conjecturing.py")
load("gt.sage")

#load the database
load("objects-invariants-properties/gt_precomputed_database.sage")
db = os.environ['HOME'] +'/objects-invariants-properties/gt_precomputed_database.db'

#now get a table out of the precomptred database that can be used by the invariant-relation conjecturing program
precomputed_invs = precomputed_invariants_for_conjecture(database=db)

#check that a value *agrees* with what is in the db
verify_invariant_values([independence_number], [graphs.CycleGraph(15)], database=db)

#add independence number of c15 to database
update_invariant_database([independence_number], [graphs.CycleGraph(15)], database = db)

#now check
precomputed_invs = precomputed_invariants_for_conjecture(database=db)
invs, object_key, invariant_key = precomputed_invs
invs[object_key(starfish)][invariant_key(Graph.lovasz_theta)]

#load a function that has special cached values
#only need to run this when new special hard values have been computed
load("objects-invariants-properties/gt_precomputed_values.sage")
store_values(database=db)
store_values(database=db, verbose=True)

#example of adding distinct degrees computation for all graph objects
update_invariant_database([distinct_degrees], graph_objects, timeout=60, database=db, verbose=False)

list_missing_invariants(efficiently_computable_invariants, graph_objects, database=db)

#update all efficiently computed invariants for all graph objects to the database
update_invariant_database(efficiently_computable_invariants, graph_objects, timeout=60, database=db, verbose=False)

#add computation of all invariants in *invariants* list for the Wagner graph
update_invariant_database(invariants, [graphs.WagnerGraph()], timeout=60, database=db, verbose=False)

#example of a conjecture run using the database of precomputed graph invariants
load("conjecturing.py")
load("gt.sage")

objects = graph_objects

invariants = efficiently_computable_invariants + [independence_number]

conjs = conjecture(objects, invariants, invariants.index(independence_number), precomputed = precomputed_invs)
for c in conjs:
    print c

##example of a conjecture run using the database of precomputed graph invariants
#and best use of *theory*
#this couldn't beat lovasz theta and annihilation number before timing out
#we need more invariants!!!

load("conjecturing.py")
load("gt.sage")

annihilation_thm = lambda g: annihilation_number(g)
fractional_thm = lambda g: fractional_alpha(g)
kwok_thm = lambda g: order(g) - (size(g)/max_degree(g))
cvetkovic_thm = lambda g: cvetkovic(g)
trivial_thm = lambda g: order(g)
min_degree_thm = lambda g: order(g) - min_degree(g)
hansen_thm = lambda g: floor(1/2 + sqrt(1/4 + order(g)**2 - order(g) - 2*size(g)))
borg_thm = lambda g: order(g) - ceil((order(g) - 1) / max_degree(g))
matching_number_thm = lambda g: order(g) - matching_number(g)
lovasz_theta_thm = lambda g: g.lovasz_theta()

objects = graph_objects

invariants = efficiently_computable_invariants + [independence_number]

theorems = [annihilation_thm, lovasz_theta_thm]
min_theorem = lambda g: floor(min(f(g) for f in theorems))

conjs = conjecture(objects, invariants, invariants.index(independence_number), theory = [min_theorem], precomputed = precomputed_invs)
for c in conjs:
    print c

#2nd try with longer timeout


load("conjecturing.py")
load("gt.sage")

annihilation_thm = lambda g: annihilation_number(g)
fractional_thm = lambda g: fractional_alpha(g)
kwok_thm = lambda g: order(g) - (size(g)/max_degree(g))
cvetkovic_thm = lambda g: cvetkovic(g)
trivial_thm = lambda g: order(g)
min_degree_thm = lambda g: order(g) - min_degree(g)
hansen_thm = lambda g: floor(1/2 + sqrt(1/4 + order(g)**2 - order(g) - 2*size(g)))
borg_thm = lambda g: order(g) - ceil((order(g) - 1) / max_degree(g))
matching_number_thm = lambda g: order(g) - matching_number(g)
lovasz_theta_thm = lambda g: g.lovasz_theta()

objects = graph_objects

invariants = efficiently_computable_invariants + [independence_number]

theorems = [annihilation_thm, lovasz_theta_thm]
min_theorem = lambda g: floor(min(f(g) for f in theorems))

conjs = conjecture(objects, invariants, invariants.index(independence_number), theory = [min_theorem], precomputed = precomputed_invs, time = 1000)
for c in conjs:
    print c

#NOTE: why aren't there any conjectures
#(1) no function of the invaqriants could beat the theory within the timeout itme
#in case, we'd need MORE INVARIANTS!
#(2) there's still a corrupt value in the database
#in this case the program can't make a true conjecture because it has a value for an upper bound for independence that's less than independence

starfish.show()

#example of a lower bound for alpha conjecture run using the database of precomputed graph invariants
#with no theory

load("conjecturing.py")
load("gt.sage")

objects = graph_objects

invariants = efficiently_computable_invariants + [independence_number]

conjs = conjecture(objects, invariants, invariants.index(independence_number), upperBound = False, precomputed = precomputed_invs)
for c in conjs:
    print c

#example of a lower bound for alpha conjecture run using the database of precomputed graph invariants
#with  theory

load("conjecturing.py")
load("gt.sage")

radius_thm = lambda g: g.radius()
max_even_thm = lambda g: max_even_minus_even_horizontal(g)
residue_thm = lambda g: residue(g)

theorems = [radius_thm, max_even_thm, residue_thm]
max_theorem = lambda g: ceil(max(f(g) for f in theorems))

objects = graph_objects

invariants = efficiently_computable_invariants + [independence_number]

conjs = conjecture(objects, invariants, invariants.index(independence_number), upperBound = False, theory = [max_theorem], precomputed = precomputed_invs)
for c in conjs:
    print c

precomputed_invs = precomputed_invariants_for_conjecture(database=db)
invs, object_key, invariant_key = precomputed_invs
invs[object_key(starfish)][invariant_key(Graph.lovasz_theta)]

for g in graph_objects:
    print g.name(), invs[object_key(g)][invariant_key(independence_number)], invs[object_key(g)][invariant_key(Graph.lovasz_theta)]

#NOTE: the database had a wrongly computed value of lovasz theta for the sylvester graph
#added the correct value in gt_precompted_calues.sage store_values function
#add the correct value to the database

#load a function that has special cached values
#only need to run this when new special hard values have been computed
load("objects-invariants-properties/gt_precomputed_values.sage")
store_values(database=db)

#check
precomputed_invs = precomputed_invariants_for_conjecture(database=db)
invs, object_key, invariant_key = precomputed_invs
invs[object_key(sylvester)][invariant_key(Graph.lovasz_theta)]

#STILL a pblem we see
#need to reload the database?

load("objects-invariants-properties/gt_precomputed_database.sage")
db = os.environ['HOME'] +'/objects-invariants-properties/gt_precomputed_database.db'
precomputed_invs = precomputed_invariants_for_conjecture(database=db)
invs, object_key, invariant_key = precomputed_invs
invs[object_key(sylvester)][invariant_key(Graph.lovasz_theta)]

#aha! set the overwrite flag to True
store_values(overwrite = True, database=db)

#check
precomputed_invs = precomputed_invariants_for_conjecture(database=db)
invs, object_key, invariant_key = precomputed_invs
invs[object_key(sylvester)][invariant_key(Graph.lovasz_theta)]

load("objects-invariants-properties/gt_precomputed_database.sage")
db = os.environ['HOME'] +'/objects-invariants-properties/gt_precomputed_database.db'
precomputed_invs = precomputed_invariants_for_conjecture(database=db)
invs, object_key, invariant_key = precomputed_invs
invs[object_key(sylvester)][invariant_key(Graph.lovasz_theta)]

#now have a database with corrected values of lovasz theta
#will we get some upper bound conjectures?!?!?!?!??!?!?!?!??!?!

load("conjecturing.py")
load("gt.sage")

annihilation_thm = lambda g: annihilation_number(g)
fractional_thm = lambda g: fractional_alpha(g)
kwok_thm = lambda g: order(g) - (size(g)/max_degree(g))
cvetkovic_thm = lambda g: cvetkovic(g)
trivial_thm = lambda g: order(g)
min_degree_thm = lambda g: order(g) - min_degree(g)
hansen_thm = lambda g: floor(1/2 + sqrt(1/4 + order(g)**2 - order(g) - 2*size(g)))
borg_thm = lambda g: order(g) - ceil((order(g) - 1) / max_degree(g))
matching_number_thm = lambda g: order(g) - matching_number(g)
lovasz_theta_thm = lambda g: g.lovasz_theta()

objects = graph_objects

invariants = efficiently_computable_invariants + [independence_number]

theorems = [annihilation_thm, lovasz_theta_thm]
min_theorem = lambda g: floor(min(f(g) for f in theorems))

conjs = conjecture(objects, invariants, invariants.index(independence_number), theory = [min_theorem], precomputed = precomputed_invs, time = 1000)
for c in conjs:
    print c

#why weren't there any conjectures???
for g in graph_objects:
    if min_theorem(g) != independence_number(g):
        print g.name(), independence_number(g), min_theorem(g)

#is min_theorem pulling values from the database when using the conjecturing program???

#now have a database with corrected values of lovasz theta
#will we get some upper bound conjectures?!?!?!?!??!?!?!?!??!?!

load("conjecturing.py")
load("gt.sage")

annihilation_thm = lambda g: annihilation_number(g)
lovasz_theta_thm = lambda g: g.lovasz_theta()

objects = [sylvester]

invariants = [Graph.lovasz_theta, independence_number]

theorems = [annihilation_thm]
min_theorem = lambda g: floor(min(f(g) for f in theorems))

conjs = conjecture(objects, invariants, invariants.index(independence_number), theory = [min_theorem], precomputed = precomputed_invs, verbose = True, debug = True)
for c in conjs:
    print c

independence_number(sylvester)
annihilation_number(sylvester)

efficiently_computable_invariants[:1]

#trying conjecturing only with graphs where alpha < floor(lovasz_theta)
load("conjecturing.py")
load("gt.sage")

annihilation_thm = lambda g: annihilation_number(g)
lovasz_theta_thm = lambda g: g.lovasz_theta()

#objects = [sylvester, graphs.ClebschGraph(), c24, c60, starfish]
objects = [starfish]

invariants = [independence_number] + efficiently_computable_invariants[:1]

theorems = [Graph.lovasz_theta]

def get_value(invariant, o):
    precomputed_value = None
    o_key = precomputed_invs[1](o)
    i_key = precomputed_invs[2](invariant)
    if precomputed_invs:
        if o_key in precomputed_invs[0]:
            if i_key in precomputed_invs[0][o_key]:
                precomputed_value = precomputed_invs[0][o_key][i_key]
    if precomputed_value is None:
        return invariant(o)
    else:
        return precomputed_value

min_theorem = lambda g: floor(min(get_value(f,g) for f in theorems))

get_value(lovasz_theta_thm, starfish)

conjs = conjecture(objects, invariants, invariants.index(independence_number), theory = [min_theorem], precomputed = precomputed_invs, verbose = True, debug = True)
for c in conjs:
    print c

load("objects-invariants-properties/gt_precomputed_database.sage")
db = os.environ['HOME'] +'/objects-invariants-properties/gt_precomputed_database.db'
precomputed_invs = precomputed_invariants_for_conjecture(database=db)
invs, object_key, invariant_key = precomputed_invs
invs[object_key(starfish)][invariant_key(Graph.lovasz_theta)]

load("objects-invariants-properties/gt_precomputed_database.sage")
db = os.environ['HOME'] +'/objects-invariants-properties/gt_precomputed_database.db'
precomputed_invs = precomputed_invariants_for_conjecture(database=db)
invs, object_key, invariant_key = precomputed_invs
invs[object_key(sylvester)][invariant_key(Graph.lovasz_theta)]

for g in [sylvester, graphs.ClebschGraph(), c24, c60, starfish]:
    print g.name(), independence_number(g), invs[object_key(g)][invariant_key(Graph.lovasz_theta)]

lovasz_theta_thm(starfish)

graph_objects[77].name()

load("conjecturing.py")
load("gt.sage")

annihilation_thm = lambda g: annihilation_number(g)
fractional_thm = lambda g: fractional_alpha(g)
kwok_thm = lambda g: order(g) - (size(g)/max_degree(g))
cvetkovic_thm = lambda g: cvetkovic(g)
trivial_thm = lambda g: order(g)
min_degree_thm = lambda g: order(g) - min_degree(g)
hansen_thm = lambda g: floor(1/2 + sqrt(1/4 + order(g)**2 - order(g) - 2*size(g)))
borg_thm = lambda g: order(g) - ceil((order(g) - 1) / max_degree(g))
matching_number_thm = lambda g: order(g) - matching_number(g)
lovasz_theta_thm = lambda g: g.lovasz_theta()

objects = [starfish]

invariants = [independence_number] + efficiently_computable_invariants[:1]

theorems = [Graph.lovasz_theta]
#use get_value so that conjecture program uses precomputed value in theory calculation instead of recomputing - maybe incoorectly
min_theorem = lambda g: floor(min(get_value(f, g) for f in theorems))
#for this to work each "theorem" that has a potential numerical error needs to be precomputed and included in the db

conjs = conjecture(objects, invariants, invariants.index(independence_number), theory = [min_theorem], precomputed = precomputed_invs, verbose = true, debug = true, time = 100)
for c in conjs:
    print c

get_value(lovasz_theta_thm, starfish)

get_value(Graph.lovasz_theta, starfish)

load("conjecturing.py")
load("gt.sage")

annihilation_thm = lambda g: annihilation_number(g)
fractional_thm = lambda g: fractional_alpha(g)
kwok_thm = lambda g: order(g) - (size(g)/max_degree(g))
cvetkovic_thm = lambda g: cvetkovic(g)
trivial_thm = lambda g: order(g)
min_degree_thm = lambda g: order(g) - min_degree(g)
hansen_thm = lambda g: floor(1/2 + sqrt(1/4 + order(g)**2 - order(g) - 2*size(g)))
borg_thm = lambda g: order(g) - ceil((order(g) - 1) / max_degree(g))
matching_number_thm = lambda g: order(g) - matching_number(g)
lovasz_theta_thm = lambda g: g.lovasz_theta()

objects = graph_objects[:100]

invariants = [independence_number] + efficiently_computable_invariants

theorems = [annihilation_number]
#use get_value so that conjecture program uses precomputed value in theory calculation instead of recomputing (maybe incorrectly)
min_theorem = lambda g: floor(min(get_value(f, g) for f in theorems))
#for this to work each "theorem" that has a potential numerical error needs to be precomputed and included in the db

conjs = conjecture(objects, invariants, invariants.index(independence_number), theory = [min_theorem], precomputed = precomputed_invs, debug = true, time = 10)
for c in conjs:
    print c

objects = graph_objects[70:]

theorems = [Graph.lovasz_theta]
#use get_value so that conjecture program uses precomputed value in theory calculation instead of recomputing (maybe incorrectly)
min_theorem = lambda g: floor(min(get_value(f, g) for f in theorems))
#for this to work each "theorem" that has a potential numerical error needs to be precomputed and included in the db

for g in objects:
    print g.name(), independence_number(g), min_theorem(g)

load("conjecturing.py")
load("gt.sage")

annihilation_thm = lambda g: annihilation_number(g)
fractional_thm = lambda g: fractional_alpha(g)
kwok_thm = lambda g: order(g) - (size(g)/max_degree(g))
cvetkovic_thm = lambda g: cvetkovic(g)
trivial_thm = lambda g: order(g)
min_degree_thm = lambda g: order(g) - min_degree(g)
hansen_thm = lambda g: floor(1/2 + sqrt(1/4 + order(g)**2 - order(g) - 2*size(g)))
borg_thm = lambda g: order(g) - ceil((order(g) - 1) / max_degree(g))
matching_number_thm = lambda g: order(g) - matching_number(g)
lovasz_theta_thm = lambda g: g.lovasz_theta()

objects = graph_objects[:]

invariants = [independence_number] + efficiently_computable_invariants

theorems = [Graph.lovasz_theta]
#use get_value so that conjecture program uses precomputed value in theory calculation instead of recomputing (maybe incorrectly)
min_theorem = lambda g: floor(min(get_value(f, g) for f in theorems))
#for this to work each "theorem" that has a potential numerical error needs to be precomputed and included in the db

conjs = conjecture(objects, invariants, invariants.index(independence_number), theory = [min_theorem], precomputed = precomputed_invs, debug = false, time = 10000)
for c in conjs:
    print c