Merging in additional glpk options and statistics from CAV submission.

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

Replace lemma sending with EQ assertions. Fix a typo in hex_to_int function.

Replace lemma sending with EQ assertions. Fix a typo in hex_to_int function.

More preparation for CASC proofs.  Minor fix for sort inference (rewrite new assertions).  Bug fix for ambqi : simplify correctly for multi-sorted case.  Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real.

Bug fixes to CBQI.  Add first draft of CASC j7 TFF script.  Add regression, minor changes.

Fix for example installation.

Initial draft of run scripts for CASC j7

Add variable ordering to ambqi.  Bug fix to macros. More preparation for CASC proofs.

Major simplifications to macros module.

Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers.  Minor fixes to ambqi.  Preparation for CASC proof output.  Add NNF option.

Basic optimizations for ambqi : only normalize UF applied to variables, direct handling of NOT

Adding encoding of sha1 collision for the hashing example

patch to the last commit: add a single character case

fix a bug in contain

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

add splits

add splits

Fixes to ambqi, now solution-sound.

First draft of ambqi_builder (new implementation of MBQI based on disjoint sets).

fix a bug in replace and contains

add constant regular expression check for intersection.

Improving documentation for glpk-cut-log switch.

Valuation::entailmentCheck() proxy for TheoryEngine version.  Signature and contract is the same as for TheoryEngine version.

Fix typo in bitvectors example; thanks to Adam Gashlin for reporting the issue.

Simplification of EqualityEngine::areDisequal.  Comparison for production : church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=6444&reference_id=6445&p=5.  Comparison for debug : http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=6449&reference_id=6446&p=5.

Fix assertion from previous commit.

Add option --dt-stc-ind for strengthening skolemization.  Refactor skolemization.

More minor optimizations for datatypes.

Minor optimizations to datatypes, revert to checkClash not mod eq.  Minor clean up.

Merge remote-tracking branch 'upstream/master' into sets

decision engine: cache start index for and/or nodes

This is done only in "hard" case. Limited testing has not shown
improvement in the "easy" case.

This was triggerred by a benchmark sent by andy/viktor.

performance comparison notes for the change on wiki
http://church.cims.nyu.edu/wiki/User:Kshitij/decisioncacheindex

T-entailment work, and QCF (quant conflict find) work that uses it.

This commit includes work from the past month on the T-entailment check
infrastructure (due to Tim), an entailment check for arithmetic
(also Tim), and QCF work that uses T-entailment (due to Andrew Reynolds).

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

Fix warnings, cleanup in strings typechecker.

Fix compiler warning re: TheoryUF destructor.

Fix simplify output for SMT2 printer.

Fix for (user) context-dependence of arith TO_INT/IS_INT rewriting and rewrite-divk.

Mostly resolves bug #561 memory leaks, and more.

Fix for --force-logic to extend its reach to the parser.

fixed couple of more warnings

fix was compiler warning in antlr_input, crashing test case with the old fix

Revert a compiler warning fix from ea6a5a6.

fix a typo: --string-exp => --strings-exp; fix a signed int warning in antlr

add leading zeros support for str.to.int

Significantly improve performance for producing datatypes models.

Merge remote-tracking branch 'upstream/master' into sets

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

add strings-opt2 for regular splitting

cleanup

minor change with kshitij's change

nodemanager robust skolem numbering

add strings-opt2 for regular splitting

Merge pull request #25 from kbansal/sets

Sets

Preparation for models for co-inductive datatypes. Minor cleanup.

Optimizations for datatypes: check for clashes modulo equality.  Avoid building model at fullModel=false when possible.  Minor cleanup.

minor fix

Merge remote-tracking branch 'upstream/master' into sets

travis, please!

attempt to improve CVC4's "parse error" message

rm undocument/non-working* "feature"

*test of unsigned for negative

minor change: add a heuristic for preventing constant splitting.

optimization

Avoid assigning constructor terms to 1-constructor datatype eqcs, when possible, to ensure termination for codatatypes. Minor changes.

Compute care graph for datatypes.  Preliminary results show 20x speed up on larger problems.  Improve datatypes rewriter.

Add --inst-max-level=N option for Kshitij.  Support define-const command in Smt2.

Minor fix to avoid rewriting datatype equalities into non-equalitiers, as required.  Add APPLY_UF to congruence types to avoid model construction bugs.

Eh, what?

fix warnings in strings/

Allow fmf-bound-int to be set with set-option and via API.

simplify mkSkolem naming system: don't use $$

Short summary: By default NODEID is appeneded, just continue doing what you
were, just don't add the _$$ at the end.

Long summary:

Before this commit there were four (yes!) ways to specify the names for new
skolems, which result in names as given below

1) mkSkolem("name", ..., SKOLEM_FLAG_DEFAULT)  -> "name_NODEID"
2) mkSkolem("name", ..., SKOLEM_EXACT_NAME)  -> "name"
3) mkSkolem("name_$$", ..., SKOLEM_FLAG_DEFAULT) -> "name_NODEID"
4) mkSkolem("na_$$_me", ..., SKOLEM_FLAG_DEFAULT) -> "na_NODEID_me"

After this commit, only 1) and 2) stay.

90% usage is of 1) or 3), which results in exact same behavior (and
looking at the source code it doesn't look like everyone realized that
the _$$ is just redundant).

Almost no one used 4), which is the only reason to even have $$. Post this
commit if you really want a number in the middle, manually construct the
name and use the SKOLEM_EXACT_NAME flag.

use internal skolem numbering

Minor refactoring and optimizing.

Fix bug in mbqi=fmc handling theory symbols.  Fix mbqi=fmc models (Bug 557).  Improve datatypes rewrite, make option for previous dt semantics.

Add initial support for co-datatypes.

Better support for building with mingw64; thanks to Nicolas Roche @ Altran for the fix.

setType -> setOfType, resolves bug 556

Fix the build; --check-proof works for UF but not for the new UFC logic.

Expand definitions in theory datatypes, now has the expected semantics for incorrectly applied selector terms.

Boolean terms conversion fix for datatypes, fixes a problem Andy discovered on his branch.

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

minor fix for strings

minor fix for strings

Add support for cardinality constraints logic UFC.  Add regressions in fmf/.  Fix datatypes E-matching bug.  Change defaults : mbqi=fmc, decision heuristic stoponly=false for quantified logics, decision=justification for ALL_SUPPORTED, full-saturate-quant=false.  Minor fix for fmc models.  Add infrastructure to datatypes to prepare for next commit.

refactor .travis.yml

Merge pull request #24 from kbansal/sets-model

sets, misc

Minor change to better support parameterized partial/total kinds (for upcoming datatypes work).

Revert E-matching datatypes fix.

Handle fmf.card as input from user, add support in SMT2 parser, as requested by Martin Brain.  Fix two minor bugs : E-matching with datatypes, instantiation caching with incremental.

fix get-info error-behavior

add tests

fix

prep for fix

try foreach on CD datastructure

inputs to trigger bug

more

some debugging changes

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

Reduced example from pcc's bug report.

Merge pull request #21 from pcc/ite-fix

Fix for ite of >=64bit wide bitvectors with unconstrained condition.

fix for hiding prompt/header in shell, error-behavior options as in SMTLIB