Age | Commit message (Collapse) | Author | |
---|---|---|---|
2010-02-12 | build fix | Dejan Jovanović | |
2010-02-12 | Fix to compile out Debug(...) << ... statements in optimized mode. Someone ↵ | Dejan Jovanović | |
please look to see if it makes sense. | |||
2010-02-12 | Changes to hashing that solve the xinetd boolean benchmark in 14s (from ↵ | Dejan Jovanović | |
~25min). Switched to standard hash_set, hash_map, new hash for the vector of node values (from boost), changed the hash for nodes to be over id's, all the hash values are now size_t. The parser is down from 11s to 10s on the benchmark, so most of the solve time is parsing and we need to figure this out. | |||
2010-02-11 | svn ignore | Dejan Jovanović | |
2010-02-11 | Adding precedence regressions | Christopher L. Conway | |
2010-02-10 | note on setup(); for discussion at 2010.02.11 meeting | Morgan Deters | |
2010-02-10 | svn:ignore for build stuff; add Liana to AUTHORS | Morgan Deters | |
2010-02-10 | fixing annoying eclipse build settings, no more broken pipe errors with ↵ | Dejan Jovanović | |
these settings | |||
2010-02-10 | Added calls to destructor in CDList plus optional flag to disable. | Clark Barrett | |
2010-02-09 | Changes to the CNF conversion and the SAT solver. All regression pass now, ↵ | Dejan Jovanović | |
and we're ready for nightly testing. We should not add regression tests that test future behaviour, as the builds will nag for all failing regressions. Thus, I've separated the multi-query regressions into multiple regressions until the cnf/context/sat is able to handle it. Also, fixed a typo in the CVC parser. | |||
2010-02-09 | removing other pieces of autotools stuff to fix bug #24 | Morgan Deters | |
2010-02-09 | moving built-in kinds out of the kind.h prologue/middle for uniformity; ↵ | Morgan Deters | |
added TUPLE built-in | |||
2010-02-09 | empty stubs for push and pop to fix the build fail | Dejan Jovanović | |
2010-02-08 | Disabling the failing test case for the context. | Dejan Jovanović | |
2010-02-08 | Fixing the test case, it had a unary or. The cnf converter should be adapted ↵ | Dejan Jovanović | |
to handle cases like this. | |||
2010-02-08 | Push/Pop parsing and commands | Dejan Jovanović | |
2010-02-08 | Moving the template stuff back into the header in order to use CDList. | Dejan Jovanović | |
2010-02-07 | Documenting type.h/cpp | Christopher L. Conway | |
Making Boolean and Kind types singletons | |||
2010-02-06 | force sorting of AC_CONFIG_FILES, otherwise different computers generate the ↵ | Morgan Deters | |
configure script differently and we get useless commits of it; fix NodeBuilder memory leak in response to Kaustubh's expr code review (bug#15) | |||
2010-02-06 | Preliminary support for types in parser | Christopher L. Conway | |
2010-02-05 | final fixes to addsourcedir source-directory-Makefile-generation script | Morgan Deters | |
2010-02-05 | auto-generated list of AC_CONFIG_FILES so that you needn't add each ↵ | Morgan Deters | |
recursive Makefile to configure.ac | |||
2010-02-05 | automatic generator script for sourcedir Makefiles and Makefile.ams | Morgan Deters | |
2010-02-05 | remove the last vestiges of support for "make build-profile" without first ↵ | Morgan Deters | |
configuring the build-profile, simplifying the build process and closing bug 21 | |||
2010-02-04 | minor interface changes to TheoryEngine/Theory after meeting and ↵ | Morgan Deters | |
conversation with Tim | |||
2010-02-04 | fix run_regression script | Morgan Deters | |
2010-02-04 | beautification of the prop engine | Dejan Jovanović | |
2010-02-04 | assign expected-status to regressions | Morgan Deters | |
2010-02-04 | build system for multi-level regressions | Morgan Deters | |
2010-02-04 | remove warnings from use of __gnu_cxx::hash_map<>; also spacing fixes in ↵ | Morgan Deters | |
symbol table | |||
2010-02-04 | remove -*- c++ -*- emacs tag from source files (it overrides ↵ | Morgan Deters | |
cvc4-c++-editing-mode from contrib/editing-with-emacs | |||
2010-02-04 | Changed mapping from atoms to literals in the prop engine to be atoms to vars. | Tim King | |
2010-02-04 | Moved regressions into various levels based on running time. | Tim King | |
2010-02-04 | test infrastructure updated for multiple-level regressions | Morgan Deters | |
2010-02-04 | minor cleanup; give the main driver a different exit code for ↵ | Morgan Deters | |
SAT-INVALID/UNSAT-VALID | |||
2010-02-04 | src/expr/kind.h is now automatically generated. | Morgan Deters | |
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. | |||
2010-02-04 | minor fix for update-copyright.pl; ran update-copyright.pl on all sources; ↵ | Morgan Deters | |
regenerated configure script | |||
2010-02-04 | added bool and arith theory makefiles to AC_CONFIG_FILES in configure.ac | Morgan Deters | |
2010-02-04 | Added theory output channel interfaces and "Interrupted" exception. | Morgan Deters | |
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. | |||
2010-02-04 | Fixes to the cnf converter. Also a barebones utility for printing out a ↵ | Tim King | |
satisifying model. | |||
2010-02-03 | Adding extra test to parser | Christopher L. Conway | |
2010-02-03 | adding an option to minisat to not do any debug checks/output | Dejan Jovanović | |
2010-02-03 | Fixing bad commit | Christopher L. Conway | |
2010-02-03 | Adding functions/predicates to SMT grammar | Christopher L. Conway | |
2010-02-03 | Addressed many of the concerns of bug 10 (build system code review). | Morgan Deters | |
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. | |||
2010-02-03 | ELSEIF support and parser debugging with '-d parser' | Dejan Jovanović | |
2010-02-03 | simple ITE parsing | Dejan Jovanović | |
2010-02-03 | By popular demand, I also added a printAst to Expr. | Tim King | |
2010-02-03 | I hacked in a temporary way to restart minisat for multiple queries. | Tim King | |
2010-02-03 | Within node I added printAst(..) for general purpose debugging use ↵ | Tim King | |
throughout the code. I also added debugPrint() to Node for use within gdb. |