cvc5.git
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...
2020-11-30 Abdalrhman... Eliminate uses of SExpr from the parser. (#5496)
2020-11-30 Andrew ReynoldsRemove includes for old API from internal code (#5536)
2020-11-30 Andrew Reynolds(proof-new) Proofs for regular expression elimination...
2020-11-26 Gereon KremerMake CAD solver work for empty set of assertions (...
2020-11-26 Andrew ReynoldsRemoving infrastructure related to SMT model (#5527)
2020-11-26 Andrew ReynoldsMove expand definitions to its own file (#5528)
2020-11-26 Andrew ReynoldsFully decouple SmtEngine and the Expr layer (#5532)
2020-11-26 Andrew ReynoldsFix missed case of theory preprocessing (#5531)
2020-11-26 Andrew ReynoldsDisable fact vs lemma optimization in datatypes for...
2020-11-25 Andrew ReynoldsAdd regressions for closed issues (#5526)
2020-11-25 Gereon KremerFix transcendental secant plane lemmas (#5525)
2020-11-25 Andrew ReynoldsUse symbol manager for printing responses get-model...
2020-11-25 Andrew ReynoldsAllow printing of null node in let binder (#5523)
2020-11-25 Gereon KremerRefactor transcendental solver (#5514)
2020-11-23 Andrew ReynoldsFix regular expression consume for nested star (#5518)
2020-11-23 Andrew ReynoldsChange UF ho to ppRewrite instead of expand definition...
2020-11-23 Andrew ReynoldsFix for sygusToBuiltinEval for non-ground composite...
2020-11-23 Andrew Reynolds(proof-new) Miscellaneous changes from proof-new (...
2020-11-23 Andrew ReynoldsAdd declare model symbol methods to SymbolManager and...
2020-11-23 Gereon KremerAdd get-info :time. (#5485)
2020-11-23 Andrew ReynoldsFix quantifiers scope issue in strings preprocessor...
2020-11-21 mudathirmahgoubAdd posRewriteEqual to bags rewriter (#5498)
2020-11-21 Aina NiemetzRename symfpu_literal.(h.in|cpp) -> floatingpoint_liter...
2020-11-21 Aina NiemetzRename floatingpoint.h.in -> floatingpoin.h. (#5500)
2020-11-20 Andrew ReynoldsFix remove term formula policy for terms beneath quanti...
2020-11-20 Aina NiemetzRoundingMode: Rename enum values to conform to code...
2020-11-20 Aina NiemetzFloatingPoint: Separate out symFPU glue code. (#5492)
2020-11-20 Aina NiemetzFix #5493. (#5495)
2020-11-20 Andrew ReynoldsSupport nested quantifier elimination for get-qe comman...
2020-11-20 Andrew ReynoldsUpdates to API in preparation for using symbol manager...
2020-11-20 Aina NiemetzFix compiler warnings. (#5493)
2020-11-20 Andrew ReynoldsFix use of declaration sequence command in cvc parser...
2020-11-20 Gereon Kremer(proof-new) Replace LazyCDProofSet by generic CDProofSe...
2020-11-20 Gereon KremerAllow to pass ProofGenerator to arithmetic inference...
2020-11-19 Andrew ReynoldsEnable new implementation of CEGQI based on nested...
2020-11-19 Aina Niemetzfloatingpoint.h: Split in preparation to cleanly separa...
2020-11-19 Andrew ReynoldsUse new let binding utility in smt2 printer (#5472)
2020-11-19 Aina NiemetzInclude stddef.h (needed for size_t) in cvc4_public...
2020-11-19 Andrew ReynoldsAdd nested quantifier elimination module (#5422)
2020-11-19 Andrew ReynoldsFix issues related to eliminating extended arithmetic...
2020-11-19 Andrew ReynoldsUse symbol manager for unsat cores (#5468)
2020-11-18 Mathias PreinerAdd -> operator overload for cd* iterators. (#5464)
2020-11-18 Andrew ReynoldsDisable slow nl regression (#5467)
2020-11-18 Andrew ReynoldsAdd let binding utility (#5444)
next