- 08 Jul, 2010 4 commits
-
-
Francois Bobot authored
-
Francois Bobot authored
-
Francois Bobot authored
-
Francois Bobot authored
-
- 07 Jul, 2010 7 commits
-
-
Andrei Paskevich authored
- dependent transformations (ones that depend on cloning history and/or metaproperties) have now the same type Trans.trans and can be registered via Trans, too. - load_driver accumulates appropriate tdecls to be appended to tasks before transformation/printing. At this moment, we have almost everything in place and are ready to remove Register module (subsumed by Trans and Printer in core/) and Prover module (its functions will move to Driver), and convert all printers and transformations to use the new infrastructure. Not implemented yet: - appending driver-imposed tdecls to tasks - when and where? - metas-options - what is the best way to implement them? - syntax/typing for metas in theories and drivers.
-
Francois Bobot authored
-
MARCHE Claude authored
-
Jean-Christophe Filliâtre authored
-
Francois Bobot authored
-
Francois Bobot authored
completion : complete theories and goals
-
MARCHE Claude authored
-
- 06 Jul, 2010 11 commits
-
-
Andrei Paskevich authored
(thus, e.g., both alt-ergo and smt printers can register "AC")
-
Andrei Paskevich authored
-
MARCHE Claude authored
-
Jean-Christophe Filliâtre authored
-
Francois Bobot authored
-
Francois Bobot authored
-
Francois Bobot authored
-
Francois Bobot authored
-
Francois Bobot authored
-
Jean-Christophe Filliâtre authored
-
Andrei Paskevich authored
-
- 05 Jul, 2010 11 commits
-
-
Jean-Christophe Filliâtre authored
-
MARCHE Claude authored
-
Jean-Christophe Filliâtre authored
-
Jean-Christophe Filliâtre authored
-
MARCHE Claude authored
-
Jean-Christophe Filliâtre authored
installation (work in progress, currently for developers only); why.conf is also searched for in the installation path (Config.why_libdir); in why.conf, theories and drivers filenames are relative to why.conf dirname (when relative)
-
Jean-Christophe Filliâtre authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
MARCHE Claude authored
-
Jean-Christophe Filliâtre authored
-
- 04 Jul, 2010 2 commits
-
-
Andrei Paskevich authored
- introduce a new Theory.tdecl "Meta" to be used for tags - simplify cloning procedure, get rid of the th_clone field - when a goal proposition is discarded during cloning, it's still keeped in the theory as a "skip proposition", this is needed to preserve/clone every local identifier. Skip propositions are eliminated during task formation. - get rid of a separate Task.tdecl type - reorganize the Task.task_hd record: * use/clone history is cached in a theory-keyed map; * meta-properties are cached in a tagname-keyed map. This is done to simplify the fine-grained configuration of transformations.
-
Jean-Christophe Filliâtre authored
-
- 02 Jul, 2010 4 commits
-
-
MARCHE Claude authored
-
Jean-Christophe Filliâtre authored
-
Andrei Paskevich authored
-
MARCHE Claude authored
-
- 01 Jul, 2010 1 commit
-
-
Jean-Christophe Filliâtre authored
-