summaryrefslogtreecommitdiff
path: root/src/expr
AgeCommit message (Collapse)Author
2011-11-16Addressed many of the concerns raised in the public interface review of CVC4 ↵Morgan Deters
Datatypes (bug #283) by Chris Conway. Thanks, Chris!
2011-11-15Bindings work (ocaml bindings are now sort of working); also minor cleanupMorgan Deters
2011-11-06datatype stuff in compatibility interface implementedMorgan Deters
2011-11-04STRING_TYPE and CONST_STRING and associate type infrastructure implemented.Morgan Deters
2011-11-01Improvements to header installation on user machines. Internally, we canMorgan Deters
still write, for example: #include "expr/node.h" but public CVC4 headers, upon installation to /usr/include/cvc4 (or wherever), have such #includes rewritten automatically to: #include <cvc4/expr/node.h>
2011-10-29fix unit testsMorgan Deters
2011-10-29Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, ↵Morgan Deters
SmtEngine::getProof(), a few other things..
2011-10-28* ability to output NodeBuilders without first converting them to ↵Morgan Deters
Nodes---useful for debugging. * language-dependent Node::toString() * some minor proof-related cleanup
2011-10-13Interruption, time-out, and deterministic time-out ("resource-out") features.Morgan Deters
Details here: http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_October_14,_2011#Resource.2Ftime_limiting_API This will need more work, but it's a start. Also implemented TheoryEngine::properPropagation(). Other minor things.
2011-10-07Some new Datatype public functionality, as per Chris Conway's suggestions on ↵Morgan Deters
the dev mailing list.
2011-10-05Reverting a fix from earlier today that fixed a Mac OS warning but ↵Morgan Deters
completely broke Linux. :-(
2011-10-05minor visibility fixesMorgan Deters
2011-10-04Yet Another Antlr3 Mod---this time, all my fault: for configuration ↵Morgan Deters
auto-detection of libantlr3c, I chose an innocent-looking function that was present in both versions. But it's signature had changed, breaking source compatibility in both directions. Just like the other function that started the whole mess. Silly me.
2011-09-30interfaces fixes and cleanups...and examples of each interface!Morgan Deters
2011-09-29build system fixesMorgan Deters
2011-09-29Some base infrastructure for user push/pop; a few bugfixes to user push/pop ↵Morgan Deters
and model gen also. I also expect this commit to fix bug #273. No performance change is expected on regressions with this commit, see http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863
2011-09-23interface cleanup, java bindings workMorgan Deters
2011-09-21considerable bindings interface work, some improvements to buildMorgan Deters
2011-09-20Merge from "swig" branch: language binding for Java is compiling and ↵Morgan Deters
linking. Enable with --enable-language-bindings=java
2011-09-16dump define-funs correctly with "--dump declarations", whether the function ↵Morgan Deters
is defined via API or through input language
2011-09-16fix numerous documentation issues; doxygen complains much less, nowMorgan Deters
2011-09-15additional stuff for sharing, Dejan Jovanović
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
Dumping infrastructure. Can dump preprocessed queries and clauses. Can also dump queries (for testing with another solver) to see if any conflicts are missed, T-propagations are missed, all lemmas are T-valid, etc. For a full list of options see --dump=help. CUDD building much cleaner. Documentation and assertion fixes. Printer improvements, printing of commands in language-defined way, etc. Typechecker stuff in expr package now autogenerated, no need to manually edit the expr package when adding a new theory. CVC3 compatibility layer (builds as libcompat). SWIG detection and language binding support (infrastructure). Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode (when not in compliance mode). Copyright and file headers regenerated.
2011-09-02Partial merge of integers work; this is simple B&B and some pseudobooleanMorgan Deters
infrastructure, and takes care not to affect CVC4's performance on LRA benchmarks.
2011-07-11merge from symmetry branchMorgan Deters
2011-07-09minor fixupsMorgan Deters
2011-07-09surprize surprizeDejan Jovanović
2011-07-05updated preprocessing and rewriting input equalities into inequalities for LRADejan Jovanović
2011-06-30only use theory registration if (1) a theory requests it, or (2) if there's ↵Morgan Deters
more than one "real" theory (not BUILTIN or BOOL) active
2011-06-30some things I had laying around in a directory but never got committed; ↵Morgan Deters
minor fix-ups to documentation and some node stuff
2011-06-18Some fixes inspired by Fedora 15:Morgan Deters
* compilation fixes for GCC 4.6.x + ptrdiff_t is now in std:: * fix some make rules that are ok in Make 3.81 but broke in Make 3.82 * look for cxxtestgen.py as well as cxxtestgen.pl, and look for cxxtest headers in /usr/include
2011-06-06Fix for Mac OS breakage (x86 didn't crash, but probably would, eventually, ↵Morgan Deters
on some problems---valgrind gave many complaints): the problem was that calloc() (in the Backtracker) wasn't allocating enough space for the type located at the resulting address. Resolves bug #263. Also, some debugging improvements.
2011-06-03datatypes workMorgan Deters
2011-06-01minor fix, and better output for type errorsMorgan Deters
2011-06-01type ascriptions (casts) for parameterized datatypes, e.g. "nil :: list[INT]Morgan Deters
2011-05-23fixes for "make dist" and "make doc", minor cleanupsMorgan Deters
2011-05-23Merge from arrays2 branch.Morgan Deters
2011-05-14reverting node manager change from 1881; also part of parameterized ↵Morgan Deters
datatypes review
2011-05-14add AscriptionType stuff to support nullary parameterized datatypes; also, ↵Morgan Deters
review of Andy's earlier commit, with some minor code clean-up and documentation
2011-05-13added support for parametric datatypes, updated cvc parser to handle ↵Andrew Reynolds
parametric datatypes, type ascriptions are not implemented yet
2011-05-05Merge from nonclausal-simplification-v2 branch:Morgan Deters
* Preprocessing-time, non-clausal, Boolean simplification round to support "quasi-non-linear rewrites" as discussed at last few meetings. * --simplification=none is the default for now, but we'll probably change that to --simplification=incremental. --simplification=batch is also a possibility. See --simplification=help for details. * RecursionBreaker<T> now uses a hash set for the seen trail. * Fixes to TLS stuff to support that. * Fixes to theory and SmtEngine documentation. * Fixes to stream indentation. * Other miscellaneous stuff.
2011-05-02Minor fixes to various parts of CVC4, including the removal of the uintptr_t ↵Morgan Deters
constructors for Type and Expr (which existed due to ANTLR limitations). These issues are now handled (as a hack, due to said limitations) in the parser rather than the CVC4 core.
2011-05-01minor fixes, plus experimental readline support in InteractiveShellMorgan Deters
2011-04-25Monday tasks:Morgan Deters
* new "well-foundedness" type property (like cardinality) specified in Theory kinds files; specifies well-foundedness and a ground term * well-foundedness / finite checks in Datatypes now superseded by type system isFinite(), isWellFounded(), mkGroundTerm(). * new "RecursionBreaker" template class, a convenient class that keeps a "seen" trail without you having to pass it around (which is difficult in cases of mutual recursion) of the idea of passing around a "seen" trail
2011-04-25Weekend work. The main points:Morgan Deters
* Type::getCardinality() returns the cardinality for for all types. Theories give a cardinality in the their kinds file. For cardinalities that depend on a type argument, a "cardinality computer" function is named in the kinds file, which takes a TypeNode and returns its cardinality. * There's a bitmap for the set of "active theories" in the TheoryEngine. Theories become "active" when a term that is owned by them, or whose type is owned by them, is pre-registered (run CVC4 with --verbose to see theory activation). Non-active theories don't get any calls for check() or propagate() or anything, and if we're running in single-theory mode, the shared term manager doesn't have to get involved. This is really important for get() performance (which can only skimp on walking the entire sub-DAG only if the theory doesn't require it AND the shared term manager doesn't require it). * TheoryEngine now does not call presolve(), registerTerm(), notifyRestart(), etc., on a Theory if that theory doesn't declare that property in its kinds file. To avoid coding errors, mktheorytraits greps the theory header and gives warnings if: + the theory appears to declare one of the functions (check, propagate, etc.) that isn't listed among its kinds file properties (but probably should be) + the theory appears NOT to declare one of the functions listed in its kinds file properties * some bounded token stream work
2011-04-23* reviewed BooleanSimplification, added documentation & unit testMorgan Deters
* work around a lexer ambiguity in CVC grammar * add support for tracing antlr parser/lexer * add parsing support for more language features * initial parameterized types parsing work to support Andy's work
2011-04-20numerous bugfixesMorgan Deters
2011-04-20Minor mixed-bag commit. Expected performance impact negligible.Morgan Deters
* Fixed hole in arrays typechecking. * Fixed "make dist". * Better ouroborous test, and some printer fixes. * Continued cleanup in CVC parser, removed some warnings. * Better output.
2011-04-20Tuesday end-of-day commit.Morgan Deters
Expected performance impact outside of datatypes/CVC parser is negligible. * CVC language LAMBDA, functional LET, type LET, precedence fixes, bitvectors, and arrays, with partial parsing support also for quantifiers, tuples, subranges, subtypes, and records * support for complex recursive DATATYPE selectors, e.g. tree = node(children:ARRAY INT OF tree) | leaf(data:INT) these are complicated because they have to be left unresolved at parse time and dealt with in a second pass. * bugfix for Exprs/Types that occurred when setting them to null (not Nodes/TypeNodes, just Exprs/Types). * Cleanup/code review items
2011-04-18more work on CVC languageMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback