More aggressive skolem caching for strings, document and clean preprocessor (#2478)

Make strings model construction robust to lengths that are not propagated equal (#2444)

This fixes #2429.

This was caused by arithmetic not notifying an equality between shared terms that it assigned to the same value.  See explanation in comment.

We should investigate a bit more why this is happening. I didnt think arithmetic was allowed to assign the same value to unpropagated shared length terms.  I've opened issue https://github.com/CVC4/CVC4/issues/2443 to track this.

Regardless, the strings model construction should be robust to handle this case, which this PR does.

Follow redirects with cURL in contrib/get* scripts (#2471)

On systems without `wget`, we use `curl` to download dependencies.
However, we were not using the `-L` (follow redirects) option, which is
necessary to download certain dependencies, e.g. CryptoMiniSat.

Remove broken dumping support from portfolio build (#2470)

Dumping support for portfolio builds was introduced in
84f26af22566f7c10dea45b399b944cb50b5e317 but as far as I can tell, the
implementation has already been problematic in the original implementation. The
current implementation has the following issues:

- Dumping with a portfolio build (even when using the single threaded
executable) results in a segfault. The reason is that the DumpChannel variable
is declared as an `extern` and exists for the duration of the program. The
problem is that it stores a `CommandSequence`, which indirectly may store
nodes. When shutting down CVC4, the destructor of `DumpC` is called, which
destroys the `CommandSequence`, which results in a segfault because the
`NodeManager` does not exist anymore. The node manager is (indirectly) owned
and destroyed by the `api::Solver` object.
- Additionally, adding commands to the `CommandSequence` is not thread safe (it
just calls `CommandSequence::addCommand()`, which in turn pushes back to a
vector [0] (which is not thread safe [1]). A single instance of `DumpChannel`
is shared among all threads (it is not declared `thread_local` [2]).
- The `CommandSequence` in `DumpC` was not used in the original implementation
and is still unused on master. The original commit mentions that the portfolio
build stores the commands in the `CommandSequence` but not why.

This commit removes the `CommandSequence` and related methods from `DumpC` to
avoid the issue when destroying `DumpChannel`. It disables dumping for
portfolio builds and adds a check at configure-time that not both options have
been enabled simultaneously.  Given that the option was not functional
previously, the problematic implementation, and the fact that the dump of
multiple threads wouldn't be very useful, disabling dumping for portfolio
builds is unlikely to be problem. An improvement that could be made is to
disable dumping support only for the pcvc4 binary and while enabling it for the
single-threaded version, even when using `--with-portfolio`. However, we
currently do not have the infrastructure for that (we use the same libcvc4
library for both binaries).

[0] https://github.com/CVC4/CVC4/blob/c2111c86973b8a80e20a3fdf3cbd0b2ff0dc7010/src/smt/command.cpp#L756
[1] https://en.cppreference.com/w/cpp/container
[2] https://github.com/CVC4/CVC4/blob/c2111c86973b8a80e20a3fdf3cbd0b2ff0dc7010/src/smt/dump.h#L117

Remove unnecessary tracing from preprocessing (#2472)

With the introduction of the PreprocessingPass class,
tracing/dumping/time keeping is done automatically in the base class,
eliminating the need for doing it manually. This commit cleans up
SmtEngine, removing tracing/dumping/time keeping in preprocessing that
is not needed anymore.

Decision strategy: incorporate UF with cardinality constraints (#2476)

Decision strategy: incorporate sygus feasible and sygus stream feasible (#2462)

Refactor how assertions are added to decision engine (#2396)

Before refactoring the preprocessing passes, we were using three
arguments to add assertions to the decision engine. Now all that
information lives in the AssertionPipeline. This commit moves the
AssertionPipeline to its own file and changes the `addAssertions()`
methods related to the decision engine to take an AssertionPipeline as
an arguement instead of three separate ones. Additionally, the
TheoryEngine now uses an AssertionPipeline for lemmas.

Add Skolem cache for strings, refactor length registration (#2457)

This PR is in preparation for doing more aggressive caching of skolems (for example, in the strings preprocessor).

It refactors sendLengthLemma -> registerLength, which unifies how length lemmas for skolems and other string terms are handled.

Generalize CandidateRewriteDatabase to ExprMiner (#2340)

Fix #include for minisat headers in bvminisat. (#2463)

Uses information gain heuristic for building better solutions from DTs (#2451)

Simplify storing of transcendental function applications that occur in assertions (#2458)

 Decision strategy: incorporate CEGQI (#2460)

New C++ API: Try to fix (false positive) Coverity warnings. (#2454)

Examples: Remove obsolete flag CVC4_MAKE_EXAMPLES. (#2461)

 Initial infrastructure for theory decision manager (#2447)

Fix for when strings process loop is disabled. (#2456)

Fixe compiler warning in line_buffer.cpp. (#2453)

Support model cores via option --produce-model-cores. (#2407)

This adds support for model cores, fixes #1233.

It includes some minor cleanup and additions to utility functions.

Avoid calling size() every iteration (#2450)

Fix global negate (#2449)

fix (#2446)

Set NodeManager to nullptr when  exporting vars (#2445)

PR #2409 assumed that temporarily setting the NodeManager to nullptr
when creating variables is not needed anymore. However, this made our
portfolio build fail. This commit reintroduces the temporary NodeManager
change while creating variables.

Using a single condition enumerator in sygus-unif (#2440)

This commit allows the use of unification techniques in which the search space for conditions in explored independently of the search space for return values (i.e. there is a single condition enumerator for which we always ask new values, similar to the PBE case).

In comparison with asking the ground solver to come up with a minimal number of condition values to resolve all my separation conflicts:

- _main advantage_: can quickly enumerate relevant condition values for solving the problem
- _main disadvantage_: there are many "spurious" values (as in not useful for actual solutions) that get in the way of "good" values when we build solutions from the lazy trie.

A follow-up PR will introduce an information-gain heuristic for building solutions, which ultimately greatly outperforms the other flavor of sygus-unif.

There is also small improvements for trace messages.

Refactor non-clausal simplify preprocessing pass. (#2425)

Squash implementation of counterexample-guided instantiation (#2423)

Add (str.replace (str.replace y w y) y z) rewrite (#2441)

Replace boost::integer_traits with std::numeric_limits. (#2439)

Further, remove redundant gmp.h include in options_handler.cpp.

Remove clock_gettime() replacement for macOS. (#2436)

Not needed anymore since macOS 10.12 introduced clock_gettime().

 Make isClosedEnumerable a member of TypeNode (#2434)

 Further simplify and fix initialization of ce guided instantiation (#2437)

Refactor and document quantifiers variable elimination and conditional splitting (#2424)

Minor improvements to interface for rep set. (#2435)

 More extended rewrites for strings equality (#2431)

 Eliminate select over store in quantifier bodies (#2433)

Use std::uniqe_ptr for d_eq_infer to make Coverity happy. (#2432)

Remove printing support for sygus enumeration types (#2430)

Finer-grained inference of substitutions in incremental mode (#2403)

Add regex grammar to rewriter verification tests (#2426)

 Extended rewriter for string equalities (#2427)

Add HAVE_CLOCK_GETTIME guard to clock_gettime.c (#2428)

Remove redundant strings rewrite. (#2422)

str.in.re( x, re.++( str.to.re(y), str.to.re(z) ) ) ---> x = str.++( y, z ) is not necessary since

re.++( str.to.re(y), str.to.re(z) ) -> str.to.re( str.++( y, z ) )
str.in.re( x, str.to.re( str.++(y, z) ) ) ---> x = str.++( y, z )

This PR removes the above rewrite, which was implemented incorrectly and was dead code.

Update INSTALL instructions (#2420)

Fixes #2419. This commit adds more information about optional
dependencies, updates macOS-related information, and fixes some details.

Remove CVC3 compatibility layer (#2418)

Remove unused options file (#2413)

Minor improvements to theory model builder interface. (#2408)

Make quantifiers strategies exit immediately when in conflict (#2099)

Transfer ownership of learned literals from SMT engine to circuit propagator. (#2421)

Fix merge mishap of #2359.

Refactor ceg conjecture initialization (#2411)

Allows SAT checks of repair const to have different options (#2412)

Refactor and document alpha equivalence. (#2402)

Fix export of bound variables (#2409)

Refactor theory preprocess into preprocessing pass. (#2395)

Use useBland option in FCSimplexDecisionProcedure (#2405)

Add regular expression elimination module (#2400)

Refactor MipLibTrick preprocessing pass. (#2359)

Forcing attribute_internals.h to use uint64_t's for shift operations. (#2370)

fix bv total ops printing (#2365)

 Split term canonize utility to own file and document (#2398)

Reorder circuit propagator class.

Move flag needsFinish from SMT engine to circuit propagator.

 Fix for get constraints method in fmf-fun (#2399)

Solve equalities between Boolean variables in presolve. (#2390)

Remove throw specifiers in FP type checker (#2392)

Remove dead code in fp_converter (#2388)

This should fix Coverity issues 1473025 and 1459599.

Fix sort inference for quantified variables of interpreted types (#2393)

 Address more coverity warnings (#2394)

Fix warning in sygus io. (#2391)

Remove dead code in evaluator (#2389)

This should fix Coverity issue 1470214.

Refactor extended rewriter, move rewrites to aggressive (#2387)

This is work towards #2305.

With this PR, CVC4's performance is fairly reasonable on the Kind2 BMC benchmarks with --decision=internal --ext-rew-prep --ext-rew-prep-agg.

New C++ API: Fix isDefinedKind() to not be ambigious with respect to … (#2384)

…underlying type.

Use std:unique_ptr instead of raw pointers in theory/bv. (#2385)

This should also fix CIDs 1465687, 1465695, 1465696, and 1465701.

Resolution proof: separate printing from proof (#1964)

Currently, we have an LFSCSatProof which inherits from TSatProof and
implements printing the proof. The seperation is not clean (e.g.
clauseName is used for printing only but is in TSatProof) and the
inheritance does not add any value while making dependencies more
confusing. The plan is that TSatProof becomes a self-contained part that
the MiniSat implementations generate and ProofManager prints out. This
commit is a first step in that direction. For SAT solvers with native
capabilities for producing proofs, we would simply implement a different
LFSC printer of their proof representation without changing the SAT
solver itself. The inheritance would make this awkward to deal with.

Additionally, the commit cleans up some unused functions and adjusts the
visibility of TSatProof methods and members.

Make division chainable in the smt2 parser (#2367)

Remove Coverity build from Travis (#2373)

The Coverity build is now done as part of our nightlies and the Travis
Coverity build was timing out most of the time anyway, so this commit
removes it.

Use uniform length limit for String constants (#2381)

Fix unsigned integer type issues in strings (#2380)

* Fix unsigned integer types in strings.

* Format

Refactor unconstrained simplification pass (#2374)

Refactor quantifier macros preprocessing pass (#1840)

Moved `src/theory/quantifiers/macros.{cpp,h}` to `src/preprocessing/passes/quantifier_macros.{cpp,h}`,
and added the necessary methods for inheritance from PreprocessingPass.

No need to add a test - regress0 fails when adding Assert(false) when assertions had changed.

Refactor nlExtPurify preprocessing pass (#1963)

Clean up quantifiers engine initialization. (#2371)

 Fix more simple coverity warnings (#2372)

 Remove spurious disabling of cbqi-all (#2368)

Add tests that enumerate and verify rewrite rules (#2344)

 Do not print internally generated datatypes in external outputs with sygus (#2234)

New C++ API: Add checks for kind arguments. (#2369)

This should hopefully also take care of the open coverity issues for cvc4cpp.cpp.

Add missing overrides in unit tests (#2362)

Replacing allocatedInCMM and d_noTrash with false everywhere in cdhashmap (#2355)

There do not appear to be any instances these can be positive.

Makes the filename be set in the SMT engine by default (#2366)

 Fixing some coverity warnings (#2357)

Fix regression requiring proof build. (#2364)

Refactor ITE simplification preprocessing pass. (#2360)

Use "filename" instead of "name" in SmtEngine::setInfo() (#2361)

global-negate preprocessing pass (#2317)

More regressions that increase coverage (#2354)

 More unused code elimination (#2358)

Generating less consistency lemmas in bv-ackermann preprocessing pass (#2253)

Wrapping TheorySetsPrivate in a unique_ptr. (#2356)