bug 374 fix: assert litVal=desiredVal only for leaf nodes

Bug 374 benchmarks

Fix failure in non-assertion builds on incorrect SmtEngine use.

Fixes for Boolean terms in arrays (including fix for bug 517).

Fix clang static initialization order issue; fixes bug 512.

Per SMT-LIB spec, allow (set-info..) command to succeed implicitly with unknown key.

SMT-LIB printer updates (some missing cases).

Fix bug where strict mode didn't allow DIV or MOD, and Ints permitted real division

Standardize SMT-LIBv2 set of logics to use LogicInfo.

Previously, SMT-LIB logics were treated specially, as in SMT-LIB v1.2.
This led to inconsistencies---such as nonstandard logics like "QF_LIRA"
being accepted in set-logic but not providing the "Real" sort.  Now,
the LogicInfo is used and queried, so nonstandard logics should work
fine and declare the correct symbols.  SMT-LIB v1.2, unfortunately,
can't take advantage of this fully since symbols like "Array" have
substantially different meanings in different logics.

Fix bug 512: an assertion failure only appearing with clang on Mac OS, due to improper ITE removal in quantifier instantiations.

Fix an error that valgrind found.

Fix incremental bug in symmetry breaker.

Thanks to Christoph Sticksel for reporting this.

Fix error reporting on use of (nonlinear) div,mod,/ symbols

Update THANKS to mention David Cok's contributions.

Detect multiply-defined :named annotations and issue an error.

Thanks to David Cok for pointing out this issue.

Conflicts:
library_versions

Fix parsing of SMT-LIBv2 |quoted| symbols that span newlines in interactive mode.

Thanks to David Cok for raising this issue.

Compliance fixes for :named annotations: they must name closed subterms, the names must be user-permitted names, etc.

Thanks to David Cok for raising this issue.

Don't allow get-model & co after a user push/pop

This makes us more strictly adhere to the spec, but it's useful anyway:
previously we would support a get-model until the problem was explicitly
changed with e.g. a new assertion.  That meant you could check-sat, then
pop, then get-model, but you'd only get the part of the model still in
scope.  This is strange, and would likely lead to problems, so it's now
disabled.

Thanks to David Cok for inquiring about this.

As per SMT-LIB standard: make - and xor take n>2 args and be left-assoc; => takes n>2 args and is right-assoc.

Thanks to David Cok for pointing out this issue.

Fix for equality-chaining of Booleans in SMT-LIBv2.

Thanks to David Cok for reporting this.

Fix destruction issue in GetValueCommand leading to crash.

Thanks to David Cok for reporting this.

Better error on invalid logic strings.

Thanks to David Cok for reporting this issue.

Conflicts:
library_versions

Better error on illegal (pop N); also more compliant SMT-LIB error messages in some places

Thanks to David Cok for reporting these issues.

A couple of fixes to the get-option command for compliance with SMT-LIB.

Thanks to David Cok for reporting this issue.

Disallow construction of (_ BitVec 0).

Thanks to David Cok for reporting this issue.

Fixed "success" response to (push N) / (pop N) with N > 1.

Thanks to David Cok for reporting this issue.

Fix to empty response to (get-assignment).

Thanks to David Cok for reporting this issue.

configure fix for building with glpk on redhat, perhaps others

minor changes to language bindings

disable Logic-checking with finite model finding for now, since FMF uses Rationals, making the check think arithmetic should be enabled (but it's not)

Fix erroneous results when the logic was incorrectly specified (by throwing LogicException).  Also correct a case where sharing was doing some work during pure theory solving.

Prerelease versioning for 1.2.x

Merge tag 'smteval2013'

Cutting release 1.2.

Removing arithmetic compile warning for release

update versioning

final updates for smt-eval script

Fixed assertion bug

fix for smt-eval run script

BV strategy for SMT-EVAL

fix for nonterminating model-based array loop

added type checking rule to check for bit-vector constants of size 0

one more fix for rewrites

fixed bv rewrite blow-up

fix for bug500

Fixes a bug with arithmetic's new attempt solution infrastructure.  This caused arithmetic to think it was in a conflict incorrectly. This lead to it not properly responding to new input and lead to an inconsistency bug.

This could be triggered previously by running:
./builds/bin/cvc4 --stats --no-restrict-pivots --enable-miplib-trick --miplib-trick-subs=2 --fc-penalties --collect-pivot-stats --new-prop --dio-decomps --unconstrained-simp --fancy-final /home/taking/benchmarks/smtlib2/QF_LRA/miplib/opt1217--17.smt2

Improving arithmetic debugging output.

Disabling an incorrect prototyping line from the simplex merges.  Fixes bug 510.

Change SMT-EVAL run-script to use Tim's best QF_LRA command-line parameters

fixed bv rewrite rule bug

Removing excess verbosity from ApproxSimplex (after discussing with Tim)

Adding a heuristic for guessing an optimization function when using glpk.

Disables justification stop only for LRA if the problem contains no ites. This is a bandaid for constraints-tempo-width family of benchmarks.

Some bug fixes for mb arrays

Adding cut offs for likely integer infeasible paths.

Adding a smarter technique for pivoting in solutions for glpk.

Fixing compilation of unit tests. These problems were due to splitLemma() being pure virtual.

More misc. arithmetic cleanup. Removing unused files and functions. Also removing an ugly forward declaration that was needed to get error set bound information on basic variables.

Code cleanup.  Reducing misc. warnings in arithmetic.

Removing arithmetic legacy code and unifying functions.

Fixing a debug typo.

Merging branch 'soiquickexplain'.

Merge branch 'fcexplanations'

Adding quick explain for soi simplex.

* splitLemma to request atoms
* normalizing in bv before bitblasting

merged master

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

Comment out some debug-related things in attribute code, no longer needed

Fix to dumping re: boolean terms, datatypes

Fix to boolean-terms; resolves bug #507

removed tracing code causing slowdown; cleaned up some code

Working on the new explanation system.

added back BitwiseEq rule

Adding a missing makefile to the dist (fixes distcheck)

Making propagation more conversative.

Draft of the new propagation code.

fixed merge conflicts

merged cvc4 master

updated the author name

added several rewrite rules (BitwiseSlicing, Ule/SleEliminate, ExtractSignExtend) and bvurem lemma

added bvule, bvsle operator elimination rulesl; added bvurem lemma generation

added some bv rewrite rules

innd examples are solved fast, but destruction assertion fail

fixed compile error

uncompiling new bv to bool lifting

finished implementing bv to bool lifting and added --bv-to-bool option

more work on boolean lifting

started work on bv1 to boolean lifting

added support for dumping the SAT problem the sat solver is working on

updated the author name

Add option in quantifiers for clause splitting

added several rewrite rules (BitwiseSlicing, Ule/SleEliminate, ExtractSignExtend) and bvurem lemma

add decision_attributes.h for make dist

Adding has bound counts and tracking for rows.

Some fixes for GCC 4.2, and for Java on Mac

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