summaryrefslogtreecommitdiff
path: root/src/proof
AgeCommit message (Collapse)Author
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-30Fix use-after-free with unsat cores/proofs (#174)Andres Nötzli
In TSatProof<Solver>::finalizeProof(), we got a clause from the clause allocator, called resolveUnit() and then size() on the clause. The problem is that resolveUnit() can reallocate memory (and there is even a comment warning about that in finalizeProof()), which invalidates the clause. This commit gets the clause again from the clause allocator before calling size().
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-05-31A more informative error message when a theory is not yet supported by the ↵guykatzz
proof infrastructure (e.g., quantifiers)
2017-05-26Fix use-after-free with ResChainsAndres Noetzli
This commit fixes an issue where the ResChain in `d_resolutionChains` gets deleted here: https://github.com/CVC4/CVC4/blob/master/src/proof/sat_proof_implementation.h#L729 The condition immediately after is false because the condition on line 727 is true. Thus, `d_resolutionChains` now has a deleted entry for `id`. When CVC4 afterwards gets the ResChain associated with `id` in `checkResolution()`, it accesses the deleted entry: https://github.com/CVC4/CVC4/blob/master/src/proof/sat_proof_implementation.h#L303
2017-05-04skolemization manager may be called also when just unsatCores are on ↵guykatzz
(related to bug 717)
2017-03-23support incremental unsat coresguykatzz
2017-03-17better support for proof production when encountering bool terms: handle the ↵guykatzz
new proof constructs generated by the equality engine. proof production for bool-array.smt2 passes
2017-03-14fix uninitialized variableAndres Notzli
2017-03-09bug fixguykatzz
2017-03-09better proof support for bools and formulasguykatzz
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-11-18Removing some throw specifiers from OutputChannel. Fixes bug 716.Tim King
2016-10-13Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git"Tim King
This reverts commit 3395c5c13cd61d98aec0d9806e3b9bc3d707968a, reversing changes made to 5f415d4585134612bc24e9a823289fee35541a01.
2016-10-11Merge branch 'origin' of https://github.com/CVC4/CVC4.gitPaul Meng
Conflicts: src/options/quantifiers_options
2016-10-05Added an option that allow empty dependencies when attempting to minimize ↵guykatzz
preprocessing holes
2016-09-27Removing an unused iterator.Tim King
2016-09-16Let arith_proof print its own termsGuy
2016-08-24Merge remote-tracking branch 'origin/master'PaulMeng
2016-08-11Add support for fewer preprocessing holesAndres Notzli
This commit adds support for the --fewer-preprocessing-holes flag. This flag changes the preprocessing part in proofs in two ways: it (1) removes assertions that are just restating inputs and uses the inputs directly instead and it (2) changes the form of the preprocessed assertions to contain the input that they originate from. The code in this commit is mostly taken from the proofs branch in Guy's fork.
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-08-05Minor: add/fix comments, remove redundant includesAndres Notzli
2016-08-03Fixed an issue where arrays proofs would sometimes have an extra ")" at the end.Guy
2016-07-28The "aggressive" optimizer for lemma L now returns the conjunction of all ↵Guy
lemmas L' that originated from L and were used in the unsat core
2016-07-28Bug fix involving negated lemmasGuy
2016-07-27Proper handling of IFF lemmas in the unsat core.Guy
Don't return duplicates in the unsat core
2016-07-27Added an option for a more aggressive weakest implicant optimizationGuy
2016-07-27If we can't find a weaker implicant, fail gracefully and return the original ↵Guy
lemma
2016-07-26Fix warnings in src/proofAndres Notzli
Fix warning due to `ProofLetCount` being defined as `struct` in `proof_utils.h` and `class` in `proof.h`. Fix warnings due to different number of arguments of `printConstantDisequalityProof()` and `printTheoryLemmaProof()` in subclasses.
2016-07-26Bug fix:Guy
If a lemma (a disjunction) has a "false" literal in it, it can be ignored, but a "true" literal really should stay
2016-07-26Letification of BV constantsGuy
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-25Bug fixGuy
2016-07-25Propagate the usage of proof let maps into constant disequality proofsGuy
2016-07-25Bug fixGuy
2016-07-24Use letification for the aliasing declarations as well (consequently, print ↵Guy
the global let map before the aliasing part)
2016-07-19Bug fixGuy
2016-07-19Allow a caller to query whether an unsat core is available or notGuy
2016-07-15Moved the assertion to a better spotGuy
2016-07-15The ProofManager now allows theory solvers to get their lemmas that ↵Guy
participate in the unsat cores. Currently this is only limited to lemmas generated via the d_out->lemma() interface, i.e. no propagations and conflict lemmas.
2016-07-06A few proof bugs fixedGuy
2016-07-05Merge branch 'master' of https://github.com/CVC4/CVC4.gitPaulMeng
Conflicts: proofs/signatures/Makefile.am src/Makefile.am src/expr/datatype.cpp src/options/datatypes_options src/options/options_template.cpp src/options/quantifiers_options src/proof/arith_proof.cpp src/proof/arith_proof.h src/proof/array_proof.cpp src/proof/array_proof.h src/proof/bitvector_proof.cpp src/proof/bitvector_proof.h src/proof/cnf_proof.cpp src/proof/cnf_proof.h src/proof/proof_manager.cpp src/proof/proof_manager.h src/proof/sat_proof.h src/proof/sat_proof_implementation.h src/proof/skolemization_manager.h src/proof/theory_proof.cpp src/proof/theory_proof.h src/proof/uf_proof.cpp src/proof/uf_proof.h src/prop/cnf_stream.cpp src/prop/cnf_stream.h src/prop/minisat/core/Solver.cc src/prop/prop_engine.cpp src/prop/prop_engine.h src/prop/theory_proxy.cpp src/smt/smt_engine.cpp src/smt/smt_engine_check_proof.cpp src/theory/arrays/array_proof_reconstruction.cpp src/theory/arrays/theory_arrays.cpp src/theory/bv/eager_bitblaster.cpp src/theory/bv/lazy_bitblaster.cpp src/theory/datatypes/theory_datatypes.cpp src/theory/quantifiers/alpha_equivalence.cpp src/theory/quantifiers/candidate_generator.cpp src/theory/quantifiers/candidate_generator.h src/theory/quantifiers/ce_guided_single_inv.cpp src/theory/quantifiers/ceg_instantiator.cpp src/theory/quantifiers/conjecture_generator.cpp src/theory/quantifiers/equality_infer.cpp src/theory/quantifiers/equality_infer.h src/theory/quantifiers/inst_match_generator.cpp src/theory/quantifiers/inst_propagator.cpp src/theory/quantifiers/inst_propagator.h src/theory/quantifiers/inst_strategy_e_matching.cpp src/theory/quantifiers/inst_strategy_e_matching.h src/theory/quantifiers/instantiation_engine.cpp src/theory/quantifiers/model_builder.cpp src/theory/quantifiers/model_engine.cpp src/theory/quantifiers/quant_conflict_find.cpp src/theory/quantifiers/quant_conflict_find.h src/theory/quantifiers/quant_split.cpp src/theory/quantifiers/quant_util.cpp src/theory/quantifiers/quantifiers_rewriter.cpp src/theory/quantifiers/quantifiers_rewriter.h src/theory/quantifiers/term_database.cpp src/theory/quantifiers/term_database.h src/theory/quantifiers/trigger.cpp src/theory/quantifiers/trigger.h src/theory/quantifiers_engine.cpp src/theory/quantifiers_engine.h src/theory/sets/kinds src/theory/sets/theory_sets_private.cpp src/theory/sets/theory_sets_private.h src/theory/sets/theory_sets_rewriter.cpp src/theory/sets/theory_sets_type_rules.h src/theory/strings/theory_strings.cpp src/theory/strings/theory_strings.h src/theory/theory_engine.cpp src/theory/theory_engine.h src/theory/uf/equality_engine.cpp test/regress/regress0/fmf/Makefile.am test/regress/regress0/quantifiers/Makefile.am test/regress/regress0/strings/Makefile.am test/regress/regress0/sygus/Makefile.am test/regress/regress0/sygus/max2-univ.sy
2016-07-01When proving a lemma, ignore literals that don't belong to the theory in ↵Guy
question, except for equalties
2016-07-01Handle bitvector lemmas where a literal gets rewritten into false, and ↵Guy
consequently the lemma doesn't match a recorded conflict
2016-06-30Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-06-30Support for the letification of chained AND and OR operations in LFSC proofsGuy
2016-06-23Fixed some warnings, fixed bug in cdhashmap that was crashing cdmap_black,Clark Barrett
re-enabled cdmap_black.
2016-06-20Addressed a bug that occurs when proof production is triggered via text ↵Guy
flags in the input. Separated some initialization into two phases: 1. Those that can be done when the proof compiliation flag is set 2. Those that can be done only when the --proof option is set. For #2, deferred their execution until the text flags in the input have been processed
2016-06-20Fixed a bug where the proofManager's init() call was not getting called, ↵Guy
resutling a null point deference
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback