Shuffling around public vs. private headers
- Adding a script contrib/test_install_headers.h that tests whether one can include all cvc4_public headers. CVC4 can pass this test after this commit.
- Making lib/{clock_gettime.h,ffs.h,strtok_r.h} cvc4_private.
- Making prop/sat_solver_factory.h cvc4_private.
- Moving the expr iostream manipulators into their own files: expr_iomanip.{h,cpp}.
- Setting the generated *_options.h files back to being cvc4_private.
-- Removing the usage of options/expr_options.h from expr.h.
-- Removing the include of base_options.h from options.h.
- Cleaning up CPP macros in cvc4_public headers.
-- Changing the ROLL macro in floatingpoint.h into an inline function.
-- Removing the now unused flag -D__BUILDING_STATISTICS_FOR_EXPORT.

Adding a missing header include for cvc4_assert.h in smt_engine_check_proof.cpp for when proofs are disabled.

Merged my changes from experimental branch (new array decision procedure,
translation to bit-vectors for QF_NIA).

Changing the attribute on the forward declaration of SetType in emptyset.h. This seems to give many fewer warnings.

Adding a missing return on the new ArrayStoreAll::operator= .

Miscellaneous fixes
- Splitting the two instances of CheckArgument. The template version is now always defined in base/exception.h and is available in a cvc4_public header. This version has lost its variadic version (due to swig not supporting va_list's). The CPP macro version has been renamed PrettyCheckArgument. (Taking suggestions for a better name.) This is now only defined in base/cvc4_assert.h. Only use this in cvc4_private headers and in .cpp files that can use cvc4_private headers. To use a variadic version of CheckArguments, outside of this scope, you need to duplicate this macro locally. See cvc3_compat.cpp for an example.
- Making fitsSignedInt() and fitsUnsignedInt() work more robustly for CLN on 32 bit systems.
- Refactoring ArrayStoreAll to avoid potential problems with circular header inclusions.
- Changing some headers to use iosfwd when possible.

Enabled array propagation during lemma propagation - this should catch some
conflicts that now require extra splitting.

Added extract.cpp example

Bug fix uf-ss-totality.

Always split on constructor types for datatypes involving uninterpreted sorts when finite model finding is enabled, add regressions.

Bug fix for cbqi, do not use model values for terms involving non-enumerable sorts.

Modifying emptyset.h and sexpr. Adding SetLanguage.

- Modifies expr/emptyset.h to use SetType only as an incomplete type within expr/emptyset.h. This breaks the include cycle between expr/emptyset.h, expr/expr.h and expr/type.h.
- Refactors SExpr to avoid a potentially infinite cycle. This is likely overkill, but it works.
- Moving Expr::setlanguage and related utilities out of the Expr class and into their own file. This allows files in util/ to know the output language set on an ostream.

Minor

Removing the Record iterator from the swig interface. Moving the cvc4 autogen include in interactive_shell.cpp.

Work on purification for quantifiers, minor updates.

Breaking the include cycle between Record and Expr.

Adding destructors for CDO an CDOhash_map in the restore() functions.

Removing the build cycle for predicate.

Moving SExpr(bool) out of the header into sexpr.cpp to be less verbose about the warning.

Making logic_info_forward.h a public header for now.

Add option uf-ss-fair-monotone. Minor cleanup and improvement of sort inference.

Refactoring Options Handler & Library Cycle Breaking

What to Know As a User:
A number of files have moved. Users that include files in the public API in more refined ways than using #include <cvc4.h> should consult which files have moved. Note though that some files may move again after being cleaned up. A number of small tweaks have been made to the swig interfaces that may cause issues. Please file bug reports for any problems.

The Problem:
The build order of CVC4 used to be [roughly] specified as:
  options < expr < util < libcvc4 < parsers < main
Each of these had their own directories and their own Makefile.am files. With the exception of the util/ directory, each of the subdirectories built exactly one convenience library. The util/ directory additionally built a statistics library. While the order above was partially correct, the build order was more complicated as options/Makefile.am executed building the sources for expr/Makefile.am as part of its BUILT_SOURCES phase. This options/Makefile.am also build the options/h and options.cpp files in other directories. There were cyclical library dependencies between the first four above libraries. All of these aspects combined to make options extremely brittle and hard to develop. Maintaining these between clang versus gcc, and bazel versus autotools has become increasing unpredictable.

The Solution:
To address these cyclic build problems, I am simplifying the build process. Here are the main things that have to happen:
1. util/ will be split into 3 separate directories: base, util, and smt_util. Each will have their own library and Makefile.am file.
2. Dependencies for options/ will be moved into options/. If a type appears as an option, this file will be moved into options.
3. All of the old options_handlers.h files have been refactored.
4. Some files have moved from util into expr/ to resolve cycles. Some of these moves are temporary.
5. I am removing the libstatistics library.

The constraints that the CVC4 build system will eventually satisfy are:
- The include order for both the .h and .cpp files for a directory must respect the order libraries are built. For example, a file in options/ cannot include from the expr/ directory. This includes built source files such as those coming from */kinds files and */options files.
- The types definitions must also respect the build order. Forward type declarations will be allowed in exceptional, justified cases.
- The Makefile.am for a directory cannot generate a file outside of the directory it controls. (Or call another Makefile.am except through subdirectory calls.)
- One library per Makefile.am.
- No extra copies of libraries will be built for the purpose of distinguishing between external and internal visibility in libraries for building parser/ or main/ libraries and binaries. Any function used by parser/ and main/ will be labeled with CVC4_PUBLIC and be in a public API. (AFAICT, libstatistics was being built exactly to skirt this.)

The build order of CVC4 can now be [roughly] specified as
  base < options < util < expr < smt_util < libcvc4 < parsers < main
The distinction between "base < options < util < expr" are currently clean. The relationship between expr and the subsequent directories/libraries are not yet clean.

More details about the directories:

base/
The new directory base/ contains the shared utilities that are absolutely crucial to starting cvc4. The list currently includes just: cvc4_assert.{h,cpp}, output.{h,cpp}, exception.{h,cpp}, and tls.{h, h.in, cpp}. These are things that are required everywhere.

options/
The options/ directory is self contained.
- It contains all of the enums that appear as options. This includes things like theory/bv/bitblast_mode.h .
- There are exactly 4 classes that handled currently using forward declarations currently to this: LogicInfo, LemmaInputChannel, LemmaOutputChannel, and CommandSequence. These will all be removed from options.
- Functionality of the options_handlers.h files has been moved into smt/smt_options_handler.h. The options library itself only uses an interface class defined in options/options_handler_interface.h. We are now using virtual dispatch to avoid using inlined functions as was previously done.
- The */options_handlers.h files have been removed.
- The generated smt/smt_options.cpp file has been be replaced by pushing the functionality that was generated into: options/options_handler_{get,set}_option_template.cpp . The non-generated functionality was moved into smt_engine.cpp.
- All of the options files have been moved from their directories into options/. This means includes like theory/arith/options.h have changed to change to options/arith_options.h .

util/
The util/ directory continues to contain core utility classes that may be used [almost] everywhere. The exception is that these are not used by options/ or base/. This includes things like rational and integer. These may not use anything in expr/ or libcvc4. A number of files have been moved out of this directory as they have cyclic dependencies graph with exprs and types. The build process up to this directory is currently clean.

expr/
The expr/ directory continues to be the home of expressions. The major change is files moving from util/ moving into expr/. The reason for this is that these files form a cycle with files in expr/.
- An example is datatype.h. This includes "expr/expr.h", "expr/type.h" while "expr/command.h" includes datatype.h.
- Another example is predicate.h. This uses expr.h and is also declared in a kinds file and thus appears in kinds.h.
- The rule of thumb is if expr/ pulls it in it needs to be independent of expr/, in which case it is in util/, or it is not, in which case it is pulled into expr/.
- Some files do not have a strong justification currently. Result, ResourceManager and SExpr can be moved back into util/ once the iostream manipulation routines are refactored out of the Node and Expr classes.
- Note the kinds files are expected to remain in the theory/ directories. These are only read in order to build sources.
- This directory is not yet clean. It contains forward references into libcvc4 such as the printer. It also makes some classes used by main/ and parser CVC4_PUBLIC.

smt_util/
The smt_util/ directory contains those utility classes which require exprs, but expr/ does not require them. These are mostly utilities for working with expressions and nodes. Examples include ite_removal.h, LemmaInputChannel and LemmaOutputChannel.

What is up next:
- A number of new #warning "TODO: ..." items have been scattered throughout the code as reminders to myself. Help with these issues is welcomed.
- The expr/ directory needs to be cleaned up in a similar to options/. Before this happens statistics needs to be cleaned up.

Add option fmf-empty-sorts.

Reverting a previous change to the options_handlers.h. Using inline defintions again to better handle a circular dependency.

Removing the generated directory from the parsers.

Modifying the src/options/Makefile.am for travis.

Modifying options/Makefile.am to pass distcheck. There is an unpleasant hack in this fix.

Adds Google, Inc. to the AUTHORS file.

Minor fixes for cegqi-si-partial.

Separating the steps of the old mkoptions script into smaller phases.

Guarding the destruction of the a linux specific variable on WIN32.

Merge pull request #79 from CVC4/fix-mac-build-script

Adds required steps to contrib/mac-build.

Adds attempt to download config.guess to get-antlr-3.4 script.

This should work around the case where autogen.sh hasn't been run,
as long as the download succeeds.

Reverts addition of autogen.sh to mac-build script.

The file autogen.sh isn't present in dist tarballs so this will
break some users.

More work on --cegqi-si-partial, incomplete.

Initial work on --cegqi-si-partial, refactoring.

Adds required steps to contrib/mac-build.

autogen.sh must be run before get-antlr-3.4 or it fails with
    I need the file config/config.guess to tell MACHINE_TYPE

autogen.sh can't run unless the autoconf, automake and libtools
MacPorts packages are installed.

Update to new implementation of single invocation partition by default.

Front-end support for get-value of sort cardinality, minor fixes for sygus solution reconstruction.

Infrastructure for partially single invocation properties. Bug fix for unconstrained functions in sygus solver.

Adding a missing delete to smt2_compliance.

Adding a missing delete to InstStrategyCegqi destructor.

Isolating the dependencies on CVC4_ANTLR3_OLD_INPUT_STREAM. Also freeing more memory for antlr input.

Switching travis over to using the containers infrastructure.

Freeing memory allocated for signal handling.

Option for midpoints in cbqi.

Improve relevant domain computation for arithmetic, full saturation strategy. Simply E-matching trigger selection, do not use non-trivial triggers unless necessary. Add option to strings.

Updating the contrib/new-theory script and travis to use the new Makefile.theories script.

Updating the contrib/new-theory script and travis to use the new Makefile.theories script.

Minor fixes and improvements to purify quant, relational triggers.

Minor fixes to cbqi, purify-quant. Better error checking in addInstantiation.

Fix infinite loop in datatype enumerator. Minor fixes and improvements to cbqi, full saturate. Add option --purify-quant. Use disequality triggers when using relational triggers. Add regressions.

Replacing an inefficient use of std::find(...) to use std::set's find() instead.

Changing file permissions to add or remove executable tag as appropriate.

Merging the google branch back into master.

Fixes some initialization and desctruction problems in quantifiers. Also restricts the desctructors of some components to not throw exceptions for pickier compiliers. Also changes some formatting of regression scripts.

This commit slightly generalizes the scripts for generating the _tags files.

Better combination of UF with cbqi, refactor quantifiers intialization.

Fixing typo.

Adding a test to ensure the <build>/src/theory directory is available to the scripts in src/Makefile.am. This should fix a bug in building the debian packages.

Improvements to handling of mixed Int/Real quantifiers.

Removes an extra dollar sign from src/options/mktagheaders. The extra dollar sign came in as a copy paste from a Makefile. This was not proper bash.

Adding the new mkdirs script to EXTRA_DIST. This should fix the failing nightly distcheck.

This commit fixes a bug related to a public header depending on a compiler flag. This resulted in user code seeing a different size for the SmtEngine class than what was compiled in the library. Proofs are enabled by default again. See cvc4.cs.nyu.edu/bugs/show_bug.cgi?id=688 for more information.

This commit removes using absolute paths in the generation of the .subdirs file. This also rearranges generation of the file so that one .subdirs file is generated once per Makefile.am file. This keeps using relative paths clean.

This commit moves the scripts for building the Debug_tags, Traces_tags, Debug_tags.h and Trace_tags.h out of options/Makefile.am and into seperate scripts. This also enables these files always being created.

This fixes a one definition rule violation for reduceDB_lt in Solver.cc in minisat and bvminisat. This also moves BVMinisat into CVC4. This also wrapped code in cpp files into the namespaces instead of having using namespace *.

Promote InstStrategyCbqi to quantifier module. Cleanup unused code.

Extend counterexample-guided instantiation to extended theory of Int/Real, mixed Int/Real. Bug fixes. Updates to quantifiers rewriter.

Revert "Default builds are now proof enabled."

This reverts commit 4fd18dee3156a6dd1903b95662034d6e996ff88b.

Fixes related to string contains.

This removes a bug for reading data that has been popped from the back of a vector using a stale reference in the unconstrained simplifier.

Specify that the default initialization must always be done for CDOhash_map's data field. Without doing this, there exists a loop where uninitialized data can be read. This can happen if T is a type like bool. The trace goes: CDOhash_map::set(data) calls ContextObj::make_current(). Now (d_pScope->isCurrent()) is false. So ContextObj::make_current() calls ContextObj::update(). ContextObj::update() calls CDOhash_map::save(). CDOhash_map::save() calls return new(pCMM) CDOhash_map(*this) which calls the copy constructor which reads the data using d_data(other.d_data).

Switching Options::current() to return a pointer. This helps avoid undefined behavior due to dereferencing a null pointer in the future.

Changes configure.ac so that the single recurisve invocation runs with a relative path. This lets the @srcdir@ variable in configuration be a relative path.

This patch slightly generalizes how the std::isfinite function in <cmath> is referred.

Enable counterexample-guided quantifier instantiation by default for quantified logics that include at least one relevant theory. Enforce restriction on model building to last call. Update options, refactor. Update regressions.

Minor refactoring in strings related to length.

Refactor strings, remove old cycle checks in normalize eqc.

Clean up explanations involving string length. Add regression.

Improve stratification of strings extended function reductions, add regressions. Eliminate preprocess for regexp.

Improve regexp rewriter, simplify regexp preprocess, add basic trans closure for string contains, refactoring.

Fix for no condense func values.

Add option to interleave enumerative instantiation with other strategies.

Throw error for recursively defined types involving Boolean.

Fix for codatatype constant rewrite, add regression.

Fix congruence check in strings, fixes bug 686.

Change semantics of str.substr to allow endpoint out of bounds, and return empty string for error conditions. Improve rewriter for str.substr.

Decompose string contains, minor refactoring.

Merge pull request #77 from kbansal/macsegfault

remove options infrastructure code which depended on undefined behavior

remove options infrastructure code which depended on undefined behavior

appears to be source of crashes on mac

Merge pull request #76 from CVC4/proofs

Proofs

fix regression tests, support fallback mode for proofs

Default builds are now proof enabled.

Fix strings preprocessing + incremental, fixes bug 682. Add initial infrastructure for str.contains inferences.

Temporary reverting commit 477e72b (proofs as default build) until we fix nightly builds.

Minor improvements to strings. Refactor rewriter. Enable fairness for multiple sorts in UF finite model finding by default.

Default builds are now proof enabled.

Disabled donePPSimpITE when unsat-cores are enabled (fixes bug648)

Minor improvements, add endpoint eq inference to strings.