cvc5.git
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 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 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.

10 years agoreplace charat uf with internal one
Tianyi Liang [Sat, 25 Jan 2014 18:49:19 +0000 (12:49 -0600)]
replace charat uf with internal one

10 years agominor fix, indexof rewriter opt
Tianyi Liang [Sat, 25 Jan 2014 04:32:45 +0000 (22:32 -0600)]
minor fix, indexof rewriter opt

10 years agofix: indexof, replace rewriting
Tianyi Liang [Fri, 24 Jan 2014 23:50:47 +0000 (17:50 -0600)]
fix: indexof, replace rewriting

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

10 years agorev diseq
Tianyi Liang [Fri, 24 Jan 2014 21:39:13 +0000 (15:39 -0600)]
rev diseq

10 years agorev const split
Tianyi Liang [Fri, 24 Jan 2014 20:22:37 +0000 (14:22 -0600)]
rev const split

10 years agooptimize for the reverse direction
Tianyi Liang [Fri, 24 Jan 2014 17:58:07 +0000 (11:58 -0600)]
optimize for the reverse direction

10 years agorev diseq
Tianyi Liang [Fri, 24 Jan 2014 21:39:13 +0000 (15:39 -0600)]
rev diseq

10 years agorev const split
Tianyi Liang [Fri, 24 Jan 2014 20:22:37 +0000 (14:22 -0600)]
rev const split

10 years agoSimplify the QCF algorithm by more aggressive flattening, removes EqRegistry approach...
Andrew Reynolds [Fri, 24 Jan 2014 19:58:52 +0000 (13:58 -0600)]
Simplify the QCF algorithm by more aggressive flattening, removes EqRegistry approach.  Minor change to quantifier macros.  Add option --quant-cf-mode.

10 years agooptimize for the reverse direction
Tianyi Liang [Fri, 24 Jan 2014 17:58:07 +0000 (11:58 -0600)]
optimize for the reverse direction

10 years agofix: constants are inferred to be the same
Tianyi Liang [Thu, 23 Jan 2014 22:59:58 +0000 (16:59 -0600)]
fix: constants are inferred to be the same

10 years agominor fix
Tianyi Liang [Thu, 23 Jan 2014 08:48:41 +0000 (02:48 -0600)]
minor fix

10 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Tianyi Liang [Wed, 22 Jan 2014 20:08:47 +0000 (14:08 -0600)]
Merge branch 'master' of https://github.com/CVC4/CVC4

10 years agoSome minor fixes to SmtEngine strings settings.
Morgan Deters [Wed, 22 Jan 2014 20:08:04 +0000 (15:08 -0500)]
Some minor fixes to SmtEngine strings settings.

10 years agocommented out all_supported in strings for now, it has a bug here.
Tianyi Liang [Wed, 22 Jan 2014 20:07:10 +0000 (14:07 -0600)]
commented out all_supported in strings for now, it has a bug here.

10 years agosolve string exp issue for regexp
Tianyi Liang [Wed, 22 Jan 2014 19:50:39 +0000 (13:50 -0600)]
solve string exp issue for regexp

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Wed, 22 Jan 2014 19:42:54 +0000 (13:42 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

Conflicts:
src/smt/smt_engine.cpp

10 years agoadd warning for using strings in ALL_SUPPORTED
Tianyi Liang [Wed, 22 Jan 2014 19:40:54 +0000 (13:40 -0600)]
add warning for using strings in ALL_SUPPORTED

10 years agoSmarter options, but still have a bug
Tianyi Liang [Tue, 21 Jan 2014 19:40:00 +0000 (13:40 -0600)]
Smarter options, but still have a bug

10 years agoDelay QuantifiersEngine and UF strong solver initialization until after final options...
Morgan Deters [Wed, 22 Jan 2014 15:06:04 +0000 (10:06 -0500)]
Delay QuantifiersEngine and UF strong solver initialization until after final options/logic are set.

10 years agoSmarter options, but still have a bug
Tianyi Liang [Tue, 21 Jan 2014 19:40:00 +0000 (13:40 -0600)]
Smarter options, but still have a bug

10 years agoimprove string contains
Tianyi Liang [Tue, 21 Jan 2014 00:09:11 +0000 (18:09 -0600)]
improve string contains

10 years agoimprove string contains
Tianyi Liang [Mon, 20 Jan 2014 22:45:11 +0000 (16:45 -0600)]
improve string contains

10 years agoFixed non-termination issue in bounded integers.
Andrew Reynolds [Sat, 18 Jan 2014 18:13:47 +0000 (12:13 -0600)]
Fixed non-termination issue in bounded integers.

10 years agoPerformance optimization for E-matching, working on using QCF module for propagations.
Andrew Reynolds [Sat, 18 Jan 2014 17:27:45 +0000 (11:27 -0600)]
Performance optimization for E-matching, working on using QCF module for propagations.

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Sat, 18 Jan 2014 17:11:03 +0000 (11:11 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agostrings with new ideas
Tianyi Liang [Fri, 17 Jan 2014 23:56:08 +0000 (17:56 -0600)]
strings with new ideas

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

10 years agoFix for quote-escaping in smt2 printer
Morgan Deters [Sat, 18 Jan 2014 03:59:39 +0000 (22:59 -0500)]
Fix for quote-escaping in smt2 printer

10 years agostrings with new ideas
Tianyi Liang [Fri, 17 Jan 2014 23:56:08 +0000 (17:56 -0600)]
strings with new ideas

10 years agoMore optimizations for quantifiers conflict find. Add trust user patterns mode.
Andrew Reynolds [Fri, 17 Jan 2014 15:57:12 +0000 (09:57 -0600)]
More optimizations for quantifiers conflict find.  Add trust user patterns mode.

10 years agoMerge branch '1.3.x'
Kshitij Bansal [Fri, 17 Jan 2014 14:12:25 +0000 (09:12 -0500)]
Merge branch '1.3.x'

10 years agoenable search for html doc
Kshitij Bansal [Fri, 17 Jan 2014 14:11:58 +0000 (09:11 -0500)]
enable search for html doc

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Thu, 16 Jan 2014 21:40:01 +0000 (15:40 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

Conflicts:
src/printer/smt2/smt2_printer.cpp

10 years agoadds partial functions
Tianyi Liang [Thu, 16 Jan 2014 21:37:58 +0000 (15:37 -0600)]
adds partial functions

10 years agoadds smt2 print for strings
Tianyi Liang [Wed, 15 Jan 2014 23:20:27 +0000 (17:20 -0600)]
adds smt2 print for strings

10 years agoadds smt2 print for strings
Tianyi Liang [Wed, 15 Jan 2014 23:20:27 +0000 (17:20 -0600)]
adds smt2 print for strings

10 years agoOptimizations for quantifiers conflict find: better caching, process matching constra...
Andrew Reynolds [Wed, 15 Jan 2014 16:22:10 +0000 (10:22 -0600)]
Optimizations for quantifiers conflict find: better caching, process matching constraints eagerly.

10 years agonormal form breaking
Tianyi Liang [Fri, 10 Jan 2014 23:42:01 +0000 (17:42 -0600)]
normal form breaking

10 years agoadd repalce
Tianyi Liang [Fri, 10 Jan 2014 19:26:56 +0000 (13:26 -0600)]
add repalce

10 years agoAdd stats to quantifiers conflict find. Added option for qcf. Working on handling...
Andrew Reynolds [Fri, 10 Jan 2014 16:50:56 +0000 (10:50 -0600)]
Add stats to quantifiers conflict find.  Added option for qcf.  Working on handling non-APPLY_UF terms.

10 years agoAdd new method --quant-cf for finding conflicts eagerly for quantified formulas....
Andrew Reynolds [Fri, 10 Jan 2014 08:04:51 +0000 (02:04 -0600)]
Add new method --quant-cf for finding conflicts eagerly for quantified formulas.  This module can efficiently determine when there exists a conflict wrt quantified formulas that is implied by the current set of equalities, and reports the single lemma corresponding to the conflict. It does so before resorting to heuristic instantiation.  Clean up the rewriter, other minor cleanup.

10 years agomove new functions under exp options
Tianyi Liang [Fri, 10 Jan 2014 00:23:15 +0000 (18:23 -0600)]
move new functions under exp options

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Thu, 9 Jan 2014 22:25:34 +0000 (16:25 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agoadd constant replace, indexof
Tianyi Liang [Thu, 9 Jan 2014 22:23:59 +0000 (16:23 -0600)]
add constant replace, indexof

10 years agoadd constant replace, indexof
Tianyi Liang [Thu, 9 Jan 2014 22:23:59 +0000 (16:23 -0600)]
add constant replace, indexof

10 years agoMerge branch '1.3.x'
Morgan Deters [Thu, 9 Jan 2014 21:48:32 +0000 (16:48 -0500)]
Merge branch '1.3.x'

10 years agogmp is again default, not cln, for build ID (reverting due to license discussion...
Morgan Deters [Thu, 9 Jan 2014 21:48:21 +0000 (16:48 -0500)]
gmp is again default, not cln, for build ID (reverting due to license discussion at Monday meeting)

10 years agoAnother way to handle negative contain
Tianyi Liang [Thu, 9 Jan 2014 19:24:27 +0000 (13:24 -0600)]
Another way to handle negative contain

10 years agoMerge branch '1.3.x'
Morgan Deters [Wed, 8 Jan 2014 20:32:59 +0000 (15:32 -0500)]
Merge branch '1.3.x'

Conflicts:
COPYING
NEWS
config/cvc4.m4

10 years agoSwitch license default back to BSD, and add --best and --enable-gpl options.
Morgan Deters [Wed, 8 Jan 2014 20:27:26 +0000 (15:27 -0500)]
Switch license default back to BSD, and add --best and --enable-gpl options.

10 years agoCache apt packages on Travis.
Morgan Deters [Wed, 18 Dec 2013 02:13:12 +0000 (21:13 -0500)]
Cache apt packages on Travis.

10 years agoclean some code
Tianyi Liang [Wed, 8 Jan 2014 18:07:56 +0000 (12:07 -0600)]
clean some code

10 years agoFix LogicInfo parsing for string logics
Morgan Deters [Wed, 8 Jan 2014 16:18:02 +0000 (11:18 -0500)]
Fix LogicInfo parsing for string logics

10 years agoFix LogicInfo parsing for string logics
Morgan Deters [Wed, 8 Jan 2014 16:17:32 +0000 (11:17 -0500)]
Fix LogicInfo parsing for string logics

10 years agoremove a warning in strings
Tianyi Liang [Wed, 8 Jan 2014 02:04:27 +0000 (20:04 -0600)]
remove a warning in strings

10 years agominor fix, bring back the assertion.
Tianyi Liang [Wed, 8 Jan 2014 01:18:55 +0000 (19:18 -0600)]
minor fix, bring back the assertion.

10 years agostring contain changes
Tianyi Liang [Wed, 8 Jan 2014 00:12:08 +0000 (18:12 -0600)]
string contain changes

10 years agoRemoving and consolidating options for uf-ss and quantifiers. Bug fix for inst gen...
Andrew Reynolds [Sat, 4 Jan 2014 04:36:55 +0000 (22:36 -0600)]
Removing and consolidating options for uf-ss and quantifiers.  Bug fix for inst gen-style MBQI.

10 years agoAdded support for proof production in Equality Engine. Cleaned up existing proof...
Andrew Reynolds [Fri, 3 Jan 2014 18:13:13 +0000 (12:13 -0600)]
Added support for proof production in Equality Engine.  Cleaned up existing proof signatures and added proof signature for theory of arrays.  Added new MBQI technique based on interval abstraction.  Cleaned up option names.  Improved symmetry breaking for uf strong solver.  Other minor cleanup.

10 years agoMerge branch '1.3.x'
Morgan Deters [Thu, 2 Jan 2014 19:13:17 +0000 (14:13 -0500)]
Merge branch '1.3.x'

10 years agoUpdate copyright year.
Morgan Deters [Thu, 2 Jan 2014 19:13:08 +0000 (14:13 -0500)]
Update copyright year.

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Fri, 27 Dec 2013 17:27:16 +0000 (11:27 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agominor fix
Tianyi Liang [Fri, 27 Dec 2013 17:24:14 +0000 (11:24 -0600)]
minor fix

10 years agominor fix
Tianyi Liang [Fri, 27 Dec 2013 17:24:14 +0000 (11:24 -0600)]
minor fix

10 years agoMerge branch '1.3.x'
Morgan Deters [Fri, 27 Dec 2013 17:21:25 +0000 (12:21 -0500)]
Merge branch '1.3.x'

10 years agoFix for ANTLR warning.
Morgan Deters [Fri, 27 Dec 2013 17:21:20 +0000 (12:21 -0500)]
Fix for ANTLR warning.

10 years agonew functions in strings
Tianyi Liang [Thu, 26 Dec 2013 23:18:26 +0000 (17:18 -0600)]
new functions in strings

10 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Tianyi Liang [Thu, 26 Dec 2013 00:44:59 +0000 (18:44 -0600)]
Merge branch 'master' of https://github.com/CVC4/CVC4

10 years agofix for some nightly build failures
Morgan Deters [Wed, 25 Dec 2013 22:18:40 +0000 (17:18 -0500)]
fix for some nightly build failures

10 years agoCleanup related to output language fix.
Morgan Deters [Tue, 24 Dec 2013 18:26:31 +0000 (13:26 -0500)]
Cleanup related to output language fix.

10 years agoMerge branch '1.3.x'
Morgan Deters [Tue, 24 Dec 2013 18:25:30 +0000 (13:25 -0500)]
Merge branch '1.3.x'

Conflicts:
NEWS

10 years agoBetter automatic handling of output language setting.
Morgan Deters [Tue, 24 Dec 2013 18:24:56 +0000 (13:24 -0500)]
Better automatic handling of output language setting.

10 years agoBetter get-value parse error message for common user error.
Morgan Deters [Mon, 16 Dec 2013 14:49:05 +0000 (09:49 -0500)]
Better get-value parse error message for common user error.

10 years agoMinor code cleanup.
Morgan Deters [Tue, 24 Dec 2013 17:45:13 +0000 (12:45 -0500)]
Minor code cleanup.

10 years agoMerge branch '1.3.x'
Morgan Deters [Tue, 24 Dec 2013 15:57:28 +0000 (10:57 -0500)]
Merge branch '1.3.x'

10 years agoJava datatype API fixups, datatype API examples
Morgan Deters [Mon, 3 Jun 2013 22:18:24 +0000 (18:18 -0400)]
Java datatype API fixups, datatype API examples