projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2020-12-08 Abdalrhman... Fix a bug with synth-fun printer (#5512) commit | commitdiff | tree
2020-12-08 Haniel Barbosa[proof-new] Updating SAT proof to use MACRO_RESOLUTION... commit | commitdiff | tree
2020-12-08 yoni206bv-to-int: Expand definitions of bvudiv and bvurem... commit | commitdiff | tree
2020-12-08 Andrew ReynoldsMake term indices in the strings base solver aware... commit | commitdiff | tree
2020-12-08 Andrew ReynoldsProper implementation of expand definitions for sequenc... commit | commitdiff | tree
2020-12-08 Andrew ReynoldsFix collect model values for sequences of sequences... commit | commitdiff | tree
2020-12-08 Haniel Barbosa[proof-new] Adding MACRO_RESOLUTION rule and updating... commit | commitdiff | tree
2020-12-08 Mathias PreinerAdd support for BV proofs with the simple bitblasting... commit | commitdiff | tree
2020-12-08 Mathias PreinerDisable algebraic BV subtheory by default and make... commit | commitdiff | tree
2020-12-07 Andrew ReynoldsFix and reenable fact vs lemma optimization in datatype... commit | commitdiff | tree
2020-12-07 makaimannAdd bitwise refinement mode for IAND (#5328) commit | commitdiff | tree
2020-12-07 Andrew ReynoldsFix issue with free variables introduced by quantifier... commit | commitdiff | tree
2020-12-07 Gereon KremerRefactor initial phase of transcendental solver (#5599) commit | commitdiff | tree
2020-12-07 Andrew ReynoldsDo not expand theory definitions at the beginning of... commit | commitdiff | tree
2020-12-07 Andrew Reynolds (proof-new) Split proof ensure closed checks to own... commit | commitdiff | tree
2020-12-07 Gereon KremerAdd regression from #4927 (#5556) commit | commitdiff | tree
2020-12-07 Andrew ReynoldsFix bugs in getFreeVariables (#5601) commit | commitdiff | tree
2020-12-05 Everett MausChange generated options to be thread_local. (#5583) commit | commitdiff | tree
2020-12-04 Aina Niemetzgoogle test: expr: Migrate attribute_black. (#5598) commit | commitdiff | tree
2020-12-04 Aina Niemetzgoogle test: context: Migrate cdo_black. (#5586) commit | commitdiff | tree
2020-12-04 Aina Niemetzgoogle test: context: Migrate cdmap_white. (#5585) commit | commitdiff | tree
2020-12-04 Andrew ReynoldsFix bug in hasBoundVar (#5600) commit | commitdiff | tree
2020-12-04 Aina Niemetzgoogle test: api: Migrate sort_black. (#5594) commit | commitdiff | tree
2020-12-04 Aina Niemetzgoogle test: context: Migrate cdmap_black. (#5584) commit | commitdiff | tree
2020-12-04 Aina Niemetzgoogle test: context: Migrate cdlist_black. (#5582) commit | commitdiff | tree
2020-12-04 Alex OzdemirUse NodeDfsIterable for makeBinary (#5595) commit | commitdiff | tree
2020-12-04 Mathias Preinerupdate-copyright: Preserve file permissions. (#5597) commit | commitdiff | tree
2020-12-03 Andrew Reynolds(proof-new) Updates to SMT proof manager and SmtEngine... commit | commitdiff | tree
2020-12-03 Aina Niemetzgoogle test: api: Migrate solver_black. (#5570) commit | commitdiff | tree
2020-12-03 Gereon KremerUse mkAnd where the number of children may be less... commit | commitdiff | tree
2020-12-03 yoni206Models as (#5581) commit | commitdiff | tree
2020-12-03 Aina Niemetzgoogle test: Add fixture for context tests. (#5590) commit | commitdiff | tree
2020-12-03 Andrew ReynoldsRefactor handling of global declarations (#5577) commit | commitdiff | tree
2020-12-03 Gereon KremerMake run_regression.py executable. (#5588) commit | commitdiff | tree
2020-12-03 Aina NiemetzUpdate copyright headers. commit | commitdiff | tree
2020-12-03 Aina Niemetzgoogle test: base: Migrate map_util_black. (#5580) commit | commitdiff | tree
2020-12-02 Aina NiemetzFix RoundingMode mapping in API. (#5578) commit | commitdiff | tree
2020-12-02 Andrew ReynoldsRemove Record object and convert to Node-level API... commit | commitdiff | tree
2020-12-02 Aina NiemetzRename macro Message to CVC4Message. (#5576) commit | commitdiff | tree
2020-12-02 Andrew ReynoldsRemove dagification visitor (#5574) commit | commitdiff | tree
2020-12-02 Aina Niemetzgoogle test: api: Migrate term_black. (#5571) commit | commitdiff | tree
2020-12-02 Aina Niemetzgoogle test: api: Use individual fixture for datatype_b... commit | commitdiff | tree
2020-12-02 Andrew ReynoldsAdd associative utilities to node manager (#5530) commit | commitdiff | tree
2020-12-02 Aina Niemetzgoogle test: api: Migrate op_black. (#5567) commit | commitdiff | tree
2020-12-02 Aina Niemetzgoogle test: api: Migrate grammar_black. (#5566) commit | commitdiff | tree
2020-12-02 Andrew ReynoldsUse new let binding for cvc printer (#5561) commit | commitdiff | tree
2020-12-02 Andrew Reynolds(proof-new) Proofs for expand definitions (#5562) commit | commitdiff | tree
2020-12-02 Gereon KremerAdd regressions from #3687. (#5553) commit | commitdiff | tree
2020-12-02 Aina Niemetzgoogle test: api: Migrate result_black. (#5569) commit | commitdiff | tree
2020-12-02 Aina NiemetzRemove use of this-> in FP literal. (#5565) commit | commitdiff | tree
2020-12-02 Andrew ReynoldsRemove assertion related to CEGQI dependency lemmas... commit | commitdiff | tree
2020-12-02 Aina Niemetzgoogle test: Infrastructure and first api test. (#5548) commit | commitdiff | tree
2020-12-02 Andrew ReynoldsFix issues related to model declarations (#5560) commit | commitdiff | tree
2020-12-01 Andres NoetzliImprove rewriting of str.<= (#4848) commit | commitdiff | tree
2020-12-01 Gereon KremerRefactor transcendental solver (#5539) commit | commitdiff | tree
2020-12-01 Gereon KremerAdd regressions from #5099 (#5557) commit | commitdiff | tree
2020-12-01 Gereon KremerAdd regression for #4335. (#5554) commit | commitdiff | tree
2020-12-01 Gereon KremerAdd regressions for #4707. (#5555) commit | commitdiff | tree
2020-12-01 Andrew ReynoldsMore fixes for quantifier elimination (#5533) commit | commitdiff | tree
2020-12-01 yoni206fix metadata for a test (#5546) commit | commitdiff | tree
2020-11-30 Aina Niemetzfp_converter: Properly separate out symbolic glue code... commit | commitdiff | tree
2020-11-30 Andrew ReynoldsUse new let binding in AST printer (#5529) commit | commitdiff | tree
2020-11-30 Aina Niemetzfloatingpoint: Use unique_ptr for FloatingPointLiteral... commit | commitdiff | tree
2020-11-30 Abdalrhman... Eliminate uses of SExpr from the parser. (#5496) commit | commitdiff | tree
2020-11-30 Andrew ReynoldsRemove includes for old API from internal code (#5536) commit | commitdiff | tree
2020-11-30 Andrew Reynolds(proof-new) Proofs for regular expression elimination... commit | commitdiff | tree
2020-11-26 Gereon KremerMake CAD solver work for empty set of assertions (... commit | commitdiff | tree
2020-11-26 Andrew ReynoldsRemoving infrastructure related to SMT model (#5527) commit | commitdiff | tree
2020-11-26 Andrew ReynoldsMove expand definitions to its own file (#5528) commit | commitdiff | tree
2020-11-26 Andrew ReynoldsFully decouple SmtEngine and the Expr layer (#5532) commit | commitdiff | tree
2020-11-26 Andrew ReynoldsFix missed case of theory preprocessing (#5531) commit | commitdiff | tree
2020-11-26 Andrew ReynoldsDisable fact vs lemma optimization in datatypes for... commit | commitdiff | tree
2020-11-25 Andrew ReynoldsAdd regressions for closed issues (#5526) commit | commitdiff | tree
2020-11-25 Gereon KremerFix transcendental secant plane lemmas (#5525) commit | commitdiff | tree
2020-11-25 Andrew ReynoldsUse symbol manager for printing responses get-model... commit | commitdiff | tree
2020-11-25 Andrew ReynoldsAllow printing of null node in let binder (#5523) commit | commitdiff | tree
2020-11-25 Gereon KremerRefactor transcendental solver (#5514) commit | commitdiff | tree
2020-11-23 Andrew ReynoldsFix regular expression consume for nested star (#5518) commit | commitdiff | tree
2020-11-23 Andrew ReynoldsChange UF ho to ppRewrite instead of expand definition... commit | commitdiff | tree
2020-11-23 Andrew ReynoldsFix for sygusToBuiltinEval for non-ground composite... commit | commitdiff | tree
2020-11-23 Andrew Reynolds(proof-new) Miscellaneous changes from proof-new (... commit | commitdiff | tree
2020-11-23 Andrew ReynoldsAdd declare model symbol methods to SymbolManager and... commit | commitdiff | tree
2020-11-23 Gereon KremerAdd get-info :time. (#5485) commit | commitdiff | tree
2020-11-23 Andrew ReynoldsFix quantifiers scope issue in strings preprocessor... commit | commitdiff | tree
2020-11-21 mudathirmahgoubAdd posRewriteEqual to bags rewriter (#5498) commit | commitdiff | tree
2020-11-21 Aina NiemetzRename symfpu_literal.(h.in|cpp) -> floatingpoint_liter... commit | commitdiff | tree
2020-11-21 Aina NiemetzRename floatingpoint.h.in -> floatingpoin.h. (#5500) commit | commitdiff | tree
2020-11-20 Andrew ReynoldsFix remove term formula policy for terms beneath quanti... commit | commitdiff | tree
2020-11-20 Aina NiemetzRoundingMode: Rename enum values to conform to code... commit | commitdiff | tree
2020-11-20 Aina NiemetzFloatingPoint: Separate out symFPU glue code. (#5492) commit | commitdiff | tree
2020-11-20 Aina NiemetzFix #5493. (#5495) commit | commitdiff | tree
2020-11-20 Andrew ReynoldsSupport nested quantifier elimination for get-qe comman... commit | commitdiff | tree
2020-11-20 Andrew ReynoldsUpdates to API in preparation for using symbol manager... commit | commitdiff | tree
2020-11-20 Aina NiemetzFix compiler warnings. (#5493) commit | commitdiff | tree
2020-11-20 Andrew ReynoldsFix use of declaration sequence command in cvc parser... commit | commitdiff | tree
2020-11-20 Gereon Kremer(proof-new) Replace LazyCDProofSet by generic CDProofSe... commit | commitdiff | tree
2020-11-20 Gereon KremerAllow to pass ProofGenerator to arithmetic inference... commit | commitdiff | tree
2020-11-19 Andrew ReynoldsEnable new implementation of CEGQI based on nested... commit | commitdiff | tree
2020-11-19 Aina Niemetzfloatingpoint.h: Split in preparation to cleanly separa... commit | commitdiff | tree
2020-11-19 Andrew ReynoldsUse new let binding utility in smt2 printer (#5472) commit | commitdiff | tree
next