Disable sygus inference when combined with incremental and proofs (#3539)

Fix case of uninterpreted constant instantiation in FMF (#3543)

Fixes #3537.
This benchmark triggers a potential unsoundness caused by instantiating with an uninterpreted constant (which is unsound).

Make theory rewriters non-static (#3547)

This commit changes theory rewriters to be non-static. This refactoring
is needed as a stepping stone to making our rewriter configurable: If we
have multiple solver objects with different rewrite configurations, we
cannot use `static` variables for the rewriter table in the BV rewriter
for example. It is also in line with our goal of getting rid of
  singletons in general. Note that the `Rewriter` class is still a
  singleton, which will be changed in a future commit.

[Regressions] Require proof support for abduction (#3546)

Simplify rewrite for character matching (#3545)

Use str.subtr in str.to.int/int.to.str reduction (#3544)

Previously, we were using UFs to encode substrings in the
`str.to.int`/`int.to.str` reductions. Our experiments have shown,
however, that using `str.substr` is more efficient instead.

Throw exception instead of warning for approximate models (#3542)

Add lemma for str.to.int/int.to.str (#3541)

This commit adds a lemma to our encoding of `str.to.int` and
`int.to.str` that relates the integer value in the encodings to the
value of partial results.

Optimize the rewriter for DT_SYGUS_EVAL (#3529)

This makes it so that we don't construct intermediate unfoldings of applications of DT_SYGUS_EVAL, which wastes time in node construction. It makes the sygusToBuiltin utility in TermDbSygus use this implementation.

New algorithm for interpolation and abduction based on unsat cores (#3255)

Add ExprManager as argument to Datatype (#3535)

[proof] Eliminate side-condition from ER signature (#3230)

* [proof] Eliminate the side condition in er.plf

By tweaking the axioms a bit, I got rid of the lone SC in the Extended
Resolution signature.

* [proof] Changed er_proof.cpp in line with signature

The new signature requires slightly different proof printing.

* [proof] clang-format er_proof.cpp

* Fix tests

* [proof] Actually delete the SC

* Apply suggestions from code review

Co-Authored-By: yoni206 <yoni206@users.noreply.github.com>
* Add LFSC-checking unit test for ER proof

* Gate the lfsc invocation on the build system

* Properly gate the lfsc check on the build system

* gate the plf_signatures forward def on the build system

contrib: Setup all dependencies in deps/ directory. (#3534)

Introduce the Node-level Datatypes API (#3462)

This adds classes corresponding to the Node-level Datatype API "DType", which is a specification for a datatype type. It does not enable the use of this layer yet. A followup PR will update the Expr-level Datatype to use the Node-level code, which is currently verified to be functional on this branch: https://github.com/ajreynol/CVC4/tree/dtype-integrate. Futher PRs will make the internal (Node-level) code forgo the use of the Expr-layer datatype, which will then enable the Expr-layer to be replaced by the Term-layer datatype.

Most of the documentation for the methods in DType/DTypeConstructor/DTypeSelector was copied from Datatype/DatatypeConstructor/DatatypeConstructorArg.

Make nonlinear solver intercept model assignments from the linear arithmetic solver (#3525)

Refactor mode options for Unif+PI (#3531)

Bi-directional unrolling of R* regular expressions (#3532)

Add mkOp for a single Kind (#3522)

Fix the subtyping relation for functions (#3494)

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)