Support ackermannization on uninterpreted sorts in BV (#3372)

Support ackermannization on uninterpreted sorts in BV. For uninterpreted sorts, we create a bit-vector sort to replace it. For an uninterpreted sort `S`, if the number of variables within sort `S` is `n`, the replacing bit-vector will have size (log n)+1.

Move Datatype management to ExprManager (#3568)

This is further work towards decoupling the Expr layer from the Node layer.

This commit makes it so that ExprManager does memory management for Datatype while NodeManager maintains a list of DType.

As a reminder, the ownership policy (and level of indirection through DatatypeIndex) is necessary due to not being able to store Datatype within Node since this leads to circular dependencies in the Node AST.

Fix evaluator for non-evaluatable nodes (#3575)

This ensures that the Evaluator always returns the result of substitution + rewriting for constant substitutions.

This requires a few further extensions to the code, namely:
(1) Applying substutitions to operators,
(2) Reconstructing all nodes that fail to evaluate by taking into account evaluation of their children.

Revert evaluate as node. (#3574)

Trace tags for dumping the decision tree in org-mode format (#2871)

This would add tracing options to print the decision tree in [org-mode](https://orgmode.org/) format which can be viewed with emacs or [vim-orgmode](https://github.com/jceb/vim-orgmode).

In the raw format, the number of asterisks denote the decision level of a decision, and within a propagation node, the number of spaces denote the level. Most viewers render the asterisks as indented bullets.

There are some options for controlling verbosity:
`dtview` - prints the decisions (basic option)
`dtview::command` - also prints smt-lib commands as they're issued
`dtview::conflict` - also prints conflicts
`dtview::prop` - also prints propagations

Example usage:
`cvc4 -t dtview -t dtview::command -t dtview::conflict -t dtview::prop <example smt2 file> &> example-trace.org`

The resulting file when opened with an org-mode viewer has collapsible nodes, where "..." marks a node with children.

Minor improvement to evaluator (#3570)

Fixes a bug where we don't return the partially evaluated version (for unevaluatable nodes). Also adds `NONLINEAR_MULT` whose semantics is identical to `MULT`.

Simple optimizations for the core rewriter (#3569)

In some SyGuS applications, the bottleneck is the rewriter.  This PR makes a few simple optimizations to the core rewriter, namely:
(1) Minimize the overhead of `theoryOf` calls, which take about 10-15% of the runtime in the rewriter.  This PR avoids many calls to `theoryOf` by the observation that nodes with zero children never rewrite, hence we can return the node itself immediately.  Furthermore, the `theoryOf` call can be simplified to hardcode the context under which we were using it: get the theory (based on type) where due to the above, we can assume that the node is not a variable.
The one (negligible) change in behavior due to this change is that nodes with more than one child for which `isConst` returns true (this is limited to the case of `APPLY_CONSTRUCTOR` in datatypes) lookup their theory based on the Kind, not their type, which should always be the same theory unless a theory had a way of constructing constant nodes of a type belonging to another theory.
(2) Remove deprecated infrastrastructure for a "neverIsConst" function, which was adding about a 1% of the runtime for some SyGuS benchmarks.

This makes SyGuS for some sets of benchmarks roughly 3% faster.

Eliminate Expr-level calls in TypeNode (#3562)

Add support for set comprehension (#3312)

Disable check-synth-sol in regression with recursive functions (#3560)

 FP converter: convert: Use std::vector as instead of std::stack. (#3563)

The word-blasting function `FpConverter::convert` used a `std::stack` with `deque` as an underlying data structure (default) for node traversal. Previous experiments suggested that using `std::stack<T, std::deque<T>>` performs worse than using `std::vector<T>`, and we decided, as a guideline, to always use `std::vector` for stacks: https://github.com/CVC4/CVC4/wiki/Code-Style-Guidelines#stack.

This PR refactors `FpConverter::convert` to use `std::vector`. Runs on all incremental and non-incremental FP logics in SMT-LIB showed a slight improvement over the previous (`std::stack<T, std::deque<T>>`) implementation, and an even greater (albeit still slight) improvement over using `std::stack<T, std::vector<T>>`.

Make CEGIS sampling robust to non-vanilla CEGIS (#3559)

Fix Unif+PI algorithm with symbolic unfolding (#3558)

Use the node-level datatypes API (#3556)

Fixes for regressions (#3557)

Fix CEGIS refinement for recursive functions evaluation (#3555)

Activate node-level datatype API (#3540)

Do not substitute beneath arithmetic terms in the non-linear solver (#3324)

Support symbolic unfolding in UNIF+PI (#3553)

Incorporate rewriting on demand in the evaluator (#3549)

Fix ufho issues (#3551)

Allow unsat cores with sygus inference (#3550)

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)