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

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
2020-09-12	Andrew Reynolds	(proof-new) Add SMT proof manager (#5054)	commit \| commitdiff \| tree
2020-09-12	Andrew Reynolds	(proof-new) Update TheoryEngine lemma and conflict...	commit \| commitdiff \| tree
2020-09-11	Andrew Reynolds	Move finite model minimization to UF last call effort...	commit \| commitdiff \| tree
2020-09-11	Andrew Reynolds	(proof-new) Handle mismatched assumptions in proof...	commit \| commitdiff \| tree
2020-09-11	Andrew Reynolds	(proof-new) Use deep copy for final lemma step in proof...	commit \| commitdiff \| tree
2020-09-11	Andrew Reynolds	Add witness to cvc printer. (#5057)	commit \| commitdiff \| tree
2020-09-10	Andrew Reynolds	Parser error for wrong number of datatypes (#5049)	commit \| commitdiff \| tree
2020-09-10	Andrew Reynolds	Use state and inference manager in UF CardinalityExtension...	commit \| commitdiff \| tree
2020-09-09	Andrew Reynolds	(proof-new) Minor changes to proof node updater (#5011)	commit \| commitdiff \| tree
2020-09-09	Andrew Reynolds	(proof-new) Make proofs in term formula removal term...	commit \| commitdiff \| tree
2020-09-09	Andrew Reynolds	(proof-new) Generalize single step helper in eager...	commit \| commitdiff \| tree
2020-09-09	Andrew Reynolds	Fixes for regular expressions + sygus (#5044)	commit \| commitdiff \| tree
2020-09-09	Andrew Reynolds	Split term registry from theory state in sets (#5037)	commit \| commitdiff \| tree
2020-09-08	Andrew Reynolds	Eliminate a custom use of TheorySep in quantifiers...	commit \| commitdiff \| tree
2020-09-04	Andrew Reynolds	Add asLemma flag to theory inference process (#5030)	commit \| commitdiff \| tree
2020-09-04	Andrew Reynolds	(new theory) Update TheoryBV to new standard for collectMode...	commit \| commitdiff \| tree
2020-09-04	Andrew Reynolds	Add interfaces for making trust nodes in TheoryInferenceMana...	commit \| commitdiff \| tree
2020-09-03	Andrew Reynolds	Update sets inference manager to inherit from InferenceManag...	commit \| commitdiff \| tree
2020-09-03	Andrew Reynolds	Minor cleanup of quantifiers engine (#4994)	commit \| commitdiff \| tree
2020-09-03	Andrew Reynolds	Make ExtTheory independent of Theory (#5010)	commit \| commitdiff \| tree
2020-09-03	Andrew Reynolds	(proof-new) Support proofs of quantifier instantiation...	commit \| commitdiff \| tree
2020-09-03	Andrew Reynolds	(proof-new) Improve debugging infrastructure for open...	commit \| commitdiff \| tree
2020-09-02	Andrew Reynolds	(proof-new) Updates to builtin proof checker (#4962)	commit \| commitdiff \| tree
2020-09-02	Andrew Reynolds	(proof-new) Add proof support in TheoryUF (#5002)	commit \| commitdiff \| tree
2020-09-02	Andrew Reynolds	(proof-new) Make term conversion proof generator optionally...	commit \| commitdiff \| tree
2020-09-02	Andrew Reynolds	Minor updates to theory inference manager (#5004)	commit \| commitdiff \| tree
2020-09-02	Andrew Reynolds	(new theory) Update TheoryArrays to the new standard...	commit \| commitdiff \| tree
2020-09-02	Andrew Reynolds	(new theory) Update TheorySets to the new interface...	commit \| commitdiff \| tree
2020-09-01	Andrew Reynolds	(new theory) Update TheoryDatatypes to the new standard...	commit \| commitdiff \| tree
2020-09-01	Andrew Reynolds	Add TheoryInference base class (#4990)	commit \| commitdiff \| tree
2020-09-01	Andrew Reynolds	Add the inference manager for datatypes (#4968)	commit \| commitdiff \| tree
2020-08-31	Andrew Reynolds	(new theory) Update TheoryStrings to new standard ...	commit \| commitdiff \| tree
2020-08-31	Andrew Reynolds	Simplify interface for computing relevant terms. (...	commit \| commitdiff \| tree
2020-08-31	Andrew Reynolds	Basic proof support in inference manager (#4975)	commit \| commitdiff \| tree
2020-08-29	Andrew Reynolds	(proof-new) More term context utilities. (#4912)	commit \| commitdiff \| tree
2020-08-28	Andrew Reynolds	Replace Theory::Set with TheoryIdSet (#4959)	commit \| commitdiff \| tree
2020-08-28	Andrew Reynolds	(proof-new) Make CombinationEngine proof producing...	commit \| commitdiff \| tree
2020-08-28	Andrew Reynolds	(new theory) Update TheoryQuantifiers to the new interface...	commit \| commitdiff \| tree
2020-08-28	Andrew Reynolds	(proof-new) Add the SMT proof post processor (#4913)	commit \| commitdiff \| tree
2020-08-28	Andrew Reynolds	(new theory) Update TheoryFP to the new interface ...	commit \| commitdiff \| tree
2020-08-28	Andrew Reynolds	Do not delay processing equivalence class merges in...	commit \| commitdiff \| tree
next

RSS Atom