cvc5.git
9 years agoHandle recursive singleton case for codatatypes, add regression. Simplify implementa...
ajreynol [Fri, 13 Feb 2015 13:12:32 +0000 (14:12 +0100)]
Handle recursive singleton case for codatatypes, add regression.  Simplify implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes.

9 years agotry curl before wget, workaround for issue with FTP PASV
Kshitij Bansal [Thu, 12 Feb 2015 13:49:50 +0000 (08:49 -0500)]
try curl before wget, workaround for issue with FTP PASV

9 years agoChanging CXXFLAGS for custom cln installation in configure.ac.
Tim King [Thu, 12 Feb 2015 11:04:57 +0000 (12:04 +0100)]
Changing CXXFLAGS for custom cln installation in configure.ac.

Making sure the CVC4 flags do not get overwritten after being set.

9 years agoBetter support for solving multiple functions with cegqi-si. Minor cleanup.
ajreynol [Wed, 11 Feb 2015 18:07:49 +0000 (19:07 +0100)]
Better support for solving multiple functions with cegqi-si.  Minor cleanup.

9 years agoMove si solution reconstruction to own file, make more robust. Other refactoring.
ajreynol [Wed, 11 Feb 2015 12:10:11 +0000 (13:10 +0100)]
Move si solution reconstruction to own file, make more robust. Other refactoring.

9 years agoHandle missing cases for single inv solution reconstruction. Minor fixes. Refactor.
ajreynol [Fri, 6 Feb 2015 08:35:49 +0000 (09:35 +0100)]
Handle missing cases for single inv solution reconstruction.  Minor fixes. Refactor.

9 years agoMinor clean up
Tianyi Liang [Fri, 6 Feb 2015 00:42:08 +0000 (18:42 -0600)]
Minor clean up

9 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Fri, 6 Feb 2015 00:29:06 +0000 (18:29 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

9 years agoImproved string performance, thanks to Peter's benchmarks.
Tianyi Liang [Fri, 6 Feb 2015 00:27:47 +0000 (18:27 -0600)]
Improved string performance, thanks to Peter's benchmarks.

9 years agoImproved string performance, thanks to Peter's benchmarks.
Tianyi Liang [Fri, 6 Feb 2015 00:27:47 +0000 (18:27 -0600)]
Improved string performance, thanks to Peter's benchmarks.

9 years agoWorking version of sygus solution reconstruction from single inv cegqi. Heuristics...
ajreynol [Thu, 5 Feb 2015 13:50:09 +0000 (14:50 +0100)]
Working version of sygus solution reconstruction from single inv cegqi.  Heuristics to fit syntax.

9 years agoInitial draft of solution reconstruction into syntax for single inv cegqi.
ajreynol [Wed, 4 Feb 2015 21:16:45 +0000 (22:16 +0100)]
Initial draft of solution reconstruction into syntax for single inv cegqi.

9 years agoWork on solution reconstruction for single inv. Fix compiler error found by Tim...
ajreynol [Wed, 4 Feb 2015 14:25:16 +0000 (15:25 +0100)]
Work on solution reconstruction for single inv.  Fix compiler error found by Tim regarding Trace.isOn

9 years agoRefactor sygus_util to TermDb. Initial work on solution reconstruction into syntax...
ajreynol [Wed, 4 Feb 2015 12:29:28 +0000 (13:29 +0100)]
Refactor sygus_util to TermDb.  Initial work on solution reconstruction into syntax for single inv properties.

9 years agoStart work on simplifying single inv solutions. Minor.
ajreynol [Wed, 4 Feb 2015 08:19:46 +0000 (09:19 +0100)]
Start work on simplifying single inv solutions.  Minor.

9 years agoSimple variable elimination for single inv properties. Relax conditions for partial...
ajreynol [Tue, 3 Feb 2015 10:39:03 +0000 (11:39 +0100)]
Simple variable elimination for single inv properties.  Relax conditions for partial inst variables for LTE.

9 years agoSolutions for single invocation conjectures.
ajreynol [Mon, 2 Feb 2015 23:21:52 +0000 (00:21 +0100)]
Solutions for single invocation conjectures.

9 years agoSingle invocation module for counterexample guided quantifier instantiation --cegqi...
ajreynol [Mon, 2 Feb 2015 16:42:31 +0000 (17:42 +0100)]
Single invocation module for counterexample guided quantifier instantiation --cegqi-si. Minor improvements to syntax-guided case, refactoring.  Do not apply exhaustive tester inference for sygus datatypes.

9 years agoRepresentative programs must be minimal size, minor fixes, improvements to ITE handli...
ajreynol [Mon, 2 Feb 2015 07:48:51 +0000 (08:48 +0100)]
Representative programs must be minimal size, minor fixes, improvements to ITE handling in sygus.

9 years agoGeneralization of sygus lemmas based on arguments and content.
ajreynol [Sun, 1 Feb 2015 19:54:28 +0000 (20:54 +0100)]
Generalization of sygus lemmas based on arguments and content.

9 years agoBug fix fairness for commutative operators in sygus. Minor.
ajreynol [Sat, 31 Jan 2015 17:50:01 +0000 (18:50 +0100)]
Bug fix fairness for commutative operators in sygus.  Minor.

9 years agoLemmas instead of conflicts in sygus sym break (do not expand explanations). Minor...
ajreynol [Sat, 31 Jan 2015 10:12:09 +0000 (11:12 +0100)]
Lemmas instead of conflicts in sygus sym break (do not expand explanations).  Minor improvements to sygus splitting.

9 years agoGeneralize conflict clauses in sygus sym break, merge caches, refactor. Preparation...
ajreynol [Fri, 30 Jan 2015 19:59:05 +0000 (20:59 +0100)]
Generalize conflict clauses in sygus sym break, merge caches, refactor.  Preparation for single invocation properties.  Set output lang to SMT2 for sygus.

9 years agoApply sygus search space narrowing for all subprograms of current global state.
ajreynol [Thu, 29 Jan 2015 16:09:21 +0000 (17:09 +0100)]
Apply sygus search space narrowing for all subprograms of current global state.

9 years agoRestrict LtePartialInst instantiations based on E-matching, promote to quantifiers...
ajreynol [Thu, 29 Jan 2015 12:08:31 +0000 (13:08 +0100)]
Restrict LtePartialInst instantiations based on E-matching, promote to quantifiers module.  Refactor QuantifiersEngine registration and check.

9 years agoApply global search space narrowing for multiple synth-fun, enable its conflict lemmas.
ajreynol [Thu, 29 Jan 2015 09:17:58 +0000 (10:17 +0100)]
Apply global search space narrowing for multiple synth-fun, enable its conflict lemmas.

9 years agoAdd module for sygus search space narrowing based on global state.
ajreynol [Thu, 29 Jan 2015 07:27:18 +0000 (08:27 +0100)]
Add module for sygus search space narrowing based on global state.

9 years agoMinor refactor CEGQI.
ajreynol [Wed, 28 Jan 2015 14:21:21 +0000 (15:21 +0100)]
Minor refactor CEGQI.

9 years agoAlways miniscope nested quantifiers. Disable miniscoping when cegqi enabled. Simpli...
ajreynol [Tue, 27 Jan 2015 17:17:27 +0000 (18:17 +0100)]
Always miniscope nested quantifiers.  Disable miniscoping when cegqi enabled.  Simplify option names.

9 years agoRecognize when synthesis conjectures are in single invocation fragment.
ajreynol [Tue, 27 Jan 2015 13:09:32 +0000 (14:09 +0100)]
Recognize when synthesis conjectures are in single invocation fragment.

9 years agoOutput solutions for synthesis conjectures with --dump-synth. Minor refactor of...
ajreynol [Mon, 26 Jan 2015 12:11:01 +0000 (13:11 +0100)]
Output solutions for synthesis conjectures with --dump-synth.  Minor refactor of previous commit.

9 years agoGeneralize sygus search space narrowing to arbitrary theory rewriting.
ajreynol [Mon, 26 Jan 2015 09:41:51 +0000 (10:41 +0100)]
Generalize sygus search space narrowing to arbitrary theory rewriting.

9 years agoVariable patterns only look at eligible terms. Minor refactoring of quantifiers...
ajreynol [Sat, 24 Jan 2015 18:42:21 +0000 (19:42 +0100)]
Variable patterns only look at eligible terms.  Minor refactoring of quantifiers check for sat.

9 years agoAdd --lte-restrict-inst-closure option. Push dt.size fairness constraints inside...
ajreynol [Sat, 24 Jan 2015 18:00:59 +0000 (19:00 +0100)]
Add --lte-restrict-inst-closure option.  Push dt.size fairness constraints inside splitting lemmas for sygus.

9 years agoRefactor sygus arg nf. Minor improvements.
ajreynol [Fri, 23 Jan 2015 19:40:57 +0000 (20:40 +0100)]
Refactor sygus arg nf.  Minor improvements.

9 years agoCEGQI fairness based on term height. Fix sygus-nf fairness bug for wrongly applied...
ajreynol [Fri, 23 Jan 2015 13:53:19 +0000 (14:53 +0100)]
CEGQI fairness based on term height.  Fix sygus-nf fairness bug for wrongly applied selectors.

9 years agoRework inst-closure.
ajreynol [Fri, 23 Jan 2015 09:04:38 +0000 (10:04 +0100)]
Rework inst-closure.

9 years agoNarrow sygus search space based on NNF and rewriting constant arguments.
ajreynol [Thu, 22 Jan 2015 16:09:29 +0000 (17:09 +0100)]
Narrow sygus search space based on NNF and rewriting constant arguments.

9 years agoAdd option --lte-partial-inst. Remove inst-closure.
ajreynol [Thu, 22 Jan 2015 10:47:39 +0000 (11:47 +0100)]
Add option --lte-partial-inst.  Remove inst-closure.

9 years agoDo not drop patterns during boolean term rewriting. Narrow sygus search space based...
ajreynol [Thu, 22 Jan 2015 08:40:51 +0000 (09:40 +0100)]
Do not drop patterns during boolean term rewriting. Narrow sygus search space based on commutative operators.

9 years agoAvoid redundant constant arguments for SygusNormalForm. Refactor.
ajreynol [Wed, 21 Jan 2015 14:44:27 +0000 (15:44 +0100)]
Avoid redundant constant arguments for SygusNormalForm. Refactor.

9 years agoInitial work on sygusNormalForm.
ajreynol [Wed, 21 Jan 2015 10:34:55 +0000 (11:34 +0100)]
Initial work on sygusNormalForm.

9 years agoMark datatypes as sygus. Add option to normalize sygus terms in search. Add sygus...
ajreynol [Tue, 20 Jan 2015 13:23:04 +0000 (14:23 +0100)]
Mark datatypes as sygus.  Add option to normalize sygus terms in search.  Add sygus regressions.

9 years agoHandle miniscoping of conjunctions in synthesis properties. Refactor construction...
ajreynol [Tue, 20 Jan 2015 09:23:08 +0000 (10:23 +0100)]
Handle miniscoping of conjunctions in synthesis properties.  Refactor construction of sygus datatypes.  Expand define-fun in evaluators.

9 years agoAdding tests for get-value output for arithmetic.
Tim King [Mon, 19 Jan 2015 17:57:29 +0000 (18:57 +0100)]
Adding tests for get-value output for arithmetic.

Fixing bug where (- 1).0 was printed by get-value. Thanks to Christoph Sticksel for the bug report.

9 years agoAdding an additional search path to configure.ac for cxxtestgen to reflect the cxxtes...
Tim King [Fri, 16 Jan 2015 10:31:33 +0000 (11:31 +0100)]
Adding an additional search path to configure.ac for cxxtestgen to reflect the cxxtest git repository.

9 years agoAvoid name conflicts for multiple synth-fun.
ajreynol [Sat, 17 Jan 2015 10:01:32 +0000 (11:01 +0100)]
Avoid name conflicts for multiple synth-fun.

9 years agoLinearize multiplication by constants in sygus grammars. Handle unary minus integer...
ajreynol [Fri, 16 Jan 2015 16:17:56 +0000 (17:17 +0100)]
Linearize multiplication by constants in sygus grammars. Handle unary minus integer numerals.  Refactor to smt2.cpp.

9 years agoAllow uninterpreted/defined functions in Sygus grammars. Fix bug regarding declare...
ajreynol [Fri, 16 Jan 2015 11:38:08 +0000 (12:38 +0100)]
Allow uninterpreted/defined functions in Sygus grammars. Fix bug regarding declare-var vs synth-fun arguments.  Handle ground properties in sythesis conjectures.

9 years agoMinor: Ensure indexed terms are in EE. Add support for bv constants in sygus parser.
ajreynol [Fri, 16 Jan 2015 08:29:15 +0000 (09:29 +0100)]
Minor: Ensure indexed terms are in EE.  Add support for bv constants in sygus parser.

9 years agosygus input language and benchmark
Morgan Deters [Fri, 24 Oct 2014 00:58:08 +0000 (20:58 -0400)]
sygus input language and benchmark

9 years agoFix #line numbering.
Morgan Deters [Tue, 13 Jan 2015 20:00:31 +0000 (15:00 -0500)]
Fix #line numbering.

9 years agoFix a memory issue in ResourceManager on 32-bit (resolves bug #606).
Morgan Deters [Tue, 13 Jan 2015 19:40:05 +0000 (14:40 -0500)]
Fix a memory issue in ResourceManager on 32-bit (resolves bug #606).

9 years agoRemove private #include.
Morgan Deters [Tue, 13 Jan 2015 19:18:09 +0000 (14:18 -0500)]
Remove private #include.

9 years agoFix typo.
Morgan Deters [Tue, 13 Jan 2015 18:24:09 +0000 (13:24 -0500)]
Fix typo.

9 years agoRemove old .orig files that were added to the repository.
Morgan Deters [Tue, 13 Jan 2015 00:10:03 +0000 (19:10 -0500)]
Remove old .orig files that were added to the repository.

9 years agoadjusted to both v2.0 and v2.5 string literals
Tianyi Liang [Sun, 11 Jan 2015 18:00:10 +0000 (12:00 -0600)]
adjusted to both v2.0 and v2.5 string literals

9 years agoblocked unprintable characters in string literals;
Tianyi Liang [Fri, 9 Jan 2015 15:40:10 +0000 (09:40 -0600)]
blocked unprintable characters in string literals;
disabled string literal test case for smtlib v2.5

9 years agoswitch ascii encoding to unsigned char
Tianyi Liang [Thu, 8 Jan 2015 17:37:58 +0000 (11:37 -0600)]
switch ascii encoding to unsigned char

9 years agopatch to the last commit
Tianyi Liang [Wed, 7 Jan 2015 18:24:14 +0000 (12:24 -0600)]
patch to the last commit

9 years agobug fix, thanks to Pierre's report
Tianyi Liang [Wed, 7 Jan 2015 16:50:58 +0000 (10:50 -0600)]
bug fix, thanks to Pierre's report

9 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Wed, 7 Jan 2015 16:03:29 +0000 (10:03 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

9 years agoadded initial AX rules;
Tianyi Liang [Wed, 7 Jan 2015 16:02:01 +0000 (10:02 -0600)]
added initial AX rules;
fixed a bug for empty string in regex

9 years agoadded initial AX rules;
Tianyi Liang [Wed, 7 Jan 2015 16:02:01 +0000 (10:02 -0600)]
added initial AX rules;
fixed a bug for empty string in regex

9 years agoDisable prenex by default when using fmf bound int, minor improvement to datatypes...
ajreynol [Sun, 28 Dec 2014 04:42:28 +0000 (05:42 +0100)]
Disable prenex by default when using fmf bound int, minor improvement to datatypes rewriter

9 years agoAdding an option to the equality engine constructor to treat all constants as
Dejan Jovanovic [Sat, 27 Dec 2014 03:15:13 +0000 (19:15 -0800)]
Adding an option to the equality engine constructor to treat all constants as
trigger terms. I've disabled constants as triggers for all equality engines
except for the shared terms engine where it is needed.

9 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Mon, 22 Dec 2014 22:24:08 +0000 (16:24 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

9 years agobug fix for constant regular expression model building
Tianyi Liang [Mon, 22 Dec 2014 22:22:42 +0000 (16:22 -0600)]
bug fix for constant regular expression model building

9 years agobug fix for constant regular expression model building
Tianyi Liang [Mon, 22 Dec 2014 22:22:42 +0000 (16:22 -0600)]
bug fix for constant regular expression model building

9 years agoDo not collapse wrongly applied selectors for non-well-founded codatatypes pre-model.
ajreynol [Mon, 22 Dec 2014 22:21:40 +0000 (23:21 +0100)]
Do not collapse wrongly applied selectors for non-well-founded codatatypes pre-model.

9 years agoAdd misc trigger options.
ajreynol [Sun, 21 Dec 2014 23:49:27 +0000 (00:49 +0100)]
Add misc trigger options.

9 years agoFix oversight in dumping assertions in preprocessing.
Morgan Deters [Tue, 16 Dec 2014 23:04:47 +0000 (18:04 -0500)]
Fix oversight in dumping assertions in preprocessing.

9 years agoAdd cvc parsing support for cardinality constraints. Bug fix for enumerating element...
ajreynol [Fri, 12 Dec 2014 11:03:26 +0000 (12:03 +0100)]
Add cvc parsing support for cardinality constraints.  Bug fix for enumerating elements to meet cardinality lower bounds.

9 years agoMinor fixes to language bindings. (Resolves #607.)
Morgan Deters [Thu, 11 Dec 2014 22:04:29 +0000 (17:04 -0500)]
Minor fixes to language bindings. (Resolves #607.)

9 years agoOption to enable/disable cyclicity check in datatypes.
ajreynol [Thu, 11 Dec 2014 13:09:54 +0000 (14:09 +0100)]
Option to enable/disable cyclicity check in datatypes.

9 years agobug fix, thanks to Guy's example.
Tianyi Liang [Thu, 11 Dec 2014 02:59:32 +0000 (20:59 -0600)]
bug fix, thanks to Guy's example.

9 years agoBetter error description (related to bug 605).
Morgan Deters [Tue, 9 Dec 2014 23:48:55 +0000 (18:48 -0500)]
Better error description (related to bug 605).

9 years agoCleanup.
Morgan Deters [Tue, 9 Dec 2014 23:48:43 +0000 (18:48 -0500)]
Cleanup.

9 years agoAdded string constant in java api example.
Tianyi Liang [Sat, 6 Dec 2014 21:28:52 +0000 (15:28 -0600)]
Added string constant in java api example.

9 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Sat, 6 Dec 2014 19:26:39 +0000 (13:26 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

9 years agoAdded C++/Java api examples;
Tianyi Liang [Sat, 6 Dec 2014 19:24:01 +0000 (13:24 -0600)]
Added C++/Java api examples;
Converted cset to be vector of char, instead of vector of int, since we only accept ascii in input.

9 years agoAdded C++/Java api examples;
Tianyi Liang [Sat, 6 Dec 2014 19:24:01 +0000 (13:24 -0600)]
Added C++/Java api examples;
Converted cset to be vector of char, instead of vector of int, since we only accept ascii in input.

9 years agoFix dt.size care graph.
ajreynol [Sat, 6 Dec 2014 00:26:44 +0000 (01:26 +0100)]
Fix dt.size care graph.

9 years agoRelaxed the constant requirement for regular expression loop;
Tianyi Liang [Fri, 5 Dec 2014 00:17:55 +0000 (18:17 -0600)]
Relaxed the constant requirement for regular expression loop;
Added "ignoring negative membership" option (fragment checking is not provided,
and users must make sure the constraint is in the fragment;
otherwise, the solution may not be correct).

9 years agoclean up and improve intersection
Tianyi Liang [Thu, 4 Dec 2014 22:13:41 +0000 (16:13 -0600)]
clean up and improve intersection

9 years agoFix valgrind-flagged error about uninitialized value.
Morgan Deters [Thu, 4 Dec 2014 06:40:21 +0000 (01:40 -0500)]
Fix valgrind-flagged error about uninitialized value.

9 years agoFix segfault in lambdas when constructed via API.
Morgan Deters [Thu, 4 Dec 2014 06:39:53 +0000 (01:39 -0500)]
Fix segfault in lambdas when constructed via API.

9 years agoFix UnsatCore in language bindings.
Morgan Deters [Thu, 4 Dec 2014 02:58:50 +0000 (21:58 -0500)]
Fix UnsatCore in language bindings.

9 years agoFloating point infrastructure.
Martin Brain [Thu, 4 Dec 2014 02:29:43 +0000 (21:29 -0500)]
Floating point infrastructure.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
9 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Kshitij Bansal [Wed, 3 Dec 2014 17:09:14 +0000 (12:09 -0500)]
Merge branch 'master' of https://github.com/CVC4/CVC4

9 years agoRevert "Disable constants sharing in eq engine, disable hack in theory engine."
Kshitij Bansal [Wed, 3 Dec 2014 16:38:36 +0000 (11:38 -0500)]
Revert "Disable constants sharing in eq engine, disable hack in theory engine."

This partially reverts commit f70804a7159390fcb01d8c1ec208fbfd8e544fba.

In particular, it DOES NOT revert
  "Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring.  Fix assertion failure in quantifiers engine."
which is part of the same commit.

9 years agodisable inter cache
Tianyi Liang [Wed, 3 Dec 2014 05:44:26 +0000 (23:44 -0600)]
disable inter cache

10 years agoSynchronize conjecture generation with E-matching. Minor fix to --full-saturate...
ajreynol [Fri, 28 Nov 2014 15:27:19 +0000 (16:27 +0100)]
Synchronize conjecture generation with E-matching.  Minor fix to --full-saturate-quant.

10 years agoadd intersection rewriting
Tianyi Liang [Thu, 27 Nov 2014 04:09:38 +0000 (22:09 -0600)]
add intersection rewriting

10 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Thu, 27 Nov 2014 01:34:37 +0000 (19:34 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

10 years agoadd more regexp rewriting
Tianyi Liang [Thu, 27 Nov 2014 01:32:32 +0000 (19:32 -0600)]
add more regexp rewriting

10 years agoadd more functions for regular expressions
Tianyi Liang [Thu, 27 Nov 2014 00:11:35 +0000 (18:11 -0600)]
add more functions for regular expressions

10 years agoadd more regexp rewriting
Tianyi Liang [Thu, 27 Nov 2014 01:32:32 +0000 (19:32 -0600)]
add more regexp rewriting

10 years agoadd more functions for regular expressions
Tianyi Liang [Thu, 27 Nov 2014 00:11:35 +0000 (18:11 -0600)]
add more functions for regular expressions

10 years agoFix bug in --term-db-mode=relevant with variable triggers. Support inst-closure...
ajreynol [Tue, 25 Nov 2014 15:15:10 +0000 (16:15 +0100)]
Fix bug in --term-db-mode=relevant with variable triggers.  Support inst-closure predicate and mode --term-db-inst-closure.  Minor changes to theory_quantifiers.