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

2021-10-13	Andrew Reynolds	Eliminate uses of rewrite from datatypes theory (#7354)	commit \| commitdiff \| tree
2021-10-13	Andrew Reynolds	Make (proof) equality engine use Env (#7336)	commit \| commitdiff \| tree
2021-10-12	Andrew Reynolds	Simplify refinement in sygus solver (#7343)	commit \| commitdiff \| tree
2021-10-12	Andrew Reynolds	Eliminate calls to currentResourceManager (#7350)	commit \| commitdiff \| tree
2021-10-12	Andrew Reynolds	Provide a non-traversal interface to term formula removal...	commit \| commitdiff \| tree
2021-10-12	Andrew Reynolds	Minor cleaning of instantiation utilities (#7334)	commit \| commitdiff \| tree
2021-10-12	Andrew Reynolds	Simplify skolemization in sygus solver (#7331)	commit \| commitdiff \| tree
2021-10-11	Andrew Reynolds	Connect the LFSC printer (#7323)	commit \| commitdiff \| tree
2021-10-11	Andrew Reynolds	Add cardinality constraint utilities (#7286)	commit \| commitdiff \| tree
2021-10-08	Andrew Reynolds	Make skolem definition manager robust to function skolems...	commit \| commitdiff \| tree
2021-10-08	Andrew Reynolds	Add argument to distinguish lemmas and input assertions...	commit \| commitdiff \| tree
2021-10-08	Andrew Reynolds	A few more miscellaneous uses of EnvObj (#7325)	commit \| commitdiff \| tree
2021-10-07	Andrew Reynolds	Move preprocessor to smt solver (#7321)	commit \| commitdiff \| tree
2021-10-07	Andrew Reynolds	Finish the LFSC printer (#7285)	commit \| commitdiff \| tree
2021-10-07	Andrew Reynolds	Use skolem lemma in prop layer interfaces (#7320)	commit \| commitdiff \| tree
2021-10-07	Andrew Reynolds	Make the cardinality of the alphabet of strings configurable...	commit \| commitdiff \| tree
2021-10-07	Andrew Reynolds	Miscellaneous fixes from proof-new (#7313)	commit \| commitdiff \| tree
2021-10-07	Andrew Reynolds	Fast exit for string extended equality rewriter (#7312)	commit \| commitdiff \| tree
2021-10-07	Andrew Reynolds	Eliminate more circular dependencies on solver engine...	commit \| commitdiff \| tree
2021-10-06	Andrew Reynolds	Refactor skolem definitions notifications for the decision...	commit \| commitdiff \| tree
2021-10-06	Andrew Reynolds	Eliminate more hard coded uses of user context (#7309)	commit \| commitdiff \| tree
2021-10-04	Andrew Reynolds	Refactor internally generated bounded quantified formulas...	commit \| commitdiff \| tree
2021-10-04	Andrew Reynolds	Move isFiniteType from theory engine to Env (#7287)	commit \| commitdiff \| tree
2021-10-04	Andrew Reynolds	Make decision engine use env (#7300)	commit \| commitdiff \| tree
2021-10-04	Andrew Reynolds	Eliminating static calls to rewriter in quantifiers...	commit \| commitdiff \| tree
2021-10-04	Andrew Reynolds	Eliminating static calls to rewriter from strings ...	commit \| commitdiff \| tree
2021-10-01	Andrew Reynolds	Update theory preprocessor to use Env (#7288)	commit \| commitdiff \| tree
2021-10-01	Andrew Reynolds	Fix ascription check for return types on ordinary functions...	commit \| commitdiff \| tree
2021-10-01	Andrew Reynolds	Make preregistration safe for uninterpreted constants...	commit \| commitdiff \| tree
2021-10-01	Andrew Reynolds	Add the LFSC printer (#7158)	commit \| commitdiff \| tree
2021-10-01	Andrew Reynolds	Add the print benchmark utility (#7196)	commit \| commitdiff \| tree
2021-10-01	Andrew Reynolds	Use the proper evaluator for optimized SyGuS datatype...	commit \| commitdiff \| tree
2021-09-30	Andrew Reynolds	Make theory engine modules use Env (#7277)	commit \| commitdiff \| tree
2021-09-30	Andrew Reynolds	Simplify the syntax and representation of the separation...	commit \| commitdiff \| tree
2021-09-29	Andrew Reynolds	Properly restrict PBE symmetry breaking for abduction...	commit \| commitdiff \| tree
2021-09-29	Andrew Reynolds	Update the syntax for tuples in smt2 (#7265)	commit \| commitdiff \| tree
2021-09-29	Andrew Reynolds	Add the strings array solver (#7232)	commit \| commitdiff \| tree
2021-09-24	Andrew Reynolds	Eliminate calls to Rewriter::rewrite from strings entailment...	commit \| commitdiff \| tree
2021-09-23	Andrew Reynolds	Generalize string enumerator for fixed length sequences...	commit \| commitdiff \| tree
2021-09-23	Andrew Reynolds	More uses of EnvObj (#7230)	commit \| commitdiff \| tree
2021-09-23	Andrew Reynolds	Implement alpha equivalence proofs (#7066)	commit \| commitdiff \| tree
2021-09-22	Andrew Reynolds	Make cegqi subsolvers EnvObj (#7205)	commit \| commitdiff \| tree
2021-09-22	Andrew Reynolds	Towards standard usage of evaluator (#7189)	commit \| commitdiff \| tree
2021-09-22	Andrew Reynolds	Add extensionality option for strings disequalities...	commit \| commitdiff \| tree
2021-09-22	Andrew Reynolds	Minimal fixing version for tuple update parsing (#7228)	commit \| commitdiff \| tree
2021-09-20	Andrew Reynolds	Add the LFSC proof post-processor (#7134)	commit \| commitdiff \| tree
2021-09-18	Andrew Reynolds	Fix printer for datatype udpater (#7208)	commit \| commitdiff \| tree
2021-09-16	Andrew Reynolds	Fix relevant domain for parametric operators (#7198)	commit \| commitdiff \| tree
2021-09-15	Andrew Reynolds	Minor changes to E-matching utilities (#7062)	commit \| commitdiff \| tree
2021-09-15	Andrew Reynolds	Eliminate global access to options:: from quantifiers...	commit \| commitdiff \| tree
2021-09-14	Andrew Reynolds	Add get-difficulty to the API (#7194)	commit \| commitdiff \| tree
2021-09-14	Andrew Reynolds	Support sygus version 2.1 command assume (#7081)	commit \| commitdiff \| tree
2021-09-14	Andrew Reynolds	Utilities in preparation for print benchmark utility...	commit \| commitdiff \| tree
2021-09-14	Andrew Reynolds	Add proof manager method to translate difficulty map...	commit \| commitdiff \| tree
2021-09-14	Andrew Reynolds	Reimplement `--dump=raw-benchmark` as `-o raw-benchmark...	commit \| commitdiff \| tree
2021-09-13	Andrew Reynolds	Connect difficulty manager to TheoryEngine (#7161)	commit \| commitdiff \| tree
2021-09-11	Andrew Reynolds	Add casc 28 scripts (#7070)	commit \| commitdiff \| tree
2021-09-10	Andrew Reynolds	More refactoring of set defaults (#7160)	commit \| commitdiff \| tree
2021-09-09	Andrew Reynolds	Add difficulty manager (#7151)	commit \| commitdiff \| tree
2021-09-09	Andrew Reynolds	Add difficulty post-processor (#7150)	commit \| commitdiff \| tree
2021-09-09	Andrew Reynolds	Disable shared selectors for quantified logics without...	commit \| commitdiff \| tree
2021-09-09	Andrew Reynolds	Remove deprecated SyGuS method evaluateWithUnfolding...	commit \| commitdiff \| tree
2021-09-08	Andrew Reynolds	Add Lfsc print channel utilities (#7123)	commit \| commitdiff \| tree
2021-09-08	Andrew Reynolds	Improve pre-skolemization, move quantifiers preprocess...	commit \| commitdiff \| tree
2021-09-08	Andrew Reynolds	Towards standard usage of ExtendedRewriter (#7145)	commit \| commitdiff \| tree
2021-09-08	Andrew Reynolds	Add option for using bound inference for relevant assertions...	commit \| commitdiff \| tree
2021-09-08	Andrew Reynolds	Add LFSC side condition conversion utility for list...	commit \| commitdiff \| tree
2021-09-08	Andrew Reynolds	Use rewriteViaMethod instead of accessing builtin proof...	commit \| commitdiff \| tree
2021-09-07	Andrew Reynolds	Refactoring of proof manager initialization (#7073)	commit \| commitdiff \| tree
2021-09-07	Andrew Reynolds	Refactoring and fixes of set defaults for quantifiers...	commit \| commitdiff \| tree
2021-09-03	Andrew Reynolds	Standardize Rewriter::rewriteViaMethod call (#7119)	commit \| commitdiff \| tree
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
next

RSS Atom