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

Age	Commit message (Collapse)	Author
2019-12-06	[proof] Eliminate side-condition from ER signature (#3230)	Alex Ozdemir
	* [proof] Eliminate the side condition in er.plf By tweaking the axioms a bit, I got rid of the lone SC in the Extended Resolution signature. * [proof] Changed er_proof.cpp in line with signature The new signature requires slightly different proof printing. * [proof] clang-format er_proof.cpp * Fix tests * [proof] Actually delete the SC * Apply suggestions from code review Co-Authored-By: yoni206 <yoni206@users.noreply.github.com> * Add LFSC-checking unit test for ER proof * Gate the lfsc invocation on the build system * Properly gate the lfsc check on the build system * gate the plf_signatures forward def on the build system
2019-01-15	Extended Resolution Signature (#2788)	Alex Ozdemir
	* Extended Resolution Signature While extended resolution is a fairly general technique, the paper "Extended Resolution Simulates DRAT" / the drat2er uses exactly one new type of rule: definitions of the form new <=> old v (~l_1 ^ ~l_2 ^ ... ^ ~l_n) This PR adds axioms supporting this kind of definition, and adds a test making use of those new axioms. The axioms support the following ideas: 1. Introducing a fresh variable, defined in the form above 2. Clausifying that definition to produce proofs of $$ n + 2 $$ new clauses in the form of two clauses, and a cnf with $$ n $$ clauses 3. An axiom for unrolling the proof of the cnf into proofs of the original clauses. * Addressing Yoni's comments 1. Added a new (trivial) test 2. Improved a bunch of documentation * Update proofs/signatures/er.plf Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu> * Removed references to RATs from the signature There are still a few references in the header comment. * Aside on continuations * Scrap the elision annotations