| Age | Commit message (Collapse) | Author |
|---|
|
Thanks to David Cok for pointing out this issue.
Conflicts:
library_versions
|
|
Thanks to David Cok for reporting this issue.
|
|
|
|
|
|
|
|
* update some copyrights for 2013
* cleaned up some comments/ifdefs, indentation
* some spelling corrections
* add some missing makefiles
|
|
|
|
* Fix creation of bound variables in CVC native language parser
* This corrects a problem with misleading model output
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
Also some fixes to parametric datatypes I found, and fixes for a handful of bugs, including some observed with --check-models --incremental on together.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
* remove from public interface (ExprManager, Type)
* CVC parser reports an unimplemented feature error if used
I didn't want to tear it out completely (from NodeManager, TypeNode,
type-checking, pre-processing, etc.) because that's a lot of hassle
and we'll add it back in after the release anyway. It *does* mean
that CVC4::Predicate is in the public interface, but that it can't be
used for anything (by users).
(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.)
|
|
(rather than SAT context)
* Enable part of CVC3 system test (resolves bug 375)
* Fix infinite recursion in beta reduction code (resolves bug 417)
* Some model-building assertions have been added
* Other minor changes
(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.)
|
|
collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models
|
|
* add support for mkBoundVar() (BOUND_VAR_LISTs in quantifiers must be bound vars)
|
|
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).
|
|
* rename DeclarationScope to SymbolTable
* rename all HashStrategy -> HashFunction (which we often have anyways)
* remove CDCircList (no one is currently using it)
|
|
(extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.
|
|
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.
|
|
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.
|
|
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
|
|
* SMT-LIBv2 parser now supports (echo...).
* Dump() gestures can now dump EchoCommands in CVC and SMT-LIB formats.
This can make it much easier to interpret output.
|
|
the branch arithmetic/remove_const_int.
|
|
Changes include
* fixed term visitor from the bvprop branch
* removed all the warnings from builds -- warnings are there to be noted *NOT* to be used as scribbles
* moved the LogicInfo into the theory constructor
|
|
* Permit "BOOL = BOOL" in CVC language parser (auto-replaced with IFF
internally, except in strict mode).
* SExpr atoms now can be string-, integer-, or rational-valued.
* SmtEngine::setInfo(":status", ...) now properly dumps a
SetBenchmarkStatusCommand rather than a SetInfoCommand.
* Some dumping fixes (resolves bug 313)
|
|
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!
|
|
lambdas; resolves bug 294
|
|
Datatypes (bug #283) by Chris Conway. Thanks, Chris!
|
|
SmtEngine::getProof(), a few other things..
|
|
|
|
#define true and false to their own ANTLR3_TRUE and ANTLR3_FALSE, wreaking havoc on our parsers. I'm really fed up with this package.
|
|
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
|
|
infrastructure, and takes care not to affect CVC4's performance on LRA
benchmarks.
|
|
parametric datatype versions of paper benchmarks are now working
|
|
|
|
|
|
parametric datatypes, type ascriptions are not implemented yet
|
|
* Preprocessing-time, non-clausal, Boolean simplification round to
support "quasi-non-linear rewrites" as discussed at last few meetings.
* --simplification=none is the default for now, but we'll probably
change that to --simplification=incremental. --simplification=batch
is also a possibility. See --simplification=help for details.
* RecursionBreaker<T> now uses a hash set for the seen trail.
* Fixes to TLS stuff to support that.
* Fixes to theory and SmtEngine documentation.
* Fixes to stream indentation.
* Other miscellaneous stuff.
|
|
|
|
constructors for Type and Expr (which existed due to ANTLR limitations). These issues are now handled (as a hack, due to said limitations) in the parser rather than the CVC4 core.
|
|
* Type::getCardinality() returns the cardinality for for all types.
Theories give a cardinality in the their kinds file. For
cardinalities that depend on a type argument, a "cardinality
computer" function is named in the kinds file, which takes a
TypeNode and returns its cardinality.
* There's a bitmap for the set of "active theories" in the
TheoryEngine. Theories become "active" when a term that is owned by
them, or whose type is owned by them, is pre-registered (run CVC4
with --verbose to see theory activation). Non-active theories don't
get any calls for check() or propagate() or anything, and if we're
running in single-theory mode, the shared term manager doesn't have
to get involved. This is really important for get() performance
(which can only skimp on walking the entire sub-DAG only if the
theory doesn't require it AND the shared term manager doesn't
require it).
* TheoryEngine now does not call presolve(), registerTerm(),
notifyRestart(), etc., on a Theory if that theory doesn't declare
that property in its kinds file. To avoid coding errors,
mktheorytraits greps the theory header and gives warnings if:
+ the theory appears to declare one of the functions (check,
propagate, etc.) that isn't listed among its kinds file properties
(but probably should be)
+ the theory appears NOT to declare one of the functions listed in
its kinds file properties
* some bounded token stream work
|
|
|
|
* work around a lexer ambiguity in CVC grammar
* add support for tracing antlr parser/lexer
* add parsing support for more language features
* initial parameterized types parsing work to support Andy's work
|
|
|
|
* Fixed hole in arrays typechecking.
* Fixed "make dist".
* Better ouroborous test, and some printer fixes.
* Continued cleanup in CVC parser, removed some warnings.
* Better output.
|
|
Expected performance impact outside of datatypes/CVC parser is
negligible.
* CVC language LAMBDA, functional LET, type LET, precedence fixes,
bitvectors, and arrays, with partial parsing support also for
quantifiers, tuples, subranges, subtypes, and records
* support for complex recursive DATATYPE selectors, e.g.
tree = node(children:ARRAY INT OF tree) | leaf(data:INT)
these are complicated because they have to be left unresolved
at parse time and dealt with in a second pass.
* bugfix for Exprs/Types that occurred when setting them to null
(not Nodes/TypeNodes, just Exprs/Types).
* Cleanup/code review items
|
