summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus
AgeCommit message (Collapse)Author
2021-04-09Rename CVC4__ header guards to CVC5__. (#6326)Aina Niemetz
2021-04-08Add identifiers for sources of incompleteness (#6311)Andrew Reynolds
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.
2021-04-08Initial support for parametric datatypes in sygus (#6304)Andrew Reynolds
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.
2021-04-07Fixes for abducts (#6279)Andrew Reynolds
Fixes benchmarks 2 and 3 from #5848.
2021-04-07Replace calls to NodeManager::mkSkolem with SkolemManager::mkDummySkolem (#6291)Andrew Reynolds
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.
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-31Eliminate dependencies on quantifiers engine in internal quantifiers code ↵Andrew Reynolds
(#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.
2021-03-30Miscellaneous elimination of dependencies on quantifiers engine (#6238)Andrew Reynolds
This should be the last PR before quantifiers engine will not be passed to quantifiers modules.
2021-03-29Eliminate the use of quantifiers engine in sygus solver (#6232)Andrew Reynolds
2021-03-29Move decision manager into theory inference manager (#6231)Andrew Reynolds
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.
2021-03-26Pass term registry to quantifiers modules (#6216)Andrew Reynolds
2021-03-25Add missing includes. (#6207)Gereon Kremer
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.
2021-03-24Use inference manager to access intantiate utility instead of quantifiers ↵Andrew Reynolds
engine (#6198) Towards breaking dependencies on quantifers engine.
2021-03-23Remove internal includes of Api header. (#6193)Aina Niemetz
2021-03-23Replace old sygus term reconstruction algorithm with a new one. (#5779)Abdalrhman Mohamed
This PR replaces the old algorithm for reconstructing sygus terms with a new "proper" implementation.
2021-03-15Reorganizing initialization of term registry in quantifiers (#6127)Andrew Reynolds
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.
2021-03-11Delete Expr layer. (#6117)Aina Niemetz
2021-03-09Some more cleanup of includes (#6083)Gereon Kremer
This PR does some more cleanup of the includes.
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-05Remove partial UDIV/UREM operators. (#6069)Mathias Preiner
This commit removes the partial UDIV/UREM operator handling. BITVECTOR_UDIV and BITVECTOR_UREM are now total.
2021-03-03More cleanup of includes to reduce compilation times (#6037)Gereon Kremer
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.
2021-03-03Remove uses of SExpr class. (#6035)Abdalrhman Mohamed
This PR is a step towards removing SExpr class. It replaces SExpr with std::string for set-info and set-option commands.
2021-03-02Introduce quantifiers term registry (#5983)Andrew Reynolds
This groups utilities related to ground terms into TermRegistry which will be passed to quantifier modules.
2021-03-02Clean up includes to reduce compile times (#6031)Gereon Kremer
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.
2021-02-22Eliminate raw use of output channel and valuation in quantifiers (#5933)Andrew Reynolds
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.
2021-02-22Move quantifiers attributes to quantifiers registry (#5929)Andrew Reynolds
This moves the utility class beneath quantifiers registry.
2021-02-17Eliminate non-static members in term util (#5919)Andrew Reynolds
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.
2021-02-17Move methods from term util to quantifiers registry (#5916)Andrew Reynolds
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.
2021-02-17Add InferenceId to buffered inference manager (#5911)Gereon Kremer
This PR collects the InferenceId in the InferenceManagerBuffered class.
2021-02-08Use quantifiers inference manager for lemma management (#5867)Andrew Reynolds
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.
2021-02-04Introduce quantifiers registry utility (#5829)Andrew Reynolds
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.
2021-02-02Cleanup some includes (#5847)Andrew Reynolds
In particular, theory_engine.h is included many places spuriously. A few blocks of code changed indentation, updated to guidelines.
2021-01-26Use standard conflict mechanism in quantifiers state (#5822)Andrew Reynolds
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.
2021-01-26Introduce quantifiers inference manager (#5821)Andrew Reynolds
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.
2021-01-26Refactor quantifiers engine initialization (#5813)Andrew Reynolds
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.
2021-01-20Refactoring the single invocation solver (#5706)Andrew Reynolds
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.
2021-01-11Further simplifications in preparation for removing Expr layer (#5756)Andrew Reynolds
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.
2020-12-23Dumping unsat cores after check-sat-assuming/QUERY (#5724)Haniel Barbosa
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.
2020-12-18Simplify internal API for sygus (#5687)Andrew Reynolds
This makes simplifications to the internal sygus API now that the SmtEngine interface is independent of parsing.
2020-12-15Consolidate basic sygus utilities regarding sygus conjectures (#5421)Andrew Reynolds
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.
2020-12-09Fixed a bunch of clang warnings. (#5637)Gereon Kremer
2020-12-02Update copyright headers.Aina Niemetz
2020-11-30Remove includes for old API from internal code (#5536)Andrew Reynolds
The only code including the old API now are in parser/ and main/ which will require further untangling.
2020-11-23Fix for sygusToBuiltinEval for non-ground composite terms (#5466)Andrew Reynolds
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.
2020-11-20RoundingMode: Rename enum values to conform to code style guidelines. (#5494)Aina Niemetz
2020-11-19Enable new implementation of CEGQI based on nested quantifier elimination ↵Andrew Reynolds
(#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.
2020-11-12Simplify sygus solver and sygus stream (#5389)Andrew Reynolds
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.
2020-11-12Fix redundant refinement lemma in sygus solver (#5399)Andrew Reynolds
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.
2020-11-05Split sygus template inference to its own file (#5388)Andrew Reynolds
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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback