Aina Niemetz [Tue, 12 Oct 2021 18:31:57 +0000 (11:31 -0700)]
Clean up occurrences of SmtEngine in comments. (#7349)
Aina Niemetz [Tue, 12 Oct 2021 18:09:22 +0000 (11:09 -0700)]
Get rid of unused member d_smtStats in ExpandDefs. (#7346)
This further renames d_smtStats to d_slvStats in ProcessAssertions.
Aina Niemetz [Tue, 12 Oct 2021 17:53:03 +0000 (10:53 -0700)]
Rename SmtEngineState to SolverEngineState. (#7344)
Gereon Kremer [Tue, 12 Oct 2021 16:37:51 +0000 (09:37 -0700)]
Fix glpk, add antlr.so (#7341)
This PR makes the cmake integration of GLPK compatible with cmake 3.9.
Also, it adds a missing BUILD_BYPRODUCT for antlr.
Andrew Reynolds [Tue, 12 Oct 2021 16:24:40 +0000 (11:24 -0500)]
Provide a non-traversal interface to term formula removal (#7328)
Towards making theory preprocessing a single pass.
Andrew Reynolds [Tue, 12 Oct 2021 15:29:38 +0000 (10:29 -0500)]
Minor cleaning of instantiation utilities (#7334)
Also fixes a bug in the quantifiers macro utility which did not compute the instantiation constant body of a quantified formula properly.
This is work towards a major refactoring of conflict-based instantiation / entailment checks.
Andrew Reynolds [Tue, 12 Oct 2021 14:03:29 +0000 (09:03 -0500)]
Simplify skolemization in sygus solver (#7331)
The core sygus solver predates the use of subsolvers. When doing verification checks in the CEGIS loop, we previously added unique lemmas to the main solver with fresh skolem variables. We now call subsolvers only, meaning that the set of skolem variables used in verification calls can be fixed.
Ouyancheng [Tue, 12 Oct 2021 09:44:50 +0000 (02:44 -0700)]
fix deprecation of std::iterator (#7332)
When compiling cvc5 with clang-13, it will emit lots of warnings of usages of `std::iterator` as it's deprecated since C++17.
The recommended implementation of iterators is to manually define the following five types:
```
template< class Iter >
struct iterator_traits;
difference_type Iter::difference_type
value_type Iter::value_type
pointer Iter::pointer
reference Iter::reference
iterator_category Iter::iterator_category
```
And the iterator-related types could be accessed by for example `typename std::iterator_traits<Iter>::value_type value`.
This pull request performs the fix, and the program is semantically equivalent before and after the fix.
References:
https://en.cppreference.com/w/cpp/iterator/iterator_traits
https://en.cppreference.com/w/cpp/iterator/iterator
Mathias Preiner [Mon, 11 Oct 2021 23:54:34 +0000 (16:54 -0700)]
Start post-release for 0.0.2
Mathias Preiner [Mon, 11 Oct 2021 23:54:34 +0000 (16:54 -0700)]
Bump version to 0.0.2
Mathias Preiner [Mon, 11 Oct 2021 23:53:17 +0000 (16:53 -0700)]
Fix release action.
Aina Niemetz [Mon, 11 Oct 2021 23:21:32 +0000 (16:21 -0700)]
Rename SmtEngineStatistics to SolverEngineStatistics. (#7339)
Mathias Preiner [Mon, 11 Oct 2021 22:45:50 +0000 (15:45 -0700)]
Start post-release for 0.0.1
Mathias Preiner [Mon, 11 Oct 2021 22:45:50 +0000 (15:45 -0700)]
Bump version to 0.0.1
Gereon Kremer [Mon, 11 Oct 2021 20:54:30 +0000 (13:54 -0700)]
Antlr: runtime -> libraries (#7338)
For static builds, there was a mixup of variable naming in FindANTLR3 (RUNTIME vs LIBRARIES).
Aina Niemetz [Mon, 11 Oct 2021 19:13:46 +0000 (12:13 -0700)]
Rename SmtScope to SolverEngineScope. (#7284)
Gereon Kremer [Mon, 11 Oct 2021 17:48:09 +0000 (10:48 -0700)]
Revert #7257 (#7337)
This PR reverts #7257 and restores compatibility with ancient glibc versions.
Gereon Kremer [Mon, 11 Oct 2021 16:31:21 +0000 (09:31 -0700)]
Add CI workflow to test different cmake versions (#7254)
This refactors the CI setup by moving parts of the CI workflow into new composite actions. This allows to reuse this parts in a new workflow that tests against many different cmake versions. It is mostly useful after modifying our cmake setup to check compatibility with older cmake versions.
The workflow is not triggered automatically, but can be started manually.
Andrew Reynolds [Mon, 11 Oct 2021 14:28:51 +0000 (09:28 -0500)]
Connect the LFSC printer (#7323)
This adds the option --proof-format=lfsc.
It adds an initial regression to test the LFSC printer. This will be followed up with a more comprehensive plan for regression tests.
Andrew Reynolds [Mon, 11 Oct 2021 08:20:19 +0000 (03:20 -0500)]
Add cardinality constraint utilities (#7286)
This class will be used to replace the `fmf.card` operator with a 0-ary indexed parameterized nullary predicate for representing cardinality constraints for UF.
This is in preparation for eliminating hacks in the core of theory combination for e.g. not considering the dummy arguments of cardinality constraints to be shared terms.
Gereon Kremer [Mon, 11 Oct 2021 06:26:49 +0000 (23:26 -0700)]
Restore compatibility with cmake 3.9 (#7329)
This goes back to the new cmake setup and makes it compatible again with cmake 3.9.
It mostly means we can not link object libraries and also not link other libraries to object libraries.
I've tested these changes within docker on `ubuntu:18-04` with a manually installed `cmake-3.9.6`.
Gereon Kremer [Sat, 9 Oct 2021 15:19:15 +0000 (08:19 -0700)]
Remove static accesses to options where EnvObj is used (#7330)
This PR removes a bunch of static accesses in places where EnvObj is used now, and we can thus use options().
Andrew Reynolds [Fri, 8 Oct 2021 20:32:24 +0000 (15:32 -0500)]
Make skolem definition manager robust to function skolems (#7327)
This led to a model soundness issue in a development branch that reorganizes theory preprocessing.
This ensures that skolem definition manager looks for skolems that appear in operators.
This is important for inputs like:
(declare-fun h (Int) Int)
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(assert (= h (ite A f g)))
(assert (= (h 0) ...)))
Andrew Reynolds [Fri, 8 Oct 2021 20:23:15 +0000 (15:23 -0500)]
Add argument to distinguish lemmas and input assertions (#7326)
Work towards virtual clause deletion, where lemmas will be SAT-context dependent.
This adds an argument to the decision engine so it can distinguish lemmas from input assertions.
Andrew Reynolds [Fri, 8 Oct 2021 16:36:55 +0000 (11:36 -0500)]
A few more miscellaneous uses of EnvObj (#7325)
Gereon Kremer [Fri, 8 Oct 2021 11:02:51 +0000 (04:02 -0700)]
Ignore zip files for docs upload diff (#7322)
This fixes the diff mechanism to detect whether the current PR changes the documentation. It ignores zip files now, i.e. the javadoc search index files.
Gereon Kremer [Fri, 8 Oct 2021 10:46:47 +0000 (03:46 -0700)]
Attach the static binaries to a release (#7324)
This adds another step to our CI pipeline that uploads the binary build by some of the jobs to a release.
Andrew Reynolds [Thu, 7 Oct 2021 20:10:26 +0000 (15:10 -0500)]
Move preprocessor to smt solver (#7321)
This breaks the circular dependency of preprocessing pass context of solver engine.
It also moves the preprocessor to be owned by SMT solver, instead of Solver engine.
It also changes the behavior of reset assertions: now, the preprocessing pass context is reset, whereas previously it was not. I believe this is the right behavior, as it eliminates stale data (e.g. learned literals, symbols in assertion cache).
Gereon Kremer [Thu, 7 Oct 2021 18:26:31 +0000 (11:26 -0700)]
Add a binary / SMT-LIB quickstart (#7315)
This PR adds a binary/SMT-LIBv2 quickstart example, based on the cpp quickstart example.
Andrew Reynolds [Thu, 7 Oct 2021 17:45:50 +0000 (12:45 -0500)]
Finish the LFSC printer (#7285)
This adds the remaining implementation of the LFSC printer.
It also corrects a bug introduced during merging the last PR.
The printer will be connected to the proof manager in a follow up PR. It will also be extended with support for DSL proof rule printing when the infrastructure is added.
Andrew Reynolds [Thu, 7 Oct 2021 16:49:41 +0000 (11:49 -0500)]
Use skolem lemma in prop layer interfaces (#7320)
Gereon Kremer [Thu, 7 Oct 2021 14:51:09 +0000 (07:51 -0700)]
Add new versioning scheme (#7253)
This introduces a new versioning mechanism that allows for better automation.
Andrew Reynolds [Thu, 7 Oct 2021 12:18:08 +0000 (07:18 -0500)]
Make the cardinality of the alphabet of strings configurable (#7298)
This adds an option to change the cardinality of the alphabet of strings. The alphabet of strings is always a prefix of the interval of unicode code points in the string standard.
mudathirmahgoub [Thu, 7 Oct 2021 11:29:28 +0000 (06:29 -0500)]
Add missing functions in Term.java (#7297)
This adds recent API functions that were added to terms.
It also uses BigInteger now for integer terms.
Gereon Kremer [Thu, 7 Oct 2021 10:59:50 +0000 (03:59 -0700)]
Fix/Improve static and shared builds with CLN or Poly (#7306)
We already created two dependency targets `GMP_SHARED` and `GMP_STATIC`, as we could not use `libgmp.a` for shared linking (as it is built without `-fPIC`). This PR fixes our handling of CLN and Poly: they would always link with `GMP_STATIC`, leading to having both `GMP_SHARED` and `GMP_STATIC` in the linker command line in certain situations. We now also have `*_SHARED` and `*_STATIC` for both CLN and Poly.
Andrew Reynolds [Thu, 7 Oct 2021 09:53:59 +0000 (04:53 -0500)]
Miscellaneous fixes from proof-new (#7313)
Includes a few fixes for strings and datatypes theory lemma proofs.
Andrew Reynolds [Thu, 7 Oct 2021 09:41:01 +0000 (04:41 -0500)]
Fast exit for string extended equality rewriter (#7312)
In benchmarks with many string equalities between variables and constants, a significant portion of the run time is spent on extended equality rewriting. This adds a fast exit when the equality is between variable/constants only.
Gereon Kremer [Thu, 7 Oct 2021 03:03:17 +0000 (20:03 -0700)]
Replace doubles by rationals in C++ quickstart (#7317)
This PR removes the conversion of rationals to double in favour of properly handling them as rationals (as pairs of integers) in the C++ quickstart example.
Andrew Reynolds [Thu, 7 Oct 2021 01:16:20 +0000 (20:16 -0500)]
Eliminate more circular dependencies on solver engine (#7311)
This is work towards replacing our old dump infrastructure. This PR also does some initial reorganization towards printing assertions using the print benchmark utility.
Gereon Kremer [Thu, 7 Oct 2021 00:37:08 +0000 (17:37 -0700)]
Change behaviour of Term::getRealValue() (#7316)
This PR modifies the API function Term::getRealValue() to always return a fraction. Beforehand, it would return rationals in fractional notation (15/2) and integers in decimal notation (2.0).
Gereon Kremer [Wed, 6 Oct 2021 23:12:46 +0000 (16:12 -0700)]
Change semantics of dumpUnsatCoresFull (#7314)
This PR changes --dump-unsat-cores-full to --print-unsat-cores-full.
It also makes it so that solely having --dump-unsat-cores-full no longer automatically prints unsat cores.
Andrew Reynolds [Wed, 6 Oct 2021 16:45:13 +0000 (11:45 -0500)]
Refactor skolem definitions notifications for the decision engine (#7310)
These changes are taken from the SAT relevancy branch. This does not change the behavior of the current code, it breaks the dependency of decision engine on the skolem definition manager and makes the latter solely managed by TheoryProxy.
This is in preparation for virtual clause deletion.
Gereon Kremer [Wed, 6 Oct 2021 16:27:33 +0000 (09:27 -0700)]
Enable static builds in CI (#7281)
This PR modifies our CI builds to have two static production builds. These binaries will be used as release artifacts later.
Gereon Kremer [Wed, 6 Oct 2021 15:55:55 +0000 (08:55 -0700)]
Remove timestamped javadoc comments (#7304)
This PR also removes the javadoc timestamps from index.html, which for some reason does not honor the -notimestamp option.
Andrew Reynolds [Wed, 6 Oct 2021 15:12:17 +0000 (10:12 -0500)]
Eliminate more hard coded uses of user context (#7309)
This is in preparation to make the "lemma context" configurable.
Abdalrhman Mohamed [Wed, 6 Oct 2021 00:41:05 +0000 (19:41 -0500)]
Avoid calling `quoteSymbol` multiple times. (#7307)
Calling `quoteSymbol(...)` twice on an empty string `""` returns `"|__|"`.
Gereon Kremer [Tue, 5 Oct 2021 20:06:53 +0000 (13:06 -0700)]
First round of refactoring on NlModel (#7255)
This PR performs a first refactoring on the NlModel class. It improves model value computation, comparison and stores the model substitutions in a map (instead of two vectors).
Gereon Kremer [Tue, 5 Oct 2021 16:45:08 +0000 (09:45 -0700)]
Reformulate (#7305)
Gereon Kremer [Tue, 5 Oct 2021 00:16:18 +0000 (17:16 -0700)]
Finish refactoring on option handlers (#7295)
This PR finishes refactoring on the option handlers.
Gereon Kremer [Mon, 4 Oct 2021 23:46:49 +0000 (16:46 -0700)]
Add sygus examples to documentation (#7303)
For some reason, we didn't have any SMT-LIB (or rather SyGuS) example files for the SyGuS examples yet.
This PR adds these missing examples.
Gereon Kremer [Mon, 4 Oct 2021 20:59:28 +0000 (13:59 -0700)]
Various improvements to documentation (#7283)
This PR adds a couple of improvements to our documentation setup
- add an explicit dependency on the extension so that sphinx rebuilds pages appropriately when an extension is modified
- sphinx now emits warnings for examples that are not implemented in all languages (smt2, cpp, java and python)
- add -v to make the sphinx output more log-file friendly
- avoid a warning when the java bindings (and thus java docs) are not build
- replace file(WRITE by configure_file to avoid rather common erroneous rebuilds of python docs
- fix a reference to a label in the python docs
- suppress timestamps in javadoc output to avoid docs-ci being triggered for every PR
- improve placeholder message when java bindings are disabled
Andrew Reynolds [Mon, 4 Oct 2021 19:47:13 +0000 (14:47 -0500)]
Refactor internally generated bounded quantified formulas (#7291)
This changes the attribute on internally generated bounded quantified formulas from `isInternal` to `isQuantBounded`. This makes it clear that bounded integers is the module that should process them. It also moves the utility for constructing these quantified formulas from strings to BoundedIntegers itself. This is to accommodate other theories, e.g. bags, that may make use of reductions to bounded quantifiers.
Andrew Reynolds [Mon, 4 Oct 2021 19:00:09 +0000 (14:00 -0500)]
Move isFiniteType from theory engine to Env (#7287)
In preparation for breaking more dependencies on TheoryEngine.
Andrew Reynolds [Mon, 4 Oct 2021 18:32:20 +0000 (13:32 -0500)]
Make decision engine use env (#7300)
Gereon Kremer [Mon, 4 Oct 2021 18:05:59 +0000 (11:05 -0700)]
No longer build docs by default. Use make docs. (#7296)
This PR changes our policy when to build the documentation. Beforehand, make docs was included in make and make all.
Now, you need to run make docs explicitly.
Andrew Reynolds [Mon, 4 Oct 2021 17:54:58 +0000 (12:54 -0500)]
Eliminating static calls to rewriter in quantifiers (#7301)
Andrew Reynolds [Mon, 4 Oct 2021 17:42:39 +0000 (12:42 -0500)]
Eliminating static calls to rewriter from strings (#7302)
mudathirmahgoub [Fri, 1 Oct 2021 23:21:02 +0000 (18:21 -0500)]
Update java examples using the new Java API (#7225)
This PRs updates java examples using the new Java API, by converting C++ examples to Java.
Examples CVC4Streams.java and PipedInput.java are removed since they are not longer supported by the API.
All examples are not included in the build which would be added in a future PR.
Andrew Reynolds [Fri, 1 Oct 2021 21:47:02 +0000 (16:47 -0500)]
Update theory preprocessor to use Env (#7288)
In preparation for making the "lemma context" configurable.
Andrew Reynolds [Fri, 1 Oct 2021 21:38:15 +0000 (16:38 -0500)]
Fix ascription check for return types on ordinary functions (#7290)
Fixes #7274.
Andrew Reynolds [Fri, 1 Oct 2021 21:19:01 +0000 (16:19 -0500)]
Make preregistration safe for uninterpreted constants (#7292)
Work towards addressing #6908.
Gereon Kremer [Fri, 1 Oct 2021 20:59:07 +0000 (13:59 -0700)]
Remove (apparently obsolete) checks in cms config (#7294)
This removes checks from the CryptoMiniSat config for the existence of a couple of static libraries. Apparently, these are not necessary any more.
Gereon Kremer [Fri, 1 Oct 2021 20:40:05 +0000 (13:40 -0700)]
Clean options handlers (#7201)
Some cleanup on the option handlers, starting with handlers for base and main options.
Gereon Kremer [Fri, 1 Oct 2021 19:40:15 +0000 (12:40 -0700)]
Fix some python docstrings which lead to sphinx warnings (#7293)
This PR fixes some docstrings that are not properly indented for sphinx.
Andrew Reynolds [Fri, 1 Oct 2021 14:07:34 +0000 (09:07 -0500)]
Add the LFSC printer (#7158)
This adds the LFSC printer for proof nodes. This PR has been split to not include support for DSL rewrite rules yet, or its main print method which will be added in a followup PR.
Further PRs will connect this printer as a possible output format for cvc5.
Andrew Reynolds [Fri, 1 Oct 2021 13:58:14 +0000 (08:58 -0500)]
Add the print benchmark utility (#7196)
This utility is capable of printing a vector of Node as a valid (SMT-LIB) benchmark with no prior bookkeeping. It also optionally allows for taking a vector Node corresponding to define-fun.
It will be used to replace the old internal benchmark dumping infrastructure which was error prone.
Andrew Reynolds [Fri, 1 Oct 2021 04:49:08 +0000 (23:49 -0500)]
Use the proper evaluator for optimized SyGuS datatype rewriting (#7266)
This updates the datatypes rewriter to use the evaluator from Env instead of creating local copies of Evaluator. This makes all uses of the Evaluator dependent on the proper options (e.g. which will be based later on the cardinality of the alphabet for strings).
This moves one utility method (sygusToBuiltinEval) to the datatypes rewriter, as it uses an Evaluator that will be dependent on options.
Notice that this is another instance where it is important for us to make the cache for the rewriter local. The same issue occurs for other places where rewriting is dependent on options. This issue will be revisited when the option for strings alphabet cardinality is added.
Aina Niemetz [Fri, 1 Oct 2021 01:57:24 +0000 (18:57 -0700)]
Rename SmtEngine to SolverEngine. (#7282)
Aina Niemetz [Thu, 30 Sep 2021 21:14:59 +0000 (14:14 -0700)]
Rename files smt_engine.(cpp|h) to solver_engine.(cpp|h). (#7279)
This is in preparation for renaming SmtEngine to SolverEngine.
Gereon Kremer [Thu, 30 Sep 2021 20:34:33 +0000 (13:34 -0700)]
Integrate javadoc documentation (#7278)
This PR adds the cmake setup to generate javadoc documentation for the java API and integrates it into the sphinx documentation. Right now, we simply link to the javadoc. This PR also modifies a bunch of javadoc comments to use proper javadoc syntax.
Mathias Preiner [Thu, 30 Sep 2021 20:07:38 +0000 (13:07 -0700)]
configure: Fix --static flag. (#7280)
Mathias Preiner [Thu, 30 Sep 2021 19:52:09 +0000 (12:52 -0700)]
bv: Refactor ppRewrite and move to TheoryBV. (#7271)
This commit moves and refactors the ppRewrite() and ppStaticLearn() code from the layered solver to TheoryBV in order to apply a default set of preprocessing rules for each solver. BV solver can still implement additional rules.
Note: Some of the rewrite rules in ppRewrite() have been removed since cluster runs showed that they don't improve anything, but actually makes the solver a lot worse.
Gereon Kremer [Thu, 30 Sep 2021 19:15:24 +0000 (12:15 -0700)]
Refactor our static builds (#7251)
This PR does a major refactoring on how we organize our builds to allow both shared and static builds. We now build the libraries using object libraries to allow building the libraries both dynamically and statically in the same build folder, though the static library is optional (ENABLE_STATIC_LIBRARY). The binary is linked either dynamically or statically (depending on ENABLE_STATIC_BINARY).
Mathias Preiner [Thu, 30 Sep 2021 17:20:04 +0000 (10:20 -0700)]
Properly cache assertions in static learning preprocessing pass. (#7242)
The cache is user-context dependent and guarantees that ppStaticLearn is only called once per assertion in a given context - if assertions are popped from the context and added again ppStaticLearn is called again on that assertion. Further, the preprocessing pass now also handles the splitting of top-level AND terms. Before that each theory was responsible for splitting and caching. Refactoring the corresponding ppStaticLearn theory methods will be part of future PRs.
Marking do-not-merge until cluster runs finished.
mudathirmahgoub [Thu, 30 Sep 2021 17:07:39 +0000 (12:07 -0500)]
Finish the Java Api (#6396)
This commit finishes the implementation of the Java API.
It also includes all java files in the build along with their unit tests.
Andrew Reynolds [Thu, 30 Sep 2021 16:48:12 +0000 (11:48 -0500)]
Make theory engine modules use Env (#7277)
This updates several core modules of TheoryEngine to use Env and eliminates some getters from TheoryEngine.
Andrew Reynolds [Thu, 30 Sep 2021 15:38:44 +0000 (10:38 -0500)]
Simplify the syntax and representation of the separation logic empty heap constraint (#7268)
Since ~1 year ago, we insist that the location and data types of the separation logic heap are set upfront, analogous to the set-logic command. This means that the separation logic empty heap constraint does not need to be annotated with its types.
This makes SEP_EMP a nullary Boolean operator instead of binary predicate (taking dummy arguments whose types specify the heap type). It changes the smt2 extended syntax from (_ emp T1 T2) to sep.emp.
Gereon Kremer [Thu, 30 Sep 2021 13:59:52 +0000 (06:59 -0700)]
Remove usage of static options in arithmetic theory (#7221)
This PR removes the usage of static accesses to options from the arithmetic theory, mostly by making more classes inherit from EnvObj.
Abdalrhman Mohamed [Thu, 30 Sep 2021 02:59:18 +0000 (21:59 -0500)]
Print `str.is_digit` and `int.pow2` correctly. (#7276)
Andres Noetzli [Thu, 30 Sep 2021 02:37:22 +0000 (19:37 -0700)]
[Printer] Only quote `set-info` value if necessary (#7262)
PR #7240 changed the printing of set-info to always include quote the
value. This commit changes the policy to only quote a symbol if
necessary using existing an existing helper method. Otherwise,
(set-info :status sat) is for example printed as (set-info :status |sat|), which is a bit unusual and may break certain scripts.
Andres Noetzli [Wed, 29 Sep 2021 22:06:36 +0000 (15:06 -0700)]
[API] Update comments w.r.t. SymFPU, fix typos (#7263)
Previously, SymFPU was an optional dependency but it is now required.
The comments in the API were not updated to reflect that. This commit
fixes the comments.
Abdalrhman Mohamed [Wed, 29 Sep 2021 21:32:31 +0000 (16:32 -0500)]
Remove support for extended `(check-sat <term>)` command. (#7270)
This commit removes support for the extended `(check-sat <term>)` command which overlaps in functionality with the standard `(check-sat-assuming (<prop_literal>*))` command.
Andrew Reynolds [Wed, 29 Sep 2021 21:23:27 +0000 (16:23 -0500)]
Properly restrict PBE symmetry breaking for abduction queries (#7269)
This ensures we infer when a conjecture is PBE based on the conjecture plus the side condition for abduction. This fixes issues where the sygus solver was over-pruning solutions for abduction queries.
It also changes the names of internal symbols used for abduction/interpolation queries. These names are used when the experimental sygus-stream is used. These symbols are changed (from "A") to avoid confusion with user symbols.
Andrew Reynolds [Wed, 29 Sep 2021 18:40:08 +0000 (13:40 -0500)]
Update the syntax for tuples in smt2 (#7265)
This changes mkTuple -> tuple and tupSel -> tuple_select.
This is in line with the most recent syntax for tuples in preparation for the theory of tables in smt2.
Andrew Reynolds [Wed, 29 Sep 2021 15:39:50 +0000 (10:39 -0500)]
Add the strings array solver (#7232)
This adds the arrays subsolver utility. It does not yet connect it down to the core array solver, or up to TheoryStrings.
It adds implementation of its lemma schemas for processing nth/update over concat.
Andres Noetzli [Wed, 29 Sep 2021 04:41:37 +0000 (21:41 -0700)]
Update `--lang=help` (#7260)
Support for the CVC language was removed in #7219 but the help message
for languages was not updated. This removes the mention of CVC from the
help message.
mudathirmahgoub [Wed, 29 Sep 2021 03:28:36 +0000 (22:28 -0500)]
Add Statistics and Stat to the Java API (#7243)
This adds Statistics and Stat to the Java API
Gereon Kremer [Wed, 29 Sep 2021 03:10:45 +0000 (20:10 -0700)]
remove stuff (#7258)
This PR removes the BUILD_LIB_ONLY cmake option, and the associated --lib-only configure script option.
If you only want the library, just run make cvc5 instead of make.
Mathias Preiner [Wed, 29 Sep 2021 02:59:47 +0000 (19:59 -0700)]
contrib: Fix check for get-script-header.sh. (#7259)
PR #7219 removed CVC language support and therefore also the file src/parser/cvc/Cvc.g. This commit fixes the check (and the nightlies).
mudathirmahgoub [Wed, 29 Sep 2021 00:30:24 +0000 (19:30 -0500)]
Add Sort.java to the java API (#6382)
This adds Sort.java SortTest.java and cvc5_Sort.cpp to the java api.
Gereon Kremer [Tue, 28 Sep 2021 23:20:24 +0000 (16:20 -0700)]
Remove linking against RT (#7257)
This PR removes long obsolete cmake code that is only required when using a pre-2013 glibc.
Andrew Reynolds [Fri, 24 Sep 2021 05:11:24 +0000 (00:11 -0500)]
Eliminate calls to Rewriter::rewrite from strings entailment checks (#7203)
There are a few further circular references that prevent us from not passing Rewriter to the strings TheoryRewriter constructor, this can be cleaned in future PRs.
Andrew Reynolds [Thu, 23 Sep 2021 23:50:16 +0000 (18:50 -0500)]
Generalize string enumerator for fixed length sequences (#7234)
This adds a utility to get enumerators for fixed length constants of a given sequence type.
This will be used to construct fixed length gaps in array models.
Gereon Kremer [Thu, 23 Sep 2021 23:14:08 +0000 (16:14 -0700)]
Eliminate Output macro in favor of simple Env functions (#7223)
This PR eliminates the Output macro together with the associated output stream (stored in a static variable). It is replaces by a set of simple utility functions of the Env class, and we instead use the output stream from options.base.out.
To achieve this, a couple of quantifier classes are now derived from EnvObj.
Lachnitt [Thu, 23 Sep 2021 22:35:32 +0000 (15:35 -0700)]
[proofs[ Alethe: Fix Order of Arguments of addAletheStepFromOr (#7237)
Changes the order of the arguments of addAletheStepFromOr to be consistent with addAletheStep.
Lachnitt [Thu, 23 Sep 2021 22:08:31 +0000 (15:08 -0700)]
[proofs] Alethe: Translate THEORY_REWRITE (#7236)
Implementation of the translation of THEORY_REWRITE rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
Lachnitt [Thu, 23 Sep 2021 21:46:05 +0000 (14:46 -0700)]
[proofs] Alethe: Add Alethe Files to be Compiled (#7241)
Adds Alethe proof rule and option. Adds alethe_post_processor and alethe_proof_rule files to list of files to be compiled.
During incorporating these changes errors occurred in the SCOPE rule that are also fixed in this PR.
Gereon Kremer [Thu, 23 Sep 2021 21:20:42 +0000 (14:20 -0700)]
Refactor check interface of nonlinear extension (#7235)
This PR does a first step for refactoring the main check interface of the nonlinear extension. It does not change anything yet, but merely moves code around.
Andrew Reynolds [Thu, 23 Sep 2021 18:54:03 +0000 (13:54 -0500)]
More uses of EnvObj (#7230)
Lachnitt [Thu, 23 Sep 2021 17:38:27 +0000 (10:38 -0700)]
[proofs] Alethe: Translate SCOPE rule (#7224)
Implementation of the translation of SCOPE rules into the Alethe calculus.
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>