cvc5.git
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.

2 years agoFix bug in evaluator for division by zero (#7942)
Andrew Reynolds [Thu, 13 Jan 2022 19:18:07 +0000 (13:18 -0600)]
Fix bug in evaluator for division by zero (#7942)

Fixes #7917.

2 years agoUnify abstract values and uninterpreted constants (#7424)
Andres Noetzli [Thu, 13 Jan 2022 01:42:26 +0000 (17:42 -0800)]
Unify abstract values and uninterpreted constants (#7424)

This commit unifies abstract values and "uninterpreted constants" into a
single kind. Note that "uninterpreted constants" is a bit of a misnomer
in the context of the new API, since they do not correspond to the
equivalent of a declare-const command, but instead are values for
symbols of an uninterpreted sort (and thus special cases of abstract
values). Instead of treating "uninterpreted constants" as a separate
kind, this commit extends abstract values to hold a type (instead of
marking their type via attribute in NodeManager::mkAbstractValue())
and uses the type of the abstract values to determine whether they are a
value for a constant of uninterpreted sort or not. Unifying these
representations simplifies code and brings the terminology more in line
with the SMT-LIB standard.

This commit also updates the APIs to remove support for creating
abstract values and "uninterpreted constants". Users should never create
those. They can only be returned as a value for a term after a
satisfiability check.

Finally, the commit removes code in the parser for parsing abstract
values and updates the code for getting values involving abstract
values. Since the parser does not allow the declaration/definition of
abstract values, and determining whether a symbol is an abstract value
was broken (not all symbols starting with an @ are abstract values),
the code was effectively dead. Getting values involving "uninterpreted
constants" now no longer requires parsing the string of the values, but
instead, we can use existing API functionality.

2 years agoRefactor post rewriter for addition (#7931)
Gereon Kremer [Thu, 13 Jan 2022 00:55:46 +0000 (16:55 -0800)]
Refactor post rewriter for addition (#7931)

This makes the post rewriter for addition aware of real algebraic numbers. Also, it tries a bit harder to avoid the normal_form utilities if only constants are present.

2 years agoFix check whether we have a tag (#7901)
Gereon Kremer [Thu, 13 Jan 2022 00:14:06 +0000 (16:14 -0800)]
Fix check whether we have a tag (#7901)

This PR fixes a subtle issue with the docs upload for releases. While most of the context of the original action is passed into the docs upload action, the git ref changes from refs/tags/... to refs/heads/.... However, we still can check the current ref against the head_branch of the original workflow.

2 years agoAdd -o learned-lits to output learned literals (#7934)
Andrew Reynolds [Wed, 12 Jan 2022 23:28:02 +0000 (17:28 -0600)]
Add -o learned-lits to output learned literals (#7934)

Prints both literals learned during preprocessing, and during search.

This feature was recently requested by Cetora.

2 years agoRefactor atom rewriting to be RAN-aware (#7928)
Gereon Kremer [Wed, 12 Jan 2022 22:51:29 +0000 (14:51 -0800)]
Refactor atom rewriting to be RAN-aware (#7928)

This PR starts refactoring the arithmetic rewriter by making rewriting of atoms aware of real algebraic numbers.
It also is slightly more aggressive now, directly rewriting relational operators where lhs = rhs in the preRewrite stage.

2 years agoRefactor rewriteMinus (#7932)
Gereon Kremer [Wed, 12 Jan 2022 22:19:31 +0000 (14:19 -0800)]
Refactor rewriteMinus (#7932)

Refactors rewriteMinus to be generally simpler and explicitly rely on rewriting addition.
Note that rewriteMinus would almost never be called in post rewrite anyway, as it would rewrite to addition in pre rewrite.

2 years agoEnsure configuration of shared selectors is consistent in SyGuS subsolver (#7927)
Andrew Reynolds [Wed, 12 Jan 2022 21:46:38 +0000 (15:46 -0600)]
Ensure configuration of shared selectors is consistent in SyGuS subsolver (#7927)

This prevents the SyGuS subsolver from having a different configuration of dt-share-sel than the main SyGuS solver. Having this mismatch can lead to incorrect synthesis results.

Fixes #7925.

2 years agoAlways enable RAN, but disable its implementation without poly (#7910)
Gereon Kremer [Wed, 12 Jan 2022 18:59:29 +0000 (10:59 -0800)]
Always enable RAN, but disable its implementation without poly (#7910)

This PR makes sure that the RealAlgebraicNumber class is always visible, but its implementation is only enabled when libpoly is available. This allows us to use this class in more places of cvc5.

2 years agoAdd mkRealAlgebraicNumber (#7923)
Gereon Kremer [Wed, 12 Jan 2022 18:18:19 +0000 (10:18 -0800)]
Add mkRealAlgebraicNumber (#7923)

This PR adds the convenience function NodeManager::mkRealAlgebraicNumber().

2 years agoAlways use partial function for sqrt (#7926)
Andrew Reynolds [Wed, 12 Jan 2022 17:52:07 +0000 (11:52 -0600)]
Always use partial function for sqrt (#7926)

Fixes the behavior reported in #7924.

2 years agoEliminate use of subtyping from results of quantifier elimination (#7885)
Andrew Reynolds [Wed, 12 Jan 2022 15:58:14 +0000 (09:58 -0600)]
Eliminate use of subtyping from results of quantifier elimination (#7885)

Fixes #7870.

Notice this node converter is potentially unnecessary if we ever get rid of arithmetic subtyping.

2 years agoAdds a kind to hold RealAlgebraicNumber constants (#7908)
Gereon Kremer [Tue, 11 Jan 2022 22:44:43 +0000 (14:44 -0800)]
Adds a kind to hold RealAlgebraicNumber constants (#7908)

This PR adds a new kind that holds RealAlgebraicNumber constants. As it can not be a constant in the sense of isConst(), it is wrapped within an operator, similar to IAND or CARDINALITY_CONSTRAINT.

2 years agoDisable filtering of shapes in sygus-rcons pool. (#7922)
Abdalrhman Mohamed [Tue, 11 Jan 2022 21:58:17 +0000 (15:58 -0600)]
Disable filtering of shapes in sygus-rcons pool. (#7922)

This PR disables filtering of enumerated shapes in the pool of the Sygus reconstruction algorithm.

2 years agoFix `TypeNode::substitute()` for type constants (#7920)
Andres Noetzli [Tue, 11 Jan 2022 17:19:15 +0000 (09:19 -0800)]
Fix `TypeNode::substitute()` for type constants (#7920)

Fixes cvc5/cvc5-projects#395. The
TypeNode::substitute() method did not account for type constants such
as the Boolean type and was trying to use a NodeBuilder to build such
constants instead. This commit fixes the issue by adding a special case
for types without children.

2 years agoapi: Fix formatting of docs for Term::getSetValue(). (#7914)
Aina Niemetz [Tue, 11 Jan 2022 16:25:00 +0000 (08:25 -0800)]
api: Fix formatting of docs for Term::getSetValue(). (#7914)

2 years agoRemove static accesses to options (#7913)
Gereon Kremer [Tue, 11 Jan 2022 16:03:41 +0000 (08:03 -0800)]
Remove static accesses to options (#7913)

This PR removes some more calls like options::foo() in favor of options().module.foo.

2 years agoTighten policy for unsat cores in sygus core connective (#7911)
Andrew Reynolds [Tue, 11 Jan 2022 15:10:41 +0000 (09:10 -0600)]
Tighten policy for unsat cores in sygus core connective (#7911)

Previous policy was due to limitations on options on subsolvers, which no longer exist.

Fixes cvc5/cvc5-projects#354.
Fixes #7902.

2 years agoGuard use of unsat core mode pp-only (#7899)
Andrew Reynolds [Tue, 11 Jan 2022 14:48:14 +0000 (08:48 -0600)]
Guard use of unsat core mode pp-only (#7899)

Fixes cvc5/cvc5-projects#366. Now gives
(error "Error in option parsing: Unsat core mode pp-only is for internal use only.")