cvc5.git
6 years agoAdd parameterized datatypes example. (#1676)
Aina Niemetz [Tue, 20 Mar 2018 15:56:07 +0000 (08:56 -0700)]
Add parameterized datatypes example. (#1676)

6 years agocorrect instruction for running example (#1669)
yoni206 [Tue, 20 Mar 2018 15:18:15 +0000 (08:18 -0700)]
correct instruction for running example (#1669)

6 years agoEnable CEGQI for non-linear (#1674)
Andrew Reynolds [Tue, 20 Mar 2018 04:16:45 +0000 (23:16 -0500)]
Enable CEGQI for non-linear (#1674)

6 years agoDocument inferences for strings (#1642)
Andrew Reynolds [Mon, 19 Mar 2018 16:17:40 +0000 (11:17 -0500)]
Document inferences for strings (#1642)

6 years agoUse Cryptominisat version 5.0.2 (instead of 4.2.0). (#1664)
Mathias Preiner [Tue, 13 Mar 2018 22:47:34 +0000 (15:47 -0700)]
Use Cryptominisat version 5.0.2 (instead of 4.2.0). (#1664)

6 years agoSmtEngine::getModel() is now public. (#1665)
Aina Niemetz [Tue, 13 Mar 2018 22:03:41 +0000 (15:03 -0700)]
SmtEngine::getModel() is now public. (#1665)

6 years agoPrinters are now managed as unique_ptr (fix mem leak). (#1654)
Aina Niemetz [Fri, 9 Mar 2018 21:26:14 +0000 (13:26 -0800)]
Printers are now managed as unique_ptr (fix mem leak). (#1654)

6 years agoSome minor cleanup in bv::utils. (#1663)
Aina Niemetz [Fri, 9 Mar 2018 21:01:26 +0000 (13:01 -0800)]
Some minor cleanup in bv::utils. (#1663)

6 years agoAdd support for SMT-LIB v2.5 command get-unsat-assumptions (#1653)
Aina Niemetz [Fri, 9 Mar 2018 19:40:59 +0000 (11:40 -0800)]
Add support for SMT-LIB v2.5 command get-unsat-assumptions (#1653)

6 years agoSkip (get-unsat-assumptions) tests not supported (#1656)
Andres Noetzli [Fri, 9 Mar 2018 18:54:31 +0000 (10:54 -0800)]
Skip (get-unsat-assumptions) tests not supported (#1656)

(get-unsat-assumptions) requires the proof infrastructure,so we can't
run the regression tests if CVC4 has not been configured for it. This
commit changes the regression script to skip tests containing
(get-unsat-assumptions) when CVC4 has not been compiled with proof
support.

6 years agoCleanup Cryptominisat SAT wrapper. (#1652)
Mathias Preiner [Fri, 9 Mar 2018 02:42:03 +0000 (18:42 -0800)]
Cleanup Cryptominisat SAT wrapper. (#1652)

Cryptominisat has name conflicts with the other Minisat implementations since
the Minisat implementations export var_Undef, l_True, ... as macro whereas
Cryptominisat uses static const. In order to avoid these conflicts we
forward declare CMSat::SATSolver and include the cryptominisat header only
in cryptominisat.cpp.

Further, the helper functions are moved into an anonymous namespace in the .cpp file and functions that were not used are removed.

6 years agoFixed message in get-antlr script.
Aina Niemetz [Fri, 9 Mar 2018 01:39:45 +0000 (17:39 -0800)]
Fixed message in get-antlr script.

6 years agoFix Travis for unit test compilation errors. (#1651)
Mathias Preiner [Fri, 9 Mar 2018 00:03:01 +0000 (16:03 -0800)]
Fix Travis for unit test compilation errors. (#1651)

make units does not fail if we have compile error for a unit test, however, make check does.
-Wsuggest-override is now explicitly disabled for unit tests since CxxTest does not add override keywords to the generated source code and thus get a lot of compiler warnings.

Further, this fixes some issues introduced with #1647 due to make units not failing on Travis and fixes the nightly builds.

6 years agoMake statistics output consistent. (#1647)
Mathias Preiner [Wed, 7 Mar 2018 00:54:06 +0000 (16:54 -0800)]
Make statistics output consistent. (#1647)

* Fixes --hide-zero-stats (and really skips the 0 values)
* Removes the additional newline after each statistic
* Introduces theory::getStatsPrefix(TheoryId) to generate consistent
  prefixes for statistics based on the theory id
  (e.g., THEORY_BV -> "theory::bv").

6 years agoSimplify initialization of quantifiers engine (#1641)
Andrew Reynolds [Tue, 6 Mar 2018 22:13:31 +0000 (16:13 -0600)]
Simplify initialization of quantifiers engine (#1641)

6 years agoRefactor symmetry breaking in datatypes sygus (#1640)
Andrew Reynolds [Tue, 6 Mar 2018 20:22:43 +0000 (14:22 -0600)]
Refactor symmetry breaking in datatypes sygus (#1640)

6 years agoRemove printf from output utilities (#1629)
Andres Noetzli [Tue, 6 Mar 2018 18:18:54 +0000 (10:18 -0800)]
Remove printf from output utilities (#1629)

This commit removes the unused printf functions from the output utilities. It also adds `const` keywords where possible. Finally, it removes overloaded `const char*` functions if the same function existed for `const std::string&` and the `const char*` version was only casting the `const char*` to an `std::string`. This conversion happens implicitly, so the `const char*` version is not needed.

6 years agoUpdate semantics for string indexof and replace (#1630)
Andrew Reynolds [Tue, 6 Mar 2018 02:36:17 +0000 (20:36 -0600)]
Update semantics for string indexof and replace (#1630)

6 years agoFix boost url in contrib/get-win-dependencies.
Mathias Preiner [Mon, 5 Mar 2018 23:37:10 +0000 (15:37 -0800)]
Fix boost url in contrib/get-win-dependencies.

This fixes the broken windows nightly builds.

6 years agoEnable -Wsuggest-override by default. (#1643)
Mathias Preiner [Mon, 5 Mar 2018 23:36:50 +0000 (15:36 -0800)]
Enable -Wsuggest-override by default. (#1643)

Adds missing override keywords.

6 years agoFix for sampler. (#1639)
Andrew Reynolds [Mon, 5 Mar 2018 22:53:44 +0000 (16:53 -0600)]
Fix for sampler. (#1639)

6 years agoAdd support for check-sat-assuming. (#1637)
Aina Niemetz [Mon, 5 Mar 2018 22:05:26 +0000 (14:05 -0800)]
Add support for check-sat-assuming. (#1637)

This adds support for check-sat-assuming. It further adds support for SmtEngine::query() over a
vector of Expressions, e.g., smtEngine->query({a, b}); checks the validity (of the current input
formula) under assumption (not (or a b)).

6 years agoAdd CVC4_PUBLIC keyword to overloads of << for Expr containers. (#1644)
Aina Niemetz [Mon, 5 Mar 2018 20:59:23 +0000 (12:59 -0800)]
Add CVC4_PUBLIC keyword to overloads of << for Expr containers. (#1644)

6 years agoAdd uniform way to serialize containers of Expr to stream. (#1638)
Aina Niemetz [Mon, 5 Mar 2018 19:26:53 +0000 (11:26 -0800)]
Add uniform way to serialize containers of Expr to stream. (#1638)

6 years agoFixed typo.
Aina Niemetz [Fri, 2 Mar 2018 23:09:43 +0000 (15:09 -0800)]
Fixed typo.

6 years agoOptimization for sygus streaming mode (#1636)
Andrew Reynolds [Fri, 2 Mar 2018 21:56:16 +0000 (15:56 -0600)]
Optimization for sygus streaming mode (#1636)

6 years agoSimplify sygus wrt miniscoping (#1634)
Andrew Reynolds [Fri, 2 Mar 2018 20:44:04 +0000 (14:44 -0600)]
Simplify sygus wrt miniscoping (#1634)

6 years agoFixed comments in smt_engine.h.
Aina Niemetz [Fri, 2 Mar 2018 19:49:49 +0000 (11:49 -0800)]
Fixed comments in smt_engine.h.

6 years agoPrint candidate rewrites in terms of original grammar (#1635)
Andrew Reynolds [Fri, 2 Mar 2018 17:59:42 +0000 (11:59 -0600)]
Print candidate rewrites in terms of original grammar (#1635)

6 years agoCreate infrastructure for sygus modules (#1632)
Andrew Reynolds [Fri, 2 Mar 2018 03:32:11 +0000 (21:32 -0600)]
Create infrastructure for sygus modules (#1632)

6 years agoSmtEngine::getAssignment now returns a vector of assignments. (#1628)
Aina Niemetz [Wed, 28 Feb 2018 20:19:25 +0000 (12:19 -0800)]
SmtEngine::getAssignment now returns a vector of assignments. (#1628)

6 years agoMinor fixes for rec-fun (#1616)
Andrew Reynolds [Wed, 28 Feb 2018 04:50:47 +0000 (22:50 -0600)]
Minor fixes for rec-fun (#1616)

6 years agoRemove unused code in pushDefineFunRecScop in smt2.cpp. (#1627)
Aina Niemetz [Wed, 28 Feb 2018 03:06:58 +0000 (19:06 -0800)]
Remove unused code in pushDefineFunRecScop in smt2.cpp. (#1627)

6 years agoImprove rewriter for string indexof (#1592)
Andrew Reynolds [Tue, 27 Feb 2018 22:52:57 +0000 (16:52 -0600)]
Improve rewriter for string indexof (#1592)

6 years agoOption to not use partial function semantics for arithmetic div by zero (#1620)
Andrew Reynolds [Tue, 27 Feb 2018 21:15:07 +0000 (15:15 -0600)]
Option to not use partial function semantics for arithmetic div by zero (#1620)

6 years agoImprovements to sygus sampling (#1621)
Andrew Reynolds [Tue, 27 Feb 2018 19:58:45 +0000 (13:58 -0600)]
Improvements to sygus sampling (#1621)

6 years agoAdd unit tests for BitVector, minor BV rewrite fix (#1622)
Andres Noetzli [Sat, 24 Feb 2018 02:02:53 +0000 (18:02 -0800)]
Add unit tests for BitVector, minor BV rewrite fix (#1622)

This commit adds unit tests for the BitVector class and adds some additional argument checks. Additionally, it fixes a minor issue in the ZeroExtendUltConst rule if the zero_extend was by 0 bits. In that case, the rule was calling BitVector::extract() with high < low.

6 years agoSplit and document bitvector.h. (#1615)
Aina Niemetz [Fri, 23 Feb 2018 19:57:10 +0000 (11:57 -0800)]
Split and document bitvector.h. (#1615)

6 years agoFix cd-simplification for strings (#1624)
Andrew Reynolds [Fri, 23 Feb 2018 17:18:40 +0000 (11:18 -0600)]
Fix cd-simplification for strings (#1624)

6 years agoMinor improvements to string rewriter (#1572)
Andrew Reynolds [Thu, 22 Feb 2018 20:08:13 +0000 (14:08 -0600)]
Minor improvements to string rewriter (#1572)

6 years agoFixed disabling the BV equality slicer for quantifiers. (#1623)
Aina Niemetz [Thu, 22 Feb 2018 19:11:39 +0000 (11:11 -0800)]
Fixed disabling the BV equality slicer for quantifiers. (#1623)

This fixes an incorrect condition introduced in #1619 to disable the BV equality slicer.

6 years agoDisable BV equality slicer if not pure QF_BV. (#1619)
Aina Niemetz [Thu, 22 Feb 2018 01:09:23 +0000 (17:09 -0800)]
Disable BV equality slicer if not pure QF_BV. (#1619)

6 years agoImprove documentation of bv::utils::isCoreTerm (#1617)
Aina Niemetz [Tue, 20 Feb 2018 23:21:57 +0000 (15:21 -0800)]
Improve documentation of bv::utils::isCoreTerm (#1617)

6 years agoMoved and simplified bv::utils::intersect. (#1614)
Aina Niemetz [Tue, 20 Feb 2018 21:02:00 +0000 (13:02 -0800)]
Moved and simplified bv::utils::intersect. (#1614)

Tested against the recursive implementation with a temporary assertion on regression tests
with --bv-eq-slicer=auto.

6 years agoMinor fixes and additions for transcendental functions (#1612)
Andrew Reynolds [Tue, 20 Feb 2018 18:53:12 +0000 (12:53 -0600)]
Minor fixes and additions for transcendental functions (#1612)

Also adds parsing support for PI in smt2 with syntax "real.pi".

6 years agoUnrecursified and merged bv::utils::is(Core|Equality)Term. (#1605)
Aina Niemetz [Tue, 20 Feb 2018 18:05:05 +0000 (10:05 -0800)]
Unrecursified and merged bv::utils::is(Core|Equality)Term. (#1605)

This unrecursifies and merges bv::utils::isCoreTerm and bv::utils::isEqualityTerm to avoid
code duplication.

In the best case, the recursive implementation visits less nodes. This can be achieved with
the non-recursive implementation, however, at the cost of increased code complexity.
In practice, on QF_BV the new implementation slightly improves performance.

Tested against the recursive implementation with a temporary assertion on regression
tests (bv::utils::isCoreTerm was tested with --bv-eq-slicer=auto).
Further tested on QF_BV with a TO of 300s (slight performance improvement).

6 years agobv::utils::mk(And|Or) Do not return true if size of vector is 0. (#1613)
Aina Niemetz [Sat, 17 Feb 2018 00:41:29 +0000 (16:41 -0800)]
bv::utils::mk(And|Or) Do not return true if size of vector is 0. (#1613)

6 years agoMake regress1 default, only test regress0 on Travis. (#1611)
Aina Niemetz [Fri, 16 Feb 2018 15:05:14 +0000 (07:05 -0800)]
Make regress1 default, only test regress0 on Travis. (#1611)

6 years agoRemoved bv::utils::mkConjunction (redundant). (#1610)
Aina Niemetz [Fri, 16 Feb 2018 01:51:42 +0000 (17:51 -0800)]
Removed bv::utils::mkConjunction (redundant). (#1610)

6 years agoFix corner case for rewrite of mult by pow 2 (#1601)
Andrew Reynolds [Thu, 15 Feb 2018 23:34:54 +0000 (17:34 -0600)]
Fix corner case for rewrite of mult by pow 2 (#1601)

6 years agoRefactor regressions (#1581)
Andrew Reynolds [Thu, 15 Feb 2018 21:31:48 +0000 (15:31 -0600)]
Refactor regressions (#1581)

6 years agoFix context memory manager unit test (#1609)
Andres Noetzli [Thu, 15 Feb 2018 18:26:08 +0000 (10:26 -0800)]
Fix context memory manager unit test (#1609)

Commit 83f150c727f197c530d6f46a75b516eea52bed29 changed the flag
that we use to determine whether to use the context memory manager
or the debug version. However, the change was not reflected in
the context memory manager unit test. This commit fixes the unit
test to check the correct flag.

6 years agoQuantifiers subdirectories (#1608)
Andrew Reynolds [Wed, 14 Feb 2018 23:55:23 +0000 (17:55 -0600)]
Quantifiers subdirectories (#1608)

6 years agoRemove unused cd_set_collection.h (#1606)
Andres Noetzli [Wed, 14 Feb 2018 01:29:50 +0000 (17:29 -0800)]
Remove unused cd_set_collection.h (#1606)

6 years agoProvide a uniform way to serialize node containers to output stream. (#1604)
Aina Niemetz [Wed, 14 Feb 2018 00:34:08 +0000 (16:34 -0800)]
Provide a uniform way to serialize node containers to output stream. (#1604)

6 years agoMoved (unrecursified) bv::utils::collectVars. (#1602)
Aina Niemetz [Tue, 13 Feb 2018 23:02:28 +0000 (15:02 -0800)]
Moved (unrecursified) bv::utils::collectVars. (#1602)

6 years agoSkip header for determining top contributors list. (#1603)
Aina Niemetz [Tue, 13 Feb 2018 19:04:27 +0000 (11:04 -0800)]
Skip header for determining top contributors list. (#1603)

6 years agoOption to use extended rewriter as a preprocessing pass (#1600)
Andrew Reynolds [Tue, 13 Feb 2018 00:16:59 +0000 (18:16 -0600)]
Option to use extended rewriter as a preprocessing pass (#1600)

6 years agoMinor improvements to sygus sampler (#1598)
Andrew Reynolds [Mon, 12 Feb 2018 22:14:29 +0000 (16:14 -0600)]
Minor improvements to sygus sampler (#1598)

6 years agoMove (unrecursified) bv::utils::numNodes to lazy_bitblaster.cpp. (#1594)
Aina Niemetz [Sun, 11 Feb 2018 19:13:33 +0000 (11:13 -0800)]
Move (unrecursified) bv::utils::numNodes to lazy_bitblaster.cpp. (#1594)

This unrecursifies and moves bv::utils::numNodes to an unnamed namespace in lazy_bitblaster.cpp
(only place where it is used). Tested against the recursive implementation (with a temporary
Assertion) on regression tests.

6 years agoMore minor improvements to synth-rr (#1597)
Andrew Reynolds [Sun, 11 Feb 2018 02:13:29 +0000 (20:13 -0600)]
More minor improvements to synth-rr (#1597)

6 years agoMove BitVector specific funs from bv::utils to util/bitvector.h. (#1589)
Aina Niemetz [Sat, 10 Feb 2018 06:10:30 +0000 (22:10 -0800)]
Move BitVector specific funs from bv::utils to util/bitvector.h. (#1589)

6 years agoRemove mkNode from bv::utils (#1587)
Aina Niemetz [Sat, 10 Feb 2018 02:38:12 +0000 (18:38 -0800)]
Remove mkNode from bv::utils (#1587)

6 years agoRemoving an always true comparison (unsigned) >= 0u. (#1582)
Tim King [Fri, 9 Feb 2018 23:14:48 +0000 (15:14 -0800)]
Removing an always true comparison (unsigned) >= 0u.  (#1582)

6 years agoClass to reduce printing of redundant candidate rewrites (#1588)
Andrew Reynolds [Fri, 9 Feb 2018 21:08:11 +0000 (15:08 -0600)]
Class to reduce printing of redundant candidate rewrites (#1588)

6 years agoRenaming CHECK to CVC4_CHECK. This avoids name collisions with other popular assertio...
Tim King [Fri, 9 Feb 2018 20:34:47 +0000 (12:34 -0800)]
Renaming CHECK to CVC4_CHECK. This avoids name collisions with other popular assertion macros. This name is likely temporary while Assert() is deprecated. (#1590)

6 years agoReplacing an incorrect reference to an injected class name when the type was meant...
Tim King [Fri, 9 Feb 2018 19:23:31 +0000 (11:23 -0800)]
Replacing an incorrect reference to an injected class name when the type was meant. (#1585)

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)