GitHub PushEvent at 2014-11-24 16:34:58
Repository: gapt
Actor: gisellemnr
Payload: {"shas":[["caa1f117f7cc61ba821748eeeecbf7f0f87393af","c488743f76fd6bd0ae65864e7b9bd38fdf5a6bc3@85d21ef8-add0-11de-ae77-5bfb9c5a3f34","Set FOLApp, FOLAbs protected.\nHad to remove some debugging pretty-printing code from TreeGrammarDecomposition in order to do so.\n\n\ngit-svn-id: https://gapt.googlecode.com/svn/trunk@2331 85d21ef8-add0-11de-ae77-5bfb9c5a3f34","fraini",false],["cf3517fa4baaedd145a3702c97ad200484ac9ab4","ea7692f0ed5eff8231bf59dc3398bed13c9bc5f3@gmail.com","Fixing error on renaming\n\nWhen the maxVariant in the backlist is not a\nVariantSymbol, it can be of any other type, not\nonly StringSymbol.\n\ngit-svn-id: https://gapt.googlecode.com/svn/trunk@2332 85d21ef8-add0-11de-ae77-5bfb9c5a3f34","giselle.mnr@gmail.com",false],["f27d7a0ad634ce6cb18b24df761e12e8c5ec0c3b","ea7692f0ed5eff8231bf59dc3398bed13c9bc5f3@gmail.com","Modification to the testCutIntro script\n\nThe calls were simplified and the logging is now\nconcentrated in one place.\n\ngit-svn-id: https://gapt.googlecode.com/svn/trunk@2333 85d21ef8-add0-11de-ae77-5bfb9c5a3f34","giselle.mnr@gmail.com",false],["6889fddf547d9ad62e042624f533c1330e62388b","ea7692f0ed5eff8231bf59dc3398bed13c9bc5f3@gmail.com","Organizing cut-introduction code\n\nThe actual code that executes the cut-introduction\nalgorithm is inside private methods and three\npublic methods were created, one for each case:\n- one_cut_one_quantifier\n- one_cut_many_quantifiers\n- many_cuts_one_quantifier\n\nThe object NCutIntroduction was deleted and its\nmethods were moved to CutIntroduction.\n\nConflicts:\n\tsource/algorithms/cutIntroduction/src/main/scala/at/logic/algorithms/cutIntroduction/CutIntroduction.scala\n\ngit-svn-id: https://gapt.googlecode.com/svn/trunk@2334 85d21ef8-add0-11de-ae77-5bfb9c5a3f34","giselle.mnr@gmail.com",false],["23e3c805f39bccfa466b9018f00d1477008db9ce","ea7692f0ed5eff8231bf59dc3398bed13c9bc5f3@gmail.com","Adapting cut-introduction tests to the new methods\n\nAlso added a comment regarding the format of the log.\n\ngit-svn-id: https://gapt.googlecode.com/svn/trunk@2335 85d21ef8-add0-11de-ae77-5bfb9c5a3f34","giselle.mnr@gmail.com",false],["6d28decc0bbe37f1cd8d9e747ac14d9429a9a445","ea7692f0ed5eff8231bf59dc3398bed13c9bc5f3@gmail.com","Removing a documentation comment\n\nPrivate methods don't need documentation.\n\ngit-svn-id: https://gapt.googlecode.com/svn/trunk@2336 85d21ef8-add0-11de-ae77-5bfb9c5a3f34","giselle.mnr@gmail.com",false],["059a9e51cf4bdd11c410e4c501a423b4dc2e4529","ea7692f0ed5eff8231bf59dc3398bed13c9bc5f3@gmail.com","Removing Constraints package\n\nWith the new implementation of cut-introduction\nthere is no need for constraints anymore.\nAlso adapting the help text to the new functions.\n\ngit-svn-id: https://gapt.googlecode.com/svn/trunk@2337 85d21ef8-add0-11de-ae77-5bfb9c5a3f34","giselle.mnr@gmail.com",false],["69cef1c4a712a780f61bf260d00fda54bacd8643","ea7692f0ed5eff8231bf59dc3398bed13c9bc5f3@gmail.com","Correcting the size of the smallest grammar\n\nOn the method for cut-introduction using maxsat, a\nlist of grammars is returned because of the\ncurrent implementation that supports only grammars\nof the type U o S. Since the method needs more\ngeneral grammars, i.e., U o S1 o ... o Sn, this is\nachieved by having a list of simpler grammars.\nConsequently the computation of the size of these\ngrammars needs some adaptation.\n\ngit-svn-id: https://gapt.googlecode.com/svn/trunk@2338 85d21ef8-add0-11de-ae77-5bfb9c5a3f34","giselle.mnr@gmail.com",false],["6f67c45931ec3a95e8c328625b99d17e7726cffa","ea7692f0ed5eff8231bf59dc3398bed13c9bc5f3@gmail.com","Fixing test script for cut-introduction\n\ngit-svn-id: https://gapt.googlecode.com/svn/trunk@2339 85d21ef8-add0-11de-ae77-5bfb9c5a3f34","giselle.mnr@gmail.com",false],["453d82b15279f0ae70bb6b7c4d0a9eeb93a5c4cb","14b411be59ed7ad577cfffa4d65d71b140dee865@gmail.com","LK Equality rules now have a solid foundation grounded in positions. The existing constructors have been modified to use position logic and check for correctness. Additionally, I've added macro rules that automatically choose the right version of an equality rule (i.e. EquationLeft1 or EquationLeft2) and can insert several rules at once if more than one term is exchanged. Several algorithms have been adjusted to use these macro rules in lieu of the elementary equality rules since there are inferences in some of our tests and proof data that don't correspond to single rules.\n\n\ngit-svn-id: https://gapt.googlecode.com/svn/trunk@2340 85d21ef8-add0-11de-ae77-5bfb9c5a3f34","szivota@gmail.com",false],["0a5993cc44de4674bdffd514c074fda914d05780","b95b3fc12d2fb0d36b80ce477c7eb7535c072350@gmail.com","Load resources using the classloader, not hard-coded paths.\n\nThis allows the tests to be run in IntelliJ.\n\n\ngit-svn-id: https://gapt.googlecode.com/svn/trunk@2341 85d21ef8-add0-11de-ae77-5bfb9c5a3f34","2b7e15@gmail.com",false],["73b2b195f08e2954589b34df18b0270e88cfd50b","b95b3fc12d2fb0d36b80ce477c7eb7535c072350@gmail.com","Add missing file from last commit.\n\n\ngit-svn-id: https://gapt.googlecode.com/svn/trunk@2342 85d21ef8-add0-11de-ae77-5bfb9c5a3f34","2b7e15@gmail.com",false],["7079bef0a1c5900b5d405ca97bf0bdf0befa0da5","b95b3fc12d2fb0d36b80ce477c7eb7535c072350@gmail.com","Fix bitrot in array_init example.\n\ngit-svn-id: https://gapt.googlecode.com/svn/trunk@2343 85d21ef8-add0-11de-ae77-5bfb9c5a3f34","2b7e15@gmail.com",false],["2778002c2f0f5eb46f70380c61cb1fd80e672285","ea7692f0ed5eff8231bf59dc3398bed13c9bc5f3@gmail.com","Adding gitignore file.","Giselle Reis",true],["a2156fa2ada6e949750f78bc74fdd3d5a01cf412","ea7692f0ed5eff8231bf59dc3398bed13c9bc5f3@gmail.com","Removing println from StandartClauseSet.","Giselle Reis",true],["c0bf214d77ac4dec22de7bc9bc2e3ad5ba4f4ab9","ea7692f0ed5eff8231bf59dc3398bed13c9bc5f3@gmail.com","Removing logging\n\nThe logging mechanism, although useful, is being\nin my opinion overly used in gapt. We shouldn't\nuse logging for debugging, and we shouldn't leave\ndebugging lines in the main repository code. Also,\nmaking a class extend yet another interface is\nreally overloading its responsabilites and the\ncode is often harder to read with all the\ndebugging lines around. Another reason I can think\nof for removing the logging from all these files\nis the fact that we either need to keep a very\nlong (and constantly needing updates) log4j file\nor we live with its warning messages.\nFor running the cut-introduction experiments, the\nonly logging that is left is the one in the test\nscript itself, and no other if I can help it.","Giselle Reis",true],["053cf65606b1e01b6be6a7ad71073926e4e13d3c","ea7692f0ed5eff8231bf59dc3398bed13c9bc5f3@gmail.com","Organizing cut-introduction code\n\nThe actual code that executes the cut-introduction\nalgorithm is inside private methods and three\npublic methods were created, one for each case:\n- one_cut_one_quantifier\n- one_cut_many_quantifiers\n- many_cuts_one_quantifier\n\nThe object NCutIntroduction was deleted and its\nmethods were moved to CutIntroduction.","Giselle Reis",true]],"size":17,"ref":"refs/heads/experiments","head":"053cf65606b1e01b6be6a7ad71073926e4e13d3c"}