cvc5.git
6 years agoMake 256 the default cardinality for strings (#1783)
Andrew Reynolds [Mon, 16 Apr 2018 17:12:24 +0000 (12:12 -0500)]
Make 256 the default cardinality for strings (#1783)

6 years agoRemoveTermFormulas: Remove ContainsTermITEVisitor (#1782)
Andres Noetzli [Mon, 16 Apr 2018 16:42:34 +0000 (09:42 -0700)]
RemoveTermFormulas: Remove ContainsTermITEVisitor (#1782)

6 years agoSkolemize candidate rewrite rule checks (#1777)
Andrew Reynolds [Mon, 16 Apr 2018 13:14:53 +0000 (08:14 -0500)]
Skolemize candidate rewrite rule checks (#1777)

6 years agoMake strings fmf apply to all but internally generated Skolems (#1780)
Andrew Reynolds [Mon, 16 Apr 2018 01:52:46 +0000 (20:52 -0500)]
Make strings fmf apply to all but internally generated Skolems (#1780)

6 years agoFix type error with regexp (#1778)
Andrew Reynolds [Sun, 15 Apr 2018 18:58:21 +0000 (13:58 -0500)]
Fix type error with regexp (#1778)

6 years agoFix mk type const (#1776)
Andrew Reynolds [Sun, 15 Apr 2018 15:18:34 +0000 (10:18 -0500)]
Fix mk type const (#1776)

This was a new utility, only used so far by the extended rewriter in EqChain simplification.

6 years agoAnother fix for sygus rr stats. (#1768)
Andrew Reynolds [Sat, 14 Apr 2018 14:14:07 +0000 (09:14 -0500)]
Another fix for sygus rr stats. (#1768)

6 years ago[Reg] Make status/unsat-core detection more robust (#1775)
Andres Noetzli [Sat, 14 Apr 2018 09:27:44 +0000 (02:27 -0700)]
[Reg] Make status/unsat-core detection more robust (#1775)

This commit changes the regression script to look for status patterns or
get-unsat-core/get-unsat-assumption commands in the benchmark file
instead of the metadata file (i.e. the .expect file if it exists or the
benchmark file otherwise). This fix is not strictly necessary for our
current regressions but might have lead to surprising outcomes in the
future.

6 years agoFix get-unsat-core detection in regression script (#1773)
Andres Noetzli [Sat, 14 Apr 2018 08:28:17 +0000 (01:28 -0700)]
Fix get-unsat-core detection in regression script (#1773)

Due to a typo in the regression script, the (get-unsat-core) command was
not recognized (the script was looking for (get-unsat-cores)), so it
tried to run a regression script containing (get-unsat-core) even when
CVC4 was compiled without proof support. This commit fixes the typo.

6 years agoallowing --bool-to-bv without quantifiers (#1771)
yoni206 [Sat, 14 Apr 2018 05:58:37 +0000 (22:58 -0700)]
allowing --bool-to-bv without quantifiers (#1771)

6 years agoFix use-after-free in eager bitblaster (#1772)
Andres Noetzli [Sat, 14 Apr 2018 01:22:11 +0000 (18:22 -0700)]
Fix use-after-free in eager bitblaster (#1772)

There was a use-after-free in the eager bitblaster: the context used by
the SAT solver was destroyed before the solver. This lead to a
use-after-free in the destructor of the SAT solver when destroying
context-dependent objects. This commit fixes the issue by changing the
desctruction order such that the context is destroyed after the SAT
solver.

Note: This issue was introduced in commit
a917cc2ab4956b542b1f565abf0e62b197692f8d because d_nullContext and
d_satSolver were changed to be std::unique_ptrs.

6 years agoDisable split for negative contains. (#1774)
Andrew Reynolds [Sat, 14 Apr 2018 00:38:17 +0000 (19:38 -0500)]
Disable split for negative contains. (#1774)

6 years agoFix issue in regression script when proofs enabled (#1770)
Andres Noetzli [Fri, 13 Apr 2018 22:53:44 +0000 (15:53 -0700)]
Fix issue in regression script when proofs enabled (#1770)

There were two issues in the new Python regression script when proofs
were enabled: It would try to run "--check-proofs" on SAT benchmarks and
the parameters added to check unsat cores were wrong. This commit fixes
both issues.

6 years agoFix alpha equivalence for higher-order (#1769)
Andrew Reynolds [Fri, 13 Apr 2018 00:59:59 +0000 (19:59 -0500)]
Fix alpha equivalence for higher-order (#1769)

6 years agoFixes for free variables in assertions (#1762)
Andrew Reynolds [Thu, 12 Apr 2018 17:23:57 +0000 (12:23 -0500)]
Fixes for free variables in assertions (#1762)

6 years agoRefactored BVGauss preprocessing pass. (#1766)
Aina Niemetz [Wed, 11 Apr 2018 01:52:54 +0000 (18:52 -0700)]
Refactored BVGauss preprocessing pass. (#1766)

6 years agoProperly implement function extensionality based on cardinality (#1765)
Andrew Reynolds [Wed, 11 Apr 2018 01:24:34 +0000 (20:24 -0500)]
Properly implement function extensionality based on cardinality (#1765)

6 years ago Improve accuracy of stats for sygus sampler (#1755)
Andrew Reynolds [Tue, 10 Apr 2018 21:44:02 +0000 (16:44 -0500)]
 Improve accuracy of stats for sygus sampler (#1755)

6 years agoRemove unused arith options (#1758)
Andres Noetzli [Tue, 10 Apr 2018 06:45:23 +0000 (23:45 -0700)]
Remove unused arith options (#1758)

Commit 629824db3911ab11ae286e4b14151a537602ba5a added options when
introducing the pseudo boolean processor that were never used. This
commit removes them.

6 years agoFix hasSubterm calls for higher-order (#1760)
Andrew Reynolds [Tue, 10 Apr 2018 02:18:19 +0000 (21:18 -0500)]
Fix hasSubterm calls for higher-order (#1760)

6 years agoFix dumping of benchmark in SmtEngine::checkSatisfiability(). (#1764)
Aina Niemetz [Tue, 10 Apr 2018 01:50:39 +0000 (18:50 -0700)]
Fix dumping of benchmark in SmtEngine::checkSatisfiability(). (#1764)

6 years agoFix higher-order term indexing. (#1754)
Andrew Reynolds [Tue, 10 Apr 2018 01:09:51 +0000 (20:09 -0500)]
Fix higher-order term indexing. (#1754)

6 years agoFix sygus substr static symmetry breaking (#1761)
Andrew Reynolds [Mon, 9 Apr 2018 20:29:08 +0000 (15:29 -0500)]
Fix sygus substr static symmetry breaking (#1761)

6 years agoWarn about trailing spaces in src/Makefile.am (#1759)
Andres Noetzli [Sun, 8 Apr 2018 23:50:40 +0000 (16:50 -0700)]
Warn about trailing spaces in src/Makefile.am (#1759)

6 years agoAllow predetermined first-order variables when constructing deep embedding. (#1757)
Andrew Reynolds [Sun, 8 Apr 2018 21:17:07 +0000 (16:17 -0500)]
Allow predetermined first-order variables when constructing deep embedding. (#1757)

6 years agoCheck free variables in assertions (#1737)
Andrew Reynolds [Sun, 8 Apr 2018 20:23:20 +0000 (15:23 -0500)]
Check free variables in assertions (#1737)

6 years agoDo not introduce uinterpreted constants in TPTP parser (#1743)
Andrew Reynolds [Sun, 8 Apr 2018 20:01:52 +0000 (15:01 -0500)]
Do not introduce uinterpreted constants in TPTP parser (#1743)

6 years agoAdd quantifier name attribute. (#1756)
Andrew Reynolds [Sun, 8 Apr 2018 19:36:20 +0000 (14:36 -0500)]
Add quantifier name attribute. (#1756)

6 years agoFixed get-authors.
Aina Niemetz [Sat, 7 Apr 2018 18:45:16 +0000 (11:45 -0700)]
Fixed get-authors.

6 years agoAdd define rec fun to cvc parser (#1738)
Arjun Viswanathan [Fri, 6 Apr 2018 22:50:48 +0000 (17:50 -0500)]
Add define rec fun to cvc parser (#1738)

6 years ago Python regression script (#1662)
Andres Noetzli [Fri, 6 Apr 2018 04:45:17 +0000 (21:45 -0700)]
 Python regression script (#1662)

Until now, we have been using a bash script for the running the
regressions. That script had several issues, e.g. it was creating many
temprorary files and it was calling itself recursively, making it
difficult to maintain. This commit replaces the script with a Python
script. The Python script uses the TAP protocol, which allows us to
display the results of multiple tests per file (e.g. with --check-models
and without) separately and with more details. It also outputs whenever it starts running
a test, which allows finding "stuck" regression tests on Travis. As recommended in the
automake documentation [0], the commit copies the TAP driver to enable
TAP support for the test driver.

Note: the commit also changes some of the regressions slightly because
we were using "%" for the test directives in SMT files which does not
correspond to the comment character ";". Using the comment character
simplifies the handling and makes it easier for users to reproduce a
failure (they can simply run CVC4 on the regression file).

[0]
https://www.gnu.org/software/automake/manual/html_node/Use-TAP-with-the-Automake-test-harness.html

6 years agoAdd more general SignExtendUltConst rewriting. (#1385)
Mathias Preiner [Thu, 5 Apr 2018 18:40:34 +0000 (11:40 -0700)]
Add more general SignExtendUltConst rewriting. (#1385)

This also adds an additional check in processAssertions to ensure that all
assertions are guaranteed to be rewritten (there was only a comment stating
this).

6 years agoMake Python bindings example compatible w/ Python3 (#1751)
Andres Noetzli [Thu, 5 Apr 2018 18:06:26 +0000 (11:06 -0700)]
Make Python bindings example compatible w/ Python3 (#1751)

6 years agoUpdate README for regression tests (#1746)
Andres Noetzli [Thu, 5 Apr 2018 05:43:48 +0000 (22:43 -0700)]
Update README for regression tests (#1746)

6 years agoProper initialization and destruction of sygus unif (#1750)
Andrew Reynolds [Wed, 4 Apr 2018 23:17:02 +0000 (18:17 -0500)]
Proper initialization and destruction of sygus unif (#1750)

6 years agoFix for corner case of higher-order matching (#1708)
Andrew Reynolds [Wed, 4 Apr 2018 21:17:35 +0000 (16:17 -0500)]
Fix for corner case of higher-order matching  (#1708)

6 years agoDo not debug check models when unknown (#1748)
Andrew Reynolds [Wed, 4 Apr 2018 16:56:59 +0000 (11:56 -0500)]
Do not debug check models when unknown (#1748)

6 years agoFix sygus infer (#1747)
Andrew Reynolds [Wed, 4 Apr 2018 14:40:19 +0000 (09:40 -0500)]
Fix sygus infer (#1747)

6 years agoRefactor IntToBV preprocessing pass (#1716)
Andres Noetzli [Wed, 4 Apr 2018 03:43:37 +0000 (20:43 -0700)]
Refactor IntToBV preprocessing pass (#1716)

This commit refactors the IntToBV preprocessing pass into the new style.
This commit is essentially just a code move, it does not attempt to fix
issues (e.g. #1715).

6 years agoOption to turn arbitrary input into sygus (#1704)
Andrew Reynolds [Wed, 4 Apr 2018 01:29:26 +0000 (20:29 -0500)]
Option to turn arbitrary input into sygus (#1704)

Preprocessing pass that turns an arbitrary (e.g. smt2) input into a sygus conjecture, which is helpful for Horn clause solving.

This includes improvements to the robustness of the sygus solver.

6 years ago[BVMiniSat] Avoid duplicates in conflicts (#1745)
Andres Noetzli [Wed, 4 Apr 2018 00:30:41 +0000 (17:30 -0700)]
[BVMiniSat] Avoid duplicates in conflicts (#1745)

If analyzeFinal() in BVMiniSat was called with a literal that also
occurred in the trail, it could happen that the set of assumptions that
led to the assignment of `p` contained `p` twice.
BitVectorProof::endBVConflict would then register that conflict with the
duplicate literal but at the same time compute a conflict expression
with the duplicate removed. LFSCSatProof::printAssumptionsResolution
would then output two resolutions for the same literal, which made the
simplify_clause side condition fail because it couldn't find the literal
in the clause anymore after the first removal.

The fix simply avoid adding `p` to the set of assumptions if it is found
in the trail. In this situation, `p` is guaranteed to be in the set of
assumptions already because it has been added at the beginning of
analyzeFinal(). This issue originally came up in PR #1384. With this fix
the regression tests pass in #1384.

6 years agoMake sygus unif I/O an subclass of sygus unif (#1741)
Andrew Reynolds [Tue, 3 Apr 2018 23:13:04 +0000 (18:13 -0500)]
Make sygus unif I/O an subclass of sygus unif (#1741)

6 years agoUse choice when expanding definitions for inverse transcendental functions (#1742)
Andrew Reynolds [Tue, 3 Apr 2018 20:49:43 +0000 (15:49 -0500)]
Use choice when expanding definitions for inverse transcendental functions (#1742)

6 years agoInternal sygus type checking (#1734)
Andrew Reynolds [Tue, 3 Apr 2018 15:48:34 +0000 (10:48 -0500)]
Internal sygus type checking (#1734)

6 years agoImprovements to extended rewriter for Booleans and ITE (#1705)
Andrew Reynolds [Tue, 3 Apr 2018 01:03:16 +0000 (20:03 -0500)]
Improvements to extended rewriter for Booleans and ITE (#1705)

6 years agoMake sygus unif utility use sygus unif strategies (#1732)
Andrew Reynolds [Mon, 2 Apr 2018 22:50:31 +0000 (17:50 -0500)]
Make sygus unif utility use sygus unif strategies (#1732)

6 years agoa formula should be an instance of itself (#1668)
yoni206 [Mon, 2 Apr 2018 21:15:02 +0000 (14:15 -0700)]
a formula should be an instance of itself (#1668)

Proof checking failed when applying the instantiation rule so that the original formula and the instantiated formula are the same. Fixed using the new "ifequal" construct in lfsc.

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.