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

2020-07-28	Ying Sheng	fixing issue #4808. (#4810)	commit \| commitdiff \| tree
2020-07-28	Andrew Reynolds	Remove arrays lazy rintro option (#4806)	commit \| commitdiff \| tree
2020-07-28	Andres Noetzli	Replace Expr with Node in Term/Op (#4781)	commit \| commitdiff \| tree
2020-07-28	Andrew Reynolds	Fix regular expression delta for complement (#4765)	commit \| commitdiff \| tree
2020-07-28	yoni206	Supporting seq.nth (#4723)	commit \| commitdiff \| tree
2020-07-28	Ying Sheng	Interpolation: Add interface for SyGuS interpolation...	commit \| commitdiff \| tree
2020-07-28	Andrew Reynolds	Use lemma property enum for OutputChannel::lemma (...	commit \| commitdiff \| tree
2020-07-27	Andrew Reynolds	(proof-new) Proof production for term formula removal...	commit \| commitdiff \| tree
2020-07-27	Andrew Reynolds	(proof-new) Arithmetic operator elim proof producing...	commit \| commitdiff \| tree
2020-07-27	Alex Ozdemir	Consider negation's proof before triggering arith pfs...	commit \| commitdiff \| tree
2020-07-21	Aina Niemetz	GH Actions: Cancel builds on push, remove redundant...	commit \| commitdiff \| tree
2020-07-21	Andrew Reynolds	Support uninterpreted constants in the evaluator (...	commit \| commitdiff \| tree
2020-07-21	Gereon Kremer	Preparations for a CAD-based arithmetic solver (#4762)	commit \| commitdiff \| tree
2020-07-20	Alex Ozdemir	Fix a deadlock in the signature tests. (#4772)	commit \| commitdiff \| tree
2020-07-18	Haniel Barbosa	Improving equality engine tracing (#4770)	commit \| commitdiff \| tree
2020-07-18	Andrew Reynolds	(proof-new) Proof recording for assertions pipeline...	commit \| commitdiff \| tree
2020-07-18	Andrew Reynolds	Enumerate shapes feature in fast sygus enumerator ...	commit \| commitdiff \| tree
2020-07-17	Andres Noetzli	Add NodeManagerScopes to fix use-after-free issues...	commit \| commitdiff \| tree
2020-07-17	Andrew Reynolds	Replace options listener infrastructure (#4764)	commit \| commitdiff \| tree
2020-07-17	Andrew V. Jones	Support for using 'libedit' over 'readline' #4571 ...	commit \| commitdiff \| tree
2020-07-17	Andrew Reynolds	(proof-new) Updates to strings core solver (#4642)	commit \| commitdiff \| tree
2020-07-17	Andrew Reynolds	Add option manager and simpler option listener (#4745)	commit \| commitdiff \| tree
2020-07-17	Gereon Kremer	Integration of libpoly (#4679)	commit \| commitdiff \| tree
2020-07-17	Haniel Barbosa	Fix EqProof to ProofNode conversion (#4760)	commit \| commitdiff \| tree
2020-07-16	Haniel Barbosa	(proof-new) Implements the conversion between EqProof...	commit \| commitdiff \| tree
2020-07-16	Gereon Kremer	Resource manager cleanup (#4732)	commit \| commitdiff \| tree
2020-07-16	Andrew Reynolds	Split abstract values utility from SmtEngine (#4754)	commit \| commitdiff \| tree
2020-07-16	Andrew Reynolds	Make ExtTheory a utility and not a member of Theory...	commit \| commitdiff \| tree
2020-07-16	Gereon Kremer	Remove cumulative time limits and cpu time limits ...	commit \| commitdiff \| tree
2020-07-16	Gereon Kremer	Fixes memory leak when an exception goes through runCvc4...	commit \| commitdiff \| tree
2020-07-16	Haniel Barbosa	(proof-new) Adding API for converting EqProof into...	commit \| commitdiff \| tree
2020-07-15	Andres Noetzli	Use Nodes for SmtEngine assertions (#4752)	commit \| commitdiff \| tree
2020-07-15	Andrew Reynolds	Split abduction solver from SmtEngine (#4733)	commit \| commitdiff \| tree
2020-07-15	Andres Noetzli	Use TypeNode in UninterpretedConstant (#4748)	commit \| commitdiff \| tree
2020-07-15	Gereon Kremer	Add missing header (Fixes #4743) (#4749)	commit \| commitdiff \| tree
2020-07-15	Andrew Reynolds	Simplify entailment check interface (#4744)	commit \| commitdiff \| tree
2020-07-14	Andrew Reynolds	Make use of options in setDefaults more consistent...	commit \| commitdiff \| tree
2020-07-14	Andrew Reynolds	Remove sygus print callback (#4727)	commit \| commitdiff \| tree
2020-07-14	Andrew Reynolds	Fix regression output. (#4741)	commit \| commitdiff \| tree
2020-07-14	Andrew Reynolds	(proof-new) Skeleton proof support in the Rewriter...	commit \| commitdiff \| tree
2020-07-14	Andres Noetzli	Use TypeNode in EmptySet (#4740)	commit \| commitdiff \| tree
2020-07-14	Andrew Reynolds	Debug instantiations output (#4739)	commit \| commitdiff \| tree
2020-07-14	Andrew Reynolds	Minor refactoring of subsolver initialization (#4731)	commit \| commitdiff \| tree
2020-07-14	Andres Noetzli	Fix caching in TheoryEngine::getExplanation() (#4736)	commit \| commitdiff \| tree
2020-07-14	Haniel Barbosa	Fix options messages that were inverted (#4734)	commit \| commitdiff \| tree
2020-07-14	Andres Noetzli	Use TypeNode/Node in ArrayStoreAll (#4728)	commit \| commitdiff \| tree
2020-07-14	Andrew Reynolds	Fix type comparisons involving pointer. (#4738)	commit \| commitdiff \| tree
2020-07-14	Andrew Reynolds	Fix whitespace issue in instantiations output. (#4737)	commit \| commitdiff \| tree
2020-07-13	Andrew Reynolds	(proof-new) SMT Preprocess proof generator (#4708)	commit \| commitdiff \| tree
2020-07-13	Andrew Reynolds	User-facing print debug option for sygus candidates...	commit \| commitdiff \| tree
2020-07-13	Andrew Reynolds	Statistics on instantiations per quantified formula...	commit \| commitdiff \| tree
2020-07-13	Gereon Kremer	Implement --tlimit for windows (#4716)	commit \| commitdiff \| tree
2020-07-13	Andrew Reynolds	Add support for string/sequence update (#4725)	commit \| commitdiff \| tree
2020-07-13	Andres Noetzli	Remove ExprSequence (#4724)	commit \| commitdiff \| tree
2020-07-11	Andrew Reynolds	Cache explanations in TheoryEngine::getExplanation...	commit \| commitdiff \| tree
2020-07-11	yoni206	Changing bv_to_int options (#4721)	commit \| commitdiff \| tree
2020-07-11	Haniel Barbosa	Adding test for whether a kind is n-ary (#4718)	commit \| commitdiff \| tree
2020-07-11	Andrew V. Jones	Add support for printing 'get-abduct' in verbose mode...	commit \| commitdiff \| tree
2020-07-11	Andrew Reynolds	(proof-new) Add ONCE and FIXPOINT modes for term conversion...	commit \| commitdiff \| tree
2020-07-11	Andrew Reynolds	(proof-new) Update Theory interface for proof-new ...	commit \| commitdiff \| tree
2020-07-10	Andres Noetzli	Always Update Git information when rebuilding (#4696)	commit \| commitdiff \| tree
2020-07-10	Andrew Reynolds	Front end support for integer AND (#4717)	commit \| commitdiff \| tree
2020-07-10	Ying Sheng	[Interpolation] Add interface for SyGuS interpolation...	commit \| commitdiff \| tree
2020-07-10	Gereon Kremer	Add deps/install/lib to RPATH and warn user when using...	commit \| commitdiff \| tree
2020-07-10	Andrew Reynolds	Update competition scripts (#4715)	commit \| commitdiff \| tree
2020-07-10	Andrew Reynolds	Ensure legal elimination for witness rewrite (#4688)	commit \| commitdiff \| tree
2020-07-09	Andrew Reynolds	Disable unsat cores in timeout regression (#4713)	commit \| commitdiff \| tree
2020-07-09	Andrew Reynolds	Associate all lemmas in non-linear arithmetic with...	commit \| commitdiff \| tree
2020-07-09	Andrew Reynolds	(proof-new) Theory engine proof generator (#4657)	commit \| commitdiff \| tree
2020-07-08	Gereon Kremer	Re-implement handling of --tlimit (#4655)	commit \| commitdiff \| tree
2020-07-08	Mathias Preiner	Add getName() method to options. (#4704)	commit \| commitdiff \| tree
2020-07-08	Andrew Reynolds	Always interleave theory combination with quantifiers...	commit \| commitdiff \| tree
2020-07-08	Andrew Reynolds	Improve and fix secant and tangent lemmas in the transcenden...	commit \| commitdiff \| tree
2020-07-07	Andrew Reynolds	Transfer ownership of internal Options from NodeManager...	commit \| commitdiff \| tree
2020-07-07	Andrew V. Jones	Increase the minimum version of CMake due to the use...	commit \| commitdiff \| tree
2020-07-06	Andrew Reynolds	Front end support for sequences (#4690)	commit \| commitdiff \| tree
2020-07-06	Andres Noetzli	[GitHub] Add link to fuzzing guidelines in issues ...	commit \| commitdiff \| tree
2020-07-03	Andres Noetzli	Remove SWIG bindings (#4683)	commit \| commitdiff \| tree
2020-07-02	Andrew Reynolds	Fix regression option (#4680)	commit \| commitdiff \| tree
2020-07-02	Andrew Reynolds	(proof-new) Updates to skolem manager interface (...	commit \| commitdiff \| tree
2020-07-02	Andrew Reynolds	(proof-new) Proof rule checkers run on skolem forms...	commit \| commitdiff \| tree
2020-07-02	Andrew Reynolds	(proof-new) Proof node updater (#4647)	commit \| commitdiff \| tree
2020-07-01	Andrew Reynolds	Add solver for integer AND (#4681)	commit \| commitdiff \| tree
2020-07-01	Andres Noetzli	Add testing infrastructure for LFSC signatures (#4678)	commit \| commitdiff \| tree
2020-07-01	Andrew Reynolds	Inferences and model construction taking into account...	commit \| commitdiff \| tree
2020-07-01	Andrew Reynolds	(proof-new) Updates to evaluator (#4659)	commit \| commitdiff \| tree
2020-07-01	Andrew Reynolds	(proof-new) Improve rewriter for WITNESS (#4661)	commit \| commitdiff \| tree
2020-06-30	Andrew Reynolds	Fix normal form for re.comp (#4676)	commit \| commitdiff \| tree
2020-06-30	Andres Noetzli	Update NEWS post 1.8 release (#4666)	commit \| commitdiff \| tree
2020-06-30	Mathias Preiner	Fix GMP compilation for win64. (#4675)	commit \| commitdiff \| tree
2020-06-30	Andrew Reynolds	Simplify quantifiers strategy for when to apply last...	commit \| commitdiff \| tree
2020-06-30	Ying Sheng	Interpolation step 1 (#4638)	commit \| commitdiff \| tree
2020-06-30	Mathias Preiner	contrib: Update to GMP 6.2.0, compile static and shared...	commit \| commitdiff \| tree
2020-06-30	Andrew Reynolds	Add internal support for integer and operator (#4668)	commit \| commitdiff \| tree
2020-06-29	Andres Noetzli	Make ExprManager constructor private (#4669)	commit \| commitdiff \| tree
2020-06-29	makaimann	Python Sort tests (#4639)	commit \| commitdiff \| tree
2020-06-29	Andres Noetzli	Fix memory leak in unit test node_algorithm_black ...	commit \| commitdiff \| tree
2020-06-28	Andrew Reynolds	Fix non-termination issues in simpleRegExpConsume ...	commit \| commitdiff \| tree
2020-06-28	Alex Ozdemir	Proof Rules and Checker for Arithmetic (#4665)	commit \| commitdiff \| tree
2020-06-27	Andres Noetzli	Add API for retrieving separation heap/nil term (#4663)	commit \| commitdiff \| tree
next

RSS Atom