| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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>
|
|
|
|
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.
|
|
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.
|
|
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.
|
|
Fixes #4075.
|
|
Fixes #4130.
This further makes an attempt at more consistent error printing.
|
|
The RE derive inference was not designed to handle re.comp. This makes the application of this inference more conservative.
|
|
Separates them from the core datatype utilities.
Code move only.
|
|
|
|
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.
|
|
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.
|
|
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.
|
|
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.
|
|
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.
|
|
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.
|
|
Adds an extension of CDProof where facts can be mapped to (lazy) proof generators.
|
|
Adds the eager proof generator. This lives in theory/ since it has utilities for generating TrustNode, which is specific to theory/.
|
|
This option only marginally helped and will be difficult to support with the new proof infrastructure.
|
|
This is a common class for adding steps for theory-specific proof rules into a ProofStepBuffer.
|
|
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`.
|
|
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`.
|
|
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.
|
|
This is a core data structure for associating a formula with a proof generator.
|
|
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.
|
|
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>
|
|
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.
|
|
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.
|
|
Also adds a commonly used proof generator: the proof reference proof generator.
|
|
This commit fixes the following Coverity issues:
- 1495606: uninitialized field
- 1495605: uninitialized field
- 1488953: uninitialized field
- 1495604: mismatched iterator
|
|
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.
|
|
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.
|
|
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.
|
|
Also includes some minor improvement to expand definitions in TheoryDatatypes leftover from the branch.
Adds 3 regressions using the option --dt-nested-rec.
|
|
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.
|
|
This updates CDProof with several new functionalities, including making it agnostic to symmetry of (dis)equalites.
|
|
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.
|
|
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.
|
|
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.
|
|
|
|
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.
|
|
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
|
|
## 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>
|
|
|
|
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.
|
|
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.
|
|
This adds the remaining API guards in the Solver object (incl. unit tests).
|
|
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.
|
|
Previously we were treating constructor/selector/tester symbols as arguments to the abduct-to-synthesize.
|
