| Age | Commit message (Collapse) | Author |
|---|
|
* Removing attribute cleanups.
|
|
Since we are using C++11, we can replace the triple and quad classes
with std::tuple.
|
|
|
|
|
|
When dumping a `get-unsat-assumptions` command, CVC4 was instead dumping
two `get-unsat-cores` commands. This commit splits
`SmtEngine::getUnsatCores()` into a part that does the dumping and an
internal part that actually gets the unsat core without dumping.
`SmtEngine::getUnsatAssumptions()` now calls the internal version to
avoid the redundant dumping of a `get-unsat-cores` command and changes
the command that gets dumped in `SmtEngine::getUnsatAssumptions()`.
|
|
|
|
Fixes #2298. The `get-unsat-assumptions` command was printing the result
with square brackets and commas instead of parentheses and spaces
between the assumptions.
|
|
* Removing support for T* and const T* attributes. These are unused.
|
|
@taking pointed out that part of the issue fixed in #2293 is also that
we should be more robust to different (de-)initialization orders. A
common, portable way to achieve this is to allocate the object in
question on the heap and make the pointer to it static [0]. This commit
fixes the variable in question.
I have tested this fix in ASAN (without using --no-static-init flag for
CxxTest) and it works.
[0] https://isocpp.org/wiki/faq/ctors#construct-on-first-use-v2
|
|
|
|
|
|
|
|
|
|
* Proposal for adding map utility functions to CVC4.
|
|
|
|
|
|
|
|
|
|
Removes some hacks due to Swig 2's incomplete C++11 support and adds
checks for version 3 at configuration time as well as in swig.h
|
|
Currently, there is code duplication for parsing constants in sygus grammars, e.g.:
https://github.com/CVC4/CVC4/blob/master/src/parser/smt2/Smt2.g#L1048
https://github.com/CVC4/CVC4/blob/master/src/parser/smt2/Smt2.g#L2304
This PR removes this duplication by introducing a new ANTLR grammar "termAtomic" in Smt2.g.
As a result of this PR, we now parse sygus grammars with any constant we otherwise parse. This addresses known issues where CVC4 rejects grammars with floating point constants.
It also removes some unnecessary code for converting builtin kinds to their total versions.
This is work towards #2197. We still do not support sygus grammars with non-trivial *composite* terms, such as applications of indexed function symbols.
|
|
|
|
|
|
C++11 supports explicitly deleting functions that should not be used
(explictly or implictly), e.g. copy or assignment constructors. We were
previously using the CVC4_UNDEFINED macro that used a compiler-specific
attribute. The C++11 feature should be more portable.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
sygus (#2269)
|
|
|
|
This includes:
- Enabling sygus-specific options in SmtEngine::setDefaults,
- Disabling a variant of miniscoping (triggered by many chc-comp18 benchmarks),
- Treating free constants as functions to synthesize
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
