Fix non-linear equality solving that involves mixed real/integer arithmetic (#3739)

* Fix non-linear equality solving that involves mixed real/integer.

* Format

* Fix

* Revert

Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>

cmake: Remove unused ENABLE_OPTIMIZED option. (#3749)

Fix term simplification based on entailment in quantifiers rewriter (#3746)

Update issue templates

Remove `--strings-binary-csp` option (#3743)

Refactor `CoreSolver::processSimpleNEq()` (#3736)

This commit refactors and documents `CoreSolver::processSimpleNEq()`.
This method processes equalities between normal forms.

Use example evaluation cache instead of sygus PBE  (#3733)

Implement LFSCArithProof::equalityType. (#3740)

Also, missed an armType use.

Add function for tightening literals (#3732)

* Add function for tightening literals

The function tightens a literal if it can be tightened, and prints a
proof of the result.

* Include a #include

Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>

cmake: Use ld.gold if available for faster link times. (#3738)

Add more IntReal predicates (#3731)

Fix rewrite rules sat regressions (#3734)

Quantifier rewrite rules are not robust to preprocessing within our check-model infrastructure. This disables check-model on 2 satisfiable rewrite rules regressions. Fixes nightlies.

Make "unknown" non-critical for unsat cores check (#3728)

Split strings finite model finding strategy (#3727)

Split core solver from the theory of strings (#3713)

This splits the main procedure from Liang et al CAV 2014 to its own file, the "core solver" of theory of strings.

I have intentionally not updated or clang-formatted the code in core_solver.cpp since I would prefer this PR to involve as little change to behavior as possible (it is copied verbatim from theory_strings.cpp). Future PRs will clean this code up.

Interface for example evaluation cache utilities (#3726)

This adds interfaces in synth_conjecture for getting an ExampleEvalCache, per enumerator.
It also adds a specialization `checkRefinementEvalLemmas` of `getRefinementEvalLemmas` in the cegis module, which does evaluation on CEGIS refinement lemmas without structural generalization.  This function will be used as an alternative to `getRefinementEvalLemmas` for fast enumerators.

The next PR will update all utilities to use ExampleEvalCache instead of SygusPbe for evaluating examples.

Univeset Cardinality constraints for infinite types (#3712)

Refactor check-model handling in SmtEngine (#3723)

Propagate expected types through UF arguments (#3717)

Add `ArithProof::{printInteger,getLfscFunction}` (#3716)

Statistics for fast enumerator (#3699)

Example evaluation cache utility (#3698)

Fix exact sqrt (#3721)

Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>

Generalize containsQuantifiers to hasClosure (#3722)

Fix QF_NIA smt comp script (#3715)

Update INSTALL.md (#3714)

Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>

Articulate proof-related debug statements in arith (#3700)

--fp-exp: Better warning message. (#3709)

Fix header installation on MacOS. (#3660)

On MacOS sed -i requires a suffix to be set.

Split base solver from the theory of strings (#3680)

Revert semantic change from refactoring (#3711)

Regression tests for arithmetic proofs. (#3701)

* Add more arith proof regression tests

These tests are designed to test interesting cases of arithmetic proofs,
such as mixing integers and reals and tightening bounds.

Right now, they have the --no-check-proofs flag set, which prevents them
from testing the proof machinery. However, once we check that machinery
into master, we'll remove that flag, thus enabling the full effect of
the tests.

* A few comments explaining things.

* Add another tightening test

* Add new test to CMake

* No --no-check-models. There are no models anyway.

* Delete smt-lib-version, per Yoni

Increase regression test time limit to 1200s. (#3704)

Fixes #3565.

Fix corner case - might need to REWRITE_AGAIN (#3706)

Utility function for getting component types (#3703)

Minor fixes to regressions (#3702)

Fixes two issues in regressions, fixes regress1.

Fix cardinality of uninterpreted types when univset is not used (#3663)

* Fixed bug 3662

* format

* small change

* added bug3663.smt2 file

* throw Logic Exception

* throw Logic Exception

* ;EXIT: 1

Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>

Split on model values when repaired model from non-linear is inconsisent (#3668)

Fix invariant template inference for trivially infeasible conjecture (#3693)

Fix corner case of empty domains in bounded fmf (#3690)

Example inference utility (#3670)

Renaming '--bsd' to '--no-gpl' (#3609)

Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>

Handle `expectedType` in TheoryProofEngine (#3691)

`TheoryProofEngine` now uses the `expectedType` optional argument.
  * When printing terms, it sets this for theories that it dispatches too
  * It occasionally asks theories for help determining the `expectedType` using `equalityType`, which has a sensible default implementation.
  * It is mindful of `expectedType` when using the let map.

I also moved to hpp function implementations into the cpp.

Allow PBE symmetry breaking with sygus stream (#3686)

Refactor relevance vectors for asserted quantifiers (#3666)

Update sygus grammar normalization to use node-level datatype. (#3567)

Refactor sygus stats (#3684)

Minor refactoring of constructor classes in fast enumerator (#3685)

Fix arithmetic rewriter for exponential (#3688)

Fix rep set increment for empty domains (#3682)

Make eq chain an aggressive rewrite in extended rewriter (#3679)

Eliminate spurious postprocessing step for single invocation (#3674)

Ensure literals in FMF decision strategies are in the CNF stream (#3669)

Weaken assertion for models with approximations (#3667)

Move disequality list to solver state in strings (#3678)

Example minimize evaluation utility. (#3671)

External cache argument for evaluator (#3672)

Do not debug check model for models with approximations (#3673)

We don't run check-model for models with approximate values, however we were still running the internal debugCheckModel method, which leads to assertion failures. This disables this check.

Fixes #3652.

Better heuristics for marking congruent variables (#3677)

Modularize more steps in the strings strategy (#3676)

Minor updates to string utilities (#3675)

expectedType in proof-printing code (#3665)

* expectedType in proof-printing code

To print lemma proofs in theories that use multiple sorts that have a
subtype relationship, we need to increase communication between the
TheoryProofEngine and the theory proofs themselves.

This commit add an (optional) argument `expectedType` to many
term-printing functions in TheoryProofEngine and TheoryProof.

Right now it is unused, so always takes on the default value of "null"
(meaning no type expectation), but in the future the TheoryProofEngine
will use it to signal TheoryProof about what type is expected to be
printed.

* TypeNode, Don't mix default args & virtual

* Use TypeNode instead of Type (The former are lighter)
* Don't add default arguments to virtual functions, because these cannot
  be dynamically overriden during a dynamic dispatch.
  * Since we don't want them to be overidable anyway, we use two
    functions: one that is non-virtual and has a default, the other that
    is virtual but has no default. The former just calls the latter.

* clang-format after signature changes

Fix isLeq function in String utility (#3659)

Do not insist on bound values being constant in arithmetic instantiation (#3643)

Avoid PLUS with one child for bv2nat elimination (#3639)

Axioms for affine function bounds. Tests. (#3632)

* Axioms for affine function bounds. Tests.

* Apply suggestions from code review

Co-Authored-By: yoni206 <yoni206@users.noreply.github.com>
* Clarify descriptions of th_lira tests

Thanks, Yoni!

Co-authored-by: yoni206 <yoni206@users.noreply.github.com>

Fix trivial solve method for single invocation (#3650)

Fix subtyping for instantiations where internal representatives are chosen (#3641)

Fix substitution in nl solver (#3638)

* Fix for 3614

* Add regression

* Remove regression

Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>

Fix single invocation partition for non-function non-atomic types (#3642)

Fix check for subtypes in sygus PBE (#3640)

Fix parameteric sorts involving Booleans in sygus default grammars (#3629)

Types and side conditions for affine bounds (#3631)

* Types and side conditions for affine bounds

Bounds (being positive, non-negative) actually have an arithmetic.
This PR defines that.

Useful b/c Farkas proofs are basically just sums of bounded affine
functions.

* Address Yoni's comments. Thanks!

* Moved a positivity-test to th_real
* Describe what an affine bound is in better detail

Affine Axioms (#3630)

Used for proving that real terms are affine functions of their
variables.

Types & side-conditions for linear and affine fns (#3627)

This commit introduces types for linear combinations of arith variables
along with side conditions for their arithmetic.

It does the same for affine functions.

These primitives are ultimately used in our machinery for Farkas proofs.

Axioms (and side conditions) for tightening bounds (#3613)

* Axioms (and side conditions) for tightening bounds

* Side conditions for verifying floor/ceiling-like functions
* Axioms for their correct execution
* Axioms for bound tightening.

* Apply suggestions from code review

Co-Authored-By: yoni206 <yoni206@users.noreply.github.com>
* Address Yoni's comments by addings documentation.

Thanks Yoni!

Co-authored-by: yoni206 <yoni206@users.noreply.github.com>

LIRA proof: Arithmetic predicates & reification thereof (#3612)

* Merge branch 'master' into lira-pf-arith-pred

* Shorten reify_arith_pred, thanks Yoni!

Use recursion!

* typo

LIRA sig: int, real terms, and conversions (#3610)

* LIRA sig: int, real terms, and conversions

* Address Yoni's comments.

* Better description of "reify" functions
* explicit (rather than implicit) `fail` when reifying integer division

Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>

Use axioms when checking goal entailment for abduction algorithm (#3611)

New C++ API: Add nullary constructor for Result. (#3603)

Generalize example-based sym breaking to conjectures with constant function apps (#3605)

Disable unsat cores for regression that times out (#3607)

Regression `regress2/strings/issue3203.smt2` is currently timing out
depending on the version of the libraries loaded (see #3606 for more
info). This commit temporarily disables the regression to get the
nightlies to pass again.

Support arbitrary unsigned integer attributes (#3591)

Fixes #3586. On macOS, `size_t` resolves to `unsigned long` whereas `uint64_t`
resolves to `unsigned long long`. Even though the types have the same bit-width
and signedness, they are not considered the same type. This caused issues with
`Attribute`s that store `size_t` values because we only specialized the
`getTable()` struct for `uint64_t`. This commit changes the specialization to
work for arbitrary unsigned integer types of at most 64-bit. It does that by
generalizing the specialization of `getTable()` and by implementing a
`KindValueToTableValueMapping` for unsigned integer attributes of up to 64-bit
that casts integers between the attributes bit-width and `uint64_t`.

Fix side condition check in sygus core connective (#3600)

Fix enum names in AIG bitblaster. (#3599)

Fix printing of models of uninterpreted sorts (#3597)

Track trivial cases in transition inference (#3598)

Optimize str.substr reduction (#3595)

This commit optimizes the `str.substr` reduction by replacing the
if-then-else term for the length of the suffix `len(sk2) = ite(len(s) >=
n+m, len(s) - (n + m), 0)` with `(len(sk2) = len(s) - (n + m) v
len(sk2) = 0) ^ len(skt) <= m`. Experiments have shown that the latter
encoding is more efficient.

Fix backtracking issue in sygus fast enumerator (#3593)

Universe set cardinality for finite types with finite cardinality (#3392)

* rewrote set cardinality for finite-types

* small changes and format

Fix unary minus parse check (#3594)

Update any-constant and normalization policies for sygus grammars (#3583)

Fix finiteness check for bounded fmf (#3589)

Recently, finite model finding via uninterpreted sorts was decoupled from finite bound inference techniques (the BoundedIntegers module in theory/quantifiers/fmf/). This module assumed that finite model finding was enabled in one place. This fixes the issue by adding an additional check. This fixes a model unsoundness issue where bounds on an uninterpreted sort were not being enforced.

This fixes #3587.

[proof] ITE translation fix (#3484)

* Bugfix: convert ifte arms to formulas for printing

We have two kinds of ITEs in our LFSC proofs:
   * ite: for sort-typed expressions
   * ifte: for formulas
Say that we have a Bool-sorted ITE. We had machinery for emitting an
`ifte` for it, but this machinery didn't actually convert the arms of
the ITE into formulas... Facepalm.

Fixed now.

* Test the lifting of ITEs from arithmetic.

This test verifies that booleans ITEs are correctly lifted to formula
ITEs in LRA proofs.

It used to fail, but now passes.

* clang-format

* Typos.

* Add test to CMake

* Set --check-proofs in test

* Address Yoni

* Expand printsAsBool documentation
* Assert ITE typing soundness

* Assert a subtype relation for ITEs, not equality

* Update src/proof/arith_proof.h

Thanks Yoni!

Co-Authored-By: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>

Initial support for string reverse (#3581)

Type rules, parsing and printing, basic rewriting including constant evaluation, reduction for string reverse (`str.rev`).

Also improves support in a few places for tolower/toupper.

Define all options modified by ENABLE_BEST using cvc4_option (#3578)

Signed-off-by: Simon Dierl <simon.dierl@cs.tu-dortmund.de>

Fix typo in smt_options.toml. (#3579)

Increment Taylor degree for tangent and secant plane inferences for transcendentals (#3577)

Avoid calling rewriter from type checker (#3548)

Fixes #3536. The type checker for the chain operator was calling the
rewriter. However, the floating-point rewriter was expecting
`TheoryFp::expandDefinition()` to be applied before rewriting. If the
chain operator had subterms that were supposed to be removed by
`TheoryFp::expandDefinition()`, the FP rewriter was throwing an
exception. This commit fixes the issue by not calling the full rewriter
in the type checker but by just expanding the chain operator. This is a
bit less efficient than before because the rewriter does not cache the
result of expanding the chain operator anymore but assuming that there
are no long chains, the performance impact should be negligible. It also
seemed like a reasonable assumption that the rewriter can expect to run
after `expandDefinition()` because otherwise the rewriter has to expand
definitions, which may be too restrictive.

Generate code for options with modes. (#3561)

This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.