Documentation
Source code API
GeometricSolver
GeometricSolver.animate()
GeometricSolver.draw_figure()
GeometricSolver.proof()
GeometricSolver.run()
GeometricSolver.write_all_outputs()
GeometricSolverBuilder
GeometricSolverBuilder.build()
GeometricSolverBuilder.with_deductive_agent()
GeometricSolverBuilder.with_deductors()
GeometricSolverBuilder.with_rule_matcher()
GeometricSolverBuilder.with_rules()
GeometricSolverBuilder.with_rules_from_file()
make_agent()
DeductiveAgent
DDARNStats
DDARN
DeductionType
CachedRuleDeduction
ARPremiseConstruction
CachedARDeduction
CachedNumericalCheckDeduction
CachedReflexivityDeduction
DeductionProvider
FollowDeductionsStats
FollowDeductions
DoubleCheckError
NamedFunction
HumanAgent
ProofAnimation
ProofAnimation.animate()
html_animation()
PointArtists
ArtistInAnimation
init_point_name_to_artist()
ClauseArtists
init_clauses_to_draw()
GoalArtists
init_goals_to_draw()
JustificationArtists
JustificationToDraw
init_justifications_to_draw()
draw_generic_justification()
ProofAnimationParts
TextAnimation
ARReason
ARReason.ANGLE_CHASING
ARReason.RATIO_CHASING
ARCoefficient
ARPremise
ARDeduction
Deductor
add_to_deductors()
check_from_deductors()
justify_from_deductors()
draw_ar_application()
draw_deps_predicates()
init_figure()
draw_figure()
draw_point()
ArtistKwargs
draw_circle_symbol()
draw_circle()
draw_triangle()
draw_segment()
draw_arrow()
draw_complete_arrow()
draw_jgex_problem_clauses()
draw_jgex_constructions()
random()
draw_predicate()
draw_perp_rectangle()
draw_line_symbol()
draw_line()
draw_free_perpendicular_symbol()
draw_rule_application()
circumcenter_of_triangle()
DrawTheme
fill_missing()
apply_commands_effects_on_elements()
commands_to_newclid_assumptions()
elements_to_newclid_assumptions()
relationships_to_newclid_assumptions()
RelationShipType
ParaRelationship
OrthoRelationship
BisectorLineRelationship
BisectorPointRelationship
TangentRelationship
GeogebraProblemBuilder
load_ggb_file()
GGBSetup
read_commands()
GGBReadCommandType
GGBLineCommand
GGBParaCommand
GGBOrthogonalLineCommand
GGBIntersectCommand
GGBCircleCommand
GGBCircumcircleCommand
GGBCompassCommand
GGBAddPointOnObjectCommand
GGBCenterCommand
GGBMidpointCommand
GGBAngularBisectorLinesCommand
GGBAngularBisectorPointsCommand
GGBTangentOnCircleCommand
GGBTangentOutsideCircleCommand
GGBXMLCommandType
GGBXMLCommandComponents
GGBElementType
GGBPoint
GGBLine
GGBConic
read_elements()
relationships_from_commands()
HeuristicName
HeuristicName.LINE_INTERSECTIONS
HeuristicName.CENTERS
HeuristicName.ANGLE_VERTICES
HeuristicName.MIDPOINT
HeuristicName.EQDISTANCE
HeuristicName.FOOT
HeuristicName.REFLECT_ON_CENTER
HeuristicName.THREE_CIRCUMCIRCLES_FOR_EQANGLE_GOAL
Heuristic
Heuristic.new_clauses()
HeuristicSetup
HeuristicSetup.model_config
HeuristicSetup.points
HeuristicSetup.free_points
HeuristicSetup.lines
HeuristicSetup.circles
HeuristicSetup.angles
HeuristicSetup.goals
get_available_from_alphabet()
AngleVerticesHeuristicConfig
AngleVerticesHeuristic
apply_complete_the_picture_heuristics()
apply_heuristics_on_nc_problem()
build_nc_problem_from_jgex_problem()
CentersOfCyclicHeuristicConfig
CentersOfCyclicHeuristic
ThreeCircumcirclesForEqangleGoalHeuristicConfig
ThreeCircumcirclesForEqangleGoalHeuristic
FootHeuristicConfig
FootHeuristic
LineHeuristic
CircleHeuristic
AngleHeuristic
read_geometric_objects_from_predicate_constructions()
heuristic_from_name()
config_from_name()
heuristic_from_config()
LineIntersectionsHeuristicConfig
LineIntersectionsHeuristic
MidpointHeuristicConfig
MidpointHeuristic
ReflectOnCenterHeuristicConfig
ReflectOnCenterHeuristic
TransferDistancesHeuristicConfig
TransferDistancesHeuristic
ang_of()
ang_between()
JGEXConstruction
rename_jgex_construction()
is_numerical_argument()
JGEXClause
order_clauses_by_points_construction_order()
SketchConstruction
SketchCall
v()
JGEXDefinition
mapping_from_construction()
input_points_of_clause()
ensure_not_too_close_numerical()
ensure_not_too_far_numerical()
JGEXConstructionError
PointTooCloseError
PointTooFarError
InvalidIntersectError
JGEXFormulation
jgex_formulation_from_txt_file()
alphabetize()
LENGTH_UNIT
JGEXPoint
JGEXGeometry
JGEXLine
JGEXCircle
perpendicular_bisector()
solve_quad()
intersect()
circle_circle_intersection()
line_circle_intersection()
line_line_intersection()
reduce_intersection()
PredicateConstructionInSetup
JGEXClauseInProof
JGEXSetupData
jgex_clauses_to_setup_data()
JGEXProblemBuilder
sketch()
sketch_function_name()
sketch_aline()
sketch_aline0()
sketch_acircle()
sketch_amirror()
sketch_bisect()
sketch_exbisect()
sketch_bline()
sketch_dia()
sketch_tangent()
sketch_circle()
sketch_cc_tangent()
sketch_e5128()
random_rfss()
head_from()
sketch_eq_quadrangle()
sketch_iso_trapezoid()
sketch_eqangle2()
sketch_eqangle3()
sketch_eqdia_quadrangle()
random_points()
sketch_free()
sketch_isos()
sketch_line()
sketch_cyclic()
sketch_midp()
sketch_pentagon()
sketch_pline()
sketch_pmirror()
sketch_quadrangle()
sketch_r_trapezoid()
sketch_r_triangle()
sketch_rectangle()
sketch_reflect()
sketch_risos()
sketch_rotaten90()
sketch_rotatep90()
sketch_s_angle()
sketch_aconst()
sketch_segment()
sketch_shift()
sketch_square()
sketch_isquare()
sketch_tline()
sketch_trapezoid()
sketch_triangle()
sketch_triangle12()
sketch_trisect()
sketch_trisegment()
sketch_ieq_triangle()
sketch_incenter2()
sketch_excenter2()
sketch_centroid()
sketch_ninepoints()
sketch_2l1c()
sketch_3peq()
sketch_isosvertex()
sketch_eqratio()
sketch_rconst()
sketch_eqratio6()
sketch_lconst()
sketch_rconst2()
sketch_between()
sketch_between_bound()
sketch_iso_trapezoid2()
sketch_acute_triangle()
sketch_cc_itangent()
sketch_simtri()
sketch_simtrir()
sketch_contri()
sketch_contrir()
sketch_test_r20()
sketch_test_r25()
sketch_l2const()
sketch_r2const()
build_newclid_problem()
add_clause_to_problem()
JGEXClauseConsequences
rename_points_in_clause_consequences()
JGEXConstructionConsequences
rename_points_in_construction_consequences()
Assumption
NumericalCheck
Reflexivity
DirectConsequence
justify_dependency()
justify_predicate()
PredicatesGraph
close_enough()
nearly_zero()
sign()
same_clock()
clock()
PointNum
line_num_from_points()
LineNum
circle_num_from_points_around()
circle_num_from_center_and_point()
CircleNum
predicate_class_from_type()
predicate_from_construction()
Circumcenter
Coll
NColl
Cong
angle_between_4_points()
ConstantAngle
ACompute
aconst_from_acompute()
ConstantLength
LCompute
lconst_from_lcompute()
ConstantRatio
RCompute
rconst_from_rcompute()
Cyclic
Diff
EqAngle
EqRatio
AngleEquation
LengthEquation
MidPoint
ObtuseAngle
Para
NPara
Perp
NPerp
PythagoreanPremises
PythagoreanConclusions
SameClock
SameSide
NSameSide
SquaredConstantLength
SquaredConstantRatio
ContriClock
ContriReflect
two_triangles()
SimtriClock
SimtriReflect
CompetitionIds
Competition
ProblemFormulation
Problem
efficient_version()
PerpStatement
PerpPredicate
ParaStatement
ParaPredicate
EqangleStatement
EqanglePredicate
EqratioStatement
EqratioPredicate
CongStatement
CongPredicate
MidptStatement
MidptPredicate
TriangleStatement
TrianglePredicate
CollStatement
CollPredicate
CircleStatement
CirclePredicate
CyclicStatement
CyclicPredicate
generate_permutations()
cyclic_perms()
coll_perms()
circle_perms()
triangle_perms()
normalize_triangle()
normalize_midpt()
midpt_perms()
normalize_cong()
cong_perms()
normalize_eqratio()
eqratio_perms()
normalize_eqangle()
eqangle_perms()
normalize_para()
para_perms()
normalize_perp()
perp_perms()
normalize_coll()
normalize_circle()
normalize_cyclic()
get_representative_of_equivalence_class()
RuleMatcher
MappingMatcher
TheoremMapper
CCMapper
FilterMapper
predictates_by_type_name_from_hypergraph()
iterate_mapping_with_complementary_assignments()
PartialMapping
iterate_mappings()
generate_permutations_as_dicts()
CircleSymbol
CirclesRegistry
CircleMerge
LineSymbol
LinesRegistry
LineMerge
SymbolMergeHistory
representent_of()
merge_symbols()
Point
PointsRegisty
SymbolsRegistry
DEFAULT_RULES
ALL_RULES
DEACTIVATED_RULES
TRIAGE_NO_RULE_NEEDED
TRIAGE_LEAVE_RULE_OUT
ProblemBuilder
ProblemBuilder.build()
PythonDefault
PythonDefault.default_rule_matcher()
PythonDefault.default_deductors()
PythonDefault.default_deductive_agent()
PythonDefault.callback()
APIDefault
APIDefault.default_rule_matcher()
APIDefault.default_deductors()
APIDefault.default_deductive_agent()
APIDefault.callback()
NewclidOptions
NewclidOptions.output_dir
NewclidOptions.saturate
NewclidOptions.agent
NewclidOptions.seed
NewclidOptions.log_level
NewclidOptions.model_config
parse_cli_args()
make_cli_parser()
LogLevel
LogLevel.DEBUG
LogLevel.INFO
LogLevel.WARNING
LogLevel.ERROR
new_problem_from_llm_aux_output()
problem_to_llm_input()
problem_to_llm_input_without_predicates()
TrainingDatapoint
TrainingDatapoint.aux_io
TrainingDatapoint.proof_output
TrainingDatapoint.from_proof_data()
TrainingDatapoint.from_proof_data_aux_combinations()
TrainingDatapoint.model_config
AuxTrainingDatapoint
AuxTrainingDatapoint.input
AuxTrainingDatapoint.aux_output
AuxTrainingDatapoint.from_setup_data()
AuxTrainingDatapoint.from_setup_data_aux_combinations()
AuxTrainingDatapoint.model_config
PredicateArgument
PredicateConstruction
PredicateConstruction.string
PredicateConstruction.predicate_type
PredicateConstruction.args
PredicateConstruction.canonicalize()
PredicateConstruction.from_tuple()
PredicateConstruction.from_str()
PredicateConstruction.from_predicate_type_and_args()
PredicateConstruction.model_config
predicate_from_str()
predicate_to_construction()
predicate_points()
rename_predicate_construction()
ProblemSetup
ProblemSetup.name
ProblemSetup.points
ProblemSetup.assumptions
ProblemSetup.goals
ProblemSetup.check_points_are_unique()
ProblemSetup.check_assumptions_and_goals_refer_to_existing_points()
ProblemSetup.with_new()
ProblemSetup.pretty_str()
ProblemSetup.model_config
nc_problem_is_valid()
rename_points_in_nc_problem()
filter_points_from_nc_problem()
PredicateInProof
PredicateInProof.id
PredicateInProof.predicate
PredicateInProof.model_config
ProofStep
ProofStep.proven_predicate
ProofStep.justification
ProofStep.applied_on_predicates
ProofStep.model_config
ProofData
ProofData.proof_length
ProofData.proof_rules_length
ProofData.points
ProofData.proven_goals
ProofData.unproven_goals
ProofData.construction_assumptions
ProofData.model_config
ProofData.numerical_checks
ProofData.trivial_predicates
ProofData.proof_steps
ProofData.set_proof_length()
proof_data_from_state()
proof_justifications_to_proof_data()
goals_justifications()
ProofBuildError
ProofState
ProofState.match_theorem()
ProofState.apply()
ProofState.check()
ProofState.check_numerical()
ProofState.justify()
ProofState.check_goals()
ProofSections
ProofSections.points
ProofSections.assumptions
ProofSections.numerical_checks
ProofSections.trivial_predicates
ProofSections.proven_goals
ProofSections.unproven_goals
ProofSections.proof_steps
ProofSections.appendix_ar
ProofSections.model_config
write_proof()
write_proof_sections()
CarryOver
CarryOver.update()
setup_rng()
RuleConstruction
RuleConstruction.name
RuleConstruction.variables
RuleConstruction.model_config
RuleApplication
RuleApplication.predicate
RuleApplication.rule
RuleApplication.premises
RuleApplication.dependency_type
RuleApplication.canonicalize()
RuleApplication.model_config
Rule
Rule.model_config
Rule.id
Rule.description
Rule.premises_txt
Rule.conclusions_txt
Rule.allow_point_repetition
Rule.premises
Rule.conclusions
Rule.fullname
Rule.variables
rules_from_file()
rules_from_txt()
RunInfos
RunInfos.runtime
RunInfos.success
RunInfos.steps
RunInfos.success_per_goal
RunInfos.agent_stats
RunInfos.model_config
run_loop()
InfQuotientError
get_quotient()
atomize()
str_to_fraction()
fraction_to_len()
fraction_to_ratio()
fraction_to_angle()
reshape()
add_edge()
run_static_server()
boring_predicate()
point_construction_tuple()
points_by_construction_order()
pretty_basemodel_diff()
pretty_basemodel_list_diff()
pull_to_server()
discriminator_from_name()
AuxFromHEPointsDeps
AuxFromNewclidTraceback
ConstructionDefinition
ConstructionDefinition.in_args
ConstructionDefinition.out_args
ConstructionDefinition.n_required_points
ConstructionDefinition.model_config
load_constructions()
SubproblemSummaryStats
SubproblemSummaryStats.skipped_not_enough_rules_applications_subproblems
SubproblemSummaryStats.unhandled_failure_to_build_subproblem_count
SubproblemSummaryStats.skipped_blacklisted_aux_setup_pairs
SubproblemSummaryStats.model_config
FailedClauseAttempt
FailedClauseAttempt.problem
FailedClauseAttempt.clause
FailedClauseAttempt.attempt_time
FailedClauseAttempt.model_config
DiagramGenerationMetadata
DiagramGenerationMetadata.run_uuid
DiagramGenerationMetadata.diagram_uuid
DiagramGenerationMetadata.is_predefined_diagram
DiagramGenerationMetadata.config
DiagramGenerationMetadata.diagram_construction_time_sec
DiagramGenerationMetadata.diagram_succeeded
DiagramGenerationMetadata.saturation_succeeded
DiagramGenerationMetadata.saturation_time_sec
DiagramGenerationMetadata.agent_saturation_stats
DiagramGenerationMetadata.failed_clause_attempts
DiagramGenerationMetadata.created_at
DiagramGenerationMetadata.subproblem_summary_stats
DiagramGenerationMetadata.model_config
Diagram
Diagram.solver
Diagram.problem
Diagram.dependencies
Diagram.setup_graph
Diagram.jgex_problem
Diagram.nc_problem
Diagram.jgex_clauses_consequences
build_diagram()
setupgraph()
SingleDoubleCheckStatistics
SingleDoubleCheckStatistics.setup_clauses
SingleDoubleCheckStatistics.aux_clauses_used
SingleDoubleCheckStatistics.aux_clauses_unused
SingleDoubleCheckStatistics.alpha_mapping
SingleDoubleCheckStatistics.run_infos
SingleDoubleCheckStatistics.double_check_setup
SingleDoubleCheckStatistics.double_check_proof
SingleDoubleCheckStatistics.model_config
DoubleCheckStatistics
DoubleCheckStatistics.single_double_check_stats
DoubleCheckStatistics.model_config
DoubleCheckStatistics.true_aux_clauses
DoubleCheckStatistics.false_positive_aux_clauses
DoubleCheckStatistics.final_proof
DoubleCheckStatistics.training_data
do_double_check()
points_requirements_graph_from_jgex_clauses()
SubProblemDatapoint
SubProblemDatapoint.double_check_statistics
SubProblemDatapoint.subproblem_str
SubProblemDatapoint.alphabetized_subproblem_str
SubProblemDatapoint.sub_problem_proof
SubProblemDatapoint.level_predicate_count
SubProblemDatapoint.solution_natural_language
SubProblemDatapoint.model_config
SubProblemDatapoint.larger_problem
SubProblemDatapoint.larger_nc_problem
SubProblemDatapoint.has_double_checked_aux_construction
generate_subproblems_datapoints()
extract_subproblems_and_their_dependencies()
IntersectCases
IntersectCases.INTERSECT
IntersectCases.OTHER
DiagramGenerationConfig
DiagramGenerationConfig.min_pts
DiagramGenerationConfig.max_pts
DiagramGenerationConfig.initial_jgex_problem
DiagramGenerationConfig.output_gcs_file
DiagramGenerationConfig.emit_only_double_checked_aux_subproblems
DiagramGenerationConfig.aux_discriminator
DiagramGenerationConfig.debug
DiagramGenerationConfig.debug_problem
DiagramGenerationConfig.double_check_probability
DiagramGenerationConfig.skip_aux_setup_pairs_previous_false_positive
DiagramGenerationConfig.min_rules_applied
DiagramGenerationConfig.random_seed
DiagramGenerationConfig.attempts_per_diagram_build
DiagramGenerationConfig.max_check_per_predicate
DiagramGenerationConfig.construction_counter_reporting_rate
DiagramGenerationConfig.attempts_per_clause
DiagramGenerationConfig.aux_tag
DiagramGenerationConfig.pmf_additional_free_points_sweep
DiagramGenerationConfig.model_config
DiagramGenerationConfig.pmf_intersect_vs_other_sweep
DiagramGenerationConfig.pmf_num_intersecting_to_sample_sweep
DiagramGenerationConfig.run_uuid
DiagramGenerationConfig.timeout
DiagramGenerationConfig.n_workers
DiagramGenerationConfig.jsonl_dump_file
DiagramGenerationConfig.log_level
DiagramGenerationConfig.validate_pmf_sweep()
DiagramGenerationConfig.validate_output_gcs_file()
DiagramGenerationConfig.validate_min_max_pts()
SweepSelection
SweepSelection.model_config
SweepSelection.additional_free_points_sweep_selection
SweepSelection.intersect_vs_other_sweep_selection
SweepSelection.num_intersecting_to_sample_sweep_selection
sample_sweep_parameters()
Datapoint
Datapoint.subproblem
Datapoint.generation_metadata
Datapoint.model_config
run_data_generation_loop()
hydra_to_pydantic_generation_config()
read_datapoints_from_file()
sample_from_pmf()
sample_order_from_pmf()
combinations_in_random_order()
SolverInterface
SolverInterface.solve_problem()
SolverError
NewclidSolver
NewclidSolver.solve_problem()
StubJGEXSolver
StubJGEXSolver.with_outputs_for_problem_clauses()
StubJGEXSolver.solve_problem()
Definitions of free points in a specific formation or figure.