string fmf changes

Fix Java destruction order issue; thanks to Zheng Manchun for reporting this bug.

Minor fix for swig bindings.

Merge remote-tracking branch 'CVC4root/master'

Substantial Changes:

-ITE Simplification
-- Moved the utilities in src/theory/ite_simplifier.{h,cpp} to ite_utilities.
-- Separated simpWithCare from simpITE.
-- Disabled ite simplification on repeat simplification by default. Currently, ite simplification cannot help unless we internally make new constant leaf ites equal to constants.
-- simplifyWithCare() is now only run on QF_AUFBV by default. Speeds up nec benchmarks dramatically.
-- Added a new compress ites pass that is only run on QF_LIA by default.  This targets the perverse structure of ites generated during ite simplification on nec benchmarks.
-- After ite simplification, if the ite simplifier was used many times and the NodeManager's node pool is large enough, this garbage collects: zombies from the NodeManager repeatedly, the ite simplification caches, and the theory rewrite caches.

- TheoryEngine
-- Added TheoryEngine::donePPSimpITE() which orchestrates a number of ite simplifications above.
-- Switched UnconstrainedSimplifier to a pointer.

- RemoveITEs
-- Added a heuristic for checking whether or not a node contains term ites and if not, not bothering to invoke the rest of RemoveITE::run(). This safely changes the type of the cache used on misses of run. This cache can be cleared in the future. Currently disabled pending additional testing.

- TypeChecker
-- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls.

- Theory Bool Rewriter
-- Added additional simplifications for boolean ites.

Minor Changes:

- TheoryModel
-- Removed vestigial copy of the ITESimplifier.
- AttributeManager
-- Fixed a garbage collection bug when deleting the node table caused the NodeManager to reclaimZombies() which caused memory corruption by deleting from the attributeManager.

- TypeChecker
-- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls.

-NodeManager
-- Added additional functions for reclaiming zombies.
-- Exposed the size of the node pool for heuristics that worry about memory consumption.

- NaryBuilder
-- Added convenience classes for constructing associative and commutative n-ary operators.
-- Added a pass that turns associative and commutative n-ary operators into binary operators. (Mostly for printing expressions for strict parsers.)

Array collectModelInfo fix for Andy

Adding the changes needed to delete rewriter attributes.  This includes being able to list attributes.  Additionally, added debugging hooks to node manager and attribute manager.

Changing the number of bits allocated per field in node values.

Bug fix for previous commit

Add fair strategy for finite model finding multiple sorts --uf-ss-fair.

Minor fixes for Mac OS Mavericks

Allow empty record literals (fixing an oversight in previous work on empty tuples/records)

Some patches to CVC3 compatibility layer tests; Thanks to Adam Buchbinder @ Google for the report and patch!

Datatype::getCardinality() caching

Add virtual destructors where missing

Some patches to CVC3 compatibility layer; Thanks to Adam Buchbinder @ Google for the report and patch!

Another build fix; the dust should be settled now.

Minor portfolio fixes for some platforms.

Some additional explanation for a common configure error.

lb change

add string progress measurements

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

add loop cache

add loop cache

Fix new-theory script for new, flattened build system.

Minor build system cleanup

length lemma is changed, var-split lemma is changed

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

Expanded usefulness of (set-info :cvc4-logic ...)

Some fixes to build system with dependency-tracking is off; should fix RPM/Debian builds.

Change exit status to be more consistent with other command-line tools: 0 success, nonzero error

Fix compat-java library naming on Mac OS; thanks to Zheng Manchun for reporting this issue

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

Fix "make distclean", which should fix some of the build issues from last night

Minor fixups to last commit

Flatten libcvc4 build structure; remove some #include interdependences

Fix "make distclean", which should fix some of the build issues from last night

Minor fixups to last commit

Flatten libcvc4 build structure; remove some #include interdependences

Adds the header file into makefile, solving building error; adds cache for derivative; disables loop detection when finite model finding is enabled.

Adds the header file into makefile, solving building error; adds cache for derivative; disables loop detection when finite model finding is enabled.

bug fix

change options

Bug fixes for bounded integer quantification.  Current best strategy is to turn off MBQI.  Disable relevant triggers by default.

bug fix

Bug fixes for bounded integer quantification.  Current best strategy is to turn off MBQI.  Disable relevant triggers by default.

change options

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

add seperate regular expression files

add seperate regular expression files

fixed proof regression script and added a new uf test case

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

Turn off model-based arrays (causing crashes in portfolio)

Fix for bug515

add back eager approach

bug fix for loop rule

bug fix

bug fixes: some issues remain, need more discussion later

remove nested re or; opt loop

string fix

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

add a string test case

bug fix for string special case

add a string test case

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

bug fix for string special case

adds regular expression range

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

adds regular expression range

adds regular expression range

minor fix to last commit (gitignore)

.gitignore personal configuration files

adds fmf for strings

renames for strings fmf

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

bug fix in strings : change from assert to  alwaysassert

removes some junks

performance optimizations for quantifier instantiation

bug fix in strings : change from assert to  alwaysassert

performance optimizations for quantifier instantiation

removes some junks

bug fix: string cache cleaning

add another regexp test

Adds Regular Expression support.

Adds regular expression support, it is actually CFL because of variables.

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

add constant membership

adds native regexp.

add constant membership

Minor bug fix to datatypes.

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

adds native regexp.

adds native regexp.

fixed options::proof() segfault

cleaned up proof code

fixed uf proof bug: now storing deleted theory lemmas

More improvements to datatypes, eager selector collapsing, improved collect model info. Also fix bug in model post-processor.

added currying for uf proofs; still needs debugging

fixed uf proof with holes bugs

Optimizations for datatypes theory.  There seems to be a bug in trans_closure, currently implemented a work around.