summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2020-07-20Fix 4771fix4771Andres Noetzli
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
2020-07-15Add missing header (Fixes #4743) (#4749)Gereon Kremer
2020-07-15Simplify entailment check interface (#4744)Andrew Reynolds
2020-07-14Make use of options in setDefaults more consistent (#4729)Andrew Reynolds
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-13Debug instantiations output (#4739)Andrew Reynolds
2020-07-13Minor refactoring of subsolver initialization (#4731)Andrew Reynolds
2020-07-13Fix caching in TheoryEngine::getExplanation() (#4736)Andres Noetzli
2020-07-13Fix options messages that were inverted (#4734)Haniel Barbosa
2020-07-13Use TypeNode/Node in ArrayStoreAll (#4728)Andres Noetzli
2020-07-13Fix type comparisons involving pointer. (#4738)Andrew Reynolds
2020-07-13Fix whitespace issue in instantiations output. (#4737)Andrew Reynolds
2020-07-13 (proof-new) SMT Preprocess proof generator (#4708)Andrew Reynolds
2020-07-13 User-facing print debug option for sygus candidates (#4720)Andrew Reynolds
2020-07-13Statistics on instantiations per quantified formula. (#4719)Andrew Reynolds
2020-07-13Implement --tlimit for windows (#4716)Gereon Kremer
2020-07-12Add support for string/sequence update (#4725)Andrew Reynolds
2020-07-12Remove ExprSequence (#4724)Andres Noetzli
2020-07-11Cache explanations in TheoryEngine::getExplanation (#4722)Andrew Reynolds
2020-07-11Changing bv_to_int options (#4721)yoni206
2020-07-10Adding test for whether a kind is n-ary (#4718)Haniel Barbosa
2020-07-10Add support for printing 'get-abduct' in verbose mode (#4710)Andrew V. Jones
2020-07-10(proof-new) Add ONCE and FIXPOINT modes for term conversion proof generator (...Andrew Reynolds
2020-07-10(proof-new) Update Theory interface for proof-new (#4648)Andrew Reynolds
2020-07-10Always Update Git information when rebuilding (#4696)Andres Noetzli
2020-07-10Front end support for integer AND (#4717)Andrew Reynolds
2020-07-10[Interpolation] Add interface for SyGuS interpolation module (#4677)Ying Sheng
2020-07-09Ensure legal elimination for witness rewrite (#4688)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback