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

2022-04-08	Andrew Reynolds	Eliminate more uses of CONST_RATIONAL (#8590)	commit \| commitdiff \| tree
2022-04-08	Andrew Reynolds	Properly parse numerals as real when integers are disabled...	commit \| commitdiff \| tree
2022-04-07	Andrew Reynolds	Generalization for sygus verify utility (#8586)	commit \| commitdiff \| tree
2022-04-07	Andrew Reynolds	Internal representation of oracle interface quantifiers...	commit \| commitdiff \| tree
2022-04-07	Andrew Reynolds	Add method to get leaves of a NodeTrie (#8583)	commit \| commitdiff \| tree
2022-04-07	Andrew Reynolds	Make sets and bags operators left-associative (#8584)	commit \| commitdiff \| tree
2022-04-07	Andrew Reynolds	Eliminate SmtSolver dependency on SolverEngineState...	commit \| commitdiff \| tree
2022-04-07	Andrew Reynolds	Minor fix for printing nullary operators in smt2 (...	commit \| commitdiff \| tree
2022-04-07	Andrew Reynolds	Fix proof checker for SUBS (#8578)	commit \| commitdiff \| tree
2022-04-06	Andrew Reynolds	Fixes for LFSC printing and signatures (#8579)	commit \| commitdiff \| tree
2022-04-05	Andrew Reynolds	Make inst constant attribute robust to purification...	commit \| commitdiff \| tree
2022-04-05	Andrew Reynolds	Be permissive for subtyping in function definitions...	commit \| commitdiff \| tree
2022-04-04	Andrew Reynolds	Rename getInstantiatedConstructorTerm to getInstantiatedTerm...	commit \| commitdiff \| tree
2022-04-04	Andrew Reynolds	Use raw symbols in proofs (#8550)	commit \| commitdiff \| tree
2022-04-04	Andrew Reynolds	Fix for get-value with empty uninterpreted sort domain...	commit \| commitdiff \| tree
2022-04-02	Andrew Reynolds	Rename mkSygusGrammar to mkGrammar (#8544)	commit \| commitdiff \| tree
2022-04-02	Andrew Reynolds	Remove variant of mkDatatypeDecl with one sort parameter...	commit \| commitdiff \| tree
2022-04-02	Andrew Reynolds	Ignore irrelevant exponential terms (#8534)	commit \| commitdiff \| tree
2022-04-02	Andrew Reynolds	Require that used model values are constant in CEGQI...	commit \| commitdiff \| tree
2022-04-02	Andrew Reynolds	Add a few miscellaneous pieces of documentation (#8533)	commit \| commitdiff \| tree
2022-04-02	Andrew Reynolds	Add more explanations in the API (#8493)	commit \| commitdiff \| tree
2022-04-01	Andrew Reynolds	Simplifications to the datatypes API (#8511)	commit \| commitdiff \| tree
2022-04-01	Andrew Reynolds	Internal simplifications to constructing datatypes...	commit \| commitdiff \| tree
2022-04-01	Andrew Reynolds	Fix sygus-inst when combined with bounded string quantifiers...	commit \| commitdiff \| tree
2022-03-31	Andrew Reynolds	Handled quoted symbols in indexed operators (#8491)	commit \| commitdiff \| tree
2022-03-31	Andrew Reynolds	Disable minisat variable elimination when a parametric...	commit \| commitdiff \| tree
2022-03-31	Andrew Reynolds	Do not export dt.size (#8483)	commit \| commitdiff \| tree
2022-03-31	Andrew Reynolds	Fix check for whether PI is reduced (#8485)	commit \| commitdiff \| tree
2022-03-31	Andrew Reynolds	Fix lower vs upper bound issue for eager RE conflicts...	commit \| commitdiff \| tree
2022-03-31	Andrew Reynolds	Fix non-termination in the strings rewriter (#8438)	commit \| commitdiff \| tree
2022-03-31	Andrew Reynolds	Fix case of Boolean skolem for ground term E-matching...	commit \| commitdiff \| tree
2022-03-30	Andrew Reynolds	Fix policy for purifying arguments of exp (#8416)	commit \| commitdiff \| tree
2022-03-30	Andrew Reynolds	Fixes for sygus-inst (#8448)	commit \| commitdiff \| tree
2022-03-30	Andrew Reynolds	Fix subtype issue in cegqi arithmetic (#8440)	commit \| commitdiff \| tree
2022-03-30	Andrew Reynolds	Change tuple tokens and update datatypes theory ref...	commit \| commitdiff \| tree
2022-03-30	Andrew Reynolds	Add LFSC to internal proof checker (#8442)	commit \| commitdiff \| tree
2022-03-29	Andrew Reynolds	Make ensureTermSort private (#8436)	commit \| commitdiff \| tree
2022-03-29	Andrew Reynolds	Add information for cardinality constraint to the API...	commit \| commitdiff \| tree
2022-03-29	Andrew Reynolds	Make ProofNodeManager mkScope more robust (#8435)	commit \| commitdiff \| tree
2022-03-29	Andrew Reynolds	Fix issue related to use of Boolean term variable for...	commit \| commitdiff \| tree
2022-03-28	Andrew Reynolds	Mark more methods as experimental (#8426)	commit \| commitdiff \| tree
2022-03-28	Andrew Reynolds	Fix synth result python unit test (#8418)	commit \| commitdiff \| tree
2022-03-26	Andrew Reynolds	Fix spurious assertion failure (#8404)	commit \| commitdiff \| tree
2022-03-26	Andrew Reynolds	Throw logic exception for set.map (#8403)	commit \| commitdiff \| tree
2022-03-26	Andrew Reynolds	More minor cleaning of options (#8401)	commit \| commitdiff \| tree
2022-03-26	Andrew Reynolds	Fixes for API kind documentation (#8397)	commit \| commitdiff \| tree
2022-03-25	Andrew Reynolds	Update checkSynth and checkSynthNext to return SynthResult...	commit \| commitdiff \| tree
2022-03-25	Andrew Reynolds	Change output of abduction/interpolation for failed...	commit \| commitdiff \| tree
2022-03-25	Andrew Reynolds	Fixes related to set defaults for sygus/proofs (#8395)	commit \| commitdiff \| tree
2022-03-25	Andrew Reynolds	Properly guard commands in the SyGuS API (#8390)	commit \| commitdiff \| tree
2022-03-25	Andrew Reynolds	Recategorize options (#8386)	commit \| commitdiff \| tree
2022-03-25	Andrew Reynolds	Fixes for theory reference for datatypes (#8380)	commit \| commitdiff \| tree
2022-03-24	Andrew Reynolds	Minor updates for quantifiers options (#8385)	commit \| commitdiff \| tree
2022-03-24	Andrew Reynolds	Standardize more instances of skolems (#8351)	commit \| commitdiff \| tree
2022-03-24	Andrew Reynolds	Fix a couple of parse error messages for sygus (#8381)	commit \| commitdiff \| tree
2022-03-23	Andrew Reynolds	Clean options (#8309)	commit \| commitdiff \| tree
2022-03-23	Andrew Reynolds	Add SynthResult to the API (#8370)	commit \| commitdiff \| tree
2022-03-23	Andrew Reynolds	Make IDOF_MAX rewrite only apply when all children...	commit \| commitdiff \| tree
2022-03-23	Andrew Reynolds	Add internal synth result class (#8352)	commit \| commitdiff \| tree
2022-03-23	Andrew Reynolds	Initial documentation on LFSC (#8365)	commit \| commitdiff \| tree
2022-03-23	Andrew Reynolds	Fix non-termination issue in sygus enumerator (#8340)	commit \| commitdiff \| tree
2022-03-22	Andrew Reynolds	Change null terminator for regular expression intersection...	commit \| commitdiff \| tree
2022-03-22	Andrew Reynolds	Updates for the theory reference for separation logic...	commit \| commitdiff \| tree
2022-03-22	Andrew Reynolds	Fixes for witness terms appearing in CEGQI instantiations...	commit \| commitdiff \| tree
2022-03-22	Andrew Reynolds	Refactor result class (#8313)	commit \| commitdiff \| tree
2022-03-21	Andrew Reynolds	Fix return value for candidate rewrite database (#8354)	commit \| commitdiff \| tree
2022-03-21	Andrew Reynolds	Fix LFSC conversion for seq unit (#8353)	commit \| commitdiff \| tree
2022-03-21	Andrew Reynolds	Fix learned literals for top-level AND (#8336)	commit \| commitdiff \| tree
2022-03-17	Andrew Reynolds	Update care graph computations to use standard node...	commit \| commitdiff \| tree
2022-03-16	Andrew Reynolds	Fix getModelValue for arithmetic (#8316)	commit \| commitdiff \| tree
2022-03-16	Andrew Reynolds	Ensure trusted steps are given for skolem lemmas when...	commit \| commitdiff \| tree
2022-03-15	Andrew Reynolds	Make learned literal computation more robust (#8308)	commit \| commitdiff \| tree
2022-03-15	Andrew Reynolds	Add unit test involving seq concat term (#8257)	commit \| commitdiff \| tree
2022-03-15	Andrew Reynolds	Fix issues involving multiple sources of model substitutions...	commit \| commitdiff \| tree
2022-03-15	Andrew Reynolds	Properly guard sort instantiate (#8247)	commit \| commitdiff \| tree
2022-03-15	Andrew Reynolds	Remove unecessary separation logic options (#8269)	commit \| commitdiff \| tree
2022-03-15	Andrew Reynolds	Fix to consider leafs of theory sets to be variables...	commit \| commitdiff \| tree
2022-03-15	Andrew Reynolds	Simplify reductions for set and bag choose (#8304)	commit \| commitdiff \| tree
2022-03-14	Andrew Reynolds	Fixes for skolem definition management (#8301)	commit \| commitdiff \| tree
2022-03-14	Andrew Reynolds	Remove unecessary methods from the API (#8260)	commit \| commitdiff \| tree
2022-03-14	Andrew Reynolds	Add rewrite for allchar beneath union + star (#8299)	commit \| commitdiff \| tree
2022-03-14	Andrew Reynolds	Run preprocess rewrite on equalities until fixed point...	commit \| commitdiff \| tree
2022-03-13	Andrew Reynolds	Minor sync from proof-new (#8293)	commit \| commitdiff \| tree
2022-03-12	Andrew Reynolds	Introduce new splitting inference in sets + cardinality...	commit \| commitdiff \| tree
2022-03-12	Andrew Reynolds	Add algorithm for finding pairs of paths in a node...	commit \| commitdiff \| tree
2022-03-12	Andrew Reynolds	Improvements for sygus query generation (#8224)	commit \| commitdiff \| tree
2022-03-12	Andrew Reynolds	Document type rules (#8248)	commit \| commitdiff \| tree
2022-03-12	Andrew Reynolds	Always ensure literal when requiring phase via inference...	commit \| commitdiff \| tree
2022-03-11	Andrew Reynolds	Remove old decision justification heurstic (#8275)	commit \| commitdiff \| tree
2022-03-11	Andrew Reynolds	Update abduction and interpolation API to not use pass...	commit \| commitdiff \| tree
2022-03-11	Andrew Reynolds	Fix maximum value for pedantic proof level (#8246)	commit \| commitdiff \| tree
2022-03-11	Andrew Reynolds	Guard parametric datatypes instantiated by non-first...	commit \| commitdiff \| tree
2022-03-11	Andrew Reynolds	Remove unecessary CEGQI options (#8281)	commit \| commitdiff \| tree
2022-03-11	Andrew Reynolds	Consider APPLY_CONSTRUCTOR applied to values to be...	commit \| commitdiff \| tree
2022-03-11	Andrew Reynolds	Fix reduction for arc trig functions (#8289)	commit \| commitdiff \| tree
2022-03-10	Andrew Reynolds	Fix issue with subtyping from set membership in models...	commit \| commitdiff \| tree
2022-03-10	Andrew Reynolds	Fix theoryOf call in get equality status (#8279)	commit \| commitdiff \| tree
2022-03-10	Andrew Reynolds	Eliminate unecessary datatype options (#8280)	commit \| commitdiff \| tree
2022-03-10	Andrew Reynolds	Add output -o pre-asserts (#8270)	commit \| commitdiff \| tree
2022-03-10	Andrew Reynolds	Disable timing out regressions (#8273)	commit \| commitdiff \| tree
next

RSS Atom