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.

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

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

Multiple fixes for datatypes theory solver: add support for parametric datatypes in type enumerator, fix infinite loop in type enumerator, fix fairness issue for splitting (moves constructor selection into model generation procedure), fixes bug 532, find conflict for constructor with conflicting label eagerly.  Add representive flattening for quantifiers (currently disabled). Other minor cleanup.

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

Adding example proof signatures for LFSC.

Added support for converting unsorted problems to multi-sorted problems via sort inference and monotonicity.  Minor cleanup.

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

Conflicts:
src/theory/strings/theory_strings.cpp

adds some fixes. it solves kaluza problems

Adding example proof signatures for LFSC.

Added support for converting unsorted problems to multi-sorted problems via sort inference and monotonicity.  Minor cleanup.

adds partial function substr. the use of this function should be guarded, especially for disequalities

adds partial function substr. the use of this function should be guarded, especially for disequalities

Fix a bug in smt2 parser for quantified formulas with attributes, fixes bug 535

replace with a new method for disequality, move to QF_S

add x=y

fixed a loop bug

Bug fixes and improvements for symmetry breaking, it now supports multiple sorts.  Working on monotonicity inference.

Some fixes to recent strings commits.

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

adds communication with arith engine

Add new symmetry breaking technique for finite model finding.  Improvements to bounded integer quantifier instantiation.

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

removes unsound cases, adds unrolling

fix the infinite issue

for morgan to see the regression problems

fix loop detection for multi-vars

optimizing model generation for strings

adds model generation for strings, and a hacked way in arith engine for models

removes unsound cases, adds unrolling

fix the infinite issue

for morgan to see the regression problems

Reduce compiler dependencies on substitutions.h,
Some new functionality in substitutions.h/cpp

Better fix for bug 528

fix loop detection for multi-vars

optimizing model generation for strings

adds model generation for strings, and a hacked way in arith engine for models

Revert Clark's last commit, at his request; there are some bugs.

This reverts commit 9775bced75843c6f01e9524c2d0e7021535e3ec0.

Cleaner version of bug-fix for 528, also moved substitutions.h out of theory.h
for faster compilation

Fix for bug 528

Support a personal build configuration and make rules.

Support for bv2nat/int2bv in parser and BV rewriter.

Fixes to theoryof-mode; no longer static in Theory class.

Fix (extraneous) command dumping.

Change default option of simple ite lifting within quantifier bodies.  add some debug messages.

Fix sat_proof "parentheses into the void" after conferring with Liana.

Move some regress benchmarks around that took too long, other test cleanup.

Documentation fixes, some code typo fixes, file perms, other minor things.

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

fix bug 534: portfolio define-fun duplicate model

Theory of strings.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>

Another minor fix for datatypes to repair my previous commit.

Add support for check-sat with argument.

Fix declare-datatypes dumping bug (bug 385).

Support per-command verbosity settings.

Support empty (and 1-ary) tuples and records.

Fix some line-numbering in auto-generated metakind.h.  Thanks to Martin Brain for reporting this.

Fix portfolio on bug411.smt2.  (get-model command should only go to last winner)

Ensure no cost for datatypes debugging when not tracing it.

Fix datatypes for bug 503

Fix FLOOR and DISTINCT in CVC language parser.

Fix lambda handling in CVC parser

Permit setOption(decision-mode)

Fix bugs/issues with missed-t-prop dump output

Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a segfault in smt2 printer

Add ability to mkConst(TupleSelect) and friends in language bindings

Merge branch '1.2.x'

bug 374 fix: assert litVal=desiredVal only for leaf nodes

Bug 374 benchmarks

Change recursive expandDefinitions() to an interative worklist-based one; we were blowing the stack.  Fixes a segfault reported by Pantazis Deligiannis.

--segv-nospin is now default.

Minor cleanup.

Minor fixes for --fmf-fmc for quantifiers containing datatypes

initial modifications for per-ic cbqi

Clean up "make install"-produced intermediate files (resolves bug 526)