summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2010-02-02Adding support for escapes in string literals (strings like "\n\t\"")Dejan Jovanović
2010-02-02Fixed compile errorsClark Barrett
2010-02-02Updates to context:Clark Barrett
2010-02-01Fixing the CVC grammar for parsing Boolean expressions. All the associativity...Dejan Jovanović
2010-02-01fix node manager code (bugzilla #15, comment #2) in case where there's a hash...Morgan Deters
2010-02-01Added this test back to avoid make check problems.Tim King
2010-01-30cnf conversion (variable-introducing), cleanups, fixes to minisat calling for...Morgan Deters
2010-01-30Checking in small test fixes for node_blackTim King
2010-01-29fixing the last context build problem, it compiles nowDejan Jovanović
2010-01-29one more bugClark Barrett
2010-01-29Fixed compile errorsClark Barrett
2010-01-29Adding Makefile.in to svn:ignoreChristopher L. Conway
2010-01-29Adding Makefile.in to svn:ignoreChristopher L. Conway
2010-01-29Fixing boolean operator precedencesChristopher L. Conway
2010-01-29Update of context moduleClark Barrett
2010-01-29fixed CNF conversion, and more modular; CNF conversion command line option; v...Morgan Deters
2010-01-28Removing Makefile.in'sChristopher L. Conway
2010-01-28Replacing hand-coded autogen.sh with buildconf versionChristopher L. Conway
2010-01-27support "make check" in src/ subdirs for unit-testing of just that module; al...Morgan Deters
2010-01-27test framework fixes; bug 13 closedMorgan Deters
2010-01-27Added additional tests to node_black.h. CVC4 currently passes all but 1 test.Tim King
2010-01-26Undoing stupid commit mistake. Rolling back to -r 102 for test/unit/expr/nod...Tim King
2010-01-26Added test/regress/boolean.cvcTim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback