| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2010-10-22 | fix valgrind-reported errors in parser builder; a non-SMT parser was always ↵ | Morgan Deters | |
| used (rather than an Smt or Smt2) regardless of input language | |||
| 2010-10-22 | Saving state between lines in interactive mode (Fixes: #223) | Christopher L. Conway | |
| 2010-10-22 | Using Options in ParserBuilder and InteractiveShell | Christopher L. Conway | |
| 2010-10-22 | Merging main/getopt.cpp, main/usage.h, and smt/options.h in | Christopher L. Conway | |
| util/options.h,cpp | |||
| 2010-10-22 | Code cleanup for TheoryArith. | Tim King | |
| 2010-10-22 | comment out the "interactive" check in SmtEngine::getValue() for now ↵ | Morgan Deters | |
| (resolves bug 224), and fix a comment in NodeManager header | |||
| 2010-10-22 | Fixes to getValue for TheoryArith. | Tim King | |
| 2010-10-21 | * Option --no-type-checking now disables type checks in SmtEngine | Christopher L. Conway | |
| * Adding options --lazy-type-checking and --eager-type-checking to control type checking in NodeBuilder, which can now be enabled in production mode and disabled in debug mode * Option --no-checking implies --no-type-checking * Adding constructor SmtEngine(ExprManager* em) that uses default options | |||
| 2010-10-20 | Changing --no-early-type-checking to --no-type-checking | Christopher L. Conway | |
| Disabling type checking when --no-checking is given (Fixes: #221) | |||
| 2010-10-20 | Enabling semantic checks in ParserBuilder | Christopher L. Conway | |
| 2010-10-20 | Adding detection of TTY vs. piped input for interactive mode | Christopher L. Conway | |
| 2010-10-20 | Fixing minor whitespace bug in the parser | Christopher L. Conway | |
| 2010-10-20 | Adding support for interactive mode | Christopher L. Conway | |
| 2010-10-20 | fix bug #220 (assertion fails if no query/check-sat); add bug220.smt2 and ↵ | Morgan Deters | |
| bug217.smt2 as regressions; fix to build system to only run regressions (not units) if you "make -C test regress", for example (this matches behavior elsewhere) | |||
| 2010-10-14 | Fixed computation of infinitesimals for arithmetic model generation. | Tim King | |
| 2010-10-13 | Removed vector<Monomial> monos from Polynomial. Now using ↵ | Tim King | |
| expr::NodeSelfIterator. | |||
| 2010-10-13 | Added test/regress/regress1/arith and populated it with some fast SMT LIB ↵ | Tim King | |
| problems. | |||
| 2010-10-12 | with --stats, statistics are dumped for memouts and (normal) exceptions. | Morgan Deters | |
| 2010-10-12 | IDENTITY has been removed. | Tim King | |
| 2010-10-12 | minor unit test fix-ups | Morgan Deters | |
| 2010-10-12 | fix debugPrintNode(), debugPrintTNode(), debugPrintNodeValue(), ↵ | Morgan Deters | |
| debugPrintTypeNode() -- thanks Tim for pointing this out | |||
| 2010-10-12 | fix some leaks in parser, add debug code to node manager to find more | Morgan Deters | |
| 2010-10-12 | hooked up "we are incomplete" flag after conversation with Tim (a theory ↵ | Morgan Deters | |
| notifies the theory engine through its output channel); some cleanup; add a regression for bug #216 | |||
| 2010-10-12 | Merge from cc-memout branch. Here are the main points | Morgan Deters | |
| * Add ContextMemoryAllocator<T> allocator type, conforming to STL allocator requirements. * Extend the CDList<> template to take an allocator (defaults to std::allocator<T>). * Add a specialized version of the CDList<> template (in src/context/cdlist_context_memory.h) that allocates a list in segments, in context memory. * Add "forward" headers -- cdlist_forward.h, cdmap_forward.h, and cdset_forward.h. Use these in public headers, and other places where you don't need the full header (just the forward-declaration). These types justify their own header (instead of just forward-declaring yourself), because they are complex templated types, with default template parameters, specializations, etc. * theory_engine.h no longer depends on individual theory headers. (Instead it forward-declares Theory implementations.) This is especially important now that theory .cpp files depend on TheoryEngine (to implement Theory::getValue()). Previously, any modification to any theory header file required *all* theories, and the engine, to be completely rebuilt. * Support memory cleanup for nontrivial CONSTANT kinds. This resolves an issue with arithmetic where memory leaked for each distinct Rational or Integer that was wrapped in a Node. | |||
| 2010-10-12 | check last result in (get-assignment); some context cleanup | Morgan Deters | |
| 2010-10-11 | use "forward" headers | Morgan Deters | |
| 2010-10-10 | additional model gen and SMT-LIBv2 compliance work: (get-assignment) now ↵ | Morgan Deters | |
| supported; work on Result type (biggest noticeable change is that CVC4 now outputs lowercase "sat" and "unsat"), Options class moved to src/smt, to allow for future work on runtime configuration via (set-option) command | |||
| 2010-10-09 | reverting some changes to parser from last commit | Morgan Deters | |
| 2010-10-09 | support for SMT-LIBv2 :named attributes, and attributes in general; zero-ary ↵ | Morgan Deters | |
| define-fun; several set-info, set-option, get-option, get-info improvementss | |||
| 2010-10-09 | fix to unit tests | Morgan Deters | |
| 2010-10-09 | bug fixes to model gen | Morgan Deters | |
| 2010-10-09 | Model generation for arith, boolean, and uf theories via | Morgan Deters | |
| (get-value ...) SMT-LIBv2 command. As per SMT-LIBv2 spec, you must pass --interactive --produce-models on the command line (although they don't currently make us do any extra work). Closes bug #213. | |||
| 2010-10-08 | * (define-fun...) now has proper type checking in non-debug builds | Morgan Deters | |
| (resolves bug #212) * also closed some other type checking loopholes in SmtEngine * small fixes to define-sort (resolves bug #214) * infrastructural support for printing expressions in languages other than the internal representation language using an IO manipulator, e.g.: cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << expr; main() sets the output language for all streams to correspond to the input language * support delaying type checking in debug builds, so that one can debug the type checker itself (before it was difficult, because debug builds did all the type checking on Node creation!): new command-line flag --no-early-type-checking (only makes sense for debug builds) * disallowed copy-construction of ExprManager and NodeManager, and made other constructors explicit; previously it was easy to unintentionally create duplicate managers, with really weird results (i.e., disappearing attributes!) | |||
| 2010-10-08 | support (set-info) on status, source, category, difficulty, smt-lib-version, ↵ | Morgan Deters | |
| and notes; reduces extraneous "unsupported" output | |||
| 2010-10-07 | oops, reverting a change to a regression test that had intentionally caused ↵ | Morgan Deters | |
| a typechecking violation | |||
| 2010-10-07 | type checking for define-fun in production builds; related to (and might ↵ | Morgan Deters | |
| resolve) bug 212 | |||
| 2010-10-07 | NodeSelfIterator implementation and unit test (resolves bug #204); also fix ↵ | Morgan Deters | |
| ParserBlack unit test initialization | |||
| 2010-10-07 | Small tableau optimization. | Tim King | |
| 2010-10-07 | SMT-LIBv2 (define-fun...) command now functional; does eager expansion at ↵ | Morgan Deters | |
| preprocessing time | |||
| 2010-10-06 | declare-sort, define-sort working but not thoroughly tested; define-fun half ↵ | Morgan Deters | |
| working (just need to decide where to expand) | |||
| 2010-10-05 | parser and core support for SMT-LIBv2 commands get-info, set-option, ↵ | Morgan Deters | |
| get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly... | |||
| 2010-10-04 | fix gdb issues (at least for static builds); resolves bug 194 | Morgan Deters | |
| 2010-10-04 | fix regular expressions in build system | Morgan Deters | |
| 2010-10-04 | fixing CLN builds, which had broken the build tonight; will re-run ↵ | Morgan Deters | |
| regression script | |||
| 2010-10-04 | re-add a dependency to fix compile warnings | Morgan Deters | |
| 2010-10-04 | remove/shuffle some #include dependencies; fix some documentation; apply ↵ | Morgan Deters | |
| coding standards | |||
| 2010-10-04 | Fix to bug 211. ArithVar is now typedefed to uint32_t. | Tim King | |
| 2010-10-03 | file header documentation regenerated with contributors names; no code ↵ | Morgan Deters | |
| modified in this commit | |||
| 2010-10-02 | revert a workaround fix to CDMap that was committed as part of the ↵ | Morgan Deters | |
| arith-indexed-vars merge, and fix the root cause (maybe?) in attribute.cpp: previously, items from the cdnodes attribute table weren't properly being "obliterated" from the table due to a typo | |||
| 2010-10-02 | dump statistics on abnormal output: unexpected exceptions, SEGV, ILL, memout... | Morgan Deters | |
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback