Enable ccache on Travis, disable debug symbols (#1094)

Enable ccache on Travis for faster compile times. Also
disable debug symbols for the debug builds on Travis to
use the available cache more efficiently. Note: this
change only works on GCC, support for Clang will require
additional changes but the time savings should already be
pretty significant.

Initial infrastructure for BV instantiation via word-level inversions. (#1056)

* Initial infrastructure for BV instantiation via word-level inversions.

* Minor clean up.

* Change visited to unordered set.

Adding reasonable breaks in switch statement in TheoryStrings::normalizeRegexp. Minor code reorganization and applying clang-tidy to the function. (#1079)

Addressing a coverity scan complaint in theory_strings.cpp. I believe the root cause is that d_normal_forms_exp[r[0]] could have referred to different vectors (as operator[] is inserting for maps). (#1080)

Ensure that expand definitions is called on all non-variable expressi… (#1070)

* Ensure that expand definitions is called on all non-variable expressions. In particular, it is necessary that the sets theory is notified when a set universe term occurs in the input to ensure options are set correctly. The commit moves this check from within check() to expandDefinitions(), and also adds the check for join image which relies on universe set. This fixes a bug reported by Arjun. Add and update regressions.

* Add comments concerning expandDefinitions

* Expand comment, move to .h

Properly handle user cardinality constraints for uf-ss=none. (#1068)

Fix link in configure.ac.

Remove support for conversions between uint32/uint16 and string. (#1069)

* Remove support for conversions between uint32/uint16 and string.

* Temporarily disable regression.

Add travis debug build with cln. (#1066)

Until now, all travis builds where built with gmp. This commit adds an additional debug build built with cln.

Add GCC7 jobs to Travis (#1054)

This commit adds two jobs (debug, with portfolio, test groups 0 and 1) to Travis.
Both jobs are added using matrix.include, based on the example in the documentation:
https://docs.travis-ci.com/user/languages/cpp/#GCC-on-Linux . This
unfortunately requires some code duplication but there does not seem to be a
way to do it in a much better fashion.

Replace CVC4_THREADLOCAL in interactive_shell (#1065)

Commit 546d795470ca7c30fc62fe9b6c7b8e5838e1eed4
caused our nightly builds to fail because it did
not replace CVC4_THREADLOCAL with
CVC4_THREAD_LOCAL in interactive_shell. This
commit fixes the issue and adds readline to
Travis, s.t. readline related code gets compiled
as part of our CI tests.

Answer unknown when uf-ss=no-minimal is combined with cardinality constraints from user input, add regressions. (#1060)

Use thread_local instead of compiler extensions (#210)

C++11 introduced the thread_local keyword, so we don't need to use
non-standard extensions or our custom pthread extension anymore.
The behavior was previously introduced as a workaround in commit
753a072c542c1c254d7c6adbf10e091ba585ede5. This commit
introduces the macro CVC4_THREAD_LOCAL that can be used to
declare variables as thread local. For Swig, this macro is defined to
be empty.

Fix model construction for parametric types (#1059)

Fix model construction for parametric types so that we enumerate types in order of dependencies, and avoid subterms of previously enumerated values.

There was a bug in model construction for parametric types which was related to enumerating values that are subterms of other previously enumerated values created during model construction (which were not recorded).

This commit adds all subterms of values we enumerate to the "already used value" sets of their respective types, as reflected in the changes to TypeSet.

There is an extra wrinkle in making the above change, which was caught by the regression test/regress/regress0/fmf/dt-proper-model.smt2. The issue is specific to finite model finding and can be corrected by ensuring that base types (e.g. uninterpreted sorts) are enumerated first.

The change to TheoryModel::buildModel that replaces "allTypes" with "type_list" fixes this wrinkle. This constructs a partially ordered list of types where T1 comes before T2 if values of T2 can contain terms of type T1 but not vice versa. Ordering our enumeration in this way is probably a good idea in general. This ensures we enumerate values for equivalence classes of e.g. Int before (Array Int Int) and means we exclude fewer intermediate values during model construction.

Remove Coverity SSL certificate workaround from Travis configuration. (#1058)

Coverity works without the SSL certificate workaround and is not needed anymore. Note that we don't require sudo anymore and we could switch to container-based Travis builds (instead of VM-based).  However, container-based environments only provide 4G of memory (instead of 7.5G for VMs) , which is not enough for the current CVC4 build environment.

Fix indentation for disabled Java tests.

Disable Java tests for now until they get fixed.

Run Ant on Travis

Travis: Package instead of download for cxxtest (#1055)

Before this commit, we were downloading cxxtest from Sourceforge. This commit
instead installs the Ubuntu package, which is easier and more reliable. Instead
of adding the package to the list of packages for Coverity and the common list
of packages, this commit changes the Coverity package list to just refer to the
common list of packages.

Move LFSC checker out of the CVC repository. (#222)

LFSC now lives outside of the CVC4 repository and is not part of the CVC4 distribution
anymore. As a consequence, we

+ Add --with-lfsc and --with-lfsc-directory as configure options.
   In the case where CVC4 has not been built with integrated LFSC, all code that interacts with
   LFSC is disabled.

+ Disable proof checking if CVC4_USE_LFSC is not defined.
   Configuring the build with --check-proofs but without --with-lfsc results in an error.

+ Do not call LFSC's cleanup function (but we should in the future).
   LFSC checker segfaults during cleanup on regression testcase regress0/bv/core/bitvec7.smt.
   Disabled call to lfscc_cleanup until the problem in lfscc is fixed.

+ Disable building with LFSC for the distcheck travis build since it is not part of the distribution
   anymore. Further, make distcheck with LFSC would require to call contrib/get-lfsc-checker
   before calling make check on the temp build (the build of the unpacked distribution tar ball).

Added missing includes (algorithm).

Algorithm was previously removed from src/util/regexp.h which broke
compilation on some platforms.

Test Java API on CI

Add include to fix build

Merge pull request #191 from timothy-king/cleanup-regexp

Cleaning up the CVC4::String class.

Fix typos

Removing TODO for 'Optimize via the iterator'. Not a priority. (#1051)

Cleanup: use Assert rather than C assert. (#1052)

Updated NYU -> Stanford

Change Bugzilla urls to Github issues.

Remove unused SubrangeBound(s) classes (#221)

As discussed in pull request #220, commit
360d6ee8d3cdd5ddb47c328043eaed3a107b8db1 mostly got rid of SubrangeBound(s).
There were still a few mentions of it left in the code, most of them commented
out. The occurrences in expr.i and expr_manager.i, however, created issues with
the Python wrapper. This commit removes the SubrangeBound(s) implementation and
other leftovers.

Add mbqi interleave option, change option fs-inst to fs-interleave.

Minimize includes in expr.h: remove dups, iostream (#219)

Move function definitions from metakind.h to cpp (#218)

Move function definitions from kind.h to kind.cpp (#217)

Move function defns from smt_engine_scope.h to cpp (#216)

Additionally, this commit removes unnecessary includes, adds includes to
smt_engine.h in files that require it and removes s_smtEngine_current from
smt_engine_scope.h.

Use antlr-3.4 directory if already present in CVC4 root directory (#213)

* Find antlr-3.4 directory if installed via contrib/get-antlr-3.4.

Merge pull request #214 from CVC4/fix_warn_nonlinear

Fix compiler warnings in theory/arith/nonlinear_extension.cpp

Build and test suite fixes for Windows (#186)

- Build fixes for Windows
- Make proof checking tempfile handling portable
- Test suite fixes for Windows

Fix compiler warnings in theory/arith/nonlinear_extension.cpp

Maintain frontier for tangent planes.

Fix line numbers in options_template

Fix compiler warning in src/context/context.h.

Fix help message for disable-unit-testing in configure.ac (don't -> do not)

Previous help message broke syntax highlighting in vim.

Remove AigBitblaster implementation if ABC is not compiled (#212)

* Guard use of AigBitblaster with CVC4_USE_ABC.

This removes the Unreachable() implementation of AigBitblaster in case CVC4 is
not compiled with ABC support.

Fix Assertion (compiler warning) in theory/bv/theory_bv.cpp

Fix compiler warning in sat_proof_implementation

Use cache for datatypes cycle check, add regression.

Merge pull request #211 from CVC4/fix_warn_sygus

Fix compiler warning in theory/quantifiers/term_database_sygus.cpp

Optionally split regression tests into test groups (#207)

To prevent timing out on Travis, this commit adds the option to split
the regression tests into groups and run each group in a separate job.
The group of a test is determined by computing a checksum of its name.

Fix compiler warning in theory/quantifiers/term_database_sygus.cpp

Change sygus output for failed reconstruction case.

Make quantifier elimination more robust to preprocessing.

Reorganized bitvector.h

Fix comments

Fix typos in comments

Set default language to smt lib 2.6 (including as a base language for sygus), update regressions.

Disable debug symbols for production builds.

Minor improvement for enumerative instantiation.

Fix memory leak in symbol table (#209)

Commit 4cab39bd4f166716cd3d357a175c346afb838137 moved d_exprMap, d_typeMap,
and d_functions into SymbolTable::Implementation but did not move the deletion
of those objects from SymbolTable to the SymbolTable::Implementation
desconstructor, resulting in a memory leak. This commit fixes the issue.

Change remaining hash_set -> unordered_set (#208)

The nightly competition build has been failing due to a remaining use of
hash_set in approx_simplex.cpp. This commit changes the remaining uses
of hash_set to unordered_set.
The remaining uses of hash_set were in LFSC. Switching to C++11 for LFSC
required changing the configure.ac for LFSC to require C++11 support to
make sure that it can be compiled independently from the rest of CVC4 (some
of our Travis tests do that as well). To have the macros for these additional
checks available, the commit adds a symlink to the files in config that contain
the macros). I did not find a way to add macros from a parent's folder that
did not break `make distcheck

Add support for charat in native language, minor cleanup.

Fix cache issues for cyclic string equations.

-Og for non-opt build, parallel pcvc4 check (#206)

-Og enables optimizations that do not interfere with debugging. This is the new
default for debug builds if the compiler supports the flag. This commit also
enables parallel checking for the portfolio build on Travis.

Use TEST_CPPFLAGS/TEST_CXXFLAGS to add path to CxxTest headers in configure.ac. (#200)

CxxTest headers were included in test/unit/Makefile.am as -I@CXXTEST@. However, in configure.ac if CXXTEST was not set by the user, it was initially set to `dirname "$CXXTESTGEN"` while determining the path to the header files. If CXXTESTGEN pointed to /usr/bin and if the headers were found in /usr/include, CXXTEST was not reset, which led to CXXTEST being replaced by /usr/bin in test/unit/Makefile.am. As a consequence, the locale binary in /usr/bin got included instead of the locale header file.

Disabling compiling unit tests with coverity scan for now.

Deprecating the unused convenience_node_builders.h (#203)

Consolidating the opaque pointers in SymbolTable. (#204)

* Consolidating the opaque pointers in SymbolTable. This removes details about the implementation from a public header.

* Removing the guard for SymbolTable for the move constructor.

Merge branch 'master' into cleanup-regexp

Moving from the gnu extensions for hash maps to the c++11 hash maps

* Replacing __gnu_cxx::hash_map with std::unordered_map.
* Replacing __gnu_cxx::hash_set with std::unordered_set.
* Replacing __gnu_cxx::hash with std::hash.
* Adding missing includes.

Fix a few bugs related to sygus.

Removing the unused CDAttribute. This makes CDHashMap::obliterate unused. Removing it as well.

Fix simple_vc_compat_cxx example (#202)

The CVC3 compatibility layer was broken because it was setting
simplification mode to SIMPLIFICATION_MODE_INCREMENTAL, which
is not supported anymore since commit
2dbe1f150d30f0fb0c8522f891104270ce09db4c . This commit changes
the compatibility layer to not set the option anymore.

This addresses bug 833, which had been reported on the cvc-bugs mailing list.

Adding a garbage list that get collected during the ~Scope. Removing the CDHashMap garbage.

Fixing the order of the comparison operation.

Merge branch 'master' into cleanup-regexp

Use is_sorted, merge, copy from std (#199)

Previously, we were checking whether we should use is_sorted
from std or __gnu_cxx. With C++11, std::is_sorted is
guaranteed to exist. This commit changes
arith/normal_form.{h,cpp} to always use std::is_sorted and
also removes the custom implementations for merge and copy by
using the std implementations instead.

Remove PtrCloser (#198)

With C++11, we don't need PtrCloser anymore because we can
just use std::unique_ptr.

Moving to static_assert now that c++11 is available.

Use CXXFLAGS when compiling parsers (#197)

ANTLR generates C files that we compile with the C++ compiler.
To do so, we set CC=CXX in the `Makefile.am`s of the parsers.
Previously, we did not copy the CXXFLAGS to the CFLAGS, which
could result in problems, e.g. when using -std=gnu++11 in the
CXXFLAGS, compiling the parsers would fail if they used C++11
features (configure.ac usually modifies CXX to include the
-std=gnu++11 flag but if it is included in CXXFLAGS, the CXX
is not changed).

Fix warning about unknown escape sequence (#196)

Disable separate gnu++11 tests on Travis (#193)

Given that we are now always compiling with gnu++11, we don't need
separate tests anymore.

Removing BOOST_FOREACH usage.

Cleaning up the CVC4::String class.

Merge pull request #188 from aniemetz/cx11

autoconf: make -std=gnu++11 mandatory

autoconf: make -std=gnu++11 mandatory

Fix unit tests for subranges. Fix destructors for context objs in unit tests.

Fix .i files from last commit.

Make type rules more strict for operators whose type rules involve subtypes. Disable support for subrange and predicate subtypes (which were only partially supported previously).

Remove trailing slashes from directories if specified via command line.

Do not exit when value/model/unsat-core/proof is requested at wrong time, for bug 831.

Add nl regression.

Merge ntExt branch. Adds support for transcendental functions. Refactoring of non-linear extension. Add factoring lemma scheme for non-linear. Add regressions.

Separate sygus term utilities to new file, minor cleanup from last commit.

Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.

Prerelease versioning for master.

Cutting release 1.5.

Disable tarball signing for now.

Merge branch 'master' of github.com:CVC4/CVC4

Update copyright year and refer to authors URL.

Remove unused stacking_vector class (#185)