summaryrefslogtreecommitdiff
path: root/src/expr
AgeCommit message (Expand)Author
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
2020-07-28Replace Expr with Node in Term/Op (#4781)Andres Noetzli
2020-07-27(proof-new) Proof production for term formula removal (#4687)Andrew Reynolds
2020-07-17Add NodeManagerScopes to fix use-after-free issues (#4768)Andres Noetzli
2020-07-17(proof-new) Updates to strings core solver (#4642)Andrew Reynolds
2020-07-15Use TypeNode in UninterpretedConstant (#4748)Andres Noetzli
2020-07-14Remove sygus print callback (#4727)Andrew Reynolds
2020-07-14(proof-new) Skeleton proof support in the Rewriter (#4730)Andrew Reynolds
2020-07-14Use TypeNode in EmptySet (#4740)Andres Noetzli
2020-07-13Use TypeNode/Node in ArrayStoreAll (#4728)Andres Noetzli
2020-07-13Fix type comparisons involving pointer. (#4738)Andrew Reynolds
2020-07-13 (proof-new) SMT Preprocess proof generator (#4708)Andrew Reynolds
2020-07-12Add support for string/sequence update (#4725)Andrew Reynolds
2020-07-12Remove ExprSequence (#4724)Andres Noetzli
2020-07-10Adding test for whether a kind is n-ary (#4718)Haniel Barbosa
2020-07-10(proof-new) Add ONCE and FIXPOINT modes for term conversion proof generator (...Andrew Reynolds
2020-07-07Transfer ownership of internal Options from NodeManager to SmtEngine (#4682)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback