summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-23Missing format from #5112.Aina Niemetz
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
2020-09-22ICP-based solver for nonlinear arithmetic (#5017)Gereon Kremer
2020-09-21Require dumping in a dumping test (#5108)yoni206
2020-09-21(proof-new) Add the arrays proof checker (#5047)Andrew Reynolds
2020-09-20More flexible design for model manager distributed (#4976)Andrew Reynolds
2020-09-19Standardize equality engine notifications in sets (#5098)Andrew Reynolds
2020-09-18Fix assertion list for globally defined recursive functions (#5084)Andrew Reynolds
2020-09-18Add the shared solver (#4982)Andrew Reynolds
2020-09-18bv2int: quantifiers support (#5080)yoni206
2020-09-18Fix muzzled builds (#5093)Andres Noetzli
2020-09-18[proof-new] Proof utilities for normalizing clauses at the Node level (#5089)Haniel Barbosa
2020-09-18Logic exception for arrays indexed by arrays (#5073)Andrew Reynolds
2020-09-18[Strings] Fix extended equality rewriter (#5092)Andres Noetzli
2020-09-17(proof-new) Updates to proof node updater algorithm (#5088)Andrew Reynolds
2020-09-17(proof-new) Rewrites involving operators in term conversion proof generator (...Andrew Reynolds
2020-09-17(proof-new) Fixes for theory engine proof generator (#5087)Andrew Reynolds
2020-09-17[proof-new] Have mkScope agnostic to True assumptions (#5086)Haniel Barbosa
2020-09-17(cad-solver) Fix square-free-basis computation (#5085)Gereon Kremer
2020-09-17Reduce recursion in term formula removal (#5052)Andrew Reynolds
2020-09-17Use new inference manager in transcendental solver (#5022)Gereon Kremer
2020-09-17Do not allow to build Python bindings if building statically (#4784)Andrew V. Jones
2020-09-16Further standardization of datatypes (#5076)Andrew Reynolds
2020-09-16Dumping internal define-funs with no arguments (#5077)yoni206
2020-09-16Only rewrite replace_re(_all) if regexp is const (#5075)Andres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback