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