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

2020-08-28	Andrew Reynolds	(new theory) Update TheoryFP to the new interface ...	commit \| commitdiff \| tree
2020-08-28	Gereon Kremer	(cad-solver) Fixed excluding lemma generation. (#4958)	commit \| commitdiff \| tree
2020-08-28	Andrew Reynolds	Do not delay processing equivalence class merges in...	commit \| commitdiff \| tree
2020-08-28	Andrew Reynolds	Add the buffered inference manager (#4954)	commit \| commitdiff \| tree
2020-08-28	Andrew Reynolds	(new theory) Update TheorySep to new interface (#4947)	commit \| commitdiff \| tree
2020-08-28	Gereon Kremer	Make iand lemmas use proper Inference types. (#4956)	commit \| commitdiff \| tree
2020-08-27	Andrew Reynolds	(proof-new) Add the proof equality engine (#4881)	commit \| commitdiff \| tree
2020-08-27	Andrew Reynolds	Add irrelevant kinds infrastructure to TheoryModel...	commit \| commitdiff \| tree
2020-08-27	Andrew Reynolds	Add the theory inference manager (#4948)	commit \| commitdiff \| tree
2020-08-27	Andrew Reynolds	(new theory) Update TheoryUF to new interface (#4944)	commit \| commitdiff \| tree
2020-08-26	Andrew Reynolds	Connect combination engine to theory engine (#4940)	commit \| commitdiff \| tree
2020-08-26	Andrew Reynolds	Replace Expr-level datatype with Node-level DType ...	commit \| commitdiff \| tree
2020-08-25	Haniel Barbosa	Eliminating spurious replay of commands for define...	commit \| commitdiff \| tree
2020-08-25	Andrew Reynolds	Add the combination engine (#4939)	commit \| commitdiff \| tree
2020-08-24	Andrew Reynolds	Add a few basic extensions for equality engine (#4937)	commit \| commitdiff \| tree
2020-08-24	Gereon Kremer	Fix memory issue in AntlrInput::parseError (#4873)	commit \| commitdiff \| tree
2020-08-24	Andrew Reynolds	Do not use relevance during non-linear check model...	commit \| commitdiff \| tree
2020-08-24	Mathias Preiner	Increase regress level to 2 for production build. ...	commit \| commitdiff \| tree
2020-08-24	Andrew Reynolds	Add the distributed model manager (#4934)	commit \| commitdiff \| tree
2020-08-24	Andrew Reynolds	Extend the standard Theory template based on equality...	commit \| commitdiff \| tree
2020-08-22	Andrew Reynolds	Remove unecessary theory model builder base class ...	commit \| commitdiff \| tree
2020-08-21	Andrew Reynolds	Dynamic allocation of model equality engine (#4911)	commit \| commitdiff \| tree
2020-08-21	Andrew Reynolds	Limit trigger terms to shared terms in arrays (#4932)	commit \| commitdiff \| tree
2020-08-21	Andrew Reynolds	Remove spurious theory methods calls (#4931)	commit \| commitdiff \| tree
2020-08-21	Andrew Reynolds	Connect the relevance manager to TheoryEngine and use...	commit \| commitdiff \| tree
2020-08-21	Andrew Reynolds	Simplify and fix care graph for ufHo (#4924)	commit \| commitdiff \| tree
2020-08-21	Andrew Reynolds	Remove BV equality slicer (#4928)	commit \| commitdiff \| tree
2020-08-20	Andrew Reynolds	Add TheoryState objects to each Theory (#4920)	commit \| commitdiff \| tree
2020-08-20	Andrew Reynolds	Split QuantElimSolver from SmtEngine (#4919)	commit \| commitdiff \| tree
2020-08-20	Andrew Reynolds	Simplify trigger notifications in equality engine ...	commit \| commitdiff \| tree
2020-08-20	Andrew Reynolds	Remove example theory (#4922)	commit \| commitdiff \| tree
2020-08-20	Andrew Reynolds	Add strings-exp to regression (#4923)	commit \| commitdiff \| tree
2020-08-19	Gereon Kremer	(cad solver) Add a partial check method. (#4904)	commit \| commitdiff \| tree
2020-08-19	Andrew Reynolds	Make sets and strings solver states inherit from TheoryState...	commit \| commitdiff \| tree
2020-08-19	Andres Noetzli	Require `--strings-exp` when using `str.substr` (#4916)	commit \| commitdiff \| tree
2020-08-19	Gereon Kremer	Changes assertion (about maximum set cardinality) to...	commit \| commitdiff \| tree
2020-08-19	Andres Noetzli	[Regressions] Do not test `--check-proofs` anymore...	commit \| commitdiff \| tree
2020-08-19	Gereon Kremer	Fix SmtEngine::reset() (#4917)	commit \| commitdiff \| tree
2020-08-18	Abdalrhman Mohamed	Refactor functions that print commands (Part 2) (#4905)	commit \| commitdiff \| tree
2020-08-18	Andrew Reynolds	(proof-new) Theory preprocessor proof producing (#4807)	commit \| commitdiff \| tree
2020-08-18	Andrew Reynolds	Introduce the theory state object (#4910)	commit \| commitdiff \| tree
2020-08-18	Andrew Reynolds	Standardize collectModelInfo and theory-specific collectRele...	commit \| commitdiff \| tree
2020-08-18	Andrew Reynolds	(proof-new) Minor updates to trust node (#4900)	commit \| commitdiff \| tree
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	Alex Ozdemir	Add identifier name for side condition. (#4902)	commit \| commitdiff \| tree
2020-08-17	Andres Noetzli	[CI] Update package list (#4906)	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-16	Gereon Kremer	(cad solver) Use the current model as initial assignment...	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-14	E Polgreen	correctly parse sygus lang option (#4884)	commit \| commitdiff \| tree
2020-08-14	Gereon Kremer	Inspect roots to avoid certain resultants (Algorithm...	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-13	Haniel Barbosa	[proof-new] Adding support for corner case of transitivity...	commit \| commitdiff \| tree
2020-08-12	Haniel Barbosa	generalize handling MERGED_THROUGH_CONSTANST in EqProof...	commit \| commitdiff \| tree
2020-08-12	Abdalrhman Mohamed	Refactor functions that print commands (Part 1) (#4869)	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	makaimann	Add option to only build library (#4801)	commit \| commitdiff \| tree
2020-08-12	Andrew Reynolds	(proof-new) Witness form proof generator (#4782)	commit \| commitdiff \| tree
2020-08-12	Gereon Kremer	Add naive support for integer variables. (#4835)	commit \| commitdiff \| tree
2020-08-12	Haniel Barbosa	(proof-new) Improving proof-production in Equality...	commit \| commitdiff \| tree
2020-08-12	Andrew Reynolds	Fix connection to master equality engine in sets (...	commit \| commitdiff \| tree
2020-08-12	Gereon Kremer	Fix infinite loop in arith_ite_simp (#4805)	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-11	Aina Niemetz	New C++ API: Remove redundant API functions for mkReal...	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-07	Aina Niemetz	GH Actions: Remove cancel action. (#4843)	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-05	Gereon Kremer	Improve error message for unsupported exponents (#4852)	commit \| commitdiff \| tree
2020-08-05	Andrew V. Jones	When checking models, ensure that error message is...	commit \| commitdiff \| tree
2020-08-05	Andres Noetzli	[Strings] Add eager context-dependent evaluation (...	commit \| commitdiff \| tree
2020-08-05	Gereon Kremer	Add dummy returns if libpoly is unavailable. (#4845)	commit \| commitdiff \| tree
2020-08-04	Andrew Reynolds	Fixes for getInterpolant and getAbduct API methods...	commit \| commitdiff \| tree
2020-08-04	Mathias Preiner	Add documentation and build instructions for recompilation...	commit \| commitdiff \| tree
2020-08-04	Abdalrhman Mohamed	Modify the smt2 parser to use the Sygus grammar. (...	commit \| commitdiff \| tree
next

RSS Atom