Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-08-26 | Use uniform length limit for String constantsfixNightlies | Andres Noetzli | |
This commit changes the code in the strings solver to use the String::maxSize() length limit everywhere instead of having multiple constants defined in different places. This fixes an issue in our nightlies where we were trying to rewrite an indexof operation with a start index greater than the maximum value of a 32-bit integer. The rewriter was checking for a start index greater than the maximum of a 64-bit integer before trying to convert the Rational into a 32-bit number, which failed with CLN. This commit fixes the check. | |||
2018-08-26 | Fix unsigned integer type issues in strings (#2380) | Andrew Reynolds | |
* Fix unsigned integer types in strings. * Format | |||
2018-08-25 | Refactor unconstrained simplification pass (#2374) | Andres Noetzli | |
2018-08-25 | Refactor quantifier macros preprocessing pass (#1840) | yoni206 | |
Moved `src/theory/quantifiers/macros.{cpp,h}` to `src/preprocessing/passes/quantifier_macros.{cpp,h}`, and added the necessary methods for inheritance from PreprocessingPass. No need to add a test - regress0 fails when adding Assert(false) when assertions had changed. | |||
2018-08-24 | Refactor nlExtPurify preprocessing pass (#1963) | Haniel Barbosa | |
2018-08-24 | Clean up quantifiers engine initialization. (#2371) | Andrew Reynolds | |
2018-08-24 | Fix more simple coverity warnings (#2372) | Andrew Reynolds | |
2018-08-24 | Remove spurious disabling of cbqi-all (#2368) | Andrew Reynolds | |
2018-08-24 | Add tests that enumerate and verify rewrite rules (#2344) | Andres Noetzli | |
2018-08-23 | Do not print internally generated datatypes in external outputs with sygus ↵ | Andrew Reynolds | |
(#2234) | |||
2018-08-23 | New C++ API: Add checks for kind arguments. (#2369) | Aina Niemetz | |
This should hopefully also take care of the open coverity issues for cvc4cpp.cpp. | |||
2018-08-23 | Add missing overrides in unit tests (#2362) | Andres Noetzli | |
2018-08-23 | Replacing allocatedInCMM and d_noTrash with false everywhere in cdhashmap ↵ | Tim King | |
(#2355) There do not appear to be any instances these can be positive. | |||
2018-08-23 | Makes the filename be set in the SMT engine by default (#2366) | Haniel Barbosa | |
2018-08-23 | Fixing some coverity warnings (#2357) | Andrew Reynolds | |
2018-08-23 | Fix regression requiring proof build. (#2364) | Andrew Reynolds | |
2018-08-23 | Refactor ITE simplification preprocessing pass. (#2360) | Aina Niemetz | |
2018-08-23 | Use "filename" instead of "name" in SmtEngine::setInfo() (#2361) | Andres Noetzli | |
2018-08-22 | global-negate preprocessing pass (#2317) | yoni206 | |
2018-08-22 | More regressions that increase coverage (#2354) | Andrew Reynolds | |
2018-08-22 | More unused code elimination (#2358) | Andrew Reynolds | |
2018-08-22 | Generating less consistency lemmas in bv-ackermann preprocessing pass (#2253) | yoni206 | |
2018-08-22 | Wrapping TheorySetsPrivate in a unique_ptr. (#2356) | Tim King | |
2018-08-22 | Fix option for real2int regression. (#2353) | Andrew Reynolds | |
2018-08-22 | Adds regression test for automatic generation of SyGuS BV grammars (#2345) | Haniel Barbosa | |
2018-08-22 | Fix invalid iterator comparisons (#2349) | Andrew Reynolds | |
2018-08-21 | Fix processing of nested Variable construct in sygus let bodies (#2351) | Andrew Reynolds | |
2018-08-21 | Removing unused bool members in command.cpp. Also initializes a bool member. ↵ | Tim King | |
(#2321) | |||
2018-08-21 | Warn and enable quantifiers when using sygus + logics with QF (#2352) | Andrew Reynolds | |
2018-08-21 | Makes the new row propagation system default (#2335) | Haniel Barbosa | |
2018-08-21 | Move d_realAssertionsEnd from SmtEnginePrivate to AssertionPipeline. (#2350) | Mathias Preiner | |
2018-08-21 | Add constexpr annotations to help coverity understand constant ... (#2314) | Tim King | |
2018-08-21 | Use cbqi-full for sygus (#2346) | Andrew Reynolds | |
2018-08-20 | Remove support for *.expect files in regressions (#2341) | Andres Noetzli | |
Currently, we can optionally specify an *.expect file with the metadata of a regression test. This commit removes that option because it was not widely used, adds maintenance overhead and makes the transition to a new build system more cumbersome. Regression files can still be fed to a solver without removing the metadata first since they are in comments of the corresponding input format (note that this was not always the case, it changed in efc6163629c6c5de446eccfe81777c93829995d5). | |||
2018-08-20 | Fix initialization of d_smt in ValidityChecker for changes from #2240. (#2343) | Aina Niemetz | |
2018-08-20 | Remove disabled system test cvc3_george. (#2342) | Aina Niemetz | |
Disabled since 6 years, @mdeters commented when disabling it that it takes a very long time to build, see 868ee6d. | |||
2018-08-20 | More unused code elimination (#2339) | Andrew Reynolds | |
2018-08-20 | Remove support for prototype (non-sygus) synthesis (#2338) | Andrew Reynolds | |
2018-08-20 | Add regressions that increase coverage (#2337) | Andrew Reynolds | |
2018-08-20 | Minor improvements to the interface for sygus sampler (#2326) | Andrew Reynolds | |
2018-08-20 | Make sygus inference a preprocessing pass (#2334) | Andrew Reynolds | |
2018-08-18 | run-regress script: Exit with exit code > 0 on failure. (#2336) | Aina Niemetz | |
This is in preparation for migration to cmake since ctest determines failure via exit code. | |||
2018-08-17 | Remove support for flipDecision (#2319) | Andrew Reynolds | |
2018-08-17 | Remove miscellaneous unused code (#2333) | Andrew Reynolds | |
2018-08-17 | Add sygus stream regressions (#2330) | Andrew Reynolds | |
2018-08-17 | Split sygus grammar to its own ANTLR grammar (#2307) | Andrew Reynolds | |
2018-08-17 | Fix spurious warning in sort inference (#2331) | Andrew Reynolds | |
2018-08-17 | Fix arithmetic division by zero in sygus repair constant module (#2329) | Andrew Reynolds | |
2018-08-17 | Eliminate partial operators in sygus grammar normalization (#2323) | Andrew Reynolds | |
This corrects a bug that was introduced in #2266 (the hack removed there was necessary). This ensures that we handle operators like bvudiv, bvsdiv, bvurem, div, rem, / properly in sygus. This also enables total semantics for BV div-by-zero for sygus. | |||
2018-08-16 | Initialize inputAssertions only when proofRecipe is non-null (#2325) | Tim King | |
Most of the PR is clang-format cruft from picking up the contents of a PROOF({ ... }); |