Add statistics for proof gen./checking time, size (#2850)

This commit adds a statistic that records the total size of all proofs
generated by an instance of `SmtEngine`. The commit also moves
`SmtEngine::checkProof()` into `smt_engine.cpp` because it needs to know
the complete type of `d_stats` (and the separate file for that method
didn't seem that useful). Additionally, it changes
`smt::SmtEngine::checkProofTime` to `smt::SmtEngine::lfscCheckProofTime`
that only measures the time spent in LFSC and adds a statistic
`proof::ProofManager::proofProductionTime` that measures the proof
production time separately (also works with `get-proof`/`--dump-proof`).

Remove spurious data member. (#2857)

Fix public headers for make install. (#2856)

This commit fixes make install, which previously copied all public header files to ${CMAKE_INSTALL_PREFIX}/ instead of ${CMAKE_INSTALL_PREFIX}/cvc4.
Further, the old build system modified all #include directives in the installed public header files to use the installed headers, e.g., #include "cvc4_public.h" was changed to #include <cvc4/cvc4_public.h>. Now, after make install the script src/fix-install-headers.sh is executed to change the #include directives accordingly (this should be obsolete with the new C++ API).

Add option --sygus-rr-synth-rec for considering all grammar types recursively (#2270)

 Move tuple/record update elimination from ppRewrite to expandDefinition (#2839)

ErProof class with LFSC output (#2812)

* ErProof class with LFSC output

* Created a TraceCheckProof class
   * parsable from text
* Created an ErProof class
   * constructible from a TraceCheckProof
   * writable as LFSC
* A bunch of unit tests

* Reponded to Mathias's first set of comments.

Credits to Mathias for many of the fixes!

* Responed to Andres's first set, fixed tests

I accidentally deleted a "!" last time, causing stuff to fail.

* Use Configuration::isAssertionBuild

* Clarified comment

* Responded to Andres's 2nd review

* Gaurding against a memory error.
* Renaming a file.
* Aggressively unlinking temporary files.

Use string stream for proofs instead of tmp files (#2841)

This commit changes CVC4 to use a string stream instead of a temporary
files for proof checking. Note: This change requires a version of LFSC
that supports checking streams (see
https://github.com/CVC4/LFSC/pull/14).

Tested: `make check` passed, changing `holds` to `xholds` in the proof
produced by proof_manager.cpp makes the proofs fail.

ClangFormat: Disable DerivePointerAlignment (#2842)

The option `DerivePointerAlignment` tries to automatically determine the
pointer alignment used by the input. In our case, we would eventually
like the code base to be consistent throughtout, so this commit disables
that option.

New C++ API: Remove redundant declareFun function. (#2837)

Rewrite simple regexp pattern to str.contains (#2827)

New C++ API: Remove redundant mkTerm function. (#2836)

Delete temporary proof files when aborting CVC4 (#2834)

CVC4 was not deleting temporary proof files when crashing or being
terminated externally. This commit uses an early `unlink()` to remove
the files as soon as CVC4 terminates.

New C++ API: Unit tests for declare* functions. (#2831)

Make stripConstantEndpoints() less aggressive (#2830)

Add rewrite for contains + const strings replace (#2828)

Fix corner case in stripConstantEndpoints (#2824)

`stripConstantEndpoints()` was returning `true` when the first argument
was a list only containing an empty string, which could lead to rewrite
loops. This commit checks for that case and adds a unit test for it.

Fix warning due to catching polymorphic exceptions (#2821)

New C++ API: Fix checks for mkTerm. (#2820)

This required fixing the OpTerm handling for mkTerm functions in the API.

Strings: Remove redundant replace rewrite (#2822)

Pulling the first constant string from a replace if there is no overlap
with the search term is subsumed by the rewrite using
`stripConstantEndpoints()`.

Extended DRAT signature to operational DRAT (#2815)

* Extended DRAT signature to operational DRAT

The DRAT signature now supports both operational and specified DRAT.
That is, either kind of proof will be accepted.

The goal of this implementation of operational DRAT was to re-use as
much of the specified DRAT machinery as possible. However, by writing a
separate operational signature, we could make it much more efficient
(after all, operational DRAT came about because of a push for efficient
cheking).

You can run the new AND old DRAT tests by running

```
lfscc sat.plf smt.plf lrat.plf drat.plf drat_test.plf
```

* Apply suggestions from code review (Yoni)

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>

Avoid using ProofManager in non-proof CMS build (#2814)

PR #2786 changed `CryptoMinisatSolver::addClause()` to register clauses
with the bit-vector proof if proofs are turned on. The new code
requested the `ProofManager` even when proofs were turned off, which
made the `eager-inc-cryptominisat.smt2` regression and our nightlies
fail. This commit guards the access to the `ProofManager`, restoring the
semantics of the original code when proofs are turned off.

Strings: Strengthen multiset reasoning (#2817)

This commit introduces three helper methods for performing multiset
reasoning: an entailment check whether a term is always a strict subset
of another term in the multiset domain (`checkEntailMultisetSubset()`),
a check whether a string term is always homogeneous
(`checkEntailHomogeneousString()`), and an overapproximation for the
multiset domain (`getMultisetApproximation()`). It also adds unit tests
related to multiset reasoning.

 Fix tuple and record CVC printing (#2818)

 Fix parsing of overloaded parametric datatype selectors (#2819)

New README (markdown). (#2797)

Fix missing-override warning (#2811)

`TLazyBitblaster::setProofLog()` was defined even though the method was
not virtual before PR #2808 and `TBitblaster` was implementing the same
method. After that PR, which made the method virtual, GCC complained
about a missing `override` keyword for `setProofLog()`. However, the
method should have been removed (see
[comment](https://github.com/CVC4/CVC4/pull/2786#discussion_r247299617)).
This commit removes the function definition.

Extract DIMACS Printing (#2800)

Creating LRAT proofs reuqires writing SAT problems in the DIMACS format.
Before this code was in the LRAT class.

However, since creating ER proofs will also require writing DIMACS, I
decided to extract it.

At the same time I realized that my prior representation of used clauses
was unnecessarily poor. I had chosen it to align with
`CnfProof::collectAtomsForClauses`, but the format is really bad (it
requires extra allocations & manual memory management), and I discovered
that the aforementioned method is super simple, so I'm moving to a
better format.

Strings: Introduce checkEntailContains() (#2809)

 Fix ABC build (#2808)

PR #2786 introduced a pure virtual method `TBitblaster::getSatSolver()`.
`AigBitblaster` was missing the implementation of that method. This
commit adds an implementation that simply returns the underlying SAT
solver. Note: The method is currently only used for proofs and CVC4 does
not support proofs in combination with ABC. To make this explicit, the
commit also adds a check in `SmtEngine::setDefaults()` that makes sure
that we are not trying to produce proofs with `--bitblast-aig` (before
the commit, we just crashed with an assertion failure/null pointer
dereference).

Add option to print BV constants in binary (#2805)

This commit adds the option `--bv-print-consts-in-binary` to print
bit-vector constants in binary, e.g. `#b0001`, instead of decimal, e.g.
`(_ bv1 4)`). The option is on by default to match the behavior of Z3
and Boolector.

Update NEWS file (#2804)

Bugfix: LFSC clause equality (#2801)

* Bugfix: LFSC clause equality

My implementation of clause equality had an undocumented assumption that
the clauses didn't have any duplicate literals. Now that assumption is
gone, and the tests suite has been expanded.

* Added an empty clause test

* Typo fix: Yoni

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Address Yoni's comments

* Remove a duplicate clause_eq test.
* Add an ordering clause_eq test.
* Improve the documentation of clause_eq.

Extended Resolution Signature (#2788)

* Extended Resolution Signature

While extended resolution is a fairly general technique, the paper
"Extended Resolution Simulates DRAT" / the drat2er uses exactly one new
type of rule: definitions of the form

    new <=> old v (~l_1 ^ ~l_2 ^ ... ^ ~l_n)

This PR adds axioms supporting this kind of definition, and adds a test
making use of those new axioms. The axioms support the following ideas:

   1. Introducing a **fresh** variable, defined in the form above
   2. Clausifying that definition to produce proofs of $$ n + 2 $$ new
      clauses in the form of two clauses, and a cnf with $$ n $$ clauses
   3. An axiom for unrolling the proof of the cnf into proofs of the
      original clauses.

* Addressing Yoni's comments

1. Added a new (trivial) test
2. Improved a bunch of documentation

* Update proofs/signatures/er.plf

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Removed references to RATs from the signature

There are still a few references in the header comment.

* Aside on continuations

* Scrap the elision annotations

Fix constant contains ITOS rewrite (#2799)

CMake: Fix search for static libraries (#2798)

When configuring CVC4 with `--static`, we change
`CMAKE_FIND_LIBRARY_SUFFIXES` to prefer static libraries (`*.a`) over
shared ones. However, instead of prepending `.a` to the list of
`CMAKE_FIND_LIBRARY_SUFFIXES`, we created a single element with `.a` and
the previous list.

Output of `message("${CMAKE_FIND_LIBRARY_SUFFIXES}")` before the change:

```
.a .tbd;.dylib;.so;.a
```

After the change:

```
.a;.tbd;.dylib;.so;.a
```

On macOS, both the static and the shared library of GMP are available
(when installed via homebrew) and before the change, CMake would pick the
shared library when compiling with `--static --no-static-binary`. This
commit fixes that issue.

Strings: Add option to change loop process mode (#2794)

This commit adds an option `--strings-process-loop-mode` that allows
finer-grained control over CVC4 processes looping word equation. In
particular, performing normal loop breaking sometimes leads to worse
performance. The "simple" mode disables that inference.

 Fix unsound double abs rewrite rule for FP (#2792)

 Only check disequal terms with sygus-rr-verify (#2793)

ClausalBitvectorProof (#2786)

* [DRAT] ClausalBitvectorProof

Created a class, `ClausalBitvectorProof`, which represents a bitvector
proof of UNSAT using an underlying clausal technique (DRAT, LRAT, etc)

It fits into the `BitvectorProof` class hierarchy like this:

```
              BitvectorProof
              /            \
             /              \
ClausalBitvectorProof  ResolutionBitvectorProof
```

This change is a painful one because all of the following BV subsystems
referenced ResolutionBitvectorProof (subsequently RBVP) or
BitvectorProof (subsequently BVP):
   * CnfStream
   * SatSolver (specifically the BvSatSolver)
   * CnfProof
   * TheoryProof
   * TheoryBV
   * Both bitblasters

And in particular, ResolutionBitvectorProof, the CnfStream, and the
SatSolvers were tightly coupled.

This means that references to and interactions with (R)BVP were
pervasive.

Nevertheless, an SMT developer must persist.

The change summary:
  * Create a subclass of BVP, called ClausalBitvectorProof, which has
    most methods stubbed out.
  * Make a some modifications to BVP and ResolutionBitvectorProof as the
    natural division of labor between the different classes becomes
    clear.
  * Go through all the components in the first list and try to figure
    out which kind of BVP they should **actually** be interacting with,
    and how. Make tweaks accordingly.
  * Add a hook from CryptoMinisat which pipes the produced DRAT proof
    into the new ClausalBitvectorProof.
  * Add a debug statement to ClausalBitvectorProof which parses and
    prints that DRAT proof, for testing purposes.

Test:
  * `make check` to verify that we didn't break any old stuff, including
    lazy BB, and eager BB when using bvminisat.
  * `cvc4 --dump-proofs --bv-sat-solver=cryptominisat --bitblast=eager
  -d bv::clausal test/regress/regress0/bv/ackermann2.smt2`, and see that
     1. It crashed with "Unimplemented"
     2. Right before that it prints out the (textual) DRAT proof.

* Remove 2 unneeded methods

* Missed a rename

* Typos

Thanks Andres!

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Address Andres comments

* Reorder members of TBitblaster

LFSC LRAT Output (#2787)

* LFSC ouput & unit test

* Renamed lrat unit test file

* s/DRAT/LRAT/

Thanks Andres!

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Addressed Andres' comments

1. Extracted a filter whitespace function.
2. Added @param annotations.

* Addressing Yoni's comments

Tweaked the test method name for LRAT output as LFSC
Added assertions for verifying that clause index lists are sorted during
LFSC LRAT output.

LratInstruction inheritance (#2784)

While implementing and testing LRAT proof output as LFSC, I discovered
that my implementation of LratInstruction as a tagged union was subtly
broken for reasons related to move/copy assignment/constructors.

While I could have figured out how to fix it, I decided to stop fighting
the system and use inheritance.

This PR will be followed by one using the inheritance-based
LratInstruction to implement output to LFSC.

Fixed linking against drat2er, and use drat2er (#2785)

* Fixed linking against drat2er/drat-trim

We have machinery for linking against drat2er. However, this machinery
didn't quite work because libdrat2er.a contains an (undefined) reference
to `run_drat_trim` from libdrat-trim.a.

Thus, when linking against libdrat2er.a, we also need to link against
libdrat-trim.a.

I made this change, and then tested it by actually calling a function
from the drat2er library (CheckAndConvertToLRAT) which relies on
`run_drat_trim`. Since this invocation compiles, we know that the
linking is working properly now.

* Combined the two libs, per Mathias

* drat2er configured gaurds

New C++ API: Add unit tests for setInfo, setLogic, setOption. (#2782)

New C++ API: Get rid of mkConst functions (simplify API). (#2783)

Do not rewrite 1-constructor sygus testers to true (#2780)

[BV Proofs] Option for proof format (#2777)

We're building out a system whereby (eager) BV proofs can be emitted in
one of three formats. Let's add an option for specifying which!

My testing mechanism was not very thorough: I verified that I could specify each of the following option values:
* `er`
* `lrat`
* `drat`
* `help`

and that I could not provide random other option values.

Clause proof printing (#2779)

* Print LFSC proofs of CNF formulas

* Unit Test for clause printing

* Added SAT input proof printing unit test

* Fixed cnf_holds reference. Proofs of CMap_holds

There were references to clauses_hold, which should have been references
to cnf_holds.

Also added a function for printing a value of type CMap_holds, and a
test for this function.

LFSC drat output (#2776)

* LFSC drat output

* Addressed Mathias' review

Addressing Mathias' review with the following changes:
* Added a few blank lines
* Added a unit test for LRAT output as LFSC

New C++ API: Add missing getType() calls to kick off type checking. (#2773)

[DRAT] DRAT data structure  (#2767)

* Copied old DRAT data-structure files.

Next step: clean up the code, and adapt them to our current usage plans.

* Polished the DRAT class.

Notably, removed the idea of lazy-parsing, this is now just a DRAT
wrapper class.

More explicit about whether methods handle binary or text.

Better constructor patterns

* Added implementation of textual DRAT output

* reordered the DratInstruction structure.
* removed the public modifier from the above struct
* removed the operator << implementation for DratInstruction

* use emplace_back

* Addressing Yoni's first review

* Extracted "write literal in DIMACS format" idea as a function
* Replaced some spurious Debug streams with `os`. (they were left over
from an earlier refactor)
* Improved some documentation

* Removed aside about std::string

* Addressed Mathias' comments

Specifically
* SCREAMING_SNAKE_CASED enum variants.
* Extracted some common logic from two branches of a conditional.
* Cleaned out some undefined behavior from bit manipulation.

* Unit tests for binary DRAT parsing

* Added text output test

* s/white/black/ derp

cmake: Disable unit tests for static builds. (#2775)

--static now implies --no-unit-testing.

Fixes #2672.

C++ API: Fix OOB read in unit test (#2774)

There were two typos in the unit tests that caused OOB accesses. Instead
of doing `d_solver.mkConst(CONST_BITVECTOR, std::string("101"), 6)`, the
closing parenthesis was in the wrong place resulting in
`std::string("101", 6)`. The second argument to `std::string(const
char*, size_t)` says how many characters to copy and results in
undefined behavior if the number is greater than the length of the
string, thus the OOB access. The commit fixes the typo and removes one
of the tests because it should not actually fail (16 is an accepted
base).

[LRAT] A C++ data structure for LRAT. (#2737)

* [LRAT] A C++ data structure for LRAT.

Added a data structure for storing (abstract) LRAT proofs.

The constructor will take a drat binary proof and convert it to LRAT
using drat-trim. However, this is unimplemented in this PR.

Subsequent PRs will add:
   * LFSC representation of LRAT
   * Bitvector Proofs based on LRAT
   * Enabled tests for those proofs

* Documenting LRAT constructors

* Apply suggestions from code review

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Responding to Andres' review

Consisting of
   * Naming nits
   * Closed fds
   * Better implementation of disjoint union for LratInstruction
   * DRAT -> LRAT conversion is no longer an LratProof constructor

* include reorder

* Update src/proof/lrat/lrat_proof.h

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Addressed Andres' comments

* ANonymous namespaces and name resolution?

* Remove inlines, fix i negation

Thanks Andres!

* Use `std::abs`

Credit to Andres

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Remove uneeded public

New C++ API: Add missing catch blocks for std::invalid_argument. (#2772)

API/Smt2 parser: refactor termAtomic (#2674)

C++ API: Reintroduce zero-value mkBitVector method (#2770)

PR #2764 removed `Solver::mkBitVector(uint32_t)` (returns a bit-vector
of a given size with value zero), which made the build fail when SymFPU
was enabled because solver_black used it for SymFPU-enabled builds. This
commit simply adds a zero default argument to `mkBitVector(uint32_t,
uint64_t)` to allow users to create zero-valued bit-vectors without
explicitly specifying the value again. Additionally, the commit replaces
the use of the `CVC4_USE_SYMFPU` macro by a call to
`Configuration::isBuiltWithSymFPU()`, making sure that we can catch
compile-time errors regardless of configuration. Finally,
`Solver::mkConst(Kind, uint32_t, uint32_t, Term)` now checks whether
CVC4 has been compiled with SymFPU when creating a `CONST_FLOATINGPOINT`
and throws an exception otherwise (solver_black has been updated
correspondingly).

[LRA proof] Recording & Printing LRA Proofs (#2758)

* [LRA proof] Recording & Printing LRA Proofs

Now we use the ArithProofRecorder to record and later print arithmetic
proofs.

If an LRA lemma can be proven by a single farkas proof, then that is
done. Otherwise, we `trust` the lemma.

I haven't **really** enabled LRA proofs yet, so `--check-proofs` still
is a no-op for LRA.

To test, do
```
lfsccvc4 <(./bin/cvc4 --dump-proofs ../test/regress/regress0/lemmas/mode_cntrl.induction.smt | tail -n +2)
```

where `lfsccvc4` is an alias invoking `lfscc` with all the necessary
signatures. On my machine that is:

```
alias lfsccvc4="/home/aozdemir/repos/LFSC/build/src/lfscc \
/home/aozdemir/repos/CVC4/proofs/signatures/sat.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/smt.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/lrat.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_base.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_bv.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_bv_bitblast.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_arrays.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_int.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_quant.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_real.plf \
/home/aozdemir/repos/CVC4/proofs/signatures/th_real.plf"

```

* Added guards to proof recording

Also reverted some small, unintentional changes.

Also had to add printing for STRING_SUBSTR??

* Responding to Yoni's review

* SimpleFarkasProof examples

* Respond to Aina's comments

* Reorder Constraint declarations

* fix build

* Moved friend declaration in Constraint

* Trichotomy example

* Lift getNumChildren invocation in PLUS case

Credits to aina for spotting it.

* Clang-format

New C++ API: Add tests for mk-functions in solver object. (#2764)

Clean up BV kinds and type rules. (#2766)

Add missing type rules for parameterized operator kinds. (#2766)

Fix issues with REWRITE_DONE in floating point rewriter (#2762)

Remove noop. (#2763)

 Configured for linking against drat2er (#2754)

drat2er is a C/C++ project which includes support for
   * Checking DRAT proofs
   * Converting DRAT proofs to LRAT proofs
   * Converting DRAT proofs to ER proofs

It does the first 2 by using drat-trim under the hood.

I've modified our CMake configuration to allow drat2er to be linked into
CVC4, and I added a contrib script.

New C++ API: Add tests for term object. (#2755)

DRAT Signature (#2757)

* DRAT signature

Added the DRAT signature to CVC4.

We'll need this in order to compare three BV proof pipelines:
   1. DRAT -> Resolution -> Check
   2. DRAT -> LRAT -> Check
   3. DRAT -> Check (this one!)

Tested the signature using the attached test file. i.e. running
```
lfscc sat.plf smt.plf lrat.plf drat.plf drat_test.plf
```

* Added type annotations for tests

* Respond to Yoni's review

* Apply Yoni's suggestions from code review

Documentation polish

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Whoops, missed a spot or two

Revert "Move ss-combine rewrite to extended rewriter (#2703)" (#2759)

 [LRA Proof] Storage for LRA proofs  (#2747)

* [LRA Proof] Storage for LRA proofs

During LRA solving the `ConstraintDatabase` contains the reasoning
behind different constraints. Combinations of constraints are
periodically used to justify lemmas (conflict clauses, propegations, ...
?). `ConstraintDatabase` is SAT context-dependent.

ArithProofRecorder will be used to store concise representations of the
proof for each lemma raised by the (LR)A theory. The (LR)A theory will
write to it, and the ArithProof class will read from it to produce LFSC
proofs.

Right now, it's pretty simplistic -- it allows for only Farkas proofs.

In future PRs I'll:
   1. add logic that stores proofs therein
   2. add logic that retrieves and prints proofs
   3. enable LRA proof production, checking, and testing

* Document ArithProofRecorder use-sites

* Update src/proof/arith_proof_recorder.cpp

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Yoni's review

* clang-format

* Response to Mathias' review.

Fixed typos.

New C++ API: Add tests for opterm object. (#2756)

 Fix extended rewriter for binary associative operators. (#2751)

This was causing assertion failures when using Sets + Sygus.

Make single invocation and invariant pre/post condition templates independent (#2749)

--cegqi-si=none previously disabled pre/post-condition templates for invariant synthesis. This PR eliminates this dependency.

There are no major code changes in this PR, unfortunately a large block of code changed indentation so I refactored it to be more up to date with the coding guidelines.

New C++ API: Add tests for sort functions of solver object. (#2752)

Remove spurious map (#2750)

Fix compiler warnings. (#2748)

API: Add simple empty/sigma regexp unit tests (#2746)

[LRA proof] More complete LRA example proofs. (#2722)

* [LRA proof] Refine "poly" and "term Real" distinction

Short Version:

Refined the LRA signature and used the refined version to write two new
test proofs which are close to interface compatible with the LRA proofs
that CVC4 will produce.

Love Version:

LRA proofs have the following interface:
   * Given predicates between real terms
   * Prove bottom

However, even though the type of the interface does not express this,
the predicates are **linear bounds**, not arbitrary real bounds. Thus
LRA proofs have the following structure:

   1. Prove that the input predicates are equivalent to a set of linear
      bounds.
   2. Use the linear bounds to prove bottom using farkas coefficients.

Notice that the distinction between linear bounds (associated in the
signature with the string "poly") and real predicates (which relate
"term Real"s to one another) matters quite a bit. We have certain inds
of axioms for one, and other axioms for the other.

The signature used to muddy this distinction using a constructor called
"term_poly" which converted between them. I decided it was better to buy
into the distinction fully.

Now all of the axioms for step (2) use the linear bounds and axioms for
step (1) use both kinds of bounds, which makes sense because step (1) is
basically a conversion.

Also had to add an axiom or two, because some were missing.

* Update proofs/signatures/th_lra.plf

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Improved test readability, removed unused axioms

The LRA proof tests did not have appropriate documentation, and did not
specify **what** they proved. Now they each have a header comment
stating their premises and conclusion, and that conclusion is enforced
by a type annotation in the test.

The LRA signature included some unused axioms concerning `poly_term`.
Now they've been removed.

Credits to Yoni for noticing both problems.

[LRAT] signature robust against duplicate literals (#2743)

* [LRAT] signature robust against duplicate literals

The LRAT signature previously had complex, surprising, and occasionally
incorrect behavior when given clauses with duplicate literals.

Now it does not. Now clauses have true set semantics, and clauses with
duplicate literals are treated identically to those without.

* Test with logically = but structurally != clauses.

Remove alternate versions of mbqi (#2742)

LRAT signature (#2731)

* LRAT signature

Added an LRAT signature. It is almost entirely side-conditions, but it
works.

There is also a collection of tests for it. You can run them by invoking

```
lfscc smt.plf sat.plf lrat.plf lrat_test.plf
```

* Update proofs/signatures/lrat.plf per Yoni's suggestion.

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Responding to Yoni's comments.

* Removed unused varaibles

Some tests declared `var`s which were unused.
Now they don't.

BoolToBV modes (off, ite, all) (#2530)

Strings: Make EXTF_d inference more conservative (#2740)

Arith Constraint Proof Loggin (#2732)

* Arith Constraint Proof Logging

Also a tiny documentation update.

* Debug.isOn check around iterated output

* reference iteratees

Enable BV proofs when using an eager bitblaster (#2733)

* Enable BV proofs when using and eager bitblaster

Specifically:
   * Removed assertions that blocked them.
   * Made sure that only bitvectors were stored in the BV const let-map
   * Prevented true/false from being bit-blasted by the eager bitblaster

Also:
   * uncommented "no-check-proofs" from relevant tests

* Option handler logic for BV proofs

BV eager proofs only work when minisat is the sat solver being used by
the BV theory.

Added logic to the --proof hanlder to  verify this or throw an option
exception.

* Bugfix for proof options handler

I forgot that proofEnabledBuild runs even if the --proof option is
negated. In my handler I now check that proofs are enabled.

* Clang-format

Fix use-after-free due to destruction order (#2739)

A test for PR #2737 was failing even though the PR only added dead code.
This PR fixes the issue by fixing two use-after-free bugs:

- `ResolutionBitVectorProof` has a `Context` and a
`std::unique_ptr<BVSatProof>` member. The `BVSatProof` depends on the
`Context` and tries to access it (indirectly) in its constructor but
because the context was declared after the proof, the context was
destroyed before the proof, leading to a use-after-free in a method
called from the proof's destructor. This commit reorders the two
members.
- `TLazyBitblaster` was destroyed before the `LFSCCnfProof` in
`BitVectorProof` because `SmtEngine`'s destructor first destroyed the
theory engine and then the proof manager. This lead to a use-after-free
because `LFSCCnfProof` was using the `d_nullContext` of
`TLazyBitblaster`, which got indirectly accessed in `LFSCCnfProof`'s
destructor. This commit moves the destruction of `ProofManager` above
the destruction of the theory engine.

The issues were likely introduced by #2599. They went undetected because
our nightlies' ASAN check does not use proofs due to known memory leaks
in the proof module of CVC4.

I have tested this PR up to regression level 2 with ASAN with leak
detection disabled.

 Take into account minimality and types for cached PBE solutions (#2738)

Apply extended rewriting on PBE static symmetry breaking. (#2735)

Enable regular expression elimination by default. (#2736)

Seems to have no impact on Norn, and is helpful for a number of applications.

 Skip non-cardinality types in sets min card inference (#2734)

Bit vector proof superclass (#2599)

* Split BitvectorProof into a sub/superclass

The superclass contains general printing knowledge.

The subclass contains CNF or Resolution-specific knowledge.

* Renames & code moves

* Nits cleaned in prep for PR

* Moved CNF-proof from ResolutionBitVectorProof to BitVectorProof

Since DRAT BV proofs will also contain a CNF-proof, the CNF proof should
be stored in `BitVectorProof`.

* Unique pointers, comments, and code movement.

Adjusted the distribution of code between BVP and RBVP.
  Notably, put the CNF proof in BVP because it isn't
  resolution-specific.
Added comments to the headers of both files -- mostly BVP.
Changed two owned pointers into unique_ptr.
  BVP's pointer to a CNF proof
  RBVP's pointer to a resolution proof

BVP: `BitVectorProof`
RBVP: `ResolutionBitVectorProof`

* clang-format

* Undo manual copyright modification

* s/superclass/base class/

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* make LFSCBitVectorProof::printOwnedSort public

* Andres's Comments

Mostly cleaning up (or trying to clean up) includes.

* Cleaned up one header cycle

However, this only allowed me to move the forward-decl, not eliminate
it, because there were actually two underlying include cycles that the
forward-decl solved.

* Added single _s to header gaurds

* Fix Class name in debug output

Credits to Andres

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Reordered methods in BitVectorProof per original  ordering

Optimizations for PBE strings (#2728)

 Infrastructure for sygus side conditions (#2729)

Combine sygus stream with PBE (#2726)

Improve interface for sygus grammar cons (#2727)

Information gain heuristic for PBE (#2719)

Optimize re-elim for re.allchar components (#2725)

Improve skolem caching by normalizing skolem args (#2723)

In certain cases, we can share skolems between similar reductions, e.g.
`(str.replace x y z)` and `(str.replace (str.substr x 0 n) y z)` because the
first occurrence of `y` in `x` has to be the first occurrence
of `y` in `(str.substr x 0 n)` (assuming that `y` appears in both, otherwise the value of
the skolems does not matter). This commit adds a helper function in the
skolem cache that does some of those simplifications.

Generalize sygus stream solution filtering to logical strength (#2697)

Improve cegqi engine trace. (#2714)

Make (T)NodeTrie a general utility (#2489)

This moves quantifiers::TermArgTrie in src/theory/quantifiers/term_database to (T)NodeTrie in src/expr, and cleans up all references to it.

Fix coverity warnings in datatypes (#2553)

This caches some information regarding tester applications and changes int -> size_t in a few places.