yoni206 [Thu, 26 Jul 2018 22:16:04 +0000 (15:16 -0700)]
Disabling bvLazyRewriteExtf in the right place (#2214)
Tim King [Thu, 26 Jul 2018 20:55:53 +0000 (13:55 -0700)]
Changing CDInsertHashMap to store <const Key, const Data> pairs. This is in preparation for adding map utility functions. (#2209)
Tim King [Thu, 26 Jul 2018 20:13:43 +0000 (13:13 -0700)]
Changing the arithmetic static learner to use CDHashMap. This is 2/3 PRs for deprecating CDTrailHashMap. (#2207)
Andrew Reynolds [Thu, 26 Jul 2018 19:48:40 +0000 (14:48 -0500)]
Fix rewriter for lambda (#2211)
The rewriter for lambda is currently too aggressive, there are cases like:
lambda xy. x = y
that are converted into an array representation that when indexing based on x gives (store y true false), which is subsequently converted to:
lambda fv_1 fv_2. fv_1 = y
where fv_1 and fv_2 are canonical free variables. Here, y is used as index but was not substituted hence is incorrectly made free.
To make things simpler, this PR disables any rewriting for lambda unless the array representation of the lambda is a constant, which hardcodes/simplifies a previous argument (reqConst=true). This fixes a sygus issue I ran into yesterday (regression added in this PR).
Some parts of the code were formatted as a result.
Andrew Reynolds [Thu, 26 Jul 2018 19:27:37 +0000 (14:27 -0500)]
Fix a few issues in the sygus sampler related to evaluation (#2215)
ayveejay [Thu, 26 Jul 2018 18:27:46 +0000 (19:27 +0100)]
Avoid explicit dependency on Python 3 (#2195)
Aina Niemetz [Thu, 26 Jul 2018 17:00:21 +0000 (10:00 -0700)]
New C++ API: Third batch of commands (SMT-LIB). (#2212)
Aina Niemetz [Thu, 26 Jul 2018 16:00:18 +0000 (09:00 -0700)]
New C++ API: Second batch of commands (SMT-LIB). (#2201)
Tim King [Wed, 25 Jul 2018 23:56:34 +0000 (16:56 -0700)]
Changing ArithIteUtils to use CDInsertHashMap. (#2206)
This is 1/3 PRs for deprecating CDTrailHashMap.
Tim King [Wed, 25 Jul 2018 23:13:18 +0000 (16:13 -0700)]
Removing support for CDHashMap::iterator's postfix increment. (#2208)
Andrew Reynolds [Wed, 25 Jul 2018 17:34:32 +0000 (12:34 -0500)]
Move reg exp rewrites from prerewrite to postrewrite (#2204)
ayveejay [Wed, 25 Jul 2018 16:59:05 +0000 (17:59 +0100)]
Performing clang-format on the original change-set of #2194 (#2203)
Mathias Preiner [Wed, 25 Jul 2018 16:40:22 +0000 (09:40 -0700)]
Use CryptoMiniSat 5.6.3. (#2205)
Andrew Reynolds [Tue, 24 Jul 2018 22:01:38 +0000 (17:01 -0500)]
Improvements to sets + cardinality + quantifiers (#2200)
ayveejay [Tue, 24 Jul 2018 21:16:16 +0000 (22:16 +0100)]
Adding API access methods to get heap/nil expressions when using separation logic (#2194)
Aina Niemetz [Tue, 24 Jul 2018 17:11:24 +0000 (10:11 -0700)]
New C++ API: First batch of commands (SMT-LIB and non-SMT-LIB). (#2199)
Andrew Reynolds [Mon, 23 Jul 2018 23:02:36 +0000 (18:02 -0500)]
Improve rewriter for regular expression concatenation (#2196)
Andrew Reynolds [Mon, 23 Jul 2018 22:39:12 +0000 (17:39 -0500)]
Generalize symmetry detection for 1 symmetry variable mapped to n input variables (#1888)
Aina Niemetz [Mon, 23 Jul 2018 21:38:37 +0000 (14:38 -0700)]
New C++ API: Implementation of Solver class: OpTerm handling. (#2164)
Aina Niemetz [Mon, 23 Jul 2018 19:29:03 +0000 (12:29 -0700)]
New C++ API: declare-datatype. (#2166)
Andrew Reynolds [Mon, 23 Jul 2018 18:36:53 +0000 (13:36 -0500)]
sygusComp2018: add regressions (#2191)
Andrew Reynolds [Mon, 23 Jul 2018 17:01:02 +0000 (12:01 -0500)]
Fix warning in sygus PBE (#2190)
Andrew Reynolds [Sun, 22 Jul 2018 04:50:57 +0000 (23:50 -0500)]
sygusComp2018: Improvements to CEGIS loop (#2187)
Andrew Reynolds [Sat, 21 Jul 2018 14:19:31 +0000 (09:19 -0500)]
Optimizations and fixes for computing whether a type is finite (#2179)
Andrew Reynolds [Sat, 21 Jul 2018 12:27:28 +0000 (07:27 -0500)]
sygusComp2018: refactor and improve sygus io utility (#2185)
yoni206 [Sat, 21 Jul 2018 12:02:01 +0000 (05:02 -0700)]
Remove --no-check-proofs and --no-check-unsat-cores from a satisfiable test (#2184)
Andrew Reynolds [Fri, 20 Jul 2018 23:42:25 +0000 (01:42 +0200)]
Cleanup and additions for candidate generator (#2173)
Andrew Reynolds [Fri, 20 Jul 2018 20:34:18 +0000 (22:34 +0200)]
sygusComp2018: minor changes to repair constant utility (#2110)
Andrew Reynolds [Tue, 17 Jul 2018 23:51:28 +0000 (01:51 +0200)]
sygusComp2018: pbe multi-enumerator fairness option (#2178)
yoni206 [Tue, 17 Jul 2018 21:20:46 +0000 (14:20 -0700)]
Refactor sep-pre-skolem-emp preprocessing pass
Andrew Reynolds [Tue, 17 Jul 2018 17:53:14 +0000 (19:53 +0200)]
Minor cleanup and fixes for conflict-based instantiation (#2123)
Andrew Reynolds [Tue, 17 Jul 2018 17:07:22 +0000 (19:07 +0200)]
Do extended rewrite on results of quantifier elimination. (#2119)
Andrew Reynolds [Tue, 17 Jul 2018 16:25:13 +0000 (18:25 +0200)]
Purify applications of exp to transcendental arguments (#2097)
Andrew Reynolds [Tue, 17 Jul 2018 15:37:03 +0000 (17:37 +0200)]
sygusComp2018: update policies for solution reconstruction (#2109)
Andrew Reynolds [Tue, 17 Jul 2018 14:17:43 +0000 (16:17 +0200)]
sygusComp2018: Improvements to datatypes sygus solver (#2177)
Andrew Reynolds [Tue, 17 Jul 2018 11:02:32 +0000 (13:02 +0200)]
sygusComp 2018: updates to sygus term database (#2170)
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
Andres Noetzli [Sat, 14 Jul 2018 08:45:58 +0000 (01:45 -0700)]
exportTo only if needed for --sygus-rr-synth-check (#2168)
Andrew Reynolds [Sat, 14 Jul 2018 08:08:11 +0000 (10:08 +0200)]
sygusComp2018: update semantics for declare-fun in sygus. (#2102)
Andrew Reynolds [Fri, 13 Jul 2018 22:30:04 +0000 (00:30 +0200)]
Fix and improve grammar normalization for any constant. (#2101)
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.
Andrew Reynolds [Fri, 13 Jul 2018 15:36:01 +0000 (17:36 +0200)]
sygusComp2018: optimization for collect model info (#2105)
Aina Niemetz [Fri, 13 Jul 2018 10:04:49 +0000 (03:04 -0700)]
New C++ API: Minor reorder. (#2163)
Aina Niemetz [Fri, 13 Jul 2018 08:57:24 +0000 (01:57 -0700)]
New C++ API: Implementation of datatype classes. (#2142)
Aina Niemetz [Fri, 13 Jul 2018 08:06:18 +0000 (01:06 -0700)]
New C++ API: Implementation of Solver class: Consts handling. (#2145)
Caleb Donovick [Wed, 11 Jul 2018 00:27:16 +0000 (17:27 -0700)]
Move rewrite to pass (#2128)
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
Andrew Reynolds [Sat, 7 Jul 2018 06:49:11 +0000 (07:49 +0100)]
sygusComp2018: improve extended rewriter for Bool (#2107)
Andrew Reynolds [Fri, 6 Jul 2018 19:58:31 +0000 (20:58 +0100)]
Split ext theory to own file and document (#1809)
Martin [Fri, 6 Jul 2018 18:22:57 +0000 (19:22 +0100)]
Feature/fp rewrite improvement (#2154)
Aina Niemetz [Fri, 6 Jul 2018 17:26:00 +0000 (10:26 -0700)]
New C++ API: Implementation of Solver class: Term handling. (#2144)
Aina Niemetz [Fri, 6 Jul 2018 16:53:21 +0000 (09:53 -0700)]
New C++ API: Implementation of Solver class: Sort handling. (#2143)
Andres Noetzli [Fri, 6 Jul 2018 11:03:58 +0000 (04:03 -0700)]
Add option for timeout for rewrite candidate check (#2156)
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.
Andrew Reynolds [Thu, 5 Jul 2018 16:22:53 +0000 (17:22 +0100)]
Make string length lemmas more robust to rewriting (#2150)
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)
Andres Noetzli [Thu, 5 Jul 2018 02:32:29 +0000 (19:32 -0700)]
sygusComp2018: Improve string rewriter (#2141)
Andrew Reynolds [Wed, 4 Jul 2018 15:34:17 +0000 (16:34 +0100)]
More cleanup in strings (#2138)
Aina Niemetz [Wed, 4 Jul 2018 15:10:27 +0000 (08:10 -0700)]
New C++ API: Implementation of datatype declaration classes. (#2136)
Andrew Reynolds [Wed, 4 Jul 2018 13:31:14 +0000 (14:31 +0100)]
Reorganize candidate rewrite rule filtering (#2116)
Andres Noetzli [Wed, 4 Jul 2018 10:58:24 +0000 (03:58 -0700)]
Remove unused CDVector (#2139)
Aina Niemetz [Wed, 4 Jul 2018 08:31:02 +0000 (01:31 -0700)]
New C++ API: Implementation of OpTerm. (#2132)
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.
Aina Niemetz [Tue, 3 Jul 2018 16:27:59 +0000 (09:27 -0700)]
New C++ API: Implementation of Term. (#2131)
Aina Niemetz [Tue, 3 Jul 2018 15:59:35 +0000 (08:59 -0700)]
New C++ API: Implementation of Kind maps. (#2130)
Aina Niemetz [Tue, 3 Jul 2018 11:49:38 +0000 (04:49 -0700)]
Fix datatypes example: nil constructor was missing. (#2135)
Andrew Reynolds [Tue, 3 Jul 2018 02:42:55 +0000 (21:42 -0500)]
sygusComp2018: update sygus-related options setting in smt engine (#2108)
Andrew Reynolds [Tue, 3 Jul 2018 01:08:53 +0000 (20:08 -0500)]
Remove miscellaneous dead and unused code from quantifiers (#2121)
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.
Aina Niemetz [Mon, 2 Jul 2018 23:51:03 +0000 (16:51 -0700)]
Refactor ApplySubsts preprocessing pass. (#2120)
Aina Niemetz [Mon, 2 Jul 2018 23:16:02 +0000 (16:16 -0700)]
New C++ API: Implementation of Sort. (#2122)
Andrew Reynolds [Mon, 2 Jul 2018 21:47:50 +0000 (16:47 -0500)]
Remove some dead code from theory strings (#2125)
Caleb Donovick [Mon, 2 Jul 2018 21:26:58 +0000 (14:26 -0700)]
Add missing include (#2127)
Andrew Reynolds [Mon, 2 Jul 2018 17:45:48 +0000 (12:45 -0500)]
Modify cegqi heuristic for finite datatypes (#2126)
Andrew Reynolds [Mon, 2 Jul 2018 17:20:10 +0000 (12:20 -0500)]
Improve error message. (#2124)
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
Aina Niemetz [Fri, 29 Jun 2018 00:54:33 +0000 (17:54 -0700)]
New C++ API: Implementation of Result. (#2112)
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.
Andrew Reynolds [Thu, 28 Jun 2018 20:44:45 +0000 (15:44 -0500)]
sygusComp2018: optimization for invariance test (#2104)
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.
Andrew Reynolds [Thu, 28 Jun 2018 18:53:36 +0000 (13:53 -0500)]
Do not rename uninterpreted constants (#2098)
Andrew Reynolds [Thu, 28 Jun 2018 15:43:08 +0000 (10:43 -0500)]
Split and document ceg theory instantiators (#2094)
Aina Niemetz [Wed, 27 Jun 2018 21:00:58 +0000 (14:00 -0700)]
Header for new C++ API. (#1697)
Andrew Reynolds [Wed, 27 Jun 2018 19:12:17 +0000 (14:12 -0500)]
Synthesize candidate-rewrites from standard inputs (#1918)
Andrew Reynolds [Tue, 26 Jun 2018 23:59:28 +0000 (18:59 -0500)]
sygusComp2018: add scripts. (#2103)
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.
Andrew Reynolds [Tue, 26 Jun 2018 22:32:30 +0000 (17:32 -0500)]
Add casc j9 tfn script (#2100)
Andrew Reynolds [Tue, 26 Jun 2018 22:11:31 +0000 (17:11 -0500)]
Disable uf symmetry breaker in incremental mode (#2091)
Andrew Reynolds [Tue, 26 Jun 2018 20:45:27 +0000 (15:45 -0500)]
Fix assertion for relational triggers (#2096)
Andrew Reynolds [Tue, 26 Jun 2018 19:52:34 +0000 (14:52 -0500)]
Do not dagify printing over binders (#2093)
Andrew Reynolds [Tue, 26 Jun 2018 17:58:25 +0000 (12:58 -0500)]
Remove unnecessary code in register quantifier internal (#2092)
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.
Aina Niemetz [Tue, 26 Jun 2018 01:07:55 +0000 (18:07 -0700)]
Bump library version to 1.7-prerelease.
Aina Niemetz [Tue, 26 Jun 2018 00:21:27 +0000 (17:21 -0700)]
Cutting release 1.6.
Aina Niemetz [Mon, 25 Jun 2018 21:27:20 +0000 (14:27 -0700)]
More updates to NEWS 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.
Aina Niemetz [Fri, 22 Jun 2018 20:12:07 +0000 (13:12 -0700)]
Bump library version.
Aina Niemetz [Fri, 22 Jun 2018 20:07:43 +0000 (13:07 -0700)]
Update copyright year in configuration.cpp:copyright().
Aina Niemetz [Fri, 22 Jun 2018 20:04:40 +0000 (13:04 -0700)]
Updated copyright headers.
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).