cvc5.git
2021-11-22 Andrew ReynoldsImprove error for check theory assertions with model...
2021-11-22 Andrew ReynoldsFix const RE test for internal regexp rv kind (#7678)
2021-11-20 yoni206bv2int module: translation of more cases (#7653)
2021-11-19 Andres Noetzli[API] Avoid copying values (#7666)
2021-11-19 Andres NoetzliClean up relationship of metakind and node_manager...
2021-11-19 Andrew ReynoldsRemove n-ary builder (#7671)
2021-11-19 Mathias PreinerAllow negative denominator for CLN Rationals constructe...
2021-11-18 Aina Niemetzapi: Fix categorization of DT kinds in kind maps. ...
2021-11-18 Gereon KremerRefactor CAD option for linear model seed (#7657)
2021-11-18 Haniel Barbosa[proofs] Fix trace in SatProofManager (#7664)
2021-11-18 Lachnitt[proofs] Alethe: Rename DUPLICATED_LITERALS (#7661)
2021-11-18 Aina Niemetzapi: Fix kind documentation for BAG_MAKE. (#7663)
2021-11-17 Haniel BarbosaImprove naming in term canonization when handling HO...
2021-11-17 Haniel Barbosa[sat] Fix indentation in "reason" (#7662)
2021-11-17 Gereon KremerAdd documentation for z3py compatibility API (#7652)
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)
next