projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Add getters to retrieve constants from api::Term (#5677)
[cvc5.git] / test /
2020-12-15 Gereon KremerAdd getters to retrieve constants from api::Term (... tree | commitdiff
2020-12-14 Andrew ReynoldsProperly implement datatype selector triggers (#5624) tree | commitdiff
2020-12-14 Andrew ReynoldsFix SAT-context dependent issue in strings preregistrat... tree | commitdiff
2020-12-11 yoni206bv-to-int: new tests from an issue (#5654) tree | commitdiff
2020-12-11 Andrew ReynoldsFix length assumption for deq norm emp rule (#5623) tree | commitdiff
2020-12-10 Gereon KremerRefactor KindMap (#5646) tree | commitdiff
2020-12-10 Aina Niemetzgoogle test: expr: Migrate node_algorithm_black. (... tree | commitdiff
2020-12-10 Andrew ReynoldsRefactor regressions (#5639) tree | commitdiff
2020-12-10 Aina Niemetzgoogle test: expr: Migrate kind_black. (#5634) tree | commitdiff
2020-12-09 Aina Niemetzgoogle test: expr: Migrate kind_map_black. (#5640) tree | commitdiff
2020-12-09 Aina Niemetzgoogle test: expr: Migrate attribute_white. (#5632) tree | commitdiff
2020-12-09 Andrew ReynoldsMake decision engine independent of AssertionsPipeline... tree | commitdiff
2020-12-09 Andrew ReynoldsRemove obsolete regressions (#5633) tree | commitdiff
2020-12-09 Aina Niemetzgoogle test: context: Migrate context_white. (#5630) tree | commitdiff
2020-12-09 Aina NiemetzDelete obsolete unit tests for Expr and ExprManager... tree | commitdiff
2020-12-09 Andrew ReynoldsEnsure CEGQI is applied for parametric datatypes when... tree | commitdiff
2020-12-08 Aina Niemetzgoogle test: context: Migrate context_mm_black. (#5592) tree | commitdiff
2020-12-08 Aina Niemetzgoogle test: context: Migrate context_black. (#5587) tree | commitdiff
2020-12-08 Gereon KremerAdd regression from #1978. (#5552) tree | commitdiff
2020-12-08 Abdalrhman MohamedFix a bug with synth-fun printer (#5512) tree | commitdiff
2020-12-08 yoni206bv-to-int: Expand definitions of bvudiv and bvurem... tree | commitdiff
2020-12-08 Andrew ReynoldsMake term indices in the strings base solver aware... tree | commitdiff
2020-12-08 Andrew ReynoldsProper implementation of expand definitions for sequenc... tree | commitdiff
2020-12-08 Andrew ReynoldsFix collect model values for sequences of sequences... tree | commitdiff
2020-12-08 Mathias PreinerDisable algebraic BV subtheory by default and make... tree | commitdiff
2020-12-07 Andrew ReynoldsFix and reenable fact vs lemma optimization in datatype... tree | commitdiff
2020-12-07 makaimannAdd bitwise refinement mode for IAND (#5328) tree | commitdiff
2020-12-07 Andrew ReynoldsFix issue with free variables introduced by quantifier... tree | commitdiff
2020-12-07 Andrew ReynoldsDo not expand theory definitions at the beginning of... tree | commitdiff
2020-12-07 Gereon KremerAdd regression from #4927 (#5556) tree | commitdiff
2020-12-04 Aina Niemetzgoogle test: expr: Migrate attribute_black. (#5598) tree | commitdiff
2020-12-04 Aina Niemetzgoogle test: context: Migrate cdo_black. (#5586) tree | commitdiff
2020-12-04 Aina Niemetzgoogle test: context: Migrate cdmap_white. (#5585) tree | commitdiff
2020-12-04 Aina Niemetzgoogle test: api: Migrate sort_black. (#5594) tree | commitdiff
2020-12-04 Aina Niemetzgoogle test: context: Migrate cdmap_black. (#5584) tree | commitdiff
2020-12-04 Aina Niemetzgoogle test: context: Migrate cdlist_black. (#5582) tree | commitdiff
2020-12-03 Aina Niemetzgoogle test: api: Migrate solver_black. (#5570) tree | commitdiff
2020-12-03 Gereon KremerUse mkAnd where the number of children may be less... tree | commitdiff
2020-12-03 yoni206Models as (#5581) tree | commitdiff
2020-12-03 Aina Niemetzgoogle test: Add fixture for context tests. (#5590) tree | commitdiff
2020-12-03 Gereon KremerMake run_regression.py executable. (#5588) tree | commitdiff
2020-12-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-12-03 Aina Niemetzgoogle test: base: Migrate map_util_black. (#5580) tree | commitdiff
2020-12-02 Aina NiemetzFix RoundingMode mapping in API. (#5578) tree | commitdiff
2020-12-02 Aina NiemetzRename macro Message to CVC4Message. (#5576) tree | commitdiff
2020-12-02 Aina Niemetzgoogle test: api: Migrate term_black. (#5571) tree | commitdiff
2020-12-02 Aina Niemetzgoogle test: api: Use individual fixture for datatype_b... tree | commitdiff
2020-12-02 Aina Niemetzgoogle test: api: Migrate op_black. (#5567) tree | commitdiff
2020-12-02 Aina Niemetzgoogle test: api: Migrate grammar_black. (#5566) tree | commitdiff
2020-12-02 Andrew ReynoldsUse new let binding for cvc printer (#5561) tree | commitdiff
2020-12-02 Gereon KremerAdd regressions from #3687. (#5553) tree | commitdiff
2020-12-02 Aina Niemetzgoogle test: api: Migrate result_black. (#5569) tree | commitdiff
2020-12-02 Aina Niemetzgoogle test: Infrastructure and first api test. (#5548) tree | commitdiff
2020-12-02 Andrew ReynoldsFix issues related to model declarations (#5560) tree | commitdiff
2020-12-01 Andres NoetzliImprove rewriting of str.<= (#4848) tree | commitdiff
2020-12-01 Gereon KremerAdd regressions from #5099 (#5557) tree | commitdiff
2020-12-01 Gereon KremerAdd regression for #4335. (#5554) tree | commitdiff
2020-12-01 Gereon KremerAdd regressions for #4707. (#5555) tree | commitdiff
2020-12-01 Andrew ReynoldsMore fixes for quantifier elimination (#5533) tree | commitdiff
2020-12-01 yoni206fix metadata for a test (#5546) tree | commitdiff
2020-11-26 Gereon KremerMake CAD solver work for empty set of assertions (... tree | commitdiff
2020-11-26 Andrew ReynoldsFully decouple SmtEngine and the Expr layer (#5532) tree | commitdiff
2020-11-26 Andrew ReynoldsDisable fact vs lemma optimization in datatypes for... tree | commitdiff
2020-11-25 Andrew ReynoldsAdd regressions for closed issues (#5526) tree | commitdiff
2020-11-25 Andrew ReynoldsUse symbol manager for printing responses get-model... tree | commitdiff
2020-11-23 Andrew ReynoldsFix regular expression consume for nested star (#5518) tree | commitdiff
2020-11-23 Andrew ReynoldsChange UF ho to ppRewrite instead of expand definition... tree | commitdiff
2020-11-23 Andrew ReynoldsFix quantifiers scope issue in strings preprocessor... tree | commitdiff
2020-11-21 mudathirmahgoubAdd posRewriteEqual to bags rewriter (#5498) tree | commitdiff
2020-11-20 Andrew ReynoldsFix remove term formula policy for terms beneath quanti... tree | commitdiff
2020-11-20 Andrew ReynoldsSupport nested quantifier elimination for get-qe comman... tree | commitdiff
2020-11-20 Andrew ReynoldsUpdates to API in preparation for using symbol manager... tree | commitdiff
2020-11-19 Andrew ReynoldsEnable new implementation of CEGQI based on nested... tree | commitdiff
2020-11-19 Andrew ReynoldsUse new let binding utility in smt2 printer (#5472) tree | commitdiff
2020-11-19 Andrew ReynoldsFix issues related to eliminating extended arithmetic... tree | commitdiff
2020-11-18 Andrew ReynoldsDisable slow nl regression (#5467) tree | commitdiff
2020-11-18 Andrew ReynoldsDo not expand definitions of extended arithmetic operat... tree | commitdiff
2020-11-18 Andrew ReynoldsUse symbol manager for get assignment (#5451) tree | commitdiff
2020-11-18 Andrew ReynoldsFix asan issues related to solver and symbol manager... tree | commitdiff
2020-11-14 Andrew ReynoldsFix double conflict in extended string solver (#5435) tree | commitdiff
2020-11-13 Andrew ReynoldsMake regular expression difference left associative... tree | commitdiff
2020-11-12 yoni206Models standard (#5415) tree | commitdiff
2020-11-11 Andrew ReynoldsMove symbol manager to src/expr/ (#5420) tree | commitdiff
2020-11-11 Andrew ReynoldsPass symbol manager to commands (#5410) tree | commitdiff
2020-11-11 Andrew ReynoldsFix preregistration in TheorySep before declare-heap... tree | commitdiff
2020-11-10 Andrew ReynoldsDo not mark extended functions as reduced based on... tree | commitdiff
2020-11-10 Andrew ReynoldsAdd proper support for the declare-heap command for... tree | commitdiff
2020-11-09 Andrew ReynoldsAdd symbol manager (#5380) tree | commitdiff
2020-11-09 Andrew ReynoldsSimplify handling of subtypes in smt2 printer (#5401) tree | commitdiff
2020-11-09 Andrew ReynoldsDo not regress explanations of datatype lemmas (#5376) tree | commitdiff
2020-11-06 mudathirmahgoubFix issue #5342 (#5349) tree | commitdiff
2020-11-06 Andrew ReynoldsSimplify printing with respect to expression types... tree | commitdiff
2020-11-05 mudathirmahgoubRemove mkSingleton from the API (#5366) tree | commitdiff
2020-11-04 Andres NoetzliAdd constants from equality engine evaluation to model... tree | commitdiff
2020-11-03 Andres NoetzliAdd support for printing `re.loop` and `re.^` (#5392) tree | commitdiff
2020-11-03 Andrew ReynoldsReset built model flag at presolve in nonlinear (#5386) tree | commitdiff
2020-11-03 makaimannRun python tests during make check (#5226) tree | commitdiff
2020-11-02 Andrew ReynoldsUpdate strings proxy variable map to be context indepen... tree | commitdiff
2020-10-30 Andrew ReynoldsUpdate api::Sort to use TypeNode instead of Type (... tree | commitdiff
2020-10-29 mudathirmahgoubAdd mkInteger to the API (#5274) tree | commitdiff
next