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.
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).
Mathias Preiner [Fri, 8 Jun 2018 20:25:13 +0000 (13:25 -0700)]
Disable BV-abstraction in the competition script. (#2061)
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.
Aina Niemetz [Thu, 7 Jun 2018 18:37:04 +0000 (11:37 -0700)]
Remove invalid assertion (#1993). (#2057)
Andrew Reynolds [Thu, 7 Jun 2018 02:46:56 +0000 (21:46 -0500)]
Clear pending inferences during datatypes splitting (#2056)
Andres Noetzli [Tue, 5 Jun 2018 02:28:44 +0000 (19:28 -0700)]
Only enable transcendentals if logic is N[I]RAT (#2052)
Andrew Reynolds [Mon, 4 Jun 2018 19:55:10 +0000 (14:55 -0500)]
Move assertion. (#2051)
Andres Noetzli [Mon, 4 Jun 2018 19:30:28 +0000 (12:30 -0700)]
[SMT-COMP] Add new logics to run-scripts (#2022)
Andrew Reynolds [Mon, 4 Jun 2018 18:58:14 +0000 (13:58 -0500)]
Enable cegqi (with model values) for floating point by default (#2023)
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.
Andrew Reynolds [Sat, 2 Jun 2018 19:18:24 +0000 (14:18 -0500)]
Fix assertion involving unassigned Boolean eqc in model (#2050)
Andrew Reynolds [Sat, 2 Jun 2018 18:39:20 +0000 (13:39 -0500)]
Fix corner case of mixed int/real cegqi. (#2046)
Mathias Preiner [Sat, 2 Jun 2018 18:18:36 +0000 (11:18 -0700)]
Fix BV-abstraction check to consider SKOLEM. (#2042)
Further, fix a bug in the AIG bitblaster that was also uncovered with the
minimized file.
Andrew Reynolds [Sat, 2 Jun 2018 17:15:48 +0000 (12:15 -0500)]
Fix preinitialization pass for finite model finding (#2047)
Andrew Reynolds [Fri, 1 Jun 2018 22:42:13 +0000 (17:42 -0500)]
Fix quantified bv variable elimination (#2039)
Andrew Reynolds [Fri, 1 Jun 2018 22:10:52 +0000 (17:10 -0500)]
Fix quantifiers conflict lemma handling (#2043)
Andrew Reynolds [Fri, 1 Jun 2018 20:29:05 +0000 (15:29 -0500)]
Apply preprocessing to counterexample lemmas in CEGQI (#2027)
Andrew Reynolds [Fri, 1 Jun 2018 20:10:23 +0000 (15:10 -0500)]
Use monomial sum utility to solve for quantifiers macros (#2038)
Andrew Reynolds [Fri, 1 Jun 2018 00:06:55 +0000 (19:06 -0500)]
Reduce before preregister. (#2025)
Mathias Preiner [Thu, 31 May 2018 02:12:28 +0000 (19:12 -0700)]
Fix bv-abstraction check for AND with non bit-vector atoms. (#2024)
Aina Niemetz [Wed, 30 May 2018 23:28:58 +0000 (16:28 -0700)]
Ignore license key in set-info command. (#2021)
Andres Noetzli [Wed, 30 May 2018 22:02:29 +0000 (15:02 -0700)]
Fix for issue #2002 (#2012)
Andrew Reynolds [Wed, 30 May 2018 20:34:05 +0000 (15:34 -0500)]
Fixes for quantifiers + incremental (#2009)
Andres Noetzli [Wed, 30 May 2018 19:04:38 +0000 (12:04 -0700)]
[SMT-COMP] Print non-(un)sat output to stderr (#2019)
In the SMT-COMP runscript, we are currently discarding output on stdout
that is not "sat" or "unsat" when using `trywith` (this is not the case
with `finishwith`). Due to this, our tests might miss cases where CVC4
fails and prints an error on stdout when using `trywith`. This commit
changes the script to print output other than "sat" or "unsat" to
stderr.
Mathias Preiner [Wed, 30 May 2018 18:42:40 +0000 (11:42 -0700)]
Normalize negated bit-vector terms over equalities. (#2017)
Mathias Preiner [Wed, 30 May 2018 18:17:35 +0000 (11:17 -0700)]
Use CaDiCaL for eager bit-blasting in QF_NIA and QF_UFBV. (#2018)
Andrew Reynolds [Wed, 30 May 2018 17:49:46 +0000 (12:49 -0500)]
Draft run script for strings smt comp 2018. (#2016)
Andres Noetzli [Tue, 29 May 2018 18:25:13 +0000 (11:25 -0700)]
Make user's SMT2 version override file version (#2004)
Andrew Reynolds [Tue, 29 May 2018 17:46:35 +0000 (12:46 -0500)]
Disable minisat elimination when nonlinear is enabled (#2006)
Andres Noetzli [Tue, 29 May 2018 12:43:20 +0000 (05:43 -0700)]
Track input language in a single place (#2003)
Andrew Reynolds [Mon, 28 May 2018 15:35:17 +0000 (10:35 -0500)]
Builtin evaluation functions for sygus (#1991)
Andrew Reynolds [Sun, 27 May 2018 20:10:08 +0000 (15:10 -0500)]
Fix cegqi assertions for quantified non-linear cases. (#1999)
Andres Noetzli [Sun, 27 May 2018 18:39:36 +0000 (11:39 -0700)]
Fix no-cbqi-innermost option name in run script (#1994)
Mathias Preiner [Sat, 26 May 2018 22:56:16 +0000 (15:56 -0700)]
Update SymFPU. (#1992)
Andrew Reynolds [Fri, 25 May 2018 21:19:58 +0000 (16:19 -0500)]
Reenable repair const (#1983)
Andres Noetzli [Fri, 25 May 2018 20:26:16 +0000 (13:26 -0700)]
MiniSat: Be more careful about running proof code (#1982)
In `addClause_()`, we were checking the condition `ca[confl].size() ==
1` regardless if proofs were enabled or not, even though both branches
of the if statement only do something when proofs are enabled. This lead
to issue #1978 occurring even when not generating proofs. Note: This
commit is *not* a fix for #1978 but it makes sure that the issue does
not occur when not generating proofs/unsat cores.
Mathias Preiner [Fri, 25 May 2018 18:02:32 +0000 (11:02 -0700)]
Add QF_BV configuration for SMTCOMP'18. (#1981)
Andrew Reynolds [Fri, 25 May 2018 16:46:56 +0000 (11:46 -0500)]
Fix various nl assertions. (#1980)
Andrew Reynolds [Fri, 25 May 2018 00:55:47 +0000 (19:55 -0500)]
Fix (#1979)
Andrew Reynolds [Thu, 24 May 2018 22:28:59 +0000 (17:28 -0500)]
Improve simple constant symmetry breaking for sygus (#1977)
Andres Noetzli [Thu, 24 May 2018 20:01:33 +0000 (13:01 -0700)]
Fix compiler warnings (#1959)
Andrew Reynolds [Thu, 24 May 2018 19:24:44 +0000 (14:24 -0500)]
Fix (#1975)
Andrew Reynolds [Thu, 24 May 2018 19:01:44 +0000 (14:01 -0500)]
Fixes for non-linear check model (#1974)
Andrew Reynolds [Thu, 24 May 2018 15:03:23 +0000 (10:03 -0500)]
Fix nl regression for unsat cores. (#1973)
Andrew Reynolds [Thu, 24 May 2018 01:41:11 +0000 (20:41 -0500)]
Remove spurious assertion in nonlinear extension (#1972)
Haniel Barbosa [Wed, 23 May 2018 23:18:51 +0000 (18:18 -0500)]
Towards better symbolic enumeration in SyGuS (#1971)
Andrew Reynolds [Wed, 23 May 2018 20:44:50 +0000 (15:44 -0500)]
Add notions of evaluated kinds in TheoryModel (#1947)
Andres Noetzli [Wed, 23 May 2018 13:53:06 +0000 (06:53 -0700)]
Remove ProofProxy (#1965)
Andrew Reynolds [Wed, 23 May 2018 12:00:40 +0000 (07:00 -0500)]
Generalize check-model in NonLinearExtension for quadratic equations (#1892)
Andres Noetzli [Wed, 23 May 2018 05:20:59 +0000 (22:20 -0700)]
Set same options for proofs as for unsat cores (#1957)
In SmtEngine::setDefaults() we were setting options such as
--simplifciation=none for unsat cores but not proofs. Producing unsat
cores relies on the same infrastructure as proofs and should be a subset
of the same work in most cases. Thus, this commit changes
SmtEngine::setDefaults() to set the same options for proofs as we
previously only did for unsat cores. Additionally, it changes the
function to only set the simplificationMode to SIMPLIFICATION_MODE_BATCH
if proofs and unsat cores are not enabled. Fixes issue #1953.
Andrew Reynolds [Wed, 23 May 2018 01:27:32 +0000 (20:27 -0500)]
Repair constants using symbolic constructors (#1960)
Andrew Reynolds [Tue, 22 May 2018 23:12:54 +0000 (18:12 -0500)]
Parse error for sygus grammar term with multiple let bodies (#1961)
Andres Noetzli [Tue, 22 May 2018 18:43:15 +0000 (11:43 -0700)]
Disable symmetry breaker for unsat cores (#1958)
Currently, --check-unsat-cores fails for one of our regressions. It
turns out that the issue is due to preprocessing done by the symmetry
breaker. The symmetry breaker does not add dependencies and thus the
generated unsat core is incomplete/wrong. This commit disables the
symmetry breaker when we are generating unsat cores (it was previously
only disabled when generating proofs). Fixes issue #1953.
Andrew Reynolds [Tue, 22 May 2018 18:08:31 +0000 (13:08 -0500)]
Make sygus infer find function definitions (#1951)
Andrew Reynolds [Tue, 22 May 2018 01:54:52 +0000 (20:54 -0500)]
Infrastructure for strings strategies (#1883)
Mathias Preiner [Tue, 22 May 2018 00:54:09 +0000 (17:54 -0700)]
Add SymFPU licensing information. (#1952)
Andrew Reynolds [Mon, 21 May 2018 22:52:26 +0000 (17:52 -0500)]
Improvements in parsing and printing related to mixed int/real (#1879)
This eliminates some hacks for dealing with Int/Real.
- Eliminates the use of "to_real" to cast decimals like "2.0" that happen to be Int. We now replace these by (/ 2 1) instead of (to_real 2), which has the advantage of being smt-lib compliant for all theories, including QF_LRA.
- Eliminates the use of a hack to use "type ascriptions" when returning values from a get-value command. Instead, we use division with 1 when necessary. This affects the output of a few regressions, but we remain smt-lib compliant.
- Addresses a bug with printing arbitrary type ascriptions for smt2 terms. This partially addresses #1852.
- Updates our printing of negative rationals to be (/ (- n) m) instead of (- (/ n m)), which is consistent with the smt lib standard for real values (http://smtlib.cs.uiowa.edu/theories-Reals.shtml).
Andrew Reynolds [Mon, 21 May 2018 21:33:17 +0000 (16:33 -0500)]
Infrastructure to mark unused sygus strategies (#1950)
makaimann [Mon, 21 May 2018 21:07:48 +0000 (14:07 -0700)]
Handle IMPLIES in bool-to-bv and test it in regress0 (#1929)
Andrew Reynolds [Mon, 21 May 2018 19:09:12 +0000 (14:09 -0500)]
Refactor sygus eval unfold (#1946)
Andres Noetzli [Mon, 21 May 2018 18:37:26 +0000 (21:37 +0300)]
Remove Eclipse project files (#1928)
No one of the core devs is currently using Eclipse, so the Eclipse
project files are essentially useless since they are not guaranteed to
be up-to-date.
Andres Noetzli [Mon, 21 May 2018 18:00:44 +0000 (21:00 +0300)]
Fix compiler warning in hashsmt example (#1927)
Previously, we were using delete for an array allocated on the heap,
which caused a warning. @dddejan fixed this and other issues in PR #1909
but after @ajreynol fixed the other issues in a separate PR and to not
waste @dddejan's time, I am submitting this fix separately (note: the
fix is slightly different in that it changes the array to a vector,
making a delete[] unnecessary).
Haniel Barbosa [Mon, 21 May 2018 17:21:33 +0000 (12:21 -0500)]
Assign weight 1 for Boolean variables in SyGuS default grammars (#1948)
Caleb Donovick [Mon, 21 May 2018 15:29:14 +0000 (08:29 -0700)]
Fix file extension (#1919)
* Fix file extension
* Update Makefile
Haniel Barbosa [Sat, 19 May 2018 01:49:13 +0000 (20:49 -0500)]
changing default (#1944)
Andrew Reynolds [Fri, 18 May 2018 22:54:11 +0000 (17:54 -0500)]
Cache isInterpretedFinite (#1943)
Andrew Reynolds [Fri, 18 May 2018 20:02:18 +0000 (15:02 -0500)]
Cegis unif defaults to cegis when no unif (#1942)
Andrew Reynolds [Fri, 18 May 2018 17:53:53 +0000 (12:53 -0500)]
Unified fairness scheme for cegis unif (#1941)
Andrew Reynolds [Thu, 17 May 2018 21:31:30 +0000 (16:31 -0500)]
Catch type errors in sygus grammars for lambda (define-fun) constructors (#1937)
Andrew Reynolds [Thu, 17 May 2018 21:03:39 +0000 (16:03 -0500)]
Fix debugPrint and add regress. (#1934)
Haniel Barbosa [Thu, 17 May 2018 19:47:30 +0000 (14:47 -0500)]
Option to force return values of Bool functions to be constant in CegisUnif (#1930)
Andrew Reynolds [Thu, 17 May 2018 19:09:46 +0000 (14:09 -0500)]
Cegis-specific infrastructure (#1933)
Andrew Reynolds [Thu, 17 May 2018 14:23:14 +0000 (09:23 -0500)]
Internal propagation for refinement lemmas (#1932)
Andrew Reynolds [Wed, 16 May 2018 23:22:35 +0000 (18:22 -0500)]
Improve the separation resolution scheme in cegis unif (#1931)
yoni206 [Wed, 16 May 2018 01:17:01 +0000 (18:17 -0700)]
Refactor static learning preprocessing pass (#1857)
Andrew Reynolds [Tue, 15 May 2018 20:39:27 +0000 (15:39 -0500)]
Refactoring get enumerator values in construct candidate for cegis unif (#1926)
Haniel Barbosa [Tue, 15 May 2018 19:48:43 +0000 (14:48 -0500)]
adding regressions (#1925)
Haniel Barbosa [Tue, 15 May 2018 17:20:13 +0000 (12:20 -0500)]
Building and refining solutions with dynamic condition generation in CegisUnif (#1920)
Andrew Reynolds [Tue, 15 May 2018 15:40:29 +0000 (10:40 -0500)]
Fix free variables in cbqi preregister inst. (#1921)
Andrew Reynolds [Tue, 15 May 2018 03:25:40 +0000 (22:25 -0500)]
Fix annotations in regress2. (#1917)
Andrew Reynolds [Tue, 15 May 2018 02:27:07 +0000 (21:27 -0500)]
Minor improvements to --nl-ext-purify (#1896)
Andrew Reynolds [Tue, 15 May 2018 00:27:58 +0000 (19:27 -0500)]
Incorporating dynamic condition enumeration into cegis unif (#1916)
Martin [Mon, 14 May 2018 23:18:31 +0000 (00:18 +0100)]
Floating point theory solver based on SymFPU (#1895)
* Add some symfpu accessor functions to reduce the size of the literal 'back-end'.
* Enable the bit-vector theory when setting the logic, not in expandDefinition.
This is needed because it is possible to add variables of float or rounding mode
sort but not use any theory specific functions or predicates and thus not enable
the bit-vector theory.
* Use symfpu to implement the literal floating-point objects.
* Add kinds for bit-blasted components.
* Print the new kinds.
* Typing rules for the new kinds.
* Constant folding for the component kinds.
* Add support for components to the theory solver.
* Add explicit equivalences between classification functions and equalities.
* Use symfpu to do symbolic conversions of floating-point operations.
* Implement conversions via (over-)approximation and refinement.
* Correct a copy and paste error in the generation of uninterpretted functions for conversions.
Mathias Preiner [Mon, 14 May 2018 22:36:52 +0000 (15:36 -0700)]
Add contrib/get-symfpu for downloading symfpu. (#1905)
Haniel Barbosa [Mon, 14 May 2018 20:09:31 +0000 (15:09 -0500)]
Fix purification in SygusUnifRL (#1912)
Andrew Reynolds [Mon, 14 May 2018 16:33:14 +0000 (11:33 -0500)]
Add regressions, change defaults. (#1911)
Andrew Reynolds [Mon, 14 May 2018 15:29:08 +0000 (10:29 -0500)]
Flag to check invariance of entire values in sygus explain (#1908)
Florian Schanda [Mon, 14 May 2018 12:43:42 +0000 (13:43 +0100)]
Small change for more sensible line breaking in the output of get-model. (#1910)
Aina Niemetz [Fri, 11 May 2018 18:49:45 +0000 (11:49 -0700)]
Remove obsolete unit test for ackermannization. (#1906)
With #1902, test/regress/regress1/bug520-eager.smt2 is now obsolete.
Aina Niemetz [Fri, 11 May 2018 15:47:02 +0000 (08:47 -0700)]
Fix ackermannize preprocessing pass. (#1904)
Ackermannization did not consider cases where UF are Boolean. Model generation is
still not supported, but now guarded against when bit-vectors are combined with arrays
and/or uninterpreted functions and --bitblast=eager.
Andres Noetzli [Fri, 11 May 2018 02:34:30 +0000 (19:34 -0700)]
Support multiple sets of command line args in regs (#1902)
This commit adds support for multiple sets of command line arguments for
regressions. Each use of a `COMMAND-LINE` directive is interpreted as a
separate set of command line arguments.
Haniel Barbosa [Fri, 11 May 2018 01:43:09 +0000 (20:43 -0500)]
Also exclude ITEs from ITE conditions in SygusUnifStrat (#1903)
Andrew Reynolds [Thu, 10 May 2018 22:43:48 +0000 (17:43 -0500)]
Exclude Boolean connectives from ITE conditions in SygusUnifStrat (#1900)
Andrew Reynolds [Thu, 10 May 2018 21:48:51 +0000 (16:48 -0500)]
Sygus repair constants (#1812)
Haniel Barbosa [Thu, 10 May 2018 20:57:54 +0000 (15:57 -0500)]
Static learn redundant operators in CegisUnif (#1899)
Andrew Reynolds [Thu, 10 May 2018 20:35:51 +0000 (15:35 -0500)]
Add ITE to default Boolean sygus grammar (#1898)
Aina Niemetz [Thu, 10 May 2018 18:25:19 +0000 (11:25 -0700)]
Refactored BVAckermann preprocessing pass. (#1889)
Andrew Reynolds [Thu, 10 May 2018 16:38:03 +0000 (11:38 -0500)]
Fix priority of decisions for cegis unif (#1897)
Haniel Barbosa [Wed, 9 May 2018 21:45:43 +0000 (16:45 -0500)]
Piecing solutions together in CegisUnif (#1894)