summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2010-03-30Merging from branches/antlr3 (r246:354)Christopher L. Conway
2010-03-30again, re-enabling integer/rational tests (though they still fail to compile ↵Morgan Deters
on 32-bit)
2010-03-30I think this finishes off the CDMap<>/Attribute leaksMorgan Deters
2010-03-30fixing mistaken commit to unit test Makefile.am which removed testsMorgan Deters
2010-03-30Highlights of this commit are:Morgan Deters
* 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
2010-03-28Improved the documentation and testing for Rational.Tim King
2010-03-28Rm'ing test file (sorry for spam)Christopher L. Conway
2010-03-28Adding test fileChristopher L. Conway
2010-03-26Added GMP backed Rational and Integer classes, and white box tests for them. ↵Tim King
You may have to reconfigure after this update.
2010-03-25Merging let/flet rules in SMT parserChristopher L. Conway
2010-03-25Adding comments to NodeManagerChristopher L. Conway
Minor name changes for cleanup and hash function templates
2010-03-25new domain-specific language for kinds files: permits characterization of ↵Morgan Deters
different "kinds of kinds" (special, operator, parameterized, and constant), and permits doxygen comments on them
2010-03-23Documented that ContextObj::destroy() only restores back to context level 0.Clark Barrett
If there is more cleanup to do, it has to be done by the destructor.
2010-03-23Fixed some memory cleanup and destruction issues with ContextObj, ECData, ↵Tim King
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
2010-03-16* test/unit/Makefile.am, test/unit/expr/attribute_white.h,Morgan Deters
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
2010-03-15This checkin resolves bug #57.Morgan Deters
* 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)
2010-03-14* test/unit/context/context_black.h: added a test for Clark's fix to bug #45.Morgan Deters
* test/unit/context/cdlist_black.h: comment fix
2010-03-13Fix for bug 45Clark Barrett
2010-03-12* src/context/cdmap.h: rename orderedIterator to iterator, do awayMorgan Deters
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.
2010-03-12Fixing unnecessary construction of NOT nodes when generating conflict ↵Dejan Jovanović
clauses and: * adding the smallest test case (eq_diamond23.smt) that memouts in 50s * adding the initial attributes black box test
2010-03-12* Added shutdown() functions to SmtEngine, TheoryEngine, PropEngine,Morgan Deters
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.
2010-03-11naive rewriting to fix minisat invariant; rewrite x == x ==> TRUEMorgan Deters
2010-03-11Changing const TNode& to TNode in the CNF conversion + a new small benchmark ↵Dejan Jovanović
that fail on "x != x"
2010-03-11Added some hand generated UF tests. Unfortunartely all of them work. Also ↵Tim King
fixed some cleanup stuff.
2010-03-11Boolean variables were marked as theory literals by mistake. Fixed, should ↵Dejan Jovanović
give us back the SAT performance we had before the theory stuff.
2010-03-11Fix for the main bug that was bugging me -- Bug 49. The assertions queue in ↵Dejan Jovanović
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.
2010-03-10fix production-build unit testing errors (they assumed that assertions were on)Morgan Deters
2010-03-10Lexical scoping for let-bound variables (Bug #53)Christopher L. Conway
2010-03-10Adding preliminary let/flet support to SMT parser (Bug #51)Christopher L. Conway
2010-03-09Adding support for "distinct" builtin in SMT parserChristopher L. Conway
2010-03-09Adding support for sort U in QF_UF.Christopher L. Conway
2010-03-09Adding the smallest of test cases from the smtlib.Dejan Jovanović
2010-03-09removing makefile.inDejan Jovanović
2010-03-09Fixed non-debug build problemsTim King
2010-03-09one more simple test for ufDejan Jovanović
2010-03-09(no commit message)Dejan Jovanović
2010-03-08This fixes regressions at levels >= 1 which were failingMorgan Deters
* 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
2010-03-08adding simple-uf to the regressions, and the code that apparently solves itDejan Jovanović
2010-03-08Fixing Debug("prop") => Debug("node") typoDejan Jovanović
2010-03-08Improved output for theory ufTim King
2010-03-08some more sat stuff for tim: assertions now go to theory_uf Dejan Jovanović
2010-03-08Adding quiet output of make by default. There are two additional options to ↵Dejan Jovanović
configure --enable-silent-rules less verbose build output (undo: `make V=1') --disable-silent-rules verbose build output (undo: `make V=0') If you need the verbose output, you can either reconfigure with --disable-silent-rules, or do a make V=0.
2010-03-05* public/private code untangled (smt/smt_engine.h no longer #includesMorgan Deters
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
2010-03-04Committing a bug fix from Dejan. This resolves an issue with restoring ECData.Tim King
2010-03-04Adding phase-caching to minisat. Dejan Jovanović
(A Lightweight Component Caching Scheme for Satisfiability Solvers <http://www.springerlink.com/content/y802q03263x84159/>)
2010-03-03Some SAT stuff, not doing anything special yet, just to keep it in sync.Dejan Jovanović
2010-03-02* NodeBuilder work: specifically, convenience builders. "a && b && c || d && e"Morgan Deters
(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
2010-03-01Added theory black box test.Tim King
2010-03-01Node builder tests that targetted properly detecting and handling expections ↵Tim King
have been changed to be debug mode. (The Assert(..) calls these checks rely on get compiled out of production mode.) Production and debug mode should now both pass make check on everything.
2010-03-01Added some documentation to theory_uf.Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback