summaryrefslogtreecommitdiff
path: root/src/proof/sat_proof.h
AgeCommit message (Collapse)Author
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
Fixes 2887.
2019-03-26Update copyright headers.Aina Niemetz
2018-08-27Resolution proof: separate printing from proof (#1964)Andres Noetzli
Currently, we have an LFSCSatProof which inherits from TSatProof and implements printing the proof. The seperation is not clean (e.g. clauseName is used for printing only but is in TSatProof) and the inheritance does not add any value while making dependencies more confusing. The plan is that TSatProof becomes a self-contained part that the MiniSat implementations generate and ProofManager prints out. This commit is a first step in that direction. For SAT solvers with native capabilities for producing proofs, we would simply implement a different LFSC printer of their proof representation without changing the SAT solver itself. The inheritance would make this awkward to deal with. Additionally, the commit cleans up some unused functions and adjusts the visibility of TSatProof methods and members.
2018-06-25Updated copyright headers.Aina Niemetz
2018-05-23Remove ProofProxy (#1965)Andres Noetzli
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
Adds missing override keywords.
2018-02-09Replacing an incorrect reference to an injected class name when the type was ↵Tim King
meant. (#1585)
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
2017-06-16Fix segfault by making unit conflict CDMaybeAndres Nötzli
This commit fixes bug 819 by making d_unitConflictId context dependent and adds a test case.
2017-03-23support incremental unsat coresguykatzz
2016-07-26Added functionality to retrieve a lemma's "weakest implicant" in the unsat ↵Guy
core. Currently, lemmas that are not conjunctions and their own weakest implicants; but for lemmas that *are* conjunctions, we may return only a subset of the conjuncts.
2016-07-19Allow a caller to query whether an unsat core is available or notGuy
2016-04-30Reviewed Tim's Asan changes and improved SatProof comments.Liana Hadarean
2016-04-26Fixing memory leaks for garbage collection of ResChains in the sat proof ↵Tim King
implementation. As a part of tracking this down, I've modified a number of accessor functions in TSatProof to be const. An expert in this code will need to do a pass over this.
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-02-01Fixing white spaces in sat_proof.h.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-04-17moved Minisat namespace into CVC4Finn Haedicke
This avoids conflicts when CVC4 is linked to an application that also uses plain Minisat.
2015-03-16Fixed proof unitialized memory and minor memory leaks.Liana Hadarean
2014-08-22Unsat core infrastruture and API (SMT-LIB compliance to come).Morgan Deters
2014-07-01Update copyrights.Morgan Deters
2013-12-24Java datatype API fixups, datatype API examplesMorgan 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-11-13Add virtual destructors where missingMorgan Deters
2013-10-09cleaned up proof codelianah
2013-10-09fixed uf proof bug: now storing deleted theory lemmaslianah
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-05-10fixes to the proof system so it works with theory lemmas and explanationslianah
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-02-16Some cleanup and copyright updatingMorgan Deters
* update some copyrights for 2013 * cleaned up some comments/ifdefs, indentation * some spelling corrections * add some missing makefiles
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-29fix some doxygen warningsMorgan Deters
2011-10-29Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, ↵Morgan Deters
SmtEngine::getProof(), a few other things..
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