| Age | Commit message (Collapse) | Author |
|---|
|
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 utility will be used to track pools for pool-based instantiation.
|
|
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.
|
|
Currently, NodeBuilder takes a single template argument: An integer
that determines the expected number of arguments. This argument is used
to determine the size of the d_inlineNvChildSpace array. This array is
used to construct nodes inline. The advantage of this is that we don't
have to allocate a NodeValue on the heap for the node under
construction until we are sure that the node is new. While templating
the array size may save some stack space (or avoid a heap allocation if
we statically know that we a fixed number of children and that number is
greater than 10), it complicates the code and leads to longer compile
times. Thus, this commit removes the template argument and moves some of
the NodeBuilder code to a source file for faster compilation.
CPU build time before change (debug build): 2429.68s
CPU build time after change (debug build): 2228.44s
Signed-off-by: Andres Noetzli noetzli@amazon.com
|
|
Each theory has its own proof checker, responsible for checking the rules pertaining to that theory. The main proof checker uses these specialized checkers. Previously the main proof checker (of the proof node manager used across the SMT solver) was connected to these theory proof checkers during initialization of the theory. This commit adds an interface to the theories for retrieving its proof checker (analogous to how one retrieves the rewriter of a theory) which is used by a new method in the theory engine to register a theory proof checker to a given proof checker according to a theory id.
This is in preparation for the new unsat cores based on proofs.
|
|
|
|
|
|
(#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.
|
|
We require tracking of instantiation lemmas for quantifier elimination. Recently, this feature was removed in favor of reconstructing instantiations via substitutions. This does not quite work if instantiation lemmas have more complex post-processing, e.g. virtual term substitution.
This PR reimplements a much simpler form of instantiation tracking that simply adds instantiation bodies to a vector, per quantified formula. It uses this vector for quantifier elimination.
Fixes #5899.
|
|
pool-based instantiation (#6234)
This is in preparation for a new pool-based instantiation technique.
|
|
This should be the last PR before quantifiers engine will not be passed to quantifiers modules.
|
|
|
|
This also makes minor updates to how term tuple enumerators are constructed.
|
|
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 centralizes our utilities for generating triggers. It also splits the statistics class from quantifiers off from quantifiers engine.
|
|
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.
|
|
Model is now nested into term registry.
This PR also resolves some complications due to namespaces within quantifiers.
|
|
|
|
This PR replaces the old algorithm for reconstructing sygus terms with a new "proper" implementation.
|
|
After this PR, utilities for instantiation are available from the quantifiers inference manager instead of quantifiers engine. This means that the majority of the dependencies on quantifiers engine will (finally) start being cleaned up after this PR.
|
|
This simplifies the initialization of quantifiers engine.
This PR also makes general improvements to EqualityQuery.
|
|
This is in preparation for breaking several circular dependencies and moving
the instantiate utility into the theory inference manager.
|
|
|
|
This also moves some methods from TermEnumeration to QuantifiersBoundInference.
This is required for breaking several cyclic dependencies within quantifiers.
|
|
|
|
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 a first round of refactoring on the statistics, in particular the Stat class and derived classes.
It significantly shrinks the class hierarchy, modernizes some code (e.g. use std::chrono instead of clock_gettime), removes unused features (e.g. nesting of statistics) and does some general cleanup and consolidation.
Subsequent PRs are planned to change the ownership model (right now every module owns the Stat object) which makes the whole register / unregister mechanism obsolete.
|
|
|
|
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 also renames metakind::getLowerBoundForKind and
metakind::getUpperBoundForKind for consistency.
Note that the NodeManager class needs to be reordered to comply to our
style guidelines. This PR does not reorder but introduces a public block
at the top (where the rest of the public interface of the class should
go eventually).
|
|
calculus (#6051)
This makes a simplification to the internal proof calculus. In particular, purification skolems are no longer are special case of witness skolems. They are now independent concepts. The concept of "witness form" is replaced in most places by "original form".
This is required for fixing two issues:
(1) variable shadowing issues in skolemization.
(2) bookkeeping issues for bound variables introduced to construct witness terms. This made the LFSC proof conversion extremely cumbersome for e.g. string reductions.
In this PR, the main changes:
The internals of SkolemManager are changed to use original form vs witness form when necessary. This eliminates the need to do variable renaming in SkolemManager::skolemize.
the rule WITNESS_INTRO is replaced by SKOLEM_INTRO
MACRO_SR_* rules use original form
Proof post processing is simplified
These changes imply that ppRewrite should not return WITNESS terms. Followup PRs will modify arithmetic preprocessing so that its ppRewrite method returns skolems instead.
|
|
This PR does some more cleanup of the includes.
|
|
|
|
Fixes #5922. We were not correctly handling when a Boolean bound variable was negated.
|
|
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 commit adds support for cross-compiling for aarch64 platforms and simplifies cross-compilation handling for Windows. The configure script now automatically downloads and cross-compiles the required dependencies ANTLR3 and GMP when passing option --arm64 or --win64.
Fixes #1479 #5769.
|
|
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.
|
|
|
|
In preparation for refactoring E-matching to not pass QuantifiersEngine pointer to its utilities.
|
|
This eliminates the need for direct references to TheoryEngine from quantifiers and UF+cardinality.
This PR also eliminates an unnecessary reference to TheoryEngine in TheoryModelBuilder and breaks a few more dependencies in quantifiers modules.
|
|
This makes enumerative instantiation generalize the failures in Instantiate::addInstantiate and increment its enumeration accordingly.
This leads to (+104-6) using enumerative instantiation only on SMT-LIB quantified benchmarks, 60 second timeout.
This is in preparation for further improvements to enumerative instantiation.
|
