| Age | Commit message (Collapse) | Author |
|---|
|
just in general, and some documentation adjustments.
|
|
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
closes bug 419, fix typo, fix warning
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
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.)
|
|
|
|
|
|
* fix minor issue with s-expr parsing in CVC and SMT grammars
* other minor things
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
* more minor cleanup/doc
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
* Remove defunct --no-theory-registration option
* Point people to Wiki tutorial
* Modernize the cut-release script
* Misc cleanup, documentation
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
workaround option till we fix bug 409. for now, I have kept --wait-to-join to
be default (old behavior). We could technically make --no-wait-to-join the
default when using non-incremental mode, but still possible for problems at
exit I think
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
declare-const
declare-funs
declare-preds
define
simplify
* don't output --help on bad options, just invite user to try --help
* Datatypes from SMT2 parser now name the tester is-cons (e.g.)
* unknown results produce models, --check-model doesn't fail hard for
incorrect unknown models. removed the assert that kept arithmetic
from producing models if it saw nonlinear
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
Other changes:
* fix compile error in smt_engine in debug builds
* add getLogicInfo in smt_engine
* remove "empty-channel" and "disable-lemma-sharing" debug tags
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
* respect output lang
* fix export variable for BOUND_VARIABLE
* support export of SUBRANGE_TYPE
* statistic for lastWinner, other minor stat changes
* fix running of multiple threads on checsat/query
* changes of Assert -> assert which became private
* fix some destruction time order issues
* fix Pickler with AssertionException going private
Fixed by not fixing:
* portfolio+datatypes does not work
- added ExportUnsupportedException to more places, switches
to sequential
(still TODO / decide : not switch silently, but print error)
> note: this exception now needs to be (and is) defined in expr.h
Known issues:
* problems in portfolio+quantifiers
- at least some problems appear to be because of static variables
(will be later "fixed" like the datatypes)
(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.
|
|
* Change --lang smt to mean SMT-LIBv2
* --lang smt1 now means SMT-LIBv1
* SMT-LIBv2 parser now gives helpful error if input looks like v1
* SMT-LIBv1 parser now gives helpful error if input looks like v2
* CVC presentation language parser now gives helpful error if input
looks like either SMT-LIB v1 or v2
* Other associated changes
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
* --early-exit and --no-early-exit command line options (the former is default for all builds except debug builds)
* New SEXPR kind for doing lists of things (we previously used TUPLEs for this purpose, but TUPLEs will be used in future by the datatypes theory, and so cannot have function symbols in them, etc.).
* SMT-LIB compliant output for (set-option :produce-unsat-cores true) and (get-unsat-core)
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
Statistics-printing problem, limited to certain benchmarks).
Mark some unlabeled header files "cvc4_private.h".
Other minor cleanup.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
The external interface (e.g., what's answered by ExprManager::getStatistics() and SmtEngine::getStatistics()) is a snapshot of the current statistics (rather than a reference to the actual StatisticsRegistry).
The StatisticsRegistry is now internal-only. However, it's built as a convenience library so that the parser and driver can use it too (by re-linking against it).
This is part of the ongoing effort to clean up the public interface.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
consistency, error-reporting, and documentation.
|
|
|
|
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
A "command executer" layer between parsing commands and invoking them.
New implementation of portfolio driver splits only when check-sat or query
command is encountered, and then switches back to sequential till the next
one. As side effect, restores functionality of interactive mode and
push/pops.
|
|
College London (via Peter Collingbourne):
cvc4-0001-Look-for-cxxtestgen-as-well-as-cxxtestgen.pl-and-cxx.patch
* better checking for cxxtest
cvc4-0002-Do-not-read-an-additional-command-after-failure.patch
* more correct failure behavior for interactive tools
cvc4-0003-Only-exit-when-encountering-a-CommandFailure.patch
* don't consider "unsupported" as a failure (accepted with modifications)
cvc4-0004-Produce-SMT-LIB-v2-conformant-output-for-get-info.patch
* better get-info responses (accepted with modifications)
These patches will help the group build Boogie support for CVC4.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
|
|
Also some cleanup of option-related exceptions infrastructure.
|
|
1. changes the way options are declared (see http://church.cims.nyu.edu/wiki/Options)
2. moves module-specific options enumerations (SimplificationMode, DecisionMode, ArithUnateLemmaMode, etc.) to their own header files, also they are no longer inside the Options:: class namespace.
3. includes many SMT-LIBv2 compliance fixes, especially to (set-option..) and (get-option..)
The biggest syntactical changes (outside of adding new options) you'll notice are in accessing and setting options:
* to access an option, write (e.g.) options::unconstrainedSimp() instead of Options::current()->unconstrainedSimp.
* to determine if an option value was set by the user, check (e.g.) options::unconstrainedSimp.wasSetByUser().
* ensure that you have the option available (you have to #include the right module's options.h file, e.g. #include "theory/uf/options.h" for UF options)
*** this point is important. If you access an option and it tells you the option doesn't exist, you aren't #including the appropriate options.h header file ***
Note that if you want an option to be directly set (i.e., other than via command-line parsing or SmtEngine::setOption()), you need to mark the option :read-write in its options file (otherwise it's read-only), and you then write (e.g.) options::unconstrainedSimp.set(true).
Adding new options is incredibly simple for primitive types (int, unsigned, bool, string, double). For option settings that you need to turn into a member of an enumerated type, you write a custom "handler" for the option---this is no additional work than it was before, and there are many examples to copy from (a good one is stringToSimplificationMode() in src/smt/options_handlers.h).
Benefits of the new options system include:
1. changes to options declarations don't require a full-source rebuild (you only have to rebuild those sources that depend on the set of options that changed).
2. lots of sanity checks (that the same option isn't declared twice, that option values are in range for their type, that all options are documented properly, etc.)
3. consistency: Boolean-valued option --foo gets a --no-foo automatically, documentation is generated consistently, the option-parsing matches the documented option name, etc.
4. setting options programmatically via SmtEngine::setOption() is enabled, and behaves the same as command-line equivalents (including checking the value is in range, etc.)
5. the notion of options being "set by the user" is now primitive; you can use (e.g.) options::unconstrainedSimp.wasSetByUser() instead of having to use (and maintain) a separate Boolean option for the purpose
I've taken lots of care not to break anything. Hopefully, I've succeeded in that.
|
|
Basically, this involves creating a separate StatisticsRegistry for the
ExprManager and for the SmtEngine. Otherwise, theories register the
same statistic twice. This is a larger problem, though, for creating
multiple instances of theories, and that is unaddressed. Still,
separating out the expr statistics into a separate registry is probably
a good idea, since the expr package is somewhat separate anyway (and in
the short term it allows two SmtEngines to co-exist).
|
|
|
|
See below for details.
* Fix the "assert" name-collision bug (resolves bug #364).
Our identifiers should never be named "assert", as that's a preprocessor
definition in <assert.h>, which is often #included indirectly (so simply
having a policy of not including <assert.h> isn't good enough---one of
our dependences might include it). It was once the case that we didn't
have anything named "assert", but "assert()" has now crept back in.
Instead, name things "assertFoo()" or similar. Thanks to Tim for the
report.
To fix this, I've changed some of Dejan's circuit-propagator code from
"assert()" to "assertTrue()". Ditto for Andy's explanation manager.
Guys, if you prefer a different name in your code, please change it.
* Fix the incorrect parsing of lets in SMT-LIBv2 parser (resolves bug #365).
Inner lets now shadow outer lets (previously, they incorrectly gave an
error). Additionally, while looking at this, I found that a sequential let
was implemented rather than a parallel let. This is now fixed. Thanks to
Liana for the report.
* Remove ANTLR parser generation warnings in CVC parser (resolves bug #314).
* There were a lot of Debug lines in bitvectors that had embedded toString()
calls. This wasted a LOT of time in debug builds for BV benchmarks
(like in "make regress"). Added if(Debug.isOn(...)) guards; much faster
now.
* Support for building public-facing interface documentation only (as opposed
to all internals documentation). Now "make doc" does the public-facing and
"make doc-internals" does documentation of everything. (Along with changes
to the nightly build script---which will now build and publish both types
of Doxygen documentation---this resolves bug #359).
* Fix the lambda typechecking bug (resolves bug #322). Thanks to Andy for the
report (a long long time ago--sorry).
* The default output language for all streams is now based on the current set
of Options (if there is one). This has been a constant annoyance, especially
when stringstreams are used to construct output. However, it doesn't work
for calls from outside the library, so it's mainly an annoyance-fixer for
CVC4 library code itself.
* Add some CVC4_UNUSED markers to local variables in theory_arith.cpp that
are used only in assertions-enabled builds (and thus give warnings in
production builds). This was briefly discussed at the meeting this week.
|
|
\file tags corrected, copyright added to files that had it missing, etc.
I ensured that I didn't change any code with this commit, and even tested on the cluster to be doubly sure:
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4655&reference_id=4646&p=0
|
|
|
|
- include directive works
- no keyword : 'fof', 'cnf', ... can be used for symbols name
- real -> unsorted -> real (for the one that appear, so no bijection bitween real and unsorted)
- same thing for string
But:
- string not distinct by projection to real, not sure if the current state of string theory make them distinct
- filtering in include is not done
- the result is not printed in the TPTP way (currently SMT2 way)
|
|
plowed ahead to the next command). Now the driver exits on the first error, unless it's in interactive mode.
|
|
track; (set-option :print-success true) supported, (exit) causes immediate exit regardless of EOF, etc.
|
|
|
|
* enables decision heuristic (justification) for QF_BV and QF_AUFBV
* disables a failing regression in aufbv (because of equality engine
assert failure trigerred by above change)
* moves around the init procedure smt_engine
* destruction time issues because of moving this -- still to be fixed,
currently get around by not destucting stuff in driver
|
|
condition when reading from stdin. This should completely resolve bug #319.
However, on large inputs especially (like the stp/testcase benchmarks), this inlining feature can speed parsing by 5-10%, at the cost of not supporting interactive sessions on stdin (like in the SMT-COMP application track).
So I updated the submission script and competition build so that
* a competition build with antlr-inlining is built for the main and parallel tracks
* a competition build without antlr-inlining is built for the application track
Again, the effect is only when reading the stdin stream (but that's how SMT-COMP works). For normal (non-competition) builds, we need to support interactive sessions (from e.g. KIND) on stdin, so this inlining is off for all builds except main- and parallel-track competition builds.
Also added a "get-antlr-3.4" script that automatically downloads and locally installs a copy of libantlr3c and the antlr parser generator inside the CVC4 source tree.
Closing bug #319.
|
|
(no performace or search behavior changes expected)
|
|
other C++-level exceptions, we'll exit the C++ way rather than our custom way (so we don't get statistics etc.)
|
|
|
|
Dump("foo") << FooCommand(...);
now "dumps" the textual representation of the command (in the current
output language) to a file, IF dumping is on at configure-time, AND the
"muzzle" feature is off, AND the "foo" flag is turned on for the dump
stream during this run.
If it's a portfolio build, the above will also store the command in a
CommandSequence, IF the "foo" flag is turned on for the dump stream
during this run. This is done even if the muzzle is on.
This commit also cleans up some code that used the dump feature (in arrays,
particularly).
|
|
support incrementality.
Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.
Expected performance change negligible; slightly better on memory:
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!
|
|
|
|
SMT-LIBv1 and SMT-LIBv2 input:
In SMT-LIBv1, you specify the "cvc4_logic" benchmark attribute; for instance:
(benchmark actually_a_sat_benchmark_but_looks_like_uf
:logic QF_UF
:cvc4_logic { QF_SAT }
[...]
In SMT-LIBv2, you use a set-info; for instance:
(set-logic QF_UF)
(set-info :cvc4-logic "QF_SAT")
[...]
Right now, the only thing this does is disable the symmetry breaker for
benchmarks like the above ones.
As part of this work, TheoryEngine::setLogic() was removed (the logic field there
wasn't actually used anywhere, its need disappeared when
Theory::setUninterpretedSortOwner() was provided).
Also, Theory::d_uninterpretedSortOwner got a name change to
Theory::s_uninterpretedSortOwner, to highlight that it is static to the Theory
class. This represents a breakage of our separation goals for CVC4, since it
means that two SmtEngines cannot be created separately to solve a QF_AX and
QF_UF problem. A bug report is pending.
|
|
(Clark-requested change)
|
|
|
|
and SMT-LIBv2).
There are --enable-symmetry-breaker and --disable-symmetry-breaker
options that are always respected regardless of this default.
Expected performance impact: positive
New default (UF only) compared to old default (always on):
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3594&reference_id=3595&p=5
Symmetry breaker remains a big win on UF:
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3594&reference_id=3596&p=5
The last link to results looks at first that the symmetry breaker should
always be turned off, since its use loses more regressions than it gains.
*However*, the lost ones are only our "QF_SAT" benchmarks. For these, we
should indeed turn off the symmetry breaker, but that's impossible for
now because we tag them internally with the logic "QF_UF."
|
|
allows a (limited) form of error recovery, matching what we had previously
|
