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.

More improvements to strings rewriter for regexps, contains, indexof, replace and others.  Enable non-recursive flat form inferences in strings theory solver. Refactor extf reductions. Use non-constant length terms when checking length equality. Add option --strings-eager-len.

Fixes related to explanations for cycles, sym inferences. Minor fixes and improvements.

Improvements to rewriter for regexp, contains, indexof. Improvements and fixes for reduction of indexof. Fixes bugs 612 and 615. Fix bug in find+offset in strings util. Add regressions.

Evaluate extended operators on partially concrete arguments. More aggressive rewriting. Bug fix explanations for inferences. Avoid spurious cardinality splits. Do not do disequality splits for non-disequal terms. Work towards non-recursive handling of flat forms.

More improvements to strings. More aggressive inference of constant eqc, reductions based on congruence, precheck for cycles.

Refactor strings, bug fix inferences vs lemmas.

Fix for fmf+incremental. Restrict cbqi to literals from ce body.  Add regressions.

Improve quantifiers engine wrt incremental presolve. Add regressions.

Minor fix

Minor fixes to strings, add regressions.

Add missing regression

Fix bug for trivial extf inferences in strings. Improve caching for splits in strings. Other improvements.

Improved handling of extended operators.  Do preprocess on memberships eagerly, only process contains/memberships that have non-constant arguments.  Cleanup.

Lazy preprocessing of extended operators in strings.  Add regressions. Fixes bug 613.

Better organization of quantifiers modules, promote full saturation to module. Add heuristics for cbqi LIA instantiation with coefficients.

Clear term caches for quantifiers + incremental, fixes bug 674.  Refactoring of term database, other refactoring. Bug fixes for cbqi+datatypes.

Counterexample-guided instantiation for datatypes.  Make sygus parsing more liberal.

Improve ITE redundant branch elimination in quantifiers.

Fix for sets segfault (reported by Ravi Kandhadai)

fix involves sets getModelValue handling the case when element theory
doesn't have model

Fix bug in quantifiers engine where model construction could be skipped.

More work mixing UF and sygus.

Allow most smt2 commands as sygus commands. Fix bug in fmf-fun regarding quantified formulas with non-constant polarity.

Add option --fmf-fun-rlv, remove deprecated option --axiom-inst.

Fix bug related to quantifiers + incremental, thanks John Backes for the bug report.  Other minor cleanup.

Minor cleanup related to codatatypes.

Models for codatatypes. Fixes bug 662.

Normalization of codatatype constants, codatatype now has a fair enumerator.

Fix bug 670.  Minor.

Fix bug in strings rewriter regarding lengths of substr terms.

Working towards a fair enumerator for codatatypes.

Improve quantifiers rewriter, minor refactoring.

Working fix for bugs 610 and 643 regarding check-model with preprocessed quantified formulas.

Fix bugs related to fmf with incremental. Reinitialize sorts on user pop, bug fix enumeration for uninitialized sorts, do not decide combined cardinality constraints that have not been allocated in user context. Fixes bug 654.

Fix bugs 605 and 667.

fix regressions

Merge remote-tracking branch 'origin/master'

Fixed but with getAssertions

Minor improvement to sygus sol reconstruction.