pycaliper.synth package

Submodules

pycaliper.synth.alignsynthesis module

class pycaliper.synth.alignsynthesis.AlignSynthesizer(tmgr)

Bases: object

synthesize(specmodule, dc)

Return type:

SpecModule

pycaliper.synth.btorsynthesizer module

class pycaliper.synth.btorsynthesizer.BTORVerifier2TraceIncremental(gui=None)

Bases: PYCBTORInterface

can_add(hole_id)

Check if the hole can be added

Return type:

bool

disable_hole_assm(hole_id)

Disable a hole by removing its assumptions and assertions

enable_hole_assm(hole_id)

Enable a hole by adding its assumptions and assertions

unroll(specmodule, des, dc)

Synthesizer for inductive two-safety property

Perform hole-synthesis for a single module w.r.t. the following property:

input_eq && state_eq |-> ##1 output_eq && state_eq

Returns:

synthesis result

Return type:

bool

verify()

Check if the program is safe

Return type:

BTORVerifResult

pycaliper.synth.iis_strategy module

class pycaliper.synth.iis_strategy.IISStrategy

Bases: object

get_candidate_order(unexplored, **kwargs)

get_next_candidate(unexplored, **kwargs)

get_stats()

Return type:

str

class pycaliper.synth.iis_strategy.LLMStrategy

Bases: IISStrategy

get_candidate_order(unexplored, ctx, prev_attempts=[], **kwargs)

get_next_candidate(unexplored, current, ctx, **kwargs)

get_stats()

Return type:

str

class pycaliper.synth.iis_strategy.RandomStrategy

Bases: IISStrategy

get_candidate_order(unexplored, **kwargs)

get_next_candidate(unexplored, **kwargs)

get_stats()

Return type:

str

class pycaliper.synth.iis_strategy.SeqStrategy

Bases: IISStrategy

get_candidate_order(unexplored, **kwargs)

get_next_candidate(unexplored, **kwargs)

get_stats()

Return type:

str

pycaliper.synth.iis_strategy.extract_markdown(content)

Extracts the markdown from the test content

Return type:

str

pycaliper.synth.iis_strategy.get_client()

pycaliper.synth.persynthesis module

Synthesis for equality invariants using Jasper FV Interface

class pycaliper.synth.persynthesis.HoudiniSynthesizer

Bases: object

synthesize(topmod, des, dc, strategy=<pycaliper.synth.iis_strategy.SeqStrategy object>, synconfig=HoudiniSynthesizerConfig(fuelbudget=10, stepbudget=10, retries=1))

Return type:

tuple[SpecModule, HoudiniSynthesizerStats]

class pycaliper.synth.persynthesis.HoudiniSynthesizerBTOR(gui=None)

Bases: HoudiniSynthesizer

class pycaliper.synth.persynthesis.HoudiniSynthesizerConfig(fuelbudget=10, stepbudget=10, retries=1)

Bases: object

fuelbudget: int = 10

retries: int = 1

stepbudget: int = 10

class pycaliper.synth.persynthesis.HoudiniSynthesizerJG

Bases: HoudiniSynthesizer

class pycaliper.synth.persynthesis.HoudiniSynthesizerStats(solvecalls, steps, minfuel, success)

Bases: object

minfuel: int

solvecalls: int

steps: int

success: bool

class pycaliper.synth.persynthesis.PERSynthesizer(pyconfig, strategy=<pycaliper.synth.iis_strategy.SeqStrategy object>, fuelbudget=3, stepbudget=10)

Bases: object

reset_state()

safe()

synthesize(topmod, retries=1)

Return type:

SpecModule

class pycaliper.synth.persynthesis.SynthesisTree(asrts=[], assms=[], parent=None, inherits=None)

Bases: object

add_asrt(asrt)

add_child(cand)

add_secondary_assm(assm)

counter = 0

is_self_inductive()

pycaliper.synth.synthprog module

class pycaliper.synth.synthprog.LUTSynthProgram

Bases: object

add_values()

get_inv()

solve()

class pycaliper.synth.synthprog.ZDDLUTSynthProgram(ctr, out)

Bases: object

MAX_DEPTH = 10

add_entries(ctr_vals, out_vals)

get_cons()

get_inv()

solve(depth=10)

Module contents