cvc5.git
10 years agofix a typo: --string-exp => --strings-exp; fix a signed int warning in antlr
Tianyi Liang [Tue, 29 Apr 2014 21:54:26 +0000 (16:54 -0500)]
fix a typo: --string-exp => --strings-exp; fix a signed int warning in antlr

10 years agoadd leading zeros support for str.to.int
Tianyi Liang [Tue, 29 Apr 2014 20:32:38 +0000 (15:32 -0500)]
add leading zeros support for str.to.int

10 years agoSignificantly improve performance for producing datatypes models.
ajreynol [Tue, 29 Apr 2014 13:39:11 +0000 (15:39 +0200)]
Significantly improve performance for producing datatypes models.

10 years agoMerge remote-tracking branch 'upstream/master' into sets
Kshitij Bansal [Mon, 28 Apr 2014 23:11:59 +0000 (19:11 -0400)]
Merge remote-tracking branch 'upstream/master' into sets

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

10 years agoadd strings-opt2 for regular splitting
Tianyi Liang [Mon, 28 Apr 2014 21:29:27 +0000 (16:29 -0500)]
add strings-opt2 for regular splitting

10 years agocleanup
Kshitij Bansal [Mon, 28 Apr 2014 22:18:24 +0000 (18:18 -0400)]
cleanup

10 years agominor change with kshitij's change
Tianyi Liang [Mon, 28 Apr 2014 22:21:25 +0000 (17:21 -0500)]
minor change with kshitij's change

10 years agonodemanager robust skolem numbering
Kshitij Bansal [Mon, 28 Apr 2014 22:18:07 +0000 (18:18 -0400)]
nodemanager robust skolem numbering

10 years agoadd strings-opt2 for regular splitting
Tianyi Liang [Mon, 28 Apr 2014 21:29:27 +0000 (16:29 -0500)]
add strings-opt2 for regular splitting

10 years agoMerge pull request #25 from kbansal/sets
Kshitij Bansal [Mon, 28 Apr 2014 18:11:14 +0000 (14:11 -0400)]
Merge pull request #25 from kbansal/sets

Sets

10 years agoPreparation for models for co-inductive datatypes. Minor cleanup.
Andrew Reynolds [Mon, 28 Apr 2014 17:28:16 +0000 (12:28 -0500)]
Preparation for models for co-inductive datatypes. Minor cleanup.

10 years agoOptimizations for datatypes: check for clashes modulo equality. Avoid building model...
ajreynol [Mon, 28 Apr 2014 15:34:00 +0000 (17:34 +0200)]
Optimizations for datatypes: check for clashes modulo equality.  Avoid building model at fullModel=false when possible.  Minor cleanup.

10 years agominor fix
Kshitij Bansal [Mon, 28 Apr 2014 15:31:29 +0000 (11:31 -0400)]
minor fix

10 years agoMerge remote-tracking branch 'upstream/master' into sets
Kshitij Bansal [Mon, 28 Apr 2014 15:28:25 +0000 (11:28 -0400)]
Merge remote-tracking branch 'upstream/master' into sets

10 years agotravis, please!
Kshitij Bansal [Mon, 28 Apr 2014 04:20:26 +0000 (00:20 -0400)]
travis, please!

10 years agoattempt to improve CVC4's "parse error" message
Kshitij Bansal [Fri, 25 Apr 2014 01:35:03 +0000 (21:35 -0400)]
attempt to improve CVC4's "parse error" message

10 years agorm undocument/non-working* "feature"
Kshitij Bansal [Sun, 27 Apr 2014 22:41:03 +0000 (18:41 -0400)]
rm undocument/non-working* "feature"

*test of unsigned for negative

10 years agominor change: add a heuristic for preventing constant splitting.
Tianyi Liang [Thu, 24 Apr 2014 22:30:15 +0000 (17:30 -0500)]
minor change: add a heuristic for preventing constant splitting.

10 years agooptimization
Kshitij Bansal [Thu, 24 Apr 2014 21:06:43 +0000 (17:06 -0400)]
optimization

10 years agoAvoid assigning constructor terms to 1-constructor datatype eqcs, when possible,...
ajreynol [Thu, 24 Apr 2014 14:47:46 +0000 (16:47 +0200)]
Avoid assigning constructor terms to 1-constructor datatype eqcs, when possible, to ensure termination for codatatypes. Minor changes.

10 years agoCompute care graph for datatypes. Preliminary results show 20x speed up on larger...
Andrew Reynolds [Thu, 24 Apr 2014 12:27:38 +0000 (14:27 +0200)]
Compute care graph for datatypes.  Preliminary results show 20x speed up on larger problems.  Improve datatypes rewriter.

10 years agoAdd --inst-max-level=N option for Kshitij. Support define-const command in Smt2.
Andrew Reynolds [Thu, 24 Apr 2014 08:35:08 +0000 (03:35 -0500)]
Add --inst-max-level=N option for Kshitij.  Support define-const command in Smt2.

10 years agoMinor fix to avoid rewriting datatype equalities into non-equalitiers, as required...
Andrew Reynolds [Tue, 22 Apr 2014 08:16:56 +0000 (03:16 -0500)]
Minor fix to avoid rewriting datatype equalities into non-equalitiers, as required.  Add APPLY_UF to congruence types to avoid model construction bugs.

10 years agoEh, what?
Kshitij Bansal [Sat, 19 Apr 2014 20:44:20 +0000 (16:44 -0400)]
Eh, what?

10 years agofix warnings in strings/
Kshitij Bansal [Sat, 19 Apr 2014 20:45:13 +0000 (16:45 -0400)]
fix warnings in strings/

10 years agoAllow fmf-bound-int to be set with set-option and via API.
Morgan Deters [Thu, 17 Apr 2014 19:16:42 +0000 (15:16 -0400)]
Allow fmf-bound-int to be set with set-option and via API.

10 years agosimplify mkSkolem naming system: don't use $$
Kshitij Bansal [Thu, 17 Apr 2014 17:03:30 +0000 (13:03 -0400)]
simplify mkSkolem naming system: don't use $$

Short summary: By default NODEID is appeneded, just continue doing what you
were, just don't add the _$$ at the end.

Long summary:

Before this commit there were four (yes!) ways to specify the names for new
skolems, which result in names as given below

1) mkSkolem("name", ..., SKOLEM_FLAG_DEFAULT)  -> "name_NODEID"
2) mkSkolem("name", ..., SKOLEM_EXACT_NAME)  -> "name"
3) mkSkolem("name_$$", ..., SKOLEM_FLAG_DEFAULT) -> "name_NODEID"
4) mkSkolem("na_$$_me", ..., SKOLEM_FLAG_DEFAULT) -> "na_NODEID_me"

After this commit, only 1) and 2) stay.

90% usage is of 1) or 3), which results in exact same behavior (and
looking at the source code it doesn't look like everyone realized that
the _$$ is just redundant).

Almost no one used 4), which is the only reason to even have $$. Post this
commit if you really want a number in the middle, manually construct the
name and use the SKOLEM_EXACT_NAME flag.

10 years agouse internal skolem numbering
Kshitij Bansal [Wed, 9 Apr 2014 20:56:56 +0000 (16:56 -0400)]
use internal skolem numbering

10 years agoMinor refactoring and optimizing.
Andrew Reynolds [Thu, 17 Apr 2014 09:24:11 +0000 (04:24 -0500)]
Minor refactoring and optimizing.

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