projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2021-11-16 Haniel Barbosa[proofs] Make sure --proof-check=... is no-op when... commit | commitdiff | tree
2021-11-16 Andres NoetzliRefactor `metakind` (#7639) commit | commitdiff | tree
2021-11-15 Aina Niemetzapi: Rename BOUND_VAR_LIST to VARIABLE_LIST. (#7632) commit | commitdiff | tree
2021-11-15 Andres Noetzli[Strings] Minor refactor of eager solver (#7628) commit | commitdiff | tree
2021-11-15 mudathirmahgoubAdd documentation for theory_bags_type_rules.h (#7642) commit | commitdiff | tree
2021-11-13 Andres NoetzliSkip `str.code` inferences for sequence eqcs (#7644) commit | commitdiff | tree
2021-11-13 mudathirmahgoubFix type error for rewriting bag.map bag.union_disjoint... commit | commitdiff | tree
2021-11-13 mudathirmahgoubAdd operator set.map to theory of sets (#7641) commit | commitdiff | tree
2021-11-12 mudathirmahgoubbags: Rename kinds with a more consistent naming scheme... commit | commitdiff | tree
2021-11-12 Andrew Reynolds[proofs] Cancel SYMM in CDProof, throw an error for... commit | commitdiff | tree
2021-11-12 Andres NoetzliFix redundant definitions of `NodeValue::getConst`... commit | commitdiff | tree
2021-11-12 Andrew ReynoldsAdd some basic rewrites for regular expression intersec... commit | commitdiff | tree
2021-11-12 Andres NoetzliRemove `ConstantMap<Rational>` (#7635) commit | commitdiff | tree
2021-11-12 Gereon KremerVarious minor docs improvements (#7626) commit | commitdiff | tree
2021-11-11 Abdalrhman... Add an API method to get the raw name of a term. (... commit | commitdiff | tree
2021-11-11 Andrew ReynoldsGeneralize front-end checks to check for shadowed varia... commit | commitdiff | tree
2021-11-11 Andrew ReynoldsAdd lazy approach for handling lambdas in the HO extens... commit | commitdiff | tree
2021-11-11 Andrew ReynoldsFixes for update/nth over constant sequences (#7631) commit | commitdiff | tree
2021-11-10 Aina Niemetzapi: Add Solver::mkRegexpAll(). (#7614) commit | commitdiff | tree
2021-11-10 Lachnitt[proofs] Alethe: Translate of Arithmetic rules (#7613) commit | commitdiff | tree
2021-11-10 Lachnitt[proofs] Alethe: Translate INSTANTIATE rule (#7607) commit | commitdiff | tree
2021-11-10 Mathias Preinerdocs: Also create javadoc for generated Kind.java ... commit | commitdiff | tree
2021-11-10 mudathirmahgoubFix soundness issue of missing premises for count bag... commit | commitdiff | tree
2021-11-10 Mathias Preinerjava: Fix building cvc5.jar for cmake 3.16. (#7623) commit | commitdiff | tree
2021-11-10 Andrew ReynoldsFix parsing array constants (#7617) commit | commitdiff | tree
2021-11-10 Aina Niemetzsets: Rename set.intersection to set.inter. (#7622) commit | commitdiff | tree
2021-11-10 Aina NiemetzReorganize test/unit/api directory. (#7612) commit | commitdiff | tree
2021-11-09 Lachnitt[proofs] Alethe: Translate Further Equality rules ... commit | commitdiff | tree
2021-11-09 Lachnitt[proofs] Alethe: Translate Equality rules (#7605) commit | commitdiff | tree
2021-11-09 Andrew ReynoldsOnly eliminate lambdas in higher-order elimination... commit | commitdiff | tree
2021-11-09 Andrew ReynoldsMinor optimizations for term database (#7600) commit | commitdiff | tree
2021-11-09 Aina NiemetzClean up ctest configuration and CI test configuration... commit | commitdiff | tree
2021-11-09 Haniel Barbosa[proofs] Generalize trivial cycle detection in LazyCDPr... commit | commitdiff | tree
2021-11-09 Lachnitt[proofs] Alethe: Translate REORDERING rule (#7533) commit | commitdiff | tree
2021-11-09 Aina Niemetzsets: Update theory reference and smt2 examples. (... commit | commitdiff | tree
2021-11-09 Andrew ReynoldsPreparation for non-constant lambda models (#7604) commit | commitdiff | tree
2021-11-09 Gereon KremerMake secant points user context dependent (#7567) commit | commitdiff | tree
2021-11-09 Abdalrhman... Remove redundant rules for generating Java and Python... commit | commitdiff | tree
2021-11-09 Andrew ReynoldsAdd LFSC signature for strings (#7523) commit | commitdiff | tree
2021-11-09 Aina Niemetzregex: Rename REGEXP_EMPTY and REGEXP_SIGMA to match... commit | commitdiff | tree
2021-11-09 Gereon KremerRemove `CVC5Message` (#7610) commit | commitdiff | tree
2021-11-09 Gereon KremerRemove antlr_tracing.h (#7608) commit | commitdiff | tree
2021-11-09 Gereon KremerRemove more static option accesses (#7582) commit | commitdiff | tree
2021-11-09 Gereon KremerRemove command-verbosity option (#7581) commit | commitdiff | tree
2021-11-09 Mathias Preinercmake: Use fastcov for generating coverage reports... commit | commitdiff | tree
2021-11-08 Gereon KremerImprove rendering of expert options. (#7589) commit | commitdiff | tree
2021-11-08 mudathirmahgoubexpand bag.choose operator (#7481) commit | commitdiff | tree
2021-11-08 Andrew ReynoldsAdd lambda lift utility (#7601) commit | commitdiff | tree
2021-11-08 Aina Niemetzsets: Rename kinds with a more consistent naming scheme... commit | commitdiff | tree
2021-11-08 Andrew ReynoldsEvaluate cast-to-real operator (#7599) commit | commitdiff | tree
2021-11-08 Haniel Barbosa[proofs] Adding NoSubtype node converter to Alethe... commit | commitdiff | tree
2021-11-08 Haniel Barbosa[proofs] Method to convert node representation of Aleth... commit | commitdiff | tree
2021-11-06 Gereon KremerIntegrate java unit tests into ctest (#7593) commit | commitdiff | tree
2021-11-06 Abdalrhman... Print `unsupported` for unrecognized flags. (#7384) commit | commitdiff | tree
2021-11-06 Haniel Barbosabetter traces in node converter (#7590) commit | commitdiff | tree
2021-11-06 Andrew ReynoldsDo not use extended rewrites on recursive function... commit | commitdiff | tree
2021-11-06 Gereon KremerOnly run regress0 for static build (#7592) commit | commitdiff | tree
2021-11-06 Gereon KremerRemove `Notice()` in favor of new `verbose()` (#7588) commit | commitdiff | tree
2021-11-06 Mathias PreinerDisable regress2 test. (#7591) commit | commitdiff | tree
2021-11-05 Andrew ReynoldsFix exclusion criteria for codatatype model values... commit | commitdiff | tree
2021-11-05 Haniel Barbosa[proofs] Fix open sat proof (#7509) commit | commitdiff | tree
2021-11-05 Andrew ReynoldsEliminate a level of nesting of traversals in theory... commit | commitdiff | tree
2021-11-05 Gereon KremerRemove `Chat()` in favor of new `verbose()` (#7586) commit | commitdiff | tree
2021-11-05 Andrew ReynoldsMove functions and lambdas from builtin to uf (#7570) commit | commitdiff | tree
2021-11-05 Andres Noetzli[FP] Do not assert that model has shared term (#7585) commit | commitdiff | tree
2021-11-05 Gereon KremerFix some issues with the java api (#7583) commit | commitdiff | tree
2021-11-05 LachnittAlethe: Translate CNF rules (#7532) commit | commitdiff | tree
2021-11-05 Haniel BarbosaMinor changes to circuit propagator (#7584) commit | commitdiff | tree
2021-11-05 Andrew ReynoldsRemove many static calls to rewrite (#7580) commit | commitdiff | tree
2021-11-05 Gereon KremerRemove quadratic solving in NlModel (#7542) commit | commitdiff | tree
2021-11-05 Gereon KremerEliminate `Warning` macro in favor of `EnvObj::warning... commit | commitdiff | tree
2021-11-05 Gereon KremerRemove a bunch of debugging/logging code from the linea... commit | commitdiff | tree
2021-11-04 Andrew ReynoldsAdd -o sygus-grammar to print auto-generated SyGuS... commit | commitdiff | tree
2021-11-04 Andrew ReynoldsImprove defaults for sygus default grammars (#7553) commit | commitdiff | tree
2021-11-04 Andrew ReynoldsReplace the old dump infrastructure (#7572) commit | commitdiff | tree
2021-11-04 Gereon KremerStart refactoring of `-o` and `-v` (#7449) commit | commitdiff | tree
2021-11-04 Gereon KremerRefactor cmake to build either static or shared (#7534) commit | commitdiff | tree
2021-11-04 Gereon Kremer Fix links in README.md (#7568) commit | commitdiff | tree
2021-11-04 Gereon KremerEnable CDCAC solver for selected quantified logics... commit | commitdiff | tree
2021-11-04 Gereon KremerAdd support for special tag collectors (#7562) commit | commitdiff | tree
2021-11-04 Gereon KremerMinor cleanup in SolverEngine::setInfo() (#7566) commit | commitdiff | tree
2021-11-04 Andres NoetzliMake `Theory::get()` private (#7518) commit | commitdiff | tree
2021-11-03 Aina Niemetzapi: Rename some separation logic functions for consist... commit | commitdiff | tree
2021-11-03 Aina NiemetzAdd unit test to cover previous failure with second... commit | commitdiff | tree
2021-11-03 mudathirmahgoubEnable CI for Junit tests (#7436) commit | commitdiff | tree
2021-11-03 Andrew ReynoldsFix debug trace for miplib (#7563) commit | commitdiff | tree
2021-11-03 Andrew ReynoldsRefactor skolem construction (#7561) commit | commitdiff | tree
2021-11-03 Andrew ReynoldsFormalize more string skolems (#7554) commit | commitdiff | tree
2021-11-03 Andrew ReynoldsFix preregistration for floating point theory (#7558) commit | commitdiff | tree
2021-11-02 Mathias Preinerbv: Disable equality engine for --bitblast=eager and... commit | commitdiff | tree
2021-11-02 Abdalrhman... Move `fmf.card` printing code. (#7559) commit | commitdiff | tree
2021-11-02 Abdalrhman... Add printing methods for some commands. (#7557) commit | commitdiff | tree
2021-11-02 Andrew ReynoldsImprove syntax for fmf cardinality constraints (#7556) commit | commitdiff | tree
2021-11-02 Andrew ReynoldsAdd LFSC signature for quantifiers (#7540) commit | commitdiff | tree
2021-11-02 Mathias PreinerFix setDefaults() for proofs with bitblast-internal... commit | commitdiff | tree
2021-11-02 Mathias Preinerbv: Remove remaining Rewriter::rewrite calls. (#7545) commit | commitdiff | tree
2021-11-02 Andrew ReynoldsMake quant elimination robust to presence of other... commit | commitdiff | tree
2021-11-01 Andrew ReynoldsEliminate calls to Rewriter::rewrite and options::... commit | commitdiff | tree
2021-11-01 Andrew ReynoldsWeaken assertion in CEGQI (#7548) commit | commitdiff | tree
2021-11-01 Gereon KremerAdd explicit option enum value __MAX_VALUE (#7547) commit | commitdiff | tree
next