Age | Commit message (Collapse) | Author | |
---|---|---|---|
2014-04-28 | Merge pull request #25 from kbansal/sets | Kshitij Bansal | |
Sets | |||
2014-04-28 | Preparation for models for co-inductive datatypes. Minor cleanup. | Andrew Reynolds | |
2014-04-28 | Optimizations for datatypes: check for clashes modulo equality. Avoid ↵ | ajreynol | |
building model at fullModel=false when possible. Minor cleanup. | |||
2014-04-28 | minor fix | Kshitij Bansal | |
2014-04-28 | Merge remote-tracking branch 'upstream/master' into sets | Kshitij Bansal | |
2014-04-28 | travis, please! | Kshitij Bansal | |
2014-04-27 | attempt to improve CVC4's "parse error" message | Kshitij Bansal | |
2014-04-27 | rm undocument/non-working* "feature" | Kshitij Bansal | |
*test of unsigned for negative | |||
2014-04-24 | minor change: add a heuristic for preventing constant splitting. | Tianyi Liang | |
2014-04-24 | optimization | Kshitij Bansal | |
2014-04-24 | Avoid assigning constructor terms to 1-constructor datatype eqcs, when ↵ | ajreynol | |
possible, to ensure termination for codatatypes. Minor changes. | |||
2014-04-24 | Compute care graph for datatypes. Preliminary results show 20x speed up on ↵ | Andrew Reynolds | |
larger problems. Improve datatypes rewriter. | |||
2014-04-24 | Add --inst-max-level=N option for Kshitij. Support define-const command in ↵ | Andrew Reynolds | |
Smt2. | |||
2014-04-22 | Minor fix to avoid rewriting datatype equalities into non-equalitiers, as ↵ | Andrew Reynolds | |
required. Add APPLY_UF to congruence types to avoid model construction bugs. | |||
2014-04-19 | Eh, what? | Kshitij Bansal | |
2014-04-19 | fix warnings in strings/ | Kshitij Bansal | |
2014-04-17 | Allow fmf-bound-int to be set with set-option and via API. | Morgan Deters | |
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-17 | use internal skolem numbering | Kshitij Bansal | |
2014-04-17 | Minor refactoring and optimizing. | Andrew Reynolds | |
2014-04-14 | Fix bug in mbqi=fmc handling theory symbols. Fix mbqi=fmc models (Bug 557). ↵ | Andrew Reynolds | |
Improve datatypes rewrite, make option for previous dt semantics. | |||
2014-04-14 | Add initial support for co-datatypes. | Andrew Reynolds | |
2014-04-11 | Better support for building with mingw64; thanks to Nicolas Roche @ Altran ↵ | Morgan Deters | |
for the fix. | |||
2014-04-10 | setType -> setOfType, resolves bug 556 | Morgan Deters | |
2014-04-10 | Fix the build; --check-proof works for UF but not for the new UFC logic. | Morgan Deters | |
2014-04-10 | Expand definitions in theory datatypes, now has the expected semantics for ↵ | Andrew Reynolds | |
incorrectly applied selector terms. | |||
2014-04-10 | Boolean terms conversion fix for datatypes, fixes a problem Andy discovered ↵ | Morgan Deters | |
on his branch. | |||
2014-04-10 | Merge branch 'master' of github.com:tiliang/CVC4 | Tianyi Liang | |
2014-04-10 | minor fix for strings | Tianyi Liang | |
2014-04-10 | minor fix for strings | Tianyi Liang | |
2014-04-10 | Add support for cardinality constraints logic UFC. Add regressions in fmf/. ↵ | Andrew Reynolds | |
Fix datatypes E-matching bug. Change defaults : mbqi=fmc, decision heuristic stoponly=false for quantified logics, decision=justification for ALL_SUPPORTED, full-saturate-quant=false. Minor fix for fmc models. Add infrastructure to datatypes to prepare for next commit. | |||
2014-04-10 | refactor .travis.yml | Kshitij Bansal | |
2014-04-09 | Merge pull request #24 from kbansal/sets-model | Kshitij Bansal | |
sets, misc | |||
2014-04-09 | Minor change to better support parameterized partial/total kinds (for ↵ | Morgan Deters | |
upcoming datatypes work). | |||
2014-04-09 | Revert E-matching datatypes fix. | Andrew Reynolds | |
2014-04-09 | Handle fmf.card as input from user, add support in SMT2 parser, as requested ↵ | Andrew Reynolds | |
by Martin Brain. Fix two minor bugs : E-matching with datatypes, instantiation caching with incremental. | |||
2014-04-09 | fix get-info error-behavior | Kshitij Bansal | |
2014-04-09 | add tests | Kshitij Bansal | |
2014-04-09 | fix | Kshitij Bansal | |
2014-04-09 | prep for fix | Kshitij Bansal | |
2014-04-09 | try foreach on CD datastructure | Kshitij Bansal | |
2014-04-09 | inputs to trigger bug | Kshitij Bansal | |
2014-04-09 | more | Kshitij Bansal | |
2014-04-09 | some debugging changes | Kshitij Bansal | |
2014-04-06 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Kshitij Bansal | |
2014-04-06 | Reduced example from pcc's bug report. | Tim King | |
2014-04-06 | Merge pull request #21 from pcc/ite-fix | Tim King | |
Fix for ite of >=64bit wide bitvectors with unconstrained condition. | |||
2014-04-06 | fix for hiding prompt/header in shell, error-behavior options as in SMTLIB | Kshitij Bansal | |
2014-04-04 | For security, add --no-filesystem-access option, which disables SMT-LIB ↵ | Morgan Deters | |
script access to filesystem. | |||
2014-04-04 | Allow turning off the interactive prompt while in interactive mode. | Morgan Deters | |