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

2020-10-14	yoni206	bv2int: implementing the iand-sum mode (#5265)	commit \| commitdiff \| tree
2020-10-14	Alex Ozdemir	(proof-new) debug statements & docs for INT_TRUST ...	commit \| commitdiff \| tree
2020-10-14	Alex Ozdemir	(proof-new) pfs in TheoryArith(Private) explainations...	commit \| commitdiff \| tree
2020-10-14	Andrew Reynolds	Guard uses of printing approximations for constants...	commit \| commitdiff \| tree
2020-10-14	Alex Ozdemir	(proof-new) pfs for conflicts in TheoryArithPrivate...	commit \| commitdiff \| tree
2020-10-14	yoni206	bv2int: rewritings and unsat cores (#5263)	commit \| commitdiff \| tree
2020-10-14	Haniel Barbosa	using NOT_NOT_ELIM rather than macros to do double...	commit \| commitdiff \| tree
2020-10-14	Alex Ozdemir	(proof-new) Prove lemmas in Constraint (#5254)	commit \| commitdiff \| tree
2020-10-14	Andrew Reynolds	(proof-new) Generalize preprocess proof generator ...	commit \| commitdiff \| tree
2020-10-14	Andrew Reynolds	(proof-new) Simplifications for proof rule checker...	commit \| commitdiff \| tree
2020-10-14	Andrew Reynolds	(proof-new) Miscellaneous minor improvements and fixes...	commit \| commitdiff \| tree
2020-10-13	Andrew Reynolds	(proof-new) New rules for Booleans (#5243)	commit \| commitdiff \| tree
2020-10-13	Andrew Reynolds	(proof-new) Change merge policy for proof node updater...	commit \| commitdiff \| tree
2020-10-13	yoni206	bv2int: improving bvand tables (#5235)	commit \| commitdiff \| tree
2020-10-12	Andrew Reynolds	Remove uf-ss-totality option (#5251)	commit \| commitdiff \| tree
2020-10-12	Andrew Reynolds	Eliminate uses of Expr in SmtEngine interface (#5240)	commit \| commitdiff \| tree
2020-10-12	Andrew Reynolds	Ensure uninterpreted sort owner is UF if uf-ho or finite...	commit \| commitdiff \| tree
2020-10-11	Mathias Preiner	SyGuS instantiation modes (#5228)	commit \| commitdiff \| tree
2020-10-11	Gereon Kremer	Add conversion of poly polynomial to cvc node. (#5218)	commit \| commitdiff \| tree
2020-10-10	Abdalrhman Mohamed	Provide API version of some SMT Commands. (#5222)	commit \| commitdiff \| tree
2020-10-10	yoni206	bv2int: bvand translation code move (#5227)	commit \| commitdiff \| tree
2020-10-09	Mathias Preiner	Remove deprecated add-path commands and use $GITHUB_PATH... ...deprecated add-path commands and use $GITHUB_PATH instead. (#5232)	commit \| commitdiff \| tree
2020-10-09	Alex Ozdemir	use right arith explanation fn to fix regressions ...	commit \| commitdiff \| tree
2020-10-09	Alex Ozdemir	(proof-new) proofs for arith-constraint explanations...	commit \| commitdiff \| tree
2020-10-09	Andres Noetzli	reset-assertions: Remove all non-global symbols in...	commit \| commitdiff \| tree
2020-10-09	Andrew Reynolds	Simplify approach for collapsed selectors over non...	commit \| commitdiff \| tree
2020-10-09	Andrew Reynolds	(proof-new) Add lazy proof set utility (#5221)	commit \| commitdiff \| tree
2020-10-09	Andrew Reynolds	(proof-new) Theory engine proof producing (#5195)	commit \| commitdiff \| tree
2020-10-08	Andrew Reynolds	(proof-new) Fixes and improvements for smt proof postprocess...	commit \| commitdiff \| tree
2020-10-08	makaimann	Get correct NodeManagerScope for toStrings in API ...	commit \| commitdiff \| tree
2020-10-08	yoni206	fix unit failures on debug without symfpu (#5212)	commit \| commitdiff \| tree
2020-10-07	Alex Ozdemir	(proof-new) proofs in ee -> arith pipeline (#5215)	commit \| commitdiff \| tree
2020-10-07	Aina Niemetz	New C++ API: Rename Term::isConst() to Term::isValue...	commit \| commitdiff \| tree
2020-10-07	Gereon Kremer	Make sure conflicts are not rewritten (in arithmetic...	commit \| commitdiff \| tree
2020-10-07	Andrew Reynolds	(proof-new) Add the strings proof constructor (#4903)	commit \| commitdiff \| tree
2020-10-07	Malte Mues	Improve OSX support by adding os detection and adapting...	commit \| commitdiff \| tree
2020-10-07	Andrew Reynolds	Process pending inferences at the beginning of datatypes...	commit \| commitdiff \| tree
2020-10-06	yoni206	bv-to-int: change order of passes (#5208)	commit \| commitdiff \| tree
2020-10-06	Alex Ozdemir	(proof-new) proofs for ArithCongMan -> ee facts (#5207)	commit \| commitdiff \| tree
2020-10-06	Andrew Reynolds	(proof-new) Add interface for trusted substitution...	commit \| commitdiff \| tree
2020-10-06	Andrew Reynolds	(proof-new) Allow null proofs from generators in LazyCDProof...	commit \| commitdiff \| tree
2020-10-06	mudathirmahgoub	Add operators bag.from_set, bag.to_set to the theory...	commit \| commitdiff \| tree
2020-10-06	Andrew Reynolds	Add arithmetic preprocess module (#5188) ...strings preprocess module (https://github.com/CVC4/CVC4/blob/master/src...	commit \| commitdiff \| tree
2020-10-06	Abdalrhman Mohamed	Recover from some exceptions. (#5203)	commit \| commitdiff \| tree
2020-10-06	mudathirmahgoub	Remove subtyping for sets (#5205)	commit \| commitdiff \| tree
2020-10-05	Aina Niemetz	cmake: Add warning when unit testing is disabled due...	commit \| commitdiff \| tree
2020-10-05	Aina Niemetz	SyGuS: Add fp.sub to default FP grammar. (#5206)	commit \| commitdiff \| tree
2020-10-05	Aina Niemetz	Integer: GMP: Move implementation of member functions...	commit \| commitdiff \| tree
2020-10-05	Andrew Reynolds	Make sygus more robust to unknown responses in solution...	commit \| commitdiff \| tree
2020-10-04	mudathirmahgoub	Remove subtyping for sets theory (#5179)	commit \| commitdiff \| tree
2020-10-03	Aina Niemetz	sygus-inst: Add more special BV values. (#5191)	commit \| commitdiff \| tree
2020-10-03	Andrew Reynolds	Fix theory white unit test (#5194)	commit \| commitdiff \| tree
2020-10-03	Andrew Reynolds	Standardization of Theory (#5181)	commit \| commitdiff \| tree
2020-10-02	Andrew Reynolds	Minor simplifications to substitution map class (#5180)	commit \| commitdiff \| tree
2020-10-02	Andrew Reynolds	(proof-new) Fixes for theory preprocessing proofs ...	commit \| commitdiff \| tree
2020-10-02	Andrew Reynolds	(proof-new) Make shared solver proof producing (#5169)	commit \| commitdiff \| tree
2020-10-02	Gereon Kremer	Allow for theory combination of strings with nonlinear...	commit \| commitdiff \| tree
2020-10-02	Andrew Reynolds	Decouple modules from TheoryArithPrivate (#5184)	commit \| commitdiff \| tree
2020-10-02	Alex Ozdemir	(proof-new) New proofs in arith::Constraint::externalExplain...	commit \| commitdiff \| tree
2020-10-02	Alex Ozdemir	Remove duplicate declarations in th_bv.plf (#5183)	commit \| commitdiff \| tree
2020-10-02	Aina Niemetz	SyGuS: Add min/max (sub)normal constants to FP default...	commit \| commitdiff \| tree
2020-10-01	Andrew Reynolds	(proof-new) Make arrays proof producing (#5112)	commit \| commitdiff \| tree
2020-10-01	Mathias Preiner	Add additional ground terms to SyGuS instantiation...	commit \| commitdiff \| tree
2020-10-01	Andrew Reynolds	Update theory of arithmetic to standard check (#5178)	commit \| commitdiff \| tree
2020-10-01	Aina Niemetz	FloatingPoint: Add utility functions for largest and...	commit \| commitdiff \| tree
2020-10-01	Gereon Kremer	Allow to use the initial assignment for CAD (#5177)	commit \| commitdiff \| tree
2020-10-01	Andrew Reynolds	(proof-new) Preprocessing passes use proper interfaces...	commit \| commitdiff \| tree
2020-10-01	Andrew Reynolds	Make SygusSolver use sygus attributes directly (#5172)	commit \| commitdiff \| tree
2020-10-01	Mathias Preiner	Add GH action to cancel previous pending/running CI...	commit \| commitdiff \| tree
2020-10-01	Aina Niemetz	BitVector: Extend interface of setBit to set it to...	commit \| commitdiff \| tree
2020-09-30	Aina Niemetz	FloatingPoint: Add utility functions for largest and...	commit \| commitdiff \| tree
2020-09-30	Gereon Kremer	Remove too strict assertion to allow for approximate...	commit \| commitdiff \| tree
2020-09-30	Gereon Kremer	Add missing includes. (#5170)	commit \| commitdiff \| tree
2020-09-30	Gereon Kremer	Add strategy for nonlinear extension (#5160)	commit \| commitdiff \| tree
2020-09-30	Andrew Reynolds	Dynamic allocation of equality engine for shared solver...	commit \| commitdiff \| tree
2020-09-30	Andrew Reynolds	(proof-new) Add the term conversion sequence generator...	commit \| commitdiff \| tree
2020-09-29	Haniel Barbosa	[proof-new] Adds a proof manager for prop engine (...	commit \| commitdiff \| tree
2020-09-29	mudathirmahgoub	Fix bags headers (#5165)	commit \| commitdiff \| tree
2020-09-29	Alex Ozdemir	(proof-new) Add proof managers and eager gens to arith...	commit \| commitdiff \| tree
2020-09-29	Andrew Reynolds	(proof-new) Fixes for preprocess proof generator and...	commit \| commitdiff \| tree
2020-09-29	Haniel Barbosa	[proof-new] Adds a proof post processor for the Prop...	commit \| commitdiff \| tree
2020-09-29	Haniel Barbosa	[proof-new] Updates to proof node updater (#5156)	commit \| commitdiff \| tree
2020-09-29	Haniel Barbosa	[proof-new] Adds a proof-producing CNF converter (...	commit \| commitdiff \| tree
2020-09-29	Gereon Kremer	Clean up nonlinear extension (#5149)	commit \| commitdiff \| tree
2020-09-29	Andrew Reynolds	Reset assertions on resetAssertions (#5153)	commit \| commitdiff \| tree
2020-09-29	Alex Ozdemir	Add utilities for arith/proof_checker and build it...	commit \| commitdiff \| tree
2020-09-29	Haniel Barbosa	[proof-new] Removing spurious forward declaration in...	commit \| commitdiff \| tree
2020-09-29	Haniel Barbosa	[proof-new] Adds a proof node hash function (#5154)	commit \| commitdiff \| tree
2020-09-29	Andrew Reynolds	Disable regression that is timing out (#5142)	commit \| commitdiff \| tree
2020-09-28	Andrew Reynolds	Minor fixes to quantifiers proofs (#5151)	commit \| commitdiff \| tree
2020-09-28	Haniel Barbosa	[proof-new] Adds a proof manager for the SAT solver...	commit \| commitdiff \| tree
2020-09-28	mudathirmahgoub	Implement bags rewriter (#5132)	commit \| commitdiff \| tree
2020-09-28	Gereon Kremer	Add new arithmetic BoundInference class (#5148)	commit \| commitdiff \| tree
2020-09-27	Andrew Reynolds	Fix sygus quantifier elimination preprocess for multiple...	commit \| commitdiff \| tree
2020-09-26	Gereon Kremer	Use inference manager for nl_solver (#5125)	commit \| commitdiff \| tree
2020-09-26	Andrew Reynolds	Connect the shared solver to theory engine (#5103)	commit \| commitdiff \| tree
2020-09-26	Andrew Reynolds	Use original quantified formula for single invocation...	commit \| commitdiff \| tree
2020-09-26	Aina Niemetz	Restrict bvxnor to only allow two operands (was n-ary...	commit \| commitdiff \| tree
2020-09-25	Andrew Reynolds	Make sygus refinement step more robust to unevaluatable...	commit \| commitdiff \| tree
2020-09-25	Haniel Barbosa	Cleaning and documenting cnf stream (#5134)	commit \| commitdiff \| tree
next

RSS Atom