summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2010-02-22fix bug 33 (statically link the "cvc4" binary); also main driver cleanupMorgan Deters
2010-02-22fix bug 22 (remove tracing from non-trace builds; remove all outputMorgan Deters
2010-02-19specialized implementation for boolean node attributes ("flags"): they now sh...Morgan Deters
2010-02-19* Attribute infrastructure -- static design. Documentation is coming.Morgan Deters
2010-02-19Changing minArity of AND/OR to 1 in SMT parserChristopher L. Conway
2010-02-18Adding --no-checking option to disable semantic checks in parserChristopher L. Conway
2010-02-17Initial draft of TheoryUF. Should compile without problems. A decent amount o...Tim King
2010-02-16Moving parser error checking into AntlrParserChristopher L. Conway
2010-02-16Adding --parse-only optionChristopher L. Conway
2010-02-16removing assertion and warning that shouldn't be there. adding initialization...Dejan Jovanović
2010-02-16Converting semantic predicates in parser to AlwaysAssertionsChristopher L. Conway
2010-02-13simplification minisat Dejan Jovanović
2010-02-13Improvements to CNF conversion when already in CNFDejan Jovanović
2010-02-12build fixDejan Jovanović
2010-02-12Fix to compile out Debug(...) << ... statements in optimized mode. Someone pl...Dejan Jovanović
2010-02-12Changes to hashing that solve the xinetd boolean benchmark in 14s (from ~25mi...Dejan Jovanović
2010-02-10note on setup(); for discussion at 2010.02.11 meetingMorgan Deters
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, an...Dejan Jovanović
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-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-04minor interface changes to TheoryEngine/Theory after meeting and conversation...Morgan Deters
2010-02-04beautification of the prop engineDejan Jovanović
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-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 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 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-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ć
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback