cvc5.git
6 years agoCleanup and additions for candidate generator (#2173)
Andrew Reynolds [Fri, 20 Jul 2018 23:42:25 +0000 (01:42 +0200)]
Cleanup and additions for candidate generator (#2173)

6 years ago sygusComp2018: minor changes to repair constant utility (#2110)
Andrew Reynolds [Fri, 20 Jul 2018 20:34:18 +0000 (22:34 +0200)]
 sygusComp2018: minor changes to repair constant utility (#2110)

6 years ago sygusComp2018: pbe multi-enumerator fairness option (#2178)
Andrew Reynolds [Tue, 17 Jul 2018 23:51:28 +0000 (01:51 +0200)]
 sygusComp2018: pbe multi-enumerator fairness option (#2178)

6 years agoRefactor sep-pre-skolem-emp preprocessing pass
yoni206 [Tue, 17 Jul 2018 21:20:46 +0000 (14:20 -0700)]
Refactor sep-pre-skolem-emp preprocessing pass

6 years agoMinor cleanup and fixes for conflict-based instantiation (#2123)
Andrew Reynolds [Tue, 17 Jul 2018 17:53:14 +0000 (19:53 +0200)]
Minor cleanup and fixes for conflict-based instantiation (#2123)

6 years agoDo extended rewrite on results of quantifier elimination. (#2119)
Andrew Reynolds [Tue, 17 Jul 2018 17:07:22 +0000 (19:07 +0200)]
Do extended rewrite on results of quantifier elimination. (#2119)

6 years ago Purify applications of exp to transcendental arguments (#2097)
Andrew Reynolds [Tue, 17 Jul 2018 16:25:13 +0000 (18:25 +0200)]
 Purify applications of exp to transcendental arguments (#2097)

6 years ago sygusComp2018: update policies for solution reconstruction (#2109)
Andrew Reynolds [Tue, 17 Jul 2018 15:37:03 +0000 (17:37 +0200)]
 sygusComp2018: update policies for solution reconstruction (#2109)

6 years agosygusComp2018: Improvements to datatypes sygus solver (#2177)
Andrew Reynolds [Tue, 17 Jul 2018 14:17:43 +0000 (16:17 +0200)]
sygusComp2018: Improvements to datatypes sygus solver (#2177)

6 years agosygusComp 2018: updates to sygus term database (#2170)
Andrew Reynolds [Tue, 17 Jul 2018 11:02:32 +0000 (13:02 +0200)]
sygusComp 2018: updates to sygus term database (#2170)

6 years agoAvoid ambiguous overloads in BitVector (#2169)
Andres Noetzli [Sun, 15 Jul 2018 11:25:57 +0000 (04:25 -0700)]
Avoid ambiguous overloads in BitVector (#2169)

`long` is a 32-bit integer on Windows. CVC4's BitVector class had a
constructor for `unsigned int` and `unsigned long`, which lead to issues
with the new CVC4 C++ API because the two constructors were ambiguous
overloads. This commit changes the constructors to use `uint32_t` and
`uint64_t`, which are plattform independent and more explicit (mirroring

6 years agoexportTo only if needed for --sygus-rr-synth-check (#2168)
Andres Noetzli [Sat, 14 Jul 2018 08:45:58 +0000 (01:45 -0700)]
exportTo only if needed for --sygus-rr-synth-check (#2168)

6 years agosygusComp2018: update semantics for declare-fun in sygus. (#2102)
Andrew Reynolds [Sat, 14 Jul 2018 08:08:11 +0000 (10:08 +0200)]
sygusComp2018: update semantics for declare-fun in sygus. (#2102)

6 years agoFix and improve grammar normalization for any constant. (#2101)
Andrew Reynolds [Fri, 13 Jul 2018 22:30:04 +0000 (00:30 +0200)]
Fix and improve grammar normalization for any constant. (#2101)

6 years agoProperly clean up assertion stack in CnfProof (#2147)
Andres Noetzli [Fri, 13 Jul 2018 20:24:43 +0000 (13:24 -0700)]
Properly clean up assertion stack in CnfProof (#2147)

Fixes issue #2137. CnfProof has a stack of assertions that are being
converted to clauses. Previously, it could happen that while an
assertion was being added, TheoryProxy::explainPropagation() would be
called from Solver::reason() and push an assertion to the stack that was
then not removed. This lead to a clause id of the assertion being
associated with the explanation instead, which in turn could lead to a
wrong unsat core. This commit identifies two cases where
TheoryProxy::explainPropagation() is called without cleaning up the
assertion stack afterwards. It also adds an assertion that the assertion
stack must be empty when we are getting the unsat core.

6 years ago sygusComp2018: optimization for collect model info (#2105)
Andrew Reynolds [Fri, 13 Jul 2018 15:36:01 +0000 (17:36 +0200)]
 sygusComp2018: optimization for collect model info (#2105)

6 years agoNew C++ API: Minor reorder. (#2163)
Aina Niemetz [Fri, 13 Jul 2018 10:04:49 +0000 (03:04 -0700)]
New C++ API: Minor reorder. (#2163)

6 years agoNew C++ API: Implementation of datatype classes. (#2142)
Aina Niemetz [Fri, 13 Jul 2018 08:57:24 +0000 (01:57 -0700)]
New C++ API: Implementation of datatype classes. (#2142)

6 years agoNew C++ API: Implementation of Solver class: Consts handling. (#2145)
Aina Niemetz [Fri, 13 Jul 2018 08:06:18 +0000 (01:06 -0700)]
New C++ API: Implementation of Solver class: Consts handling. (#2145)

6 years agoMove rewrite to pass (#2128)
Caleb Donovick [Wed, 11 Jul 2018 00:27:16 +0000 (17:27 -0700)]
Move rewrite to pass (#2128)

6 years agoAdd more sophisticated floating-point sampler (#2155)
Andres Noetzli [Sun, 8 Jul 2018 20:38:45 +0000 (13:38 -0700)]
Add more sophisticated floating-point sampler (#2155)

This commit adds a floating-point sampler inspired by PyMPF [0]. It also
creates a new Sampler class that can be used for creating random values
of different sorts (currently BV and FP values).

[0] https://github.com/florianschanda/PyMPF

6 years ago sygusComp2018: improve extended rewriter for Bool (#2107)
Andrew Reynolds [Sat, 7 Jul 2018 06:49:11 +0000 (07:49 +0100)]
 sygusComp2018: improve extended rewriter for Bool (#2107)

6 years agoSplit ext theory to own file and document (#1809)
Andrew Reynolds [Fri, 6 Jul 2018 19:58:31 +0000 (20:58 +0100)]
Split ext theory to own file and document (#1809)

6 years agoFeature/fp rewrite improvement (#2154)
Martin [Fri, 6 Jul 2018 18:22:57 +0000 (19:22 +0100)]
Feature/fp rewrite improvement (#2154)

6 years agoNew C++ API: Implementation of Solver class: Term handling. (#2144)
Aina Niemetz [Fri, 6 Jul 2018 17:26:00 +0000 (10:26 -0700)]
New C++ API: Implementation of Solver class: Term handling. (#2144)

6 years agoNew C++ API: Implementation of Solver class: Sort handling. (#2143)
Aina Niemetz [Fri, 6 Jul 2018 16:53:21 +0000 (09:53 -0700)]
New C++ API: Implementation of Solver class: Sort handling. (#2143)

6 years agoAdd option for timeout for rewrite candidate check (#2156)
Andres Noetzli [Fri, 6 Jul 2018 11:03:58 +0000 (04:03 -0700)]
Add option for timeout for rewrite candidate check (#2156)

6 years agosygusComp2018: simplify beta reduction in uf rewriter. (#2106)
Andrew Reynolds [Fri, 6 Jul 2018 07:20:23 +0000 (08:20 +0100)]
sygusComp2018: simplify beta reduction in uf rewriter. (#2106)

This is PR 8/18 from the sygus comp 2018 branch (https://github.com/ajreynol/CVC4/tree/sygusComp2018-2).

I am not sure how it is possible in any circumstance that the complication in the comment I am deleting would ever happen, without doing something very strange. I think it is referring to some sort of inter-dependence between macro expansion + beta-reductions. This should not concern the rewriter. Here is the commit that introduced it: bdaa304.

6 years ago Make string length lemmas more robust to rewriting (#2150)
Andrew Reynolds [Thu, 5 Jul 2018 16:22:53 +0000 (17:22 +0100)]
 Make string length lemmas more robust to rewriting (#2150)

6 years agoMinor changes to sygus-rr utilities to support floating point rewrites (#2148)
Andrew Reynolds [Thu, 5 Jul 2018 03:23:19 +0000 (04:23 +0100)]
Minor changes to sygus-rr utilities to support floating point rewrites (#2148)

6 years agosygusComp2018: Improve string rewriter (#2141)
Andres Noetzli [Thu, 5 Jul 2018 02:32:29 +0000 (19:32 -0700)]
sygusComp2018: Improve string rewriter (#2141)

6 years agoMore cleanup in strings (#2138)
Andrew Reynolds [Wed, 4 Jul 2018 15:34:17 +0000 (16:34 +0100)]
More cleanup in strings (#2138)

6 years agoNew C++ API: Implementation of datatype declaration classes. (#2136)
Aina Niemetz [Wed, 4 Jul 2018 15:10:27 +0000 (08:10 -0700)]
New C++ API: Implementation of datatype declaration classes. (#2136)

6 years agoReorganize candidate rewrite rule filtering (#2116)
Andrew Reynolds [Wed, 4 Jul 2018 13:31:14 +0000 (14:31 +0100)]
Reorganize candidate rewrite rule filtering (#2116)

6 years agoRemove unused CDVector (#2139)
Andres Noetzli [Wed, 4 Jul 2018 10:58:24 +0000 (03:58 -0700)]
Remove unused CDVector (#2139)

6 years agoNew C++ API: Implementation of OpTerm. (#2132)
Aina Niemetz [Wed, 4 Jul 2018 08:31:02 +0000 (01:31 -0700)]
New C++ API: Implementation of OpTerm. (#2132)

6 years agoFix fmf-fun for non-equality function definitions (#2134)
Andrew Reynolds [Wed, 4 Jul 2018 05:21:01 +0000 (00:21 -0500)]
Fix fmf-fun for non-equality function definitions (#2134)

Fixes #2133. In that issue, a quantifiers rewrite triggered a model-unsoundness in fmf-fun. The rewrite made a function definition have an ITE at top-level instead of equality. The corrected code was model-unsound, since it assumed that quantified formulas that are not EQUAL can be ignored.

6 years agoNew C++ API: Implementation of Term. (#2131)
Aina Niemetz [Tue, 3 Jul 2018 16:27:59 +0000 (09:27 -0700)]
New C++ API: Implementation of Term. (#2131)

6 years agoNew C++ API: Implementation of Kind maps. (#2130)
Aina Niemetz [Tue, 3 Jul 2018 15:59:35 +0000 (08:59 -0700)]
New C++ API: Implementation of Kind maps. (#2130)

6 years agoFix datatypes example: nil constructor was missing. (#2135)
Aina Niemetz [Tue, 3 Jul 2018 11:49:38 +0000 (04:49 -0700)]
Fix datatypes example: nil constructor was missing. (#2135)

6 years agosygusComp2018: update sygus-related options setting in smt engine (#2108)
Andrew Reynolds [Tue, 3 Jul 2018 02:42:55 +0000 (21:42 -0500)]
sygusComp2018: update sygus-related options setting in smt engine (#2108)

6 years agoRemove miscellaneous dead and unused code from quantifiers (#2121)
Andrew Reynolds [Tue, 3 Jul 2018 01:08:53 +0000 (20:08 -0500)]
Remove miscellaneous dead and unused code from quantifiers (#2121)

6 years agoAdd regression test for issue #1986 (#2114)
Andres Noetzli [Tue, 3 Jul 2018 00:45:04 +0000 (17:45 -0700)]
Add regression test for issue #1986 (#2114)

The issue is not triggered anymore after PR #2059 but the test case is
good to have for changes in MiniSat code.

6 years agoRefactor ApplySubsts preprocessing pass. (#2120)
Aina Niemetz [Mon, 2 Jul 2018 23:51:03 +0000 (16:51 -0700)]
Refactor ApplySubsts preprocessing pass. (#2120)

6 years agoNew C++ API: Implementation of Sort. (#2122)
Aina Niemetz [Mon, 2 Jul 2018 23:16:02 +0000 (16:16 -0700)]
New C++ API: Implementation of Sort. (#2122)

6 years agoRemove some dead code from theory strings (#2125)
Andrew Reynolds [Mon, 2 Jul 2018 21:47:50 +0000 (16:47 -0500)]
Remove some dead code from theory strings (#2125)

6 years agoAdd missing include (#2127)
Caleb Donovick [Mon, 2 Jul 2018 21:26:58 +0000 (14:26 -0700)]
Add missing include (#2127)

6 years agoModify cegqi heuristic for finite datatypes (#2126)
Andrew Reynolds [Mon, 2 Jul 2018 17:45:48 +0000 (12:45 -0500)]
Modify cegqi heuristic for finite datatypes  (#2126)

6 years agoImprove error message. (#2124)
Andrew Reynolds [Mon, 2 Jul 2018 17:20:10 +0000 (12:20 -0500)]
Improve error message. (#2124)

6 years agoUse evaluator in sygus sampler. (#2117)
Andrew Reynolds [Fri, 29 Jun 2018 18:39:59 +0000 (13:39 -0500)]
Use evaluator in sygus sampler. (#2117)

* Use evaluator for sygus sampler.

* Format

6 years agoNew C++ API: Implementation of Result. (#2112)
Aina Niemetz [Fri, 29 Jun 2018 00:54:33 +0000 (17:54 -0700)]
New C++ API: Implementation of Result. (#2112)

6 years agoRemove comment about model value hack (#2118)
Andrew Reynolds [Thu, 28 Jun 2018 23:11:23 +0000 (18:11 -0500)]
Remove comment about model value hack (#2118)

This fixes #821.

For some background, some special cases were added to equality engine and theory engine a few years ago to handle constants properly. As a result of these changes, a comment in the code was added about a HACK for getModelValue, but the code is completely reasonable looking to me (it says that the model value of a constant is itself). This PR removes that comment.

From what I can tell issue #821 can be closed.

6 years ago sygusComp2018: optimization for invariance test (#2104)
Andrew Reynolds [Thu, 28 Jun 2018 20:44:45 +0000 (15:44 -0500)]
 sygusComp2018: optimization for invariance test (#2104)

6 years agoFix stale reference in MiniSat when generating UC (#2113)
Andres Noetzli [Thu, 28 Jun 2018 19:18:47 +0000 (12:18 -0700)]
Fix stale reference in MiniSat when generating UC (#2113)

In MiniSat's analyze(), we were taking a reference of a clause that
could be invalidated by a call to resolveOutUnit(). resolveOutUnit() can
lead to allocation of clauses which in turn can lead to clauses being
reallocated, making the reference stale. The commit encloses the
reference in a code block that makes the lifetime of the reference more
obvious and removes uses of the potentially stale reference.

6 years agoDo not rename uninterpreted constants (#2098)
Andrew Reynolds [Thu, 28 Jun 2018 18:53:36 +0000 (13:53 -0500)]
Do not rename uninterpreted constants (#2098)

6 years agoSplit and document ceg theory instantiators (#2094)
Andrew Reynolds [Thu, 28 Jun 2018 15:43:08 +0000 (10:43 -0500)]
Split and document ceg theory instantiators (#2094)

6 years agoHeader for new C++ API. (#1697)
Aina Niemetz [Wed, 27 Jun 2018 21:00:58 +0000 (14:00 -0700)]
Header for new C++ API. (#1697)

6 years agoSynthesize candidate-rewrites from standard inputs (#1918)
Andrew Reynolds [Wed, 27 Jun 2018 19:12:17 +0000 (14:12 -0500)]
Synthesize candidate-rewrites from standard inputs (#1918)

6 years agosygusComp2018: add scripts. (#2103)
Andrew Reynolds [Tue, 26 Jun 2018 23:59:28 +0000 (18:59 -0500)]
sygusComp2018: add scripts. (#2103)

6 years agosygusComp2018: Add evaluator (#2090)
Andres Noetzli [Tue, 26 Jun 2018 23:09:03 +0000 (16:09 -0700)]
sygusComp2018: Add evaluator (#2090)

This commit adds the Evaluator class that can be used to quickly
evaluate terms under a given substitution without going through the
rewriter. This has been shown to lead to significant performance
improvements on SyGuS PBE problems with a large number of inputs because
candidate solutions are evaluated on those inputs. With this commit, the
evaluator only gets called from the SyGuS solver but there are
potentially other places in the code that could profit from it.

6 years agoAdd casc j9 tfn script (#2100)
Andrew Reynolds [Tue, 26 Jun 2018 22:32:30 +0000 (17:32 -0500)]
Add casc j9 tfn script (#2100)

6 years ago Disable uf symmetry breaker in incremental mode (#2091)
Andrew Reynolds [Tue, 26 Jun 2018 22:11:31 +0000 (17:11 -0500)]
 Disable uf symmetry breaker in incremental mode (#2091)

6 years agoFix assertion for relational triggers (#2096)
Andrew Reynolds [Tue, 26 Jun 2018 20:45:27 +0000 (15:45 -0500)]
Fix assertion for relational triggers (#2096)

6 years ago Do not dagify printing over binders (#2093)
Andrew Reynolds [Tue, 26 Jun 2018 19:52:34 +0000 (14:52 -0500)]
 Do not dagify printing over binders (#2093)

6 years agoRemove unnecessary code in register quantifier internal (#2092)
Andrew Reynolds [Tue, 26 Jun 2018 17:58:25 +0000 (12:58 -0500)]
Remove unnecessary code in register quantifier internal (#2092)

6 years agoMinor improvements in SMT2 and CVC printers (#2089)
Andres Noetzli [Tue, 26 Jun 2018 02:12:23 +0000 (19:12 -0700)]
Minor improvements in SMT2 and CVC printers (#2089)

This commit adds support for string concatenation, charat, and length
operators in the CVC printer and support for re.nostr, re.allchar, and
insert into a set in the SMT2 printer.

6 years agoBump library version to 1.7-prerelease.
Aina Niemetz [Tue, 26 Jun 2018 01:07:55 +0000 (18:07 -0700)]
Bump library version to 1.7-prerelease.

6 years agoCutting release 1.6.
Aina Niemetz [Tue, 26 Jun 2018 00:21:27 +0000 (17:21 -0700)]
Cutting release 1.6.

6 years agoMore updates to NEWS for 1.6.
Aina Niemetz [Mon, 25 Jun 2018 21:27:20 +0000 (14:27 -0700)]
More updates to NEWS for 1.6.

6 years agoUpdate AUTHORS, NEWS, README, RELEASE-NOTES and THANKS file for 1.6.
Aina Niemetz [Mon, 25 Jun 2018 20:51:11 +0000 (13:51 -0700)]
Update AUTHORS, NEWS, README, RELEASE-NOTES and THANKS file for 1.6.

6 years agoBump library version.
Aina Niemetz [Fri, 22 Jun 2018 20:12:07 +0000 (13:12 -0700)]
Bump library version.

6 years agoUpdate copyright year in configuration.cpp:copyright().
Aina Niemetz [Fri, 22 Jun 2018 20:07:43 +0000 (13:07 -0700)]
Update copyright year in configuration.cpp:copyright().

6 years agoUpdated copyright headers.
Aina Niemetz [Fri, 22 Jun 2018 20:04:40 +0000 (13:04 -0700)]
Updated copyright headers.

6 years agoDo not use git blame -C in get-authors (too many false positives).
Aina Niemetz [Fri, 22 Jun 2018 19:58:13 +0000 (12:58 -0700)]
Do not use git blame -C in get-authors (too many false positives).

6 years agoFix update-copyright script for files without a header.
Aina Niemetz [Fri, 22 Jun 2018 19:27:27 +0000 (12:27 -0700)]
Fix update-copyright script for files without a header.

6 years agoAdded Makai and Yoni to get-authors script.
Aina Niemetz [Fri, 22 Jun 2018 18:15:39 +0000 (11:15 -0700)]
Added Makai and Yoni to get-authors script.

6 years agoRemove parentheses for prefix ops without args (#2082)
Andres Noetzli [Mon, 25 Jun 2018 17:57:26 +0000 (10:57 -0700)]
Remove parentheses for prefix ops without args (#2082)

In the CVC printer, function definitions without arguments are printed
like constants but when actually using that function we were printing in
the form of `x()`.

For example:

```
(set-logic QF_BV)
(define-fun x1480 () Bool true)
(define-fun x2859 () Bool true)
(define-fun x2387 () Bool x2859)
(check-sat)
```

Was dumped as:

```
OPTION "incremental" false;
OPTION "logic" "QF_BV";
x1480 : BOOLEAN = TRUE;
x2859 : BOOLEAN = TRUE;
x2387 : BOOLEAN = x2859();
```

This commit removes these parentheses when prefix functions with zero arguments
are printed, so the example above becomes:

```
OPTION "incremental" false;
OPTION "logic" "QF_BV";
x1480 : BOOLEAN = TRUE;
x2859 : BOOLEAN = TRUE;
x2387 : BOOLEAN = x2859();
```

6 years agoFix warnings and enable -Wnon-virtual-dtor warning (#2079)
Andres Noetzli [Thu, 21 Jun 2018 03:28:50 +0000 (20:28 -0700)]
Fix warnings and enable -Wnon-virtual-dtor warning (#2079)

This commit fixes warnings for an unused variable, comparison of two
different types and add virtual destructors to classes that were
previously missing them. It also enables the -Wnon-virtual-dtor warning
which warns about any class definition with virtual methods that does
not have a virtual destructor (except if the destructor is protected).
This flag is supported by both clang and GCC and not enabled by default.

6 years agoCheck unsat cores in regressions also without LFSC (#1955)
Andres Noetzli [Thu, 21 Jun 2018 02:37:28 +0000 (19:37 -0700)]
Check unsat cores in regressions also without LFSC (#1955)

When moving the LFSC checker out of the CVC4 repository in commit
dfa69ff98a14fcc0f2387e59a0c9994ef440e7d0, we disabled checking unsat
cores when CVC4 was compiled without LFSC due to the complexity of the
regression script. This commit changes the new(-ish) Python regression
script to check unsat cores even when CVC4 was compiled without LFSC.
This is done by having two separate flags, --with-lfsc and
--enable-proof, for the regression script that mirror the configuration
flags. The regression script performs unsat cores and proofs checks
based on those flags.

Additionally, this commit changes the regression script to check proofs
and unsat cores in two independent runs. Testing them in a single run
masked issues #1953 and #1954.

6 years agoUpdated installation instructions to mention autogen.sh (#1477)
Aina Niemetz [Thu, 21 Jun 2018 02:01:28 +0000 (19:01 -0700)]
Updated installation instructions to mention autogen.sh (#1477)

6 years agoResolve CVC4_USE_SYMFPU in headers at config-time (#2077)
Andres Noetzli [Wed, 20 Jun 2018 20:32:18 +0000 (13:32 -0700)]
Resolve CVC4_USE_SYMFPU in headers at config-time (#2077)

As described in issue #2013, we had `#ifdef CVC4_USE_SYMFPU` conditions
in floatingpoint.h, which was problematic when installing the header
files because the definition of `CVC4_USE_SYMFPU` was a compile-flag and
simply including the header files in another project would be missing
that definition. This commit moves floatingpoint.h to a template file
floatingpoint.h.in and substitutes the value of `CVC4_USE_SYMFPU` at
configure-time when generating floatingpoint.h (this is the same
solution that integer.h and rational.h use). I have tested the fix with
the examples provided in #2013 and they work.

6 years agoDisable solving non-linear BV literals by default (#2070)
Andrew Reynolds [Fri, 15 Jun 2018 18:28:45 +0000 (13:28 -0500)]
Disable solving non-linear BV literals by default (#2070)

6 years agoWorkaround for incremental unsat cores (#1962)
Andres Noetzli [Wed, 13 Jun 2018 22:16:24 +0000 (15:16 -0700)]
Workaround for incremental unsat cores (#1962)

This commit implements a workaround for computing unsat cores while
doing incremental solving to address #1349. Currently, our resolution
proofs do not handle clauses with a lower-than-assertion-level correctly
because the resolution proofs for them get removed when popping the
context but the SAT solver keeps using them. The workaround changes the
behavior of the SAT solver to add clauses always at the current level if
incremental solving and unsat cores are enabled. This makes sure that
all learned clauses are removed when we pop below the level that they
were learned at. This may degrade performance because the SAT solver has
to relearn clauses.

6 years agoFix simple regexp consume (#2066)
Andrew Reynolds [Wed, 13 Jun 2018 18:36:22 +0000 (13:36 -0500)]
Fix simple regexp consume (#2066)

6 years agoDisable unconstrainedSimp pass when proofs enabled (#1976)
Andres Noetzli [Wed, 13 Jun 2018 17:04:34 +0000 (10:04 -0700)]
Disable unconstrainedSimp pass when proofs enabled (#1976)

Currently, we may end up enabling the unconstrainedSimp pass when proofs
are enabled because the check that this pass is disabled happens before
a check for automatically enabling it. This lead to issues when running
for example on regress0/aufbv/bug00.smt with --check-proofs. This commit
moves the code for automatically enabling the pass to only be run if
proofs and unsat cores are disabled. Note: This commit is mostly a
simple code move but formatting in setDefaults was a bit off, so there
are a lot of formatting changes.

6 years agoFix strip constant endpoint for ITOS in strings rewriter (#2067)
Andrew Reynolds [Tue, 12 Jun 2018 20:22:15 +0000 (15:22 -0500)]
Fix strip constant endpoint for ITOS in strings rewriter (#2067)

6 years agoFix equality conflicts reported by FP (#2064)
Andrew Reynolds [Mon, 11 Jun 2018 02:43:14 +0000 (21:43 -0500)]
Fix equality conflicts reported by FP (#2064)

6 years agoDisable test that fails in competition mode (#2063)
Andres Noetzli [Sun, 10 Jun 2018 02:13:28 +0000 (19:13 -0700)]
Disable test that fails in competition mode (#2063)

Commit 106e764a04e4099cc36d13de9cec47cbf717b6cc missed one test case.
This commit disables that test case for the competition build.

6 years agoAdd flag to skip regression if feature enabled (#2062)
Andres Noetzli [Sat, 9 Jun 2018 06:16:13 +0000 (23:16 -0700)]
Add flag to skip regression if feature enabled (#2062)

This commit adds the option of skipping regressions when a specified
feature is enabled. It also changes some of the regression tests to be
skipped when it is a competition build because regressions fail
otherwise. In the tests changed in this commit, we do not care about
reproducing error messages in a competition build, so we can skip them.

6 years agoReset decisions at SAT level after solving (#2059)
Andres Noetzli [Sat, 9 Jun 2018 04:05:01 +0000 (21:05 -0700)]
Reset decisions at SAT level after solving (#2059)

Some quick background: CVC4 has two primary contexts: the assertion
context (which corresponds to the push/pops issued by the user) and the
decision/SAT context (which corresponds to the push/pops done by the
user and each decision made by MiniSat.

Before 2cc0e2c6a691fb6d30ed8879832b49bc1f277d77, we had an additonal
push/pop when doing the actual solving. With these removed, it could
happen that we get a wrong result when doing incremental solving:

```
...
; check-sat call returns sat, the decision level in the SAT solver is
; non-zero at this point
(check-sat)
; Solver::addClause_() determines that we cannot add the clause to the
; SAT solver directly because the decision level is non-zero (i.e. the
; clause is treated like a theory lemma), thus it is added to the lemmas
; list.
(assert false)
; The solver stores some information about the current state, including
; the value of the "ok" flag in Solver, which indicates whether the
; current constraints are unsatisfiable. Note that "ok" is true at this
; point.
(push)
; Now, in Solver::updateLemmas(), we add clauses from the lemmas list.
; The problem is that empty clauses (which "false" is after removing "false"
; literals) and unit clauses are not added like normal clauses. Instead,
; the empty clause, essentially just results in the "ok" flag being set to
; false (unit clauses are added to the decision trail).
(check-sat)
; Here, the solver restores the information stored during
; (push), including the "ok" flag, which is now true again.
(pop)
; At this point, the solver has "forgotten" about (assert false) since
; the "ok" flag is back to true and it answers sat.
(check-sat)
```

There are multiple ways to look at the problem and to fix it:

- One could argue that an input assertion should always be added
directly to the clauses in the SAT solver, i.e. the solver should
always be at decision level 0 when we are adding input clauses. The
advantage of this is that it is relatively easy to implement,
corresponds to what the original MiniSat code does (it calls
Solver::cancelUntil(0) after solving), and is no worse than what we had
before commit 2cc0e2c6a691fb6d30ed8879832b49bc1f277d77 (push/pop do a
strict superset of what resetting the decision at the current assertion
level does). The disadvantage is that we might throw away some useful work.

- One could argue that is fine that (assert false) is treated like a
theory lemma. The advantage being that it might result in more efficient
solving and the disadvantage being that it is much trickier to
implement.

Unfortunately, it is not quite clear from the code what the original
intention was but we decided to implement the first solution. This
commit exposes a method in MiniSat to reset the decisions at the current
assertion level. We call this method from SmtEngine after solving.
Resetting the decisions directly after solving while we are still in
MiniSat does not work because it causes issues with datastructures in
the SMT solver that use the decision context (e.g.
TheoryEngine::d_incomplete seems to be reset too early, resulting in us
answering sat instead of unknown).

6 years agoDisable BV-abstraction in the competition script. (#2061)
Mathias Preiner [Fri, 8 Jun 2018 20:25:13 +0000 (13:25 -0700)]
Disable BV-abstraction in the competition script. (#2061)

6 years agoLook for cryptominisat5_simple, not cryptominisat5 (#2058)
Andres Noetzli [Thu, 7 Jun 2018 20:56:06 +0000 (13:56 -0700)]
Look for cryptominisat5_simple, not cryptominisat5 (#2058)

If the boost program_options library is missing, CryptoMiniSat5 only
builds a cryptominisat5_simple binary and omits the cryptominisat5,
which has more command-line options. We do not use the binary anyway, so
this commit changes the cryptominisat.m4 script to look for the
cryptominisat5_simple binary, which is always generated.

6 years agoRemove invalid assertion (#1993). (#2057)
Aina Niemetz [Thu, 7 Jun 2018 18:37:04 +0000 (11:37 -0700)]
Remove invalid assertion (#1993). (#2057)

6 years agoClear pending inferences during datatypes splitting (#2056)
Andrew Reynolds [Thu, 7 Jun 2018 02:46:56 +0000 (21:46 -0500)]
Clear pending inferences during datatypes splitting (#2056)

6 years agoOnly enable transcendentals if logic is N[I]RAT (#2052)
Andres Noetzli [Tue, 5 Jun 2018 02:28:44 +0000 (19:28 -0700)]
Only enable transcendentals if logic is N[I]RAT (#2052)

6 years agoMove assertion. (#2051)
Andrew Reynolds [Mon, 4 Jun 2018 19:55:10 +0000 (14:55 -0500)]
Move assertion. (#2051)

6 years ago[SMT-COMP] Add new logics to run-scripts (#2022)
Andres Noetzli [Mon, 4 Jun 2018 19:30:28 +0000 (12:30 -0700)]
[SMT-COMP] Add new logics to run-scripts (#2022)

6 years agoEnable cegqi (with model values) for floating point by default (#2023)
Andrew Reynolds [Mon, 4 Jun 2018 18:58:14 +0000 (13:58 -0500)]
Enable cegqi (with model values) for floating point by default (#2023)

6 years agoRegressions: Support for requiring CVC4 features (#2044)
Andres Noetzli [Mon, 4 Jun 2018 17:56:19 +0000 (10:56 -0700)]
Regressions: Support for requiring CVC4 features (#2044)

This commit adds supprt for the `REQUIRES` directive in our regression
benchmarks. This directive can be used to enable certain benchmarks only
if CVC4 has been configured with certain features enabled.

6 years ago Fix assertion involving unassigned Boolean eqc in model (#2050)
Andrew Reynolds [Sat, 2 Jun 2018 19:18:24 +0000 (14:18 -0500)]
 Fix assertion involving unassigned Boolean eqc in model (#2050)