summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-08-02Merge branch 'master' into fixAsanInteractiveShellBlackfixAsanInteractiveShellBlackAndrew Reynolds
2020-08-02Fix ASan failure in interactive_shell_blackAndres Noetzli
2020-08-01Ensure strict length constraint for decompose rule (#4821)Andres Noetzli
2020-08-01Add methods for constructing datatype types from NodeManager (#4823)Andrew Reynolds
2020-08-01Ensure that we only find '.a's when building statically (#4785)Andrew V. Jones
2020-08-01Fix component contains for splicing due to substring. (#4705)Andrew Reynolds
2020-07-31Add SyGuS Python API (#4812)yoni206
2020-07-31Split listener classes from SmtEngine (#4816)Andrew Reynolds
2020-07-30Standardize explanations in arrays (#4804)Andrew Reynolds
2020-07-30Python API: Add support for sequences (#4757)Andres Noetzli
2020-07-30Cad implementation (#4774)Gereon Kremer
2020-07-30Adds the interface for the CAD-based arithmetic solver. (#4773)Gereon Kremer
2020-07-30When linking Editline, use 'pkg-config' to correctly find the link-time depen...Andrew V. Jones
2020-07-30Fix null case for sygus printing (#4793)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-28fixing issue #4808. (#4810)Ying Sheng
2020-07-28Remove arrays lazy rintro option (#4806)Andrew Reynolds
2020-07-28Replace Expr with Node in Term/Op (#4781)Andres Noetzli
2020-07-28Fix regular expression delta for complement (#4765)Andrew Reynolds
2020-07-28Supporting seq.nth (#4723)yoni206
2020-07-28Interpolation: Add interface for SyGuS interpolation module (step3) (#4726)Ying Sheng
2020-07-28Use lemma property enum for OutputChannel::lemma (#4755)Andrew Reynolds
2020-07-27(proof-new) Proof production for term formula removal (#4687)Andrew Reynolds
2020-07-27(proof-new) Arithmetic operator elim proof producing (#4783)Andrew Reynolds
2020-07-27Consider negation's proof before triggering arith pfs. (#4776)Alex Ozdemir
2020-07-21GH Actions: Cancel builds on push, remove redundant mac OS build. (#4779)Aina Niemetz
2020-07-21Support uninterpreted constants in the evaluator (#4777)Andrew Reynolds
2020-07-21Preparations for a CAD-based arithmetic solver (#4762)Gereon Kremer
2020-07-20Fix a deadlock in the signature tests. (#4772)Alex Ozdemir
2020-07-17Improving equality engine tracing (#4770)Haniel Barbosa
2020-07-17(proof-new) Proof recording for assertions pipeline (#4766)Andrew Reynolds
2020-07-17Enumerate shapes feature in fast sygus enumerator (#4742)Andrew Reynolds
2020-07-17Add NodeManagerScopes to fix use-after-free issues (#4768)Andres Noetzli
2020-07-17Replace options listener infrastructure (#4764)Andrew Reynolds
2020-07-17Support for using 'libedit' over 'readline' #4571 (#4579)Andrew V. Jones
2020-07-17(proof-new) Updates to strings core solver (#4642)Andrew Reynolds
2020-07-17Add option manager and simpler option listener (#4745)Andrew Reynolds
2020-07-17Integration of libpoly (#4679)Gereon Kremer
2020-07-16Fix EqProof to ProofNode conversion (#4760)Haniel Barbosa
2020-07-16(proof-new) Implements the conversion between EqProof and ProofNode (#4756)Haniel Barbosa
2020-07-16Resource manager cleanup (#4732)Gereon Kremer
2020-07-16Split abstract values utility from SmtEngine (#4754)Andrew Reynolds
2020-07-16Make ExtTheory a utility and not a member of Theory (#4753)Andrew Reynolds
2020-07-16Remove cumulative time limits and cpu time limits (#4711)Gereon Kremer
2020-07-15Fixes memory leak when an exception goes through runCvc4(). (Fixes #4590) (#4...Gereon Kremer
2020-07-15(proof-new) Adding API for converting EqProof into ProofNode (#4747)Haniel Barbosa
2020-07-15Use Nodes for SmtEngine assertions (#4752)Andres Noetzli
2020-07-15Split abduction solver from SmtEngine (#4733)Andrew Reynolds
2020-07-15Use TypeNode in UninterpretedConstant (#4748)Andres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback