Initial refactoring of conflict-based instantiation (#7380)

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

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

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

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

Add Card solver to bags (#7986)

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

More fixes and improvements for query generator (#7988)

Includes proper printing of dumped benchmarks.

Add output -o post-asserts (#7987)

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

Start post-release for 0.0.6

Bump version to 0.0.6

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

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

Fixes and improvements to sygus satisfiable query generation (#7980)

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

[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.

[Strings] Remove redundant call to rewriter (#7978)

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

[FP] Fix unused variable warning (#7977)

Disable regression if poly is not available (#7981)

This regression fails if poly is not available.

Always compile RANs (#7979)

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

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.

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.

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.

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.

Ref count nodes in trigger trie (#7972)

Fixes cvc5/cvc5-projects#437.

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.

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>

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.

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.

Fix CI build for macOS (#7970)

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

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.

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.

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.

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.

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.

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.

[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.

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

Print original form for substitutions and learned literals (#7959)

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.

[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.

Change how RANs are printed (#7955)

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

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.

Improve names for sygus enumeration option (#7945)

Also deletes the unused (naive) basic enumerator.

Clean enumerative instantiation options (#7947)

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

Implement -o subs to show learned top-level substitutions (#7944)

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

Rename python APIs (#7950)

Rename python APIs to "base" and "pythonic"

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.

refactor div rewriter, add support for ran (#7941)

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

Fix learned rewrite pass for non-real equalties (#7936)

Fixes #7918.

Add operator<<(RewriteStatus) (#7952)

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

Weaken assertion in relevance manager (#7943)

Fixes #7937.

Refactor arithmetic pre-rewriter for multiplication (#7930)

This PR refactors the pre-rewrite stage for multiplication.

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.

Add RAN support in UMINUS rewriter (#7933)

This adds rewriting for UMINUS of real algebraic numbers

Add arithmetic rewriter for RAN (#7929)

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

Fix bug in evaluator for division by zero (#7942)

Fixes #7917.

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.

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.

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.

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.

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.

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.

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.

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.

Add mkRealAlgebraicNumber (#7923)

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

Always use partial function for sqrt (#7926)

Fixes the behavior reported in #7924.

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.

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.

Disable filtering of shapes in sygus-rcons pool. (#7922)

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

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.

api: Fix formatting of docs for Term::getSetValue(). (#7914)

Remove static accesses to options (#7913)

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

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.

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

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.

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.

Add new idiomatic examples (#7912)

[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.

Fix internal type error when printing lambdas with more than one variable in LFSC (#7909)

Check arity in Sort::instantiate (#7897)

Fixes cvc5/cvc5-projects#386.

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.

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.

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.

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>

Start post-release for 0.0.5

Bump version to 0.0.5

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.

Python Idomatic API: Document solver, results, utilities, and fns (#7882)

I put fns into "Core & Booleans".

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>

Fix eager string preprocessing in incremental mode (#7895)

Fixes #5780.

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

Some minor improvements to the theory references (#7881)

Add regressions for array sequence solver (#7874)

This closes the seqArray branch.

Document quantifiers in idiomatic python API (#7880)

[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.

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).

Disallow separation logic in incremental mode (#7888)

Fixes #5541. Fixes #5607.

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.

Fix non-idempotent rewrite in arrays (#7887)

Fixes #6807.

Minor cleaning of non-clausal simplification (#7886)

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.

Py idiomatic API: Doc sets, datatypes, FP (#7877)

api: Add missing guard for Datatype::isFinite(). (#7879)

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.

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.

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.

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