summaryrefslogtreecommitdiff
path: root/proofs
AgeCommit message (Collapse)Author
2018-04-02a formula should be an instance of itself (#1668)yoni206
Proof checking failed when applying the instantiation rule so that the original formula and the instantiated formula are the same. Fixed using the new "ifequal" construct in lfsc.
2018-03-20correct instruction for running example (#1669)yoni206
2017-08-25Move LFSC checker out of the CVC repository. (#222)Aina Niemetz
LFSC now lives outside of the CVC4 repository and is not part of the CVC4 distribution anymore. As a consequence, we + Add --with-lfsc and --with-lfsc-directory as configure options. In the case where CVC4 has not been built with integrated LFSC, all code that interacts with LFSC is disabled. + Disable proof checking if CVC4_USE_LFSC is not defined. Configuring the build with --check-proofs but without --with-lfsc results in an error. + Do not call LFSC's cleanup function (but we should in the future). LFSC checker segfaults during cleanup on regression testcase regress0/bv/core/bitvec7.smt. Disabled call to lfscc_cleanup until the problem in lfscc is fixed. + Disable building with LFSC for the distcheck travis build since it is not part of the distribution anymore. Further, make distcheck with LFSC would require to call contrib/get-lfsc-checker before calling make check on the temp build (the build of the unpacked distribution tar ball).
2017-07-29Change remaining hash_set -> unordered_set (#208)Andres Noetzli
The nightly competition build has been failing due to a remaining use of hash_set in approx_simplex.cpp. This commit changes the remaining uses of hash_set to unordered_set. The remaining uses of hash_set were in LFSC. Switching to C++11 for LFSC required changing the configure.ac for LFSC to require C++11 support to make sure that it can be compiled independently from the rest of CVC4 (some of our Travis tests do that as well). To have the macros for these additional checks available, the commit adds a symlink to the files in config that contain the macros). I did not find a way to add macros from a parent's folder that did not break `make distcheck
2017-04-05Merge pull request #143 from FabianWolff/masterClark Barrett
Fix several spelling errors
2017-04-05[LFSC] Fix segfaultAndres Notzli
LFSC did not detect when the number of arguments provided to a side condition did not match the expected number of arguments, which could lead to out-of-bounds reads and writes. This commit adds a check and fixes one of the proof rules that provided the wrong number of arguments.
2017-04-05Fix several spelling errorsFabian Wolff
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-09bug fixguykatzz
2017-03-09better proof support for bools and formulasguykatzz
2017-03-06Adding support for bool-to-bvClark Barrett
Squashed commit of the following: commit 5197a663eb262afbeb7740f53b5bd27479dccea0 Author: Clark Barrett <barrett@cs.stanford.edu> Date: Mon Mar 6 00:16:16 2017 -0800 Remove IFF case commit 2119b25a30ed42eca54f632e7232c9f76ae5755a Author: guykatzz <katz911@gmail.com> Date: Mon Feb 20 12:37:06 2017 -0800 proof support for bvcomp commit d8c0c0d2c9c92ce06a5033ec0f3f85ea7bda1a22 Author: Clark Barrett <barrett@cs.stanford.edu> Date: Fri Feb 17 21:09:04 2017 -0800 Added missing cases to operator<< for bv rewrite rules. commit 0ed797c31d0e66cadc35b2397716c841d1aff270 Author: Clark Barrett <barrett@cs.stanford.edu> Date: Fri Feb 17 11:43:51 2017 -0800 Added rewrite rules for new bitvector kinds. commit 3b23dffb317de5559f8a95118fef633f711c114a Author: Clark Barrett <barrett@cs.stanford.edu> Date: Mon Feb 13 14:41:49 2017 -0800 First draft of bool-to-bv pass.
2017-01-16[LFSC] Fix performance issues, more determinismAndres Notzli
For certain proofs, the performance was drastically different on different OSes. The cause for this difference was a pointer comparison in the deduplication in `Expr::defeq()`. Depending on how the OS allocated the memory, an expression `a` would get replaced with an equivalent expression `b` or vice versa, which in turn affected performance of `Expr::free_in()` dramatically (sub-second vs. >5 min running times). This commit makes the process more deterministic by using a heuristic that favors symbolic expressions and greedily tries to make small refcounts smaller when replacing, and changes `Expr::free_in()` to not repeatedly explore the same subexpressions.
2017-01-04Marking the proof signature files as non-executable.Tim King
2017-01-04Reverting two files encoding with DOS linebreaks back into using unix ↵Tim King
linebreaks.
2017-01-04Merge pull request #122 from 4tXJ7f/fix_lfsc_strAndrew Reynolds
[LFSC] Minor fixes/improvements
2016-12-28[LFSC] Minor fixes/improvementsAndres Notzli
- Avoid mixing new/delete with malloc/free - Remove reimplementation of strcmp - Add assertions
2016-12-28[LFSC] Fix memory leaks when creating CExprsfix_lfsc_mem_leaksAndres Notzli
In certain cases, LFSC was creating CExprs with the single-argument constructor, which allocates an array of one child, only to immediately replace it with a new array (without deleting the old one). Additionally, this commit fixes the construction of TYPE/KIND/MPZ/MPQ expressions (the null pointer is appended automatically by the single argument constructor, an array with two null pointer entries should not be necessary).
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-09-25Adding virtual destructors to several classes in expr.h .Tim King
2016-08-24Merge remote-tracking branch 'origin/master'PaulMeng
2016-08-15Expression sharing on demand in LFSC (replace definitionally equivalent ↵ajreynol
child arguments after successful comparison).
2016-08-05Minor: add/fix comments, remove redundant includesAndres Notzli
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-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-03Better infrastructure for proving constant disequality.Guy
Added support for the BV case
2016-06-03A better mechanism for handling BV terms with aliases: inject the alias at ↵Guy
the decl_bblast step, instead of having an individual "with alias" rule for each BV operation
2016-06-01Merge from proof branchGuy
2016-06-01Revert "Merging proof branch"Guy
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
2016-06-01Merging proof branchGuy
2016-05-05Compute term indices lazily in TermDb. Optimization for qcf to recognize ↵ajreynol
irrelevant quantifiers based on irrelevant functions. Fix rewriter for prefix merges. Minor optimizations for LFSC. Work on --literal-matching. Updates to inst propagate, move instantiation filtering within qe. Enable sygus for string inputs.
2016-05-02Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, ↵ajreynol
do not combine quantifier prefixes with annotations. Eliminate use of context-dependent attributes in quantifiers.
2016-04-20update from the masterPaulMeng
2016-03-23squash-merge from proof branchGuy
2016-01-26Merged bit-vector and uf proof branch.Liana Hadarean
2015-04-23A few more minor updates to match google repository with CVC4 repositoryClark Barrett
(mostly whitespace differences).
2015-04-21Changes needed to compile at Google, plus some bug fixes from Google.Clark Barrett
2015-03-10CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf ↵ajreynol
signature. Add regressions.
2014-08-20Update bv proof signature and example, after discussions with Liana.ajreynol
2014-08-08Add draft of BV proof signature (incomplete) and example proof.ajreynol
2014-05-23Fix bug in E-matching Real/Int terms.Andrew Reynolds
2014-05-16lfsc_checker: fix some warnings reported by _both_ gcc and clangKshitij Bansal
2014-03-19Fix proof signatures makefileMorgan Deters
2014-03-19Fix a memory leak in LFSC proof checker. Largest QF_UF proof from Morgan ↵Andrew Reynolds
(problematic-lfsc-pf) now successfully checks in 58 seconds using ~8 GB memory. Add example test proof.
2014-03-14dos2unix on the proof signatures, and fix the makefile.Morgan Deters
2014-03-13Add working example of LFSC proof with quantifiers. Update quantifiers ↵Andrew Reynolds
signature to avoid dependent types in side condition.
2014-03-12Work on array pf signature, add working example. Add quantifiers proof ↵Andrew Reynolds
signature. Ignore terms not in current master EE for QCF. Minor refactoring. Make --rewrite-rules true by default.
2014-01-03Added support for proof production in Equality Engine. Cleaned up existing ↵Andrew Reynolds
proof signatures and added proof signature for theory of arrays. Added new MBQI technique based on interval abstraction. Cleaned up option names. Improved symmetry breaking for uf strong solver. Other minor cleanup.
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-18Reduce autoconf version for dependence (should fix 32-bit builds).Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback