cvc5.git
5 years agoOptimize DRAT optimization: clause matching (#3074)
Alex Ozdemir [Tue, 2 Jul 2019 09:37:44 +0000 (02:37 -0700)]
Optimize DRAT optimization: clause matching (#3074)

* improved proof production statistics

This commit creates new statistics which will help us understand what is
so expensive about proof production.

There are already statistics for:
* Net time spent building/printing the LFSC proof.
* Size of the LFSC proof.

This commit adds statistics for:
* The time cost of DRAT optimization:
   * net time
   * tool time (drat-trim)
   * clause matching time (matching core clauses with input clauses)
      * Non-trivial because drat-trim can (and does) dedup and reorder
        literals
* The advantage of DRAT optimization (proof/formula size before/after)
* The time cost of DRAT translation [to LRAT or ER] (net time, tool time)
* The time cost of skeleton traversal
* The time cost of printing declatations
* The time cost of printing CNF proofs
* The time cost of printing theory lemmas
* The time cost of printing final UNSAT proof.

There is a method, toStream, which is responsible for much of proof
production. The whole method was timed, but subsections were not. The
timings above consider subsections of it.

I also wanted to better understand the cost of DRAT optimization and
translation.

* [BV Proof] Optimize DRAT optimization

tldr: I made a bad data-structure/algorithm choice when implementing
part of DRAT/CNF-optimization, which consumed **a lot** of time on some
bechmarks. This commit fixes that choice.

Long Version:

Set-Keyed Maps Considered Harmful
=================================

Algorithmic Problem
-------------------

The DRAT optimization process spits out a unsatifiable core of the CNF.
The clauses in the core are all from the original formula, but their
literals may have been reordered and deduplicated.  We must match the
old clauses with new ones, so we know which old clauses are in the core.

Old (BAD) Solution
------------------

Before I didn't really think about this process very much. I built a
solution in which clauses were canonically represented by hash sets of
literals, and made a hash map from canonical clauses to clause indices
into the original CNF.

Problem With Old Solution
-------------------------

In hindsight this was a bad idea. First, it required a new hash set to
be heap-allocated for every clause in the CNF. Second, the map lookups
required set-hashes (reasonable -- linear time, once) and hash-set
equality (not reasonable -- quadratic time, multiple times) on every
lookup.

New Solution
------------

The ideal solution is probably to have the map from clauses to clause
ids be something like a trie. STL doesn't have a trie, but representing
clauses as sorted, deduped vectors of literal in a tree based on
lexicographical comparison is pretty closed to this. On randomly chosen
examples it seems to be a huge improvement over the old
map-keyed-by-sets solution, and I'm in the process of running a full set
of bechmarks.

Also, we store pointers to the clauses already stored elsewhere in the
proof, instead of allocating new memory for them.

Future Work
-----------

It may also be reasonable to do a hash map of sorted, deduped, vector
clauses. I haven't tried this, yet (there's a TODO in the code).

* Update src/proof/clausal_bitvector_proof.h

Thanks andres!

Co-Authored-By: Andres Noetzli <andres.noetzli@gmail.com>
* Respond to Andres' Review: better use of CodeTimer

* Removed commented code (Andres)

5 years agoRefactoring of relevance vector in quantifiers (#3070)
Andrew Reynolds [Mon, 1 Jul 2019 22:27:53 +0000 (17:27 -0500)]
Refactoring of relevance vector in quantifiers (#3070)

5 years agoSupport sygus version 2 format (#3066)
Andrew Reynolds [Mon, 1 Jul 2019 21:33:34 +0000 (16:33 -0500)]
Support sygus version 2 format (#3066)

5 years ago Split higher-order UF solver (#2890)
Andrew Reynolds [Mon, 1 Jul 2019 21:02:18 +0000 (16:02 -0500)]
 Split higher-order UF solver (#2890)

5 years agoAdd higher-order elimination preprocessing pass (#2865)
Andrew Reynolds [Mon, 1 Jul 2019 20:23:15 +0000 (15:23 -0500)]
Add higher-order elimination preprocessing pass (#2865)

5 years agoMake mkOpTerm const (#3072)
makaimann [Fri, 28 Jun 2019 09:36:16 +0000 (02:36 -0700)]
Make mkOpTerm const (#3072)

5 years agoVariable elimination rewrite for quantified strings (#3071)
Andrew Reynolds [Thu, 27 Jun 2019 18:51:40 +0000 (13:51 -0500)]
Variable elimination rewrite for quantified strings (#3071)

5 years agoStratify unfolding of regular expressions based on polarity (#3067)
Andrew Reynolds [Mon, 24 Jun 2019 15:30:27 +0000 (10:30 -0500)]
Stratify unfolding of regular expressions based on polarity (#3067)

5 years agoFix memory leak in unit test (#3068)
Andres Noetzli [Mon, 24 Jun 2019 10:23:15 +0000 (03:23 -0700)]
Fix memory leak in unit test (#3068)

PR #3062 changed `Smt2::setLogic()` to return a heap-allocated command,
which didn't get cleaned up by our `parser_black` unit test. This commit
fixes the memory leak.

5 years agoAdd floating-point support in the Java API (#3063)
Andres Noetzli [Sat, 22 Jun 2019 05:29:01 +0000 (22:29 -0700)]
Add floating-point support in the Java API (#3063)

This commit adds support for the theory of floating-point numbers in the
Java API. Previously, floating-point related classes were missing in the
JAR. The commit also provides an example that showcases how to work with
the theory of floating-point numbers through the API.

5 years agoFix and simplify handling of --force-logic (#3062)
Andres Noetzli [Fri, 21 Jun 2019 18:58:25 +0000 (11:58 -0700)]
Fix and simplify handling of --force-logic (#3062)

The `--force-logic` command line argument can be used to override a
logic specified in an input file or to set a logic when none is given.
Before this commit, both the `SmtEngine` and the parser were aware of
that argument. However, there were two issues if an input file didn't
specify a logic but `--force-logic` was used:

- Upon parsing `--force-logic`, the `SmtEngine` was informed about it
  and set the logic to the forced logic. Then, the parser detected that
  there was no `set-logic` command, so it set the logic to `ALL` and
  emitted a corresponding warning. Finally, `SmtEngine::setDefaults()`
  detected that `forceLogic` was set by the user and changed the logic
  back to the forced logic. The warning was confusing and setting the
  logic multiple times was not elegant.
- For eager bit-blasting, the logic was checked before resetting the
  logic to the forced logic, so it would emit an error that eager
  bit-blasting couldn't be used with the logic (which was `ALL` at that
  point of the execution). This was a problem in the competition because
  our runscript parses the `set-logic` command to decide on the
  appropriate arguments to use and passes the logic to CVC4 via
  `--force-logic`.

This commit moves the handling of `--force-logic` entirely into the
parser. The rationale for that is that this is not an API-level issue
(if you use the API you simply set the logic you want, forcing a
different logic in addition doesn't make sense) and simplifies the
handling of the option (no listeners need to be installed and the logic
is set only once). This commit also removes the option to set the logic
via `(set-option :cvc4-logic ...)` because it complicates matters (e.g.
which method of setting the logic takes precedence?). For the CVC and
the TPTP languages the commit creates a command to set the logic in
`SmtEngine` when the logic is forced in the parser instead of relying on
`SmtEngine` to figure it out itself.

5 years agoUse TMPDIR environment variable for temp files (#2849)
Andres Noetzli [Fri, 21 Jun 2019 17:55:03 +0000 (10:55 -0700)]
Use TMPDIR environment variable for temp files (#2849)

Previously, we were just writing temporary files to `/tmp/` but this
commit allows the user to use the `TMPDIR` environment variable to
determine which directory the temporary file should be written to. The
commit adds a helper function for this and also includes some minor
cleanup of existing code.

5 years ago Strings: More aggressive skolem normalization (#2761)
Andres Noetzli [Tue, 18 Jun 2019 17:04:08 +0000 (10:04 -0700)]
 Strings: More aggressive skolem normalization (#2761)

This PR makes the skolem normalization in the string solver quite a bit
more aggressive by reducing more skolems to prefix and suffix skolems.
Experiments show that this PR significantly improves performance on CMU
benchmarks.

5 years agoUse Ubuntu 16.04 on Travis (#3059)
Andres Noetzli [Sat, 15 Jun 2019 17:23:33 +0000 (10:23 -0700)]
Use Ubuntu 16.04 on Travis (#3059)

Travis has started to switch to Ubuntu 16.04 [0]. We were explicitly
specifying 14.04 as the `dist` in our `.travis.yml`. This commit changes
that specification to 16.04, updates the Java version, and removes
a workaround for an old Travis issue.

[0] https://changelog.travis-ci.com/xenial-as-the-default-build-environment-99476

5 years agoAdd lemma for the range of values of str.indexof (#3054)
Andres Noetzli [Fri, 14 Jun 2019 01:39:10 +0000 (18:39 -0700)]
Add lemma for the range of values of str.indexof (#3054)

This commit adds a lemma that the value of `str.indexof(x, y, n)` must
be between -1 and `str.len(x)`.

5 years ago Shorten explanation for strings inference I_Norm_S (#3051)
Andrew Reynolds [Thu, 13 Jun 2019 18:08:15 +0000 (13:08 -0500)]
 Shorten explanation for strings inference I_Norm_S (#3051)

5 years agoFix warning (#3053)
Haniel Barbosa [Thu, 13 Jun 2019 06:33:17 +0000 (01:33 -0500)]
Fix warning (#3053)

5 years agoRefactor parser to define fewer tokens for symbols (#2936)
Andres Noetzli [Wed, 12 Jun 2019 16:07:00 +0000 (09:07 -0700)]
Refactor parser to define fewer tokens for symbols (#2936)

5 years agoDisable dumping regression for non-dumping builds (#3046)
Andres Noetzli [Wed, 12 Jun 2019 00:54:14 +0000 (17:54 -0700)]
Disable dumping regression for non-dumping builds (#3046)

`let_shadowing.smt2` uses dumping to test our printing infrastructure.
Since some builds do not support dumping, this commit disables that
regression for non-dumping builds. Additionally, it enables an error
message when trying to dump with a muzzled build and corrects the output
of `--show-config` to indicate that muzzled builds cannot dump.
Previously, the dumping output of a muzzled build was just silently
empty.

Most of the changes in `dump.cpp` are due to reformatting.

5 years agoFix compilation issue for Java bindings + CLN (#3045)
Andres Noetzli [Wed, 12 Jun 2019 00:21:54 +0000 (17:21 -0700)]
Fix compilation issue for Java bindings + CLN (#3045)

Fixes #3044. When using CLN instead of GMP, SWIG produces different Java
files for the CLN classes. The bindings expected the GMP files even when
building with CLN, so compilation failed. This commit fixes the issue by
changing the list of files depending on whether we build with CLN or
GMP.

5 years agoNA Tangent reverse implication (#3050)
Ahmed Irfan [Tue, 11 Jun 2019 23:16:01 +0000 (16:16 -0700)]
NA Tangent reverse implication (#3050)

5 years ago Minor cleaning of conflict-based instantiation (#2966)
Andrew Reynolds [Tue, 11 Jun 2019 22:30:26 +0000 (17:30 -0500)]
 Minor cleaning of conflict-based instantiation (#2966)

5 years agoDo not require sygus constructors to be flattened (#3049)
Andrew Reynolds [Tue, 11 Jun 2019 21:47:13 +0000 (16:47 -0500)]
Do not require sygus constructors to be flattened (#3049)

5 years ago Fix spurious assertion in get-value (#3052)
Andrew Reynolds [Tue, 11 Jun 2019 20:50:06 +0000 (15:50 -0500)]
 Fix spurious assertion in get-value (#3052)

5 years agoOptimization for negative concatenation membership. (#3048)
Andrew Reynolds [Mon, 10 Jun 2019 21:19:35 +0000 (16:19 -0500)]
Optimization for negative concatenation membership. (#3048)

5 years agoOptimization for strings normalize disequalities (#3047)
Andrew Reynolds [Mon, 10 Jun 2019 20:51:21 +0000 (15:51 -0500)]
Optimization for strings normalize disequalities (#3047)

5 years agoPrevent letification from shadowing variables (#3042)
Andres Noetzli [Wed, 5 Jun 2019 20:01:34 +0000 (13:01 -0700)]
Prevent letification from shadowing variables (#3042)

Fixes #3005. When printing nodes, we introduce `let` expressions on the
fly. However, when doing that, we have to be careful that we don't
shadow existing variables with the same name. When quantifiers are
involved, we do not descend into the quantifiers to avoid letifying
terms with bound variables that then go out of scope (see #1863). Thus,
to avoid shadowing variables appearing in quantifiers, we have to
collect all the variables appearing in that term to make sure that the
let does not shadow them. In #3005, the issue was caused by a `let` that
was introduced outside of a quantifier and then was shadowed in the body
of the quantifier by another `let` introduced for that body.

5 years agoDRAT-Optimization (#2971)
Alex Ozdemir [Wed, 5 Jun 2019 19:16:46 +0000 (12:16 -0700)]
DRAT-Optimization (#2971)

This commit enables DRAT-optimization, which consists of two sub-processes:
1. removing unnecessary instructions from DRAT-proofs and
2. not proving clauses which are not needed by DRAT proofs.

These changes have the effect of dramatically shortening some some bit-vector proofs. Specifically,  proofs using lemmas in the ER, DRAT, and LRAT formats, since proofs in any of these formats are derived from a (now optimized!) DRAT proof produced by CryptoMiniSat. What follows is a description of the main parts of this PR:

## DRAT Optimization

The DRAT-optimization is done by `drat-trim`, which is bundled with `drat2er`. The (new) function `ClausalBitVectorProof::optimizeDratProof` is our interface to the optimization machinery, and most of the new logic in this PR is in that function.

## CNF Representation

The ability to not prove unused clauses requires a slight architectural change as well. In particular, we need to be able to describe **which** subset of the original clause set actually needs to be proved. To facilitate this, when the clause set for CryptoMiniSat is first formed it is represented as a (a) map from clause indices to clauses and (b) a list of indices. Then, when the CNF is optimized, we temporarily store a new list of the clauses in the optimized formula. This change in representation requires a number of small tweaks throughout the code.

## Small Fixes to Signatures

When we decided to check and accept two different kinds of DRAT, some of our DRAT-checking broke. In particular, when supporting one kind of DRAT, it is okay to `fail` (crash) when a proof fails to check. If you're supporting two kinds of DRAT, crashing in response to the first checker rejecting the proof denies the second checker an opportunity to check the proof. This PR tweaks the signatures slightly (and soundly!) to do something else instead of `fail`ing.

5 years agoAdd support for SWIG 4 (#3041)
Andres Noetzli [Wed, 5 Jun 2019 16:36:40 +0000 (09:36 -0700)]
Add support for SWIG 4 (#3041)

SWIG 4 seems to change the name for `std::map<CVC4::Expr, CVC4::Expr>`
to include the implicit template argument for comparisons. To make the
code compatible with both SWIG 4.0.0 and older versions, this commit
creates an explicit instance of the template.

5 years agoEnable proof checking for QF_LRA benchmarks (#2928)
Andres Noetzli [Tue, 4 Jun 2019 23:37:27 +0000 (16:37 -0700)]
Enable proof checking for QF_LRA benchmarks (#2928)

Due to issues in the current proof code, this commit also disables proof
checking for five QF_LRA benchmarks (see issue #2855).

5 years agoAdd check that result matches benchmark status (#3028)
Andres Noetzli [Tue, 4 Jun 2019 21:48:21 +0000 (14:48 -0700)]
Add check that result matches benchmark status (#3028)

This commit adds a check to make sure that the result of a `(check-sat)`
call matches the expected result set via `(set-info :status ...)`.  In
doing so, it also fixes an issue where CVC4 would crash if asked for the
unsat core after setting the status to `unsat` but before calling
`(check-sat)` (see regression for concrete example). This happened
because CVC4 was storing the expected result and the computed result
both in the same variable (the expected result wasn't really being used
though). This commit keeps track of the expected result and the computed
result in separate variables to fix that issue.

5 years ago[SMT-COMP] No unconstrained simp for QF_LIA UC (#3039)
Andres Noetzli [Mon, 3 Jun 2019 23:15:54 +0000 (16:15 -0700)]
[SMT-COMP] No unconstrained simp for QF_LIA UC (#3039)

`--unconstrained-simp` is not compatible with unsat cores.

5 years ago[SMT-COMP] Increase sequential portfolio times (#3038)
Andres Noetzli [Mon, 3 Jun 2019 05:04:41 +0000 (22:04 -0700)]
[SMT-COMP] Increase sequential portfolio times (#3038)

This year's timeout is 40min up from 20min last year. This commit scales
the timeouts accordingly.

5 years ago[SMT-COMP 2019] Use lazy BV as backup for QF_UFBV (#3037)
Andres Noetzli [Mon, 3 Jun 2019 04:23:52 +0000 (21:23 -0700)]
[SMT-COMP 2019] Use lazy BV as backup for QF_UFBV (#3037)

We cannot Ackermannize all the QF_UFBV benchmarks due to uninterpreted
sorts. This commit adds lazy bit-blasting as a backup strategy.

5 years agoEnable SymFPU assertions in production (#3036)
Andres Noetzli [Mon, 3 Jun 2019 03:01:48 +0000 (20:01 -0700)]
Enable SymFPU assertions in production (#3036)

This commit enables SymFPU assertions in production. The reason for this
is that there are some known problems with certain bit-widths, so we
prefer to be conservative. The commit also updates the run scripts for SMT-COMP 2019 to use `--fp-exp` since we have those additional checks in place now.

5 years ago[SMT-COMP 2019] Update run script for unsat cores (#3034)
Andres Noetzli [Mon, 3 Jun 2019 02:30:10 +0000 (19:30 -0700)]
[SMT-COMP 2019] Update run script for unsat cores (#3034)

`--unconstrained-simp` is not compatible with unsat cores, so this
commit removes it for QF_LRA. `--bitblast=eager` is not compatible with
unsat cores for QF_UFBV because the dependencies are not tracked
correctly in the Ackermannization preprocessing pass, so the commit
changes the script to use the lazy BV solver instead. Strings need some
additional options to use the correct theory symbols.

5 years agoAdd check for limit of number of node children (#3035)
Andres Noetzli [Mon, 3 Jun 2019 01:54:02 +0000 (18:54 -0700)]
Add check for limit of number of node children (#3035)

This commit adds a check that makes sure that we do not try to create
nodes with more children than the maxmimum number. This can currently
happen when flattening nodes in QF_BV with lots of duplicate children.

5 years agoUpdate QF_BV options for SMT-COMP 2019. (#3033)
Aina Niemetz [Sat, 1 Jun 2019 23:40:33 +0000 (16:40 -0700)]
Update QF_BV options for SMT-COMP 2019. (#3033)

5 years ago Require that FMF model basis terms are variables (#3031)
Andrew Reynolds [Sat, 1 Jun 2019 07:39:16 +0000 (09:39 +0200)]
 Require that FMF model basis terms are variables (#3031)

The commit fixes an issue where FMF could theoretically chose interpreted function applications as "model basis terms". This triggered an incorrect model (caught by an AlwaysAssert) when the interpreted function later did not appear in a model and was chosen by FMF to be equal to a wrong value.

5 years agoFix rewriter for regular expression consume (#3029)
Andrew Reynolds [Sat, 1 Jun 2019 07:04:17 +0000 (09:04 +0200)]
Fix rewriter for regular expression consume  (#3029)

5 years agoQuote symbol when printing empty symbol name (#3025)
Andres Noetzli [Thu, 30 May 2019 18:05:42 +0000 (11:05 -0700)]
Quote symbol when printing empty symbol name (#3025)

When printing an empty symbol name, which can appear in an SMT2 file as
`||`, we were printing the empty string instead of quoting the symbol.
This commit fixes the issue and adds a regression test.

5 years agoAvoid substituting Boolean term variables (#3022)
Andres Noetzli [Mon, 27 May 2019 23:36:17 +0000 (16:36 -0700)]
Avoid substituting Boolean term variables (#3022)

Fixes #3020. Boolean terms that appear in other terms, e.g. a Boolean
array index, are replaced by `BOOLEAN_TERM_VARIABLE`s to make sure that
they are handled properly in theory combination. When doing this
replacement, an equality of the form `(= <Boolean term> <Boolean term
variable)` is added to the assertions. The problem was that
`Theory::ppAssert()` would derive a substitution when this equality was
registered. The commit fixes the problem by not allowing to add
substitutions for `BOOLEAN_TERM_VARIABLE`s.

5 years agoUpdate to symfpu 0.0.7, fixes RTI 3/5 issue (#3007)
Martin [Tue, 21 May 2019 17:49:37 +0000 (18:49 +0100)]
Update to symfpu 0.0.7, fixes RTI 3/5 issue (#3007)

Fixes #2932. fp.roundToIntegral was rounding some very small subnormals up to
between 1 and 2, which is A. wrong and B. not idempotent.  The
corresponding symfpu update fixes this as it was an overflow caused
by the unpacked significand not being able to represent an extra
significand bits.

5 years ago[SMT-COMP 2019] Update run scripts to match tracks (#3018)
Andres Noetzli [Mon, 20 May 2019 18:24:31 +0000 (11:24 -0700)]
[SMT-COMP 2019] Update run scripts to match tracks (#3018)

The "Application Track" has been renamed to "Incremental Track" this
year, so this commit renames the script accordingly and updates the name
of the CVC4 binary that the script calls to be just `cvc4`. The commit
also adds an initial script for the model validation track.

5 years agoFP: Fix regression test and enable SymFPU on Travis. (#3013)
Aina Niemetz [Sat, 18 May 2019 22:13:00 +0000 (15:13 -0700)]
FP: Fix regression test and enable SymFPU on Travis. (#3013)

5 years agoUpdate QF_NIA strategy (#3012)
Andrew Reynolds [Sat, 18 May 2019 04:07:48 +0000 (23:07 -0500)]
Update QF_NIA strategy (#3012)

5 years ago[SMT-COMP2019] Better strings configuration (#3010)
Andres Noetzli [Sat, 18 May 2019 03:35:27 +0000 (20:35 -0700)]
[SMT-COMP2019] Better strings configuration (#3010)

5 years agoSupport for incremental bit-blasting with CaDiCaL (#3006)
Andres Noetzli [Sat, 18 May 2019 02:16:55 +0000 (19:16 -0700)]
Support for incremental bit-blasting with CaDiCaL (#3006)

This commit adds support for eager bit-blasting with CaDiCaL on
incremental benchmarks. Since not all CaDiCaL versions support
incremental solving, the commit adds a CMake check that checks whether
`CaDiCaL::Solver::assume()` exists.

Note: The check uses `check_cxx_source_compiles`, which is not very
elegant but I could not find a better solution (e.g.
`check_cxx_symbol_exists()` does not seem to support methods in classes
and `check_struct_has_member()` only seems to support data members).

5 years agoFix BV ITE rewrite (#3004)
Andres Noetzli [Sat, 18 May 2019 01:47:09 +0000 (18:47 -0700)]
Fix BV ITE rewrite (#3004)

The rewrite `BvIteConstChildren` assumes that `BvIteEqualChildren` has
been applied before it runs. However, with nested ITEs, it was possible
to violate that assertion. Given `bvite(c1, bvite(c2, 0, 0), bvite(c3,
0, 0))`, `BvIteEqualChildren` would rewrite that term to `bvite(c2, 0,
0)`. The `LinearRewriteStrategy` then ran `BvIteConstChildren` on
`bvite(c2, 0, 0)` which complained about the equal children. This commit
implements a simple fix that splits the `LinearRewriteStrategy` into two
strategies to make sure that if `BvIteEqualChildren` rewrites a node, we
drop back to the `Rewriter`. This ensures that the rewrites on the
rewritten node are invoked in the correct order.

5 years agoAdd the problematic input from issue 2183 as a regression test (#3008)
Martin [Fri, 17 May 2019 23:10:19 +0000 (00:10 +0100)]
Add the problematic input from issue 2183 as a regression test (#3008)

Although CVC4's behaviour is actually correct, this is to make
things a bit clearer and prevent confusion in the future.

5 years agoFix iterators in Java API (#3000)
Andres Noetzli [Thu, 16 May 2019 00:18:48 +0000 (00:18 +0000)]
Fix iterators in Java API (#3000)

Fixes #2989. SWIG 3 seems to have an issue properly resolving
`T::const_iterator::value_type` if that type itself is a `typedef`.
This is for example the case in the `UnsatCore` class, which `typedef`s
`const_iterator` to `std::vector<Expr>::const_iterator`. As a
workaround, this commit changes the `JavaIteratorAdapter` class to take
two template parameters, one of which is the `value_type`. The commit
also adds a compile-time assertion that `T::const_iterator::value_type`
can be converted to `value_type` to avoid nasty surprises. A nice
side-effect of this solution is that explicit `typemap`s are not
necessary anymore, so they are removed. Additionally, the commit adds a
`toString()` method for the Java API of `UnsatCore` and adds examples
that show and test the iteration over the unsat core and the statistics.
Iterating over `Statistics` now returns instances of `Statistic` instead
of `Object[]`, which is a bit cleaner and requires less glue code.

5 years agocmake: Install JAR and JNI files for Java bindings. (#3002)
Mathias Preiner [Wed, 15 May 2019 23:26:06 +0000 (16:26 -0700)]
cmake: Install JAR and JNI files for Java bindings. (#3002)

Default install paths are:
  - libcvc4jni.so in /usr/lib/
  - CVC4.jar in /usr/share/java/cvc4

Fixes #2990.

5 years ago BV: Do not enable abstraction when eager bit-blasting by default. (#3001)
Aina Niemetz [Wed, 15 May 2019 20:29:00 +0000 (13:29 -0700)]
 BV: Do not enable abstraction when eager bit-blasting by default. (#3001)

5 years agoFix model of Boolean vars with eager bit-blaster (#2998)
Andres Noetzli [Wed, 15 May 2019 17:38:04 +0000 (17:38 +0000)]
Fix model of Boolean vars with eager bit-blaster (#2998)

When bit-blasting eagerly, we were not assigning values to the Boolean
variables in the `TheoryModel`. With eager bit-blasting, the BV SAT
solver gets all (converted) terms, including the Boolean ones, so
`EagerBitblaster::collectModelInfo()` is responsible for assigning
values to Boolean variables. However, it has only been assigning values
to bit-vector variables, which lead to wrong models. This commit fixes
the issue by asking the `CnfStream` for the Boolean variables, querying
the SAT solver for their value, and assigning them in the `TheoryModel`.

5 years agoFix printing of bvurem (#2963)
Andrew Reynolds [Wed, 15 May 2019 16:41:03 +0000 (11:41 -0500)]
Fix printing of bvurem (#2963)

5 years agoDisable relational triggers (#2994)
Andrew Reynolds [Fri, 10 May 2019 15:51:24 +0000 (10:51 -0500)]
Disable relational triggers (#2994)

5 years agoFixes for relational triggers (#2967)
Andrew Reynolds [Thu, 9 May 2019 14:33:22 +0000 (09:33 -0500)]
Fixes for relational triggers (#2967)

5 years agoAdd support for re.all (#2980)
Andres Noetzli [Mon, 6 May 2019 13:05:19 +0000 (06:05 -0700)]
Add support for re.all (#2980)

5 years agoSimple optimizations to core strings theory. (#2988)
Andrew Reynolds [Thu, 2 May 2019 13:35:42 +0000 (08:35 -0500)]
Simple optimizations to core strings theory. (#2988)

5 years agoFix re-elim-agg regressions (#2987)
Andrew Reynolds [Wed, 1 May 2019 17:28:08 +0000 (12:28 -0500)]
Fix re-elim-agg regressions (#2987)

5 years ago Use total versions of div/mod in re-elim-agg (#2986)
Andrew Reynolds [Wed, 1 May 2019 05:35:14 +0000 (00:35 -0500)]
 Use total versions of div/mod in re-elim-agg (#2986)

5 years agoFix concat-find regexp elimination (#2983)
Andres Noetzli [Tue, 30 Apr 2019 19:32:50 +0000 (12:32 -0700)]
Fix concat-find regexp elimination (#2983)

5 years agoRemove stoi solve rewrite (#2985)
Andrew Reynolds [Tue, 30 Apr 2019 19:11:16 +0000 (14:11 -0500)]
Remove stoi solve rewrite (#2985)

5 years agoFix use of APPLY kind in examples (#2984)
Andres Noetzli [Tue, 30 Apr 2019 11:12:47 +0000 (04:12 -0700)]
Fix use of APPLY kind in examples (#2984)

5 years agoEliminate APPLY kind (#2976)
Andrew Reynolds [Tue, 30 Apr 2019 01:27:20 +0000 (20:27 -0500)]
Eliminate APPLY kind (#2976)

5 years agoOptimization for evaluation with unfolding (#2979)
Andrew Reynolds [Mon, 29 Apr 2019 21:40:31 +0000 (16:40 -0500)]
Optimization for evaluation with unfolding (#2979)

5 years agoNew C++ API: Clean up API: mkVar vs mkConst vs mkBoundVar. (#2977)
Aina Niemetz [Fri, 26 Apr 2019 01:02:57 +0000 (18:02 -0700)]
New C++ API: Clean up API: mkVar vs mkConst vs mkBoundVar. (#2977)

This cleans up naming of API functions to create first-order constants and variables.

mkVar -> mkConst
mkBoundVar -> mkVar
declareConst is redundant (= mkConst) and thus, in an effort to avoid redundancy, removed.

Note that we want to avoid redundancy in order to reduce code duplication and maintenance
overhead (we do not allow nested API calls, since this is problematic when tracing API calls).

5 years agoFix compiler warning. (#2975)
Aina Niemetz [Thu, 25 Apr 2019 03:10:47 +0000 (20:10 -0700)]
Fix compiler warning. (#2975)

5 years agoDo not use __ prefix for header guards. (#2974)
Mathias Preiner [Wed, 24 Apr 2019 22:39:24 +0000 (15:39 -0700)]
Do not use __ prefix for header guards. (#2974)

Fixes 2887.

5 years agoDco fix (#2973)
Clark Barrett [Wed, 24 Apr 2019 21:39:08 +0000 (14:39 -0700)]
Dco fix (#2973)

5 years agoREADME: Remove project leaders, history.
Aina Niemetz [Wed, 24 Apr 2019 18:46:33 +0000 (11:46 -0700)]
README: Remove project leaders, history.

5 years agoCONTRIBUTING: Fix project leaders link.
Aina Niemetz [Wed, 24 Apr 2019 18:39:12 +0000 (11:39 -0700)]
CONTRIBUTING: Fix project leaders link.

5 years ago[BV] An option for SAT proof optimization (#2915)
Alex Ozdemir [Tue, 23 Apr 2019 22:58:57 +0000 (15:58 -0700)]
[BV] An option for SAT proof optimization (#2915)

* [BV] An option for SAT proof optimization

The option doesn't **do** anything yet, but exists.

* CopyPaste Fix: BvOptimizeSatProof documentation

It was the documentation for a different option. Now it has been
updated.

* Fix Typos per Mathias' review.

Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
5 years agoRefactor normal forms in strings (#2897)
Andrew Reynolds [Tue, 23 Apr 2019 18:40:27 +0000 (13:40 -0500)]
Refactor normal forms in strings (#2897)

5 years agoAdd CONTRIBUTING file. (#2968)
Aina Niemetz [Mon, 22 Apr 2019 23:32:25 +0000 (16:32 -0700)]
Add CONTRIBUTING file. (#2968)

5 years agoFail fast strategy for propagating instances (#2939)
Andrew Reynolds [Thu, 18 Apr 2019 19:45:39 +0000 (14:45 -0500)]
Fail fast strategy for propagating instances (#2939)

5 years ago Less aggressive caching in equality engine when proofs are enabled (#2964)
Andrew Reynolds [Thu, 18 Apr 2019 19:07:49 +0000 (14:07 -0500)]
 Less aggressive caching in equality engine when proofs are enabled (#2964)

5 years agoCache explanations in the equality engine (#2937)
Andrew Reynolds [Wed, 17 Apr 2019 21:35:51 +0000 (16:35 -0500)]
Cache explanations in the equality engine (#2937)

5 years agoMore use of isClosure (#2959)
Andrew Reynolds [Wed, 17 Apr 2019 17:42:11 +0000 (12:42 -0500)]
More use of isClosure  (#2959)

5 years agoFix extended function decomposition (#2960)
Andrew Reynolds [Wed, 17 Apr 2019 15:26:46 +0000 (10:26 -0500)]
Fix extended function decomposition (#2960)

Fixes #2958.

The issue was: we had substr(x,0,2) in R, and the "derivable substitution" modifed this to substr(substr(x,0,2),0,2) in R, since substr(x,0,2) was the representative of x (which is a bad choice, but regardless is legal). Then decomposition inference asked "can i reduce substr(substr(x,0,2),0,2) in R"? It determines substr(substr(x,0,2),0,2) in R rewrites to substr(x,0,2) in R, which is already true. However, substr(x,0,2) in R was what we started with.

The fix makes things much more conservative: we never mark extended functions reduced based on decomposition, since there isnt a strong argument based on an ordering.

5 years agoAdd interface for term enumeration (#2956)
Andrew Reynolds [Tue, 16 Apr 2019 20:06:00 +0000 (15:06 -0500)]
Add interface for term enumeration (#2956)

5 years agoMake bv{add,mul,and,or,xor,xnor} left-associative (#2955)
Andres Noetzli [Tue, 16 Apr 2019 19:11:37 +0000 (12:11 -0700)]
Make bv{add,mul,and,or,xor,xnor} left-associative (#2955)

The most recent version of SMT-LIB defines bv{add,mul,and,or,xor,xnor}
[0, 1] as left-associative. CVC4 treats all but bvxnor as having
variable arity anyway but the arity check was too strict when using
`--strict-parsing`.  This commit changes the strict parsing check. For
bvxnor, it adds code to the parser that expands an application of bvxnor
into multiple applications of a binary bvxnor if needed.

References:
[0] http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml (bvand,
bvor, bvadd, bvmul)
[1] http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV (bvxor, bvxnor)

5 years agoStratify enumerative instantiation (#2954)
Andrew Reynolds [Tue, 16 Apr 2019 16:53:45 +0000 (11:53 -0500)]
Stratify enumerative instantiation (#2954)

5 years agoMinor simplifications to theory quantifiers (#2953)
Andrew Reynolds [Tue, 16 Apr 2019 15:38:35 +0000 (10:38 -0500)]
Minor simplifications to theory quantifiers (#2953)

5 years agoCheck for rt library in configuration -- support for glibc<2.17 (#2854)
makaimann [Tue, 16 Apr 2019 00:17:29 +0000 (17:17 -0700)]
Check for rt library in configuration -- support for glibc<2.17 (#2854)

This is a minor fix for systems with glibc version < 2.17. In that case, we need to link with `-lrt` according to the clock_gettime man page.

5 years agoInitial version of run scripts for SMT-COMP 2019 (#2951)
Andres Noetzli [Mon, 15 Apr 2019 22:03:00 +0000 (15:03 -0700)]
Initial version of run scripts for SMT-COMP 2019 (#2951)

For now, they are just copies of the 2018 version of the scripts.

5 years agoReferring to prerelease 1.8 (#2943)
Haniel Barbosa [Fri, 12 Apr 2019 21:16:33 +0000 (16:16 -0500)]
Referring to prerelease 1.8 (#2943)

5 years ago Eliminate Boolean ITE within terms, fixes 2947 (#2949)
Andrew Reynolds [Thu, 11 Apr 2019 18:06:08 +0000 (13:06 -0500)]
 Eliminate Boolean ITE within terms, fixes 2947 (#2949)

5 years agoRemoving references to cvc4-bugs@... (#2945)
Haniel Barbosa [Tue, 9 Apr 2019 16:14:31 +0000 (11:14 -0500)]
Removing references to cvc4-bugs@... (#2945)

5 years ago"prerelease -> release" in INSTALL (#2944)
Haniel Barbosa [Tue, 9 Apr 2019 00:55:50 +0000 (19:55 -0500)]
"prerelease -> release" in INSTALL (#2944)

5 years agoFix email address of the bugs email list and delete obsolete RELEASE-NOTES.
Aina Niemetz [Tue, 9 Apr 2019 00:11:57 +0000 (17:11 -0700)]
Fix email address of the bugs email list and delete obsolete RELEASE-NOTES.

5 years agofix copyright year in configuration file (#2942)
Haniel Barbosa [Mon, 8 Apr 2019 16:26:58 +0000 (11:26 -0500)]
fix copyright year in configuration file (#2942)

5 years agoprerelease -> release (#2941)
Haniel Barbosa [Fri, 5 Apr 2019 21:02:41 +0000 (16:02 -0500)]
prerelease -> release (#2941)

5 years agoFix another corner case of datatypes+PBE (#2938)
Andrew Reynolds [Fri, 5 Apr 2019 20:31:20 +0000 (15:31 -0500)]
Fix another corner case of datatypes+PBE (#2938)

5 years agofix fp issue (#2940)
Haniel Barbosa [Fri, 5 Apr 2019 19:01:33 +0000 (14:01 -0500)]
fix fp issue (#2940)

5 years agoSatClauseSetHashFunction (#2916)
Alex Ozdemir [Fri, 5 Apr 2019 17:03:05 +0000 (10:03 -0700)]
SatClauseSetHashFunction (#2916)

* SatClauseHashFunction

Added to the same file as SatLiteralHashFunction.

* clang-format

Thanks Andres!

5 years agoadding sygus news (#2934)
Haniel Barbosa [Thu, 4 Apr 2019 18:30:27 +0000 (13:30 -0500)]
adding sygus news (#2934)

5 years agoIgnoring FP benchmarks with "unsafe" sizes unless option (#2931)
Haniel Barbosa [Thu, 4 Apr 2019 17:31:21 +0000 (12:31 -0500)]
Ignoring FP benchmarks with "unsafe" sizes unless option (#2931)

5 years agoUpdate release notes and lib version (#2933)
Haniel Barbosa [Thu, 4 Apr 2019 02:06:25 +0000 (21:06 -0500)]
Update release notes and lib version (#2933)

5 years agoUpdate copyright headers.
Aina Niemetz [Wed, 3 Apr 2019 22:54:55 +0000 (15:54 -0700)]
Update copyright headers.