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

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
2021-11-05	Andres Noetzli	[FP] Do not assert that model has shared term (#7585)	commit \| commitdiff \| tree
2021-11-05	Gereon Kremer	Fix some issues with the java api (#7583)	commit \| commitdiff \| tree
2021-11-05	Lachnitt	Alethe: Translate CNF rules (#7532)	commit \| commitdiff \| tree
2021-11-05	Haniel Barbosa	Minor changes to circuit propagator (#7584)	commit \| commitdiff \| tree
2021-11-05	Andrew Reynolds	Remove many static calls to rewrite (#7580)	commit \| commitdiff \| tree
2021-11-05	Gereon Kremer	Remove quadratic solving in NlModel (#7542)	commit \| commitdiff \| tree
2021-11-05	Gereon Kremer	Eliminate `Warning` macro in favor of `EnvObj::warning...	commit \| commitdiff \| tree
2021-11-05	Gereon Kremer	Remove a bunch of debugging/logging code from the linear...	commit \| commitdiff \| tree
2021-11-04	Andrew Reynolds	Add -o sygus-grammar to print auto-generated SyGuS...	commit \| commitdiff \| tree
2021-11-04	Andrew Reynolds	Improve defaults for sygus default grammars (#7553)	commit \| commitdiff \| tree
2021-11-04	Andrew Reynolds	Replace the old dump infrastructure (#7572)	commit \| commitdiff \| tree
2021-11-04	Gereon Kremer	Start refactoring of `-o` and `-v` (#7449)	commit \| commitdiff \| tree
2021-11-04	Gereon Kremer	Refactor 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 Kremer	Enable CDCAC solver for selected quantified logics...	commit \| commitdiff \| tree
2021-11-04	Gereon Kremer	Add support for special tag collectors (#7562)	commit \| commitdiff \| tree
2021-11-04	Gereon Kremer	Minor cleanup in SolverEngine::setInfo() (#7566)	commit \| commitdiff \| tree
2021-11-04	Andres Noetzli	Make `Theory::get()` private (#7518)	commit \| commitdiff \| tree
2021-11-03	Aina Niemetz	api: Rename some separation logic functions for consistency...	commit \| commitdiff \| tree
2021-11-03	Aina Niemetz	Add unit test to cover previous failure with second...	commit \| commitdiff \| tree
2021-11-03	mudathirmahgoub	Enable CI for Junit tests (#7436)	commit \| commitdiff \| tree
2021-11-03	Andrew Reynolds	Fix debug trace for miplib (#7563)	commit \| commitdiff \| tree
2021-11-03	Andrew Reynolds	Refactor skolem construction (#7561)	commit \| commitdiff \| tree
2021-11-03	Andrew Reynolds	Formalize more string skolems (#7554)	commit \| commitdiff \| tree
2021-11-03	Andrew Reynolds	Fix preregistration for floating point theory (#7558)	commit \| commitdiff \| tree
2021-11-02	Mathias Preiner	bv: Disable equality engine for --bitblast=eager and...	commit \| commitdiff \| tree
2021-11-02	Abdalrhman Mohamed	Move `fmf.card` printing code. (#7559)	commit \| commitdiff \| tree
2021-11-02	Abdalrhman Mohamed	Add printing methods for some commands. (#7557)	commit \| commitdiff \| tree
2021-11-02	Andrew Reynolds	Improve syntax for fmf cardinality constraints (#7556)	commit \| commitdiff \| tree
2021-11-02	Andrew Reynolds	Add LFSC signature for quantifiers (#7540)	commit \| commitdiff \| tree
2021-11-02	Mathias Preiner	Fix setDefaults() for proofs with bitblast-internal...	commit \| commitdiff \| tree
2021-11-02	Mathias Preiner	bv: Remove remaining Rewriter::rewrite calls. (#7545)	commit \| commitdiff \| tree
2021-11-02	Andrew Reynolds	Make quant elimination robust to presence of other...	commit \| commitdiff \| tree
2021-11-01	Andrew Reynolds	Eliminate calls to Rewriter::rewrite and options::...	commit \| commitdiff \| tree
2021-11-01	Andrew Reynolds	Weaken assertion in CEGQI (#7548)	commit \| commitdiff \| tree
2021-11-01	Gereon Kremer	Add explicit option enum value __MAX_VALUE (#7547)	commit \| commitdiff \| tree
2021-11-01	Mathias Preiner	bv: Remove layered solver. (#7455)	commit \| commitdiff \| tree
2021-11-01	Aina Niemetz	api: Fix documentation for kind IAND. (#7536)	commit \| commitdiff \| tree
2021-11-01	Gereon Kremer	Fix a couple of issues with uploading docs for releases...	commit \| commitdiff \| tree
2021-11-01	Gereon Kremer	Clean up CLN includes (#7544)	commit \| commitdiff \| tree
2021-11-01	Gereon Kremer	Add fuzzing target for murxla (#7490)	commit \| commitdiff \| tree
2021-11-01	Andrew Reynolds	Fix upwards closure for relations (#7515)	commit \| commitdiff \| tree
2021-11-01	Gereon Kremer	Replace more static options accesses (#7531)	commit \| commitdiff \| tree
2021-11-01	Gereon Kremer	Refactor DidYouMean (#7535)	commit \| commitdiff \| tree
2021-10-31	Mathias Preiner	api: Add guard against querying value from term with...	commit \| commitdiff \| tree
2021-10-31	mudathirmahgoub	Fix soundess issue for bags with negative multiplicity...	commit \| commitdiff \| tree
2021-10-31	mudathirmahgoub	Remove assertSkeleton for bag elements during model...	commit \| commitdiff \| tree
2021-10-29	Gereon Kremer	Fix proof of nl lemma for a corner case (#7530)	commit \| commitdiff \| tree
2021-10-29	Gereon Kremer	Remove options::X__numValues (#7419)	commit \| commitdiff \| tree
2021-10-29	Andrew Reynolds	Minor cleanup of proof messages (#7494)	commit \| commitdiff \| tree
2021-10-29	Andrew Reynolds	Fix model construction for higher order involving irrelevant...	commit \| commitdiff \| tree
2021-10-29	Andrew Reynolds	Add PfRule ARITH_POLY_NORM (#7501)	commit \| commitdiff \| tree
2021-10-29	Andrew Reynolds	Improvements for LFSC proof conversion (#7524)	commit \| commitdiff \| tree
2021-10-29	Gereon Kremer	Remove static access to options in decision folder...	commit \| commitdiff \| tree
2021-10-28	Gereon Kremer	Fix proof for xor in circuit propagator (#7525)	commit \| commitdiff \| tree
2021-10-28	Gereon Kremer	Combine `--static` and `--static-binary` (#7520)	commit \| commitdiff \| tree
2021-10-28	Haniel Barbosa	[proofs] Fix assertion in EqProof conversion (#7522)	commit \| commitdiff \| tree
2021-10-28	Andrew V. Jones	Add support for checking if a `-Wno` flag exists before...	commit \| commitdiff \| tree
2021-10-28	Abdalrhman Mohamed	Add a `define-fun` command for each `:named` term....	commit \| commitdiff \| tree
2021-10-28	Andrew Reynolds	Properly guard proof construction for STRINGS_EXTF_EQ_REW...	commit \| commitdiff \| tree
2021-10-28	Andrew Reynolds	LFSC signature for linear arithmetic (#7445)	commit \| commitdiff \| tree
2021-10-28	Andrew Reynolds	LFSC signature for CNF (#7444)	commit \| commitdiff \| tree
2021-10-28	Andrew Reynolds	LFSC signature for Booleans (#7443)	commit \| commitdiff \| tree
2021-10-28	Andrew Reynolds	LFSC signature for equality (#7442)	commit \| commitdiff \| tree
2021-10-28	Abdalrhman Mohamed	Fix `(set-info <sexpr>)` parsing and printing bugs...	commit \| commitdiff \| tree
2021-10-28	Gereon Kremer	Remove separate cpp docs for UnknownExplanation (#7516)	commit \| commitdiff \| tree
2021-10-28	Gereon Kremer	Build shared and static in CI (#7472)	commit \| commitdiff \| tree
2021-10-27	Andrew Reynolds	Add missing API checks to getValue (#7475)	commit \| commitdiff \| tree
2021-10-27	Gereon Kremer	Add comments for arith type rules. (#7488)	commit \| commitdiff \| tree
2021-10-27	Gereon Kremer	Add documentation on output tags (#7499)	commit \| commitdiff \| tree
2021-10-27	Andres Noetzli	[Regression Script] Fix use of undefined variables...	commit \| commitdiff \| tree
2021-10-27	Gereon Kremer	Fix patching for poly on windows (#7513)	commit \| commitdiff \| tree
2021-10-27	Andres Noetzli	Require ITE branches to be first class types (#7508)	commit \| commitdiff \| tree
2021-10-27	Andrew Reynolds	Fix care graph computation for higher-order (#7474)	commit \| commitdiff \| tree
2021-10-27	Andrew Reynolds	Fix model unsoundness for relation join (#7511)	commit \| commitdiff \| tree
2021-10-27	yoni206	Python api documentation for sorts (#7440)	commit \| commitdiff \| tree
2021-10-27	Andrew Reynolds	Avoid non-terminating check with assumptions in strings...	commit \| commitdiff \| tree
2021-10-27	Andrew Reynolds	Deterministic variables for RE elim (#7489)	commit \| commitdiff \| tree
2021-10-27	mudathirmahgoub	Fix mac compile errors in sort.cpp (#7507)	commit \| commitdiff \| tree
2021-10-27	Gereon Kremer	Make --version exit (#7506)	commit \| commitdiff \| tree
next

RSS Atom