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

2020-08-18	Andrew Reynolds	(proof-new) SMT proof postprocess callback (#4883)	commit \| commitdiff \| tree
2020-08-18	Andrew Reynolds	Quantifiers engine stores a pointer to the master equality...	commit \| commitdiff \| tree
2020-08-18	Andrew Reynolds	Split SygusSolver from SmtEngine (#4891)	commit \| commitdiff \| tree
2020-08-18	Andrew Reynolds	Add the relevance manager module (#4894)	commit \| commitdiff \| tree
2020-08-18	Andrew Reynolds	(proof-new) Callbacks for term-context-sensitive terms...	commit \| commitdiff \| tree
2020-08-17	Andrew Reynolds	Dynamic allocation of equality engine in Theory (#4890)	commit \| commitdiff \| tree
2020-08-17	Andrew Reynolds	(proof-new) Prepare the theory of strings for proof...	commit \| commitdiff \| tree
2020-08-16	Andrew Reynolds	Add non-emptiness to conclusion of positive RE star...	commit \| commitdiff \| tree
2020-08-15	Andrew Reynolds	Minor cleanup related to notifications (#4898)	commit \| commitdiff \| tree
2020-08-15	Andrew Reynolds	Add finishInit method to PropEngine (#4895)	commit \| commitdiff \| tree
2020-08-15	Andrew Reynolds	(proof-new) Add the strings proof checker (#4858)	commit \| commitdiff \| tree
2020-08-14	Andrew Reynolds	Simplify equality engine notifications (#4896)	commit \| commitdiff \| tree
2020-08-13	Andrew Reynolds	Split SmtSolver from SmtEngine (#4880)	commit \| commitdiff \| tree
2020-08-13	Andrew Reynolds	Fixes for corner case of decision tree learning with...	commit \| commitdiff \| tree
2020-08-13	Andrew Reynolds	More basic fix for dumping synth-fun (#4886)	commit \| commitdiff \| tree
2020-08-13	Andrew Reynolds	Add the distributed equality engine manager (#4867)	commit \| commitdiff \| tree
2020-08-12	Andrew Reynolds	Fixes for degenerate case of sygus decision tree learning...	commit \| commitdiff \| tree
2020-08-12	Andrew Reynolds	(proof-new) Improve robustness of CONG rule (#4882)	commit \| commitdiff \| tree
2020-08-12	Andrew Reynolds	(proof-new) Proof support in the strings term registry...	commit \| commitdiff \| tree
2020-08-12	Andrew Reynolds	(proof-new) Improve interfaces to proof generators...	commit \| commitdiff \| tree
2020-08-12	Andrew Reynolds	(proof-new) Witness form proof generator (#4782)	commit \| commitdiff \| tree
2020-08-12	Andrew Reynolds	Fix connection to master equality engine in sets (...	commit \| commitdiff \| tree
2020-08-12	Andrew Reynolds	Fix unsupported option in regress1. (#4874)	commit \| commitdiff \| tree
2020-08-12	Andrew Reynolds	Split SmtEngineState from SmtEngine (#4855)	commit \| commitdiff \| tree
2020-08-12	Andrew Reynolds	Prepare theory of sets for dynamic allocation of equality...	commit \| commitdiff \| tree
2020-08-12	Andrew Reynolds	Final preparations for changing API to use the Node...	commit \| commitdiff \| tree
2020-08-12	Andrew Reynolds	(proof-new) Extensions to proof checker interface ...	commit \| commitdiff \| tree
2020-08-11	Andrew Reynolds	Update Expr-level unit tests that depend on datatypes...	commit \| commitdiff \| tree
2020-08-11	Andrew Reynolds	Remove instantiation model true option (#4861)	commit \| commitdiff \| tree
2020-08-09	Andrew Reynolds	Make valuation class more robust to null underlying...	commit \| commitdiff \| tree
2020-08-09	Andrew Reynolds	Splitting a few utility classes from EqualityEngine...	commit \| commitdiff \| tree
2020-08-08	Andrew Reynolds	Move datatype index constant to its own file (#4859)	commit \| commitdiff \| tree
2020-08-06	Andrew Reynolds	Updates not related to creation for eliminating Expr...	commit \| commitdiff \| tree
2020-08-06	Andrew Reynolds	Split preprocessor from SmtEngine (#4854)	commit \| commitdiff \| tree
2020-08-06	Andrew Reynolds	(proof-new) Refactor regular expression operation ...	commit \| commitdiff \| tree
2020-08-05	Andrew Reynolds	Split Assertions from SmtEngine (#4788)	commit \| commitdiff \| tree
2020-08-04	Andrew Reynolds	Fixes for getInterpolant and getAbduct API methods...	commit \| commitdiff \| tree
2020-08-04	Andrew Reynolds	Add API interface for specialized constructor term...	commit \| commitdiff \| tree
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
next

RSS Atom