summaryrefslogtreecommitdiff
path: root/src/printer
AgeCommit message (Collapse)Author
2013-11-27General pre-release cleanup commitMorgan Deters
* Rename {model,util_model}.{h,cpp} files to match class names * Fix alreadyVisited() issue in TheoryEngine * Remove spurious Message that causes compliance issues * Update copyrights, fix public/private markings in headers * minor comment fixes * remove EXTRACT_OP as a special-case in typechecker * note about rewriters in theoryskel readme * Clean up some compiler warnings * Code typos and spacing
2013-11-26Fix a segfault in the printer infrastructure when called from API and no ↵Morgan Deters
language is set
2013-11-19Add fair strategy for finite model finding multiple sorts --uf-ss-fair.Andrew Reynolds
2013-11-10Flatten libcvc4 build structure; remove some #include interdependencesMorgan Deters
2013-09-18Support for bv2nat/int2bv in parser and BV rewriter.Morgan Deters
2013-09-05Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a ↵Morgan Deters
segfault in smt2 printer
2013-07-11Support for TPTP's TFF0 (with arithmetic)Morgan Deters
This commit reverses an "SZS ontology compliance hack" that was done for CASC-24 this year, and adds a TPTP pretty-printer which is capable of outputting results in the TPTP way (rather than the SMT way). This commit includes minor changes to the Expr package to add obvious missing functionality, and to fix the way expressions with builtin operators are made. These changes are truly a _fix_, the implementation had not been properly aligned with the design vision for some corner cases.
2013-07-06Model output is now const; this related to bug 519Morgan Deters
2013-06-27Minor printer cleanup for SMT-LIBv2 symbols "div" and "mod".Morgan Deters
Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.
2013-06-24Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk ↵Morgan Deters
allows linearization of div,mod,/ by a constant.
2013-06-09another fix for array-store-all printingMorgan Deters
2013-06-09Better array-store-all output for SMT-LIB.Morgan Deters
2013-05-29Merge branch '1.2.x'Morgan Deters
2013-05-29SMT-LIB printer updates (some missing cases).Morgan Deters
2013-05-14Add support for quantifier patterns in smt2 printer.Andrew Reynolds
2013-05-01Fix to dumping re: boolean terms, datatypesMorgan Deters
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-03-26Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javacMorgan Deters
2013-03-22Support for Boolean term conversion in datatypes.Morgan Deters
2013-03-21Some model and printing fixes for defined functions in input.Morgan Deters
2013-03-20Properly |quote| symbols in SMT-LIBv2 output.Morgan Deters
2013-03-14Merge branch '1.0.x'Morgan Deters
2013-03-14fix to build system: #include the proper file when they are in both builds ↵Morgan Deters
and src
2013-02-24added option --model-u-dt-enum for outputting uninterpreted sorts as ↵Andrew Reynolds
datatype enumerations + minor update to array rewriter to improve output for this option, minor refactoring of representative selection for quantifier instantiation, initial draft of disequality propagation option --uf-ss-deq-prop, other refactoring of uf strong solver, fixed bug 496, improvement for fmf enumeration of finite built-in sorts
2013-01-08SMT-LIB get-model output now is easier to machine-parse: contains (model...) ↵Morgan Deters
bracketing
2012-12-18Fix printing of EXISTS in CVC language printerMorgan Deters
2012-12-15Fix printing of EXISTS in CVC language printerMorgan Deters
2012-12-12* fixed bug 481 by adding check for division by 0 in bit-vector division circuitlianah
* added printing for total bit-vector division kinds for debugging purposes
2012-12-01another part of last commitMorgan Deters
2012-11-30internal variables (skolems) aren't printed as part of the modelMorgan Deters
(this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-30Partial fix for bug 435; still needs some effort.Morgan Deters
(this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-27First chunk of boolean-terms support.Morgan Deters
Passes simple tests and doesn't break existing functionality. Still need some work merged in for models. This version enables BV except for pure arithmetic (since we might otherwise need Boolean term support, which uses BV). Tonight's nightly regression run should tell us if/how that hurts performance. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-27Tuples and records merge. Resolves bug 270.Morgan Deters
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.)
2012-11-17* Fix for bug 445 agreed to in meeting 11/13/2012: always dump in ↵Morgan Deters
ALL_SUPPORTED logic * Java bindings fixes: fixed access to ostreams, iterators * Make SmtEngine::setUserAttribute() (and others) take a const string& * Also a few compliance fixes (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-16Fix dumping of array-select expressions in CVC native language.Morgan Deters
Thanks to Wei for the bug report.
2012-11-14Fix for bug 407. mkAnonymousFunction() in the parser no longer uses ':'. CVC ↵Tim King
printer now properly prints LAMBDAs. Model builing now gives bound variables names that can be parsed bypresentation language.
2012-11-12minor bug fixes for quantifiers, added sort inference module (not ready to ↵Andrew Reynolds
be used yet), added new totality lemma option for uf strong solver
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
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.)
2012-10-06* Clean up some options documentationMorgan Deters
* 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.)
2012-10-05Bug-related:Morgan Deters
* ITE removal fixed to be context-dependent (on UserContext). Resolves incrementality bugs 376 and 396 (which had given wrong answers). * some bugfixes for incrementality that Dejan found (fixes bug 394) * fix for bug in SmtEngine::getValue() where definitions weren't respected (partially resolves bug 411, but get-model is still broken). * change status of microwave21.ec.minimized.smt2 (it's actually unsat, but was labeled sat); re-enable it for "make regress" Also: * --check-model doesn't fail if quantified assertions don't simplify away. * fix some examples, and the Java system test, for the disappearance of the BoolExpr class * add copy constructor to array type enumerator (the type enumerator framework requires copy ctors, and the automatically-generated copy ctor was copying pointers that were then deleted, leaving dangling pointers in the copy and causing segfaults) * --dump=assertions now implies --dump=skolems * --dump=assertions:pre-<PASS> and --dump=assertions:post-<PASS> now allow you to dump before/after a particular preprocessing pass. E.g., --dump=assertions:pre-ite-removal or --dump=assertions:post-static-learning. "--dump=assertions" by itself is after all preprocessing, just before CNF conversion. * minor fixes to dumping output * include Model in language bindings Minor refactoring/misc: * fix compiler warning in src/theory/model.cpp * remove unnecessary SmtEngine::printModel(). * mkoptions script doesn't give progress output if stdout isn't a terminal (e.g., if it's written to a log, or piped through less(1), or whatever). * add some type enumerator unit tests * de-emphasize --parse-only and --preprocess-only (they aren't really "common" options) * fix some exception throw() specifications in SmtEngine * minor documentation clarifications
2012-10-05BoolExpr removed and replaced with ExprDejan Jovanović
2012-10-04Implemented array type enumerator, more fixes for modelsClark Barrett
2012-09-28Public interface review items:Morgan Deters
* 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.
2012-09-27* Rename SMT parts (printer, parser) to SMT1Morgan Deters
* 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.)
2012-09-26Finish off SEXPR kind work.Morgan Deters
(this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-24some api changesDejan Jovanović
2012-09-22Separate public-facing and internal-facing interfaces to Statistics.Morgan Deters
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.)
2012-09-21Fixes for datatype dumping and printing. Add a new test case for dumping.Morgan Deters
(this commit was certified error- and warning-free by the test-and-commit script.)
2012-09-21SMT-LIBv2 compliance updates:Morgan Deters
* chainability of =, <, <=, >, >= via the new CHAINABLE kind and TheoryBuiltin rewriter support (resolves bug #383) * with --smtlib2, force interactive mode off by default Also: * fix a few bugs causing crashes * better "alias" processing for options * configure-time fixes to readline detection (this commit was certified error- and warning-free by the test-and-commit script.)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback