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)

 Model API for domain elements (#3243)

Explicitly pass current sygus solution to exclude (#3209)

Refactoring CEGQI interface (#3239)

Towards incremental SyGuS in SMT engine (#3195)

More details in substitution function documentation (#3244)

Move getCounterexampleLiteral out of term utilities (#3238)

Fix DAGification for printer. (#3233)

 Fixes related to destructing null (#3231)

Remove duplicate regression tests. (#3227)

Fix out-of-bounds access in regexp inclusion test (#3242)

If `re.*(re.allchar)` was at the end of a regular expression
concatenation, the regular expression inclusion test could cause
out-of-bound accesses. For `re.*(re.allchar)`, we were blindly adding
the index after it to the set of indices being considered. Later in the
loop, we were assuming that all the indices are smaller than the number
of components in the concatenation, thus leading to out-of-bound
accesses. This commit adds a check before adding the index to the set of
indices.

Signed-off-by: Andres Noetzli <andres.noetzli@gmail.com>

Undo unintential change to FindCxxTest (#3240)

Better heuristic for str.code/re.range (#3220)

To make sure that our `str.code` function is injectve (except for -1 in
the codomain), we send the inference that `str.code(x) == -1 v
str.code(x) != str.code(y) v x == y` for each pair of `str.code` terms.
Because of the order of disjuncts, `str.code(x) != str.code(y)` was
usually assigned true. This in turn lead to a difficult problem for the
arithmetic engine if there were more `str.code` applications than the
size of the domain. E.g. if we had `0 <= str.code(xi) < 10` for 0 <= i
<= 10, then the arithmetic engine had a difficult time finding a
conflict. This PR improves the heuristic by setting the phase of
`str.code(x) != str.code(y)` to false, so we prefer to keep the
`str.code` values equal instead of trying to make them different.

This change is also reflected in the models produced for inputs
involving `str.code`: Previously, we were producing models with
different values for the `str.code` whereas now the models are much more
uniform.

The PR adds two regressions, one testing `str.code` performance directly
and one testing it for `str.code` terms generated by `re.range`.

Signed-off-by: Andres Noetzli <anoetzli@amazon.com>

Infer conflicts based on regular expression inclusion (#3234)

We have a conflict if we have `str.in.re(x, R1)` and `~str.in.re(x, R2)`
and `R2` includes `R1` because there is no possible value for `x` that
satisfies both memberships. This commit adds code to detect regular
expression inclusion for a small fragment of regular expressions: string
literals with single char (`re.allchar`) and multichar wildcards
(`re.*(re.allchar)`).

Signed-off-by: Andres Noetzli <anoetzli@amazon.com>

Removing comments related to issues (#3232)

Fixes for get-abduct (#3229)

Make contrib/get-* more robust. (#3198)

We use the command which to determine if a command is available on the system. However, which is not installed on all platforms by default (e.g. CentOS). command is a shell builtin that can be used for the same purpose.

Remove unnecessary code from Cvc.g (#3213)

fix misuse of iterator with a different container (#3214)

fix mismatch between "delete" and "new []" (#2795)

 Infer emptiness instead of splitting when a string equality rewrites to a constant (#3218)

 Fixes for sygus regressions (#3219)

Document transition inference utility (#3207)

Exclude redundant lemmas when tracking inst lemmas. (#3210)

Update dynamic splitting strategy for quantifiers (#3162)

Fix argument in nonlinear extension. (#3216)

Minor update to term util (#3208)

 Pass synthesis conjecture to sygus modules (#3212)