| 2018-05-08 |
Aina Niemetz | Fix order of preprocessing pass registration. (#1887)
|
commit | commitdiff | tree |
| 2018-04-11 |
Aina Niemetz | Refactored BVGauss preprocessing pass. (#1766)
|
commit | commitdiff | tree |
| 2018-04-10 |
Aina Niemetz | Fix dumping of benchmark in SmtEngine::checkSatisfiability...
|
commit | commitdiff | tree |
| 2018-04-07 |
Aina Niemetz | Fixed get-authors.
|
commit | commitdiff | tree |
| 2018-03-21 |
Aina Niemetz | Add bit-vector extract example. (#1681)
|
commit | commitdiff | tree |
| 2018-03-20 |
Aina Niemetz | Add parameterized datatypes example. (#1676)
|
commit | commitdiff | tree |
| 2018-03-13 |
Aina Niemetz | SmtEngine::getModel() is now public. (#1665)
|
commit | commitdiff | tree |
| 2018-03-09 |
Aina Niemetz | Printers are now managed as unique_ptr (fix mem leak...
|
commit | commitdiff | tree |
| 2018-03-09 |
Aina Niemetz | Some minor cleanup in bv::utils. (#1663)
|
commit | commitdiff | tree |
| 2018-03-09 |
Aina Niemetz | Add support for SMT-LIB v2.5 command get-unsat-assumptions...
|
commit | commitdiff | tree |
| 2018-03-09 |
Aina Niemetz | Fixed message in get-antlr script.
|
commit | commitdiff | tree |
| 2018-03-05 |
Aina Niemetz | Add support for check-sat-assuming. (#1637)
|
commit | commitdiff | tree |
| 2018-03-05 |
Aina Niemetz | Add CVC4_PUBLIC keyword to overloads of << for Expr...
|
commit | commitdiff | tree |
| 2018-03-05 |
Aina Niemetz | Add uniform way to serialize containers of Expr to...
|
commit | commitdiff | tree |
| 2018-03-02 |
Aina Niemetz | Fixed typo.
|
commit | commitdiff | tree |
| 2018-03-02 |
Aina Niemetz | Fixed comments in smt_engine.h.
|
commit | commitdiff | tree |
| 2018-02-28 |
Aina Niemetz | SmtEngine::getAssignment now returns a vector of assignments...
|
commit | commitdiff | tree |
| 2018-02-28 |
Aina Niemetz | Remove unused code in pushDefineFunRecScop in smt2...
|
commit | commitdiff | tree |
| 2018-02-23 |
Aina Niemetz | Split and document bitvector.h. (#1615)
|
commit | commitdiff | tree |
| 2018-02-22 |
Aina Niemetz | Fixed disabling the BV equality slicer for quantifiers...
|
commit | commitdiff | tree |
| 2018-02-22 |
Aina Niemetz | Disable BV equality slicer if not pure QF_BV. (#1619)
|
commit | commitdiff | tree |
| 2018-02-20 |
Aina Niemetz | Improve documentation of bv::utils::isCoreTerm (#1617)
|
commit | commitdiff | tree |
| 2018-02-20 |
Aina Niemetz | Moved and simplified bv::utils::intersect. (#1614)
|
commit | commitdiff | tree |
| 2018-02-20 |
Aina Niemetz | Unrecursified and merged bv::utils::is(Core|Equality...
|
commit | commitdiff | tree |
| 2018-02-17 |
Aina Niemetz | bv::utils::mk(And|Or) Do not return true if size of...
|
commit | commitdiff | tree |
| 2018-02-16 |
Aina Niemetz | Make regress1 default, only test regress0 on Travis...
|
commit | commitdiff | tree |
| 2018-02-16 |
Aina Niemetz | Removed bv::utils::mkConjunction (redundant). (#1610)
|
commit | commitdiff | tree |
| 2018-02-14 |
Aina Niemetz | Provide a uniform way to serialize node containers...
|
commit | commitdiff | tree |
| 2018-02-13 |
Aina Niemetz | Moved (unrecursified) bv::utils::collectVars. (#1602)
|
commit | commitdiff | tree |
| 2018-02-13 |
Aina Niemetz | Skip header for determining top contributors list....
|
commit | commitdiff | tree |
| 2018-02-11 |
Aina Niemetz | Move (unrecursified) bv::utils::numNodes to lazy_bitblaster...
|
commit | commitdiff | tree |
| 2018-02-10 |
Aina Niemetz | Move BitVector specific funs from bv::utils to util...
|
commit | commitdiff | tree |
| 2018-02-10 |
Aina Niemetz | Remove mkNode from bv::utils (#1587)
|
commit | commitdiff | tree |
| 2018-02-08 |
Aina Niemetz | Clean up bv utils (part one). (#1580)
|
commit | commitdiff | tree |
| 2018-02-08 |
Aina Niemetz | Updated copyright
|
commit | commitdiff | tree |
| 2018-02-08 |
Aina Niemetz | Simplify and cleanup bv::utils::mkConjunction. (#1571)
|
commit | commitdiff | tree |
| 2018-02-08 |
Aina Niemetz | Reduce number of Travis builds. (#1578)
|
commit | commitdiff | tree |
| 2018-02-07 |
Aina Niemetz | Use template for bv::utils::mkOr. (#1570)
|
commit | commitdiff | tree |
| 2018-02-07 |
Aina Niemetz | Use template for bv::utils::mkAnd. (#1569)
|
commit | commitdiff | tree |
| 2018-02-07 |
Aina Niemetz | Renamed bv::utils::isBVGroundTerm to isBvConstTerm...
|
commit | commitdiff | tree |
| 2018-02-07 |
Aina Niemetz | Split and document theory_bv_utils. (#1566)
|
commit | commitdiff | tree |
| 2018-02-06 |
Aina Niemetz | Updated copyright header for bv_inverter.(cpp|h).
|
commit | commitdiff | tree |
| 2018-02-06 |
Aina Niemetz | Updated year in update-copyright script.
|
commit | commitdiff | tree |
| 2018-02-06 |
Aina Niemetz | Updated authors list
|
commit | commitdiff | tree |
| 2018-01-25 |
Aina Niemetz | Added unit tests for PLUS, NEG, NOT ICs for CBQI BV...
|
commit | commitdiff | tree |
| 2018-01-23 |
Aina Niemetz | Fix MULT handling for CBQI BV. (#1531)
|
commit | commitdiff | tree |
| 2018-01-22 |
Aina Niemetz | Add previous concat handling for CBQI BV as heuristic...
|
commit | commitdiff | tree |
| 2018-01-22 |
Aina Niemetz | Refactor and fix solveBvLit for CBQI BV. (#1526)
|
commit | commitdiff | tree |
| 2018-01-14 |
Aina Niemetz | Remove BITVECTOR_SUB from isInvertible(). (#1513)
|
commit | commitdiff | tree |
| 2018-01-10 |
Aina Niemetz | Removed division by constant handling for CBQI BV ...
|
commit | commitdiff | tree |
| 2018-01-09 |
Aina Niemetz | Reorganized bitvector.h. (#1505)
|
commit | commitdiff | tree |
| 2018-01-09 |
Aina Niemetz | Fix output of --trace=help. (#1500)
|
commit | commitdiff | tree |
| 2018-01-09 |
Aina Niemetz | Add bv util mkConst(unsigned, Integer&). (#1499)
|
commit | commitdiff | tree |
| 2018-01-09 |
Aina Niemetz | Added division by constant handling for CBQI BV. (...
|
commit | commitdiff | tree |
| 2018-01-08 |
Aina Niemetz | Remove portfolio option from builds. (#1496)
|
commit | commitdiff | tree |
| 2018-01-05 |
Aina Niemetz | Fix side condition handling for PLUS, XOR, SIGN_EXTEND...
|
commit | commitdiff | tree |
| 2018-01-03 |
Aina Niemetz | Add side conditions for UGT/SGT over BITVECTOR_UREM...
|
commit | commitdiff | tree |
| 2018-01-03 |
Aina Niemetz | Add side conditions for inequalities over BITVECTOR_MULT...
|
commit | commitdiff | tree |
| 2018-01-03 |
Aina Niemetz | Add side conditions for inequalities over BITVECTOR_UDIV...
|
commit | commitdiff | tree |
| 2018-01-03 |
Aina Niemetz | Simplify side condition for SGE over UREM (index =...
|
commit | commitdiff | tree |
| 2017-12-30 |
Aina Niemetz | Add side conditions for inequalities over BITVECTOR_UREM...
|
commit | commitdiff | tree |
| 2017-12-30 |
Aina Niemetz | Fix RNG for seed = 0. (#1459)
|
commit | commitdiff | tree |
| 2017-12-29 |
Aina Niemetz | Fix unit tests for ineq for CBQI BV. (#1456)
|
commit | commitdiff | tree |
| 2017-12-29 |
Aina Niemetz | Add unit tests for side conditions for inequality for...
|
commit | commitdiff | tree |
| 2017-12-28 |
Aina Niemetz | Minor refactor for inequality handling for CBQI BV...
|
commit | commitdiff | tree |
| 2017-12-21 |
Aina Niemetz | Add explicit disequality handling when generating side...
|
commit | commitdiff | tree |
| 2017-12-19 |
Aina Niemetz | Fix travis write errors. (#1445)
|
commit | commitdiff | tree |
| 2017-12-16 |
Aina Niemetz | Enable side condition handling for shifts introduced...
|
commit | commitdiff | tree |
| 2017-12-14 |
Aina Niemetz | Add missing side conditions for SHL, LSHR, ASHR for...
|
commit | commitdiff | tree |
| 2017-12-08 |
Aina Niemetz | Fixed side conditions for CBQI BV, added unit tests...
|
commit | commitdiff | tree |
| 2017-12-06 |
Aina Niemetz | Fixed time stats for MiniSat solve time. (#1431)
|
commit | commitdiff | tree |
| 2017-11-30 |
Aina Niemetz | Add Gaussian Elimination as a preprocessing pass for...
|
commit | commitdiff | tree |
| 2017-11-17 |
Aina Niemetz | Add random number generator. (#1370)
|
commit | commitdiff | tree |
| 2017-11-09 |
Aina Niemetz | Add modular arithmetic operators. (#1321)
|
commit | commitdiff | tree |
| 2017-11-06 |
Aina Niemetz | Add getValue() for Rational and Integer (GMP and CLN...
|
commit | commitdiff | tree |
| 2017-10-25 |
Aina Niemetz | CBQI BV: Add handling for missing operators. (#1274)
|
commit | commitdiff | tree |
| 2017-10-24 |
Aina Niemetz | CBQI BV: Add ULT/SLT inverse handling. (#1268)
|
commit | commitdiff | tree |
| 2017-10-19 |
Aina Niemetz | CBQI BV: Refactor solve_bv_constraint. (#1265)
|
commit | commitdiff | tree |
| 2017-10-13 |
Aina Niemetz | CBQI BV: Added EXTRACT handling. (#1240)
|
commit | commitdiff | tree |
| 2017-10-12 |
Aina Niemetz | Enable regressions for CBQI BV and fix inverse for...
|
commit | commitdiff | tree |
| 2017-10-10 |
Aina Niemetz | Add copyright information. (#1201)
|
commit | commitdiff | tree |
| 2017-10-10 |
Aina Niemetz | CBQI BV: Add inverse for more operators. (#1213)
|
commit | commitdiff | tree |
| 2017-10-05 |
Aina Niemetz | Add mkZero, mkOne and mkUmulo to bv utils. (#1200)
|
commit | commitdiff | tree |
| 2017-09-27 |
Aina Niemetz | CEGQI for BV: Add inverse for BITVECTOR_MULT. (#1153)
|
commit | commitdiff | tree |
| 2017-09-01 |
Aina Niemetz | Add travis debug build with cln. (#1066)
|
commit | commitdiff | tree |
| 2017-08-25 |
Aina Niemetz | Move LFSC checker out of the CVC repository. (#222)
|
commit | commitdiff | tree |
| 2017-08-25 |
Aina Niemetz | Added missing includes (algorithm).
|
commit | commitdiff | tree |
| 2017-08-22 |
Aina Niemetz | Cleanup: use Assert rather than C assert. (#1052)
|
commit | commitdiff | tree |
| 2017-08-14 |
Aina Niemetz | Merge pull request #214 from CVC4/fix_warn_nonlinear
|
commit | commitdiff | tree |
| 2017-08-12 |
Aina Niemetz | Fix compiler warnings in theory/arith/nonlinear_extension.cpp
|
commit | commitdiff | tree |
| 2017-08-09 |
Aina Niemetz | Fix help message for disable-unit-testing in configure...
|
commit | commitdiff | tree |
| 2017-08-09 |
Aina Niemetz | Fix Assertion (compiler warning) in theory/bv/theory_bv.cpp
|
commit | commitdiff | tree |
| 2017-08-08 |
Aina Niemetz | Fix compiler warning in theory/quantifiers/term_database_syg...
|
commit | commitdiff | tree |
| 2017-08-05 |
Aina Niemetz | Reorganized bitvector.h
|
commit | commitdiff | tree |
| 2017-08-04 |
Aina Niemetz | Fix comments
|
commit | commitdiff | tree |
| 2017-08-04 |
Aina Niemetz | Fix typos in comments
|
commit | commitdiff | tree |
| 2017-07-13 |
Aina Niemetz | Merge pull request #188 from aniemetz/cx11
|
commit | commitdiff | tree |
| 2017-07-13 |
Aina Niemetz | autoconf: make -std=gnu++11 mandatory
|
commit | commitdiff | tree |
| 2017-07-06 |
Aina Niemetz | cut-release: git co -> git checkout
|
commit | commitdiff | tree |
| 2017-07-06 |
Aina Niemetz | cut-release: option handling, get-antlr
|
commit | commitdiff | tree |
|
projects / cvc5.git / search