Relax what is generated in the model from NL (#8113)

This makes it so that we don't assign concrete values to equivalence classes with transcendental functions.

It also removes some unused infrastructure.

[proofs] [dot] Enable DAG and tree printing with dot files (#8107)

Add a proof option that allows DAG and tree print format when using dot files.

Signed-off-by: Vinícius Braga Freire vinicius.braga.freire@gmail.com

Fixes and additions for LFSC signatures (#8120)

Fixes a critical issue in the re intersection rule, where a null terminator was missed.

Also adds a sketch of the theory signature for floating points.

Add unit test for fixed issue with get-difficulty (#8060)

Fixed by recent updates to get-difficulty.

Fixes cvc5/cvc5-projects#434.

Throw option exceptions when combining input conversion preprocessing with sygus (#8059)

Fixes cvc5/cvc5-projects#436.

Add well formed term check to solver engine (#8056)

Fixes cvc5/cvc5-projects#413.

Improve `STRINGS_ARRAY_UPDATE_BOUND` inference (#8123)

This changes the `STRINGS_ARRAY_UPDATE_BOUND` inference to explicitly
include the disequality between the term before and after the update if
the update has an effect. This is an optimization that prevents us from
splitting on that (dis-)equality later on.

Make spurious assertion into warning (#8051)

Fixes cvc5/cvc5-projects#401.

Fix `STRINGS_ARRAY_NTH_UPDATE` inference (#8121)

Our `STRINGS_ARRAY_NTH_UPDATE` inference was missing an explanation that
establishes the relation between the update and the nth term. On the
current set of benchmarks, this does not cause an issue, but there
should be cases where it does. The commit also changes the array core solver
to take better advantage of `d_indexMap`.

Introduce skolem function to make transcendental function purification consistent (#8116)

Previously, we could introduce multiple purifications for the same sin term.

Missing ids for arith conflicts (#8108)

Fixes #8097.

Remove some irrelevant node kinds from the model (#8110)

There are several kinds of nodes that are currently sent to the model that don't need to be. Furthermore, we require not sending some of these due to the new invariants in #8095.

[proofs] [alethe] Introduce all_simplify and replace old trust rules (#8100)

Instead of printing "trust" in the case of a simplification rule that cannot be translated to an Alethe simplify rule print "all_simplify". This also replaces the heuristic in THEORY_REWRITE to determine which simplify rule is needed.

[proofs] Consolidate multiple substitutions to single AND proof in trust substitution map (#8109)

This ensures that a common proof node is used for a substitution instead of copying its children. This optimization had been noted in a comment but had not yet been enabled.

This should speed up proof reconstruction for substitutions.

[proofs] Make cache (optionally) persistent in lazy CD proof (#8104)

Should address severe performance issues in some use cases of proofs.

Only consider relevant terms in the array-inspired sequence solver (#8105)

Avoids segfault in model construction due to asking for the value of irrelevant (non-shared) term.

Support `try` and `all` reconstruction modes. (#8098)

This PR adds a simple procedure to quickly reconstruct Sygus terms that are already in the grammar. This new procedure fails if the terms are not in the grammar.

Ensure proofs are fully disabled when incompatible (#8092)

Was causing regression failures on proof-new when proofs + sygus are enabled. We now force proofs to be disabled.

Fix for lambda-to-array constant conversion for unused arguments (#8082)

Fixes #4434.

Fix type check of `seq.nth` (#8093)

The code for type checking `seq.nth` was trying to retrieve the sequence
element type before ensuring that the type of the first argument was a
sequence, which lead to assertion failures. This commit reorders the
checks to avoid this issue.

Add assertion to require inference ids (#8091)

Use witness terms to represent values for large strings in models (#8089)

This makes it so that we don't prematurely fail on some Facebook benchmarks.

bv: Add --tlimit-per support for CryptoMiniSat. (#8086)

bv: Add --tlimit-per support for CaDiCaL. (#8085)

This commit adds --tlimit-per support for CaDiCaL via CaDiCaL's Terminator class.

Fixes #8049

Fix handling of `LogicException` during solving (#8000)

Fixes #7974. This commit fixes our handling of LogicExceptions during solving. Instead of leaving MiniSat in a bad state, it catches the exception, resets the decision trail, prints the error message, and then returns unknown.

[Seq] Fix rewrite of `(seq.nth s n)` for large `n` (#8083)

When rewriting (seq.nth s n) where both terms are constants, cvc5 was
blindly converting the n to a uint32_t, which caused issues when n
was greater than the largest value that can be represented by a 32-bit
integer. This commit introduces a corresponding check and does not
perform the rewrite for large n.

Add addition utilities for the arithmetic rewriter (#8013)

This PR adds methods to deal with sums in the arithmetic rewriter. Sums are stored as std::map<Node,RealAlgebraicNumber> (see the code for some reasoning), and we implement adding terms to sums, collecting sums into nodes and distributing a multiplication over nested sums.

Simplify formalism of introduced arithmetic skolems (#8073)

This ensures that all skolems introduced by arithmetic have concrete terms as witnesses. This avoids introducing witness terms.

This PR is important for ensuring that the "original form" of terms does not contain introduced free variables. This means that certain features (quantifier elimination, learned literals) are useful to the user. This was requested by Certora.

This also will improve proof reconstruction for extensions of non-linear arithmetic.

It also ensures that we share skolems in some cases, e.g. we use the same skolem for eliminating (div x y) and (mod x y).

Distinguish proof mode from unsat core mode (#8062)

Previously, we were making unsat cores mode the source of our configuration for unsat cores and proofs at the same time.

This led to a lot of unnecessary complication in the logic, and would allow bugs e.g. if produce-difficulty but not produce-unsat-cores was enabled.

Fixes cvc5/cvc5-projects#406.

Fix LFSC node conversion for non-shared selectors (#8078)

Print more commonly used murxla commands (#8046)

Given that murxla requires multiple invocations with different arguments for a typical workflow, I found it very helpful to have them recalled whenever I build it.

Always produce assertions (#8041)

There is no reason to disable --produce-assertions, this simplifies the code to assume that assertions are always available, and always warns if the user disables this option.

Make witness form visited ref counted (#8081)

Fixes #8079.

Generalize LFSC concat unify for splitting constants (#8077)

Was causing LFSC proof failures on ~5 SMT-LIB strings benchmarks.

Add user documentation for resource limits (#8058)

Though we regularly get questions about how resource limits work, they were entirely undocumented. This PR adds some general explanation to the user docs.

Fix unsoundness in IAND solver (#8053)

Fixes #5461, fixes #8063. The initial lemma schema was assuming arguments were in bounds.

This also modifies the solver so that we throw logic exceptions when encountering iand or transcendentals.

Allow non-value model values (#8076)

We previously required model values to be "values", i.e., constants or constant-like stuff like real algebraic numbers or lambdas. This is an inherent problem for, e.g, transcendental models: the simplest model for a transcendental problem may legitimately be 3 * PI or PI + exp(3). This PR removes this restriction, only requiring that values are rewritten.

Improve combination of NRA and transcendentals (#8075)

This PR tackles two issues when combining transcendental reasoning with nonlinear arithmetic.
Firstly, the NRAT logic would inadvertently have transcendental reasoning disabled because we only checked for integers. This simply adds an additional check at the end to enforce transcendental reasoning if necessary.
Secondly, we assert that we never add multiple substitutions for the same variable. This weakens the check to allow add the very same substitution multiple times.
Fixes #7984.

[BV] Fix response of `RewriteConcat` (#8074)

RewriteConcat was returning REWRITE_DONE, but it could happen that
applying ExtractWhole was removing an extract around another
concat that could then be flattened (see added unit test for an
example). This commit makes the response more conservative and only
returns REWRITE_DONE if the node did not change.

Fix indexof_re reduction (#8065)

Fixes https://github.com/cvc5/cvc5/issues/6654.

Note that this regression now answers unknown with `--ext-rewrite-quant`; the regression without this option is added.

Correct search location for CLN libs (#8070)

On (e.g.,) openSUSE, the default install path (via CMake) for libraries is lib64 and not lib. However, FindCLN.cmake is hard-coded to only search in lib.

This PR corrects FindCLN.cmake such that the build looks in ${CMAKE_INSTALL_LIBDIR} instead.

Signed-off-by: Andrew V. Jones andrewvaughanj@gmail.com

[Seq] Check types for split on indices (#8066)

We applied `STRINGS_ARRAY_EQ_SPLIT` to pairs of `seq.nth` terms of
different types. This lead to assertion (in debug) and performance
problems (in production). The commit adds a type check.

Fix another rewrite involving iand (#8054)

Fixes #8052.

[Rewriter] Always rewrite again when kind changes (#8007)

Fixes cvc5/cvc5-projects#438. The rewriter
returned REWRITE_DONE prematurely when rewriting operators such as
bvand in certain cases. If only a single term was left after removing
duplicates from a bvand, the kind of the current node would change and
another pre-rewrite could apply, but the rewriter still returned
REWRITE_DONE. After adding an assertion in the rewriter that checks
that REWRITE_DONE implies that no other pre-rewrite applies, it was
discovered that not only the bit-vector rewriter has this issue, but
other rewriters, e.g., the Boolean rewriter, as well. This commit
changes our semantics for REWRITE_DONE to mean that no other rewrite
applies provided that the kind did not change. This makes it easier for
developers to decide when to return REWRITE_DONE, because it only
requires reasoning about rewrites that apply to a single kind.

Standardizing notifications for setting options in set_defaults (#8057)

FP: Rename tester kinds. (#8037)

This renames FP tester kinds for consistency:
FLOATINGPOINT_ISINF -> FLOATINGPOINT_IS_INF
FLOATINGPOINT_ISN -> FLOATINGPOINT_IS_NORMAL
FLOATINGPOINT_ISNAN -> FLOATINGPOINT_IS_NAN
FLOATINGPOINT_ISNEG -> FLOATINGPOINT_IS_NEG
FLOATINGPOINT_ISPOS -> FLOATINGPOINT_IS_POS
FLOATINGPOINT_ISZ -> FLOATINGPOINT_IS_ZERO

Use Add instead of Plus (#8043)

This fixes the current documentation builds for the pythonic API

Simplify handling of disequalities in strings (#8047)

This simplifies how string disequalities are handled, and fixes a caching bug in our implementation of extensionality.

The simplifications are two-fold:
- We track disequalities via assertions, not via an equality engine callback
- We process disequalities by iterating on the disequality list, not via iterating on pairs of equivalence classes

Extensionality is fixed by not *explaining* disequalities, which leads to being out of sync with the cache (as the disequality could have a different explanation in another SAT context).

This fixes the last known issues with `--seq-array=X`.

Improve theory combination over real algebraic models (#8045)

Though we support real algebraic models now for theory combination, cvc5/cvc5-projects#451 uncovered the possibility to assert if an equality was in fact not equal during theory combination and the difference was real algebraic.
This PR fixes this issue by adding the proper check.
Fixes cvc5/cvc5-projects#451.

Eliminate even more static uses of rewrite (#8044)

Test proof granularity theory-rewrite by default (#8038)

Recently we updated proof granularity to be macro by default, but we should test theory-rewrite granularity in our regressions.

Replace a some more static options (#8042)

We now have access to the options in a few more places in quantifiers.

Eliminate more static uses of rewrite (#8040)

Add table.product operator (#8020)

Add miscellaneous missing theory definitions for LFSC (#8039)

Add node utils for the arithmetic rewriter (#8012)

This PR adds a bunch of small utilities to inspect or create nodes in the arithmetic rewriter.

Send all `nth` terms to the core array solver (#7990)

This updates our policy for the sequences array solver to send all
updates to the array core solver.

Rename kind PLUS -> ADD. (#8036)

This renames the arithmetic internal and API kind PLUS to ADD for
consistency with our naming scheme for other operators (e.g.,
BITVECTOR_ADD, FLOATINGPOINT_ADD).

api: Remove obsolete function declaration in Cython bindings. (#8032)

api: Rename kinds MINUS -> SUB and UMINUS -> NEG. (#8034)

This renames the arithmetic kinds MINUS and UMINUS on the
API level for consistency with our naming scheme for other
operators (e.g., BITVECTOR_SUB, FLOATINGPOINT_SUB).

api: Add explicit guard for option produce-assertions in blockModelValues(). (#7958)

Fixes cvc5/cvc5-projects#412.

Change name of Python API's package from pycvc5 to cvc5. (#7953)

In the process, I changed a CMake target name from pycvc5 to
cvc5_base_py_api. I could not change the target to cvc5, because that
name is taken.

Fix rewrite for eliminating constant factors of PI from argument to sine (#8031)

Fixes cvc5/cvc5-projects#441.
Fixes cvc5/cvc5-projects#414.

Rename kinds MINUS -> SUB and UMINUS -> NEG. (#8035)

This renames the internal arithmetic kinds MINUS and UMINUS for
consistency with our naming scheme for other operators (e.g.,
BITVECTOR_SUB, FLOATINGPOINT_SUB).

Use proper filename in -o subs documentation (#8030)

We somehow used the wrong filename in #7944.

Fix invalid rewrite involving iand (#8026)

Fixes #8016.

api: Rename mk<Value> functions for FP for consistency. (#8033)

Fix printing of re.loop as an operator in LFSC (#8029)

Make LFSC side condition for concat unify robust to equality with full string (#8028)

Was leading to LFSC proof checking failures.

Add missing null terminators for regexp (#8027)

Led to some LFSC proof checking failures on strings benchmarks.

Add additional check to avoid cyclic substitution (#7991)

The substitutions we extract from equalities in the nonlinear solver would sometimes generate cyclic substitutions.
This PR tries harder to avoid such cases.
Fixes cvc5/cvc5-projects#444.

Update datatypes.rst (#8009)

Remove more static calls to rewrite (#8025)

Extend proof step buffer to optionally ensure unique conclusions (#8017)

Fixes cvc5/cvc5-projects#439.

This extended (theory) proof step buffer with options for discarding duplicate conclusions. This option is now used in the strings theory proof construction, which may have duplication of conclusions due to purification. It simplifies some of the logic regarding popStep in this utility which is required due to the new policy.

Fix parser issue with tuple_project operator (#8021)

The current parser accepts the smtlib code below since it ignores all arguments after z.
This PR fixes this issue by sending all arguments to the operator to be checked.

(set-logic ALL)
(declare-fun z () (Tuple Int Int Int Int Int Int))
(declare-fun f () (Tuple Int Int Int))
(assert (= f ((_ tuple_project 0 1 2) z f f f f f f f f 0 0 0 0 0)))
(check-sat)

[BV] Fix strategy for `RewriteExtract` (#8011)

`RewriteExtract` was being too eager to return `REWRITE_DONE`. In
particular, it could happen that a term could be rewritten by a series
of `ExtractExtract` and `ExtractConcat` rewrites, but the method would
return `REWRITE_AGAIN` after the first application of `ExtractExtract`.
This commit fixes the method to be more conservative and return
`REWRITE_AGAIN` whenever a rewrite changed the node being rewritten.
Additionally, the commit makes constant folding the last step (to
maximize the chances that it applies) and makes `ExtractExtract` rewrite
multiple nested applications of `extract` with a single application.

[BV] Fix order of rewrites for `concat` (#8010)

This commit fixes the order of the rewrites for bit-vector
concatentation such that the rewrite that merges adjacents constants
comes last (the commit also updates the comments to be less confusing).
Before, it could happen that the rewrite step that removes unnecessary
extract operations introduces constants then then would not get merged
before returning REWRITE_DONE.

Add new ordering utility (#8008)

This PR provides a clean implementation of the comparators from the normal form utility, also supporting real algebraic numbers. They will be used within the refactored arithmetic rewriter.

Add variant of get-difficulty for full effort lemmas (#8018)

Add variant of get-difficulty for full effort lemmas

[Arrays] Fix response for `store` chains (#8015)

When rewriting applying the rule store(store(a,i,v),i,w) ---> store(a,i,w), the arrays rewriter would return REWRITE_DONE. However,
this is incorrect if there are three or more nested stores of that kind
or the rewrite store(a,i,select(a,i)) ---> a applies to the result.
This commit fixes the response to always be REWRITE_AGAIN.

Add bag.filter operator (#8006)

Consider RANs in variable ordering (#7964)

The variable ordering in the arithmetic normal form should also consider real algebraic numbers. This PR also adds new comparators (essentially doing the same) in the rewriter that will replace the normal form utility classes.

Add utilities for flattening nodes (#7961)

This PR adds new utilities for flattening nodes and checking whether they can be flattened. They replace the custom implementation we used in the arithmetic rewriter.

Fix memory leak in quantifier info (#8005)

Fixes #8001. One of the maps in `QuantInfo` was containing
heap-allocated objects that were not being destroyed. This commit
changes the raw pointers to `std::unique_ptr<MatchGen>` to avoid the
memory leak.

Rename docs-releases to docs (#7999)

This renames the repository URL where documentation for releases is stored. It now lives at https://cvc5.github.io/docs/

Start post-release for 0.0.7

Bump version to 0.0.7

Try a bit harder on the EQ_NCTN rewrite rule (#7998)

This makes a small change to the sequence rewriter to work a bit harder
on one of the rewrite rule. This fixes some performance issues we've
observed.

Signed-off-by: Bruno Dutertre <dutebrun@amazon.com>

Fix docs upload once again (#7997)

This PR finally sorts out the ambiguity of different commits from PRs, tags and regular branches (fingers crossed).

[Rewrite Synthesis] Fix args for non-chaining ops (#7996)

Fixes https://github.com/cvc5/cvc5-projects/issues/445. Fixes
https://github.com/cvc5/cvc5-projects/issues/446. The issue is related
to the preprocessing pass for doing rewrite rule synthesis based on the
input. It was removing duplicate arguments from both chaining operators
and non-chaining operators when constructing the corresponding
datatypes. In the case of non-chaining operators, it could happen that
the constructor of the datatype did not have the correct number of
arguments for a given kind if there was a term where multiple arguments
were the same. This commit fixes the issue by doing the duplicate
elimination only for chaining operators.

Document substitute in API (#7904)

Update AUTHORS und copyright of docs configuration. (#7994)

Properly recognize whether the current commit is a tag (#7989)

This actually fixes what #7901 tried: when uploading the documentation, we need to figure out whether it was a tag and we should upload as a release as well.
Furthermore it fixes how we setup the deploy keys.

Initial refactoring of conflict-based instantiation (#7380)

This done an initial pass at refactoring conflict-based instantiation (the code has been largely unchanged since it was written in early 2014). This code is a bottleneck on some Facebook benchmarks and needs revisiting.

This changes the style so the parent modules are made data members instead of passed to methods. Otherwise, it changes int -> size_t wherever applicable, although int is often used to denote possibly valid indices where -1 means invalid.

It updates to use range-based for loops and mostly organizes the order of data members in classes to meet style guidelines.

Followup PRs will make more significant refactoring, e.g. to split the classes into multiple utilities.

Add Card solver to bags (#7986)

This PR avoids reducing bag.card terms with quantifiers unless it is needed.
It does so by building a cardinality graph for bags and adds appropriate constraints on internal nodes in the graph and min size constraints for the leaves.
This works for many of the benchmarks where each internal node has a single set of children.
Reduction lemmas are only generated when there are multiple sets of children.
Cardinality for bag.difference_remove and bag.duplicate_removal is not supported and would handled in future PR

More fixes and improvements for query generator (#7988)

Includes proper printing of dumped benchmarks.

Add output -o post-asserts (#7987)

This is equivalent to -t assertions::post-everything.

Start post-release for 0.0.6

Bump version to 0.0.6

Send `nth(unit(...), ...)` terms to array solver (#7983)

This commit changes our policy of which terms we send to the array core
solver. Previously, we were not sending nth terms that
were applied to unit sequences. This was incorrect, because for example
the split STRINGS_ARRAY_EQ_SPLIT has to be applied to nth of units,
too, to guarantee model soundness: For example, if we have a disequality
nth(t1, i) != nth(unit(v), i), then we have to reason about the
(dis)equality of t1 and unit(v), because of the UF for the
out-of-bounds case of nth (i.e., we have to reason that Uf(t1, i) != Uf(unit(v), i), which requires t1 != unit(v)). Splitting on t1 = unit(v) is done by STRINGS_ARRAY_EQ_SPLIT.