projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2013-05-23 Andrew ReynoldsRefactoring to prepare for MBQI with integer quantifica... commit | commitdiff | tree
2013-05-22 Andrew ReynoldsMerge branch 'master' of https://github.com/CVC4/CVC4 commit | commitdiff | tree
2013-05-22 Andrew ReynoldsSignificant work on bounded integer quantification... commit | commitdiff | tree
2013-05-22 Andrew ReynoldsAdd regressions for finite model finding commit | commitdiff | tree
2013-05-21 Morgan DetersMerge branch '1.2.x' commit | commitdiff | tree
2013-05-21 Morgan DetersFix bug 512: an assertion failure only appearing with... commit | commitdiff | tree
2013-05-21 Morgan DetersFix an error that valgrind found. commit | commitdiff | tree
2013-05-21 Morgan DetersMerge branch '1.2.x' commit | commitdiff | tree
2013-05-21 Morgan DetersFix incremental bug in symmetry breaker. commit | commitdiff | tree
2013-05-20 Morgan DetersMerge branch '1.2.x' commit | commitdiff | tree
2013-05-20 Morgan DetersFix error reporting on use of (nonlinear) div,mod,... commit | commitdiff | tree
2013-05-20 Morgan DetersUpdate THANKS to mention David Cok's contributions. commit | commitdiff | tree
2013-05-20 Morgan DetersDetect multiply-defined :named annotations and issue... commit | commitdiff | tree
2013-05-20 Morgan DetersFix parsing of SMT-LIBv2 |quoted| symbols that span... commit | commitdiff | tree
2013-05-20 Morgan DetersCompliance fixes for :named annotations: they must... commit | commitdiff | tree
2013-05-20 Morgan DetersDon't allow get-model & co after a user push/pop commit | commitdiff | tree
2013-05-20 Morgan DetersAs per SMT-LIB standard: make - and xor take n>2 args... commit | commitdiff | tree
2013-05-20 Morgan DetersFix for equality-chaining of Booleans in SMT-LIBv2. commit | commitdiff | tree
2013-05-20 Morgan DetersFix destruction issue in GetValueCommand leading to... commit | commitdiff | tree
2013-05-20 Morgan DetersBetter error on invalid logic strings. commit | commitdiff | tree
2013-05-20 Morgan DetersBetter error on illegal (pop N); also more compliant... commit | commitdiff | tree
2013-05-20 Morgan DetersA couple of fixes to the get-option command for complia... commit | commitdiff | tree
2013-05-20 Morgan DetersDisallow construction of (_ BitVec 0). commit | commitdiff | tree
2013-05-20 Morgan DetersFixed "success" response to (push N) / (pop N) with... commit | commitdiff | tree
2013-05-20 Morgan DetersFix to empty response to (get-assignment). commit | commitdiff | tree
2013-05-20 Morgan Detersconfigure fix for building with glpk on redhat, perhaps... commit | commitdiff | tree
2013-05-20 Morgan Detersminor changes to language bindings commit | commitdiff | tree
2013-05-20 Morgan Detersdisable Logic-checking with finite model finding for... commit | commitdiff | tree
2013-05-20 Morgan DetersFix erroneous results when the logic was incorrectly... commit | commitdiff | tree
2013-05-20 Andrew ReynoldsPossible final version of run scripts for casc. commit | commitdiff | tree
2013-05-17 Andrew ReynoldsAdd model-producing run script for casc. commit | commitdiff | tree
2013-05-17 Andrew ReynoldsAdd support for --dump-models option, in preparation... commit | commitdiff | tree
2013-05-17 Morgan DetersAs per SMT-LIB standard: make - and xor take n>2 args... commit | commitdiff | tree
2013-05-17 Morgan DetersFix for equality-chaining of Booleans in SMT-LIBv2. commit | commitdiff | tree
2013-05-17 Morgan DetersFix destruction issue in GetValueCommand leading to... commit | commitdiff | tree
2013-05-17 Morgan DetersBetter error on invalid logic strings. commit | commitdiff | tree
2013-05-17 Morgan DetersBetter error on illegal (pop N); also more compliant... commit | commitdiff | tree
2013-05-17 Morgan DetersA couple of fixes to the get-option command for complia... commit | commitdiff | tree
2013-05-17 Morgan DetersDisallow construction of (_ BitVec 0). commit | commitdiff | tree
2013-05-17 Morgan DetersFixed "success" response to (push N) / (pop N) with... commit | commitdiff | tree
2013-05-17 Morgan DetersFix to empty response to (get-assignment). commit | commitdiff | tree
2013-05-16 Morgan Detersconfigure fix for building with glpk on redhat, perhaps... commit | commitdiff | tree
2013-05-16 Andrew ReynoldsFix minor bug in full_model_check.cpp commit | commitdiff | tree
2013-05-16 Morgan Detersminor changes to language bindings commit | commitdiff | tree
2013-05-14 Andrew ReynoldsUpdate casc24-fnt run script. Add casc24-fof run script. commit | commitdiff | tree
2013-05-14 lianahadded some extra options to the bit-vector theory commit | commitdiff | tree
2013-05-14 Andrew ReynoldsAdd support for quantifier patterns in smt2 printer. commit | commitdiff | tree
2013-05-14 Andrew ReynoldsRefactoring to separate old and new model building... commit | commitdiff | tree
2013-05-11 Andrew ReynoldsPreliminary version of finite model finding over bounde... commit | commitdiff | tree
2013-05-10 Morgan Detersdisable Logic-checking with finite model finding for... commit | commitdiff | tree
2013-05-10 lianahnow proofs print mapping between atom and propositional... commit | commitdiff | tree
2013-05-10 Andrew ReynoldsUpdate casc run script. Work on compliance for SZS... commit | commitdiff | tree
2013-05-10 lianahfixes to the proof system so it works with theory lemma... commit | commitdiff | tree
2013-05-10 Morgan DetersFix erroneous results when the logic was incorrectly... commit | commitdiff | tree
2013-05-10 Morgan DetersAdd documentation for --disable-fmf-inst-gen, which... commit | commitdiff | tree
2013-05-10 Andrew ReynoldsAdd simplification option --fo-prop-quant. Add model... commit | commitdiff | tree
2013-05-09 Kshitij BansalMerge branch 'master' of ssh://github.com/CVC4/CVC4 commit | commitdiff | tree
2013-05-09 Tim KingChanging the integer normal form to increase matching. commit | commitdiff | tree
2013-05-09 Andrew ReynoldsAdd new method for checking candidate models, --fmf... commit | commitdiff | tree
2013-05-08 Kshitij Bansalrm decision/relevancy commit | commitdiff | tree
2013-05-08 Morgan DetersPrerelease versioning for 1.2.x commit | commitdiff | tree
2013-05-08 Morgan DetersPrerelease versioning for master commit | commitdiff | tree
2013-05-08 Morgan DetersMerge tag 'smteval2013' commit | commitdiff | tree
2013-05-08 Morgan DetersCutting release 1.2. commit | commitdiff | tree
2013-05-08 Morgan DetersRemoving arithmetic compile warning for release commit | commitdiff | tree
2013-05-08 Morgan Detersupdate versioning commit | commitdiff | tree
2013-05-08 Morgan Detersfinal updates for smt-eval script commit | commitdiff | tree
2013-05-08 Clark BarrettFixed assertion bug commit | commitdiff | tree
2013-05-08 Morgan Detersfix for smt-eval run script commit | commitdiff | tree
2013-05-07 Morgan DetersBV strategy for SMT-EVAL commit | commitdiff | tree
2013-05-07 Morgan Detersfix for nonterminating model-based array loop commit | commitdiff | tree
2013-05-07 lianahadded type checking rule to check for bit-vector consta... commit | commitdiff | tree
2013-05-07 lianahone more fix for rewrites commit | commitdiff | tree
2013-05-07 lianahfixed bv rewrite blow-up commit | commitdiff | tree
2013-05-07 Dejan Jovanovićfix for bug500 commit | commitdiff | tree
2013-05-07 Tim KingFixes a bug with arithmetic's new attempt solution... commit | commitdiff | tree
2013-05-07 Tim KingImproving arithmetic debugging output. commit | commitdiff | tree
2013-05-07 Tim KingDisabling an incorrect prototyping line from the simple... commit | commitdiff | tree
2013-05-07 Morgan DetersChange SMT-EVAL run-script to use Tim's best QF_LRA... commit | commitdiff | tree
2013-05-07 Liana Hadareanfixed bv rewrite rule bug commit | commitdiff | tree
2013-05-06 Morgan DetersRemoving excess verbosity from ApproxSimplex (after... commit | commitdiff | tree
2013-05-06 Tim KingAdding a heuristic for guessing an optimization functio... commit | commitdiff | tree
2013-05-06 Tim KingDisables justification stop only for LRA if the problem... commit | commitdiff | tree
2013-05-06 Clark BarrettSome bug fixes for mb arrays commit | commitdiff | tree
2013-05-05 Tim KingAdding cut offs for likely integer infeasible paths. commit | commitdiff | tree
2013-05-04 Tim KingAdding a smarter technique for pivoting in solutions... commit | commitdiff | tree
2013-05-03 Tim KingFixing compilation of unit tests. These problems were... commit | commitdiff | tree
2013-05-03 Tim KingMore misc. arithmetic cleanup. Removing unused files... commit | commitdiff | tree
2013-05-03 Tim KingCode cleanup. Reducing misc. warnings in arithmetic. commit | commitdiff | tree
2013-05-03 Tim KingRemoving arithmetic legacy code and unifying functions. commit | commitdiff | tree
2013-05-03 Tim KingFixing a debug typo. commit | commitdiff | tree
2013-05-03 Tim KingMerging branch 'soiquickexplain'. commit | commitdiff | tree
2013-05-03 Tim KingMerge branch 'fcexplanations' commit | commitdiff | tree
2013-05-02 Tim KingAdding quick explain for soi simplex. commit | commitdiff | tree
2013-05-02 Dejan Jovanović* splitLemma to request atoms commit | commitdiff | tree
2013-05-02 lianahmerged master commit | commitdiff | tree
2013-05-02 lianahMerge branch 'master' of https://github.com/CVC4/CVC4 commit | commitdiff | tree
2013-05-01 Morgan DetersComment out some debug-related things in attribute... commit | commitdiff | tree
2013-05-01 Morgan DetersFix to dumping re: boolean terms, datatypes commit | commitdiff | tree
2013-05-01 Morgan DetersFix to boolean-terms; resolves bug #507 commit | commitdiff | tree
next