projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2013-09-09 Andrew ReynoldsAnother minor fix for datatypes to repair my previous... commit | commitdiff | tree
2013-09-09 Morgan DetersAdd support for check-sat with argument. commit | commitdiff | tree
2013-09-09 Morgan DetersFix declare-datatypes dumping bug (bug 385). commit | commitdiff | tree
2013-09-09 Morgan DetersSupport per-command verbosity settings. commit | commitdiff | tree
2013-09-09 Morgan DetersSupport empty (and 1-ary) tuples and records. commit | commitdiff | tree
2013-09-09 Morgan DetersFix some line-numbering in auto-generated metakind... commit | commitdiff | tree
2013-09-09 Morgan DetersFix portfolio on bug411.smt2. (get-model command shoul... commit | commitdiff | tree
2013-09-09 Morgan DetersEnsure no cost for datatypes debugging when not tracing it. commit | commitdiff | tree
2013-09-07 Andrew ReynoldsFix datatypes for bug 503 commit | commitdiff | tree
2013-09-05 Morgan DetersFix FLOOR and DISTINCT in CVC language parser. commit | commitdiff | tree
2013-09-05 Morgan DetersFix lambda handling in CVC parser commit | commitdiff | tree
2013-09-05 Morgan DetersPermit setOption(decision-mode) commit | commitdiff | tree
2013-09-05 Morgan DetersFix bugs/issues with missed-t-prop dump output commit | commitdiff | tree
2013-09-05 Morgan DetersFix declare-fun/define-fun in dumps; resolves bugs... commit | commitdiff | tree
2013-08-31 Morgan DetersAdd ability to mkConst(TupleSelect) and friends in... commit | commitdiff | tree
2013-08-26 Kshitij BansalMerge branch '1.2.x' commit | commitdiff | tree
2013-08-26 Kshitij Bansalbug 374 fix: assert litVal=desiredVal only for leaf... commit | commitdiff | tree
2013-08-26 Kshitij BansalBug 374 benchmarks commit | commitdiff | tree
2013-08-20 Morgan DetersChange 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 DetersMinor cleanup. commit | commitdiff | tree
2013-08-13 Andrew ReynoldsMinor fixes for --fmf-fmc for quantifiers containing... commit | commitdiff | tree
2013-08-13 Andrew Reynoldsinitial modifications for per-ic cbqi commit | commitdiff | tree
2013-08-09 Morgan DetersClean up "make install"-produced intermediate files... commit | commitdiff | tree
2013-08-08 Morgan DetersFix a serious bug in the preprocessor; problem inputs... commit | commitdiff | tree
2013-08-08 Morgan DetersParameterized, uninterpreted sorts need no Boolean... commit | commitdiff | tree
2013-07-30 Morgan DetersMinor fixes to build system. commit | commitdiff | tree
2013-07-29 Morgan DetersFix numerous compiler warnings on various platforms commit | commitdiff | tree
2013-07-24 Morgan DetersRegressions now checking models on unknown too. But... commit | commitdiff | tree
2013-07-24 Morgan DetersFixes for building with mingw win64. commit | commitdiff | tree
2013-07-24 Morgan DetersDon't allow --stats if not a statistics-enabled build commit | commitdiff | tree
2013-07-24 Morgan Deterssome portfolio driver cleanup commit | commitdiff | tree
2013-07-24 Morgan DetersSome fixes for (get-info :all-options) commit | commitdiff | tree
2013-07-23 Morgan Detersfix 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 DetersAllow BV and DT in either order in the logic string commit | commitdiff | tree
2013-07-22 Andrew ReynoldsAdd option --cbqi-recurse. commit | commitdiff | tree
2013-07-22 Andrew ReynoldsBug fix for --fmf-fmc for non-uninterpreted sort quanti... commit | commitdiff | tree
2013-07-20 Morgan Detersenable bug521 regression tests commit | commitdiff | tree
2013-07-19 Dejan Jovanovicpossible fix for bug 521 commit | commitdiff | tree
2013-07-19 Morgan DetersMinor fix for --no-condense-function-values commit | commitdiff | tree
2013-07-18 Andrew ReynoldsFix quantifier instantiation bug in cbqi, add default... commit | commitdiff | tree
2013-07-17 Morgan DetersFix bug 516; include some bug testcases. commit | commitdiff | tree
2013-07-16 Liana Hadareanfixed seg fault when bv equality is turned off commit | commitdiff | tree
2013-07-16 Liana Hadareanfixed bug520 commit | commitdiff | tree
2013-07-16 Morgan DetersFix 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 DetersMinor bugfixes to model-building commit | commitdiff | tree
2013-07-13 Morgan DetersRemove now-unused language bindings interface file. commit | commitdiff | tree
2013-07-13 Morgan DetersFix language bindings and portfolio builds. commit | commitdiff | tree
2013-07-12 Morgan DetersFix for curious GCC 4.8 translation with -O. commit | commitdiff | tree
2013-07-11 Morgan DetersRemove auto-aritization from TPTP parser commit | commitdiff | tree
2013-07-11 Morgan DetersSupport for TPTP's TFF0 (with arithmetic) commit | commitdiff | tree
2013-07-11 Morgan DetersFix for Boolean-term rewriting and LAMBDAs commit | commitdiff | tree
2013-07-10 Morgan DetersFix for bug 519; don't involve ITESimplifier in model... commit | commitdiff | tree
2013-07-09 Andrew Reynoldsadd relevant domain computation commit | commitdiff | tree
2013-07-07 Morgan DetersModel output is now const; this related to bug 519 commit | commitdiff | tree
2013-07-05 Morgan DetersFix for a datatype parsing bug that Tim found. commit | commitdiff | tree
2013-07-02 Andrew ReynoldsMake uf strong solver user-context dependent, fixes... commit | commitdiff | tree
2013-07-02 Andrew ReynoldsMinor fixes for bounded integers, rewrite engine. commit | commitdiff | tree
2013-06-28 Andrew ReynoldsMore bug fixes for interval models. commit | commitdiff | tree
2013-06-28 Morgan DetersFix portfolio builds after yesterday's commits. commit | commitdiff | tree
2013-06-27 Morgan DetersBetter check-models output for some kinds of problems... commit | commitdiff | tree
2013-06-27 Morgan DetersFix minor warnings found by recent clang/gcc. commit | commitdiff | tree
2013-06-27 Morgan DetersRemove output.h from public space, to avoid clashes... commit | commitdiff | tree
2013-06-27 Morgan DetersSmall fix for IS_INTEGER. commit | commitdiff | tree
2013-06-27 Morgan DetersRemove macros EXPECT_TRUE / EXPECT_FALSE from cvc4_publ... commit | commitdiff | tree
2013-06-27 Morgan DetersBetter user documentation for mkVar() and mkBoundVar(). commit | commitdiff | tree
2013-06-27 Morgan DetersMinor printer cleanup for SMT-LIBv2 symbols "div" and... commit | commitdiff | tree
2013-06-26 Andrew ReynoldsAdd support for interval models in bounded integers... commit | commitdiff | tree
2013-06-25 Morgan DetersMerge branch '1.2.x' commit | commitdiff | tree
2013-06-25 Morgan DetersProposed fix for bug #513 commit | commitdiff | tree
2013-06-25 Andrew ReynoldsRefactoring of model engine to separate individual... commit | commitdiff | tree
2013-06-25 Morgan DetersAdd files missing from last commit commit | commitdiff | tree
2013-06-25 Morgan DetersSupport for abs, to_int, is_int, divisible in SMT-LIB... commit | commitdiff | tree
2013-06-24 Andrew ReynoldsAdd options for symmetry breaking in uf+ss totality... commit | commitdiff | tree
2013-06-21 Morgan DetersFix failure in non-assertion builds on incorrect SmtEng... commit | commitdiff | tree
2013-06-19 Morgan DetersMerge branch '1.2.x' commit | commitdiff | tree
2013-06-19 Morgan DetersWorkaround for suspected clang 3.0 codegen bug on Mac commit | commitdiff | tree
2013-06-19 Morgan DetersFix to the "include" extended feature of the SMT-LIB... commit | commitdiff | tree
2013-06-19 Morgan DetersGive a more useful parse error message for "undeclared... commit | commitdiff | tree
2013-06-17 Morgan DetersJava streams example I forgot to add a long time ago commit | commitdiff | tree
2013-06-17 Andrew ReynoldsMake --var-elim-quant true by default. Add rewrite... commit | commitdiff | tree
2013-06-16 Andrew ReynoldsFix in SMT2 parser for parametric datatypes commit | commitdiff | tree
2013-06-10 Morgan Detersanother fix for array-store-all printing commit | commitdiff | tree
2013-06-10 Morgan DetersBetter array-store-all output for SMT-LIB. commit | commitdiff | tree
2013-06-08 Morgan DetersFix typos in alttheoryskel commit | commitdiff | tree
2013-06-08 Morgan DetersFixes for Boolean terms in arrays (including fix for... commit | commitdiff | tree
2013-06-07 Morgan DetersOne more case for arrays of Boolean. commit | commitdiff | tree
2013-06-07 Morgan DetersFix for bug 517. commit | commitdiff | tree
2013-06-07 Morgan DetersAllow 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 ReynoldsFix bug in --fmf-fmc for producing models of functions... commit | commitdiff | tree
2013-06-04 Morgan DetersFile inclusion in Smt2 parser. commit | commitdiff | tree
2013-06-04 Morgan DetersAdd --no-condense-function-values option for explicit... commit | commitdiff | tree
2013-06-04 Morgan DetersMerge branch '1.2.x' commit | commitdiff | tree
2013-06-04 Morgan DetersFix clang static initialization order issue; fixes... commit | commitdiff | tree
2013-06-04 Andrew ReynoldsAdd partial support for MBQI with arrays when using... commit | commitdiff | tree
next