Updated CASC scripts, as provided to Geoff Sutcliffe

Possible final version of run scripts for casc.

Add model-producing run script for casc.

Add support for --dump-models option, in preparation for casc.

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.

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

Fix minor bug in full_model_check.cpp

minor changes to language bindings

Update casc24-fnt run script.  Add casc24-fof run script.

added some extra options to the bit-vector theory

Add support for quantifier patterns in smt2 printer.

Refactoring to separate old and new model building/checking code.

Preliminary version of finite model finding over bounded integer quantification. Minor update to casc script.

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)

now proofs print mapping between atom and propositional variable as a comment in LFSC

Update casc run script.  Work on compliance for SZS output.

fixes to the proof system so it works with theory lemmas and explanations

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.

Add documentation for --disable-fmf-inst-gen, which removes a warning

Add simplification option --fo-prop-quant.  Add model support for new model-checking procedure.  Add run script for casc24-fnt.

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

Changing the integer normal form to increase matching.

Add new method for checking candidate models, --fmf-fmc.  Add infrastructure for handling bounded integer quantification (quantifiers/bounded_integers.h and .cpp).  Add option for disabling model minimality restriction for finite model finding, --disable-uf-ss-min-model.  Add option for relational triggers such as x = f(y), --relational-trigger.

rm decision/relevancy

Prerelease versioning for master

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.