| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
This PR cleans up a ton of includes, based on the suggestions of iwyu.
Mostly, it removes includes from header files in favor of forward declarations and adds includes to source files.
|
|
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
|
|
|
|
|
|
Fixes 2887.
|
|
|
|
C++11 supports explicitly deleting functions that should not be used
(explictly or implictly), e.g. copy or assignment constructors. We were
previously using the CVC4_UNDEFINED macro that used a compiler-specific
attribute. The C++11 feature should be more portable.
|
|
|
|
|
|
|
|
CDHashMap garbage.
|
|
|
|
context/ classes, and their subclasses. Fixes compilation issues with clang 3.5 and -std=c++11 'exception specification of overriding function is more lax than base version' for a couple of different classes.
|
|
|
|
What to Know As a User:
A number of files have moved. Users that include files in the public API in more refined ways than using #include <cvc4.h> should consult which files have moved. Note though that some files may move again after being cleaned up. A number of small tweaks have been made to the swig interfaces that may cause issues. Please file bug reports for any problems.
The Problem:
The build order of CVC4 used to be [roughly] specified as:
options < expr < util < libcvc4 < parsers < main
Each of these had their own directories and their own Makefile.am files. With the exception of the util/ directory, each of the subdirectories built exactly one convenience library. The util/ directory additionally built a statistics library. While the order above was partially correct, the build order was more complicated as options/Makefile.am executed building the sources for expr/Makefile.am as part of its BUILT_SOURCES phase. This options/Makefile.am also build the options/h and options.cpp files in other directories. There were cyclical library dependencies between the first four above libraries. All of these aspects combined to make options extremely brittle and hard to develop. Maintaining these between clang versus gcc, and bazel versus autotools has become increasing unpredictable.
The Solution:
To address these cyclic build problems, I am simplifying the build process. Here are the main things that have to happen:
1. util/ will be split into 3 separate directories: base, util, and smt_util. Each will have their own library and Makefile.am file.
2. Dependencies for options/ will be moved into options/. If a type appears as an option, this file will be moved into options.
3. All of the old options_handlers.h files have been refactored.
4. Some files have moved from util into expr/ to resolve cycles. Some of these moves are temporary.
5. I am removing the libstatistics library.
The constraints that the CVC4 build system will eventually satisfy are:
- The include order for both the .h and .cpp files for a directory must respect the order libraries are built. For example, a file in options/ cannot include from the expr/ directory. This includes built source files such as those coming from */kinds files and */options files.
- The types definitions must also respect the build order. Forward type declarations will be allowed in exceptional, justified cases.
- The Makefile.am for a directory cannot generate a file outside of the directory it controls. (Or call another Makefile.am except through subdirectory calls.)
- One library per Makefile.am.
- No extra copies of libraries will be built for the purpose of distinguishing between external and internal visibility in libraries for building parser/ or main/ libraries and binaries. Any function used by parser/ and main/ will be labeled with CVC4_PUBLIC and be in a public API. (AFAICT, libstatistics was being built exactly to skirt this.)
The build order of CVC4 can now be [roughly] specified as
base < options < util < expr < smt_util < libcvc4 < parsers < main
The distinction between "base < options < util < expr" are currently clean. The relationship between expr and the subsequent directories/libraries are not yet clean.
More details about the directories:
base/
The new directory base/ contains the shared utilities that are absolutely crucial to starting cvc4. The list currently includes just: cvc4_assert.{h,cpp}, output.{h,cpp}, exception.{h,cpp}, and tls.{h, h.in, cpp}. These are things that are required everywhere.
options/
The options/ directory is self contained.
- It contains all of the enums that appear as options. This includes things like theory/bv/bitblast_mode.h .
- There are exactly 4 classes that handled currently using forward declarations currently to this: LogicInfo, LemmaInputChannel, LemmaOutputChannel, and CommandSequence. These will all be removed from options.
- Functionality of the options_handlers.h files has been moved into smt/smt_options_handler.h. The options library itself only uses an interface class defined in options/options_handler_interface.h. We are now using virtual dispatch to avoid using inlined functions as was previously done.
- The */options_handlers.h files have been removed.
- The generated smt/smt_options.cpp file has been be replaced by pushing the functionality that was generated into: options/options_handler_{get,set}_option_template.cpp . The non-generated functionality was moved into smt_engine.cpp.
- All of the options files have been moved from their directories into options/. This means includes like theory/arith/options.h have changed to change to options/arith_options.h .
util/
The util/ directory continues to contain core utility classes that may be used [almost] everywhere. The exception is that these are not used by options/ or base/. This includes things like rational and integer. These may not use anything in expr/ or libcvc4. A number of files have been moved out of this directory as they have cyclic dependencies graph with exprs and types. The build process up to this directory is currently clean.
expr/
The expr/ directory continues to be the home of expressions. The major change is files moving from util/ moving into expr/. The reason for this is that these files form a cycle with files in expr/.
- An example is datatype.h. This includes "expr/expr.h", "expr/type.h" while "expr/command.h" includes datatype.h.
- Another example is predicate.h. This uses expr.h and is also declared in a kinds file and thus appears in kinds.h.
- The rule of thumb is if expr/ pulls it in it needs to be independent of expr/, in which case it is in util/, or it is not, in which case it is pulled into expr/.
- Some files do not have a strong justification currently. Result, ResourceManager and SExpr can be moved back into util/ once the iostream manipulation routines are refactored out of the Node and Expr classes.
- Note the kinds files are expected to remain in the theory/ directories. These are only read in order to build sources.
- This directory is not yet clean. It contains forward references into libcvc4 such as the printer. It also makes some classes used by main/ and parser CVC4_PUBLIC.
smt_util/
The smt_util/ directory contains those utility classes which require exprs, but expr/ does not require them. These are mostly utilities for working with expressions and nodes. Examples include ite_removal.h, LemmaInputChannel and LemmaOutputChannel.
What is up next:
- A number of new #warning "TODO: ..." items have been scattered throughout the code as reminders to myself. Help with these issues is welcomed.
- The expr/ directory needs to be cleaned up in a similar to options/. Before this happens statistics needs to be cleaned up.
|
|
|
|
|
|
|
|
|
|
|
|
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.)
|
|
make it unambiguous for case-insensitive filesystems like on Mac. Fixes Mac builds
|
|
* notifications are now through the interface subclass instead of a template
* notifications include constants being merged
* changed contextNotifyObj::notify to contextNotifyObj::contextNotifyPop so it's more descriptive and doesn't clutter methods when subclassed
* sat solver now has explicit methods to make true and false constants
* 0-level literals are removed from explanations of propagations
|
|
CDSet -> CDHashSet
|
|
upcoming internal branch-&-bound for integers)
|
|
and model gen also.
I also expect this commit to fix bug #273.
No performance change is expected on regressions with this commit, see
http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863
|
|
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.
|
|
|
|
on some problems---valgrind gave many complaints): the problem was that calloc() (in the Backtracker) wasn't allocating enough space for the type located at the resulting address. Resolves bug #263.
Also, some debugging improvements.
|
|
are somewhat disparate but belonged on the same branch because they were
held back from trunk all for the same reason (to keep the trunk stable
for furious bitvector development). Dejan has now given me the go-ahead
for a merge.
=========================================
THIS COMMIT CHANGES THE THEORY INTERFACE!
=========================================
Theory constructors are expected to take an additional "Valuation*"
parameter that each Theory should send along to the base class
constructor. The base class Theory keeps the Valuation* in a
d_valuation field for use by it and by its derived classes.
Theory::getValue() no longer takes a Valuation* (it is expected
to use d_valuation instead). This allows other theory functions
to take advantage of getValue() for debugging or heuristic
purposes.
TODO BEFORE MERGE TO TRUNK:
****implement BitIterator find() in CDAttrHash<bool>.
Specifically:
* Added QF_BV support for SMT-LIB v2.
* Two adjustments to the theory interface as requested by Tim King:
1. As described above.
2. Theories now have const access to the fact queue through base
class functions facts_begin() and facts_end(); useful for
debugging.
* Added an "Asserted" attribute so that theories can check if something
has been asserted or not (and therefore not propagate it). However, this
has been disabled for now, pending more data on the overhead of it, and
pending discussion at the 3/25/2011 meeting.
* Do not define NDEBUG in MiniSat in assertion-enabled builds (so
that MiniSat asserts are evaluated).
* As a result of the new MiniSat assertions, some --incremental
regressions had to be disabled; also, some bitvectors ?!!
* Bug 71 is resolved by adding a specialization for CDAttrHash<> in the
attribute package.
* Fixes for some warnings flagged by clang.
* System tests have arrived! So far mainly infrastructure for having
system tests, but there is a system test aimed at improving code
coverage of the printer package.
* Minor other adjustments to documentation and coding to be more
conformant to CVC4 policy.
Tests have been performed to demonstrate that these changes have no or
negligible effect on performance. In particular, changing the
CDAttrHash<> doesn't have any real effect on performance or memory right
now, since there is only one context-dependent boolean flag (as soon
as another is added, the effect is noticeable but probably still slight).
|
|
|
|
|
|
|
|
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.
|
|
|
|
+ Context* getContext() -- gets the context
+ ContextMemoryManager* getCMM() -- gets the CMM
+ int getLevel() -- the scope level of the ContextObj's most recent update
+ bool isCurrent() -- true iff the most recent update is the current top level
In particular, the ContextObj::getCMM() call cleans up by TheoryUF's
ECData::addPredecessor() function substantially (re: code review bug #64).
* Fix serious bugs in context operations that corrupted the ContextObj
linked lists. Closes bug #85.
* Identified a bug in the way objects of the "Link" class are
allocated; see bug #96.
* Re-enable context white-box tests that ensure proper links in linked
lists. Closes bug #86.
* Re-enable CDMap<>::emptyTrash(). Closes bug #87.
* Add a tracing option (-t foo or --trace foo) to the driver to enable
Trace("foo") output stream. -d foo implies -t foo.
* Minor clean-up of some TheoryUF code; addition of some documentation
(re: code review bug #64).
* Address some things that caused Doxygen discomfort.
* Address an issue raised in NodeManager's code review (bug #65).
* Remove an inaccurate comment in Attribute code (re: code review bug #61).
|
|
instead of assuming it's atomic based on kind. Atomicity is
determined at node building time. Fixes bug #81. If this is
determined to make node building too slow, we can allocate another
attribute "AtomicHasBeenComputed" to lazily compute atomicity.
* TheoryImpl<> has gone away. Theory implementations now derive from
Theory directly and share a single RegisteredAttr attribute for term
registration (which shouldn't overlap: every term is "owned" by
exactly one Theory). Fixes bug #79.
* Additional atomicity tests in ExprBlack unit test.
* More appropriate whitebox testing for attribute ID assignment
(AttributeWhite unit test).
* Better (and more correct) assertion checking in NodeBuilderBlack.
* run-regression script now checks exit status against what's provided
in "% EXIT: " gesture in .cvc input files, and stderr against
"% EXPECT-ERROR: ". These can be used to support intended failures.
Fixes bug #84. Also add "% EXIT: " gestures to all .cvc regressions
in repository.
* Solved some "control reaches end of non-void function" warnings in
src/parser/bounded_token_buffer.cpp by replacing
"AlwaysAssert(false)" with "Unreachable()" (which is known
statically to never return normally).
* Regression tests now use the cvc4 binary under
builds/$(CURRENT_BUILD)/src/main instead of the one in bin/ which
may not be properly installed yet at that point of the build.
(Partially fixes bug #46.)
* -fvisibility=hidden is now included by configure.ac instead of each
Makefile.am, which will make it easier to support platforms
(e.g. cygwin) that do things a different way.
* TheoryUF code formatting. (re: my code review bug #64)
* CDMap<> is leaking memory again, pending a fix for bug #85 in the
context subsystem. (To avoid serious errors, can't free context
objects.)
* add ContextWhite unit test for bug #85 (though it's currently
"defanged," awaiting the bugfix)
* Minor documentation, other cleanup.
|
|
If there is more cleanup to do, it has to be done by the destructor.
|
|
CDList, and CDMap. Added the d_underTheShotgun field to NodeManager to keep track of which NodeValue is currently being deleted. If a Node or TNode has this node value, it can always be deleted. This avoids the need for introducing SoftNodes. Currently passes Debug and Production make check
|
|
|
|
with old iterator (closes bug #47).
* src/context/cdset.h: implemented.
* src/expr/node_builder.h: fixed all the strict-aliasing warnings.
* Remove Node::hash() and Expr::hash() (they had been aliases for
getId()). There's now a NodeValue::internalHash(), for internal
expr package purposes only, that doesn't depend on the ID. That's
the only hashing of Nodes or Exprs.
* Automake-quiet generation of kind.h, theoryof_table.h, and CVC and
SMT parsers.
* various minor code cleanups.
|
|
expr/node.h). This removes the warnings we had during compilation,
and heads off a number of potential linking errors due to improper
inlining of private (library-only) stuff in client (out-of-library)
code.
* "configure" now takes some options as part of a "bare-option" build
type (e.g., "./configure debug-coverage" or "./configure production-muzzle").
* split cdo.h, cdlist.h, cdmap.h, and cdset.h from context.h
* split cdlist_black unit test from context_black
* implement CDMap<>.
* give ExprManagers ownership of the context (and have SmtEngine share
that one)
* fix main driver to properly report file-not-found
* fix MemoryMappedInputBuffer class to report reasons for
"errno"-returned system errors
* src/expr/attribute.h: context-dependent attribute kinds now
supported
* test/unit/expr/node_white.h: context-dependent attribute tests
* src/prop/cnf_conversion.h and associated parts of src/util/options.h
and src/main/getopt.cpp: obsolete command-line option, removed.
* src/util/Assert.h: assertions are now somewhat more useful (in debug
builds, anyway) during stack unwinding.
* test/unit/theory/theory_black.h: test context-dependent behavior of
registerTerm() attribute for theories
* src/expr/node_builder.h: formatting, fixes for arithmetic
convenience node builders, check memory allocations
* test/unit/expr/node_builder_black.h: add tessts for addition,
subtraction, unary minus, and multiplication convenience node
builders
* src/expr/attribute.h: more comments
* (various) code formatting, comment cleanup, added throws specifier
to some destructors
* contrib/code-checker: prototype perl script to test (some) code policy
* contrib/indent-settings: command line for GNU indent to indent using
CVC4 style (sort of; this is a work in progress)
* COPYING: legal stuff
* DESIGN_QUESTIONS: obsolete, removed
|
|
instead of the assignment operator. This is important as Nodes, for example, check that d_nv != NULL in the assignemnt operator.
* node.h - Simplified the constructors, apparently it's ok to write ~ref_count in the template declaration. All the constructed nodes are now the ref-counted ones, i.e. eqNode() will return a ref-counted node.
|
