projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2013-05-21
Morgan Deters
Merge branch '1.2.x'
commit
|
commitdiff
|
tree
2013-05-21
Morgan Deters
Fix bug 512: an assertion failure only appearing with...
commit
|
commitdiff
|
tree
2013-05-21
Morgan Deters
Fix an error that valgrind found.
commit
|
commitdiff
|
tree
2013-05-21
Morgan Deters
Merge branch '1.2.x'
commit
|
commitdiff
|
tree
2013-05-21
Morgan Deters
Fix incremental bug in symmetry breaker.
commit
|
commitdiff
|
tree
2013-05-20
Morgan Deters
Merge branch '1.2.x'
commit
|
commitdiff
|
tree
2013-05-20
Morgan Deters
Fix error reporting on use of (nonlinear) div,mod,...
commit
|
commitdiff
|
tree
2013-05-20
Morgan Deters
Update THANKS to mention David Cok's contributions.
commit
|
commitdiff
|
tree
2013-05-20
Morgan Deters
Detect multiply-defined :named annotations and issue...
commit
|
commitdiff
|
tree
2013-05-20
Morgan Deters
Fix parsing of SMT-LIBv2 |quoted| symbols that span...
commit
|
commitdiff
|
tree
2013-05-20
Morgan Deters
Compliance fixes for :named annotations: they must...
commit
|
commitdiff
|
tree
2013-05-20
Morgan Deters
Don't allow get-model & co after a user push/pop
commit
|
commitdiff
|
tree
2013-05-20
Morgan Deters
As per SMT-LIB standard: make - and xor take n>2 args...
commit
|
commitdiff
|
tree
2013-05-20
Morgan Deters
Fix for equality-chaining of Booleans in SMT-LIBv2.
commit
|
commitdiff
|
tree
2013-05-20
Morgan Deters
Fix destruction issue in GetValueCommand leading to...
commit
|
commitdiff
|
tree
2013-05-20
Morgan Deters
Better error on invalid logic strings.
commit
|
commitdiff
|
tree
2013-05-20
Morgan Deters
Better error on illegal (pop N); also more compliant...
commit
|
commitdiff
|
tree
2013-05-20
Morgan Deters
A couple of fixes to the get-option command for complia...
commit
|
commitdiff
|
tree
2013-05-20
Morgan Deters
Disallow construction of (_ BitVec 0).
commit
|
commitdiff
|
tree
2013-05-20
Morgan Deters
Fixed "success" response to (push N) / (pop N) with...
commit
|
commitdiff
|
tree
2013-05-20
Morgan Deters
Fix to empty response to (get-assignment).
commit
|
commitdiff
|
tree
2013-05-20
Morgan Deters
configure fix for building with glpk on redhat, perhaps...
commit
|
commitdiff
|
tree
2013-05-20
Morgan Deters
minor changes to language bindings
commit
|
commitdiff
|
tree
2013-05-20
Morgan Deters
disable Logic-checking with finite model finding for...
commit
|
commitdiff
|
tree
2013-05-20
Morgan Deters
Fix erroneous results when the logic was incorrectly...
commit
|
commitdiff
|
tree
2013-05-20
Andrew Reynolds
Possible final version of run scripts for casc.
commit
|
commitdiff
|
tree
2013-05-17
Andrew Reynolds
Add model-producing run script for casc.
commit
|
commitdiff
|
tree
2013-05-17
Andrew Reynolds
Add support for --dump-models option, in preparation...
commit
|
commitdiff
|
tree
2013-05-17
Morgan Deters
As per SMT-LIB standard: make - and xor take n>2 args...
commit
|
commitdiff
|
tree
2013-05-17
Morgan Deters
Fix for equality-chaining of Booleans in SMT-LIBv2.
commit
|
commitdiff
|
tree
2013-05-17
Morgan Deters
Fix destruction issue in GetValueCommand leading to...
commit
|
commitdiff
|
tree
2013-05-17
Morgan Deters
Better error on invalid logic strings.
commit
|
commitdiff
|
tree
2013-05-17
Morgan Deters
Better error on illegal (pop N); also more compliant...
commit
|
commitdiff
|
tree
2013-05-17
Morgan Deters
A couple of fixes to the get-option command for complia...
commit
|
commitdiff
|
tree
2013-05-17
Morgan Deters
Disallow construction of (_ BitVec 0).
commit
|
commitdiff
|
tree
2013-05-17
Morgan Deters
Fixed "success" response to (push N) / (pop N) with...
commit
|
commitdiff
|
tree
2013-05-17
Morgan Deters
Fix to empty response to (get-assignment).
commit
|
commitdiff
|
tree
2013-05-16
Morgan Deters
configure fix for building with glpk on redhat, perhaps...
commit
|
commitdiff
|
tree
2013-05-16
Andrew Reynolds
Fix minor bug in full_model_check.cpp
commit
|
commitdiff
|
tree
2013-05-16
Morgan Deters
minor changes to language bindings
commit
|
commitdiff
|
tree
2013-05-14
Andrew Reynolds
Update casc24-fnt run script. Add casc24-fof run script.
commit
|
commitdiff
|
tree
2013-05-14
lianah
added some extra options to the bit-vector theory
commit
|
commitdiff
|
tree
2013-05-14
Andrew Reynolds
Add support for quantifier patterns in smt2 printer.
commit
|
commitdiff
|
tree
2013-05-14
Andrew Reynolds
Refactoring to separate old and new model building...
commit
|
commitdiff
|
tree
2013-05-11
Andrew Reynolds
Preliminary version of finite model finding over bounde...
commit
|
commitdiff
|
tree
2013-05-10
Morgan Deters
disable Logic-checking with finite model finding for...
commit
|
commitdiff
|
tree
2013-05-10
lianah
now proofs print mapping between atom and propositional...
commit
|
commitdiff
|
tree
2013-05-10
Andrew Reynolds
Update casc run script. Work on compliance for SZS...
commit
|
commitdiff
|
tree
2013-05-10
lianah
fixes to the proof system so it works with theory lemma...
commit
|
commitdiff
|
tree
2013-05-10
Morgan Deters
Fix erroneous results when the logic was incorrectly...
commit
|
commitdiff
|
tree
2013-05-10
Morgan Deters
Add documentation for --disable-fmf-inst-gen, which...
commit
|
commitdiff
|
tree
2013-05-10
Andrew Reynolds
Add simplification option --fo-prop-quant. Add model...
commit
|
commitdiff
|
tree
2013-05-09
Kshitij Bansal
Merge branch 'master' of ssh://github.com/CVC4/CVC4
commit
|
commitdiff
|
tree
2013-05-09
Tim King
Changing the integer normal form to increase matching.
commit
|
commitdiff
|
tree
2013-05-09
Andrew Reynolds
Add new method for checking candidate models, --fmf...
commit
|
commitdiff
|
tree
2013-05-08
Kshitij Bansal
rm decision/relevancy
commit
|
commitdiff
|
tree
2013-05-08
Morgan Deters
Prerelease versioning for 1.2.x
commit
|
commitdiff
|
tree
2013-05-08
Morgan Deters
Prerelease versioning for master
commit
|
commitdiff
|
tree
2013-05-08
Morgan Deters
Merge tag 'smteval2013'
commit
|
commitdiff
|
tree
2013-05-08
Morgan Deters
Cutting release 1.2.
commit
|
commitdiff
|
tree
2013-05-08
Morgan Deters
Removing arithmetic compile warning for release
commit
|
commitdiff
|
tree
2013-05-08
Morgan Deters
update versioning
commit
|
commitdiff
|
tree
2013-05-08
Morgan Deters
final updates for smt-eval script
commit
|
commitdiff
|
tree
2013-05-08
Clark Barrett
Fixed assertion bug
commit
|
commitdiff
|
tree
2013-05-08
Morgan Deters
fix for smt-eval run script
commit
|
commitdiff
|
tree
2013-05-07
Morgan Deters
BV strategy for SMT-EVAL
commit
|
commitdiff
|
tree
2013-05-07
Morgan Deters
fix for nonterminating model-based array loop
commit
|
commitdiff
|
tree
2013-05-07
lianah
added type checking rule to check for bit-vector consta...
commit
|
commitdiff
|
tree
2013-05-07
lianah
one more fix for rewrites
commit
|
commitdiff
|
tree
2013-05-07
lianah
fixed bv rewrite blow-up
commit
|
commitdiff
|
tree
2013-05-07
Dejan Jovanović
fix for bug500
commit
|
commitdiff
|
tree
2013-05-07
Tim King
Fixes a bug with arithmetic's new attempt solution...
commit
|
commitdiff
|
tree
2013-05-07
Tim King
Improving arithmetic debugging output.
commit
|
commitdiff
|
tree
2013-05-07
Tim King
Disabling an incorrect prototyping line from the simple...
commit
|
commitdiff
|
tree
2013-05-07
Morgan Deters
Change SMT-EVAL run-script to use Tim's best QF_LRA...
commit
|
commitdiff
|
tree
2013-05-07
Liana Hadarean
fixed bv rewrite rule bug
commit
|
commitdiff
|
tree
2013-05-06
Morgan Deters
Removing excess verbosity from ApproxSimplex (after...
commit
|
commitdiff
|
tree
2013-05-06
Tim King
Adding a heuristic for guessing an optimization functio...
commit
|
commitdiff
|
tree
2013-05-06
Tim King
Disables justification stop only for LRA if the problem...
commit
|
commitdiff
|
tree
2013-05-06
Clark Barrett
Some bug fixes for mb arrays
commit
|
commitdiff
|
tree
2013-05-05
Tim King
Adding cut offs for likely integer infeasible paths.
commit
|
commitdiff
|
tree
2013-05-04
Tim King
Adding a smarter technique for pivoting in solutions...
commit
|
commitdiff
|
tree
2013-05-03
Tim King
Fixing compilation of unit tests. These problems were...
commit
|
commitdiff
|
tree
2013-05-03
Tim King
More misc. arithmetic cleanup. Removing unused files...
commit
|
commitdiff
|
tree
2013-05-03
Tim King
Code cleanup. Reducing misc. warnings in arithmetic.
commit
|
commitdiff
|
tree
2013-05-03
Tim King
Removing arithmetic legacy code and unifying functions.
commit
|
commitdiff
|
tree
2013-05-03
Tim King
Fixing a debug typo.
commit
|
commitdiff
|
tree
2013-05-03
Tim King
Merging branch 'soiquickexplain'.
commit
|
commitdiff
|
tree
2013-05-03
Tim King
Merge branch 'fcexplanations'
commit
|
commitdiff
|
tree
2013-05-02
Tim King
Adding quick explain for soi simplex.
commit
|
commitdiff
|
tree
2013-05-02
Dejan Jovanović
* splitLemma to request atoms
commit
|
commitdiff
|
tree
2013-05-02
lianah
merged master
commit
|
commitdiff
|
tree
2013-05-02
lianah
Merge branch 'master' of https://github.com/CVC4/CVC4
commit
|
commitdiff
|
tree
2013-05-01
Morgan Deters
Comment out some debug-related things in attribute...
commit
|
commitdiff
|
tree
2013-05-01
Morgan Deters
Fix to dumping re: boolean terms, datatypes
commit
|
commitdiff
|
tree
2013-05-01
Morgan Deters
Fix to boolean-terms; resolves bug #507
commit
|
commitdiff
|
tree
2013-05-01
lianah
removed tracing code causing slowdown; cleaned up some...
commit
|
commitdiff
|
tree
2013-05-01
Tim King
Working on the new explanation system.
commit
|
commitdiff
|
tree
2013-05-01
lianah
added back BitwiseEq rule
commit
|
commitdiff
|
tree
2013-05-01
Morgan Deters
Adding a missing makefile to the dist (fixes distcheck)
commit
|
commitdiff
|
tree
next