summaryrefslogtreecommitdiff
path: root/src/expr
AgeCommit message (Expand)Author
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
2020-06-18Improve memory management in Java bindings (#4629)Andres Noetzli
2020-06-16Update copyright headers.Aina Niemetz
2020-06-15(proof-new) Add quantifiers proof checker (#4593)Andrew Reynolds
2020-06-15(proof-new) Update proof node, add proof node algorithm utility file. (#4600)Andrew Reynolds
2020-06-12(proof-new) Term conversion proof generator utility (#4603)Andrew Reynolds
2020-06-11 (proof-new) Add lazy proof utility (#4589)Andrew Reynolds
2020-06-09(proof-new) Refactor skolemization (#4586)Andrew Reynolds
2020-06-08(proof-new) Add abstract proof generator class (#4574)Andrew Reynolds
2020-06-06Fix destruction order in NodeManager (#4578)Andres Noetzli
2020-06-05Datatypes with nested recursion are not handled in TheoryDatatypes unless opt...Andrew Reynolds
2020-06-05(proof-new) Updates to CDProof (#4565)Andrew Reynolds
2020-06-05(proof-new) Rename ProofSkolemCache to SkolemManager (#4556)Andrew Reynolds
2020-06-05Fix lifetime and copy issues with NodeDfsIterable (#4569)Andres Noetzli
2020-06-03(proof-new) Adding rules and proof checker for EUF (#4559)Haniel Barbosa
2020-06-03(proof-new) Adding rules and proof checker for Boolean reasoning (#4560)Haniel Barbosa
2020-06-03(proof-new) Add builtin proof checker (#4537)Andrew Reynolds
2020-06-01(proof-new) Proof step buffer utilities (#4533)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback