summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-11-18Fix reduction of `sqrt` (#3478)Andres Noetzli
2019-11-18Add a few comments to ProofManager (#3477)Alex Ozdemir
2019-11-18Signature documentation update (#3476)Alex Ozdemir
This comment was slightly out-of-date.
2019-11-18Use -Wimplicit-fallthrough (#3464)Andres Noetzli
This commit enables compiler warnings for implicit fallthroughs in switch statements that are not explicitly marked as such. The commit introduces a new macro `CVC4_FALLTHROUGH` that can be used to indicate that a fallthrough is intentional. The commit fixes existing warnings and a bug in the arithmetic rewriter for `abs` (the bug likely couldn't be triggered easily because we rewrite `abs` to an `ite` while expanding definitions). To have the new macro also available in the parser, the commit changes `src/base/check.h` to be visible to the parser (it includes `cvc4_private_library.h` now instead of `cvc4_private.h`).
2019-11-18Use standard sygus interface for abduction and rewrite rule synthesis (#3471)Andrew Reynolds
2019-11-18Improve interface for sygus datatype, fix utilities (#3473)Andrew Reynolds
2019-11-17Updates to the unit tests, api, and examples for datatypes (#3459)Andrew Reynolds
* Updates to the unit tests, api, and examples for datatypes * Format
2019-11-16Add support for ThreadSanitizer instrumentation (#3467)Andres Noetzli
This commit adds support for compiling CVC4 with ThreadSanitizer instrumentation. This is useful for debugging issues when CVC4 is used in a multi-threaded context (e.g. #3292).
2019-11-15Use standard interface for sygus default grammar construction (#3466)Andrew Reynolds
2019-11-15Introduce SyGuS datatype API (#3465)Andrew Reynolds
2019-11-15Fix wrong kind in sygus version 1 parser (#3463)Andrew Reynolds
2019-11-14Use Shebang in cxxtestgen when appropriate (#3458)Alex Ozdemir
CxxTest's generator has one of three names, depending on the CxxTest version: * `cxxtestgen.py`, a python program * `cxxtestgen`, some kind of program with a shebang * `cxxtestgen.pl`, a perl program We were mistakenly assuming that the `cxxtestgen` form was always a python program. Now, if we find that form on the system, we assume that it is has a shebang, and is executable.
2019-11-13Allow (set-logic ...) after (reset) (#3457)Andres Noetzli
Fixes #3353. #3062 introduced a flag that tracks whether we have seen a `(set-logic ...)` command to improve the handling of `--force-logic`. However, the flag was not set to `false` when `(reset)` was called. This commit fixes the issue.
2019-11-13Distinguish unknown status for model printing (#3454)Andrew Reynolds
2019-11-12Refactor non-linear extension for model-based refinement (#3452)Andrew Reynolds
* Refactor non-linear extension for model-based refinement * Format * Minor * Address
2019-11-11Add missing utilities for Node-level Datatype API (#3451)Andrew Reynolds
2019-11-11Fix mkConst<RoundingMode>() for Python bindings (#3447)Andres Noetzli
2019-11-11Update README according to the new website (#3438)yoni206
2019-11-11Eliminate remaining references to type/expr in datatype type rules. (#3450)Andrew Reynolds
2019-11-10Fix bugs related to sygus higher-order + recursive functions (#3448)Andrew Reynolds
2019-11-09Fixes in relations related to datatypes not passed by reference (#3449)Andrew Reynolds
The current code is creating/destroying datatypes unnecessarily.
2019-11-08cmake: Disable C++ GNU extensions. (#3446)Mathias Preiner
Fixes #971.
2019-11-06Move more string utility functions (#3398)Andrew Reynolds
This is work towards splitting a "core solver" object from TheoryStrings. This moves global functions from TheoryStrings to InferenceManager/SolverState, making them accessible in the future by modules that have references to these objects. It also corrects an issue where we were maintaining two `d_conflict` fields.
2019-11-06Migrate more datatype methods to the Node level (#3443)Andrew Reynolds
This adds node-level interfaces for a few missing functions that will be necessary to have a Node-level API for datatypes.
2019-11-06[Regressions] Remove leading whitespace in output (#3444)Andres Noetzli
2019-11-06Support for SyGuS PBE + recursive functions (#3433)Andrew Reynolds
2019-11-05Remove casts to subclasses of Type in API (#3420)Andres Noetzli
2019-11-05Separate model object in non-linear extension (#3426)Andrew Reynolds
2019-11-05Refactor type matcher utility (#3439)Andrew Reynolds
2019-11-04[Regressions] Support for running w/ default args (#3436)Andres Noetzli
2019-11-04Make check synth solution robust to auxiliary assertions (#3432)Andrew Reynolds
2019-11-04Fix ho extensionality in collect model info (#3435)Andrew Reynolds
2019-11-04Avoid non-well-founded sygus grammars (#3434)Andrew Reynolds
2019-11-04Make getSynthSolution return a Bool (#3306)Andrew Reynolds
2019-11-04Eliminate deprecated utility function from sygus (#3431)Andrew Reynolds
2019-11-01Fix non-termination in datatype type enumerator (#3369)Andrew Reynolds
2019-11-01Fix and refactor TheoryStrings::checkFlatForms() (#3326)Andres Noetzli
This commit fixes some minor (performance) issues in `TheoryStrings::checkFlatForms()`: The `inelig` vector was initialized with copies of the `start` element instead of all the elements before `start` and the `else` branch of `count == asize` was looping over all elements from `1` instead of `start + 1`. Additionally, this commit refactors the code to be a bit more readable.
2019-11-01Eagerly beta reduce during sygus to builtin term conversion (#3418)Andrew Reynolds
2019-10-31Rename datatypes sygus solver (#3417)Andrew Reynolds
2019-10-31Fix Unimplemented() macros missed in #3366. (#3424)Mathias Preiner
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-10-29Split some generic utilities from the non-linear extension (#3419)Andrew Reynolds
* Split arith util * Cleaner * cpp * Format * Minor
2019-10-28Fix for non-linear models (#3410)Andrew Reynolds
* Towards fix for non-linear models * Format * Fix * More * Improve * Format * More
2019-10-28Fix integer division rewrite (#3415)Andres Noetzli
2019-10-27Fix collect model info for higher-order (#3409)Andrew Reynolds
This ensures we add lemmas when collect model info fails for the higher order extension of UF. This fixes #3405 (that benchmark now answers unknown).
2019-10-27Fix global-declarations support (#3403)Andres Noetzli
2019-10-23Fixes for SyGuS + regular expressions (#3313)Andrew Reynolds
This commit fixes numerous issues involving the combination of SyGuS and regular expressions. Combining SyGuS and regular expressions may involve constructing regular expressions that are neither variables nor builtin regular expression operators. The code was not robust for this case, either throwing spurious assertion failures or having incorrect behavior.
2019-10-22Refactoring skolems for sets (#3381)Andrew Reynolds
This refactors skolems introduced in the theory of sets. This is analogous to how skolems are treated for the theory of strings. A key change that this commit enables is to identify "variable" sets based on those that weren't introduced by the SkolemCache (instead of via a check that their kind is `VARIABLE`, which is done currently and is error prone).
2019-10-22NodeValue: Eliminate redundant NBITS macros. (#3400)Aina Niemetz
Previously, the metakind header defined macros for the number of bits reserved for fields in the NodeValue "header" (for the reference count, the node kind, the number of children and the node id). These macros were redundant, since the only one using them was the NodeValue itself, which redefined them (while using them) as constants in the class. Additionally, MAX_CHILDREN was defined (using these macros) not only in the metakind header, but redefined in other places. This commit defines the above values as constexpr members of the NodeValue class and cleans up redundancy.
2019-10-20Cleaning-up the declaration of wrapped functions/methods, which have no ↵Andrew V. Jones
definitions (#3399) Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback