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

2021-05-20	Alex Ozdemir	Expand arith's farkas lemma rule as a macro (#6577)	commit \| commitdiff \| tree
2021-05-14	Alex Ozdemir	Add getId function to python API (#6523)	commit \| commitdiff \| tree
2021-05-13	Alex Ozdemir	Fix error message in toPythonObj (#6524)	commit \| commitdiff \| tree
2021-03-11	Alex Ozdemir	arith proof rules shuffle & add ARITH_SUM_UB (#6118)	commit \| commitdiff \| tree
2021-01-27	Alex Ozdemir	Thread proofs through arith channels & similar (#5818)	commit \| commitdiff \| tree
2021-01-26	Alex Ozdemir	Add proofs to TheoryArithPrivate::propagate (#5812)	commit \| commitdiff \| tree
2021-01-21	Alex Ozdemir	arith: Proofs for Diophantine cuts (#5792)	commit \| commitdiff \| tree
2021-01-19	Alex Ozdemir	Implement proofs for arith BRAB lemmas (#5784)	commit \| commitdiff \| tree
2020-12-18	Alex Ozdemir	Bugfix: proofs for props of non-normal arith lits ...	commit \| commitdiff \| tree
2020-12-04	Alex Ozdemir	Use NodeDfsIterable for makeBinary (#5595)	commit \| commitdiff \| tree
2020-11-10	Alex Ozdemir	Pin LFSC version (#5412)	commit \| commitdiff \| tree
2020-10-21	Alex Ozdemir	(proof-new) Add arith proof macros file to CMake (...	commit \| commitdiff \| tree
2020-10-21	Alex Ozdemir	(proof-new) arith: dedup literals in flattenImpl (...	commit \| commitdiff \| tree
2020-10-15	Alex Ozdemir	(proof-new) TheoryArithPrivate: farkas lemma proof...	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	Alex Ozdemir	(proof-new) pfs for conflicts in TheoryArithPrivate...	commit \| commitdiff \| tree
2020-10-14	Alex Ozdemir	(proof-new) Prove lemmas in Constraint (#5254)	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-07	Alex Ozdemir	(proof-new) proofs in ee -> arith pipeline (#5215)	commit \| commitdiff \| tree
2020-10-06	Alex Ozdemir	(proof-new) proofs for ArithCongMan -> ee facts (#5207)	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-09-29	Alex Ozdemir	(proof-new) Add proof managers and eager gens to arith...	commit \| commitdiff \| tree
2020-09-29	Alex Ozdemir	Add utilities for arith/proof_checker and build it...	commit \| commitdiff \| tree
2020-09-01	Alex Ozdemir	Add arithmetic-specific, runtime, proof-macros. (#4992)	commit \| commitdiff \| tree
2020-08-17	Alex Ozdemir	Add identifier name for side condition. (#4902)	commit \| commitdiff \| tree
2020-07-27	Alex Ozdemir	Consider negation's proof before triggering arith pfs...	commit \| commitdiff \| tree
2020-07-20	Alex Ozdemir	Fix a deadlock in the signature tests. (#4772)	commit \| commitdiff \| tree
2020-06-28	Alex Ozdemir	Proof Rules and Checker for Arithmetic (#4665)	commit \| commitdiff \| tree
2020-06-20	Alex Ozdemir	Use traversal iterators in IntToBv (#4169)	commit \| commitdiff \| tree
2020-04-11	Alex Ozdemir	Add skip predicate to node traversal. (#4222)	commit \| commitdiff \| tree
2020-03-28	Alex Ozdemir	Node traversal iterator (#3845)	commit \| commitdiff \| tree
2020-03-18	Alex Ozdemir	Move node visitor class from smt_util/ to expr/ (#4110)	commit \| commitdiff \| tree
2020-03-16	Alex Ozdemir	Remove AlwaysAssert(false) for hole.	commit \| commitdiff \| tree
2020-03-16	Alex Ozdemir	clang-format	commit \| commitdiff \| tree
2020-03-16	Alex Ozdemir	Fix simplicity check in prop	commit \| commitdiff \| tree
2020-03-16	Alex Ozdemir	Fix antecedent loop. Whoops	commit \| commitdiff \| tree
2020-03-16	Alex Ozdemir	Only save farkas+tightening proofs. Error on holes	commit \| commitdiff \| tree
2020-03-16	Alex Ozdemir	Expand the definition of a "simple" farkas proof.	commit \| commitdiff \| tree
2020-03-10	Alex Ozdemir	Document bv-to-bool recursion (#3848)	commit \| commitdiff \| tree
2020-03-05	Alex Ozdemir	Add a new arith constraint proof rule: IntTightenAP...	commit \| commitdiff \| tree
2020-03-05	Alex Ozdemir	Revert "Add a new arith constraint proof rule: IntTightenAP...	commit \| commitdiff \| tree
2020-02-22	Alex Ozdemir	RIP th_lra.plf (#3796)	commit \| commitdiff \| tree
2020-02-22	Alex Ozdemir	Switch to th_lira.plf (#3741)	commit \| commitdiff \| tree
2020-02-21	Alex Ozdemir	Remove IntReal tightening axioms from th_lira.plf ...	commit \| commitdiff \| tree
2020-02-11	Alex Ozdemir	Implement LFSCArithProof::equalityType. (#3740)	commit \| commitdiff \| tree
2020-02-10	Alex Ozdemir	Add function for tightening literals (#3732)	commit \| commitdiff \| tree
2020-02-10	Alex Ozdemir	Add more IntReal predicates (#3731)	commit \| commitdiff \| tree
2020-02-07	Alex Ozdemir	Propagate expected types through UF arguments (#3717)	commit \| commitdiff \| tree
2020-02-07	Alex Ozdemir	Add `ArithProof::{printInteger,getLfscFunction}` (...	commit \| commitdiff \| tree
2020-02-04	Alex Ozdemir	Articulate proof-related debug statements in arith...	commit \| commitdiff \| tree
2020-02-04	Alex Ozdemir	Regression tests for arithmetic proofs. (#3701)	commit \| commitdiff \| tree
2020-02-01	Alex Ozdemir	Handle `expectedType` in TheoryProofEngine (#3691)	commit \| commitdiff \| tree
2020-01-30	Alex Ozdemir	expectedType in proof-printing code (#3665)	commit \| commitdiff \| tree
2020-01-26	Alex Ozdemir	Axioms for affine function bounds. Tests. (#3632)	commit \| commitdiff \| tree
2020-01-21	Alex Ozdemir	Types and side conditions for affine bounds (#3631)	commit \| commitdiff \| tree
2020-01-21	Alex Ozdemir	Affine Axioms (#3630)	commit \| commitdiff \| tree
2020-01-21	Alex Ozdemir	Types & side-conditions for linear and affine fns ...	commit \| commitdiff \| tree
2020-01-21	Alex Ozdemir	Axioms (and side conditions) for tightening bounds...	commit \| commitdiff \| tree
2020-01-18	Alex Ozdemir	LIRA proof: Arithmetic predicates & reification thereof...	commit \| commitdiff \| tree
2020-01-17	Alex Ozdemir	LIRA sig: int, real terms, and conversions (#3610)	commit \| commitdiff \| tree
2019-12-31	Alex Ozdemir	[proof] ITE translation fix (#3484)	commit \| commitdiff \| tree
2019-12-06	Alex Ozdemir	[proof] Eliminate side-condition from ER signature...	commit \| commitdiff \| tree
2019-11-19	Alex Ozdemir	Add a few comments to ProofManager (#3477)	commit \| commitdiff \| tree
2019-11-19	Alex Ozdemir	Signature documentation update (#3476)	commit \| commitdiff \| tree
2019-11-14	Alex Ozdemir	Use Shebang in cxxtestgen when appropriate (#3458)	commit \| commitdiff \| tree
2019-07-02	Alex Ozdemir	Optimize DRAT optimization: clause matching (#3074)	commit \| commitdiff \| tree
2019-06-05	Alex Ozdemir	DRAT-Optimization (#2971)	commit \| commitdiff \| tree
2019-04-23	Alex Ozdemir	[BV] An option for SAT proof optimization (#2915)	commit \| commitdiff \| tree
2019-04-05	Alex Ozdemir	SatClauseSetHashFunction (#2916)	commit \| commitdiff \| tree
2019-03-16	Alex Ozdemir	Enable CryptoMiniSat-backed BV proofs (#2847)	commit \| commitdiff \| tree
2019-03-01	Alex Ozdemir	ErProof class with LFSC output (#2812)	commit \| commitdiff \| tree
2019-01-24	Alex Ozdemir	Extended DRAT signature to operational DRAT (#2815)	commit \| commitdiff \| tree
2019-01-18	Alex Ozdemir	Extract DIMACS Printing (#2800)	commit \| commitdiff \| tree
2019-01-16	Alex Ozdemir	Bugfix: LFSC clause equality (#2801)	commit \| commitdiff \| tree
2019-01-16	Alex Ozdemir	Extended Resolution Signature (#2788)	commit \| commitdiff \| tree
2019-01-14	Alex Ozdemir	ClausalBitvectorProof (#2786)	commit \| commitdiff \| tree
2019-01-13	Alex Ozdemir	LFSC LRAT Output (#2787)	commit \| commitdiff \| tree
2019-01-12	Alex Ozdemir	LratInstruction inheritance (#2784)	commit \| commitdiff \| tree
2019-01-11	Alex Ozdemir	Fixed linking against drat2er, and use drat2er (#2785)	commit \| commitdiff \| tree
2019-01-09	Alex Ozdemir	[BV Proofs] Option for proof format (#2777)	commit \| commitdiff \| tree
2019-01-09	Alex Ozdemir	Clause proof printing (#2779)	commit \| commitdiff \| tree
2019-01-09	Alex Ozdemir	LFSC drat output (#2776)	commit \| commitdiff \| tree
2019-01-06	Alex Ozdemir	[DRAT] DRAT data structure (#2767)	commit \| commitdiff \| tree
2019-01-04	Alex Ozdemir	[LRAT] A C++ data structure for LRAT. (#2737)	commit \| commitdiff \| tree
2019-01-03	Alex Ozdemir	[LRA proof] Recording & Printing LRA Proofs (#2758)	commit \| commitdiff \| tree
2018-12-17	Alex Ozdemir	Configured for linking against drat2er (#2754)	commit \| commitdiff \| tree
2018-12-17	Alex Ozdemir	DRAT Signature (#2757)	commit \| commitdiff \| tree
2018-12-15	Alex Ozdemir	[LRA Proof] Storage for LRA proofs (#2747)	commit \| commitdiff \| tree
2018-12-12	Alex Ozdemir	[LRA proof] More complete LRA example proofs. (#2722)	commit \| commitdiff \| tree
2018-12-12	Alex Ozdemir	[LRAT] signature robust against duplicate literals...	commit \| commitdiff \| tree
2018-12-11	Alex Ozdemir	LRAT signature (#2731)	commit \| commitdiff \| tree
2018-12-07	Alex Ozdemir	Arith Constraint Proof Loggin (#2732)	commit \| commitdiff \| tree
2018-12-07	Alex Ozdemir	Enable BV proofs when using an eager bitblaster (#2733)	commit \| commitdiff \| tree
2018-12-03	Alex Ozdemir	Bit vector proof superclass (#2599)	commit \| commitdiff \| tree
2018-11-27	Alex Ozdemir	LRA proof signature fixes and a first proof for linear...	commit \| commitdiff \| tree
2018-11-20	Alex Ozdemir	Change lemma proof step storage & iterators (#2712)	commit \| commitdiff \| tree
2018-10-02	Alex Ozdemir	Fix documentation for `make regress`. (#2557)	commit \| commitdiff \| tree

RSS Atom