More complete guess instantiation strategy, cvc4 now typically times out instead of answering unknown for benchmarks with quantifiers.  Modified regressions accordingly.  Minor fix for QCF regarding variable ordering.  Improved relevant domain computation.  Minor optimization for --mbqi=fmc

Minor fix for previous commit

Oops.. premature push on lexer fix (remove debugging output)

Fixes for escape-handling for string literals in SMT-LIBv2 lexer

Bug fix for theory strings related to old cycle detection code (was leading to bogus model).  Minor cleanup of QCF.

Do not use transitive closure module for cycle detection in datatypes (was bottleneck).

Add variable ordering for QCF to accelerate matching procedure.  Preparing for QCF_MC mode.

Handle nested (universal) quantifiers in QCF algorithm.  Make relevant domain instantiation breadth-first.

Substr fix: (= (str.substr "" 0 3) "xxx") should be SAT in the defintion of SMT-Lib

Refactor QCF slightly.  Bug fix for relevant domain (non-ground terms were added).  Bug fix for QCF (was missing instantiations due to not using getRepresentative).

stats for eq/diseq splits

another name change

change string stats text names

adds stats

roll back to uf implementation for substr and charat

add prefixof, suffixof

merge internal and user of charat & substr into one

More optimizations of quantifier instantiation data structures.

Merge branch '1.3.x'

URL update

More optimization of QCF and instantiation caching.  Fix CDInstMatchTrie.

More optimization of QCF.  Fixed InstMatchTrie for caching instantiations.  Use non-context dependent cache for instantiations when not incremental.  Instantiate from relevant domain when no other instantiations apply.  Minor cleanup of relevance for triggers.

replace charat uf with internal one

minor fix, indexof rewriter opt

fix: indexof, replace rewriting

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

rev diseq

rev const split

optimize for the reverse direction

rev diseq

rev const split

Simplify the QCF algorithm by more aggressive flattening, removes EqRegistry approach.  Minor change to quantifier macros.  Add option --quant-cf-mode.

optimize for the reverse direction

fix: constants are inferred to be the same

minor fix

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

Some minor fixes to SmtEngine strings settings.

commented out all_supported in strings for now, it has a bug here.

solve string exp issue for regexp

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

Conflicts:
src/smt/smt_engine.cpp

add warning for using strings in ALL_SUPPORTED

Smarter options, but still have a bug

Delay QuantifiersEngine and UF strong solver initialization until after final options/logic are set.

Smarter options, but still have a bug

improve string contains

improve string contains

Fixed non-termination issue in bounded integers.

Performance optimization for E-matching, working on using QCF module for propagations.

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

strings with new ideas

Merge branch '1.3.x'

Fix for quote-escaping in smt2 printer

strings with new ideas

More optimizations for quantifiers conflict find.  Add trust user patterns mode.

Merge branch '1.3.x'

enable search for html doc

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

Conflicts:
src/printer/smt2/smt2_printer.cpp

adds partial functions

adds smt2 print for strings

adds smt2 print for strings

Optimizations for quantifiers conflict find: better caching, process matching constraints eagerly.

normal form breaking

add repalce

Add stats to quantifiers conflict find.  Added option for qcf.  Working on handling non-APPLY_UF terms.

Add new method --quant-cf for finding conflicts eagerly for quantified formulas.  This module can efficiently determine when there exists a conflict wrt quantified formulas that is implied by the current set of equalities, and reports the single lemma corresponding to the conflict. It does so before resorting to heuristic instantiation.  Clean up the rewriter, other minor cleanup.

move new functions under exp options

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

add constant replace, indexof

add constant replace, indexof

Merge branch '1.3.x'

gmp is again default, not cln, for build ID (reverting due to license discussion at Monday meeting)

Another way to handle negative contain

Merge branch '1.3.x'

Conflicts:
COPYING
NEWS
config/cvc4.m4

Switch license default back to BSD, and add --best and --enable-gpl options.

Cache apt packages on Travis.

clean some code

Fix LogicInfo parsing for string logics

Fix LogicInfo parsing for string logics

remove a warning in strings

minor fix, bring back the assertion.

string contain changes

Removing and consolidating options for uf-ss and quantifiers.  Bug fix for inst gen-style MBQI.

Added support for proof production in Equality Engine.  Cleaned up existing proof signatures and added proof signature for theory of arrays.  Added new MBQI technique based on interval abstraction.  Cleaned up option names.  Improved symmetry breaking for uf strong solver.  Other minor cleanup.

Merge branch '1.3.x'

Update copyright year.

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

minor fix

minor fix

Merge branch '1.3.x'

Fix for ANTLR warning.

new functions in strings

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

fix for some nightly build failures

Cleanup related to output language fix.

Merge branch '1.3.x'

Conflicts:
NEWS

Better automatic handling of output language setting.

Better get-value parse error message for common user error.

Minor code cleanup.

Merge branch '1.3.x'

Java datatype API fixups, datatype API examples