Age | Commit message (Collapse) | Author |
|
|
|
|
|
* 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
|
|
|
|
You may have to reconfigure after this update.
|
|
test/unit/expr/node_white.h: add whitebox attribute test (pulled out
attribute stuff from node_white)
* test/unit/parser/parser_black.h: fix memory leaks uncovered by
valgrind
* src/theory/interrupted.h: actually make this "lightweight" (not
derived from CVC4::Exception), as promised in my last commit
* src/theory/uf/theory_uf.h, test/unit/expr/attribute_black.h: match
the new-style cleanup function definition
* src/expr/attribute.cpp, src/expr/attribute.h: support for attribute
deletion, custom cleanup functions, clearer cleanup function
definition.
* src/expr/node_manager.h, src/expr/node_manager.cpp: reclaim
remaining zombies in dtor, rename NodeValueSet ==> "NodeValuePool",
and enable freeing of NodeValues
* src/expr/type.h, src/expr/type.cpp: reference-counting for types,
customized cleanup function for types, also code cleanup
* (various): changed "const Type*" to "Type*" (to enable
reference-counting etc. Types are still immutable.)
* src/util/output.h: add ::isOn()-- which queries whether a
Debug/Trace flag is currently on or not.
* src/smt/smt_engine.cpp, src/parser/antlr_parser.cpp,
src/expr/type.cpp, src/expr/expr_manager.cpp, various others:
minor code cleanup
|
|
* CVC4::theory::Interrupted no longer derives CVC4::Exception.
* Interrupted is only thrown if "safe" parameter is TRUE !
* UF returns one conflict (instead of waiting for Interrupted to be thrown).
* Minor build system work (quieter builds if V=0, better handling of build
profiles in configure)
|
|
DecisionEngine, and Theory. These are triggered from the SmtEngine
dtor before the other engines are deleted. This is important
because of potential issues with outstanding TNodes in Theory
implementations (which fail if the destruction is done in the wrong
order, in certain cases).
* Favor "FactQueueResetter" instead of clearAssertionQueues() for
resetting facts queue in Theory implementations.
* Better theory-rewriting code.
* Minor cleanups.
|
|
* implement zombification and garbage collection of NodeValues
(but GC not turned on yet)
* implement removal of key nodes from all attribute tables
* audit NodeBuilder and fix memory leaks and improper reference-count
management. This is in many places a re-write. Clearly documented
invariants on NodeBuilder state. (Closes Bug 38)
* created a "BackedNodeBuilder" that can be used to construct
NodeBuilders with a stack-based backing store for a size that's not
a compile-time constant.
* NodeValues no longer depend on Node for toStream()'ing
* make unit test-building "silent" with --enable-silent-rules
* (Makefile.am, Makefile.builds.in) fix top-level build system so that
"make regressN" works with unbuilt/out-of-date source trees in the
expected way.
* (various) code cleanup, documentation, formatting
|
|
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
|
|
(etc.) now work for Nodes a, b, c, d, e. Also refcounting fixes for
NodeBuilder in certain cases
* (various places) don't overload __gnu_cxx::hash<>, instead provide
an explicit hash function to hash_maps and hash_sets.
* add a new kind of assert, DtorAssert(), which doesn't throw
exceptions (right now it operates like a usual C assert()). For use
in destructors.
* don't import NodeValue into CVC4 namespace (leave under CVC4::expr::).
* fix some Make rule dependencies
* reformat node.h as per code formatting policy
* added Theory and NodeBuilder unit tests
|
|
marginal improvement (<5%) on big benchmarks.
|
|
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).
|
|
* configure.ac, test/unit/Makefile.am: Resolved an issue where even
when not testing, one unit test was built.
* Re-ran contrib/update-copyright.pl on all source files to ensure
consistent and correct header comments.
* contrib/get-authors: Change definition of "minor contributor"
to >= 10% of lines (rather than strictly greater than 10% of lines)
|
|
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
|
|
|
|
|
|
|
|
please look to see if it makes sense.
|
|
conversation with Tim
|
|
cvc4-c++-editing-mode from contrib/editing-with-emacs
|
|
SAT-INVALID/UNSAT-VALID
|
|
Build src/expr before src/util.
Moved CVC4::Command to the expr package.
Re-quieted the "result is sat/invalid" etc. from PropEngine (this is
now done at the main driver level).
Added file-level documentation to Antlr sources
When built for debug, spin on SEGV instead of aborting. Really useful
for debugging problems that crop up only on long runs. Added
'--segv-nospin' to override this spinning so that "make check,"
nightly regressions, etc. don't hang when built with debug.
Updated src/main/about.h for 2010.
|
|
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.
|
|
|
|
|
|
|
|
for multiple-query cases
|
|
various cleanups; renamed numChildren() to getNumChildren() and added it to NodeBuilder interface; fancier, non-exponential CNF conversion with variable introduction is still buggy (?)
|
|
|
|
NodeBuilder. outstanding SEGVs fixed
|
|
|
|
|
|
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()
|
|
public tests
|
|
by "make production ASSERTIONS=1")
|
|
Makefile.am files - remove obsolete INCLUDES, incorporate into AM_CPPFLAGS
Makefile files in src/ - support "make" under src/ (current build profile)
configure.ac - updates to fix warnings
config/antlr.m4 - updates to fix warnings
autogen.sh - updates to generate warnings from autotools; also support Macs
src/include/cvc4_config.h - guard with #ifdef
total reimplementation of NodeBuilder
ExprValue => NodeValue
context_mm.{h,cpp} - fixed numerous compile errors
|
|
optimized expressions and the internal expression manager.
|
|
|
|
|
|
|
|
and build process
|
|
due to some problems in the prop_engine
* default null expr and expr value and reorganisation/rewrite of some methods
* fixed some bugs
* expressions should always be passed as const Expr& to methods, otherwise copy constructors are called
Problematic code:
* Expr class has a bunch of methods that return Exprs, such as a.andExpr(b). None of these know what is their expression manager. We should
(a) Not allow this, all expression construction should go through the ExprBuilder or directly thorugh the expression manager
(b) Allow this, as it is now, but the have the default expression manager be setup in every entry into the smt solver + these construction methods shouldn't be available to the user (oterwise a mess ensues)
* We have to decide how to construct ExprBuilders:
(a) constructing ExprBuilders with em = ExprBuilder(e).andExpr(b) is problematic as at construction we can't know the expression manager, and the kind of em will be UNDEFINED, so when adding b we can't assume its not UNDEFINED
(b) constructing it with ExprBuilder(em) << AND << a << b or ExprBuilder(em, AND) << a << b seems like a nicer approach
I am still confused about these expression builders so we should talk about this.
|
|
found handling
|
|
expressions, output classes, and minisat
|
|
|
|
yet to be finalized, it should work as expected
|