Fix a bug with synth-fun printer (#5512)

This PR fixes #5448. SynthFunCommand::toStream used to call d_grammar->resolve even when d_grammar is a nullptr. This PR fixes the issue and modifies the signature of Printer::toStreamCmdSynthFun to make it clear that grammar is an optional argument.

[proof-new] Updating SAT proof to use MACRO_RESOLUTION (#5613)

bv-to-int: Expand definitions of bvudiv and bvurem during bv-to-int preprocessing pass (#5620)

#5544 enforces expandDefinition not to run before preprocessing.
The bv-to-int preprocessing pass used to rely on expandDefinition to replace BITVECTOR_UDIV and BITVECTOR_UREM with their _TOTAL versions.
This PR performs the replacement in the preprocessing pass itself.
A regression that timed out is now fixed and is brought back to the regressions.

Make term indices in the strings base solver aware of types (#5589)

This is required for handling inputs that combine strings and sequences.

Fixes #5542.

Proper implementation of expand definitions for sequences (#5616)

Expand definitions for sequences was wrong in two ways: (1) we replaced str.from_code with a witness term. This led to it being unevaluatable in models. (2) we did not handle seq.nth, meaning its model value was unevaluatable if it was out of bounds. Now it evaluates the value of the uninterpreted function we replace with.

This corrects both issues and adds a regression to demonstrate both kinds of terms evaluate correctly.

To do this, I added a helper function to skolem cache as well as a new (internal-only) kind SEQ_NTH_TOTAL. Notice applications of this kind should only be used for model evaluation.

Notice this fixes several check-model warnings in the regressions. It still does not fix others since other things must be corrected for model evaluation (e.g. expandDefinitions must be applied on theory assertions for --debug-check-models). This will be done in later PRs.

Fix collect model values for sequences of sequences (#5579)

Fixes #5543.

Recently we changed our model construction for sequences here: #5391.

This fix is not safe for sequences of sequences, where Valuation::getModelValue should not be called, since the argument of the seq.unit is not a shared term.

This makes our model construction for sequences more robust, however I'm not sure this is the end solution. In particular, it is still questionable whether we should call Valuation::getModelValue at all (consider sequences of theories whose model construction comes after strings), or for cases of (seq.unit x) where x is a sequence or string that does not have a concrete value. Regardless, this PR could be merged in the meantime since it should definitely fix some of the current issues.

[proof-new] Adding MACRO_RESOLUTION rule and updating proof checker (#5612)

Previously CHAIN_RESOLUTION's definition and checker were not properly capturing its intended behavior as merely an n-ary RESOLUTION rule (i.e., no factoring nor reordering). A new rule, MACRO_RESOLUTION, now captures this behavior: it combines CHAIN_RESOLUTION, FACTORING, and REORDERING.

This commit also adds a proof checker for the new rule and updates the proof checker of CHAIN_RESOLUTION.

Add support for BV proofs with the simple bitblasting solver. (#5603)

Disable algebraic BV subtheory by default and make experimental. (#5596)

Fixes #5370, #5462.

Fix and reenable fact vs lemma optimization in datatypes (#5614)

This corrects an issue where terms internal to datatypes were not getting properly registered e.g. as part of the indices that determine the care graph, due to a context-independent cache being used (when a SAT-context-dependent one was required).

This reenables the fact vs lemma optimization in datatypes, as it is conjectured to be correct.

Add bitwise refinement mode for IAND (#5328)

Adds an option to do "bitwise" comparisons in the lazy IAND solver. Instead of creating an exact match for the value of a term using a sum, this would lazily fix groups of bits using integer extracts (divs and mods) when the abstract and concrete values differ at those bits.

For example, with a 1-bit granularity, you might learn a lemma like:

((_ iand 4) x y), value = 1
  actual (2, 3) = 2
  bv-value = #b0001
  bv-actual (#b0010, #b0011) = #b0010
IAndSolver::Lemma: (let ((_let_1 ((_ iand 4) x y)))
         (and (and true
                  (= (mod _let_1 2) (ite (and (= (mod x 2) 1) (= (mod y 2) 1)) 1 0)))
                  (= (mod (div _let_1 2) 2) (ite (and (= (mod (div x 2) 2) 1) (= (mod (div y 2) 2) 1)) 1 0))))
        ; BITWISE_REFINE

which is just forcing the bottom two bits of the iand operator result to implement bitwise-AND semantics.

Fix issue with free variables introduced by quantifier rewriter (#5602)

This was caused by the quantifiers rewriting eliminating extended arithmetic operators, which was required due to the way counterexample-guided quantifier instantiation used to work with preprocessing. The technique is now more robust and this option can be deleted.

This fixes a debug assertion failure from UFNIA SMT-LIB, a minimized benchmark is included as a regression.

Refactor initial phase of transcendental solver (#5599)

This PR refactors the initialization of the transcendental solver, decoupling the setup of generic caches from initial lemmas for exponential and sine functions.

Do not expand theory definitions at the beginning of preprocessing (#5544)

This updates the preprocessor so that expand definitions does not expand theory symbols at the beginning of preprocessing.

This also restores the previous expandDefinitions method in arithmetic, which is required for correctly interpreting division by zero in models, but should not be applied at the beginning of preprocessing. Moreover it ensures that only partial operators are eliminated in arithmetic expandDefinitions, which required an additional argument partialOnly to arith::OperatorElim.

This adds -q to suppress warnings for many quantified regressions which now emit warnings with --check-model. This will be addressed later as part of CVC4/cvc4-wishues#43.

The purpose of this PR is two-fold:
(1) Currently our responses to get-value are incorrect for partial operators like div, mod, seq.nth since partial operators can be left unevaluated.
(2) The preprocessor should have the opportunity to rewrite and eliminate extended operators before they are expanded. This is required for addressing performance issues for non-linear arithmetic. It is also required for ensuring that trigger selection can be done properly for datatype selectors (to be addressed on a later PR).

 (proof-new) Split proof ensure closed checks to own file (#5522)

Split proof ensure closed checks to own file

Add regression from #4927 (#5556)

The error from #4927 has been fixed in the meantime, this PR adds the example as regression.
Closes #4927.

Fix bugs in getFreeVariables (#5601)

Did not consider scopes properly, which would fail to say that formulas with escaped variables (both bound and unbound) in formula had free variables.

Change generated options to be thread_local. (#5583)

Signed-off-by: Everett Maus <evmaus@google.com>

google test: expr: Migrate attribute_black. (#5598)

google test: context: Migrate cdo_black. (#5586)

google test: context: Migrate cdmap_white. (#5585)

Fix bug in hasBoundVar (#5600)

Led to issues while debugging another issue related to free variables in assumptions.

google test: api: Migrate sort_black. (#5594)

google test: context: Migrate cdmap_black. (#5584)

google test: context: Migrate cdlist_black. (#5582)

Use NodeDfsIterable for makeBinary (#5595)

Replaces the manual dag traversal in BVToInt::makeBinarywith NodeDfsIterable.

This is a subset of the changes in #4176, updated to apply to master.

update-copyright: Preserve file permissions. (#5597)

When updating the copyright headers file permissions were not preserved. In some cases this results in losing the permission to execute scripts. This commit makes sure to preserve the file permissions for updated files.

(proof-new) Updates to SMT proof manager and SmtEngine (#5446)

This PR adds infrastructure in SmtEngine and ProofManager for checking and printing proofs. It updates a previous interface that used ProofGenerator in favor of ProofNode.

This makes it so that it only remains to make PropEngine to be proof producing.

google test: api: Migrate solver_black. (#5570)

Use mkAnd where the number of children may be less than two. (#5551)

An AND was constructed from a vector that may only hold a single or no element.
This PR uses mkAnd instead.
Fixes #5550 .

Models as (#5581)

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

delete the model keyword (done in #5415 )
avoid printing extra declarations by default (done in #5432 )
wrap UF values with as expressions.
This PR does step 3, fixes a regression accordingly, and adds the formula from #4987 and a variant of it to the regressions.

google test: Add fixture for context tests. (#5590)

Context test PRs will be updated to use this after this is merged to
master.

Refactor handling of global declarations (#5577)

This refactors how global declarations are handled in the parser. In particular, we do not push/pop user contexts in the symbol table and manager when global declarations are true, which is an equivalent behavior to declaring symbols globally.

This further refactors to not use ExprManager flags, thus breaking most of the dependencies on the old API.

This is work towards fixing global declarations in the smt2 parser. The parser still does not behave correctly for overloaded symbols + global declarations (e.g. see #4767), which require further refactoring.

This is also work towards migrating the parser not to depend on the old API. There are a few miscellaneous things to change after this PR, but we are very close to breaking this dependency now.

Make run_regression.py executable. (#5588)

Update copyright headers.

google test: base: Migrate map_util_black. (#5580)

Fix RoundingMode mapping in API. (#5578)

Fixes #5524.

Remove Record object and convert to Node-level API (#5575)

Required for detangling NodeManager from the Expr layer.

Rename macro Message to CVC4Message. (#5576)

Remove dagification visitor (#5574)

This has fully been replaced by the new let binding.

google test: api: Migrate term_black. (#5571)

google test: api: Use individual fixture for datatype_black. (#5568)

This is to prevent name clashes with other tests.

Add associative utilities to node manager (#5530)

Required for updating the new API to use Node utilites as backend.

These utilities are copied directly from ExprManager and converted Expr -> Node.

google test: api: Migrate op_black. (#5567)

google test: api: Migrate grammar_black. (#5566)

Use new let binding for cvc printer (#5561)

Also changes names slightly to avoid accidental uses of toStream, which can lead to infinite loops if the wrong version is used.

(proof-new) Proofs for expand definitions (#5562)

Add regressions from #3687. (#5553)

The error from #3687 has been fixed in the meantime.
This PR adds the two examples from this issue as regressions.
Closes #3687

google test: api: Migrate result_black. (#5569)

google test: api: Migrate result_black.

Remove use of this-> in FP literal. (#5565)

Remove assertion related to CEGQI dependency lemmas (#5559)

This assertion does not hold when we mix --sygus-inst with normal CEGQI.

Should fix the nightlies.

google test: Infrastructure and first api test. (#5548)

This sets up the infrastructure for migrating unit tests from CxxTest to
Google Test. It further migrates api/datatype_api_black to the new
infrastructure.

Fix issues related to model declarations (#5560)

This corrects two issues related to model declarations:
(1) model declaration terms were mistaken not cleared,
(2) the model needs to be explicitly destructed before the node manager because it contains references to Node.

Fixes #5540

Improve rewriting of str.<= (#4848)

This commit improves our rewriting of str.<= slightly. If we have
constant prefixes that are different, we can always rewrite the term to
a constant. Previously, we were only doing so when the result was
false.

Refactor transcendental solver (#5539)

This PR does another round of refactoring on the transcendental solver. It cleans up some variable names, introduces an enum type for Convexity and passes both the intended taylor degree and the actual taylor degree (which will be needed for proofs).

Add regressions from #5099 (#5557)

The issue from #5099 has been fixed in the meantime, this PR adds the examples as regressions.
Closes #5099.

Add regression for #4335. (#5554)

The error from #4335 has been fixed in the meantime, this PR adds a regression for this issue.
Closes #4335.

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.