Age | Commit message (Collapse) | Author |
|
|
|
This PR classifies all internal kinds of incompleteness as identifiers.
It makes it so TheoryEngine records an identifier when its incomplete flag is set.
The next step will be to possibly communicate this value to the user.
|
|
Fixes #6298.
Enables parsing of par in the sygus parser, and adds support for default grammar construction.
Also fixes a bug related to single invocation for non-function types.
|
|
Fixes benchmarks 2 and 3 from #5848.
|
|
This is in preparation for refactoring skolem creation throughout the code base to improve proofs and migrate Theory::expandDefinitions to Rewriter::expandDefinitions.
This PR also eliminates some unused code in TheoryArithPrivate.
Followup PRs will start formalizing/eliminating calls to mkDummySkolem.
|
|
|
|
|
|
(#6240)
This completes eliminating dependencies on quantifiers engine from internal quantifiers code. It eliminates quantifiers_engine.h as an include from src/theory/quantifiers/ apart from theory_quantifiers.cpp where it is owned.
Followup PRs will further eliminate circular dependencies that arose will refactoring quantifiers engine.
|
|
This should be the last PR before quantifiers engine will not be passed to quantifiers modules.
|
|
|
|
This makes it so that the decision manager is accessible from TheoryInferenceManager.
This is work towards breaking circular dependencies in quantifiers, and also helps simplify several other dependencies in e.g. UF and datatypes.
|
|
|
|
This PR adds includes that are missing from source files, but currently provided by other includes.
This mostly concerns <sstream> which is currently included by the statistics, which will change in the future.
|
|
engine (#6198)
Towards breaking dependencies on quantifers engine.
|
|
|
|
This PR replaces the old algorithm for reconstructing sygus terms with a new "proper" implementation.
|
|
This is in preparation for moving several utilities into the quantifiers inference manager.
This PR moves ownership of TermRegistry and QuantifiersRegistry to TheoryQuantifiers from QuantifiersEngine.
|
|
|
|
This PR does some more cleanup of the includes.
|
|
|
|
This commit removes the partial UDIV/UREM operator handling. BITVECTOR_UDIV and BITVECTOR_UREM are now total.
|
|
Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files.
|
|
This PR is a step towards removing SExpr class. It replaces SExpr with std::string for set-info and set-option commands.
|
|
This groups utilities related to ground terms into TermRegistry which will be passed to quantifier modules.
|
|
This PR cleans up a ton of includes, based on the suggestions of iwyu.
Mostly, it removes includes from header files in favor of forward declarations and adds includes to source files.
|
|
This makes all lemmas in quantifiers sent through the inference manager. It begins adding InferenceId values for some of these calls. All uses of Valuation are replaced by calls to QuantifiersState.
|
|
This moves the utility class beneath quantifiers registry.
|
|
This makes it so that TermUtil is now a collection of static methods. Further refactoring will make this a standalone file of utility methods.
This breaks all dependencies on the TermUtil object in QuantifiersEngine. It also starts breaking some of the depenendencies on quantifiers engine in sygus.
|
|
Towards eliminating dependencies on quantifiers engine, and eliminating the TermUtil class.
Note that QuantifiersModule had to be moved to its own file to avoid circular include dependencies.
|
|
This PR collects the InferenceId in the InferenceManagerBuffered class.
|
|
Towards eliminating dependencies on quantifiers engine.
This replaces the custom implementation of lemma management in quantifiers engine with the standard one.
It makes a few minor changes to the standard inference manager classes to ensure the same behavior for quantifiers.
Note that some minor changes in behavior are introduced in this PR, such as being more consistent about caching/rewriting lemmas. This should not have any major impact.
|
|
This is a simple module for determining which quantifiers module has ownership of quantified formulas.
This is work towards eliminating dependencies of quantifiers modules.
Note that quantifiers attributes module (which no longer has a dependency on QuantifiersEngine after this PR) will be embedded into this module in a later PR.
|
|
In particular, theory_engine.h is included many places spuriously.
A few blocks of code changed indentation, updated to guidelines.
|
|
Work towards eliminating dependencies on quantifiers engine, this updates quantifiers module to use the standard SAT-context dependent flag in quantifiers state instead of the one in QuantifiersEngine. It also eliminates the use of a custom call to theoryEngineNeedsCheck.
|
|
This is the second prerequisite for eliminating dependencies on quantifiers engine. This PR threads a quantifiers inference manager through all modules in quantifiers that add lemmas.
The code for adding lemmas in quantifiers engine will be migrated to this class.
|
|
This is a step towards breaking up the quantifiers engine.
The key change is that QuantifiersEngine will not be passed as a pointer to the modules it contains. This PR makes it so that necessary modules take a QuantifiersState, which will eventually be extended as needed with additional query methods. For now, modules will take both until the dependencies on QuantifersEngine are removed.
This required that QuantifiersEngine now lives in TheoryQuantifiers, instead of in TheoryEngine, since the QuantifiersEngine must be initialized with QuantifiersState, which is a member of TheoryQuantifiers. Now, TheoryEngine retrieves the QuantifiersEngine from TheoryQuantifiers prior to finishing initialization on theories.
|
|
This does an intermediate refactoring of the single invocation solver to make a few things clearer and to add preliminary support for functions that have been marked as solved by external techniques.
This is in preparation for generalizing the CAV 2015 single invocation techniques.
|
|
This deletes variable flags from NodeManager::mkVar and moves ExprManager sort flags to NodeManager.
These flags are used for determining when a variable or sort should be printed via the old dump infrastructure. The old dump infrastructure is simplified in this PR accordingly.
This PR should preserve behavior of the previous dumping with a minor exception that the internal trace "declarations" will also included symbols introduced from define-fun. This will be further refactored later. This is in preparation for removing the includes expr.h/expr_manager.h from node_manager.h.
|
|
Previously we were not printing unsat cores when passing the option to dump them if we used the check-sat-assuming command or the QUERY command. This commit fixes this.
It also kills the redundant dump-synth option, as it simplifies a bit what is going on in the command executor.
|
|
This makes simplifications to the internal sygus API now that the SmtEngine interface is independent of parsing.
|
|
This is required for new work on generalizing CAV 2015 single invocation techniques.
It adds a new system of marking solutions for synthesis conjectures as attributes, which will be used as a way of eliminating functions from a conjecture while still preserving their solution in a response to check-synth.
|
|
|
|
|
|
The only code including the old API now are in parser/ and main/ which will require further untangling.
|
|
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.
|
|
|
|
(#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.
|
|
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.
|
|
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.
|
|
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.
|