| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
(#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.
|
|
|
|
In current master, the following fails whenever <name> contains a /:
./configure.sh --python-bindings --name=<name>
The reason is that src/api/python/genkinds.py adds a directory to the python path while relying on the fact that the build directory is located directly under the main repo directory, which is not the case if <name> contains a /.
This PR fixes this by having cmake determine the right directory to add to the python path.
|
|
|
|
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.
|
|
|
|
|
|
Since one of the last changes to the total time collection in the driver, this collection fails when the solver terminates unexpectedly (either by a signal or an exception). This PR fixes this issue and does some cleanup along the way.
|
|
This should be the last PR before quantifiers engine will not be passed to quantifiers modules.
|
|
This PR enables us to build gtest ourselves if it is not already installed.
|
|
|
|
|
|
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.
|
|
This replaces static helpers for creating special consts with
constructors. This is in preparation for a FP literal implementation
using MPFR. In the next step, I'll introduce a FloatingPointLiteral base
class, from which the specialization FloatingPointSymFPULiteral is
derived. The MPFR implementation will also be derived from the base class.
This is in order to make unit tests that compare between the two
possible. Further, in the worst case, MPFR will have to use SymFPU for
unsupported cases (to be determined).
|
|
As title; attempts to correct #6224.
Signed-off-by: Andrew V. Jones andrewvaughanj@gmail.com
|
|
This PR refactors our first, and arguably most fragile, dependency.
Right now all dependencies need to be manually installed (by calling the appropriate contrib/get-X script). For optional dependencies, we additionally need to enable them when calling the configure script (or via ccmake).
This PR is the first step in refactoring all dependencies to be automatically build (if required) as an external project.
Note that this not only eliminates the need to call contrib scripts, but also simplifies cross compilation: as all dependencies are now built within the build folders, every build folder has its own copy which may use different toolchains.
|
|
|
|
FloatingPoint(Literal) private. (#6211)
|
|
|
|
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 PR further decouples LFSC from the remaining build system, but makes it more convenient to use at the same time.
The contrib/get-lfsc-checker script is now completely standalone and installs LFSC and the necessary signatures to deps/, as well as wrapper scripts to conveniently run lfscc from there and directly check cvc4 proofs.
The goal would be to automatically use LFSC in our regressions as well.
|
|
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 PR does some refactoring on how we handle statistics in the driver, and some minor cleanup along the way.
The SmtEngine now has dedicated statistics for the data collected within the driver and provides utility functions to set them.
The driver pushes the collected statistics to the SmtEngine instead of adding them itself to the statistics registry.
The node manager no longer holds a statistics registry (that nobody used anymore anyway)
The command executor no longer holds a pointer to the SmtEngine itself. The pointer is not necessary and seems to become stale after we call reset on the command executor (which, luckily, we don't seem to do usually)
The main motivation for this change is to make the whole statistics infrastructure private to the library and not exporting it to the outside world.
|
|
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.
|
|
This creates a central utility for managing "skolem definitions", e.g. mapping between skolems and the lemmas that define their behavior.
This utility is taken from the satRlv branch. It will also be used for the new implementation of the justification decision heuristic.
Note that this PR takes some helper functions out of term formula removal (e.g. hasSkolems) Prior to this PR, these helper functions were incorrect since term formula removal does not account for all introduced skolems. For instance, Theory::ppRewrite may introduce skolems directly. This PR consolidates these cases into the new class, which is called from PropEngine when lemmas and assertions are added. At the moment, the only use of this method is for CEGQI, which needs to do its own tracking of skolems in certain literals.
It also makes some minor reorganization to prop engine.
|
|
|
|
In rare cases, we may reuse skolems for different terms (those that are the same up to purification) due to recent changes in how skolem are generated. This guards for this case in the term formula remover, which avoids assertion failures in cd insert hash map.
Fixes #6132.
|
|
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.
|
|
After this PR, with only a few exceptions, all calls to output channel for lemmas, conflicts are made through inference manager.
This is work towards standardizing the statistics for theories.
|
|
Helps debugging model issues.
|
