| Age | Commit message (Collapse) | Author |
|---|
|
Added the operator choice to Smt2.g and Cvc.g.
Removed the unused parameter hasBoundVars from TheoryModel::getModelValue
|
|
This commit should fix the nightlies.
|
|
CVC4 supports `bv2nat` and `int2bv` to convert bit-vectors to/from
integers. Those operators are not standard. This commit only enables
those operators when parsing is non-strict and both bit-vectors and
integers are enabled in the logic. To achieve this, the commit
simplifies the handling of logics in the parser: Instead of defining a
separate `Logic` enum in the `Smt2` class, we simply use `LogicInfo`
directly.
|
|
CVC4 was printing success when `--force-logic` was used because
internally, `--force-logic` generates a `SetBenchmarkLogicCommand`. This
caused issues with the SMT-COMP trace executor. This commit fixes the
behavior by muting the command if it was not issued by the user.
The issue was likely introduced with #3062.
|
|
The `--force-logic` command line argument can be used to override a
logic specified in an input file or to set a logic when none is given.
Before this commit, both the `SmtEngine` and the parser were aware of
that argument. However, there were two issues if an input file didn't
specify a logic but `--force-logic` was used:
- Upon parsing `--force-logic`, the `SmtEngine` was informed about it
and set the logic to the forced logic. Then, the parser detected that
there was no `set-logic` command, so it set the logic to `ALL` and
emitted a corresponding warning. Finally, `SmtEngine::setDefaults()`
detected that `forceLogic` was set by the user and changed the logic
back to the forced logic. The warning was confusing and setting the
logic multiple times was not elegant.
- For eager bit-blasting, the logic was checked before resetting the
logic to the forced logic, so it would emit an error that eager
bit-blasting couldn't be used with the logic (which was `ALL` at that
point of the execution). This was a problem in the competition because
our runscript parses the `set-logic` command to decide on the
appropriate arguments to use and passes the logic to CVC4 via
`--force-logic`.
This commit moves the handling of `--force-logic` entirely into the
parser. The rationale for that is that this is not an API-level issue
(if you use the API you simply set the logic you want, forcing a
different logic in addition doesn't make sense) and simplifies the
handling of the option (no listeners need to be installed and the logic
is set only once). This commit also removes the option to set the logic
via `(set-option :cvc4-logic ...)` because it complicates matters (e.g.
which method of setting the logic takes precedence?). For the CVC and
the TPTP languages the commit creates a command to set the logic in
`SmtEngine` when the logic is forced in the parser instead of relying on
`SmtEngine` to figure it out itself.
|
|
The most recent version of SMT-LIB defines bv{add,mul,and,or,xor,xnor}
[0, 1] as left-associative. CVC4 treats all but bvxnor as having
variable arity anyway but the arity check was too strict when using
`--strict-parsing`. This commit changes the strict parsing check. For
bvxnor, it adds code to the parser that expands an application of bvxnor
into multiple applications of a binary bvxnor if needed.
References:
[0] http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml (bvand,
bvor, bvadd, bvmul)
[1] http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV (bvxor, bvxnor)
|
|
When parsing with `--strict-parsing`, we are checking whether the
operators that we encounter have been explicitly added to the
`d_logicOperators` set in the `Parser` class. We did not do that for the
indexed operator `(_ to_fp ...)` (which is represented by the kind
`FLOATINGPOINT_TO_FP_GENERIC`). This commit adds the operator.
|
|
|
|
|
|
|
|
Until now, regression tests were split across tens of different
Makefile.am, which required a lot of code duplication and does not
really seem to be in the spirit of automake. If we want to change the
LOG_COMPILER/LOG_DRIVER for example, we have to change every single
Makefile.am, which is cumbersome (I was able to get something
semi-working by exporting those variables but it didn't seem very
clean). Additionally, it made the output of the regression tests fairly
verbose and split the output across multiple log files. Finally
it also limited parallelism when running the regression tests (this fix lowers
the time it takes to run regression level 1 from 3m to 1m45s on my
machine with 16 threads).
This commit moves all the regression tests into
test/regress/Makefile.tests and changes test/regress/Makefile.am to deal
with this new structure. Finally, it changes how the test summary in
test/Makefile.am is produced: instead of relying on the log files for
the subdirectories, it greps for the test results in the log files of
the individual tests. Not the most elegant solution but we should
probably anyway delegate that task to a Python script at some point.
|
|
* Add regression from pull request #50, which was fixed separately in pull request #1162.
* Improve comment in regression
|
|
With the recent changes to the regress tests, some of the Makefiles were
not in sync anymore. This commit fixes that.
|
|
|
|
|
|
disabled string literal test case for smtlib v2.5
|
|
* support for new commands meta-info, declare-const, echo, get-model,
reset, and reset-assertions
* support for set-option :global-declarations
* support for set-option :produce-assertions
* support for set-option :reproducible-resource-limit
* support for get-info :assertion-stack-levels
* support for set-info :smt-lib-version 2.5
* ascribe types for abstract values (the new 2.5 standard clarifies that
this is required)
* SMT-LIB v2.5 string literals (we still support 2.0 string literals when
in 2.0 mode)
What's still to do:
* check-sat-assumptions/get-unsat-assumptions (still being hotly debated).
Also set-option :produce-unsat-assumptions.
* define-fun-rec doesn't allow mutual recursion
* All options should be restored to defaults with (reset) command.
(Currently :incremental and maybe others get "stuck" due to late driver
integration.)
|
|
9978c259f30b1f4b2c70c04589a309033a6eb1f6
|
