Age | Commit message (Collapse) | Author | |
---|---|---|---|
2013-03-14 | Merge branch '1.0.x' | Morgan Deters | |
2013-03-14 | Fix warning (line annotation) | Morgan Deters | |
2013-03-14 | fix to build system: #include the proper file when they are in both builds ↵ | Morgan Deters | |
and src | |||
2013-03-13 | Added a rewrite for iff: | Clark Barrett | |
x = c iff x = d ---> false This fixes Andy's problem if unconstrained simplification is turned on. | |||
2013-03-11 | ite removal option for quantifiers --ite-remove-quant, e-matching for ↵ | Andrew Reynolds | |
boolean terms, improvement for pre skolemization | |||
2013-03-08 | Disallow overflow in bitvector literals (parser only) | Morgan Deters | |
* For example, (_ bv5 1) is now an error instead of being silently truncated. * Probably inappropriate for 1.0.x because it changes exception specifications. | |||
2013-03-06 | Best heuristics for handling decision requests from arrays | Clark Barrett | |
2013-03-06 | fixed two bugs for the new E-matching implementation, added aggressive ↵ | Andrew Reynolds | |
miniscoping option --ag-miniscope-quant, minor cleanup | |||
2013-03-05 | Merge branch '1.0.x' | Morgan Deters | |
Conflicts: src/smt/smt_engine.cpp | |||
2013-03-05 | Bugfix for SmtEngine: proper unsubscribing for NodeManager events | Morgan Deters | |
2013-03-01 | Merge branch '1.0.x' | Morgan Deters | |
2013-02-26 | Bug fix for rep-set. | Morgan Deters | |
(Cherry-picked from commit c71ec27 in master.) | |||
2013-02-26 | Fix for quantifiers containing Boolean terms. | Morgan Deters | |
2013-02-26 | Merge branch '1.0.x' | lianah | |
2013-02-26 | Merge branch '1.0.x' of https://github.com/CVC4/CVC4 into 1.0.x | lianah | |
2013-02-26 | fix for bv crash in incremental mode; this is a temporary fix for bug 493 | lianah | |
2013-02-24 | added option --model-u-dt-enum for outputting uninterpreted sorts as ↵ | Andrew Reynolds | |
datatype enumerations + minor update to array rewriter to improve output for this option, minor refactoring of representative selection for quantifier instantiation, initial draft of disequality propagation option --uf-ss-deq-prop, other refactoring of uf strong solver, fixed bug 496, improvement for fmf enumeration of finite built-in sorts | |||
2013-02-20 | Single -q quiets messages/warnings. Double -qq silences sat/unsat output too. | Morgan Deters | |
2013-02-20 | Some exception specification fixes in SmtEngine/Command infrastructure | Morgan Deters | |
2013-02-18 | Fix for gitinfo (resolves bug 399). | Morgan Deters | |
2013-02-16 | Merge branch '1.0.x' | Kshitij Bansal | |
2013-02-16 | gitinfo modifications fix | Kshitij Bansal | |
2013-02-16 | Merge pull request #6 from kbansal/decNewoptions | Kshitij Bansal | |
decision/ code refactoring | |||
2013-02-16 | decision: jh: more refactoring (.h->.cpp, xor/iff) | Kshitij Bansal | |
2013-02-16 | decision/ : jh: refactor embedded ITE, other minor | Kshitij Bansal | |
other minor: cleanup some remaning fragments of GiveUpException(), hopefully all is gone now. | |||
2013-02-16 | decision/: justification: refactor ITE out | Kshitij Bansal | |
2013-02-16 | refactoring justification_heuristic code | Kshitij Bansal | |
2013-02-16 | rm decision jh GiveUp related code | Kshitij Bansal | |
2013-02-16 | Some cleanup and copyright updating | Morgan Deters | |
* update some copyrights for 2013 * cleaned up some comments/ifdefs, indentation * some spelling corrections * add some missing makefiles | |||
2013-02-16 | Merge branch '1.0.x' | Morgan Deters | |
2013-02-16 | Fix version identification for new git repository. | Morgan Deters | |
2013-02-16 | Fix typo in error message | Morgan Deters | |
2013-02-15 | Merge branch '1.0.x' | Kshitij Bansal | |
2013-02-15 | prvs commit: lower warning to notice | Kshitij Bansal | |
Signed-off-by: Kshitij Bansal <kshitij@cs.nyu.edu> | |||
2013-02-15 | make incremental+portfolio experimental | Kshitij Bansal | |
2013-02-15 | make incremental+portfolio experimental | Kshitij Bansal | |
2013-02-15 | Merge branch '1.0.x' | Morgan Deters | |
2013-02-15 | Fix ECHO command in CVC language parser to not output quotation marks | Morgan Deters | |
2013-02-15 | Merge branch '1.0.x' | Tim King | |
2013-02-15 | repairs a bug in rewriterule engine: constructor cannot be used as a pattern | Tianyi Liang | |
(cherry picked from commit c33a1abc78bcd51f3f95562b117498caf252cafc) Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> | |||
2013-02-14 | Removing BVDebug and replacing with Debug. | Tim King | |
2013-02-13 | repairs a bug in rewriterule engine: constructor cannot be used as a pattern | Tianyi Liang | |
2013-02-12 | Fix a preprocessing performance issue. | Morgan Deters | |
2013-02-08 | Fix user-values in SMT-LIB v1.2 | Morgan Deters | |
2013-02-07 | Merge branch '1.0.x' | Morgan Deters | |
Conflicts: src/theory/quantifiers/theory_quantifiers.cpp | |||
2013-02-07 | Only put quantifier assertions in model equality engine if fullModel==true | Morgan Deters | |
2013-02-07 | Significant work on bug #491 (not yet closed). | Morgan Deters | |
2013-02-07 | More complete fix for bug 484 (includes fixes for records and tuples). | Morgan Deters | |
2013-02-07 | Fix error in tuple type-checking. | Morgan Deters | |
2013-02-07 | Make --default-dag-thresh apply to stringstreams | Morgan Deters | |