cvc5.git
6 years agoRemove references to nyu (#1721)
Clark Barrett [Mon, 2 Apr 2018 20:35:24 +0000 (13:35 -0700)]
Remove references to nyu (#1721)

6 years agoReorganize bitblaster code. (#1695)
Mathias Preiner [Mon, 2 Apr 2018 19:48:44 +0000 (12:48 -0700)]
Reorganize bitblaster code. (#1695)

This splits bitblaster_template.h into the separate header files {aig,eager,lazy}_bitblaster.h and
bitblaster.h (the template class TBitblaster). All the bitblaster related code is moved into the
sub-directory bitblast/.

6 years agoDo not call toString() on malformed node when throwing TypeCheckingExceptionPrivate...
yoni206 [Mon, 2 Apr 2018 18:40:48 +0000 (11:40 -0700)]
Do not call toString() on malformed node when throwing TypeCheckingExceptionPrivate. (#1733)

While throwing a TypeCheckingExceptionPrivate, an IllegalArgumentException was thrown when
trying calling toString() on a malformed node. Fixed by printing the kind of the node and its children
rather than calling toString() on the malformed node.

6 years agoDisable regression (#1731)
Andrew Reynolds [Fri, 30 Mar 2018 19:26:28 +0000 (14:26 -0500)]
Disable regression (#1731)

6 years agoSplit strategy representation from SygusUnif (#1730)
Andrew Reynolds [Fri, 30 Mar 2018 18:36:04 +0000 (13:36 -0500)]
Split strategy representation from SygusUnif (#1730)

6 years agoDo not use factoring inference for transcendental functions (#1707)
Andrew Reynolds [Fri, 30 Mar 2018 16:37:14 +0000 (11:37 -0500)]
Do not use factoring inference for transcendental functions (#1707)

6 years agoSimplify sygus unif so that it is one-to-one with functions to synthesize (#1726)
Andrew Reynolds [Thu, 29 Mar 2018 15:29:02 +0000 (10:29 -0500)]
Simplify sygus unif so that it is one-to-one with functions to synthesize (#1726)

6 years agoMake sygus pbe use sygus unif utility (#1724)
Andrew Reynolds [Tue, 27 Mar 2018 21:54:05 +0000 (16:54 -0500)]
Make sygus pbe use sygus unif utility (#1724)

6 years agoFix for --sygus-rr-synth (#1723)
Andrew Reynolds [Tue, 27 Mar 2018 19:37:01 +0000 (14:37 -0500)]
Fix for --sygus-rr-synth (#1723)

6 years agoMake sygus unif utility (#1720)
Andrew Reynolds [Tue, 27 Mar 2018 17:30:15 +0000 (12:30 -0500)]
Make sygus unif utility (#1720)

6 years agoFilter candidate rewrites based on matching (#1682)
Andrew Reynolds [Tue, 27 Mar 2018 16:53:49 +0000 (11:53 -0500)]
Filter candidate rewrites based on matching (#1682)

6 years agoBetter normalization of string concatenation (#1719)
Andres Noetzli [Tue, 27 Mar 2018 02:27:31 +0000 (19:27 -0700)]
Better normalization of string concatenation (#1719)

6 years agoDocumentation and simplifications for PBE (#1677)
Andrew Reynolds [Tue, 27 Mar 2018 02:02:32 +0000 (21:02 -0500)]
Documentation and simplifications for PBE (#1677)

6 years agoRegression level 0 for distcheck on Travis (#1714)
Andres Noetzli [Mon, 26 Mar 2018 20:30:26 +0000 (13:30 -0700)]
Regression level 0 for distcheck on Travis (#1714)

We are running all our Travis tests with regression level 0 except for
distcheck, which is running with the default level 1. This commit lowers
the level to 0 to make all jobs consistent.

6 years agoAdd support for filtering regressions with regex (#1711)
Andres Noetzli [Mon, 26 Mar 2018 19:59:58 +0000 (12:59 -0700)]
Add support for filtering regressions with regex (#1711)

This commit adds support for filtering the regression tests using a
regex. For example:

```
TEST_REGEX=quantifiers make regress0
```

Runs regression tests from level 0 that have "quantifiers" in their
name.

6 years agoFix memory leak in bvminisat (#1710)
Andres Noetzli [Mon, 26 Mar 2018 19:34:05 +0000 (12:34 -0700)]
Fix memory leak in bvminisat (#1710)

While reviewing #1695, I realized that bvminisat is leaking memory for
each call to setNotify(). This commit uses std::unique_ptr to fix the
issue. It also adds std::unique_ptr to manage d_minisat.

6 years agoMake Java bindings work with newer build envs (#1709)
Andres Noetzli [Mon, 26 Mar 2018 19:09:33 +0000 (12:09 -0700)]
Make Java bindings work with newer build envs (#1709)

Our current build scripts did not work with Automake 1.16. At configure
time, the .swig_deps target in src/bindings/Makefile.am was executed due
to the `@mk_include@ .swig_deps` (which is not the case with older
versions of Automake). This ultimately caused configure to fail because
SWIG was complaining about missing files (generated source files, such
as src/expr/expr.h). This commit fixes the issue by adding
`-ignoremissing` to the call to SWIG. With that option, SWIG is not
complaining about the missing files and the dependency generation
completes successfully.

Currently, the src/bindings/compat/java/create_impl.py script is not
compatible with Python 3, which leads to errors when building on systems
where `python` links to Python 3 (e.g. on Arch Linux). This commit makes
the script compatible with both Python 2 and 3.

Our build scripts were using old -source/-target versions when calling
`javac`. Those are not supported by newer Java versions (e.g.  Java 9).
This commit updates the version to 1.6, which is still fairly old, so
should be broadly supported.

Finally, some systems (e.g. Arch Linux' AUR package for SWIG 2) refer to
SWIG 2 as `swig-2`.  This commit adds support for detecting this at
configure time.

6 years ago Add reasoning for inequalities in str rewriter (#1713)
Andres Noetzli [Mon, 26 Mar 2018 18:44:29 +0000 (11:44 -0700)]
 Add reasoning for inequalities in str rewriter (#1713)

6 years agoSynth-check and accelerate options for sygus-rr (#1691)
Andrew Reynolds [Mon, 26 Mar 2018 18:03:08 +0000 (13:03 -0500)]
Synth-check and accelerate options for sygus-rr (#1691)

6 years agoAbort when sygus-verify finds unsoundness. (#1717)
Andrew Reynolds [Mon, 26 Mar 2018 16:53:51 +0000 (11:53 -0500)]
Abort when sygus-verify finds unsoundness. (#1717)

6 years agoRewrites for substr of strings of length one (#1712)
Andres Noetzli [Mon, 26 Mar 2018 15:52:40 +0000 (08:52 -0700)]
Rewrites for substr of strings of length one (#1712)

This commit adds a rewrite for substrings of strings of length one to
the empty string if it can be shown that it is not possible that the
start position and the length are both greater than zero:

```
(str.substr "A" x y) --> "" if x = 0 |= 0 >= y
```

The commit introduces a set of functions to check such entailments
with assumptions.

6 years agoCheck model only when sat (#1694)
Andrew Reynolds [Mon, 26 Mar 2018 05:45:38 +0000 (00:45 -0500)]
Check model only when sat (#1694)

6 years agoCleanup various exit calls (#1692)
Andrew Reynolds [Sun, 25 Mar 2018 16:47:38 +0000 (11:47 -0500)]
Cleanup various exit calls (#1692)

6 years agoRemove doc/libcvc4.3 from options/Makefile.am. (#1696)
Mathias Preiner [Sun, 25 Mar 2018 06:38:34 +0000 (23:38 -0700)]
Remove doc/libcvc4.3 from options/Makefile.am. (#1696)

This commit fixes an issue with calling make clean && make.

The final doc/libcvc4.3 is now generated during ./autogen.sh and should not
be deleted with make clean.

6 years agoAdd a few quantifiers regressions to improve coverage (#1702)
Andrew Reynolds [Fri, 23 Mar 2018 21:15:16 +0000 (16:15 -0500)]
Add a few quantifiers regressions to improve coverage (#1702)

6 years agoRemove abstract regular expression constant (#1698)
Andrew Reynolds [Fri, 23 Mar 2018 20:23:00 +0000 (15:23 -0500)]
Remove abstract regular expression constant (#1698)

6 years agoRemove unused code (#1700)
Andrew Reynolds [Fri, 23 Mar 2018 19:13:38 +0000 (14:13 -0500)]
Remove unused code (#1700)

6 years agoMinor reorganization for ematching (#1701)
Andrew Reynolds [Fri, 23 Mar 2018 18:33:12 +0000 (13:33 -0500)]
Minor reorganization for ematching (#1701)

6 years agoEnable post-condition strenghtening by default for non-syntax restricted invariant...
Andrew Reynolds [Fri, 23 Mar 2018 17:20:23 +0000 (12:20 -0500)]
Enable post-condition strenghtening by default for non-syntax restricted invariant synthesis (#1703)

6 years agoIgnore whitespaces and moved code for contrib/get-authors.
Mathias Preiner [Thu, 22 Mar 2018 00:15:32 +0000 (17:15 -0700)]
Ignore whitespaces and moved code for contrib/get-authors.

6 years agoFix 'make regress' (#1683)
Andres Noetzli [Wed, 21 Mar 2018 23:51:56 +0000 (16:51 -0700)]
Fix 'make regress' (#1683)

Commit b8db52f9bad5b1053810c93f0067de8423349da3 removed the option to do "make regress" (I only tested with "make regressX" and "make check"). This commit reenables "make regress".

6 years agoRefactor mkoptions (#1631)
Mathias Preiner [Wed, 21 Mar 2018 22:48:57 +0000 (15:48 -0700)]
Refactor mkoptions (#1631)

This commit refactors code generation for options. It uses a new configuration format for defining options (*.toml) and a new Python script mkoptions.py to generate the source code and option documentation.

The option behavior did not change for most of the options, except that for bool --enable-/--disable- long options enable/disable was removed. E.g. --enable-miplib-trick and --disable-miplib-trick got changed to --miplib-trick and --no-miplib-trick.

This commit fixes also an issues with set-option/get-option via the SMT2 interface. Before long options were only accessible if the name included the =ARG part.

6 years agoAdd bit-vector extract example. (#1681)
Aina Niemetz [Wed, 21 Mar 2018 22:09:46 +0000 (15:09 -0700)]
Add bit-vector extract example. (#1681)

6 years agoMore rewrites for indexof (#1648)
Andrew Reynolds [Wed, 21 Mar 2018 21:29:41 +0000 (16:29 -0500)]
More rewrites for indexof (#1648)

6 years ago Move regression tests to single Makefile.am (#1658)
Andres Noetzli [Wed, 21 Mar 2018 20:10:24 +0000 (13:10 -0700)]
 Move regression tests to single Makefile.am (#1658)

Until now, regression tests were split across tens of different
Makefile.am, which required a lot of code duplication and does not
really seem to be in the spirit of automake. If we want to change the
LOG_COMPILER/LOG_DRIVER for example, we have to change every single
Makefile.am, which is cumbersome (I was able to get something
semi-working by exporting those variables but it didn't seem very
clean). Additionally, it made the output of the regression tests fairly
verbose and split the output across multiple log files. Finally
it also limited parallelism when running the regression tests (this fix lowers
the time it takes to run regression level 1 from 3m to 1m45s on my
machine with 16 threads).

This commit moves all the regression tests into
test/regress/Makefile.tests and changes test/regress/Makefile.am to deal
with this new structure. Finally, it changes how the test summary in
test/Makefile.am is produced: instead of relying on the log files for
the subdirectories, it greps for the test results in the log files of
the individual tests. Not the most elegant solution but we should
probably anyway delegate that task to a Python script at some point.

6 years agoFix various regression tests (#1657)
Andres Noetzli [Wed, 21 Mar 2018 16:41:50 +0000 (09:41 -0700)]
Fix various regression tests (#1657)

While reorganizing the regression tests, I found three tests with a
wrong status, one that CVC4 reported unknown for and some regression
tests that had command line options set in the Makefile.am instead of
the tests themselves. This commit fixes the status of the three
regression tests (verified the status with Z3), adds command line
options to make the previously "unknown" test work, and moves the
command line options from the Makefile.am into the individual regression
tests. The latter also required some minor changes to the regression
script because it would not try to determine the expected output from
the (set-info :status ...) command if there was one directive (such as
EXPECT/COMMAND-LINE/etc.).  This was an issue with the tests that now
have a COMMAND-LINE directive.

6 years agoFix for string disequality processing (#1679)
Andrew Reynolds [Wed, 21 Mar 2018 13:03:48 +0000 (08:03 -0500)]
Fix for string disequality processing (#1679)

6 years agoAdd support for CaDiCaL as eager BV SAT solver. (#1675)
Mathias Preiner [Tue, 20 Mar 2018 23:11:15 +0000 (16:11 -0700)]
Add support for CaDiCaL as eager BV SAT solver. (#1675)

6 years agoMinor refactor datatypes sygus (#1673)
Andrew Reynolds [Tue, 20 Mar 2018 22:32:43 +0000 (17:32 -0500)]
Minor refactor datatypes sygus (#1673)

6 years agoInternally remove redundant assertions and infer equalities in NonLinearExtension...
Andrew Reynolds [Tue, 20 Mar 2018 19:03:04 +0000 (14:03 -0500)]
Internally remove redundant assertions and infer equalities in NonLinearExtension (#1633)

6 years agoFix datatype dump regression. (#1672)
Andrew Reynolds [Tue, 20 Mar 2018 18:38:28 +0000 (13:38 -0500)]
Fix datatype dump regression. (#1672)

6 years agoMinor fix and addition to sygus sampler (#1678)
Andrew Reynolds [Tue, 20 Mar 2018 17:13:13 +0000 (12:13 -0500)]
Minor fix and addition to sygus sampler (#1678)

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)