cvc5.git
2 years agoFix another rewrite involving iand (#8054)
Andrew Reynolds [Sat, 5 Feb 2022 00:15:22 +0000 (18:15 -0600)]
Fix another rewrite involving iand (#8054)

Fixes #8052.

2 years ago[Rewriter] Always rewrite again when kind changes (#8007)
Andres Noetzli [Fri, 4 Feb 2022 19:04:07 +0000 (11:04 -0800)]
[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.

2 years agoStandardizing notifications for setting options in set_defaults (#8057)
Andrew Reynolds [Fri, 4 Feb 2022 17:55:27 +0000 (11:55 -0600)]
Standardizing notifications for setting options in set_defaults (#8057)

2 years agoFP: Rename tester kinds. (#8037)
Aina Niemetz [Fri, 4 Feb 2022 15:01:42 +0000 (07:01 -0800)]
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

2 years agoUse Add instead of Plus (#8043)
Gereon Kremer [Fri, 4 Feb 2022 01:19:08 +0000 (17:19 -0800)]
Use Add instead of Plus (#8043)

This fixes the current documentation builds for the pythonic API

2 years agoSimplify handling of disequalities in strings (#8047)
Andrew Reynolds [Thu, 3 Feb 2022 23:48:39 +0000 (17:48 -0600)]
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`.

2 years agoImprove theory combination over real algebraic models (#8045)
Gereon Kremer [Thu, 3 Feb 2022 23:14:38 +0000 (15:14 -0800)]
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.

2 years agoEliminate even more static uses of rewrite (#8044)
Andrew Reynolds [Thu, 3 Feb 2022 21:33:56 +0000 (15:33 -0600)]
Eliminate even more static uses of rewrite (#8044)

2 years agoTest proof granularity theory-rewrite by default (#8038)
Andrew Reynolds [Thu, 3 Feb 2022 20:58:20 +0000 (14:58 -0600)]
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.

2 years agoReplace a some more static options (#8042)
Gereon Kremer [Thu, 3 Feb 2022 19:57:41 +0000 (11:57 -0800)]
Replace a some more static options (#8042)

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

2 years agoEliminate more static uses of rewrite (#8040)
Andrew Reynolds [Thu, 3 Feb 2022 19:19:31 +0000 (13:19 -0600)]
Eliminate more static uses of rewrite (#8040)

2 years agoAdd table.product operator (#8020)
mudathirmahgoub [Thu, 3 Feb 2022 15:55:16 +0000 (09:55 -0600)]
Add table.product operator (#8020)

2 years agoAdd miscellaneous missing theory definitions for LFSC (#8039)
Andrew Reynolds [Thu, 3 Feb 2022 14:56:34 +0000 (08:56 -0600)]
Add miscellaneous missing theory definitions for LFSC (#8039)

2 years agoAdd node utils for the arithmetic rewriter (#8012)
Gereon Kremer [Thu, 3 Feb 2022 10:15:15 +0000 (02:15 -0800)]
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.

2 years agoSend all `nth` terms to the core array solver (#7990)
Andres Noetzli [Thu, 3 Feb 2022 05:58:49 +0000 (21:58 -0800)]
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.

2 years agoRename kind PLUS -> ADD. (#8036)
Aina Niemetz [Thu, 3 Feb 2022 04:25:14 +0000 (20:25 -0800)]
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).

2 years agoapi: Remove obsolete function declaration in Cython bindings. (#8032)
Aina Niemetz [Thu, 3 Feb 2022 03:24:43 +0000 (19:24 -0800)]
api: Remove obsolete function declaration in Cython bindings. (#8032)

2 years agoapi: Rename kinds MINUS -> SUB and UMINUS -> NEG. (#8034)
Aina Niemetz [Thu, 3 Feb 2022 02:18:51 +0000 (18:18 -0800)]
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).

2 years agoapi: Add explicit guard for option produce-assertions in blockModelValues(). (#7958)
Aina Niemetz [Thu, 3 Feb 2022 00:18:45 +0000 (16:18 -0800)]
api: Add explicit guard for option produce-assertions in blockModelValues(). (#7958)

Fixes cvc5/cvc5-projects#412.

2 years agoChange name of Python API's package from pycvc5 to cvc5. (#7953)
Alex Ozdemir [Wed, 2 Feb 2022 23:45:42 +0000 (15:45 -0800)]
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.

2 years agoFix rewrite for eliminating constant factors of PI from argument to sine (#8031)
Andrew Reynolds [Wed, 2 Feb 2022 23:10:55 +0000 (17:10 -0600)]
Fix rewrite for eliminating constant factors of PI from argument to sine (#8031)

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

2 years agoRename kinds MINUS -> SUB and UMINUS -> NEG. (#8035)
Aina Niemetz [Wed, 2 Feb 2022 22:27:14 +0000 (14:27 -0800)]
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).

2 years agoUse proper filename in -o subs documentation (#8030)
Gereon Kremer [Wed, 2 Feb 2022 21:47:15 +0000 (13:47 -0800)]
Use proper filename in -o subs documentation (#8030)

We somehow used the wrong filename in #7944.

2 years agoFix invalid rewrite involving iand (#8026)
Andrew Reynolds [Wed, 2 Feb 2022 21:21:24 +0000 (15:21 -0600)]
Fix invalid rewrite involving iand (#8026)

Fixes #8016.

2 years agoapi: Rename mk<Value> functions for FP for consistency. (#8033)
Aina Niemetz [Wed, 2 Feb 2022 20:59:37 +0000 (12:59 -0800)]
api: Rename mk<Value> functions for FP for consistency. (#8033)

2 years agoFix printing of re.loop as an operator in LFSC (#8029)
Andrew Reynolds [Wed, 2 Feb 2022 20:24:39 +0000 (14:24 -0600)]
Fix printing of re.loop as an operator in LFSC (#8029)

2 years agoMake LFSC side condition for concat unify robust to equality with full string (#8028)
Andrew Reynolds [Wed, 2 Feb 2022 20:05:03 +0000 (14:05 -0600)]
Make LFSC side condition for concat unify robust to equality with full string (#8028)

Was leading to LFSC proof checking failures.

2 years agoAdd missing null terminators for regexp (#8027)
Andrew Reynolds [Wed, 2 Feb 2022 19:32:48 +0000 (13:32 -0600)]
Add missing null terminators for regexp (#8027)

Led to some LFSC proof checking failures on strings benchmarks.

2 years agoAdd additional check to avoid cyclic substitution (#7991)
Gereon Kremer [Wed, 2 Feb 2022 18:51:20 +0000 (10:51 -0800)]
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.

2 years agoUpdate datatypes.rst (#8009)
mudathirmahgoub [Wed, 2 Feb 2022 16:59:28 +0000 (10:59 -0600)]
Update datatypes.rst (#8009)

2 years agoRemove more static calls to rewrite (#8025)
Andrew Reynolds [Wed, 2 Feb 2022 16:37:03 +0000 (10:37 -0600)]
Remove more static calls to rewrite (#8025)

2 years agoExtend proof step buffer to optionally ensure unique conclusions (#8017)
Andrew Reynolds [Wed, 2 Feb 2022 14:46:48 +0000 (08:46 -0600)]
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.

2 years agoFix parser issue with tuple_project operator (#8021)
mudathirmahgoub [Wed, 2 Feb 2022 14:16:26 +0000 (08:16 -0600)]
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)

2 years ago[BV] Fix strategy for `RewriteExtract` (#8011)
Andres Noetzli [Tue, 1 Feb 2022 21:58:41 +0000 (13:58 -0800)]
[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.

2 years ago[BV] Fix order of rewrites for `concat` (#8010)
Andres Noetzli [Tue, 1 Feb 2022 20:27:56 +0000 (12:27 -0800)]
[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.

2 years agoAdd new ordering utility (#8008)
Gereon Kremer [Tue, 1 Feb 2022 19:16:24 +0000 (11:16 -0800)]
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.

2 years agoAdd variant of get-difficulty for full effort lemmas (#8018)
Andrew Reynolds [Tue, 1 Feb 2022 18:11:21 +0000 (12:11 -0600)]
Add variant of get-difficulty for full effort lemmas (#8018)

Add variant of get-difficulty for full effort lemmas

2 years ago[Arrays] Fix response for `store` chains (#8015)
Andres Noetzli [Tue, 1 Feb 2022 17:26:16 +0000 (09:26 -0800)]
[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.

2 years agoAdd bag.filter operator (#8006)
mudathirmahgoub [Tue, 1 Feb 2022 14:58:04 +0000 (08:58 -0600)]
Add bag.filter operator (#8006)

2 years agoConsider RANs in variable ordering (#7964)
Gereon Kremer [Tue, 1 Feb 2022 02:19:58 +0000 (18:19 -0800)]
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.

2 years agoAdd utilities for flattening nodes (#7961)
Gereon Kremer [Mon, 31 Jan 2022 21:49:21 +0000 (13:49 -0800)]
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.

2 years agoFix memory leak in quantifier info (#8005)
Andres Noetzli [Mon, 31 Jan 2022 18:19:35 +0000 (10:19 -0800)]
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.

2 years agoRename docs-releases to docs (#7999)
Gereon Kremer [Sat, 29 Jan 2022 01:41:44 +0000 (17:41 -0800)]
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/

2 years agoStart post-release for 0.0.7
Mathias Preiner [Fri, 28 Jan 2022 20:34:14 +0000 (12:34 -0800)]
Start post-release for 0.0.7

2 years agoBump version to 0.0.7
Mathias Preiner [Fri, 28 Jan 2022 20:34:14 +0000 (12:34 -0800)]
Bump version to 0.0.7

2 years agoTry a bit harder on the EQ_NCTN rewrite rule (#7998)
Bruno Dutertre [Fri, 28 Jan 2022 20:33:10 +0000 (12:33 -0800)]
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>
2 years agoFix docs upload once again (#7997)
Gereon Kremer [Fri, 28 Jan 2022 19:57:30 +0000 (11:57 -0800)]
Fix docs upload once again (#7997)

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

2 years ago[Rewrite Synthesis] Fix args for non-chaining ops (#7996)
Andres Noetzli [Fri, 28 Jan 2022 16:56:27 +0000 (08:56 -0800)]
[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.

2 years agoDocument substitute in API (#7904)
Andrew Reynolds [Thu, 27 Jan 2022 23:35:13 +0000 (17:35 -0600)]
Document substitute in API (#7904)

2 years agoUpdate AUTHORS und copyright of docs configuration. (#7994)
Aina Niemetz [Thu, 27 Jan 2022 22:24:28 +0000 (14:24 -0800)]
Update AUTHORS und copyright of docs configuration. (#7994)

2 years agoProperly recognize whether the current commit is a tag (#7989)
Gereon Kremer [Thu, 27 Jan 2022 00:34:16 +0000 (16:34 -0800)]
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.

2 years agoInitial refactoring of conflict-based instantiation (#7380)
Andrew Reynolds [Wed, 26 Jan 2022 19:07:56 +0000 (13:07 -0600)]
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.

2 years agoAdd Card solver to bags (#7986)
mudathirmahgoub [Wed, 26 Jan 2022 18:41:26 +0000 (12:41 -0600)]
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

2 years agoMore fixes and improvements for query generator (#7988)
Andrew Reynolds [Wed, 26 Jan 2022 01:20:01 +0000 (19:20 -0600)]
More fixes and improvements for query generator (#7988)

Includes proper printing of dumped benchmarks.

2 years agoAdd output -o post-asserts (#7987)
Andrew Reynolds [Tue, 25 Jan 2022 19:50:50 +0000 (13:50 -0600)]
Add output -o post-asserts (#7987)

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

2 years agoStart post-release for 0.0.6
Mathias Preiner [Tue, 25 Jan 2022 19:19:53 +0000 (11:19 -0800)]
Start post-release for 0.0.6

2 years agoBump version to 0.0.6
Mathias Preiner [Tue, 25 Jan 2022 19:19:53 +0000 (11:19 -0800)]
Bump version to 0.0.6

2 years agoSend `nth(unit(...), ...)` terms to array solver (#7983)
Andres Noetzli [Tue, 25 Jan 2022 17:46:20 +0000 (09:46 -0800)]
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.

2 years agoFixes and improvements to sygus satisfiable query generation (#7980)
Andrew Reynolds [Tue, 25 Jan 2022 17:15:51 +0000 (11:15 -0600)]
Fixes and improvements to sygus satisfiable query generation (#7980)

Fixes issues related to the use of partial functions. Also ensures we avoid duplicate queries.

2 years ago[Strings] Avoid trivial explanation (#7982)
Andres Noetzli [Tue, 25 Jan 2022 04:33:13 +0000 (20:33 -0800)]
[Strings] Avoid trivial explanation (#7982)

The `STRINGS_N_UNIFY` inference could produce trivial explanations. For
example, if both `x` and `y` were of kind `seq.unit`, then the
explanation was `(= 1 1)`. This lead to issues when checking proofs.

2 years ago[Strings] Remove redundant call to rewriter (#7978)
Andres Noetzli [Tue, 25 Jan 2022 04:01:13 +0000 (20:01 -0800)]
[Strings] Remove redundant call to rewriter (#7978)

The term being rewritten was already rewritten a couple of lines above.

2 years ago[FP] Fix unused variable warning (#7977)
Andres Noetzli [Tue, 25 Jan 2022 03:22:48 +0000 (19:22 -0800)]
[FP] Fix unused variable warning (#7977)

2 years agoDisable regression if poly is not available (#7981)
Gereon Kremer [Mon, 24 Jan 2022 22:54:18 +0000 (14:54 -0800)]
Disable regression if poly is not available (#7981)

This regression fails if poly is not available.

2 years agoAlways compile RANs (#7979)
Gereon Kremer [Mon, 24 Jan 2022 21:43:28 +0000 (13:43 -0800)]
Always compile RANs (#7979)

This PR makes sure that we always compile with real algebraic numbers, following #7976.

2 years agoUse proper RAN nodes for nl model (#7939)
Gereon Kremer [Mon, 24 Jan 2022 19:58:56 +0000 (11:58 -0800)]
Use proper RAN nodes for nl model (#7939)

This PR finally uses proper RealAlgebraicNumber (wrapped in nodes) to represent nonlinear model values. This simplifies the implementation of getEqualityStatus, and should make theory combination much more robust.
Also, we reintroduce the possibility to have getEqualityStatus return unknown, though this should only happen in the presence of witness terms.

2 years agoRefactor how arith rewriting checks for mult-by-zero (#7962)
Gereon Kremer [Mon, 24 Jan 2022 19:23:41 +0000 (11:23 -0800)]
Refactor how arith rewriting checks for mult-by-zero (#7962)

This adds an explicit check for a zero factor in the post rewriter for multiplication.

2 years agoEnable dump tester. (#7884)
Abdalrhman Mohamed [Mon, 24 Jan 2022 18:34:14 +0000 (12:34 -0600)]
Enable dump tester. (#7884)

This PR enables the dump tester, a parse-print-parse test for cvc5, on CI. It also includes some changes that reduce the number of regressions that fail with this tester.

2 years agoHave RAN fall back to RANs (#7976)
Gereon Kremer [Mon, 24 Jan 2022 17:49:02 +0000 (09:49 -0800)]
Have RAN fall back to RANs (#7976)

Right now, the RealAlgebraicNumber can not be used if libpoly is not available. This makes using it in the arithmetic rewriter incredibly awkward. This PR makes it fall back to a wrapper around Rational if libpoly is disabled, making its usage way easier.

2 years agoRef count nodes in trigger trie (#7972)
Andrew Reynolds [Fri, 21 Jan 2022 18:20:45 +0000 (12:20 -0600)]
Ref count nodes in trigger trie (#7972)

Fixes cvc5/cvc5-projects#437.

2 years agoFix trivial explantions in sequences array solver (#7973)
Andrew Reynolds [Fri, 21 Jan 2022 00:42:51 +0000 (18:42 -0600)]
Fix trivial explantions in sequences array solver (#7973)

Also tightens the explanation slightly, we were previously adding a spurious equality to the representative, instead of the base of the normal form.

2 years agoFix `Nth-Update` rule, add `Update-Bound` rule (#7968)
Andres Noetzli [Thu, 20 Jan 2022 23:03:02 +0000 (15:03 -0800)]
Fix `Nth-Update` rule, add `Update-Bound` rule (#7968)

This commit updates the inferences in the sequences array solver to more
closely resemble the current rules in the paper. Concretely, it adds an
implementation of the `Update-Bound` rule and it fixes the `Nth-Update`
rule to take into account all three branches in the conclusion of the
rule.

Co-authored-by: Yoni Zohar <yoni206@gmail.com>
2 years agoFix proofs for trivial cases of datatypes tester merge (#7969)
Andrew Reynolds [Thu, 20 Jan 2022 20:39:59 +0000 (14:39 -0600)]
Fix proofs for trivial cases of datatypes tester merge (#7969)

Fixes cvc5/cvc5-projects#433.

Also ensures we don't add (= t t) as part of a reported conflict.

2 years agoRefactor abs rewriting (#7935)
Gereon Kremer [Thu, 20 Jan 2022 18:29:25 +0000 (10:29 -0800)]
Refactor abs rewriting (#7935)

This PR refactors rewriting for ABS to also support real algebraic number. We also generalize the ABS operator to real arguments in general, instead of integer arguments.

2 years agoFix CI build for macOS (#7970)
Andres Noetzli [Thu, 20 Jan 2022 18:10:40 +0000 (10:10 -0800)]
Fix CI build for macOS (#7970)

The macOS CI could not find the Cython executable anymore for some reason. This commit fixes the issue.

2 years agoAdd rewrites for `seq.update`/`seq.nth` (#7966)
Andres Noetzli [Wed, 19 Jan 2022 23:45:21 +0000 (15:45 -0800)]
Add rewrites for `seq.update`/`seq.nth` (#7966)

This commit adds rewrites for `seq.update` and `seq.nth`. It adds a
rewrite to check if an update is out of bounds and it adds rewrites to
evaluate these operators using `stripSymbolicLength()`. This allows us
for example to evaluate updates on concatenations of non-constant
`seq.unit`s.

2 years agoFix a subtle issue with double negations in coverings proof (#7967)
Gereon Kremer [Wed, 19 Jan 2022 22:36:08 +0000 (14:36 -0800)]
Fix a subtle issue with double negations in coverings proof (#7967)

When the coverings solver finds a conflict that consists only of a single negated assertion, the way we constructed the lemma would silently drop the double negation. While this is not a problem by itself, the generated proof is out of sync then.
This PR makes sure the double negation stays in place and is only removed by rewriting in the core lemma processing.
Fixes cvc5/cvc5-projects#430.

2 years agoMake tracing for arithmetic rewriter more consistent and useful (#7960)
Gereon Kremer [Wed, 19 Jan 2022 18:02:48 +0000 (10:02 -0800)]
Make tracing for arithmetic rewriter more consistent and useful (#7960)

Tracing in the arithmetic rewriter was very inconsistent and oftentimes not particularly helpful. This adds a general trace showing all top-level calls to the arithmetic rewriter.

2 years agoUpdate to latest libpoly version (#7963)
Gereon Kremer [Wed, 19 Jan 2022 17:25:13 +0000 (09:25 -0800)]
Update to latest libpoly version (#7963)

The latest libpoly version has a fix for the conversion of algebraic numbers to rationals. We need this in our arithmetic rewriter to properly simplify real algebraic numbers to rationals.

2 years agoDistinguish purification types for strings proof reconstruction (#7521)
Andrew Reynolds [Tue, 18 Jan 2022 21:03:26 +0000 (15:03 -0600)]
Distinguish purification types for strings proof reconstruction (#7521)

This improves the success rate for strings proof reconstruction for context-dependent simplifications.

It also makes a minor modification to how EXTF inferences work. As a special case, A => B becomes A ^ ~B => false when B is already equal to false. This PR removes this behavior for the sake of consistency. (This could be explored as a more general strategy for turning facts to conflicts from any source if necessary).

The strings solver applies context-dependent simplification in various ways. This ensures that the proof reconstruction is faithful for cases of congruence + rewriting instead of substitution+rewriting, which the inferences STRINGS_EXTF and STRINGS_EXTF_N rely on.

This fixes 11 cases where proof reconstruction fails for string theory lemmas on Amazon benchmarks.

2 years agoSome random documentation issues (#7921)
Gereon Kremer [Tue, 18 Jan 2022 20:32:17 +0000 (12:32 -0800)]
Some random documentation issues (#7921)

This PR fixes a few issues in the documentation, mostly about examples that were not included where they should be.

2 years ago[API] Add missing arity check (#7905)
Andres Noetzli [Tue, 18 Jan 2022 19:55:54 +0000 (11:55 -0800)]
[API] Add missing arity check (#7905)

Fixes #7894. The API was not performing an arity check for associative
operators with less than two children. This commit adds the missing
check.

2 years agoFix CMake script for static, auto-download, cln configuration (#7957)
Matthew Sotoudeh [Tue, 18 Jan 2022 17:24:02 +0000 (09:24 -0800)]
Fix CMake script for static, auto-download, cln configuration (#7957)

The script was previously creating a 'CLN_STATIC_LIBRARIES' variable that
wasn't known about elsewhere in the code and caused issues when the Makefiles
depended on a CLN_LIBRARIES variable. Instead, the static libraries should just
go into CLN_LIBRARIES as normal.

This only seems to have affected the case where cln is set to auto-download and
the build is static.

Signed-off-by: Matthew Sotoudeh sotoudeh@stanford.edu
2 years agoPrint original form for substitutions and learned literals (#7959)
Andrew Reynolds [Tue, 18 Jan 2022 17:06:41 +0000 (11:06 -0600)]
Print original form for substitutions and learned literals (#7959)

2 years agoRefactor options related to rewriting and symmetry breaking in sygus (#7949)
Andrew Reynolds [Mon, 17 Jan 2022 19:05:55 +0000 (13:05 -0600)]
Refactor options related to rewriting and symmetry breaking in sygus (#7949)

Note this also corrects a few inconsistencies in how the rewriter is invoked in fast / variable agnostic enumeration.

Notably, fast enumeration now leverages the term datatype sygus for rewriting, meaning it can evaluate recursive functions for enumerated terms.

2 years ago[Strings] Fix rewriter for `re.loop` (#7956)
Andres Noetzli [Mon, 17 Jan 2022 03:55:27 +0000 (19:55 -0800)]
[Strings] Fix rewriter for `re.loop` (#7956)

Fixes cvc5/cvc5-projects#409. Our
strings/sequences rewriter was applying rewrites for re.loop in the
wrong order. As a result, it rewrote ((_ re.loop 2 1) re.all) to
re.all instead of re.none as required by the SMT-LIB standard when
the lower bound is greater than the upper bound. This commit changes the
order s.t. the bounds check happens first.

2 years agoChange how RANs are printed (#7955)
Gereon Kremer [Sat, 15 Jan 2022 03:17:29 +0000 (19:17 -0800)]
Change how RANs are printed (#7955)

This PR adds real algebraic number as a special case in the smt2 printer.

2 years agoAdd inverse inference for update-over-concat (#7954)
Andrew Reynolds [Sat, 15 Jan 2022 02:16:20 +0000 (20:16 -0600)]
Add inverse inference for update-over-concat (#7954)

This adds an inference that applies when an atomic update term becomes equal to a concatenation term.

This fixes bogus models discovered when writing the model soundness proof for the sequences array solver.

2 years agoImprove names for sygus enumeration option (#7945)
Andrew Reynolds [Fri, 14 Jan 2022 23:59:58 +0000 (17:59 -0600)]
Improve names for sygus enumeration option (#7945)

Also deletes the unused (naive) basic enumerator.

2 years agoClean enumerative instantiation options (#7947)
Andrew Reynolds [Fri, 14 Jan 2022 22:56:46 +0000 (16:56 -0600)]
Clean enumerative instantiation options (#7947)

--full-saturate-quant is kept as a generic option, and implies --enum-inst.

2 years agoImplement -o subs to show learned top-level substitutions (#7944)
Andrew Reynolds [Fri, 14 Jan 2022 22:17:57 +0000 (16:17 -0600)]
Implement -o subs to show learned top-level substitutions (#7944)

Also adds substitutions as part of the output of -o learned-lits for completeness.

2 years agoRename python APIs (#7950)
Alex Ozdemir [Fri, 14 Jan 2022 21:45:19 +0000 (13:45 -0800)]
Rename python APIs (#7950)

Rename python APIs to "base" and "pythonic"

2 years agoPreprare central model building for RANs (#7951)
Gereon Kremer [Fri, 14 Jan 2022 21:05:03 +0000 (13:05 -0800)]
Preprare central model building for RANs (#7951)

This PR uses a new utility isEvaluationResult() instead of isConst() within the core model building. This prepares model building for model values that are not constants (in the sense of isConst()) but still constant-lilke values, like real algebraic numbers.

2 years agorefactor div rewriter, add support for ran (#7941)
Gereon Kremer [Fri, 14 Jan 2022 20:27:50 +0000 (12:27 -0800)]
refactor div rewriter, add support for ran (#7941)

This extends the rewriter for division to also support real algebraic numbers.

2 years agoFix learned rewrite pass for non-real equalties (#7936)
Andrew Reynolds [Fri, 14 Jan 2022 20:00:37 +0000 (14:00 -0600)]
Fix learned rewrite pass for non-real equalties (#7936)

Fixes #7918.

2 years agoAdd operator<<(RewriteStatus) (#7952)
Gereon Kremer [Fri, 14 Jan 2022 19:16:47 +0000 (11:16 -0800)]
Add operator<<(RewriteStatus) (#7952)

Adds a streaming operator for RewriteStatus. I found it helpful while refactoring / debugging the rewriter.

2 years agoWeaken assertion in relevance manager (#7943)
Andrew Reynolds [Fri, 14 Jan 2022 17:05:20 +0000 (11:05 -0600)]
Weaken assertion in relevance manager (#7943)

Fixes #7937.

2 years agoRefactor arithmetic pre-rewriter for multiplication (#7930)
Gereon Kremer [Fri, 14 Jan 2022 16:30:14 +0000 (08:30 -0800)]
Refactor arithmetic pre-rewriter for multiplication (#7930)

This PR refactors the pre-rewrite stage for multiplication.

2 years agoAdd support for RANs in rewriter for `MULT` (#7940)
Gereon Kremer [Fri, 14 Jan 2022 15:57:24 +0000 (07:57 -0800)]
Add support for RANs in rewriter for `MULT` (#7940)

This PR refactors the post rewriter for multiplication. It now supports real algebraic numbers and tries a bit harder to avoid the overhead of the normal form abstraction.

2 years agoAdd RAN support in UMINUS rewriter (#7933)
Gereon Kremer [Fri, 14 Jan 2022 15:36:17 +0000 (07:36 -0800)]
Add RAN support in UMINUS rewriter (#7933)

This adds rewriting for UMINUS of real algebraic numbers

2 years agoAdd arithmetic rewriter for RAN (#7929)
Gereon Kremer [Thu, 13 Jan 2022 21:53:16 +0000 (13:53 -0800)]
Add arithmetic rewriter for RAN (#7929)

This adds a rewriter for real arithmetic constants, possibly rewriting them to a rational.