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

2021-09-03	Andrew Reynolds	Make quantifier module classes derive from EnvObj ...	commit \| commitdiff \| tree
2021-09-03	Andrew Reynolds	Eliminate backwards ref to SmtEngine from abduction...	commit \| commitdiff \| tree
2021-09-02	Andrew Reynolds	Add LFSC node converter (#6944)	commit \| commitdiff \| tree
2021-09-02	Andrew Reynolds	Remove more instances of ufHo (#7087)	commit \| commitdiff \| tree
2021-09-02	Andrew Reynolds	Implement lazy proof checking modes (#7106)	commit \| commitdiff \| tree
2021-09-01	Andrew Reynolds	Print response to get-model using the API (#7084)	commit \| commitdiff \| tree
2021-09-01	Andrew Reynolds	Fix issues with cyclic proofs due to double SYMM application...	commit \| commitdiff \| tree
2021-09-01	Andrew Reynolds	Lazy proof reconstruction for strings theory solver...	commit \| commitdiff \| tree
2021-08-31	Andrew Reynolds	Fix normal forms context-dependent simplification for...	commit \| commitdiff \| tree
2021-08-31	Andrew Reynolds	Make regular expression sort not closed enumerable...	commit \| commitdiff \| tree
2021-08-30	Andrew Reynolds	Further refactoring of set defaults for incompatibility...	commit \| commitdiff \| tree
2021-08-30	Andrew Reynolds	Fix proof equality engine for "no-explain" premises...	commit \| commitdiff \| tree
2021-08-30	Andrew Reynolds	Fix quantifiers dynamic split module for parametric...	commit \| commitdiff \| tree
2021-08-27	Andrew Reynolds	Expand definitions in sygus operators at the SMT level...	commit \| commitdiff \| tree
2021-08-27	Andrew Reynolds	Add n-ary match trie utility (#6909)	commit \| commitdiff \| tree
2021-08-27	Andrew Reynolds	Add missing methods to Solver API for models (#7052)	commit \| commitdiff \| tree
2021-08-26	Andrew Reynolds	Eliminate currentSmtEngine for subsolver calls (#7068)	commit \| commitdiff \| tree
2021-08-26	Andrew Reynolds	Dump models for isNotEntailed results (#7071)	commit \| commitdiff \| tree
2021-08-26	Andrew Reynolds	Make datatype selector expansion to its own accessible...	commit \| commitdiff \| tree
2021-08-25	Andrew Reynolds	Eliminate calls to currentSmtEngine (#7060)	commit \| commitdiff \| tree
2021-08-24	Andrew Reynolds	Split higher-order term database (#7045)	commit \| commitdiff \| tree
2021-08-24	Andrew Reynolds	Refactor enumerator management in synth conjecture...	commit \| commitdiff \| tree
2021-08-24	Andrew Reynolds	Top-level structure for set defaults (#7047)	commit \| commitdiff \| tree
2021-08-24	Andrew Reynolds	Uniform treatment of trusted theory inferences in proofs...	commit \| commitdiff \| tree
2021-08-24	Andrew Reynolds	Miscellaneous changes from proof-new (#7042)	commit \| commitdiff \| tree
2021-08-23	Andrew Reynolds	Fix non-deterministism in quantified datatypes expansion...	commit \| commitdiff \| tree
2021-08-23	Andrew Reynolds	Purify substitutions in strings proof reconstruction...	commit \| commitdiff \| tree
2021-08-23	Andrew Reynolds	Generalize inequality elimination in quantifiers rewriter...	commit \| commitdiff \| tree
2021-08-23	Andrew Reynolds	Fix single invocation partition for higher-order (...	commit \| commitdiff \| tree
2021-08-22	Andrew Reynolds	Simplify model printing modes (#7049)	commit \| commitdiff \| tree
2021-08-22	Andrew Reynolds	Prenex quantified formulas with user annotations by...	commit \| commitdiff \| tree
2021-08-20	Andrew Reynolds	Simplify how user-provided quantifier attributes are...	commit \| commitdiff \| tree
2021-08-20	Andrew Reynolds	More refactoring of set defaults (#7043)	commit \| commitdiff \| tree
2021-08-20	Andrew Reynolds	Support sygus standard command syntax set-feature ...	commit \| commitdiff \| tree
2021-08-20	Andrew Reynolds	Eliminate eager model building (#7038)	commit \| commitdiff \| tree
2021-08-19	Andrew Reynolds	Catch cases where recursive functions reference functions...	commit \| commitdiff \| tree
2021-08-19	Andrew Reynolds	Split proof final callback to its own file (#6984)	commit \| commitdiff \| tree
2021-08-19	Andrew Reynolds	Refactor proof output for TPTP (#7029)	commit \| commitdiff \| tree
2021-08-18	Andrew Reynolds	Make TheoryProxy use Env, simplify initialization of...	commit \| commitdiff \| tree
2021-08-17	Andrew Reynolds	Make SmtEngineState use Env (#7028)	commit \| commitdiff \| tree
2021-08-17	Andrew Reynolds	Refactoring theory-specific variable elimination in...	commit \| commitdiff \| tree
2021-08-17	Andrew Reynolds	Fix policy for eliminating quantified formulas (#7017)	commit \| commitdiff \| tree
2021-08-17	Andrew Reynolds	Make theory BV use central eq engine when option is...	commit \| commitdiff \| tree
2021-08-17	Andrew Reynolds	Cosmetic improvements to theory datatypes (#7020)	commit \| commitdiff \| tree
2021-08-17	Andrew Reynolds	Improve conversion to skolems in expression miner ...	commit \| commitdiff \| tree
2021-08-17	Andrew Reynolds	Initial refactoring of set defaults (#7021)	commit \| commitdiff \| tree
2021-08-05	Andrew Reynolds	Generalize term canonizer for type classes (#6895)	commit \| commitdiff \| tree
2021-08-05	Andrew Reynolds	Fix policy for rewriting string equalities (#6916)	commit \| commitdiff \| tree
2021-08-04	Andrew Reynolds	Proper printing of proofs in the internal calculus...	commit \| commitdiff \| tree
2021-08-04	Andrew Reynolds	Fix policy for merging subproofs (#6981)	commit \| commitdiff \| tree
2021-08-04	Andrew Reynolds	Add inference ids for remainder of sygus solver (#6977)	commit \| commitdiff \| tree
2021-08-04	Andrew Reynolds	Add optional debug information for dumping instantiations...	commit \| commitdiff \| tree
2021-08-04	Andrew Reynolds	Add containsAssumption proof utility (#6953)	commit \| commitdiff \| tree
2021-08-04	Andrew Reynolds	Add missing inference identifiers (#6962)	commit \| commitdiff \| tree
2021-08-04	Andrew Reynolds	Remove dependencies on smt engine in smt solver (#6965)	commit \| commitdiff \| tree
2021-08-03	Andrew Reynolds	Refactor shared solver to use theory builtin inference...	commit \| commitdiff \| tree
2021-08-03	Andrew Reynolds	Remove "inUnsatCore" flag throughout (#6964)	commit \| commitdiff \| tree
2021-07-30	Andrew Reynolds	Simplify smt2 printer (#6954)	commit \| commitdiff \| tree
2021-07-29	Andrew Reynolds	Integrate central equality engine approach into theory...	commit \| commitdiff \| tree
2021-07-29	Andrew Reynolds	Minor updates to shared terms database for central...	commit \| commitdiff \| tree
2021-07-28	Andrew Reynolds	Minor changes to arrays in preparation for central...	commit \| commitdiff \| tree
2021-07-28	Andrew Reynolds	Make extended rewriter methods const (#6948)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Track instantiation reasons in proofs (#6935)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Add basic LFSC utilities (#6879)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Move enum value generator to own file (#6941)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Minor fix for term database + central equality engine...	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Revert change to regression (#6940)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Make all dependencies in the fast enumerator optional...	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Add print expression utility (#6880)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Minor changes from proof-new (#6937)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Miscellaneous fixes from proof-new (#6914)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Add proof letify utility (#6881)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Fix eq proof conversion for constant merged parameterized...	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Default equality proofs for bags and separation logic...	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Add sygus enumerator callback (#6923)	commit \| commitdiff \| tree
2021-07-26	Andrew Reynolds	Enable default equality proofs for sets (#6931)	commit \| commitdiff \| tree
2021-07-26	Andrew Reynolds	More updates to arithmetic in preparation for central...	commit \| commitdiff \| tree
2021-07-25	Andrew Reynolds	Changes to datatypes in preparation for central equality...	commit \| commitdiff \| tree
2021-07-25	Andrew Reynolds	Refactor equality engine setup for arithmetic congruence...	commit \| commitdiff \| tree
2021-07-22	Andrew Reynolds	Simplify computation of relevant terms in datatypes...	commit \| commitdiff \| tree
2021-07-22	Andrew Reynolds	Add the central equality engine manager (#6893)	commit \| commitdiff \| tree
2021-07-22	Andrew Reynolds	Miscellaneous changes in preparation for central equality...	commit \| commitdiff \| tree
2021-07-22	Andrew Reynolds	Preparation for carry the rewrite rule database in...	commit \| commitdiff \| tree
2021-07-18	Andrew Reynolds	Add n-ary term utilities (#6896)	commit \| commitdiff \| tree
2021-07-16	Andrew Reynolds	Do not exhaustive instantiation when FMF is disabled...	commit \| commitdiff \| tree
2021-07-15	Andrew Reynolds	Fix context for proofs of instantiations (#6890)	commit \| commitdiff \| tree
2021-07-15	Andrew Reynolds	Distinguish quantifiers preprocess as its own proof...	commit \| commitdiff \| tree
2021-07-15	Andrew Reynolds	Connect the equality solver to theory arith (#6894)	commit \| commitdiff \| tree
2021-07-15	Andrew Reynolds	Arithmetic equality solver (#6876)	commit \| commitdiff \| tree
2021-07-15	Andrew Reynolds	Move master equality engine notification to own file...	commit \| commitdiff \| tree
2021-07-15	Andrew Reynolds	Add node converter utility (#6878)	commit \| commitdiff \| tree
2021-07-14	Andrew Reynolds	Fix for context on input proof generator (#6873)	commit \| commitdiff \| tree
2021-07-14	Andrew Reynolds	Move synthesis verification check to own file (#6882)	commit \| commitdiff \| tree
2021-07-14	Andrew Reynolds	Refactor setup of proof equality engine for central...	commit \| commitdiff \| tree
2021-07-14	Andrew Reynolds	Fix models for sequences of infinite element type ...	commit \| commitdiff \| tree
2021-07-13	Andrew Reynolds	Add branch and bound lemma if linear arithmetic generates...	commit \| commitdiff \| tree
2021-07-12	Andrew Reynolds	Add branch and bound (#6865)	commit \| commitdiff \| tree
2021-07-12	Andrew Reynolds	Fix for learned rewrite pass, add regression (#6850)	commit \| commitdiff \| tree
2021-07-12	Andrew Reynolds	Add arithmetic preprocess rewrite equality module ...	commit \| commitdiff \| tree
2021-07-12	Andrew Reynolds	Add trace for combination splits (#6862)	commit \| commitdiff \| tree
next

RSS Atom