summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-08-25Minor cleanup preprocessing, add ppNotifyAssertions.ajreynol
2016-08-25Options for counterexample guided instantiation.ajreynol
2016-08-24Merge remote-tracking branch 'origin/master'PaulMeng
2016-08-19Fixed two bugsClark Barrett
2016-08-19Added fitsSignedLong and fitsUnsignedLongClark Barrett
2016-08-16Initial infrastructure for ExtTheory, generalize extended term handling in ↵ajreynol
TheoryStrings to use this.
2016-08-15Expression sharing on demand in LFSC (replace definitionally equivalent ↵ajreynol
child arguments after successful comparison).
2016-08-15Enable bounded set membership with --fmf-bound. Map to term models for ↵ajreynol
bounded set membership.
2016-08-12Add a few more regressions.ajreynol
2016-08-12Minor 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-12Merge pull request #90 from 4tXJ7f/fewer_preproc_holesguykatzz
Add support for fewer preprocessing holes
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-11Minor change to strings, introduce proxy vars only when necessary.ajreynol
2016-08-10Improvements 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-09Merge pull request #89 from 4tXJ7f/fix_proof_spacesguykatzz
Fix missing/redundant spaces in proofs
2016-08-09Fixes for sep star rewrite.ajreynol
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-05Merge pull request #88 from 4tXJ7f/fix_commentsguykatzz
Minor: add/fix comments, remove redundant includes
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-08-03Merge pull request #87 from 4tXJ7f/fix_oob_accessbarrettcw
Fix out-of-bounds access in ExprManager
2016-07-30Prioritize inferences when processing normal forms in strings.ajreynol
2016-07-28fixed construction of TC graphPaul Meng
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-28fixed construction of TC graphPaulMeng
2016-07-28Merge branch 'master' of https://github.com/CVC4/CVC4Guy
2016-07-28Bug fix involving negated lemmasGuy
2016-07-28Fix bug 749.ajreynol
2016-07-28Add the negative conjunction caseGuy
2016-07-27Fix out-of-bounds access in ExprManagerAndres 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-27Proper instrumentation of the preprocessing phaseGuy
2016-07-27proper handling of ITEsGuy
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-26Merge pull request #86 from 4tXJ7f/fix_warningsguykatzz
Fix warnings in src/proof
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback