summaryrefslogtreecommitdiff
path: root/src/expr
AgeCommit message (Expand)Author
2020-10-13(proof-new) Simplifications for proof rule checker interface (#5244)Andrew Reynolds
2020-10-13(proof-new) New rules for Booleans (#5243)Andrew Reynolds
2020-10-13(proof-new) Change merge policy for proof node updater (#5242)Andrew Reynolds
2020-10-11SyGuS instantiation modes (#5228)Mathias Preiner
2020-10-08(proof-new) Add lazy proof set utility (#5221)Andrew Reynolds
2020-10-08(proof-new) Fixes and improvements for smt proof postprocessor (#5197)Andrew Reynolds
2020-10-06(proof-new) Allow null proofs from generators in LazyCDProof (#5196)Andrew Reynolds
2020-10-05Remove subtyping for sets (#5205)mudathirmahgoub
2020-10-04Remove subtyping for sets theory (#5179)mudathirmahgoub
2020-10-02(proof-new) Fixes for theory preprocessing proofs (#5171)Andrew Reynolds
2020-09-30(proof-new) Add the term conversion sequence generator (#5097)Andrew Reynolds
2020-09-29[proof-new] Updates to proof node updater (#5156)Haniel Barbosa
2020-09-28[proof-new] Adds a proof node hash function (#5154)Haniel Barbosa
2020-09-28Minor fixes to quantifiers proofs (#5151)Andrew Reynolds
2020-09-28[proof-new] Adds a proof manager for the SAT solver (#5140)Haniel Barbosa
2020-09-23Modify lemma vs fact policy for datatype equalities (#5115)Andrew Reynolds
2020-09-22Add skeleton for theory of bags (multisets) (#5100)mudathirmahgoub
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
2020-09-21(proof-new) Add the arrays proof checker (#5047)Andrew Reynolds
2020-09-17(proof-new) Updates to proof node updater algorithm (#5088)Andrew Reynolds
2020-09-17(proof-new) Rewrites involving operators in term conversion proof generator (...Andrew Reynolds
2020-09-17[proof-new] Have mkScope agnostic to True assumptions (#5086)Haniel Barbosa
2020-09-16[proof-new] Adds Lazy CDProof chain data-structure (#5060)Haniel Barbosa
2020-09-16[proof-new] Resolution rules and checkers (#5070)Haniel Barbosa
2020-09-15[proof-new] A simple proof generator for buffered proof steps (#5069)Haniel Barbosa
2020-09-11(proof-new) Handle mismatched assumptions in proof equality engine during mkS...Andrew Reynolds
2020-09-11(proof-new) Use deep copy for final lemma step in proof equality engine (#5013)Andrew Reynolds
2020-09-09(proof-new) Minor changes to proof node updater (#5011)Andrew Reynolds
2020-09-02(proof-new) Improve debugging infrastructure for open proofs (#4984)Andrew Reynolds
2020-09-02Remove #line directives from generated files. (#5005)Gereon Kremer
2020-09-02(proof-new) Updates to builtin proof checker (#4962)Andrew Reynolds
2020-09-02(proof-new) Add proof support in TheoryUF (#5002)Andrew Reynolds
2020-09-02(proof-new) Make term conversion proof generator optionally term-context sens...Andrew Reynolds
2020-08-31Basic proof support in inference manager (#4975)Andrew Reynolds
2020-08-28(proof-new) More term context utilities. (#4912)Andrew Reynolds
2020-08-25Replace Expr-level datatype with Node-level DType (#4875)Andrew Reynolds
2020-08-18(proof-new) Theory preprocessor proof producing (#4807)Andrew Reynolds
2020-08-18(proof-new) Callbacks for term-context-sensitive terms (#4842)Andrew Reynolds
2020-08-15(proof-new) Add the strings proof checker (#4858)Andrew Reynolds
2020-08-12(proof-new) Improve robustness of CONG rule (#4882)Andrew Reynolds
2020-08-12(proof-new) Improve interfaces to proof generators (#4803)Andrew Reynolds
2020-08-12(proof-new) Witness form proof generator (#4782)Andrew Reynolds
2020-08-11Final preparations for changing API to use the Node-level datatype (#4863)Andrew Reynolds
2020-08-11(proof-new) Extensions to proof checker interface (#4857)Andrew Reynolds
2020-08-07Move datatype index constant to its own file (#4859)Andrew Reynolds
2020-08-06Updates not related to creation for eliminating Expr-level datatype (#4838)Andrew Reynolds
2020-08-02Updates to dtype constructor in preparation for eliminating Expr-level dataty...Andrew Reynolds
2020-08-01Add methods for constructing datatype types from NodeManager (#4823)Andrew Reynolds
2020-07-30(proof-new) Stream output for ProofNode (#4789)Andrew Reynolds
2020-07-29(proof-new) Fixes for getFreeAssumptions (#4802)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback