| Age | Commit message (Collapse) | Author |
|---|
|
This replaces a bunch of static accesses to options (`options::foo()`) by using the `EnvObj::options()` method.
|
|
This makes relational triggers its own kind of instantiation match generator. Future PRs will delete the code interleaved in the core InstMatchGenerator class for handling relational triggers.
This PR also fixes two issues related to how trigger techniques are combined:
(1) instantiation match generators that are generated as part of multi-triggers now are properly specialized (using getInstMatchGenerator),
(2) there was a bug with auto-generated triggers: when the first auto-generated trigger was generated that was already a user trigger, then we would ignore all other auto-generated triggers.
This is work towards finding a solution for the choice.move.hard Facebook benchmark, where relational-triggers appear to be a possible solution.
|
|
Towards addressing some bottlenecks on Facebook benchmarks.
|
|
|
|
This PR removes a bunch of static accesses in places where EnvObj is used now, and we can thus use options().
|
|
This changes the attribute on internally generated bounded quantified formulas from `isInternal` to `isQuantBounded`. This makes it clear that bounded integers is the module that should process them. It also moves the utility for constructing these quantified formulas from strings to BoundedIntegers itself. This is to accommodate other theories, e.g. bags, that may make use of reductions to bounded quantifiers.
|
|
This is in preparation for renaming SmtEngine to SolverEngine.
|
|
This PR eliminates the Output macro together with the associated output stream (stored in a static variable). It is replaces by a set of simple utility functions of the Env class, and we instead use the output stream from options.base.out.
To achieve this, a couple of quantifier classes are now derived from EnvObj.
|
|
This makes the evaluator accessible via EnvObj through the Rewriter. It furthermore removes Rewriter::rewrite from inside the evaluator itself.
Construction of Evaluator utilities is now discouraged.
The include dependencies were cleaned slightly in this PR, leading to more precise includes throughout.
This is work towards having a configurable cardinality for strings, as well as eliminating SmtEngineScope.
|
|
|
|
|
|
This commit removes TheoryState::options() by changing more classes to
EnvObjs.
|
|
This eliminates another call to currentSmtEngine.
After this, there are only two remaining calls (one for normalizing sygus grammars wrt user define-funs, and the other for Rewriter::rewrite).
|
|
This splits higher-order term database as a derived class of term database, thus separating higher-order specific things out of our core term database.
This eliminates many of the references to the deprecated option uf-ho.
This is work towards eliminating that option.
|
|
Our policy is now accurate to the help message on prenexUserQuant: we only prenex quantified formulas if they do not have user-provided patterns. Previously we also did not prenex any quantified formulas with any annotations.
This should avoid some more "unknown" responses on facebook benchmarks.
Also fixes a minor issue with when we print warnings about quantified formulas with no triggers.
FYI @barrettcw .
|
|
PR #7017 fixed the policy for eliminating quantifiers but introduced
some minor issues, which this commit fixes:
the InstantiationEngine::checkOwnership() method was changed to look
for patterns in the wrong node.
the PR changed the modes of the --user-pat=MODE method but reused
one of the names. This commit fixes the name and adds a check in the
options script.
fixing the policy caused cvc5 to answer unsat instead of the
expected unknown for regress0/use_approx/bug812_approx.smt2. The
commit updates the expected result.
|
|
This also consolidates the option strictTriggers into userPatMode.
Fixes #6996.
|
|
This complete the implementation of dump-instantiations-debug.
With this option, we can print the source of instantiations. For example:
$ cvc5 regress1/quantifiers/dump-inst-proof.smt2 --dump-instantiations-debug --produce-proofs
unsat
(instantiations (forall ((x Int)) (or (P x) (Q x)))
(! ( 2 ) :source QUANTIFIERS_INST_E_MATCHING_SIMPLE ((not (= (P x) true))))
)
(instantiations (forall ((x Int)) (or (not (S x)) (not (Q x))))
(! ( 2 ) :source QUANTIFIERS_INST_E_MATCHING_SIMPLE ((not (= (S x) false))))
)
|
|
The only remaining unknown inferences covered by our regressions are from the sygus solver, will address in later PR.
|
|
This adds optional arguments to INSTANTIATE steps in proofs to track fine-grained reasons for relevant instantiations.
Also simplifies an old argument modEq which was unused.
FYI @MikolasJanota
|
|
Fixes #6259.
|
|
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.
|
|
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
|
|
This removes the expandOnly flag from expandDefinitions.
The use of expandOnly = true is equivalent to applying top-level substitutions only, which should be done explicitly via Env::getTopLevelSubstitutions. It updates the trust substitutions utility to distinguish apply vs applyTrusted for convenience for this purpose.
This also breaks several dependencies in e.g. expand definitions module.
|
|
Fixes #6495.
|
|
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.
|
|
|
|
|
|
|
|
|
|
|
|
(#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.
|
|
Towards having complete stats on inference ids for each lemma, fact, and conflict.
|
|
This should be the last PR before quantifiers engine will not be passed to quantifiers modules.
|
|
|
|
This PR centralizes our utilities for generating triggers. It also splits the statistics class from quantifiers off from quantifiers engine.
|
|
engine (#6198)
Towards breaking dependencies on quantifers engine.
|
|
Model is now nested into term registry.
This PR also resolves some complications due to namespaces within quantifiers.
|
|
This simplifies the initialization of quantifiers engine.
This PR also makes general improvements to EqualityQuery.
|
|
|
|
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 makes quantifiers use standard inference ids.
This eliminates the need to track ad-hoc statistics, per instantiation type.
This makes minor modifications to a few interfaces in quantifiers to enable this.
|
|
This PR does some more cleanup of the includes.
|
|
|
|
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.
|
|
|
|
In preparation for refactoring E-matching to not pass QuantifiersEngine pointer to its utilities.
|
|
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.
|
