cvc5.git
2020-12-15 Andrew ReynoldsConsolidate basic sygus utilities regarding sygus conje...
2020-12-15 Andrew ReynoldsFix datatypes compute ground value (#5671)
2020-12-15 Andrew ReynoldsRemove bv divide by zero option (#5672)
2020-12-15 Gereon KremerAdd getters to retrieve constants from api::Term (...
2020-12-14 Haniel Barbosa[proof-new] Making the CDCL(T) Minisat proof producing...
2020-12-14 Haniel Barbosa[proof-new] Make prop engine proof producing (#5667)
2020-12-14 Andrew ReynoldsProperly implement datatype selector triggers (#5624)
2020-12-14 Haniel Barbosa[proof-new] Updating interfaces between prop engine...
2020-12-14 Andrew Reynolds(proof-new) Add bound variable manager (#5655)
2020-12-14 Andrew ReynoldsFix and improve evaluator (#5563)
2020-12-14 Andrew ReynoldsFix SAT-context dependent issue in strings preregistrat...
2020-12-12 Andrew ReynoldsFlush statistics through NodeManager in SmtEngine ...
2020-12-11 yoni206bv-to-int: new tests from an issue (#5654)
2020-12-11 Haniel Barbosa [proof-new] Updating theory proxy to new proof infrast...
2020-12-11 Andrew ReynoldsFix length assumption for deq norm emp rule (#5623)
2020-12-10 Gereon KremerRefactor KindMap (#5646)
2020-12-10 Aina Niemetzgoogle test: expr: Migrate node_algorithm_black. (...
2020-12-10 Andrew ReynoldsRefactor regressions (#5639)
2020-12-10 Aina Niemetzgoogle test: expr: Migrate kind_black. (#5634)
2020-12-10 Gereon KremerFixed a bunch of clang warnings. (#5637)
2020-12-09 Aina NiemetzFix compiler warnings. (#5644)
2020-12-09 Andrew Reynolds(proof-new) Make theory preprocessor proofs self contai...
2020-12-09 Aina Niemetzgoogle test: expr: Migrate kind_map_black. (#5640)
2020-12-09 Aina Niemetzkind_map: Remove unused Accessor class. (#5641)
2020-12-09 Aina Niemetzgoogle test: expr: Migrate attribute_white. (#5632)
2020-12-09 Andrew ReynoldsMake decision engine independent of AssertionsPipeline...
2020-12-09 Andrew ReynoldsRemove obsolete regressions (#5633)
2020-12-09 Aina Niemetzgoogle test: context: Migrate context_white. (#5630)
2020-12-09 Gereon KremerSplit initial exp lemma into separate lemmas. (#5622)
2020-12-09 Aina NiemetzDelete obsolete unit tests for Expr and ExprManager...
2020-12-09 Andrew ReynoldsEnsure CEGQI is applied for parametric datatypes when...
2020-12-09 Andrew ReynoldsDo not check FP at last call if not necessary (#5627)
2020-12-09 Aina Niemetzite_utilities: Fix infinite loop in compressTerm. ...
2020-12-09 yoni206update doc (#5619)
2020-12-08 Aina Niemetzgoogle test: context: Migrate context_mm_black. (#5592)
2020-12-08 Aina Niemetzgoogle test: context: Migrate context_black. (#5587)
2020-12-08 Gereon KremerAdd regression from #1978. (#5552)
2020-12-08 Abdalrhman... Fix a bug with synth-fun printer (#5512)
2020-12-08 Haniel Barbosa[proof-new] Updating SAT proof to use MACRO_RESOLUTION...
2020-12-08 yoni206bv-to-int: Expand definitions of bvudiv and bvurem...
2020-12-08 Andrew ReynoldsMake term indices in the strings base solver aware...
2020-12-08 Andrew ReynoldsProper implementation of expand definitions for sequenc...
2020-12-08 Andrew ReynoldsFix collect model values for sequences of sequences...
2020-12-08 Haniel Barbosa[proof-new] Adding MACRO_RESOLUTION rule and updating...
2020-12-08 Mathias PreinerAdd support for BV proofs with the simple bitblasting...
2020-12-08 Mathias PreinerDisable algebraic BV subtheory by default and make...
2020-12-07 Andrew ReynoldsFix and reenable fact vs lemma optimization in datatype...
2020-12-07 makaimannAdd bitwise refinement mode for IAND (#5328)
2020-12-07 Andrew ReynoldsFix issue with free variables introduced by quantifier...
2020-12-07 Gereon KremerRefactor initial phase of transcendental solver (#5599)
2020-12-07 Andrew ReynoldsDo not expand theory definitions at the beginning of...
2020-12-07 Andrew Reynolds (proof-new) Split proof ensure closed checks to own...
2020-12-07 Gereon KremerAdd regression from #4927 (#5556)
2020-12-07 Andrew ReynoldsFix bugs in getFreeVariables (#5601)
2020-12-05 Everett MausChange generated options to be thread_local. (#5583)
2020-12-04 Aina Niemetzgoogle test: expr: Migrate attribute_black. (#5598)
2020-12-04 Aina Niemetzgoogle test: context: Migrate cdo_black. (#5586)
2020-12-04 Aina Niemetzgoogle test: context: Migrate cdmap_white. (#5585)
2020-12-04 Andrew ReynoldsFix bug in hasBoundVar (#5600)
2020-12-04 Aina Niemetzgoogle test: api: Migrate sort_black. (#5594)
2020-12-04 Aina Niemetzgoogle test: context: Migrate cdmap_black. (#5584)
2020-12-04 Aina Niemetzgoogle test: context: Migrate cdlist_black. (#5582)
2020-12-04 Alex OzdemirUse NodeDfsIterable for makeBinary (#5595)
2020-12-04 Mathias Preinerupdate-copyright: Preserve file permissions. (#5597)
2020-12-03 Andrew Reynolds(proof-new) Updates to SMT proof manager and SmtEngine...
2020-12-03 Aina Niemetzgoogle test: api: Migrate solver_black. (#5570)
2020-12-03 Gereon KremerUse mkAnd where the number of children may be less...
2020-12-03 yoni206Models as (#5581)
2020-12-03 Aina Niemetzgoogle test: Add fixture for context tests. (#5590)
2020-12-03 Andrew ReynoldsRefactor handling of global declarations (#5577)
2020-12-03 Gereon KremerMake run_regression.py executable. (#5588)
2020-12-03 Aina NiemetzUpdate copyright headers.
2020-12-03 Aina Niemetzgoogle test: base: Migrate map_util_black. (#5580)
2020-12-02 Aina NiemetzFix RoundingMode mapping in API. (#5578)
2020-12-02 Andrew ReynoldsRemove Record object and convert to Node-level API...
2020-12-02 Aina NiemetzRename macro Message to CVC4Message. (#5576)
2020-12-02 Andrew ReynoldsRemove dagification visitor (#5574)
2020-12-02 Aina Niemetzgoogle test: api: Migrate term_black. (#5571)
2020-12-02 Aina Niemetzgoogle test: api: Use individual fixture for datatype_b...
2020-12-02 Andrew ReynoldsAdd associative utilities to node manager (#5530)
2020-12-02 Aina Niemetzgoogle test: api: Migrate op_black. (#5567)
2020-12-02 Aina Niemetzgoogle test: api: Migrate grammar_black. (#5566)
2020-12-02 Andrew ReynoldsUse new let binding for cvc printer (#5561)
2020-12-02 Andrew Reynolds(proof-new) Proofs for expand definitions (#5562)
2020-12-02 Gereon KremerAdd regressions from #3687. (#5553)
2020-12-02 Aina Niemetzgoogle test: api: Migrate result_black. (#5569)
2020-12-02 Aina NiemetzRemove use of this-> in FP literal. (#5565)
2020-12-02 Andrew ReynoldsRemove assertion related to CEGQI dependency lemmas...
2020-12-02 Aina Niemetzgoogle test: Infrastructure and first api test. (#5548)
2020-12-02 Andrew ReynoldsFix issues related to model declarations (#5560)
2020-12-01 Andres NoetzliImprove rewriting of str.<= (#4848)
2020-12-01 Gereon KremerRefactor transcendental solver (#5539)
2020-12-01 Gereon KremerAdd regressions from #5099 (#5557)
2020-12-01 Gereon KremerAdd regression for #4335. (#5554)
2020-12-01 Gereon KremerAdd regressions for #4707. (#5555)
2020-12-01 Andrew ReynoldsMore fixes for quantifier elimination (#5533)
2020-12-01 yoni206fix metadata for a test (#5546)
2020-11-30 Aina Niemetzfp_converter: Properly separate out symbolic glue code...
2020-11-30 Andrew ReynoldsUse new let binding in AST printer (#5529)
2020-11-30 Aina Niemetzfloatingpoint: Use unique_ptr for FloatingPointLiteral...
next