projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2020-12-09 Aina Niemetzgoogle test: expr: Migrate kind_map_black. (#5640) commit | commitdiff | tree
2020-12-09 Aina Niemetzkind_map: Remove unused Accessor class. (#5641) commit | commitdiff | tree
2020-12-09 Aina Niemetzgoogle test: expr: Migrate attribute_white. (#5632) commit | commitdiff | tree
2020-12-09 Andrew ReynoldsMake decision engine independent of AssertionsPipeline... commit | commitdiff | tree
2020-12-09 Andrew ReynoldsRemove obsolete regressions (#5633) commit | commitdiff | tree
2020-12-09 Aina Niemetzgoogle test: context: Migrate context_white. (#5630) commit | commitdiff | tree
2020-12-09 Gereon KremerSplit initial exp lemma into separate lemmas. (#5622) commit | commitdiff | tree
2020-12-09 Aina NiemetzDelete obsolete unit tests for Expr and ExprManager... commit | commitdiff | tree
2020-12-09 Andrew ReynoldsEnsure CEGQI is applied for parametric datatypes when... commit | commitdiff | tree
2020-12-09 Andrew ReynoldsDo not check FP at last call if not necessary (#5627) commit | commitdiff | tree
2020-12-09 Aina Niemetzite_utilities: Fix infinite loop in compressTerm. ... commit | commitdiff | tree
2020-12-09 yoni206update doc (#5619) commit | commitdiff | tree
2020-12-08 Aina Niemetzgoogle test: context: Migrate context_mm_black. (#5592) commit | commitdiff | tree
2020-12-08 Aina Niemetzgoogle test: context: Migrate context_black. (#5587) commit | commitdiff | tree
2020-12-08 Gereon KremerAdd regression from #1978. (#5552) commit | commitdiff | tree
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
next