Merge pull request #9 from kbansal/master

 Merge experimental decisionweight branch

Fixes to FCSimplex for some versions of compilers

Fixing the failure for make distcheck.

Merge experimental decisionweight branch

None of these are enabled by default, so any performance impact
counts as a bug

Options added are:

--decision-threshold=N :default 0
+ ignore all nodes greater than threshold in first attempt to pick decision

--decision-use-weight bool :default false
+ use the weight nodes (locally, by looking at children) to direct recursive search

--decision-random-weight=N int :default 0
+ assign random weights to nodes between 0 and N-1 (0: disable)

--decision-weight-internal=HOW
+ computer weights of internal nodes using children: off, max, sum, usr1 (meaning evolving)

Squashed commit of the following:

commit 0dbae066c19abde37092517b50f23255398539db
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Fri Apr 26 16:42:36 2013 -0400

    contentless cleanup

commit 62bb99b33deceb803ba5afc563fd322b4b5d1b7e
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Tue Apr 16 21:43:55 2013 -0400

    bugfixes in usr1 auto weight computation

commit 9f039cba805bfd722466734920e758d48ae3b23e
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Fri Mar 29 15:01:33 2013 -0400

    DECISION_WEIGHT_INTERNAL_USR1

commit 744e16d514594e5f1c69b36473b03cf501d9b9d1
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Wed Mar 27 11:05:43 2013 -0400

    split theory and decision requests

commit f379d8a821df31c74b42a7722e891abc5c944f16
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Wed Mar 27 09:51:58 2013 -0400

    fix potential bug with threshold

commit 3dcb45eb5ee648d3edbeddf76b838076afea3d12
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Wed Feb 27 20:29:38 2013 -0500

    stat bv::weightComputationTimer

commit 2ab97d063e221357d2bb017af4589105777fd5a3
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Sat Feb 23 17:02:43 2013 -0500

    decision: option to auto compute weight of boolean structure

commit 0a8c29e699ad96d5f73bc14d31ad9254f6711ae8
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Sat Feb 23 14:53:50 2013 -0500

    decision: fix design to do partial explorations

    * make findSplitterRec and all related helper functions' return
      type trivalued, to be able to distinguish between
      "partial exploration" vs "done exploration but found nothing"

    * keep additional data structure to remember to what extent the
      partial exploration has been completed so not to repeat it. we
      can use this to make multiple passes on formula with arbritrary
      order of thresholds for exploration

commit 0815991fc1b0f1d63f0e8124d4672d782e89d671
Author: lianah <lianahady@gmail.com>
Date:   Fri Feb 22 17:55:40 2013 -0500

    added simple node weight computation for bv.

commit e4c507e2e2fdc8794fd04c31093660a80c7f44c3
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Wed Feb 20 02:35:21 2013 -0500

    --decision-use-weight, --decision-random-weight=N

commit 0624177d66d6ed2b3cc7fdb13df775990cfe50c2
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Tue Feb 19 23:36:49 2013 -0500

    decisionThreshold option

commit ac3579a52e452e3118ce116ff1823d6c6885544b
Author: Kshitij Bansal <kshitij@cs.nyu.edu>
Date:   Tue Feb 19 20:22:51 2013 -0500

    DecisionWeightAttr

FCSimplex branch merge

Add ability to run different regression levels with "make check"

Theory "alternates" support

* This is a feature that Dejan and I want for the upcoming tutorial.
  It allows rapid prototyping of new decision procedure implementations
  (which we may choose to demonstrate), and a new --use-theory command-line
  option to select from different available implementations.  It has no
  affect on the current set of theories, as no "alternates" are defined.

* Also update the new-theory script, which was broken and incomplete.

add bit0 and bit1 constants to smt-lib v1 parser

making sure sat context is zero when user context is popped to 0 in SmtEngine destructor

fixing destruction order in SmtEngine

bool flatten: node num_children workaround

boolean flatten: bug fix in dfs search

(this is not intended to (and doesn't) address the issue with
NodeBuilder limit)

boolean flatten rewrite: dont re-rewrite

generalize to handle and

flatten or nodes

Improved speed of no redundant lemma assertion by using hash set

Fixes for getModelVal in bv theory

Added check for infinite lemma loop

fixed getModelValue to only query the value of leaves and evaluate more complex bv terms

Change TPTP parser to not use the STRING type; this necessary to repurpose strings for the upcoming string theory

Fix unit test (compile error) for new SatSolver interface

* changing the bitblast-eager to bitblast on pre-register
* the newVar interface of the sat solver now changed to include (isTheoryLiteral, preRegister, canEliminate)
* when bitblast-eager all bv atoms are (theory=false, prereg = true, canelim = true)
* bitblast-eager implies decision=internal

Prerelease versioning for master.

Pre-release versioning

Cutting release 1.1.

Some final minor changes before cutting 1.1.

* update documentation
* update the cut-release script
* spelling/wording updates
* add a (previously-failing) fuzzer regression

updated NEWS to include inequality solver

abort quantifiers check if master equality engine is inconsistent.

Making arithmetic model reversion on unsat checks an option.

Regenerated copyrights: canonicalized names, no emails

Remove old README file from rewrite-rules left over from new-theory script long ago

Fix get-authors script to not extract email addresses, canonicalize names, add .mailmap

One final fix to "make submission" rule

update copyrights

Adjust release Makefile rules, new run script

Fix regression error by turning off model-based solver when models are on
(ironic, yes, but model-based solver doesn't yet produce models)

Turning on model based array solver for QF_AX

Made eager lemmas an option, enabled for QF_AX

Disabling eager array index splitting for QF_AX

Fixes for two bugs:

* one that Tim found in model generation for records containing Booleans
* another that the fuzzer found in quantifiers + check-models

Test cases enabled/added for both.

Cleaning up the demand restart code.

Adding a restart test strategy to integers.

Adding demand restart.

Adding tests for the previous commit.

Merging some cleanup work:

* Comment cleanup
* Spelling fixes
* Fix warnings
* Documentation updates
* References in docs to cryptominisat removed
* Unneeded scope resolutions removed
* Old, unused regression removed

Fix for iff terms over equalities between the same term and differing constants.

Fix bug 491 and related issues with checkModel() and quantifiers.  Enabling previously-failing testcase.

fixed TheoryBool rewriter bug

fixed bug 502; now the core bv solver only gives the model for variables and shared terms.

changed option to run inequality solver by default

Disabling eager array index splitting for QF_AUFLIA
Minor changes to model-based array solver

do simple ite rewriting within quantifiers

make Boolean term conversion partially non-recursive (resolves bug 501)

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

removing cryptominisat since we're not using it

fix memory corruption in arrays destructor

some Java bindings fixes (fixes Debian build problems)

Fixed a warning, made eager-index default to true (better for QF_AUFBV)

Fixed bug in arrays

Added assertion

Updates to model-based array solver
Minor fixes to bv and theory_engine

New model-based array procedure

reverted the core solver to do static slicing, added option --bv-core-solver

fixed inequality checkDisequalities inefficiency

Merge branch 'master' into bv-core

fixed some model stuff

fixed  model generation bug; commented out attempt at inequality propagation

inequality solver now only splits on disequalities when complete

added model generation for bv subtheories and bv-inequality solver option

Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javac

Make --incremental the default when running interactively

core theory currently disabled

getModelValue implementation in bitvectors

adding
* getModelValue to valuation
* getModelValue to theory engine
* getModelValue to theory
implemented getModelValue in bitvector

the purpose of getModelValue is to ask for a concrete value of a shared term

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

moving bv before arrays

fixed inequality bugs due to improper explanation

cleaned up the bv subtheory interface; added check for inequality theory completeness

java input stream adapters working

getEqualityStatus now also queries the inequality solver

Fix for SCM detection

Merge pull request #7 from kbansal/portfolio

finish removal of separateOutput

finish removal of separateOutput

added support for disequalities in the inequality solver

incremental inequality solver implemented

Fix bug in portfolio executor output; fixes nightly portfolio-checking runs.

non-incremental inequality solver seems to be bug-free (i.e. passes fuzzing)

fixed some explanation problems for the core theory; still slow

Merge remote-tracking branch 'dddejan/c++11'

Conflicts:
src/smt/boolean_terms.cpp

changing string hash function to use the gnu namespace
due to namesapce resolution std namespace was used instead, which hashes the string pointers leading to mayhem

Support for Boolean term conversion in datatypes.

compiles with
export CXXFLAGS='-std=gnu++0x' before configure
fails all regressions in the parser

Merge branch 'master' into bv-core

another typo/bugfix for equality constant evaluation

Merge branch 'master' into bv-core

fixed more equality stuff

Better error in case of nonlinear assertions while in linear logic

Add the ability to "mute" commands, needed for SMT-LIB compliance.

fixing markings of internal nodes in equality engine

fixed compilation problem