add new theory (sets)

Specification (smt2) -- as per this commit, subject to change

- Parameterized sort Set, e.g. (Set Int)

- Empty set constant (typed), use with "as" to specify the type, e.g.
    (as emptyset (Set Int))

- Create a singleton set
    (setenum X (Set X)) : creates singleton set

- Functions/operators
    (union (Set X) (Set X) (Set X))
    (intersection (Set X) (Set X) (Set X))
    (setminus (Set X) (Set X) (Set X))

- Predicates
    (in X (Set X) Bool) : membership
    (subseteq (Set X) (Set X) Bool) : set containment

fix a -Wunused

fix makefile

add more tests, and define int.to.str(NEGATIVE)=""

add two cases to the regression test

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

Conflicts:
src/theory/strings/theory_strings_preprocess.cpp

hot fix for str2int/int2str

add negative int2str

String parsing example in CVC parser

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

Conflicts:
src/theory/strings/theory_strings_preprocess.cpp

hot fix for str2int/int2str

add negative int2str

String parsing example in CVC parser

Fix ite and iff handling in QCF.  Add option for heuristic instantiation in QCF (not working yet).  Improve automatic option setting for quantifiers.

portfolio: add stat to track time spent waiting for interrupted threads to stop

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

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

Merge branch '1.3.x'

Stopping non-linear terms from entering the dio solver. Fixes bug 547.

add negative int2str

String parsing example in CVC parser

missed files for the latter commit

str.to.int(INVALID) = -1

switch to total function str.to.int: maps invalid and non-digit strings to 0

bring back the commits which is lost accidentally.

add str2int

Fix for strings-exp: enable quantifiers

Fix strings preprocessing for justification heuristic

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

type conversion

type conversion

Make QCF more incremental.  Fix bug in QCF handling of ITE formulas, add support for ITE terms.  Add full-delay inst-when mode.  Make strings come before quantifiers in check.  Minor cleanup.

partial function charat

fix expanding def

bug fix for reverse check

lexer fix: disable smt-lib conversion for string literals

minor fix for recognizing the tail backslash, still have smt-lib compliance issue.

resolve merge conflicts

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

Conflicts:
src/theory/strings/theory_strings.cpp

escaped characters, having an issue with smt-lib defintion, further repair is needed.

minor fix for merge

minor cleanup for merge

minor fix for merge

escaped characters, having an issue with smt-lib defintion, further repair is needed.

Fix build (some nonexistent files listed in Makefile)

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

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

minor cleanup for merge

minor fix for merge

minor cleanup for merge

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

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

minor fix for merge

minor fix for merge

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.