| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-08-16 | Merge branch 'master' into moveKindedmoveKinded | Andrew Reynolds | |
| 2018-08-15 | Removing attribute cleanups. (#2300) | Tim King | |
| * Removing attribute cleanups. | |||
| 2018-08-15 | remove kinded from node_algorithm | Andres Noetzli | |
| 2018-08-15 | Add missing files, update comments | Andres Noetzli | |
| 2018-08-15 | Move node algorithms | Andres Noetzli | |
| 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-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 | 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-03 | Eliminate option for sygus UF evaluation functions (#2262) | Andrew Reynolds | |
| 2018-08-01 | Fix API call for reg exp. (#2248) | Andrew Reynolds | |
| 2018-08-01 | Fix issues with printing parametric datatypes in smt2 (#2213) | Andrew Reynolds | |
| 2018-07-27 | Fix Node::hasFreeVar for function variables (#2216) | Andrew Reynolds | |
| A Node has free variables if its operator has free variables. | |||
| 2018-07-21 | Optimizations and fixes for computing whether a type is finite (#2179) | Andrew Reynolds | |
| 2018-07-14 | exportTo only if needed for --sygus-rr-synth-check (#2168) | Andres Noetzli | |
| 2018-07-13 | New C++ API: Implementation of datatype classes. (#2142) | Aina Niemetz | |
| 2018-06-28 | Do not rename uninterpreted constants (#2098) | Andrew Reynolds | |
| 2018-06-25 | Updated copyright headers. | Aina Niemetz | |
| 2018-05-28 | Builtin evaluation functions for sygus (#1991) | Andrew Reynolds | |
| 2018-05-24 | Fix compiler warnings (#1959) | Andres Noetzli | |
| 2018-05-18 | Cache isInterpretedFinite (#1943) | Andrew Reynolds | |
| 2018-05-10 | Exclude Boolean connectives from ITE conditions in SygusUnifStrat (#1900) | Andrew Reynolds | |
| 2018-04-10 | Properly implement function extensionality based on cardinality (#1765) | Andrew Reynolds | |
| 2018-04-09 | Fix hasSubterm calls for higher-order (#1760) | Andrew Reynolds | |
| 2018-04-08 | Check free variables in assertions (#1737) | Andrew Reynolds | |
| 2018-04-02 | Do not call toString() on malformed node when throwing ↵ | yoni206 | |
| TypeCheckingExceptionPrivate. (#1733) While throwing a TypeCheckingExceptionPrivate, an IllegalArgumentException was thrown when trying calling toString() on a malformed node. Fixed by printing the kind of the node and its children rather than calling toString() on the malformed node. | |||
| 2018-03-23 | Remove abstract regular expression constant (#1698) | Andrew Reynolds | |
| 2018-03-06 | Make 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-05 | Enable -Wsuggest-override by default. (#1643) | Mathias Preiner | |
| Adds missing override keywords. | |||
| 2018-03-05 | Add support for check-sat-assuming. (#1637) | Aina Niemetz | |
| This adds support for check-sat-assuming. It further adds support for SmtEngine::query() over a vector of Expressions, e.g., smtEngine->query({a, b}); checks the validity (of the current input formula) under assumption (not (or a b)). | |||
| 2018-03-05 | Add CVC4_PUBLIC keyword to overloads of << for Expr containers. (#1644) | Aina Niemetz | |
| 2018-03-05 | Add uniform way to serialize containers of Expr to stream. (#1638) | Aina Niemetz | |
| 2018-03-02 | Fixed typo. | Aina Niemetz | |
| 2018-02-13 | Provide a uniform way to serialize node containers to output stream. (#1604) | Aina Niemetz | |
| 2018-02-07 | Fixing line numbers on type_checker_template.cpp (#1574) | Tim King | |
| 2018-02-05 | Using getOperator() directly instead of using -1. CID 1172262. (#1559) | Tim King | |
| 2018-01-27 | Removing an unused variable. Resolves CID 1172257. (#1542) | Tim King | |
| 2018-01-26 | Removing structurally dead code. (#1540) | Tim King | |
| 2018-01-17 | Removes yet more throw specifiers. Updating the documentation as needed. (#1518) | Tim King | |
| 2018-01-14 | Removing throw specifiers from Type. (#1511) | Tim King | |
| 2018-01-10 | Removing throw specifiers for TypeRules. (#1501) | Tim King | |
| 2018-01-09 | Cleaning up throw specifiers on Exception and subclasses. (#1475) | Tim King | |
| 2018-01-09 | Removing throw specifiers from miscellaneous src/expr/ classes. (#1503) | Tim King | |
| 2018-01-08 | Remove throw specifiers from symbol table. (#1490) | Tim King | |
| 2018-01-08 | Remove throw specifiers from datatype. (#1489) | Tim King | |
| 2018-01-04 | Removing miscellaneous throw specifiers. (#1474) | Tim King | |
| 2017-12-10 | Fix issue with mkConst/getConst of TypeConstant (#1439) | Andres Noetzli | |
| When compiling the Java bindings on macOS, the linker complained about CVC4::ExprManager::mkConst<CVC4::TypeConstant>() and CVC4::Expr::getConst<CVC4::TypeConstant>() being undefined. After some research, I found that the issue has been introduced by commit 36bf9f8bcb2a1a3aea1f90eb4d13aed3bbf6da8f. It looks like adding the -no-undefined flags resulted in the symbols in question being omitted due to TypeConstant not being exported. This commit makes TypeConstant CVC4_PUBLIC, which fixes the issue. | |||
| 2017-12-01 | Minor additions for sygus (#1419) | Andrew Reynolds | |
| 2017-11-22 | Converting defined functions and let expressions from Sygus grammars to ↵ | Haniel Barbosa | |
| lambdas (#1403) This partially solves issue #1344. Definitions are expanded when the grammar normalizer is called. When this becomes default then the code that expands definitions elsewhere will be removed. The PR also contains minor changes to the PrintCallback and SygusGrammarNormalize module. | |||
| 2017-11-22 | Sygus Lambda Grammars (#1390) | Andrew Reynolds | |
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback