cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2018-12-11	[LRAT] signature robust against duplicate literals (#2743)	Alex Ozdemir
	* [LRAT] signature robust against duplicate literals The LRAT signature previously had complex, surprising, and occasionally incorrect behavior when given clauses with duplicate literals. Now it does not. Now clauses have true set semantics, and clauses with duplicate literals are treated identically to those without. * Test with logically = but structurally != clauses.
2018-12-11	LRAT signature (#2731)	Alex Ozdemir
	* LRAT signature Added an LRAT signature. It is almost entirely side-conditions, but it works. There is also a collection of tests for it. You can run them by invoking ``` lfscc smt.plf sat.plf lrat.plf lrat_test.plf ``` * Update proofs/signatures/lrat.plf per Yoni's suggestion. Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu> * Responding to Yoni's comments. * Removed unused varaibles Some tests declared `var`s which were unused. Now they don't.