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

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
2021-10-27	Gereon Kremer	Fix libpoly build on windows (#7502)	commit \| commitdiff \| tree
2021-10-26	Haniel Barbosa	[proofs] Fix singleton check in MACRO_RES post-processing...	commit \| commitdiff \| tree
2021-10-26	Haniel Barbosa	[proofs] Modularize check for whether a clause is singleton...	commit \| commitdiff \| tree
2021-10-26	Haniel Barbosa	[proofs] Reset local var in SatProofManager since incrementa...	commit \| commitdiff \| tree
2021-10-26	Andrew Reynolds	Disable automatic symmetry in proofs of theory explanations...	commit \| commitdiff \| tree
2021-10-26	Haniel Barbosa	[proofs] Fix and simplify CHAIN_RESOLUTION checker...	commit \| commitdiff \| tree
2021-10-26	Andrew Reynolds	Add regressions for fixed issues (#7495)	commit \| commitdiff \| tree
2021-10-26	Andrew Reynolds	Disable sygus-inst when incremental (#7485)	commit \| commitdiff \| tree
2021-10-26	Lachnitt	[proofs] Alethe: Translate Block of clause pattern...	commit \| commitdiff \| tree
2021-10-26	Lachnitt	[proofs] Alethe: Translate AND_INTRO rule (#7405)	commit \| commitdiff \| tree
2021-10-26	Lachnitt	[proofs] Alethe: Translate AND_ELIM rule (#7404)	commit \| commitdiff \| tree
2021-10-26	Lachnitt	[proofs] Alethe: Translate CONTRA rule (#7403)	commit \| commitdiff \| tree
2021-10-26	Gereon Kremer	Upload docs for tags to docs-releases (#7415)	commit \| commitdiff \| tree
2021-10-26	Gereon Kremer	Fix frequent rebuild of options target (#7450)	commit \| commitdiff \| tree
2021-10-26	Gereon Kremer	Fix Configuration::isStaticBuild (#7456)	commit \| commitdiff \| tree
2021-10-26	Lachnitt	[proofs] Alethe: Translate NOT_NOT_ELIM rule (#7402)	commit \| commitdiff \| tree
2021-10-25	Lachnitt	[proofs] Alethe: Translate MODUS_PONENS rule (#7401)	commit \| commitdiff \| tree
2021-10-25	Andrew Reynolds	Add new method for enumerating unsat queries with SyGuS...	commit \| commitdiff \| tree
2021-10-25	Lachnitt	[proofs] Alethe: Translate EQ_RESOLVE rule (#7400)	commit \| commitdiff \| tree
2021-10-25	Andrew Reynolds	Fix spurious checks to closed proofs (#7484)	commit \| commitdiff \| tree
2021-10-25	Andrew Reynolds	Java and python unit tests for mkCardinalityConstraint...	commit \| commitdiff \| tree
2021-10-25	Andrew Reynolds	Fix more missing uses of CDProof::isSame (#7491)	commit \| commitdiff \| tree
2021-10-25	Andrew Reynolds	Fix support for global declarations (#7480)	commit \| commitdiff \| tree
2021-10-25	Andrew Reynolds	Remove HOL/fmf bound messages in set defaults (#7487)	commit \| commitdiff \| tree
2021-10-25	mudathirmahgoub	Add inference for count map (#7264)	commit \| commitdiff \| tree
2021-10-25	Andrew Reynolds	Reenable proofs on some regressions (#7483)	commit \| commitdiff \| tree
2021-10-25	Lachnitt	[proofs] Alethe: Translate SPLIT rule (#7399)	commit \| commitdiff \| tree
2021-10-25	Andres Noetzli	[Regression Script] Support older Python versions ...	commit \| commitdiff \| tree
2021-10-24	mudathirmahgoub	Delete redundant file option_Info.cpp (#7477)	commit \| commitdiff \| tree
2021-10-24	Andrew Reynolds	Add new eager conflict detection in strings for integer...	commit \| commitdiff \| tree
2021-10-23	Andrew Reynolds	Remove spurious assertoin (#7458)	commit \| commitdiff \| tree
2021-10-22	Andrew Reynolds	Add requires libpoly to regression (#7467)	commit \| commitdiff \| tree
2021-10-22	mudathirmahgoub	Refactor java package name from cvc5 to io.github.cvc5... ...java package name from cvc5 to io.github.cvc5.api (#7340) ...java package name from cvc5 to io.github.cvc5.api.	commit \| commitdiff \| tree
2021-10-22	Gereon Kremer	Remove options::X__name (#7414)	commit \| commitdiff \| tree
2021-10-22	Andrew Reynolds	Remove stale pointer to proof node manager from skolemize...	commit \| commitdiff \| tree
2021-10-22	Haniel Barbosa	[proof] Fixing CHAIN_RESOLUTION checker (#7465)	commit \| commitdiff \| tree
2021-10-22	Gereon Kremer	Fix out-of-sync pruning in CDCAC proofs (#7470)	commit \| commitdiff \| tree
2021-10-22	Gereon Kremer	Fix another double negation proof issue (#7468)	commit \| commitdiff \| tree
2021-10-22	Andrew Reynolds	Remove `--uf-ho` option (#7463)	commit \| commitdiff \| tree
2021-10-22	Andrew Reynolds	Fix symmetry issue in theory engine conflicts (#7469)	commit \| commitdiff \| tree
2021-10-22	Andrew Reynolds	Add more abduction regressions (#7461)	commit \| commitdiff \| tree
2021-10-22	Lachnitt	[proofs] Alethe: Translate FACTORING rule (#7398)	commit \| commitdiff \| tree
2021-10-22	Lachnitt	[proofs] Alethe: Translate CHAIN_RESOLUTION rule (...	commit \| commitdiff \| tree
next

RSS Atom