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

2021-02-04	yoni206	Adding an option to optimize polite combination for...	commit \| commitdiff \| tree
2021-02-04	Andrew Reynolds	Introduce quantifiers registry utility (#5829)	commit \| commitdiff \| tree
2021-02-04	yoni206	Clarifying documentation of `--static-binary` (#5844)	commit \| commitdiff \| tree
2021-02-04	Andrew Reynolds	Eliminate equality query dependence on quantifiers...	commit \| commitdiff \| tree
2021-02-04	Haniel Barbosa	[proof-new] Catch trivial cycles in SAT proof generation...	commit \| commitdiff \| tree
2021-02-03	Mathias Preiner	Add BV solver bitblast. (#5851)	commit \| commitdiff \| tree
2021-02-03	Haniel Barbosa	[proof-new] Fix MACRO_RESOLUTION expansion for singleton...	commit \| commitdiff \| tree
2021-02-02	Andrew Reynolds	(proof-new) Miscellaneous fixes and regressions (#5841)	commit \| commitdiff \| tree
2021-02-02	Andrew Reynolds	(proof-new) Refactor theory preprocessing (#5835)	commit \| commitdiff \| tree
2021-02-02	Andrew Reynolds	Remove quantifiers regression from decision folder...	commit \| commitdiff \| tree
2021-02-02	Andrew Reynolds	Cleanup some includes (#5847)	commit \| commitdiff \| tree
2021-02-02	Andrew Reynolds	Improvements for NL traces (#5846)	commit \| commitdiff \| tree
2021-02-02	Haniel Barbosa	[proof-new] Fix bug in expansion of MACRO_RESOLUTION...	commit \| commitdiff \| tree
2021-02-01	Andrew Reynolds	Eliminate PREPROCESS lemma property (#5827)	commit \| commitdiff \| tree
2021-02-01	Andrew Reynolds	Simplify alpha equivalence module (#5839)	commit \| commitdiff \| tree
2021-02-01	Abdalrhman Mohamed	Avoid calling the printers while converting sexpr to...	commit \| commitdiff \| tree
2021-02-01	mudathirmahgoub	Fix BagsRewriter::rewriteUnionDisjoint (#5840)	commit \| commitdiff \| tree
2021-01-30	Andrew Reynolds	Fix unguarded call to get representative (#5838)	commit \| commitdiff \| tree
2021-01-29	Haniel Barbosa	[proof-new] Connecting new unsat cores (#5834)	commit \| commitdiff \| tree
2021-01-29	mudathirmahgoub	Add bag inferences for operators: intersection, duplicate_re...	commit \| commitdiff \| tree
2021-01-29	Andrew Reynolds	(proof-new) Distinguish pre vs post rewrites in term...	commit \| commitdiff \| tree
2021-01-28	Andrew Reynolds	Reorganize calls to quantifiers engine from SmtEngine...	commit \| commitdiff \| tree
2021-01-28	mudathirmahgoub	Remove regex header from cvc4cpp.cpp (#5826)	commit \| commitdiff \| tree
2021-01-28	Andrew Reynolds	Simplify lemma interface (#5819)	commit \| commitdiff \| tree
2021-01-28	Andrew Reynolds	Use standard equality engine information in quantifiers...	commit \| commitdiff \| tree
2021-01-28	Andrew Reynolds	Always theory-preprocess lemmas (#5817)	commit \| commitdiff \| tree
2021-01-27	Andrew Reynolds	Add option for whether to filter candidate rewrite...	commit \| commitdiff \| tree
2021-01-27	Andrew Reynolds	Split pattern term selector from trigger (#5811)	commit \| commitdiff \| tree
2021-01-27	Andrew Reynolds	(proof-new) Improvements to quantifiers engine and...	commit \| commitdiff \| tree
2021-01-27	Alex Ozdemir	Thread proofs through arith channels & similar (#5818)	commit \| commitdiff \| tree
2021-01-27	Andrew Reynolds	Use term canonizer utility locally in quantifiers ...	commit \| commitdiff \| tree
2021-01-27	Andrew Reynolds	Use standard conflict mechanism in quantifiers state...	commit \| commitdiff \| tree
2021-01-26	Andrew Reynolds	Introduce quantifiers inference manager (#5821)	commit \| commitdiff \| tree
2021-01-26	Andrew Reynolds	Remove deprecated quantifiers modules (#5820)	commit \| commitdiff \| tree
2021-01-26	Andrew Reynolds	Refactor quantifiers engine initialization (#5813)	commit \| commitdiff \| tree
2021-01-26	Haniel Barbosa	Reestablishing support for define-sort (#5810)	commit \| commitdiff \| tree
2021-01-26	Alex Ozdemir	Add proofs to TheoryArithPrivate::propagate (#5812)	commit \| commitdiff \| tree
2021-01-25	mudathirmahgoub	Refactor bags::SolverState (#5783)	commit \| commitdiff \| tree
2021-01-25	Andrew Reynolds	Ensure uses of ground terms in triggers are preprocessed...	commit \| commitdiff \| tree
2021-01-25	Andrew Reynolds	Split inst match generator into multiple files (#5805)	commit \| commitdiff \| tree
2021-01-25	Andrew Reynolds	Split E-matching strategies to own files (#5807)	commit \| commitdiff \| tree
2021-01-25	mudathirmahgoub	rename InferInfo::d_newSkolem to InferInfo::d_skolems...	commit \| commitdiff \| tree
2021-01-24	Andrew Reynolds	Initial cleaning of e-matching instantiation strategy...	commit \| commitdiff \| tree
2021-01-24	Andrew Reynolds	Initial cleaning of triggers (#5795)	commit \| commitdiff \| tree
2021-01-24	Andrew Reynolds	Initial cleaning of inst match generator (#5794)	commit \| commitdiff \| tree
2021-01-24	Andrew Reynolds	(proof-new) Instantiation list utility (#5768)	commit \| commitdiff \| tree
2021-01-24	Andrew Reynolds	Add interface for getting preprocessed term (#5798)	commit \| commitdiff \| tree
2021-01-22	Haniel Barbosa	[proof-new] Expanding MACRO_RESOLUTION in post-processing...	commit \| commitdiff \| tree
2021-01-21	Andrew Reynolds	Add div, mod, abs in non-strict parsing mode (#5793)	commit \| commitdiff \| tree
2021-01-21	Alex Ozdemir	arith: Proofs for Diophantine cuts (#5792)	commit \| commitdiff \| tree
2021-01-20	Andrew Reynolds	Refactoring the single invocation solver (#5706)	commit \| commitdiff \| tree
2021-01-20	Andrew Reynolds	Fix type issues with relevant domain computation (...	commit \| commitdiff \| tree
2021-01-20	Andrew Reynolds	Fix corner case of wrongly applied selector as trigger...	commit \| commitdiff \| tree
2021-01-20	Andrew Reynolds	Do not track processed in remove term formulas loop...	commit \| commitdiff \| tree
2021-01-20	Aina Niemetz	SMT2 parser: Do not add non-linear symbols for linear...	commit \| commitdiff \| tree
2021-01-20	Andrew Reynolds	Use arbitrary ground term assignment for sorts where...	commit \| commitdiff \| tree
2021-01-19	Alex Ozdemir	Implement proofs for arith BRAB lemmas (#5784)	commit \| commitdiff \| tree
2021-01-15	Andrew Reynolds	Implement --no-strings-lazy-pp as a preprocessing pass...	commit \| commitdiff \| tree
2021-01-14	Andrew Reynolds	Updates to theory preprocess equality (#5776)	commit \| commitdiff \| tree
2021-01-13	Andrew Reynolds	Split eager solver from strings solver state (#5775)	commit \| commitdiff \| tree
2021-01-13	Ying Sheng	Add unit test for api getInterpolant() -- issue #5593...	commit \| commitdiff \| tree
2021-01-13	Andrew Reynolds	Do not call ppRewrite on Boolean equalities (#5762)	commit \| commitdiff \| tree
2021-01-12	Aina Niemetz	google test: expr: Migrate node_black. (#5764)	commit \| commitdiff \| tree
2021-01-12	Aina Niemetz	google test: Use ASSERT_* instead of EXPECT_*. (#5765)	commit \| commitdiff \| tree
2021-01-12	yoni206	Foreign theory rewrite option (#5763)	commit \| commitdiff \| tree
2021-01-11	Andrew Reynolds	Merge theory registrar and theory proxy (#5758)	commit \| commitdiff \| tree
2021-01-11	Andrew Reynolds	Further simplifications in preparation for removing...	commit \| commitdiff \| tree
2021-01-11	Andrew Reynolds	Remove extended rewrite for arithmetic (#5760)	commit \| commitdiff \| tree
2021-01-09	yoni206	Strings arith checks preprocessing pass: step 2 (#5750)	commit \| commitdiff \| tree
2021-01-09	mudathirmahgoub	Fix issue 5513 (#5757)	commit \| commitdiff \| tree
2021-01-08	mudathirmahgoub	Rename getAntecedent to getPremises (#5754)	commit \| commitdiff \| tree
2021-01-08	Haniel Barbosa	[proof-new] Implementing getProof in the API and SMT...	commit \| commitdiff \| tree
2021-01-08	mudathirmahgoub	Add bags inference generator (#5731)	commit \| commitdiff \| tree
2021-01-08	yoni206	bv-to-int: avoid binarizing nodes twice (#5749)	commit \| commitdiff \| tree
2021-01-07	Gereon Kremer	Make sure polynomials are properly factorized in nl...	commit \| commitdiff \| tree
2021-01-07	Haniel Barbosa	Remove dependency on expression layer in TPTP parser...	commit \| commitdiff \| tree
2021-01-07	Haniel Barbosa	Fix warning in TPTP parser (#5752)	commit \| commitdiff \| tree
2021-01-06	yoni206	strings arith checks preprocessing pass: step 1 (#5747)	commit \| commitdiff \| tree
2021-01-06	Andrew Reynolds	Add new interfaces to term formula removal and theory...	commit \| commitdiff \| tree
2021-01-05	yoni206	Adding str.len to triggers (#5746)	commit \| commitdiff \| tree
2021-01-05	Andrew Reynolds	Remove a few miscellaneous references to the expr layer...	commit \| commitdiff \| tree
2020-12-24	Haniel Barbosa	[proof-new] Only use old proofs for unsat cores if...	commit \| commitdiff \| tree
2020-12-23	Haniel Barbosa	Dumping unsat cores after check-sat-assuming/QUERY...	commit \| commitdiff \| tree
2020-12-23	Andrew Reynolds	Add option to track and notify from CNF stream (#5708)	commit \| commitdiff \| tree
2020-12-23	Andrew Reynolds	Remove quant EPR option (#5716)	commit \| commitdiff \| tree
2020-12-23	Haniel Barbosa	[proof-new] Adding a manager for the new unsat cores...	commit \| commitdiff \| tree
2020-12-23	Andrew Reynolds	(proof-new) Miscelleneous fixes from proof-new (#5714)	commit \| commitdiff \| tree
2020-12-23	Gereon Kremer	Add proofs for nonlinear sign lemmas. (#5707)	commit \| commitdiff \| tree
2020-12-23	Andrew Reynolds	Minor simplification to Theory::theoryOf (#5719)	commit \| commitdiff \| tree
2020-12-22	yoni206	Delete duplicated code (#5718)	commit \| commitdiff \| tree
2020-12-22	Andrew Reynolds	Move slow regression to regress3 (#5715)	commit \| commitdiff \| tree
2020-12-22	Andrew Reynolds	Make theory preprocess rewrite equalities a preprocessing...	commit \| commitdiff \| tree
2020-12-22	Andrew Reynolds	Remove preregister instantiation heuristic (#5713)	commit \| commitdiff \| tree
2020-12-21	Gereon Kremer	Add proof for pi bound lemma (#5709)	commit \| commitdiff \| tree
2020-12-21	Haniel Barbosa	Have unsat core regression agnostic to number of assertions...	commit \| commitdiff \| tree
2020-12-21	Andrew Reynolds	Move ownership of theory preprocessor to TheoryProxy...	commit \| commitdiff \| tree
2020-12-21	Gereon Kremer	Add proof for sine shift lemmas. (#5710)	commit \| commitdiff \| tree
2020-12-21	Gereon Kremer	(proof-new) Make nl-ext factoring lemmas proof producing...	commit \| commitdiff \| tree
2020-12-21	Andrew Reynolds	Eliminate recursion from the internals of term formula...	commit \| commitdiff \| tree
2020-12-21	Andrew Reynolds	Fix issue with selector triggers (#5689)	commit \| commitdiff \| tree
next

RSS Atom