| Age | Commit message (Collapse) | Author |
|---|
|
Fix datatypes E-matching bug. Change defaults : mbqi=fmc, decision heuristic stoponly=false for quantified logics, decision=justification for ALL_SUPPORTED, full-saturate-quant=false. Minor fix for fmc models. Add infrastructure to datatypes to prepare for next commit.
|
|
|
|
Previously, SMT-LIB logics were treated specially, as in SMT-LIB v1.2.
This led to inconsistencies---such as nonstandard logics like "QF_LIRA"
being accepted in set-logic but not providing the "Real" sort. Now,
the LogicInfo is used and queried, so nonstandard logics should work
fine and declare the correct symbols. SMT-LIB v1.2, unfortunately,
can't take advantage of this fully since symbols like "Array" have
substantially different meanings in different logics.
|
|
|
|
|
|
|
|
just the header comments at the top, though. Don't update to this rev if
you don't have time for a complete rebuild, and exclude this rev if you
want to see what's new across a range of commits.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
|
|
* Internal uses of CheckArgument changed to AssertArgument/AlwaysAssertArgument()
* Make util/Assert.h cvc4_private instead of public, so AssertionException and friends are now internal-only
* CheckArgument() throws non-AssertionException
* things outside the core library (parsers, driver) use regular C-style assert,
or a public exception type.
* auto-generated documentation for Smt options and internal options
Also, a small fix to SMT-LIBv1 QF_ABV and QF_AUFBV definitions, which were nonstandard.
|
|
no explicit setLogic(). This is important for the CVC language, where the parser doesn't ensure that setLogic() is called, and for API uses. setLogicInternal() should be called in order to properly set up heuristics, even if the logic is just ALL_SUPPORTED.
This means that the CVC language can now take advantage of statistics.
Also added the ability to set the logic from CVC presentation language via (e.g.)
OPTION "logic" "QF_UFLIA";
Disabled the justification decision heuristic for ALL_SUPPORTED, as it interferes with incrementality. Kshitij may have a fix (I warned him about this commit).
|
|
|
|
SmtEngine resolved.
ALL_SUPPORTED and QF_ALL_SUPPORTED logics now supported by SMT-LIB parsers. In SMT-LIBv2, if a (set-logic..) command is missing, ALL_SUPPORTED is assumed, and a warning is issued, as discussed on the cvc4-devel mailing list.
|
|
QF_UF and maybe others
|
|
src/theory/logic_info.{h,cpp} contains the CVC4::LogicInfo class, which keeps
track of which theories are active (which should remain constant throughout
the life of an SmtEngine) and other details (like integers, reals,
linear/nonlinear, etc.).
This class has a default constructor which is the most all-inclusive logic.
Alternatively, this class can be constructed from an SMT-LIB logic string
(the empty string gives the same as "QF_SAT"). Once constructed, theories
can be enabled or disabled, quantifiers flipped on and off, integers flipped
on and off, etc. At any point an SMT-LIB-like logic string can be extracted.
The SmtEngine keeps a LogicInfo for itself and shares with the TheoryEngine
(and, in turn, the theories) only a const reference to it. This ensures that
the logic info doesn't mutate over the course of the run.
As part of this commit, the TheoryEngine's old notion of "active theories"
has been completely removed. As a result, SMT benchmarks that are incorrectly
tagged with a logic will assert-fail or worse. (We should probably fail
more gracefully in this case.) One such example was bug303.smt2,
which used UF reasoning but was tagged QF_LIA. This has been fixed.
|
