New grammar construction modes for SyGuS (#3486)

Fix (#3530)

Fixes for SyGuS PBE + templated string concatenations + datatypes (#3492)

Fix single invocation solution construction for multiple function case (#3516)

Fix corner case in model construction of strings (#3524)

This commit fixes a corner case in the model construction of strings:
For a given length, we were assuming that for each equivalence class, we
could always find an initial guess for a constant to assign to it. This
was not always true, however, because a preceding equivalence class
could use up all constants and get assigned the last remaining one, so
we wouldn't have a constant remaining for the current class. This
resulted in an assertion failure (in debug) or a crash (in production).
This commit fixes the issue by checking whether we've run out of
constants before assigning an initial constant for an equivalence class.

Improve flexibility of lemma output in non-linear solver (#3518)

Fix clang-format file for brace wrapping with case labels. (#3523)

More recent clang version introduce an extra flag AfterCaseLabel for brace wrapping after case labels. Default is false, with the effect opening braces after case labels will be aligned on the same line as the label. Our style requires it to be set to true.

Rewrite `str.contains` used for character matching (#3519)

Add isNullHelper to avoid calling API function isNull with CVC4_API_CHECK_NOT_NULL (#3520)

Minor refactor: rename opterm_black to op_black (#3521)

[SMT2 Printer] Quote symbols starting with digit (#3517)

OpTerm Refactor: Allow retrieving OpTerm used to create Term in public C++ API (#3355)

* Treat uninterpreted functions as a child in Term iteration

* Remove unnecessary const_iterator constructor

* Add parameter comments to const_iterator constructor

* Use operator[] instead of storing a vector of Expr children

* Switch pos member variable from int to uint32_t

* Add comment about how UFs are treated in iteration

* Allow OpTerm to contain a single Kind, update OpTerm construction

* Update mkTerm to use only an OpTerm (and not also a Kind)

* Remove unnecessary function checkMkOpTerm

* Update mkOpTerm comments to not use _OP Kinds

* Update examples to use new mkTerm

* First pass on fixing unit test

* Override kind for Constructor and Selector Terms

* More fixes to unit tests

* Updates to parser

* Remove old assert (for Kind, OpTerm pattern which was removed)

* Remove *_OP kinds from public API

* Add hasOpTerm and getOpTerm methods to Term

* Add test for UF iteration

* Add unit test for getOpTerm

* Move OpTerm implementation above Term implemenation to match header file

Moved in header because Term::getOpTerm() returns an OpTerm and the compiler complains
if OpTerm is not defined earlier. Simply moving the declaration is easier/cleaner than
forward declaring within the same file that it's declared.

* Fix mkTerm in datatypes-new.cpp example

* Use helper function for creating term from Kind to avoid nested API calls

* Rename: OpTerm->Op in API

* Update OpTerm->Op in examples/tests/parser

* Add case for APPLY_TESTER

* operator term -> operator

* Update src/api/cvc4cpp.h

Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>
* Comment comment suggestion

Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>
* Add not-null checks and implement Op from a single Kind constructor

* Undo sed mistake for OpTerm replacement

* Add 'd_' prefix to member vars

* Fix comment and remove old commented-out code

* Formatting

* Revert "Formatting"

This reverts commit d1d5fc1fb71496daeba668e97cad84c213200ba9.

* More fixes for sed mistakes

* Minor formatting

* Undo changes in CVC parser

* Add isIndexed and prefix with d_

* Create helper function for isIndexed to avoid calling API functions in other API functions

 Update ownership policy for dynamic quantifiers splitting (#3493)

Fix case of higher-order + sygus inference (#3509)

Ensure quantifiers options are set with --no-strings-lazy-pp (#3515)

Prevent ref count from reaching zero in BV instantiator (#3512)

improving parsing error messages related to HOL (#3510)

Competition build: Skip parsing error regression (#3511)

Fix fast SyGuS enumeration for interpreted constants (#3501)

Check free variables in assertions when using SyGuS (#3504)

Fix sygus inference for choice functions introduced at preprocess (#3500)

Enable sygusRecFun by default and fixes SyGuS+RecFun+HO issues (#3502)

 Fix indexof range lemma (#3499)

Better front-end type checking for SyGuS (#3496)

Minor refactoring of compute model value for nl (#3489)

* Refactor compute model value for nl

* Format

fixing stupid typo (#3488)

hard limit for rec-fun eval (#3485)

Evaluation unfolding for symbolic SyGuS constructors (#3483)

Lazy evaluation via rec-funs of ITE expressions  (#3482)

Fix reduction of `sqrt` (#3478)

Add a few comments to ProofManager (#3477)

Signature documentation update (#3476)

This comment was slightly out-of-date.

Use -Wimplicit-fallthrough (#3464)

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`).

Use standard sygus interface for abduction and rewrite rule synthesis (#3471)

Improve interface for sygus datatype, fix utilities (#3473)

Updates to the unit tests, api, and examples for datatypes (#3459)

* Updates to the unit tests, api, and examples for datatypes

* Format

Add support for ThreadSanitizer instrumentation (#3467)

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).

Use standard interface for sygus default grammar construction (#3466)

Introduce SyGuS datatype API (#3465)

Fix wrong kind in sygus version 1 parser (#3463)

Use Shebang in cxxtestgen when appropriate (#3458)

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.

Allow (set-logic ...) after (reset) (#3457)

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.

Distinguish unknown status for model printing (#3454)

Refactor non-linear extension for model-based refinement (#3452)

* Refactor non-linear extension for model-based refinement

* Format

* Minor

* Address

Add missing utilities for Node-level Datatype API (#3451)

Fix mkConst<RoundingMode>() for Python bindings (#3447)

Update README according to the new website (#3438)

Eliminate remaining references to type/expr in datatype type rules. (#3450)

Fix bugs related to sygus higher-order + recursive functions (#3448)

Fixes in relations related to datatypes not passed by reference (#3449)

The current code is creating/destroying datatypes unnecessarily.

cmake: Disable C++ GNU extensions. (#3446)

Fixes #971.

Move more string utility functions (#3398)

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.

Migrate more datatype methods to the Node level (#3443)

This adds node-level interfaces for a few missing functions that will be necessary to have a Node-level API for datatypes.

[Regressions] Remove leading whitespace in output (#3444)

Support for SyGuS PBE + recursive functions (#3433)

Remove casts to subclasses of Type in API (#3420)

Separate model object in non-linear extension (#3426)

Refactor type matcher utility (#3439)

[Regressions] Support for running w/ default args (#3436)

Make check synth solution robust to auxiliary assertions (#3432)

Fix ho extensionality in collect model info (#3435)

Avoid non-well-founded sygus grammars (#3434)

Make getSynthSolution return a Bool (#3306)

Eliminate deprecated utility function from sygus (#3431)

Fix non-termination in datatype type enumerator (#3369)

Fix and refactor TheoryStrings::checkFlatForms() (#3326)

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.

Eagerly beta reduce during sygus to builtin term conversion (#3418)

Rename datatypes sygus solver (#3417)

Fix Unimplemented() macros missed in #3366. (#3424)

Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)

Split some generic utilities from the non-linear extension (#3419)

* Split arith util

* Cleaner

* cpp

* Format

* Minor

Fix for non-linear models (#3410)

* Towards fix for non-linear models

* Format

* Fix

* More

* Improve

* Format

* More

Fix integer division rewrite (#3415)

Fix collect model info for higher-order (#3409)

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).

Fix global-declarations support (#3403)

Fixes for SyGuS + regular expressions (#3313)

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.

Refactoring skolems for sets (#3381)

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).

NodeValue: Eliminate redundant NBITS macros. (#3400)

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.

Cleaning-up the declaration of wrapped functions/methods, which have no definitions (#3399)

Signed-off-by: Andrew V. Jones <andrewvaughanj@gmail.com>

Update overflow check to handle negative numbers (#3396)

 Move datatype utility functions to own file (#3397)

Solver state for theory of strings (#3181)

This refactors the theory of strings to use a solver state object, which manages state information regarding assertions.

It also deletes some unused/undefined functions in theory_strings.h.

There are no major changes to the behavior of the code or its documentation in this PR.

This is work towards #1881.

Fix line numbers in templates (#3391)

This commit updates the line numbers in templates to address warnings
due to wrong line numbers.

Remove remaining references to Boost and Autotools (#3390)

This commit removes references to Boost and Autotools in the copyright
information and CMakeLists.txt.

Fix OOB access (#3383)

In theory_engine.cpp, we were calling `theoryOf()` with
`THEORY_SAT_SOLVER` as the theory id. However, `THEORY_SAT_SOLVER` is
defined as `THEORY_LAST` and thus out-of-bounds of the `d_theoryTable`
defined in theory_engine.h (which is of size `THEORY_LAST`. This commit
adds an assertion that detects the out-of-bound access and introduces a
method to turn a theory id into a string which correctly handles
`THEORY_SAT_SOLVER`.

Fix regression (#3393)

PR #3388 didn't disable the regression correctly (due to using `REQUIRE`
instead of `REQUIRES`). This commit fixes the issue.

Disable regression test for competition build (#3388)

This commit disables a regression test that was failing for the
competition build due to not emitting the expected error message.

Remove benchmark (#3389)

Support UF in default sygus grammars (#3319)

Apply sygus repair constant techniques restricted to refinement lemmas (#3386)

Ensure lemmas from sygus repair const are guarded (#3385)

Minor refactor in strings rewriter (#3387)

Eliminate negative constant coefficients in div/mod (#2929)

Fixes #1399.

Check that logic is set when synth-fun command is encountered (#3384)

Add support for UBSan instrumentation (#3382)

This commit adds support for compiling CVC4 with UBSan instrumentation.
The commit also adds a dummy version of `AigBitblaster`. Previously,
when CVC4 was built without ABC, `AigBitblaster` was not fully defined
(the class was declared but the implementation was not being compiled).
This lead to missing RTTI information when compiling with UBSan
instrumentation.

Make order of theories explicit in the source code. (#3379)

Fixes #2517.

This makes the order of theories explicit in the source code rather than relying on the order defined via the build system. Previously, the build system ensured the order of the theories via the KINDS_FILES variable, which is a list of kinds files that is fed to code generation scripts (mkkind, mkmetakind, mkrewriter, mktheorytraits). The generated code critical to the order of theories w.r.t. soundess is the TheoryId enum, and the CVC4_FOR_EACH_THEORY macro. Ideally, we would want to get rid of the latter (ugly and error prone), which is not possible in the current configuration, and to be discussed in the future.

This PR moves the TheoryID enum and related functions to theory/theory_id.h, and the CVC4_FOR_EACH_THEORY macro to theory/theory_engine.cpp, the only place where it is used.

I ran it on whole SMT-LIB (non-incremental and incremental) and did not encounter any soundness issues. The only issue that did occur is not related to these changes, non-critical and known: #2993

Warning instead of assertion for failing propagating instance (#3380)

test: Add TS_UTILS_EXPECT_ABORT macro for unit tests. (#3378)

TS_UTILS_EXPECT_ABORT can be used if an expression in a unit test is
expected to abort() instead of throwing an exception. This can happen if
CVC4_CHECK or CVC4_DCHECK fail.

NodeValue: Use 'using' instead of 'typedef'. (#3374)

NodeValue: Use fixed width return type for getRefCount(). (#3374)