| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
Fix the case in NodeBuilderBlack that triggered bug #82. (Fixes bug #82.)
This also fixes regression failures from this morning (2010 Apr 4), in
the optimized builds, for which a fix was included in 365 and reverted
in 375. They looked like this:
In ExprBlack::testGetConst:
/usr/local/share/cvc4/src/cvc4-2010-04-04/builds/x86_64-unknown-linux-gnu/production/../../../test/unit/expr/expr_black.h:377: Error: Expected (a->getConst<Kind>()) to throw (IllegalArgumentException) but it didn't throw
/usr/local/share/cvc4/src/cvc4-2010-04-04/builds/x86_64-unknown-linux-gnu/production/../../../test/unit/expr/expr_black.h:378: Error: Expected (b->getConst<Kind>()) to throw (IllegalArgumentException) but it didn't throw
[etc..]
|
|
|
|
comments to files without them
|
|
Type code review and closed bug #25.
* Do assertions on Expr creation (public library interface) even when
assertions are off. Also a similar check for proper kind (in public
interface) when Expr::getConst<>() is called. This fixes a unit
test that was failing in production builds (an exception wasn't
thrown but should have been).
* kind::XOR must have exactly 2 arguments, not 2-or-more.
|
|
* 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.
|
|
|
|
|
|
|
|
* 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
|
|
Minor name changes for cleanup and hash function templates
|
|
different "kinds of kinds" (special, operator, parameterized, and constant), and permits doxygen comments on them
|
|
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
|
|
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)
|
|
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.
|
|
clauses and:
* adding the smallest test case (eq_diamond23.smt) that memouts in 50s
* adding the initial attributes black box test
|
|
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.
|
|
|
|
fixed some cleanup stuff.
|
|
the theories didn't get cleared on SatSolver backtracking so there were unasserted literals being returned as part of some conflicts. Sat solver now explicitely calls in the theory engine after it backtracks in order to clear the queues (clearAssertionQueues).
Also, changed the let.smt as it used to exibit "single literal conflict" problem. The sat solve can not except conflicts similar to (x != x), these should be rewritten to false during pre-processing.
Adding 3 more small problems from the library that we can solve now to the regressions.
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
TNode to a Node at one point in the code. TNode failed for a completely unknown reason. I'm try to isolate the problem is a bit, but I am commiting this for now so other things can move forward.
|
|
policy discussion (no dead code, no unimplemented unit tests...), and
other fixes:
* src/expr/node_builder.h: uncomment AndNodeBuilder, OrNodeBuilder,
PlusNodeBuilder, and MultNodeBuilder. (These had been dead code for
awhile.)
* src/expr/node_value.cpp: toString() is much more reasonable now,
printing S-exprs and using variable names (instead of printing raw
pointer values). Next, we'll want to define a pretty-printing
theory interface and perhaps hook this up to that.
* test/unit/expr/node_black.h: implement testIterator(),
testToString(), and testToStream().
* test/unit/expr/node_builder_black.h: implement testIterator() and
testAppend(), and add some code to avoid the warnings on clear() for
unused NodeBuilders.
* src/expr/node_builder.h: redefine "iterator" to be over Nodes rather
than over NodeValues. Doesn't make sense to expose the underlying
NodeValues. This shouldn't affect anyone, no one was using
NodeBuilder iterators.
* fix some comments in source code
|
|
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).
|
|
currently do not pass. (See bug 39.) I modified node.h/cpp to get gdb debug printing working again
|
|
corrected conflict generation to reflect this morning's discussion.
|
|
There remain memory leaks (and some over-decrementing of refcounts) that
I've identified; another commit forthcoming.
* src/expr/attribute.h: keys are now NodeValue* instead of TNode
* src/theory/output_channel.h: change OutputChannel::conflict() to the
negation of what we had before: it now takes an AND of TRUE literals
as a conflict clause rather than an OR of FALSE ones.
* src/expr/node.cpp: (non-template) CVC4::expr::debugPrint() routine
for use inside gdb
* src/expr/node.h: remove Node::debugPrint() member (now a function
instead of a member function, since Node is now a template it wasn't
being properly instantiated(?) and couldn't be called from gdb)
* src/expr/Makefile.am: add node.cpp
* src/expr/node_manager.h: code formatting
|
|
recognize an instantiation of the join conversion/copy ctor with
ref_count = ref_count_1 as a copy constructor. Problems with
reference counts ensue.
* src/theory/theory.h, src/theory/theory.cpp: Theory base
implementation work. Changed from continuation-style theory calls
to having an data member for the output channel. registerTerm() and
preRegisterTerm() work.
* src/theory/output_channel.h, src/theory/theory.h,
src/theory/theory.cpp, src/theory/uf/theory_uf.h,
src/theory/uf/theory_uf.cpp: merged ExplainOutputChannel into
OutputChannel.
* test/unit/expr/node_black.h: remove testPlusNode(),
testUMinusNode(), testMultNode().
* src/expr/attribute.h: new facilities ManagedAttribute<> and
CDAttribute<>, and add new template parameters to Attribute<>. Make
CDAttribute<>s work with context manager.
* src/expr/attribute.h, src/expr/node_manager.h: VarNameAttr and
TypeAttr are now "owned" (defined) by the NodeManager. The
AttributeManager knows nothing of specific attributes, it just as
all the code for dealing generically with attributes.
* test/unit/expr/node_white.h: test new attribute facilities.
* src/expr/soft_node.h: removed: We now have TNode, so SoftNode goes
away.
* src/theory/Makefile.am: fixed improper linking of theories
* src/theory/theory_engine.h: some implementation work (mainly stubs
for now, just to make sure TheoryUF can be instantiated properly,
etc.)
* src/expr/node_value.cpp, src/expr/node_value.h: move a number of
function implementations to the header and make them inline
* src/expr/node_manager.cpp, src/expr/node_manager.h: move a number of
function implementations to the header and make them inline
* src/theory/theoryof_table_prologue.h,
src/theory/theoryof_table_epilogue.h, src/theory/mktheoryof,
src/theory/Makefile.am: make the theoryOf() table from kinds and
implement TheoryEngine::theoryOf().
* src/theory/arith/Makefile, src/theory/bool/Makefile: generated these
stub Makefiles (with contrib/addsourcedir) as per policy
* src/theory/arith, src/theory/bool [directory properties]: add .deps
to svn:ignore.
* contrib/configure-in-place: permit configuring "in-place" in the
source directory.
* contrib/get-authors, contrib/dimacs_to_smt.pl,
contrib/update-copyright.pl, contrib/get-authors,
contrib/addsourcedir, src/expr/mkkind: copyright notice
* src/expr/node_manager.h, src/expr/node_builder.h,
src/prop/prop_engine.h, src/prop/prop_engine.cpp,
src/theory/theory_engine.h, src/smt/smt_engine.h, src/smt/smt_engine.cpp,
src/theory/output_channel.h: turn "const Node&"-typed formal
parameters into "TNode"
* src/theory/bool, src/theory/booleans: "bool" directory renamed "booleans"
to avoid keyword clash on containing namespace
* src/theory/booleans/theory_def.h, src/theory/uf/theory_def.h,
src/theory/arith/theory_def.h: "define" a theory simply (for automatic
theoryOf() generator).
* src/Makefile.am: build theory subdirectory before prop, smt, etc. so that
src/theory/theoryof_table.h header gets generated before it's needed
* src/expr/node_prologue.h, src/expr/node_middle.h: move "Kind" into a
separate CVC4::kind namespace to avoid its contents from cluttering
the CVC4 root namespace. Import the symbol "Kind" into the CVC4 namespace
but not the enum values.
* src/expr/node_manager.h, src/expr/node.h, src/expr/node_value.h,
src/expr/node_value.cpp, src/expr/expr.cpp, src/theory/uf/theory_uf.cpp,
src/prop/cnf_stream.cpp, src/parser/smt/smt_parser.g,
src/parser/cvc/cvc_parser.g, src/parser/antlr_parser.cpp,
test/unit/expr/node_white.h, test/unit/expr/node_black.h,
test/unit/expr/kind_black.h, test/unit/expr/node_builder_black.h:
update for having moved Kind into CVC4::kind.
* src/parser/parser.cpp: added file-does-not-exist check (was failing
silently).
|
|
|
|
problems for Moragn. Also cleaned up theory uf and ecdata, and updated both to reflect attribute. Should be close now.
|
|
(leftovers from before switching to Node)
|
|
* 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)
|
|
* Add virtual destructors to CnfStream, Theory, OutputChannel, and
ExplainOutputChannel. Safer and stops a compiler warning.
* node attributes: fix compiler warnings on 64-bit.
* Node: add asserts to make sure the current NodeManager is non-NULL
when it's needed. This can happen when public-facing functions
don't properly set the node manager, and it can look like a bug in
another part of the library. Also some code format cleanup.
* configure.ac, config/cvc4.m4: added --enable-static-binary (see
discussion on bug 33), fixed bad configure lines (bug 19), added
documentation for some things.
* config.h.in: removed; it's auto-generated.
|
|
correct, etc..
|
|
ExplainOutputChannel. Safer and stops a compiler warning.
* node attributes: fix compiler warnings on 64-bit.
* Node: add asserts to make sure the current NodeManager is non-NULL
when it's needed. This can happen when public-facing functions
don't properly set the node manager, and it can look like a bug in
another part of the library. Also some code format cleanup.
* configure.ac, config/cvc4.m4: added --enable-static-binary (see
discussion on bug 32), fixed bad configure lines (bug 19), added
documentation for some things.
* config.h.in: removed; it's auto-generated.
|
|
of functionality is stubbed out. Still needs a bit of cleanup.
|
|
|
|
conversation with Tim
|
|
cvc4-c++-editing-mode from contrib/editing-with-emacs
|
|
regenerated configure script
|
|
Updated contrib/update-copyright to handle Antlr (.g) parser/lexer inputs.
Updated copyright year.
Added a new "bool" theory (right now just to hold a kind.h contribution).
Added "kinds" files to UF and the new "bool" theory.
|
|
various cleanups; renamed numChildren() to getNumChildren() and added it to NodeBuilder interface; fancier, non-exponential CNF conversion with variable introduction is still buggy (?)
|
|
|
