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)

Reorder NodeValue class according to our code style guidelines. (#3374)

Avoid printing success for `--force-logic` (#3363)

CVC4 was printing success when `--force-logic` was used because
internally, `--force-logic` generates a `SetBenchmarkLogicCommand`. This
caused issues with the SMT-COMP trace executor. This commit fixes the
behavior by muting the command if it was not issued by the user.

The issue was likely introduced with #3062.

cmake: Fix include of CVC4JavaTargets.cmake. (#3373)

Only include Java targets if Java bindings are enabled.

New C++ API: Term: Add missing checks for null. (#3364)

Co-Authored-By: Andres Noetzli <andres.noetzli@gmail.com>

Limit cases of sygus inference based on type (#3370)

This makes `--sygus-inference` a no-op for inputs where there is a free function whose sort cannot be handled in a sygus grammar.

It also fixes an issue where skolem variables were not being treated as functions-to-synthesize.

Fixes #3250 and fixes #3356.

Fix method for getting arithmetic function definition body (#3371)

prefer prefix ++ operator for iterators

Detected with cppcheck static analyser, which said: (performance) Prefer
prefix ++/-- operators for non-primitive types. Reformat with clang-format
as needed.

Signed-off-by: Piotr Trojanek <piotr.trojanek@gmail.com>

pass parameters by reference where it affects performance

Detected with cppcheck static analyser, which said: (performance) Function
parameter should be passed by reference. Reformat with clang-format as
needed.

Signed-off-by: Piotr Trojanek <piotr.trojanek@gmail.com>

[CVC Parser] Add support for regular expressions (#3346)

Disallow --proof and --incremental (#3332)

Make ackermannization generally applicable rather than just BV (#3315)

The ackermannization process is currently already support general theories rather than specifically for BV. In this pull request, an option has been added to turn on ackermannization independently.

Build system: Add build type for incremental competition builds. (#3365)

Previously, competition builds for incremental tracks required to
manually pass in -DCVC4_SMTCOMP_APPLICATION_TRACK as compiler flag. This
introduces an additional build type for incremental competition builds
to simplify configuration for such builds.

New C++ API: Add Term::getId(). (#3360)

+ use explicit types in NodeValue
+ add unit test for Term::isParameterized()

Co-Authored-By: makaimann <makaim@stanford.edu>

[SMT2 Parser] Move code of `rewriterulesCommand` (#3334)

This commit moves the code in `rewriterulesCommand` in the SMT2 parser
to the `Smt2` class. Additionally, it creates a `boundVarList` rule to
reduce code duplication.

Fix typo in regression (#3359)

Fix str to int reduction (#3358)

This fixes a corner case of the str-to-int reduction for the case where the argument is the empty string.

This fixes #3357.

Avoid duplicate lemmas in datatypes (#3310)

We previously were sending e.g. dt.size >= 0 lemmas when size terms are pre-registered, which can happen multiple times in a user context. This ensures we cache whether a lemma is sent in a user-context dependent way in the datatypes solver. This ensures we don't send the same lemma twice for dt.size >= 0 lemmas.

Disable proofs for unsupported logics (#3327)

This commit makes CVC4 complain if the user asked for proofs for an unsupported logic (in this contest, ALL is considered unsupported).
Changes in the regression script are introduced as well, in order to only request proofs for regressions in supported logics.

Travis: Reenable building and running of examples. (#3351)

Add missing type definitions to CDHashMap iterator (#3330)

Our `CDMapBlack` test failed to compile with newer versions of libstdc++
because they require the `value_type` to be defined for the iterator
(accessed via `std::iterator_traits`). Due to the implementation of
`std::iterator_traits`, we also need to define `iterator_category`,
`difference_type`, `pointer`, and `reference`.

[SMT2 Parser] Move code of `sygusCommand` (#3335)

This commit moves the code in `sygusCommand` in the SMT2 parser to the
`Smt2` class. The original code was pushing and popping the current
scope inline. This commit adds a class `SynthFunFactory` that takes care
of that upon creation and destruction.

Fix compiler warning. (#3348)

[SMT-COMP] Remove --unconstrained-simp for incremental QF_LIA (#3333)

Fixes #3058. Commit a7c4cd3ecacb1e484a076edde0274c282bb43ffb changed
CVC4's behavior to emit an error when `--unconstrained-simp` is used
with `--incremental`. Before, we were silently disabling it. For some
reason, we had that option enabled for the incremental QF_LIA track of
SMT-COMP, so CVC4 failed on those benchmarks. This commit changes the
corresponding competition script to not use the option.

Trivial solve method for single invocation sygus (#3328)

This short circuits CEGQI when the conjecture is solvable by simple equality reasoning. It adds two examples where we previously would have fallen back on enumeration due to not having an instantiation technique for strings, despite the conjectures being trivially solvable.

Add rewrite for splitting equalities (#2957)

Add help for sygus 2.0 (#3318)

Avoid cases of empty sygus grammars (#3301)

Fail single invocation techniques when utility inference fails. (#3322)

Introduce template classes for simple type rules (#2835)

This commit introduces two template classes `SimpleTypeRule` and
`SimpleTypeRuleVar` to help define simple type rules without writing
lots of redundant code. The main advantages of this approach are:

- Less code
- More consistent error reporting
- Easier to extend type checking with other functionality (e.g. getting
the type of a symbol)

Support smt2 language "match" term  (#3258)

Fix case of disjunctive conclusion in strings (#3254)

Make substitution index context-independent (#2474)

When we do solving in incremental mode, we store substitutions at a
special index in our list of assertions. Previously, we used a
context-dependent variable for that. However, this is not needed since
the list of assertions just consists of the assertions currently being
processed, which are independent of the assertions seen so far. This
commit changes the index to be an ordinary integer and moves it to the
AssertionPipeline. Additionally, it abstracts access to the index in
preparation for splitting AssertionPipeline into three vectors (see
issue #2473).

CVC print support for recoverable failure (#3323)

 Fix off by one error in strings flat form explanation (#3273)

Fixes #3272.

This was caused by not explaining the last equal component in a flat form inference.  For example, if `x=y`, we may infer `z=""` from `u++x++z=u++y` since the 1st and 2nd components of these strings are equal. However, we would not add the explanation of `x=y` due to an off-by-one error.

Notice that this code is very rarely used (the code for F_EndpointEmp is not covered by our regressions). This is since length elaboration should catch conflicting cases like above, where `len(u++x++z)!=len(u++y)` if `x=y` and `z!=""` and thus `u++x++z != u++y`.  #3272 happened to catch a rare case where it is applied. This is likely due to theory combination not propagating an equality prior to running a full effort call to strings check, which is unexpected but not impossible.

Add isParameterized function to Expr (#3303)