summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
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-26Merge branch 'master' of https://github.com/CVC4/CVC4Guy
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-26Add option to minimize sygus solutions based on using weakest implicants of ↵ajreynol
instantiations in unsat cores.
2016-07-26Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-07-26Letification of BV constantsGuy
2016-07-26Minor improvements to strings related to constant splitting, including a few ↵ajreynol
options (disabled by default).
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-25Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-07-24cleanupGuy
2016-07-24Use letification for the aliasing declarations as well (consequently, print ↵Guy
the global let map before the aliasing part)
2016-07-24Proper 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-22Minor, error handling for polymorphism + sep logic.ajreynol
2016-07-21Fixes for strings, explanations for constant split propagations, substr ↵ajreynol
under concat rewrite. Avoid duplicate re.range length lemmas.
2016-07-20Infrastructure 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-20Print 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-20Infer conflicts in strings based on abstracting equality as contains. Minor ↵ajreynol
cleanup.
2016-07-19Bug fixGuy
2016-07-19Allow a caller to query whether an unsat core is available or notGuy
2016-07-19Add 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-16Refactor strings extf evaluation info. Ensure strings eager preprocess ↵ajreynol
eliminates all extf symbols during ppRewrite. Add options stringGuessModel and stringUfReduct. Minor optimizations.
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-15Minor simplification to normal form explanations.ajreynol
2016-07-08Minor fix to last commit.ajreynol
2016-07-07Simplifications for strings normal forms, fix case for concat reps in normal ↵ajreynol
forms.
2016-07-07Ensure heap disjointness in sep refinements.ajreynol
2016-07-07Refactoring 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-06A few proof bugs fixedGuy
2016-07-06Minor cleanup in strings, mostly related to negated str.contains.ajreynol
2016-07-06Add comment field for model, resolves hack for printing sep logic models.ajreynol
2016-07-05Refactor last call for theories, only create one model when quantifiers are ↵ajreynol
enabled. Fix sep.nil preregistration in TheorySep.
2016-07-05Add option --trigger-active-sel. Recognize simple triggers with polarity. Do ↵ajreynol
not drop patterns from merged prenex (fixes bug 743).
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-23Add theory/sep/kinds to EXTRA_DIST to fix distcheck failures.Clark Barrett
2016-06-23Fixed some warnings, fixed bug in cdhashmap that was crashing cdmap_black,Clark Barrett
re-enabled cdmap_black.
2016-06-20Merge branch 'master' of https://github.com/CVC4/CVC4Guy
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-20Minor change to sep/kindsajreynol
2016-06-20Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-06-20Fixed a bug where the proofManager's init() call was not getting called, ↵Guy
resutling a null point deference
2016-06-18Fix unit test.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback