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)

 Local substitutions for context-depdendent simplification in strings (#3204)

Fixes for sygus inference on quantifier free problems (#3202)

New C++ API: Add checks for Solver::checkValid and Solver::checkValidAssuming. (#3197)

Context-independent regular expression unfolding (#3168)

 Cleaning make bound var in smt2 parser (#3192)

Move quantifiers relevance module inside E-matching module (#3186)

Mark symbols introduced by named attributes as defined. (#3190)

 Fix for when to apply single invocation techniques (#3193)

cmake: Use ExactVersion instead of SameMinorVersion. (#3191)

Remove option --continued-execution. (#3189)

 Update to standard implementation of getting free variables (#3175)

Call separate SMT engine for single invocation sygus (#3151)

cmake: Export CVC4 library interface. (#3179)

Enable Clang-Format for Java (#3064)

Minor cleaning of sygus term database (#3159)

Fix issue related to higher-order purification in term database (#3157)

SmtEngine: Reorganize class according to guidelines, some cleanup. (#3183)

New C++ API: Add checks and tests for Solver::simplify. (#3170)

New C++ API: Fix test names of solver_black unit test. (#3170)

New C++ API: Reorganize Solver code (move only). (#3170)

 Track sygus variable to term relationship via attribute (#3182)

Update option to disable symbolic definitions in strings (#3180)

Add string rewrite involving allchar stars (#3167)

Properly implement logic info for separation logic (#3176)

Implement check abduct feature (#3152)

Introduce smt2 parsing utility ParseOp and refactor (#3165)

Clean smt2 parsing of named attributes (#3172)

 Give rewrite engine pointer to conflict-based instantiation module (#3174)

New C++ API: Add documentation/guidelines for API guards. (#3178)

New C++ API: Add templated getIndices method for OpTerm (#3073)

* Implement templated getIndices method for OpTerm

* Add getIndices unit tests

* Update src/api/cvc4cpp.cpp

Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>
* Update src/api/cvc4cpp.cpp

Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>
* Add comment about DIVISIBLE_OP

* Update test/unit/api/opterm_black.h

Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>
* Update test/unit/api/opterm_black.h

Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>
* Update test/unit/api/opterm_black.h

Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>
* Update test/unit/api/opterm_black.h

Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>
* Add exception checks to other unit tests (instead of having its own function)

* Fix unit test names in opterm_black.h

* Add description to docstring for getIndices

* Formatting

* Clang format older commits

* Use '-' in docstring list to match other docstrings

* Support creating DIVISIBLE_OP with a string (for arbitrary precision integers)

* Move mkOpTerm(DIVISIBLE_OP, <str>) test to solver_black.h

* Fix pointer access

* Replace switch statement with if statement

* Guard string input for CVC4::Integer in mkOpTerm for consistency on GMP/CLN back-end

Simplify how defined functions are tracked during parsing (#3177)

Add option to only dump unsolved queries for --sygus-query-gen (#3173)

Reorganize includes for quantifiers engine (#3169)

Add subdirectories to contrib for competition scripts (#3164)

Fix issues with Ninja build system and add configure option. (#3166)

Adds option --ninja to configure.sh.

New C++ API: Add checks and tests for push/pop. (#3121)

New C++ API: Introduce macros for try-catch blocks in Solver. (#3121)

New C++ API: Fix branch prediction in CHECK macros. (#3161)

Properly parse qualified identifiers  (#3111)

Scripts for CASC-27 (#3163)

Fix drat signature wrt side condition return types. (#3160)

Remove forward declarations in quantifiers engine (#3156)

Fix regression script for incremental SMT-LIB v2 benchmarks. (#3155)

The regression script did not extract the expected status from incremental
SMT-LIB v2 benchmarks correctly if status was given via (set-info :status ...). The
script used re.search for finding the status, which only searches for
the first occurrence instead of finding all (set-info :status ...).

This commit fixes the issue by using re.findall instead.

Fix printing issue related to nested quotes (#3154)

Collapse @ chains in SMT2 printer (#3140)

Update CaDiCaL to version 1.0.3. (#3137)

* Removes incremental API check (#3011)
* Fixes toSatValueLit to use the new semantics of CaDiCaL's val()

Fixes #3011

Flip the polarity of the argument of get-abduct (#3153)

Add better Python detection for contrib scripts. (#3150)

 Move basic sygus enumerator to its own file (#3149)

Remove simplification specialized for sygus si solution reconstruction (#3147)

Support default sygus grammar for strings (#3148)

Throw option exception when track inst lemmas is not used (#3145)

Fix solution filtering for streaming abducts (#3143)

Fix BVGauss unit tests. (#3142)

pass_bv_gauss_white.h included bv_gauss.cpp to test the functions in the
anonymous namespace, which resulted in ODR (one definition rule)
violations reported by ASAN.

This commit exposes the functionality required in the unit tests as
private static members of the BVGauss class. Since this is a white unit
test, we can access private members in the tests.

Enable sygus logic when produce-abducts is true (#3144)

Use python realpath instead of relying on shell realpath (#3117)

* Use a custom implementation instead of relying on realpath, because it doesn't exist on Mac

* Use local variables and move portable_realpath to its own file

* Replace portable_realpath with python realpath

* Consistent command substitution

Co-Authored-By: Andres Noetzli <andres.noetzli@gmail.com>
* Substitute pwd directly

Fix memory leak in rewriter (debug mode). (#3141)

s_rewriteStack in rewriter.cpp was not properly cleaned up. This commit
wraps s_rewriteStack in a std::unique_ptr to automatically free the
memory.

Move some generic utilities out of quantifiers (#3139)

 Regular expression intersection modes (#3134)

Parsing THF and adding several regressions (#3131)

adding bv_gauss unit test to build files (#3135)

Add some missing cases in evaluator (#3133)

Eager conflict detection in strings based on constant prefix/suffix (#3110)

 Track solver execution mode (#3132)

Code to activate hoelim preprocessing pass (#3129)

Minor improvement for rewriter for str.replace (#3124)

 Handle RE intersections modulo equality (#3120)

Remove hard coded option for TPTP regressions in run_regression (#3128)

Model blocker feature (#3112)

Support get-abduct smt2 command (#3122)

Fix match trie for polymorphic operators (#3125)