Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-01-06 | Removing throw specifiers from src/parser/. (#1486) | Tim King | |
2018-01-05 | Add special {SGE,SGT,NE}_UDIV1 side conditions for BV of size 1. (#1483) | Mathias Preiner | |
This commit further fixes some other issues with bit-vectors of size 1. | |||
2018-01-05 | Use simpler EQUAL SCs for LSHR0, LSHR1, ASHR0, AHSR1, SHL0, SHL1. (#1482) | Mathias Preiner | |
2018-01-05 | Add UGT/SGT side conditions for AND/OR + other fixes. (#1481) | Mathias Preiner | |
2018-01-04 | Fix side condition handling for PLUS, XOR, SIGN_EXTEND for CBQI BV. (#1480) | Aina Niemetz | |
2018-01-04 | Add side conditions for inequalities of SHL. (#1472) | Mathias Preiner | |
2018-01-04 | Improvements for CBQI (#1478) | Andrew Reynolds | |
Includes: - Basic rewriting for choice functions in the builtin rewriter, - Do not consider more than one equal term in ceg instantiator (helps cases where we have a repeated pattern of duplicate instantiations), - Do not introduce dummy extract equalities in the cbqi-bv-rm-extract pass (dummy concat equalities suffice). - Do not consider extracts in nested quantified formulas in the cbqi-bv-rm-extract pass. | |||
2018-01-04 | Removing miscellaneous throw specifiers. (#1474) | Tim King | |
2018-01-03 | Removing throw specifiers from context/. (#1473) | Tim King | |
2018-01-03 | Add side conditions for UGT/SGT over BITVECTOR_UREM for CBQI BV. (#1470) | Aina Niemetz | |
2018-01-03 | Add UGT/SGT side conditions for LSHR. (#1469) | Mathias Preiner | |
2018-01-03 | Add side conditions for inequalities over BITVECTOR_MULT for CBQI BV. (#1468) | Aina Niemetz | |
2018-01-03 | Global negate (#1466) | Andrew Reynolds | |
2018-01-02 | Add side conditions for inequalities of ASHR. (#1461) | Mathias Preiner | |
2018-01-02 | Add side conditions for inequalities over BITVECTOR_UDIV for CBQI BV. (#1464) | Aina Niemetz | |
We now can handle all cases of (in|dis)equality over BITVECTOR_UREM. This also simplifies some of the side conditions for equality. | |||
2018-01-02 | Simplify side condition for SGE over UREM (index = 1) for CBQI BV. (#1463) | Aina Niemetz | |
2018-01-02 | Fix handling for UGT/SGT. (#1467) | Mathias Preiner | |
Previously, we only handled the case x s < t. With this fix, we now get BITVECTOR_[SU]GT for litk if we encounter a literal t < x s. | |||
2018-01-02 | Rewrites for BitVector multiplication (#1465) | Andrew Reynolds | |
2018-01-02 | Add side conditions for inequalities of LSHR. (#1462) | Mathias Preiner | |
2018-01-02 | Improve rewriter for string equality (#1427) | Andrew Reynolds | |
2017-12-29 | Add side conditions for inequalities over BITVECTOR_UREM for CBQI BV. (#1460) | Aina Niemetz | |
We now can handle all cases of (in|dis)equality over UREM. Previously, we could not handle equality for index=0 and had to rewrite x % s = t to x - x / s * s. Since we can now handle this case, we do not apply this rewriting anymore. | |||
2017-12-29 | Fix RNG for seed = 0. (#1459) | Aina Niemetz | |
The default value for the seed for CVC4's RNG is 0. However, xorshift* requires a non-zero seed, else it generates only zero values. This fixes and prevents this behavior by resetting a given zero seed to ~0. | |||
2017-12-29 | Cbqi repeat solve literal (#1458) | Andrew Reynolds | |
2017-12-29 | Add side conditions for inequalities of AND/OR. (#1457) | Mathias Preiner | |
2017-12-28 | Fix unit tests for ineq for CBQI BV. (#1456) | Aina Niemetz | |
2017-12-28 | Add unit tests for side conditions for inequality for CBQI BV. (#1455) | Aina Niemetz | |
2017-12-28 | Fixes for cbqi (#1453) | Andrew Reynolds | |
2017-12-27 | Rel smt parser (#1446) | Arjun Viswanathan | |
2017-12-27 | Minor refactor for inequality handling for CBQI BV. (#1452) | Aina Niemetz | |
2017-12-27 | Disable sygus PBE when sygus stream is enabled (#1451) | Andrew Reynolds | |
2017-12-20 | Fixes for cbqi-bv (#1449) | Andrew Reynolds | |
2017-12-20 | Add explicit disequality handling when generating side condition for CBQI ↵ | Aina Niemetz | |
BV. (#1447) This refactors solveBvLit to support explicit handling of disequalities (and, in the next step, inequalities) when generating side conditions. | |||
2017-12-20 | Add rewriting rule for ranking benchmarks. (#1448) | Mathias Preiner | |
2017-12-20 | Transcendental functions check model (#1443) | Andrew Reynolds | |
2017-12-18 | Fix travis write errors. (#1445) | Aina Niemetz | |
For reasons unknown, after the latest update of the Trusty environment on Travis, we encountered write errors for the three Clang builds. As suggested here https://github.com/travis-ci/travis-ci/issues/4704#issuecomment-321777557, adding filter_secrets: false to the .travis.yml fixes the problem. Note: switching back to the deprecated builds did not fix the problem. | |||
2017-12-15 | Enable side condition handling for shifts introduced in #1441. (#1444) | Aina Niemetz | |
PR #1441 forgot to enable the missing side condition handling for shifts. This PR enables it. | |||
2017-12-13 | Add missing side conditions for SHL, LSHR, ASHR for CBQI BV. (#1441) | Aina Niemetz | |
This adds side conditions for operators BITVECTOR_SHL, BITVECTOR_LSHR and BITVECTOR_ASHR for index = 1, i.e., s << x = t and s >> x = t. Previously, we treated these cases as non-invertible. | |||
2017-12-12 | Add SIGTERM handler. (#1440) | Mathias Preiner | |
Print statistics if CVC4 gets a SIGTERM signal. | |||
2017-12-10 | Add new infrastructure for preprocessing passes (#1053) | justinxu421 | |
This commit adds new infrastructure for preprocessing passes. It is preparation only, it does not change how the current preprocessing passes work (this will be done in future commits). | |||
2017-12-10 | Fix issue 1433. (#1435) | Andrew Reynolds | |
2017-12-10 | Fix issue with mkConst/getConst of TypeConstant (#1439) | Andres Noetzli | |
When compiling the Java bindings on macOS, the linker complained about CVC4::ExprManager::mkConst<CVC4::TypeConstant>() and CVC4::Expr::getConst<CVC4::TypeConstant>() being undefined. After some research, I found that the issue has been introduced by commit 36bf9f8bcb2a1a3aea1f90eb4d13aed3bbf6da8f. It looks like adding the -no-undefined flags resulted in the symbols in question being omitted due to TypeConstant not being exported. This commit makes TypeConstant CVC4_PUBLIC, which fixes the issue. | |||
2017-12-08 | Add CEGQI BV linearization of additions and equalities over additions. (#1417) | Mathias Preiner | |
Adds support for linearizing additions w.r.t. to a variable. For example, a * x + b + c * d * -x = e + x is rewritten to x * (a - c * d - 1) = e - b. This also adds an additional rewriting rule x * x = x --> x < 2. | |||
2017-12-08 | Fixed side conditions for CBQI BV, added unit tests. (#1434) | Aina Niemetz | |
This fixes the side conditions for BITVECTOR_UREM_TOTAL, BITVECTOR_UDIV_TOTAL, BITVECTOR_LSHR, BITVECTOR_ASHR, BITVECTOR_SHL. It refactors side condition generation for better readability and unit testing. It further adds unit tests for all side conditions we generate in order to check if they too weak or to restrictive (which may result in unsound behavior). This is achieved by checking the following two implications: not (exists x. s * x = t => SC) ... if sat, SC is too restrictive not (SC => exists x. s * x = t) ... if sat SC is too weak This simplifies to checking not (SC <=> exists x. s * x = t). | |||
2017-12-08 | Document and clean datatypes rewriter (#1437) | Andrew Reynolds | |
2017-12-08 | Make collect model info return a Bool (#1421) | Andrew Reynolds | |
2017-12-07 | Fixes related to SyGuS + real arithmetic (#1432) | Andrew Reynolds | |
2017-12-06 | Add command for define-fun-rec and add to API (#1412) | Andrew Reynolds | |
2017-12-06 | Fixed time stats for MiniSat solve time. (#1431) | Aina Niemetz | |
Also, moved implementation of BVMinisatSatSolver::MinisatNotify::notify to .cpp file. | |||
2017-12-06 | Remove CDChunkList (#1414) | Andres Noetzli | |
2017-12-05 | Fix output of --show-trace-tags. (#1430) | Mathias Preiner | |
Now prints each tag in a separate line. |