| 2011-07-05 |
Dejan Jovanović | updated preprocessing and rewriting input equalities... |
blob | commitdiff | raw |
| 2011-05-23 |
Morgan Deters | fixes for "make dist" and "make doc", minor cleanups |
blob | commitdiff | raw | diff to current |
| 2011-05-23 |
Morgan Deters | Merge from arrays2 branch. |
blob | commitdiff | raw | diff to current |
| 2011-05-05 |
Morgan Deters | Merge from nonclausal-simplification-v2 branch: |
blob | commitdiff | raw | diff to current |
| 2011-05-02 |
Morgan Deters | fix a performance issue from last commit |
blob | commitdiff | raw | diff to current |
| 2011-05-02 |
Morgan Deters | Minor fixes to various parts of CVC4, including the... |
blob | commitdiff | raw | diff to current |
| 2011-04-25 |
Morgan Deters | Monday tasks: |
blob | commitdiff | raw | diff to current |
| 2011-04-22 |
Morgan Deters | fix to last commit |
blob | commitdiff | raw | diff to current |
| 2011-04-22 |
Morgan Deters | Fixing SmtEngine::getValue() by adding a NodeManagerSco... |
blob | commitdiff | raw | diff to current |
| 2011-04-20 |
Morgan Deters | Minor mixed-bag commit. Expected performance impact... |
blob | commitdiff | raw | diff to current |
| 2011-04-18 |
Morgan Deters | Partial merge from datatypes-merge branch: |
blob | commitdiff | raw | diff to current |
| 2011-04-13 |
Morgan Deters | cache the LET rewriting (and defined-function expansion... |
blob | commitdiff | raw | diff to current |
| 2011-04-04 |
Tim King | Merging the satliteral-before-prereg branch into trunk... |
blob | commitdiff | raw | diff to current |
| 2011-04-01 |
Morgan Deters | This commit is a merge from the "betterstats" branch... |
blob | commitdiff | raw | diff to current |
| 2011-03-15 |
Morgan Deters | Merge from cudd branch. This mostly just adds support... |
blob | commitdiff | raw | diff to current |
| 2011-01-05 |
Dejan Jovanović | Commit for the theory engine and rewriter changes.... |
blob | commitdiff | raw | diff to current |
| 2010-11-19 |
Morgan Deters | Merge from ufprop branch, including: |
blob | commitdiff | raw | diff to current |
| 2010-11-16 |
Morgan Deters | SmtEngine now fails with a ModalException if --incremen... |
blob | commitdiff | raw | diff to current |
| 2010-11-09 |
Dejan Jovanović | Lemmas on demand work, push-pop, some cleanup. |
blob | commitdiff | raw | diff to current |
| 2010-11-08 |
Morgan Deters | command-line flag to disable theory registration, also... |
blob | commitdiff | raw | diff to current |
| 2010-11-08 |
Morgan Deters | cleanup, documentation, SMT-LIBv2 compliance |
blob | commitdiff | raw | diff to current |
| 2010-10-31 |
Morgan Deters | enable dependence graphs in doxygen; fix lots of doxyge... |
blob | commitdiff | raw | diff to current |
| 2010-10-22 |
Christopher L. Conway | Merging main/getopt.cpp, main/usage.h, and smt/options... |
blob | commitdiff | raw | diff to current |
| 2010-10-22 |
Morgan Deters | comment out the "interactive" check in SmtEngine::getVa... |
blob | commitdiff | raw | diff to current |
| 2010-10-21 |
Christopher L. Conway | * Option --no-type-checking now disables type checks... |
blob | commitdiff | raw | diff to current |
| 2010-10-12 |
Morgan Deters | hooked up "we are incomplete" flag after conversation... |
blob | commitdiff | raw | diff to current |
| 2010-10-12 |
Morgan Deters | Merge from cc-memout branch. Here are the main points |
blob | commitdiff | raw | diff to current |
| 2010-10-12 |
Morgan Deters | check last result in (get-assignment); some context... |
blob | commitdiff | raw | diff to current |
| 2010-10-10 |
Morgan Deters | additional model gen and SMT-LIBv2 compliance work... |
blob | commitdiff | raw | diff to current |
| 2010-10-09 |
Morgan Deters | support for SMT-LIBv2 :named attributes, and attributes... |
blob | commitdiff | raw | diff to current |
| 2010-10-09 |
Morgan Deters | bug fixes to model gen |
blob | commitdiff | raw | diff to current |
| 2010-10-09 |
Morgan Deters | Model generation for arith, boolean, and uf theories via |
blob | commitdiff | raw | diff to current |
| 2010-10-08 |
Morgan Deters | * (define-fun...) now has proper type checking in non... |
blob | commitdiff | raw | diff to current |
| 2010-10-08 |
Morgan Deters | support (set-info) on status, source, category, difficu... |
blob | commitdiff | raw | diff to current |
| 2010-10-07 |
Morgan Deters | type checking for define-fun in production builds;... |
blob | commitdiff | raw | diff to current |
| 2010-10-07 |
Morgan Deters | SMT-LIBv2 (define-fun...) command now functional; does... |
blob | commitdiff | raw | diff to current |
| 2010-10-06 |
Morgan Deters | declare-sort, define-sort working but not thoroughly... |
blob | commitdiff | raw | diff to current |
| 2010-10-05 |
Morgan Deters | parser and core support for SMT-LIBv2 commands get... |
blob | commitdiff | raw | diff to current |
| 2010-09-24 |
Dejan Jovanović | equality triggers for the equality engine |
blob | commitdiff | raw | diff to current |
| 2010-08-17 |
Morgan Deters | Merge from "cc" branch: |
blob | commitdiff | raw | diff to current |
| 2010-06-04 |
Morgan Deters | ** Don't fear the files-changed list, almost all change... |
blob | commitdiff | raw | diff to current |
| 2010-05-25 |
Dejan Jovanović | Some initial changes to allow for lemmas on demand. |
blob | commitdiff | raw | diff to current |
| 2010-03-16 |
Morgan Deters | * test/unit/Makefile.am, test/unit/expr/attribute_white.h, |
blob | commitdiff | raw | diff to current |
| 2010-03-12 |
Morgan Deters | * Added shutdown() functions to SmtEngine, TheoryEngine... |
blob | commitdiff | raw | diff to current |
| 2010-03-11 |
Morgan Deters | naive rewriting to fix minisat invariant; rewrite ... |
blob | commitdiff | raw | diff to current |
| 2010-03-08 |
Morgan Deters | This fixes regressions at levels >= 1 which were failing |
blob | commitdiff | raw | diff to current |
| 2010-03-05 |
Morgan Deters | * public/private code untangled (smt/smt_engine.h no... |
blob | commitdiff | raw | diff to current |
| 2010-03-03 |
Dejan Jovanović | Some SAT stuff, not doing anything special yet, just... |
blob | commitdiff | raw | diff to current |
| 2010-02-25 |
Morgan Deters | * src/expr/node.h: add a copy constructor. Apparently... |
blob | commitdiff | raw | diff to current |
| 2010-02-23 |
Dejan Jovanović | cosmetic changes, comments, and renaming of Expr relate... |
blob | commitdiff | raw | diff to current |
| 2010-02-22 |
Morgan Deters | * configure.ac: Remove doc/ from search path for Makefi... |
blob | commitdiff | raw | diff to current |
| 2010-02-22 |
Dejan Jovanović | Small changes to the smt-engine, removed the assertions... |
blob | commitdiff | raw | diff to current |
| 2010-02-19 |
Morgan Deters | * Attribute infrastructure -- static design. Documenta... |
blob | commitdiff | raw | diff to current |
| 2010-02-09 |
Dejan Jovanović | Changes to the CNF conversion and the SAT solver. All... |
blob | commitdiff | raw | diff to current |
| 2010-02-09 |
Dejan Jovanović | empty stubs for push and pop to fix the build fail |
blob | commitdiff | raw | diff to current |
| 2010-02-04 |
Morgan Deters | minor interface changes to TheoryEngine/Theory after... |
blob | commitdiff | raw | diff to current |
| 2010-02-04 |
Dejan Jovanović | beautification of the prop engine |
blob | commitdiff | raw | diff to current |
| 2010-02-04 |
Morgan Deters | remove -*- c++ -*- emacs tag from source files (it... |
blob | commitdiff | raw | diff to current |
| 2010-02-04 |
Morgan Deters | src/expr/kind.h is now automatically generated. |
blob | commitdiff | raw | diff to current |
| 2010-02-04 |
Morgan Deters | minor fix for update-copyright.pl; ran update-copyright... |
blob | commitdiff | raw | diff to current |
| 2010-02-03 |
Morgan Deters | Addressed many of the concerns of bug 10 (build system... |
blob | commitdiff | raw | diff to current |
| 2010-02-02 |
Tim King | Switched cnf conversion to go through CnfStream. |
blob | commitdiff | raw | diff to current |
| 2010-01-29 |
Morgan Deters | fixed CNF conversion, and more modular; CNF conversion... |
blob | commitdiff | raw | diff to current |
| 2010-01-26 |
Morgan Deters | cnf conversion |
blob | commitdiff | raw | diff to current |
| 2010-01-26 |
Morgan Deters | fixes to build structure, util classes, lots of fixes... |
blob | commitdiff | raw | diff to current |
| 2009-12-17 |
Morgan Deters | update-copyright.pl now retrieves and incorporates... |
blob | commitdiff | raw | diff to current |
| 2009-12-17 |
Morgan Deters | coding standard fix on SmtEngine; fix recursive make |
blob | commitdiff | raw | diff to current |
| 2009-12-17 |
Morgan Deters | + test infrastructure fixes |
blob | commitdiff | raw | diff to current |
| 2009-12-11 |
Dejan Jovanović | Extracted the public Expr and ExprManager interface... |
blob | commitdiff | raw | diff to current |
| 2009-12-10 |
Dejan Jovanović | killing expr into node... |
blob | commitdiff | raw | diff to current |
| 2009-12-09 |
Dejan Jovanović | A mess of changes in the expression manager, simple... |
blob | commitdiff | raw | diff to current |
| 2009-12-08 |
Morgan Deters | work on propositional layer, expression builder support... |
blob | commitdiff | raw | diff to current |
| 2009-12-03 |
Morgan Deters | parsing/expr/command/result/various other fixes |
blob | commitdiff | raw | diff to current |
| 2009-11-25 |
Morgan Deters | additional work on parser hookup, configuration + build |
blob | commitdiff | raw | diff to current |
| 2009-11-24 |
Morgan Deters | oops, missed a file |
blob | commitdiff | raw | diff to current |
|
projects / cvc5.git / history