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

For security, add --no-filesystem-access option, which disables SMT-LIB script access to filesystem.

Allow turning off the interactive prompt while in interactive mode.

Properly quote symbols in SMT-LIB printer.

Some incremental bugs for Boolean terms, fixed.  Thanks to Pantazis Deligiannis and Jeroen Ketema for discovering this issue.

Merge branch '1.3.x'

Fixing bug 552.  There was a bug when integers are made using a string with a lot of leading 0s on old versions of CLN.

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

windows build fix for UINT32_MAX

windows build fix for UINT32_MAX

Travis-CI test for new-theory script, also related bugfixes.

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

add str to u16/u32, and u16/u32 to str

minor typo/bug fix

add str to u16/u32, and u16/u32 to str

Merge pull request #23 from kbansal/sets-model

Sets model

rm old unused code

get-antlr error on missing config.guess

add construles, type_rules rm redundant, kinds cleanup

minor printer fix; intersection fix

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

Conflicts:
src/theory/strings/regexp_operation.cpp
src/theory/strings/regexp_operation.h

adds new feature: re.loop

adds intersection

deriv symbolic regexp

adds intersection

adds new feature: re.loop

Merge branch '1.3.x'

Conflicts:
src/theory/arith/normal_form.cpp

Win32 build script fixes (to allow portfolio builds).

Fix an off-the-end string pointer bug (showed up only in some Win32 builds).

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

deriv symbolic regexp

adds intersection

deriv symbolic regexp

Merging in a fix from 1.3.x.
Fixes an idempotency issue for non-linear multiplication with integer and real variables.

Conflicts:
src/theory/arith/normal_form.cpp

Fixes an idempotency issue for non-linear multiplication with integer and real variables.

adds intersection

Merge pull request #22 from kbansal/sets-model

Sets model

cleanup

fix for sets/mar2014/..317minimized..

Observed behavior:
  --check-model failed for set-term (union (z3f69 z3v151) (setenum z3v143))
with different set of elements in the model for representative and the node
itself.

Issue:
  The trouble with data structure being mainted to ensure that things
for which lemmas have been generated are not generated again. This
data structure (d_pendingEverInserted) needs to be user context
dependent. The bug was in the sequence of steps from requesting that
a lemma be generated to when it actually was. Sequence was:
addToPending (and also adds to pending ever inserted) ->
isComplete (might remove things from pending if requirment met in other ways) ->
getLemma (actually generated the lemma, if requirement not already met)

Resolution:
  adding terms to d_pendingEverInserted was moved from addToPending()
to getLemma().

Fix for registration issues of term appearing in a shared lemma

(brought to attention by lianah -- fix currently just adapted using
arrays -- this is to remind me to raise why do we even have this
isPreregistered bussiness)

rewriter fix, weaken an assertion

constant normal form and rewrite

fix a sharing issues with sets

push subtyping for sets to the element type

for eg, (Set Int) is subtype of (Set Real) if Int is subtype of Real

enable check-models for sets/ regressions

work on set model

testlemma regressions

Minor fix for CBQI, ignore inst constant nodes.

Fix documentation for Theory::preRegisterTerm().

Refactor the theory specific parts of definition expansion into the theory solvers.

In the process of doing this I may have fixed some bugs or some potential bugs so there
may be some user visible results of this refactoring.

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

Set dumping options from (set-option..) and API more directly.

Fix for bug 555; SMT-LIBv2 symbols now output with proper quoting.

Move the translator binary from src/main to examples, no longer built by default.

Appease compilers from latest XCode release (v5.1).

Minor usability fixes related to SMT-LIB compliance.

Fix proof signatures makefile