reverse the order of link arguments to -lcln -lgmp, fixes linking errors for static-binary CLN-enabled builds on greed

Type enumerator infrastructure and uninterpreted constant support.  No support yet for enumerating arrays, or for enumerating non-trivial datatypes.

Applying Dejan's patch for bug #369, which resolves it by adding a new (let..) form for each introduced binding.

fixing make dist

fix a warning in unit test compilation

svn ignore

an example that uses bitvectors to simulate sha1 computation and dumps an smt problem corresponding to the hash-inversion problem

removing readme from fmf-devel

merged fmf-devel branch, includes support for SMT2 command get-value and (extended) SMT command get-model.  added collectModelInfo and removed getValue from theory interface.  merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface.  The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.

svn ingore

* fixing the simple_vc_cxx.cpp compile issue (no more Integer constants)
* adding as examples the programs i used to translate nonlinear smt2 problems to other formats

going back to 1. being a non decimal

small changes:
* smtlib2 decimal constant can be "1.", i.e. doesn't need digits after the point
* adding CVC4_PUBLIC to rational output operator, otherwise it's unusable for users

minor fix-ups

fix portfolio build

fix eXecutable bit on a script

minor SMT-LIBv2 compliance issues

remove a debugging line from configure script that was left in inadvertently

another signed-ness warning fix for newer GCC

Minor changes to avoid some warnings on GCC 4.7.1 (Debian wheezy/sid).  ANDY - please look at the diff and make sure I didn't do something stupid

Bugs resolved by this commit: #314, #322, #359, #364, #365.
See below for details.

* Fix the "assert" name-collision bug (resolves bug #364).

  Our identifiers should never be named "assert", as that's a preprocessor
  definition in <assert.h>, which is often #included indirectly (so simply
  having a policy of not including <assert.h> isn't good enough---one of
  our dependences might include it).  It was once the case that we didn't
  have anything named "assert", but "assert()" has now crept back in.
  Instead, name things "assertFoo()" or similar.  Thanks to Tim for the
  report.

  To fix this, I've changed some of Dejan's circuit-propagator code from
  "assert()" to "assertTrue()".  Ditto for Andy's explanation manager.
  Guys, if you prefer a different name in your code, please change it.

* Fix the incorrect parsing of lets in SMT-LIBv2 parser (resolves bug #365).
  Inner lets now shadow outer lets (previously, they incorrectly gave an
  error).  Additionally, while looking at this, I found that a sequential let
  was implemented rather than a parallel let.  This is now fixed.  Thanks to
  Liana for the report.

* Remove ANTLR parser generation warnings in CVC parser (resolves bug #314).

* There were a lot of Debug lines in bitvectors that had embedded toString()
  calls.  This wasted a LOT of time in debug builds for BV benchmarks
  (like in "make regress").  Added if(Debug.isOn(...)) guards; much faster
  now.

* Support for building public-facing interface documentation only (as opposed
  to all internals documentation).  Now "make doc" does the public-facing and
  "make doc-internals" does documentation of everything.  (Along with changes
  to the nightly build script---which will now build and publish both types
  of Doxygen documentation---this resolves bug #359).

* Fix the lambda typechecking bug (resolves bug #322).  Thanks to Andy for the
  report (a long long time ago--sorry).

* The default output language for all streams is now based on the current set
  of Options (if there is one).  This has been a constant annoyance, especially
  when stringstreams are used to construct output.  However, it doesn't work
  for calls from outside the library, so it's mainly an annoyance-fixer for
  CVC4 library code itself.

* Add some CVC4_UNUSED markers to local variables in theory_arith.cpp that
  are used only in assertions-enabled builds (and thus give warnings in
  production builds).  This was briefly discussed at the meeting this week.

Various fixes to documentation---typos, some incomplete documentation fixed, \file tags corrected, copyright added to files that had it missing, etc.

I ensured that I didn't change any code with this commit, and even tested on the cluster to be doubly sure:

  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4655&reference_id=4646&p=0

Adding std namespace to a couple of make_pair instances.

Added include unistd to main/util.cpp

Added virtual destructor to PpRewrite.

Some changes to configure.ac:

1. Includes BOOST_CPPFLAGS during compilation of all files, not just portfolio-relevant files.  This is necessary since we now have a general dependence on Boost (not just its threading stuff).  This resolves bug 357.

2. Support --disable-thread-support and --enable-thread-support, in an effort to get to the bottom of bug 361.

These changes shouldn't affect performance, though #1 will build the cvc4 libs with a couple of pthread definitions that conceivably could change the behavior of #included standard headers.  Let's keep an eye on tonight's regressions.

svn:ignore

Fixed bug in bv rewriter that caused wrong answer in SMT-COMP

fix a link error on church, due to Antlr #defining "true" and "false" :-( --for now, just #undef them after the #include

Fixing a bug in proof production for the DioSolver.

This adds TheoryArith::safeToReset().  This fixes bug 363.

Adding access to simplex's ArithPriorityQueue to TheoryArith for ArithPriorityQueue::reduce(), ::begin() and ::end().

Improved debugging output.

Improved debugging output.

Adding reduce() to the ArithPriorityQueue. This reduces the queue from a superset of the basic variables that violate a bound to the exact set.

Added a warning to arithmetic for a known dio solver bug. Somehow the fix never made it to trunk. Do not know how. The fix to the bug is pending the hunt for bug 363.

TPTP: add parser for cnf and fof
 - include directive works
 - no keyword : 'fof', 'cnf', ... can be used for symbols name
 - real -> unsorted -> real (for the one that appear, so no bijection bitween real and unsorted)
 - same thing for string

But:
 - string not distinct by projection to real, not sure if the current state of string theory make them distinct
 - filtering in include is not done
 - the result is not printed in the TPTP way (currently SMT2 way)

parser: add some acces function and recover the original nextToken from antlr3
in order to be able to use the stack of streams.

fix : function AntlrInput::tokenTextSubstr

Parser: add the possibility to bind at level 0.

qf_lra strategy

Reverting buggy rewriter code

another qf_lra strategy update

Fixed bug in rewriter

unnecessary ^ in regular expression; warning produced on smt-exec

QF_LRA strategy in run script, now final (?) for smt-comp 2012

final sources (?) for competition

Fix for slow array rewrite and minor bug fix in arrays that popped up as a result

small bug fix and performance fix in ite simplifier

fixed smt version 1 parser for quantifiers

tracing code to make sure decision options are being set correctly

bugfix, enable only QF_LRA, not other arith

QF_LRA, Quantifiers: enable use decision for (only for) stopping search

Fixing bug 360.  The driver wasn't exiting when there was an error (it just plowed ahead to the next command).  Now the driver exits on the first error, unless it's in interactive mode.

QF_AUFLIA: enable use decision for (only for) stopping search

fixing a problem due to lemmas produced while backtracking

--decision=justification-stoponly : use decision engine only for stopping
search early, not to make decisions

new options.h :)

enabling theoryof=term for quantifiers with sharing
disableing one test case in equantifiers/decision that runs long

fixing wrong assertion

Removed assertion that can fail

fixing makefile error that brakes build

Fix array bug causing incorrect answers

small change to equality assertions so that one doesn't get x = y and y = x

Adding the failing QF_AUFLIA regression mentioned in last commit.
pp-regfile.delta02.smt is the one to look at with
--decision=justificaiton, the delta minimized version of pp-regfile,
which also gives wrong answer. due to various commits/fixes, delta01
gives correct answer currently.

This is an attempt to fix the bug in the justification heuristic. The
other minor change is removing dependency of header file in
theory_engine.h

It fixes all known wrong answers in QF_BV and QF_AUFBV. It doesn't fix a
wrong answer for QF_AUFLIA -- it is currently unclear what is the cause
of this bug, could be sharing.

Performance impact (turns out) is none on QF_BV and QF_AUFBV (except, of
course, those for which the answer was wrong earlier; and also perhaps
one or two off-cases)

The issue was with how the infinite loop in justification stuff was prevented.
To keep it short, I skip what was wrong earlier, and this is what is done
now:
* whenever an atomic formula is seen, a list of pairs of <IteSkolemVariable,
  AssertionCorrespondingToIteSkolem> is created for each skolem occuring in
  the atom.
* we iterate over this list, doing the following: check if skolem is marked
  as visited. if not, mark visited, recurse, when back unmark.

I lied, I will tell you what was being done earlier was -- 1. the check for
not being visited was being done in each recursive call, not just for atoms.
2. The AssertionCorrespondingToIteSkolem was being used to check if something
is visited and not IteSkolemVariable. I don't know if this makes any
difference, but anyhow, I think this is cleaner & clearer, so I keep this.

updated build script for smt-comp submission

changing theoryOf in shared mode with arrays to move equalities to arrays
disabled in bitvectors due to non-stably infinite problems

the option to enable it is --theoryof-mode=term

Fixing if condition for trivial equalities in arithmetic. Also some whitespace issues in smt_engine.cpp.

Bug fix in justification heuristic. Had to do with how
a "visited" node in the recursive findSplitter method was
handled (which would lead to infinite loop). Earlier,
they were ignored assuming the ancestor would split on it
later. The right thing to do is to split on it right away.

(Fixes errors from the fuzzer, not the ones from last night's
regression)

Reverting rewrite rule to working version

Fixes some assertion failures

Fix for incompleteness bug with decision engine: repeated simplification
could introduce additional assertions that were not beign processed by the
decision engine.  Now these assertions are merged in with pre-ITE-removal
assertions, ensuring the decision engine sees them.

Fixing mac compilation issues.

one bug fixed

WIP

fixing the problems with the bvminisat. there was a case when things would get bitblasted, it would restart to add the clauses, and loose propagation information.

add failing regression, move error up

Fixing a case for explanation of non-normal form equalities.

bug fixes in justification heuristic
* remove assert iteSkolemMap gives ite-s (not true with repeatSimp)
* handle a corner case in findSplitter triggered by repeatSimp

Fixing a bug related to explaining propagations with non-normalized witnesses.

enabling fixed bug345 case

fixes for the hasTerm issues in the shared database under the decision heuristic

New substitutions implementation - fixes performance issue seen in nonclausal
simplification for some benchmarks

Fixed arithmetic consistency issue.  The simplex conflict variable had to be reenqueued so that the queue was a superset of the failing assertions.  This adds a super expensive debug routine unenqueuedVariablesAreConsistent() that catches this bug.  This is enabled when -d arith::consistency is turned on. make check passes with this flag enabled.

fix for clark's bug
imporant: theories SHOULD NOT use getSatValue at all, otherwise they might create a conflict with a literal they didn't get()

don't run rewriterules regressions by default; fixes needed

fix quantifier non-bug

Removed an assertion, unneeded header file

some changes to make CVC4 work nicely with trace executor for application track; (set-option :print-success true) supported, (exit) causes immediate exit regardless of EOF, etc.

making --simplification=none the default for quantified logics; this a request from andy.  evidence of performance improvement: church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4516&reference_id=4475&p=5

bug ifx, mv

restore destruction of stuff in driver

This commit:
* enables decision heuristic (justification) for QF_BV and QF_AUFBV
* disables a failing regression in aufbv (because of equality engine
  assert failure trigerred by above change)
* moves around the init procedure smt_engine
* destruction time issues because of moving this -- still to be fixed,
  currently get around by not destucting stuff in driver

failing quantifier

The "no-tears-in-competition-mode" commit.  Change all (non-driver, non-SAT-solver) uses of std::cout to the Message stream, and all uses of std::cerr to the Warning stream.

fix cout, fix statname, rm deadcode

add passing regression

changing to a more natural propagation order in uf, seems to pay off

some changes to the uf engine
* dramatically less terms to manage by doing reflexivity semantically
* fixes the problem clark had with not detecting inconsistencies with shared terms
i'm not sure what's the performance impact, but this is so much better and we'll deal with performance later

Brings the tuning branch into trunk. This includes the changes from restricted-simplex.