From 186f16788562bf4d6064e1fc48ec2179c5d34bb6 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 9 May 2018 20:34:17 -0500 Subject: [PATCH] update doc --- msat_test/index.html | 2 + odoc.css | 127 +++++++----------- .../Sidekick_backend/Backend_intf/index.html | 3 +- .../Backend_intf/module-type-S/index.html | 3 +- .../Coq/Make/argument-1-S/Atom/index.html | 2 +- .../Coq/Make/argument-1-S/Clause/index.html | 2 +- .../Coq/Make/argument-1-S/index.html | 14 +- .../Coq/Make/argument-2-A/index.html | 8 +- sidekick/Sidekick_backend/Coq/Make/index.html | 3 +- .../Coq/Simple/argument-1-S/Atom/index.html | 2 +- .../Coq/Simple/argument-1-S/Clause/index.html | 2 +- .../Coq/Simple/argument-1-S/index.html | 14 +- .../Coq/Simple/argument-2-A/index.html | 8 +- .../Sidekick_backend/Coq/Simple/index.html | 3 +- sidekick/Sidekick_backend/Coq/index.html | 4 +- .../Coq/module-type-Arg/index.html | 8 +- .../Coq/module-type-S/index.html | 3 +- .../Dedukti/Make/argument-1-S/Atom/index.html | 2 +- .../Make/argument-1-S/Clause/index.html | 2 +- .../Dedukti/Make/argument-1-S/index.html | 14 +- .../Dedukti/Make/argument-2-A/index.html | 2 +- .../Sidekick_backend/Dedukti/Make/index.html | 3 +- sidekick/Sidekick_backend/Dedukti/index.html | 2 +- .../Dedukti/module-type-Arg/index.html | 2 +- .../Dedukti/module-type-S/index.html | 3 +- .../Dimacs/Make/argument-1-St/Atom/index.html | 2 +- .../Make/argument-1-St/Clause/index.html | 5 +- .../Make/argument-1-St/Formula/index.html | 2 +- .../Dimacs/Make/argument-1-St/Var/index.html | 4 +- .../Dimacs/Make/argument-1-St/index.html | 20 ++- .../Sidekick_backend/Dimacs/Make/index.html | 8 +- sidekick/Sidekick_backend/Dimacs/index.html | 3 +- .../Dimacs/module-type-S/index.html | 8 +- .../Dot/Default/argument-1-S/Atom/index.html | 2 +- .../Default/argument-1-S/Clause/index.html | 2 +- .../Dot/Default/argument-1-S/index.html | 14 +- .../Sidekick_backend/Dot/Default/index.html | 10 +- .../Dot/Make/argument-1-S/Atom/index.html | 2 +- .../Dot/Make/argument-1-S/Clause/index.html | 2 +- .../Dot/Make/argument-1-S/index.html | 14 +- .../Dot/Make/argument-2-A/index.html | 9 +- sidekick/Sidekick_backend/Dot/Make/index.html | 3 +- .../Dot/Simple/argument-1-S/Atom/index.html | 2 +- .../Dot/Simple/argument-1-S/Clause/index.html | 2 +- .../Dot/Simple/argument-1-S/index.html | 14 +- .../Dot/Simple/argument-2-A/index.html | 9 +- .../Sidekick_backend/Dot/Simple/index.html | 5 +- sidekick/Sidekick_backend/Dot/index.html | 6 +- .../Dot/module-type-Arg/index.html | 9 +- .../Dot/module-type-S/index.html | 3 +- sidekick/Sidekick_backend/index.html | 2 +- .../Sidekick_backend__Backend_intf/index.html | 3 +- .../module-type-S/index.html | 3 +- .../Make/argument-1-S/Atom/index.html | 2 +- .../Make/argument-1-S/Clause/index.html | 2 +- .../Make/argument-1-S/index.html | 14 +- .../Make/argument-2-A/index.html | 8 +- .../Sidekick_backend__Coq/Make/index.html | 3 +- .../Simple/argument-1-S/Atom/index.html | 2 +- .../Simple/argument-1-S/Clause/index.html | 2 +- .../Simple/argument-1-S/index.html | 14 +- .../Simple/argument-2-A/index.html | 8 +- .../Sidekick_backend__Coq/Simple/index.html | 3 +- sidekick/Sidekick_backend__Coq/index.html | 4 +- .../module-type-Arg/index.html | 8 +- .../module-type-S/index.html | 3 +- .../Make/argument-1-S/Atom/index.html | 2 +- .../Make/argument-1-S/Clause/index.html | 2 +- .../Make/argument-1-S/index.html | 14 +- .../Make/argument-2-A/index.html | 2 +- .../Sidekick_backend__Dedukti/Make/index.html | 3 +- sidekick/Sidekick_backend__Dedukti/index.html | 2 +- .../module-type-Arg/index.html | 2 +- .../module-type-S/index.html | 3 +- .../Make/argument-1-St/Atom/index.html | 2 +- .../Make/argument-1-St/Clause/index.html | 5 +- .../Make/argument-1-St/Formula/index.html | 2 +- .../Make/argument-1-St/Var/index.html | 4 +- .../Make/argument-1-St/index.html | 20 ++- .../Sidekick_backend__Dimacs/Make/index.html | 8 +- sidekick/Sidekick_backend__Dimacs/index.html | 3 +- .../module-type-S/index.html | 8 +- .../Default/argument-1-S/Atom/index.html | 2 +- .../Default/argument-1-S/Clause/index.html | 2 +- .../Default/argument-1-S/index.html | 14 +- .../Sidekick_backend__Dot/Default/index.html | 10 +- .../Make/argument-1-S/Atom/index.html | 2 +- .../Make/argument-1-S/Clause/index.html | 2 +- .../Make/argument-1-S/index.html | 14 +- .../Make/argument-2-A/index.html | 9 +- .../Sidekick_backend__Dot/Make/index.html | 3 +- .../Simple/argument-1-S/Atom/index.html | 2 +- .../Simple/argument-1-S/Clause/index.html | 2 +- .../Simple/argument-1-S/index.html | 14 +- .../Simple/argument-2-A/index.html | 9 +- .../Sidekick_backend__Dot/Simple/index.html | 5 +- sidekick/Sidekick_backend__Dot/index.html | 6 +- .../module-type-Arg/index.html | 9 +- .../module-type-S/index.html | 3 +- sidekick/Sidekick_dimacs/index.html | 3 +- sidekick/Sidekick_dimacs__/Lexer/index.html | 2 +- sidekick/Sidekick_dimacs__/Parser/index.html | 2 +- sidekick/Sidekick_dimacs__/index.html | 2 +- sidekick/Sidekick_dimacs__Lexer/index.html | 2 +- sidekick/Sidekick_dimacs__Parser/index.html | 2 +- sidekick/Sidekick_sat/Make/Clause/index.html | 2 +- sidekick/Sidekick_sat/Make/Formula/index.html | 2 +- sidekick/Sidekick_sat/Make/Lit/index.html | 2 +- .../Sidekick_sat/Make/Proof/Atom/index.html | 2 +- .../Make/Proof/Clause/Tbl/index.html | 2 +- .../Sidekick_sat/Make/Proof/Clause/index.html | 2 +- .../Sidekick_sat/Make/Proof/Tbl/index.html | 2 +- sidekick/Sidekick_sat/Make/Proof/index.html | 2 +- .../Make/argument-1-E/Form/index.html | 8 +- .../Sidekick_sat/Make/argument-1-E/index.html | 4 +- sidekick/Sidekick_sat/Make/index.html | 2 +- .../Sidekick_sat/Res/Make/Atom/index.html | 2 +- .../Sidekick_sat/Res/Make/Clause/index.html | 2 +- .../Res/Make/argument-1-St/Atom/index.html | 2 +- .../Res/Make/argument-1-St/Clause/index.html | 5 +- .../Res/Make/argument-1-St/Formula/index.html | 2 +- .../Res/Make/argument-1-St/Var/index.html | 4 +- .../Res/Make/argument-1-St/index.html | 20 ++- sidekick/Sidekick_sat/Res/Make/index.html | 14 +- sidekick/Sidekick_sat/Res/index.html | 2 +- .../Res/module-type-FULL/Atom/index.html | 2 +- .../Res/module-type-FULL/Clause/index.html | 2 +- .../Res/module-type-FULL/St/Atom/index.html | 2 +- .../Res/module-type-FULL/St/Clause/index.html | 5 +- .../module-type-FULL/St/Formula/index.html | 2 +- .../Res/module-type-FULL/St/Var/index.html | 4 +- .../Res/module-type-FULL/St/index.html | 20 ++- .../Res/module-type-FULL/index.html | 14 +- .../Res/module-type-S/Atom/index.html | 2 +- .../Res/module-type-S/Clause/index.html | 2 +- .../Sidekick_sat/Res/module-type-S/index.html | 14 +- .../Solver_types_intf/C_fields/index.html | 4 +- .../Solver_types_intf/Var_fields/index.html | 4 +- .../Sidekick_sat/Solver_types_intf/index.html | 3 +- .../module-type-S/Atom/index.html | 2 +- .../module-type-S/Clause/index.html | 5 +- .../module-type-S/Formula/index.html | 2 +- .../module-type-S/Var/index.html | 4 +- .../module-type-S/index.html | 20 ++- sidekick/Sidekick_sat/Theory_intf/index.html | 14 +- .../Theory_intf/module-type-S/Form/index.html | 8 +- .../Theory_intf/module-type-S/index.html | 4 +- sidekick/Sidekick_sat/index.html | 5 +- .../module-type-S/Clause/index.html | 3 +- .../module-type-S/Formula/index.html | 2 +- .../Sidekick_sat/module-type-S/Lit/index.html | 2 +- .../module-type-S/Proof/Atom/index.html | 2 +- .../module-type-S/Proof/Clause/index.html | 2 +- .../module-type-S/Proof/index.html | 14 +- .../Sidekick_sat/module-type-S/index.html | 18 ++- .../Sidekick_sat__/Internal/Make/H/index.html | 2 +- .../Internal/Make/Proof/Atom/index.html | 2 +- .../Internal/Make/Proof/Clause/Tbl/index.html | 2 +- .../Internal/Make/Proof/Clause/index.html | 2 +- .../Internal/Make/Proof/St/Atom/index.html | 2 +- .../Make/Proof/St/Clause/Tbl/index.html | 2 +- .../Internal/Make/Proof/St/Clause/index.html | 2 +- .../Internal/Make/Proof/St/Formula/index.html | 2 +- .../Internal/Make/Proof/St/Var/index.html | 2 +- .../Internal/Make/Proof/St/index.html | 2 +- .../Internal/Make/Proof/Tbl/index.html | 2 +- .../Internal/Make/Proof/index.html | 2 +- .../Make/argument-1-St/Atom/index.html | 2 +- .../Make/argument-1-St/Clause/index.html | 5 +- .../Make/argument-1-St/Formula/index.html | 2 +- .../Make/argument-1-St/Var/index.html | 4 +- .../Internal/Make/argument-1-St/index.html | 20 ++- .../Make/argument-2-Th/Form/index.html | 8 +- .../Internal/Make/argument-2-Th/index.html | 4 +- .../Sidekick_sat__/Internal/Make/index.html | 2 +- sidekick/Sidekick_sat__/Internal/index.html | 2 +- .../Sidekick_sat__/Res/Make/Atom/index.html | 2 +- .../Sidekick_sat__/Res/Make/Clause/index.html | 2 +- .../Res/Make/argument-1-St/Atom/index.html | 2 +- .../Res/Make/argument-1-St/Clause/index.html | 5 +- .../Res/Make/argument-1-St/Formula/index.html | 2 +- .../Res/Make/argument-1-St/Var/index.html | 4 +- .../Res/Make/argument-1-St/index.html | 20 ++- sidekick/Sidekick_sat__/Res/Make/index.html | 14 +- sidekick/Sidekick_sat__/Res/index.html | 2 +- .../Res/module-type-FULL/Atom/index.html | 2 +- .../Res/module-type-FULL/Clause/index.html | 2 +- .../Res/module-type-FULL/St/Atom/index.html | 2 +- .../Res/module-type-FULL/St/Clause/index.html | 5 +- .../module-type-FULL/St/Formula/index.html | 2 +- .../Res/module-type-FULL/St/Var/index.html | 4 +- .../Res/module-type-FULL/St/index.html | 20 ++- .../Res/module-type-FULL/index.html | 14 +- .../Res/module-type-S/Atom/index.html | 2 +- .../Res/module-type-S/Clause/index.html | 2 +- .../Res/module-type-S/index.html | 14 +- sidekick/Sidekick_sat__/Res_intf/index.html | 2 +- .../Res_intf/module-type-FULL/Atom/index.html | 2 +- .../module-type-FULL/Clause/index.html | 2 +- .../module-type-FULL/St/Atom/index.html | 2 +- .../module-type-FULL/St/Clause/index.html | 5 +- .../module-type-FULL/St/Formula/index.html | 2 +- .../module-type-FULL/St/Var/index.html | 4 +- .../Res_intf/module-type-FULL/St/index.html | 20 ++- .../Res_intf/module-type-FULL/index.html | 14 +- .../Res_intf/module-type-S/Atom/index.html | 2 +- .../Res_intf/module-type-S/Clause/index.html | 2 +- .../Res_intf/module-type-S/index.html | 14 +- .../Solver/Make/Clause/index.html | 3 +- .../Solver/Make/Formula/index.html | 2 +- .../Sidekick_sat__/Solver/Make/Lit/index.html | 2 +- .../Solver/Make/Proof/Atom/index.html | 2 +- .../Solver/Make/Proof/Clause/index.html | 2 +- .../Solver/Make/Proof/index.html | 14 +- .../Solver/Make/argument-1-St/Atom/index.html | 2 +- .../Make/argument-1-St/Clause/index.html | 5 +- .../Make/argument-1-St/Formula/index.html | 2 +- .../Solver/Make/argument-1-St/Var/index.html | 4 +- .../Solver/Make/argument-1-St/index.html | 20 ++- .../Solver/Make/argument-2-Th/Form/index.html | 8 +- .../Solver/Make/argument-2-Th/index.html | 4 +- .../Sidekick_sat__/Solver/Make/index.html | 18 ++- sidekick/Sidekick_sat__/Solver/index.html | 3 +- .../Solver/module-type-S/Clause/index.html | 3 +- .../Solver/module-type-S/Formula/index.html | 2 +- .../Solver/module-type-S/Lit/index.html | 2 +- .../module-type-S/Proof/Atom/index.html | 2 +- .../module-type-S/Proof/Clause/index.html | 2 +- .../Solver/module-type-S/Proof/index.html | 14 +- .../Solver/module-type-S/index.html | 18 ++- .../Sidekick_sat__/Solver_intf/index.html | 10 +- .../module-type-S/Clause/index.html | 3 +- .../module-type-S/Formula/index.html | 2 +- .../Solver_intf/module-type-S/Lit/index.html | 2 +- .../module-type-S/Proof/Atom/index.html | 2 +- .../module-type-S/Proof/Clause/index.html | 2 +- .../module-type-S/Proof/index.html | 14 +- .../Solver_intf/module-type-S/index.html | 19 ++- .../Solver_types/Make/Atom/index.html | 2 +- .../Solver_types/Make/Clause/index.html | 5 +- .../Solver_types/Make/Formula/index.html | 2 +- .../Solver_types/Make/Var/index.html | 4 +- .../Make/argument-1-E/Form/index.html | 8 +- .../Solver_types/Make/argument-1-E/index.html | 4 +- .../Solver_types/Make/index.html | 20 ++- .../Sidekick_sat__/Solver_types/index.html | 6 +- .../module-type-S/Atom/index.html | 2 +- .../module-type-S/Clause/index.html | 5 +- .../module-type-S/Formula/index.html | 2 +- .../Solver_types/module-type-S/Var/index.html | 4 +- .../Solver_types/module-type-S/index.html | 20 ++- .../Solver_types_intf/C_fields/index.html | 4 +- .../Solver_types_intf/Var_fields/index.html | 4 +- .../Solver_types_intf/index.html | 3 +- .../module-type-S/Atom/index.html | 2 +- .../module-type-S/Clause/index.html | 5 +- .../module-type-S/Formula/index.html | 2 +- .../module-type-S/Var/index.html | 4 +- .../module-type-S/index.html | 20 ++- .../Sidekick_sat__/Theory_intf/index.html | 14 +- .../Theory_intf/module-type-S/Form/index.html | 8 +- .../Theory_intf/module-type-S/index.html | 4 +- sidekick/Sidekick_sat__/index.html | 2 +- .../Sidekick_sat__Internal/Make/H/index.html | 2 +- .../Make/Proof/Atom/index.html | 2 +- .../Make/Proof/Clause/Tbl/index.html | 2 +- .../Make/Proof/Clause/index.html | 2 +- .../Make/Proof/St/Atom/index.html | 2 +- .../Make/Proof/St/Clause/Tbl/index.html | 2 +- .../Make/Proof/St/Clause/index.html | 2 +- .../Make/Proof/St/Formula/index.html | 2 +- .../Make/Proof/St/Var/index.html | 2 +- .../Make/Proof/St/index.html | 2 +- .../Make/Proof/Tbl/index.html | 2 +- .../Make/Proof/index.html | 2 +- .../Make/argument-1-St/Atom/index.html | 2 +- .../Make/argument-1-St/Clause/index.html | 5 +- .../Make/argument-1-St/Formula/index.html | 2 +- .../Make/argument-1-St/Var/index.html | 4 +- .../Make/argument-1-St/index.html | 20 ++- .../Make/argument-2-Th/Form/index.html | 8 +- .../Make/argument-2-Th/index.html | 4 +- .../Sidekick_sat__Internal/Make/index.html | 2 +- sidekick/Sidekick_sat__Internal/index.html | 2 +- .../Sidekick_sat__Res/Make/Atom/index.html | 2 +- .../Sidekick_sat__Res/Make/Clause/index.html | 2 +- .../Make/argument-1-St/Atom/index.html | 2 +- .../Make/argument-1-St/Clause/index.html | 5 +- .../Make/argument-1-St/Formula/index.html | 2 +- .../Make/argument-1-St/Var/index.html | 4 +- .../Make/argument-1-St/index.html | 20 ++- sidekick/Sidekick_sat__Res/Make/index.html | 14 +- sidekick/Sidekick_sat__Res/index.html | 2 +- .../module-type-FULL/Atom/index.html | 2 +- .../module-type-FULL/Clause/index.html | 2 +- .../module-type-FULL/St/Atom/index.html | 2 +- .../module-type-FULL/St/Clause/index.html | 5 +- .../module-type-FULL/St/Formula/index.html | 2 +- .../module-type-FULL/St/Var/index.html | 4 +- .../module-type-FULL/St/index.html | 20 ++- .../module-type-FULL/index.html | 14 +- .../module-type-S/Atom/index.html | 2 +- .../module-type-S/Clause/index.html | 2 +- .../module-type-S/index.html | 14 +- sidekick/Sidekick_sat__Res_intf/index.html | 2 +- .../module-type-FULL/Atom/index.html | 2 +- .../module-type-FULL/Clause/index.html | 2 +- .../module-type-FULL/St/Atom/index.html | 2 +- .../module-type-FULL/St/Clause/index.html | 5 +- .../module-type-FULL/St/Formula/index.html | 2 +- .../module-type-FULL/St/Var/index.html | 4 +- .../module-type-FULL/St/index.html | 20 ++- .../module-type-FULL/index.html | 14 +- .../module-type-S/Atom/index.html | 2 +- .../module-type-S/Clause/index.html | 2 +- .../module-type-S/index.html | 14 +- .../Make/Clause/index.html | 3 +- .../Make/Formula/index.html | 2 +- .../Sidekick_sat__Solver/Make/Lit/index.html | 2 +- .../Make/Proof/Atom/index.html | 2 +- .../Make/Proof/Clause/index.html | 2 +- .../Make/Proof/index.html | 14 +- .../Make/argument-1-St/Atom/index.html | 2 +- .../Make/argument-1-St/Clause/index.html | 5 +- .../Make/argument-1-St/Formula/index.html | 2 +- .../Make/argument-1-St/Var/index.html | 4 +- .../Make/argument-1-St/index.html | 20 ++- .../Make/argument-2-Th/Form/index.html | 8 +- .../Make/argument-2-Th/index.html | 4 +- sidekick/Sidekick_sat__Solver/Make/index.html | 18 ++- sidekick/Sidekick_sat__Solver/index.html | 3 +- .../module-type-S/Clause/index.html | 3 +- .../module-type-S/Formula/index.html | 2 +- .../module-type-S/Lit/index.html | 2 +- .../module-type-S/Proof/Atom/index.html | 2 +- .../module-type-S/Proof/Clause/index.html | 2 +- .../module-type-S/Proof/index.html | 14 +- .../module-type-S/index.html | 18 ++- sidekick/Sidekick_sat__Solver_intf/index.html | 10 +- .../module-type-S/Clause/index.html | 3 +- .../module-type-S/Formula/index.html | 2 +- .../module-type-S/Lit/index.html | 2 +- .../module-type-S/Proof/Atom/index.html | 2 +- .../module-type-S/Proof/Clause/index.html | 2 +- .../module-type-S/Proof/index.html | 14 +- .../module-type-S/index.html | 19 ++- .../Make/Atom/index.html | 2 +- .../Make/Clause/index.html | 5 +- .../Make/Formula/index.html | 2 +- .../Make/Var/index.html | 4 +- .../Make/argument-1-E/Form/index.html | 8 +- .../Make/argument-1-E/index.html | 4 +- .../Make/index.html | 20 ++- .../Sidekick_sat__Solver_types/index.html | 6 +- .../module-type-S/Atom/index.html | 2 +- .../module-type-S/Clause/index.html | 5 +- .../module-type-S/Formula/index.html | 2 +- .../module-type-S/Var/index.html | 4 +- .../module-type-S/index.html | 20 ++- .../C_fields/index.html | 4 +- .../Var_fields/index.html | 4 +- .../index.html | 3 +- .../module-type-S/Atom/index.html | 2 +- .../module-type-S/Clause/index.html | 5 +- .../module-type-S/Formula/index.html | 2 +- .../module-type-S/Var/index.html | 4 +- .../module-type-S/index.html | 20 ++- sidekick/Sidekick_sat__Theory_intf/index.html | 14 +- .../module-type-S/Form/index.html | 8 +- .../module-type-S/index.html | 4 +- sidekick/Sidekick_smt/Ast/Ty/index.html | 3 + sidekick/Sidekick_smt/Ast/Var/index.html | 2 + sidekick/Sidekick_smt/Ast/index.html | 2 +- sidekick/Sidekick_smt/Bag/index.html | 3 +- sidekick/Sidekick_smt/Config/Key/index.html | 2 + sidekick/Sidekick_smt/Config/index.html | 2 +- .../Congruence_closure/index.html | 7 +- sidekick/Sidekick_smt/Cst/index.html | 2 +- sidekick/Sidekick_smt/Equiv_class/index.html | 15 ++- .../Sidekick_smt/Explanation/Set/index.html | 2 +- sidekick/Sidekick_smt/Explanation/index.html | 2 +- sidekick/Sidekick_smt/Hash/index.html | 2 +- sidekick/Sidekick_smt/Het_map/Key/index.html | 2 + sidekick/Sidekick_smt/Het_map/Map/index.html | 2 + sidekick/Sidekick_smt/Het_map/Tbl/index.html | 2 + sidekick/Sidekick_smt/Het_map/index.html | 2 +- sidekick/Sidekick_smt/Lit/index.html | 2 +- sidekick/Sidekick_smt/Model/index.html | 2 +- sidekick/Sidekick_smt/Solver/Proof/index.html | 2 + .../Solver/Sat_solver/Clause/index.html | 3 + .../Solver/Sat_solver/Formula/index.html | 2 + .../Solver/Sat_solver/Lit/index.html | 2 + .../Solver/Sat_solver/Proof/Atom/index.html | 2 + .../Solver/Sat_solver/Proof/Clause/index.html | 2 + .../Solver/Sat_solver/Proof/index.html | 14 ++ .../Sidekick_smt/Solver/Sat_solver/index.html | 18 +++ sidekick/Sidekick_smt/Solver/index.html | 2 +- sidekick/Sidekick_smt/Solver_types/index.html | 16 ++- sidekick/Sidekick_smt/Stat/index.html | 2 +- sidekick/Sidekick_smt/Term/index.html | 2 +- .../Term_cell/Make_eq/argument-1-X/index.html | 2 +- .../Sidekick_smt/Term_cell/Make_eq/index.html | 2 +- sidekick/Sidekick_smt/Term_cell/index.html | 2 +- .../Term_cell/module-type-ARG/index.html | 2 +- .../Sidekick_smt/Theory/Clause/index.html | 2 +- sidekick/Sidekick_smt/Theory/index.html | 9 +- .../Theory_combine/Form/index.html | 8 ++ .../Theory_combine/Proof/index.html | 2 + .../Sidekick_smt/Theory_combine/index.html | 4 +- sidekick/Sidekick_smt/Ty/index.html | 2 +- sidekick/Sidekick_smt/Ty_card/index.html | 2 +- sidekick/Sidekick_smt/index.html | 2 +- sidekick/Sidekick_smt__Ast/Ty/index.html | 3 +- sidekick/Sidekick_smt__Ast/Var/index.html | 2 +- sidekick/Sidekick_smt__Ast/index.html | 2 +- sidekick/Sidekick_smt__Bag/index.html | 3 +- sidekick/Sidekick_smt__Config/Key/index.html | 2 +- sidekick/Sidekick_smt__Config/index.html | 2 +- .../index.html | 7 +- sidekick/Sidekick_smt__Cst/index.html | 2 +- sidekick/Sidekick_smt__Equiv_class/index.html | 15 ++- .../Sidekick_smt__Explanation/Set/index.html | 2 +- sidekick/Sidekick_smt__Explanation/index.html | 2 +- sidekick/Sidekick_smt__Hash/index.html | 2 +- sidekick/Sidekick_smt__Het_map/Key/index.html | 2 +- sidekick/Sidekick_smt__Het_map/Map/index.html | 2 +- sidekick/Sidekick_smt__Het_map/Tbl/index.html | 2 +- sidekick/Sidekick_smt__Het_map/index.html | 2 +- sidekick/Sidekick_smt__Lit/index.html | 2 +- sidekick/Sidekick_smt__Model/index.html | 2 +- .../Sidekick_smt__Solver/Proof/index.html | 2 +- .../Sat_solver/Clause/index.html | 3 +- .../Sat_solver/Formula/index.html | 2 +- .../Sat_solver/Lit/index.html | 2 +- .../Sat_solver/Proof/Atom/index.html | 2 +- .../Sat_solver/Proof/Clause/index.html | 2 +- .../Sat_solver/Proof/index.html | 14 +- .../Sat_solver/index.html | 18 ++- sidekick/Sidekick_smt__Solver/index.html | 2 +- .../Sidekick_smt__Solver_types/index.html | 16 ++- sidekick/Sidekick_smt__Stat/index.html | 2 +- sidekick/Sidekick_smt__Term/index.html | 2 +- .../Make_eq/argument-1-X/index.html | 2 +- .../Make_eq/index.html | 2 +- sidekick/Sidekick_smt__Term_cell/index.html | 2 +- .../module-type-ARG/index.html | 2 +- .../Sidekick_smt__Theory/Clause/index.html | 2 +- sidekick/Sidekick_smt__Theory/index.html | 9 +- .../Form/index.html | 8 +- .../Proof/index.html | 2 +- .../Sidekick_smt__Theory_combine/index.html | 4 +- sidekick/Sidekick_smt__Ty/index.html | 2 +- sidekick/Sidekick_smt__Ty_card/index.html | 2 +- sidekick/Sidekick_smtlib/Process/index.html | 2 +- sidekick/Sidekick_smtlib/index.html | 3 +- sidekick/Sidekick_smtlib__/Lexer/index.html | 2 +- .../Sidekick_smtlib__/Locations/index.html | 2 +- .../Sidekick_smtlib__/Parse_ast/index.html | 2 +- sidekick/Sidekick_smtlib__/Parser/index.html | 2 +- sidekick/Sidekick_smtlib__/Process/index.html | 2 +- .../Typecheck/Ctx/index.html | 2 + .../Sidekick_smtlib__/Typecheck/index.html | 2 +- sidekick/Sidekick_smtlib__/index.html | 2 +- sidekick/Sidekick_smtlib__Lexer/index.html | 2 +- .../Sidekick_smtlib__Locations/index.html | 2 +- .../Sidekick_smtlib__Parse_ast/index.html | 2 +- sidekick/Sidekick_smtlib__Parser/index.html | 2 +- sidekick/Sidekick_smtlib__Process/index.html | 2 +- .../Sidekick_smtlib__Typecheck/Ctx/index.html | 2 +- .../Sidekick_smtlib__Typecheck/index.html | 2 +- sidekick/Sidekick_th_bool/Lit/index.html | 2 +- sidekick/Sidekick_th_bool/T_cell/index.html | 2 +- sidekick/Sidekick_th_bool/index.html | 2 +- .../Sidekick_util/BitField/Make/index.html | 4 + sidekick/Sidekick_util/BitField/index.html | 17 ++- .../BitField/module-type-S/index.html | 4 + .../Heap/Make/argument-1-X/index.html | 2 +- sidekick/Sidekick_util/Heap/Make/index.html | 6 +- sidekick/Sidekick_util/Heap/index.html | 2 +- .../Heap/module-type-RANKED/index.html | 2 +- .../Heap/module-type-S/index.html | 6 +- sidekick/Sidekick_util/Heap_intf/index.html | 2 +- .../Heap_intf/module-type-RANKED/index.html | 2 +- .../Heap_intf/module-type-S/index.html | 6 +- sidekick/Sidekick_util/IArray/index.html | 4 +- sidekick/Sidekick_util/ID/B/index.html | 2 + sidekick/Sidekick_util/ID/index.html | 2 +- sidekick/Sidekick_util/Intf/index.html | 2 +- .../Intf/module-type-EQ/index.html | 2 +- .../Intf/module-type-HASH/index.html | 2 +- .../Intf/module-type-ORD/index.html | 2 +- .../Intf/module-type-PRINT/index.html | 2 +- sidekick/Sidekick_util/Log/index.html | 3 +- sidekick/Sidekick_util/Util/index.html | 2 +- sidekick/Sidekick_util/Vec/index.html | 11 +- sidekick/Sidekick_util/index.html | 2 +- .../Sidekick_util__BitField/Make/index.html | 4 +- sidekick/Sidekick_util__BitField/index.html | 19 +-- .../module-type-S/index.html | 4 +- .../Make/argument-1-X/index.html | 2 +- sidekick/Sidekick_util__Heap/Make/index.html | 6 +- sidekick/Sidekick_util__Heap/index.html | 2 +- .../module-type-RANKED/index.html | 2 +- .../module-type-S/index.html | 6 +- sidekick/Sidekick_util__Heap_intf/index.html | 2 +- .../module-type-RANKED/index.html | 2 +- .../module-type-S/index.html | 6 +- sidekick/Sidekick_util__IArray/index.html | 4 +- sidekick/Sidekick_util__ID/B/index.html | 2 +- sidekick/Sidekick_util__ID/index.html | 2 +- sidekick/Sidekick_util__Intf/index.html | 2 +- .../module-type-EQ/index.html | 2 +- .../module-type-HASH/index.html | 2 +- .../module-type-ORD/index.html | 2 +- .../module-type-PRINT/index.html | 2 +- sidekick/Sidekick_util__Log/index.html | 3 +- sidekick/Sidekick_util__Util/index.html | 2 +- sidekick/Sidekick_util__Vec/index.html | 11 +- sidekick/index.html | 22 ++- 519 files changed, 2151 insertions(+), 582 deletions(-) create mode 100644 msat_test/index.html create mode 100644 sidekick/Sidekick_smt/Ast/Ty/index.html create mode 100644 sidekick/Sidekick_smt/Ast/Var/index.html create mode 100644 sidekick/Sidekick_smt/Config/Key/index.html create mode 100644 sidekick/Sidekick_smt/Het_map/Key/index.html create mode 100644 sidekick/Sidekick_smt/Het_map/Map/index.html create mode 100644 sidekick/Sidekick_smt/Het_map/Tbl/index.html create mode 100644 sidekick/Sidekick_smt/Solver/Proof/index.html create mode 100644 sidekick/Sidekick_smt/Solver/Sat_solver/Clause/index.html create mode 100644 sidekick/Sidekick_smt/Solver/Sat_solver/Formula/index.html create mode 100644 sidekick/Sidekick_smt/Solver/Sat_solver/Lit/index.html create mode 100644 sidekick/Sidekick_smt/Solver/Sat_solver/Proof/Atom/index.html create mode 100644 sidekick/Sidekick_smt/Solver/Sat_solver/Proof/Clause/index.html create mode 100644 sidekick/Sidekick_smt/Solver/Sat_solver/Proof/index.html create mode 100644 sidekick/Sidekick_smt/Solver/Sat_solver/index.html create mode 100644 sidekick/Sidekick_smt/Theory_combine/Form/index.html create mode 100644 sidekick/Sidekick_smt/Theory_combine/Proof/index.html create mode 100644 sidekick/Sidekick_smtlib__/Typecheck/Ctx/index.html create mode 100644 sidekick/Sidekick_util/BitField/Make/index.html create mode 100644 sidekick/Sidekick_util/BitField/module-type-S/index.html create mode 100644 sidekick/Sidekick_util/ID/B/index.html diff --git a/msat_test/index.html b/msat_test/index.html new file mode 100644 index 00000000..48c555c8 --- /dev/null +++ b/msat_test/index.html @@ -0,0 +1,2 @@ + +index (msat_test.index)
\ No newline at end of file diff --git a/odoc.css b/odoc.css index d84a27de..e7808926 100644 --- a/odoc.css +++ b/odoc.css @@ -1,7 +1,7 @@ @charset "UTF-8"; /* Copyright (c) 2016 Daniel C. Bünzli. All rights reserved. Distributed under the ISC license, see terms at the end of the file. - %%NAME%% %%VERSION%% */ + odoc 1.2.0 */ /* Reset a few things. */ @@ -21,32 +21,32 @@ table { border-collapse: collapse; border-spacing: 0; } body { font-family: Helvetica, "DejaVu Sans", Arial, sans-serif; font-weight: normal; - font-size: 14px; - line-height:20px; + font-size: 0.875rem; + line-height:1.25rem; text-align: left; min-width: 40ex; max-width: 78ex; - padding: 20px; - margin-left: 60px; + padding: 1.25rem; + margin-left: 3.75rem; color: #222; background: #FAFAFA; } /* Basic markup elements */ b, strong { font-weight: bold; } -i, em { font-style: italic; } +em { font-style: italic; } sup { vertical-align: super; } sub { vertical-align: sub; } -sup, sub { font-size : 12px; line-height: 0; margin-left: 0.2ex; } +sup, sub { font-size : 0.75rem; line-height: 0; margin-left: 0.2ex; } -p, div, img { margin-top: 20px; } +p, div, img { margin-top: 1.25rem; } ul, ol -{ margin-top: 10px; margin-bottom: 10px; list-style-position: outside } +{ margin-top: 0.625rem; margin-bottom: 0.625rem; list-style-position: outside } ul { list-style-type: square } -ul > li { margin-left: 22px; } -ol > li { margin-left: 27.2px; } +ul > li { margin-left: 1.375rem; } +ol > li { margin-left: 1.7rem; } li > *:first-child { margin-top: 0 } /* Text alignements, this should be forbidden. */ @@ -63,9 +63,8 @@ a:hover { box-shadow:0 1px 0 0 #2C5CBD; } { background-color: #FFF8E5; box-shadow: 0 0 0 2px #FFF8E5, 0 0 0 3px #DDD; } -*:hover > a.anchor { - visibility: visible; -} +.spec:hover > a.anchor, /* FIXME remove */ +.anchored:hover a.anchor { visibility: visible; } a.anchor:before { content: "#" } a.anchor:hover { box-shadow: none; text-decoration: underline } @@ -84,21 +83,19 @@ a.anchor we restart the sequence there like h2 */ h1, h2, h3, h4, h5, h6, .h7, .h8, .h9, .h10 -{ font-weight: bold; margin-top: 20px; } - -h1 + *, h2 + *, .h7 + * { margin-top: 10px; } +{ font-weight: bold; margin-top: 1.25rem; } +h1 + *, h2 + *, .h7 + * { margin-top: 0.625rem; } h1, h2, .h7 -{ font-size: 20px; - line-height: 39px; - padding-top: 10px; +{ font-size: 1.25rem; + line-height: 2.4375rem; /* 2.5rem - border width */ + padding-top: 0.625rem; border-top: solid; border-width: 1px; border-color: #DDD; } -h3 { font-size: 18px; } - -h2 + h3, .h7 + .h8 { margin-top: 10px; } +h3, .h8 { font-size: 1.125rem; } +h2 + h3, .h7 + .h8 { margin-top: 0.625rem; } /* Preformatted and code */ @@ -106,18 +103,18 @@ tt, code, pre { font-family: Menlo, "DejaVu Sans Mono", "Bitstream Vera Sans Mono", monospace; font-weight: normal; - font-size: 12px; } + font-size: 0.75rem; } pre -{ padding-left: 4px; padding-right: 4px; - margin-left: -4px; margin-right: -4px; - padding-top: 5px; padding-bottom: 5px; - margin-top: 20px; /* margin-bottom: 0.625rem; */ - line-height: 19px; +{ padding-left: 0.25rem; padding-right: 0.25rem; + margin-left: -0.25rem; margin-right: -0.25rem; + padding-top: 0.3125rem; padding-bottom: 0.3125rem; + margin-top: 1.25rem; /* margin-bottom: 0.625rem; */ + line-height: 1.1875rem; background: #F1F1F1; } -h1 tt, h1 code, h2 tt, h2 code, .h7 tt, .h7 code { font-size: 18px } -h3 tt, h3 code { font-size: 16px } +h1 tt, h1 code, h2 tt, h2 code, .h7 tt, .h7 code { font-size: 1.125rem } +h3 tt, h3 code { font-size: 1rem } /* Code lexemes */ @@ -125,33 +122,19 @@ h3 tt, h3 code { font-size: 16px } /* Module member specification */ -div.def { margin-top: 0; text-indent: -2ex; padding-left: 2ex; } -div.def + div.doc { margin-left: 1ex; margin-top: 2.5px } -div.doc > *:first-child { margin-top: 0; } - -/* The elements other than heading should be wrapped in