projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2013-09-09
Morgan Deters
Add support for check-sat with argument.
commit
|
commitdiff
|
tree
2013-09-09
Morgan Deters
Fix declare-datatypes dumping bug (bug 385).
commit
|
commitdiff
|
tree
2013-09-09
Morgan Deters
Support per-command verbosity settings.
commit
|
commitdiff
|
tree
2013-09-09
Morgan Deters
Support empty (and 1-ary) tuples and records.
commit
|
commitdiff
|
tree
2013-09-09
Morgan Deters
Fix some line-numbering in auto-generated metakind...
commit
|
commitdiff
|
tree
2013-09-09
Morgan Deters
Fix portfolio on bug411.smt2. (get-model command shoul...
commit
|
commitdiff
|
tree
2013-09-09
Morgan Deters
Ensure no cost for datatypes debugging when not tracing it.
commit
|
commitdiff
|
tree
2013-09-07
Andrew Reynolds
Fix datatypes for bug 503
commit
|
commitdiff
|
tree
2013-09-05
Morgan Deters
Fix FLOOR and DISTINCT in CVC language parser.
commit
|
commitdiff
|
tree
2013-09-05
Morgan Deters
Fix lambda handling in CVC parser
commit
|
commitdiff
|
tree
2013-09-05
Morgan Deters
Permit setOption(decision-mode)
commit
|
commitdiff
|
tree
2013-09-05
Morgan Deters
Fix bugs/issues with missed-t-prop dump output
commit
|
commitdiff
|
tree
2013-09-05
Morgan Deters
Fix declare-fun/define-fun in dumps; resolves bugs...
commit
|
commitdiff
|
tree
2013-08-31
Morgan Deters
Add ability to mkConst(TupleSelect) and friends in...
commit
|
commitdiff
|
tree
2013-08-26
Kshitij Bansal
Merge branch '1.2.x'
commit
|
commitdiff
|
tree
2013-08-26
Kshitij Bansal
bug 374 fix: assert litVal=desiredVal only for leaf...
commit
|
commitdiff
|
tree
2013-08-26
Kshitij Bansal
Bug 374 benchmarks
commit
|
commitdiff
|
tree
2013-08-20
Morgan Deters
Change recursive expandDefinitions() to an interative...
commit
|
commitdiff
|
tree
2013-08-13
Morgan Deters
--segv-nospin is now default.
commit
|
commitdiff
|
tree
2013-08-13
Morgan Deters
Minor cleanup.
commit
|
commitdiff
|
tree
2013-08-13
Andrew Reynolds
Minor fixes for --fmf-fmc for quantifiers containing...
commit
|
commitdiff
|
tree
2013-08-13
Andrew Reynolds
initial modifications for per-ic cbqi
commit
|
commitdiff
|
tree
2013-08-09
Morgan Deters
Clean up "make install"-produced intermediate files...
commit
|
commitdiff
|
tree
2013-08-08
Morgan Deters
Fix a serious bug in the preprocessor; problem inputs...
commit
|
commitdiff
|
tree
2013-08-08
Morgan Deters
Parameterized, uninterpreted sorts need no Boolean...
commit
|
commitdiff
|
tree
2013-07-30
Morgan Deters
Minor fixes to build system.
commit
|
commitdiff
|
tree
2013-07-29
Morgan Deters
Fix numerous compiler warnings on various platforms
commit
|
commitdiff
|
tree
2013-07-24
Morgan Deters
Regressions now checking models on unknown too. But...
commit
|
commitdiff
|
tree
2013-07-24
Morgan Deters
Fixes for building with mingw win64.
commit
|
commitdiff
|
tree
2013-07-24
Morgan Deters
Don't allow --stats if not a statistics-enabled build
commit
|
commitdiff
|
tree
2013-07-24
Morgan Deters
some portfolio driver cleanup
commit
|
commitdiff
|
tree
2013-07-24
Morgan Deters
Some fixes for (get-info :all-options)
commit
|
commitdiff
|
tree
2013-07-23
Morgan Deters
fix for win32 option parsing via mingw32
commit
|
commitdiff
|
tree
2013-07-23
Morgan Deters
(get-info :all-options) to get option values; also...
commit
|
commitdiff
|
tree
2013-07-22
Morgan Deters
Allow BV and DT in either order in the logic string
commit
|
commitdiff
|
tree
2013-07-22
Andrew Reynolds
Add option --cbqi-recurse.
commit
|
commitdiff
|
tree
2013-07-22
Andrew Reynolds
Bug fix for --fmf-fmc for non-uninterpreted sort quanti...
commit
|
commitdiff
|
tree
2013-07-20
Morgan Deters
enable bug521 regression tests
commit
|
commitdiff
|
tree
2013-07-19
Dejan Jovanovic
possible fix for bug 521
commit
|
commitdiff
|
tree
2013-07-19
Morgan Deters
Minor fix for --no-condense-function-values
commit
|
commitdiff
|
tree
2013-07-18
Andrew Reynolds
Fix quantifier instantiation bug in cbqi, add default...
commit
|
commitdiff
|
tree
2013-07-17
Morgan Deters
Fix bug 516; include some bug testcases.
commit
|
commitdiff
|
tree
2013-07-16
Liana Hadarean
fixed seg fault when bv equality is turned off
commit
|
commitdiff
|
tree
2013-07-16
Liana Hadarean
fixed bug520
commit
|
commitdiff
|
tree
2013-07-16
Morgan Deters
Fix for get-antlr script and PIC/non-PIC objects, on...
commit
|
commitdiff
|
tree
2013-07-16
Morgan Deters
"Tabular"-style function definitions in models with...
commit
|
commitdiff
|
tree
2013-07-16
Morgan Deters
Minor bugfixes to model-building
commit
|
commitdiff
|
tree
2013-07-13
Morgan Deters
Remove now-unused language bindings interface file.
commit
|
commitdiff
|
tree
2013-07-13
Morgan Deters
Fix language bindings and portfolio builds.
commit
|
commitdiff
|
tree
2013-07-12
Morgan Deters
Fix for curious GCC 4.8 translation with -O.
commit
|
commitdiff
|
tree
2013-07-11
Morgan Deters
Remove auto-aritization from TPTP parser
commit
|
commitdiff
|
tree
2013-07-11
Morgan Deters
Support for TPTP's TFF0 (with arithmetic)
commit
|
commitdiff
|
tree
2013-07-11
Morgan Deters
Fix for Boolean-term rewriting and LAMBDAs
commit
|
commitdiff
|
tree
2013-07-10
Morgan Deters
Fix for bug 519; don't involve ITESimplifier in model...
commit
|
commitdiff
|
tree
2013-07-09
Andrew Reynolds
add relevant domain computation
commit
|
commitdiff
|
tree
2013-07-07
Morgan Deters
Model output is now const; this related to bug 519
commit
|
commitdiff
|
tree
2013-07-05
Morgan Deters
Fix for a datatype parsing bug that Tim found.
commit
|
commitdiff
|
tree
2013-07-02
Andrew Reynolds
Make uf strong solver user-context dependent, fixes...
commit
|
commitdiff
|
tree
2013-07-02
Andrew Reynolds
Minor fixes for bounded integers, rewrite engine.
commit
|
commitdiff
|
tree
2013-06-28
Andrew Reynolds
More bug fixes for interval models.
commit
|
commitdiff
|
tree
2013-06-28
Morgan Deters
Fix portfolio builds after yesterday's commits.
commit
|
commitdiff
|
tree
2013-06-27
Morgan Deters
Better check-models output for some kinds of problems...
commit
|
commitdiff
|
tree
2013-06-27
Morgan Deters
Fix minor warnings found by recent clang/gcc.
commit
|
commitdiff
|
tree
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
next