Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-08-14 | Remove unused declaration (#2310) | Andres Noetzli | |
2018-08-13 | Fix get-unsat-assumptions output (#2301) | Andres Noetzli | |
Fixes #2298. The `get-unsat-assumptions` command was printing the result with square brackets and commas instead of parentheses and spaces between the assumptions. | |||
2018-08-13 | Removing support for T* and const T* attributes. (#2297) | Tim King | |
* Removing support for T* and const T* attributes. These are unused. | |||
2018-08-11 | Make attributes robust to static init orderings (#2295) | Andres Noetzli | |
@taking pointed out that part of the issue fixed in #2293 is also that we should be more robust to different (de-)initialization orders. A common, portable way to achieve this is to allocate the object in question on the heap and make the pointer to it static [0]. This commit fixes the variable in question. I have tested this fix in ASAN (without using --no-static-init flag for CxxTest) and it works. [0] https://isocpp.org/wiki/faq/ctors#construct-on-first-use-v2 | |||
2018-08-10 | Fix portfolio command executor for changes from #2240. (#2294) | Aina Niemetz | |
2018-08-09 | Fix char overflow issues in regular expression solver (#2275) | Andrew Reynolds | |
2018-08-08 | Plug solver API object into parser. (#2240) | Aina Niemetz | |
2018-08-08 | Fixing documentation nit from PR#2232. (#2289) | Tim King | |
2018-08-08 | Proposal for adding map utility functions to CVC4. (#2232) | Tim King | |
* Proposal for adding map utility functions to CVC4. | |||
2018-08-08 | Disable argument relevance for sygus by default (#2288) | Andrew Reynolds | |
2018-08-08 | Add debug test for sygus subcall verify calls. (#2287) | Andrew Reynolds | |
2018-08-08 | Move uf model code from uf to quantifiers (#2095) | Andrew Reynolds | |
2018-08-08 | Do beta-reduction in expandDefinitions (#2286) | Andrew Reynolds | |
2018-08-07 | Require Swig 3 (#2283) | Andres Noetzli | |
Removes some hacks due to Swig 2's incomplete C++11 support and adds checks for version 3 at configuration time as well as in swig.h | |||
2018-08-07 | Simplify and improve the sygus parser (#2266) | Andrew Reynolds | |
Currently, there is code duplication for parsing constants in sygus grammars, e.g.: https://github.com/CVC4/CVC4/blob/master/src/parser/smt2/Smt2.g#L1048 https://github.com/CVC4/CVC4/blob/master/src/parser/smt2/Smt2.g#L2304 This PR removes this duplication by introducing a new ANTLR grammar "termAtomic" in Smt2.g. As a result of this PR, we now parse sygus grammars with any constant we otherwise parse. This addresses known issues where CVC4 rejects grammars with floating point constants. It also removes some unnecessary code for converting builtin kinds to their total versions. This is work towards #2197. We still do not support sygus grammars with non-trivial *composite* terms, such as applications of indexed function symbols. | |||
2018-08-07 | Document/refactor datatypes sygus simple symmetry breaking (#2233) | Andrew Reynolds | |
2018-08-07 | Fix simple reg exp consume rewrite (#2281) | Andrew Reynolds | |
2018-08-07 | Delete functions instead of using CVC4_UNDEFINED (#1794) | Andres Noetzli | |
C++11 supports explicitly deleting functions that should not be used (explictly or implictly), e.g. copy or assignment constructors. We were previously using the CVC4_UNDEFINED macro that used a compiler-specific attribute. The C++11 feature should be more portable. | |||
2018-08-07 | Wait to do sygus qe preprocess until full effort check (#2282) | Andrew Reynolds | |
2018-08-07 | Fix inference of pre and post conditions for non variable arguments. (#2237) | Andrew Reynolds | |
2018-08-07 | Make output of flushInformation and safeFlushInformation consistent. (#2280) | Mathias Preiner | |
2018-08-07 | Add rewrite for nested BITVECTOR_ITE that can be merged. (#2273) | Aina Niemetz | |
2018-08-06 | Make flat form inferences optional in strings (#2277) | Andrew Reynolds | |
2018-08-06 | Add RegLan to smt2/sygus parsers. (#2276) | Andrew Reynolds | |
2018-08-06 | Move sygus quantifier elimination step for non-ground-single-invocation to ↵ | Andrew Reynolds | |
sygus (#2269) | |||
2018-08-06 | Remove support for Enum sygus syntax. (#2264) | Andrew Reynolds | |
2018-08-06 | Fixes for sygus inference (#2238) | Andrew Reynolds | |
This includes: - Enabling sygus-specific options in SmtEngine::setDefaults, - Disabling a variant of miniscoping (triggered by many chc-comp18 benchmarks), - Treating free constants as functions to synthesize | |||
2018-08-06 | Fixes and improvements for single invocation inference (#2261) | Andrew Reynolds | |
2018-08-06 | Fix degenerate case of sygus grammar construction for 0-argument Bools (#2260) | Andrew Reynolds | |
2018-08-03 | Add rewrite for nested BITVECTOR_ITE with cond_outer == cond_inner. (#2272) | Aina Niemetz | |
2018-08-03 | Add rewrite for BITVECTOR_ITE with const children. (#2271) | Aina Niemetz | |
2018-08-03 | Add rewrite for BITVECTOR_ITE with term_then == term_else. (#2268) | Aina Niemetz | |
2018-08-03 | Eliminate option for sygus UF evaluation functions (#2262) | Andrew Reynolds | |
2018-08-03 | Fix printing statistics in case of signals. (#2267) | Mathias Preiner | |
2018-08-02 | Add timer for BV inequality solver. (#2265) | Aina Niemetz | |
2018-08-02 | Parse standard separation logic inputs (#2257) | Andrew Reynolds | |
2018-08-02 | Improve CEGQI heuristics involving equality and multiple instantiations (#2254) | Andrew Reynolds | |
2018-08-02 | Fix candidate rewrite utilities for non-first-class types (#2256) | Andrew Reynolds | |
2018-08-02 | Make strings robust to regular expression variables. (#2255) | Andrew Reynolds | |
The theory solver for strings does not support regular expression variables. With this PR, we properly throw an exception if it is given one. However, the rewriter needs to handle regular expression variables (for various reasons: rewriting an expression before its asserted, sygus explanation generalization, etc.). This corrects a few miscellaneous issues in the strings rewriter to make it sound for these cases. It also corrects a seg fault in simpleRegexpConsume when testing memberships `(str.in.re "" R)`, where R is a *non-constant* regular expression (which will now be allowed if variables are allowed). This is in preparation for adding `RegLan` as a token to the smt2/sygus parsers. | |||
2018-08-02 | Add rewrites for BITVECTOR_ITE and BITVECTOR_COMP with const ↵ | Aina Niemetz | |
condition/child. (#2259) | |||
2018-08-02 | Remove references to deprecated propagate as decision feature (#2258) | Andrew Reynolds | |
2018-08-02 | Remove Subversion build info (#2250) | Andres Noetzli | |
2018-08-01 | Fix API call for reg exp. (#2248) | Andrew Reynolds | |
2018-08-01 | Improvements and fixes in cegqi arithmetic (#2247) | Andrew Reynolds | |
This includes several improvements for cegqi with arithmetic: - Randomly choose either lower or upper bounds instead of always using lower bounds (this is similar to cegqi+BV), - Equalities are handled by processAssertions, - Resort to *only* model values at full effort instead of trying to mix model values/bounds (this is also similar to cegqi+BV), - cegqi+arithmetic does not try multiple instantiations unless the flag cbqiMultiInst is set. This makes it so that ceg_instantiator does not have exponential behavior when the strategy is non-monotonic. It also includes a core fix to computing what bound is optimal based on an ordering that incorporates virtual terms. Previously, we would consider, e.g.: `a+b*delta > c+d*delta if a>=c and b>=d` Whereas the correct check is lexicographic: `a+b*delta > c+d*delta if a>c or a=c and b>d` This means e.g. 2+(-1)*delta > 3 was previously wrongly inferred. This is part of merging https://github.com/ajreynol/CVC4/tree/cegqiSingleInst, which is +3-0 on SMTLIB BV and +12-9 on SMTLIB LIA+LRA+NRA+NIA. | |||
2018-08-01 | Remove outdated references to TLS (#2245) | Andres Noetzli | |
2018-08-01 | Fix issues with printing parametric datatypes in smt2 (#2213) | Andrew Reynolds | |
2018-08-01 | Fix wrong evaluation of STRING_STOI (#2252) | Andres Noetzli | |
2018-08-01 | Fix bool-to-bv preprocessing pass for non-{bv,bool} equalities. (#2251) | Mathias Preiner | |
2018-08-01 | InteractiveShell: Remove redundant options argument. (#2244) | Aina Niemetz | |
2018-08-01 | New C++ API: Fixed ownership of options object. (#2243) | Aina Niemetz | |