| 2013-06-27 |
Morgan Deters | Remove output.h from public space, to avoid clashes... |
commit | commitdiff | tree |
| 2013-06-27 |
Morgan Deters | Small fix for IS_INTEGER. |
commit | commitdiff | tree |
| 2013-06-27 |
Morgan Deters | Remove macros EXPECT_TRUE / EXPECT_FALSE from cvc4_publ... |
commit | commitdiff | tree |
| 2013-06-27 |
Morgan Deters | Better user documentation for mkVar() and mkBoundVar(). |
commit | commitdiff | tree |
| 2013-06-27 |
Morgan Deters | Minor printer cleanup for SMT-LIBv2 symbols "div" and... |
commit | commitdiff | tree |
| 2013-06-26 |
Andrew Reynolds | Add support for interval models in bounded integers... |
commit | commitdiff | tree |
| 2013-06-25 |
Morgan Deters | Merge branch '1.2.x' |
commit | commitdiff | tree |
| 2013-06-25 |
Morgan Deters | Proposed fix for bug #513 |
commit | commitdiff | tree |
| 2013-06-25 |
Andrew Reynolds | Refactoring of model engine to separate individual... |
commit | commitdiff | tree |
| 2013-06-25 |
Morgan Deters | Add files missing from last commit |
commit | commitdiff | tree |
| 2013-06-25 |
Morgan Deters | Support for abs, to_int, is_int, divisible in SMT-LIB... |
commit | commitdiff | tree |
| 2013-06-24 |
Andrew Reynolds | Add options for symmetry breaking in uf+ss totality... |
commit | commitdiff | tree |
| 2013-06-21 |
Morgan Deters | Fix failure in non-assertion builds on incorrect SmtEng... |
commit | commitdiff | tree |
| 2013-06-19 |
Morgan Deters | Merge branch '1.2.x' |
commit | commitdiff | tree |
| 2013-06-19 |
Morgan Deters | Workaround for suspected clang 3.0 codegen bug on Mac |
commit | commitdiff | tree |
| 2013-06-19 |
Morgan Deters | Fix to the "include" extended feature of the SMT-LIB... |
commit | commitdiff | tree |
| 2013-06-19 |
Morgan Deters | Give a more useful parse error message for "undeclared... |
commit | commitdiff | tree |
| 2013-06-17 |
Morgan Deters | Java streams example I forgot to add a long time ago |
commit | commitdiff | tree |
| 2013-06-17 |
Andrew Reynolds | Make --var-elim-quant true by default. Add rewrite... |
commit | commitdiff | tree |
| 2013-06-16 |
Andrew Reynolds | Fix in SMT2 parser for parametric datatypes |
commit | commitdiff | tree |
| 2013-06-10 |
Morgan Deters | another fix for array-store-all printing |
commit | commitdiff | tree |
| 2013-06-10 |
Morgan Deters | Better array-store-all output for SMT-LIB. |
commit | commitdiff | tree |
| 2013-06-08 |
Morgan Deters | Fix typos in alttheoryskel |
commit | commitdiff | tree |
| 2013-06-08 |
Morgan Deters | Fixes for Boolean terms in arrays (including fix for... |
commit | commitdiff | tree |
| 2013-06-07 |
Morgan Deters | One more case for arrays of Boolean. |
commit | commitdiff | tree |
| 2013-06-07 |
Morgan Deters | Fix for bug 517. |
commit | commitdiff | tree |
| 2013-06-07 |
Morgan Deters | Allow disabling include-file feature |
commit | commitdiff | tree |
| 2013-06-07 |
Dejan Jovanović | small parese issue in IDL |
commit | commitdiff | tree |
| 2013-06-06 |
Dejan Jovanović | typo |
commit | commitdiff | tree |
| 2013-06-06 |
Dejan Jovanović | IDL example theory (to be used with --use-theory=idl). |
commit | commitdiff | tree |
| 2013-06-05 |
Andrew Reynolds | Fix bug in --fmf-fmc for producing models of functions... |
commit | commitdiff | tree |
| 2013-06-04 |
Morgan Deters | File inclusion in Smt2 parser. |
commit | commitdiff | tree |
| 2013-06-04 |
Morgan Deters | Add --no-condense-function-values option for explicit... |
commit | commitdiff | tree |
| 2013-06-04 |
Morgan Deters | Merge branch '1.2.x' |
commit | commitdiff | tree |
| 2013-06-04 |
Morgan Deters | Fix clang static initialization order issue; fixes... |
commit | commitdiff | tree |
| 2013-06-04 |
Andrew Reynolds | Add partial support for MBQI with arrays when using... |
commit | commitdiff | tree |
| 2013-06-03 |
Morgan Deters | Merge tag 'casc24' |
commit | commitdiff | tree |
| 2013-06-03 |
Morgan Deters | Updated CASC scripts, as provided to Geoff Sutcliffe |
commit | commitdiff | tree |
| 2013-05-29 |
Morgan Deters | Merge branch '1.2.x' |
commit | commitdiff | tree |
| 2013-05-29 |
Morgan Deters | Per SMT-LIB spec, allow (set-info..) command to succeed... |
commit | commitdiff | tree |
| 2013-05-29 |
Morgan Deters | SMT-LIB printer updates (some missing cases). |
commit | commitdiff | tree |
| 2013-05-29 |
Morgan Deters | Fix bug where strict mode didn't allow DIV or MOD,... |
commit | commitdiff | tree |
| 2013-05-28 |
Morgan Deters | Standardize SMT-LIBv2 set of logics to use LogicInfo. |
commit | commitdiff | tree |
| 2013-05-23 |
Andrew Reynolds | Refactoring to prepare for MBQI with integer quantifica... |
commit | commitdiff | tree |
| 2013-05-22 |
Andrew Reynolds | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2013-05-22 |
Andrew Reynolds | Significant work on bounded integer quantification... |
commit | commitdiff | tree |
| 2013-05-22 |
Andrew Reynolds | Add regressions for finite model finding |
commit | commitdiff | tree |
| 2013-05-21 |
Morgan Deters | Merge branch '1.2.x' |
commit | commitdiff | tree |
| 2013-05-21 |
Morgan Deters | Fix bug 512: an assertion failure only appearing with... |
commit | commitdiff | tree |
| 2013-05-21 |
Morgan Deters | Fix an error that valgrind found. |
commit | commitdiff | tree |
| 2013-05-21 |
Morgan Deters | Merge branch '1.2.x' |
commit | commitdiff | tree |
| 2013-05-21 |
Morgan Deters | Fix incremental bug in symmetry breaker. |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Merge branch '1.2.x' |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Fix error reporting on use of (nonlinear) div,mod,... |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Update THANKS to mention David Cok's contributions. |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Detect multiply-defined :named annotations and issue... |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Fix parsing of SMT-LIBv2 |quoted| symbols that span... |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Compliance fixes for :named annotations: they must... |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Don't allow get-model & co after a user push/pop |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | As per SMT-LIB standard: make - and xor take n>2 args... |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Fix for equality-chaining of Booleans in SMT-LIBv2. |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Fix destruction issue in GetValueCommand leading to... |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Better error on invalid logic strings. |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Better error on illegal (pop N); also more compliant... |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | A couple of fixes to the get-option command for complia... |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Disallow construction of (_ BitVec 0). |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Fixed "success" response to (push N) / (pop N) with... |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Fix to empty response to (get-assignment). |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | configure fix for building with glpk on redhat, perhaps... |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | minor changes to language bindings |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | disable Logic-checking with finite model finding for... |
commit | commitdiff | tree |
| 2013-05-20 |
Morgan Deters | Fix erroneous results when the logic was incorrectly... |
commit | commitdiff | tree |
| 2013-05-20 |
Andrew Reynolds | Possible final version of run scripts for casc. |
commit | commitdiff | tree |
| 2013-05-17 |
Andrew Reynolds | Add model-producing run script for casc. |
commit | commitdiff | tree |
| 2013-05-17 |
Andrew Reynolds | Add support for --dump-models option, in preparation... |
commit | commitdiff | tree |
| 2013-05-17 |
Morgan Deters | As per SMT-LIB standard: make - and xor take n>2 args... |
commit | commitdiff | tree |
| 2013-05-17 |
Morgan Deters | Fix for equality-chaining of Booleans in SMT-LIBv2. |
commit | commitdiff | tree |
| 2013-05-17 |
Morgan Deters | Fix destruction issue in GetValueCommand leading to... |
commit | commitdiff | tree |
| 2013-05-17 |
Morgan Deters | Better error on invalid logic strings. |
commit | commitdiff | tree |
| 2013-05-17 |
Morgan Deters | Better error on illegal (pop N); also more compliant... |
commit | commitdiff | tree |
| 2013-05-17 |
Morgan Deters | A couple of fixes to the get-option command for complia... |
commit | commitdiff | tree |
| 2013-05-17 |
Morgan Deters | Disallow construction of (_ BitVec 0). |
commit | commitdiff | tree |
| 2013-05-17 |
Morgan Deters | Fixed "success" response to (push N) / (pop N) with... |
commit | commitdiff | tree |
| 2013-05-17 |
Morgan Deters | Fix to empty response to (get-assignment). |
commit | commitdiff | tree |
| 2013-05-16 |
Morgan Deters | configure fix for building with glpk on redhat, perhaps... |
commit | commitdiff | tree |
| 2013-05-16 |
Andrew Reynolds | Fix minor bug in full_model_check.cpp |
commit | commitdiff | tree |
| 2013-05-16 |
Morgan Deters | minor changes to language bindings |
commit | commitdiff | tree |
| 2013-05-14 |
Andrew Reynolds | Update casc24-fnt run script. Add casc24-fof run script. |
commit | commitdiff | tree |
| 2013-05-14 |
lianah | added some extra options to the bit-vector theory |
commit | commitdiff | tree |
| 2013-05-14 |
Andrew Reynolds | Add support for quantifier patterns in smt2 printer. |
commit | commitdiff | tree |
| 2013-05-14 |
Andrew Reynolds | Refactoring to separate old and new model building... |
commit | commitdiff | tree |
| 2013-05-11 |
Andrew Reynolds | Preliminary version of finite model finding over bounde... |
commit | commitdiff | tree |
| 2013-05-10 |
Morgan Deters | disable Logic-checking with finite model finding for... |
commit | commitdiff | tree |
| 2013-05-10 |
lianah | now proofs print mapping between atom and propositional... |
commit | commitdiff | tree |
| 2013-05-10 |
Andrew Reynolds | Update casc run script. Work on compliance for SZS... |
commit | commitdiff | tree |
| 2013-05-10 |
lianah | fixes to the proof system so it works with theory lemma... |
commit | commitdiff | tree |
| 2013-05-10 |
Morgan Deters | Fix erroneous results when the logic was incorrectly... |
commit | commitdiff | tree |
| 2013-05-10 |
Morgan Deters | Add documentation for --disable-fmf-inst-gen, which... |
commit | commitdiff | tree |
| 2013-05-10 |
Andrew Reynolds | Add simplification option --fo-prop-quant. Add model... |
commit | commitdiff | tree |
| 2013-05-09 |
Kshitij Bansal | Merge branch 'master' of ssh://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog