cvc5.git
11 years agominor fix to last commit (gitignore)
Kshitij Bansal [Thu, 17 Oct 2013 18:03:25 +0000 (14:03 -0400)]
minor fix to last commit (gitignore)

11 years ago.gitignore personal configuration files
Kshitij Bansal [Thu, 17 Oct 2013 18:02:27 +0000 (14:02 -0400)]
.gitignore personal configuration files

11 years agoadds fmf for strings
Tianyi Liang [Wed, 16 Oct 2013 18:24:56 +0000 (13:24 -0500)]
adds fmf for strings

11 years agorenames for strings fmf
Tianyi Liang [Wed, 16 Oct 2013 15:16:59 +0000 (10:16 -0500)]
renames for strings fmf

11 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Wed, 16 Oct 2013 14:37:17 +0000 (09:37 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4

11 years agobug fix in strings : change from assert to alwaysassert
Tianyi Liang [Tue, 15 Oct 2013 22:23:51 +0000 (17:23 -0500)]
bug fix in strings : change from assert to  alwaysassert

11 years agoremoves some junks
Tianyi Liang [Tue, 15 Oct 2013 19:23:08 +0000 (14:23 -0500)]
removes some junks

11 years agoperformance optimizations for quantifier instantiation
Andrew Reynolds [Tue, 15 Oct 2013 19:23:20 +0000 (14:23 -0500)]
performance optimizations for quantifier instantiation

11 years agobug fix in strings : change from assert to alwaysassert
Tianyi Liang [Tue, 15 Oct 2013 22:23:51 +0000 (17:23 -0500)]
bug fix in strings : change from assert to  alwaysassert

11 years agoperformance optimizations for quantifier instantiation
Andrew Reynolds [Tue, 15 Oct 2013 19:23:20 +0000 (14:23 -0500)]
performance optimizations for quantifier instantiation

11 years agoremoves some junks
Tianyi Liang [Tue, 15 Oct 2013 19:23:08 +0000 (14:23 -0500)]
removes some junks

11 years agobug fix: string cache cleaning
Tianyi Liang [Tue, 15 Oct 2013 18:16:03 +0000 (13:16 -0500)]
bug fix: string cache cleaning

11 years agoadd another regexp test
Tianyi Liang [Mon, 14 Oct 2013 21:39:13 +0000 (16:39 -0500)]
add another regexp test

11 years agoAdds Regular Expression support.
Tianyi Liang [Mon, 14 Oct 2013 21:27:33 +0000 (16:27 -0500)]
Adds Regular Expression support.

11 years agoAdds regular expression support, it is actually CFL because of variables.
Tianyi Liang [Fri, 11 Oct 2013 21:54:22 +0000 (16:54 -0500)]
Adds regular expression support, it is actually CFL because of variables.

11 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Fri, 11 Oct 2013 08:34:04 +0000 (03:34 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4

11 years agoadd constant membership
Tianyi Liang [Fri, 11 Oct 2013 08:32:33 +0000 (03:32 -0500)]
add constant membership

11 years agoadds native regexp.
Tianyi Liang [Thu, 10 Oct 2013 17:06:25 +0000 (12:06 -0500)]
adds native regexp.

11 years agoadd constant membership
Tianyi Liang [Fri, 11 Oct 2013 08:32:33 +0000 (03:32 -0500)]
add constant membership

11 years agoMinor bug fix to datatypes.
Andrew Reynolds [Thu, 10 Oct 2013 17:36:24 +0000 (12:36 -0500)]
Minor bug fix to datatypes.

11 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Thu, 10 Oct 2013 17:07:40 +0000 (12:07 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4

11 years agoadds native regexp.
Tianyi Liang [Thu, 10 Oct 2013 17:06:25 +0000 (12:06 -0500)]
adds native regexp.

11 years agoadds native regexp.
Tianyi Liang [Thu, 10 Oct 2013 17:06:25 +0000 (12:06 -0500)]
adds native regexp.

11 years agoMore improvements to datatypes, eager selector collapsing, improved collect model...
Andrew Reynolds [Wed, 9 Oct 2013 17:26:11 +0000 (12:26 -0500)]
More improvements to datatypes, eager selector collapsing, improved collect model info. Also fix bug in model post-processor.

11 years agoOptimizations for datatypes theory. There seems to be a bug in trans_closure, curren...
Andrew Reynolds [Tue, 8 Oct 2013 14:01:13 +0000 (09:01 -0500)]
Optimizations for datatypes theory.  There seems to be a bug in trans_closure, currently implemented a work around.

11 years agoMultiple fixes for datatypes theory solver: add support for parametric datatypes...
Andrew Reynolds [Mon, 7 Oct 2013 15:02:57 +0000 (10:02 -0500)]
Multiple fixes for datatypes theory solver: add support for parametric datatypes in type enumerator, fix infinite loop in type enumerator, fix fairness issue for splitting (moves constructor selection into model generation procedure), fixes bug 532, find conflict for constructor with conflicting label eagerly.  Add representive flattening for quantifiers (currently disabled). Other minor cleanup.

11 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Tianyi Liang [Thu, 3 Oct 2013 16:17:12 +0000 (11:17 -0500)]
Merge branch 'master' of https://github.com/CVC4/CVC4

11 years agoAdding example proof signatures for LFSC.
Andrew Reynolds [Thu, 3 Oct 2013 14:52:24 +0000 (09:52 -0500)]
Adding example proof signatures for LFSC.

11 years agoAdded support for converting unsorted problems to multi-sorted problems via sort...
Andrew Reynolds [Wed, 2 Oct 2013 19:22:36 +0000 (14:22 -0500)]
Added support for converting unsorted problems to multi-sorted problems via sort inference and monotonicity.  Minor cleanup.

11 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Thu, 3 Oct 2013 15:53:46 +0000 (10:53 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4

Conflicts:
src/theory/strings/theory_strings.cpp

11 years agoadds some fixes. it solves kaluza problems
Tianyi Liang [Thu, 3 Oct 2013 15:48:25 +0000 (10:48 -0500)]
adds some fixes. it solves kaluza problems

11 years agoAdding example proof signatures for LFSC.
Andrew Reynolds [Thu, 3 Oct 2013 14:52:24 +0000 (09:52 -0500)]
Adding example proof signatures for LFSC.

11 years agoAdded support for converting unsorted problems to multi-sorted problems via sort...
Andrew Reynolds [Wed, 2 Oct 2013 19:22:36 +0000 (14:22 -0500)]
Added support for converting unsorted problems to multi-sorted problems via sort inference and monotonicity.  Minor cleanup.

11 years agoadds partial function substr. the use of this function should be guarded, especially...
Tianyi Liang [Wed, 2 Oct 2013 01:03:30 +0000 (20:03 -0500)]
adds partial function substr. the use of this function should be guarded, especially for disequalities

11 years agoadds partial function substr. the use of this function should be guarded, especially...
Tianyi Liang [Wed, 2 Oct 2013 01:03:30 +0000 (20:03 -0500)]
adds partial function substr. the use of this function should be guarded, especially for disequalities

11 years agoFix a bug in smt2 parser for quantified formulas with attributes, fixes bug 535
Andrew Reynolds [Tue, 1 Oct 2013 16:05:23 +0000 (11:05 -0500)]
Fix a bug in smt2 parser for quantified formulas with attributes, fixes bug 535

11 years agoreplace with a new method for disequality, move to QF_S
Tianyi Liang [Tue, 1 Oct 2013 04:29:57 +0000 (23:29 -0500)]
replace with a new method for disequality, move to QF_S

11 years agoadd x=y
Tianyi Liang [Mon, 30 Sep 2013 20:51:25 +0000 (15:51 -0500)]
add x=y

11 years agofixed a loop bug
Tianyi Liang [Mon, 30 Sep 2013 16:43:20 +0000 (11:43 -0500)]
fixed a loop bug

11 years agoBug fixes and improvements for symmetry breaking, it now supports multiple sorts...
Andrew Reynolds [Mon, 30 Sep 2013 15:14:32 +0000 (10:14 -0500)]
Bug fixes and improvements for symmetry breaking, it now supports multiple sorts.  Working on monotonicity inference.

11 years agoSome fixes to recent strings commits.
Morgan Deters [Fri, 27 Sep 2013 22:42:13 +0000 (18:42 -0400)]
Some fixes to recent strings commits.

11 years agoMerge branch 'master' of github.com:tiliang/CVC4
Morgan Deters [Fri, 27 Sep 2013 21:52:51 +0000 (17:52 -0400)]
Merge branch 'master' of github.com:tiliang/CVC4

11 years agoadds communication with arith engine
Tianyi Liang [Fri, 27 Sep 2013 21:46:33 +0000 (16:46 -0500)]
adds communication with arith engine

11 years agoAdd new symmetry breaking technique for finite model finding. Improvements to bounde...
Andrew Reynolds [Fri, 27 Sep 2013 14:27:19 +0000 (09:27 -0500)]
Add new symmetry breaking technique for finite model finding.  Improvements to bounded integer quantifier instantiation.

11 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Fri, 27 Sep 2013 14:26:57 +0000 (09:26 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4

11 years agoremoves unsound cases, adds unrolling
Tianyi Liang [Fri, 27 Sep 2013 14:24:42 +0000 (09:24 -0500)]
removes unsound cases, adds unrolling

11 years agofix the infinite issue
Tianyi Liang [Wed, 25 Sep 2013 18:23:23 +0000 (13:23 -0500)]
fix the infinite issue

11 years agofor morgan to see the regression problems
Tianyi Liang [Wed, 25 Sep 2013 18:00:13 +0000 (13:00 -0500)]
for morgan to see the regression problems

11 years agofix loop detection for multi-vars
Tianyi Liang [Tue, 24 Sep 2013 19:17:36 +0000 (14:17 -0500)]
fix loop detection for multi-vars

11 years agooptimizing model generation for strings
Tianyi Liang [Mon, 23 Sep 2013 23:21:58 +0000 (18:21 -0500)]
optimizing model generation for strings

11 years agoadds model generation for strings, and a hacked way in arith engine for models
Tianyi Liang [Mon, 23 Sep 2013 21:54:32 +0000 (16:54 -0500)]
adds model generation for strings, and a hacked way in arith engine for models

11 years agoremoves unsound cases, adds unrolling
Tianyi Liang [Fri, 27 Sep 2013 14:24:42 +0000 (09:24 -0500)]
removes unsound cases, adds unrolling

11 years agofix the infinite issue
Tianyi Liang [Wed, 25 Sep 2013 18:23:23 +0000 (13:23 -0500)]
fix the infinite issue

11 years agofor morgan to see the regression problems
Tianyi Liang [Wed, 25 Sep 2013 18:00:13 +0000 (13:00 -0500)]
for morgan to see the regression problems

11 years agoReduce compiler dependencies on substitutions.h,
Clark Barrett [Tue, 24 Sep 2013 23:56:06 +0000 (16:56 -0700)]
Reduce compiler dependencies on substitutions.h,
Some new functionality in substitutions.h/cpp

11 years agoBetter fix for bug 528
Clark Barrett [Tue, 24 Sep 2013 23:25:53 +0000 (16:25 -0700)]
Better fix for bug 528

11 years agofix loop detection for multi-vars
Tianyi Liang [Tue, 24 Sep 2013 19:17:36 +0000 (14:17 -0500)]
fix loop detection for multi-vars

11 years agooptimizing model generation for strings
Tianyi Liang [Mon, 23 Sep 2013 23:21:58 +0000 (18:21 -0500)]
optimizing model generation for strings

11 years agoadds model generation for strings, and a hacked way in arith engine for models
Tianyi Liang [Mon, 23 Sep 2013 21:54:32 +0000 (16:54 -0500)]
adds model generation for strings, and a hacked way in arith engine for models

11 years agoRevert Clark's last commit, at his request; there are some bugs.
Morgan Deters [Mon, 23 Sep 2013 23:56:01 +0000 (19:56 -0400)]
Revert Clark's last commit, at his request; there are some bugs.

This reverts commit 9775bced75843c6f01e9524c2d0e7021535e3ec0.

11 years agoCleaner version of bug-fix for 528, also moved substitutions.h out of theory.h
Clark Barrett [Mon, 23 Sep 2013 21:33:53 +0000 (14:33 -0700)]
Cleaner version of bug-fix for 528, also moved substitutions.h out of theory.h
for faster compilation

11 years agoFix for bug 528
Clark Barrett [Thu, 19 Sep 2013 21:29:29 +0000 (14:29 -0700)]
Fix for bug 528

11 years agoSupport a personal build configuration and make rules.
Morgan Deters [Thu, 5 Sep 2013 13:14:39 +0000 (09:14 -0400)]
Support a personal build configuration and make rules.

11 years agoSupport for bv2nat/int2bv in parser and BV rewriter.
Morgan Deters [Wed, 18 Sep 2013 20:53:18 +0000 (16:53 -0400)]
Support for bv2nat/int2bv in parser and BV rewriter.

11 years agoFixes to theoryof-mode; no longer static in Theory class.
Morgan Deters [Tue, 17 Sep 2013 21:21:26 +0000 (17:21 -0400)]
Fixes to theoryof-mode; no longer static in Theory class.

11 years agoFix (extraneous) command dumping.
Morgan Deters [Sat, 14 Sep 2013 23:41:53 +0000 (19:41 -0400)]
Fix (extraneous) command dumping.

11 years agoChange default option of simple ite lifting within quantifier bodies. add some debug...
Andrew Reynolds [Fri, 13 Sep 2013 16:23:30 +0000 (11:23 -0500)]
Change default option of simple ite lifting within quantifier bodies.  add some debug messages.

11 years agoFix sat_proof "parentheses into the void" after conferring with Liana.
Morgan Deters [Fri, 16 Aug 2013 21:07:22 +0000 (17:07 -0400)]
Fix sat_proof "parentheses into the void" after conferring with Liana.

11 years agoMove some regress benchmarks around that took too long, other test cleanup.
Morgan Deters [Fri, 16 Aug 2013 19:04:14 +0000 (15:04 -0400)]
Move some regress benchmarks around that took too long, other test cleanup.

11 years agoDocumentation fixes, some code typo fixes, file perms, other minor things.
Morgan Deters [Fri, 16 Aug 2013 19:15:03 +0000 (15:15 -0400)]
Documentation fixes, some code typo fixes, file perms, other minor things.

11 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Kshitij Bansal [Fri, 13 Sep 2013 20:08:56 +0000 (16:08 -0400)]
Merge branch 'master' of https://github.com/CVC4/CVC4

11 years agofix bug 534: portfolio define-fun duplicate model
Kshitij Bansal [Thu, 12 Sep 2013 18:44:49 +0000 (14:44 -0400)]
fix bug 534: portfolio define-fun duplicate model

11 years agoTheory of strings.
Tianyi Liang [Wed, 11 Sep 2013 15:23:19 +0000 (11:23 -0400)]
Theory of strings.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
11 years agoAnother minor fix for datatypes to repair my previous commit.
Andrew Reynolds [Mon, 9 Sep 2013 23:40:45 +0000 (18:40 -0500)]
Another minor fix for datatypes to repair my previous commit.

11 years agoAdd support for check-sat with argument.
Morgan Deters [Mon, 19 Aug 2013 22:15:21 +0000 (18:15 -0400)]
Add support for check-sat with argument.

11 years agoFix declare-datatypes dumping bug (bug 385).
Morgan Deters [Fri, 6 Sep 2013 00:59:18 +0000 (20:59 -0400)]
Fix declare-datatypes dumping bug (bug 385).

11 years agoSupport per-command verbosity settings.
Morgan Deters [Thu, 5 Sep 2013 00:29:24 +0000 (20:29 -0400)]
Support per-command verbosity settings.

11 years agoSupport empty (and 1-ary) tuples and records.
Morgan Deters [Wed, 4 Sep 2013 23:55:16 +0000 (19:55 -0400)]
Support empty (and 1-ary) tuples and records.

11 years agoFix some line-numbering in auto-generated metakind.h. Thanks to Martin Brain for...
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.

11 years agoFix portfolio on bug411.smt2. (get-model command should only go to last winner)
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)

11 years agoEnsure no cost for datatypes debugging when not tracing it.
Morgan Deters [Mon, 9 Sep 2013 18:41:21 +0000 (14:41 -0400)]
Ensure no cost for datatypes debugging when not tracing it.

11 years agoFix datatypes for bug 503
Andrew Reynolds [Sat, 7 Sep 2013 02:34:44 +0000 (21:34 -0500)]
Fix datatypes for bug 503

11 years agoFix FLOOR and DISTINCT in CVC language parser.
Morgan Deters [Thu, 5 Sep 2013 19:43:47 +0000 (15:43 -0400)]
Fix FLOOR and DISTINCT in CVC language parser.

11 years agoFix lambda handling in CVC parser
Morgan Deters [Thu, 5 Sep 2013 14:47:07 +0000 (10:47 -0400)]
Fix lambda handling in CVC parser

11 years agoPermit setOption(decision-mode)
Morgan Deters [Fri, 16 Aug 2013 23:41:36 +0000 (19:41 -0400)]
Permit setOption(decision-mode)

11 years agoFix bugs/issues with missed-t-prop dump output
Morgan Deters [Thu, 5 Sep 2013 13:37:01 +0000 (09:37 -0400)]
Fix bugs/issues with missed-t-prop dump output

11 years agoFix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a segfault...
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

11 years agoAdd ability to mkConst(TupleSelect) and friends in language bindings
Morgan Deters [Sat, 31 Aug 2013 01:00:56 +0000 (21:00 -0400)]
Add ability to mkConst(TupleSelect) and friends in language bindings

11 years agoMerge branch '1.2.x'
Kshitij Bansal [Mon, 26 Aug 2013 23:48:10 +0000 (19:48 -0400)]
Merge branch '1.2.x'

11 years agobug 374 fix: assert litVal=desiredVal only for leaf nodes
Kshitij Bansal [Mon, 26 Aug 2013 22:56:39 +0000 (18:56 -0400)]
bug 374 fix: assert litVal=desiredVal only for leaf nodes

11 years agoBug 374 benchmarks
Kshitij Bansal [Mon, 26 Aug 2013 22:54:42 +0000 (18:54 -0400)]
Bug 374 benchmarks

11 years agoChange recursive expandDefinitions() to an interative worklist-based one; we were...
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.

11 years ago--segv-nospin is now default.
Morgan Deters [Tue, 13 Aug 2013 15:59:26 +0000 (11:59 -0400)]
--segv-nospin is now default.

11 years agoMinor cleanup.
Morgan Deters [Tue, 13 Aug 2013 21:58:30 +0000 (17:58 -0400)]
Minor cleanup.

11 years agoMinor fixes for --fmf-fmc for quantifiers containing datatypes
Andrew Reynolds [Tue, 13 Aug 2013 21:10:41 +0000 (16:10 -0500)]
Minor fixes for --fmf-fmc for quantifiers containing datatypes

11 years agoinitial modifications for per-ic cbqi
Andrew Reynolds [Mon, 22 Jul 2013 22:59:47 +0000 (17:59 -0500)]
initial modifications for per-ic cbqi

11 years agoClean up "make install"-produced intermediate files (resolves bug 526)
Morgan Deters [Fri, 9 Aug 2013 13:56:50 +0000 (09:56 -0400)]
Clean up "make install"-produced intermediate files (resolves bug 526)

11 years agoFix a serious bug in the preprocessor; problem inputs reported by Pantazis Deligiannis.
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.

11 years agoParameterized, uninterpreted sorts need no Boolean-term conversion
Morgan Deters [Thu, 8 Aug 2013 16:23:59 +0000 (12:23 -0400)]
Parameterized, uninterpreted sorts need no Boolean-term conversion

11 years agoMinor fixes to build system.
Morgan Deters [Tue, 30 Jul 2013 16:37:04 +0000 (12:37 -0400)]
Minor fixes to build system.