| Age | Commit message (Collapse) | Author |
|---|
|
with that of Node.
* If NodeBuilder<> hasn't yet been assigned a Kind, several member functions
related to children now throw an IllegalArgumentException:
* getNumChildren()
* begin()
* end()
* operator[]
* getChild()
This is because if you later assign the NodeBuilder<> a PARAMETERIZED kind,
the children are "reinterpreted" -- the first being an operator. Interface-wise,
it doesn't make sense to return one thing for nb[0], then later, after setting
the kind, to return another thing for nb[0].
* Fixed unit tests depending on this behavior.
* Added a warning to the testing summary if unit tests didn't run (because this
is likely due to compilation problems, and without a warning it looks kind of
like a test success)
* VERBOSE wasn't exported to the environment for unit test "make check." Fixed.
|
|
g++ 4.3 and 4.4 issue
|
|
|
|
before being used. Fixed a bug in node_builder.h's crop where a pointer is dereferenced after a realloc call.
|
|
Adding general support for associative operators in SMT v1 and v2
|
|
|
|
to its final destination. Added a basic rewriter to TheoryUF. (x=x rewrites to true.) Added DIVISION to src/expr/node_manager.cpp's getType. Fixed the theory returned for variables in theoryOf() for bool and arith. Fixed TheoryEngine rewrite children to properly handle APPLY_UFs. Removed the special case for equality in TheoryEngine rewrite. A few tests are currently broken due to deallocation errors. Morgan and I will try to commit a fix to this in a little bit.
|
|
|
|
potential design for later. Resolves bug 113, invalidates bugs 93 and 94.
|
|
|
|
|
|
Real. See Bug 127 for a discussion of the hack. I am also adding a regression test that does not work (bug 128). It is not enabled so make check should still be fine.
|
|
fixes and organizational changes. The theory is now enabled to perform checking in the TheoryEngine. This draft can now solve 2 new regression tests test/regress/regress0/ineq_slack.smt and test/regress/regress0/ineq_basic.smt. There is also a small bug fix inside src/expr/attribute.h.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
generation).
|
|
|
|
instead of the kind, i.e.
Expr op = ..."f"...
em.mkExpr(op, children);
Operator kinds are automatically associated with the enclosing expression kind in the DSL and generated.
|
|
|
|
|
|
|
|
the Node level.
|
|
|
|
|
|
* Types are now represented as nodes in the attribute table and are managed, i.e. you can say
Type booleanType = d_nodeManager->booleanType();
Type t = d_nodeManager->mkFunctionType(booleanType, booleanType);
FunctionType ft = (FunctionType)t;
Assert(ft.getArgTypes()[0], booleanType);
* The attributes now have a table for Nodes and a table for TNodes (both should be used with caution)
* Changes the way nodes are extracted from NodeBuilder, added several methods to
extract a Node, NodeValue, or Node*, with corresponding methods for extraction
* Used the above in the construction of Expr and Type objects
* The NodeManager now destroys the attributes in the destructor by pausing the
garbage collection
* To achive destruction a flag d_inDesctruction has been added to loosen the assertion
in NodeValue::dec() (there might be -refcount TNodes leftover)
* Beginnings of the Bitvector constants using GMP
Not yet in tiptop phase, needs more documentation, and Types should be pulled out to TypeNodes eventually. Also, the types are currently defined in the builting_kinds, and I need to add these to the theory specific definitions with special 'type' constructs.
I hate branching and merging.
|
|
auto-generated headers (metakind.h etc.), so they don't have to be
recompiled every time. This drastically improves build time when
only small updates are made.
* Added "memory.h" unit test header for checking out-of-memory
conditions. cdlist_black uses it.
* Added helpful output when you "make lcov" in a non-coverage-enabled
build.
* Removed strict aliasing warning when compiling metakind.h header
with optimization on.
* Removed const version of NodeBuilder::operator Node()---it was
poorly performing, better to not permit it---and fixed the
convenience builders to use the non-const version
(re: code review #63)
* Color-coded test output on capable terminals.
* Fixed some warnings in unit tests.
|
|
|
|
|
|
coverage for util and context classes; implemented some output functionality that was missing; reclassified some tests white -> black or black -> public; other minor fixes
|
|
+ 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).
|
|
|
|
|
|
|
|
NodeManager (bug #65). Better documentation, etc.
* As part of this, removed NodeManager::mkVar() (which created a
variable of unknown type). This requires changes to lots of unit
tests, which were using this function.
* Performed some review of parser code (my code review #73).
+ I changed the way exceptions were caught and rethrown in
src/parser/input.cpp.
+ ParserExceptions weren't being properly constructed (d_line and
d_column weren't intiialized and could contain junk, leading to
weird error messages). Fixed.
* Fix to the current working directory used by run_regression script.
Makes exceptional output easier to match against (in expected error
output).
* (configure.ac) Ensure that CFLAGS has -fexceptions in it, in case we
compile any C code and don't use the C++ compiler.
|
|
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.
|
|
|
