cvc5.git
4 years ago(proof-new) Add quantifiers proof checker (#4593)
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.

4 years ago(proof-new) Update proof node, add proof node algorithm utility file. (#4600)
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.

4 years agoSupport AND/OR definitions in lambda to array rewriting (#4615)
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.

4 years agoBV: Add missing type check for BITVECTOR_REPEAT_OP. (#4614)
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.

4 years agoBV: Add missing type check for INT_TO_BITVECTOR. (#4613)
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.

4 years ago Do RE derivation inference only for concrete constant RE (#4609)
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.

4 years agoMove sygus datatype utility functions to their own file (#4595)
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.

4 years agoUpdate to consistent policy for removed terms in quantifier bodies. (#4602)
Andrew Reynolds [Fri, 12 Jun 2020 23:30:19 +0000 (18:30 -0500)]
Update to consistent policy for removed terms in quantifier bodies. (#4602)

4 years ago(proof-new) Term conversion proof generator utility (#4603)
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.

4 years ago(proof-new) Minor updates to strings base solver (#4606)
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.

4 years agoCardinality-related inferences per type in theory of strings (#4585)
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.

4 years ago(proof-new) Split TheoryEngine (#4558)
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.

4 years agoFix install of static builds (#4604)
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.

4 years agoAdd rewrite for str.replace_re. (#4601)
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.

4 years ago (proof-new) Add lazy proof utility (#4589)
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.

4 years ago(proof-new) Add eager proof generator utility. (#4592)
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/.

4 years ago(proof-new) Remove arith-snorm option. (#4591)
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.

4 years ago(proof-new) Theory proof step buffer utility (#4580)
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.

4 years agoAdd support for str.replace_re/str.replace_re_all (#4594)
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`.

4 years agoFix getKind for Python bindings (#4496)
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`.

4 years ago(proof-new) Refactor skolemization (#4586)
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.

4 years ago(proof-new) Add trust node utility (#4588)
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.

4 years agoLanguage bindings: Enable catching of exceptions (#2813)
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.

4 years agoEnsure correct CMake dependencies on Debug_tags.h/Trace_tags.h/git_versioninfo.cpp...
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>
4 years agoFix Java target and Relations example (#4583)
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.

4 years agoFix ambiguous overload in unit test (#4582)
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.

4 years ago(proof-new) Add abstract proof generator class (#4574)
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.

4 years agoFix Coverity issues (#4587)
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

4 years agoUse NlLemma utility for all lemmas in non-linear. (#4573)
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.

4 years agoFix destruction order in NodeManager (#4578)
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.

4 years agoKeep definitions when global-declarations enabled (#4572)
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.

4 years agoSmt2 parsing support for nested recursive datatypes (#4575)
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.

4 years agoDatatypes with nested recursion are not handled in TheoryDatatypes unless option...
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.

4 years ago(proof-new) Updates to CDProof (#4565)
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.

4 years agoSkip parse-error regression for comp builds (#4567)
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.

4 years ago(proof-new) Rename ProofSkolemCache to SkolemManager (#4556)
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.

4 years agoChanging default language (#4561)
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.

4 years agoPrinting FP values as binary or indexed BVs according to option (#4554)
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)

4 years agoFix handling of Boolean term variables (#4550)
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.

4 years agoFix lifetime and copy issues with NodeDfsIterable (#4569)
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

4 years agoIf using 'ninja', tell the user to run 'ninja' not 'make' (#4568)
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>
4 years agoAdd a method for retrieving base of a constant array through API (#4494)
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)

4 years agoUpdate Java tests to match changes in API (#4535)
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.

4 years agoWrap Result in Python API (#4473)
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.

4 years agoNew C++ Api: Second and last batch of API guards. (#4563)
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).

4 years agoAdd sygus datatype substitution utility method (#4390)
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.

4 years agoFix abduction with datatypes (#4566)
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.

4 years agoTheory strings preprocess (#4534)
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.

4 years agoNew C++ Api: First batch of API guards. (#4557)
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.

4 years ago(proof-new) Adding rules and proof checker for EUF (#4559)
Haniel Barbosa [Wed, 3 Jun 2020 23:52:49 +0000 (20:52 -0300)]
(proof-new) Adding rules and proof checker for EUF (#4559)

4 years ago(proof-new) Adding rules and proof checker for Boolean reasoning (#4560)
Haniel Barbosa [Wed, 3 Jun 2020 21:54:47 +0000 (18:54 -0300)]
(proof-new) Adding rules and proof checker for Boolean reasoning (#4560)

4 years ago(proof-new) Add builtin proof checker (#4537)
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.

4 years agoFix normalization of author names in contrib/get-authors. (#4553)
Mathias Preiner [Wed, 3 Jun 2020 14:12:07 +0000 (07:12 -0700)]
Fix normalization of author names in contrib/get-authors. (#4553)

4 years agoDo not apply unconstrained simplification when quantifiers are present (#4532)
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.

4 years agoUpdate CEGQI to use lemma status instead of forcing preprocess (#4551)
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.

4 years agoUse prenex normal form when using cegqi-nested-qe (#4522)
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).

4 years agoAdd Term::substitute to Python bindings (#4499)
makaimann [Wed, 3 Jun 2020 01:10:18 +0000 (18:10 -0700)]
Add Term::substitute to Python bindings (#4499)

4 years agoAdd hash Op, Sort and Term in Python bindings (#4498)
makaimann [Tue, 2 Jun 2020 22:18:15 +0000 (15:18 -0700)]
Add hash Op, Sort and Term in Python bindings (#4498)

4 years agoFix scope issue with pulling ITEs in extended rewriter. (#4547)
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.

4 years agoDo not handle universal quantification on functions in model-based FMF (#4226)
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.

4 years agoNew C++ API: Keep reference to solver object in non-solver objects. (#4549)
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.

4 years ago(proof-new) Proof step buffer utilities (#4533)
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.

4 years agoMove non-linear files to src/theory/arith/nl (#4548)
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.

4 years agoSet theoryof-mode after theory widening (#4545)
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.

4 years agoDo not parse ->/lambda unless --uf-ho enabled (#4544)
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.

4 years agoIncorporate sequences into the word interface (#4543)
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.

4 years agoDo not cache operator eliminations in arith (#4542)
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`.

4 years agoupdate example in README to use ctest. (#4540)
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`

4 years agoAdd the sequence type (#4539)
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.

4 years agoFix term registry for constant case, simplify. (#4538)
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.

4 years agoAdd the Expr-level sequence datatype (#4526)
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.

4 years agoTweak the use of static_assert to support older compilers. (#4536)
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...

4 years agoFix an incorrect limit in conversion from real to float (#4418)
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.

4 years agoConvert more uses of strings to words (#4527)
Andrew Reynolds [Tue, 26 May 2020 17:41:31 +0000 (12:41 -0500)]
Convert more uses of strings to words (#4527)

4 years agoFix mismatched iterators (CID 1493892). (#4531)
Mathias Preiner [Tue, 26 May 2020 16:44:51 +0000 (09:44 -0700)]
Fix mismatched iterators (CID 1493892). (#4531)

Issue found by coverity.

4 years ago(proof-new) Update proof checker. (#4511)
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.

4 years ago(proof-new) Updates to strings skolem cache. (#4524)
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.

4 years agoUpdate to CaDiCaL version 1.2.1. (#4530)
Mathias Preiner [Tue, 26 May 2020 01:56:39 +0000 (18:56 -0700)]
Update to CaDiCaL version 1.2.1. (#4530)

4 years ago[SMT-COMP] Redirect non-answers to /dev/null (#4528)
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

4 years agoremove unused field d_emp_exp in TheorySetsPrivate (#4521)
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

4 years agoAdd the sequence datatype (#4153)
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.

4 years agoFix mistakes in sygus API comments. (#4520)
Abdalrhman Mohamed [Sat, 23 May 2020 04:55:29 +0000 (23:55 -0500)]
Fix mistakes in sygus API comments. (#4520)

4 years agoRefactor operator elimination in arithmetic (#4519)
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.

4 years ago[SMT-COMP] Use tear-down-incremental for arithmetic (#4518)
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.

4 years agoCaDiCaL: Clean up initialization on creation. (#4516)
Aina Niemetz [Fri, 22 May 2020 21:09:54 +0000 (14:09 -0700)]
CaDiCaL: Clean up initialization on creation. (#4516)

4 years ago(proof-new) Add rewrite corresponding to regular expression inclusion (#4513)
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.

4 years agoCryptominisat: Clean up initialization on creation. (#4515)
Aina Niemetz [Fri, 22 May 2020 16:47:55 +0000 (09:47 -0700)]
Cryptominisat: Clean up initialization on creation. (#4515)

4 years agoAdd support for SAT solver Kissat. (#4514)
Aina Niemetz [Fri, 22 May 2020 13:41:50 +0000 (06:41 -0700)]
Add support for SAT solver Kissat. (#4514)

4 years ago(proof-new) Proof node to SExpr utility. (#4512)
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.

4 years agoUpdate string kind names in new API (#4509)
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.

4 years ago(proof-new) Minor update to strings solver state (#4510)
Andrew Reynolds [Fri, 22 May 2020 04:10:24 +0000 (23:10 -0500)]
(proof-new) Minor update to strings solver state (#4510)

4 years agoDisable re-elim by default (#4508)
Andrew Reynolds [Thu, 21 May 2020 23:33:14 +0000 (18:33 -0500)]
Disable re-elim by default (#4508)

Disabling re-elim performs better overall in many recent experiments.

4 years agoMake Grammar reusable. (#4506)
Abdalrhman Mohamed [Thu, 21 May 2020 18:01:14 +0000 (13:01 -0500)]
Make Grammar reusable. (#4506)

This PR modifies the Grammar implementation to make it reusable (i.e., can be copied or passed multiple times to synthFun/synthInv) with the catch that it becomes read-only after the first use.

4 years agoThrow logic exception for equality between regular expressions (#4505)
Andrew Reynolds [Thu, 21 May 2020 03:27:04 +0000 (22:27 -0500)]
Throw logic exception for equality between regular expressions (#4505)

Fixes #4503.

4 years agoFix missing check for cardinality one in unconstrained simplifier (#4504)
Andrew Reynolds [Thu, 21 May 2020 02:22:25 +0000 (21:22 -0500)]
Fix missing check for cardinality one in unconstrained simplifier (#4504)

Fixes #4482.

4 years agoNormal form equality conflicts and uniqueness check (#4497)
Andrew Reynolds [Wed, 20 May 2020 15:20:34 +0000 (10:20 -0500)]
Normal form equality conflicts and uniqueness check (#4497)

This adds a new inference schema to strings that was discovered by the internal proof checker. It says that we are in conflict when an equality between the normal forms of two terms in the same equivalence class rewrites to false.

It also improves the efficiency of processing normal forms by only considering normal forms that are unique up to rewriting.

4 years agoAdd proof skolem cache (#4485)
Andrew Reynolds [Wed, 20 May 2020 14:14:54 +0000 (09:14 -0500)]
Add proof skolem cache (#4485)

This adds the general utility for maintaining mappings from Skolems to their witness form via attributes.

I am sending this as a PR now since it would be helpful to use this class for fixing some of the recent unconstrained-simp bugs.

4 years agoFix parametric datatype instantiation (#4493)
Andrew Reynolds [Wed, 20 May 2020 12:47:24 +0000 (07:47 -0500)]
Fix parametric datatype instantiation (#4493)

A bug was introduced when adding the Node-level datatype implementation in d803e7f. The code did not probably get the arity of a sort constructor. This adds TypeNode::getSortConstructorArity and uses it during parametric datatype type resolution.

4 years agoCegqiBv: Clean up after renaming options. (#4487)
Aina Niemetz [Wed, 20 May 2020 07:08:43 +0000 (00:08 -0700)]
CegqiBv: Clean up after renaming options. (#4487)

4 years agoUse debug-check-model to enable internal debugging in check-model (#4480)
Andrew Reynolds [Wed, 20 May 2020 05:05:58 +0000 (00:05 -0500)]
Use debug-check-model to enable internal debugging in check-model (#4480)

Notice this also updates our regression script to use --debug-check-model, preserving previous behavior.

Fixes #4461, fixes #4470, fixes #4471, fixes #4475, fixes #4448, fixes #4466, fixes #4460, fixes #4458, fixes #4455, fixes #4456, fixes #4386, fixes #4385, fixes #4478, fixes #4474.