cvc5.git
2010-03-04 Dejan JovanovićAdding phase-caching to minisat.
2010-03-03 Dejan JovanovićSome SAT stuff, not doing anything special yet, just...
2010-03-02 Morgan Deters* NodeBuilder work: specifically, convenience builders...
2010-03-01 Tim KingAdded theory black box test.
2010-03-01 Tim KingNode builder tests that targetted properly detecting...
2010-03-01 Tim KingAdded some documentation to theory_uf.
2010-02-28 Dejan Jovanović* context.h - Changed cdlist::push_back to use a new...
2010-02-28 Tim KingTheoryUFWhite is passing. I fixed 2 errors. Unfortunat...
2010-02-27 Morgan Detersfix compile error in black parser unit test after today...
2010-02-27 Morgan DetersA bag of unrelated fixes to bring trunk more in-line...
2010-02-27 Christopher... Adding --mmap option to use memory-mapped file input...
2010-02-26 Morgan Deters* test/unit/context/context_black.h: Test CDList<>...
2010-02-26 Tim KingTheoryUFWhite tests are added. There are also accompany...
2010-02-26 Tim KingFixed a bug in CDList reallocation. (Also corrected...
2010-02-26 Dejan JovanovićChanging the hashing in attributes to what Nodes do...
2010-02-25 Christopher... Adding Node::getOperator()
2010-02-25 Tim KingUpdated uf to reflect APPLY structure after conversatio...
2010-02-25 Morgan Deters* src/expr/node_builder.h: fixed some overly-aggressive...
2010-02-25 Morgan Deters* src/expr/node.h: add a copy constructor. Apparently...
2010-02-25 Tim KingCreated basic node builder and kind tests. Also fixed...
2010-02-24 Tim KingCleaned up and documented ecdata and theory_uf.
2010-02-24 Tim KingCommitting small changes to attribute, and theory to...
2010-02-23 Christopher... Minor optimizations to parser (use const string& for...
2010-02-23 Dejan Jovanovićcosmetic changes, comments, and renaming of Expr relate...
2010-02-22 Dejan Jovanovićfinally works
2010-02-22 Dejan JovanovićMerging from branch branches/Liana r241
2010-02-22 Christopher... Switching to types-as-attributes in parser
2010-02-22 Morgan Deters* src/expr/attribute.h: fixed an issue with "const...
2010-02-22 Morgan Deters* configure.ac: Remove doc/ from search path for Makefi...
2010-02-22 Morgan DetersRe-committing revision 232 properly:
2010-02-22 Morgan Detersundoing improperly-committed revision 232; will re...
2010-02-22 Cesare Tinelli* Add virtual destructors to CnfStream, Theory, OutputC...
2010-02-22 Dejan JovanovićSmall changes to the smt-engine, removed the assertions...
2010-02-22 Morgan Detersresolve bug 32; public-facing interface functions in...
2010-02-22 Morgan Detersfix bug 33 (statically link the "cvc4" binary); also...
2010-02-22 Morgan Detersfix bug 22 (remove tracing from non-trace builds; remov...
2010-02-19 Morgan Detersspecialized implementation for boolean node attributes...
2010-02-19 Morgan Deters* Attribute infrastructure -- static design. Documenta...
2010-02-19 Christopher... Changing minArity of AND/OR to 1 in SMT parser
2010-02-18 Christopher... Adding --no-checking option to disable semantic checks...
2010-02-18 Christopher... Rm'ing doc from SUBDIRS
2010-02-18 Christopher... Adding doxygen configuration parameters and doxygen...
2010-02-17 Tim KingInitial draft of TheoryUF. Should compile without probl...
2010-02-17 Morgan Detersfix bug 27: --with-cxxtest-dir=(relative-path) now...
2010-02-16 Christopher... Moving parser error checking into AntlrParser
2010-02-16 Christopher... Adding --parse-only option
2010-02-16 Dejan Jovanovićremoving assertion and warning that shouldn't be there...
2010-02-16 Christopher... Removing spurious commit of configure
2010-02-16 Christopher... Converting semantic predicates in parser to AlwaysAsser...
2010-02-13 Dejan Jovanovićsimplification minisat
2010-02-13 Dejan JovanovićImprovements to CNF conversion when already in CNF
2010-02-12 Dejan Jovanovićbuild fix
2010-02-12 Dejan JovanovićFix to compile out Debug(...) << ... statements in...
2010-02-12 Dejan JovanovićChanges to hashing that solve the xinetd boolean benchm...
2010-02-11 Dejan Jovanovićsvn ignore
2010-02-11 Christopher... Adding precedence regressions
2010-02-10 Morgan Detersnote on setup(); for discussion at 2010.02.11 meeting
2010-02-10 Morgan Deterssvn:ignore for build stuff; add Liana to AUTHORS
2010-02-10 Dejan Jovanovićfixing annoying eclipse build settings, no more broken...
2010-02-10 Clark BarrettAdded calls to destructor in CDList plus optional flag...
2010-02-09 Dejan JovanovićChanges to the CNF conversion and the SAT solver. All...
2010-02-09 Morgan Detersremoving other pieces of autotools stuff to fix bug #24
2010-02-09 Morgan Detersmoving built-in kinds out of the kind.h prologue/middle...
2010-02-09 Dejan Jovanovićempty stubs for push and pop to fix the build fail
2010-02-08 Dejan JovanovićDisabling the failing test case for the context.
2010-02-08 Dejan JovanovićFixing the test case, it had a unary or. The cnf conver...
2010-02-08 Dejan JovanovićPush/Pop parsing and commands
2010-02-08 Dejan JovanovićMoving the template stuff back into the header in order...
2010-02-07 Christopher... Documenting type.h/cpp
2010-02-06 Morgan Detersforce sorting of AC_CONFIG_FILES, otherwise different...
2010-02-06 Christopher... Preliminary support for types in parser
2010-02-05 Morgan Detersfinal fixes to addsourcedir source-directory-Makefile...
2010-02-05 Morgan Detersauto-generated list of AC_CONFIG_FILES so that you...
2010-02-05 Morgan Detersautomatic generator script for sourcedir Makefiles...
2010-02-05 Morgan Detersremove the last vestiges of support for "make build...
2010-02-04 Morgan Detersminor interface changes to TheoryEngine/Theory after...
2010-02-04 Morgan Detersfix run_regression script
2010-02-04 Dejan Jovanovićbeautification of the prop engine
2010-02-04 Morgan Detersassign expected-status to regressions
2010-02-04 Morgan Detersbuild system for multi-level regressions
2010-02-04 Morgan Detersremove warnings from use of __gnu_cxx::hash_map<>;...
2010-02-04 Morgan Detersremove -*- c++ -*- emacs tag from source files (it...
2010-02-04 Tim KingChanged mapping from atoms to literals in the prop...
2010-02-04 Tim KingMoved regressions into various levels based on running...
2010-02-04 Morgan Deterstest infrastructure updated for multiple-level regressions
2010-02-04 Morgan Detersminor cleanup; give the main driver a different exit...
2010-02-04 Morgan Deterssrc/expr/kind.h is now automatically generated.
2010-02-04 Morgan Detersminor fix for update-copyright.pl; ran update-copyright...
2010-02-04 Morgan Detersadded bool and arith theory makefiles to AC_CONFIG_FILE...
2010-02-04 Morgan DetersAdded theory output channel interfaces and "Interrupted...
2010-02-04 Tim KingFixes to the cnf converter. Also a barebones utility...
2010-02-03 Christopher... Adding extra test to parser
2010-02-03 Dejan Jovanovićadding an option to minisat to not do any debug checks...
2010-02-03 Christopher... Fixing bad commit
2010-02-03 Christopher... Adding functions/predicates to SMT grammar
2010-02-03 Morgan DetersAddressed many of the concerns of bug 10 (build system...
2010-02-03 Dejan JovanovićELSEIF support and parser debugging with '-d parser'
2010-02-03 Dejan Jovanovićsimple ITE parsing
2010-02-03 Tim KingBy popular demand, I also added a printAst to Expr.
2010-02-03 Tim KingI hacked in a temporary way to restart minisat for...
next