| Age | Commit message (Collapse) | Author |
|---|
|
Since
https://github.com/CVC4/LFSC/commit/1d1c55fa17b08e2bc8cb686b9d07ec63bf0dd4a2
LFSC requires Flex, so we need to install the corresponding packages in
our CI environment. This commit also removes SWIG from the list of
packages to install since we do not use it anymore.
|
|
This commit updates Theory so that equality engines are allocated dynamically. The plan is to make this configurable based on the theory combination method.
The fundamental changes include:
- Add `d_equalityEngine` (raw) pointer to Theory, which is the "official" equality engine of the theory.
- Standardize methods for initializing Theory. This is now made more explicit in the documentation in theory.h, and includes a method `finishInitStandalone` for users of Theory that don't have an associated TheoryEngine.
- Refactor TheoryEngine::finishInit, including how Theory is initialized to incorporate the new policy.
- Things related to master equality engine are now specific to EqEngineManagerDistributed and hence can be removed from TheoryEngine. This will be further refactored in forthcoming PRs.
Note that the majority of changes are due to changing `d_equalityEngine.` to `d_equalityEngine->` throughout.
|
|
This updates the internal data structure for strings inferences "InferInfo" such that it is amenable to proof reconstruction.
Currently, the explanation for a conclusion is in two parts:
(1) d_ant, the antecedents that can be explained by the current equality engine,
(2) d_antn, the antecedents that cannot.
For proof reconstruction, the order of some antecedents matters. This is difficult with the above data structure since elements in these two vectors are not given an ordering relative to each other. After this PR, we store:
(1) d_ant, all antecedants, which are ordered in a way that is amenable to proofs (to be introduced on following PRs),
(2) d_noExplain, the subset of d_ant that cannot be explained by the current equality engine.
This PR modifies calls to InferenceManager in preparation for extending it with a proof reconstructor InferProofCons which will convert strings::InferInfo into instructions for building ProofNode.
|
|
A recent commit (77e9881) simplified the form of the conclusion in regular expression star unfolding for the sake of uniformity in our internal proof calculus. However, this led to a noticeable drop in performance on a few specific RE benchmarks (the Norn set). This preserves the old behavior by extending the core rule for RE unfolding.
It also makes one minor change to the strings proof checker carried over from the proof-new branch.
|
|
This PR implements a first naive way to employ the linear model (obtained from the nonlinear extension) to guide the initial sampling within the cad solver.
|
|
This includes eliminating TheoryBV's call to eqNotifyNewEqClass and fixing an issue with string's eqNotifyNewEqClass method, which was registering constant integers.
It also removes some unnecessary methods in Theory.
|
|
This changes an initialization issue in regarding PropEngine and TheoryEngine.
In the constructor for PropEngine, we convert and assert literals for true and false to CNF stream. Doing so triggers several things, including calls that preregister these literals with the associated TheoryEngine. This means that literals are preregistered to TheoryEngine before it has been fully initialized (TheoryEngine::finishInit). This is not currently an issue since this only involves modules that are constructed statically (e.g. SharedTermsDatabase), but this will lead to issues when the TheoryEngine is more configurable.
The solution is to additionally have a PropEngine::finishInit, which is called after TheoryEngine::finishInit, which does this step. The PropEngine should not assert anything to CNF before this method is called.
|
|
It also adds enumeration for two new rules that have been recently added.
|
|
Previously, there was methods for being informed just before and just after equivalence classes are merged (eqNotifyPreMerge and eqNotifyPostMerge). The purpose of this was to allow e.g. the theory to inspect the equivalence classes in question before the equality engine modified them. However this is no longer used, and moreover is discouraged since Theory should generally buffer their usage of EqualityEngine while it is making internal calls.
TheoryStrings was the only theory to use eqNotifyPreMerge (somewhat arbitrarily), all others used eqNotifyPostMerge. This makes post-merge the default, renames it to eqNotifyMerge and removes pre notifications.
This will simplify the work of the new theory combination methods as well as leading to fewer spurious calls to callbacks in equality engine.
|
|
--lang sygus is a synonym for --lang sygus2
also fixes typo in error message for language options parsing
Signed-off-by: polgreen <epolgreen@gmail.com>
|
|
This PR adds a small improvement to the CAD solver.
In Algorithm 4 of https://arxiv.org/pdf/2003.05633.pdf in lines 8 and 9, we only consider polynomials for resultant computations that have roots outside of the current interval.
This PR implements this check.
Fixes CVC4/cvc4-projects#210.
|
|
This class is responsible for maintaining TheoryEngine and PropEngine and implementing the check-sat command. It also has an interface for processing/pushing the current assertions into the PropEngine.
This class will be used directly by other extension solvers (for abduction, interpolation, qe, sygus, etc.).
|
|
There was a last minute change was a typo when merging 103b5ea .
Also the fix in that commit needed to be slightly more robust to the case when either branch of an ITE had a different sygus type.
Fixes regress1.
|
|
The commit (079a04b) appears to have broken the nightlies due to compile issues related a necessary addition to the Dump class (so that std::string could be printing on Dump streams).
This changes the temporary solution so that we simply print a string on the standard output, when the Dump is enabled. This is required for temporarily keeping dump=raw-benchmark working for synth-fun commands.
|
|
This is the first step towards making the approach for theory combination in CVC4 configurable.
This PR introduces the "distributed equality engine manager", which encapsulates the current policy that TheoryEngine uses regarding equality engines: each Theory creates a separate copy of an equality engine. The eventual plan is that the official equality engine of Theory is not necessarily unique to the theory, if equality engines are shared. A variant of this class could implement that policy.
This PR does not impact the code, it simply adds the definition of the class. A forthcoming PR will integrate this class into TheoryEngine, which will use dynamic allocation for equality engine objects.
FYI @barrettcw
|
|
MERGED_THROUGH_CONSTANTS (#4879)
|
|
Now that we are using the constant folding in equality engine for more than equality it is necessary to generalize the previously-hard-coded handling of MERGED_THROUGH_CONSTANTS.
|
|
This PR is a step towards migrating commands to the Term/Sort level. The functions for printing synth-fun command and its grammar were modified to remove their dependency on command objects and use nodes instead of exprs and types. Similar changes to other functions that print commands will follow.
|
|
Fixes #4790.
Fixes two bugs in the decision tree learning solver for sygus, one involving evaluation of "templated" enumerators, and one involving ITE strategies where child types are different than the root.
|
|
This makes it so that the explicit Kind is wrapped in a Node as an argument to the CONG proof rule. This allows us to distinguish applications with the same parameterized operator but different kinds (e.g. APPLY_SELECTOR vs APPLY_SELECTOR_TOTAL).
|
|
Adds basic support for proofs in the strings term registry. This code is not yet active until further parts of proof-new are merged.
|
|
This includes configurable naming and a caching policy for term conversion proof generator.
Also corrects a subtle issue in LazyCDProof related to making getProofFor idempotent using the notion of owned proofs.
|
|
This PR would add an option to only build the CVC4 library and not the parser or executable. This can be used for projects that only intend to use CVC4 through the API.
It seems to be working now, but it's not necessarily the cleanest solution. In particular, if you'd like the polarity to be different I'm happy to change that. Polarity meaning something like "${WITH_BINARY}" STREQUAL "YES" instead of NOT "${LIB_ONLY} STREQUAL "YES" which is admittedly a little strange.
|
|
This class is responsible for the connection between terms and their witness form in the final proof.
|
|
This PR adds naive support for integer reasoning to the CAD-based solver.
Essentially, it checks whether the sampled value is integral. If this is not the case, we "invent" a new interval covering the area between the two neighbouring integers with appropriate border polynomials.
|
|
This commit improves functionalities of the equality engine so that it is easier to produce proofs for its reasoning. They are:
avoiding assertion of already entailed predicates/equalities.
better EqProof of disequalities with constants
correct EqProof involving n-ary congruence kinds
|
|
This corrects an issue introduced by a merge of a previous commit (b5b2858) which dropped the connection from sets to its master equality engine.
Fixes several issues in sets regressions, including a timeout in regress0.
|
|
We have an open issue with an infinite loop with --ite-simp for a long time in #789 , for example on
(declare-fun a () Int)
(declare-fun b () Int)
(assert
(and
(= 1 (+ a b))
(or (= 0 a) (= 0 b))
(or (= 0 b) (>= b 8))
(or (= 0 a) (not (>= b 8)))
)
)
(check-sat)
The problem goes back to arith_ite_utils.cpp and roughly is as follows:
The method solveBinOr looks for patterns like (or (= b 0) (= b 1)). It introduces a new Boolean variable deor_1 and substitutes b -> (ite deor_1 1 0).
The method also stores another mapping in d_skolems: deor_1 -> (>= b 8) here which is also used in selectForCmp. However, these skolems are also used to add even more substitutions here after applying the already added substitutions to it. Eventually, we have a substitution deor_1 -> (>= (ite deor_1 1 0) 8) which inevitably leads to an infinite loop.
I have found no reason for the second mapping (deor_1 -> (>= b 8)) to be added as a substitution, and thus this PR removes it.
Benchmarks are running to check whether there are further issues with this, and whether this simplification is beneficial.
Fixes #789.
|
|
Fixes regress1.
|
|
This splits a utility for tracking the "basic" state of the SmtEngine. This class tracks its high-level state, including the "SMT mode", last/expected status and manages the contexts. It is not responsible more detailed state information (e.g. the assertions).
|
|
In forthcoming PRs, Theory objects will be assigned equality engine objects dynamically.
This PR prepares the theory of sets for this update, which involves refactoring of its internal members.
|
|
This includes all fixes encountered while fixing unit tests with the Term -> Node version of Datatypes in the API.
After all pending PRs are merged, the next step will be to convert the new API to use e.g. CVC4::DType instead of CVC4::Datatype everywhere.
|
|
This includes support for pedantic levels, as well as a utility for wrapping Kind in a Node (for the updated CONG rule, to be updated in a later PR).
|
|
In preparation for eliminating the Expr-level datatype.
|
|
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 further removes redundant API functions with a `const char*`
parameter. These are redundant (and can create ambiguity) since they
have `const string&` counterparts.
|
|
In some use cases (unit tests, old proofs infrastructure), we use a Theory with no associated TheoryEngine. This PR makes the Valuation class more robust to this case.
This includes making the "unevaluated kinds" a no-op in this case (this is necessary for Theory::finishInit with no TheoryEngine) and adding some assertions to cases that the Theory should never call without TheoryEngine.
This is required for a new policy for dynamically configuring equality engine infrastructure in Theory.
|
|
Includes iterators and notification callbacks. These classes will be highly relevant for planned extensions to the core theory engine infrastructure.
|
|
Towards removing the Expr-level datatype.
Moves DatatypeIndex to its own file, which is the only thing that is necessary remaining from expr/datatype.h.
Also updates the datatype kinds file in preparation for the removal.
|
|
The previously introduced action to cancel running builds is not able to
cancel builds on other branches, only on the same branch. As a consequence,
when pushing to a branch for which a PR has been submitted, builds on the
main repository are not cancelled.
This removes the cancel build. If we want behavior similar to how it was
on Travis, we need a workaround / more sophisticated solution since GH
Actions doesn't really allow / support this (due to permission issues).
|
|
This updates remaining uses of the Expr-level Datatype that are not related to their creation / memory management in ExprManager.
This required updating a unit test from Expr -> Node.
|
|
This splits a collection of utilities from SmtEngine that work in cooperation to preprocess assertions (Boolean circuit propagator, preprocessing context, process assertions, term formula removal).
It updates various interfaces in SmtEngine from Expr -> Node and simplifies SmtEngine to use this utility.
|
|
This refactors the regular expression operation class so that some of its key methods are static, so that they can used by both the regular expression solver and the strings proof checker.
Notice that many cases of regular expression unfolding are deleted by this PR, since they are unnecessary. This is due to the fact that all regular expression memberships are rewritten except those whose RHS are re.++ or re.*.
|
|
This splits all things related to storing assertions in the SmtEngine into a separate class "Assertions". It also converts the interface for its methods from Expr to Node.
|
|
We have had a few issues where essentially users misinterpreted the error message about which types of exponents are supported for (^ base exp). Given that this is rewritten to a multiplication of length exp, we only support reasonably small natural numbers.
This PR improves the error message.
Fixes #4692
|
|
Issue
When CVC4 is checking models and encounters an issue, it presents an message like this:
Internal error detectedTHEORY_ARITH has an asserted fact that the model doesn't satisfy.
Notice: there's no space between detected and THEORY_ARITH.
Resolution
This PR ensures that the error message is correctly formatted.
Signed-off-by: Andrew V. Jones andrew.jones@vector.com
|
|
This commit adds eager evaluation of string terms based on the current
context. To do so, it declares the string kinds to be "interpreted" in
the equality engine. This allows us to avoid making a series of
decisions such as:
** (= "describe" (str.substr actionName 0 8)) :DE-DECISION:
*** (= actionName "deletecertificate") :DE-DECISION:
**** (= resource_partition "aws") :DE-DECISION:
***** (= resource_region "af-south-1") :DE-DECISION:
****** (= resource_account "") :DE-DECISION:
******* (= (str.len (str.substr actionName 0 3)) 0) :DE-DECISION:
******** (= (str.len (str.substr actionName 0 4)) 0) :DE-DECISION:
********* (= (str.len (str.substr actionName 0 6)) 0) :DE-DECISION:
********** (= (str.len (str.substr actionName 0 5)) 0) :DE-DECISION:
*********** (= (str.len (str.substr actionName 0 9)) 0) :DE-DECISION:
************ (= (str.len (str.substr actionName 0 7)) 0) :DE-DECISION:
************* (= (str.len (str.substr actionName 0 10)) 0) :DE-DECISION:
************** (= (str.len (str.substr actionName 0 2)) 0) :DE-DECISION:
*************** (= (str.len (str.substr actionName 0 13)) 0) :DE-DECISION:
**************** (= (str.len (str.substr actionName 0 12)) 0) :DE-DECISION:
***************** (= (str.len resource_service) 0) :DE-DECISION:
****************** (= (str.len resource_account) 0) :DE-DECISION:
In such a case, we can detect that there is a conflict after the first
two decisions because (str.substr "deletecertificate" 0 8) is
deletece which is different from describe. The equality engine uses
the rewriter to evaluate interpreted kinds with constant arguments.
This technique leads to a significant speedup on some of the newer
Amazon benchmarks.
|
|
This PR adds dummy return statements do CadSolver in case libpoly is not available.
|
|
This fixes three issues in the getInterpolant method in the API, which was also copied to the getAbduct method:
(1) Use Node not Expr
(2) Must set up ExprManager scope
(3) The wrong solver pointer was passed to the returned term, which was causing segfaults on all abduction regressions.
We should also consider changing the interface of this method to return the term instead of a Boolean. This could be done as future work.
This fixes regress1.
|
|
|
