Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
* adapt gitignore for Intellij * remove old unused files * Fixed Haddock errors needed for the Haskell Intellij-plugin * fix haddock errors necessary for Intelliij Haskell plugin * different way of fixing haddock * Revert "Fixed Haddock errors" This reverts commit 71d30f4. * whole subterms squashed * Contradictions.hs * Goals.hs (void insertFormula) * Guarded.hs * LTerm.hs * Pretty.hs * Reduction.hs (insertFormula stuff) * Signature.hs (unsure what stFunSyms is...) * Simplify.hs (without freshOrdering) * System.hs (hasSubtermCycle) * Term.hs (elemNotBelowReducible) * Token.hs (opSubterm << ⊏) * Wellformedness.hs * towards a compiling version * reverting insertFormula change * a compiling version! * first subtermStore stuff * partially integrated subtermStore * add SubtermG * solve SubtermGoal * simpSubterms in Simplify.hs * reducibleFormula * somewhat finished left todo's are: - show a "trace found" (e.g. in SubtermTests --> WrongSplitSubterms) - show a message "no further proof possible" if reducible operators are left * removed todo * replace plainOpenGoals by openGoals and add minimal test file * little fix regarding duplicate goals (one solved and one unsolved) * advanced freshOrdering (using subterms) * little fix * Natural Number Cherry Picking * Natural Number compiling version * minor adaptions * Term Parser: moving from "Parser (Term l)" to "Parser LNTerm" * small tidy-up * re-enabled NatSubtermD in splitSubterm * proper usage of splitting subterms * heuristics adapted * implemented nat-cycle algorithm * little parser fix * Parser don't know fix * maude parser fix * removed debugging * fixed sort of tone * debugging output kills performance (400%) * removing already false negative subterms * fix such that non-splits do not appear in the goals * arityOneDeduction * enhanced freshOrdering rule ##careful!!! this will impact the regression tests!!! * fixed forgotten persistent fact exclusion * fixed serious bug in the enhanced freshOrdering * advanced partialAtomValuation for subterms * Fix parser merge * partial evaluation of CR-rule S_neg * deduce KU(%nat) automatically like done with KU($pub) * Better detection of injective facts * detection of non-changing and monotonic positions * monotonic injective facts! (pairs are a todo) * s vs t bugfix * (decreasing, strict vs non-strict) rework of the injective fact monotonicity TODO: properly test it * uncomment non-increasing stuff as models diverge with it * bugfix concerning detection of monotonicity with pairs * fixed looping bug for non-strictly increasing stuff **and: now, no subterms are introduced by monotonicity** * sanity kill whenever right side of a subterm has reducible operator on top [just for the paper] * Regression updates * Parse proofs with subterm * Move addition of less relation from injective fact as looping simplifier * Docker fixes * fix compiler error * fixing parser errors but creating other ones * parser sorting checks * porting natCheck to diff * fix maude merging error * removing freshOrdering if it's a sapic file because that makes it slower see opc_ua_secure_conversation.spthy * Removing nat intruder rules as it is constructed directly in NatConstrRule * fix download proof and reimport error and diff quantifier sort error * change advanced fresh order to only insert `<` and never a disjunction (and check that the equalities are impossible) * `System>safePartialAtomValuation` now uses `SubtermStore>isTrueFalse` as well * comment changes * removing outdated TODO's * apply addNonInjectiveFactInstances non-looping * updating the regression tests to be the ones from develop * some variable renaming that killed the regression test performance * re-enabled freshOrdering for sapic - including actions in detection * added missing regression test to case-studies-regression which was produced by the makefile * fixing bug in freshOrder * added natural numbers to regression tests * fixing heavy observational equivalence bug * Yellow Color! * yellow diff fixes * update regression tests * updated regression tests for merged changes from develop * Remove remnant debug trace from Message Derivation checks. * Remove unnecessary Debug.Trace include * remove unnecessary Debug.Trace import. * expand comment on DiffUnfinishable in code * adding small tests for subterms and numbers * make fst/snd by default Constructor again, instead of Destructor. * minor cleanup changes, as discussed in PR * remove unnecessary (commented) imports, typo fixes * fixed runtime issue in diff mode * trying to fix issue with nat vars * fixing timeout for derivation checks * Better messages for derivation checks * fix timeout, again... * fix output: don't show empty warning * fix warnings * fix more warnings * missing regression test file * Fixed Makefile to include xor-diff target. * Update ALL regression targets. --------- Co-authored-by: Charlie Jacomme <jacomme@crans.org> Co-authored-by: Philip Lukert <c01phlu@colossus06.cispa.saarland> Co-authored-by: Ralf Sasse <ralf.sasse@gmail.com> Co-authored-by: Jannik Dreier <jannik.dreier@loria.fr>
- Loading branch information
5 people
committed
Jul 31, 2023
1 parent
a35488c
commit c704b61