summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-03-12less aggressiverewInferAndres Noetzli
2019-03-12minorAndres Noetzli
2019-03-12rewrite infAndres Noetzli
2019-02-05Make stripConstantEndpoints() less aggressiveAndres Noetzli
`stripConstantEndpoints({ "A" }, { "A". (int.to.str n) }, {}, {}, 0)` was cutting off "A" because it is a non-digit. This is wrong, however, because `(int.to.str n)` can return the empty string. This commit makes `stripConstantEndpoints()` less aggressive by not using `str.to.int` terms to cut off non-digits anymore.
2019-02-04mergeAndres Noetzli
2019-02-04Formatajreynol
2019-02-04Minorajreynol
2019-02-04Generalize sygus rr verify feature.ajreynol
2019-02-03Add rewrite for contains + const strings replace (#2828)Andres Noetzli
2019-02-03Merge branch 'REtoCtn' into cav2019stringsAndres Noetzli
2019-02-03Merge branch 'ctnRew' into cav2019stringsAndres Noetzli
2019-02-03Fix issueAndres Noetzli
2019-02-03Add rewrite for contains + const strings replaceAndres Noetzli
2019-02-03Rewrite simple regexp pattern to str.containsAndres Noetzli
2019-02-02Fix corner case in stripConstantEndpoints (#2824)Andres Noetzli
`stripConstantEndpoints()` was returning `true` when the first argument was a list only containing an empty string, which could lead to rewrite loops. This commit checks for that case and adds a unit test for it.
2019-01-29Fix warning due to catching polymorphic exceptions (#2821)Andres Noetzli
2019-01-29TestAndres Noetzli
2019-01-29New C++ API: Fix checks for mkTerm. (#2820)Aina Niemetz
This required fixing the OpTerm handling for mkTerm functions in the API.
2019-01-29Strings: Remove redundant replace rewrite (#2822)Andres Noetzli
Pulling the first constant string from a replace if there is no overlap with the search term is subsumed by the rewrite using `stripConstantEndpoints()`.
2019-01-29Merge branch 'fixStripConstantEndpoints' into cav2019stringsAndres Noetzli
2019-01-29Fix corner case in stripConstantEndpointsAndres Noetzli
`stripConstantEndpoints()` was returning `true` when the first argument was a list only containing an empty string, which could lead to rewrite loops. This commit checks for that case and adds a unit test for it.
2019-01-25Add approx optAndres Noetzli
2019-01-25Revert adding rewritesAndres Noetzli
2019-01-25Merge branch 'disableRewrite' into cav2019stringsAndres Noetzli
2019-01-25Strings: Remove redundant replace rewriteAndres Noetzli
Pulling the first constant string from a replace if there is no overlap with the search term is subsumed by the rewrite using `stripConstantEndpoints()`.
2019-01-24Extended DRAT signature to operational DRAT (#2815)Alex Ozdemir
* Extended DRAT signature to operational DRAT The DRAT signature now supports both operational and specified DRAT. That is, either kind of proof will be accepted. The goal of this implementation of operational DRAT was to re-use as much of the specified DRAT machinery as possible. However, by writing a separate operational signature, we could make it much more efficient (after all, operational DRAT came about because of a push for efficient cheking). You can run the new AND old DRAT tests by running ``` lfscc sat.plf smt.plf lrat.plf drat.plf drat_test.plf ``` * Apply suggestions from code review (Yoni) Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
2019-01-23Merge branch 'strongerContainsRew' into cav2019stringsAndres Noetzli
2019-01-23Revert "Minor"Andres Noetzli
This reverts commit b6dcaeb9b1e430941f1f4345152ebad21634a0be.
2019-01-23Merge branch 'strongerContainsRew' into cav2019stringsAndres Noetzli
2019-01-23MinorstrongerContainsRewAndres Noetzli
2019-01-23Merge branch 'strongerContainsRew' into cav2019stringsAndres Noetzli
2019-01-23FixAndres Noetzli
2019-01-23Merge branch 'strongerContainsRew' into cav2019stringsAndres Noetzli
2019-01-23MinorAndres Noetzli
2019-01-23Merge branch 'strongerContainsRew' into cav2019stringsAndres Noetzli
2019-01-23Strengthen contains rewritesAndres Noetzli
2019-01-23Add trace statementsAndres Noetzli
2019-01-23Avoid using ProofManager in non-proof CMS build (#2814)Andres Noetzli
PR #2786 changed `CryptoMinisatSolver::addClause()` to register clauses with the bit-vector proof if proofs are turned on. The new code requested the `ProofManager` even when proofs were turned off, which made the `eager-inc-cryptominisat.smt2` regression and our nightlies fail. This commit guards the access to the `ProofManager`, restoring the semantics of the original code when proofs are turned off.
2019-01-23mergeAndres Noetzli
2019-01-23FixAndres Noetzli
2019-01-22Strings: Strengthen multiset reasoning (#2817)Andres Noetzli
This commit introduces three helper methods for performing multiset reasoning: an entailment check whether a term is always a strict subset of another term in the multiset domain (`checkEntailMultisetSubset()`), a check whether a string term is always homogeneous (`checkEntailHomogeneousString()`), and an overapproximation for the multiset domain (`getMultisetApproximation()`). It also adds unit tests related to multiset reasoning.
2019-01-22Add option for stripping constant endpoints, fixing entail contains checksAndres Noetzli
2019-01-22Add multiset reasoning optionAndres Noetzli
2019-01-22Merge branch 'overapproxMultiset' into cav2019stringsAndres Noetzli
2019-01-22Merge branch 'master' into overapproxMultisetAndres Noetzli
2019-01-22Address commentsAndres Noetzli
2019-01-22 Fix tuple and record CVC printing (#2818)Andrew Reynolds
2019-01-22 Fix parsing of overloaded parametric datatype selectors (#2819)Andrew Reynolds
2019-01-22New README (markdown). (#2797)Aina Niemetz
2019-01-22Strings: Strengthen multiset reasoningAndres Noetzli
This commit introduces three helper methods for performing multiset reasoning: an entailment check whether a term is always a strict subset of another term in the multiset domain (`checkEntailMultisetSubset()`), a check whether a string term is always homogeneous (`checkEntailHomogeneousString()`), and an overapproximation for the multiset domain (`getMultisetApproximation()`). It also adds unit tests related to multiset reasoning.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback