cvc5.git
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
2013-06-10 Morgan DetersBetter array-store-all output for SMT-LIB.
2013-06-08 Morgan DetersFix typos in alttheoryskel
2013-06-08 Morgan DetersFixes for Boolean terms in arrays (including fix for...
2013-06-07 Morgan DetersOne more case for arrays of Boolean.
2013-06-07 Morgan DetersFix for bug 517.
2013-06-07 Morgan DetersAllow disabling include-file feature
2013-06-07 Dejan Jovanovićsmall parese issue in IDL
2013-06-06 Dejan Jovanovićtypo
2013-06-06 Dejan JovanovićIDL example theory (to be used with --use-theory=idl).
2013-06-05 Andrew ReynoldsFix bug in --fmf-fmc for producing models of functions...
2013-06-04 Morgan DetersFile inclusion in Smt2 parser.
2013-06-04 Morgan DetersAdd --no-condense-function-values option for explicit...
2013-06-04 Morgan DetersMerge branch '1.2.x'
2013-06-04 Morgan DetersFix clang static initialization order issue; fixes...
2013-06-04 Andrew ReynoldsAdd partial support for MBQI with arrays when using...
2013-06-03 Morgan DetersMerge tag 'casc24'
2013-06-03 Morgan DetersUpdated CASC scripts, as provided to Geoff Sutcliffe
2013-05-29 Morgan DetersMerge branch '1.2.x'
2013-05-29 Morgan DetersPer SMT-LIB spec, allow (set-info..) command to succeed...
2013-05-29 Morgan DetersSMT-LIB printer updates (some missing cases).
2013-05-29 Morgan DetersFix bug where strict mode didn't allow DIV or MOD,...
2013-05-28 Morgan DetersStandardize SMT-LIBv2 set of logics to use LogicInfo.
2013-05-23 Andrew ReynoldsRefactoring to prepare for MBQI with integer quantifica...
2013-05-22 Andrew ReynoldsMerge branch 'master' of https://github.com/CVC4/CVC4
2013-05-22 Andrew ReynoldsSignificant work on bounded integer quantification...
2013-05-22 Andrew ReynoldsAdd regressions for finite model finding
2013-05-21 Morgan DetersMerge branch '1.2.x'
2013-05-21 Morgan DetersFix bug 512: an assertion failure only appearing with...
2013-05-21 Morgan DetersFix an error that valgrind found.
2013-05-21 Morgan DetersMerge branch '1.2.x'
2013-05-21 Morgan DetersFix incremental bug in symmetry breaker.
2013-05-20 Morgan DetersMerge branch '1.2.x'
2013-05-20 Morgan DetersFix error reporting on use of (nonlinear) div,mod,...
2013-05-20 Morgan DetersUpdate THANKS to mention David Cok's contributions.
2013-05-20 Morgan DetersDetect multiply-defined :named annotations and issue...
2013-05-20 Morgan DetersFix parsing of SMT-LIBv2 |quoted| symbols that span...
2013-05-20 Morgan DetersCompliance fixes for :named annotations: they must...
2013-05-20 Morgan DetersDon't allow get-model & co after a user push/pop
2013-05-20 Morgan DetersAs per SMT-LIB standard: make - and xor take n>2 args...
2013-05-20 Morgan DetersFix for equality-chaining of Booleans in SMT-LIBv2.
2013-05-20 Morgan DetersFix destruction issue in GetValueCommand leading to...
2013-05-20 Morgan DetersBetter error on invalid logic strings.
2013-05-20 Morgan DetersBetter error on illegal (pop N); also more compliant...
2013-05-20 Morgan DetersA couple of fixes to the get-option command for complia...
2013-05-20 Morgan DetersDisallow construction of (_ BitVec 0).
2013-05-20 Morgan DetersFixed "success" response to (push N) / (pop N) with...
2013-05-20 Morgan DetersFix to empty response to (get-assignment).
2013-05-20 Morgan Detersconfigure fix for building with glpk on redhat, perhaps...
2013-05-20 Morgan Detersminor changes to language bindings
2013-05-20 Morgan Detersdisable Logic-checking with finite model finding for...
2013-05-20 Morgan DetersFix erroneous results when the logic was incorrectly...
2013-05-20 Andrew ReynoldsPossible final version of run scripts for casc.
2013-05-17 Andrew ReynoldsAdd model-producing run script for casc.
2013-05-17 Andrew ReynoldsAdd support for --dump-models option, in preparation...
2013-05-17 Morgan DetersAs per SMT-LIB standard: make - and xor take n>2 args...
2013-05-17 Morgan DetersFix for equality-chaining of Booleans in SMT-LIBv2.
2013-05-17 Morgan DetersFix destruction issue in GetValueCommand leading to...
2013-05-17 Morgan DetersBetter error on invalid logic strings.
2013-05-17 Morgan DetersBetter error on illegal (pop N); also more compliant...
2013-05-17 Morgan DetersA couple of fixes to the get-option command for complia...
2013-05-17 Morgan DetersDisallow construction of (_ BitVec 0).
2013-05-17 Morgan DetersFixed "success" response to (push N) / (pop N) with...
2013-05-17 Morgan DetersFix to empty response to (get-assignment).
2013-05-16 Morgan Detersconfigure fix for building with glpk on redhat, perhaps...
2013-05-16 Andrew ReynoldsFix minor bug in full_model_check.cpp
2013-05-16 Morgan Detersminor changes to language bindings
2013-05-14 Andrew ReynoldsUpdate casc24-fnt run script. Add casc24-fof run script.
2013-05-14 lianahadded some extra options to the bit-vector theory
2013-05-14 Andrew ReynoldsAdd support for quantifier patterns in smt2 printer.
2013-05-14 Andrew ReynoldsRefactoring to separate old and new model building...
next