summaryrefslogtreecommitdiff
path: root/src/proof/cnf_proof.h
AgeCommit message (Collapse)Author
2021-05-20Remove old unsat cores (#6581)Haniel Barbosa
This commit removes the remaining old proof code and the code to produce unsat cores based on it.
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
2021-04-14Rename public and private headers in src/include. (#6352)Aina Niemetz
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-09Rename CVC4__ header guards to CVC5__. (#6326)Aina Niemetz
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-11Delete Expr layer. (#6117)Aina Niemetz
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-03More cleanup of includes to reduce compilation times (#6037)Gereon Kremer
Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files.
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
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
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
Fixes 2887.
2019-03-26Update copyright headers.Aina Niemetz
2019-03-16Enable CryptoMiniSat-backed BV proofs (#2847)Alex Ozdemir
* Connect the plumbing so that BV proofs are enabled when using CryptoMiniSat * Also fixed a bug in CNF-proof generation * Specifically, CNF proofs broke when proving tautological clauses. Now they don't.
2019-01-14ClausalBitvectorProof (#2786)Alex Ozdemir
* [DRAT] ClausalBitvectorProof Created a class, `ClausalBitvectorProof`, which represents a bitvector proof of UNSAT using an underlying clausal technique (DRAT, LRAT, etc) It fits into the `BitvectorProof` class hierarchy like this: ``` BitvectorProof / \ / \ ClausalBitvectorProof ResolutionBitvectorProof ``` This change is a painful one because all of the following BV subsystems referenced ResolutionBitvectorProof (subsequently RBVP) or BitvectorProof (subsequently BVP): * CnfStream * SatSolver (specifically the BvSatSolver) * CnfProof * TheoryProof * TheoryBV * Both bitblasters And in particular, ResolutionBitvectorProof, the CnfStream, and the SatSolvers were tightly coupled. This means that references to and interactions with (R)BVP were pervasive. Nevertheless, an SMT developer must persist. The change summary: * Create a subclass of BVP, called ClausalBitvectorProof, which has most methods stubbed out. * Make a some modifications to BVP and ResolutionBitvectorProof as the natural division of labor between the different classes becomes clear. * Go through all the components in the first list and try to figure out which kind of BVP they should **actually** be interacting with, and how. Make tweaks accordingly. * Add a hook from CryptoMinisat which pipes the produced DRAT proof into the new ClausalBitvectorProof. * Add a debug statement to ClausalBitvectorProof which parses and prints that DRAT proof, for testing purposes. Test: * `make check` to verify that we didn't break any old stuff, including lazy BB, and eager BB when using bvminisat. * `cvc4 --dump-proofs --bv-sat-solver=cryptominisat --bitblast=eager -d bv::clausal test/regress/regress0/bv/ackermann2.smt2`, and see that 1. It crashed with "Unimplemented" 2. Right before that it prints out the (textual) DRAT proof. * Remove 2 unneeded methods * Missed a rename * Typos Thanks Andres! Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu> * Address Andres comments * Reorder members of TBitblaster
2018-07-13Properly clean up assertion stack in CnfProof (#2147)Andres Noetzli
Fixes issue #2137. CnfProof has a stack of assertions that are being converted to clauses. Previously, it could happen that while an assertion was being added, TheoryProxy::explainPropagation() would be called from Solver::reason() and push an assertion to the stack that was then not removed. This lead to a clause id of the assertion being associated with the explanation instead, which in turn could lead to a wrong unsat core. This commit identifies two cases where TheoryProxy::explainPropagation() is called without cleaning up the assertion stack afterwards. It also adds an assertion that the assertion stack must be empty when we are getting the unsat core.
2018-06-25Updated copyright headers.Aina Niemetz
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
Adds missing override keywords.
2017-07-20Moving from the gnu extensions for hash maps to the c++11 hash mapsTim King
* Replacing __gnu_cxx::hash_map with std::unordered_map. * Replacing __gnu_cxx::hash_set with std::unordered_set. * Replacing __gnu_cxx::hash with std::hash. * Adding missing includes.
2017-07-07Update copyright headers.Mathias Preiner
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
2016-02-24Unifying the definitions of ClauseId to a single source of truth.Tim King
2016-01-26Merged bit-vector and uf proof branch.Liana Hadarean
2015-12-24Miscellaneous fixesTim King
- Splitting the two instances of CheckArgument. The template version is now always defined in base/exception.h and is available in a cvc4_public header. This version has lost its variadic version (due to swig not supporting va_list's). The CPP macro version has been renamed PrettyCheckArgument. (Taking suggestions for a better name.) This is now only defined in base/cvc4_assert.h. Only use this in cvc4_private headers and in .cpp files that can use cvc4_private headers. To use a variadic version of CheckArguments, outside of this scope, you need to duplicate this macro locally. See cvc3_compat.cpp for an example. - Making fitsSignedInt() and fitsUnsignedInt() work more robustly for CLN on 32 bit systems. - Refactoring ArrayStoreAll to avoid potential problems with circular header inclusions. - Changing some headers to use iosfwd when possible.
2015-03-10CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf ↵ajreynol
signature. Add regressions.
2014-08-22Unsat core infrastruture and API (SMT-LIB compliance to come).Morgan Deters
2014-07-01Update copyrights.Morgan Deters
2013-12-23Proof-checking code; fixups of segfaults and missing functionality in proof ↵Morgan Deters
generation; fix bug 285. * segfaults/assert-fails in proof-generation fixed, including bug 285 * added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present) * proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals) * proofs are *not* yet supported in incremental mode * added --dump-proofs to dump out proofs, like --dump-models * run_regression script now runs with --check-proofs where appropriate * options scripts now support :link-smt for SMT options, like :link for command-line
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-10-09cleaned up proof codelianah
2013-10-08fixed uf proof with holes bugslianah
2013-10-07first draft implementation of uf proofs with holesLiana Hadarean
2013-05-10now proofs print mapping between atom and propositional variable as a ↵lianah
comment in LFSC
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
just the header comments at the top, though. Don't update to this rev if you don't have time for a complete rebuild, and exclude this rev if you want to see what's new across a range of commits. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-24Fix the memout issue seen in recent nightly regressions (was due to aMorgan Deters
Statistics-printing problem, limited to certain benchmarks). Mark some unlabeled header files "cvc4_private.h". Other minor cleanup. (this commit was certified error- and warning-free by the test-and-commit script.)
2011-10-28* ability to output NodeBuilders without first converting them to ↵Morgan Deters
Nodes---useful for debugging. * language-dependent Node::toString() * some minor proof-related cleanup
2011-10-28merged the proofgen3 branch into trunk:Liana Hadarean
- can now output LFSC checkable resolution proofs - added configuration option --enable-proof - added command line argument --proof To turn proofs on build with proofs enabled and run with --proof.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback