| Age | Commit message (Collapse) | Author |
|---|
|
This renames everything but GitHub links and build system related
macros. Switching the build system to cvc5 will be the last step in the
renaming process.
|
|
Adds an instantiation strategy based on user-provided pool annotations.
The next PR will connect this to quantifiers engine.
|
|
Refactoring out the code from `inst_strategy_enumerative` into a separate
class. Some additional tricks to avoid duplicate instantiations, most
notably, before instantiation, a tuple is checked if it's not a
super-tuple of some tuple that had earlier resulted in a useless
instantiation.
Signed-off-by: mikolas <mikolas.janota@gmail.com>
|
|
This was used in the old method for unsat core tracking for instantiation lemmas, which will soon be subsumed.
This is also work towards eliminating the dependencies on quantifiers engine from Instantiate.
|
|
This makes the terms registered to the term database (those considered by E-matching) optionally stored in a SAT-context-dependent manner. The motivation is to have a more flexible/fine-grained set of terms considered by E-matching, e.g. if preregistration becomes lazier in the future.
This uncovered 2 issues:
The induction techniques in "conjecture generator" were using private interfaces, this PR removes the friend relaionship and cleans the code
The conflict-based instantiation module was accessing the signature tables for BOUND_VARIABLES when an operator of an APPLY_UF was a BOUND_VARIABLE. This is possible when options::ufHo is enabled. This makes conflict-based instantiation skip such terms.
|
|
This was a feature implemented for "Deciding Local Theory Extensions via E-matching" CAV 2015 that is not used anymore, and will be a burden to maintain further with potential changes to term database.
It also simplifies the TermDatabase::addTerm method (which changed indentation).
|
|
(#5814)
This makes printing instantiations done at the SmtEngine level instead of deeply embedded within the Instantiate module. This provides much better flexibility for future uses of instantiations (e.g. how they are minimized in the new proof infrastructure).
Note this PR breaks the functionality that instantiations are minimized based on the old unsat cores infrastructure (see the disabled regression). This will be fixed once proof-new is fully merged.
|
|
|
|
In preparation for splitting trigger.h/cpp into multiple files.
This updates the code to conform to guidelines. No major changes, apart from a heuristic related to "pure theory triggers" is deleted and simplified.
|
|
This was an experimental option used in combination with separation logic.
|
|
This was a hack to improve the QF arithmetic solver by ensuring that certain instantiation lemmas were preregistered. This is no longer needed and will be a hindrance to the currently line of refactoring.
|
|
This ensures that datatype selectors are properly handled as triggers in E-matching.
This is challenging since selectors in quantified formulas are of kind APPLY_SELECTOR but are theory-preprocessed to APPLY_SELECTOR_TOTAL/APPLY_UF. Hence, we must match on 2 possible operators, and ones that do not match the operator of the trigger. This adds a custom candidate generator for this case.
It also removes a deprecated option that is no longer used (in part due to our use of shared selectors).
This is in preparation for further work on optimizing cvc4 on benchmarks from Facebook.
Note that there is not a convienient way to call expandDefinitions currently (which is required to get the proper operators to match). This PR calls smt::getCurrentSmtEngine() to do this, although we should find a better solution soon, e.g. adding expandDefinitions to the rewriter.
FYI @barrettcw
|
|
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.
|
|
This PR adds three instantiation modes to the SyGuS instantiation module.
|
|
This makes it so that an "unknown" response in a CEGIS verification step causes the sygus solver to exclude the current solution and mark incomplete. Previously, the sygus solver was non-terminating in such cases, trying the same solution continously.
This also removes the option "sygusVerifySubcall", as this option should always be used. It also makes --nl-ext-tplanes enabled by default when sygus is enabled.
|
|
This PR adds options to add additional ground terms to the SyGuS instantiation grammars.
|
|
This was an option that rejected instantiations that are true according to the current
model's equality engine.
This option was never helpful and will be burdensome to maintain with new updates
to equality engine infrastructure.
|
|
This prints # instantiations per round (during solving) for each quantified formula with `--debug-inst`, giving output like this:
```
(num-instantiations myQuant1 1)
(num-instantiations myQuant2 1)
unsat
```
It also changes the default value of print-inst-full to match the behavior of unsat-cores vs unsat-cores-full (by default, nameless quantifiers are ignored).
It fixes an issue with qid, where mkVar was accidentally used instead of mkConst, leading to assertion failures in debug. Marking major since this fixes debug regress1.
|
|
This makes an option --debug-sygus available to the user for tracing the sygus solver. For the classic max2 example the option is:
(sygus-enum 0)
(sygus-candidate (max 0))
(sygus-enum 0)
(sygus-enum 1)
(sygus-enum x)
(sygus-enum x)
(sygus-candidate (max x))
(sygus-enum x)
(sygus-enum y)
(sygus-enum y)
(sygus-candidate (max y))
(sygus-enum y)
(sygus-enum (+ x x))
(sygus-enum (+ x 1))
(sygus-enum (+ 1 1))
...
(sygus-enum (ite (<= x y) y 1))
(sygus-candidate (max (ite (<= x y) y 1)))
(sygus-enum (ite (<= x y) y 1))
(sygus-enum (ite (<= x y) y x))
(sygus-enum (ite (<= x y) y x))
(sygus-enum (ite (<= x y) y x))
(sygus-candidate (max (ite (<= x y) y x)))
unsat
(define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
Where sygus-enum denotes enumerated terms and sygus-candidate is one that passes a CEGIS refinement check.
|
|
This adds a new print format for instantiations --print-instantiations=num, which prints the total number of instantations of quantified formulas. This count is user-context-dependent, which is in sync with the existing print-instantiation format (list).
It also simplifies and improves printing of Instantiation Tries.
|
|
This PR decouples Options from NodeManager. Instead, options now live in SmtEngine.
The changes that were required for this PR include:
The main internal options object is now owned by SmtEngine instead of ExprManager.
The ownership resource manager is moved from NodeManager to SmtEngine.
Node manager listeners are deleted, timeouts and resource limits are set during SmtEngine::finishInit.
A temporary hack was added to make the last constructed SmtEngine to be the one in scope. This ensures that options are in scope whenever an SmtEngine is created.
The methods for invoking "subsolvers" (theory/smt_engine_subsolver.h,cpp) was simplified, as versions of these calls that change options do not have to clone a new copy of the ExprManager anymore.
Resource manager was removed from the smt2 parser.
Minor refactoring was done in SmtEngine to copy "original options" so that options are restored to their state after parsing command line options on reset.
Updates to unit tests to ensure conformance to new options scoping.
|
|
Previously, we used a specialized variant of prenex normal form that allowed top level disjunctions. However, the method to put quantifiers into this form led to variable shadowing on some benchmarks in SMT-LIB LRA.
This simplifies the code so that we use standard prenex normal form when cegqi-nested-qe is used and deletes the old variant (DISJ_NORMAL).
|
|
|
|
This updates option names to be consistent across uses of counterexample-guided quantifier instantiation (ceqgi), which was previously called "counterexample-based quantifier instantiation" (cbqi), and sygus.
Notably, the trace "cegqi-engine" is changed to "sygus-engine" by this commit.
The changes were done by these commands in the given directories:
src/:
for f in $(find -name '.'); do sed -i 's/options::cbqi/options::cegqi/g' $f;sed -i 's/cegqi-engine/sygus-engine/g' $f; done;sed -i 's/"cbqi/"cegqi/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/--cbqi/--cegqi/g' $f; done
src/: and test/regress/:
for f in $(find -name '.'); do sed -i 's/cegqi-si/sygus-si/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/no-cbqi/no-cegqi/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/:cbqi/:cegqi/g' $f; done
And a few minor fixes afterwards.
This should be merged close to the time of the next stable release.
|
|
|
|
These options are not robust and are not used.
Fixes #4282 and fixes #4291.
|
|
Fixes #4105.
It appears that the two (experimental) options in that issue were incompatible.
A block of code changed indentation in this PR and was updated to guidelines.
|
|
|
|
This option was unimplemented and was equivalent to setting the instantiation level of all quantified formulas to 0.
|
|
Fixes #4019.
This feature was never fully implemented.
|
|
This option enables the sygus solver (previous name was ceGuidedInst, deprecated from CAV 15 specific approach).
It also improves when this option is set. In particular we ensure it is enabled when sygus is enabled for any reason.
|
|
(#3841)
Fixes #3839.
Previously, the quantifiers rewriter had a rewriting step that was an ad-hoc version of some of the rewrites that have been incorporated into the extended rewriter. Moreover, the code for that pass was buggy.
This eliminates the previous conditional rewriting step from the "term process" rewrite pass in quantifiers. It additional adds an optional (disabled by default) rewriting pass that calls the extended rewriter on the body of quantified formulas. This subsumes the previous behavior and should not be buggy.
Notice that the indentation in computeProcessTerms changed and subsequently has been updated to the new coding standards.
This PR relies on #3840.
|
|
|
|
|
|
|
|
This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
