summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2021-11-15Merge branch 'master' into refactorEagerSolverrefactorEagerSolverAndrew Reynolds
2021-11-15Add documentation for theory_bags_type_rules.h (#7642)mudathirmahgoub
2021-11-13Skip `str.code` inferences for sequence eqcs (#7644)Andres Noetzli
2021-11-13Fix type error for rewriting bag.map bag.union_disjoint (#7640)mudathirmahgoub
2021-11-13Add operator set.map to theory of sets (#7641)mudathirmahgoub
2021-11-13addressAndres Noetzli
2021-11-12bags: Rename kinds with a more consistent naming scheme (#7611)mudathirmahgoub
2021-11-12[proofs] Cancel SYMM in CDProof, throw an error for cyclic proofs during doub...Andrew Reynolds
2021-11-12Fix redundant definitions of `NodeValue::getConst` (#7636)Andres Noetzli
2021-11-12Add some basic rewrites for regular expression intersection (#7629)Andrew Reynolds
2021-11-12Remove `ConstantMap<Rational>` (#7635)Andres Noetzli
2021-11-12Various minor docs improvements (#7626)Gereon Kremer
2021-11-11Add an API method to get the raw name of a term. (#7618)Abdalrhman Mohamed
2021-11-11Generalize front-end checks to check for shadowed variables (#7634)Andrew Reynolds
2021-11-11Add lazy approach for handling lambdas in the HO extension (#7625)Andrew Reynolds
2021-11-11Fixes for update/nth over constant sequences (#7631)Andrew Reynolds
2021-11-10api: Add Solver::mkRegexpAll(). (#7614)Aina Niemetz
2021-11-10[Strings] Minor refactor of eager solverAndres Noetzli
2021-11-10[proofs] Alethe: Translate of Arithmetic rules (#7613)Lachnitt
2021-11-10[proofs] Alethe: Translate INSTANTIATE rule (#7607)Lachnitt
2021-11-10Fix soundness issue of missing premises for count bag lemmas (#7615)mudathirmahgoub
2021-11-10java: Fix building cvc5.jar for cmake 3.16. (#7623)Mathias Preiner
2021-11-10Fix parsing array constants (#7617)Andrew Reynolds
2021-11-10sets: Rename set.intersection to set.inter. (#7622)Aina Niemetz
2021-11-09[proofs] Alethe: Translate Further Equality rules (#7606)Lachnitt
2021-11-09[proofs] Alethe: Translate Equality rules (#7605)Lachnitt
2021-11-09Only eliminate lambdas in higher-order elimination if ho-elim is enabled (#7603)Andrew Reynolds
2021-11-09Minor optimizations for term database (#7600)Andrew Reynolds
2021-11-09[proofs] Generalize trivial cycle detection in LazyCDProofChain (#7619)Haniel Barbosa
2021-11-09[proofs] Alethe: Translate REORDERING rule (#7533)Lachnitt
2021-11-09Preparation for non-constant lambda models (#7604)Andrew Reynolds
2021-11-09Make secant points user context dependent (#7567)Gereon Kremer
2021-11-09Remove redundant rules for generating Java and Python kinds. (#7616)Abdalrhman Mohamed
2021-11-09regex: Rename REGEXP_EMPTY and REGEXP_SIGMA to match SMT-LIB. (#7609)Aina Niemetz
2021-11-09Remove `CVC5Message` (#7610)Gereon Kremer
2021-11-09Remove antlr_tracing.h (#7608)Gereon Kremer
2021-11-09Remove more static option accesses (#7582)Gereon Kremer
2021-11-09Remove command-verbosity option (#7581)Gereon Kremer
2021-11-08Improve rendering of expert options. (#7589)Gereon Kremer
2021-11-08expand bag.choose operator (#7481)mudathirmahgoub
2021-11-08Add lambda lift utility (#7601)Andrew Reynolds
2021-11-08sets: Rename kinds with a more consistent naming scheme. (#7595)Aina Niemetz
2021-11-08Evaluate cast-to-real operator (#7599)Andrew Reynolds
2021-11-08[proofs] Adding NoSubtype node converter to Alethe (#7587)Haniel Barbosa
2021-11-08[proofs] Method to convert node representation of Alethe rule (#7598)Haniel Barbosa
2021-11-06Integrate java unit tests into ctest (#7593)Gereon Kremer
2021-11-06Print `unsupported` for unrecognized flags. (#7384)Abdalrhman Mohamed
2021-11-06better traces in node converter (#7590)Haniel Barbosa
2021-11-06Do not use extended rewrites on recursive function definitions (#7549)Andrew Reynolds
2021-11-06Remove `Notice()` in favor of new `verbose()` (#7588)Gereon Kremer
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback