Add regressions for #4707. (#5555)

The error from #4707 has been fixed in the meantime, this PR adds the example inputs as regressions.
Closes #4707.

More fixes for quantifier elimination (#5533)

Fixes #5506, fixes #5507.

fix metadata for a test (#5546)

A COMMAND was used instead of COMMAND-LINE.

fp_converter: Properly separate out symbolic glue code. (#5501)

File fp_converter.h encapsulates the symbolic glue code for symFPU and
implements the actual word-blaster (class FpConverter).
This header should not be included in any other headers in order to no
pull in symFPU headers where it's not needed. However, it was included
in src/theory/fp/theory_fp.h.

This properly separates it out and does some clean up in TheoryFP, which
still needs more love to conform to code style guidelines, and also
more documentation. More love and documentation is postponed to future
PRs to make reviewing easier.

Use new let binding in AST printer (#5529)

Required for removing the old DagificationVisitor

floatingpoint: Use unique_ptr for FloatingPointLiteral pointer. (#5503)

Eliminate uses of SExpr from the parser. (#5496)

This is a step towards migrating Commands to the API. SExpr is an internal module that's not used by the API but is used by the parser and some commands. This PR replaces SExpr with terms of kind SEXPR in the parser and strings in commands (which brings them more inline with the API).

Remove includes for old API from internal code (#5536)

The only code including the old API now are in parser/ and main/ which will require further untangling.

(proof-new) Proofs for regular expression elimination (#5361)

Adds support for proofs for regular expression elimination in TheoryStrings::ppRewrite via a coarse-grained rule RE_ELIM.
This rule is updated by this PR to distinguish whether we apply aggressive elimination. Aggressive elimination is not currently supported, since it is non-deterministic due to generating fresh BOUND_VARIABLE.

Make CAD solver work for empty set of assertions (#5535)

When called with no assertions, the CAD solver would still go to work and then segfault when trying to access the first variable.
This PR adds an explicit check for this case and adds a regression.
Fixes #5534 .

Removing infrastructure related to SMT model (#5527)

Now, SMT models do not store an internal list of commands, and are not dependent on a reference to SmtEngine.

The next cleanup step will be to merge OutputManager, DumpManager, and SmtEngineNodeListener.

Move expand definitions to its own file (#5528)

We are changing our policy on how expand definitions is handled during preprocessing.

This will require some additions to expand definitions handling. This PR makes a standalone module for expanding definitions.

Fully decouple SmtEngine and the Expr layer (#5532)

This removes the remaining dependencies of SmtEngine on the Expr layer. It now takes a NodeManager instead of a ExprManager.

Fix missed case of theory preprocessing (#5531)

This fixes a rare case of theory preprocessing where rewriting a quantified formula would introduce a term that would not be preprocessed. This led to solution unsoundness on a branch where the relationship between expand definitions and preprocessing is modified.

This is required for updating to the new policy for expand definitions.

Disable fact vs lemma optimization in datatypes for now (#5521)

This optimization needs more work to determine its correctness. It is currently leading to incorrect candidate models on Facebook benchmarks.

Add regressions for closed issues (#5526)

We can close #5520, we can close #5378.

Fix transcendental secant plane lemmas (#5525)

The refactoring of the transcendental solver introduced a subtle issue that lead to incorrect secant plane lemmas.
This PR fixes this issue, so that we now produce the correct lemmas again.

Use symbol manager for printing responses get-model (#5516)

This makes symbol manager be in charge of determining which sorts and terms to print in response to get-model. This eliminates the need for the parser to call ExprManager::mkVar (and similar methods) with custom flags.

This requires significant simplifications to the printers for models, where instead of a NodeCommand, we take a Sort or Term to print in the model.

This is one of the last remaining steps for migrating the parser to the new API.

The next step will be to remove a lot of the internal infrastructure for managing expression names, commands to print in models, node commands, node listeners, etc.

Allow printing of null node in let binder (#5523)

Refactor transcendental solver (#5514)

The transcendental solver has grown over time, and a refactoring was due.
This PR splits the transcendental solver into five components:

a utility to compute taylor approximations
a common state for transcendental solvers
a solver for exponential function
a solver for sine function
a solver that wraps everything to a transcendental solver.

Fix regular expression consume for nested star (#5518)

The issue was caused by simple regular expression consume being too aggressive when a recursive call was made to the method. In particular, we were assuming that the body of the star must be unrolled to fully consume a string, when it can be skipped if we are not at top level.

Fixes #5510.

Change UF ho to ppRewrite instead of expand definition (#5499)

UF uses expandDefinitions to convert fully applied HO_APPLY to APPLY_UF. The more appropriate place to do this is in Theory::ppRewrite.

Fix for sygusToBuiltinEval for non-ground composite terms (#5466)

There was a bug in the method for computing the evaluation of a sygus term applied to arguments.

The case that was wrong was for (DT_SYGUS_EVAL t c1 ... cn) where t contained a subterm (op t1 ... tn) where:
(1) (op t1 ... tn) is a non-ground sygus datatype term
(2) op was an operator of the form (lambda ((z T)) (g z xi)) where xi is a variable from the formal argument list of the function to synthesize.
In this case, xi was not getting replaced by ci.

This bug appears when using sygus repair for grammars with composite term that involve variables from the formal argument list of the synth-fun.

(proof-new) Miscellaneous changes from proof-new (#5445)

Add declare model symbol methods to SymbolManager and Model (#5480)

This is in preparation for the symbol manager determining which symbols are printed in the model.

Add get-info :time. (#5485)

This PR adds the new info `:time` that can be queried with `(get-info :time)` and returns the spent CPU time (as returned by `std::clock()`.
 @pjljvandelaar
Fixes CVC4/CVC4-projects#102

Fix quantifiers scope issue in strings preprocessor (#5491)

Leads to free variables in assertions when using `str.<=` whose reduction uses EXISTS not FORALL.

Fixes #5483.

Add posRewriteEqual to bags rewriter (#5498)

This PR fixes #5460 by adding posRewriteEqual to bags rewriter

Rename symfpu_literal.(h.in|cpp) -> floatingpoint_literal_symfpu.(h.in|cpp). (#5502)

Rename floatingpoint.h.in -> floatingpoin.h. (#5500)

Fix remove term formula policy for terms beneath quantifiers (#5497)

Now that extended arithmetic symbols are not eliminated during expandDefinitions, this allowed for a chain of events that would not apply theory preprocessing on certain terms.

In particular, a term t would not have theory preprocessing applied to it if it was a strict subterm of ITE-term s that occurred in a term position in a quantified formula body, and s did not have free variables. In this case, term formula removal would add a lemma corresponding to the ITE skolem definition, whose subterms did not have theory preprocessing applied. This meant that a (div a d) term was not being preprocessed in #5482, leading to solution unsoundness.

This changes the policy in term formula removal to be in sync with theory preprocessing: term formula removal and theory preprocessing only apply to terms that are not beneath quantifiers. In particular, this means that ground terms in quantifier bodies are left untouched until they are introduced e.g. by instantiation.

This fixes the solution soundness issue (fixes #5482).

RoundingMode: Rename enum values to conform to code style guidelines. (#5494)

FloatingPoint: Separate out symFPU glue code. (#5492)

This works towards having the symFPU headers only included where it's
absolutely needed (only in the .cpp files, not in any other headers).

Note: src/util/floatingpoint.h.in will be converted to a regular .h file
      in the next step to simplify reviewing.

Fix #5493. (#5495)

Support nested quantifier elimination for get-qe command (#5490)

Uses new nested-qe utility for eliminating nested quantification before doing quantifier elimination.

Fixes CVC4/cvc4-wishues#26

Fixes #5484.

Updates to API in preparation for using symbol manager for model (#5481)

printModel no longer makes sense if the list of declared symbols is managed outside the solver.

Also, mkConst needs a variant to distinguish a provided name of "" vs. a name that is not provided.

Fix compiler warnings. (#5493)

Fix use of declaration sequence command in cvc parser (#5479)

This is required to make the cvc parser work properly with the new version of getting models based on the symbol manager.

(proof-new) Replace LazyCDProofSet by generic CDProofSet (#5487)

This PR replaces the LazyCDProofSet, that was hardcoded to use LazyCDProof objects, by a templated CDProofSet.

Allow to pass ProofGenerator to arithmetic inference manager. (#5488)

This PR prepares the addition of proofs for the arithmetic theory by making addPendingArithLemma() accept a ProofGenerator*.

Enable new implementation of CEGQI based on nested quantifier elimination (#5477)

This replaces the old implementation of CEGQI based on nested quantifier elimination (--cegqi-nested-qe) with the new implementation.

The previous implementation used some convoluted internal attributes to manage dependencies between quantified formulas, the new implementation is much simpler: it simply eliminates nested quantification eagerly.

Fixes #5365, fixes #5279, fixes #4849, fixes #4433.

This PR also required fixes related to how quantifier elimination is computed.

floatingpoint.h: Split in preparation to cleanly separate symFPU glue code. (#5478)

Use new let binding utility in smt2 printer (#5472)

Also fixes some whitespace issues in printing quantified formulas.

Include stddef.h (needed for size_t) in cvc4_public.h (#5476)

This further removes obsolete explicit includes of stdint.h.

Add nested quantifier elimination module (#5422)

This has static utilities for doing nested quantifier elimination and some data structures for maintaining a context-dependent set of quantified formulas that have been processed.

This is work towards CVC4/cvc4-wishues#26, and work reimplementation of the option --ceqgi-nested-qe.

Fix issues related to eliminating extended arithmetic operators (#5475)

This fixes 2 issues related to eliminating arithmetic operators:
(1) counterexample lemmas in CEGQI were not being preprocessed
(2) ensureLiteral was not doing term formula removal.
This corrects these two issues. Now ensureLiteral does full theory preprocessing on the term we are ensuring literal for, meaning this may trigger lemmas if the term contains extended arithmetic operators like div.

Fixes #5469, fixes #5470, fixes #5471.

This adds --sygus-inst to 2 of these benchmarks which moreover makes them solvable.

This also improves our assertions and trace messages.

Use symbol manager for unsat cores (#5468)

This PR uses the symbol manager for handling names for unsat cores.

This replaces interfaces in SmtEngine for managing expression names. It removes the SetExpressionName command.

Add -> operator overload for cd* iterators. (#5464)

Disable slow nl regression (#5467)

Add let binding utility (#5444)

This utility will replace the dagification visitor for printing lets for Node in the smt2 printer, and will be used further in e.g. LFSC proof printing.

Minor cleanup of SmtEngine (#5450)

Do not expand definitions of extended arithmetic operators (#5433)

This PR makes it so that extended arithmetic operators are not expanded during expand definitions. Instead they are eliminated at theory preprocessing, which occurs as the last step of preprocessing.

The motivation for this is three fold:
(1) Some quantified LIA benchmarks lead to CVC4 failing to eliminate div functions from quantifier instantiation, this leads to spurious logic failures. A regression is included, which now is correctly solved.
(2) We should allow better rewriting and preprocessing for extended arithmetic functions, especially for div/mod which is important for many users of QF_NIA.
(3) More generally,Theory::expandDefinitions will be deleted. All functionalities in expandDefinitions should move to Theory::ppRewrite.

This changes impacts many benchmarks that involve non-linear and quantifiers:

Many benchmarks (as expected) give a warning during check-models since (/ n 0) cannot be evaluated. I've added -q to disable these warnings. Fully addressing this is part of an agenda to improve our support for --check-models.
Several fuzzing benchmarks involving NL+quantifiers now time out. However, several can be solved by --sygus-inst, which is now the preferred instantiation strategy for NL+quantifiers.
2 other non-linear regressions time out, which are disabled in this PR.
one sygus-inference benchmark (regress1/sygus/issue3498.smt2), now correctly times out (previously it did not timeout since the preprocessor was unable to apply sygus-inference and resorted to normal methods, now sygus-inference can apply but as expected times out).
Fixes #5237.

Use symbol manager for get assignment (#5451)

This replaces the previous methods for get-assignment which involving making a DefinedNamedFunctIonCommand and storing the expression names map in the SmtEngine.

Note: we now limit :named terms to those not beneath quantifiers and let-bindings.

Fix asan issues related to solver and symbol manager (#5457)

Should fix the nightlies.

FloatingPoint: Use uint32_t instead of unsigned. (#5459)

FloatingPoint: Clean up and document header, format. (#5453)

This cleans up the src/util/floatingpoint.h.in header to conform to the
code style guidelines of CVC4. This further attempts to fully document
the header. The main changes (except for added documentation) are
renames of member variables, getting rid of the redundant functions
FloatingPointSize::exponent() and FloatingPointSize::significand(),
and a more explicit naming of CVC4 wrapper types vs symFPU trait
types. Else, it's mainly reordering and formatting.

ci: Simplify Python dependency installs for Linux and macOS. (#5458)

Fix tangent plane lemmas (#5455)

The previous refactoring of tangent plane lemmas introduced incorrect lemmas.
This PR fixes this issue and actually generated the lemmas described in the comment.
Fixes #5452.

Refactor tangent plane lemmas (#5449)

The original lemma only proposed an implication for the tangent plane lemmas, while our implementation adds the inverse implication as well (in a somewhat verbose way).
This PR replaces this by simply constructing the equivalence.

Cleaning up scopes in preparation for symbol manager (#5442)

This changes the default of Parser::pushScope and prepares symbol manager further for maintaining expression names.

Improve accuracy of resource limitation (#4763)

The main goal of the resource limitation mechanism (via `--rlimit`) is to have a deterministic limitation on runtime. The ultimate goal would be that the actual runtime grows linearly with the spent resources.
To achieve this, this PR does the following:
- introduce new resources spent in places that are not yet covered
- find resource weights that best approximate the runtime

It provides a contrib script `learn_resource_weights.py` that uses statistics from a given benchmark run and uses linear regression to find good resource weights. The script also evaluates this estimate and identifies outliers, benchmarks for which this approximation is particularly bad. This probably indicates that on such a benchmark, some part of the code takes a significant amount of time but is not yet represented by a resource.

Eventually, we should use the resulting resource weights as defaults for the options like `--rewrite-step`, `--theory-check-step`, etc.

Fix double conflict in extended string solver (#5435)

Fixes #5384.

Previously we were not breaking on conflict in all cases.

(proof-new) Proofs for non-clausal simplification (#5409)

Adds proof support in non-clausal simplification, connecting the proofs from circuit propagator.

(proof-new) Enable proofs for datatypes (#5436)

This enables initial proof support in datatypes, which includes connecting the inference-to-proof constructor to the inference manager and making the proper calls to the inference manager using TheoryDatatypes.

Model declarations printing options (#5432)

This PR relates to #4987 .
Our plan is to:

delete the model keyword
avoid printing extra declarations by default
wrap UF values with as expressions.
This PR is step 2. It allows the user to choose the model printing style in case of uninterpreted elements: either using datatypes, or using declare-sorts and declare-funs or just using declare-funs.

The default option, which is closest to the standard, is just using declare-funs. In step 3, these will be replaced by abstract values using as.

Add more features to symbol manager (#5434)

This is in preparation for having the symbol manager manage expression names at the parser level instead of inside SmtEngine.

This adds some necessary features regarding scopes and global declarations.

This PR still does not change the behavior of the parser.

Make regular expression difference left associative (#5430)

Fixes #5428.

Simplify sygus solver and sygus stream (#5389)

This simplifies the sygus solver based on the fact that verification lemmas are always processed in a separate subsolver.

In particular, this means that the implementation of --sygus-stream can be simplified signficantly.

Fix printing of define named function (#5425)

Fixes the case where the type of the function is not a function type.

Models standard (#5415)

This PR relates to #4987 .
Our plan is to:

delete the model keyword
avoid printing extra declarations by default
wrap UF values with as expressions.
This PR does step 1, and fixes regressions accordingly.

(proof-new) Separate explanation stages in proof equality engine (#5356)

This fixes potential cycles in assertLemma commands in the proof equality engine by using separate proof data structures for the topmost 2 stages of proof generation for equality engine proofs. This fix is required to support datatype proofs for lemmas.

This PR also removes support for the ProofStepBuffer interface in ProofEqEngine, since it is unused, and suffers similar issues and would require a different unique fix.

Fix redundant refinement lemma in sygus solver (#5399)

This ensures we do manual exclusion of candidate solutions that have counterexamples that are repeated, in particular in the case where the synthesis conjecture has no free variables.

This PR removes special casing for ground synthesis conjectures and fixes the exclusion during the refinement stage of sygus.

This is a prerequisite for updating arithmetic to not eliminate extended operators at expand definitions, which forces this feature to be exercised in a number of regressions.

(proof-new) Proofs for skolemization (#5339)

This adds support for proofs in the quantifiers module that performs skolemization.

Also fixes a bug in the proof checker for skolemization.

(proof-new) Fix true explanations of propagations in pf equality engine (#5338)

This ensures we construct proper proofs for propagations whose conclusions are of the form (=> true lit). Literals may be propagated with "true" as an explanation in datatypes, e.g. discriminators for datatypes with 1 constructor.

(proof-new) Improve printing and debugging for pedantic checking  (#5337)

This improves trace/error messages for proof-new-pedantic, and also merges the proof-new-pedantic-eager with the proof-new-eager-checking option.

(proof-new) Add datatypes inference to proof constructor (#5408)

This adds the module that constructs proofs from inference steps.

A followup PR will integrate proof support into the datatypes inference manager.

Make symbol manager context dependent (#5424)

This follows a similar style to symbol_table.h/cpp. This is required since context dependent data structures are cvc4_private, and symbol manager is cvc4_public.

Move symbol manager to src/expr/ (#5420)

This is required since symbol manager will use context dependent data structures (in its cpp).

This is required since classes in src/parser/ are not allowed to include private headers.

Rewrite witness terms at prerewrite (#5419)

Ensures (witness ((x Int)) (= x (+ 1 a)) is rewritten to (+ 1 a), instead of e.g. (witness ((x Int)) (= a (- x 1)).

This is required for supporting purification skolems for arithmetic terms in the new proof architecture.

Add simple substitution utility (#5397)

A few new algorithms for CEGQI and single invocation sygus will use this utility for managing transformations.

Pass symbol manager to commands (#5410)

This PR passes the symbol manager to Command::invoke.

There are no behavior changes in this PR. This is in preparation for reimplementing several features in the parser related to symbols.

Fix preregistration in TheorySep before declare-heap (#5411)

Followup to fix for #5343. This catches cases where separation logic constraints are preregistered to TheorySep before the heap has been declared, which should also result in an error.

Do not mark extended functions as reduced based on decomposing contains (#5407)

Fixes #5381.

Pin LFSC version (#5412)

I chose commit 61ef1dc55d2bc909656f905699b28c99ddcfc518,
which is missing:

any changes to the OSX build process
(We're still figuring this out)
change to top-level identifier shadowing
(we have a few versions of the signatures floating around, and I
worry that they may not all be fixed w.r.t. no re-using identifiers)

Make mkGroundTerm deterministic (#5347)

This ensures mkGroundTerm is deterministic using attributes.

This was uncovered by failures in the proof checker for datatypes.

Add getSubtermKinds to node algorithm (#5398)

Required for a new algorithm for nested quantifier elimination.

Add proper support for the declare-heap command for separation logic (#5405)

This adds proper support for the (declare-heap (T U)) command, which declares the type of the heap in separation logic. This command is part of the standard for separation logic.

This previous was handled in an ad-hoc way where the type of the heap would be inferred on demand. This was a poor solution and has led to a number of issues related to when the heap is inferred.

Fixes #5343, fixes #4926.

Work towards CVC4/cvc4-wishues#22.

Migrate some documentation about attributes (#5390)

From old wiki.

Add symbol manager (#5380)

This add the symbol manager class, which is a Term-level utility, separate of the API. This class manages things like expression and assertion names, which is intentionally done outside the solver.

The symbol manager is intended to live at the same level as the Solver. When parsing input, the symbol manager will be used to model any interaction of e.g. named expressions and assertions. It also stores the symbol table of the parser.

This PR adds the basic interface for the symbol manager and passes it to the parser.

Later PRs will migrate the functionality for named expression out of e.g. SmtEngine and into SymbolManager. Commands will take Solver+SymbolManager instead of Solver. This will allow the parser to be fully migrated to the new API.

Marking "complex" since this impacts further design of the parser and the code that lives in src/main.

FYI @4tXJ7f

Simplify handling of subtypes in smt2 printer (#5401)

This makes major simplifications to how subtypes are enforced in the smt2 printer.

It is now the principle that the smt2 prints things faithfully to the AST, regardless of whether it conforms to the smt2 standard.

It also fixes the current smt2 printing of to_real.

Conversely, this removes a hack from GetValueCommand which forced casting via x -> (/ x 1). This is now properly handled in Solver::getValue.

Some regressions change expected output as a result. Notice that internally generated Node may not conform to the smt2 standard, but user-level terms will.

Properly clear interrupt for solve() as well. (#5403)

The minisat solver stores whether it has been interrupted in asynch_interrupt and expects it to be reset before another call to solve(). MinisatSatSolver::solve() failed to do this, leading to incorrect unknown results as observed in CVC4/cvc4-projects#106. The alternative MinisatSatSolver::solve(unsigned long& resource) already did the correct thing.
Fixes CVC4/cvc4-projects#106.

Do not regress explanations of datatype lemmas (#5376)

This modifies datatypes to not regress explanations for lemmas. This avoids segfaults in some corner cases of sygus (see attached) and leads to slightly better performance on Facebook verification benchmarks.

Fix issue #5342 (#5349)

This PR fixes issue #5342 by adding the rewrite rule (setminus A (setminus A B)) = (intersection A B).

(proof-new) Miscellaneous changes to strings for proofs (#5362)

This includes all minor remaining changes from proof-new for strings that were not merged to master.

This includes mostly minor changes to make proofs pass, including reordering assertions. It also removes some non-standard pedantic checks as these are now subsumed by standard ones.

It also makes the strings rewriter slightly more safe when checking arithmetic entailment under assumptions. This code used substitution, which was not safe when quantifiers were involved. This is replaced by capture avoiding substitution here.

Split sygus template inference to its own file (#5388)

This splits techniques for inferring templates for functions-to-synthesize to their own file.

This is work towards cleaning up the single invocation utility, which will be undergoing some additions.

Simplify printing with respect to expression types (#5394)

This removes infrastructure for stream property related to printing type annotations on all variables.

This is towards refactoring the printers.

Remove mkSingleton from the API (#5366)

This PR removes mkSingleton from the API after removing subtyping from set theory and introducing mkInteger to the API.
Instead the user needs to use Solver::mkTerm(api::SINGLETON, element) where element has the right type.
Internally NodeManager::mkSingleton(type, element) is still needed to determine the type of the set.
Other changes:

Renamed Solver::mkTerm(Op op, .. functions to Solver::mkTermFromOp(Op op, ...
Added mkTermFromOp to the python API

Add constants from equality engine evaluation to model (#5391)

Fixes #5330. The issue mentions to related model checking failures:

When the theory of strings computes a model, there is a step that
chooses a constant that is different from other constants of the same
length in other equivalence classes. In the example, the issue was
that the constant "A" was introduced by doing evaluation in the
equality engine of the theory of strings. The constant was then not
added to the term set and was skipped while asserting the equality
engine to the theory model. As a result, an equivalence class was
assigned "A" even though it already existed, which made the model
invalid. The fix ensures that all constants in the equality engine are
added to the theory model. It should be ok to handle the issue during
model construction because other theories shouldn't have to care about
the constants that we computed internally within the theory of
strings.
When an equivalence class has a normal form that consists of a single
seq.unit, then we need to make sure that the value for the argument
is consistent with the rest of the model and we have to make sure that
we choose different values for different equivalence classes. The
commit adds code for retrieving the value of the argument to
seq.unit from the model and adds the resulting constant to the
theory model to block it for other equivalence classes. Previously,
this was not done and we ended up with two different equivalence
classes being assigned the same constant.

Add scope methods constructing types in API (#5393)

This addresses the nightly failures. It ensures a node manager is in scope when constructing type nodes.

It also simplifies the construction of atomic type nodes to avoid an extra TypeNode(...) constructor.

Add support for printing `re.loop` and `re.^` (#5392)

In the new SMT-LIB string standard, re.loop and re.^ are indexed
operators but the printer was not updated to print them correctly. This
commit adds support for printing re.loop and re.^.