cvc5.git
6 years agoReplace CMM flag with debug CMM flag, fix leak in debug CMM (#1586)
Andres Noetzli [Fri, 9 Feb 2018 02:36:12 +0000 (18:36 -0800)]
Replace CMM flag with debug CMM flag, fix leak in debug CMM (#1586)

Previously, we had -DCVC4_CONTEXT_MEMORY_MANAGER that needed to be added as a compile flag
to use the context memory manager (which we want by default). This makes compiling with
other build systems cumbersome because you have to know about the flag.

This commit replaces the -DCVC4_CONTEXT_MEMORY_MANAGER flag with a -DCVC4_DEBUG_CONTEXT_MEMORY_MANAGER
flag that does the opposite (in absence of the flag, we use the context memory manager).
Additionally, the commit fixes a memory leak in the debug context memory manager (the
destructor did not clean up the allocations).

6 years agoInlining line_buffered_input to avoid warning about unused variables in production...
Tim King [Fri, 9 Feb 2018 00:12:07 +0000 (16:12 -0800)]
Inlining line_buffered_input to avoid warning about unused variables in production builds. (#1584)

6 years agoClean up bv utils (part one). (#1580)
Aina Niemetz [Thu, 8 Feb 2018 23:19:36 +0000 (15:19 -0800)]
Clean up bv utils (part one). (#1580)

This is part one of an effort to clean up bv utils. It addresses review comments not addressed in
#1566 (changes of moved code), removes unused functions and moves a helper to compute the
gcd over Index.

6 years agoAdding virtual destructors on classes with virtual functions. (#1583)
Tim King [Thu, 8 Feb 2018 21:52:36 +0000 (13:52 -0800)]
Adding virtual destructors on classes with virtual functions. (#1583)

6 years agoMinor improvements to sygus sampling. (#1577)
Andrew Reynolds [Thu, 8 Feb 2018 20:01:17 +0000 (14:01 -0600)]
Minor improvements to sygus sampling. (#1577)

6 years agoUpdated copyright
Aina Niemetz [Thu, 8 Feb 2018 19:18:19 +0000 (11:18 -0800)]
Updated copyright

6 years agoInitializing Timer::d_wall_limit (CID 1362899). (#1573)
Tim King [Thu, 8 Feb 2018 16:59:05 +0000 (08:59 -0800)]
Initializing Timer::d_wall_limit (CID 1362899). (#1573)

6 years agoSimplify and cleanup bv::utils::mkConjunction. (#1571)
Aina Niemetz [Thu, 8 Feb 2018 16:10:36 +0000 (08:10 -0800)]
Simplify and cleanup bv::utils::mkConjunction. (#1571)

6 years agoCheck whether Cryptominisat4/ABC was installed via get-* script. (#1565)
Mathias Preiner [Thu, 8 Feb 2018 15:27:16 +0000 (07:27 -0800)]
Check whether Cryptominisat4/ABC was installed via get-* script. (#1565)

6 years agoRemove invalid regression test (#1579)
Andres Noetzli [Thu, 8 Feb 2018 14:52:16 +0000 (06:52 -0800)]
Remove invalid regression test (#1579)

6 years agoRemoving an unused variable. (#1576)
Tim King [Thu, 8 Feb 2018 06:52:40 +0000 (22:52 -0800)]
Removing an unused variable. (#1576)

6 years agoFixing more inconsistent usages of override. (#1575)
Tim King [Thu, 8 Feb 2018 03:06:11 +0000 (19:06 -0800)]
Fixing more inconsistent usages of override. (#1575)

6 years agoReduce number of Travis builds. (#1578)
Aina Niemetz [Thu, 8 Feb 2018 01:51:46 +0000 (17:51 -0800)]
Reduce number of Travis builds. (#1578)

6 years agoFixing line numbers on type_checker_template.cpp (#1574)
Tim King [Thu, 8 Feb 2018 00:11:36 +0000 (16:11 -0800)]
Fixing line numbers on type_checker_template.cpp (#1574)

6 years agoCleanup Cryptominisat header. (#1561)
Mathias Preiner [Wed, 7 Feb 2018 23:00:41 +0000 (15:00 -0800)]
Cleanup Cryptominisat header. (#1561)

Clang formatted sat_solver_factor.cpp

6 years agoUse template for bv::utils::mkOr. (#1570)
Aina Niemetz [Wed, 7 Feb 2018 20:34:59 +0000 (12:34 -0800)]
Use template for bv::utils::mkOr. (#1570)

6 years agoAdds a new CHECK macro that abort()s on failure. (#1532)
Tim King [Wed, 7 Feb 2018 18:19:04 +0000 (10:19 -0800)]
Adds a new CHECK macro that abort()s on failure. (#1532)

6 years agoAdd remaining transcendental functions (#1551)
Andrew Reynolds [Wed, 7 Feb 2018 15:12:59 +0000 (09:12 -0600)]
Add remaining transcendental functions (#1551)

6 years agoUse template for bv::utils::mkAnd. (#1569)
Aina Niemetz [Wed, 7 Feb 2018 08:55:44 +0000 (00:55 -0800)]
Use template for bv::utils::mkAnd. (#1569)

6 years agoRenamed bv::utils::isBVGroundTerm to isBvConstTerm. (#1568)
Aina Niemetz [Wed, 7 Feb 2018 07:20:20 +0000 (23:20 -0800)]
Renamed bv::utils::isBVGroundTerm to isBvConstTerm. (#1568)

6 years agoSplit and document theory_bv_utils. (#1566)
Aina Niemetz [Wed, 7 Feb 2018 05:42:25 +0000 (21:42 -0800)]
Split and document theory_bv_utils. (#1566)

This moves the implementation from the header to the .cpp file. It further documents all functions in
the header file.

6 years agoUse separate shell script for common get-* script parts. (#1567)
Mathias Preiner [Wed, 7 Feb 2018 03:46:04 +0000 (19:46 -0800)]
Use separate shell script for common get-* script parts. (#1567)

6 years agoFixes two memory leaks coming from Transf. (#1564)
Tim King [Wed, 7 Feb 2018 02:25:45 +0000 (18:25 -0800)]
Fixes two memory leaks coming from Transf. (#1564)

First, it adds a virtual destructor so the subclasses will get cleaned up. Second, it wraps the returned
pointer in a unique_ptr. Should fix ASAN failures in the nightly run.

6 years agoUpdated copyright header for bv_inverter.(cpp|h).
Aina Niemetz [Tue, 6 Feb 2018 23:35:20 +0000 (15:35 -0800)]
Updated copyright header for bv_inverter.(cpp|h).

6 years agoUpdated year in update-copyright script.
Aina Niemetz [Tue, 6 Feb 2018 23:32:30 +0000 (15:32 -0800)]
Updated year in update-copyright script.

6 years agoResolving warnings from -Winconsistent-missing-override on clang. (#1563)
Tim King [Tue, 6 Feb 2018 23:55:40 +0000 (15:55 -0800)]
Resolving warnings from -Winconsistent-missing-override on clang. (#1563)

6 years agoFix two multiply-by-constant corner cases for bv rewriter (#1562)
Andrew Reynolds [Tue, 6 Feb 2018 22:13:41 +0000 (16:13 -0600)]
Fix two multiply-by-constant corner cases for bv rewriter (#1562)

6 years agoUpdated authors list
Aina Niemetz [Tue, 6 Feb 2018 18:56:41 +0000 (10:56 -0800)]
Updated authors list

6 years agoFix rewrite for string replace (#1537)
Andrew Reynolds [Tue, 6 Feb 2018 17:20:16 +0000 (11:20 -0600)]
Fix rewrite for string replace (#1537)

6 years agoUsing getOperator() directly instead of using -1. CID 1172262. (#1559)
Tim King [Tue, 6 Feb 2018 07:47:26 +0000 (23:47 -0800)]
Using getOperator() directly instead of using -1. CID 1172262. (#1559)

6 years agoAborting on errors in StatisticsRegistry::unregisterStat() instead of throwing except...
Tim King [Tue, 6 Feb 2018 03:07:17 +0000 (19:07 -0800)]
Aborting on errors in StatisticsRegistry::unregisterStat() instead of throwing exceptions. This is called from destructors and therefore it is inappropraiate to throw exceptions. This solution is temporary until Assert() is deprecated in favor of an aborting version. (#1539)

6 years agoStatically eliminate redundant sygus constructors (#1560)
Andrew Reynolds [Tue, 6 Feb 2018 00:59:13 +0000 (18:59 -0600)]
Statically eliminate redundant sygus constructors (#1560)

6 years agoCleaning up the printing of theory model representative sets. (#1538)
Tim King [Mon, 5 Feb 2018 23:17:45 +0000 (15:17 -0800)]
Cleaning up the printing of theory model representative sets. (#1538)

6 years agoRemoving references to __gnu_cxx. (#1541)
Tim King [Mon, 5 Feb 2018 20:38:13 +0000 (12:38 -0800)]
Removing references to __gnu_cxx. (#1541)

6 years agoSample based on sygus grammar by default (#1558)
Andrew Reynolds [Sun, 4 Feb 2018 18:46:05 +0000 (12:46 -0600)]
Sample based on sygus grammar by default (#1558)

6 years agoOption to use sampling for CEGIS (#1555)
Andrew Reynolds [Sat, 3 Feb 2018 03:04:49 +0000 (21:04 -0600)]
Option to use sampling for CEGIS (#1555)

6 years agoRestoring ostream format. Resolves a few CIDs 1362780. (#1543)
Tim King [Sat, 3 Feb 2018 01:03:10 +0000 (17:03 -0800)]
Restoring ostream format. Resolves a few CIDs 1362780. (#1543)

6 years agoFix remaining synthesis solution regressions (#1557)
Andrew Reynolds [Fri, 2 Feb 2018 23:20:44 +0000 (17:20 -0600)]
Fix remaining synthesis solution regressions (#1557)

6 years agoOption to check solutions produced by SyGuS solver (#1553)
Haniel Barbosa [Fri, 2 Feb 2018 21:34:44 +0000 (15:34 -0600)]
Option to check solutions produced by SyGuS solver (#1553)

6 years agoAdd interface in sygus to get synthesis solution Nodes (#1552)
Andrew Reynolds [Thu, 1 Feb 2018 19:52:34 +0000 (13:52 -0600)]
Add interface in sygus to get synthesis solution Nodes (#1552)

6 years agoUse sygus to synthesize/verify rewrite rules (#1547)
Andrew Reynolds [Thu, 1 Feb 2018 18:13:54 +0000 (12:13 -0600)]
Use sygus to synthesize/verify rewrite rules (#1547)

6 years agoFurther clean and document datatypes rewriter (#1548)
Andrew Reynolds [Tue, 30 Jan 2018 17:42:31 +0000 (11:42 -0600)]
Further clean and document datatypes rewriter (#1548)

6 years agoGeneralize explanations for PBE sygus strings based on negative contains when multipl...
Andrew Reynolds [Mon, 29 Jan 2018 22:59:13 +0000 (16:59 -0600)]
Generalize explanations for PBE sygus strings based on negative contains when multiple strategies are present (#1546)

6 years agoSort children of all commutative operators for sygus. (#1544)
Andrew Reynolds [Sun, 28 Jan 2018 22:37:54 +0000 (16:37 -0600)]
Sort children of all commutative operators for sygus. (#1544)

6 years agoRemoving an unused variable. Resolves CID 1172257. (#1542)
Tim King [Sat, 27 Jan 2018 20:50:54 +0000 (12:50 -0800)]
Removing an unused variable. Resolves CID 1172257. (#1542)

6 years agoRemoving structurally dead code. (#1540)
Tim King [Sat, 27 Jan 2018 00:29:16 +0000 (16:29 -0800)]
Removing structurally dead code. (#1540)

6 years agoCommenting out throw specifiers on SmtEngine. These can later be refined into better...
Tim King [Thu, 25 Jan 2018 03:55:59 +0000 (19:55 -0800)]
Commenting out throw specifiers on SmtEngine. These can later be refined into better documentation. (#1512)

6 years agoAdded unit tests for PLUS, NEG, NOT ICs for CBQI BV. (#1534)
Aina Niemetz [Thu, 25 Jan 2018 00:19:50 +0000 (16:19 -0800)]
Added unit tests for PLUS, NEG, NOT ICs for CBQI BV. (#1534)

6 years agoFix MULT handling for CBQI BV. (#1531)
Aina Niemetz [Tue, 23 Jan 2018 20:02:42 +0000 (12:02 -0800)]
Fix MULT handling for CBQI BV. (#1531)

6 years agoCommenting out throw specifiers for DeltaRationExceptions. These functions can be...
Tim King [Tue, 23 Jan 2018 08:14:43 +0000 (00:14 -0800)]
Commenting out throw specifiers for DeltaRationExceptions. These functions can be cleaned up later. (#1529)

6 years agoAdd previous concat handling for CBQI BV as heuristic for EQ. (#1528)
Aina Niemetz [Mon, 22 Jan 2018 18:06:26 +0000 (10:06 -0800)]
Add previous concat handling for CBQI BV as heuristic for EQ. (#1528)

Previously, we computed an inverse for s1 o x, x o s2, s1 o x o s2 while disregarding that invertibility
depends on si. This adds this handling as an optional heuristic for concats over (dis)equality since it improves performance on a considerable number of benchmarks.

6 years agoRefactor and fix solveBvLit for CBQI BV. (#1526)
Aina Niemetz [Mon, 22 Jan 2018 04:41:39 +0000 (20:41 -0800)]
Refactor and fix solveBvLit for CBQI BV. (#1526)

This refactors and simplifies solveBvLit() and fixes the following:

- generate side conditions for BITVECTOR_NEG, BITVECTOR_NOT, BITVECTOR_PLUS,
BITVECTOR_XOR over inequalities and disequality
- fix CONCAT handling (generate side conditions rather then computing an inverse which was incorrect)
- fix SIGN_EXTEND handling (same as with CONCATs)

6 years agoOnly push/pop around check-sat if it is associated with an assertion (#1525)
Andrew Reynolds [Mon, 22 Jan 2018 02:06:58 +0000 (20:06 -0600)]
Only push/pop around check-sat if it is associated with an assertion (#1525)

6 years agoRemoves yet more throw specifiers. Updating the documentation as needed. (#1518)
Tim King [Wed, 17 Jan 2018 20:16:17 +0000 (12:16 -0800)]
Removes yet more throw specifiers. Updating the documentation as needed. (#1518)

6 years agoRemoving more miscellaneous throw specifiers. (#1509)
Tim King [Tue, 16 Jan 2018 06:47:40 +0000 (22:47 -0800)]
Removing more miscellaneous throw specifiers. (#1509)

Removing more miscellaneous throw specifiers. Also fixing the spelling of amount in several places.

6 years agoRemoving throw specifiers from Type. (#1511)
Tim King [Mon, 15 Jan 2018 07:56:56 +0000 (23:56 -0800)]
Removing throw specifiers from Type. (#1511)

6 years agoRemoving throw specifiers from OptionsHandler. (#1510)
Tim King [Sun, 14 Jan 2018 08:59:54 +0000 (00:59 -0800)]
Removing throw specifiers from OptionsHandler. (#1510)

6 years agoRemove BITVECTOR_SUB from isInvertible(). (#1513)
Aina Niemetz [Sun, 14 Jan 2018 06:12:27 +0000 (22:12 -0800)]
Remove BITVECTOR_SUB from isInvertible(). (#1513)

6 years agoImprovements for CBQI BV (#1504)
Andrew Reynolds [Fri, 12 Jan 2018 22:05:52 +0000 (16:05 -0600)]
Improvements for CBQI BV (#1504)

6 years agoRemoved division by constant handling for CBQI BV (unsound). (#1508)
Aina Niemetz [Wed, 10 Jan 2018 23:18:13 +0000 (15:18 -0800)]
Removed division by constant handling for CBQI BV (unsound). (#1508)

This removes division by constant handling in the BV inverter introduced in #1498.
Division by constant was simplified to:
x / s OP t ---> x = t / s^-1 if s odd and there exists a multiplicative modular inverse s^-1.
This however, is incorrect since
x / s * 1 / s^-1 != x / (s * s^-1)

6 years agoRemoving throw specifiers for TypeRules. (#1501)
Tim King [Wed, 10 Jan 2018 20:57:38 +0000 (12:57 -0800)]
Removing throw specifiers for TypeRules. (#1501)

6 years agoRemoving throw specifiers from type enumerators. (#1502)
Tim King [Wed, 10 Jan 2018 16:52:01 +0000 (08:52 -0800)]
Removing throw specifiers from type enumerators. (#1502)

6 years agoCleaning up throw specifiers on Exception and subclasses. (#1475)
Tim King [Wed, 10 Jan 2018 06:05:02 +0000 (22:05 -0800)]
Cleaning up throw specifiers on Exception and subclasses. (#1475)

6 years agoFix linearization for terms where the solve variable does not occur. (#1506)
Mathias Preiner [Wed, 10 Jan 2018 02:12:32 +0000 (18:12 -0800)]
Fix linearization for terms where the solve variable does not occur. (#1506)

6 years agoReorganized bitvector.h. (#1505)
Aina Niemetz [Tue, 9 Jan 2018 23:35:44 +0000 (15:35 -0800)]
Reorganized bitvector.h. (#1505)

6 years agoFix output of --trace=help. (#1500)
Aina Niemetz [Tue, 9 Jan 2018 20:44:27 +0000 (12:44 -0800)]
Fix output of --trace=help. (#1500)

6 years agoRemoving throw specifiers from miscellaneous src/expr/ classes. (#1503)
Tim King [Tue, 9 Jan 2018 14:20:52 +0000 (06:20 -0800)]
Removing throw specifiers from miscellaneous src/expr/ classes. (#1503)

6 years agoRemoving more miscellaneous throw specifiers. (#1488)
Tim King [Tue, 9 Jan 2018 06:04:02 +0000 (22:04 -0800)]
Removing more miscellaneous throw specifiers. (#1488)

Removing more miscellaneous throw specifiers.

6 years agoAdd bv util mkConst(unsigned, Integer&). (#1499)
Aina Niemetz [Tue, 9 Jan 2018 04:16:33 +0000 (20:16 -0800)]
Add bv util mkConst(unsigned, Integer&). (#1499)

6 years agoRemove throw specifiers from symbol table. (#1490)
Tim King [Tue, 9 Jan 2018 02:38:20 +0000 (18:38 -0800)]
Remove throw specifiers from symbol table. (#1490)

6 years agoAdded division by constant handling for CBQI BV. (#1498)
Aina Niemetz [Tue, 9 Jan 2018 00:52:36 +0000 (16:52 -0800)]
Added division by constant handling for CBQI BV. (#1498)

6 years agoRemove portfolio option from builds. (#1496)
Aina Niemetz [Mon, 8 Jan 2018 23:30:16 +0000 (15:30 -0800)]
Remove portfolio option from builds. (#1496)

6 years agoRemoves throw specifiers from command.{h,cpp}. (#1485)
Tim King [Mon, 8 Jan 2018 21:28:04 +0000 (13:28 -0800)]
Removes throw specifiers from command.{h,cpp}. (#1485)

6 years agoImprovements to quant+BV/Bool variable elimination (#1495)
Andrew Reynolds [Mon, 8 Jan 2018 19:21:29 +0000 (13:21 -0600)]
Improvements to quant+BV/Bool variable elimination (#1495)

6 years agoFix broken GMP URL in get-win-dependencies script (#1493)
Andres Noetzli [Mon, 8 Jan 2018 18:05:59 +0000 (19:05 +0100)]
Fix broken GMP URL in get-win-dependencies script (#1493)

6 years agoRemove throw specifiers from datatype. (#1489)
Tim King [Mon, 8 Jan 2018 15:49:23 +0000 (07:49 -0800)]
Remove throw specifiers from datatype. (#1489)

6 years agoRe-ordering field initialization in QuantInfo to remove compiler warning. (#1487)
Tim King [Mon, 8 Jan 2018 03:14:57 +0000 (19:14 -0800)]
Re-ordering field initialization in QuantInfo to remove compiler warning. (#1487)

6 years agoRemoves RationalFromDoubleException. Replaces this with an explicit M… (#1476)
Tim King [Mon, 8 Jan 2018 00:46:16 +0000 (16:46 -0800)]
Removes RationalFromDoubleException. Replaces this with an explicit M… (#1476)

* Removes RationalFromDoubleException. Replaces this with an explicit Maybe<Rational> datatype. Makes Maybe<T> CVC4_PUBLIC. Updates the users of Rational::fromDouble(). Miscellaneous cleanup of ApproxSimplex.

6 years agoRemoving throw specifiers from src/parser/. (#1486)
Tim King [Sat, 6 Jan 2018 23:27:11 +0000 (15:27 -0800)]
Removing throw specifiers from src/parser/. (#1486)

6 years agoAdd special {SGE,SGT,NE}_UDIV1 side conditions for BV of size 1. (#1483)
Mathias Preiner [Sat, 6 Jan 2018 06:50:21 +0000 (22:50 -0800)]
Add special {SGE,SGT,NE}_UDIV1 side conditions for BV of size 1. (#1483)

This commit further fixes some other issues with bit-vectors of size 1.

6 years agoUse simpler EQUAL SCs for LSHR0, LSHR1, ASHR0, AHSR1, SHL0, SHL1. (#1482)
Mathias Preiner [Sat, 6 Jan 2018 02:05:41 +0000 (18:05 -0800)]
Use simpler EQUAL SCs for LSHR0, LSHR1, ASHR0, AHSR1, SHL0, SHL1. (#1482)

6 years agoAdd UGT/SGT side conditions for AND/OR + other fixes. (#1481)
Mathias Preiner [Fri, 5 Jan 2018 22:24:49 +0000 (14:24 -0800)]
Add UGT/SGT side conditions for AND/OR + other fixes. (#1481)

6 years agoFix side condition handling for PLUS, XOR, SIGN_EXTEND for CBQI BV. (#1480)
Aina Niemetz [Fri, 5 Jan 2018 02:32:48 +0000 (18:32 -0800)]
Fix side condition handling for PLUS, XOR, SIGN_EXTEND for CBQI BV. (#1480)

6 years agoAdd side conditions for inequalities of SHL. (#1472)
Mathias Preiner [Fri, 5 Jan 2018 01:28:42 +0000 (17:28 -0800)]
Add side conditions for inequalities of SHL. (#1472)

6 years agoImprovements for CBQI (#1478)
Andrew Reynolds [Thu, 4 Jan 2018 23:30:25 +0000 (17:30 -0600)]
Improvements for CBQI (#1478)

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.

6 years agoRemoving miscellaneous throw specifiers. (#1474)
Tim King [Thu, 4 Jan 2018 21:09:39 +0000 (13:09 -0800)]
Removing miscellaneous throw specifiers. (#1474)

6 years agoRemoving throw specifiers from context/. (#1473)
Tim King [Thu, 4 Jan 2018 06:01:42 +0000 (22:01 -0800)]
Removing throw specifiers from context/. (#1473)

6 years agoAdd side conditions for UGT/SGT over BITVECTOR_UREM for CBQI BV. (#1470)
Aina Niemetz [Wed, 3 Jan 2018 22:18:48 +0000 (14:18 -0800)]
Add side conditions for UGT/SGT over BITVECTOR_UREM for CBQI BV. (#1470)

6 years agoAdd UGT/SGT side conditions for LSHR. (#1469)
Mathias Preiner [Wed, 3 Jan 2018 20:44:56 +0000 (12:44 -0800)]
Add UGT/SGT side conditions for LSHR. (#1469)

6 years ago Add side conditions for inequalities over BITVECTOR_MULT for CBQI BV. (#1468)
Aina Niemetz [Wed, 3 Jan 2018 19:26:40 +0000 (11:26 -0800)]
 Add side conditions for inequalities over BITVECTOR_MULT for CBQI BV. (#1468)

6 years agoGlobal negate (#1466)
Andrew Reynolds [Wed, 3 Jan 2018 15:35:27 +0000 (09:35 -0600)]
Global negate (#1466)

6 years ago Add side conditions for inequalities of ASHR. (#1461)
Mathias Preiner [Wed, 3 Jan 2018 07:57:43 +0000 (23:57 -0800)]
 Add side conditions for inequalities of ASHR. (#1461)

6 years agoAdd side conditions for inequalities over BITVECTOR_UDIV for CBQI BV. (#1464)
Aina Niemetz [Wed, 3 Jan 2018 04:30:04 +0000 (20:30 -0800)]
Add side conditions for inequalities over BITVECTOR_UDIV for CBQI BV. (#1464)

We now can handle all cases of (in|dis)equality over BITVECTOR_UREM. This also simplifies some
of the side conditions for equality.

6 years agoSimplify side condition for SGE over UREM (index = 1) for CBQI BV. (#1463)
Aina Niemetz [Wed, 3 Jan 2018 02:17:06 +0000 (18:17 -0800)]
Simplify side condition for SGE over UREM (index = 1) for CBQI BV. (#1463)

6 years agoFix handling for UGT/SGT. (#1467)
Mathias Preiner [Wed, 3 Jan 2018 00:54:32 +0000 (16:54 -0800)]
Fix handling for UGT/SGT. (#1467)

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.

6 years agoRewrites for BitVector multiplication (#1465)
Andrew Reynolds [Tue, 2 Jan 2018 22:12:45 +0000 (16:12 -0600)]
Rewrites for BitVector multiplication (#1465)

6 years agoAdd side conditions for inequalities of LSHR. (#1462)
Mathias Preiner [Tue, 2 Jan 2018 19:21:12 +0000 (11:21 -0800)]
Add side conditions for inequalities of LSHR. (#1462)

6 years agoImprove rewriter for string equality (#1427)
Andrew Reynolds [Tue, 2 Jan 2018 17:43:00 +0000 (11:43 -0600)]
Improve rewriter for string equality (#1427)

6 years agoAdd side conditions for inequalities over BITVECTOR_UREM for CBQI BV. (#1460)
Aina Niemetz [Sat, 30 Dec 2017 04:02:38 +0000 (20:02 -0800)]
Add side conditions for inequalities over BITVECTOR_UREM for CBQI BV. (#1460)

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.

6 years agoFix RNG for seed = 0. (#1459)
Aina Niemetz [Sat, 30 Dec 2017 02:08:41 +0000 (18:08 -0800)]
Fix RNG for seed = 0. (#1459)

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.