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)

Use separate CMake project for CVC4 examples. (#3196)

Add Windows cross-compiling instructions to INSTALL.md. (#3226)

Fix printing of instantiation patterns (#3305)

Return choice functions for approximate values in get-value (#3304)

Support context-(in)dependent decision strategies. (#3281)

Add support for creating constant arrays to the new C++ API (#3296)

* Add support for constant arrays to new C++ API

* Fix macro usage in unit test

* Add not null check

* Add test for null term

* Formatting

Decouple fmf-bound and finite-model-find (#3297)

Add run script for next SMT-COMP (#3298)

Minor cleaning (#3295)

 Encapsulate relevant domain (#3293)

Avoid computing cardinality when constructing models (#3268)

Remove parameterized check (#3290)

Fix spurious meta-info in regression (#3294)

Remove equality inference option for quantifiers (#3282)

Move specific attributes out of term util (#3279)

Sygus type info class (#3187)

 Fix HO model construction for functions having Boolean arguments (#3158)

Move virtual term substitution utilities to own file and document (#3278)

Return RecoverableModalException when model is not available. (#3283)

Fix compiler warning in options.cpp. (#3284)

Adding new scripts for CASC/TPTP (#3291)

Initialize fields in sets inference manager (#3289)

parser: Improve error message for unrecognized input file format. (#3285)

Disallow let in sygus grammars, check for free variables in sygus constructors (#3259)

Move higher-order matching predicate (#3280)

Split, refactor and document the theory of sets (#3085)

 Rename UF with cardinality extension (#3241)

Update to standard implementation of contains term (#3270)

 Fix default grammar construction for arrays when no free variables are present (#3225)

Encapsulate synth engine (#3271)

Refactoring finite bounds in Quantifiers Engine (#3261)

Fix not to output all warnings (#2778)

Fix syntax error when --language-bindings is java

Replace __attribute__((__unused__)) with CVC4_UNUSED macro

Signed-off-by: matken11235 <26405363+matken11235@users.noreply.github.com>

Fix type assertion in getSynthSolutions (#3252)

Infrastructure for instantiation rewriter (#3262)

Fix constructor type printing (#3246)

Fix issue related to enum in cegqi (#3267)

Fix issue in cegqi related to enum (#3265)

Remove portfolio (#3236)

Remove parsing/printing of meta-info command. (#3260)

Remove SMT1 parser. (#3228)

This commit removes the SMT1 parser infrastructure and adds the SMT2 translations of the SMT1 regression tests. For now this commit removes regression test regress3/pp-regfile.smt since the SMT2 translation has a file size of 887M (vs. 172K for the SMT1 version).

Fixes #2948 and fixes #1313.

Make CEGQI term type to enum (#3256)