summaryrefslogtreecommitdiff
path: root/src/expr
AgeCommit message (Expand)Author
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
2020-07-06Front end support for sequences (#4690)Andrew Reynolds
2020-07-02Remove SWIG bindings (#4683)Andres Noetzli
2020-07-02 (proof-new) Updates to skolem manager interface (#4664)Andrew Reynolds
2020-07-02(proof-new) Proof rule checkers run on skolem forms (#4660)Andrew Reynolds
2020-07-02(proof-new) Proof node updater (#4647)Andrew Reynolds
2020-06-29Make ExprManager constructor private (#4669)Andres Noetzli
2020-06-28Proof Rules and Checker for Arithmetic (#4665)Alex Ozdemir
2020-06-25fix and test (#4658)yoni206
2020-06-23(proof-new) Updates to proof node manager (#4617)Andrew Reynolds
2020-06-19Use traversal iterators in IntToBv (#4169)Alex Ozdemir
2020-06-19Add Match utility function. (#4632)Abdalrhman Mohamed
2020-06-19(proof-new) CDProof inherits from ProofGenerator (#4622)Andrew Reynolds
2020-06-19Convert more uses of strings to words (#4584)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback