summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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; added...Morgan Deters
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ć
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
2010-02-06force sorting of AC_CONFIG_FILES, otherwise different computers generate the ...Morgan Deters
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 recursive...Morgan Deters
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 co...Morgan Deters
2010-02-04minor interface changes to TheoryEngine/Theory after meeting and conversation...Morgan Deters
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 symb...Morgan Deters
2010-02-04remove -*- c++ -*- emacs tag from source files (it overrides cvc4-c++-editing...Morgan Deters
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 SAT-INVALID/UNS...Morgan Deters
2010-02-04src/expr/kind.h is now automatically generated.Morgan Deters
2010-02-04minor fix for update-copyright.pl; ran update-copyright.pl on all sources; re...Morgan Deters
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
2010-02-04Fixes to the cnf converter. Also a barebones utility for printing out a satis...Tim King
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
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 throughout...Tim King
2010-02-03Enabled more regress tests. Takes 26s on my machine to run a make -k check in...Tim King
2010-02-03context_mm testingDejan Jovanović
2010-02-03some more tests for the context.Dejan Jovanović
2010-02-02(no commit message)Dejan Jovanović
2010-02-02Fixed bug in context codeClark Barrett
2010-02-02for timDejan Jovanović
2010-02-02beginings of test for CDO. one failDejan Jovanović
2010-02-02Rethrow rewrite in antlr_parser. Taking LT(0) to locate the error causes the ...Dejan Jovanović
2010-02-02Switched cnf conversion to go through CnfStream.Tim King
2010-02-02Minor changes to parserChristopher L. Conway
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback