cvc5.git
2020-10-03 Aina Niemetzsygus-inst: Add more special BV values. (#5191)
2020-10-03 Mathias PreinerFix CI builds and add cancel workflow.
2020-10-03 Andrew ReynoldsFix theory white unit test (#5194)
2020-10-03 Andrew ReynoldsStandardization of Theory (#5181)
2020-10-02 Andrew ReynoldsMinor simplifications to substitution map class (#5180)
2020-10-02 Andrew Reynolds(proof-new) Fixes for theory preprocessing proofs ...
2020-10-02 Andrew Reynolds(proof-new) Make shared solver proof producing (#5169)
2020-10-02 Gereon KremerAllow for theory combination of strings with nonlinear...
2020-10-02 Andrew ReynoldsDecouple modules from TheoryArithPrivate (#5184)
2020-10-02 Alex Ozdemir(proof-new) New proofs in arith::Constraint::externalEx...
2020-10-02 Alex OzdemirRemove duplicate declarations in th_bv.plf (#5183)
2020-10-02 Aina NiemetzSyGuS: Add min/max (sub)normal constants to FP default...
2020-10-01 Andrew Reynolds(proof-new) Make arrays proof producing (#5112)
2020-10-01 Mathias PreinerAdd additional ground terms to SyGuS instantiation...
2020-10-01 Andrew ReynoldsUpdate theory of arithmetic to standard check (#5178)
2020-10-01 Aina NiemetzFloatingPoint: Add utility functions for largest and...
2020-10-01 Gereon KremerAllow to use the initial assignment for CAD (#5177)
2020-10-01 Andrew Reynolds(proof-new) Preprocessing passes use proper interfaces...
2020-10-01 Andrew ReynoldsMake SygusSolver use sygus attributes directly (#5172)
2020-10-01 Mathias PreinerAdd GH action to cancel previous pending/running CI...
2020-10-01 Aina NiemetzBitVector: Extend interface of setBit to set it to...
2020-09-30 Aina NiemetzFloatingPoint: Add utility functions for largest and...
2020-09-30 Gereon KremerRemove too strict assertion to allow for approximate...
2020-09-30 Gereon KremerAdd missing includes. (#5170)
2020-09-30 Gereon KremerAdd strategy for nonlinear extension (#5160)
2020-09-30 Andrew ReynoldsDynamic allocation of equality engine for shared solver...
2020-09-30 Andrew Reynolds(proof-new) Add the term conversion sequence generator...
2020-09-29 Haniel Barbosa[proof-new] Adds a proof manager for prop engine (...
2020-09-29 mudathirmahgoubFix bags headers (#5165)
2020-09-29 Alex Ozdemir(proof-new) Add proof managers and eager gens to arith...
2020-09-29 Andrew Reynolds(proof-new) Fixes for preprocess proof generator and...
2020-09-29 Haniel Barbosa[proof-new] Adds a proof post processor for the Prop...
2020-09-29 Haniel Barbosa[proof-new] Updates to proof node updater (#5156)
2020-09-29 Haniel Barbosa[proof-new] Adds a proof-producing CNF converter (...
2020-09-29 Gereon KremerClean up nonlinear extension (#5149)
2020-09-29 Andrew ReynoldsReset assertions on resetAssertions (#5153)
2020-09-29 Alex OzdemirAdd utilities for arith/proof_checker and build it...
2020-09-29 Haniel Barbosa[proof-new] Removing spurious forward declaration in...
2020-09-29 Haniel Barbosa[proof-new] Adds a proof node hash function (#5154)
2020-09-29 Andrew ReynoldsDisable regression that is timing out (#5142)
2020-09-28 Andrew ReynoldsMinor fixes to quantifiers proofs (#5151)
2020-09-28 Haniel Barbosa[proof-new] Adds a proof manager for the SAT solver...
2020-09-28 mudathirmahgoubImplement bags rewriter (#5132)
2020-09-28 Gereon KremerAdd new arithmetic BoundInference class (#5148)
2020-09-27 Andrew ReynoldsFix sygus quantifier elimination preprocess for multipl...
2020-09-26 Gereon KremerUse inference manager for nl_solver (#5125)
2020-09-26 Andrew ReynoldsConnect the shared solver to theory engine (#5103)
2020-09-26 Andrew ReynoldsUse original quantified formula for single invocation...
2020-09-26 Aina NiemetzRestrict bvxnor to only allow two operands (was n-ary...
2020-09-25 Andrew ReynoldsMake sygus refinement step more robust to unevaluatable...
2020-09-25 Haniel BarbosaCleaning and documenting cnf stream (#5134)
2020-09-24 Aina NiemetzSyGuS: Add default grammar for FP. (#5133)
2020-09-24 Andrew Reynolds Function definition fmf preprocessing pass (#5064)
2020-09-24 Andrew ReynoldsModify lemma vs fact policy for datatype equalities...
2020-09-23 Andrew ReynoldsDisable cegqi-bv when using sygus (#5124)
2020-09-23 Gereon KremerMake IAND solver use inference manager. (#5126)
2020-09-23 Aina NiemetzMissing format from #5112.
2020-09-23 yoni206bv2int: new options for bvand translation (#5096)
2020-09-23 Andrew ReynoldsAllow E-matching by default when strings are enabled...
2020-09-23 Aina NiemetzNew C++ API: Catch and throw recoverable exception...
2020-09-23 Aina NiemetzFP: Use Assert instead of AlwaysAssert in traits::...
2020-09-23 Abdalrhman... Refactor Commands to use the Public API. (#5105)
2020-09-23 Andrew ReynoldsFix type issue with term formula removal (#5107)
2020-09-23 Andres Noetzli[Python API] Conversion to/from Unicode strings (#5120)
2020-09-22 Aina NiemetzFP: Use Assert instead of PRECONDITION macro in convert...
2020-09-22 Mathias PreinerAdd simple BV solver (#5065)
2020-09-22 mudathirmahgoubAdd skeleton for theory of bags (multisets) (#5100)
2020-09-22 Andres NoetzliFix compilation without LibPoly (#5118)
2020-09-22 makaimannAdd method to get Python object from constant value...
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and...
2020-09-22 Gereon KremerICP-based solver for nonlinear arithmetic (#5017)
2020-09-22 yoni206Require dumping in a dumping test (#5108)
2020-09-21 Andrew Reynolds(proof-new) Add the arrays proof checker (#5047)
2020-09-20 Andrew ReynoldsMore flexible design for model manager distributed...
2020-09-19 Andrew ReynoldsStandardize equality engine notifications in sets ...
2020-09-18 Andrew ReynoldsFix assertion list for globally defined recursive funct...
2020-09-18 Andrew ReynoldsAdd the shared solver (#4982)
2020-09-18 yoni206bv2int: quantifiers support (#5080)
2020-09-18 Andres NoetzliFix muzzled builds (#5093)
2020-09-18 Haniel Barbosa[proof-new] Proof utilities for normalizing clauses...
2020-09-18 Andrew ReynoldsLogic exception for arrays indexed by arrays (#5073)
2020-09-18 Andres Noetzli[Strings] Fix extended equality rewriter (#5092)
2020-09-18 Andrew Reynolds(proof-new) Updates to proof node updater algorithm...
2020-09-18 Andrew Reynolds(proof-new) Rewrites involving operators in term conver...
2020-09-17 Andrew Reynolds(proof-new) Fixes for theory engine proof generator...
2020-09-17 Haniel Barbosa[proof-new] Have mkScope agnostic to True assumptions...
2020-09-17 Gereon Kremer(cad-solver) Fix square-free-basis computation (#5085)
2020-09-17 Andrew ReynoldsReduce recursion in term formula removal (#5052)
2020-09-17 Gereon KremerUse new inference manager in transcendental solver...
2020-09-17 Andrew V. JonesDo not allow to build Python bindings if building stati...
2020-09-17 Andrew ReynoldsFurther standardization of datatypes (#5076)
2020-09-17 yoni206Dumping internal define-funs with no arguments (#5077)
2020-09-16 Andres NoetzliOnly rewrite replace_re(_all) if regexp is const (...
2020-09-16 Abdalrhman... Dump commands in internal code using command printing...
2020-09-16 Andrew ReynoldsAdd buffered inference manager to TheorySep (#5038)
2020-09-16 Haniel Barbosa[proof-new] Adds Lazy CDProof chain data-structure...
2020-09-16 Andrew ReynoldsRefactor collectModelInfo in TheoryArith (#5027)
2020-09-16 yoni206bv2int: support models in tests (#5068)
2020-09-16 Haniel Barbosa[proof-new] Extending eqproof conversion to HO congruen...
2020-09-16 Haniel Barbosa[proof-new] Resolution rules and checkers (#5070)
next