| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
The theory solver for strings does not support regular expression variables. With this PR, we properly throw an exception if it is given one.
However, the rewriter needs to handle regular expression variables (for various reasons: rewriting an expression before its asserted, sygus explanation generalization, etc.). This corrects a few miscellaneous issues in the strings rewriter to make it sound for these cases.
It also corrects a seg fault in simpleRegexpConsume when testing memberships `(str.in.re "" R)`, where R is a *non-constant* regular expression (which will now be allowed if variables are allowed).
This is in preparation for adding `RegLan` as a token to the smt2/sygus parsers.
|
|
condition/child. (#2259)
|
|
|
|
|
|
|
|
This includes several improvements for cegqi with arithmetic:
- Randomly choose either lower or upper bounds instead of always using lower bounds (this is similar to cegqi+BV),
- Equalities are handled by processAssertions,
- Resort to *only* model values at full effort instead of trying to mix model values/bounds (this is also similar to cegqi+BV),
- cegqi+arithmetic does not try multiple instantiations unless the flag cbqiMultiInst is set. This makes it so that ceg_instantiator does not have exponential behavior when the strategy is non-monotonic.
It also includes a core fix to computing what bound is optimal based on an ordering that incorporates virtual terms. Previously, we would consider, e.g.:
`a+b*delta > c+d*delta if a>=c and b>=d`
Whereas the correct check is lexicographic:
`a+b*delta > c+d*delta if a>c or a=c and b>d`
This means e.g. 2+(-1)*delta > 3 was previously wrongly inferred.
This is part of merging https://github.com/ajreynol/CVC4/tree/cegqiSingleInst, which is +3-0 on SMTLIB BV and +12-9 on SMTLIB LIA+LRA+NRA+NIA.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This includes:
- A missing case in the smt2 printer,
- A bug in an inference of int2bv applied to bv2nat where the types are different.
|
|
Makes minor improvements and removes the need to have the assertion (which was incorrect).
This fixes the nightlies.
|
|
This ensures that the function getEnumerateUfTerm does not have out of bounds accesses. This is an alternative fix to the one brought up in #2158.
|
|
(#2236)
Currently, the discrimination tree index used for candidate rewrite rule filtering based on matching does not properly distinguish polymorphic operators, which leads to type errors. This makes the index handle them correctly.
Fixes #1923.
|
|
- Introduces a system that validating that, when not using THEORY_SEP, that it is not possible to
obtain the separation logic heap/nil (validate_exception())
- Introduces a system test demonstrating how to use the separation logic theory, and then how
to use the "getters" to obtain and interrogate the heap/nil expressions (validate_getters())
- Refactors the original getters to avoid duplicate code
- Add a check as part of the getters to ensure that THEORY_SEP is in use
|
|
|
|
Further, unifies all *limitHandler and *limitPerHandler to limitHandler.
|
|
Eager incremental solving is achieved via solving under assumptions. As soon as incremental and eager bit-blasting is enabled, assertions are passed to the SAT solver as assumptions rather than assertions. This requires the eager SAT solver to support incremental solving, which is currently only supported by CryptoMiniSat.
|
|
|
|
Changing the return type of CDHashMap::iterator* to return a reference. Requires performance testing.
|
|
Not adding the argument description for non-{bool,void} options is now an error.
Further, adds missing argument descriptions.
|
|
Fixes #2188. There were two issues related to cxxtest in configure.ac:
- `AC_PATH_PROGS` was used wrong (the third argument is a value to
assign to the first argument and cannot be used for arbitrary
commands)
- The `test` command always executes both sides of an "and" (`-a`), so
`basename` was called without arguments when `CXXTESTGEN` was empty
This commit fixes both issues.
|
|
Python is required for generating the options code. The dependency is now
required. Now autoconf searches for a Python version >= 2.7 and sets the
corresponding environment variables. mkoptions.py is now called with $(PYTHON).
This fixes the broken competition and windows nightly builds.
|
|
|
|
(#2217)
|
|
A Node has free variables if its operator has free variables.
|
|
|
|
|
|
|
|
|
|
preparation for adding map utility functions. (#2209)
|
|
deprecating CDTrailHashMap. (#2207)
|
|
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.
|
|
|
|
|
|
|
|
|
|
This is 1/3 PRs for deprecating CDTrailHashMap.
|
|
|
|
|
|
|
|
|
|
|
|
logic (#2194)
|
|
|
