| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
just the header comments at the top, though. Don't update to this rev if
you don't have time for a complete rebuild, and exclude this rev if you
want to see what's new across a range of commits.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
gestures both.
|
|
Dump("foo") << FooCommand(...);
now "dumps" the textual representation of the command (in the current
output language) to a file, IF dumping is on at configure-time, AND the
"muzzle" feature is off, AND the "foo" flag is turned on for the dump
stream during this run.
If it's a portfolio build, the above will also store the command in a
CommandSequence, IF the "foo" flag is turned on for the dump stream
during this run. This is done even if the muzzle is on.
This commit also cleans up some code that used the dump feature (in arrays,
particularly).
|
|
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
|
|
* Preprocessing-time, non-clausal, Boolean simplification round to
support "quasi-non-linear rewrites" as discussed at last few meetings.
* --simplification=none is the default for now, but we'll probably
change that to --simplification=incremental. --simplification=batch
is also a possibility. See --simplification=help for details.
* RecursionBreaker<T> now uses a hash set for the seen trail.
* Fixes to TLS stuff to support that.
* Fixes to theory and SmtEngine documentation.
* Fixes to stream indentation.
* Other miscellaneous stuff.
|
|
simplifications for the "muzzled" (i.e. competition) design, which had
been broken. Addition of some new unit test bits to ensure that
nothing is ever called in muzzled builds, e.g. things like
Warning() << expensiveFunction();
Also, fix some compiler warnings.
|
|
(propositional) assignment for theory atoms.
Fixed Debug/Trace as discussed in bug ticket #252 and on the mailing list.
This implementation leads to some compiler warnings in production builds,
but these will be corrected in coming days. There appears to be a small
speedup in the parser as a result of this fix:
http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=1902&reference_id=1886&p=5
Cleaned up a few CD Boolean attribute things.
Various small fixes to coding guidelines / test coverage.
This commit:
* Resolves bug 252 (tracing not disabled in production builds)
* Resolves bug 254 (implement CDAttrHash<>::BitIterator::find())
|
|
documentation, and make it possible to "make doc" on a clean source tree (post-configure)
|
|
coding standards
|
|
minor code
cleanup found while searching for additional cases. Closes bug 171.
|
|
should have no impact on production performance and speed up debug
performance considerably, while making the code much cleaner. On some
benchmarks, debug builds now run _much_ faster.
We no longer have to sprinkle our code with things like:
if(debugTagIsOn("context")) {
Debug("context") << theContext << std::endl;
}
which we had to do to get around performance problems previously.
Now just writing:
Debug("context") << theContext << std::endl;
does the same in production and debug builds. That is, if "context"
debugging is off, theContext isn't converted to a string, nor is it
output to a "/dev/null" ostream. I've confirmed this. In production
builds, the whole statement inlines to nothing. I've confirmed this
too.
Also, "Debug" is no longer a #definition, so you can use it directly
in production builds where you couldn't previously, e.g.
if(Debug.isOn("paranoid:check_tableau")) {
checkTableau();
}
I'm leaving debugTagIsOn() for now, but marking it as deprecated.
|
|
** file-level documentation at the top of the sources. **
This is the "make bugzilla stop bugging me" bugfix commit.
* Remove BackedNodeBuilder<> and collapse NodeBuilder<> hierarchy.
Updated documentation in the file. Resolves bug #99.
* Convenience NodeBuilders (PlusNodeBuilder, OrNodeBuilder, etc.)
moved into a separate file. Partially resolves bug #100.
* Moved isAssociative(Kind) into kind.h (and into the CVC4::kind
namespace) instead of metakind.h (where it was in CVC4::metakind).
This clears up a warning (private #inclusion) from the SMT and SMT2
parsers, and maybe makes more sense anyways, since this is based on
the kind (and not the metakind) of an operator.
* Documentation improvement; doxygen top-level \file gestures, \brief
gestures for files, etc. Changed contrib/update-copyright.pl for
this change, and post-processed to add \brief. Resolves bug #98.
* Removed ExprManager::mkExpr(Kind) and NodeManager::mkNode(Kind).
They no longer made sense. Resolves bug #91.
|
|
* Other minor changes to the new parser to match coding guidelines,
add documentation, ....
* Add CFLAGS stuff to configure.ac parser Makefile.ams. This ensures
that profiling, coverage, optimization, debugging, and warning
level options will apply to the new parser as well (which is in C,
not C++). This fixes the deprecated warning we were seeing this
evening.
* Now, if you have ANTLR_HOME set in your environment, you don't need
to specify --with-antlr-dir to ./configure or have libantlr3c
installed in standard places. --with-antlr-dir still overrides
$ANTLR_HOME, and if the installation in $ANTLR_HOME is missing or
doesn't work, the standard places are still tried.
* Extend "silent make" to new parser stuff.
* Added src/parser/bounded_token_buffer.{h,cpp} to the list of
exclusions in contrib/update-copyright.pl and mention them as
excluded from CVC4 copyright in COPYING. They are antlr3-derived
works, covered under a BSD license.
OTHER STUFF:
* expr_manager.h, expr.h, expr_manager.cpp, and expr.cpp are now
auto-generated by a "mkexpr" script. This provides the correct
instantiations of mkConst() for public use, e.g., by the parser.
* Fix doxygen documentation in expr, expr_manager.. closes bug #35
* Node::isAtomic() implemented in a better way, based on theory kinds
files. Fixes bug #40. To support this, a "nonatomic_operator"
command has been added. All other "parameterized" or "operator"
kinds are atomic.
* Added expr_black test
* Remove kind::TRUE and kind::FALSE and make a new CONST_BOOLEAN kind
that takes a "bool" payload; for example, to make "true" you now do
nodeManager->mkConst(true).
* Make new "cvc4_public.h" and "cvc4parser_public.h" headers. Private
headers should include "cvc4_private.h"
(resp. "cvc4parser_private.h"), which existed previously. Public
headers should include the others. **No one** should include the
autoheader #include (which has been renamed "cvc4autoconfig.h")
directly, and public CVC4 headers can't access its #defines. This
is to avoid us having the same distribution problem as libantlr3c.
* Preliminary fixes based on Tim's code review of attributes (bug #61).
This includes splitting hairy template internals into
attribute_internals.h, for which another code review ticket will be
opened. Bug is still outstanding, but pending further
refactoring/documentation.
* Some *HashFcns renamed to *HashStrategy to match refactoring done
elsewhere (done by Chris?) earlier this week.
* Simplified creation of make rules for generated files (expr.cpp,
expr.h, expr_manager.cpp, expr_manager.h, theoryof_table.h, kind.h,
metakind.h).
* CVC4::Configuration interface and implementation split (so private
stuff doesn't leak into public headers).
* Some documentation/code formatting fixes.
* Add required versions of autotools to autogen.sh.
* src/expr/mkmetakind: fix a nonportable thing in invocation of "expr"
that was causing warnings on Red Hat.
* src/context/cdmap.h: add workaround to what appears to be a g++ 4.1
parsing bug.
|
|
from muzzled builds)
add public-facing CVC4::Configuration class that gives CVC4's (static)
configuration (whether debugging is enabled, assertions, version
information, etc...)
add some whitebox tests for assertions, output classes, and new
CVC4::Configuration class
main driver now gets about() information from CVC4::Configuration.
configure.ac now more flexible at specifying major/minor/release
versions of CVC4
add --show-config option that dumps CVC4's static configuration
commented option processing strings in src/main/getopt.cpp
fixed some compilation problems for muzzled builds.
fixed some test code for non-assertion builds (where no assertions are expected)
|
|
share memory words properly; also, implementations of some output functionality
|
|
|
|
cvc4-c++-editing-mode from contrib/editing-with-emacs
|
|
regenerated configure script
|
|
Some parts split into other bugs: 19, 20, 21.
Addressed concerns of bug 11 (util package code review).
Slight parser source file modifications: file comments, #included
headers in generated parsers/lexers
Added CVC4::Result propagation back through
MiniSat->PropEngine->SmtEngine->main(). Silenced MiniSat when
verbosity is not requested.
|
|
repository history; re-ran update-copyright.pl; cleaned up some things with make
|
|
+ regenerate configure script
+ add CVC4::Message output class
+ add some IllegalArgument() assertion things
+ rename NodeManager::mkExpr() to mkNode()
|
|
expressions, output classes, and minisat
|
