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

2 years agoFix `TypeNode::substitute()` (#7916)
Andres Noetzli [Tue, 11 Jan 2022 14:29:49 +0000 (06:29 -0800)]
Fix `TypeNode::substitute()` (#7916)

Fixes cvc5/cvc5-projects#397. Fixes
cvc5/cvc5-projects#399. After performing the
substitution on the child node, the result was not added as a child to
the node under construction, resulting in nodes with too few children.
This commit fixes that issue.

2 years agoCheck the synthesized funs of `check-synth-next`. (#7915)
Abdalrhman Mohamed [Tue, 11 Jan 2022 06:36:20 +0000 (00:36 -0600)]
Check the synthesized funs of `check-synth-next`. (#7915)

This PR ensures that the functions synthesized by cvc5 with check-synth-next command(s) are different from the preceding ones.

2 years agoAdd new idiomatic examples (#7912)
Alex Ozdemir [Tue, 11 Jan 2022 00:49:02 +0000 (16:49 -0800)]
Add new idiomatic examples (#7912)

2 years ago[Win64] Link LibPoly statically for static builds (#7891)
Andres Noetzli [Tue, 11 Jan 2022 00:15:03 +0000 (16:15 -0800)]
[Win64] Link LibPoly statically for static builds (#7891)

Fixes #7861. LibPoly was not getting linked statically for Windows
builds, even when building a static version of cvc5. This commit fixes
the issue.

2 years agoFix internal type error when printing lambdas with more than one variable in LFSC...
Andrew Reynolds [Mon, 10 Jan 2022 22:53:40 +0000 (16:53 -0600)]
Fix internal type error when printing lambdas with more than one variable in LFSC (#7909)

2 years agoCheck arity in Sort::instantiate (#7897)
Andrew Reynolds [Mon, 10 Jan 2022 22:19:00 +0000 (16:19 -0600)]
Check arity in Sort::instantiate (#7897)

Fixes cvc5/cvc5-projects#386.

2 years agoAdd new methods for RealAlgebraicNumber (#7907)
Gereon Kremer [Mon, 10 Jan 2022 21:29:45 +0000 (13:29 -0800)]
Add new methods for RealAlgebraicNumber (#7907)

This PR adds some new methods for the RealAlgebraicNumber class: division, computing the (multiplicative) inverse and a specialization of std::hash.

2 years agoUpdate to latest libpoly version (#7906)
Gereon Kremer [Mon, 10 Jan 2022 20:14:59 +0000 (12:14 -0800)]
Update to latest libpoly version (#7906)

This PR updates to the latest libpoly version. It contains a bugfix and adds division and inverse operations for algebraic numbers.

2 years agoapi: Remove Sort::isComparableTo(). (#7903)
Aina Niemetz [Mon, 10 Jan 2022 19:27:04 +0000 (11:27 -0800)]
api: Remove Sort::isComparableTo(). (#7903)

Since we do not support arithmetic subtyping on the API level anymore,
this function is obsolete. Consequently, this now requires that
replacement terms as arguments to Term::substitute() are of the same
sort as the replaced terms.

2 years agoAvoid gcc/10.1.0 bug by moving some configuration into a namespace
Matthew Sotoudeh [Mon, 10 Jan 2022 18:29:10 +0000 (10:29 -0800)]
Avoid gcc/10.1.0 bug by moving some configuration into a namespace

Eventually there is intention to move all of cvc5::Configuration into
cvc5::configuration, this is a first step that also has the nice side-effect of
letting it build under an otherwise-buggy version of gcc/10.1.0 that was
causing issues.

Signed-off-by: Matthew Sotoudeh <sotoudeh@stanford.edu>
2 years agoStart post-release for 0.0.5
Mathias Preiner [Sat, 8 Jan 2022 00:00:41 +0000 (16:00 -0800)]
Start post-release for 0.0.5

2 years agoBump version to 0.0.5
Mathias Preiner [Sat, 8 Jan 2022 00:00:41 +0000 (16:00 -0800)]
Bump version to 0.0.5

2 years agoImprove docs extension for examples (#7900)
Gereon Kremer [Fri, 7 Jan 2022 22:25:38 +0000 (14:25 -0800)]
Improve docs extension for examples (#7900)

We recently added automatic download links for examples in our documentation, however they assumed everything to live inside the main cvc5 repo while, e.g., the examples for the z3py compat API do not. While #7896 provided a very simple fix, it mixes different concerns (rendering of tabs vs. locating the input files, though they should coincide right now).
This PR takes a more fundamental approach by extending the current pattern mechanism to allow for explicit url specification.

Closes #7896.

2 years agoPython Idomatic API: Document solver, results, utilities, and fns (#7882)
Alex Ozdemir [Fri, 7 Jan 2022 20:42:28 +0000 (12:42 -0800)]
Python Idomatic API: Document solver, results, utilities, and fns (#7882)

I put fns into "Core & Booleans".

2 years agoRemove CDDenseSet data structure (#7890)
Matthew Sotoudeh [Fri, 7 Jan 2022 20:12:18 +0000 (12:12 -0800)]
Remove CDDenseSet data structure (#7890)

It was not used anywhere, and does not appear to build under, at least,
GCC/9.1.0.

Signed-off-by: Matthew Sotoudeh <sotoudeh@stanford.edu>
2 years agoFix eager string preprocessing in incremental mode (#7895)
Andrew Reynolds [Fri, 7 Jan 2022 19:30:36 +0000 (13:30 -0600)]
Fix eager string preprocessing in incremental mode (#7895)

Fixes #5780.

Issue was caused by reintroducing skolems during preprocessing that were already solved for.

2 years agoSome minor improvements to the theory references (#7881)
Gereon Kremer [Fri, 7 Jan 2022 17:49:22 +0000 (09:49 -0800)]
Some minor improvements to the theory references (#7881)

2 years agoAdd regressions for array sequence solver (#7874)
Andrew Reynolds [Fri, 7 Jan 2022 16:32:34 +0000 (10:32 -0600)]
Add regressions for array sequence solver (#7874)

This closes the seqArray branch.

2 years agoDocument quantifiers in idiomatic python API (#7880)
Alex Ozdemir [Fri, 7 Jan 2022 04:37:08 +0000 (20:37 -0800)]
Document quantifiers in idiomatic python API (#7880)

2 years ago[Regressions] Add directive for disabling testers (#7892)
Andres Noetzli [Fri, 7 Jan 2022 04:13:56 +0000 (20:13 -0800)]
[Regressions] Add directive for disabling testers (#7892)

This commit adds a directive for regressions (`DISABLE-TESTER`) that
allows disabling a given tester for a regression. Currently, we disable
testers based on properties such as command line arguments, which can be
error prone.

2 years agoMake alpha equivalence user context dependent (#7889)
Andrew Reynolds [Thu, 6 Jan 2022 23:42:14 +0000 (17:42 -0600)]
Make alpha equivalence user context dependent (#7889)

Fixes #5373

Issues were occurring due to using quantified formulas in alpha equivalence that were stale.

This also removes spurious warnings from quantifier elimination (dropping the "strict" requirement, which unnecessarily warns if we are in a non-arithmetic logic).

2 years agoDisallow separation logic in incremental mode (#7888)
Andrew Reynolds [Thu, 6 Jan 2022 23:26:10 +0000 (17:26 -0600)]
Disallow separation logic in incremental mode (#7888)

Fixes #5541. Fixes #5607.

2 years agoImprove theory combination in the presence of real algebraic numbers (#7883)
Gereon Kremer [Thu, 6 Jan 2022 21:09:10 +0000 (13:09 -0800)]
Improve theory combination in the presence of real algebraic numbers (#7883)

This PR changes how we handle real algebraic numbers in theory combination and model construction.
The goal is to improve getEqualityStatus() and produce proper models more often.
We now use a RAN-aware evaluator for getEqualityStatus() and change the way how the nonlinear extension finalizes its model.

2 years agoFix non-idempotent rewrite in arrays (#7887)
Andrew Reynolds [Thu, 6 Jan 2022 20:25:19 +0000 (14:25 -0600)]
Fix non-idempotent rewrite in arrays (#7887)

Fixes #6807.

2 years agoMinor cleaning of non-clausal simplification (#7886)
Andrew Reynolds [Thu, 6 Jan 2022 20:05:04 +0000 (14:05 -0600)]
Minor cleaning of non-clausal simplification (#7886)

2 years agocppapi: Remove Datatype::hasNestedRecursion(). (#7878)
Aina Niemetz [Wed, 5 Jan 2022 21:20:05 +0000 (13:20 -0800)]
cppapi: Remove Datatype::hasNestedRecursion(). (#7878)

Datatypes with nested recursion are a highly experimental feature and we
currentle don't even have a decision procedure for them.

2 years agoPy idiomatic API: Doc sets, datatypes, FP (#7877)
Alex Ozdemir [Wed, 5 Jan 2022 20:47:09 +0000 (12:47 -0800)]
Py idiomatic API: Doc sets, datatypes, FP (#7877)

2 years agoapi: Add missing guard for Datatype::isFinite(). (#7879)
Aina Niemetz [Wed, 5 Jan 2022 20:23:17 +0000 (12:23 -0800)]
api: Add missing guard for Datatype::isFinite(). (#7879)

2 years agoProperly parse arithmetic values (#7876)
Andrew Reynolds [Wed, 5 Jan 2022 18:58:10 +0000 (12:58 -0600)]
Properly parse arithmetic values (#7876)

This makes our parser correct for arithmetic values e.g. (- n) is parsed as a value not UMINUS when n is a numeral, as indicated in SMT-LIB. Similarly for (/ m n) and (/ (- m) n) we parse as values and not DIVISION.

This subsumes a patch for constructing array constants where this led to issues.

2 years agoTrack input list for atoms in difficulty manager (#7851)
Andrew Reynolds [Wed, 5 Jan 2022 18:01:25 +0000 (12:01 -0600)]
Track input list for atoms in difficulty manager (#7851)

This makes our support for get-difficulty faster by tracking the set of input formulas that atoms occur in, which is highly important for benchmarks with many assertions and where many lemmas are added at standard effort.

This is work towards making get-difficulty scale on a large benchmark from Certora.

2 years agoDon't use python's collections.Set (#7875)
Alex Ozdemir [Wed, 5 Jan 2022 17:19:03 +0000 (09:19 -0800)]
Don't use python's collections.Set (#7875)

We used to use collections.Set.

Apparently this was an alias for collections.abc.Set. I can't find it
documented anywhere though, going as far back as Python 3.5. Perhaps it
was an undocumented left-over from when the collections.abc module was
split out from collections in Python 3.3?

At any rate, the alias appears broken in Python version 3.10.1.

Now we just use the builtin set type, which is what we wanted anyway,
I think.

2 years agoProperly set __file__ in python bindings (#7867)
yoni206 [Wed, 5 Jan 2022 16:26:00 +0000 (18:26 +0200)]
Properly set __file__ in python bindings (#7867)

When running make docs after changing the documentation in cvc5.pxi, the html files are not updated. This PR fixes this issue.

Co-authored-by: Gereon Kremer gereon.kremer@cs.rwth-aachen.de