Morgan Deters [Mon, 9 Sep 2013 19:27:22 +0000 (15:27 -0400)]
Fix some line-numbering in auto-generated metakind.h. Thanks to Martin Brain for reporting this.
Morgan Deters [Mon, 9 Sep 2013 19:26:50 +0000 (15:26 -0400)]
Fix portfolio on bug411.smt2. (get-model command should only go to last winner)
Morgan Deters [Mon, 9 Sep 2013 18:41:21 +0000 (14:41 -0400)]
Ensure no cost for datatypes debugging when not tracing it.
Andrew Reynolds [Sat, 7 Sep 2013 02:34:44 +0000 (21:34 -0500)]
Fix datatypes for bug 503
Morgan Deters [Thu, 5 Sep 2013 19:43:47 +0000 (15:43 -0400)]
Fix FLOOR and DISTINCT in CVC language parser.
Morgan Deters [Thu, 5 Sep 2013 14:47:07 +0000 (10:47 -0400)]
Fix lambda handling in CVC parser
Morgan Deters [Fri, 16 Aug 2013 23:41:36 +0000 (19:41 -0400)]
Permit setOption(decision-mode)
Morgan Deters [Thu, 5 Sep 2013 13:37:01 +0000 (09:37 -0400)]
Fix bugs/issues with missed-t-prop dump output
Morgan Deters [Fri, 23 Aug 2013 20:01:13 +0000 (16:01 -0400)]
Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a segfault in smt2 printer
Morgan Deters [Sat, 31 Aug 2013 01:00:56 +0000 (21:00 -0400)]
Add ability to mkConst(TupleSelect) and friends in language bindings
Kshitij Bansal [Mon, 26 Aug 2013 23:48:10 +0000 (19:48 -0400)]
Merge branch '1.2.x'
Kshitij Bansal [Mon, 26 Aug 2013 22:56:39 +0000 (18:56 -0400)]
bug 374 fix: assert litVal=desiredVal only for leaf nodes
Kshitij Bansal [Mon, 26 Aug 2013 22:54:42 +0000 (18:54 -0400)]
Bug 374 benchmarks
Morgan Deters [Tue, 20 Aug 2013 20:32:31 +0000 (16:32 -0400)]
Change recursive expandDefinitions() to an interative worklist-based one; we were blowing the stack. Fixes a segfault reported by Pantazis Deligiannis.
Morgan Deters [Tue, 13 Aug 2013 15:59:26 +0000 (11:59 -0400)]
--segv-nospin is now default.
Morgan Deters [Tue, 13 Aug 2013 21:58:30 +0000 (17:58 -0400)]
Minor cleanup.
Andrew Reynolds [Tue, 13 Aug 2013 21:10:41 +0000 (16:10 -0500)]
Minor fixes for --fmf-fmc for quantifiers containing datatypes
Andrew Reynolds [Mon, 22 Jul 2013 22:59:47 +0000 (17:59 -0500)]
initial modifications for per-ic cbqi
Morgan Deters [Fri, 9 Aug 2013 13:56:50 +0000 (09:56 -0400)]
Clean up "make install"-produced intermediate files (resolves bug 526)
Morgan Deters [Thu, 8 Aug 2013 23:29:50 +0000 (19:29 -0400)]
Fix a serious bug in the preprocessor; problem inputs reported by Pantazis Deligiannis.
Morgan Deters [Thu, 8 Aug 2013 16:23:59 +0000 (12:23 -0400)]
Parameterized, uninterpreted sorts need no Boolean-term conversion
Morgan Deters [Tue, 30 Jul 2013 16:37:04 +0000 (12:37 -0400)]
Minor fixes to build system.
Morgan Deters [Mon, 29 Jul 2013 20:08:45 +0000 (16:08 -0400)]
Fix numerous compiler warnings on various platforms
Morgan Deters [Fri, 19 Jul 2013 17:24:29 +0000 (13:24 -0400)]
Regressions now checking models on unknown too. But quantifiers don't have to be simplified by check-model in that case.
Morgan Deters [Thu, 18 Jul 2013 20:31:20 +0000 (16:31 -0400)]
Fixes for building with mingw win64.
Morgan Deters [Tue, 2 Apr 2013 19:51:44 +0000 (15:51 -0400)]
Don't allow --stats if not a statistics-enabled build
Morgan Deters [Wed, 24 Jul 2013 18:41:29 +0000 (14:41 -0400)]
some portfolio driver cleanup
Morgan Deters [Tue, 23 Jul 2013 20:59:45 +0000 (16:59 -0400)]
Some fixes for (get-info :all-options)
Morgan Deters [Thu, 18 Jul 2013 19:25:15 +0000 (15:25 -0400)]
fix for win32 option parsing via mingw32
Morgan Deters [Tue, 23 Jul 2013 15:55:39 +0000 (11:55 -0400)]
(get-info :all-options) to get option values; also command-line option suggestions
Morgan Deters [Mon, 22 Jul 2013 23:11:59 +0000 (19:11 -0400)]
Allow BV and DT in either order in the logic string
Andrew Reynolds [Mon, 22 Jul 2013 21:04:39 +0000 (16:04 -0500)]
Add option --cbqi-recurse.
Andrew Reynolds [Mon, 22 Jul 2013 19:29:28 +0000 (14:29 -0500)]
Bug fix for --fmf-fmc for non-uninterpreted sort quantifiers, added infrastructure to BV collectModelInfo in preparation for bug fix.
Morgan Deters [Sat, 20 Jul 2013 01:13:24 +0000 (21:13 -0400)]
enable bug521 regression tests
Dejan Jovanovic [Fri, 19 Jul 2013 21:27:40 +0000 (14:27 -0700)]
possible fix for bug 521
Morgan Deters [Fri, 19 Jul 2013 15:13:40 +0000 (11:13 -0400)]
Minor fix for --no-condense-function-values
Andrew Reynolds [Thu, 18 Jul 2013 18:08:56 +0000 (13:08 -0500)]
Fix quantifier instantiation bug in cbqi, add default priorities in rewrite engine.
Morgan Deters [Tue, 16 Jul 2013 22:28:03 +0000 (18:28 -0400)]
Fix bug 516; include some bug testcases.
Liana Hadarean [Tue, 16 Jul 2013 22:59:31 +0000 (17:59 -0500)]
fixed seg fault when bv equality is turned off
Liana Hadarean [Tue, 16 Jul 2013 22:20:09 +0000 (17:20 -0500)]
fixed bug520
Morgan Deters [Tue, 16 Jul 2013 17:42:30 +0000 (13:42 -0400)]
Fix for get-antlr script and PIC/non-PIC objects, on some platforms
Morgan Deters [Tue, 16 Jul 2013 21:29:42 +0000 (17:29 -0400)]
"Tabular"-style function definitions in models with --no-condense-function-values
Morgan Deters [Tue, 16 Jul 2013 21:29:30 +0000 (17:29 -0400)]
Minor bugfixes to model-building
Morgan Deters [Sat, 13 Jul 2013 15:19:53 +0000 (11:19 -0400)]
Remove now-unused language bindings interface file.
Morgan Deters [Sat, 13 Jul 2013 15:04:10 +0000 (11:04 -0400)]
Fix language bindings and portfolio builds.
Morgan Deters [Fri, 12 Jul 2013 22:18:07 +0000 (18:18 -0400)]
Fix for curious GCC 4.8 translation with -O.
Morgan Deters [Wed, 10 Jul 2013 19:05:41 +0000 (15:05 -0400)]
Remove auto-aritization from TPTP parser
Morgan Deters [Mon, 24 Jun 2013 23:58:37 +0000 (19:58 -0400)]
Support for TPTP's TFF0 (with arithmetic)
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.
Morgan Deters [Thu, 11 Jul 2013 20:47:27 +0000 (16:47 -0400)]
Fix for Boolean-term rewriting and LAMBDAs
Morgan Deters [Wed, 10 Jul 2013 01:22:53 +0000 (21:22 -0400)]
Fix for bug 519; don't involve ITESimplifier in model generation.
Andrew Reynolds [Tue, 9 Jul 2013 20:43:28 +0000 (15:43 -0500)]
add relevant domain computation
Morgan Deters [Sun, 7 Jul 2013 00:32:48 +0000 (20:32 -0400)]
Model output is now const; this related to bug 519
Morgan Deters [Fri, 5 Jul 2013 21:25:27 +0000 (17:25 -0400)]
Fix for a datatype parsing bug that Tim found.
Andrew Reynolds [Tue, 2 Jul 2013 19:09:17 +0000 (14:09 -0500)]
Make uf strong solver user-context dependent, fixes bug 522.
Andrew Reynolds [Tue, 2 Jul 2013 18:40:26 +0000 (13:40 -0500)]
Minor fixes for bounded integers, rewrite engine.
Andrew Reynolds [Fri, 28 Jun 2013 20:46:13 +0000 (15:46 -0500)]
More bug fixes for interval models.
Morgan Deters [Fri, 28 Jun 2013 13:09:47 +0000 (09:09 -0400)]
Fix portfolio builds after yesterday's commits.
Morgan Deters [Thu, 27 Jun 2013 22:39:20 +0000 (18:39 -0400)]
Better check-models output for some kinds of problems; add anassertion that the master equality engine is consistent when it needs to be.
This is intended to help root out some recent model-generation bugs.
Morgan Deters [Thu, 27 Jun 2013 21:06:56 +0000 (17:06 -0400)]
Fix minor warnings found by recent clang/gcc.
Morgan Deters [Thu, 27 Jun 2013 19:35:24 +0000 (15:35 -0400)]
Remove output.h from public space, to avoid clashes with symbols defined in users' space.
Specifically, output.h was moved to CVC4's "private-library" rules, which means that it's
not installed on users' machines, and public headers should not include it.
Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.
Morgan Deters [Thu, 27 Jun 2013 19:34:32 +0000 (15:34 -0400)]
Small fix for IS_INTEGER.
Morgan Deters [Thu, 27 Jun 2013 19:01:21 +0000 (15:01 -0400)]
Remove macros EXPECT_TRUE / EXPECT_FALSE from cvc4_public.h so that they don't escape to user space
Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.
Morgan Deters [Thu, 27 Jun 2013 18:55:55 +0000 (14:55 -0400)]
Better user documentation for mkVar() and mkBoundVar().
Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.
Morgan Deters [Thu, 27 Jun 2013 18:42:28 +0000 (14:42 -0400)]
Minor printer cleanup for SMT-LIBv2 symbols "div" and "mod".
Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.
Andrew Reynolds [Wed, 26 Jun 2013 19:40:05 +0000 (14:40 -0500)]
Add support for interval models in bounded integers MBQI (in progress).
Morgan Deters [Tue, 25 Jun 2013 23:53:02 +0000 (19:53 -0400)]
Merge branch '1.2.x'
Morgan Deters [Tue, 25 Jun 2013 23:39:32 +0000 (19:39 -0400)]
Proposed fix for bug #513
Andrew Reynolds [Tue, 25 Jun 2013 17:18:05 +0000 (12:18 -0500)]
Refactoring of model engine to separate individual implementations of model builder. Begin work on interval models for integers. Other minor cleanup.
Morgan Deters [Tue, 25 Jun 2013 00:21:37 +0000 (20:21 -0400)]
Add files missing from last commit
Morgan Deters [Mon, 24 Jun 2013 23:35:58 +0000 (19:35 -0400)]
Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk allows linearization of div,mod,/ by a constant.
Andrew Reynolds [Mon, 24 Jun 2013 17:52:07 +0000 (12:52 -0500)]
Add options for symmetry breaking in uf+ss totality axiom approach, option for using clique lemmas instead of splitting on demand, option for simplifying models in fmf-fmc, minor fixes for rewrite engine
Morgan Deters [Fri, 21 Jun 2013 15:15:57 +0000 (11:15 -0400)]
Fix failure in non-assertion builds on incorrect SmtEngine use.
Morgan Deters [Wed, 19 Jun 2013 22:28:38 +0000 (18:28 -0400)]
Merge branch '1.2.x'
Morgan Deters [Wed, 19 Jun 2013 22:27:42 +0000 (18:27 -0400)]
Workaround for suspected clang 3.0 codegen bug on Mac
Morgan Deters [Wed, 19 Jun 2013 15:11:27 +0000 (11:11 -0400)]
Fix to the "include" extended feature of the SMT-LIB parser
Morgan Deters [Wed, 19 Jun 2013 15:09:49 +0000 (11:09 -0400)]
Give a more useful parse error message for "undeclared variable -1".
Indeed, "-1" is a valid user symbol in SMT-LIB; this commit makes a small
change to the parser to detect when something like "-1" is used but
undeclared, and adds a note to the error message giving the syntax for
unary minus.
Morgan Deters [Mon, 17 Jun 2013 22:36:26 +0000 (18:36 -0400)]
Java streams example I forgot to add a long time ago
Andrew Reynolds [Mon, 17 Jun 2013 20:31:28 +0000 (15:31 -0500)]
Make --var-elim-quant true by default. Add rewrite engine to quantifiers module.
Andrew Reynolds [Sun, 16 Jun 2013 02:00:39 +0000 (21:00 -0500)]
Fix in SMT2 parser for parametric datatypes
Morgan Deters [Mon, 10 Jun 2013 03:11:55 +0000 (23:11 -0400)]
another fix for array-store-all printing
Morgan Deters [Mon, 10 Jun 2013 02:40:23 +0000 (22:40 -0400)]
Better array-store-all output for SMT-LIB.
Morgan Deters [Sat, 8 Jun 2013 23:17:03 +0000 (19:17 -0400)]
Fix typos in alttheoryskel
Morgan Deters [Fri, 7 Jun 2013 15:30:00 +0000 (11:30 -0400)]
Fixes for Boolean terms in arrays (including fix for bug 517).
Morgan Deters [Fri, 7 Jun 2013 21:35:21 +0000 (17:35 -0400)]
One more case for arrays of Boolean.
Morgan Deters [Fri, 7 Jun 2013 15:30:00 +0000 (11:30 -0400)]
Fix for bug 517.
Morgan Deters [Fri, 7 Jun 2013 19:23:36 +0000 (15:23 -0400)]
Allow disabling include-file feature
Dejan Jovanović [Fri, 7 Jun 2013 02:55:24 +0000 (22:55 -0400)]
small parese issue in IDL
Dejan Jovanović [Thu, 6 Jun 2013 19:01:21 +0000 (15:01 -0400)]
typo
Dejan Jovanović [Wed, 5 Jun 2013 20:35:37 +0000 (16:35 -0400)]
IDL example theory (to be used with --use-theory=idl).
Andrew Reynolds [Wed, 5 Jun 2013 16:23:56 +0000 (11:23 -0500)]
Fix bug in --fmf-fmc for producing models of functions not appearing in quantified formulas.
Morgan Deters [Tue, 4 Jun 2013 19:51:42 +0000 (15:51 -0400)]
File inclusion in Smt2 parser.
The extended command (include-file "filename") now includes file content.
Morgan Deters [Tue, 4 Jun 2013 22:09:48 +0000 (18:09 -0400)]
Add --no-condense-function-values option for explicit function models (useful in some applications)
Morgan Deters [Tue, 4 Jun 2013 23:16:54 +0000 (19:16 -0400)]
Merge branch '1.2.x'
Morgan Deters [Tue, 4 Jun 2013 13:10:55 +0000 (09:10 -0400)]
Fix clang static initialization order issue; fixes bug 512.
Andrew Reynolds [Tue, 4 Jun 2013 17:12:30 +0000 (12:12 -0500)]
Add partial support for MBQI with arrays when using --fmf-fmc. Fix constant bounds for bounded integers.
Morgan Deters [Mon, 3 Jun 2013 22:03:12 +0000 (18:03 -0400)]
Merge tag 'casc24'
Morgan Deters [Mon, 3 Jun 2013 22:02:33 +0000 (18:02 -0400)]
Updated CASC scripts, as provided to Geoff Sutcliffe
Morgan Deters [Wed, 29 May 2013 17:03:03 +0000 (13:03 -0400)]
Merge branch '1.2.x'
Morgan Deters [Wed, 29 May 2013 17:02:52 +0000 (13:02 -0400)]
Per SMT-LIB spec, allow (set-info..) command to succeed implicitly with unknown key.
Morgan Deters [Wed, 29 May 2013 13:48:40 +0000 (09:48 -0400)]
SMT-LIB printer updates (some missing cases).