summaryrefslogtreecommitdiff
path: root/src/proof/arith_proof.cpp
AgeCommit message (Collapse)Author
2020-09-01Removes old proof code (#4964)Haniel Barbosa
This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure. It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver).
2020-06-16Update copyright headers.Aina Niemetz
2020-03-16Remove AlwaysAssert(false) for hole.Alex Ozdemir
2020-03-16Only save farkas+tightening proofs. Error on holesAlex Ozdemir
I'll remove the error later
2020-02-21Switch to th_lira.plf (#3741)Alex Ozdemir
Switches arith_proof.cpp from th_lra to th_lira. Changes: Eliminate the d_realMode hack. instead: modify printOwnedTermAsType prints as integers OR reals, depending on expectedType. simultaneously: write printOwnedTermAsType more concisely also: reimplement printOwnedSort. Change to the LIRA axioms: Because they reason about bound types using side conditions, we no longer need to worry about choosing the correct strictness for our axiom. This allows us to cut out a lot of code, rewriting & shrinking printTheoryLemmaProof. They also have different names. This requires us to change a lot of string literals enable proof-checking for many tests.
2020-02-10Implement LFSCArithProof::equalityType. (#3740)Alex Ozdemir
Also, missed an armType use.
2020-02-10Add function for tightening literals (#3732)Alex Ozdemir
* Add function for tightening literals The function tightens a literal if it can be tightened, and prints a proof of the result. * Include a #include Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
2020-02-07Add `ArithProof::{printInteger,getLfscFunction}` (#3716)Alex Ozdemir
2020-01-29expectedType in proof-printing code (#3665)Alex Ozdemir
* expectedType in proof-printing code To print lemma proofs in theories that use multiple sorts that have a subtype relationship, we need to increase communication between the TheoryProofEngine and the theory proofs themselves. This commit add an (optional) argument `expectedType` to many term-printing functions in TheoryProofEngine and TheoryProof. Right now it is unused, so always takes on the default value of "null" (meaning no type expectation), but in the future the TheoryProofEngine will use it to signal TheoryProof about what type is expected to be printed. * TypeNode, Don't mix default args & virtual * Use TypeNode instead of Type (The former are lighter) * Don't add default arguments to virtual functions, because these cannot be dynamically overriden during a dynamic dispatch. * Since we don't want them to be overidable anyway, we use two functions: one that is non-virtual and has a default, the other that is virtual but has no default. The former just calls the latter. * clang-format after signature changes
2019-12-30[proof] ITE translation fix (#3484)Alex Ozdemir
* Bugfix: convert ifte arms to formulas for printing We have two kinds of ITEs in our LFSC proofs: * ite: for sort-typed expressions * ifte: for formulas Say that we have a Bool-sorted ITE. We had machinery for emitting an `ifte` for it, but this machinery didn't actually convert the arms of the ITE into formulas... Facepalm. Fixed now. * Test the lifting of ITEs from arithmetic. This test verifies that booleans ITEs are correctly lifted to formula ITEs in LRA proofs. It used to fail, but now passes. * clang-format * Typos. * Add test to CMake * Set --check-proofs in test * Address Yoni * Expand printsAsBool documentation * Assert ITE typing soundness * Assert a subtype relation for ITEs, not equality * Update src/proof/arith_proof.h Thanks Yoni! Co-Authored-By: yoni206 <yoni206@users.noreply.github.com> Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-03-26Update copyright headers.Aina Niemetz
2019-01-03[LRA proof] Recording & Printing LRA Proofs (#2758)Alex Ozdemir
* [LRA proof] Recording & Printing LRA Proofs Now we use the ArithProofRecorder to record and later print arithmetic proofs. If an LRA lemma can be proven by a single farkas proof, then that is done. Otherwise, we `trust` the lemma. I haven't **really** enabled LRA proofs yet, so `--check-proofs` still is a no-op for LRA. To test, do ``` lfsccvc4 <(./bin/cvc4 --dump-proofs ../test/regress/regress0/lemmas/mode_cntrl.induction.smt | tail -n +2) ``` where `lfsccvc4` is an alias invoking `lfscc` with all the necessary signatures. On my machine that is: ``` alias lfsccvc4="/home/aozdemir/repos/LFSC/build/src/lfscc \ /home/aozdemir/repos/CVC4/proofs/signatures/sat.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/smt.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/lrat.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_base.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_bv.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_bv_bitblast.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_arrays.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_int.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_quant.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_real.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_real.plf" ``` * Added guards to proof recording Also reverted some small, unintentional changes. Also had to add printing for STRING_SUBSTR?? * Responding to Yoni's review * SimpleFarkasProof examples * Respond to Aina's comments * Reorder Constraint declarations * fix build * Moved friend declaration in Constraint * Trichotomy example * Lift getNumChildren invocation in PLUS case Credits to aina for spotting it. * Clang-format
2018-12-14 [LRA Proof] Storage for LRA proofs (#2747)Alex Ozdemir
* [LRA Proof] Storage for LRA proofs During LRA solving the `ConstraintDatabase` contains the reasoning behind different constraints. Combinations of constraints are periodically used to justify lemmas (conflict clauses, propegations, ... ?). `ConstraintDatabase` is SAT context-dependent. ArithProofRecorder will be used to store concise representations of the proof for each lemma raised by the (LR)A theory. The (LR)A theory will write to it, and the ArithProof class will read from it to produce LFSC proofs. Right now, it's pretty simplistic -- it allows for only Farkas proofs. In future PRs I'll: 1. add logic that stores proofs therein 2. add logic that retrieves and prints proofs 3. enable LRA proof production, checking, and testing * Document ArithProofRecorder use-sites * Update src/proof/arith_proof_recorder.cpp Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu> * Yoni's review * clang-format * Response to Mathias' review.
2018-06-25Updated copyright headers.Aina Niemetz
2018-04-25Refactor array-proofs and uf-proofs (#1655)yoni206
This commit unifies duplicate code blocks from array_proof.cpp and uf_proof.cpp into theory_proof.cpp.
2017-11-15Adding garbage collection for Proof objects. (#1294)Tim King
2017-10-25Switching EqProof to use shared_ptr everywhere. (#1217)Tim King
This clarifies the memory ownership of EqProofs.
2017-07-07Update copyright headers.Mathias Preiner
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove ↵ajreynol
Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
2016-09-16Let arith_proof print its own termsGuy
2016-08-09Fix missing/redundant spaces in proofsfix_proof_spacesAndres Notzli
Before, in some cases, e.g. when printing sorts and in resolution proofs, the proofs contained redundant and/or missing spaces. With this commit, CVC4 now prints out `(trust_f (= (Array Index Element) let10 let12)` instead of `(trust_f (= (Array Index Element )let10 let12))`.
2016-07-24Use letification for the aliasing declarations as well (consequently, print ↵Guy
the global let map before the aliasing part)
2016-06-08Support for printing a global let map in LFSC proofs.Guy
Added a flag to enable/disbale this feature (enabled by default). Also, added some infrastructure for proving rewrite rules.
2016-06-01Merge from proof branchGuy
2016-06-01Revert "Merging proof branch"Guy
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
2016-06-01Merging proof branchGuy
2016-04-03Updating the copyright headers and scripts.Tim King
2016-03-23squash-merge from proof branchGuy
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback