cvc5.git
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.

3 years agoImprove documentation for FP rounding mode, add bibliography (#6343)
Gereon Kremer [Wed, 14 Apr 2021 21:52:06 +0000 (23:52 +0200)]
Improve documentation for FP rounding mode, add bibliography (#6343)

Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
3 years agoImprove documentation of API kinds (#6341)
Gereon Kremer [Wed, 14 Apr 2021 21:10:11 +0000 (23:10 +0200)]
Improve documentation of API kinds (#6341)

This PR improves the documentation of the api::Kind enum. Note that the docs for many of the enum values should still be improved. This PR merely makes sure that everything that is already there is actually output (/* vs /**) and properly rendered (missing spacing between lists, some formulas, etc).

3 years agoImprove documentation for API exceptions (#6340)
Gereon Kremer [Wed, 14 Apr 2021 20:35:07 +0000 (22:35 +0200)]
Improve documentation for API exceptions (#6340)

3 years agoRefactor / reimplement statistics (#6162)
Gereon Kremer [Wed, 14 Apr 2021 19:37:12 +0000 (21:37 +0200)]
Refactor / reimplement statistics (#6162)

This PR refactors how we collect statistics.
It splits the current statistic values into the values and a proxy object. The actual values now live inside the registry (making the ownership model way easier) while the proxy object are handed to whoever wants to collect a new statistic.
It also extends the C++ API to obtain and inspect the statistics.
To change the ownership, this PR needs to touch every single statistic in the whole codebase and change how it is registered.

3 years agoRename public and private headers in src/include. (#6352)
Aina Niemetz [Wed, 14 Apr 2021 18:56:47 +0000 (11:56 -0700)]
Rename public and private headers in src/include. (#6352)

3 years ago[unsat-cores] Improving new unsat cores (#6356)
Haniel Barbosa [Wed, 14 Apr 2021 17:50:10 +0000 (14:50 -0300)]
[unsat-cores] Improving new unsat cores (#6356)

This commit adds a new option to produce unsat cores based on our proof infrastructure (whereas previously we could only do so if we were also checking unsat cores) and the corresponding changes to the default settings to account for it. Since now options::unsatCores() and options::produceProofs() are incompatible, several parts of the code where we tested if we were in "old unsat cores mode", by testing the former and the negation of the latter options, are updated accordingly.

This commit also changes how SMT engine sets things by disabling proofs in the theory engine if we are in unsat core mode.

3 years agoAdd internal API methods for pool-based instantiation (#6350)
Andrew Reynolds [Wed, 14 Apr 2021 16:49:50 +0000 (11:49 -0500)]
Add internal API methods for pool-based instantiation (#6350)

3 years agoAdd interface for getting relevant assertions (#5131)
Andrew Reynolds [Wed, 14 Apr 2021 16:12:30 +0000 (11:12 -0500)]
Add interface for getting relevant assertions (#5131)

This adds an interface to TheoryEngine for getting the current set of relevant assertions if it is available.

An interface to this can further be added to the API in a future PR.