| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-12-03 | Floating point infrastructure. | Martin Brain | |
| Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> | |||
| 2014-11-17 | Resource-limiting work. | Liana Hadarean | |
| Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> | |||
| 2014-11-09 | Merge branch '1.4.x' | Morgan Deters | |
| 2014-11-09 | Work around an apparent bug in libc++ that was causing crashes on Mac.. | Morgan Deters | |
| 2014-10-23 | Parsing and infrastructure support for SMT-LIBv2.5 input and output languages. | Morgan Deters | |
| * support for new commands meta-info, declare-const, echo, get-model, reset, and reset-assertions * support for set-option :global-declarations * support for set-option :produce-assertions * support for set-option :reproducible-resource-limit * support for get-info :assertion-stack-levels * support for set-info :smt-lib-version 2.5 * ascribe types for abstract values (the new 2.5 standard clarifies that this is required) * SMT-LIB v2.5 string literals (we still support 2.0 string literals when in 2.0 mode) What's still to do: * check-sat-assumptions/get-unsat-assumptions (still being hotly debated). Also set-option :produce-unsat-assumptions. * define-fun-rec doesn't allow mutual recursion * All options should be restored to defaults with (reset) command. (Currently :incremental and maybe others get "stuck" due to late driver integration.) | |||
| 2014-10-16 | Fix clang warnings | Morgan Deters | |
| 2014-10-14 | Context-dependent expr attributes are now attached to a specific SmtEngine, ↵ | Morgan Deters | |
| and the SAT context is owned by the SmtEngine. | |||
| 2014-10-11 | Merge branch '1.4.x' | Morgan Deters | |
| 2014-10-11 | Some defensive programming at destruction time, and fix a latent dangling ↵ | Morgan Deters | |
| pointer bug. | |||
| 2014-10-06 | Merge branch '1.4.x' | Morgan Deters | |
| 2014-10-06 | Fix a bug in tuple-record handling. Thanks to Saumya Debray for the report. | Morgan Deters | |
| 2014-10-06 | Support for RESET command in CVC native language (and infrastructure for ↵ | Morgan Deters | |
| support elsewhere). | |||
| 2014-10-03 | Support exporting array-store-all expressions to other ExprManagers (fixes ↵ | Morgan Deters | |
| portfolio test failures). | |||
| 2014-10-03 | Merge branch '1.4.x' | Morgan Deters | |
| Conflicts: NEWS | |||
| 2014-10-03 | Fix output of integer-valued real constants in SMT-LIB models (thanks ↵ | Morgan Deters | |
| Christoph Sticksel for reporting). | |||
| 2014-08-26 | Improved SMT-LIBv2 language support for unsat cores. | Morgan Deters | |
| 2014-08-24 | fix option alias (minor) | Kshitij Bansal | |
| 2014-08-22 | Unsat core infrastruture and API (SMT-LIB compliance to come). | Morgan Deters | |
| 2014-08-18 | Add support for quantifier-specific instantiation levels. Add option for ↵ | ajreynol | |
| setting inst-level 0 only for input terms. | |||
| 2014-07-01 | Update copyrights. | Morgan Deters | |
| 2014-06-19 | Java bindings fixes. | Morgan Deters | |
| 2014-06-19 | Another fix for the CASC stuff. | Morgan Deters | |
| 2014-06-19 | For casc : print models of functions rewritten by sort inference. | ajreynol | |
| 2014-06-19 | Clean up some compiler warnings on 32-bit. | Morgan Deters | |
| 2014-06-06 | option to hide stats which are zero (off by default), also some aliases | Kshitij Bansal | |
| 2014-06-06 | Sets translate, and other short fixes | Kshitij Bansal | |
| - $ is a simple symbol is smt2. - ever found yourself counting in kind.h? no longer. - expose parser "logic is set" state for smt/smt2 (any better way?) - a more helpful assertion message in smt_engine | |||
| 2014-05-27 | Some fixes to GC order in Java. | Morgan Deters | |
| 2014-05-27 | Fix typo in Java destruction code; should fix some recent bug reports of ↵ | Morgan Deters | |
| crashes in Java. | |||
| 2014-05-24 | Some cleanup, fix warnings raised by Debian packager. | Morgan Deters | |
| 2014-05-11 | More preparation for CASC proofs. Minor fix for sort inference (rewrite new ↵ | Andrew Reynolds | |
| assertions). Bug fix for ambqi : simplify correctly for multi-sorted case. Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real. | |||
| 2014-05-09 | Add variable ordering to ambqi. Bug fix to macros. More preparation for ↵ | Andrew Reynolds | |
| CASC proofs. | |||
| 2014-04-28 | nodemanager robust skolem numbering | Kshitij Bansal | |
| 2014-04-17 | simplify mkSkolem naming system: don't use $$ | Kshitij Bansal | |
| Short summary: By default NODEID is appeneded, just continue doing what you were, just don't add the _$$ at the end. Long summary: Before this commit there were four (yes!) ways to specify the names for new skolems, which result in names as given below 1) mkSkolem("name", ..., SKOLEM_FLAG_DEFAULT) -> "name_NODEID" 2) mkSkolem("name", ..., SKOLEM_EXACT_NAME) -> "name" 3) mkSkolem("name_$$", ..., SKOLEM_FLAG_DEFAULT) -> "name_NODEID" 4) mkSkolem("na_$$_me", ..., SKOLEM_FLAG_DEFAULT) -> "na_NODEID_me" After this commit, only 1) and 2) stay. 90% usage is of 1) or 3), which results in exact same behavior (and looking at the source code it doesn't look like everyone realized that the _$$ is just redundant). Almost no one used 4), which is the only reason to even have $$. Post this commit if you really want a number in the middle, manually construct the name and use the SKOLEM_EXACT_NAME flag. | |||
| 2014-04-09 | Minor change to better support parameterized partial/total kinds (for ↵ | Morgan Deters | |
| upcoming datatypes work). | |||
| 2014-03-20 | Merge pull request #22 from kbansal/sets-model | Kshitij Bansal | |
| Sets model | |||
| 2014-03-20 | push subtyping for sets to the element type | Kshitij Bansal | |
| for eg, (Set Int) is subtype of (Set Real) if Int is subtype of Real | |||
| 2014-03-11 | Minor cleanup. | Morgan Deters | |
| * Reenable parts of bvsimple test * Fix typo in #endif comment | |||
| 2014-03-07 | Remove --ite-remove-quant; support pulling ground ITEs out of quantifier ↵ | Morgan Deters | |
| bodies; fix bug 551, improper ITE removal under quantifiers. | |||
| 2014-03-04 | More useful error message when someone tries mkExpr(VARIABLE). | Morgan Deters | |
| 2014-02-21 | Merge branch '1.3.x' | Morgan Deters | |
| 2014-02-21 | Fix two variants of Node::substitute(). | Morgan Deters | |
| Node::substitute() is overloaded. One version was properly substituting operators (e.g. the "f" in f(x) could be substituted). The others were ignoring anything in function position. Fixed. Thanks to Wei Wang for pointing this out. | |||
| 2014-02-21 | portfolio: fix export of emptyset | Kshitij Bansal | |
| 2014-02-21 | add new theory (sets) | Kshitij Bansal | |
| Specification (smt2) -- as per this commit, subject to change - Parameterized sort Set, e.g. (Set Int) - Empty set constant (typed), use with "as" to specify the type, e.g. (as emptyset (Set Int)) - Create a singleton set (setenum X (Set X)) : creates singleton set - Functions/operators (union (Set X) (Set X) (Set X)) (intersection (Set X) (Set X) (Set X)) (setminus (Set X) (Set X) (Set X)) - Predicates (in X (Set X) Bool) : membership (subseteq (Set X) (Set X) Bool) : set containment | |||
| 2014-01-02 | Update copyright year. | Morgan Deters | |
| 2013-12-24 | Better automatic handling of output language setting. | Morgan Deters | |
| 2013-12-24 | Minor code cleanup. | Morgan Deters | |
| 2013-12-10 | Fix warning. | Morgan Deters | |
| 2013-12-07 | fix bug 542 | Kshitij Bansal | |
| 2013-12-05 | Fix NodeValue bitfields for 32-bit; fix comment. | Morgan Deters | |
| 2013-12-05 | Update copyrights, add missing file-level documentation; fix perms. | 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