summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2010-02-12build fixDejan Jovanović
2010-02-12Fix to compile out Debug(...) << ... statements in optimized mode. Someone ↵Dejan Jovanović
please look to see if it makes sense.
2010-02-12Changes 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-11svn ignoreDejan Jovanović
2010-02-11Adding precedence regressionsChristopher L. Conway
2010-02-10note on setup(); for discussion at 2010.02.11 meetingMorgan Deters
2010-02-10svn:ignore for build stuff; add Liana to AUTHORSMorgan Deters
2010-02-10fixing annoying eclipse build settings, no more broken pipe errors with ↵Dejan Jovanović
these settings
2010-02-10Added calls to destructor in CDList plus optional flag to disable.Clark Barrett
2010-02-09Changes 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-09removing other pieces of autotools stuff to fix bug #24Morgan Deters
2010-02-09moving built-in kinds out of the kind.h prologue/middle for uniformity; ↵Morgan Deters
added TUPLE built-in
2010-02-09empty stubs for push and pop to fix the build failDejan Jovanović
2010-02-08Disabling the failing test case for the context.Dejan Jovanović
2010-02-08Fixing the test case, it had a unary or. The cnf converter should be adapted ↵Dejan Jovanović
to handle cases like this.
2010-02-08Push/Pop parsing and commandsDejan Jovanović
2010-02-08Moving the template stuff back into the header in order to use CDList.Dejan Jovanović
2010-02-07Documenting type.h/cppChristopher L. Conway
Making Boolean and Kind types singletons
2010-02-06force 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-06Preliminary support for types in parserChristopher L. Conway
2010-02-05final fixes to addsourcedir source-directory-Makefile-generation scriptMorgan Deters
2010-02-05auto-generated list of AC_CONFIG_FILES so that you needn't add each ↵Morgan Deters
recursive Makefile to configure.ac
2010-02-05automatic generator script for sourcedir Makefiles and Makefile.amsMorgan Deters
2010-02-05remove 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-04minor interface changes to TheoryEngine/Theory after meeting and ↵Morgan Deters
conversation with Tim
2010-02-04fix run_regression scriptMorgan Deters
2010-02-04beautification of the prop engineDejan Jovanović
2010-02-04assign expected-status to regressionsMorgan Deters
2010-02-04build system for multi-level regressionsMorgan Deters
2010-02-04remove warnings from use of __gnu_cxx::hash_map<>; also spacing fixes in ↵Morgan Deters
symbol table
2010-02-04remove -*- c++ -*- emacs tag from source files (it overrides ↵Morgan Deters
cvc4-c++-editing-mode from contrib/editing-with-emacs
2010-02-04Changed mapping from atoms to literals in the prop engine to be atoms to vars.Tim King
2010-02-04Moved regressions into various levels based on running time.Tim King
2010-02-04test infrastructure updated for multiple-level regressionsMorgan Deters
2010-02-04minor cleanup; give the main driver a different exit code for ↵Morgan Deters
SAT-INVALID/UNSAT-VALID
2010-02-04src/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-04minor fix for update-copyright.pl; ran update-copyright.pl on all sources; ↵Morgan Deters
regenerated configure script
2010-02-04added bool and arith theory makefiles to AC_CONFIG_FILES in configure.acMorgan Deters
2010-02-04Added 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-04Fixes to the cnf converter. Also a barebones utility for printing out a ↵Tim King
satisifying model.
2010-02-03Adding extra test to parserChristopher L. Conway
2010-02-03adding an option to minisat to not do any debug checks/outputDejan Jovanović
2010-02-03Fixing bad commitChristopher L. Conway
2010-02-03Adding functions/predicates to SMT grammarChristopher L. Conway
2010-02-03Addressed 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-03ELSEIF support and parser debugging with '-d parser'Dejan Jovanović
2010-02-03simple ITE parsingDejan Jovanović
2010-02-03By popular demand, I also added a printAst to Expr.Tim King
2010-02-03I hacked in a temporary way to restart minisat for multiple queries.Tim King
2010-02-03Within node I added printAst(..) for general purpose debugging use ↵Tim King
throughout the code. I also added debugPrint() to Node for use within gdb.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback