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

2020-08-03	Andrew Reynolds	Generalize interface for candidate rewrite database...	commit \| commitdiff \| tree
2020-08-03	Andrew Reynolds	Update datatypes in cvc parser to the new API (#4826)	commit \| commitdiff \| tree
2020-08-03	Andrew Reynolds	Split expression names from SmtEngine (#4832)	commit \| commitdiff \| tree
2020-08-03	Andrew Reynolds	Split dump manager from SmtEngine (#4824)	commit \| commitdiff \| tree
2020-08-02	Andrew Reynolds	Updates to dtype constructor in preparation for eliminating...	commit \| commitdiff \| tree
2020-08-02	Andrew Reynolds	Add methods for constructing datatype types from NodeManager...	commit \| commitdiff \| tree
2020-08-01	Andrew Reynolds	Fix component contains for splicing due to substring...	commit \| commitdiff \| tree
2020-07-31	Andrew Reynolds	Split listener classes from SmtEngine (#4816)	commit \| commitdiff \| tree
2020-07-31	Andrew Reynolds	Standardize explanations in arrays (#4804)	commit \| commitdiff \| tree
2020-07-30	Andrew Reynolds	Fix null case for sygus printing (#4793)	commit \| commitdiff \| tree
2020-07-30	Andrew Reynolds	(proof-new) Stream output for ProofNode (#4789)	commit \| commitdiff \| tree
2020-07-30	Andrew Reynolds	(proof-new) Fixes for getFreeAssumptions (#4802)	commit \| commitdiff \| tree
2020-07-28	Andrew Reynolds	Remove arrays lazy rintro option (#4806)	commit \| commitdiff \| tree
2020-07-28	Andrew Reynolds	Fix regular expression delta for complement (#4765)	commit \| commitdiff \| tree
2020-07-28	Andrew Reynolds	Use lemma property enum for OutputChannel::lemma (...	commit \| commitdiff \| tree
2020-07-27	Andrew Reynolds	(proof-new) Proof production for term formula removal...	commit \| commitdiff \| tree
2020-07-27	Andrew Reynolds	(proof-new) Arithmetic operator elim proof producing...	commit \| commitdiff \| tree
2020-07-21	Andrew Reynolds	Support uninterpreted constants in the evaluator (...	commit \| commitdiff \| tree
2020-07-18	Andrew Reynolds	(proof-new) Proof recording for assertions pipeline...	commit \| commitdiff \| tree
2020-07-18	Andrew Reynolds	Enumerate shapes feature in fast sygus enumerator ...	commit \| commitdiff \| tree
2020-07-17	Andrew Reynolds	Replace options listener infrastructure (#4764)	commit \| commitdiff \| tree
2020-07-17	Andrew Reynolds	(proof-new) Updates to strings core solver (#4642)	commit \| commitdiff \| tree
2020-07-17	Andrew Reynolds	Add option manager and simpler option listener (#4745)	commit \| commitdiff \| tree
2020-07-16	Andrew Reynolds	Split abstract values utility from SmtEngine (#4754)	commit \| commitdiff \| tree
2020-07-16	Andrew Reynolds	Make ExtTheory a utility and not a member of Theory...	commit \| commitdiff \| tree
2020-07-15	Andrew Reynolds	Split abduction solver from SmtEngine (#4733)	commit \| commitdiff \| tree
2020-07-15	Andrew Reynolds	Simplify entailment check interface (#4744)	commit \| commitdiff \| tree
2020-07-14	Andrew Reynolds	Make use of options in setDefaults more consistent...	commit \| commitdiff \| tree
2020-07-14	Andrew Reynolds	Remove sygus print callback (#4727)	commit \| commitdiff \| tree
2020-07-14	Andrew Reynolds	Fix regression output. (#4741)	commit \| commitdiff \| tree
2020-07-14	Andrew Reynolds	(proof-new) Skeleton proof support in the Rewriter...	commit \| commitdiff \| tree
2020-07-14	Andrew Reynolds	Debug instantiations output (#4739)	commit \| commitdiff \| tree
2020-07-14	Andrew Reynolds	Minor refactoring of subsolver initialization (#4731)	commit \| commitdiff \| tree
2020-07-14	Andrew Reynolds	Fix type comparisons involving pointer. (#4738)	commit \| commitdiff \| tree
2020-07-14	Andrew Reynolds	Fix whitespace issue in instantiations output. (#4737)	commit \| commitdiff \| tree
2020-07-13	Andrew Reynolds	(proof-new) SMT Preprocess proof generator (#4708)	commit \| commitdiff \| tree
2020-07-13	Andrew Reynolds	User-facing print debug option for sygus candidates...	commit \| commitdiff \| tree
2020-07-13	Andrew Reynolds	Statistics on instantiations per quantified formula...	commit \| commitdiff \| tree
2020-07-13	Andrew Reynolds	Add support for string/sequence update (#4725)	commit \| commitdiff \| tree
2020-07-11	Andrew Reynolds	Cache explanations in TheoryEngine::getExplanation...	commit \| commitdiff \| tree
2020-07-11	Andrew Reynolds	(proof-new) Add ONCE and FIXPOINT modes for term conversion...	commit \| commitdiff \| tree
2020-07-11	Andrew Reynolds	(proof-new) Update Theory interface for proof-new ...	commit \| commitdiff \| tree
2020-07-10	Andrew Reynolds	Front end support for integer AND (#4717)	commit \| commitdiff \| tree
2020-07-10	Andrew Reynolds	Update competition scripts (#4715)	commit \| commitdiff \| tree
2020-07-10	Andrew Reynolds	Ensure legal elimination for witness rewrite (#4688)	commit \| commitdiff \| tree
2020-07-09	Andrew Reynolds	Disable unsat cores in timeout regression (#4713)	commit \| commitdiff \| tree
2020-07-09	Andrew Reynolds	Associate all lemmas in non-linear arithmetic with...	commit \| commitdiff \| tree
2020-07-09	Andrew Reynolds	(proof-new) Theory engine proof generator (#4657)	commit \| commitdiff \| tree
2020-07-08	Andrew Reynolds	Always interleave theory combination with quantifiers...	commit \| commitdiff \| tree
2020-07-08	Andrew Reynolds	Improve and fix secant and tangent lemmas in the transcenden...	commit \| commitdiff \| tree
2020-07-07	Andrew Reynolds	Transfer ownership of internal Options from NodeManager...	commit \| commitdiff \| tree
2020-07-06	Andrew Reynolds	Front end support for sequences (#4690)	commit \| commitdiff \| tree
2020-07-02	Andrew Reynolds	Fix regression option (#4680)	commit \| commitdiff \| tree
2020-07-02	Andrew Reynolds	(proof-new) Updates to skolem manager interface (...	commit \| commitdiff \| tree
2020-07-02	Andrew Reynolds	(proof-new) Proof rule checkers run on skolem forms...	commit \| commitdiff \| tree
2020-07-02	Andrew Reynolds	(proof-new) Proof node updater (#4647)	commit \| commitdiff \| tree
2020-07-01	Andrew Reynolds	Add solver for integer AND (#4681)	commit \| commitdiff \| tree
2020-07-01	Andrew Reynolds	Inferences and model construction taking into account...	commit \| commitdiff \| tree
2020-07-01	Andrew Reynolds	(proof-new) Updates to evaluator (#4659)	commit \| commitdiff \| tree
2020-07-01	Andrew Reynolds	(proof-new) Improve rewriter for WITNESS (#4661)	commit \| commitdiff \| tree
2020-06-30	Andrew Reynolds	Fix normal form for re.comp (#4676)	commit \| commitdiff \| tree
2020-06-30	Andrew Reynolds	Simplify quantifiers strategy for when to apply last...	commit \| commitdiff \| tree
2020-06-30	Andrew Reynolds	Add internal support for integer and operator (#4668)	commit \| commitdiff \| tree
2020-06-28	Andrew Reynolds	Fix non-termination issues in simpleRegExpConsume ...	commit \| commitdiff \| tree
2020-06-25	Andrew Reynolds	(proof-new) Add TrustNode interfaces to OutputChannel...	commit \| commitdiff \| tree
2020-06-25	Andrew Reynolds	Remove sygus1 parser (#4651)	commit \| commitdiff \| tree
2020-06-25	Andrew Reynolds	Update option --nl-ext to enable/disable incremental...	commit \| commitdiff \| tree
2020-06-23	Andrew Reynolds	(proof-new) Updates to proof node manager (#4617)	commit \| commitdiff \| tree
2020-06-22	Andrew Reynolds	(proof-new) Add REWRITE trust node kind. (#4624)	commit \| commitdiff \| tree
2020-06-22	Andrew Reynolds	(proof-new) Add proof-new to options file (#4641)	commit \| commitdiff \| tree
2020-06-22	Andrew Reynolds	Add trascendental function kinds to list of unevaluated...	commit \| commitdiff \| tree
2020-06-20	Andrew Reynolds	(proof-new) Make static methods in re-elim (#4623)	commit \| commitdiff \| tree
2020-06-19	Andrew Reynolds	(proof-new) CDProof inherits from ProofGenerator (...	commit \| commitdiff \| tree
2020-06-19	Andrew Reynolds	Add casc j10 scripts (#4621)	commit \| commitdiff \| tree
2020-06-19	Andrew Reynolds	(proof-new) Updates to strings term registry (#4599)	commit \| commitdiff \| tree
2020-06-19	Andrew Reynolds	Convert more uses of strings to words (#4584)	commit \| commitdiff \| tree
2020-06-19	Andrew Reynolds	(proof-new) Split operator elimination from arithmetic...	commit \| commitdiff \| tree
2020-06-19	Andrew Reynolds	Clean the header file of TheoryStrings (#4272)	commit \| commitdiff \| tree
2020-06-17	Andrew Reynolds	Do not traverse WITNESS for partial substitutions in...	commit \| commitdiff \| tree
2020-06-16	Andrew Reynolds	Updates to NEWS. (#4628)	commit \| commitdiff \| tree
2020-06-16	Andrew Reynolds	(proof-new) Add quantifiers proof checker (#4593)	commit \| commitdiff \| tree
2020-06-15	Andrew Reynolds	(proof-new) Update proof node, add proof node algorithm...	commit \| commitdiff \| tree
2020-06-15	Andrew Reynolds	Do RE derivation inference only for concrete constant...	commit \| commitdiff \| tree
2020-06-13	Andrew Reynolds	Move sygus datatype utility functions to their own...	commit \| commitdiff \| tree
2020-06-12	Andrew Reynolds	Update to consistent policy for removed terms in quantifier...	commit \| commitdiff \| tree
2020-06-12	Andrew Reynolds	(proof-new) Term conversion proof generator utility...	commit \| commitdiff \| tree
2020-06-12	Andrew Reynolds	(proof-new) Minor updates to strings base solver (...	commit \| commitdiff \| tree
2020-06-12	Andrew Reynolds	Cardinality-related inferences per type in theory of...	commit \| commitdiff \| tree
2020-06-12	Andrew Reynolds	(proof-new) Split TheoryEngine (#4558)	commit \| commitdiff \| tree
2020-06-12	Andrew Reynolds	Add rewrite for str.replace_re. (#4601)	commit \| commitdiff \| tree
2020-06-11	Andrew Reynolds	(proof-new) Add lazy proof utility (#4589)	commit \| commitdiff \| tree
2020-06-11	Andrew Reynolds	(proof-new) Add eager proof generator utility. (#4592)	commit \| commitdiff \| tree
2020-06-11	Andrew Reynolds	(proof-new) Remove arith-snorm option. (#4591)	commit \| commitdiff \| tree
2020-06-10	Andrew Reynolds	(proof-new) Theory proof step buffer utility (#4580)	commit \| commitdiff \| tree
2020-06-09	Andrew Reynolds	(proof-new) Refactor skolemization (#4586)	commit \| commitdiff \| tree
2020-06-09	Andrew Reynolds	(proof-new) Add trust node utility (#4588)	commit \| commitdiff \| tree
2020-06-08	Andrew Reynolds	(proof-new) Add abstract proof generator class (#4574)	commit \| commitdiff \| tree
2020-06-06	Andrew Reynolds	Use NlLemma utility for all lemmas in non-linear. ...	commit \| commitdiff \| tree
2020-06-06	Andrew Reynolds	Smt2 parsing support for nested recursive datatypes...	commit \| commitdiff \| tree
2020-06-05	Andrew Reynolds	Datatypes with nested recursion are not handled in...	commit \| commitdiff \| tree
next

RSS Atom