cvc5.git
10 years agoFix bug in mbqi=fmc handling theory symbols. Fix mbqi=fmc models (Bug 557). Improve...
Andrew Reynolds [Mon, 14 Apr 2014 20:36:28 +0000 (15:36 -0500)]
Fix bug in mbqi=fmc handling theory symbols.  Fix mbqi=fmc models (Bug 557).  Improve datatypes rewrite, make option for previous dt semantics.

10 years agoAdd initial support for co-datatypes.
Andrew Reynolds [Mon, 14 Apr 2014 09:28:44 +0000 (04:28 -0500)]
Add initial support for co-datatypes.

10 years agoBetter support for building with mingw64; thanks to Nicolas Roche @ Altran for the...
Morgan Deters [Fri, 11 Apr 2014 19:30:31 +0000 (15:30 -0400)]
Better support for building with mingw64; thanks to Nicolas Roche @ Altran for the fix.

10 years agosetType -> setOfType, resolves bug 556
Morgan Deters [Fri, 11 Apr 2014 00:06:31 +0000 (20:06 -0400)]
setType -> setOfType, resolves bug 556

10 years agoFix the build; --check-proof works for UF but not for the new UFC logic.
Morgan Deters [Thu, 10 Apr 2014 22:34:44 +0000 (18:34 -0400)]
Fix the build; --check-proof works for UF but not for the new UFC logic.

10 years agoExpand definitions in theory datatypes, now has the expected semantics for incorrectl...
Andrew Reynolds [Thu, 10 Apr 2014 20:50:56 +0000 (15:50 -0500)]
Expand definitions in theory datatypes, now has the expected semantics for incorrectly applied selector terms.

10 years agoBoolean terms conversion fix for datatypes, fixes a problem Andy discovered on his...
Morgan Deters [Thu, 10 Apr 2014 20:38:37 +0000 (16:38 -0400)]
Boolean terms conversion fix for datatypes, fixes a problem Andy discovered on his branch.

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Thu, 10 Apr 2014 17:57:38 +0000 (12:57 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agominor fix for strings
Tianyi Liang [Thu, 10 Apr 2014 17:56:53 +0000 (12:56 -0500)]
minor fix for strings

10 years agominor fix for strings
Tianyi Liang [Thu, 10 Apr 2014 17:56:53 +0000 (12:56 -0500)]
minor fix for strings

10 years agoAdd support for cardinality constraints logic UFC. Add regressions in fmf/. Fix...
Andrew Reynolds [Thu, 10 Apr 2014 15:31:47 +0000 (10:31 -0500)]
Add support for cardinality constraints logic UFC.  Add regressions in fmf/.  Fix datatypes E-matching bug.  Change defaults : mbqi=fmc, decision heuristic stoponly=false for quantified logics, decision=justification for ALL_SUPPORTED, full-saturate-quant=false.  Minor fix for fmc models.  Add infrastructure to datatypes to prepare for next commit.

10 years agorefactor .travis.yml
Kshitij Bansal [Thu, 10 Apr 2014 13:29:58 +0000 (09:29 -0400)]
refactor .travis.yml

10 years agoMerge pull request #24 from kbansal/sets-model
Kshitij Bansal [Wed, 9 Apr 2014 22:07:32 +0000 (18:07 -0400)]
Merge pull request #24 from kbansal/sets-model

sets, misc

10 years agoMinor change to better support parameterized partial/total kinds (for upcoming dataty...
Morgan Deters [Wed, 9 Apr 2014 15:18:18 +0000 (11:18 -0400)]
Minor change to better support parameterized partial/total kinds (for upcoming datatypes work).

10 years agoRevert E-matching datatypes fix.
Andrew Reynolds [Wed, 9 Apr 2014 21:12:19 +0000 (16:12 -0500)]
Revert E-matching datatypes fix.

10 years agoHandle fmf.card as input from user, add support in SMT2 parser, as requested by Marti...
Andrew Reynolds [Wed, 9 Apr 2014 20:43:37 +0000 (15:43 -0500)]
Handle fmf.card as input from user, add support in SMT2 parser, as requested by Martin Brain.  Fix two minor bugs : E-matching with datatypes, instantiation caching with incremental.

10 years agofix get-info error-behavior
Kshitij Bansal [Wed, 9 Apr 2014 18:35:37 +0000 (14:35 -0400)]
fix get-info error-behavior

10 years agoadd tests
Kshitij Bansal [Wed, 9 Apr 2014 18:04:26 +0000 (14:04 -0400)]
add tests

10 years agofix
Kshitij Bansal [Wed, 9 Apr 2014 18:03:35 +0000 (14:03 -0400)]
fix

10 years agoprep for fix
Kshitij Bansal [Wed, 9 Apr 2014 17:46:00 +0000 (13:46 -0400)]
prep for fix

10 years agotry foreach on CD datastructure
Kshitij Bansal [Wed, 9 Apr 2014 16:21:07 +0000 (12:21 -0400)]
try foreach on CD datastructure

10 years agoinputs to trigger bug
Kshitij Bansal [Wed, 9 Apr 2014 15:35:41 +0000 (11:35 -0400)]
inputs to trigger bug

10 years agomore
Kshitij Bansal [Tue, 8 Apr 2014 19:06:38 +0000 (15:06 -0400)]
more

10 years agosome debugging changes
Kshitij Bansal [Tue, 8 Apr 2014 14:29:02 +0000 (10:29 -0400)]
some debugging changes

10 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Kshitij Bansal [Sun, 6 Apr 2014 23:46:34 +0000 (19:46 -0400)]
Merge branch 'master' of https://github.com/CVC4/CVC4

10 years agoReduced example from pcc's bug report.
Tim King [Sun, 6 Apr 2014 22:57:53 +0000 (18:57 -0400)]
Reduced example from pcc's bug report.

10 years agoMerge pull request #21 from pcc/ite-fix
Tim King [Sun, 6 Apr 2014 22:41:32 +0000 (18:41 -0400)]
Merge pull request #21 from pcc/ite-fix

Fix for ite of >=64bit wide bitvectors with unconstrained condition.

10 years agofix for hiding prompt/header in shell, error-behavior options as in SMTLIB
Kshitij Bansal [Sun, 6 Apr 2014 10:25:08 +0000 (06:25 -0400)]
fix for hiding prompt/header in shell, error-behavior options as in SMTLIB

10 years agoFor security, add --no-filesystem-access option, which disables SMT-LIB script access...
Morgan Deters [Fri, 4 Apr 2014 18:50:52 +0000 (14:50 -0400)]
For security, add --no-filesystem-access option, which disables SMT-LIB script access to filesystem.

10 years agoAllow turning off the interactive prompt while in interactive mode.
Morgan Deters [Fri, 4 Apr 2014 18:49:17 +0000 (14:49 -0400)]
Allow turning off the interactive prompt while in interactive mode.

10 years agoProperly quote symbols in SMT-LIB printer.
Morgan Deters [Thu, 3 Apr 2014 23:32:30 +0000 (19:32 -0400)]
Properly quote symbols in SMT-LIB printer.

10 years agoSome incremental bugs for Boolean terms, fixed. Thanks to Pantazis Deligiannis and...
Morgan Deters [Thu, 3 Apr 2014 23:16:39 +0000 (19:16 -0400)]
Some incremental bugs for Boolean terms, fixed.  Thanks to Pantazis Deligiannis and Jeroen Ketema for discovering this issue.

10 years agoMerge branch '1.3.x'
Tim King [Tue, 1 Apr 2014 21:17:21 +0000 (17:17 -0400)]
Merge branch '1.3.x'

10 years agoFixing bug 552. There was a bug when integers are made using a string with a lot...
Tim King [Tue, 1 Apr 2014 20:54:36 +0000 (16:54 -0400)]
Fixing bug 552.  There was a bug when integers are made using a string with a lot of leading 0s on old versions of CLN.

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Tue, 1 Apr 2014 13:25:02 +0000 (08:25 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agowindows build fix for UINT32_MAX
Tianyi Liang [Tue, 1 Apr 2014 13:16:22 +0000 (08:16 -0500)]
windows build fix for UINT32_MAX

10 years agowindows build fix for UINT32_MAX
Tianyi Liang [Tue, 1 Apr 2014 13:16:22 +0000 (08:16 -0500)]
windows build fix for UINT32_MAX

10 years agoTravis-CI test for new-theory script, also related bugfixes.
Morgan Deters [Mon, 31 Mar 2014 20:07:58 +0000 (16:07 -0400)]
Travis-CI test for new-theory script, also related bugfixes.

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Mon, 31 Mar 2014 22:37:11 +0000 (17:37 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agoadd str to u16/u32, and u16/u32 to str
Tianyi Liang [Mon, 31 Mar 2014 20:55:45 +0000 (15:55 -0500)]
add str to u16/u32, and u16/u32 to str

10 years agominor typo/bug fix
Tianyi Liang [Mon, 31 Mar 2014 22:33:35 +0000 (17:33 -0500)]
minor typo/bug fix

10 years agoadd str to u16/u32, and u16/u32 to str
Tianyi Liang [Mon, 31 Mar 2014 20:55:45 +0000 (15:55 -0500)]
add str to u16/u32, and u16/u32 to str

10 years agoMerge pull request #23 from kbansal/sets-model
Kshitij Bansal [Sun, 30 Mar 2014 04:13:29 +0000 (00:13 -0400)]
Merge pull request #23 from kbansal/sets-model

Sets model

10 years agorm old unused code
Kshitij Bansal [Fri, 28 Mar 2014 22:33:38 +0000 (18:33 -0400)]
rm old unused code

10 years agoget-antlr error on missing config.guess
Kshitij Bansal [Fri, 28 Mar 2014 22:37:02 +0000 (18:37 -0400)]
get-antlr error on missing config.guess

10 years agoadd construles, type_rules rm redundant, kinds cleanup
Kshitij Bansal [Wed, 26 Mar 2014 06:58:45 +0000 (02:58 -0400)]
add construles, type_rules rm redundant, kinds cleanup

10 years agominor printer fix; intersection fix
Tianyi Liang [Fri, 28 Mar 2014 20:17:22 +0000 (15:17 -0500)]
minor printer fix; intersection fix

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Thu, 27 Mar 2014 22:21:01 +0000 (17:21 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4

Conflicts:
src/theory/strings/regexp_operation.cpp
src/theory/strings/regexp_operation.h

10 years agoadds new feature: re.loop
Tianyi Liang [Thu, 27 Mar 2014 21:54:46 +0000 (16:54 -0500)]
adds new feature: re.loop

10 years agoadds intersection
Tianyi Liang [Tue, 25 Mar 2014 06:08:29 +0000 (01:08 -0500)]
adds intersection

10 years agoderiv symbolic regexp
Tianyi Liang [Wed, 26 Mar 2014 22:30:30 +0000 (17:30 -0500)]
deriv symbolic regexp

10 years agoadds intersection
Tianyi Liang [Tue, 25 Mar 2014 06:08:29 +0000 (01:08 -0500)]
adds intersection

10 years agoadds new feature: re.loop
Tianyi Liang [Thu, 27 Mar 2014 21:54:46 +0000 (16:54 -0500)]
adds new feature: re.loop

10 years agoMerge branch '1.3.x'
Morgan Deters [Wed, 26 Mar 2014 22:35:33 +0000 (18:35 -0400)]
Merge branch '1.3.x'

Conflicts:
src/theory/arith/normal_form.cpp

10 years agoWin32 build script fixes (to allow portfolio builds).
Morgan Deters [Tue, 25 Mar 2014 23:53:10 +0000 (19:53 -0400)]
Win32 build script fixes (to allow portfolio builds).

10 years agoFix an off-the-end string pointer bug (showed up only in some Win32 builds).
Morgan Deters [Wed, 26 Mar 2014 22:05:02 +0000 (18:05 -0400)]
Fix an off-the-end string pointer bug (showed up only in some Win32 builds).

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Wed, 26 Mar 2014 22:31:23 +0000 (17:31 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agoderiv symbolic regexp
Tianyi Liang [Wed, 26 Mar 2014 22:30:30 +0000 (17:30 -0500)]
deriv symbolic regexp

10 years agoadds intersection
Tianyi Liang [Tue, 25 Mar 2014 06:08:29 +0000 (01:08 -0500)]
adds intersection

10 years agoderiv symbolic regexp
Tianyi Liang [Wed, 26 Mar 2014 22:30:30 +0000 (17:30 -0500)]
deriv symbolic regexp

10 years agoMerging in a fix from 1.3.x.
Tim King [Wed, 26 Mar 2014 20:56:13 +0000 (16:56 -0400)]
Merging in a fix from 1.3.x.
Fixes an idempotency issue for non-linear multiplication with integer and real variables.

Conflicts:
src/theory/arith/normal_form.cpp

10 years agoFixes an idempotency issue for non-linear multiplication with integer and real variables.
Tim King [Wed, 26 Mar 2014 20:56:13 +0000 (16:56 -0400)]
Fixes an idempotency issue for non-linear multiplication with integer and real variables.

10 years agoadds intersection
Tianyi Liang [Tue, 25 Mar 2014 06:08:29 +0000 (01:08 -0500)]
adds intersection

10 years agoMerge pull request #22 from kbansal/sets-model
Kshitij Bansal [Fri, 21 Mar 2014 02:57:20 +0000 (22:57 -0400)]
Merge pull request #22 from kbansal/sets-model

Sets model

10 years agocleanup
Kshitij Bansal [Thu, 20 Mar 2014 23:27:21 +0000 (19:27 -0400)]
cleanup

10 years agofix for sets/mar2014/..317minimized..
Kshitij Bansal [Thu, 20 Mar 2014 06:01:24 +0000 (02:01 -0400)]
fix for sets/mar2014/..317minimized..

Observed behavior:
  --check-model failed for set-term (union (z3f69 z3v151) (setenum z3v143))
with different set of elements in the model for representative and the node
itself.

Issue:
  The trouble with data structure being mainted to ensure that things
for which lemmas have been generated are not generated again. This
data structure (d_pendingEverInserted) needs to be user context
dependent. The bug was in the sequence of steps from requesting that
a lemma be generated to when it actually was. Sequence was:
addToPending (and also adds to pending ever inserted) ->
isComplete (might remove things from pending if requirment met in other ways) ->
getLemma (actually generated the lemma, if requirement not already met)

Resolution:
  adding terms to d_pendingEverInserted was moved from addToPending()
to getLemma().

10 years agoFix for registration issues of term appearing in a shared lemma
Kshitij Bansal [Mon, 17 Mar 2014 22:01:10 +0000 (18:01 -0400)]
Fix for registration issues of term appearing in a shared lemma

(brought to attention by lianah -- fix currently just adapted using
arrays -- this is to remind me to raise why do we even have this
isPreregistered bussiness)

10 years agorewriter fix, weaken an assertion
Kshitij Bansal [Fri, 14 Mar 2014 02:27:22 +0000 (22:27 -0400)]
rewriter fix, weaken an assertion

10 years agoconstant normal form and rewrite
Kshitij Bansal [Fri, 14 Mar 2014 02:17:02 +0000 (22:17 -0400)]
constant normal form and rewrite

10 years agofix a sharing issues with sets
Kshitij Bansal [Thu, 13 Mar 2014 23:33:11 +0000 (19:33 -0400)]
fix a sharing issues with sets

10 years agopush subtyping for sets to the element type
Kshitij Bansal [Wed, 12 Mar 2014 18:43:37 +0000 (14:43 -0400)]
push subtyping for sets to the element type

for eg, (Set Int) is subtype of (Set Real) if Int is subtype of Real

10 years agoenable check-models for sets/ regressions
Kshitij Bansal [Wed, 12 Mar 2014 03:47:33 +0000 (23:47 -0400)]
enable check-models for sets/ regressions

10 years agowork on set model
Kshitij Bansal [Mon, 10 Mar 2014 23:02:32 +0000 (19:02 -0400)]
work on set model

10 years agotestlemma regressions
Kshitij Bansal [Wed, 12 Mar 2014 17:53:22 +0000 (13:53 -0400)]
testlemma regressions

10 years agoMinor fix for CBQI, ignore inst constant nodes.
Andrew Reynolds [Thu, 20 Mar 2014 21:10:04 +0000 (16:10 -0500)]
Minor fix for CBQI, ignore inst constant nodes.

10 years agoFix documentation for Theory::preRegisterTerm().
Morgan Deters [Wed, 19 Mar 2014 21:30:59 +0000 (17:30 -0400)]
Fix documentation for Theory::preRegisterTerm().

10 years agoRefactor the theory specific parts of definition expansion into the theory solvers.
Martin Brain [Tue, 11 Mar 2014 00:03:41 +0000 (00:03 +0000)]
Refactor the theory specific parts of definition expansion into the theory solvers.

In the process of doing this I may have fixed some bugs or some potential bugs so there
may be some user visible results of this refactoring.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
10 years agoSet dumping options from (set-option..) and API more directly.
Morgan Deters [Wed, 19 Mar 2014 20:32:05 +0000 (16:32 -0400)]
Set dumping options from (set-option..) and API more directly.

10 years agoFix for bug 555; SMT-LIBv2 symbols now output with proper quoting.
Morgan Deters [Wed, 19 Mar 2014 17:58:59 +0000 (13:58 -0400)]
Fix for bug 555; SMT-LIBv2 symbols now output with proper quoting.

10 years agoMove the translator binary from src/main to examples, no longer built by default.
Morgan Deters [Sat, 15 Mar 2014 21:41:27 +0000 (17:41 -0400)]
Move the translator binary from src/main to examples, no longer built by default.

10 years agoAppease compilers from latest XCode release (v5.1).
Morgan Deters [Sat, 15 Mar 2014 21:38:07 +0000 (17:38 -0400)]
Appease compilers from latest XCode release (v5.1).

10 years agoMinor usability fixes related to SMT-LIB compliance.
Morgan Deters [Sat, 15 Mar 2014 21:29:09 +0000 (17:29 -0400)]
Minor usability fixes related to SMT-LIB compliance.

10 years agoFix proof signatures makefile
Morgan Deters [Wed, 19 Mar 2014 14:34:41 +0000 (10:34 -0400)]
Fix proof signatures makefile

10 years agoMinor documentation fixups.
Morgan Deters [Fri, 14 Mar 2014 20:10:37 +0000 (16:10 -0400)]
Minor documentation fixups.

10 years agoFix a memory leak in LFSC proof checker. Largest QF_UF proof from Morgan (problemati...
Andrew Reynolds [Wed, 19 Mar 2014 14:03:18 +0000 (09:03 -0500)]
Fix a memory leak in LFSC proof checker.  Largest QF_UF proof from Morgan (problematic-lfsc-pf) now successfully checks in 58 seconds using ~8 GB memory.  Add example test proof.

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Mon, 17 Mar 2014 18:22:21 +0000 (13:22 -0500)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agohot fix for pre-reg term caching in strings
Tianyi Liang [Mon, 17 Mar 2014 18:17:12 +0000 (13:17 -0500)]
hot fix for pre-reg term caching in strings

10 years agohot fix for pre-reg term caching in strings
Tianyi Liang [Mon, 17 Mar 2014 18:17:12 +0000 (13:17 -0500)]
hot fix for pre-reg term caching in strings

10 years agoFix for ite of >=64bit wide bitvectors with unconstrained condition.
Peter Collingbourne [Mon, 17 Mar 2014 05:00:39 +0000 (22:00 -0700)]
Fix for ite of >=64bit wide bitvectors with unconstrained condition.

10 years agoSMT-LIB compliance: allow bin/hex set-info, e.g. (set-info :key #xffff). Thanks...
Morgan Deters [Fri, 14 Mar 2014 19:21:24 +0000 (15:21 -0400)]
SMT-LIB compliance: allow bin/hex set-info, e.g. (set-info :key #xffff).  Thanks to David Cok for the bug report.

10 years agodos2unix on the proof signatures, and fix the makefile.
Morgan Deters [Thu, 13 Mar 2014 17:00:07 +0000 (13:00 -0400)]
dos2unix on the proof signatures, and fix the makefile.

10 years agoAdd ability to provide theory-specific proof rules to EqualityEngine, extends enumera...
Andrew Reynolds [Fri, 14 Mar 2014 16:50:28 +0000 (11:50 -0500)]
Add ability to provide theory-specific proof rules to EqualityEngine, extends enumeration of MergeReasonType.  Add initial use in TheoryArrays.

10 years agoAdd working example of LFSC proof with quantifiers. Update quantifiers signature...
Andrew Reynolds [Thu, 13 Mar 2014 14:58:07 +0000 (09:58 -0500)]
Add working example of LFSC proof with quantifiers.  Update quantifiers signature to avoid dependent types in side condition.

10 years agoWork on array pf signature, add working example. Add quantifiers proof signature...
Andrew Reynolds [Wed, 12 Mar 2014 19:25:25 +0000 (14:25 -0500)]
Work on array pf signature, add working example.  Add quantifiers proof signature. Ignore terms not in current master EE for QCF.  Minor refactoring.  Make --rewrite-rules true by default.

10 years agoMinor fixes post-merge of RR.
Andrew Reynolds [Wed, 12 Mar 2014 15:51:55 +0000 (10:51 -0500)]
Minor fixes post-merge of RR.

10 years agoFix LogicInfo unit test.
Morgan Deters [Wed, 12 Mar 2014 10:18:19 +0000 (06:18 -0400)]
Fix LogicInfo unit test.

10 years agoSome standardization of regression Makefiles that got out of sync. Fixes cases of...
Morgan Deters [Wed, 12 Mar 2014 09:26:19 +0000 (05:26 -0400)]
Some standardization of regression Makefiles that got out of sync.  Fixes cases of nonterminating rewrite-rules regressions.

10 years agoDraft contrib/get-abc script for bitvectors libabc support.
Morgan Deters [Wed, 12 Mar 2014 01:32:49 +0000 (21:32 -0400)]
Draft contrib/get-abc script for bitvectors libabc support.

10 years agoMerge branch '1.3.x'
Morgan Deters [Tue, 11 Mar 2014 23:08:38 +0000 (19:08 -0400)]
Merge branch '1.3.x'

10 years agoFix for rewriterules build breakage.
Morgan Deters [Tue, 11 Mar 2014 22:47:18 +0000 (18:47 -0400)]
Fix for rewriterules build breakage.