diff --git a/_modules/index.html b/_modules/index.html index 9e306086e..86f988515 100644 --- a/_modules/index.html +++ b/_modules/index.html @@ -4,10 +4,10 @@ - Overview: module code — pyk 0.1.776 documentation + Overview: module code — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/coverage.html b/_modules/pyk/coverage.html index 49d76113d..3352039cf 100644 --- a/_modules/pyk/coverage.html +++ b/_modules/pyk/coverage.html @@ -4,10 +4,10 @@ - pyk.coverage — pyk 0.1.776 documentation + pyk.coverage — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/cterm/cterm.html b/_modules/pyk/cterm/cterm.html index 9b6b7634f..00a6ada59 100644 --- a/_modules/pyk/cterm/cterm.html +++ b/_modules/pyk/cterm/cterm.html @@ -4,10 +4,10 @@ - pyk.cterm.cterm — pyk 0.1.776 documentation + pyk.cterm.cterm — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/cterm/symbolic.html b/_modules/pyk/cterm/symbolic.html index dce85c10d..190e45b12 100644 --- a/_modules/pyk/cterm/symbolic.html +++ b/_modules/pyk/cterm/symbolic.html @@ -4,10 +4,10 @@ - pyk.cterm.symbolic — pyk 0.1.776 documentation + pyk.cterm.symbolic — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/dequote.html b/_modules/pyk/dequote.html index 7dca421e8..abcd5de47 100644 --- a/_modules/pyk/dequote.html +++ b/_modules/pyk/dequote.html @@ -4,10 +4,10 @@ - pyk.dequote — pyk 0.1.776 documentation + pyk.dequote — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kast/att.html b/_modules/pyk/kast/att.html index 38dbafbcc..030c931e4 100644 --- a/_modules/pyk/kast/att.html +++ b/_modules/pyk/kast/att.html @@ -4,10 +4,10 @@ - pyk.kast.att — pyk 0.1.776 documentation + pyk.kast.att — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kast/inner.html b/_modules/pyk/kast/inner.html index 5f0a0d1d0..ee3467216 100644 --- a/_modules/pyk/kast/inner.html +++ b/_modules/pyk/kast/inner.html @@ -4,10 +4,10 @@ - pyk.kast.inner — pyk 0.1.776 documentation + pyk.kast.inner — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kast/kast.html b/_modules/pyk/kast/kast.html index 8105eaf4c..932dac1a9 100644 --- a/_modules/pyk/kast/kast.html +++ b/_modules/pyk/kast/kast.html @@ -4,10 +4,10 @@ - pyk.kast.kast — pyk 0.1.776 documentation + pyk.kast.kast — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kast/manip.html b/_modules/pyk/kast/manip.html index 870da397e..ed151d28a 100644 --- a/_modules/pyk/kast/manip.html +++ b/_modules/pyk/kast/manip.html @@ -4,10 +4,10 @@ - pyk.kast.manip — pyk 0.1.776 documentation + pyk.kast.manip — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kast/markdown.html b/_modules/pyk/kast/markdown.html index 9191e5cd3..0c27f7120 100644 --- a/_modules/pyk/kast/markdown.html +++ b/_modules/pyk/kast/markdown.html @@ -4,10 +4,10 @@ - pyk.kast.markdown — pyk 0.1.776 documentation + pyk.kast.markdown — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kast/outer.html b/_modules/pyk/kast/outer.html index 3058dd6e3..6024be136 100644 --- a/_modules/pyk/kast/outer.html +++ b/_modules/pyk/kast/outer.html @@ -4,10 +4,10 @@ - pyk.kast.outer — pyk 0.1.776 documentation + pyk.kast.outer — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kast/outer_lexer.html b/_modules/pyk/kast/outer_lexer.html index 8899b37e5..2217e31c1 100644 --- a/_modules/pyk/kast/outer_lexer.html +++ b/_modules/pyk/kast/outer_lexer.html @@ -4,10 +4,10 @@ - pyk.kast.outer_lexer — pyk 0.1.776 documentation + pyk.kast.outer_lexer — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kast/outer_parser.html b/_modules/pyk/kast/outer_parser.html index 0384dd079..d5849f9bc 100644 --- a/_modules/pyk/kast/outer_parser.html +++ b/_modules/pyk/kast/outer_parser.html @@ -4,10 +4,10 @@ - pyk.kast.outer_parser — pyk 0.1.776 documentation + pyk.kast.outer_parser — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kast/outer_syntax.html b/_modules/pyk/kast/outer_syntax.html index 4f05a015a..80babab2b 100644 --- a/_modules/pyk/kast/outer_syntax.html +++ b/_modules/pyk/kast/outer_syntax.html @@ -4,10 +4,10 @@ - pyk.kast.outer_syntax — pyk 0.1.776 documentation + pyk.kast.outer_syntax — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kast/pretty.html b/_modules/pyk/kast/pretty.html index 6e931047a..265064565 100644 --- a/_modules/pyk/kast/pretty.html +++ b/_modules/pyk/kast/pretty.html @@ -4,10 +4,10 @@ - pyk.kast.pretty — pyk 0.1.776 documentation + pyk.kast.pretty — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kbuild/kbuild.html b/_modules/pyk/kbuild/kbuild.html index ed15f33b1..2ec62f51f 100644 --- a/_modules/pyk/kbuild/kbuild.html +++ b/_modules/pyk/kbuild/kbuild.html @@ -4,10 +4,10 @@ - pyk.kbuild.kbuild — pyk 0.1.776 documentation + pyk.kbuild.kbuild — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kbuild/project.html b/_modules/pyk/kbuild/project.html index 20f34aa9b..394831368 100644 --- a/_modules/pyk/kbuild/project.html +++ b/_modules/pyk/kbuild/project.html @@ -4,10 +4,10 @@ - pyk.kbuild.project — pyk 0.1.776 documentation + pyk.kbuild.project — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kbuild/utils.html b/_modules/pyk/kbuild/utils.html index d3f3271b2..ba0beca1d 100644 --- a/_modules/pyk/kbuild/utils.html +++ b/_modules/pyk/kbuild/utils.html @@ -4,10 +4,10 @@ - pyk.kbuild.utils — pyk 0.1.776 documentation + pyk.kbuild.utils — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kcfg/exploration.html b/_modules/pyk/kcfg/exploration.html index 77c8347ad..1af67f27b 100644 --- a/_modules/pyk/kcfg/exploration.html +++ b/_modules/pyk/kcfg/exploration.html @@ -4,10 +4,10 @@ - pyk.kcfg.exploration — pyk 0.1.776 documentation + pyk.kcfg.exploration — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kcfg/explore.html b/_modules/pyk/kcfg/explore.html index 4afce6da1..312d28d9b 100644 --- a/_modules/pyk/kcfg/explore.html +++ b/_modules/pyk/kcfg/explore.html @@ -4,10 +4,10 @@ - pyk.kcfg.explore — pyk 0.1.776 documentation + pyk.kcfg.explore — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kcfg/kcfg.html b/_modules/pyk/kcfg/kcfg.html index 9a21e4649..88ada1846 100644 --- a/_modules/pyk/kcfg/kcfg.html +++ b/_modules/pyk/kcfg/kcfg.html @@ -4,10 +4,10 @@ - pyk.kcfg.kcfg — pyk 0.1.776 documentation + pyk.kcfg.kcfg — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kcfg/semantics.html b/_modules/pyk/kcfg/semantics.html index 6d0918c08..293c9764a 100644 --- a/_modules/pyk/kcfg/semantics.html +++ b/_modules/pyk/kcfg/semantics.html @@ -4,10 +4,10 @@ - pyk.kcfg.semantics — pyk 0.1.776 documentation + pyk.kcfg.semantics — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kcfg/show.html b/_modules/pyk/kcfg/show.html index b6481ad9a..fc1a7effe 100644 --- a/_modules/pyk/kcfg/show.html +++ b/_modules/pyk/kcfg/show.html @@ -4,10 +4,10 @@ - pyk.kcfg.show — pyk 0.1.776 documentation + pyk.kcfg.show — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kcfg/store.html b/_modules/pyk/kcfg/store.html index 96a139dd3..1c83474c2 100644 --- a/_modules/pyk/kcfg/store.html +++ b/_modules/pyk/kcfg/store.html @@ -4,10 +4,10 @@ - pyk.kcfg.store — pyk 0.1.776 documentation + pyk.kcfg.store — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kcfg/tui.html b/_modules/pyk/kcfg/tui.html index 810c988e3..0bc10d8e6 100644 --- a/_modules/pyk/kcfg/tui.html +++ b/_modules/pyk/kcfg/tui.html @@ -4,10 +4,10 @@ - pyk.kcfg.tui — pyk 0.1.776 documentation + pyk.kcfg.tui — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kcovr.html b/_modules/pyk/kcovr.html index 1c0950134..d0fc401b8 100644 --- a/_modules/pyk/kcovr.html +++ b/_modules/pyk/kcovr.html @@ -4,10 +4,10 @@ - pyk.kcovr — pyk 0.1.776 documentation + pyk.kcovr — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kdist/api.html b/_modules/pyk/kdist/api.html index 44cb37f65..af14be4ec 100644 --- a/_modules/pyk/kdist/api.html +++ b/_modules/pyk/kdist/api.html @@ -4,10 +4,10 @@ - pyk.kdist.api — pyk 0.1.776 documentation + pyk.kdist.api — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kdist/utils.html b/_modules/pyk/kdist/utils.html index c17b29914..f71835775 100644 --- a/_modules/pyk/kdist/utils.html +++ b/_modules/pyk/kdist/utils.html @@ -4,10 +4,10 @@ - pyk.kdist.utils — pyk 0.1.776 documentation + pyk.kdist.utils — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kllvm/compiler.html b/_modules/pyk/kllvm/compiler.html index 11113912b..8f35424c3 100644 --- a/_modules/pyk/kllvm/compiler.html +++ b/_modules/pyk/kllvm/compiler.html @@ -4,10 +4,10 @@ - pyk.kllvm.compiler — pyk 0.1.776 documentation + pyk.kllvm.compiler — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kllvm/importer.html b/_modules/pyk/kllvm/importer.html index da30d2ec3..645e2a8f7 100644 --- a/_modules/pyk/kllvm/importer.html +++ b/_modules/pyk/kllvm/importer.html @@ -4,10 +4,10 @@ - pyk.kllvm.importer — pyk 0.1.776 documentation + pyk.kllvm.importer — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kllvm/runtime.html b/_modules/pyk/kllvm/runtime.html index 6afbc42e1..d0c8ef92e 100644 --- a/_modules/pyk/kllvm/runtime.html +++ b/_modules/pyk/kllvm/runtime.html @@ -4,10 +4,10 @@ - pyk.kllvm.runtime — pyk 0.1.776 documentation + pyk.kllvm.runtime — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kore/kompiled.html b/_modules/pyk/kore/kompiled.html index 3df269d08..9ba363050 100644 --- a/_modules/pyk/kore/kompiled.html +++ b/_modules/pyk/kore/kompiled.html @@ -4,10 +4,10 @@ - pyk.kore.kompiled — pyk 0.1.776 documentation + pyk.kore.kompiled — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kore/lexer.html b/_modules/pyk/kore/lexer.html index 349ed1987..885669569 100644 --- a/_modules/pyk/kore/lexer.html +++ b/_modules/pyk/kore/lexer.html @@ -4,10 +4,10 @@ - pyk.kore.lexer — pyk 0.1.776 documentation + pyk.kore.lexer — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kore/manip.html b/_modules/pyk/kore/manip.html index d711918ef..788f32623 100644 --- a/_modules/pyk/kore/manip.html +++ b/_modules/pyk/kore/manip.html @@ -4,10 +4,10 @@ - pyk.kore.manip — pyk 0.1.776 documentation + pyk.kore.manip — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kore/match.html b/_modules/pyk/kore/match.html index 0db3874ac..7f7e33e78 100644 --- a/_modules/pyk/kore/match.html +++ b/_modules/pyk/kore/match.html @@ -4,10 +4,10 @@ - pyk.kore.match — pyk 0.1.776 documentation + pyk.kore.match — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kore/parser.html b/_modules/pyk/kore/parser.html index 8e37be740..e8e733413 100644 --- a/_modules/pyk/kore/parser.html +++ b/_modules/pyk/kore/parser.html @@ -4,10 +4,10 @@ - pyk.kore.parser — pyk 0.1.776 documentation + pyk.kore.parser — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kore/pool.html b/_modules/pyk/kore/pool.html index bd3432a98..371a4091b 100644 --- a/_modules/pyk/kore/pool.html +++ b/_modules/pyk/kore/pool.html @@ -4,10 +4,10 @@ - pyk.kore.pool — pyk 0.1.776 documentation + pyk.kore.pool — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kore/prelude.html b/_modules/pyk/kore/prelude.html index 7aefb1a42..67d0e0378 100644 --- a/_modules/pyk/kore/prelude.html +++ b/_modules/pyk/kore/prelude.html @@ -4,10 +4,10 @@ - pyk.kore.prelude — pyk 0.1.776 documentation + pyk.kore.prelude — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kore/rpc.html b/_modules/pyk/kore/rpc.html index cfdc0df80..781d3e220 100644 --- a/_modules/pyk/kore/rpc.html +++ b/_modules/pyk/kore/rpc.html @@ -4,10 +4,10 @@ - pyk.kore.rpc — pyk 0.1.776 documentation + pyk.kore.rpc — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kore/syntax.html b/_modules/pyk/kore/syntax.html index e819c9a36..93e1f0a9c 100644 --- a/_modules/pyk/kore/syntax.html +++ b/_modules/pyk/kore/syntax.html @@ -4,10 +4,10 @@ - pyk.kore.syntax — pyk 0.1.776 documentation + pyk.kore.syntax — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kore/tools.html b/_modules/pyk/kore/tools.html index 187af9667..f63fb4d94 100644 --- a/_modules/pyk/kore/tools.html +++ b/_modules/pyk/kore/tools.html @@ -4,10 +4,10 @@ - pyk.kore.tools — pyk 0.1.776 documentation + pyk.kore.tools — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/kore_exec_covr/kore_exec_covr.html b/_modules/pyk/kore_exec_covr/kore_exec_covr.html index 9b8841b12..84a6bb6e1 100644 --- a/_modules/pyk/kore_exec_covr/kore_exec_covr.html +++ b/_modules/pyk/kore_exec_covr/kore_exec_covr.html @@ -4,10 +4,10 @@ - pyk.kore_exec_covr.kore_exec_covr — pyk 0.1.776 documentation + pyk.kore_exec_covr.kore_exec_covr — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/krepl/repl.html b/_modules/pyk/krepl/repl.html index 7be1a3d8a..12f0284b3 100644 --- a/_modules/pyk/krepl/repl.html +++ b/_modules/pyk/krepl/repl.html @@ -4,10 +4,10 @@ - pyk.krepl.repl — pyk 0.1.776 documentation + pyk.krepl.repl — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/ktool/kompile.html b/_modules/pyk/ktool/kompile.html index 918592f7b..757bbe84f 100644 --- a/_modules/pyk/ktool/kompile.html +++ b/_modules/pyk/ktool/kompile.html @@ -4,10 +4,10 @@ - pyk.ktool.kompile — pyk 0.1.776 documentation + pyk.ktool.kompile — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/ktool/kprint.html b/_modules/pyk/ktool/kprint.html index 5f3f890f5..f767d8542 100644 --- a/_modules/pyk/ktool/kprint.html +++ b/_modules/pyk/ktool/kprint.html @@ -4,10 +4,10 @@ - pyk.ktool.kprint — pyk 0.1.776 documentation + pyk.ktool.kprint — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/ktool/kprove.html b/_modules/pyk/ktool/kprove.html index 8cafad986..c2d5030f3 100644 --- a/_modules/pyk/ktool/kprove.html +++ b/_modules/pyk/ktool/kprove.html @@ -4,10 +4,10 @@ - pyk.ktool.kprove — pyk 0.1.776 documentation + pyk.ktool.kprove — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/ktool/krun.html b/_modules/pyk/ktool/krun.html index fb3a510e1..38f9f6ee1 100644 --- a/_modules/pyk/ktool/krun.html +++ b/_modules/pyk/ktool/krun.html @@ -4,10 +4,10 @@ - pyk.ktool.krun — pyk 0.1.776 documentation + pyk.ktool.krun — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/prelude/bytes.html b/_modules/pyk/prelude/bytes.html index 943a8f107..8b41bcf72 100644 --- a/_modules/pyk/prelude/bytes.html +++ b/_modules/pyk/prelude/bytes.html @@ -4,10 +4,10 @@ - pyk.prelude.bytes — pyk 0.1.776 documentation + pyk.prelude.bytes — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/prelude/collections.html b/_modules/pyk/prelude/collections.html index 171200f22..fe35fe9c8 100644 --- a/_modules/pyk/prelude/collections.html +++ b/_modules/pyk/prelude/collections.html @@ -4,10 +4,10 @@ - pyk.prelude.collections — pyk 0.1.776 documentation + pyk.prelude.collections — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/prelude/kbool.html b/_modules/pyk/prelude/kbool.html index 902b3f4bc..dfb4f12ea 100644 --- a/_modules/pyk/prelude/kbool.html +++ b/_modules/pyk/prelude/kbool.html @@ -4,10 +4,10 @@ - pyk.prelude.kbool — pyk 0.1.776 documentation + pyk.prelude.kbool — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/prelude/kint.html b/_modules/pyk/prelude/kint.html index 28524203f..461deac35 100644 --- a/_modules/pyk/prelude/kint.html +++ b/_modules/pyk/prelude/kint.html @@ -4,10 +4,10 @@ - pyk.prelude.kint — pyk 0.1.776 documentation + pyk.prelude.kint — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/prelude/ml.html b/_modules/pyk/prelude/ml.html index 16d189706..aa1ec29e2 100644 --- a/_modules/pyk/prelude/ml.html +++ b/_modules/pyk/prelude/ml.html @@ -4,10 +4,10 @@ - pyk.prelude.ml — pyk 0.1.776 documentation + pyk.prelude.ml — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/prelude/string.html b/_modules/pyk/prelude/string.html index 9dd5871a3..18f7c0c47 100644 --- a/_modules/pyk/prelude/string.html +++ b/_modules/pyk/prelude/string.html @@ -4,10 +4,10 @@ - pyk.prelude.string — pyk 0.1.776 documentation + pyk.prelude.string — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/prelude/utils.html b/_modules/pyk/prelude/utils.html index fcfeff0b0..2552d834f 100644 --- a/_modules/pyk/prelude/utils.html +++ b/_modules/pyk/prelude/utils.html @@ -4,10 +4,10 @@ - pyk.prelude.utils — pyk 0.1.776 documentation + pyk.prelude.utils — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/proof/implies.html b/_modules/pyk/proof/implies.html index 1a6a239d0..da720d2a9 100644 --- a/_modules/pyk/proof/implies.html +++ b/_modules/pyk/proof/implies.html @@ -4,10 +4,10 @@ - pyk.proof.implies — pyk 0.1.776 documentation + pyk.proof.implies — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/proof/parallel.html b/_modules/pyk/proof/parallel.html index a5b225625..022adb816 100644 --- a/_modules/pyk/proof/parallel.html +++ b/_modules/pyk/proof/parallel.html @@ -4,10 +4,10 @@ - pyk.proof.parallel — pyk 0.1.776 documentation + pyk.proof.parallel — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/proof/proof.html b/_modules/pyk/proof/proof.html index dd0cf799b..379bb89c2 100644 --- a/_modules/pyk/proof/proof.html +++ b/_modules/pyk/proof/proof.html @@ -4,10 +4,10 @@ - pyk.proof.proof — pyk 0.1.776 documentation + pyk.proof.proof — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/proof/reachability.html b/_modules/pyk/proof/reachability.html index 0ee44f3d0..87b5f843f 100644 --- a/_modules/pyk/proof/reachability.html +++ b/_modules/pyk/proof/reachability.html @@ -4,10 +4,10 @@ - pyk.proof.reachability — pyk 0.1.776 documentation + pyk.proof.reachability — pyk 0.1.777 documentation - + @@ -707,362 +707,357 @@

Source code for pyk.proof.reachability

 584                f'Cannot refute node {node.id}: unexpected non-identity substitution {csubst.subst} in Split from {closest_branch.source.id}'
 585            )
 586            return None
-587        if len(csubst.constraints) > 1:
-588            _LOGGER.error(
-589                f'Cannot refute node {node.id}: unexpected non-singleton constraints {csubst.constraints} in Split from {closest_branch.source.id}'
-590            )
-591            return None
-592
-593        last_constraint = ml_pred_to_bool(csubst.constraints[0])
-594        relevant_vars = free_vars(last_constraint)
-595        pre_split_constraints = [
-596            ml_pred_to_bool(c)
-597            for c in remove_useless_constraints(closest_branch.source.cterm.constraints, relevant_vars)
-598        ]
-599
-600        refutation_id = self.get_refutation_id(node.id)
-601        _LOGGER.info(f'Adding refutation proof {refutation_id} as subproof of {self.id}')
-602        refutation = RefutationProof(
-603            id=refutation_id,
-604            pre_constraints=pre_split_constraints,
-605            last_constraint=last_constraint,
-606            proof_dir=self.proof_dir,
-607        )
-608
-609        self.add_subproof(refutation)
-610        return refutation
+587 +588 last_constraint = ml_pred_to_bool(csubst.constraint) +589 relevant_vars = free_vars(last_constraint) +590 pre_split_constraints = [ +591 ml_pred_to_bool(c) +592 for c in remove_useless_constraints(closest_branch.source.cterm.constraints, relevant_vars) +593 ] +594 +595 refutation_id = self.get_refutation_id(node.id) +596 _LOGGER.info(f'Adding refutation proof {refutation_id} as subproof of {self.id}') +597 refutation = RefutationProof( +598 id=refutation_id, +599 pre_constraints=pre_split_constraints, +600 last_constraint=last_constraint, +601 proof_dir=self.proof_dir, +602 ) +603 +604 self.add_subproof(refutation) +605 return refutation -611 -612 +606 +607
[docs] -613class APRProver(Prover): -614 proof: APRProof -615 -616 main_module_name: str -617 dependencies_module_name: str -618 circularities_module_name: str -619 execute_depth: int | None -620 cut_point_rules: Iterable[str] -621 terminal_rules: Iterable[str] -622 counterexample_info: bool -623 always_check_subsumption: bool -624 fast_check_subsumption: bool -625 -626 _checked_for_terminal: set[int] -627 _checked_for_subsumption: set[int] -628 _checked_for_bounded: set[int] -629 -630 def __init__( -631 self, -632 proof: APRProof, -633 kcfg_explore: KCFGExplore, -634 execute_depth: int | None = None, -635 cut_point_rules: Iterable[str] = (), -636 terminal_rules: Iterable[str] = (), -637 counterexample_info: bool = False, -638 always_check_subsumption: bool = True, -639 fast_check_subsumption: bool = False, -640 ) -> None: -641 def _inject_module(module_name: str, import_name: str, sentences: list[KRuleLike]) -> None: -642 _module = KFlatModule(module_name, sentences, [KImport(import_name)]) -643 _kore_module = kflatmodule_to_kore( -644 self.kcfg_explore.cterm_symbolic._definition, self.kcfg_explore.cterm_symbolic._kompiled_kore, _module -645 ) -646 self.kcfg_explore.cterm_symbolic._kore_client.add_module(_kore_module, name_as_id=True) -647 -648 super().__init__(kcfg_explore) -649 self.proof = proof -650 self.main_module_name = self.kcfg_explore.cterm_symbolic._definition.main_module_name -651 self.execute_depth = execute_depth -652 self.cut_point_rules = cut_point_rules -653 self.terminal_rules = terminal_rules -654 self.counterexample_info = counterexample_info -655 self.always_check_subsumption = always_check_subsumption -656 self.fast_check_subsumption = fast_check_subsumption -657 -658 subproofs: list[Proof] = ( -659 [Proof.read_proof_data(proof.proof_dir, i) for i in proof.subproof_ids] -660 if proof.proof_dir is not None -661 else [] -662 ) -663 -664 dependencies_as_rules: list[KRuleLike] = [] -665 for apr_subproof in [pf for pf in subproofs if isinstance(pf, APRProof)]: -666 dependencies_as_rules.extend(apr_subproof.kcfg.to_rules(priority=20)) -667 if apr_subproof.admitted and len(apr_subproof.kcfg.predecessors(apr_subproof.target)) == 0: -668 dependencies_as_rules.append(apr_subproof.as_rule(priority=20)) -669 circularity_rule = proof.as_rule(priority=20) -670 -671 module_name = self.proof.module_name -672 self.dependencies_module_name = module_name + '-DEPENDS-MODULE' -673 self.circularities_module_name = module_name + '-CIRCULARITIES-MODULE' -674 _inject_module(self.dependencies_module_name, self.main_module_name, dependencies_as_rules) -675 _inject_module(self.circularities_module_name, self.dependencies_module_name, [circularity_rule]) +608class APRProver(Prover): +609 proof: APRProof +610 +611 main_module_name: str +612 dependencies_module_name: str +613 circularities_module_name: str +614 execute_depth: int | None +615 cut_point_rules: Iterable[str] +616 terminal_rules: Iterable[str] +617 counterexample_info: bool +618 always_check_subsumption: bool +619 fast_check_subsumption: bool +620 +621 _checked_for_terminal: set[int] +622 _checked_for_subsumption: set[int] +623 _checked_for_bounded: set[int] +624 +625 def __init__( +626 self, +627 proof: APRProof, +628 kcfg_explore: KCFGExplore, +629 execute_depth: int | None = None, +630 cut_point_rules: Iterable[str] = (), +631 terminal_rules: Iterable[str] = (), +632 counterexample_info: bool = False, +633 always_check_subsumption: bool = True, +634 fast_check_subsumption: bool = False, +635 ) -> None: +636 def _inject_module(module_name: str, import_name: str, sentences: list[KRuleLike]) -> None: +637 _module = KFlatModule(module_name, sentences, [KImport(import_name)]) +638 _kore_module = kflatmodule_to_kore( +639 self.kcfg_explore.cterm_symbolic._definition, self.kcfg_explore.cterm_symbolic._kompiled_kore, _module +640 ) +641 self.kcfg_explore.cterm_symbolic._kore_client.add_module(_kore_module, name_as_id=True) +642 +643 super().__init__(kcfg_explore) +644 self.proof = proof +645 self.main_module_name = self.kcfg_explore.cterm_symbolic._definition.main_module_name +646 self.execute_depth = execute_depth +647 self.cut_point_rules = cut_point_rules +648 self.terminal_rules = terminal_rules +649 self.counterexample_info = counterexample_info +650 self.always_check_subsumption = always_check_subsumption +651 self.fast_check_subsumption = fast_check_subsumption +652 +653 subproofs: list[Proof] = ( +654 [Proof.read_proof_data(proof.proof_dir, i) for i in proof.subproof_ids] +655 if proof.proof_dir is not None +656 else [] +657 ) +658 +659 dependencies_as_rules: list[KRuleLike] = [] +660 for apr_subproof in [pf for pf in subproofs if isinstance(pf, APRProof)]: +661 dependencies_as_rules.extend(apr_subproof.kcfg.to_rules(priority=20)) +662 if apr_subproof.admitted and len(apr_subproof.kcfg.predecessors(apr_subproof.target)) == 0: +663 dependencies_as_rules.append(apr_subproof.as_rule(priority=20)) +664 circularity_rule = proof.as_rule(priority=20) +665 +666 module_name = self.proof.module_name +667 self.dependencies_module_name = module_name + '-DEPENDS-MODULE' +668 self.circularities_module_name = module_name + '-CIRCULARITIES-MODULE' +669 _inject_module(self.dependencies_module_name, self.main_module_name, dependencies_as_rules) +670 _inject_module(self.circularities_module_name, self.dependencies_module_name, [circularity_rule]) +671 +672 self._checked_for_terminal = set() +673 self._checked_for_subsumption = set() +674 self._checked_for_bounded = set() +675 self._check_all_terminals() 676 -677 self._checked_for_terminal = set() -678 self._checked_for_subsumption = set() -679 self._checked_for_bounded = set() -680 self._check_all_terminals() -681
[docs] -682 def nonzero_depth(self, node: KCFG.Node) -> bool: -683 return not self.proof.kcfg.zero_depth_between(self.proof.init, node.id)
+677 def nonzero_depth(self, node: KCFG.Node) -> bool: +678 return not self.proof.kcfg.zero_depth_between(self.proof.init, node.id)
-684 -685 def _check_terminal(self, node: KCFG.Node) -> None: -686 if node.id not in self._checked_for_terminal: -687 _LOGGER.info(f'Checking terminal: {node.id}') -688 self._checked_for_terminal.add(node.id) -689 if self.kcfg_explore.kcfg_semantics.is_terminal(node.cterm): -690 _LOGGER.info(f'Terminal node: {node.id}.') -691 self.proof.add_terminal(node.id) -692 elif self.fast_check_subsumption and self._may_subsume(node): -693 _LOGGER.info(f'Marking node as terminal because of fast may subsume check {self.proof.id}: {node.id}') -694 self.proof.add_terminal(node.id) -695 -696 def _check_all_terminals(self) -> None: -697 for node in self.proof.kcfg.nodes: -698 self._check_terminal(node) -699 -700 def _may_subsume(self, node: KCFG.Node) -> bool: -701 node_k_cell = node.cterm.try_cell('K_CELL') -702 target_k_cell = self.proof.kcfg.node(self.proof.target).cterm.try_cell('K_CELL') -703 if node_k_cell and target_k_cell and not target_k_cell.match(node_k_cell): -704 return False -705 return True -706 -707 def _check_subsume(self, node: KCFG.Node) -> CSubst | None: -708 target_cterm = self.proof.kcfg.node(self.proof.target).cterm -709 _LOGGER.info( -710 f'Checking subsumption into target state {self.proof.id}: {shorten_hashes((node.id, target_cterm))}' -711 ) -712 if self.fast_check_subsumption and not self._may_subsume(node): -713 _LOGGER.info( -714 f'Skipping full subsumption check because of fast may subsume check {self.proof.id}: {node.id}' -715 ) -716 return None -717 _csubst = self.kcfg_explore.cterm_symbolic.implies(node.cterm, target_cterm) -718 csubst = _csubst.csubst -719 if csubst is not None: -720 _LOGGER.info(f'Subsumed into target node {self.proof.id}: {shorten_hashes((node.id, self.proof.target))}') -721 return csubst -722 +679 +680 def _check_terminal(self, node: KCFG.Node) -> None: +681 if node.id not in self._checked_for_terminal: +682 _LOGGER.info(f'Checking terminal: {node.id}') +683 self._checked_for_terminal.add(node.id) +684 if self.kcfg_explore.kcfg_semantics.is_terminal(node.cterm): +685 _LOGGER.info(f'Terminal node: {node.id}.') +686 self.proof.add_terminal(node.id) +687 elif self.fast_check_subsumption and self._may_subsume(node): +688 _LOGGER.info(f'Marking node as terminal because of fast may subsume check {self.proof.id}: {node.id}') +689 self.proof.add_terminal(node.id) +690 +691 def _check_all_terminals(self) -> None: +692 for node in self.proof.kcfg.nodes: +693 self._check_terminal(node) +694 +695 def _may_subsume(self, node: KCFG.Node) -> bool: +696 node_k_cell = node.cterm.try_cell('K_CELL') +697 target_k_cell = self.proof.kcfg.node(self.proof.target).cterm.try_cell('K_CELL') +698 if node_k_cell and target_k_cell and not target_k_cell.match(node_k_cell): +699 return False +700 return True +701 +702 def _check_subsume(self, node: KCFG.Node) -> CSubst | None: +703 target_cterm = self.proof.kcfg.node(self.proof.target).cterm +704 _LOGGER.info( +705 f'Checking subsumption into target state {self.proof.id}: {shorten_hashes((node.id, target_cterm))}' +706 ) +707 if self.fast_check_subsumption and not self._may_subsume(node): +708 _LOGGER.info( +709 f'Skipping full subsumption check because of fast may subsume check {self.proof.id}: {node.id}' +710 ) +711 return None +712 _csubst = self.kcfg_explore.cterm_symbolic.implies(node.cterm, target_cterm) +713 csubst = _csubst.csubst +714 if csubst is not None: +715 _LOGGER.info(f'Subsumed into target node {self.proof.id}: {shorten_hashes((node.id, self.proof.target))}') +716 return csubst +717
[docs] -723 def step_proof(self) -> Iterable[StepResult]: -724 if not self.proof.pending: -725 return [] -726 curr_node = self.proof.pending[0] -727 -728 if self.proof.bmc_depth is not None and curr_node.id not in self._checked_for_bounded: -729 _LOGGER.info(f'Checking bmc depth for node {self.proof.id}: {curr_node.id}') -730 self._checked_for_bounded.add(curr_node.id) -731 -732 prior_loops = [] -733 for succ in reversed(self.proof.shortest_path_to(curr_node.id)): -734 if self.kcfg_explore.kcfg_semantics.same_loop(succ.source.cterm, curr_node.cterm): -735 if succ.source.id in self.proof.prior_loops_cache: -736 if self.proof.kcfg.zero_depth_between(succ.source.id, curr_node.id): -737 prior_loops = self.proof.prior_loops_cache[succ.source.id] -738 else: -739 prior_loops = self.proof.prior_loops_cache[succ.source.id] + [succ.source.id] -740 break -741 else: -742 self.proof.prior_loops_cache[succ.source.id] = [] -743 -744 self.proof.prior_loops_cache[curr_node.id] = prior_loops +718 def step_proof(self) -> Iterable[StepResult]: +719 if not self.proof.pending: +720 return [] +721 curr_node = self.proof.pending[0] +722 +723 if self.proof.bmc_depth is not None and curr_node.id not in self._checked_for_bounded: +724 _LOGGER.info(f'Checking bmc depth for node {self.proof.id}: {curr_node.id}') +725 self._checked_for_bounded.add(curr_node.id) +726 +727 prior_loops = [] +728 for succ in reversed(self.proof.shortest_path_to(curr_node.id)): +729 if self.kcfg_explore.kcfg_semantics.same_loop(succ.source.cterm, curr_node.cterm): +730 if succ.source.id in self.proof.prior_loops_cache: +731 if self.proof.kcfg.zero_depth_between(succ.source.id, curr_node.id): +732 prior_loops = self.proof.prior_loops_cache[succ.source.id] +733 else: +734 prior_loops = self.proof.prior_loops_cache[succ.source.id] + [succ.source.id] +735 break +736 else: +737 self.proof.prior_loops_cache[succ.source.id] = [] +738 +739 self.proof.prior_loops_cache[curr_node.id] = prior_loops +740 +741 _LOGGER.info(f'Prior loop heads for node {self.proof.id}: {(curr_node.id, prior_loops)}') +742 if len(prior_loops) > self.proof.bmc_depth: +743 _LOGGER.warning(f'Bounded node {self.proof.id}: {curr_node.id} at bmc depth {self.proof.bmc_depth}') +744 return [APRProofBoundedResult(curr_node.id)] 745 -746 _LOGGER.info(f'Prior loop heads for node {self.proof.id}: {(curr_node.id, prior_loops)}') -747 if len(prior_loops) > self.proof.bmc_depth: -748 _LOGGER.warning(f'Bounded node {self.proof.id}: {curr_node.id} at bmc depth {self.proof.bmc_depth}') -749 return [APRProofBoundedResult(curr_node.id)] -750 -751 # Terminal checks for current node and target node -752 is_terminal = self.kcfg_explore.kcfg_semantics.is_terminal(curr_node.cterm) -753 target_is_terminal = self.proof.is_terminal(self.proof.target) -754 -755 terminal_result = [APRProofTerminalResult(node_id=curr_node.id)] if is_terminal else [] -756 -757 # Subsumption should be checked if and only if the target node -758 # and the current node are either both terminal or both not terminal -759 if is_terminal == target_is_terminal: -760 csubst = self._check_subsume(curr_node) -761 if csubst is not None: -762 # Information about the subsumed node being terminal must be returned -763 # so that the set of terminal nodes is correctly updated -764 return terminal_result + [APRProofSubsumeResult(csubst=csubst, node_id=curr_node.id)] +746 # Terminal checks for current node and target node +747 is_terminal = self.kcfg_explore.kcfg_semantics.is_terminal(curr_node.cterm) +748 target_is_terminal = self.proof.is_terminal(self.proof.target) +749 +750 terminal_result = [APRProofTerminalResult(node_id=curr_node.id)] if is_terminal else [] +751 +752 # Subsumption should be checked if and only if the target node +753 # and the current node are either both terminal or both not terminal +754 if is_terminal == target_is_terminal: +755 csubst = self._check_subsume(curr_node) +756 if csubst is not None: +757 # Information about the subsumed node being terminal must be returned +758 # so that the set of terminal nodes is correctly updated +759 return terminal_result + [APRProofSubsumeResult(csubst=csubst, node_id=curr_node.id)] +760 +761 if is_terminal: +762 return terminal_result +763 +764 module_name = self.circularities_module_name if self.nonzero_depth(curr_node) else self.dependencies_module_name 765 -766 if is_terminal: -767 return terminal_result -768 -769 module_name = self.circularities_module_name if self.nonzero_depth(curr_node) else self.dependencies_module_name -770 -771 self.kcfg_explore.check_extendable(self.proof, curr_node) -772 extend_result = self.kcfg_explore.extend_cterm( -773 curr_node.cterm, -774 execute_depth=self.execute_depth, -775 cut_point_rules=self.cut_point_rules, -776 terminal_rules=self.terminal_rules, -777 module_name=module_name, -778 node_id=curr_node.id, -779 ) -780 return [APRProofExtendResult(node_id=curr_node.id, extend_result=extend_result)]
+766 self.kcfg_explore.check_extendable(self.proof, curr_node) +767 extend_result = self.kcfg_explore.extend_cterm( +768 curr_node.cterm, +769 execute_depth=self.execute_depth, +770 cut_point_rules=self.cut_point_rules, +771 terminal_rules=self.terminal_rules, +772 module_name=module_name, +773 node_id=curr_node.id, +774 ) +775 return [APRProofExtendResult(node_id=curr_node.id, extend_result=extend_result)] -781 +776
[docs] -782 def failure_info(self) -> FailureInfo: -783 return APRFailureInfo.from_proof(self.proof, self.kcfg_explore, counterexample_info=self.counterexample_info)
+777 def failure_info(self) -> FailureInfo: +778 return APRFailureInfo.from_proof(self.proof, self.kcfg_explore, counterexample_info=self.counterexample_info) -784 -785 +779 +780
[docs] -786@dataclass(frozen=True) -787class APRSummary(ProofSummary): -788 id: str -789 status: ProofStatus -790 admitted: bool -791 nodes: int -792 pending: int -793 failing: int -794 vacuous: int -795 stuck: int -796 terminal: int -797 refuted: int -798 bmc_depth: int | None -799 bounded: int -800 subproofs: int -801 formatted_exec_time: str -802 -803 @property -804 def lines(self) -> list[str]: -805 _lines = [ -806 f'APRProof: {self.id}', -807 f' status: {self.status}', -808 f' admitted: {self.admitted}', -809 f' nodes: {self.nodes}', -810 f' pending: {self.pending}', -811 f' failing: {self.failing}', -812 f' vacuous: {self.vacuous}', -813 f' stuck: {self.stuck}', -814 f' terminal: {self.terminal}', -815 f' refuted: {self.refuted}', -816 f' bounded: {self.bounded}', -817 f' execution time: {self.formatted_exec_time}', -818 ] -819 if self.bmc_depth is not None: -820 _lines.append(f' bmc depth: {self.bmc_depth}') -821 _lines.append(f'Subproofs: {self.subproofs}') -822 return _lines
+781@dataclass(frozen=True) +782class APRSummary(ProofSummary): +783 id: str +784 status: ProofStatus +785 admitted: bool +786 nodes: int +787 pending: int +788 failing: int +789 vacuous: int +790 stuck: int +791 terminal: int +792 refuted: int +793 bmc_depth: int | None +794 bounded: int +795 subproofs: int +796 formatted_exec_time: str +797 +798 @property +799 def lines(self) -> list[str]: +800 _lines = [ +801 f'APRProof: {self.id}', +802 f' status: {self.status}', +803 f' admitted: {self.admitted}', +804 f' nodes: {self.nodes}', +805 f' pending: {self.pending}', +806 f' failing: {self.failing}', +807 f' vacuous: {self.vacuous}', +808 f' stuck: {self.stuck}', +809 f' terminal: {self.terminal}', +810 f' refuted: {self.refuted}', +811 f' bounded: {self.bounded}', +812 f' execution time: {self.formatted_exec_time}', +813 ] +814 if self.bmc_depth is not None: +815 _lines.append(f' bmc depth: {self.bmc_depth}') +816 _lines.append(f'Subproofs: {self.subproofs}') +817 return _lines -823 -824 +818 +819
[docs] -825@dataclass(frozen=True) -826class APRFailureInfo(FailureInfo): -827 pending_nodes: frozenset[int] -828 failing_nodes: frozenset[int] -829 path_conditions: FrozenDict[int, str] -830 failure_reasons: FrozenDict[int, str] -831 models: FrozenDict[int, frozenset[tuple[str, str]]] -832 -833 def __init__( -834 self, -835 failing_nodes: Iterable[int], -836 pending_nodes: Iterable[int], -837 path_conditions: Mapping[int, str], -838 failure_reasons: Mapping[int, str], -839 models: Mapping[int, Iterable[tuple[str, str]]], -840 ): -841 object.__setattr__(self, 'failing_nodes', frozenset(failing_nodes)) -842 object.__setattr__(self, 'pending_nodes', frozenset(pending_nodes)) -843 object.__setattr__(self, 'path_conditions', FrozenDict(path_conditions)) -844 object.__setattr__(self, 'failure_reasons', FrozenDict(failure_reasons)) -845 object.__setattr__( -846 self, 'models', FrozenDict({node_id: frozenset(model) for (node_id, model) in models.items()}) -847 ) -848 +820@dataclass(frozen=True) +821class APRFailureInfo(FailureInfo): +822 pending_nodes: frozenset[int] +823 failing_nodes: frozenset[int] +824 path_conditions: FrozenDict[int, str] +825 failure_reasons: FrozenDict[int, str] +826 models: FrozenDict[int, frozenset[tuple[str, str]]] +827 +828 def __init__( +829 self, +830 failing_nodes: Iterable[int], +831 pending_nodes: Iterable[int], +832 path_conditions: Mapping[int, str], +833 failure_reasons: Mapping[int, str], +834 models: Mapping[int, Iterable[tuple[str, str]]], +835 ): +836 object.__setattr__(self, 'failing_nodes', frozenset(failing_nodes)) +837 object.__setattr__(self, 'pending_nodes', frozenset(pending_nodes)) +838 object.__setattr__(self, 'path_conditions', FrozenDict(path_conditions)) +839 object.__setattr__(self, 'failure_reasons', FrozenDict(failure_reasons)) +840 object.__setattr__( +841 self, 'models', FrozenDict({node_id: frozenset(model) for (node_id, model) in models.items()}) +842 ) +843
[docs] -849 @staticmethod -850 def from_proof(proof: APRProof, kcfg_explore: KCFGExplore, counterexample_info: bool = False) -> APRFailureInfo: -851 target = proof.kcfg.node(proof.target) -852 pending_nodes = {node.id for node in proof.pending} -853 failing_nodes = {node.id for node in proof.failing} -854 path_conditions = {} -855 failure_reasons = {} -856 models = {} -857 for node in proof.failing: -858 node_cterm, _ = kcfg_explore.cterm_symbolic.simplify(node.cterm) -859 target_cterm, _ = kcfg_explore.cterm_symbolic.simplify(target.cterm) -860 _, reason = kcfg_explore.implication_failure_reason(node_cterm, target_cterm) -861 path_condition = kcfg_explore.pretty_print(proof.path_constraints(node.id)) -862 failure_reasons[node.id] = reason -863 path_conditions[node.id] = path_condition -864 if counterexample_info: -865 model_subst = kcfg_explore.cterm_symbolic.get_model(node.cterm) -866 if type(model_subst) is Subst: -867 model: list[tuple[str, str]] = [] -868 for var, term in model_subst.to_dict().items(): -869 term_kast = KInner.from_dict(term) -870 term_pretty = kcfg_explore.pretty_print(term_kast) -871 model.append((var, term_pretty)) -872 models[node.id] = model -873 return APRFailureInfo( -874 failing_nodes=failing_nodes, -875 pending_nodes=pending_nodes, -876 path_conditions=path_conditions, -877 failure_reasons=failure_reasons, -878 models=models, -879 )
+844 @staticmethod +845 def from_proof(proof: APRProof, kcfg_explore: KCFGExplore, counterexample_info: bool = False) -> APRFailureInfo: +846 target = proof.kcfg.node(proof.target) +847 pending_nodes = {node.id for node in proof.pending} +848 failing_nodes = {node.id for node in proof.failing} +849 path_conditions = {} +850 failure_reasons = {} +851 models = {} +852 for node in proof.failing: +853 node_cterm, _ = kcfg_explore.cterm_symbolic.simplify(node.cterm) +854 target_cterm, _ = kcfg_explore.cterm_symbolic.simplify(target.cterm) +855 _, reason = kcfg_explore.implication_failure_reason(node_cterm, target_cterm) +856 path_condition = kcfg_explore.pretty_print(proof.path_constraints(node.id)) +857 failure_reasons[node.id] = reason +858 path_conditions[node.id] = path_condition +859 if counterexample_info: +860 model_subst = kcfg_explore.cterm_symbolic.get_model(node.cterm) +861 if type(model_subst) is Subst: +862 model: list[tuple[str, str]] = [] +863 for var, term in model_subst.to_dict().items(): +864 term_kast = KInner.from_dict(term) +865 term_pretty = kcfg_explore.pretty_print(term_kast) +866 model.append((var, term_pretty)) +867 models[node.id] = model +868 return APRFailureInfo( +869 failing_nodes=failing_nodes, +870 pending_nodes=pending_nodes, +871 path_conditions=path_conditions, +872 failure_reasons=failure_reasons, +873 models=models, +874 )
-880 +875
[docs] -881 def print(self) -> list[str]: -882 res_lines: list[str] = [] -883 -884 num_pending = len(self.pending_nodes) -885 num_failing = len(self.failing_nodes) -886 res_lines.append( -887 f'{num_pending + num_failing} Failure nodes. ({num_pending} pending and {num_failing} failing)' -888 ) -889 -890 if num_pending > 0: -891 res_lines.append('') -892 res_lines.append(f'Pending nodes: {sorted(self.pending_nodes)}') -893 -894 if num_failing > 0: -895 res_lines.append('') -896 res_lines.append('Failing nodes:') -897 for node_id in self.failing_nodes: -898 reason = self.failure_reasons[node_id] -899 path_condition = self.path_conditions[node_id] -900 res_lines.append('') -901 res_lines.append(f' Node id: {str(node_id)}') -902 -903 res_lines.append(' Failure reason:') -904 res_lines += [f' {line}' for line in reason.split('\n')] -905 -906 res_lines.append(' Path condition:') -907 res_lines += [f' {path_condition}'] -908 -909 if node_id in self.models: -910 res_lines.append(' Model:') -911 for var, term in self.models[node_id]: -912 res_lines.append(f' {var} = {term}') -913 else: -914 res_lines.append(' Failed to generate a model.') -915 -916 res_lines.append('') -917 res_lines.append('Join the Runtime Verification Discord server for support: https://discord.gg/CurfmXNtbN') -918 return res_lines
+876 def print(self) -> list[str]: +877 res_lines: list[str] = [] +878 +879 num_pending = len(self.pending_nodes) +880 num_failing = len(self.failing_nodes) +881 res_lines.append( +882 f'{num_pending + num_failing} Failure nodes. ({num_pending} pending and {num_failing} failing)' +883 ) +884 +885 if num_pending > 0: +886 res_lines.append('') +887 res_lines.append(f'Pending nodes: {sorted(self.pending_nodes)}') +888 +889 if num_failing > 0: +890 res_lines.append('') +891 res_lines.append('Failing nodes:') +892 for node_id in self.failing_nodes: +893 reason = self.failure_reasons[node_id] +894 path_condition = self.path_conditions[node_id] +895 res_lines.append('') +896 res_lines.append(f' Node id: {str(node_id)}') +897 +898 res_lines.append(' Failure reason:') +899 res_lines += [f' {line}' for line in reason.split('\n')] +900 +901 res_lines.append(' Path condition:') +902 res_lines += [f' {path_condition}'] +903 +904 if node_id in self.models: +905 res_lines.append(' Model:') +906 for var, term in self.models[node_id]: +907 res_lines.append(f' {var} = {term}') +908 else: +909 res_lines.append(' Failed to generate a model.') +910 +911 res_lines.append('') +912 res_lines.append('Join the Runtime Verification Discord server for support: https://discord.gg/CurfmXNtbN') +913 return res_lines diff --git a/_modules/pyk/proof/show.html b/_modules/pyk/proof/show.html index 82881dfa6..5701518fe 100644 --- a/_modules/pyk/proof/show.html +++ b/_modules/pyk/proof/show.html @@ -4,10 +4,10 @@ - pyk.proof.show — pyk 0.1.776 documentation + pyk.proof.show — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/proof/tui.html b/_modules/pyk/proof/tui.html index d177d402a..9eba21c5b 100644 --- a/_modules/pyk/proof/tui.html +++ b/_modules/pyk/proof/tui.html @@ -4,10 +4,10 @@ - pyk.proof.tui — pyk 0.1.776 documentation + pyk.proof.tui — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/testing/plugin.html b/_modules/pyk/testing/plugin.html index c616f0906..95cc62ad2 100644 --- a/_modules/pyk/testing/plugin.html +++ b/_modules/pyk/testing/plugin.html @@ -4,10 +4,10 @@ - pyk.testing.plugin — pyk 0.1.776 documentation + pyk.testing.plugin — pyk 0.1.777 documentation - + diff --git a/_modules/pyk/utils.html b/_modules/pyk/utils.html index c7592a24a..ccc0a0dbf 100644 --- a/_modules/pyk/utils.html +++ b/_modules/pyk/utils.html @@ -4,10 +4,10 @@ - pyk.utils — pyk 0.1.776 documentation + pyk.utils — pyk 0.1.777 documentation - + diff --git a/_static/documentation_options.js b/_static/documentation_options.js index 14de1ec5b..b10ab5648 100644 --- a/_static/documentation_options.js +++ b/_static/documentation_options.js @@ -1,5 +1,5 @@ const DOCUMENTATION_OPTIONS = { - VERSION: '0.1.776', + VERSION: '0.1.777', LANGUAGE: 'en', COLLAPSE_INDEX: false, BUILDER: 'html', diff --git a/api/modules.html b/api/modules.html index 711bb73ee..06a1757d5 100644 --- a/api/modules.html +++ b/api/modules.html @@ -5,10 +5,10 @@ - pyk — pyk 0.1.776 documentation + pyk — pyk 0.1.777 documentation - + diff --git a/api/pyk.coverage.html b/api/pyk.coverage.html index 3c265ec16..b480775b2 100644 --- a/api/pyk.coverage.html +++ b/api/pyk.coverage.html @@ -5,10 +5,10 @@ - pyk.coverage module — pyk 0.1.776 documentation + pyk.coverage module — pyk 0.1.777 documentation - + diff --git a/api/pyk.cterm.cterm.html b/api/pyk.cterm.cterm.html index 622dc2ce5..4f84fd995 100644 --- a/api/pyk.cterm.cterm.html +++ b/api/pyk.cterm.cterm.html @@ -5,10 +5,10 @@ - pyk.cterm.cterm module — pyk 0.1.776 documentation + pyk.cterm.cterm module — pyk 0.1.777 documentation - + diff --git a/api/pyk.cterm.html b/api/pyk.cterm.html index 54b5d5db0..42c61ac2d 100644 --- a/api/pyk.cterm.html +++ b/api/pyk.cterm.html @@ -5,10 +5,10 @@ - pyk.cterm package — pyk 0.1.776 documentation + pyk.cterm package — pyk 0.1.777 documentation - + diff --git a/api/pyk.cterm.symbolic.html b/api/pyk.cterm.symbolic.html index b5eecdd78..9c9992bca 100644 --- a/api/pyk.cterm.symbolic.html +++ b/api/pyk.cterm.symbolic.html @@ -5,10 +5,10 @@ - pyk.cterm.symbolic module — pyk 0.1.776 documentation + pyk.cterm.symbolic module — pyk 0.1.777 documentation - + diff --git a/api/pyk.dequote.html b/api/pyk.dequote.html index b0480d219..35cb4a791 100644 --- a/api/pyk.dequote.html +++ b/api/pyk.dequote.html @@ -5,10 +5,10 @@ - pyk.dequote module — pyk 0.1.776 documentation + pyk.dequote module — pyk 0.1.777 documentation - + diff --git a/api/pyk.html b/api/pyk.html index 58b0e1fec..1388fb2a8 100644 --- a/api/pyk.html +++ b/api/pyk.html @@ -5,10 +5,10 @@ - pyk package — pyk 0.1.776 documentation + pyk package — pyk 0.1.777 documentation - + diff --git a/api/pyk.kast.att.html b/api/pyk.kast.att.html index 6112c4df0..e80e38b18 100644 --- a/api/pyk.kast.att.html +++ b/api/pyk.kast.att.html @@ -5,10 +5,10 @@ - pyk.kast.att module — pyk 0.1.776 documentation + pyk.kast.att module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kast.html b/api/pyk.kast.html index d1a3681ee..74dba2f90 100644 --- a/api/pyk.kast.html +++ b/api/pyk.kast.html @@ -5,10 +5,10 @@ - pyk.kast package — pyk 0.1.776 documentation + pyk.kast package — pyk 0.1.777 documentation - + diff --git a/api/pyk.kast.inner.html b/api/pyk.kast.inner.html index 0956cfe61..26c0f6799 100644 --- a/api/pyk.kast.inner.html +++ b/api/pyk.kast.inner.html @@ -5,10 +5,10 @@ - pyk.kast.inner module — pyk 0.1.776 documentation + pyk.kast.inner module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kast.kast.html b/api/pyk.kast.kast.html index 9f6c8f4cf..16baa4aa8 100644 --- a/api/pyk.kast.kast.html +++ b/api/pyk.kast.kast.html @@ -5,10 +5,10 @@ - pyk.kast.kast module — pyk 0.1.776 documentation + pyk.kast.kast module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kast.manip.html b/api/pyk.kast.manip.html index 2185ec6fb..9fd08b21a 100644 --- a/api/pyk.kast.manip.html +++ b/api/pyk.kast.manip.html @@ -5,10 +5,10 @@ - pyk.kast.manip module — pyk 0.1.776 documentation + pyk.kast.manip module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kast.markdown.html b/api/pyk.kast.markdown.html index 48ac4c8ca..9b78909e8 100644 --- a/api/pyk.kast.markdown.html +++ b/api/pyk.kast.markdown.html @@ -5,10 +5,10 @@ - pyk.kast.markdown module — pyk 0.1.776 documentation + pyk.kast.markdown module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kast.outer.html b/api/pyk.kast.outer.html index 3ad303133..0cace5581 100644 --- a/api/pyk.kast.outer.html +++ b/api/pyk.kast.outer.html @@ -5,10 +5,10 @@ - pyk.kast.outer module — pyk 0.1.776 documentation + pyk.kast.outer module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kast.outer_lexer.html b/api/pyk.kast.outer_lexer.html index bdcfc1463..6656bf5ac 100644 --- a/api/pyk.kast.outer_lexer.html +++ b/api/pyk.kast.outer_lexer.html @@ -5,10 +5,10 @@ - pyk.kast.outer_lexer module — pyk 0.1.776 documentation + pyk.kast.outer_lexer module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kast.outer_parser.html b/api/pyk.kast.outer_parser.html index cc01e2a17..96fa7ea18 100644 --- a/api/pyk.kast.outer_parser.html +++ b/api/pyk.kast.outer_parser.html @@ -5,10 +5,10 @@ - pyk.kast.outer_parser module — pyk 0.1.776 documentation + pyk.kast.outer_parser module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kast.outer_syntax.html b/api/pyk.kast.outer_syntax.html index 705cf1c7a..405fee61d 100644 --- a/api/pyk.kast.outer_syntax.html +++ b/api/pyk.kast.outer_syntax.html @@ -5,10 +5,10 @@ - pyk.kast.outer_syntax module — pyk 0.1.776 documentation + pyk.kast.outer_syntax module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kast.pretty.html b/api/pyk.kast.pretty.html index 246ee0825..ac721eb64 100644 --- a/api/pyk.kast.pretty.html +++ b/api/pyk.kast.pretty.html @@ -5,10 +5,10 @@ - pyk.kast.pretty module — pyk 0.1.776 documentation + pyk.kast.pretty module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kbuild.config.html b/api/pyk.kbuild.config.html index b712a71e1..442dd5f89 100644 --- a/api/pyk.kbuild.config.html +++ b/api/pyk.kbuild.config.html @@ -5,10 +5,10 @@ - pyk.kbuild.config module — pyk 0.1.776 documentation + pyk.kbuild.config module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kbuild.html b/api/pyk.kbuild.html index 6fe5c5b48..a1b93a6a2 100644 --- a/api/pyk.kbuild.html +++ b/api/pyk.kbuild.html @@ -5,10 +5,10 @@ - pyk.kbuild package — pyk 0.1.776 documentation + pyk.kbuild package — pyk 0.1.777 documentation - + diff --git a/api/pyk.kbuild.kbuild.html b/api/pyk.kbuild.kbuild.html index 2335ea593..b0ca04e42 100644 --- a/api/pyk.kbuild.kbuild.html +++ b/api/pyk.kbuild.kbuild.html @@ -5,10 +5,10 @@ - pyk.kbuild.kbuild module — pyk 0.1.776 documentation + pyk.kbuild.kbuild module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kbuild.project.html b/api/pyk.kbuild.project.html index 22344e163..0d90462cf 100644 --- a/api/pyk.kbuild.project.html +++ b/api/pyk.kbuild.project.html @@ -5,10 +5,10 @@ - pyk.kbuild.project module — pyk 0.1.776 documentation + pyk.kbuild.project module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kbuild.utils.html b/api/pyk.kbuild.utils.html index 3c7761ed6..40575abc5 100644 --- a/api/pyk.kbuild.utils.html +++ b/api/pyk.kbuild.utils.html @@ -5,10 +5,10 @@ - pyk.kbuild.utils module — pyk 0.1.776 documentation + pyk.kbuild.utils module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kcfg.exploration.html b/api/pyk.kcfg.exploration.html index d936e414d..f73b96a1b 100644 --- a/api/pyk.kcfg.exploration.html +++ b/api/pyk.kcfg.exploration.html @@ -5,10 +5,10 @@ - pyk.kcfg.exploration module — pyk 0.1.776 documentation + pyk.kcfg.exploration module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kcfg.explore.html b/api/pyk.kcfg.explore.html index 08c242432..4eb4bb82d 100644 --- a/api/pyk.kcfg.explore.html +++ b/api/pyk.kcfg.explore.html @@ -5,10 +5,10 @@ - pyk.kcfg.explore module — pyk 0.1.776 documentation + pyk.kcfg.explore module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kcfg.html b/api/pyk.kcfg.html index aa9adea62..e13deac93 100644 --- a/api/pyk.kcfg.html +++ b/api/pyk.kcfg.html @@ -5,10 +5,10 @@ - pyk.kcfg package — pyk 0.1.776 documentation + pyk.kcfg package — pyk 0.1.777 documentation - + diff --git a/api/pyk.kcfg.kcfg.html b/api/pyk.kcfg.kcfg.html index 91d43f886..609ff5689 100644 --- a/api/pyk.kcfg.kcfg.html +++ b/api/pyk.kcfg.kcfg.html @@ -5,10 +5,10 @@ - pyk.kcfg.kcfg module — pyk 0.1.776 documentation + pyk.kcfg.kcfg module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kcfg.semantics.html b/api/pyk.kcfg.semantics.html index d9a0ac419..4b748cc30 100644 --- a/api/pyk.kcfg.semantics.html +++ b/api/pyk.kcfg.semantics.html @@ -5,10 +5,10 @@ - pyk.kcfg.semantics module — pyk 0.1.776 documentation + pyk.kcfg.semantics module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kcfg.show.html b/api/pyk.kcfg.show.html index f605f5c6e..ddf3583f4 100644 --- a/api/pyk.kcfg.show.html +++ b/api/pyk.kcfg.show.html @@ -5,10 +5,10 @@ - pyk.kcfg.show module — pyk 0.1.776 documentation + pyk.kcfg.show module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kcfg.store.html b/api/pyk.kcfg.store.html index c88362c48..842da8504 100644 --- a/api/pyk.kcfg.store.html +++ b/api/pyk.kcfg.store.html @@ -5,10 +5,10 @@ - pyk.kcfg.store module — pyk 0.1.776 documentation + pyk.kcfg.store module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kcfg.tui.html b/api/pyk.kcfg.tui.html index 2e7bf4fce..f8265fa2a 100644 --- a/api/pyk.kcfg.tui.html +++ b/api/pyk.kcfg.tui.html @@ -5,10 +5,10 @@ - pyk.kcfg.tui module — pyk 0.1.776 documentation + pyk.kcfg.tui module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kcovr.html b/api/pyk.kcovr.html index 7a211ea27..b8dc498d5 100644 --- a/api/pyk.kcovr.html +++ b/api/pyk.kcovr.html @@ -5,10 +5,10 @@ - pyk.kcovr module — pyk 0.1.776 documentation + pyk.kcovr module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kdist.api.html b/api/pyk.kdist.api.html index bc17a22c6..fd55007e7 100644 --- a/api/pyk.kdist.api.html +++ b/api/pyk.kdist.api.html @@ -5,10 +5,10 @@ - pyk.kdist.api module — pyk 0.1.776 documentation + pyk.kdist.api module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kdist.html b/api/pyk.kdist.html index d02256fe2..8ba6deeb0 100644 --- a/api/pyk.kdist.html +++ b/api/pyk.kdist.html @@ -5,10 +5,10 @@ - pyk.kdist package — pyk 0.1.776 documentation + pyk.kdist package — pyk 0.1.777 documentation - + diff --git a/api/pyk.kdist.utils.html b/api/pyk.kdist.utils.html index 945145add..685932750 100644 --- a/api/pyk.kdist.utils.html +++ b/api/pyk.kdist.utils.html @@ -5,10 +5,10 @@ - pyk.kdist.utils module — pyk 0.1.776 documentation + pyk.kdist.utils module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kllvm.ast.html b/api/pyk.kllvm.ast.html index 663c53113..363f3d3bc 100644 --- a/api/pyk.kllvm.ast.html +++ b/api/pyk.kllvm.ast.html @@ -5,10 +5,10 @@ - pyk.kllvm.ast module — pyk 0.1.776 documentation + pyk.kllvm.ast module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kllvm.compiler.html b/api/pyk.kllvm.compiler.html index cf7028332..cf7d0b887 100644 --- a/api/pyk.kllvm.compiler.html +++ b/api/pyk.kllvm.compiler.html @@ -5,10 +5,10 @@ - pyk.kllvm.compiler module — pyk 0.1.776 documentation + pyk.kllvm.compiler module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kllvm.convert.html b/api/pyk.kllvm.convert.html index d82b91d85..d13682e5c 100644 --- a/api/pyk.kllvm.convert.html +++ b/api/pyk.kllvm.convert.html @@ -5,10 +5,10 @@ - pyk.kllvm.convert module — pyk 0.1.776 documentation + pyk.kllvm.convert module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kllvm.html b/api/pyk.kllvm.html index dc4bcbc85..206e2f439 100644 --- a/api/pyk.kllvm.html +++ b/api/pyk.kllvm.html @@ -5,10 +5,10 @@ - pyk.kllvm package — pyk 0.1.776 documentation + pyk.kllvm package — pyk 0.1.777 documentation - + diff --git a/api/pyk.kllvm.importer.html b/api/pyk.kllvm.importer.html index 51439fbc1..93fe6c8d3 100644 --- a/api/pyk.kllvm.importer.html +++ b/api/pyk.kllvm.importer.html @@ -5,10 +5,10 @@ - pyk.kllvm.importer module — pyk 0.1.776 documentation + pyk.kllvm.importer module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kllvm.load.html b/api/pyk.kllvm.load.html index 21b5666a6..ab7c507df 100644 --- a/api/pyk.kllvm.load.html +++ b/api/pyk.kllvm.load.html @@ -5,10 +5,10 @@ - pyk.kllvm.load module — pyk 0.1.776 documentation + pyk.kllvm.load module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kllvm.load_static.html b/api/pyk.kllvm.load_static.html index 36c0b30da..bb068e16d 100644 --- a/api/pyk.kllvm.load_static.html +++ b/api/pyk.kllvm.load_static.html @@ -5,10 +5,10 @@ - pyk.kllvm.load_static module — pyk 0.1.776 documentation + pyk.kllvm.load_static module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kllvm.parser.html b/api/pyk.kllvm.parser.html index 1d152c94a..115f5afbd 100644 --- a/api/pyk.kllvm.parser.html +++ b/api/pyk.kllvm.parser.html @@ -5,10 +5,10 @@ - pyk.kllvm.parser module — pyk 0.1.776 documentation + pyk.kllvm.parser module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kllvm.runtime.html b/api/pyk.kllvm.runtime.html index d1c17f092..c3eee5dc7 100644 --- a/api/pyk.kllvm.runtime.html +++ b/api/pyk.kllvm.runtime.html @@ -5,10 +5,10 @@ - pyk.kllvm.runtime module — pyk 0.1.776 documentation + pyk.kllvm.runtime module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kllvm.utils.html b/api/pyk.kllvm.utils.html index 71a654861..1a7080b7e 100644 --- a/api/pyk.kllvm.utils.html +++ b/api/pyk.kllvm.utils.html @@ -5,10 +5,10 @@ - pyk.kllvm.utils module — pyk 0.1.776 documentation + pyk.kllvm.utils module — pyk 0.1.777 documentation - + diff --git a/api/pyk.konvert.html b/api/pyk.konvert.html index d3c2b2c68..802f25926 100644 --- a/api/pyk.konvert.html +++ b/api/pyk.konvert.html @@ -5,10 +5,10 @@ - pyk.konvert package — pyk 0.1.776 documentation + pyk.konvert package — pyk 0.1.777 documentation - + diff --git a/api/pyk.kore.html b/api/pyk.kore.html index a891e638f..bd0d364f3 100644 --- a/api/pyk.kore.html +++ b/api/pyk.kore.html @@ -5,10 +5,10 @@ - pyk.kore package — pyk 0.1.776 documentation + pyk.kore package — pyk 0.1.777 documentation - + diff --git a/api/pyk.kore.kompiled.html b/api/pyk.kore.kompiled.html index 880ae68f5..e5e46fa91 100644 --- a/api/pyk.kore.kompiled.html +++ b/api/pyk.kore.kompiled.html @@ -5,10 +5,10 @@ - pyk.kore.kompiled module — pyk 0.1.776 documentation + pyk.kore.kompiled module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kore.lexer.html b/api/pyk.kore.lexer.html index aaef44e7a..577a36814 100644 --- a/api/pyk.kore.lexer.html +++ b/api/pyk.kore.lexer.html @@ -5,10 +5,10 @@ - pyk.kore.lexer module — pyk 0.1.776 documentation + pyk.kore.lexer module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kore.manip.html b/api/pyk.kore.manip.html index ae1aeaecc..4de075e48 100644 --- a/api/pyk.kore.manip.html +++ b/api/pyk.kore.manip.html @@ -5,10 +5,10 @@ - pyk.kore.manip module — pyk 0.1.776 documentation + pyk.kore.manip module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kore.match.html b/api/pyk.kore.match.html index 44ccbab36..01fcf9e5f 100644 --- a/api/pyk.kore.match.html +++ b/api/pyk.kore.match.html @@ -5,10 +5,10 @@ - pyk.kore.match module — pyk 0.1.776 documentation + pyk.kore.match module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kore.parser.html b/api/pyk.kore.parser.html index d2abc6481..5555ffc9d 100644 --- a/api/pyk.kore.parser.html +++ b/api/pyk.kore.parser.html @@ -5,10 +5,10 @@ - pyk.kore.parser module — pyk 0.1.776 documentation + pyk.kore.parser module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kore.pool.html b/api/pyk.kore.pool.html index b2c829599..58903a14a 100644 --- a/api/pyk.kore.pool.html +++ b/api/pyk.kore.pool.html @@ -5,10 +5,10 @@ - pyk.kore.pool module — pyk 0.1.776 documentation + pyk.kore.pool module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kore.prelude.html b/api/pyk.kore.prelude.html index 7343cf452..498ae6364 100644 --- a/api/pyk.kore.prelude.html +++ b/api/pyk.kore.prelude.html @@ -5,10 +5,10 @@ - pyk.kore.prelude module — pyk 0.1.776 documentation + pyk.kore.prelude module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kore.rpc.html b/api/pyk.kore.rpc.html index 70de5ef52..b973b06d7 100644 --- a/api/pyk.kore.rpc.html +++ b/api/pyk.kore.rpc.html @@ -5,10 +5,10 @@ - pyk.kore.rpc module — pyk 0.1.776 documentation + pyk.kore.rpc module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kore.syntax.html b/api/pyk.kore.syntax.html index 2cc905afc..20e112a89 100644 --- a/api/pyk.kore.syntax.html +++ b/api/pyk.kore.syntax.html @@ -5,10 +5,10 @@ - pyk.kore.syntax module — pyk 0.1.776 documentation + pyk.kore.syntax module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kore.tools.html b/api/pyk.kore.tools.html index f879485cc..a5c6b14f9 100644 --- a/api/pyk.kore.tools.html +++ b/api/pyk.kore.tools.html @@ -5,10 +5,10 @@ - pyk.kore.tools module — pyk 0.1.776 documentation + pyk.kore.tools module — pyk 0.1.777 documentation - + diff --git a/api/pyk.kore_exec_covr.html b/api/pyk.kore_exec_covr.html index 3ccdf223b..b8fb8d813 100644 --- a/api/pyk.kore_exec_covr.html +++ b/api/pyk.kore_exec_covr.html @@ -5,10 +5,10 @@ - pyk.kore_exec_covr package — pyk 0.1.776 documentation + pyk.kore_exec_covr package — pyk 0.1.777 documentation - + diff --git a/api/pyk.kore_exec_covr.kore_exec_covr.html b/api/pyk.kore_exec_covr.kore_exec_covr.html index adb54448c..8553c2b64 100644 --- a/api/pyk.kore_exec_covr.kore_exec_covr.html +++ b/api/pyk.kore_exec_covr.kore_exec_covr.html @@ -5,10 +5,10 @@ - pyk.kore_exec_covr.kore_exec_covr module — pyk 0.1.776 documentation + pyk.kore_exec_covr.kore_exec_covr module — pyk 0.1.777 documentation - + diff --git a/api/pyk.krepl.html b/api/pyk.krepl.html index 068038a8c..37ff26b54 100644 --- a/api/pyk.krepl.html +++ b/api/pyk.krepl.html @@ -5,10 +5,10 @@ - pyk.krepl package — pyk 0.1.776 documentation + pyk.krepl package — pyk 0.1.777 documentation - + diff --git a/api/pyk.krepl.repl.html b/api/pyk.krepl.repl.html index 37dc4a561..6f36c45f1 100644 --- a/api/pyk.krepl.repl.html +++ b/api/pyk.krepl.repl.html @@ -5,10 +5,10 @@ - pyk.krepl.repl module — pyk 0.1.776 documentation + pyk.krepl.repl module — pyk 0.1.777 documentation - + diff --git a/api/pyk.ktool.html b/api/pyk.ktool.html index cb8f40ef1..924b076ef 100644 --- a/api/pyk.ktool.html +++ b/api/pyk.ktool.html @@ -5,10 +5,10 @@ - pyk.ktool package — pyk 0.1.776 documentation + pyk.ktool package — pyk 0.1.777 documentation - + diff --git a/api/pyk.ktool.kompile.html b/api/pyk.ktool.kompile.html index 919039e71..737aea5fb 100644 --- a/api/pyk.ktool.kompile.html +++ b/api/pyk.ktool.kompile.html @@ -5,10 +5,10 @@ - pyk.ktool.kompile module — pyk 0.1.776 documentation + pyk.ktool.kompile module — pyk 0.1.777 documentation - + diff --git a/api/pyk.ktool.kprint.html b/api/pyk.ktool.kprint.html index 07f515344..9b2e582b0 100644 --- a/api/pyk.ktool.kprint.html +++ b/api/pyk.ktool.kprint.html @@ -5,10 +5,10 @@ - pyk.ktool.kprint module — pyk 0.1.776 documentation + pyk.ktool.kprint module — pyk 0.1.777 documentation - + diff --git a/api/pyk.ktool.kprove.html b/api/pyk.ktool.kprove.html index d3a47a011..a0eb1ebd4 100644 --- a/api/pyk.ktool.kprove.html +++ b/api/pyk.ktool.kprove.html @@ -5,10 +5,10 @@ - pyk.ktool.kprove module — pyk 0.1.776 documentation + pyk.ktool.kprove module — pyk 0.1.777 documentation - + diff --git a/api/pyk.ktool.krun.html b/api/pyk.ktool.krun.html index 7e12d7d85..e8a6eb8a6 100644 --- a/api/pyk.ktool.krun.html +++ b/api/pyk.ktool.krun.html @@ -5,10 +5,10 @@ - pyk.ktool.krun module — pyk 0.1.776 documentation + pyk.ktool.krun module — pyk 0.1.777 documentation - + diff --git a/api/pyk.prelude.bytes.html b/api/pyk.prelude.bytes.html index c4e7f4f70..a60708ebe 100644 --- a/api/pyk.prelude.bytes.html +++ b/api/pyk.prelude.bytes.html @@ -5,10 +5,10 @@ - pyk.prelude.bytes module — pyk 0.1.776 documentation + pyk.prelude.bytes module — pyk 0.1.777 documentation - + diff --git a/api/pyk.prelude.collections.html b/api/pyk.prelude.collections.html index b30e1e0d4..ef17f9818 100644 --- a/api/pyk.prelude.collections.html +++ b/api/pyk.prelude.collections.html @@ -5,10 +5,10 @@ - pyk.prelude.collections module — pyk 0.1.776 documentation + pyk.prelude.collections module — pyk 0.1.777 documentation - + diff --git a/api/pyk.prelude.html b/api/pyk.prelude.html index 8d52c8e57..2f24c841e 100644 --- a/api/pyk.prelude.html +++ b/api/pyk.prelude.html @@ -5,10 +5,10 @@ - pyk.prelude package — pyk 0.1.776 documentation + pyk.prelude package — pyk 0.1.777 documentation - + diff --git a/api/pyk.prelude.k.html b/api/pyk.prelude.k.html index 54effa34f..23868d614 100644 --- a/api/pyk.prelude.k.html +++ b/api/pyk.prelude.k.html @@ -5,10 +5,10 @@ - pyk.prelude.k module — pyk 0.1.776 documentation + pyk.prelude.k module — pyk 0.1.777 documentation - + diff --git a/api/pyk.prelude.kbool.html b/api/pyk.prelude.kbool.html index e7f927205..7af8d8251 100644 --- a/api/pyk.prelude.kbool.html +++ b/api/pyk.prelude.kbool.html @@ -5,10 +5,10 @@ - pyk.prelude.kbool module — pyk 0.1.776 documentation + pyk.prelude.kbool module — pyk 0.1.777 documentation - + diff --git a/api/pyk.prelude.kint.html b/api/pyk.prelude.kint.html index e6b3f7a57..1a05172f9 100644 --- a/api/pyk.prelude.kint.html +++ b/api/pyk.prelude.kint.html @@ -5,10 +5,10 @@ - pyk.prelude.kint module — pyk 0.1.776 documentation + pyk.prelude.kint module — pyk 0.1.777 documentation - + diff --git a/api/pyk.prelude.ml.html b/api/pyk.prelude.ml.html index 57ca56b2a..44cd2da72 100644 --- a/api/pyk.prelude.ml.html +++ b/api/pyk.prelude.ml.html @@ -5,10 +5,10 @@ - pyk.prelude.ml module — pyk 0.1.776 documentation + pyk.prelude.ml module — pyk 0.1.777 documentation - + diff --git a/api/pyk.prelude.string.html b/api/pyk.prelude.string.html index 838450283..9dad44e10 100644 --- a/api/pyk.prelude.string.html +++ b/api/pyk.prelude.string.html @@ -5,10 +5,10 @@ - pyk.prelude.string module — pyk 0.1.776 documentation + pyk.prelude.string module — pyk 0.1.777 documentation - + diff --git a/api/pyk.prelude.utils.html b/api/pyk.prelude.utils.html index bf744df66..b908d4bc6 100644 --- a/api/pyk.prelude.utils.html +++ b/api/pyk.prelude.utils.html @@ -5,10 +5,10 @@ - pyk.prelude.utils module — pyk 0.1.776 documentation + pyk.prelude.utils module — pyk 0.1.777 documentation - + diff --git a/api/pyk.proof.html b/api/pyk.proof.html index a03fb5cd3..2c95dfb77 100644 --- a/api/pyk.proof.html +++ b/api/pyk.proof.html @@ -5,10 +5,10 @@ - pyk.proof package — pyk 0.1.776 documentation + pyk.proof package — pyk 0.1.777 documentation - + diff --git a/api/pyk.proof.implies.html b/api/pyk.proof.implies.html index 8f7d6eda7..900999c9e 100644 --- a/api/pyk.proof.implies.html +++ b/api/pyk.proof.implies.html @@ -5,10 +5,10 @@ - pyk.proof.implies module — pyk 0.1.776 documentation + pyk.proof.implies module — pyk 0.1.777 documentation - + diff --git a/api/pyk.proof.parallel.html b/api/pyk.proof.parallel.html index d1d8a64f7..7a0c1f460 100644 --- a/api/pyk.proof.parallel.html +++ b/api/pyk.proof.parallel.html @@ -5,10 +5,10 @@ - pyk.proof.parallel module — pyk 0.1.776 documentation + pyk.proof.parallel module — pyk 0.1.777 documentation - + diff --git a/api/pyk.proof.proof.html b/api/pyk.proof.proof.html index 0494f352b..0ce24ca9f 100644 --- a/api/pyk.proof.proof.html +++ b/api/pyk.proof.proof.html @@ -5,10 +5,10 @@ - pyk.proof.proof module — pyk 0.1.776 documentation + pyk.proof.proof module — pyk 0.1.777 documentation - + diff --git a/api/pyk.proof.reachability.html b/api/pyk.proof.reachability.html index 2f6ec59a8..aadb2be6f 100644 --- a/api/pyk.proof.reachability.html +++ b/api/pyk.proof.reachability.html @@ -5,10 +5,10 @@ - pyk.proof.reachability module — pyk 0.1.776 documentation + pyk.proof.reachability module — pyk 0.1.777 documentation - + diff --git a/api/pyk.proof.show.html b/api/pyk.proof.show.html index 993e9b30a..8c48b59ba 100644 --- a/api/pyk.proof.show.html +++ b/api/pyk.proof.show.html @@ -5,10 +5,10 @@ - pyk.proof.show module — pyk 0.1.776 documentation + pyk.proof.show module — pyk 0.1.777 documentation - + diff --git a/api/pyk.proof.tui.html b/api/pyk.proof.tui.html index 316c87ccb..ddeb98bd0 100644 --- a/api/pyk.proof.tui.html +++ b/api/pyk.proof.tui.html @@ -5,10 +5,10 @@ - pyk.proof.tui module — pyk 0.1.776 documentation + pyk.proof.tui module — pyk 0.1.777 documentation - + diff --git a/api/pyk.testing.html b/api/pyk.testing.html index 29509483b..82e9d5c66 100644 --- a/api/pyk.testing.html +++ b/api/pyk.testing.html @@ -5,10 +5,10 @@ - pyk.testing package — pyk 0.1.776 documentation + pyk.testing package — pyk 0.1.777 documentation - + diff --git a/api/pyk.testing.plugin.html b/api/pyk.testing.plugin.html index 9cd49c541..5e1b98784 100644 --- a/api/pyk.testing.plugin.html +++ b/api/pyk.testing.plugin.html @@ -5,10 +5,10 @@ - pyk.testing.plugin module — pyk 0.1.776 documentation + pyk.testing.plugin module — pyk 0.1.777 documentation - + diff --git a/api/pyk.utils.html b/api/pyk.utils.html index 375ff039b..6de7b03b1 100644 --- a/api/pyk.utils.html +++ b/api/pyk.utils.html @@ -5,10 +5,10 @@ - pyk.utils module — pyk 0.1.776 documentation + pyk.utils module — pyk 0.1.777 documentation - + diff --git a/genindex.html b/genindex.html index 3bc344850..c9dbdb54c 100644 --- a/genindex.html +++ b/genindex.html @@ -4,10 +4,10 @@ - Index — pyk 0.1.776 documentation + Index — pyk 0.1.777 documentation - + diff --git a/index.html b/index.html index 0b0a6bf4f..223269d82 100644 --- a/index.html +++ b/index.html @@ -5,10 +5,10 @@ - Welcome to pyk’s documentation! — pyk 0.1.776 documentation + Welcome to pyk’s documentation! — pyk 0.1.777 documentation - + diff --git a/objects.inv b/objects.inv index 22ccd53a3..9a0e89399 100644 Binary files a/objects.inv and b/objects.inv differ diff --git a/py-modindex.html b/py-modindex.html index 4fe72dbd0..029d553f6 100644 --- a/py-modindex.html +++ b/py-modindex.html @@ -4,10 +4,10 @@ - Python Module Index — pyk 0.1.776 documentation + Python Module Index — pyk 0.1.777 documentation - + diff --git a/search.html b/search.html index 086e229c3..341995f8a 100644 --- a/search.html +++ b/search.html @@ -4,11 +4,11 @@ - Search — pyk 0.1.776 documentation + Search — pyk 0.1.777 documentation - +