| Age | Commit message (Collapse) | Author |
|---|
|
For now we do not enable unconstrained simplification when arithmetic is present. Post SMT COMP, we should investigate making arithmetic not output lemmas during preprocessing (CVC4/cvc4-wishues#71).
|
|
This also updates the SMT COMP script to revert to our previous behavior.
This is required for SMT COMP. It should be beneficial for satisfiable QF_NIA instances. I will revisit/test this independently.
|
|
This updates option names to be consistent across uses of counterexample-guided quantifier instantiation (ceqgi), which was previously called "counterexample-based quantifier instantiation" (cbqi), and sygus.
Notably, the trace "cegqi-engine" is changed to "sygus-engine" by this commit.
The changes were done by these commands in the given directories:
src/:
for f in $(find -name '.'); do sed -i 's/options::cbqi/options::cegqi/g' $f;sed -i 's/cegqi-engine/sygus-engine/g' $f; done;sed -i 's/"cbqi/"cegqi/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/--cbqi/--cegqi/g' $f; done
src/: and test/regress/:
for f in $(find -name '.'); do sed -i 's/cegqi-si/sygus-si/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/no-cbqi/no-cegqi/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/:cbqi/:cegqi/g' $f; done
And a few minor fixes afterwards.
This should be merged close to the time of the next stable release.
|
|
|
|
Fixes #4277.
|
|
Fixes #4243.
|
|
Fixes #4160.
|
|
This is a step towards refactoring the SmtEngine. It splits several core components of SmtEnginePrivate to its own independent module, ProcessAssertions which is responsible for applying preprocessing passes , simplification and expand definitions.
The main change involved moving these functions from SmtEnginePrivate to this new class. A few other minor changes were done to make this move:
A few things changed order within processAssertions to allow SmtEnginePrivate-specific things to happen outside of the main scope of processAssertions.
processAssertions had some logic to catch incompatible options and silently disable options. This was moved to setDefaults.
A few data members in SmtEngine were moved to ProcessAssertions.
Two utilities that were sitting in smt_engine.cpp were moved to their own files.
Another refactoring step will be to make ProcessAssertions take only the utilities it needs instead of taking a SmtEngine reference. This requires further detangling of Options.
|
|
Fixes #3971 and fixes #3991. In incremental mode, the logic can change from one
(check-sat) call to another. In the reported issue, we start with QF_NIA
but then switch to QF_UFNIA because there is a div term (which has a UF in
its expanded form). Dealing with this issue is challenging in general. As a
result, we have decided not to allow theory widening in
Theory::expandDefinitions() anymore but instead to do it eagerly in
SmtEngine::setDefaults().
|
|
This includes:
All options pertaining to SMTEngine are now handled at the top of setDefaults.
smtlibStrict was deleted in favor of a script.
statsEveryQuery enables stats by modifying a public option function. This is a slight hack but this code will likely get refactored as well soon.
A few other changes:
Fix a bug in SMTEngine: defineFunction should finalize options.
Call setDefaults before initilizing the TheoryEngine and ProofManager. This is necessary so that the PROOF(...) macro works earlier during initialization.
The next step will be to remove the links infrastructure for the options infrastructure. This will enable further detangling of our options dependencies.
|
|
This moves SmtEngine::setDefaults to its own file.
This design is not final. One could imagine this being a part of a "OptionsSetter" utility. I am leaving this as is until we refactor the relationship between SmtEngine and Options.
Regardless, the general file structure should be such that this method is separate from SmtEngine, since setting default options is a large task that should be addressed independently from the core of SmtEngine.
This is initial preparation towards converting the SmtEngine from Expr -> Node.
A few very minor changes were made to the code to make the separation possible.
|
