| Age | Commit message (Collapse) | Author |
|---|
|
|
|
* Fixes --hide-zero-stats (and really skips the 0 values)
* Removes the additional newline after each statistic
* Introduces theory::getStatsPrefix(TheoryId) to generate consistent
prefixes for statistics based on the theory id
(e.g., THEORY_BV -> "theory::bv").
|
|
|
|
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.
|
|
for the report.
|
|
and arith.
|
|
instantiation strategies moved from instantiators to central instantiation engine, removed instantiator objects, simplified rewrite rules candidate generator to use central equality engine, efficient e-matching now uses central equality engine
|
|
|
|
numerous bugfixes, and the cvc3 system test is enabled.
|
|
* 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
|
|
* rename DeclarationScope to SymbolTable
* rename all HashStrategy -> HashFunction (which we often have anyways)
* remove CDCircList (no one is currently using it)
|
|
|
|
|
|
support yet for enumerating arrays, or for enumerating non-trivial datatypes.
|
|
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
|
|
|
|
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.
|
|
|
|
* new "well-foundedness" type property (like cardinality) specified in
Theory kinds files; specifies well-foundedness and a ground term
* well-foundedness / finite checks in Datatypes now superseded by type
system isFinite(), isWellFounded(), mkGroundTerm().
* new "RecursionBreaker" template class, a convenient class that keeps
a "seen" trail without you having to pass it around (which is
difficult in cases of mutual recursion) of the idea of passing
around a "seen" trail
|
|
* Type::getCardinality() returns the cardinality for for all types.
Theories give a cardinality in the their kinds file. For
cardinalities that depend on a type argument, a "cardinality
computer" function is named in the kinds file, which takes a
TypeNode and returns its cardinality.
* There's a bitmap for the set of "active theories" in the
TheoryEngine. Theories become "active" when a term that is owned by
them, or whose type is owned by them, is pre-registered (run CVC4
with --verbose to see theory activation). Non-active theories don't
get any calls for check() or propagate() or anything, and if we're
running in single-theory mode, the shared term manager doesn't have
to get involved. This is really important for get() performance
(which can only skimp on walking the entire sub-DAG only if the
theory doesn't require it AND the shared term manager doesn't
require it).
* TheoryEngine now does not call presolve(), registerTerm(),
notifyRestart(), etc., on a Theory if that theory doesn't declare
that property in its kinds file. To avoid coding errors,
mktheorytraits greps the theory header and gives warnings if:
+ the theory appears to declare one of the functions (check,
propagate, etc.) that isn't listed among its kinds file properties
(but probably should be)
+ the theory appears NOT to declare one of the functions listed in
its kinds file properties
* some bounded token stream work
|
|
and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later.
|
|
get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly...
|
|
* added TheoryArith::preRewrite() to test and demonstrate
the use of pre-rewriting.
* array types and type checking now supported
* array type checking now supported
* theoryOf() dispatching properly to arrays now
* theories now required to implement a (simple) identify()
function that returns a string identifying them for
debugging/user output purposes
* added "builtin" theory to hold all built-in kinds and their
type rules and rewriting (currently only exploding distinct)
* fixed production build failure (regarding NodeSetDepth)
* removed an errant "using namespace std" in util/bitvector.h
(and made associated trivial fixes elsewhere)
* fixes to make unexpected exceptions more verbose in debug builds
* fixes to make multiple, cascading assertion fails simpler
* minor other fixes to comments etc.
|
|
|
|
* add NodeManagerWhite unit test
* change kind::APPLY to kind::APPLY_UF
* better APPLY handling: operators are no longer considered children
* more efficient pool lookup; the NodeValue doesn't have to be as fully constructed for the lookup to proceed
* extend DSL for kind declarations
+ new "theory" command declares a theory and its header. theory_def.h no longer required.
+ arity enforced on operators
+ constant mapping, hashing, equality
* CONSTANT metakinds supported (via Node::getConst<T>(), for example, Node::getConst<CVC4::Rational>() gets a Rational out of a Node (assuming it is of CONST_RATIONAL kind)
* added CONST_RATIONAL and CONST_INTEGER kinds
* builtin operators (AND, OR, PLUS, etc..) returned by Node::getOperator() are now CONSTANT metakind and are created by NodeManager
* Pretty-printing of Nodes now has a depth limit settable by a stream manipulator (e.g. "cout << Node::setdepth(5) << m << endl;" prints DAG rooted at m to a depth of 5)
* getters added to Node, TNode, NodeValue, etc., for operators and metakinds
* build-time generators for kind.h, metakind.h, and theoryof_table.h headers now have a simpler design and flag errors better, and the templates (kind_template.h etc.) are easier to understand.
* DISTINCT is now a kind, and the SMT parser now passes through DISTINCT nodes instead of blowing them up into ANDs. Until theory rewriting is online, though, DISTINCTs are directly blown up into conjunctions in TheoryEngine::rewrite().
* add gmpxx detection and inclusion
* better Asserts throughout, some documentation, cleanup
|
|
different "kinds of kinds" (special, operator, parameterized, and constant), and permits doxygen comments on them
|
|
test behavior of grow(), which was previously very broken, fixed by
Tim earlier this afternoon.
* add the notion of a "private header". Private header files (those
not intended for distribution) should now #include "cvc4_private.h"
(or "cvc4parser_private.h" for the parser code). When not actually
building libcvc4 (resp. libcvc4parser), or associated unit tests, a
warning is emitted by the preprocessor. This should make it easier
to notice (and disentangle early) any unwanted public/private
mixing. Currently the warning identifies a couple places where we
need to fix things.
* added directory infrastructure for arrays and BV theories.
* the Theory inheritance hierarchy makes some assumptions about the
way inheritance is done. These are checked at runtime when
CVC4_ASSERTIONS is on. See src/theory/theory.h's TheoryImpl<>
definition for details.
* src/theory/booleans/theory_bool.h, src/theory/booleans/theory_def.h,
src/theory/arith/theory_arith.h, src/theory/arith/theory_def.h,
src/theory/uf/theory_uf.h, src/theory/uf/theory_def.h,
src/parser/antlr_parser.h: minor code formatting fixes as per
policy.
* src/theory/uf/theory_uf.cpp: fix for non-debug builds.
* src/util/options.h, src/util/model.h, src/util/result.h,
src/expr/type.h: make CVC4_PUBLIC.
* src/util/decision_engine.h: no longer CVC4_PUBLIC.
* src/expr/expr_manager.cpp: ExprManager::booleanType() and
ExprManager::kindType() weren't returning a value ?! Fixed.
* src/expr/expr_manager.h, src/expr/node_manager.h: ExprManager no
longer depends on NodeManager (public/private interface mixing).
ExprManagerScope is an internal implementation detail, and is moved
to node_manager.h.
* src/expr/node.h: mark gdb debug routines as "used" so that GCC
always emits code for them (even though its static analysis shows
they're unused).
|
