summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-05-15Merge branch 'stringsPf' into fix-eqproof3Haniel Barbosa
2020-05-15introducing search for building better transitivity proofsHaniel Barbosa
2020-05-15Shared term database is proof producing. Simplifications to TheoryEngine in p...ajreynol
2020-05-15Address review for pscajreynol
2020-05-15Do VSplit length conclusionajreynol
2020-05-15Unify checker for constant splitajreynol
2020-05-15Merge branch 'stringsPf' into fix-eqproof3Haniel Barbosa
2020-05-15Ipc robust to sym (do not overwrite first explanations)ajreynol
2020-05-15Fixajreynol
2020-05-15fixing cyclic proof issue with congruence + transitivityHaniel Barbosa
2020-05-15Formatajreynol
2020-05-15Equality engine interfaceajreynol
2020-05-15Formatajreynol
2020-05-15Normal form equality conflictsajreynol
2020-05-14Conflict case of N_UNIFYajreynol
2020-05-14Merge pull request #34 from HanielB/fix-eqproof3Andrew Reynolds
2020-05-14fixing double substitution in disequality issueHaniel Barbosa
2020-05-14Merge branch 'stringsPf' into fix-eqproof3Haniel Barbosa
2020-05-14adding commentHaniel Barbosa
2020-05-14Minorajreynol
2020-05-14Make SCOPE closure in pfee robust to mixtures of symmetric equalitiesajreynol
2020-05-14Formatajreynol
2020-05-14N_UNIFY splice constantsajreynol
2020-05-13Revertajreynol
2020-05-13Reorg length in conclusionajreynol
2020-05-13Length in conclusion for unified V-SPLITajreynol
2020-05-13Two more fixesajreynol
2020-05-13Moreajreynol
2020-05-13Remove attributeajreynol
2020-05-13Index vars, revert to explicit caching version for regexp unfoldajreynol
2020-05-13Fixes for reduction, duplicate literals in lemmas/conflicts, word checks.ajreynol
2020-05-13Unifyajreynol
2020-05-13Working towards unifiying checker and solverajreynol
2020-05-13More fixesajreynol
2020-05-13Merge pull request #33 from HanielB/fix-eqproof3Andrew Reynolds
2020-05-13fixing issues with internal disequalities and with cyclic proofsHaniel Barbosa
2020-05-13Merge branch 'stringsPf' into fix-eqproof3Haniel Barbosa
2020-05-13fixing reflHaniel Barbosa
2020-05-12Minorajreynol
2020-05-12Formatajreynol
2020-05-12Merge pull request #32 from HanielB/fix-eqproof3Andrew Reynolds
2020-05-12Merge branch 'stringsPf' into fix-eqproof3Haniel Barbosa
2020-05-12revertHaniel Barbosa
2020-05-12formattingHaniel Barbosa
2020-05-12generalizing congruence processingHaniel Barbosa
2020-05-12Update interfaceajreynol
2020-05-12Orienting for I_CONST_MERGEajreynol
2020-05-12Fixes for EXTF_EQ and I_CONST_MERGEajreynol
2020-05-12fixing handling of n-ary operatorsHaniel Barbosa
2020-05-12Reg exp unfold, more eq proofajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback