fix some build dependencies in options-building; should fix a strange bug Andy saw when adding options & re-making, which was caused by sources not being properly recompiled when they should be

More progress on array constants.

Here's a fun way to give yourself a week-long headache: try to figure out how
to write efficient code to normalize array constants.

It's mostly there now - just need to figure out how to use type enumerators and
update once the new cardinality stuff is in place.

add some incremental in-tree regressions

rewriterules: fix a correction bug with --simplification=batch

  Rewriterules used ppAssert to obtain early the rewriterules in order
  to use them in ppRewrite. But all the simplifications (ex. f x = b :
  [f x/b]) are not done at that point. Since --simplification=batch
  remove the equality (unlike =incremental), for
  reachability_bbttf_eT_arrays.smt2 the answer was sat instead of
  unsat (thx Andy).

  Partial fix: don't take the rewriterules during ppAssert. That changes
  nothing since early rewrite was already disabled. But the complete
  fix (when early rewrite will be enabled again) will need to take the
  rewriterules more than once.

remove duplicate function TheoryEngine::getTheory(TheoryId).  It was a duplicate of TheoryEngine::theoryOf(TheoryId)

removing v1l20009.cvc, a datatypes benchmark where the TCC fails (CVC3 and CVC4 differ in the answer), so it doesn't really test anything

minor cleanup

fixes for java bindings

1. Fix for inst_match.cpp to allow compilation on fedora
2. Initial implementation of computeIsConst for arrays - still needs
   additional checks based on cardinality
3. Finally fixed pre-competition bug in array rewriter
4. Still to come: array rewrites for constants and STORE_ALL

The SmtEngine now ensures that setLogicInternal() is called even if there is no explicit setLogic().  This is important for the CVC language, where the parser doesn't ensure that setLogic() is called, and for API uses.  setLogicInternal() should be called in order to properly set up heuristics, even if the logic is just ALL_SUPPORTED.

This means that the CVC language can now take advantage of statistics.

Also added the ability to set the logic from CVC presentation language via (e.g.)
  OPTION "logic" "QF_UFLIA";

Disabled the justification decision heuristic for ALL_SUPPORTED, as it interferes with incrementality.  Kshitij may have a fix (I warned him about this commit).

bug 374 (was found through fuzzing 2012-07-18)

"Possible soundness problem somewhere in the solver
(assertion failure in DE)"

Replace propagateAsDecision() with Theory::getNextDecisionRequest():

* arrays now uses the new approach by using a CDQueue<>
* uf strong solver has had the feature disabled, pending a merge from Andy
* theory kinds files now have a getNextDecisionRequest property (if you want to take part in such decision requests you have to list that property)
* the staticLearning property has been renamed ppStaticLearn to match the function name
* theory kinds files are now checked again for correctly-declared properties (this had been disabled)
* minor documentation and other fixups

ArrayStoreAll should (for now) only allow constant expressions, as it is itself a CONSTANT.

fix exceptions and mkConst() in java binding

some fixes for language bindings

Fixes to integer wrapper classes:
* more uniform interface between the CLN and GMP wrappers
* support base inference (base == 0) on parsing strings with the CLN wrapper; this was a difference from the GMP wrapper (resolves bug #372)

Implements TheoryArith::collectModelInfo().  The current implementation is quite basic. This may need to be revisited.

Adds substituteDelta() to DeltaRational which given a value for delta returns the corresponding rational value.

Switched TheoryModel assertEqualityEngine to use const Equality Engine pointers.

Switched a number of EqClassIterator operations to const as well as the internal EqualityEngine pointer.

fix integer parsing error.. thanks dejan for the report.  this indicates that we have a problem with our Integer class though; it appears to behave differently for GMP and CLN

Make a few functions in TheoryEngine (like theoryOf()) const.

Minor cleanup.  No performance difference expected.

minor isConst()-related fixes to printing; also add some debugging stuff to see how isConst() operates: use -d isConst

Fix --no-checking option.

Public interface review items:

* don't document internal-only stuff (like DefaultCleanup for CDLists)
* NoSuchFunctionException -> TypeCheckingException

small fixes

some fixes to command and declaration tab-completion in interactive shell

Some items from the CVC4 public interface review:

* rename DeclarationScope to SymbolTable
* rename all HashStrategy -> HashFunction (which we often have anyways)
* remove CDCircList (no one is currently using it)

Fix SmtEngine::setInfo() handling for certain keys.  This fixes the "unsupported" message we see in QF_SAT nightly regressions.

Support setting :regular-output-channel and :diagnostic-output-channel.
Also some cleanup of option-related exceptions infrastructure.

removing the sat solver inmterface from being public

Cleanup of some command stuff, fixes broken Java build.

fix constant printing for datatypes

Disable failing datatypes regression, pending solution to bug #370.

isConst() rule for datatypes

the array-store "construle" for isConst

Comparisons for LogicInfos, and associated tests

ArrayStoreAll infrastructure

fix uses of getMetaKind() from outside the expr package.  (they now use isConst() and isVar() as appropriate)

also some base infrastructure for the new ::isConst().

fix for proofs-enabled builds

better parser makefile fix

fixes to paths in parser makefiles; if you've noticed strange SMT2 parser behavior the last couple days, this should fix it

array-store-all class

add isFinished() to type enumerators (so we don't rely on exception-throwing after exhaustively enumerating finite types), also fix a standards-related FIXME in SmtEngine by clarifying the text of an error message

a couple fixes to SmtEngine::setOption().  thanks Andy for the report!

fixes to some *clean targets

fix for the SmtEngine::beforeSearch() option predicate

some fixes for Mac OS

fixes for portfolio

Moving some instantiation-related stuff from src/theory to src/theory/quantifiers and src/theory/rewriterules.  This unclutters the src/theory directory somewhat.

The namespaces weren't changed, only the file locations.

fix some file documentation

Options merge.  This commit:

1. changes the way options are declared (see http://church.cims.nyu.edu/wiki/Options)
2. moves module-specific options enumerations (SimplificationMode, DecisionMode, ArithUnateLemmaMode, etc.) to their own header files, also they are no longer inside the Options:: class namespace.
3. includes many SMT-LIBv2 compliance fixes, especially to (set-option..) and (get-option..)

The biggest syntactical changes (outside of adding new options) you'll notice are in accessing and setting options:

* to access an option, write (e.g.) options::unconstrainedSimp() instead of Options::current()->unconstrainedSimp.
* to determine if an option value was set by the user, check (e.g.) options::unconstrainedSimp.wasSetByUser().
* ensure that you have the option available (you have to #include the right module's options.h file, e.g. #include "theory/uf/options.h" for UF options)
*** this point is important.  If you access an option and it tells you the option doesn't exist, you aren't #including the appropriate options.h header file ***

Note that if you want an option to be directly set (i.e., other than via command-line parsing or SmtEngine::setOption()), you need to mark the option :read-write in its options file (otherwise it's read-only), and you then write (e.g.) options::unconstrainedSimp.set(true).

Adding new options is incredibly simple for primitive types (int, unsigned, bool, string, double).  For option settings that you need to turn into a member of an enumerated type, you write a custom "handler" for the option---this is no additional work than it was before, and there are many examples to copy from (a good one is stringToSimplificationMode() in src/smt/options_handlers.h).

Benefits of the new options system include:

1. changes to options declarations don't require a full-source rebuild (you only have to rebuild those sources that depend on the set of options that changed).
2. lots of sanity checks (that the same option isn't declared twice, that option values are in range for their type, that all options are documented properly, etc.)
3. consistency: Boolean-valued option --foo gets a --no-foo automatically, documentation is generated consistently, the option-parsing matches the documented option name, etc.
4. setting options programmatically via SmtEngine::setOption() is enabled, and behaves the same as command-line equivalents (including checking the value is in range, etc.)
5. the notion of options being "set by the user" is now primitive; you can use (e.g.) options::unconstrainedSimp.wasSetByUser() instead of having to use (and maintain) a separate Boolean option for the purpose

I've taken lots of care not to break anything.  Hopefully, I've succeeded in that.

Minor cleanup after today's commits:

* change some uses of "std::cout" to "Message()"

* change some files to use Unix newlines instead of DOS newlines

* fix compiler warning

removing unecessary files

merging fmf-devel branch, includes refactored datatype theory, updates to model.h/cpp to prepare for release, and major refactoring of quantifiers/finite model finding.  Note that new datatype theory does not insist upon any interpretation for selectors applied to incorrect constructors and consequently some answers may differ with previous version

Merge quantifiers2-trunk:
   - new syntax for rewrite rules
   - better rewrite rules theory
   - remove the rewriting with rewrite rules during ppRewrite temporarily
   - theory can define their own candidate generator
   - define a general candidate generator (inefficient ask to every theory)
   - split inst_match between the pattern matching used for quantifiers (inst_match.*) and
     the one used for rewrite rules (rr_inst_match.*):
      - the pattern matching is less exhaustive for quantifiers,
      - the one for rewrite rules can use efficient-e-matching.

Datatype enumerator work.  This version is not a "fair" enumerator, but I got it in quickly for Andy.

A "fair" version forthcoming.

more compliance fixes for SMT-LIBv2

a few fixes for java system test

small change to model-generation function, after discussion w/ Andy

removing an obsolete assertion in model-generation framework, per Andy's request

removing output operator for SExprTypes, which is never used (and SExprTypes is not public-facing)---this fixes the language bindings, which fixes the broken debian build overnight

SMT-LIBv2 compliance updates:

* more correct support for get-info responses
* printer infrastructure extended to SExprs
* parser updates to correctly handle symbols and strings
  (there were some minor differences from the spec)

minor fix to prevent getValue from returning null

fix for --produce-models with CVC4 presentation language

fix an obvious oversight: "distinct" wasn't part of the SMT2 core theory---but this only gave trouble in strict parsing mode

now passes "make distcheck", which does important checks for the release (e.g., "make dist" produces a distribution that passes "make dist" and "make check", "make uninstall" actually uninstalls, "make distclean" actually cleans, ...)

fix compiler warning in unit test

stronger two_smt_engines test

fix inadvertent change to system test

Support for having two SmtEngines with the same ExprManager.

Basically, this involves creating a separate StatisticsRegistry for the
ExprManager and for the SmtEngine.  Otherwise, theories register the
same statistic twice.  This is a larger problem, though, for creating
multiple instances of theories, and that is unaddressed.  Still,
separating out the expr statistics into a separate registry is probably
a good idea, since the expr package is somewhat separate anyway (and in
the short term it allows two SmtEngines to co-exist).

found a bug in the initialization order of UF, EqualityEngine, and the UF strong solver; fixed

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