summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus
AgeCommit message (Collapse)Author
2021-06-07Remove `Options::wasSetByUser()` (#6682)Gereon Kremer
This PR removes the next heavily specialized template function Options::wasSetByUser() in favor of direct access to the *WasSetByUser flags.
2021-06-02Move public wrapper functions out of options class (#6600)Gereon Kremer
This PR moves options wrapper functions out of the Options class. These wrapper functions are meant to be called by "external" code that should not access the options modules. This PR thereby significantly reduces the interface of the Options class.
2021-05-27FP: Rename FLOATINGPOINT_PLUS to FLOATINGPOINT_ADD. (#6628)Aina Niemetz
This is to make it consistent with the name of the SMT-LIB operator (fp.add).
2021-05-26 More precise includes of `Node` constants (#6617)Andres Noetzli
We store constants, e.g., BitVector and Rational, in our node infrastructure. As a result, we were indirectly including some headers in almost all files, e.g., the GMP headers. This commit changes that by forward-declaring the classes for the constants. As a result, we have to include headers like util/rational.h explicitly when we use Rational but it saves about 3 minutes in compile time (CPU time). The commit changes RoundingMode from an enum to an enum class such that it can be forward declared.
2021-05-21Update to sygus standard output for check-synth responses (#6521)Andrew Reynolds
This PR does two things: (1) It eliminates the ad-hoc implementation of printSynthSolutions and removes it from the API. Now, printing response to a check-synth command is done in a more standard way, using the API + symbol manager. This is analogous to recent refactoring to get-model. (2) It updates cvc5's output in response to check-synth to be compliant with the upcoming sygus 2.1 standard. The standard has changed slightly: responses to check-synth are now closed in parentheses, mirroring the smt2 response to get-model. It also removes the unused command GetSynthSolutionCommand.
2021-05-21BV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589)Aina Niemetz
2021-05-18Loop over terms to reconstruct instead of obligations. (#6504)Abdalrhman Mohamed
This PR modifies the rcons algorithm to loop over terms to reconstruct instead of obligations. It also modifies the Obs data structure to reflect this change. The rest of the PR is mostly updating documentation and refactoring the affected code.
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
2021-04-28Remove exception headers from options.h (#6456)Gereon Kremer
This PR removes two headers for exceptions from options.h, and instead pushes the includes to a couple of source files.
2021-04-26First part of options refactoring (#6428)Gereon Kremer
This PR does a first round of refactoring and gets rid of a significant portion of generated code. In particular - it removes options::optionName.wasSetByUser() (we still have Options::wasSetByUser()) - it removes options::optionName.set() (we still have Options::set()) - it removes options::optionName.getName() in favor of options::optionName.name - it removes the specializations of Options::assign() and Options::assignBool() from the headers - it eliminates runHandlerAndPredicates() and runBoolPredicates() The removed methods are only used in few places with are changed to using Options::current().X() instead. In the future, we also want to get rid of options::optionName() and use Options::operator[]() instead, and furthermore not use Options::current() but use the options from the Env object. This PR already adds Env::getOption() as a shorthand for Env::getOptions()[...] and uses it as a proof of concept within SmtEngine.
2021-04-25Use fast enumeration by default for Boolean predicate synthesis (#6440)Andrew Reynolds
This updates the policy of when to apply smart enumeration: we do so if the grammar has ITE or admits Boolean connective terms. Previously, we applied smart enumeration for ITE and all Boolean grammars. However, this is misguided since e.g. partial evaluation unfolding has no opportunity to be effective if the enumerated terms are only Boolean literals. This significantly improves run time on a challenge benchmark from @makaimann.
2021-04-14Refactor / reimplement statistics (#6162)Gereon Kremer
This PR refactors how we collect statistics. It splits the current statistic values into the values and a proxy object. The actual values now live inside the registry (making the ownership model way easier) while the proxy object are handed to whoever wants to collect a new statistic. It also extends the C++ API to obtain and inspect the statistics. To change the ownership, this PR needs to touch every single statistic in the whole codebase and change how it is registered.
2021-04-14Rename public and private headers in src/include. (#6352)Aina Niemetz
2021-04-14Merge equivalent sub-obligations instead of discarding them. (#6353)Abdalrhman Mohamed
This PR modifies the behavior of the reconstruction algorithm when the term to reconstruct contains two or more equivalent sub-terms, but one is easier to reconstruct than the others. Since we do not know which one is easier to reconstruct by matching, we match against all sub-terms. If a solution is found for one sub-term, we use it to solve the others.
2021-04-14Warn about infeasible SyGuS conjectures (#6345)Andrew Reynolds
2021-04-13Avoid using substitute's input cache after the method call. (#6328)Abdalrhman Mohamed
As it traverses a node, Node::substitute populates its input cache with TNodes that are not preserved by the SygusReconstruct module and maybe destroyed after the method call. This PR fixes a bug where those unsafe TNodes are referenced throughout the module by passing the method a temporary copy of the cache instead.
2021-04-12Fix computation of whether a type is finite (#6312)Andrew Reynolds
This PR generalizes TypeNode::isFinite / TypeNode::isInterpretedFinite with TypeNode::getCardinalityClass. It then uses this method to fix our computation of when a type should be treated as finite. Fixes #4260, fixes #6100 (that benchmark now says unknown without an error).
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-09Rename CVC4_ macros to CVC5_. (#6327)Aina Niemetz
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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback