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)

Refactoring of bit-vector elimination rules (#3105)

This commit makes the following minor refactors to src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h:
- Including options/bv_options.h: this is needed because this header file is being used.
- Marking all functions as inline: details in a discussion inside the PR.

Minor improvement to term canonizer (#3123)

Input user grammar in sygus abduct (#3119)

Split infer info data structure in strings (#3107)

adding runscripts for syguscomp2019 (#3118)

Minor refactoring of regexp operation (#3116)

 Fix null node when using no-strings-lazy-pp (#3114)

 Move string util functions (#3115)

Fix sygus datatype parsing in sygus v1 format (#3113)

Fix help messages (#3096)

Get operators in node (#3094)

This commit adds a function to node_algorithm.{h,cpp} that returns the operators that occur in a given node.

Avoid move constructor of std::fstream for GCC < 5 (#3098)

GCC < 5 does not support the move constructor of `std::fstream` (see
https://gcc.gnu.org/bugzilla/show_bug.cgi?id=54316 for details). This
commit wraps the `std::fstream` in an `std::unique_ptr` to work around
that issue.

SyGuS grammar refactor (#3100)

Fixes for sygus with datatypes (#3103)

Fix case of unfolding negative membership in reg exp concatenation (#3101)

Removing forward-declaration of undefined function 'registerForceLogicListener' (#3086)

Basic rewrites for tolower/toupper (#3095)

Minor clean in strings. (#3093)

Add support for str.tolower and str.toupper (#3092)

 Add string rewrite to distribute character stars over concatenation (#3091)

Towards refactoring relations (#3078)

Refactor strings to use an inference manager object (#3076)

Use unique_ptr for UF modules (#3080)

Optimize DRAT optimization: clause matching (#3074)

* improved proof production statistics

This commit creates new statistics which will help us understand what is
so expensive about proof production.

There are already statistics for:
* Net time spent building/printing the LFSC proof.
* Size of the LFSC proof.

This commit adds statistics for:
* The time cost of DRAT optimization:
   * net time
   * tool time (drat-trim)
   * clause matching time (matching core clauses with input clauses)
      * Non-trivial because drat-trim can (and does) dedup and reorder
        literals
* The advantage of DRAT optimization (proof/formula size before/after)
* The time cost of DRAT translation [to LRAT or ER] (net time, tool time)
* The time cost of skeleton traversal
* The time cost of printing declatations
* The time cost of printing CNF proofs
* The time cost of printing theory lemmas
* The time cost of printing final UNSAT proof.

There is a method, toStream, which is responsible for much of proof
production. The whole method was timed, but subsections were not. The
timings above consider subsections of it.

I also wanted to better understand the cost of DRAT optimization and
translation.

* [BV Proof] Optimize DRAT optimization

tldr: I made a bad data-structure/algorithm choice when implementing
part of DRAT/CNF-optimization, which consumed **a lot** of time on some
bechmarks. This commit fixes that choice.

Long Version:

Set-Keyed Maps Considered Harmful
=================================

Algorithmic Problem
-------------------

The DRAT optimization process spits out a unsatifiable core of the CNF.
The clauses in the core are all from the original formula, but their
literals may have been reordered and deduplicated.  We must match the
old clauses with new ones, so we know which old clauses are in the core.

Old (BAD) Solution
------------------

Before I didn't really think about this process very much. I built a
solution in which clauses were canonically represented by hash sets of
literals, and made a hash map from canonical clauses to clause indices
into the original CNF.

Problem With Old Solution
-------------------------

In hindsight this was a bad idea. First, it required a new hash set to
be heap-allocated for every clause in the CNF. Second, the map lookups
required set-hashes (reasonable -- linear time, once) and hash-set
equality (not reasonable -- quadratic time, multiple times) on every
lookup.

New Solution
------------

The ideal solution is probably to have the map from clauses to clause
ids be something like a trie. STL doesn't have a trie, but representing
clauses as sorted, deduped vectors of literal in a tree based on
lexicographical comparison is pretty closed to this. On randomly chosen
examples it seems to be a huge improvement over the old
map-keyed-by-sets solution, and I'm in the process of running a full set
of bechmarks.

Also, we store pointers to the clauses already stored elsewhere in the
proof, instead of allocating new memory for them.

Future Work
-----------

It may also be reasonable to do a hash map of sorted, deduped, vector
clauses. I haven't tried this, yet (there's a TODO in the code).

* Update src/proof/clausal_bitvector_proof.h

Thanks andres!

Co-Authored-By: Andres Noetzli <andres.noetzli@gmail.com>
* Respond to Andres' Review: better use of CodeTimer

* Removed commented code (Andres)

Refactoring of relevance vector in quantifiers (#3070)

Support sygus version 2 format (#3066)

 Split higher-order UF solver (#2890)

Add higher-order elimination preprocessing pass (#2865)

Make mkOpTerm const (#3072)

Variable elimination rewrite for quantified strings (#3071)

Stratify unfolding of regular expressions based on polarity (#3067)