summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2020-10-01(proof-new) Preprocessing passes use proper interfaces to assertions pipeline...Andrew Reynolds
2020-10-01Make SygusSolver use sygus attributes directly (#5172)Andrew Reynolds
2020-09-30BitVector: Extend interface of setBit to set it to a specific value. (#5173)Aina Niemetz
2020-09-30FloatingPoint: Add utility functions for largest and smallest subnormal. (#5166)Aina Niemetz
2020-09-30Remove too strict assertion to allow for approximate models (#5168)Gereon Kremer
2020-09-30Add missing includes. (#5170)Gereon Kremer
2020-09-30Add strategy for nonlinear extension (#5160)Gereon Kremer
2020-09-30Dynamic allocation of equality engine for shared solver (#5152)Andrew Reynolds
2020-09-30(proof-new) Add the term conversion sequence generator (#5097)Andrew Reynolds
2020-09-29[proof-new] Adds a proof manager for prop engine (#5162)Haniel Barbosa
2020-09-29Fix bags headers (#5165)mudathirmahgoub
2020-09-29(proof-new) Add proof managers and eager gens to arith (#5159)Alex Ozdemir
2020-09-29(proof-new) Fixes for preprocess proof generator and proofs in assertion pipe...Andrew Reynolds
2020-09-29[proof-new] Adds a proof post processor for the Prop Engine (#5161)Haniel Barbosa
2020-09-29[proof-new] Updates to proof node updater (#5156)Haniel Barbosa
2020-09-29[proof-new] Adds a proof-producing CNF converter (#5137)Haniel Barbosa
2020-09-29Clean up nonlinear extension (#5149)Gereon Kremer
2020-09-28Reset assertions on resetAssertions (#5153)Andrew Reynolds
2020-09-28Add utilities for arith/proof_checker and build it (#5157)Alex Ozdemir
2020-09-28[proof-new] Removing spurious forward declaration in CnfStream (#5155)Haniel Barbosa
2020-09-28[proof-new] Adds a proof node hash function (#5154)Haniel Barbosa
2020-09-28Minor fixes to quantifiers proofs (#5151)Andrew Reynolds
2020-09-28[proof-new] Adds a proof manager for the SAT solver (#5140)Haniel Barbosa
2020-09-28Implement bags rewriter (#5132)mudathirmahgoub
2020-09-28Add new arithmetic BoundInference class (#5148)Gereon Kremer
2020-09-27Fix sygus quantifier elimination preprocess for multiple functions (#5130)Andrew Reynolds
2020-09-26Use inference manager for nl_solver (#5125)Gereon Kremer
2020-09-26Connect the shared solver to theory engine (#5103)Andrew Reynolds
2020-09-26Use original quantified formula for single invocation reconstruction (#5129)Andrew Reynolds
2020-09-25Restrict bvxnor to only allow two operands (was n-ary). (#5138)Aina Niemetz
2020-09-25Make sygus refinement step more robust to unevaluatable counterexamples (#5102)Andrew Reynolds
2020-09-25Cleaning and documenting cnf stream (#5134)Haniel Barbosa
2020-09-24SyGuS: Add default grammar for FP. (#5133)Aina Niemetz
2020-09-24 Function definition fmf preprocessing pass (#5064)Andrew Reynolds
2020-09-23Modify lemma vs fact policy for datatype equalities (#5115)Andrew Reynolds
2020-09-23Disable cegqi-bv when using sygus (#5124)Andrew Reynolds
2020-09-23Make IAND solver use inference manager. (#5126)Gereon Kremer
2020-09-23bv2int: new options for bvand translation (#5096)yoni206
2020-09-22Allow E-matching by default when strings are enabled (#5117)Andrew Reynolds
2020-09-22New C++ API: Catch and throw recoverable exception. (#5122)Aina Niemetz
2020-09-22FP: Use Assert instead of AlwaysAssert in traits::(pre|post)condition. (#5121)Aina Niemetz
2020-09-22Refactor Commands to use the Public API. (#5105)Abdalrhman Mohamed
2020-09-22Fix type issue with term formula removal (#5107)Andrew Reynolds
2020-09-22[Python API] Conversion to/from Unicode strings (#5120)Andres Noetzli
2020-09-22FP: Use Assert instead of PRECONDITION macro in converter. (#5119)Aina Niemetz
2020-09-22Add simple BV solver (#5065)Mathias Preiner
2020-09-22Add skeleton for theory of bags (multisets) (#5100)mudathirmahgoub
2020-09-22Fix compilation without LibPoly (#5118)Andres Noetzli
2020-09-22Add method to get Python object from constant value term in Python API (#5083)makaimann
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback