Age | Commit message (Collapse) | Author | |
---|---|---|---|
2016-08-25 | Minor cleanup preprocessing, add ppNotifyAssertions. | ajreynol | |
2016-08-25 | Options for counterexample guided instantiation. | ajreynol | |
2016-08-24 | Merge remote-tracking branch 'origin/master' | PaulMeng | |
2016-08-19 | Fixed two bugs | Clark Barrett | |
2016-08-19 | Added fitsSignedLong and fitsUnsignedLong | Clark Barrett | |
2016-08-16 | Initial infrastructure for ExtTheory, generalize extended term handling in ↵ | ajreynol | |
TheoryStrings to use this. | |||
2016-08-15 | Expression sharing on demand in LFSC (replace definitionally equivalent ↵ | ajreynol | |
child arguments after successful comparison). | |||
2016-08-15 | Enable bounded set membership with --fmf-bound. Map to term models for ↵ | ajreynol | |
bounded set membership. | |||
2016-08-12 | Add a few more regressions. | ajreynol | |
2016-08-12 | Minor fixes to model construction to take singleton equivalence classes into ↵ | ajreynol | |
account (fixes sets+dt model bug). Minor fix for mixed int/real quantifier instantiation. | |||
2016-08-12 | Merge pull request #90 from 4tXJ7f/fewer_preproc_holes | guykatzz | |
Add support for fewer preprocessing holes | |||
2016-08-11 | Add support for fewer preprocessing holes | Andres 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-11 | Minor change to strings, introduce proxy vars only when necessary. | ajreynol | |
2016-08-10 | Improvements to strings: work on propagations for reverse normal form ↵ | ajreynol | |
processing. Better handling of disequalities, constant splitting and neg contain approximation. Introduce proxy vars for replace. Refactoring. | |||
2016-08-09 | Merge pull request #89 from 4tXJ7f/fix_proof_spaces | guykatzz | |
Fix missing/redundant spaces in proofs | |||
2016-08-09 | Fixes for sep star rewrite. | ajreynol | |
2016-08-09 | Fix missing/redundant spaces in proofsfix_proof_spaces | Andres 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-05 | Merge pull request #88 from 4tXJ7f/fix_comments | guykatzz | |
Minor: add/fix comments, remove redundant includes | |||
2016-08-05 | Minor: add/fix comments, remove redundant includes | Andres Notzli | |
2016-08-03 | Fixed an issue where arrays proofs would sometimes have an extra ")" at the end. | Guy | |
2016-08-03 | Merge pull request #87 from 4tXJ7f/fix_oob_access | barrettcw | |
Fix out-of-bounds access in ExprManager | |||
2016-07-30 | Prioritize inferences when processing normal forms in strings. | ajreynol | |
2016-07-28 | fixed construction of TC graph | Paul Meng | |
2016-07-28 | The "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-28 | fixed construction of TC graph | PaulMeng | |
2016-07-28 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy | |
2016-07-28 | Bug fix involving negated lemmas | Guy | |
2016-07-28 | Fix bug 749. | ajreynol | |
2016-07-28 | Add the negative conjunction case | Guy | |
2016-07-27 | Fix out-of-bounds access in ExprManager | Andres Notzli | |
The size of `d_exprStatisticsVars` was `LAST_TYPE` which was not enough because the INC_STAT macro tries to access `d_exprStatisticsVars[LAST_TYPE]` in some cases, resulting in an out-of-bounds access. Found bug with UBSan. | |||
2016-07-27 | Proper instrumentation of the preprocessing phase | Guy | |
2016-07-27 | proper handling of ITEs | Guy | |
2016-07-27 | Proper handling of IFF lemmas in the unsat core. | Guy | |
Don't return duplicates in the unsat core | |||
2016-07-27 | Added an option for a more aggressive weakest implicant optimization | Guy | |
2016-07-27 | If we can't find a weaker implicant, fail gracefully and return the original ↵ | Guy | |
lemma | |||
2016-07-26 | Merge pull request #86 from 4tXJ7f/fix_warnings | guykatzz | |
Fix warnings in src/proof | |||
2016-07-26 | Fix warnings in src/proof | Andres 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-26 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy | |
2016-07-26 | Bug 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-26 | Add option to minimize sygus solutions based on using weakest implicants of ↵ | ajreynol | |
instantiations in unsat cores. | |||
2016-07-26 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy | |
2016-07-26 | Letification of BV constants | Guy | |
2016-07-26 | Minor improvements to strings related to constant splitting, including a few ↵ | ajreynol | |
options (disabled by default). | |||
2016-07-26 | Added 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-25 | Bug fix | Guy | |
2016-07-25 | Propagate the usage of proof let maps into constant disequality proofs | Guy | |
2016-07-25 | Bug fix | Guy | |
2016-07-25 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy | |
2016-07-24 | cleanup | Guy | |
2016-07-24 | Use letification for the aliasing declarations as well (consequently, print ↵ | Guy | |
the global let map before the aliasing part) |