2100 & 2132 - command line completion issues

[daniilsvc]

Related to #2100 and #2132.

1. Refactored getAllConsCheckers function in Proofs.AbstractState to remove duplicates among cons checkers.
2. Added saveConsCheckersInState function in CMDL.Interface to check valid binaries for cons checkers on start up in cmdRunShell and save them in CmdlState.
3. Function nubWith from Common.Utils now tail-recursive.
4. Function findComorphismPaths in Logic.Grothendieck changed slightly (n > 2 to n > 0 at line 893) without changing main algo. It affects performance and doesn't affect completion output.

What findComorphismPaths does is building tree of AnyComorphism (Comorphism as root and Comorphism(CompComorphism ...) in other nodes to be precise). This function doesn't produce any cycle but it grows very quick. Each branch of a tree contains composition of comorphisms and we never repeat previously used comorphism within a branch. But initial pool of comorphisms we use for building new composition is Map.elems $ comorphisms lg at line 890 which lenght is 71. So our tree grows in width pretty fast and on depth 4 we have 1724 nodes, 11669 nodes on depth 5, 71022 on depth 6 and so on. This is major problem here but if I restrict the depth of the tree to one level after the root (e.g. node > 0) then performance is OK and result is the same.

[mcodescu]

If you restrict the depth to 1, the result is the same for the CASL logic (the one in the example), but not in general. For example, you have different results for

logic QBF
spec S = 
 props a, b

[tillmo]

I agree with @mcodescu. Please implement a cycle check. I suggest not to use the Eq instance for G_sublogics, but rather check whether the logics are the same:

sameLogic (G_sublogics lid1 l1) (G_sublogics lid2 l2) =
      Logic lid1 == Logic lid2

If that does not suffice, use Dijkstra's algorithm.

[tillmo]

Cycling through the same logic can be useful, e.g. consider codings from CASL to CASL. Hence, I suggest to equip comorphisms with weights, such that e.g. CASL2CoCASL gets a high weight because it is not part of a path towards a tool-supported logic, and use Dijkstra's algorithm

[tillmo]

Here my proposal for comorphism weights:

weight 5
CASL2CoCASL
CASL2CspCASL
CASL2ExtModal
CASL2HasCASL
CASL2Hybrid
CASL2Modal
CASL2VSE
CASL2VSEImport
CASL2VSERefine
HasCASL2IsabelleDeprecated
OWL22NeSyPatterns

weight 4
CASL_DL2CASL
CASL2Propositional
CASL2OWL
OWL22CommonLogic
Propositional2CommonLogic
Propositional2OWL2
Propositional2QBF
SoftFOL2CommonLogic

weight 3
THFP_P2HasCASL
CspCASL2Modal

weight 2
OWL22CASL
Propositional2CASL
CoCASL2Isabelle
CommonLogic2Isabelle
CASL2Isabelle
CommonLogicModuleElimination
CspCASL2CspCASL_Failure
CspCASL2CspCASL_Trace
HasCASL2IsabelleOption
THFP2THF0
THFP_P2THFP

weight 1
Adl2CASL
CASL2NNF
CASL2PCFOL
CASL2PCFOLTopSort
CASL2Prenex
CASL2Skolem
CASL2SoftFOL
CASL2SoftFOLInduction
CASL2SoftFOLInduction2
CASL2SubCFOL
CASL2SubCFOLNoMembershipOrCast
CASL2SubCFOLSubsortBottoms
CASL2TPTP_FOF
CLFol2CFOL
CLFull2CFOL
CLImp2CFOL
CLSeq2CFOL
CoCASL2CoPCFOL
CoCASL2CoSubCFOL
CSMOF2CASL
DFOL2CASL
DMU2OWL2
ExtModal2CASL
ExtModal2ExtModalNoSubsorts
ExtModal2ExtModalTotal
ExtModal2HasCASL
ExtModal2OWL
HasCASL2HasCASLNoSubtypes
HasCASL2HasCASLPrograms
HasCASL2THFP_P
HolLight2Isabelle
Hybrid2CASL
Maude2CASL
Modal2CASL
MonadicTranslation
NormalisingTranslation
QBF2Propositional
QVTR2CASL
RelScheme2CASL

[mcodescu]

Looks good. I was wondering if you have a reason to give OWL22CASL and Propositional2CASL the weight 4. We get fewer cons-checkers and fewer provers for OWL and Propositional this way.

[tillmo]

good point. Have changed their weight to 2.

[daniilsvc]

@mcodescu , need your review after checks passed. Notes about the code:

• I changed weights of comorphisms, the lower weight - the higher priority as algo treats weights as disntaces from root node. Otherwise we go deep in some branch but practically don't search tree in breadth.
• The algo has some parameters for parameterisation: weight_limit at line 1027 and times_logic_in_branch at line 1030. This is the way we can stop execution of algorithm before the search tree grows too big. weight_limit is upper border of sum of all comorphism weights in tree. If wee exceeds this limit we stop adding new nodes. times_logic_in_branch is number of times a particular logic can be met within a branch.
• Right now it returns correct result (same cons_checkers as with the original findComorphismPaths). But it worth to notice that original findComorphismPaths generates 11669 comorphisms. New findComorphismPaths with current parameters generates only 200 comorphisms. If you increase weight_limit for algo to generate more nodes in tree (means more final comorphisms) you will see that get performance issue again - some freezes appear. So I would say that the problem here is not the way we generate the tree but the size of the result tree itself. In CLI it may be unacceptable to generate big tree but this problem could be solved without assigning weights to comorphism and writing new algo but simply by restricting the depth of the tree in original findComorphismPaths as I proposed earlier.

I comment out traces but I would keep them for some time, while the issue is not resolved.

[daniilsvc]

Seems like it worth to play with parameters to find optimal configuration. Some output produced by me:

-- reversed weights
-- weight_limit = 10
-- times_logic_in_branch = 3
-- correct output, no freezes
test_s> cons-- length paths: 473

cons-checker                cons-checker zchaff         cons-checker Pellet         cons-checker darwin         cons-checker leo
conservativity-check-open   cons-checker minisat        cons-checker ekrh           cons-checker e-darwin
conservativity-check        cons-checker truth tables   cons-checker darwin-non-fd  cons-checker eprover

-- original weights
-- weight_limit = 5
-- times_logic_in_branch = 3
-- correct output, have freezes
test_s> cons-- length paths: 8350

cons-checker                cons-checker Pellet         cons-checker truth tables   cons-checker e-darwin       cons-checker ekrh
conservativity-check-open   cons-checker zchaff         cons-checker darwin-non-fd  cons-checker eprover
conservativity-check        cons-checker minisat        cons-checker darwin         cons-checker leo

-- original weights
-- weight_limit = 4
-- times_logic_in_branch = 3
-- correct output, small freezes
test_s> cons-- length paths: 3220

cons-checker                cons-checker Pellet         cons-checker truth tables   cons-checker e-darwin       cons-checker ekrh
conservativity-check-open   cons-checker zchaff         cons-checker darwin-non-fd  cons-checker eprover
conservativity-check        cons-checker minisat        cons-checker darwin         cons-checker leo

-- original weights
-- weight_limit = 3
-- times_logic_in_branch = 3
-- small output, no freezes
test_s> cons-- length paths: 605

cons-checker                conservativity-check        cons-checker darwin         cons-checker eprover        cons-checker ekrh
conservativity-check-open   cons-checker darwin-non-fd  cons-checker e-darwin       cons-checker leo

-- original weights
-- weight_limit = 4
-- times_logic_in_branch = 2
--  correct output, no freezes
test_s> cons-- length paths: 1672

cons-checker                cons-checker Pellet         cons-checker truth tables   cons-checker darwin         cons-checker leo
conservativity-check-open   cons-checker zchaff         cons-checker ekrh           cons-checker e-darwin
conservativity-check        cons-checker minisat        cons-checker darwin-non-fd  cons-checker eprover

Last variant with weight_limit = 4 and times_logic_in_branch = 2 seems more or less optimal. What do you think, @mcodescu ?

[mcodescu]

I'm not sure. I think we might want to apply several transformations to a CASL theory that encode various features without changing the logic, so 2 might be too small. @tillmo what do you think?

[daniilsvc]

@mcodescu , PR is ready for review

[mcodescu]

👍