git.libre-soc.org Git - cvc5.git/search

2021-11-23	Andrew Reynolds	Make difficulty manager only consider lemmas at full...	commit \| commitdiff \| tree
2021-11-23	Andrew Reynolds	Enable model-based reduction technique for strings...	commit \| commitdiff \| tree
2021-11-23	Gereon Kremer	Add kinds to python docs (#7672)	commit \| commitdiff \| tree
2021-11-23	Gereon Kremer	Push output language inside the printing code (#7683)	commit \| commitdiff \| tree
2021-11-23	mudathirmahgoub	Add rewrite rule for bag.card operator using bag.map...	commit \| commitdiff \| tree
2021-11-23	yoni206	Python API documentation: terms (#7659)	commit \| commitdiff \| tree
2021-11-23	Andres Noetzli	Make `node_value.h` not depend on `node_manager.h`...	commit \| commitdiff \| tree
2021-11-22	Gereon Kremer	Refactor IO stream manipulators (#7555)	commit \| commitdiff \| tree
2021-11-22	Andrew Reynolds	Add rewrite for repeated re.allchar (#7681)	commit \| commitdiff \| tree
2021-11-22	Gereon Kremer	Set proper system processor for arm64 toolchain (#7665)	commit \| commitdiff \| tree
2021-11-22	Haniel Barbosa	[prop] Remove unused #define in theory proxy (#7670)	commit \| commitdiff \| tree
2021-11-22	Andrew Reynolds	Improve error for check theory assertions with model...	commit \| commitdiff \| tree
2021-11-22	Andrew Reynolds	Fix const RE test for internal regexp rv kind (#7678)	commit \| commitdiff \| tree
2021-11-20	yoni206	bv2int module: translation of more cases (#7653) https://github.com/cvc5/cvc5-projects/issues/345 https://github.com/cvc5/cvc5-projects/issues/344 https://github.com/cvc5/cvc5-projects/issues/343	commit \| commitdiff \| tree
2021-11-19	Andres Noetzli	[API] Avoid copying values (#7666)	commit \| commitdiff \| tree
2021-11-19	Andres Noetzli	Clean up relationship of metakind and node_manager...	commit \| commitdiff \| tree
2021-11-19	Andrew Reynolds	Remove n-ary builder (#7671)	commit \| commitdiff \| tree
2021-11-19	Mathias Preiner	Allow negative denominator for CLN Rationals constructed...	commit \| commitdiff \| tree
2021-11-18	Aina Niemetz	api: Fix categorization of DT kinds in kind maps. ...	commit \| commitdiff \| tree
2021-11-18	Gereon Kremer	Refactor CAD option for linear model seed (#7657)	commit \| commitdiff \| tree
2021-11-18	Haniel Barbosa	[proofs] Fix trace in SatProofManager (#7664)	commit \| commitdiff \| tree
2021-11-18	Lachnitt	[proofs] Alethe: Rename DUPLICATED_LITERALS (#7661)	commit \| commitdiff \| tree
2021-11-18	Aina Niemetz	api: Fix kind documentation for BAG_MAKE. (#7663)	commit \| commitdiff \| tree
2021-11-17	Haniel Barbosa	Improve naming in term canonization when handling HO...	commit \| commitdiff \| tree
2021-11-17	Haniel Barbosa	[sat] Fix indentation in "reason" (#7662)	commit \| commitdiff \| tree
2021-11-17	Gereon Kremer	Add documentation for z3py compatibility API (#7652)	commit \| commitdiff \| tree
2021-11-17	Andrew Reynolds	Preparations for eliminating arithmetic subtyping ...	commit \| commitdiff \| tree
2021-11-17	Andrew Reynolds	Revert change and clean datatypes cons candidate generator...	commit \| commitdiff \| tree
2021-11-17	Gereon Kremer	Implement aggressive pruning in CAD solver (#7650)	commit \| commitdiff \| tree
2021-11-17	Alex Ozdemir	Update Python packaging infrastructure (#7654)	commit \| commitdiff \| tree
2021-11-17	Gereon Kremer	make default and modes strings instead of enum values...	commit \| commitdiff \| tree
2021-11-17	Andres Noetzli	Fix binding of quoted symbols in `define-fun` (#7655)	commit \| commitdiff \| tree
2021-11-17	Alex Ozdemir	Remove documentation for --lib-only (#7648)	commit \| commitdiff \| tree
2021-11-17	mudathirmahgoub	Update SimpleVC.java (#7647)	commit \| commitdiff \| tree
2021-11-16	yoni206	Translating API tests to Python — part 1 (#7597)	commit \| commitdiff \| tree
2021-11-16	mudathirmahgoub	Fix compile errors with java examples (#7646)	commit \| commitdiff \| tree
2021-11-16	Haniel Barbosa	[proofs] Make sure --proof-check=... is no-op when...	commit \| commitdiff \| tree
2021-11-16	Andres Noetzli	Refactor `metakind` (#7639)	commit \| commitdiff \| tree
2021-11-15	Aina Niemetz	api: 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	mudathirmahgoub	Add documentation for theory_bags_type_rules.h (#7642)	commit \| commitdiff \| tree
2021-11-13	Andres Noetzli	Skip `str.code` inferences for sequence eqcs (#7644)	commit \| commitdiff \| tree
2021-11-13	mudathirmahgoub	Fix type error for rewriting bag.map bag.union_disjoint...	commit \| commitdiff \| tree
2021-11-13	mudathirmahgoub	Add operator set.map to theory of sets (#7641)	commit \| commitdiff \| tree
2021-11-12	mudathirmahgoub	bags: 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 Noetzli	Fix redundant definitions of `NodeValue::getConst`...	commit \| commitdiff \| tree
2021-11-12	Andrew Reynolds	Add some basic rewrites for regular expression intersection...	commit \| commitdiff \| tree
2021-11-12	Andres Noetzli	Remove `ConstantMap<Rational>` (#7635)	commit \| commitdiff \| tree
2021-11-12	Gereon Kremer	Various minor docs improvements (#7626)	commit \| commitdiff \| tree
2021-11-11	Abdalrhman Mohamed	Add an API method to get the raw name of a term. (...	commit \| commitdiff \| tree
2021-11-11	Andrew Reynolds	Generalize front-end checks to check for shadowed variables...	commit \| commitdiff \| tree
2021-11-11	Andrew Reynolds	Add lazy approach for handling lambdas in the HO extension...	commit \| commitdiff \| tree
2021-11-11	Andrew Reynolds	Fixes for update/nth over constant sequences (#7631)	commit \| commitdiff \| tree
2021-11-10	Aina Niemetz	api: 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 Preiner	docs: Also create javadoc for generated Kind.java ...	commit \| commitdiff \| tree
2021-11-10	mudathirmahgoub	Fix soundness issue of missing premises for count bag...	commit \| commitdiff \| tree
2021-11-10	Mathias Preiner	java: Fix building cvc5.jar for cmake 3.16. (#7623)	commit \| commitdiff \| tree
2021-11-10	Andrew Reynolds	Fix parsing array constants (#7617)	commit \| commitdiff \| tree
2021-11-10	Aina Niemetz	sets: Rename set.intersection to set.inter. (#7622)	commit \| commitdiff \| tree
2021-11-10	Aina Niemetz	Reorganize 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 Reynolds	Only eliminate lambdas in higher-order elimination...	commit \| commitdiff \| tree
2021-11-09	Andrew Reynolds	Minor optimizations for term database (#7600)	commit \| commitdiff \| tree
2021-11-09	Aina Niemetz	Clean up ctest configuration and CI test configuration...	commit \| commitdiff \| tree
2021-11-09	Haniel Barbosa	[proofs] Generalize trivial cycle detection in LazyCDProofCh...	commit \| commitdiff \| tree
2021-11-09	Lachnitt	[proofs] Alethe: Translate REORDERING rule (#7533)	commit \| commitdiff \| tree
2021-11-09	Aina Niemetz	sets: Update theory reference and smt2 examples. (...	commit \| commitdiff \| tree
2021-11-09	Andrew Reynolds	Preparation for non-constant lambda models (#7604)	commit \| commitdiff \| tree
2021-11-09	Gereon Kremer	Make secant points user context dependent (#7567)	commit \| commitdiff \| tree
2021-11-09	Abdalrhman Mohamed	Remove redundant rules for generating Java and Python...	commit \| commitdiff \| tree
2021-11-09	Andrew Reynolds	Add LFSC signature for strings (#7523)	commit \| commitdiff \| tree
2021-11-09	Aina Niemetz	regex: Rename REGEXP_EMPTY and REGEXP_SIGMA to match...	commit \| commitdiff \| tree
2021-11-09	Gereon Kremer	Remove `CVC5Message` (#7610)	commit \| commitdiff \| tree
2021-11-09	Gereon Kremer	Remove antlr_tracing.h (#7608)	commit \| commitdiff \| tree
2021-11-09	Gereon Kremer	Remove more static option accesses (#7582)	commit \| commitdiff \| tree
2021-11-09	Gereon Kremer	Remove command-verbosity option (#7581)	commit \| commitdiff \| tree
2021-11-09	Mathias Preiner	cmake: Use fastcov for generating coverage reports...	commit \| commitdiff \| tree
2021-11-08	Gereon Kremer	Improve rendering of expert options. (#7589)	commit \| commitdiff \| tree
2021-11-08	mudathirmahgoub	expand bag.choose operator (#7481)	commit \| commitdiff \| tree
2021-11-08	Andrew Reynolds	Add lambda lift utility (#7601)	commit \| commitdiff \| tree
2021-11-08	Aina Niemetz	sets: Rename kinds with a more consistent naming scheme...	commit \| commitdiff \| tree
2021-11-08	Andrew Reynolds	Evaluate 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 Alethe...	commit \| commitdiff \| tree
2021-11-06	Gereon Kremer	Integrate java unit tests into ctest (#7593)	commit \| commitdiff \| tree
2021-11-06	Abdalrhman Mohamed	Print `unsupported` for unrecognized flags. (#7384)	commit \| commitdiff \| tree
2021-11-06	Haniel Barbosa	better traces in node converter (#7590)	commit \| commitdiff \| tree
2021-11-06	Andrew Reynolds	Do not use extended rewrites on recursive function...	commit \| commitdiff \| tree
2021-11-06	Gereon Kremer	Only run regress0 for static build (#7592)	commit \| commitdiff \| tree
2021-11-06	Gereon Kremer	Remove `Notice()` in favor of new `verbose()` (#7588)	commit \| commitdiff \| tree
2021-11-06	Mathias Preiner	Disable regress2 test. (#7591)	commit \| commitdiff \| tree
2021-11-05	Andrew Reynolds	Fix 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 Reynolds	Eliminate a level of nesting of traversals in theory...	commit \| commitdiff \| tree
2021-11-05	Gereon Kremer	Remove `Chat()` in favor of new `verbose()` (#7586)	commit \| commitdiff \| tree
2021-11-05	Andrew Reynolds	Move functions and lambdas from builtin to uf (#7570)	commit \| commitdiff \| tree
next

RSS Atom