Andrew V. Jones [Fri, 19 Jun 2020 03:16:34 +0000 (04:16 +0100)]
Revert "[Python] Properly destroy CVC4 object (#3753)" (#4422)
This reverts commit
bfa008a7ce13eff2f59b022e8c2d5d71d77f9ecb.
Andres Noetzli [Thu, 18 Jun 2020 19:21:02 +0000 (12:21 -0700)]
Improve memory management in Java bindings (#4629)
Fixes #2846. One of the challenges of the Java bindings is that the
garbage collector can delete unused objects at any time in any order.
This is an issue with CVC4's API because we require all `Expr`s to be
deleted before the corresponding `ExprManager`. In the past, we were
using `NewGlobalRef`/`DeleteGlobalRef` on the wrapper object of
`ExprManager`. The problem is that we can have multiple instances of the
wrapper that internally all refer to the same `ExprManager`. This commit
implements a different approach where the Java wrappers hold an explicit
reference to the `ExprManager`. The commit also removes some unused or
unimportant API bits from the bindings.
Andrew Reynolds [Wed, 17 Jun 2020 16:26:32 +0000 (11:26 -0500)]
Do not traverse WITNESS for partial substitutions in extended rewriter (#4630)
Fixes #4620.
The extended rewrite (and A B) ---> (and A (B * { A -> true } ) triggers an unsoundness when B contains witness terms. More generally, contextual substitution into witness terms is unsound since the skolemization of witness terms is added globally whereas the substitution corresponds to a fact that holds locally. This means that A -> true above may be added as a global constraint indirectly through witness skolemization.
A general example of this unsoundness:
(or (and (>= x 0) (P (witness ((z Int)) (=> (>= x 0) (= (* z z) x))))) F)
rewrites to
(or (and (>= x 0) (P (witness ((z Int)) (= (* z z) x)))) F)
preprocesses to
(and (or (and (>= x 0) (P k)) F) (= (* k k) x))
which now implies that (>= x 0) by the last conjunct, whereas this was not implied in the original formula
This PR limits the kinds that can be traversed when applying substitutions in the extended rewriter, including from the rewrite above. In particular, the fix ensures that the partialSubstitute method is used in the extended rewriter when applicable, which now explicitly disallows recursion on WITNESS.
Notice that this fixes contextual substitutions in the extended rewriter, but does not fix the more general issue. In particular, we still should be careful to check if contextual substitutions are applied by any other preprocessing passes.
Haniel Barbosa [Wed, 17 Jun 2020 13:38:40 +0000 (10:38 -0300)]
Improve polynomial anyterm grammar (#3566)
This changes the grammar construction in the case of anyterm + polynomial grammar so that the binary predicates EQUAL and LEQ are changed to unary predicates lambda x : ANYTERM. P(x, ZERO) rather than lambda xy. P(ANYTERM, ANYTERM), in which ZERO is a 0 constant of the respective type. Currently integer and bit-vectors are supported for this transformation.
This avoid enumerating spurious terms and can lead to significant improvements in enumeration (although not necessarily in solving speed given the current unstable nature of ANYTERM usage).
Andrew Reynolds [Tue, 16 Jun 2020 23:51:10 +0000 (18:51 -0500)]
Updates to NEWS. (#4628)
Abdalrhman Mohamed [Tue, 16 Jun 2020 22:32:38 +0000 (17:32 -0500)]
Simplify sygus conversion script. (#4627)
Aina Niemetz [Tue, 16 Jun 2020 20:48:05 +0000 (13:48 -0700)]
Update copyright headers.
Aina Niemetz [Tue, 16 Jun 2020 17:57:08 +0000 (10:57 -0700)]
Add missing REQUIRES to new regressions. (#4625)
Aina Niemetz [Tue, 16 Jun 2020 16:06:34 +0000 (09:06 -0700)]
BV: Fix querying equality status in lazy bit-blaster. (#4618)
Fixes #4076.
In the lazy bit-blaster, when querying the equality status, if the SAT
solver has a full model, it is queried for the model values of the
operands of the equality. However, the check if the bit-blaster has a
full model did not consider the case where no assertions have yet been
added, which leads to querying values of bits that are still unassigned
in the SAT solver.
Co-authored-by: <mathias.preiner@gmail.com>
Aina Niemetz [Tue, 16 Jun 2020 01:18:01 +0000 (18:18 -0700)]
Fix regressions in regress1 after #4613. (#4616)
Andrew Reynolds [Tue, 16 Jun 2020 00:04:29 +0000 (19:04 -0500)]
(proof-new) Add quantifiers proof checker (#4593)
Adds core rules for quantifiers, some of which also will be used as a general way for introducing and skolemizing witness terms.
This PR also changes the order of other rules in proof_rule.h/cpp which was in an abnormal order from previous merges.
Andrew Reynolds [Mon, 15 Jun 2020 23:23:24 +0000 (18:23 -0500)]
(proof-new) Update proof node, add proof node algorithm utility file. (#4600)
Moves get free assumptions to a proof_node_algorithm.h/cpp file, analogous to node_algorithm.h/cpp. Adds a more general form of it, getFreeAssumptionsMap, which is required for future method ProofNodeManager::mkScope.
Haniel Barbosa [Mon, 15 Jun 2020 21:00:08 +0000 (18:00 -0300)]
Support AND/OR definitions in lambda to array rewriting (#4615)
This makes the conversion between lambdas and arrays, done in the theory builtin rewriter and used in higher-order model construction, robust to function definitions in terms of AND/OR.
This also improves tracing and makes a few parts of the code adhere to code guidelines.
Aina Niemetz [Mon, 15 Jun 2020 19:32:42 +0000 (12:32 -0700)]
BV: Add missing type check for BITVECTOR_REPEAT_OP. (#4614)
Fixes #4075.
Aina Niemetz [Mon, 15 Jun 2020 18:48:02 +0000 (11:48 -0700)]
BV: Add missing type check for INT_TO_BITVECTOR. (#4613)
Fixes #4130.
This further makes an attempt at more consistent error printing.
Andrew Reynolds [Mon, 15 Jun 2020 14:40:34 +0000 (09:40 -0500)]
Do RE derivation inference only for concrete constant RE (#4609)
The RE derive inference was not designed to handle re.comp. This makes the application of this inference more conservative.
Andrew Reynolds [Sat, 13 Jun 2020 00:18:42 +0000 (19:18 -0500)]
Move sygus datatype utility functions to their own file (#4595)
Separates them from the core datatype utilities.
Code move only.
Andrew Reynolds [Fri, 12 Jun 2020 23:30:19 +0000 (18:30 -0500)]
Update to consistent policy for removed terms in quantifier bodies. (#4602)
Andrew Reynolds [Fri, 12 Jun 2020 19:13:12 +0000 (14:13 -0500)]
(proof-new) Term conversion proof generator utility (#4603)
This utility is used for constructing any proof where a term is "converted" into another by small step rewrites. This utility will be used to construct the skeleton of the proofs of rewrites, preprocessing steps, expand definitions, results of substitutions, and so on.
Andrew Reynolds [Fri, 12 Jun 2020 17:57:05 +0000 (12:57 -0500)]
(proof-new) Minor updates to strings base solver (#4606)
In preparation for proofs, this PR involves flattening AND and removing spurious true literals in conjunctions.
This also updates our policy for applying cardinality, where in some rare cases we were applying cardinality for pairs of string terms for length 0 (e.g. "there is at most 1 eqc of length 0"), which is spurious due to our term registry which always splits on emptiness.
Andrew Reynolds [Fri, 12 Jun 2020 13:07:47 +0000 (08:07 -0500)]
Cardinality-related inferences per type in theory of strings (#4585)
Towards theory of sequences.
This updates various inference steps in the theory of strings that are based on collecting all equivalence classes to be per string-like type.
Andrew Reynolds [Fri, 12 Jun 2020 04:25:15 +0000 (23:25 -0500)]
(proof-new) Split TheoryEngine (#4558)
This PR splits two classes from TheoryEngine (EngineOutputChannel and TheoryPreprocess) that will be undergoing further refactoring for proofs.
This PR does not change their behavior and is code-move only modulo a few cosmetic changes.
Andres Noetzli [Fri, 12 Jun 2020 03:05:39 +0000 (20:05 -0700)]
Fix install of static builds (#4604)
We use CMAKE_INSTALL_PATH to set the installation prefix as an RPATH
in the executable. However, for static builds, changing the RPATH fails.
This commit changes our build system to only change the
CMAKE_INSTALL_PATH if we are doing a shared library build.
Andrew Reynolds [Fri, 12 Jun 2020 02:25:07 +0000 (21:25 -0500)]
Add rewrite for str.replace_re. (#4601)
This was discovered due to a proof checking abnormality, where the checker surprisingly succeeded in proving that the reduced form for a str.replace_re was equivalent for 2 different sets of skolems after rewriting.
Andrew Reynolds [Thu, 11 Jun 2020 17:47:30 +0000 (12:47 -0500)]
(proof-new) Add lazy proof utility (#4589)
Adds an extension of CDProof where facts can be mapped to (lazy) proof generators.
Andrew Reynolds [Thu, 11 Jun 2020 00:44:33 +0000 (19:44 -0500)]
(proof-new) Add eager proof generator utility. (#4592)
Adds the eager proof generator. This lives in theory/ since it has utilities for generating TrustNode, which is specific to theory/.
Andrew Reynolds [Thu, 11 Jun 2020 00:10:06 +0000 (19:10 -0500)]
(proof-new) Remove arith-snorm option. (#4591)
This option only marginally helped and will be difficult to support with the new proof infrastructure.
Andrew Reynolds [Wed, 10 Jun 2020 21:52:46 +0000 (16:52 -0500)]
(proof-new) Theory proof step buffer utility (#4580)
This is a common class for adding steps for theory-specific proof rules into a ProofStepBuffer.
Andres Noetzli [Wed, 10 Jun 2020 19:50:52 +0000 (12:50 -0700)]
Add support for str.replace_re/str.replace_re_all (#4594)
This commit adds support for the last remaining string operators from
the new SMT-LIB standard for the theory of strings. The commit adds the
kinds, type checking, reductions, and evaluation rewrites for
`str.replace_re` and `str.replace_re_all`.
makaimann [Wed, 10 Jun 2020 19:00:13 +0000 (12:00 -0700)]
Fix getKind for Python bindings (#4496)
I noticed recently that getKind for Op and Term was not correct in the python bindings. This PR would add maps to keep track of the Kind objects and the Python names (which are different from the C++ Kind names). Then a Python `kind` only needs the integer representation of a `Kind` to be constructed. Now, in `getKind` it can just pass the integer representation when constructing a `kind`.
Andrew Reynolds [Tue, 9 Jun 2020 21:36:25 +0000 (16:36 -0500)]
(proof-new) Refactor skolemization (#4586)
This PR refactors skolemization in SkolemManager so that we use a "curried" form, where witnesses for a variable x is based on the existential where the prefix up to x has already been skolemized.
This additionally adds more utility functions that will be used in the internal proof checker for quantifiers.
Andrew Reynolds [Tue, 9 Jun 2020 14:30:01 +0000 (09:30 -0500)]
(proof-new) Add trust node utility (#4588)
This is a core data structure for associating a formula with a proof generator.
Andres Noetzli [Tue, 9 Jun 2020 12:44:24 +0000 (05:44 -0700)]
Language bindings: Enable catching of exceptions (#2813)
Fixes #2810. SWIG relies on throw specifiers to determine which
exceptions a method can throw. The wrappers generated by SWIG catch
those C++ exceptions and turn them into exceptions for the target
language. However, we have removed throw specifiers because they have
been deprecated in C++11, so SWIG did not know about any of our
exceptions. This commit fixes the issue using the %catches directive,
declaring that all methods may throw a CVC4::Exception or a general
exception. Note: This means that users of the language bindings will
just receive a general CVC4::Exception instead of more specific
exceptions like TypeExceptions. Given that we are planning to have a
single exception type for the new CVC4 API, this seemed like a natural
choice.
Additionally, the commit (significantly) simplifies the mapping of C++
to Java exceptions and fixes an issue with Python exceptions not
inheriting from BaseException. Finally, the commit adds API examples
for Java and Python, which demonstrate catching exceptions, and adds
Python examples as tests in our build system.
Andrew V. Jones [Tue, 9 Jun 2020 04:42:51 +0000 (05:42 +0100)]
Ensure correct CMake dependencies on Debug_tags.h/Trace_tags.h/git_versioninfo.cpp (#4570)
## Issue
When building CVC4, and when there are no source code codes (a so-called "no op" build), it seems that some of CMake targets are still fired:
```
[avj@tempvm build]$ ninja -d explain -d stats
ninja explain: output proofs/signatures/all of phony edge with no inputs doesn't exist
ninja explain: proofs/signatures/all is dirty
ninja explain: output doc/all of phony edge with no inputs doesn't exist
ninja explain: doc/all is dirty
ninja explain: output src/base/CMakeFiles/gen-gitinfo doesn't exist
ninja explain: src/base/CMakeFiles/gen-gitinfo is dirty
ninja explain: output src/base/CMakeFiles/gen-tags-debug doesn't exist
ninja explain: src/base/Debug_tags.tmp is dirty
ninja explain: src/base/CMakeFiles/gen-tags-debug is dirty
ninja explain: src/base/Debug_tags.tmp is dirty
ninja explain: output src/base/CMakeFiles/gen-tags-trace doesn't exist
ninja explain: src/base/CMakeFiles/gen-tags-trace is dirty
ninja explain: src/base/Trace_tags.tmp is dirty
ninja explain: src/base/Debug_tags is dirty
ninja explain: src/base/Debug_tags.h is dirty
ninja explain: src/base/Trace_tags.tmp is dirty
ninja explain: src/base/Trace_tags is dirty
ninja explain: src/base/Trace_tags.h is dirty
ninja explain: src/base/CMakeFiles/gen-tags is dirty
ninja explain: src/base/Debug_tags.h is dirty
ninja explain: src/base/Trace_tags.h is dirty
ninja explain: src/base/Debug_tags is dirty
ninja explain: src/base/Trace_tags is dirty
ninja explain: src/base/gen-tags-debug is dirty
ninja explain: src/base/gen-tags-trace is dirty
ninja explain: output src/base/all of phony edge with no inputs doesn't exist
ninja explain: src/base/all is dirty
ninja explain: output src/expr/all of phony edge with no inputs doesn't exist
ninja explain: src/expr/all is dirty
ninja explain: output src/options/all of phony edge with no inputs doesn't exist
ninja explain: src/options/all is dirty
ninja explain: output src/theory/all of phony edge with no inputs doesn't exist
ninja explain: src/theory/all is dirty
ninja explain: output src/util/all of phony edge with no inputs doesn't exist
ninja explain: src/util/all is dirty
ninja explain: src/all is dirty
ninja explain: output test/regress/all of phony edge with no inputs doesn't exist
ninja explain: test/regress/all is dirty
ninja explain: test/all is dirty
[5/6] Generating Trace_tags
metric count avg (us) total (ms)
.ninja parse 2 7192.5 14.4
canonicalize str 3315 0.2 0.7
canonicalize path 3315 0.2 0.5
lookup node 5325 0.2 1.1
.ninja_log load 1 548.0 0.5
.ninja_deps load 1 3882.0 3.9
node stat 2234 1.4 3.0
StartEdge 12 76.8 0.9
FinishCommand 5 74.6 0.4
path->node hash load 0.77 (2468 entries / 3209 buckets)
```
This is mainly because `gen-tags-debug`, `gen-tags-trace` and `gen-gitinfo` are targets with no (stated) outputs and nothing that generates them.
## Solution
This commit cleans-up the CMake inside of `src/base/CMakeLists.txt` such that, on an incremental build with no changes, no targets are fired:
```
[avj@tempvm build]$ ninja -d explain -d stats
ninja explain: output proofs/signatures/all of phony edge with no inputs doesn't exist
ninja explain: proofs/signatures/all is dirty
ninja explain: output doc/all of phony edge with no inputs doesn't exist
ninja explain: doc/all is dirty
ninja explain: output src/base/all of phony edge with no inputs doesn't exist
ninja explain: src/base/all is dirty
ninja explain: output src/expr/all of phony edge with no inputs doesn't exist
ninja explain: src/expr/all is dirty
ninja explain: output src/options/all of phony edge with no inputs doesn't exist
ninja explain: src/options/all is dirty
ninja explain: output src/theory/all of phony edge with no inputs doesn't exist
ninja explain: src/theory/all is dirty
ninja explain: output src/util/all of phony edge with no inputs doesn't exist
ninja explain: src/util/all is dirty
ninja explain: src/all is dirty
ninja explain: output test/regress/all of phony edge with no inputs doesn't exist
ninja explain: test/regress/all is dirty
ninja explain: test/all is dirty
ninja: no work to do.
metric count avg (us) total (ms)
.ninja parse 2 9198.0 18.4
canonicalize str 5314 0.2 1.1
canonicalize path 5314 0.2 0.9
lookup node 7324 0.2 1.6
.ninja_log load 1 635.0 0.6
.ninja_deps load 1 4309.0 4.3
node stat 2240 1.3 3.0
path->node hash load 0.78 (2490 entries / 3209 buckets)
```
The important bit is `ninja: no work to do.` in the output.
### Notes
I think the only thing to note is that I have changed the CMake around this comment:
```
# Note: gen-tags-{debug,trace} are targets since we always want to generate
# the temporary tag files {Debug,Trace}_tags.tmp in order to check if tags
# were added/modified/deleted.
```
I believe that the intention here was to ensure that the tags are **always** generated on a source file change.
Given that the CVC4 CMake is passing in the files to be processed (`${source_files_list}`, which is a *string*), we can add a target dependency on this *list* (`${source_files}`) to ensure that `{Debug,Trace}_tags.tmp` always get regenerated on a change.
So I believe I have captured the intent of the comment, without requiring the targets to be "unconditional".
I have also added a dependency on `${gentmptags_script}`/`${gentags_script}`/`${genheader_script}` in some places because, without this, if you change one of `${gentmptags_script}`/`${gentags_script}`/`${genheader_script}` then the associated targets don't get fired.
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
Andres Noetzli [Tue, 9 Jun 2020 04:20:25 +0000 (21:20 -0700)]
Fix Java target and Relations example (#4583)
Currently, our CVC4Config file is never including the CVC4 Java targets
because of a typo in `cmake/CVC4Config.cmake.in`. For this reason, our
build system for the examples would never actually build the examples.
Fixing this issue brought up another issue in our Relations Java example
that was using an outdated `System.loadLibrary()` call. This commit
fixes the typo and the example.
Note: Most changes in `Relations.java` were caused by ClangFormat.
Andres Noetzli [Mon, 8 Jun 2020 23:38:47 +0000 (16:38 -0700)]
Fix ambiguous overload in unit test (#4582)
Fixes nightlies. The compiler version used for our nightlies (GCC 5.4.0)
complains about mkFunctionSort({bSort}, bSort) being ambiguous because
we have two variants of mkFunctionSort(): one that takes a single
Sort and one that takes a vector of Sorts. This commit makes the
function call unambiguous by removing the use of list initializations.
Andrew Reynolds [Mon, 8 Jun 2020 21:18:21 +0000 (16:18 -0500)]
(proof-new) Add abstract proof generator class (#4574)
Also adds a commonly used proof generator: the proof reference proof generator.
Andres Noetzli [Mon, 8 Jun 2020 20:12:52 +0000 (13:12 -0700)]
Fix Coverity issues (#4587)
This commit fixes the following Coverity issues:
-
1495606: uninitialized field
-
1495605: uninitialized field
-
1488953: uninitialized field
-
1495604: mismatched iterator
Andrew Reynolds [Sat, 6 Jun 2020 17:25:50 +0000 (12:25 -0500)]
Use NlLemma utility for all lemmas in non-linear. (#4573)
This makes it much easier to set custom properties of lemmas (e.g. preprocess) and also will allow proof tracking and debugging in the future.
This also enables a fix on the IAND branch related to preprocessing lemmas.
Andres Noetzli [Sat, 6 Jun 2020 16:14:40 +0000 (09:14 -0700)]
Fix destruction order in NodeManager (#4578)
Fixes #4576. ASan was reporting memory leaks because the skolem manager
was being destroyed after the attributes and zombies were already
cleaned up in the destructor of NodeManager. This commit changes the
destruction order to ensure that the skolem manager is destroyed before
the rest of the cleanup.
Note: this issue did not only make the benchmark in #4576 fail but
several tests in our regressions.
Andres Noetzli [Sat, 6 Jun 2020 08:24:17 +0000 (01:24 -0700)]
Keep definitions when global-declarations enabled (#4572)
Fixes #4552. Fixes #4555. The SMT-LIB standard mandates that definitions
are kept when `:global-declarations` are enabled. Until now, CVC4 was
keeping track of the symbols of a definition correctly but lost the body
of the definition when the user context was popped. This commit fixes
the issue by adding a `global` parameter to
`SmtEngine::defineFunction()` and `SmtEngine::defineFunctionRec()`. If
that parameter is set, the definitions of functions are added at level 0
to `d_definedFunctions` and the lemmas for recursive function
definitions are kept in an additional list and asserted during each
`checkSat` call. The commit also updates new API, the commands, and the
parsers to reflect this change.
Andrew Reynolds [Sat, 6 Jun 2020 00:04:10 +0000 (19:04 -0500)]
Smt2 parsing support for nested recursive datatypes (#4575)
Also includes some minor improvement to expand definitions in TheoryDatatypes leftover from the branch.
Adds 3 regressions using the option --dt-nested-rec.
Andrew Reynolds [Fri, 5 Jun 2020 22:57:25 +0000 (17:57 -0500)]
Datatypes with nested recursion are not handled in TheoryDatatypes unless option is set (#3707)
Towards experimental support for non-simply recursive datatypes (https://github.com/ajreynol/CVC4/tree/dtNonSimpleRec). Builds a check for non-simple recursion in the DType class. If a term of a datatype type is registered to TheoryDatatypes for a datatype that has nested recursion, we throw a LogicException unless the option dtNestedRec is set to true. Also includes a bug discovered in the TypeMatcher utility and another in expr::getComponentTypes.
It also adds a unit test using the new API for a simple parametric datatype example as well, not related to nested recursion, as this was previously missing.
Andrew Reynolds [Fri, 5 Jun 2020 20:52:30 +0000 (15:52 -0500)]
(proof-new) Updates to CDProof (#4565)
This updates CDProof with several new functionalities, including making it agnostic to symmetry of (dis)equalites.
Andres Noetzli [Fri, 5 Jun 2020 19:16:11 +0000 (12:16 -0700)]
Skip parse-error regression for comp builds (#4567)
Fixes nightlies. Competition builds do not report parsing errors like
other builds. As a result, one of the regression tests that is testing
for parse errors was failing for competition builds. In this particular
example, we just report `unknown`. This commit marks the regression to
be skipped for competition builds.
Andrew Reynolds [Fri, 5 Jun 2020 15:19:10 +0000 (10:19 -0500)]
(proof-new) Rename ProofSkolemCache to SkolemManager (#4556)
This PR changes the design of ProofSkolemCache so that it has facilities for tracking proofs. This is required so that the term formula removal pass can be made proof-producing.
This makes it so that ProofSkolemCache is renamed to SkolemManager, which lives in NodeManager. Creating (most) skolems must be accompanied by a corresponding ProofGenerator that can provide the proof for the existential corresponding to their witness form.
Further updates will include refactoring the mkSkolemExists method of SkolemManager so that its contract wrt proofs is simpler.
Once all calls to mkSkolem go through the standard interface, then NodeManager::mkSkolem will be moved to SkolemManager::mkSkolemInternal.
Haniel Barbosa [Fri, 5 Jun 2020 14:10:34 +0000 (11:10 -0300)]
Changing default language (#4561)
Useful to avoid issues when a language is not set and it cannot be easily inferred (for example via the API). Since the language that covers most operators in CVC4 is the SMT one we use that as default now.
Haniel Barbosa [Fri, 5 Jun 2020 12:54:51 +0000 (09:54 -0300)]
Printing FP values as binary or indexed BVs according to option (#4554)
Andres Noetzli [Fri, 5 Jun 2020 12:22:18 +0000 (05:22 -0700)]
Fix handling of Boolean term variables (#4550)
Fixes #4446. This commit fixes two issues related to the handling of
Boolean term variables:
Removing Boolean subterms and replacing them with a Boolean term
variable introduces an equality of the form (= v t) where v is the
Boolean term variable and t is the term. It is important that these
equalities do not get removed. This commit changes
Theory::isLegalElimination() to take this into account.
The incorrect model reported in the issue was caused by some of the
Boolean term variables not being assigned values by the SAT solver
when we decided that the benchmark is satisfiable. Our justification
heuristic (correctly) decided that it is enough to satisfy one of the
disjuncts in the assertion to satisfy the whole assertion. However,
the assignments that we received from the SAT solver restricted us to
pick a specific value for one of the Boolean constants:
Literal | Value | Expr
---------------------------------------------------------
'7 ' 0 c
'0 ' 1 true
'1 ' 0 false
'2 ' 0 (a BOOLEAN_TERM_VARIABLE_274)
'5 ' _ b
'3 ' 1 (a BOOLEAN_TERM_VARIABLE_277)
'4 ' _ BOOLEAN_TERM_VARIABLE_274
'6 ' 0 BOOLEAN_TERM_VARIABLE_277
This meant that we had to pick true for BOOLEAN_TERM_VARIABLE_274
but we picked false since we simply treated it as an unassigned
variable. In general, the justification heuristic handles embedded
skolems introduced by term removal first and asks the SAT solver to
decide on Boolean term variables. However, for some logics, such as
QF_AUFLIA, we use the justification heuristic not for decisions but
only to decide when to stop, so those decisions were not done. This
commit introduces a conservative fix that adds a check after
satsifying all the assertions that makes sure that the equalities
introduced for Boolean terms are satisfied as well. Due to the eager
treatment of Boolean term variables when we use the justification
heuristic also for decisions, it is likely that we don't really have
the problem in that case but it doesn't hurt to enable the fix. It is
also possible that this fix is only required with models but it is
definitely safer to just always enable it (there could be tricky
corner cases involving the theory combination between UF and Boolean
terms). Additionally, this commit changes the ITE-specific naming in
the justification heuristic to reflect more accurately that we are in
general dealing with skolems introduced by term removals and not only
due to ITE removal.
Andres Noetzli [Fri, 5 Jun 2020 12:03:16 +0000 (05:03 -0700)]
Fix lifetime and copy issues with NodeDfsIterable (#4569)
When running node_traversal_black with ASan and UBSan, there were two
distinct issues being reported. UBSan was complaining that we were
assigning an invalid value to a Boolean. This happened because
d_initialized in NodeDfsIterator was uninitialized and the default
copy constructor tried to copy it. This commit removes that data member.
ASan was complainig that NodeDfsIterator::begin() was trying to access
a skip function that had been freed. In particular, this happened when
NodeDfsIterable was used in a range-based for loop like so:
for (auto n : NodeDfsIterable(n).inPostorder())
{
...
}
The problem here is that the lifetime of a temporary within the range
expression is not extended (the lifetime of the result of the range
expression is extended, however) [0]. This is a problem because
NodeDfsIterable(n) is a temporary and inPostorder() returns a
reference to that temporary. It makes sense that the compiler cannot
possibly know that the reference from inPostorder() corresponds to
NodeDfsIterable(n), so it cannot extend its lifetime. See [1] for more
details on the problem with chained functions.
This commit fixes the issue by replacing the fluent interface of
NodeDfsIterable by a constructor with default arguments. Additionally,
it introduces an enum to represent the visit order to avoid having a
nondescript Boolean argument.
[0] https://en.cppreference.com/w/cpp/language/range-for#Temporary_range_expression
[1] http://cpptruths.blogspot.com/2018/10/chained-functions-break-reference.html?m=1
Andrew V. Jones [Fri, 5 Jun 2020 02:18:16 +0000 (03:18 +0100)]
If using 'ninja', tell the user to run 'ninja' not 'make' (#4568)
## Issue
If you call CVC4's `configure` script with `--ninja`, then you get a misleading status message:
```
[avj@tempvm CVC4]$ ./configure.sh --ninja --python3 | tail -n 5
Now change to 'build' and type make, followed by make check or make install.
-- Configuring done
-- Generating done
-- Build files have been written to: /home/avj/working/CVC4/build
```
## Solution
This commit simply fixes the status message to tell the user to run the correct command based on the specified generator:
```
[avj@tempvm CVC4]$ ./configure.sh --ninja --python3 | tail -n 5
Now change to 'build' and type 'ninja', followed by 'ninja check' or 'ninja install'.
-- Configuring done
-- Generating done
-- Build files have been written to: /home/avj/working/CVC4/build
```
Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>
makaimann [Fri, 5 Jun 2020 01:21:37 +0000 (18:21 -0700)]
Add a method for retrieving base of a constant array through API (#4494)
Andres Noetzli [Fri, 5 Jun 2020 00:27:33 +0000 (17:27 -0700)]
Update Java tests to match changes in API (#4535)
Commit
cfeaf40ed6a9d4d7fec925352e30d2470a1ca567 renamed
`Result::Validity` and `SmtEngine::query()` to `Result::Entailment` and
`SmtEngine::checkEntailed()`, respectively. The commit did not update
the Java tests which lead to issues in debug builds with Java bindings.
The commit also adds a corresponding `NEWS` entry.
makaimann [Thu, 4 Jun 2020 22:18:35 +0000 (15:18 -0700)]
Wrap Result in Python API (#4473)
This PR would change the Python API to wrap the C++ Result class instead of translating it to a pure Python class. This is more convenient because there are several possibilities other than sat/unsat/unknown. Furthermore, this PR updates the bitvectors.py example which had an incorrect function name "checkEntailment" and adds a floating point example contributed by Eva Darulova.
Aina Niemetz [Thu, 4 Jun 2020 18:07:41 +0000 (11:07 -0700)]
New C++ Api: Second and last batch of API guards. (#4563)
This adds the remaining API guards in the Solver object (incl. unit tests).
Andrew Reynolds [Thu, 4 Jun 2020 17:38:36 +0000 (12:38 -0500)]
Add sygus datatype substitution utility method (#4390)
This makes the method for substiutiton and generalization of sygus datatypes a generic utility method. It updates the abduction method to use it. Interpolation is another target user of this utility.
Andrew Reynolds [Thu, 4 Jun 2020 16:31:55 +0000 (11:31 -0500)]
Fix abduction with datatypes (#4566)
Previously we were treating constructor/selector/tester symbols as arguments to the abduct-to-synthesize.
Andrew Reynolds [Thu, 4 Jun 2020 14:52:55 +0000 (09:52 -0500)]
Theory strings preprocess (#4534)
This makes it so that the main reduce function in TheoryStringsPreprocess is static, so that it can be used both by the solver and the proof checker.
It also updates the functions to make use of IndexVar for constructing canonical universal variables.
Aina Niemetz [Thu, 4 Jun 2020 03:56:24 +0000 (20:56 -0700)]
New C++ Api: First batch of API guards. (#4557)
This is the first batch of API guards, mainly extending existing guards
in the Solver object with checks that Ops, Terms, Sorts, and datatype objects
are associated to this solver object.
This further changes how DatatypeConstructorDecl objects are created. Previously,
they were not created via the Solver object (while DatatypeDecl was). Now, they are
created via Solver::mkDatatypeConstructorDecl, consistent with how DatatypeDecl
objects are created.
Haniel Barbosa [Wed, 3 Jun 2020 23:52:49 +0000 (20:52 -0300)]
(proof-new) Adding rules and proof checker for EUF (#4559)
Haniel Barbosa [Wed, 3 Jun 2020 21:54:47 +0000 (18:54 -0300)]
(proof-new) Adding rules and proof checker for Boolean reasoning (#4560)
Andrew Reynolds [Wed, 3 Jun 2020 19:01:13 +0000 (14:01 -0500)]
(proof-new) Add builtin proof checker (#4537)
This adds the proof checker for TheoryBuiltin, which handles the core proof rules (SCOPE and ASSUME) and all proof rules corresponding to generic operations on Node objects. This includes proof rules for rewriting and substitution, which are added in this PR.
Mathias Preiner [Wed, 3 Jun 2020 14:12:07 +0000 (07:12 -0700)]
Fix normalization of author names in contrib/get-authors. (#4553)
Andrew Reynolds [Wed, 3 Jun 2020 13:47:46 +0000 (08:47 -0500)]
Do not apply unconstrained simplification when quantifiers are present (#4532)
Fixes #4437.
This is a simpler fix that aborts the preprocessing pass when a quantifier is encountered.
It also updates our smt2 parser to throw a logic exception when forall/exists is used in non-quantified logics. This is required to ensure that unconstrained simplification does not throw an exception to a user as a result of accidentally setting the wrong logic.
Andrew Reynolds [Wed, 3 Jun 2020 13:08:04 +0000 (08:08 -0500)]
Update CEGQI to use lemma status instead of forcing preprocess (#4551)
This PR removes a hack in counterexample-guided quantifier instantiation.
The issue is the CEGQI needs to know the form of certain lemmas, after theory preprocessing. CEGQI needs to know this since it must construct solutions (e.g. solved form of equalities) for free variables in these lemmas, which includes fresh variables in the lemma after postprocess like ITE skolems.
Previously, CEGQI was hacked so that it applied the preprocessing eagerly so that it had full knowledge of the postprocessed lemma. This PR updates CEGQI so that it uses the returned LemmaStatus as the way of getting the lemma after postprocess. It also fixes the lemma status returned by TheoryEngine so that all lemmas not just the "main lemma" are returned as a conjunction.
This PR is in preparation for major refactoring to theory preprocessing for the sake of proofs.
Andrew Reynolds [Wed, 3 Jun 2020 01:57:58 +0000 (20:57 -0500)]
Use prenex normal form when using cegqi-nested-qe (#4522)
Previously, we used a specialized variant of prenex normal form that allowed top level disjunctions. However, the method to put quantifiers into this form led to variable shadowing on some benchmarks in SMT-LIB LRA.
This simplifies the code so that we use standard prenex normal form when cegqi-nested-qe is used and deletes the old variant (DISJ_NORMAL).
makaimann [Wed, 3 Jun 2020 01:10:18 +0000 (18:10 -0700)]
Add Term::substitute to Python bindings (#4499)
makaimann [Tue, 2 Jun 2020 22:18:15 +0000 (15:18 -0700)]
Add hash Op, Sort and Term in Python bindings (#4498)
Andrew Reynolds [Tue, 2 Jun 2020 20:55:49 +0000 (15:55 -0500)]
Fix scope issue with pulling ITEs in extended rewriter. (#4547)
Fixes #4476.
Andrew Reynolds [Tue, 2 Jun 2020 17:22:17 +0000 (12:22 -0500)]
Do not handle universal quantification on functions in model-based FMF (#4226)
Fixes #4225, fixes CVC4/cvc4-projects#159, fixes CVC4/cvc4-projects#157, fixes #4289, fixes #4483.
This makes it so that the main model-based instantiation algorithm is not applied to quantified formulas with universally quantified functions.
Identation changed in a FMF function, this was refactored to conform to guidelines, and further cleaned.
Aina Niemetz [Tue, 2 Jun 2020 16:09:15 +0000 (09:09 -0700)]
New C++ API: Keep reference to solver object in non-solver objects. (#4549)
This is in preparation for adding guards to ensure that sort and term
arguments belong to the same solver.
Andrew Reynolds [Mon, 1 Jun 2020 23:34:21 +0000 (18:34 -0500)]
(proof-new) Proof step buffer utilities (#4533)
This class is used for delaying proof node creation until it is necessary.
Andrew Reynolds [Mon, 1 Jun 2020 19:31:48 +0000 (14:31 -0500)]
Move non-linear files to src/theory/arith/nl (#4548)
Also makes CVC4::theory::arith::nl namespace.
This includes some formatting changes.
Andres Noetzli [Mon, 1 Jun 2020 17:14:56 +0000 (10:14 -0700)]
Set theoryof-mode after theory widening (#4545)
Fixes #4367. We set the theoryof-mode depending on whether sharing is
enabled or not. However, we were checking whether sharing was enabled
before theory widening, leading to unexpected results. This commit moves
the check after widening the theories.
For the benchmark in the issue, setting the theoryof-mode before theory
widening lead to problems because of the following:
The main solver checks the condition for enabling term-based
theoryof-mode, decides not to do it because sharing is not enabled
Main solver adds UF to the logic
Main solver does a check-sat all
Unsat core check runs, sees both UF and NRA enabled, and switches
to term-based mode
Main solver gets to second check-sat call, now the theoryof-mode is
suddenly changed, which leads to problems in the equality engine
This commit fixes the issue in this particular instance but it is important
to note that it does not address the issue of the subsolver changing
settings in general. This can only really be solved by separating the
options from the ExprManager/NodeManager and having separate
options for each SmtEngine/Solver instance.
Andres Noetzli [Mon, 1 Jun 2020 16:41:16 +0000 (09:41 -0700)]
Do not parse ->/lambda unless --uf-ho enabled (#4544)
Fixes #4477. Logic ALL includes higher-order but we currently do not
support solving higher-order problems unless --uf-ho is enabled. This
commit changes the condition under which we parse -> and lambda to
only enabled parsing of those symbols if the logic allows higher-order
constraints and --uf-ho is enabled.
Andrew Reynolds [Mon, 1 Jun 2020 14:14:23 +0000 (09:14 -0500)]
Incorporate sequences into the word interface (#4543)
Also renames a function mkWord -> mkWordFlatten.
Andres Noetzli [Sun, 31 May 2020 16:13:39 +0000 (09:13 -0700)]
Do not cache operator eliminations in arith (#4542)
Fixes #4525. The actual problem in the issue is not that the unsat core
is satisfiable but that our unsat core check is not working as intended.
Our unsat core check uses the same `ExprManager` as the main `SmtEngine`
and thus also shares the same attributes for nodes. However, since we
have a different `SmtEngine` instance for the check, we also have
different instances of `TheoryArith`. This leads to the check failing
due to the following:
- Our only input assertion is `(> (cot 0.0) (/ 1 0)))`.
- `TheoryArith::expandDefinition()` gets called on `(> (cot 0.0) (/ 1
0))` but nothing happens.
- `TheoryArith::expandDefinition()` gets called on `(/ 1 0)`, which gets
expanded as expected but no attribute is set because it happens in a
simple `TheoryArith::eliminateOperators()` call.
- `TheoryArith::expandDefinition()` on `(cot (/ 0 1))` first expands to
`(/ 1 0)` (not cached) and then we expand it recursively to the
expected term and cache `(/ 1 0) ---> (ite (= 0 0) (divByZero 1.0) (/
1 0))`.
Up to this point, things are suboptimal but there are no correctness
issues. The problem starts when we do the same process in the unsat core
check:
- Our only input assertion is again `(> (cot 0.0) (/ 1 0)))`.
- `TheoryArith::expandDefinition()` gets called on `(> (cot 0.0) (/ 1
0))` but nothing happens.
- `TheoryArith::expandDefinition()` gets called on `(/ 1 0)`, which gets
expanded as expected but no attribute is set or checked because it
happens in a simple `TheoryArith::eliminateOperators()` call. Note
that the skolem introduced here for the division-by-zero case is
different from the skolem introduced above because this is in a
different `TheoryArith` instance that does not know the existing
skolems.
- `TheoryArith::expandDefinition()` on `(cot (/ 0 1))` first expands to
`(/ 1 0)` (not cached) and then we use the cache from our solving call
to expand it `(/ 1 0) ---> (ite (= 0 0) (divByZero 1.0) (/ 1 0))`.
Note that `divByZero` here is the skolem from the main solver.
As a result, the preprocessed assertions mix skolems from the main
`SmtEngine` with the `SmtEngine` of the unsat core check, making the
constraints satisfiable.
To solve this problem, this commit removes the caching-by-attribute
mechanism. The reason for removing it is that it is currently
ineffective (since most eliminations do not seem to be cached) and there
are caches at other levels, e.g. when expanding definitions. If we deem
the operator elimination to be a bottleneck, we can introduce a similar
mechanism at the level of `TheoryArith`.
yoni206 [Sun, 31 May 2020 04:17:59 +0000 (21:17 -0700)]
update example in README to use ctest. (#4540)
An example for restricting timeout in tests uses the old `make regress0` instead of the new `ctest -L regress0`
Andrew Reynolds [Sat, 30 May 2020 18:10:54 +0000 (13:10 -0500)]
Add the sequence type (#4539)
This adds basic infrastructure for the sequence type, including its type rules, type enumerator and extensions to type functions.
The next step will be to finalize the support in TheoryStrings for sequences and then add front end support for sequences in the API/parsers.
Andrew Reynolds [Thu, 28 May 2020 20:05:06 +0000 (15:05 -0500)]
Fix term registry for constant case, simplify. (#4538)
We were getting an assertion failure (causing nightlies to fail) due to the recent optimization to the strings skolem cache (
978f455). This ensures we ignore constant strings in TermRegistry::getRegisterTermAtomicLemma.
It also removes a deprecated option that is deleted in the proof-new branch.
Andrew Reynolds [Wed, 27 May 2020 23:05:07 +0000 (18:05 -0500)]
Add the Expr-level sequence datatype (#4526)
This adds the expr-level sequence datatypes. This is required for further progress on sequences. However, note that this class may be deleted in the further when the Expr level is replaced.
Martin [Wed, 27 May 2020 18:26:51 +0000 (19:26 +0100)]
Tweak the use of static_assert to support older compilers. (#4536)
C++11 introduces static_assert(bool, string).
C++17 introduces static_assert(bool)
By adding a message we can support older compilers such as those
used by our nightly build system...
Martin [Tue, 26 May 2020 18:49:01 +0000 (19:49 +0100)]
Fix an incorrect limit in conversion from real to float (#4418)
This error is a bit inexplicable but very very definitely wrong.
A test case from the original bug report is included.
Andrew Reynolds [Tue, 26 May 2020 17:41:31 +0000 (12:41 -0500)]
Convert more uses of strings to words (#4527)
Mathias Preiner [Tue, 26 May 2020 16:44:51 +0000 (09:44 -0700)]
Fix mismatched iterators (CID
1493892). (#4531)
Issue found by coverity.
Andrew Reynolds [Tue, 26 May 2020 15:27:45 +0000 (10:27 -0500)]
(proof-new) Update proof checker. (#4511)
This adds new required features to proof checker and the base class of proof rule checker.
This is required as the first dependency towards merging further infrastructure related to proofs.
Andrew Reynolds [Tue, 26 May 2020 14:51:13 +0000 (09:51 -0500)]
(proof-new) Updates to strings skolem cache. (#4524)
This PR makes strings skolem cache call the ProofSkolemCache. This is required for proper proof checking, as it makes all skolems be associated with their formal definition, encapsulated by a witness term.
It furthermore makes skolem sharing more uniform and aggressive by noting that most string skolems correspond to purification variables (typically for some substr term). A purification variable for a term that rewrites to a constant can be replaced by the constant itself.
It also introduces an attribute IndexVarAttribute which is used to ensure reductions involving universal variables are deterministic.
Mathias Preiner [Tue, 26 May 2020 01:56:39 +0000 (18:56 -0700)]
Update to CaDiCaL version 1.2.1. (#4530)
Andres Noetzli [Sun, 24 May 2020 03:52:29 +0000 (20:52 -0700)]
[SMT-COMP] Redirect non-answers to /dev/null (#4528)
Commit
00badd3a63a2fa568373d5c58553944b579d42bb changed our run script
to write output other than `sat`/`unsat` to a file if `$2` is passed to
it. However, it looks like StarExec does not pass that parameter to our
script despite the documentation claiming that it does [0]. This commit
makes our check more defensive by redirecting our unnecessary output to
`/dev/null` if `STAREXEC_WALLCLOCK_LIMIT` is set. I've done a quick test
run on StarExec and it looks like this does the trick.
[0]
https://wiki.uiowa.edu/display/stardev/User+Guide#UserGuide-SpecialVariables
mudathirmahgoub [Sat, 23 May 2020 15:28:50 +0000 (10:28 -0500)]
remove unused field d_emp_exp in TheorySetsPrivate (#4521)
Remove unused field d_emp_exp in TheorySetsPrivate
Andrew Reynolds [Sat, 23 May 2020 12:13:42 +0000 (07:13 -0500)]
Add the sequence datatype (#4153)
This class is the Node-level representation of a sequence. It is analogous to CVC4::String.
Abdalrhman Mohamed [Sat, 23 May 2020 04:55:29 +0000 (23:55 -0500)]
Fix mistakes in sygus API comments. (#4520)
Andrew Reynolds [Sat, 23 May 2020 03:39:16 +0000 (22:39 -0500)]
Refactor operator elimination in arithmetic (#4519)
This is a major refactor of how operators are eliminated in arithmetic. Currently there were (at least) two things wrong:
(1) ppRewriteTerm sent lemmas on the output channel. This behavior is incompatible with how preprocessing works. In particular, this caused unconstrained simplification to be unaware of terms from such lemmas, leading to incorrect "sat" answers.
(2) Lemmas used to eliminate certain "div-like" terms were processed in a context-independent way. However, lemmas should be cached in a user-context-dependent way. This was leading to incorrect "sat" answers in incremental.
The solution to these issues is to eliminate operators via the construction of witness terms. No lemmas are sent out, and instead these lemmas are the consequence of term formula removal in the standard way.
As a result of the refactor, 2 quantifiers regressions time out due to infinite branch and bound issues (one only during --check-unsat-cores). These appear to be random and I've changed the options to avoid these issues. 3 others now have check-model warnings, which I've added --quiet to. Improving check-model will be addressed on a future PR.
This PR is not required for SMT COMP since we have workarounds that avoid both the incorrect behaviors in our scripts.
Also notice that --rewrite-divk is effectively now enabled by default always.
Fixes #4484, fixes #4486, fixes #4481.
Andres Noetzli [Fri, 22 May 2020 22:33:04 +0000 (15:33 -0700)]
[SMT-COMP] Use tear-down-incremental for arithmetic (#4518)
This commit changes the run-script for the incremental track to use
`--tear-down-incremental=1` for all logics that involve arithmetic. The
main motivation for this change is avoid issues that we have with the
lemmas generated for `mod`/`div` during `ppRewrite` that cause
model-soundness issues.
Aina Niemetz [Fri, 22 May 2020 21:09:54 +0000 (14:09 -0700)]
CaDiCaL: Clean up initialization on creation. (#4516)
Andrew Reynolds [Fri, 22 May 2020 19:27:13 +0000 (14:27 -0500)]
(proof-new) Add rewrite corresponding to regular expression inclusion (#4513)
This introduces a rewrite based on regular expression inclusion (using calls to the RegExpEntail utility function).
This allows us to justify the regular expression inclusion inference as a rewrite.
Aina Niemetz [Fri, 22 May 2020 16:47:55 +0000 (09:47 -0700)]
Cryptominisat: Clean up initialization on creation. (#4515)
Aina Niemetz [Fri, 22 May 2020 13:41:50 +0000 (06:41 -0700)]
Add support for SAT solver Kissat. (#4514)
Andrew Reynolds [Fri, 22 May 2020 13:01:59 +0000 (08:01 -0500)]
(proof-new) Proof node to SExpr utility. (#4512)
This is required for dag-ifying ProofNode output.
Andrew Reynolds [Fri, 22 May 2020 04:40:44 +0000 (23:40 -0500)]
Update string kind names in new API (#4509)
To match the smt2 Unicode standard. The internal ones are left unchanged for now.