klara.klara_z3.instance_collector.InstanceCollector

class documentation

class InstanceCollector: (source)

Undocumented

Method	`__init__`	Undocumented
Method	`add_cond`	Undocumented
Method	`build_constraints`	for all conditions, create tracking bool
Method	`report_statistics`	Undocumented
Method	`use_mss_z3`	Undocumented
Method	`use_z3_check`	No minimizing instances, just get instance using `solver.check()` on all conditions
Method	`wrap_conditions`	wrap all conditions set with z3.And to get a valid z3 expr
Method	`yield_instances`	Undocumented
Method	`z3_get_all_solutions`	Undocumented
Instance Variable	`all_blocks`	Undocumented
Instance Variable	`all_ledgers`	Undocumented
Instance Variable	`blk2blk_covered`	Undocumented
Instance Variable	`conditions`	Undocumented
Instance Variable	`covered_blk2ledger`	Undocumented
Instance Variable	`failed_conditions`	Undocumented
Instance Variable	`passed_conditions`	Undocumented
Instance Variable	`removed_block`	Undocumented
Instance Variable	`root`	Undocumented
Instance Variable	`vars_sequence`	Undocumented
Method	`_add_result`	Undocumented

def __init__(self): (source)

Undocumented

def add_cond(self, cond, result=None, after_res=None): (source)

Undocumented

def build_constraints(self, conditions=None): (source)

for all conditions, create tracking bool

def report_statistics(self, file): (source)

Undocumented

def use_mss_z3(self): (source)

Undocumented

def use_z3_check(self): (source)

No minimizing instances, just get instance using `solver.check()` on all conditions

def wrap_conditions(self): (source)

wrap all conditions set with z3.And to get a valid z3 expr

def yield_instances(self, is_multi_processes=False, processes=None, use_z3_check=False): (source)

Undocumented

def z3_get_all_solutions(self): (source)

Undocumented

all_blocks: list = (source)

Undocumented

all_ledgers = (source)

Undocumented

blk2blk_covered = (source)

Undocumented

conditions: dict = (source)

Undocumented

covered_blk2ledger = (source)

Undocumented

failed_conditions = (source)

Undocumented

passed_conditions = (source)

Undocumented

removed_block = (source)

Undocumented

Undocumented

vars_sequence: list = (source)

Undocumented

def _add_result(self, model): (source)

Undocumented