cvc5.git
2013-09-24 Tianyi Liangadds model generation for strings, and a hacked way...
2013-09-23 Morgan DetersRevert Clark's last commit, at his request; there are...
2013-09-23 Clark BarrettCleaner version of bug-fix for 528, also moved substitu...
2013-09-19 Clark BarrettFix for bug 528
2013-09-18 Morgan DetersSupport a personal build configuration and make rules.
2013-09-18 Morgan DetersSupport for bv2nat/int2bv in parser and BV rewriter.
2013-09-18 Morgan DetersFixes to theoryof-mode; no longer static in Theory...
2013-09-16 Morgan DetersFix (extraneous) command dumping.
2013-09-15 Andrew ReynoldsChange default option of simple ite lifting within...
2013-09-13 Morgan DetersFix sat_proof "parentheses into the void" after conferr...
2013-09-13 Morgan DetersMove some regress benchmarks around that took too long...
2013-09-13 Morgan DetersDocumentation fixes, some code typo fixes, file perms...
2013-09-13 Kshitij BansalMerge branch 'master' of https://github.com/CVC4/CVC4
2013-09-12 Kshitij Bansalfix bug 534: portfolio define-fun duplicate model
2013-09-11 Tianyi LiangTheory of strings.
2013-09-09 Andrew ReynoldsAnother minor fix for datatypes to repair my previous...
2013-09-09 Morgan DetersAdd support for check-sat with argument.
2013-09-09 Morgan DetersFix declare-datatypes dumping bug (bug 385).
2013-09-09 Morgan DetersSupport per-command verbosity settings.
2013-09-09 Morgan DetersSupport empty (and 1-ary) tuples and records.
2013-09-09 Morgan DetersFix some line-numbering in auto-generated metakind...
2013-09-09 Morgan DetersFix portfolio on bug411.smt2. (get-model command shoul...
2013-09-09 Morgan DetersEnsure no cost for datatypes debugging when not tracing it.
2013-09-07 Andrew ReynoldsFix datatypes for bug 503
2013-09-05 Morgan DetersFix FLOOR and DISTINCT in CVC language parser.
2013-09-05 Morgan DetersFix lambda handling in CVC parser
2013-09-05 Morgan DetersPermit setOption(decision-mode)
2013-09-05 Morgan DetersFix bugs/issues with missed-t-prop dump output
2013-09-05 Morgan DetersFix declare-fun/define-fun in dumps; resolves bugs...
2013-08-31 Morgan DetersAdd ability to mkConst(TupleSelect) and friends in...
2013-08-26 Kshitij BansalMerge branch '1.2.x'
2013-08-26 Kshitij Bansalbug 374 fix: assert litVal=desiredVal only for leaf...
2013-08-26 Kshitij BansalBug 374 benchmarks
2013-08-20 Morgan DetersChange recursive expandDefinitions() to an interative...
2013-08-13 Morgan Deters--segv-nospin is now default.
2013-08-13 Morgan DetersMinor cleanup.
2013-08-13 Andrew ReynoldsMinor fixes for --fmf-fmc for quantifiers containing...
2013-08-13 Andrew Reynoldsinitial modifications for per-ic cbqi
2013-08-09 Morgan DetersClean up "make install"-produced intermediate files...
2013-08-08 Morgan DetersFix a serious bug in the preprocessor; problem inputs...
2013-08-08 Morgan DetersParameterized, uninterpreted sorts need no Boolean...
2013-07-30 Morgan DetersMinor fixes to build system.
2013-07-29 Morgan DetersFix numerous compiler warnings on various platforms
2013-07-24 Morgan DetersRegressions now checking models on unknown too. But...
2013-07-24 Morgan DetersFixes for building with mingw win64.
2013-07-24 Morgan DetersDon't allow --stats if not a statistics-enabled build
2013-07-24 Morgan Deterssome portfolio driver cleanup
2013-07-24 Morgan DetersSome fixes for (get-info :all-options)
2013-07-23 Morgan Detersfix for win32 option parsing via mingw32
2013-07-23 Morgan Deters(get-info :all-options) to get option values; also...
2013-07-22 Morgan DetersAllow BV and DT in either order in the logic string
2013-07-22 Andrew ReynoldsAdd option --cbqi-recurse.
2013-07-22 Andrew ReynoldsBug fix for --fmf-fmc for non-uninterpreted sort quanti...
2013-07-20 Morgan Detersenable bug521 regression tests
2013-07-19 Dejan Jovanovicpossible fix for bug 521
2013-07-19 Morgan DetersMinor fix for --no-condense-function-values
2013-07-18 Andrew ReynoldsFix quantifier instantiation bug in cbqi, add default...
2013-07-17 Morgan DetersFix bug 516; include some bug testcases.
2013-07-16 Liana Hadareanfixed seg fault when bv equality is turned off
2013-07-16 Liana Hadareanfixed bug520
2013-07-16 Morgan DetersFix for get-antlr script and PIC/non-PIC objects, on...
2013-07-16 Morgan Deters"Tabular"-style function definitions in models with...
2013-07-16 Morgan DetersMinor bugfixes to model-building
2013-07-13 Morgan DetersRemove now-unused language bindings interface file.
2013-07-13 Morgan DetersFix language bindings and portfolio builds.
2013-07-12 Morgan DetersFix for curious GCC 4.8 translation with -O.
2013-07-11 Morgan DetersRemove auto-aritization from TPTP parser
2013-07-11 Morgan DetersSupport for TPTP's TFF0 (with arithmetic)
2013-07-11 Morgan DetersFix for Boolean-term rewriting and LAMBDAs
2013-07-10 Morgan DetersFix for bug 519; don't involve ITESimplifier in model...
2013-07-09 Andrew Reynoldsadd relevant domain computation
2013-07-07 Morgan DetersModel output is now const; this related to bug 519
2013-07-05 Morgan DetersFix for a datatype parsing bug that Tim found.
2013-07-02 Andrew ReynoldsMake uf strong solver user-context dependent, fixes...
2013-07-02 Andrew ReynoldsMinor fixes for bounded integers, rewrite engine.
2013-06-28 Andrew ReynoldsMore bug fixes for interval models.
2013-06-28 Morgan DetersFix portfolio builds after yesterday's commits.
2013-06-27 Morgan DetersBetter check-models output for some kinds of problems...
2013-06-27 Morgan DetersFix minor warnings found by recent clang/gcc.
2013-06-27 Morgan DetersRemove output.h from public space, to avoid clashes...
2013-06-27 Morgan DetersSmall fix for IS_INTEGER.
2013-06-27 Morgan DetersRemove macros EXPECT_TRUE / EXPECT_FALSE from cvc4_publ...
2013-06-27 Morgan DetersBetter user documentation for mkVar() and mkBoundVar().
2013-06-27 Morgan DetersMinor printer cleanup for SMT-LIBv2 symbols "div" and...
2013-06-26 Andrew ReynoldsAdd support for interval models in bounded integers...
2013-06-25 Morgan DetersMerge branch '1.2.x'
2013-06-25 Morgan DetersProposed fix for bug #513
2013-06-25 Andrew ReynoldsRefactoring of model engine to separate individual...
2013-06-25 Morgan DetersAdd files missing from last commit
2013-06-25 Morgan DetersSupport for abs, to_int, is_int, divisible in SMT-LIB...
2013-06-24 Andrew ReynoldsAdd options for symmetry breaking in uf+ss totality...
2013-06-21 Morgan DetersFix failure in non-assertion builds on incorrect SmtEng...
2013-06-19 Morgan DetersMerge branch '1.2.x'
2013-06-19 Morgan DetersWorkaround for suspected clang 3.0 codegen bug on Mac
2013-06-19 Morgan DetersFix to the "include" extended feature of the SMT-LIB...
2013-06-19 Morgan DetersGive a more useful parse error message for "undeclared...
2013-06-17 Morgan DetersJava streams example I forgot to add a long time ago
2013-06-17 Andrew ReynoldsMake --var-elim-quant true by default. Add rewrite...
2013-06-16 Andrew ReynoldsFix in SMT2 parser for parametric datatypes
2013-06-10 Morgan Detersanother fix for array-store-all printing
next