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)
Aina Niemetz [Tue, 13 Mar 2018 22:03:41 +0000 (15:03 -0700)]
SmtEngine::getModel() is now public. (#1665)
Aina Niemetz [Fri, 9 Mar 2018 21:26:14 +0000 (13:26 -0800)]
Printers are now managed as unique_ptr (fix mem leak). (#1654)
Aina Niemetz [Fri, 9 Mar 2018 21:01:26 +0000 (13:01 -0800)]
Some minor cleanup in bv::utils. (#1663)
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)
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.
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.
Aina Niemetz [Fri, 9 Mar 2018 01:39:45 +0000 (17:39 -0800)]
Fixed message in get-antlr script.
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.
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").
Andrew Reynolds [Tue, 6 Mar 2018 22:13:31 +0000 (16:13 -0600)]
Simplify initialization of quantifiers engine (#1641)
Andrew Reynolds [Tue, 6 Mar 2018 20:22:43 +0000 (14:22 -0600)]
Refactor symmetry breaking in datatypes sygus (#1640)
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.
Andrew Reynolds [Tue, 6 Mar 2018 02:36:17 +0000 (20:36 -0600)]
Update semantics for string indexof and replace (#1630)
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.
Mathias Preiner [Mon, 5 Mar 2018 23:36:50 +0000 (15:36 -0800)]
Enable -Wsuggest-override by default. (#1643)
Adds missing override keywords.
Andrew Reynolds [Mon, 5 Mar 2018 22:53:44 +0000 (16:53 -0600)]
Fix for sampler. (#1639)
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)).
Aina Niemetz [Mon, 5 Mar 2018 20:59:23 +0000 (12:59 -0800)]
Add CVC4_PUBLIC keyword to overloads of << for Expr containers. (#1644)
Aina Niemetz [Mon, 5 Mar 2018 19:26:53 +0000 (11:26 -0800)]
Add uniform way to serialize containers of Expr to stream. (#1638)
Aina Niemetz [Fri, 2 Mar 2018 23:09:43 +0000 (15:09 -0800)]
Fixed typo.
Andrew Reynolds [Fri, 2 Mar 2018 21:56:16 +0000 (15:56 -0600)]
Optimization for sygus streaming mode (#1636)
Andrew Reynolds [Fri, 2 Mar 2018 20:44:04 +0000 (14:44 -0600)]
Simplify sygus wrt miniscoping (#1634)
Aina Niemetz [Fri, 2 Mar 2018 19:49:49 +0000 (11:49 -0800)]
Fixed comments in smt_engine.h.
Andrew Reynolds [Fri, 2 Mar 2018 17:59:42 +0000 (11:59 -0600)]
Print candidate rewrites in terms of original grammar (#1635)
Andrew Reynolds [Fri, 2 Mar 2018 03:32:11 +0000 (21:32 -0600)]
Create infrastructure for sygus modules (#1632)
Aina Niemetz [Wed, 28 Feb 2018 20:19:25 +0000 (12:19 -0800)]
SmtEngine::getAssignment now returns a vector of assignments. (#1628)
Andrew Reynolds [Wed, 28 Feb 2018 04:50:47 +0000 (22:50 -0600)]
Minor fixes for rec-fun (#1616)
Aina Niemetz [Wed, 28 Feb 2018 03:06:58 +0000 (19:06 -0800)]
Remove unused code in pushDefineFunRecScop in smt2.cpp. (#1627)
Andrew Reynolds [Tue, 27 Feb 2018 22:52:57 +0000 (16:52 -0600)]
Improve rewriter for string indexof (#1592)
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)
Andrew Reynolds [Tue, 27 Feb 2018 19:58:45 +0000 (13:58 -0600)]
Improvements to sygus sampling (#1621)
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.
Aina Niemetz [Fri, 23 Feb 2018 19:57:10 +0000 (11:57 -0800)]
Split and document bitvector.h. (#1615)
Andrew Reynolds [Fri, 23 Feb 2018 17:18:40 +0000 (11:18 -0600)]
Fix cd-simplification for strings (#1624)
Andrew Reynolds [Thu, 22 Feb 2018 20:08:13 +0000 (14:08 -0600)]
Minor improvements to string rewriter (#1572)
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.
Aina Niemetz [Thu, 22 Feb 2018 01:09:23 +0000 (17:09 -0800)]
Disable BV equality slicer if not pure QF_BV. (#1619)
Aina Niemetz [Tue, 20 Feb 2018 23:21:57 +0000 (15:21 -0800)]
Improve documentation of bv::utils::isCoreTerm (#1617)
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.
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".
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).
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)
Aina Niemetz [Fri, 16 Feb 2018 15:05:14 +0000 (07:05 -0800)]
Make regress1 default, only test regress0 on Travis. (#1611)
Aina Niemetz [Fri, 16 Feb 2018 01:51:42 +0000 (17:51 -0800)]
Removed bv::utils::mkConjunction (redundant). (#1610)
Andrew Reynolds [Thu, 15 Feb 2018 23:34:54 +0000 (17:34 -0600)]
Fix corner case for rewrite of mult by pow 2 (#1601)
Andrew Reynolds [Thu, 15 Feb 2018 21:31:48 +0000 (15:31 -0600)]
Refactor regressions (#1581)
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.
Andrew Reynolds [Wed, 14 Feb 2018 23:55:23 +0000 (17:55 -0600)]
Quantifiers subdirectories (#1608)
Andres Noetzli [Wed, 14 Feb 2018 01:29:50 +0000 (17:29 -0800)]
Remove unused cd_set_collection.h (#1606)
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)
Aina Niemetz [Tue, 13 Feb 2018 23:02:28 +0000 (15:02 -0800)]
Moved (unrecursified) bv::utils::collectVars. (#1602)
Aina Niemetz [Tue, 13 Feb 2018 19:04:27 +0000 (11:04 -0800)]
Skip header for determining top contributors list. (#1603)
Andrew Reynolds [Tue, 13 Feb 2018 00:16:59 +0000 (18:16 -0600)]
Option to use extended rewriter as a preprocessing pass (#1600)
Andrew Reynolds [Mon, 12 Feb 2018 22:14:29 +0000 (16:14 -0600)]
Minor improvements to sygus sampler (#1598)
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.
Andrew Reynolds [Sun, 11 Feb 2018 02:13:29 +0000 (20:13 -0600)]
More minor improvements to synth-rr (#1597)
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)
Aina Niemetz [Sat, 10 Feb 2018 02:38:12 +0000 (18:38 -0800)]
Remove mkNode from bv::utils (#1587)
Tim King [Fri, 9 Feb 2018 23:14:48 +0000 (15:14 -0800)]
Removing an always true comparison (unsigned) >= 0u. (#1582)
Andrew Reynolds [Fri, 9 Feb 2018 21:08:11 +0000 (15:08 -0600)]
Class to reduce printing of redundant candidate rewrites (#1588)
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)
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)
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).
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)
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.
Tim King [Thu, 8 Feb 2018 21:52:36 +0000 (13:52 -0800)]
Adding virtual destructors on classes with virtual functions. (#1583)
Andrew Reynolds [Thu, 8 Feb 2018 20:01:17 +0000 (14:01 -0600)]
Minor improvements to sygus sampling. (#1577)
Aina Niemetz [Thu, 8 Feb 2018 19:18:19 +0000 (11:18 -0800)]
Updated copyright
Tim King [Thu, 8 Feb 2018 16:59:05 +0000 (08:59 -0800)]
Initializing Timer::d_wall_limit (CID
1362899). (#1573)
Aina Niemetz [Thu, 8 Feb 2018 16:10:36 +0000 (08:10 -0800)]
Simplify and cleanup bv::utils::mkConjunction. (#1571)
Mathias Preiner [Thu, 8 Feb 2018 15:27:16 +0000 (07:27 -0800)]
Check whether Cryptominisat4/ABC was installed via get-* script. (#1565)
Andres Noetzli [Thu, 8 Feb 2018 14:52:16 +0000 (06:52 -0800)]
Remove invalid regression test (#1579)
Tim King [Thu, 8 Feb 2018 06:52:40 +0000 (22:52 -0800)]
Removing an unused variable. (#1576)
Tim King [Thu, 8 Feb 2018 03:06:11 +0000 (19:06 -0800)]
Fixing more inconsistent usages of override. (#1575)
Aina Niemetz [Thu, 8 Feb 2018 01:51:46 +0000 (17:51 -0800)]
Reduce number of Travis builds. (#1578)
Tim King [Thu, 8 Feb 2018 00:11:36 +0000 (16:11 -0800)]
Fixing line numbers on type_checker_template.cpp (#1574)
Mathias Preiner [Wed, 7 Feb 2018 23:00:41 +0000 (15:00 -0800)]
Cleanup Cryptominisat header. (#1561)
Clang formatted sat_solver_factor.cpp
Aina Niemetz [Wed, 7 Feb 2018 20:34:59 +0000 (12:34 -0800)]
Use template for bv::utils::mkOr. (#1570)
Tim King [Wed, 7 Feb 2018 18:19:04 +0000 (10:19 -0800)]
Adds a new CHECK macro that abort()s on failure. (#1532)
Andrew Reynolds [Wed, 7 Feb 2018 15:12:59 +0000 (09:12 -0600)]
Add remaining transcendental functions (#1551)
Aina Niemetz [Wed, 7 Feb 2018 08:55:44 +0000 (00:55 -0800)]
Use template for bv::utils::mkAnd. (#1569)
Aina Niemetz [Wed, 7 Feb 2018 07:20:20 +0000 (23:20 -0800)]
Renamed bv::utils::isBVGroundTerm to isBvConstTerm. (#1568)
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.
Mathias Preiner [Wed, 7 Feb 2018 03:46:04 +0000 (19:46 -0800)]
Use separate shell script for common get-* script parts. (#1567)
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.
Aina Niemetz [Tue, 6 Feb 2018 23:35:20 +0000 (15:35 -0800)]
Updated copyright header for bv_inverter.(cpp|h).
Aina Niemetz [Tue, 6 Feb 2018 23:32:30 +0000 (15:32 -0800)]
Updated year in update-copyright script.
Tim King [Tue, 6 Feb 2018 23:55:40 +0000 (15:55 -0800)]
Resolving warnings from -Winconsistent-missing-override on clang. (#1563)
Andrew Reynolds [Tue, 6 Feb 2018 22:13:41 +0000 (16:13 -0600)]
Fix two multiply-by-constant corner cases for bv rewriter (#1562)
Aina Niemetz [Tue, 6 Feb 2018 18:56:41 +0000 (10:56 -0800)]
Updated authors list
Andrew Reynolds [Tue, 6 Feb 2018 17:20:16 +0000 (11:20 -0600)]
Fix rewrite for string replace (#1537)
Tim King [Tue, 6 Feb 2018 07:47:26 +0000 (23:47 -0800)]
Using getOperator() directly instead of using -1. CID
1172262. (#1559)
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)
Andrew Reynolds [Tue, 6 Feb 2018 00:59:13 +0000 (18:59 -0600)]
Statically eliminate redundant sygus constructors (#1560)
Tim King [Mon, 5 Feb 2018 23:17:45 +0000 (15:17 -0800)]
Cleaning up the printing of theory model representative sets. (#1538)
Tim King [Mon, 5 Feb 2018 20:38:13 +0000 (12:38 -0800)]
Removing references to __gnu_cxx. (#1541)
Andrew Reynolds [Sun, 4 Feb 2018 18:46:05 +0000 (12:46 -0600)]
Sample based on sygus grammar by default (#1558)
Andrew Reynolds [Sat, 3 Feb 2018 03:04:49 +0000 (21:04 -0600)]
Option to use sampling for CEGIS (#1555)
Tim King [Sat, 3 Feb 2018 01:03:10 +0000 (17:03 -0800)]
Restoring ostream format. Resolves a few CIDs
1362780. (#1543)