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

2020-11-02	Andrew Reynolds	Update strings proxy variable map to be context independent...	commit \| commitdiff \| tree
2020-11-02	Andrew Reynolds	Miscellaneous cleaning of parser (#5369)	commit \| commitdiff \| tree
2020-11-02	Andrew Reynolds	Avoid dynamic allocation in symbol table implementation...	commit \| commitdiff \| tree
2020-10-30	Andrew Reynolds	Update api::Sort to use TypeNode instead of Type (...	commit \| commitdiff \| tree
2020-10-29	Andrew Reynolds	Set strings pending conflict flag (#5364)	commit \| commitdiff \| tree
2020-10-29	Andrew Reynolds	(proof-new) Update the strings inference manager for...	commit \| commitdiff \| tree
2020-10-28	Andrew Reynolds	Remove more uses of Expr (#5357)	commit \| commitdiff \| tree
2020-10-28	Andrew Reynolds	Fixes for unconstrained variables in nonlinear model...	commit \| commitdiff \| tree
2020-10-28	Andrew Reynolds	Convert symbol table from Expr-level to Term-level...	commit \| commitdiff \| tree
2020-10-28	Andrew Reynolds	Add rewrites for div/mod in the arithmetic rewriter...	commit \| commitdiff \| tree
2020-10-27	Andrew Reynolds	Add missing methods involving datatype sorts to the...	commit \| commitdiff \| tree
2020-10-26	Andrew Reynolds	(proof-new) Add datatypes proof checker (#5340)	commit \| commitdiff \| tree
2020-10-26	Andrew Reynolds	Send external equalities from collapse selector as...	commit \| commitdiff \| tree
2020-10-23	Andrew Reynolds	Apply alpha equivalence to annotated quantified formulas...	commit \| commitdiff \| tree
2020-10-23	Andrew Reynolds	Change datatypes lemma policy for equalities not coming...	commit \| commitdiff \| tree
2020-10-23	Andrew Reynolds	Fix related to preregistering boolean term variables...	commit \| commitdiff \| tree
2020-10-22	Andrew Reynolds	Remove unused equality engine types (#5319)	commit \| commitdiff \| tree
2020-10-22	Andrew Reynolds	(proof-new) Make theory preprocessor user-context dependent...	commit \| commitdiff \| tree
2020-10-21	Andrew Reynolds	(proof-new) Updates to lazy proof chain (#5317)	commit \| commitdiff \| tree
2020-10-21	Andrew Reynolds	(proof-new) Fixes for proofs in rewriter (#5307)	commit \| commitdiff \| tree
2020-10-20	Andrew Reynolds	(proof-new) Fix for CDProof::isSame (#5297)	commit \| commitdiff \| tree
2020-10-20	Andrew Reynolds	(proof-new) Update add lazy step interface in LazyCDProof...	commit \| commitdiff \| tree
2020-10-20	Andrew Reynolds	Fix miscellaneous warnings (#5256)	commit \| commitdiff \| tree
2020-10-20	Andrew Reynolds	Make seq.nth a trigger kind (#5314)	commit \| commitdiff \| tree
2020-10-20	Andrew Reynolds	Split CheckModels utility to its own file (#5303)	commit \| commitdiff \| tree
2020-10-19	Andrew Reynolds	(proof-new) Updates to assertions pipeline and preprocess...	commit \| commitdiff \| tree
2020-10-19	Andrew Reynolds	(proof-new) Update preprocessing pass context for proofs...	commit \| commitdiff \| tree
2020-10-19	Andrew Reynolds	Safer version of pending lemma processing in inference...	commit \| commitdiff \| tree
2020-10-19	Andrew Reynolds	(proof-new) Refactoring cyclic checks (#5291)	commit \| commitdiff \| tree
2020-10-18	Andrew Reynolds	(proof-new) Witness axiom reconstruction for purification...	commit \| commitdiff \| tree
2020-10-18	Andrew Reynolds	(proof-new) Implementation of trust substitution (...	commit \| commitdiff \| tree
2020-10-18	Andrew Reynolds	(proof-new) More features for SMT proof post-processor...	commit \| commitdiff \| tree
2020-10-18	Andrew Reynolds	(proof-new) Improvements for theory engine (#5292)	commit \| commitdiff \| tree
2020-10-16	Andrew Reynolds	Refactor SMT-level model object (#5277)	commit \| commitdiff \| tree
2020-10-16	Andrew Reynolds	Catch more cases of nested recursion in datatypes ...	commit \| commitdiff \| tree
2020-10-16	Andrew Reynolds	Add inference enumeration to datatypes (#5275)	commit \| commitdiff \| tree
2020-10-14	Andrew Reynolds	Guard uses of printing approximations for constants...	commit \| commitdiff \| tree
2020-10-14	Andrew Reynolds	(proof-new) Generalize preprocess proof generator ...	commit \| commitdiff \| tree
2020-10-14	Andrew Reynolds	(proof-new) Simplifications for proof rule checker...	commit \| commitdiff \| tree
2020-10-14	Andrew Reynolds	(proof-new) Miscellaneous minor improvements and fixes...	commit \| commitdiff \| tree
2020-10-13	Andrew Reynolds	(proof-new) New rules for Booleans (#5243)	commit \| commitdiff \| tree
2020-10-13	Andrew Reynolds	(proof-new) Change merge policy for proof node updater...	commit \| commitdiff \| tree
2020-10-12	Andrew Reynolds	Remove uf-ss-totality option (#5251)	commit \| commitdiff \| tree
2020-10-12	Andrew Reynolds	Eliminate uses of Expr in SmtEngine interface (#5240)	commit \| commitdiff \| tree
2020-10-12	Andrew Reynolds	Ensure uninterpreted sort owner is UF if uf-ho or finite...	commit \| commitdiff \| tree
2020-10-09	Andrew Reynolds	Simplify approach for collapsed selectors over non...	commit \| commitdiff \| tree
2020-10-09	Andrew Reynolds	(proof-new) Add lazy proof set utility (#5221)	commit \| commitdiff \| tree
2020-10-09	Andrew Reynolds	(proof-new) Theory engine proof producing (#5195)	commit \| commitdiff \| tree
2020-10-08	Andrew Reynolds	(proof-new) Fixes and improvements for smt proof postprocess...	commit \| commitdiff \| tree
2020-10-07	Andrew Reynolds	(proof-new) Add the strings proof constructor (#4903)	commit \| commitdiff \| tree
2020-10-07	Andrew Reynolds	Process pending inferences at the beginning of datatypes...	commit \| commitdiff \| tree
2020-10-06	Andrew Reynolds	(proof-new) Add interface for trusted substitution...	commit \| commitdiff \| tree
2020-10-06	Andrew Reynolds	(proof-new) Allow null proofs from generators in LazyCDProof...	commit \| commitdiff \| tree
2020-10-06	Andrew Reynolds	Add arithmetic preprocess module (#5188)	commit \| commitdiff \| tree
2020-10-05	Andrew Reynolds	Make sygus more robust to unknown responses in solution...	commit \| commitdiff \| tree
2020-10-03	Andrew Reynolds	Fix theory white unit test (#5194)	commit \| commitdiff \| tree
2020-10-03	Andrew Reynolds	Standardization of Theory (#5181)	commit \| commitdiff \| tree
2020-10-02	Andrew Reynolds	Minor simplifications to substitution map class (#5180)	commit \| commitdiff \| tree
2020-10-02	Andrew Reynolds	(proof-new) Fixes for theory preprocessing proofs ...	commit \| commitdiff \| tree
2020-10-02	Andrew Reynolds	(proof-new) Make shared solver proof producing (#5169)	commit \| commitdiff \| tree
2020-10-02	Andrew Reynolds	Decouple modules from TheoryArithPrivate (#5184)	commit \| commitdiff \| tree
2020-10-01	Andrew Reynolds	(proof-new) Make arrays proof producing (#5112)	commit \| commitdiff \| tree
2020-10-01	Andrew Reynolds	Update theory of arithmetic to standard check (#5178)	commit \| commitdiff \| tree
2020-10-01	Andrew Reynolds	(proof-new) Preprocessing passes use proper interfaces...	commit \| commitdiff \| tree
2020-10-01	Andrew Reynolds	Make SygusSolver use sygus attributes directly (#5172)	commit \| commitdiff \| tree
2020-09-30	Andrew Reynolds	Dynamic allocation of equality engine for shared solver...	commit \| commitdiff \| tree
2020-09-30	Andrew Reynolds	(proof-new) Add the term conversion sequence generator...	commit \| commitdiff \| tree
2020-09-29	Andrew Reynolds	(proof-new) Fixes for preprocess proof generator and...	commit \| commitdiff \| tree
2020-09-29	Andrew Reynolds	Reset assertions on resetAssertions (#5153)	commit \| commitdiff \| tree
2020-09-29	Andrew Reynolds	Disable regression that is timing out (#5142)	commit \| commitdiff \| tree
2020-09-28	Andrew Reynolds	Minor fixes to quantifiers proofs (#5151)	commit \| commitdiff \| tree
2020-09-27	Andrew Reynolds	Fix sygus quantifier elimination preprocess for multiple...	commit \| commitdiff \| tree
2020-09-26	Andrew Reynolds	Connect the shared solver to theory engine (#5103)	commit \| commitdiff \| tree
2020-09-26	Andrew Reynolds	Use original quantified formula for single invocation...	commit \| commitdiff \| tree
2020-09-25	Andrew Reynolds	Make sygus refinement step more robust to unevaluatable...	commit \| commitdiff \| tree
2020-09-24	Andrew Reynolds	Function definition fmf preprocessing pass (#5064)	commit \| commitdiff \| tree
2020-09-24	Andrew Reynolds	Modify lemma vs fact policy for datatype equalities...	commit \| commitdiff \| tree
2020-09-23	Andrew Reynolds	Disable cegqi-bv when using sygus (#5124)	commit \| commitdiff \| tree
2020-09-23	Andrew Reynolds	Allow E-matching by default when strings are enabled...	commit \| commitdiff \| tree
2020-09-23	Andrew Reynolds	Fix type issue with term formula removal (#5107)	commit \| commitdiff \| tree
2020-09-21	Andrew Reynolds	(proof-new) Add the arrays proof checker (#5047)	commit \| commitdiff \| tree
2020-09-20	Andrew Reynolds	More flexible design for model manager distributed...	commit \| commitdiff \| tree
2020-09-19	Andrew Reynolds	Standardize equality engine notifications in sets ...	commit \| commitdiff \| tree
2020-09-18	Andrew Reynolds	Fix assertion list for globally defined recursive functions...	commit \| commitdiff \| tree
2020-09-18	Andrew Reynolds	Add the shared solver (#4982)	commit \| commitdiff \| tree
2020-09-18	Andrew Reynolds	Logic exception for arrays indexed by arrays (#5073)	commit \| commitdiff \| tree
2020-09-18	Andrew Reynolds	(proof-new) Updates to proof node updater algorithm...	commit \| commitdiff \| tree
2020-09-18	Andrew Reynolds	(proof-new) Rewrites involving operators in term conversion...	commit \| commitdiff \| tree
2020-09-17	Andrew Reynolds	(proof-new) Fixes for theory engine proof generator...	commit \| commitdiff \| tree
2020-09-17	Andrew Reynolds	Reduce recursion in term formula removal (#5052)	commit \| commitdiff \| tree
2020-09-17	Andrew Reynolds	Further standardization of datatypes (#5076)	commit \| commitdiff \| tree
2020-09-16	Andrew Reynolds	Add buffered inference manager to TheorySep (#5038)	commit \| commitdiff \| tree
2020-09-16	Andrew Reynolds	Refactor collectModelInfo in TheoryArith (#5027)	commit \| commitdiff \| tree
2020-09-16	Andrew Reynolds	(proof-new) Make proofs mandatory in proof equality...	commit \| commitdiff \| tree
2020-09-15	Andrew Reynolds	Move sets member propagation to SolverState (#5045)	commit \| commitdiff \| tree
2020-09-15	Andrew Reynolds	Move quantifiers engine private to own file (#5053)	commit \| commitdiff \| tree
2020-09-15	Andrew Reynolds	Fix needsModel method for CEGQI (#5048)	commit \| commitdiff \| tree
2020-09-15	Andrew Reynolds	Standard equality engine notify class for Theory (...	commit \| commitdiff \| tree
2020-09-14	Andrew Reynolds	Refactoring the rewriter of sets (#4856)	commit \| commitdiff \| tree
2020-09-14	Andrew Reynolds	Standardize uses of inference manager in datatypes...	commit \| commitdiff \| tree
next

RSS Atom