| 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.
|
|
If the user manually disables ho-extensionality via expert option --no-uf-ho-ext, we should answer "unknown" instead of "sat" when applicable.
Fixes #4318.
|
|
Fixes benchmarks 2 and 3 from #5848.
|
|
Previously, we were traversing proof node as a tree, now we use a dag traversal.
This also makes sure that proofs work when we have a external proof conversion and we are in incremental mode. In such cases, the final proof must be cloned to ensure that we do not overwrite proof nodes, which may be reused across multiple check-sat.
|
|
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
|
|
Fixes #4370.
|
|
Fixes #4179.
|
|
|
|
Fixes #6271.
This was triggered by recent fixes, this fixes solution soundness issues with symbolic regular expressions due to spuriously included antecedants, which made lemmas SAT-context dependent while being cached as user-context dependent.
|
|
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.
|
|
We were getting types for set singleton/membership in a way that was unsafe for subtyping, which was leading to incorrectly computing care graphs for sets of reals.
Fixes #5705.
|
|
This PR introduces the notion of a "skolem function" to SkolemManager, which is implemented as a simple cache of canonical skolem functions/variables.
This is a prerequisite for two things:
(1) Making progress on the LFSC proof conversion, which currently is cumbersome for skolems corresponding to regular expression unfolding.
(2) Cleaning up singletons. Having the ability make canonical skolem functions in skolem manager will enable Theory::expandDefinitions to move to TheoryRewriter::expandDefinitions. This will then enable removal of calls to SmtEngine::expandDefinitions.
This PR also makes arithmetic make use of this functionality already.
The next steps will be to clean up all raw uses of NodeManager::mkSkolem, especially for other theories that manually track allocated skolem functions.
|
|
Fixes the first benchmark from #6203.
|
|
An RE unfolding lemma may rewrite to true for tautological RE memberships that our rewriter does not rewrite the membership to true.
An example is (str.in_re x (re.* (re.union (str.to_re "A") (str.to_re x))).
This PR ensures we are robust to these cases.
This fixes benchmarks 3-5 from #6203. Benchmark 3 is added here, 4-5 time out.
|
|
This ensures that we always cache regular expressions in a user-dependent manner. Previously, we were erroneously caching in a SAT-dependent way for very rare cases when non-constant regular expressions were used. Since we never dependent on current assertions for the unfolding, there is no need to cache in the SAT context.
This fixes the second benchmark from #6203.
This PR also improves our traces for checking models in strings.
|
|
This fixes the type rule for to_real to match SMT-LIB: its argument must be an integer.
This required fixing the TPTP parser which has a more relaxed semantics for to_real / to_rat.
This also fixes Solver::isReal, which should return false if we are the integer type.
Fixes #6208.
|
|
|
|
|
|
|
|
As a result of this issue, currently we are incorrectly trying to repair a model when one is not guaranteed to exist, leading to a spurious assertion failure.
Fixes #6228. The benchmarks on that issue now answer "unknown" without an assertion failure.
|
|
|
|
|
|
(#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.
|
|
|
|
Currently, SEXPR applications are given a parametric type SEXPR_TYPE applied to the types of its arguments. This means that SEXPR that are type checked consume roughly double the memory. This issue arises in practice when printing proofs in the internal calculus.
There is no need to have SEXPR_TYPE as a parametric type, this PR makes SEXPR simply typed.
Also moves some implementation of TypeNode methods to type_node.cpp.
|
|
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 introduces the header file for a more modular bv-to-int module, that will be called from the preprocessing pass bv-to-int, and possibly from the bit-vector solver after preprocessing.
The header file is basically a copy of the bv_to_int.h header file from preprocessing, with some adjustments to increase modularity.
In addition to the header file we also introduce an empty unit test that #includes the header, in order to identify compilation errors. The unit test will be populated in subsequent PRs, that will also include implementations.
|
|
|
|
In certain cases, the nonlinear extension would not re-check properly but only repeat an (already failed) model repair. The result lemma would then already be in cache and thus not be sent to the solver.
This PR ensures that modelBasedRefinement is always run and entirely removes the d_builtModel flag that was responsible for this behavior. Additionally, it asserts that the lemma that (tries to) force the model to be reconciled during theory combination is actually sent.
Fixes #6192.
|
|
This pushes all symfpu specific parts from FloatingPoint into
FloatingPointLiteral. FloatingPoint is now generic. An additional
FloatingPointLiteral implementation using MPFR will be made configurable
similiarly to how we handle Integers with either GMP or CLN backend.
|
|
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.
|
|
Linear arithmetic simply tried to branch on the first integer variable that had a non-integral assignment.
If it holds stale variables that are not part of the current input, these branches can be emitted and are processed by the solver, but the resulting new assertions will not be considered relevant and thus not added to the theory.
As it still triggers a new theory check, linear arithmetic repeats the same procedure and causes an infinite loop.
This PR explicitly tracks the currently relevant nodes by storing all preregistered nodes and only allows branching on variables from this set.
Fixes #6146.
|
|
This is leftover from a previous way of eliminating extended operators
|
|
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 eliminates one of the dependencies of TypeNode on options. In particular, this makes it so that function types are always considered first-class.
This change makes it so that higher-order types can always be constructed; logic exceptions should occur if they are used in constraints.
|
|
String terms may enter into the equality engine without appearing in assertions, due to eager context-dependent simplification internal to the equality engine (--strings-eager-eval). In rare cases, we did not catch when a new string constant appeared in the equality engine, meaning it would not be marked as relevant leading to bogus models in incremental mode.
This makes it so that proxy variables are stored in a user-context dependent manner, which impacts when terms marked as having a proxy variable are registered.
The PR also simplifies our policies for when string terms are registered slightly.
Fixes #6072.
|
