ajreynol [Fri, 14 Apr 2017 21:34:59 +0000 (16:34 -0500)]
Fix nullary operator printers, minor.
ajreynol [Fri, 14 Apr 2017 16:06:45 +0000 (11:06 -0500)]
Fix for fmf-fun when the option is set by user command.
Clark Barrett [Thu, 13 Apr 2017 18:57:19 +0000 (11:57 -0700)]
Fix for some compilers
ajreynol [Wed, 12 Apr 2017 21:47:12 +0000 (16:47 -0500)]
Add nullary operator metakind.
ajreynol [Tue, 11 Apr 2017 16:14:42 +0000 (11:14 -0500)]
Bug fix in conjecture generation for --quant-ind.
ajreynol [Fri, 7 Apr 2017 16:22:44 +0000 (11:22 -0500)]
Change option names for nl.
Clark Barrett [Thu, 6 Apr 2017 06:32:12 +0000 (23:32 -0700)]
Merge pull request #143 from FabianWolff/master
Fix several spelling errors
ajreynol [Wed, 5 Apr 2017 18:32:35 +0000 (13:32 -0500)]
Fix bug 698.
ajreynol [Wed, 5 Apr 2017 18:19:21 +0000 (13:19 -0500)]
Fixes for nlAlgSolveSubs.
Andrew Reynolds [Wed, 5 Apr 2017 18:15:31 +0000 (13:15 -0500)]
Merge pull request #145 from 4tXJ7f/fix_lfsc_args
[LFSC] Fix segfault
ajreynol [Wed, 5 Apr 2017 14:56:00 +0000 (09:56 -0500)]
Caching for fun def process, add regression.
Andres Notzli [Sun, 26 Mar 2017 21:39:07 +0000 (23:39 +0200)]
[LFSC] Fix segfault
LFSC did not detect when the number of arguments provided to a side
condition did not match the expected number of arguments, which could
lead to out-of-bounds reads and writes. This commit adds a check and
fixes one of the proof rules that provided the wrong number of
arguments.
ajreynol [Wed, 5 Apr 2017 14:09:55 +0000 (09:09 -0500)]
Remove extraneous portion of an nl regression.
ajreynol [Wed, 5 Apr 2017 14:01:55 +0000 (09:01 -0500)]
Add non-linear regressions, disable nlAlgSubs, do not do rep checking for NONLINEAR_MULT terms. Ensure shared terms have correct model values in non-linear solver.
Fabian Wolff [Tue, 4 Apr 2017 22:47:10 +0000 (00:47 +0200)]
Fix several spelling errors
ajreynol [Tue, 4 Apr 2017 17:54:26 +0000 (12:54 -0500)]
Enable multi-trigger-linear by default, add option.
ajreynol [Tue, 4 Apr 2017 16:21:30 +0000 (11:21 -0500)]
Simplify Theory::collectModelInfo interface to not take deprecated fullModel argument.
ajreynol [Tue, 4 Apr 2017 14:59:45 +0000 (09:59 -0500)]
Do not solve for 0-ary non-constant symbols (for which isVar returns true), add regressions.
Clark Barrett [Tue, 4 Apr 2017 06:17:42 +0000 (23:17 -0700)]
Merge pull request #141 from 4tXJ7f/remove_def
Remove decl. of getStatisticsRegistry(SmtEngine*)
Andrew Reynolds [Mon, 3 Apr 2017 14:38:54 +0000 (09:38 -0500)]
Merge pull request #142 from timothy-king/nlAlgMerge
Adding a model based axiom instantiation scheme for multiplication. M…
Tim King [Mon, 3 Apr 2017 02:29:36 +0000 (19:29 -0700)]
Adding a model based axiom instantiation scheme for multiplication. Merge commit for nlAlgMaster.
Andres Notzli [Fri, 31 Mar 2017 22:02:39 +0000 (15:02 -0700)]
Remove decl. of getStatisticsRegistry(SmtEngine*)
Commit
f4ef7af0a2295691f281ee1604dfeb4082fe229c removed the definition
of getStatisticsRegistry(SmtEngine*) but not the declaration.
ajreynol [Fri, 31 Mar 2017 13:43:29 +0000 (08:43 -0500)]
Add option multi-trigger-linear, minor optimization to E-matching.
Clark Barrett [Thu, 30 Mar 2017 19:49:38 +0000 (12:49 -0700)]
Merge pull request #139 from 4tXJ7f/remove_throw
[Coverity] Remove throw qualifiers in src/smt
Andres Notzli [Wed, 29 Mar 2017 21:27:56 +0000 (23:27 +0200)]
ajreynol [Thu, 30 Mar 2017 14:11:52 +0000 (09:11 -0500)]
Minor fixes for trigger selection max.
ajreynol [Wed, 29 Mar 2017 18:49:51 +0000 (13:49 -0500)]
Add quantifiers options related to model and master equality engine.
PaulMeng [Wed, 29 Mar 2017 14:36:29 +0000 (09:36 -0500)]
Merge pull request #138 from PaulMeng/master
Refactor the standard effort of relational solver
Paul Meng [Wed, 29 Mar 2017 04:08:52 +0000 (23:08 -0500)]
Refactor the standard effort of relational solver
ajreynol [Wed, 29 Mar 2017 03:22:05 +0000 (22:22 -0500)]
Fix bug 787.
Clark Barrett [Wed, 29 Mar 2017 01:29:48 +0000 (18:29 -0700)]
Fix for bug 733
ajreynol [Tue, 28 Mar 2017 21:21:12 +0000 (16:21 -0500)]
Minor refactoring sygus.
ajreynol [Tue, 28 Mar 2017 14:35:43 +0000 (09:35 -0500)]
More work on sygus. Add regress4 to Makefile.
Tim King [Tue, 28 Mar 2017 06:26:34 +0000 (23:26 -0700)]
Fixing a bug for checking whether a node was visited.
Tim King [Tue, 28 Mar 2017 05:15:23 +0000 (22:15 -0700)]
Minor cleanups to ExtTheory.
Tim King [Tue, 28 Mar 2017 03:59:48 +0000 (20:59 -0700)]
Removing the friend class modifier from ExtTheory to Theory.
Clark Barrett [Mon, 27 Mar 2017 20:20:27 +0000 (13:20 -0700)]
Merge pull request #137 from 4tXJ7f/throw_quals
Remove throw qualifiers in type enumerators
Tim King [Mon, 27 Mar 2017 19:26:14 +0000 (12:26 -0700)]
Making the ExtTheory object a private member of Theory.
Tim King [Mon, 27 Mar 2017 17:24:13 +0000 (10:24 -0700)]
Making ppNotifyAssertions take a const vector.
Tim King [Mon, 27 Mar 2017 17:02:11 +0000 (10:02 -0700)]
Moving the CareGraph into its own file.
Tim King [Mon, 27 Mar 2017 16:40:30 +0000 (09:40 -0700)]
Moving the theory::Assertion struct into its own file.
Andres Notzli [Mon, 27 Mar 2017 09:40:45 +0000 (11:40 +0200)]
Tim King [Mon, 27 Mar 2017 04:59:36 +0000 (21:59 -0700)]
Alphabetizing libcvc4_la_SOURCES.
ajreynol [Fri, 24 Mar 2017 14:56:12 +0000 (09:56 -0500)]
Add some regressions. Minor.
ajreynol [Fri, 24 Mar 2017 14:37:13 +0000 (09:37 -0500)]
Refactor model building for quantifiers to be a single pass, simplification. Modify datatypes collect model info to include dt equivalence classes. Further work on sygus. Other minor fixes.
Clark Barrett [Thu, 23 Mar 2017 22:15:56 +0000 (15:15 -0700)]
Fixing warning message.
guykatzz [Thu, 23 Mar 2017 21:13:46 +0000 (14:13 -0700)]
support incremental unsat cores
ajreynol [Wed, 22 Mar 2017 16:15:19 +0000 (11:15 -0500)]
Fix more cases of rewritten explanations in strings for bug 784. Minor.
ajreynol [Wed, 22 Mar 2017 15:58:03 +0000 (10:58 -0500)]
Minor fix for bounded integers.
ajreynol [Wed, 22 Mar 2017 13:52:42 +0000 (08:52 -0500)]
Work on new approach for sygus involving conditional solutions. Refactoring of sygus solver. Bug fix for sygus solution reconstruction.
ajreynol [Tue, 21 Mar 2017 21:39:25 +0000 (16:39 -0500)]
Improve computeCareGraph functions to check shared term equality status once per equivalence class pair.
Andrew Reynolds [Mon, 20 Mar 2017 20:42:16 +0000 (15:42 -0500)]
Merge pull request #135 from PaulMeng/master
fixed cvc4 parser for set complement
Paul Meng [Mon, 20 Mar 2017 18:49:31 +0000 (13:49 -0500)]
fixed cvc4 parser for set complement
Clark Barrett [Sat, 18 Mar 2017 23:20:56 +0000 (16:20 -0700)]
Fix for bug 707.
Clark Barrett [Sat, 18 Mar 2017 20:46:37 +0000 (13:46 -0700)]
Fix to help with bug 717
guykatzz [Fri, 17 Mar 2017 21:11:41 +0000 (14:11 -0700)]
better support for proof production when encountering bool terms: handle the new proof constructs generated by the equality engine.
proof production for bool-array.smt2 passes
Tim King [Thu, 16 Mar 2017 21:06:17 +0000 (14:06 -0700)]
Fixes bug 781. Copy constructor for Expr needed to set the NodeManagerScope.
ajreynol [Thu, 16 Mar 2017 19:19:58 +0000 (14:19 -0500)]
More fixes, features to examples.
ajreynol [Thu, 16 Mar 2017 19:05:23 +0000 (14:05 -0500)]
Minor fixes, always expand applications of lambdas at preprocess.
ajreynol [Thu, 16 Mar 2017 18:24:31 +0000 (13:24 -0500)]
Support for SMT LIB 2.6 syntax declare-datatype and match.
ajreynol [Thu, 16 Mar 2017 16:37:53 +0000 (11:37 -0500)]
Parsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for mkGroundTerm for parametric datatypes. Minor change to run_regression to allow regressions to override input language. Minor refactoring to Cvc.g.
ajreynol [Wed, 15 Mar 2017 21:28:55 +0000 (16:28 -0500)]
Fix regress1 Makefile for rewriterules, fixes bug 783.
Clark Barrett [Wed, 15 Mar 2017 21:00:17 +0000 (14:00 -0700)]
Merge pull request #134 from 4tXJ7f/fix_host
Fix win-build script to use MinGW-w64 by default
ajreynol [Wed, 15 Mar 2017 18:11:08 +0000 (13:11 -0500)]
Allow 0 argument recursive functions. Fixes bug 782.
Andres Notzli [Wed, 15 Mar 2017 08:25:39 +0000 (01:25 -0700)]
Fix win-build script to use MinGW-w64 by default
Previous changes to the win-build script left the script in an
inconsistent state: the script was updated to refer to MinGW-w64 but the
default host was still referring to MinGW.
guykatzz [Tue, 14 Mar 2017 19:52:42 +0000 (12:52 -0700)]
Merge pull request #133 from 4tXJ7f/fix_uninitialized
Fix uninitialized variable
Andres Notzli [Tue, 14 Mar 2017 18:32:26 +0000 (11:32 -0700)]
fix uninitialized variable
Clark Barrett [Tue, 14 Mar 2017 17:40:26 +0000 (10:40 -0700)]
Merge pull request #132 from 4tXJ7f/fix_mingw64
Fix MinGW-w64 build
ajreynol [Fri, 10 Mar 2017 22:36:10 +0000 (16:36 -0600)]
Minor fix for cbqi-all.
guykatzz [Thu, 9 Mar 2017 22:46:33 +0000 (14:46 -0800)]
bug fix
guykatzz [Thu, 9 Mar 2017 20:13:12 +0000 (12:13 -0800)]
better proof support for bools and formulas
Andres Notzli [Wed, 8 Mar 2017 10:50:56 +0000 (02:50 -0800)]
Fix MinGW-w64 build
This commit fixes configure.ac to try to get clock_gettime() from
pthread. Without it, clock_gettime() is detected as missing at
configuration time for MinGW-w64 but exists at compile time, which
causes conflicts. Additionally, this commit updates the helper script
for Windows to use MinGW-w64 by default instead of MinGW.
ajreynol [Tue, 7 Mar 2017 17:17:34 +0000 (11:17 -0600)]
More fixes for printing/parsing sets, fix kind name.
ajreynol [Tue, 7 Mar 2017 15:11:33 +0000 (09:11 -0600)]
Fix cvc parser for set compliment.
ajreynol [Mon, 6 Mar 2017 16:18:17 +0000 (10:18 -0600)]
Do not eagerly construct explanations in relation solver.
ajreynol [Mon, 6 Mar 2017 15:39:03 +0000 (09:39 -0600)]
Support for set compliment and universe set. Simplify approach for sep.nil nodes.
Clark Barrett [Mon, 6 Mar 2017 08:25:26 +0000 (00:25 -0800)]
Adding support for bool-to-bv
Squashed commit of the following:
commit
5197a663eb262afbeb7740f53b5bd27479dccea0
Author: Clark Barrett <barrett@cs.stanford.edu>
Date: Mon Mar 6 00:16:16 2017 -0800
Remove IFF case
commit
2119b25a30ed42eca54f632e7232c9f76ae5755a
Author: guykatzz <katz911@gmail.com>
Date: Mon Feb 20 12:37:06 2017 -0800
proof support for bvcomp
commit
d8c0c0d2c9c92ce06a5033ec0f3f85ea7bda1a22
Author: Clark Barrett <barrett@cs.stanford.edu>
Date: Fri Feb 17 21:09:04 2017 -0800
Added missing cases to operator<< for bv rewrite rules.
commit
0ed797c31d0e66cadc35b2397716c841d1aff270
Author: Clark Barrett <barrett@cs.stanford.edu>
Date: Fri Feb 17 11:43:51 2017 -0800
Added rewrite rules for new bitvector kinds.
commit
3b23dffb317de5559f8a95118fef633f711c114a
Author: Clark Barrett <barrett@cs.stanford.edu>
Date: Mon Feb 13 14:41:49 2017 -0800
First draft of bool-to-bv pass.
ajreynol [Fri, 3 Mar 2017 22:17:24 +0000 (16:17 -0600)]
Fix for collectModelInfo related to finite types + preregistration. Generalize previous fix for sets, minor changes to Datatypes.
ajreynol [Fri, 3 Mar 2017 16:33:03 +0000 (10:33 -0600)]
Another minor fix for sets related to sharing + finite element types.
ajreynol [Thu, 2 Mar 2017 22:40:39 +0000 (16:40 -0600)]
Fixes related to sets.
ajreynol [Thu, 2 Mar 2017 21:24:07 +0000 (15:24 -0600)]
Minor cleanup and reorganization related to last commit.
ajreynol [Thu, 2 Mar 2017 20:45:21 +0000 (14:45 -0600)]
Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
ajreynol [Thu, 16 Feb 2017 22:19:51 +0000 (16:19 -0600)]
Minor fixes for relations, quantifiers dsplit.
ajreynol [Thu, 16 Feb 2017 19:26:10 +0000 (13:26 -0600)]
Fixes for sets+rels check. Minor.
ajreynol [Wed, 15 Feb 2017 17:26:56 +0000 (11:26 -0600)]
Minimization modes for fmf bound.
ajreynol [Tue, 7 Feb 2017 19:26:57 +0000 (13:26 -0600)]
Generalize finite bound inference to unifiable variables in set membership literals.
ajreynol [Mon, 30 Jan 2017 17:20:29 +0000 (11:20 -0600)]
Fix regexp cache issue in strings, add regression.
Andres Noetzli [Wed, 4 Jan 2017 17:20:34 +0000 (09:20 -0800)]
Fix non-idempotent rewrite in Array rewriter
This commit fixes bug 637 (
http://church.cims.nyu.edu/bugzilla3/show_bug.cgi?id=637 ) as
proposed in Bugzilla and adds the minified test case to the
regression tests.
Andrew Reynolds [Wed, 18 Jan 2017 19:32:55 +0000 (13:32 -0600)]
Merge pull request #128 from 4tXJ7f/fix_lfsc_perf
[LFSC] Fix performance issues, more determinism
ajreynol [Wed, 18 Jan 2017 18:39:24 +0000 (12:39 -0600)]
Minor fix in relations.
Andres Notzli [Tue, 10 Jan 2017 22:23:22 +0000 (01:23 +0300)]
[LFSC] Fix performance issues, more determinism
For certain proofs, the performance was drastically different on
different OSes. The cause for this difference was a pointer comparison
in the deduplication in `Expr::defeq()`. Depending on how the OS
allocated the memory, an expression `a` would get replaced with an
equivalent expression `b` or vice versa, which in turn affected
performance of `Expr::free_in()` dramatically (sub-second vs. >5 min
running times). This commit makes the process more deterministic by
using a heuristic that favors symbolic expressions and greedily tries to
make small refcounts smaller when replacing, and changes
`Expr::free_in()` to not repeatedly explore the same subexpressions.
Clark Barrett [Sat, 14 Jan 2017 05:23:42 +0000 (21:23 -0800)]
Fix call to SExpr constructor for greater portability.
Clark Barrett [Sat, 14 Jan 2017 04:18:16 +0000 (20:18 -0800)]
Merge pull request #130 from chadbrewbaker/master
Fixing memory leak
ajreynol [Fri, 13 Jan 2017 15:40:15 +0000 (09:40 -0600)]
Do not rewrite explanations in strings.
Clark Barrett [Wed, 11 Jan 2017 22:20:22 +0000 (14:20 -0800)]
Merge pull request #129 from timothy-king/regression-scrubber
Adding regression test scrubbing.
Clark Barrett [Wed, 11 Jan 2017 22:03:11 +0000 (14:03 -0800)]
Merge pull request #131 from makaimann/fix_702
Proposed fix for bug 702
makaimann [Wed, 11 Jan 2017 21:47:06 +0000 (13:47 -0800)]
Proposed fix for bug 702. Checks to make sure the Expr's operator is not of kind BUILTIN before passing to prefixPrintGetValue()
ajreynol [Wed, 11 Jan 2017 20:34:18 +0000 (14:34 -0600)]
Fix for when variables are (partially) bound in multiple ways, add regression. Improve printing for bound int module. Track when relations are enabled in sets, set incomplete if card+rels are both enabled since model construction is not guaranteed to succeed.
Clark Barrett [Wed, 11 Jan 2017 19:03:22 +0000 (11:03 -0800)]
Merge pull request #127 from cristian-mattarei/issue_679
Bug 679 fix
Chad Brewbaker [Wed, 11 Jan 2017 02:59:20 +0000 (20:59 -0600)]
revert