cvc5.git
3 years agoFP: Move type check from expandDefinitions. (#6479)
Aina Niemetz [Tue, 4 May 2021 01:00:03 +0000 (18:00 -0700)]
FP: Move type check from expandDefinitions. (#6479)

3 years agoFP: Rewrite to_fp conversion from signed bit-vector. (#6472)
Aina Niemetz [Mon, 3 May 2021 20:27:02 +0000 (13:27 -0700)]
FP: Rewrite to_fp conversion from signed bit-vector. (#6472)

SymFPU does not allow to_fp conversion from signed bv of size 1. This
adds rewrites for this case.

Rewrites for the constant and the non-constant cases were tested in
isolation.

3 years agoAdd missing --auto-download in CI (#6478)
Gereon Kremer [Mon, 3 May 2021 20:15:36 +0000 (22:15 +0200)]
Add missing --auto-download in CI (#6478)

This PR adds --auto-download for the CI job that builds the documentation. Also makes sure that the documentation workflow never fails.

3 years agoAdd CI jobs to build docs (#6413)
Gereon Kremer [Mon, 3 May 2021 19:21:19 +0000 (21:21 +0200)]
Add CI jobs to build docs (#6413)

This PR adds CI jobs to automatically build documentation for branches on the main repository and for pull request.
The first job builds the documentation for every push and pr and stores the generated documentation in cvc5.github.io/docs-ci. All versions are stored and for every branch and PR a symbolic link to the most recent version is maintained.
Note that the PR jobs are run by the pull_request_target trigger that allows access to repository secrets, but runs in the context of the target branch and we thus need to (carefully!) pull in the relevant changes manually.
The second job runs once a week and prunes the docs-ci repository: all directories that have not been touched for a month are removed, and all commits older than a month are squashed into a single commit. This retains the full history for the last month, but effectively removes everything older than that.

3 years agoSymFPU: Automatically apply patch from 2020-11-14. (#6471)
Aina Niemetz [Mon, 3 May 2021 17:48:06 +0000 (10:48 -0700)]
SymFPU: Automatically apply patch from 2020-11-14. (#6471)

This automatically applies @martin-cs's working patch from 2020-11-14.
It fixes several issues, all covered open issues are added as
regression tests.

Fixes #3582.
Fixes #5511.
Fixes #6164.

3 years agoPython API tests for terms -- Part 1 (#6468)
yoni206 [Mon, 3 May 2021 06:35:47 +0000 (23:35 -0700)]
Python API tests for terms -- Part 1 (#6468)

This PR removes the old python api tests for terms from test/api/python/test_term.py and replaces it with a new test file test/python/unit/api/test_term.py. The new test file is obtained by translating test/unit/api/term_black.cpp.

In this PR I only include the tests that pass without requiring any change to the python API. The next PR will add functions to the python API that are currently not supported, along with corresponding tests.

Comment: This was originally done in #6460 on the wrong fork. Now it is re-opened, and addresses all comments given there.

3 years agobv: Refactor ppAssert and move to TheoryBV. (#6470)
Mathias Preiner [Fri, 30 Apr 2021 22:15:44 +0000 (15:15 -0700)]
bv: Refactor ppAssert and move to TheoryBV. (#6470)

This PR refactors ppAssert from the lazy BV solver and moves it to TheoryBV.

3 years agoAdd parameter name for argument `isPreRewrite` for FP rewrites. (#6469)
Aina Niemetz [Fri, 30 Apr 2021 22:06:30 +0000 (15:06 -0700)]
Add parameter name for argument `isPreRewrite` for FP rewrites. (#6469)

3 years agoRefactor optimization result and objective classes + add preliminary support for...
Ouyancheng [Fri, 30 Apr 2021 21:40:49 +0000 (14:40 -0700)]
Refactor optimization result and objective classes + add preliminary support for multiple objectives (#6459)

This PR is one part of multiple.
Preliminary support means currently only supports single objective.
It supports queue-ing up objectives and it always optimizes the first.
Multiple-obj optimization algorithm will be up next.

*  Refactor optimization result and objective classes
*  Add preliminary support for multiple objectives
* The unit tests are now comparing node values instead of node addresses

3 years agoUse substitutions for implementing defined functions (#6437)
Andrew Reynolds [Fri, 30 Apr 2021 19:12:56 +0000 (14:12 -0500)]
Use substitutions for implementing defined functions (#6437)

This eliminates explicit tracking of defined functions, and instead makes define-fun add to preprocessing substitutions.
In other words, the effect of:

(define-fun f X t)
is to add f -> (lambda X t) to the set of substitutions known by the preprocessor. This is essentially the same as when
(= f (lambda X t)) was an equality solved by non-clausal simplification

The motivation for this change is both uniformity and for performance, as fewer traversals of the input formula.

In this PR:

define-fun are now conceptually higher-order equalities provided to smt::Assertions. These assertions are always added as substitutions instead of being pushed to AssertionPipeline.
Top-level substitutions are moved from PreprocessingContext to Env, since they must be accessed by Assertions. Proofs for this class are enabled dynamically during SmtEngine::finishInit.
The expandDefinitions preprocessing step is replaced by apply-substs. The process assertions module no longer needs access to expand definitions.
The proof manager does not require a special case of using the define-function maps.
Define-function maps are eliminated from SmtEngine.
Further work will reorganize the relationship between the expand definitions module and the rewriter, after which global calls to SmtEngine::expandDefinitions can be cleaned up. There is also further work necessary to better integrate theory expand definitions and top-level substitutions, which will be done on a followup PR.

3 years agoAdd assertion list utility for justification heuristic (#6414)
Andrew Reynolds [Thu, 29 Apr 2021 16:48:29 +0000 (11:48 -0500)]
Add assertion list utility for justification heuristic (#6414)

3 years agoSimplify generated code for getOption() and setOption() (#6462)
Gereon Kremer [Thu, 29 Apr 2021 16:20:36 +0000 (18:20 +0200)]
Simplify generated code for getOption() and setOption() (#6462)

This PR simplifies the generated code for Options::getOption() and Options::setOption(). It now uses less string streams, less temporary vectors and the new options[...] syntax (instead of options::...().

3 years agoAdd missing include. (#6463)
Gereon Kremer [Thu, 29 Apr 2021 13:49:20 +0000 (15:49 +0200)]
Add missing include. (#6463)

This PR fixes an issue with one of our nightlies.

3 years agoAvoid exponential explosion of small constant in CEGQI (#6461)
Gereon Kremer [Thu, 29 Apr 2021 12:38:19 +0000 (14:38 +0200)]
Avoid exponential explosion of small constant in CEGQI (#6461)

This PR fixes an issue that can lead to an exponential explosion of a rational constant for repeated calls to the cegqi instantiation strategy. The d_small_const variable was squared regularly, we now simply multiply it with its original value.

3 years agoFix BV Optimization Boundary Condition when lower bound = upper bound + 1 (#6452)
Ouyancheng [Wed, 28 Apr 2021 23:10:51 +0000 (16:10 -0700)]
Fix BV Optimization Boundary Condition when lower bound = upper bound + 1 (#6452)

If lb = ub + 1 then (lb+ub)/2 =pivot == lb since it's rounding to -infinity.
and lb <= x < pivot will always be UNSAT.
We need to handle this differently.
And this only happens in minimization.

3 years agoRefactor resource manager options (#6446)
Gereon Kremer [Wed, 28 Apr 2021 19:50:23 +0000 (21:50 +0200)]
Refactor resource manager options (#6446)

This PR refactors how the resource manager options are used. It moves options relevant for the resource manager into its own file (making the number of smt options a bit smaller) and uses the Options object directly instead of using the old static accessors.

3 years agoRemove exception headers from options.h (#6456)
Gereon Kremer [Wed, 28 Apr 2021 18:32:42 +0000 (20:32 +0200)]
Remove exception headers from options.h (#6456)

This PR removes two headers for exceptions from options.h, and instead pushes the includes to a couple of source files.

3 years agoMake sure reference stats are reset properly (#6457)
Gereon Kremer [Wed, 28 Apr 2021 18:01:15 +0000 (20:01 +0200)]
Make sure reference stats are reset properly (#6457)

This PR adds a reset() method to the ReferenceStat class. It then uses it to properly reset such statistics in the minisat solvers where lifetime is an issue.

3 years agoClean up options holder class (#6458)
Gereon Kremer [Wed, 28 Apr 2021 17:31:41 +0000 (19:31 +0200)]
Clean up options holder class (#6458)

This PR does some cleanup on the options class: it puts the option defaults into the member declaration and removes the explicit constructor; it puts the holder into a unique_ptr; it uses the regular struct copy operation instead of reconstructing the holder object; it moves some macros required for option defaults into the option holder header.
Also, this PR removes some obsolete code related to suggestions for typos.

3 years agoCleanup DidYouMean (#6454)
Gereon Kremer [Wed, 28 Apr 2021 14:42:17 +0000 (16:42 +0200)]
Cleanup DidYouMean (#6454)

This PR does a bit of cleanup on our didyoumean code.

3 years agoAdd internal support for datatype update (#6450)
Andrew Reynolds [Tue, 27 Apr 2021 22:32:40 +0000 (17:32 -0500)]
Add internal support for datatype update (#6450)

3 years agoMove slow regression to regress3 (#6451)
Andrew Reynolds [Tue, 27 Apr 2021 21:58:25 +0000 (16:58 -0500)]
Move slow regression to regress3 (#6451)

Benchmark is taking 40 seconds on production, due to the configuration that tests --check-unsat-cores.

3 years agoFix refutational soundness bug in quantifier prenexing (#6448)
Andrew Reynolds [Tue, 27 Apr 2021 21:25:11 +0000 (16:25 -0500)]
Fix refutational soundness bug in quantifier prenexing (#6448)

This bug can be triggered by define-fun, quantifier macros or inferred substitutions whose RHS contain quantified formulas.

This corrects the issue by ensuring that bound variables introduced for prenexing are fresh for distinct quantified formula subterms that may share quantified variables.

This was reported by Geoff Sutcliffe via a TPTP run.

3 years agoSimplify making function types (#6447)
Andrew Reynolds [Tue, 27 Apr 2021 20:53:37 +0000 (15:53 -0500)]
Simplify making function types (#6447)

Previously, we were conditionally checking whether a function was "flat" e.g. did not have a function type as the range type.

The original motivation for this was to catch cases where the user made a declare-fun that had function return type, which is not permitted. All these checks are already done at the API level https://github.com/CVC4/CVC4/blob/master/src/api/cpp/cvc5_checks.h#L441.

However, internally we should have no such restriction. This is required for simplifying the LFSC term processor.

3 years agoInitial setup for docs of python API (#6445)
Gereon Kremer [Tue, 27 Apr 2021 13:29:19 +0000 (15:29 +0200)]
Initial setup for docs of python API (#6445)

This PR adds the basic setup for including the python API in our sphinx documentation and shows how it works using the Datatype class as an example. In detail
- it enables sphinx.ext.autodoc and makes sure the generated pycvc5 is in the search path
- adds a index page for the python API
- adds a page for the Datatype class
- adds docstrings for the Datatype class
- does some finetuning (remove source locations, but adds signature information)

3 years agoUse std::hash for API types (#6432)
Gereon Kremer [Tue, 27 Apr 2021 05:31:58 +0000 (07:31 +0200)]
Use std::hash for API types (#6432)

This PR replaces all api::*HashFunction objects by specializations of std::hash. std::hash is meant to be extended in this way, and it allows for a much cleaner usage of std::unordered_set and std::unordered_map with these types.

3 years agoBool: Move implementation of type rules to cpp. (#6420)
Aina Niemetz [Tue, 27 Apr 2021 03:33:03 +0000 (20:33 -0700)]
Bool: Move implementation of type rules to cpp. (#6420)

3 years agoGenerate docs conf.py by cmake (#6441)
Gereon Kremer [Mon, 26 Apr 2021 20:48:40 +0000 (22:48 +0200)]
Generate docs conf.py by cmake (#6441)

This PR makes cmake generate the sphinx configuration file. This will simplify dynamically modifying this file in the future, for example to add custom paths within the build directory (for the python API).

3 years agoProtect int stats methods (#6442)
Gereon Kremer [Mon, 26 Apr 2021 20:16:27 +0000 (22:16 +0200)]
Protect int stats methods (#6442)

This PR protects two methods of the IntStat class in case statistics are disabled.

3 years agoFirst part of options refactoring (#6428)
Gereon Kremer [Mon, 26 Apr 2021 19:43:15 +0000 (21:43 +0200)]
First part of options refactoring (#6428)

This PR does a first round of refactoring and gets rid of a significant portion of generated code. In particular

- it removes options::optionName.wasSetByUser() (we still have Options::wasSetByUser())
- it removes options::optionName.set() (we still have Options::set())
- it removes options::optionName.getName() in favor of options::optionName.name
- it removes the specializations of Options::assign() and Options::assignBool() from the headers
- it eliminates runHandlerAndPredicates() and runBoolPredicates()

The removed methods are only used in few places with are changed to using Options::current().X() instead.

In the future, we also want to get rid of options::optionName() and use Options::operator[]() instead, and furthermore not use Options::current() but use the options from the Env object. This PR already adds Env::getOption() as a shorthand for Env::getOptions()[...] and uses it as a proof of concept within SmtEngine.

3 years agoFix theoryOf for Boolean equalities (#6444)
Andrew Reynolds [Mon, 26 Apr 2021 18:58:53 +0000 (13:58 -0500)]
Fix theoryOf for Boolean equalities (#6444)

Required for fixing a bug in CNF stream's ensureLiteral, which was crashing when combined with unsat-cores-mode=assumptions.

With this PR, we assign a formula like (= (= x y) (= z w)) to have theoryOf THEORY_BOOL. Previously, it mistaken was assigned THEORY_UF if e.g. x,y z, w were terms whose type was an uninterpreted sort.

We should retest unsat-cores-mode=assumptions after this PR is merged.

3 years agoNew design in DOT representation, nodes colored based on visions(basic and propositio...
Diego Della Rocca de Camargos [Mon, 26 Apr 2021 17:36:55 +0000 (14:36 -0300)]
New design in DOT representation, nodes colored based on visions(basic and propositional) (#6423)

Conclusion and rule are placed on the same node (records nodes in the dot format).
Nodes are colored based on the view they will belong to.

Signed-off-by: Diego Della Rocca de Camargos diegodellarocc@gmail.com
3 years agoEnsure dependency is tracked for all substitutions (#6438)
Andrew Reynolds [Mon, 26 Apr 2021 15:13:50 +0000 (10:13 -0500)]
Ensure dependency is tracked for all substitutions (#6438)

This ensures that dependencies are tracked for all inferred substitutions, even if a trusted step is added.

This is required to ensure unsat cores are sound when we use e.g. non-clausal simplification + unsat cores.

3 years agoEnable print-inst-full by default (#6435)
Andrew Reynolds [Mon, 26 Apr 2021 14:57:36 +0000 (09:57 -0500)]
Enable print-inst-full by default (#6435)

This makes dump-instantiations print instantiations for all quantified formulas by default, regardless of whether they had an associated identifier.

3 years agoFix assertions in SAT solver (#6443)
Haniel Barbosa [Mon, 26 Apr 2021 14:46:56 +0000 (11:46 -0300)]
Fix assertions in SAT solver (#6443)

Due to our recent changes in the unsat core infrastructure we were doing a couple assertions wrong during conflict analysis. This commit fixes them.

3 years agoDo not process looping word equations over sequences (#6434)
Andrew Reynolds [Mon, 26 Apr 2021 07:34:14 +0000 (02:34 -0500)]
Do not process looping word equations over sequences (#6434)

3 years agoUse fast enumeration by default for Boolean predicate synthesis (#6440)
Andrew Reynolds [Sun, 25 Apr 2021 20:05:15 +0000 (15:05 -0500)]
Use fast enumeration by default for Boolean predicate synthesis (#6440)

This updates the policy of when to apply smart enumeration: we do so if the grammar has ITE or admits Boolean connective terms. Previously, we applied smart enumeration for ITE and all Boolean grammars. However, this is misguided since e.g. partial evaluation unfolding has no opportunity to be effective if the enumerated terms are only Boolean literals.

This significantly improves run time on a challenge benchmark from @makaimann.

3 years agoMore check models (#6439)
Andrew Reynolds [Sun, 25 Apr 2021 19:56:01 +0000 (14:56 -0500)]
More check models (#6439)

3 years agoImprove getValue for non-evaluated operators (#6436)
Andrew Reynolds [Sat, 24 Apr 2021 01:45:01 +0000 (20:45 -0500)]
Improve getValue for non-evaluated operators (#6436)

This makes it so that we attempt evaluation + rewriting on applications of operators that do not always evaluate, and return constants in case the evaluation was successful.

This fixes warnings for check-models on 43 of our regressions, and also uncovered one regression where our model was wrong but check-models silently succeeded. I've opened CVC4/cvc4-projects#276 for fixing the latter.

3 years agoAdd assumption-based unsat cores. (#6427)
Mathias Preiner [Sat, 24 Apr 2021 00:57:35 +0000 (17:57 -0700)]
Add assumption-based unsat cores. (#6427)

This PR adds an assumption-based unsat cores option. If enabled it will
disable proof logging in the SAT solver and adds input assertions as
assumptions to the SAT solver. When an unsat core is requested we
extract the unsat core in terms of the unsat assumption in the SAT
solver. Assumption-based unsat cores use the proof infrastructure to map
the input assumptions back to the original assertions.

3 years agoAdd missing dependency for CaDiCaL (#6431)
Gereon Kremer [Fri, 23 Apr 2021 21:50:02 +0000 (23:50 +0200)]
Add missing dependency for CaDiCaL (#6431)

This PR adds the dependency of the CaDiCaL cmake target on the external project CaDiCaL-EP if it is not found in the system.

3 years ago(proof-new) Proofs for sets purification lemmas (#6416)
Andrew Reynolds [Fri, 23 Apr 2021 20:44:39 +0000 (15:44 -0500)]
(proof-new) Proofs for sets purification lemmas (#6416)

This adds proofs for sets purification lemmas, which are of the form (= t (skolem t)) and (member t (skolem (singleton t))). Each can be trivially justified in the internal calculus by MACRO_SR_PRED_INTRO.

3 years agoAdd new substitution apply methods fixpoint, sequential, simultaneous (#6429)
Andrew Reynolds [Fri, 23 Apr 2021 18:31:37 +0000 (13:31 -0500)]
Add new substitution apply methods fixpoint, sequential, simultaneous (#6429)

This adds various methods for applying substitution as an options to MACRO_SR_* rules. It extends the proof checker and the proof post processor to eliminate based on these types.

It updates the trust substitutions utility used by non-clausal simplification to use fixed-point semantics for substitution, which is highly important for efficiency.

As a result of this PR, we are orders of magnitude faster for checking proofs for problems where non-clausal substitution infers many substitutions. It also makes our regressions noticeably faster:

3 years agoMake sure a ReferenceStat is set to values of the correct type (#6430)
Gereon Kremer [Fri, 23 Apr 2021 13:46:52 +0000 (15:46 +0200)]
Make sure a ReferenceStat is set to values of the correct type (#6430)

This PR fixes a very subtle issue with setting the values a ReferenceStat refers to.
ReferenceStat::set() would take a variable by const& and then store the pointer to it. When giving it a different, but implicitly convertible, type, the pointer would assume the wrong type and consequently read incorrect values from it.
This PR makes set() a template function that explicitly checks that the given type is the correct one.
As we can only export int64_t to the API, this forces users of ReferenceStat to use int64_t stats.

3 years agoEnable strings exp by default for strings specific logics (#6424)
Andrew Reynolds [Fri, 23 Apr 2021 02:18:13 +0000 (21:18 -0500)]
Enable strings exp by default for strings specific logics (#6424)

One of the main motivations for this PR is to simplify our process for doing SMT-LIB wide runs.

3 years agoBV: Add proof logging for bit-blasting. (#6373)
Aina Niemetz [Fri, 23 Apr 2021 01:19:05 +0000 (18:19 -0700)]
BV: Add proof logging for bit-blasting.  (#6373)

3 years agoMove implementation of UF rewriter to cpp (#6393)
Andrew Reynolds [Fri, 23 Apr 2021 00:06:10 +0000 (19:06 -0500)]
Move implementation of UF rewriter to cpp (#6393)

3 years agoMake trust substitution map generate proofs lazily (#6379)
Andrew Reynolds [Thu, 22 Apr 2021 22:53:15 +0000 (17:53 -0500)]
Make trust substitution map generate proofs lazily (#6379)

This is work towards addressing a bottleneck when generating proofs for substitutions from non-clausal simplification.

This makes the proof generation in trust substitution map lazy.

Further work is required to allow an alternative fixpoint semantics for substitutions in the proof checker instead of the current sequential one.

3 years agoMinor improvements to substitutions (#6380)
Andrew Reynolds [Thu, 22 Apr 2021 22:36:02 +0000 (17:36 -0500)]
Minor improvements to substitutions (#6380)

In preparation for using this class as part of our proof checker.

This removes an option that was previously used as a hack to try to make check-models work for quantifiers. It also makes supplying a context optional.

3 years agoMinor changes to unsat core default setting (#6425)
Andrew Reynolds [Thu, 22 Apr 2021 21:03:08 +0000 (16:03 -0500)]
Minor changes to unsat core default setting (#6425)

3 years agocmake: Do not require --auto-download for already downloaded dependencies. (#6417)
Mathias Preiner [Thu, 22 Apr 2021 20:22:36 +0000 (13:22 -0700)]
cmake: Do not require --auto-download for already downloaded dependencies. (#6417)

This will look for already downloaded dependencies in the build
directory and therefore will not require --auto-download if the
dependencies were already downloaded in a previous build.

3 years agoUpdate INSTALL.md (#6412)
Gereon Kremer [Thu, 22 Apr 2021 19:55:41 +0000 (21:55 +0200)]
Update INSTALL.md (#6412)

This PR updates our build and installation instructions in INSTALL.md after we have changed how we handle dependencies.
Thanks @polgreen / #6391.

3 years agoAdd API documentation for statistics (#6364)
Gereon Kremer [Thu, 22 Apr 2021 19:38:57 +0000 (21:38 +0200)]
Add API documentation for statistics (#6364)

This PR adds documentation for api::Statistics and api::Stat, as well as further explanations in sphinx.
It also adds a custom css to our sphinx theme that slightly changes how inline code blocks look.

3 years agoRemove unused stuff from options setup (#6422)
Gereon Kremer [Thu, 22 Apr 2021 19:27:54 +0000 (21:27 +0200)]
Remove unused stuff from options setup (#6422)

This PR removes some old stuff from our options setup that has not been used in a long time.
Most prominently, this includes the man pages that were still generated, and the alias and links options, which no longer worked anyway.

3 years ago Reorganizing use of skolem definition manager in prop engine (#6415)
Andrew Reynolds [Thu, 22 Apr 2021 19:12:23 +0000 (14:12 -0500)]
 Reorganizing use of skolem definition manager in prop engine (#6415)

Towards setting up the proper callbacks into the new justification heuristic.

Moves ownership of skolem definition manager from TheoryProxy to PropEngine.

3 years agoapi docs: Rename doxygen output directory. (#6426)
Aina Niemetz [Thu, 22 Apr 2021 17:46:04 +0000 (10:46 -0700)]
api docs: Rename doxygen output directory. (#6426)

3 years agoapi docs: Remove file reintroduced in past merge. (#6426)
Aina Niemetz [Thu, 22 Apr 2021 17:20:36 +0000 (10:20 -0700)]
api docs: Remove file reintroduced in past merge. (#6426)

3 years agoFix models for sygus-inference, bv2int, real2int (#6421)
Andrew Reynolds [Thu, 22 Apr 2021 15:02:05 +0000 (10:02 -0500)]
Fix models for sygus-inference, bv2int, real2int (#6421)

In each case, previously we were generating a define-fun, what we needed was to do a model substitution.

This actually meant that check-models was giving false positives. The model was incorrect but check-models succeeded due to its use of expand definitions.

3 years agoReconciling proofs and unsat cores (#6405)
Haniel Barbosa [Thu, 22 Apr 2021 14:33:38 +0000 (11:33 -0300)]
Reconciling proofs and unsat cores (#6405)

This commit changes how defaults are set and how the SMT solver is initialized so that proofs can be used fully with (new) unsat cores. Three modes of unsat cores are established now:

the upcoming assumption-based cores, which are incompatible with producing proofs (but enable proofs for preprocessing)
cores based on the SAT proof, which are incompatible with producing proofs (but enable proofs for preprocessing and the SAT solver)
cores based on the full proof, which are unrestricted
All the modes activate proofs but lead to errors if the user requires proofs but is not in the full proofs mode for cores.

3 years agoAllow in-place construction of `CDList` items (#6409)
Andres Noetzli [Thu, 22 Apr 2021 03:25:57 +0000 (20:25 -0700)]
Allow in-place construction of `CDList` items (#6409)

This commit adds CDList::emplace_back(), which allows users to create
elements in CDList in-place (as opposed to copying the items using
CDList::push_back(). This allows CDList to be used with
std::unique_ptrs, which do not allow copying. Using
CDList::emplace_back() could also be more efficient in certain cases.

3 years agoMove expand definition from Theory to TheoryRewriter (#6408)
Andrew Reynolds [Thu, 22 Apr 2021 02:42:08 +0000 (21:42 -0500)]
Move expand definition from Theory to TheoryRewriter (#6408)

This is work towards eliminating global calls to getCurrentSmtEngine()->expandDefinition.

The next step will be to add Rewriter::expandDefinition.

3 years agoArithmetic: Move implementation of type rules to cpp. (#6419)
Aina Niemetz [Wed, 21 Apr 2021 22:57:49 +0000 (15:57 -0700)]
Arithmetic: Move implementation of type rules to cpp. (#6419)

3 years agoUF: Move implementation of type rules to cpp. (#6403)
Aina Niemetz [Wed, 21 Apr 2021 22:48:38 +0000 (15:48 -0700)]
UF: Move implementation of type rules to cpp. (#6403)

3 years agoAdd explicit dependencies for base lib (#6410)
Gereon Kremer [Wed, 21 Apr 2021 21:59:07 +0000 (23:59 +0200)]
Add explicit dependencies for base lib (#6410)

This PR adds missing cmake dependencies for the base library. This makes sure that Debug_tags.h and Trace_tags.h are already present when we start compiling.

3 years agoPass GMP to libpoly (#6411)
Gereon Kremer [Wed, 21 Apr 2021 19:33:21 +0000 (21:33 +0200)]
Pass GMP to libpoly (#6411)

This PR makes sure that our build of libpoly works on systems without GMP: by passing the paths to GMP we use ourselves to libpoly, we make sure libpoly always has a suitable version of GMP.
Also, we make libpoly somewhat faster to build by disabling tests.

3 years agoDatatypes: Move implementation of type rules to cpp. (#6418)
Aina Niemetz [Wed, 21 Apr 2021 18:54:32 +0000 (11:54 -0700)]
Datatypes: Move implementation of type rules to cpp. (#6418)

3 years agoGoodbye CVC4, hello cvc5! (#6371)
Mathias Preiner [Wed, 21 Apr 2021 17:21:34 +0000 (10:21 -0700)]
Goodbye CVC4, hello cvc5! (#6371)

This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.

3 years agocmake: Add optional module name argument for check_python_module helper. (#6406)
Mathias Preiner [Wed, 21 Apr 2021 12:52:27 +0000 (05:52 -0700)]
cmake: Add optional module name argument for check_python_module helper. (#6406)

Addtionally adds checks for required documentation modules.

3 years agoSets: Move implementation of type rules to cpp. (#6401)
Aina Niemetz [Wed, 21 Apr 2021 12:27:16 +0000 (05:27 -0700)]
Sets: Move implementation of type rules to cpp. (#6401)

3 years agoArrays: Move implementation of type rules to cpp. (#6407)
Aina Niemetz [Wed, 21 Apr 2021 03:15:43 +0000 (20:15 -0700)]
Arrays: Move implementation of type rules to cpp. (#6407)

3 years agoAdd unit test for abduction (#6400)
Andrew Reynolds [Wed, 21 Apr 2021 03:02:31 +0000 (22:02 -0500)]
Add unit test for abduction (#6400)

3 years agoAdd basic utilities for new implementation of justification heuristic (#6333)
Andrew Reynolds [Wed, 21 Apr 2021 02:34:35 +0000 (21:34 -0500)]
Add basic utilities for new implementation of justification heuristic (#6333)

This sets up the core utilities for the new implementation of justification heuristic

3 years agoAdd getNumIndices to Op (#6386)
mudathirmahgoub [Wed, 21 Apr 2021 01:57:56 +0000 (20:57 -0500)]
Add getNumIndices to Op (#6386)

Add getNumIndices to Op

3 years agoSplit FP expand definitions to own module (#6392)
Andrew Reynolds [Tue, 20 Apr 2021 23:53:56 +0000 (18:53 -0500)]
Split FP expand definitions to own module (#6392)

This moves the code for expanding definitions in floating point to its own module, which lives in the rewriter.

This is work towards moving Theory::expandDefinitions to Rewriter::expandDefinitions.

The code was only moved, not modified in this PR.

3 years agoBV: Move implementation of type rules from header to .cpp. (#6360)
Aina Niemetz [Tue, 20 Apr 2021 23:06:11 +0000 (16:06 -0700)]
BV: Move implementation of type rules from header to .cpp. (#6360)

3 years agoSep: Move implementation of type rules to cpp. (#6402)
Aina Niemetz [Tue, 20 Apr 2021 22:55:56 +0000 (15:55 -0700)]
Sep: Move implementation of type rules to cpp. (#6402)

3 years agoQuantifiers: Move implementation of type rules to cpp. (#6404)
Aina Niemetz [Tue, 20 Apr 2021 22:33:39 +0000 (15:33 -0700)]
Quantifiers: Move implementation of type rules to cpp. (#6404)

3 years agoAdd InferenceId as resources (#6339)
Gereon Kremer [Tue, 20 Apr 2021 22:10:17 +0000 (00:10 +0200)]
Add InferenceId as resources (#6339)

This PR extends the resource manager to consider theory::InferenceId a resource we can spend. This should give us a robust way to have the resource limiting cover a lot of theory reasoning. To make use of this, TheoryInferenceManager now spends these resources.
Also, it makes the ResourceManager properly use the options from the Env class.

3 years agoAdd instantiation pool feature to the API (#6358)
Andrew Reynolds [Tue, 20 Apr 2021 21:40:12 +0000 (16:40 -0500)]
Add instantiation pool feature to the API (#6358)

This adds the command declare-pool to the public API. It also adds parsing support for this feature, lifts the internal kinds to public kinds, adds an example regression, and a unit test for the new declare-pool solver method.

3 years agoSplit C++ API docs from general docs (#6365)
Gereon Kremer [Tue, 20 Apr 2021 21:10:38 +0000 (23:10 +0200)]
Split C++ API docs from general docs (#6365)

3 years agoRemove support for CVC3 language. (#6369)
Aina Niemetz [Tue, 20 Apr 2021 20:25:10 +0000 (13:25 -0700)]
Remove support for CVC3 language. (#6369)

3 years agoBasic setup for examples in documentation (#6383)
Gereon Kremer [Tue, 20 Apr 2021 19:37:18 +0000 (21:37 +0200)]
Basic setup for examples in documentation (#6383)

3 years agoAdd guards to disable clang-format around placeholders in templates. (#6375)
Aina Niemetz [Tue, 20 Apr 2021 18:58:46 +0000 (11:58 -0700)]
Add guards to disable clang-format around placeholders in templates. (#6375)

3 years agoFix `ANTLR3_COMMAND` for system ANTLR3 JAR (#6399)
Andres Noetzli [Tue, 20 Apr 2021 18:46:14 +0000 (11:46 -0700)]
Fix `ANTLR3_COMMAND` for system ANTLR3 JAR (#6399)

ANTLR3_COMMAND was using a fixed path instead of relying on the
ANTLR3_JAR variable. If the ANTLR3 JAR was found on the system (for
example due to an existing deps folder at the root of the CVC4
folder), then the command would fail because the JAR was not at the
expected location. This commit changes the command to use the variable
and prints the location of the JAR file to make debugging easier.

3 years agoProperly link Poly against GMP (#6398)
Gereon Kremer [Tue, 20 Apr 2021 16:22:47 +0000 (18:22 +0200)]
Properly link Poly against GMP (#6398)

This PR fixes a linker issue with libpoly and static builds where Poly and GMP would be linked against in the wrong order.

3 years agopython API sorts: adding functions and tests (#6361)
yoni206 [Tue, 20 Apr 2021 14:33:10 +0000 (07:33 -0700)]
python API sorts: adding functions and tests (#6361)

This PR does the following:

1. removes old python sort API test
2. creates a new python sort API test, obtained by translating the (entire) cpp unit test https://github.com/CVC4/CVC4/blob/master/test/unit/api/sort_black.cpp
3. adds support for bags and datatype selectors/testers domain/codomain in the python API.

3 years agoFully incorporate quantifiers macros into ppAssert / non-clausal simplification ...
Andrew Reynolds [Mon, 19 Apr 2021 21:59:35 +0000 (16:59 -0500)]
Fully incorporate quantifiers macros into ppAssert / non-clausal simplification (#6394)

This PR removes the quantifiers macro preprocessing pass, which had several shortcomings, both in terms of performance and features.

This makes it so that quantifier macros are the (optional) implementation of TheoryQuantifiers::ppAssert.

In other words, quantifiers can now be put into "solved form", forall x. P(x) ---> P = lambda x. true.

This is part of an effort to improve proofs for preprocessing, as well as centralizing our reason about substitutions for the sake of efficiency.

3 years agoRemove linking against gmp and cln in tests and parser (#6376)
Gereon Kremer [Mon, 19 Apr 2021 09:30:04 +0000 (11:30 +0200)]
Remove linking against gmp and cln in tests and parser (#6376)

Finally, we no longer need to link against GMP and CLN for the parser and the tests.
To actually achieve this, this PR also removes some dead code and unused includes from some parser files.

3 years agoFix dependencies for stats options (#6378)
Gereon Kremer [Fri, 16 Apr 2021 15:12:03 +0000 (17:12 +0200)]
Fix dependencies for stats options (#6378)

A last-minute edit in a previous PR broke the handling of dependencies between the statistic options.

3 years agoFix ONCE for post-rewrite (#6372)
Andrew Reynolds [Fri, 16 Apr 2021 14:36:40 +0000 (09:36 -0500)]
Fix ONCE for post-rewrite (#6372)

3 years agoRefactor cmake: auto-download and default-on dependencies (#6355)
Gereon Kremer [Fri, 16 Apr 2021 11:06:40 +0000 (13:06 +0200)]
Refactor cmake: auto-download and default-on dependencies (#6355)

This PR changes a few things in how dependencies are handled during configuration:

- --x-dir are removed for most dependencies, use the generic --dep-path instead
- the cmake ENABLE_AUTO_DOWNLOAD determines whether we attempt to download missing dependencies ourselves
- external projects check this option and send an error if it is OFF
- some optional dependencies are enabled by default (CaDiCaL, Poly, SymFPU)

This will essentially fail every call to ./configure.sh until the user specifies --auto-download.

3 years agoReplace SExpr class by simpler conversion routines (#6363)
Gereon Kremer [Fri, 16 Apr 2021 10:45:10 +0000 (12:45 +0200)]
Replace SExpr class by simpler conversion routines (#6363)

This PR finally removes the SExpr class. SMT-LIB compatible output is retained by using new on-the-fly conversion to s-expression strings. This finally allows us to remove includes to integer and rational from smt_engine.h.
In detail:

- a new set of toSExpr() methods is implemented that converts certain types to s-expression strings (without an intermediate class representing s-expressions)
- SmtEngine::getInfo() returns a string instead of SExpr and uses the new toSExpr methods
- SmtEngine::getStatistic() is removed
- SExpr class is removed
- d_commandVerbosity uses int instead of Integer

3 years agocmake: Build object libraries for base and context. (#6374)
Mathias Preiner [Fri, 16 Apr 2021 06:55:25 +0000 (23:55 -0700)]
cmake: Build object libraries for base and context. (#6374)

cmake complains that the static base and context libraries are not
exported as install targets. Since we do not want to install these
libraries we'll build object libraries instead.

3 years agopreprocessing context: Add wrapper for model substitutions. (#6370)
Aina Niemetz [Thu, 15 Apr 2021 21:57:53 +0000 (14:57 -0700)]
preprocessing context: Add wrapper for model substitutions. (#6370)

Previously, preprocessing passes added model substitutions without
expanding definitions for substitutions, which can be a problem.
This adds a wrapper function to take care of it properly.

Fixes #5473.

3 years agoBuild support library from base and context. (#6368)
Mathias Preiner [Thu, 15 Apr 2021 21:45:54 +0000 (14:45 -0700)]
Build support library from base and context. (#6368)

This PR creates a support library from the utilities in base and context, which will be required in the parser as soon as we move the symbol table/manager to the parser.

Note: I decided to always build static libraries from base and context (and optionally enable -fPIC for shared builds) since I'm not sure if we want to have these libraries installed separately. Right now these are considered as cvc5 internal utilities that can be used in all cvc5 libraries, but not outside.

3 years agoAvoid options listener for resource manager. (#6366)
Gereon Kremer [Thu, 15 Apr 2021 21:05:44 +0000 (23:05 +0200)]
Avoid options listener for resource manager. (#6366)

This PR simplifies how the resource manager interacts with the options. Instead of using some notification mechanism, the resource manager simply retrieves the options via options::xyz(). This simplifies the options handler, the resource manager interface and the options.
When instructed to do so by the API, the SmtEngine now overwrites the respective option instead of calling out to the resource manager.

3 years agoRename occurrences of CVC4 to CVC5. (#6351)
Aina Niemetz [Thu, 15 Apr 2021 20:04:55 +0000 (13:04 -0700)]
Rename occurrences of CVC4 to CVC5. (#6351)

This renames everything but GitHub links and build system related
macros. Switching the build system to cvc5 will be the last step in the
renaming process.

3 years agoFix printing of stats when aborted. (#6362)
Gereon Kremer [Thu, 15 Apr 2021 19:30:49 +0000 (21:30 +0200)]
Fix printing of stats when aborted. (#6362)

This PR improves/fixes printing of statistics when the solver has been aborted, i.e. when we use printSafe(), and a few other minor issues with the new statistics setup.

add toString() methods for TypeConstant, api::Kind to allow for automatic printing by print_safe<>()
improve kindToString() to avoid std::stringstream
fix newlines between statistics in printSafe()
make printing of histograms consistent
make --stats-all, --stats-expert and --stats-every-check automatically enable --stats (and vice versa)

3 years agoReenable regression for minimizing instantiations (#6367)
Andrew Reynolds [Thu, 15 Apr 2021 19:08:00 +0000 (14:08 -0500)]
Reenable regression for minimizing instantiations (#6367)

3 years agoFix type rule for relations join image (#6349)
Andrew Reynolds [Wed, 14 Apr 2021 22:10:09 +0000 (17:10 -0500)]
Fix type rule for relations join image (#6349)

The join image type rule restricted that an argument was a constant. This is a logic restriction that should not be a part of the type checker.

This is required for not throwing type checking exceptions during proof conversion to LFSC.