summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Collapse)Author
2018-04-08Allow predetermined first-order variables when constructing deep embedding. ↵Andrew Reynolds
(#1757)
2018-04-08Check free variables in assertions (#1737)Andrew Reynolds
2018-04-08Add quantifier name attribute. (#1756)Andrew Reynolds
2018-04-05Add more general SignExtendUltConst rewriting. (#1385)Mathias Preiner
This also adds an additional check in processAssertions to ensure that all assertions are guaranteed to be rewritten (there was only a comment stating this).
2018-04-04Proper initialization and destruction of sygus unif (#1750)Andrew Reynolds
2018-04-04Fix for corner case of higher-order matching (#1708)Andrew Reynolds
2018-04-04Do not debug check models when unknown (#1748)Andrew Reynolds
2018-04-04Fix sygus infer (#1747)Andrew Reynolds
2018-04-03Option to turn arbitrary input into sygus (#1704)Andrew Reynolds
Preprocessing pass that turns an arbitrary (e.g. smt2) input into a sygus conjecture, which is helpful for Horn clause solving. This includes improvements to the robustness of the sygus solver.
2018-04-03Make sygus unif I/O an subclass of sygus unif (#1741)Andrew Reynolds
2018-04-03Use choice when expanding definitions for inverse transcendental functions ↵Andrew Reynolds
(#1742)
2018-04-03Internal sygus type checking (#1734)Andrew Reynolds
2018-04-02Improvements to extended rewriter for Booleans and ITE (#1705)Andrew Reynolds
2018-04-02Make sygus unif utility use sygus unif strategies (#1732)Andrew Reynolds
2018-04-02Reorganize bitblaster code. (#1695)Mathias Preiner
This splits bitblaster_template.h into the separate header files {aig,eager,lazy}_bitblaster.h and bitblaster.h (the template class TBitblaster). All the bitblaster related code is moved into the sub-directory bitblast/.
2018-03-30Split strategy representation from SygusUnif (#1730)Andrew Reynolds
2018-03-30Do not use factoring inference for transcendental functions (#1707)Andrew Reynolds
2018-03-29Simplify sygus unif so that it is one-to-one with functions to synthesize ↵Andrew Reynolds
(#1726)
2018-03-27Make sygus pbe use sygus unif utility (#1724)Andrew Reynolds
2018-03-27Fix for --sygus-rr-synth (#1723)Andrew Reynolds
2018-03-27Make sygus unif utility (#1720)Andrew Reynolds
2018-03-27Filter candidate rewrites based on matching (#1682)Andrew Reynolds
2018-03-26Better normalization of string concatenation (#1719)Andres Noetzli
2018-03-26Documentation and simplifications for PBE (#1677)Andrew Reynolds
2018-03-26 Add reasoning for inequalities in str rewriter (#1713)Andres Noetzli
2018-03-26Synth-check and accelerate options for sygus-rr (#1691)Andrew Reynolds
2018-03-26Abort when sygus-verify finds unsoundness. (#1717)Andrew Reynolds
2018-03-26Rewrites for substr of strings of length one (#1712)Andres Noetzli
This commit adds a rewrite for substrings of strings of length one to the empty string if it can be shown that it is not possible that the start position and the length are both greater than zero: ``` (str.substr "A" x y) --> "" if x = 0 |= 0 >= y ``` The commit introduces a set of functions to check such entailments with assumptions.
2018-03-25Cleanup various exit calls (#1692)Andrew Reynolds
2018-03-23Remove abstract regular expression constant (#1698)Andrew Reynolds
2018-03-23Remove unused code (#1700)Andrew Reynolds
2018-03-23Minor reorganization for ematching (#1701)Andrew Reynolds
2018-03-23Enable post-condition strenghtening by default for non-syntax restricted ↵Andrew Reynolds
invariant synthesis (#1703)
2018-03-21More rewrites for indexof (#1648)Andrew Reynolds
2018-03-21Fix for string disequality processing (#1679)Andrew Reynolds
2018-03-20Add support for CaDiCaL as eager BV SAT solver. (#1675)Mathias Preiner
2018-03-20Minor refactor datatypes sygus (#1673)Andrew Reynolds
2018-03-20Internally remove redundant assertions and infer equalities in ↵Andrew Reynolds
NonLinearExtension (#1633)
2018-03-20Minor fix and addition to sygus sampler (#1678)Andrew Reynolds
2018-03-19Enable CEGQI for non-linear (#1674)Andrew Reynolds
2018-03-19Document inferences for strings (#1642)Andrew Reynolds
2018-03-09Some minor cleanup in bv::utils. (#1663)Aina Niemetz
2018-03-08Fix Travis for unit test compilation errors. (#1651)Mathias Preiner
make units does not fail if we have compile error for a unit test, however, make check does. -Wsuggest-override is now explicitly disabled for unit tests since CxxTest does not add override keywords to the generated source code and thus get a lot of compiler warnings. Further, this fixes some issues introduced with #1647 due to make units not failing on Travis and fixes the nightly builds.
2018-03-06Make statistics output consistent. (#1647)Mathias Preiner
* Fixes --hide-zero-stats (and really skips the 0 values) * Removes the additional newline after each statistic * Introduces theory::getStatsPrefix(TheoryId) to generate consistent prefixes for statistics based on the theory id (e.g., THEORY_BV -> "theory::bv").
2018-03-06Simplify initialization of quantifiers engine (#1641)Andrew Reynolds
2018-03-06Refactor symmetry breaking in datatypes sygus (#1640)Andrew Reynolds
2018-03-05Update semantics for string indexof and replace (#1630)Andrew Reynolds
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
Adds missing override keywords.
2018-03-05Fix for sampler. (#1639)Andrew Reynolds
2018-03-02Optimization for sygus streaming mode (#1636)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback