Double Checking
- class SingleDoubleCheckStatistics(**data)
Bases:
BaseModelCreate a new model by parsing and validating input data from keyword arguments.
Raises [ValidationError][pydantic_core.ValidationError] if the input data cannot be validated to form a valid model.
self is explicitly positional-only to allow self as a field name.
- setup_clauses: list[str]
The setup clauses in JGEX format.
- aux_clauses_used: list[str]
The aux clauses that were used in this double check in JGEX format.
- aux_clauses_unused: list[str]
The aux clauses that were not used in this double check in JGEX format.
- alpha_mapping: dict[PredicateArgument, PredicateArgument]
The mapping from the original points to the alphabetized points.
- run_infos: RunInfos
The statistics for the solver run on the subproblem.
- double_check_setup: JGEXSetupData
The double-checked proof data of the subproblem in case it was solvable.
- double_check_proof: ProofData | None
The double-checked proof data of the subproblem in case it was solvable.
- model_config: ClassVar[ConfigDict] = {}
Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].
- class DoubleCheckStatistics(**data)
Bases:
BaseModelStatistics for a double check run.
Create a new model by parsing and validating input data from keyword arguments.
Raises [ValidationError][pydantic_core.ValidationError] if the input data cannot be validated to form a valid model.
self is explicitly positional-only to allow self as a field name.
- single_double_check_stats: list[SingleDoubleCheckStatistics]
Statistics for each aux double check.
- model_config: ClassVar[ConfigDict] = {}
Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].
- true_aux_clauses: list[str]
The double-checked true aux clauses.
- false_positive_aux_clauses: list[str]
The double-checked false positive aux clauses.
- final_proof: ProofData | None
The final double-checked proof data of the subproblem with all and only true aux clauses.
- training_data: TrainingDatapoint | None
The alphabetized i/o training data for the subproblem for each aux construction in it plus the proof to predict.
- do_double_check(subproblem, larger_problem, large_nc_problem, clauses_consequences, solver, aux_tag, rng)
- Return type:
- points_requirements_graph_from_jgex_clauses(aux_clauses)