| Age | Commit message (Collapse) | Author |
|---|
|
Fixes #5524.
|
|
Required for detangling NodeManager from the Expr layer.
|
|
|
|
This has fully been replaced by the new let binding.
|
|
Required for updating the new API to use Node utilites as backend.
These utilities are copied directly from ExprManager and converted Expr -> Node.
|
|
Also changes names slightly to avoid accidental uses of toStream, which can lead to infinite loops if the wrong version is used.
|
|
|
|
|
|
This assertion does not hold when we mix --sygus-inst with normal CEGQI.
Should fix the nightlies.
|
|
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
|
|
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.
|
|
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).
|
|
Fixes #5506, fixes #5507.
|
|
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.
|
|
Required for removing the old DagificationVisitor
|
|
|
|
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).
|
|
The only code including the old API now are in parser/ and main/ which will require further untangling.
|
|
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.
|
|
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 .
|
|
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.
|
|
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.
|
|
This removes the remaining dependencies of SmtEngine on the Expr layer. It now takes a NodeManager instead of a ExprManager.
|
|
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.
|
|
This optimization needs more work to determine its correctness. It is currently leading to incorrect candidate models on Facebook benchmarks.
|
|
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.
|
|
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.
|
|
|
|
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.
|
|
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.
|
|
UF uses expandDefinitions to convert fully applied HO_APPLY to APPLY_UF. The more appropriate place to do this is in Theory::ppRewrite.
|
|
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.
|
|
|
|
This is in preparation for the symbol manager determining which symbols are printed in the model.
|
|
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
|
|
Leads to free variables in assertions when using `str.<=` whose reduction uses EXISTS not FORALL.
Fixes #5483.
|
|
This PR fixes #5460 by adding posRewriteEqual to bags rewriter
|
|
(#5502)
|
|
|
|
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).
|
|
|
|
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.
|
|
|
|
Uses new nested-qe utility for eliminating nested quantification before doing quantifier elimination.
Fixes CVC4/cvc4-wishues#26
Fixes #5484.
|
|
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.
|
|
|
|
This is required to make the cvc parser work properly with the new version of getting models based on the symbol manager.
|
|
This PR replaces the LazyCDProofSet, that was hardcoded to use LazyCDProof objects, by a templated CDProofSet.
|
|
This PR prepares the addition of proofs for the arithmetic theory by making addPendingArithLemma() accept a ProofGenerator*.
|
|
(#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.
|
