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)

Fix option for real2int regression. (#2353)

Adds regression test for automatic generation of SyGuS BV grammars (#2345)

Fix invalid iterator comparisons (#2349)

 Fix processing of nested Variable construct in sygus let bodies (#2351)

Removing unused bool members in command.cpp. Also initializes a bool member. (#2321)

Warn and enable quantifiers when using sygus + logics with QF (#2352)

Makes the new row propagation system default (#2335)

Move d_realAssertionsEnd from SmtEnginePrivate to AssertionPipeline. (#2350)

Add constexpr annotations to help coverity understand constant ... (#2314)

Use cbqi-full for sygus (#2346)

Remove support for *.expect files in regressions (#2341)

Currently, we can optionally specify an *.expect file with the metadata
of a regression test. This commit removes that option because it was not
widely used, adds maintenance overhead and makes the transition to a new
build system more cumbersome. Regression files can still be fed to a
solver without removing the metadata first since they are in comments of
the corresponding input format (note that this was not always the case,
it changed in efc6163629c6c5de446eccfe81777c93829995d5).

Fix initialization of d_smt in ValidityChecker for changes from #2240. (#2343)

Remove disabled system test cvc3_george. (#2342)

Disabled since 6 years, @mdeters commented when disabling it that it takes a very long time to build, see 868ee6d.

More unused code elimination (#2339)

 Remove support for prototype (non-sygus) synthesis (#2338)

Add regressions that increase coverage (#2337)

Minor improvements to the interface for sygus sampler (#2326)

 Make sygus inference a preprocessing pass (#2334)

run-regress script: Exit with exit code > 0 on failure. (#2336)

This is in preparation for migration to cmake since ctest determines failure via exit code.

Remove support for flipDecision (#2319)

Remove miscellaneous unused code (#2333)

 Add sygus stream regressions (#2330)

Split sygus grammar to its own ANTLR grammar (#2307)

 Fix spurious warning in sort inference (#2331)

 Fix arithmetic division by zero in sygus repair constant module (#2329)

 Eliminate partial operators in sygus grammar normalization (#2323)

This corrects a bug that was introduced in #2266 (the hack removed there was necessary).

This ensures that we handle operators like bvudiv, bvsdiv, bvurem, div, rem, / properly in sygus.

This also enables total semantics for BV div-by-zero for sygus.

 Initialize inputAssertions only when proofRecipe is non-null (#2325)

Most of the PR is clang-format cruft from picking up the contents of a PROOF({ ... });

Refactor eager atoms preprocessing pass. (#2318)

cleaning unnecessary timers/dumps (#2327)

Adding support for bitvector SyGuS problems without grammars (#2328)

Make quantifiers-preprocess preprocessing pass (#2322)

Removing coverity warnings from theory_sep.cpp (#2320)

Refactor IteRemoval preprocessing pass (#1793)

This commit refactors the IteRemoval pass to follow the new format.
In addition to moving the code, this entails the following changes:

- The timer for the ITE removal is now called differently (the default
  timer of PreprocessingPass is used) and measures just the
  preprocessing pass without applySubstitutions(). It also measures the
  time used by both invocations of the ITE removal pass.
- Debug output will be slightly different because we now just rely on
  the default functionality of PreprocessingPass.
- d_iteRemover is now passed into the PreprocessingPassContext.
- AssertionPipeline now owns the d_iteSkolemMap, which makes it
  accessible by preprocessing passes. The idea behind this is that the
  preprocessing passes collect information in AssertionPipeline and
  d_iteSkolemMap fits that pattern.

Move node algorithms to separate file (#2311)

Minor fixes and improvement for sygus to builtin. (#2306)

Refactor extended rewriter preprocessing pass (#2324)

Refactor apply2const (#2316)

Switching an Assert to a CVC4_CHECK to test if it resolves CID 1459595. (#2315)

Removing attribute cleanups. (#2300)

* Removing attribute cleanups.

Add contrib/get-gmp script. (#2292)

Remove unused tuple classes (#2313)

Since we are using C++11, we can replace the triple and quad classes
with std::tuple.

Remove unused class DynamicArray (#2312)

Make sort inference a preprocessing pass (#2309)

Fix dumping of get-unsat-assumptions (#2302)

When dumping a `get-unsat-assumptions` command, CVC4 was instead dumping
two `get-unsat-cores` commands. This commit splits
`SmtEngine::getUnsatCores()` into a part that does the dumping and an
internal part that actually gets the unsat core without dumping.
`SmtEngine::getUnsatAssumptions()` now calls the internal version to
avoid the redundant dumping of a `get-unsat-cores` command and changes
the command that gets dumped in `SmtEngine::getUnsatAssumptions()`.

Remove unused declaration (#2310)

autotools: Remove personal builds, rename build 'default' to 'testing'. (#2303)

Fix get-unsat-assumptions output (#2301)

Fixes #2298. The `get-unsat-assumptions` command was printing the result
with square brackets and commas instead of parentheses and spaces
between the assumptions.

Removing support for T* and const T* attributes. (#2297)

* Removing support for T* and const T* attributes. These are unused.

Make attributes robust to static init orderings (#2295)

@taking pointed out that part of the issue fixed in #2293 is also that
we should be more robust to different (de-)initialization orders. A
common, portable way to achieve this is to allocate the object in
question on the heap and make the pointer to it static [0]. This commit
fixes the variable in question.

I have tested this fix in ASAN (without using --no-static-init flag for
CxxTest) and it works.

[0] https://isocpp.org/wiki/faq/ctors#construct-on-first-use-v2

Fix portfolio command executor for changes from #2240. (#2294)

Do not use static initialization in CxxTest runner (#2293)

The static initialization in the CxxTest runner was causing problems
when having `std::unique_ptr`s in test classes. When the ExprManager's
deconstructor is called, we count on certain static objects to be around
(e.g.
https://github.com/CVC4/CVC4/blob/0a02fd2b69c0c0f454fc33d8028b24f4fcf431de/src/expr/attribute_internals.h#L508).
If the ExprManager is (indirectly) owned by a `std::unique_ptr` in a
static class, however, there are no such guarantees as the destruction
order of static objects is not defined. This commit adds a flag for
CxxTest to not use static initialization in the test runner, which
solves the issue.  Additionally, the commit fixes a warning about a
missing virtual deconstructor in ParserBlack that came up after using
the new flags.

This fixes an issue reported in the nightly builds.

 Fix char overflow issues in regular expression solver (#2275)

Fix documentation of regression tests (#2290)

Plug solver API object into parser. (#2240)

Fixing documentation nit from PR#2232. (#2289)

 Proposal for adding map utility functions to CVC4. (#2232)

* Proposal for adding map utility functions to CVC4.

Disable argument relevance for sygus by default (#2288)

Add debug test for sygus subcall verify calls. (#2287)

Move uf model code from uf to quantifiers (#2095)

Do beta-reduction in expandDefinitions (#2286)

Require Swig 3 (#2283)

Removes some hacks due to Swig 2's incomplete C++11 support and adds
checks for version 3 at configuration time as well as in swig.h

Simplify and improve the sygus parser (#2266)

Currently, there is code duplication for parsing constants in sygus grammars, e.g.:
https://github.com/CVC4/CVC4/blob/master/src/parser/smt2/Smt2.g#L1048
https://github.com/CVC4/CVC4/blob/master/src/parser/smt2/Smt2.g#L2304

This PR removes this duplication by introducing a new ANTLR grammar "termAtomic" in Smt2.g.

As a result of this PR, we now parse sygus grammars with any constant we otherwise parse. This addresses known issues where CVC4 rejects grammars with floating point constants.

It also removes some unnecessary code for converting builtin kinds to their total versions.

This is work towards #2197.  We still do not support sygus grammars with non-trivial *composite* terms, such as applications of indexed function symbols.

Document/refactor datatypes sygus simple symmetry breaking (#2233)

 Fix simple reg exp consume rewrite (#2281)

Delete functions instead of using CVC4_UNDEFINED (#1794)

C++11 supports explicitly deleting functions that should not be used
(explictly or implictly), e.g. copy or assignment constructors. We were
previously using the CVC4_UNDEFINED macro that used a compiler-specific
attribute. The C++11 feature should be more portable.

 Wait to do sygus qe preprocess until full effort check  (#2282)

Fix inference of pre and post conditions for non variable arguments. (#2237)

Make output of flushInformation and safeFlushInformation consistent. (#2280)

Add rewrite for nested BITVECTOR_ITE that can be merged. (#2273)

Make flat form inferences optional in strings (#2277)

Add RegLan to smt2/sygus parsers. (#2276)

 Move sygus quantifier elimination step for non-ground-single-invocation to sygus (#2269)

Remove support for Enum sygus syntax. (#2264)

Fixes for sygus inference (#2238)

This includes:
- Enabling sygus-specific options in SmtEngine::setDefaults,
- Disabling a variant of miniscoping (triggered by many chc-comp18 benchmarks),
- Treating free constants as functions to synthesize

 Fixes and improvements for single invocation inference (#2261)

Fix degenerate case of sygus grammar construction for 0-argument Bools (#2260)

 Add rewrite for nested BITVECTOR_ITE with cond_outer == cond_inner. (#2272)

Add rewrite for BITVECTOR_ITE with const children. (#2271)

Add rewrite for BITVECTOR_ITE with term_then == term_else. (#2268)

Eliminate option for sygus UF evaluation functions (#2262)

Fix printing statistics in case of signals. (#2267)

 Add timer for BV inequality solver. (#2265)