Age | Commit message (Collapse) | Author | |
---|---|---|---|
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-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) | |||
2016-07-24 | Proper handling for lemmas that are conjuncts: | Guy | |
Record a separate recipe for each conjunct, but have as the "original lemma" in this recipe the complete conjunction, so that we can report this to the theory solver later, if asked. Refactoring: instead of propagating the proof recipes from the theory engine to the prop engine and cnf stream to be registered there, just register them at the theory engine - as the prop engine and cnf stream don't change them. | |||
2016-07-22 | Minor, error handling for polymorphism + sep logic. | ajreynol | |
2016-07-21 | Fixes for strings, explanations for constant split propagations, substr ↵ | ajreynol | |
under concat rewrite. Avoid duplicate re.range length lemmas. | |||
2016-07-20 | Infrastructure for storing and printing heap models for separation logic. ↵ | ajreynol | |
Ensure value of sep.nil is correct in models. Print instantiations as sexprs. | |||
2016-07-20 | Print only instantiations that are in the unsat core when --proof is ↵ | ajreynol | |
enabled. Add option to minimize sygus solutions based on unsat core (disabled by default). | |||
2016-07-20 | Infer conflicts in strings based on abstracting equality as contains. Minor ↵ | ajreynol | |
cleanup. | |||
2016-07-19 | Bug fix | Guy | |
2016-07-19 | Allow a caller to query whether an unsat core is available or not | Guy | |
2016-07-19 | Add infrastructure for tracking instantiation lemmas (for proofs, and ↵ | ajreynol | |
minimization of --dump-instantiations, qe and synthesis solutions). Eliminate quantified arithmetic variables that only have lower/upper bounds. Cleanup strings preprocess, minor fix for str.replace semantics. Reorder cegqi before fmf. Minor cleanup. | |||
2016-07-16 | Refactor strings extf evaluation info. Ensure strings eager preprocess ↵ | ajreynol | |
eliminates all extf symbols during ppRewrite. Add options stringGuessModel and stringUfReduct. Minor optimizations. | |||
2016-07-15 | Moved the assertion to a better spot | Guy | |
2016-07-15 | The 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-15 | Minor simplification to normal form explanations. | ajreynol | |
2016-07-08 | Minor fix to last commit. | ajreynol | |
2016-07-07 | Simplifications for strings normal forms, fix case for concat reps in normal ↵ | ajreynol | |
forms. | |||
2016-07-07 | Ensure heap disjointness in sep refinements. | ajreynol | |
2016-07-07 | Refactoring of strings preprocess module. When enabled, apply eager ↵ | ajreynol | |
preprocess during ppRewrite instead of during processAssertions. Simplify reduction for contains. Fix bug in explanations for F_EndpointEq. Minor cleanup for sep. | |||
2016-07-06 | A few proof bugs fixed | Guy | |
2016-07-06 | Minor cleanup in strings, mostly related to negated str.contains. | ajreynol | |
2016-07-06 | Add comment field for model, resolves hack for printing sep logic models. | ajreynol | |
2016-07-05 | Refactor last call for theories, only create one model when quantifiers are ↵ | ajreynol | |
enabled. Fix sep.nil preregistration in TheorySep. | |||
2016-07-05 | Add option --trigger-active-sel. Recognize simple triggers with polarity. Do ↵ | ajreynol | |
not drop patterns from merged prenex (fixes bug 743). | |||
2016-07-01 | When proving a lemma, ignore literals that don't belong to the theory in ↵ | Guy | |
question, except for equalties | |||
2016-07-01 | Handle bitvector lemmas where a literal gets rewritten into false, and ↵ | Guy | |
consequently the lemma doesn't match a recorded conflict | |||
2016-06-30 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy | |
2016-06-30 | Support for the letification of chained AND and OR operations in LFSC proofs | Guy | |
2016-06-23 | Add theory/sep/kinds to EXTRA_DIST to fix distcheck failures. | Clark Barrett | |
2016-06-23 | Fixed some warnings, fixed bug in cdhashmap that was crashing cdmap_black, | Clark Barrett | |
re-enabled cdmap_black. | |||
2016-06-20 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy | |
2016-06-20 | Addressed 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-20 | Minor change to sep/kinds | ajreynol | |
2016-06-20 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Guy | |
2016-06-20 | Fixed a bug where the proofManager's init() call was not getting called, ↵ | Guy | |
resutling a null point deference | |||
2016-06-18 | Fix unit test. | ajreynol | |
2016-06-17 | Cleanup from last commit, treat sep.nil as variable kind. | ajreynol | |