cvc5.git
3 years agoUse EnvObj-based options in preprocessing (#7165)
Gereon Kremer [Fri, 10 Sep 2021 00:21:57 +0000 (17:21 -0700)]
Use EnvObj-based options in preprocessing (#7165)

This PR is the first step in replacing options access via options::foo() to using the environment (via EnvObj and options().module.foo). It replaces all such options accesses in the preprocessing passes.

3 years agopp passes: Use EnvObj::rewrite() instead of Rewriter::rewrite(). (#7164)
Aina Niemetz [Thu, 9 Sep 2021 21:33:08 +0000 (14:33 -0700)]
pp passes: Use EnvObj::rewrite() instead of Rewriter::rewrite(). (#7164)

3 years agoRemove `TheoryState::getEnv()` (#7163)
Andres Noetzli [Thu, 9 Sep 2021 18:37:49 +0000 (11:37 -0700)]
Remove `TheoryState::getEnv()` (#7163)

3 years agoAdd Solver::getOutput() (#7162)
Gereon Kremer [Thu, 9 Sep 2021 17:34:43 +0000 (10:34 -0700)]
Add Solver::getOutput() (#7162)

Allow access to the Output() macro via the API.

3 years agoAdd difficulty manager (#7151)
Andrew Reynolds [Thu, 9 Sep 2021 15:26:34 +0000 (10:26 -0500)]
Add difficulty manager (#7151)

Towards supporting a (get-difficulty) command.

This tracks an estimate of the difficulty of preprocessed assertions during solving. It will be connected to TheoryEngine (via RelevanceManager) in a followup PR.

3 years agoAdd difficulty post-processor (#7150)
Andrew Reynolds [Thu, 9 Sep 2021 03:05:42 +0000 (22:05 -0500)]
Add difficulty post-processor (#7150)

This is work towards supporting a (get-difficulty) command.

This is a helper class for transforming the difficulty of preprocessed assertions to difficulty of the input assertions.

3 years agoDisable shared selectors for quantified logics without SyGuS (#7156)
Andrew Reynolds [Thu, 9 Sep 2021 01:50:09 +0000 (20:50 -0500)]
Disable shared selectors for quantified logics without SyGuS (#7156)

The use of shared selectors may have fairly negative effects when combined with E-matching. The issue is that it allows too many things to match. When shared selectors are disabled, a selector trigger like s(x) will only match terms that access the field of the constructor associated with s. When we use shared selectors, s(x) is converted to e.g. shared_selector_D_Int_1(x), which in turn matches applications of selectors of the same type over any constructor.

This PR disables shared selectors when quantifiers are present and SyGuS is not used.
It also disables shared selectors in single invocation subcalls, thus fixes #3109.
It further makes a minor fix to the datatypes rewriter to ensure that rewritten form does not depend on options.

3 years agoRemove `TheoryState::options()` (#7148)
Andres Noetzli [Thu, 9 Sep 2021 01:28:25 +0000 (18:28 -0700)]
Remove `TheoryState::options()` (#7148)

This commit removes TheoryState::options() by changing more classes to
EnvObjs.

3 years agoRemove deprecated SyGuS method evaluateWithUnfolding (#7155)
Andrew Reynolds [Thu, 9 Sep 2021 01:16:11 +0000 (20:16 -0500)]
Remove deprecated SyGuS method evaluateWithUnfolding (#7155)

This was a predecessor to the evaluator and TermDbSygus::rewriteNode that is no longer necessary.

This refactors the code so that evaluateWithUnfolding is replaced by rewriteNode as necessary throughout the SyGuS solver.

Note that in a few places, the extended rewriter was being used where TermDbSygus::rewriteNode (which also evaluates recursive function definitions) should have been used.

3 years agoAdd Lfsc print channel utilities (#7123)
Andrew Reynolds [Wed, 8 Sep 2021 21:42:30 +0000 (16:42 -0500)]
Add Lfsc print channel utilities (#7123)

These are utilities used for two-pass printing of LFSC proofs.

3 years agoImprove pre-skolemization, move quantifiers preprocess to own file (#7153)
Andrew Reynolds [Wed, 8 Sep 2021 20:54:22 +0000 (15:54 -0500)]
Improve pre-skolemization, move quantifiers preprocess to own file (#7153)

This also heavily refactors the preskolemization method (now in QuantifiersPreprocess), in preparation for it being enabled by default. This method previously was doing a tree traversal, it now maintains a visited cache.

It makes minor cleanup to the dependencies of this method.

3 years agoRefactor options::set() (#7138)
Gereon Kremer [Wed, 8 Sep 2021 19:36:50 +0000 (12:36 -0700)]
Refactor options::set() (#7138)

This PR refactors the code generation and the generate code for options::set().

3 years agoWork on comments (#7139)
Gereon Kremer [Wed, 8 Sep 2021 19:14:24 +0000 (12:14 -0700)]
Work on comments (#7139)

This PR fixes / improves the comments in the options scripts.

3 years agoA couple of minor cleanups (#7141)
Gereon Kremer [Wed, 8 Sep 2021 18:59:53 +0000 (11:59 -0700)]
A couple of minor cleanups (#7141)

This PR does a couple of minor cleanups related to options.

3 years agoRefactor code generation for options.h/.cpp (#7126)
Gereon Kremer [Wed, 8 Sep 2021 18:41:50 +0000 (11:41 -0700)]
Refactor code generation for options.h/.cpp (#7126)

This PR refactors the options code generation for the options/options.h/.cpp files.

3 years agoTowards standard usage of ExtendedRewriter (#7145)
Andrew Reynolds [Wed, 8 Sep 2021 17:30:31 +0000 (12:30 -0500)]
Towards standard usage of ExtendedRewriter (#7145)

This PR:

Adds extendedRewrite to EnvObj and Rewriter.
Eliminates static calls to Rewriter::rewrite from within the extended rewriter. Instead, the use of extended rewriter is always through Rewriter, which passes itself to the ExtendedRewriter.
Make most uses of extended rewriter non-static. I've added a placeholder method Rewriter::callExtendedRewrite for places in the code that call the extended rewriter are currently difficult to eliminate.

3 years agoAdd option for using bound inference for relevant assertions (#7152)
Andrew Reynolds [Wed, 8 Sep 2021 16:33:40 +0000 (11:33 -0500)]
Add option for using bound inference for relevant assertions (#7152)

The method for discarding assertions based on bound inference is quite expensive (40% of runtime) for some benchmarks with quantified formulas from Facebook. This adds an option to disable this, which is done by default for quantified logics.

3 years agoAdd LFSC side condition conversion utility for list variables (#7131)
Andrew Reynolds [Wed, 8 Sep 2021 13:39:31 +0000 (08:39 -0500)]
Add LFSC side condition conversion utility for list variables (#7131)

Required for automatic generation of side conditions from DSL rewrite rules.

3 years agoAdd Datatype.java to the Java API (#6389)
mudathirmahgoub [Wed, 8 Sep 2021 08:33:16 +0000 (03:33 -0500)]
Add Datatype.java to the Java API (#6389)

This commit adds Datatype.java DatatypeTest.java and cvc5_Datatype.cpp to the java api.

3 years agoAdd DatatypeConstructor.java, DatatypeConstructorDecl.java, DatatypeDecl.java, Dataty...
mudathirmahgoub [Wed, 8 Sep 2021 08:25:23 +0000 (03:25 -0500)]
Add DatatypeConstructor.java, DatatypeConstructorDecl.java, DatatypeDecl.java, DatatypeSelector.java (#6390)

Add DatatypeConstructor.java, DatatypeConstructorDecl.java, DatatypeDecl.java, DatatypeSelector.java and their corresponding c++ files

3 years agoUse rewriteViaMethod instead of accessing builtin proof checker (#7146)
Andrew Reynolds [Wed, 8 Sep 2021 07:00:23 +0000 (02:00 -0500)]
Use rewriteViaMethod instead of accessing builtin proof checker (#7146)

3 years agoRefactoring of proof manager initialization (#7073)
Andrew Reynolds [Tue, 7 Sep 2021 21:39:52 +0000 (16:39 -0500)]
Refactoring of proof manager initialization (#7073)

No longer takes a backwards reference to SmtEngine.

Also takes minor changes to proof post-processor from proof-new.

3 years agoUse `EnvObj` methods instead of `Theory` methods (#7144)
Andres Noetzli [Tue, 7 Sep 2021 20:52:23 +0000 (13:52 -0700)]
Use `EnvObj` methods instead of `Theory` methods (#7144)

This removes the methods `getEnv()`, `options()`, `getSatContext()`, and
`getUserContext()` from the `Theory` class because they are now part of
`EnvObj`. Additionally, this commit converts the inference managers to
`EnvObj` because of there were some calls to retrieve the contexts from
`Theory` in those classes.

3 years agosygus: Eliminate calls to Rewriter::rewrite. (#7142)
Aina Niemetz [Tue, 7 Sep 2021 18:23:29 +0000 (11:23 -0700)]
sygus: Eliminate calls to Rewriter::rewrite. (#7142)

This derives sygus unification utility objects from EnvObj where
necessary. There's one remaining occurrence of Rewriter::rewrite in
sygus_unif_rl.cpp, which is a bit tricky to address and thus subject to
a future PR.

3 years agoRefactoring and fixes of set defaults for quantifiers (#7120)
Andrew Reynolds [Tue, 7 Sep 2021 03:41:04 +0000 (22:41 -0500)]
Refactoring and fixes of set defaults for quantifiers (#7120)

This PR further refactors set defaults for incompatibility issues related to quantifiers.

It adds a new restriction that was discovered recently: --nl-rlv should not be used in quantified logics. Some regressions are modified that are impacted by this restriction.

Also does minor rearrangements to the order in which default options are set.

3 years agoEnvObj: Add options(), context(), userContext(). (#7137)
Aina Niemetz [Fri, 3 Sep 2021 23:33:33 +0000 (16:33 -0700)]
EnvObj: Add options(), context(), userContext(). (#7137)

This further renames EnvObj::getLogicInfo to EnvObj::logicInfo.

3 years agoAvoiding duplicate search in maps (#7055)
MikolasJanota [Fri, 3 Sep 2021 22:59:46 +0000 (00:59 +0200)]
Avoiding duplicate search in maps (#7055)

This commit identifies a couple of scenarios where an operation required
2 searches into a map/hashmap and replaces them with a single search.
This also makes the code shorter.

Signed-off-by: Mikolas Janota <mikolas.janota@gmail.com>
3 years agosygus: Make more classes derive from EnvObj. (#7140)
Aina Niemetz [Fri, 3 Sep 2021 22:36:44 +0000 (15:36 -0700)]
sygus: Make more classes derive from EnvObj. (#7140)

3 years agoRefactor option sanitizations (#7129)
Gereon Kremer [Fri, 3 Sep 2021 19:12:13 +0000 (12:12 -0700)]
Refactor option sanitizations (#7129)

This PR refactors the code that performs sanity checks on the parsed option data.

3 years agoStandardize Rewriter::rewriteViaMethod call (#7119)
Andrew Reynolds [Fri, 3 Sep 2021 18:42:18 +0000 (13:42 -0500)]
Standardize Rewriter::rewriteViaMethod call (#7119)

This moves the standard method for rewrites in proofs from TheoryBuiltinProofRuleChecker to Rewriter.  The motivation for this change is to make various kinds of rewrite methods (standard rewrite, extended rewrite, extended equality rewrite, evaluate) accessible throughout the code in a standard way.  After this PR, it is possible to know variants of the REWRITE proof rule application by having access to the rewriter, instead of having to get the builtin proof rule checker.  Note that TheoryBuiltinProofRuleChecker::applyRewrite *cannot* be static since access to the rewriter is not longer permitted to be static.

It also removes some unused infrastructure from Rewriter.

Followup PRs will remove applyRewrite for TheoryBuiltinProofRuleChecker in favor of calling the rewriter directly.

3 years agoCheck that alternate is only set for bool (#7125)
Gereon Kremer [Fri, 3 Sep 2021 18:26:29 +0000 (11:26 -0700)]
Check that alternate is only set for bool (#7125)

This PR slightly changes how the alternate option property is handled and explicitly checks that alternate is only set for bool options.

3 years agoRefactor options::get() and options::getNames() (#7135)
Gereon Kremer [Fri, 3 Sep 2021 18:02:58 +0000 (11:02 -0700)]
Refactor options::get() and options::getNames() (#7135)

This PR refactors the code generation and the generated code for options::get() and options::getNames().

3 years agoMake quantifier module classes derive from EnvObj (#7132)
Andrew Reynolds [Fri, 3 Sep 2021 17:09:57 +0000 (12:09 -0500)]
Make quantifier module classes derive from EnvObj (#7132)

3 years agosygus: Make CeSingleInv derive from EnvObj. (#7136)
Aina Niemetz [Fri, 3 Sep 2021 16:54:41 +0000 (09:54 -0700)]
sygus: Make CeSingleInv derive from EnvObj. (#7136)

This further reorders the header according to the code style guidelines.

3 years agoEliminate backwards ref to SmtEngine from abduction and interpol solvers (#7133)
Andrew Reynolds [Fri, 3 Sep 2021 16:33:27 +0000 (11:33 -0500)]
Eliminate backwards ref to SmtEngine from abduction and interpol solvers (#7133)

3 years agotheory: Have more classes in theory with reference to Env derive from EnvObj. (#7130)
Aina Niemetz [Fri, 3 Sep 2021 12:34:27 +0000 (05:34 -0700)]
theory: Have more classes in theory with reference to Env derive from EnvObj. (#7130)

3 years agotheory: Have Theory and TheoryArith* derive from EnvObj. (#7128)
Aina Niemetz [Fri, 3 Sep 2021 01:27:30 +0000 (18:27 -0700)]
theory: Have Theory and TheoryArith* derive from EnvObj. (#7128)

Note: the diff in theory.h is only huge because of small changes that caused huge reformat. The effective change is only that it now derives from EnvObj, does not have a member d_env (because it inherits it) and does not need getLogicInfo (because that's in EnvObj).

3 years agoRemove "experimental" options (#7124)
Gereon Kremer [Fri, 3 Sep 2021 00:42:00 +0000 (17:42 -0700)]
Remove "experimental" options (#7124)

This PR changes all options from experimental to expert and adds a check that only the well-defined option categories are used (common, regular, expert, undocumented).

3 years agopp: Have PreprocessingPassContext derive from EnvObj. (#7127)
Aina Niemetz [Fri, 3 Sep 2021 00:31:25 +0000 (17:31 -0700)]
pp: Have PreprocessingPassContext derive from EnvObj. (#7127)

3 years agoAdd LFSC node converter (#6944)
Andrew Reynolds [Thu, 2 Sep 2021 22:32:49 +0000 (17:32 -0500)]
Add LFSC node converter (#6944)

This utility converts from terms used in the internal calculus to terms that capture how they should be printed in LFSC.

3 years agoRefactor options handlers (#7080)
Gereon Kremer [Thu, 2 Sep 2021 21:34:40 +0000 (14:34 -0700)]
Refactor options handlers (#7080)

This PR does a major refactoring to the default option handlers (i.e. the piece of code that converts strings to the respective option types). It gets rid of the current multi-layer template specialization in favor of a simple overloaded template function.

3 years ago[Unit Tests] Fix shell test for Editline (#7117)
Andres Noetzli [Thu, 2 Sep 2021 20:05:59 +0000 (13:05 -0700)]
[Unit Tests] Fix shell test for Editline (#7117)

When using --editline, our interactive_shell_black unit test was not
working because the unit test was redirecting std::cin and std::cout
to std::stringstreams, which does not work with Editline. This commit
refactors our InteractiveShell class to explicitly take the input and
output streams as arguments, which fixes the issue because we do not use
Editline for input streams that are not std::cin. Additionally, the
commit updates the unit test to use SMT-LIB syntax instead of the
deprecated CVC language.

3 years agoDisable sygus-inst for regression close to time limit. (#7122)
Aina Niemetz [Thu, 2 Sep 2021 19:55:08 +0000 (12:55 -0700)]
Disable sygus-inst for regression close to time limit. (#7122)

3 years agoEnvObj: Restrict access. (#7121)
Aina Niemetz [Thu, 2 Sep 2021 19:04:11 +0000 (12:04 -0700)]
EnvObj: Restrict access. (#7121)

This makes all members of EnvObj protected in order to prevent creating
EnvObj instances and call member functions. It further uses protected
inheritance (instead of public) for derived classes in order to disallow
`EnvObj* a = new DerivedObj();`.

3 years agoAdd API check whether option in getOptionInfo() exists (#7093)
Gereon Kremer [Thu, 2 Sep 2021 18:50:18 +0000 (11:50 -0700)]
Add API check whether option in getOptionInfo() exists (#7093)

This PR adds a missing check in the API for getOptionInfo().

3 years agoDriver & Options cleanup (#7109)
Gereon Kremer [Thu, 2 Sep 2021 18:21:56 +0000 (11:21 -0700)]
Driver & Options cleanup (#7109)

This PR does some cleanup in the driver and the options. It removes the now obsolete public attribute that allowed using the options in the driver, and removes a bunch of includes from the driver that are no longer necessary.

3 years agoRemove more instances of ufHo (#7087)
Andrew Reynolds [Thu, 2 Sep 2021 18:06:46 +0000 (13:06 -0500)]
Remove more instances of ufHo (#7087)

Towards replacing that option with a logic check throughout.

3 years agoRemove options::getAll() (#7111)
Gereon Kremer [Thu, 2 Sep 2021 17:46:47 +0000 (10:46 -0700)]
Remove options::getAll() (#7111)

options::getAll() returns a list of all options and their current values as strings. The same functionality can be obtained by using options::getNames() and options::get(). This PR does exactly this replacement, getting rid of a large chunk of generated code. Calling getInfo("all-options") may suffer a minor performance hit, but not noticeable in practice.

3 years ago[CI] Add step for running unit/API tests (#7116)
Andres Noetzli [Thu, 2 Sep 2021 17:19:35 +0000 (10:19 -0700)]
[CI] Add step for running unit/API tests (#7116)

Currently, we configure one of our builds to include unit tests but then
do not compile and run them. This commit adds a step to compile and run
the unit/API tests.

3 years agoImplement lazy proof checking modes (#7106)
Andrew Reynolds [Thu, 2 Sep 2021 17:02:46 +0000 (12:02 -0500)]
Implement lazy proof checking modes (#7106)

This implements several variants of lazy proof checking in the core proof checker.

Note this extends the ProofNode class with an additional Boolean d_provenChecked indicating whether the d_proven field was checked by the underlying proof checker.

This PR updates the default proof checking mode to lazy. The previous default can now be enabled by --proof-check=eager-simple.

3 years agoRemove PreprocessingPassContext::getSmt(). (#7118)
Aina Niemetz [Thu, 2 Sep 2021 16:43:29 +0000 (09:43 -0700)]
Remove PreprocessingPassContext::getSmt().  (#7118)

3 years agoRemove unused `Backtracker` (#7115)
Andres Noetzli [Thu, 2 Sep 2021 12:26:28 +0000 (05:26 -0700)]
Remove unused `Backtracker` (#7115)

backtrackable.h was defining a datastructure Backtracker, which was
a member in ArrayInfo and Info but it was not doing anything.

3 years ago[Unit Tests] Fix bags rewrite test (#7114)
Andres Noetzli [Thu, 2 Sep 2021 04:14:56 +0000 (21:14 -0700)]
[Unit Tests] Fix bags rewrite test (#7114)

PR #7103 did not quite fix the unit test: The types of the lambda and
the expected bags were still off. This fixes the unit test.

3 years agopp: Derive PreprocessingPass from EnvObj. (#7112)
Aina Niemetz [Thu, 2 Sep 2021 03:44:06 +0000 (20:44 -0700)]
pp: Derive PreprocessingPass from EnvObj. (#7112)

3 years agoEnable sygus-inst for FP, NIA and NRA. (#7098)
Aina Niemetz [Thu, 2 Sep 2021 03:22:57 +0000 (20:22 -0700)]
Enable sygus-inst for FP, NIA and NRA. (#7098)

3 years agorewriter: Make rewriteEqualityExt non-static. (#7110)
Aina Niemetz [Thu, 2 Sep 2021 02:57:21 +0000 (19:57 -0700)]
rewriter: Make rewriteEqualityExt non-static. (#7110)

More work towards getting rid of SmtEngine::currentSmtEngine and
closing #3468.

3 years agoAdd class EnvObj. (#7113)
Aina Niemetz [Thu, 2 Sep 2021 02:10:42 +0000 (19:10 -0700)]
Add class EnvObj. (#7113)

This class will serve as base class for classes that need access to the
environment. This does not yet have classes derive from this base class.

Will update #7110 and #7112 to use this after this is in.

3 years agoUpdate CI to macOS 11 (#7104)
Andres Noetzli [Thu, 2 Sep 2021 00:42:59 +0000 (17:42 -0700)]
Update CI to macOS 11 (#7104)

`macos-latest` is currently using macOS 10.15, so this updates the CI to use `mac-11` (Big Sur).

3 years agoClean up and document PP context. (#7102)
Aina Niemetz [Wed, 1 Sep 2021 23:54:47 +0000 (16:54 -0700)]
Clean up and document PP context. (#7102)

This marks methods const where possible and adds missing documentation.

3 years agoClean up TheoryEngine header according to code style guidelines. (#7107)
Aina Niemetz [Wed, 1 Sep 2021 19:24:03 +0000 (12:24 -0700)]
Clean up TheoryEngine header according to code style guidelines. (#7107)

3 years ago[proof] [sat] Fix lost reference to reason when processing redundant literals (#7108)
Haniel Barbosa [Wed, 1 Sep 2021 18:31:56 +0000 (15:31 -0300)]
[proof] [sat] Fix lost reference to reason when processing redundant literals (#7108)

Similarly to the issue when explaining literals, it's necassary to save the
reference to the reason for propagating a redundant literal, as adding
explanations that may be added to the SAT solver during the recursive
elimination of redundant literals may change the original reference.

3 years agoPrint response to get-model using the API (#7084)
Andrew Reynolds [Wed, 1 Sep 2021 18:05:48 +0000 (13:05 -0500)]
Print response to get-model using the API (#7084)

This changes our implementation of GetModelCommand so that we use the API to print the model.

It simplifies smt::Model so that this is a pretty printing utility, and not a layer on top of TheoryModel.

It adds getModel as an API method for returning the string representation of the model, analogous to our current support for getProof.

This eliminates the last call to getSmtEngine() from the command layer.

3 years agorewriter: Make registerTheoryRewriter non-static. (#7101)
Aina Niemetz [Wed, 1 Sep 2021 14:24:02 +0000 (07:24 -0700)]
rewriter: Make registerTheoryRewriter non-static. (#7101)

More work towards getting rid of SmtEngine::currentSmtEngine and
closing #3468.

3 years agoFixed TestTheoryWhiteBagsRewriter.map failure (#7103)
mudathirmahgoub [Wed, 1 Sep 2021 13:47:26 +0000 (08:47 -0500)]
Fixed TestTheoryWhiteBagsRewriter.map failure (#7103)

Fixed TestTheoryWhiteBagsRewriter.map failure

3 years agoFix issues with cyclic proofs due to double SYMM applications (#7083)
Andrew Reynolds [Wed, 1 Sep 2021 02:51:46 +0000 (21:51 -0500)]
Fix issues with cyclic proofs due to double SYMM applications (#7083)

Our way of constructing proofs from the equality engine in very rare cases may cause cyclic proofs due to constructing double applications of SYMM, which are not recognized as assumptions in CDProof. This is due to an interplay between LazyProofChain using an underlying CDProof as its default proof generator, where the proof chain would use the proofs from the CDProof to form a cyclic proof.

This was encountered in 9 SMT-LIB benchmarks in QF_SLIA.

This makes us safer in several places related to double SYMM steps.

3 years agoMake driver::totalTime a TimerStat (#7089)
Gereon Kremer [Wed, 1 Sep 2021 02:00:58 +0000 (19:00 -0700)]
Make driver::totalTime a TimerStat (#7089)

This makes the `driver::totalTime` statistic a `TimerStat`. This eliminates the need to obtain the overall runtime in the driver and write it to the statistics towards the end of the runtime. This not only eliminates some code in the driver, but also gets rid of the call to `getSmtEngine()` that goes around the API.
One disclaimer: The statistics output changes from seconds as a double (i.e. `1.234`) to milliseconds (i.e. `1234ms`).

3 years agoNo longer use direct access to options in driver (#7094)
Gereon Kremer [Wed, 1 Sep 2021 01:17:24 +0000 (18:17 -0700)]
No longer use direct access to options in driver (#7094)

This PR refactors the driver to no longer directly access the Options object, but instead use Solver::getOption() or Solver::getOptionInfo().

3 years agorewriter: Make clearCaches non-static. (#7100)
Aina Niemetz [Wed, 1 Sep 2021 00:35:58 +0000 (17:35 -0700)]
rewriter: Make clearCaches non-static. (#7100)

This works towards getting rid of SmtEngine::currentSmtEngine and
closing #3468.

3 years agoLazy proof reconstruction for strings theory solver (#7096)
Andrew Reynolds [Wed, 1 Sep 2021 00:05:29 +0000 (19:05 -0500)]
Lazy proof reconstruction for strings theory solver (#7096)

This makes it so that we call the strings::InferProofCons::convert lazily, instead deferring to a temporary, trusted STRING_INFERENCE rule.

This decreases our average proof overhead on commonly solved instances from 64% to 58% on QF_S + QF_SLIA. It also reduces timeouts significantly, from 2010 to 1460. (Note these numbers were with a slightly extended version of this branch that includes other pending PRs for proofs).

Also fixes one subtle issue where proof reconstruction was misusing sequential substitutions (leading to warnings during proof post-processing).

3 years agobv: Remove dump=bv-rewrites. (#7099)
Aina Niemetz [Tue, 31 Aug 2021 22:26:25 +0000 (15:26 -0700)]
bv: Remove dump=bv-rewrites. (#7099)

This is work towards eliminating calls to currentSmtEngine.
This dump mode will become obsolete with the DSL, and is thus now
removed.

3 years agoMake sure modes are sorted in ModeInfo (#7097)
Gereon Kremer [Tue, 31 Aug 2021 19:27:55 +0000 (12:27 -0700)]
Make sure modes are sorted in ModeInfo (#7097)

This PR ensures that the possible modes returned in getOptionInfo() are always sorted. Their order would depend on the python dictionary ordering, which changed with a somewhat recent python version and thereby breaks our tests.

3 years agobv-to-int-module: implementations and stubs for translating operators (#7086)
yoni206 [Tue, 31 Aug 2021 16:45:48 +0000 (19:45 +0300)]
bv-to-int-module: implementations and stubs for translating operators (#7086)

This PR introduces most of the code for the translation of terms with operators. Some methods are left as stubs for future PRs.
A unit test is added with sanity checks for all implemented operators.

3 years agoFix normal forms context-dependent simplification for strings (#7090)
Andrew Reynolds [Tue, 31 Aug 2021 14:07:48 +0000 (09:07 -0500)]
Fix normal forms context-dependent simplification for strings (#7090)

This corrects an issue in our context-dependent simplification which limited the cases it was applied.

Previously, we were using a best content heuristic when it was applicable to compute the substitution, even if we were in an effort where normal forms had been computed. The latter should always be used if possible, since normal forms always have at least as much or more concrete components.

3 years agoMake regular expression sort not closed enumerable (#7092)
Andrew Reynolds [Tue, 31 Aug 2021 12:43:05 +0000 (07:43 -0500)]
Make regular expression sort not closed enumerable (#7092)

This ensures we don't try to apply e.g. enumerative instantiation to quantified formulas over regular expressions, since no type enumerator exists for RE.

Fixes #6750.

3 years agoAdd API function to obtain information about a single option (#6980)
Gereon Kremer [Mon, 30 Aug 2021 23:55:58 +0000 (16:55 -0700)]
Add API function to obtain information about a single option (#6980)

This PR adds api::Solver::getOptionInfo() that returns information about a single option, including its name, aliases, current and default value and its domain.

3 years agoAdd kind BAG_MAP and its type rule to bags (#6503)
mudathirmahgoub [Mon, 30 Aug 2021 23:26:43 +0000 (18:26 -0500)]
Add kind BAG_MAP and its type rule to bags (#6503)

This PR adds kind BAG_MAP to bags.

3 years agoFurther refactoring of set defaults for incompatibility methods (#7072)
Andrew Reynolds [Mon, 30 Aug 2021 22:36:15 +0000 (17:36 -0500)]
Further refactoring of set defaults for incompatibility methods (#7072)

This introduces standard methods for checking incompatible with models, unsat-cores, incremental, proofs.

There is one minor change in behavior in this PR.When bitblast=eager and models were enabled in combined logics, then the set defaults would change the bitblast mode to lazy. However, it would then in the same block complain that eager cannot be used in combination with incremental. After this PR, we won't complain in this case since we've already decided to change the bitblast mode to lazy.

3 years agoRefactor filename handling (#7088)
Gereon Kremer [Mon, 30 Aug 2021 21:23:29 +0000 (14:23 -0700)]
Refactor filename handling (#7088)

This PR simplifies how we store the current input file name and handle setting and getting it.
It is now an option, that can also be set and get via setInfo() and getInfo().

3 years agoFix proof equality engine for "no-explain" premises (#7079)
Andrew Reynolds [Mon, 30 Aug 2021 20:44:32 +0000 (15:44 -0500)]
Fix proof equality engine for "no-explain" premises (#7079)

There was an inconsistency between when the equality engine would explain a literal and when we would provide a proof for it. This led to rare cases where we over zealously provided a proof for a fact that should have been an assumption in the theory lemma proof.

This corrects the issue by ensuring that no-explain premises are explicitly marked via a new helper proof generator "AssumptionProofGenerator" which always supplies (ASSUME f) as the proof for f.

This corrects some proof checking errors on string benchmarks.

3 years agopython docs for Datatype-related classes (#7058)
yoni206 [Mon, 30 Aug 2021 19:32:24 +0000 (22:32 +0300)]
python docs for Datatype-related classes (#7058)

3 years agoFix quantifiers dynamic split module for parametric datatypes (#7085)
Andrew Reynolds [Mon, 30 Aug 2021 19:10:27 +0000 (14:10 -0500)]
Fix quantifiers dynamic split module for parametric datatypes (#7085)

Fixes #6838.

3 years agoAdd Driver options (#7078)
Gereon Kremer [Fri, 27 Aug 2021 18:51:02 +0000 (11:51 -0700)]
Add Driver options (#7078)

This PR adds a new API function Solver::getDriverOptions() which is used to communicate special options that (a) can not be properly communicated via getOption() and (b) need to be available in the driver (in a type-safe manner).
As of now, this concerns the input stream and output streams.
Furthermore, this PR refactors the driver to obtain them via the driver options instead of using the (deprecated) Solver::getOptions() method.

3 years agoHandle languages as strings in driver (#7074)
Gereon Kremer [Fri, 27 Aug 2021 18:23:15 +0000 (11:23 -0700)]
Handle languages as strings in driver (#7074)

This PR moves the first chunk of code in the driver to use the proper options API for the language options. It is now handled as a string.

3 years agoExpand definitions in sygus operators at the SMT level (#7077)
Andrew Reynolds [Fri, 27 Aug 2021 18:03:41 +0000 (13:03 -0500)]
Expand definitions in sygus operators at the SMT level (#7077)

Eliminates another call to currentSmtEngine.

This PR ensures we remember the mapping between operators that are embedded in sygus datatypes during preprocessing, instead of computing this within the sygus datatypes utilities when solving.

3 years agoAdd n-ary match trie utility (#6909)
Andrew Reynolds [Fri, 27 Aug 2021 17:28:31 +0000 (12:28 -0500)]
Add n-ary match trie utility (#6909)

Towards rewrite rule reconstruction

3 years agoAdd missing methods to Solver API for models (#7052)
Andrew Reynolds [Fri, 27 Aug 2021 15:36:27 +0000 (10:36 -0500)]
Add missing methods to Solver API for models (#7052)

This adds the last two remaining API methods required for implementing the text output of get-model on the API side.

A followup PR will implement GetModelCommand on the API side and eliminate the (last remaining) call to getSmtEngine() from the command layer.

This PR does some minor reorganization of the model cores code to account for the new interface. It also removes a deprecated interface from TheoryModel.

3 years agoAdd `isNull` to cpp api tests, python api, and python api tests (#7059)
yoni206 [Fri, 27 Aug 2021 00:34:12 +0000 (03:34 +0300)]
Add `isNull` to cpp api tests, python api, and python api tests (#7059)

While working on API documentation for python, I noticed that isNull is not wrapped
by the python API. It is also not tested in the cpp API tests. This PR fixes both issues,
and also updates the python api tests accordingly.

3 years agoFix a subtle issues with squashing the docs-ci history (#7075)
Gereon Kremer [Thu, 26 Aug 2021 21:03:05 +0000 (14:03 -0700)]
Fix a subtle issues with squashing the docs-ci history (#7075)

The docs-cleanup job squashes all commits from the docs-ci repository that are older than one month. The current solution to retrieve the newest commit older than this one month erroneously relied on the commit date. As the script cherry-picks all newer commits, it should rather use the author date, though. Unfortunately, rev-list does not support filtering by author date, hence we use awk now...

3 years agoEliminate currentSmtEngine for subsolver calls (#7068)
Andrew Reynolds [Thu, 26 Aug 2021 16:55:59 +0000 (11:55 -0500)]
Eliminate currentSmtEngine for subsolver calls (#7068)

This eliminates another occurrence of smt::currentSmtEngine by making it required to pass options + logic for all subsolver calls.

3 years agoDump models for isNotEntailed results (#7071)
Andrew Reynolds [Thu, 26 Aug 2021 16:32:09 +0000 (11:32 -0500)]
Dump models for isNotEntailed results (#7071)

This fixes a minor issue where models should be dumped for "not entailed" results. This fix was required when preparing the submission to CASC this year.

3 years agoMake datatype selector expansion to its own accessible method (#7069)
Andrew Reynolds [Thu, 26 Aug 2021 16:20:43 +0000 (11:20 -0500)]
Make datatype selector expansion to its own accessible method (#7069)

This eliminates another call to currentSmtEngine.

After this, there are only two remaining calls (one for normalizing sygus grammars wrt user define-funs, and the other for Rewriter::rewrite).

3 years agoImprove integration of nonlinear arithmetic into the arithmetic theory. (#6956)
Gereon Kremer [Thu, 26 Aug 2021 14:19:56 +0000 (07:19 -0700)]
Improve integration of nonlinear arithmetic into the arithmetic theory. (#6956)

The nonlinear extension used to be called only during model construction, a rather atypical place which lead to a series of subtle issues. This PR moves it into the postCheck method. To do that, a few other changes are necessary, most notably collectAssertedTerms and collectTerms are moved back from the model manager into the theory class.

3 years agoint2bv: Fix conversion of signed bit-vector values. (#7061)
Mathias Preiner [Thu, 26 Aug 2021 00:50:53 +0000 (17:50 -0700)]
int2bv: Fix conversion of signed bit-vector values. (#7061)

This commit fixes the conversion of signed bit-vector values to integers in the int-to-bv preprocessing pass.

3 years agoConsolidate language types (#7065)
Gereon Kremer [Thu, 26 Aug 2021 00:19:41 +0000 (17:19 -0700)]
Consolidate language types (#7065)

This PR combines the two enums InputLanguage and OutputLanguage into a single Language type. It makes sure that AST is not used as input language using a predicate whenever the option is set.

3 years agoAdd missing include (#7067)
Gereon Kremer [Wed, 25 Aug 2021 18:01:26 +0000 (11:01 -0700)]
Add missing include (#7067)

This adds a missing include. Compilation fails right now, if libpoly is disabled.

3 years agoEliminate calls to currentSmtEngine (#7060)
Andrew Reynolds [Wed, 25 Aug 2021 16:27:03 +0000 (11:27 -0500)]
Eliminate calls to currentSmtEngine (#7060)

Work towards supporting multiple solvers running in parallel.

There are now only 5 remaining internal calls to smt::currentSmtEngine.

More will be eliminated on future PRs.

3 years agoSplit higher-order term database (#7045)
Andrew Reynolds [Tue, 24 Aug 2021 20:54:31 +0000 (15:54 -0500)]
Split higher-order term database (#7045)

This splits higher-order term database as a derived class of term database, thus separating higher-order specific things out of our core term database.

This eliminates many of the references to the deprecated option uf-ho.

This is work towards eliminating that option.

3 years agoRefactor enumerator management in synth conjecture (#6942)
Andrew Reynolds [Tue, 24 Aug 2021 17:26:35 +0000 (12:26 -0500)]
Refactor enumerator management in synth conjecture (#6942)

This moves the method SynthConjecture::getEnumeratedValue to its own class, EnumManager.

It also integrates the sygus enumerator callback into the fast enumerator.

3 years agobv-to-int: more implementations (#7051)
yoni206 [Tue, 24 Aug 2021 01:20:56 +0000 (04:20 +0300)]
bv-to-int: more implementations (#7051)

This PR introduces more implementations for the bv-to-int module. Once all implementations are in, this module will be called from the bv-to-int preprocessing pass, and the code there will be deleted.

Here we focus on the translation of nodes without children.
Unit tests are included.

3 years agoTop-level structure for set defaults (#7047)
Andrew Reynolds [Tue, 24 Aug 2021 01:09:31 +0000 (20:09 -0500)]
Top-level structure for set defaults (#7047)

This breaks setDefaults into three functions that summarize the high-level behavior of setDefaults.