| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
Fixes #2517.
This makes the order of theories explicit in the source code rather than relying on the order defined via the build system. Previously, the build system ensured the order of the theories via the KINDS_FILES variable, which is a list of kinds files that is fed to code generation scripts (mkkind, mkmetakind, mkrewriter, mktheorytraits). The generated code critical to the order of theories w.r.t. soundess is the TheoryId enum, and the CVC4_FOR_EACH_THEORY macro. Ideally, we would want to get rid of the latter (ugly and error prone), which is not possible in the current configuration, and to be discussed in the future.
This PR moves the TheoryID enum and related functions to theory/theory_id.h, and the CVC4_FOR_EACH_THEORY macro to theory/theory_engine.cpp, the only place where it is used.
I ran it on whole SMT-LIB (non-incremental and incremental) and did not encounter any soundness issues. The only issue that did occur is not related to these changes, non-critical and known: #2993
|
|
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.
|
|
|
|
This commit moves the code in `rewriterulesCommand` in the SMT2 parser
to the `Smt2` class. Additionally, it creates a `boundVarList` rule to
reduce code duplication.
|
|
This commit moves the code in `sygusCommand` in the SMT2 parser to the
`Smt2` class. The original code was pushing and popping the current
scope inline. This commit adds a class `SynthFunFactory` that takes care
of that upon creation and destruction.
|
|
|
|
|
|
|
|
|
|
|
|
constructors (#3259)
|
|
|
|
This commit removes the SMT1 parser infrastructure and adds the SMT2 translations of the SMT1 regression tests. For now this commit removes regression test regress3/pp-regfile.smt since the SMT2 translation has a file size of 887M (vs. 172K for the SMT1 version).
Fixes #2948 and fixes #1313.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
This cleans up naming of API functions to create first-order constants and variables.
mkVar -> mkConst
mkBoundVar -> mkVar
declareConst is redundant (= mkConst) and thus, in an effort to avoid redundancy, removed.
Note that we want to avoid redundancy in order to reduce code duplication and maintenance
overhead (we do not allow nested API calls, since this is problematic when tracing API calls).
|
|
Fixes 2887.
|
|
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)
|
|
|
|
|
|
parser. (#2874)
|
|
s
|
|
|
|
|
|
|
|
|
|
|
|
Is not required anymore since we don't use autotools anymore.
|
|
|
|
|
