Skip to content
Permalink
Browse files

Support groups normally distributed assumption.

  • Loading branch information...
emjun committed Jul 10, 2019
1 parent 60c8bd3 commit e2151f6e146d433c5041f2f7deae6a5ed54f4727
Showing with 552 additions and 541 deletions.
  1. +10 −9 tea/api.py
  2. +30 −24 tea/z3_solver/solver.py
  3. +512 −508 tests/integration_tests/test_integration.py
@@ -116,16 +116,17 @@ def assume(user_assumptions: Dict[str, str], mode=None):
assumptions = user_assumptions
assumptions[alpha_keywords[1]] = alpha

if mode:
assert (mode == 'strict' or mode == 'relaxed')
# Set MODE for dealing with assumptions
if mode and mode == 'relaxed':
MODE = mode
log(f"Running under {mode.upper()} mode.\n")
if MODE == 'strict':
log(f"This means that user assertions will be checked. Should they fail, Tea will override user assertions.\n")
else:
assert(MODE == 'relaxed')
log(f"This means that user assertions will be checked. Should they fail, Tea will issue a warning but proceed as if user's assertions were true.")

log(f"\nRunning under {MODE.upper()} mode.\n")
log(f"This means that user assertions will be checked. Should they fail, Tea will issue a warning but proceed as if user's assertions were true.")
else:
assert (mode == None or mode == 'strict')
MODE = 'strict'
log(f"\nRunning under {MODE.upper()} mode.\n")
log(f"This means that user assertions will be checked. Should they fail, Tea will override user assertions.\n")

def hypothesize(vars: list, prediction: list=None):
global dataset_path, vars_objs, study_design, dataset_obj, dataset_id
global assumptions, all_results
@@ -898,7 +898,10 @@ def verify_prop(dataset: Dataset, combined_data: CombinedData, prop:AppliedPrope

if (len(prop.vars) == len(combined_data.vars)):
kwargs = {'dataset': dataset, 'var_data': combined_data, 'alpha': alpha}
prop_val = __property_to_function__[prop.__z3__](**kwargs)
if __property_to_function__ == {}:
prop_val = prop.property.function(**kwargs)
else:
prop_val = __property_to_function__[prop.__z3__](**kwargs)
else:
assert (len(prop.vars) < len(combined_data.vars))
var_data = []
@@ -952,16 +955,19 @@ def assume_properties(stat_var_map, assumptions: Dict[str,str], solver, dataset,

# CHECK ASSUMPTIONS HERE
val = verify_prop(dataset, combined_data, ap)
# if val:
# solver.add(ap.__z3__ == z3.BoolVal(True))
# else:
if MODE == 'strict':
log(f"Running under STRICT mode.")
log(f"User asserted property: {prop.name}, but is NOT supported by statistical checking. Tea will override user assertion.")
if val:
log(f"User asserted property: {prop.name} is supported by statistical checking. Tea agrees with the user.")
else:
log(f"User asserted property: {prop.name}, but is NOT supported by statistical checking. Tea will override user assertion.")
solver.add(ap.__z3__ == z3.BoolVal(val))
elif MODE == 'relaxed':
log(f"Running under RELAXED mode.")
log(f"User asserted property: {prop.name}, but is NOT supported by statistical checking. User assertion will be considered true.")
if val:
log(f"User asserted property: {prop.name} is supported by statistical checking. Tea agrees with the user.")
else:
log(f"User asserted property: {prop.name}, but is NOT supported by statistical checking. User assertion will be considered true.")
solver.add(ap.__z3__ == z3.BoolVal(val))
else:
raise ValueError(f"Invalid MODE: {MODE}")
@@ -971,24 +977,24 @@ def assume_properties(stat_var_map, assumptions: Dict[str,str], solver, dataset,
ap = prop(*stat_vars)
assumed_props.append(ap)

solver.add(ap.__z3__ == z3.BoolVal(True))

# # CHECK ASSUMPTIONS HERE
# val = verify_prop(dataset, combined_data, ap)
# if val:
# solver.add(ap.__z3__ == z3.BoolVal(True))
# else:
# if MODE == 'strict':
# log(f"Running under STRICT mode.")
# log(f"User asserted ({prop._name}) FAILS. Tea will override user assertion.")
# solver.add(ap.__z3__ == z3.BoolVal(False))
# elif MODE == 'relaxed':
# log(f"Running under RELAXED mode.")
# log(f"User asserted ({prop._name}) FAILS. User assertion will be considered true.")
# solver.add(ap.__z3__ == z3.BoolVal(True))
# else:
# raise ValueError(f"Invalid MODE: {MODE}")
# solver.add(ap.__z3__ == z3.BoolVal(True))
# CHECK ASSUMPTIONS HERE
val = verify_prop(dataset, combined_data, ap)
if MODE == 'strict':
log(f"Running under STRICT mode.")
if val:
log(f"User asserted property: {prop.name} is supported by statistical checking. Tea agrees with the user.")
else:
log(f"User asserted property: {prop.name}, but is NOT supported by statistical checking. Tea will override user assertion.")
solver.add(ap.__z3__ == z3.BoolVal(val))
elif MODE == 'relaxed':
log(f"Running under RELAXED mode.")
if val:
log(f"User asserted property: {prop.name} is supported by statistical checking. Tea agrees with the user.")
else:
log(f"User asserted property: {prop.name}, but is NOT supported by statistical checking. User assertion will be considered true.")
solver.add(ap.__z3__ == z3.BoolVal(val))
else:
raise ValueError(f"Invalid MODE: {MODE}")
else:
pass
# import pdb; pdb.set_trace()

0 comments on commit e2151f6

Please sign in to comment.
You can’t perform that action at this time.