cvc5.git
10 years agoa new regular expression engine for solving both positive and negative membership...
Tianyi Liang [Fri, 28 Feb 2014 17:05:09 +0000 (11:05 -0600)]
a new regular expression engine for solving both positive and negative membership constraints

10 years agosorry for the missing file
Tianyi Liang [Wed, 26 Feb 2014 20:37:59 +0000 (14:37 -0600)]
sorry for the missing file

10 years agobug fix (caused by merge), move cardinality option to expert option
Tianyi Liang [Wed, 26 Feb 2014 20:19:49 +0000 (14:19 -0600)]
bug fix (caused by merge), move cardinality option to expert option

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Wed, 26 Feb 2014 17:44:51 +0000 (11:44 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agoadd a new file
Tianyi Liang [Wed, 26 Feb 2014 17:43:59 +0000 (11:43 -0600)]
add a new file

10 years agofor merging
Tianyi Liang [Wed, 26 Feb 2014 17:29:38 +0000 (11:29 -0600)]
for merging

10 years agosmt-lib syntax change: str.contain -> str.contains; add some prefix syntax for cvc...
Tianyi Liang [Mon, 24 Feb 2014 20:45:06 +0000 (14:45 -0600)]
smt-lib syntax change: str.contain -> str.contains; add some prefix syntax for cvc format

10 years agofor merging
Tianyi Liang [Wed, 26 Feb 2014 17:29:38 +0000 (11:29 -0600)]
for merging

10 years agoMinor code clean up in parser.
Morgan Deters [Fri, 14 Feb 2014 23:28:02 +0000 (18:28 -0500)]
Minor code clean up in parser.

10 years agoNew translation work, support Z3-str-style string constraints.
Morgan Deters [Tue, 11 Feb 2014 02:05:16 +0000 (21:05 -0500)]
New translation work, support Z3-str-style string constraints.

10 years agoFix quotes in string constants.
Morgan Deters [Tue, 11 Feb 2014 02:04:58 +0000 (21:04 -0500)]
Fix quotes in string constants.

10 years agoAdd options --full-saturate-quant and --mbqi=trust. Other minor changes.
Andrew Reynolds [Tue, 25 Feb 2014 17:08:33 +0000 (11:08 -0600)]
Add options --full-saturate-quant and --mbqi=trust.  Other minor changes.

10 years agosmt-lib syntax change: str.contain -> str.contains; add some prefix syntax for cvc...
Tianyi Liang [Mon, 24 Feb 2014 20:45:06 +0000 (14:45 -0600)]
smt-lib syntax change: str.contain -> str.contains; add some prefix syntax for cvc format

10 years agobug fix: strings preprocess for the orignal term, causing unknown in some cases
Tianyi Liang [Mon, 24 Feb 2014 17:36:23 +0000 (11:36 -0600)]
bug fix: strings preprocess for the orignal term, causing unknown in some cases

10 years agoMerge branch '1.3.x'
Morgan Deters [Fri, 21 Feb 2014 23:16:38 +0000 (18:16 -0500)]
Merge branch '1.3.x'

10 years agoNo diamond-breaking under quantifiers (resolves bug #550).
Morgan Deters [Fri, 21 Feb 2014 22:15:43 +0000 (17:15 -0500)]
No diamond-breaking under quantifiers (resolves bug #550).

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Fri, 21 Feb 2014 21:20:35 +0000 (15:20 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agoreorganize substr, fix some potential bugs, adds cache for preprocessing
Tianyi Liang [Fri, 21 Feb 2014 21:19:05 +0000 (15:19 -0600)]
reorganize substr, fix some potential bugs, adds cache for preprocessing

10 years agoreorganize substr, fix some potential bugs, adds cache for preprocessing
Tianyi Liang [Fri, 21 Feb 2014 21:19:05 +0000 (15:19 -0600)]
reorganize substr, fix some potential bugs, adds cache for preprocessing

10 years agoMerge branch '1.3.x'
Morgan Deters [Fri, 21 Feb 2014 20:08:01 +0000 (15:08 -0500)]
Merge branch '1.3.x'

10 years agoFix two variants of Node::substitute().
Morgan Deters [Fri, 21 Feb 2014 19:45:52 +0000 (14:45 -0500)]
Fix two variants of Node::substitute().

Node::substitute() is overloaded.  One version was properly substituting
operators (e.g. the "f" in f(x) could be substituted).  The others were
ignoring anything in function position.  Fixed.  Thanks to Wei Wang for
pointing this out.

10 years agoportfolio: fix export of emptyset
Kshitij Bansal [Fri, 21 Feb 2014 18:52:34 +0000 (13:52 -0500)]
portfolio: fix export of emptyset

10 years agoFix makefile dependence for system tests.
Morgan Deters [Fri, 21 Feb 2014 17:35:37 +0000 (12:35 -0500)]
Fix makefile dependence for system tests.

10 years agodisable test cvc3_main, attempt to fix dist_check
Kshitij Bansal [Fri, 21 Feb 2014 15:09:00 +0000 (10:09 -0500)]
disable test cvc3_main, attempt to fix dist_check

10 years agoMerge pull request #10 from kbansal/sets-for-merge
Kshitij Bansal [Fri, 21 Feb 2014 13:33:23 +0000 (08:33 -0500)]
Merge pull request #10 from kbansal/sets-for-merge

Sets for merge

10 years agooption to print stats after every satisfiability or validity query
Kshitij Bansal [Fri, 21 Feb 2014 09:06:40 +0000 (04:06 -0500)]
option to print stats after every satisfiability or validity query

10 years agoadd new theory (sets)
Kshitij Bansal [Mon, 9 Sep 2013 18:47:53 +0000 (14:47 -0400)]
add new theory (sets)

Specification (smt2) -- as per this commit, subject to change

- Parameterized sort Set, e.g. (Set Int)

- Empty set constant (typed), use with "as" to specify the type, e.g.
    (as emptyset (Set Int))

- Create a singleton set
    (setenum X (Set X)) : creates singleton set

- Functions/operators
    (union (Set X) (Set X) (Set X))
    (intersection (Set X) (Set X) (Set X))
    (setminus (Set X) (Set X) (Set X))

- Predicates
    (in X (Set X) Bool) : membership
    (subseteq (Set X) (Set X) Bool) : set containment

10 years agofix a -Wunused
Kshitij Bansal [Fri, 21 Feb 2014 09:58:31 +0000 (04:58 -0500)]
fix a -Wunused

10 years agofix makefile
Tianyi Liang [Fri, 21 Feb 2014 01:52:20 +0000 (19:52 -0600)]
fix makefile

10 years agoadd more tests, and define int.to.str(NEGATIVE)=""
Tianyi Liang [Fri, 21 Feb 2014 00:31:27 +0000 (18:31 -0600)]
add more tests, and define int.to.str(NEGATIVE)=""

10 years agoadd two cases to the regression test
Tianyi Liang [Thu, 20 Feb 2014 23:16:43 +0000 (17:16 -0600)]
add two cases to the regression test

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Thu, 20 Feb 2014 23:07:24 +0000 (17:07 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

Conflicts:
src/theory/strings/theory_strings_preprocess.cpp

10 years agohot fix for str2int/int2str
Tianyi Liang [Thu, 20 Feb 2014 22:07:23 +0000 (16:07 -0600)]
hot fix for str2int/int2str

10 years agoadd negative int2str
Tianyi Liang [Wed, 19 Feb 2014 18:20:44 +0000 (12:20 -0600)]
add negative int2str

10 years agoString parsing example in CVC parser
Morgan Deters [Wed, 19 Feb 2014 04:10:44 +0000 (23:10 -0500)]
String parsing example in CVC parser

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Thu, 20 Feb 2014 23:03:24 +0000 (17:03 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

Conflicts:
src/theory/strings/theory_strings_preprocess.cpp

10 years agohot fix for str2int/int2str
Tianyi Liang [Thu, 20 Feb 2014 22:07:23 +0000 (16:07 -0600)]
hot fix for str2int/int2str

10 years agoadd negative int2str
Tianyi Liang [Wed, 19 Feb 2014 18:20:44 +0000 (12:20 -0600)]
add negative int2str

10 years agoString parsing example in CVC parser
Morgan Deters [Wed, 19 Feb 2014 04:10:44 +0000 (23:10 -0500)]
String parsing example in CVC parser

10 years agoFix ite and iff handling in QCF. Add option for heuristic instantiation in QCF ...
Andrew Reynolds [Thu, 20 Feb 2014 16:37:32 +0000 (10:37 -0600)]
Fix ite and iff handling in QCF.  Add option for heuristic instantiation in QCF (not working yet).  Improve automatic option setting for quantifiers.

10 years agoportfolio: add stat to track time spent waiting for interrupted threads to stop
Kshitij Bansal [Thu, 20 Feb 2014 13:57:39 +0000 (08:57 -0500)]
portfolio: add stat to track time spent waiting for interrupted threads to stop

10 years agoMerge branch 'master' of github.com:CVC4/CVC4
Tim King [Wed, 19 Feb 2014 21:57:51 +0000 (16:57 -0500)]
Merge branch 'master' of github.com:CVC4/CVC4

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Wed, 19 Feb 2014 21:23:46 +0000 (15:23 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agoMerge branch '1.3.x'
Tim King [Wed, 19 Feb 2014 20:50:34 +0000 (15:50 -0500)]
Merge branch '1.3.x'

10 years agoStopping non-linear terms from entering the dio solver. Fixes bug 547.
Tim King [Wed, 19 Feb 2014 20:50:07 +0000 (15:50 -0500)]
Stopping non-linear terms from entering the dio solver. Fixes bug 547.

10 years agoadd negative int2str
Tianyi Liang [Wed, 19 Feb 2014 18:20:44 +0000 (12:20 -0600)]
add negative int2str

10 years agoString parsing example in CVC parser
Morgan Deters [Wed, 19 Feb 2014 04:10:44 +0000 (23:10 -0500)]
String parsing example in CVC parser

10 years agomissed files for the latter commit
Tianyi Liang [Tue, 18 Feb 2014 17:22:46 +0000 (11:22 -0600)]
missed files for the latter commit

10 years agostr.to.int(INVALID) = -1
Tianyi Liang [Tue, 18 Feb 2014 17:08:20 +0000 (11:08 -0600)]
str.to.int(INVALID) = -1

10 years agoswitch to total function str.to.int: maps invalid and non-digit strings to 0
Tianyi Liang [Tue, 18 Feb 2014 16:48:04 +0000 (10:48 -0600)]
switch to total function str.to.int: maps invalid and non-digit strings to 0

10 years agobring back the commits which is lost accidentally.
Tianyi Liang [Tue, 18 Feb 2014 03:09:33 +0000 (21:09 -0600)]
bring back the commits which is lost accidentally.

10 years agoadd str2int
Tianyi Liang [Tue, 18 Feb 2014 01:59:03 +0000 (19:59 -0600)]
add str2int

10 years agoFix for strings-exp: enable quantifiers
Morgan Deters [Mon, 17 Feb 2014 21:19:32 +0000 (16:19 -0500)]
Fix for strings-exp: enable quantifiers

10 years agoFix strings preprocessing for justification heuristic
Morgan Deters [Mon, 17 Feb 2014 21:03:23 +0000 (16:03 -0500)]
Fix strings preprocessing for justification heuristic

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Mon, 17 Feb 2014 20:23:30 +0000 (14:23 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agotype conversion
Tianyi Liang [Mon, 17 Feb 2014 20:22:26 +0000 (14:22 -0600)]
type conversion

10 years agotype conversion
Tianyi Liang [Mon, 17 Feb 2014 20:22:26 +0000 (14:22 -0600)]
type conversion

10 years agoMake QCF more incremental. Fix bug in QCF handling of ITE formulas, add support...
Andrew Reynolds [Fri, 14 Feb 2014 21:44:21 +0000 (15:44 -0600)]
Make QCF more incremental.  Fix bug in QCF handling of ITE formulas, add support for ITE terms.  Add full-delay inst-when mode.  Make strings come before quantifiers in check.  Minor cleanup.

10 years agopartial function charat
Tianyi Liang [Fri, 14 Feb 2014 17:53:12 +0000 (11:53 -0600)]
partial function charat

10 years agofix expanding def
Tianyi Liang [Fri, 14 Feb 2014 00:08:49 +0000 (18:08 -0600)]
fix expanding def

10 years agobug fix for reverse check
Tianyi Liang [Wed, 12 Feb 2014 22:10:07 +0000 (16:10 -0600)]
bug fix for reverse check

10 years agolexer fix: disable smt-lib conversion for string literals
Tianyi Liang [Wed, 12 Feb 2014 04:50:08 +0000 (22:50 -0600)]
lexer fix: disable smt-lib conversion for string literals

10 years agominor fix for recognizing the tail backslash, still have smt-lib compliance issue.
Tianyi Liang [Wed, 12 Feb 2014 00:08:53 +0000 (18:08 -0600)]
minor fix for recognizing the tail backslash, still have smt-lib compliance issue.

10 years agoresolve merge conflicts
Tianyi Liang [Tue, 11 Feb 2014 23:10:06 +0000 (17:10 -0600)]
resolve merge conflicts

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Tue, 11 Feb 2014 22:44:23 +0000 (16:44 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

Conflicts:
src/theory/strings/theory_strings.cpp

10 years agoescaped characters, having an issue with smt-lib defintion, further repair is needed.
Tianyi Liang [Tue, 11 Feb 2014 22:35:17 +0000 (16:35 -0600)]
escaped characters, having an issue with smt-lib defintion, further repair is needed.

10 years agominor fix for merge
Tianyi Liang [Wed, 5 Feb 2014 15:19:23 +0000 (09:19 -0600)]
minor fix for merge

10 years agominor cleanup for merge
Tianyi Liang [Thu, 6 Feb 2014 17:22:43 +0000 (11:22 -0600)]
minor cleanup for merge

10 years agominor fix for merge
Tianyi Liang [Wed, 5 Feb 2014 15:19:23 +0000 (09:19 -0600)]
minor fix for merge

10 years agoescaped characters, having an issue with smt-lib defintion, further repair is needed.
Tianyi Liang [Tue, 11 Feb 2014 22:35:17 +0000 (16:35 -0600)]
escaped characters, having an issue with smt-lib defintion, further repair is needed.

10 years agoFix build (some nonexistent files listed in Makefile)
Morgan Deters [Tue, 11 Feb 2014 02:05:09 +0000 (21:05 -0500)]
Fix build (some nonexistent files listed in Makefile)

10 years agoMore complete guess instantiation strategy, cvc4 now typically times out instead...
Andrew Reynolds [Sun, 9 Feb 2014 22:14:31 +0000 (16:14 -0600)]
More complete guess instantiation strategy, cvc4 now typically times out instead of answering unknown for benchmarks with quantifiers.  Modified regressions accordingly.  Minor fix for QCF regarding variable ordering.  Improved relevant domain computation.  Minor optimization for --mbqi=fmc

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Thu, 6 Feb 2014 17:26:24 +0000 (11:26 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agominor cleanup for merge
Tianyi Liang [Thu, 6 Feb 2014 17:22:43 +0000 (11:22 -0600)]
minor cleanup for merge

10 years agominor fix for merge
Tianyi Liang [Wed, 5 Feb 2014 15:19:23 +0000 (09:19 -0600)]
minor fix for merge

10 years agominor cleanup for merge
Tianyi Liang [Thu, 6 Feb 2014 17:22:43 +0000 (11:22 -0600)]
minor cleanup for merge

10 years agoMinor fix for previous commit
Morgan Deters [Thu, 6 Feb 2014 16:13:24 +0000 (11:13 -0500)]
Minor fix for previous commit

10 years agoOops.. premature push on lexer fix (remove debugging output)
Morgan Deters [Thu, 6 Feb 2014 16:07:34 +0000 (11:07 -0500)]
Oops.. premature push on lexer fix (remove debugging output)

10 years agoFixes for escape-handling for string literals in SMT-LIBv2 lexer
Morgan Deters [Thu, 6 Feb 2014 16:05:07 +0000 (11:05 -0500)]
Fixes for escape-handling for string literals in SMT-LIBv2 lexer

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Wed, 5 Feb 2014 15:20:37 +0000 (09:20 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agominor fix for merge
Tianyi Liang [Wed, 5 Feb 2014 15:19:23 +0000 (09:19 -0600)]
minor fix for merge

10 years agominor fix for merge
Tianyi Liang [Wed, 5 Feb 2014 15:19:23 +0000 (09:19 -0600)]
minor fix for merge

10 years agoBug fix for theory strings related to old cycle detection code (was leading to bogus...
Andrew Reynolds [Wed, 5 Feb 2014 10:23:47 +0000 (04:23 -0600)]
Bug fix for theory strings related to old cycle detection code (was leading to bogus model).  Minor cleanup of QCF.

10 years agoDo not use transitive closure module for cycle detection in datatypes (was bottleneck).
Andrew Reynolds [Tue, 4 Feb 2014 16:03:25 +0000 (10:03 -0600)]
Do not use transitive closure module for cycle detection in datatypes (was bottleneck).

10 years agoAdd variable ordering for QCF to accelerate matching procedure. Preparing for QCF_MC...
Andrew Reynolds [Tue, 4 Feb 2014 15:00:28 +0000 (09:00 -0600)]
Add variable ordering for QCF to accelerate matching procedure.  Preparing for QCF_MC mode.

10 years agoHandle nested (universal) quantifiers in QCF algorithm. Make relevant domain instant...
Andrew Reynolds [Mon, 3 Feb 2014 16:23:28 +0000 (10:23 -0600)]
Handle nested (universal) quantifiers in QCF algorithm.  Make relevant domain instantiation breadth-first.

10 years agoSubstr fix: (= (str.substr "" 0 3) "xxx") should be SAT in the defintion of SMT-Lib
Tianyi Liang [Fri, 31 Jan 2014 18:22:07 +0000 (12:22 -0600)]
Substr fix: (= (str.substr "" 0 3) "xxx") should be SAT in the defintion of SMT-Lib

10 years agoRefactor QCF slightly. Bug fix for relevant domain (non-ground terms were added...
Andrew Reynolds [Thu, 30 Jan 2014 22:13:17 +0000 (16:13 -0600)]
Refactor QCF slightly.  Bug fix for relevant domain (non-ground terms were added).  Bug fix for QCF (was missing instantiations due to not using getRepresentative).

10 years agostats for eq/diseq splits
Tianyi Liang [Thu, 30 Jan 2014 22:30:21 +0000 (16:30 -0600)]
stats for eq/diseq splits

10 years agoanother name change
Tianyi Liang [Thu, 30 Jan 2014 21:26:50 +0000 (15:26 -0600)]
another name change

10 years agochange string stats text names
Tianyi Liang [Thu, 30 Jan 2014 21:18:09 +0000 (15:18 -0600)]
change string stats text names

10 years agoadds stats
Tianyi Liang [Thu, 30 Jan 2014 21:10:58 +0000 (15:10 -0600)]
adds stats

10 years agoroll back to uf implementation for substr and charat
Tianyi Liang [Wed, 29 Jan 2014 18:05:02 +0000 (12:05 -0600)]
roll back to uf implementation for substr and charat

10 years agoadd prefixof, suffixof
Tianyi Liang [Wed, 29 Jan 2014 16:32:17 +0000 (10:32 -0600)]
add prefixof, suffixof

10 years agomerge internal and user of charat & substr into one
Tianyi Liang [Tue, 28 Jan 2014 23:17:51 +0000 (17:17 -0600)]
merge internal and user of charat & substr into one

10 years agoMore optimizations of quantifier instantiation data structures.
Andrew Reynolds [Tue, 28 Jan 2014 15:51:33 +0000 (09:51 -0600)]
More optimizations of quantifier instantiation data structures.

10 years agoMerge branch '1.3.x'
Morgan Deters [Mon, 27 Jan 2014 23:04:10 +0000 (18:04 -0500)]
Merge branch '1.3.x'

10 years agoURL update
Morgan Deters [Mon, 27 Jan 2014 23:04:04 +0000 (18:04 -0500)]
URL update

10 years agoMore optimization of QCF and instantiation caching. Fix CDInstMatchTrie.
Andrew Reynolds [Mon, 27 Jan 2014 14:34:52 +0000 (08:34 -0600)]
More optimization of QCF and instantiation caching.  Fix CDInstMatchTrie.

10 years agoMore optimization of QCF. Fixed InstMatchTrie for caching instantiations. Use non...
Andrew Reynolds [Sun, 26 Jan 2014 20:23:51 +0000 (14:23 -0600)]
More optimization of QCF.  Fixed InstMatchTrie for caching instantiations.  Use non-context dependent cache for instantiations when not incremental.  Instantiate from relevant domain when no other instantiations apply.  Minor cleanup of relevance for triggers.