cvc5.git
9 years agoMinor changes related to codatatypes for 1.5 release.
ajreynol [Fri, 21 Aug 2015 12:40:06 +0000 (14:40 +0200)]
Minor changes related to codatatypes for 1.5 release.

9 years agoFix disequality bounds in cbqi, record literals for ITE skolems in cbqi. Enable...
ajreynol [Fri, 21 Aug 2015 08:07:12 +0000 (10:07 +0200)]
Fix disequality bounds in cbqi, record literals for ITE skolems in cbqi.  Enable redundant ITE branch elimination in quantifiers rewriter.

9 years agofix to bug659 due to algebraic solver model building
Liana Hadarean [Thu, 20 Aug 2015 16:21:50 +0000 (17:21 +0100)]
fix to bug659 due to algebraic solver model building

9 years agofix for bug660 and bug658 due to incorrect bit-blasting of divison by zero
Liana Hadarean [Thu, 20 Aug 2015 16:21:08 +0000 (17:21 +0100)]
fix for bug660 and bug658 due to incorrect bit-blasting of divison by zero

9 years agoMake cbqi robust to term ITE removal. Separate vts infinities for int/real.
ajreynol [Wed, 19 Aug 2015 19:45:37 +0000 (21:45 +0200)]
Make cbqi robust to term ITE removal.  Separate vts infinities for int/real.

9 years agofix bug 605
Kshitij Bansal [Wed, 19 Aug 2015 02:06:28 +0000 (22:06 -0400)]
fix bug 605

9 years agoImplementation of model-based projection in cbqi, cleanup, add regressions.
ajreynol [Wed, 19 Aug 2015 07:35:17 +0000 (09:35 +0200)]
Implementation of model-based projection in cbqi, cleanup, add regressions.

9 years agofix for bug663
Tianyi Liang [Tue, 18 Aug 2015 03:31:47 +0000 (22:31 -0500)]
fix for bug663

9 years agoMore optimizations to --macros-quant, add --macros-quant-mode=ground-uf. Cleanup...
ajreynol [Sun, 16 Aug 2015 10:44:11 +0000 (12:44 +0200)]
More optimizations to --macros-quant, add --macros-quant-mode=ground-uf. Cleanup varContains caches in term db. Fix bug related to macros in non-tracing builds.

9 years agoImprovements to --macros-quant. Enable --clause-split by default. Bug fix for cbqi...
ajreynol [Wed, 12 Aug 2015 05:33:16 +0000 (07:33 +0200)]
Improvements to --macros-quant. Enable --clause-split by default. Bug fix for cbqi regarding instantiations with free skolems, extend to boolean quantification. Infrastructure for congruence closure with free variables.

9 years agoSimplification/improvement to solving deltas in LRA cbqi. Bug fix sygus datatypes.
ajreynol [Sat, 1 Aug 2015 15:22:11 +0000 (17:22 +0200)]
Simplification/improvement to solving deltas in LRA cbqi. Bug fix sygus datatypes.

9 years agoSupport for default grammar for datatypes in sygus. Support vts for infinity.
ajreynol [Sat, 1 Aug 2015 10:25:11 +0000 (12:25 +0200)]
Support for default grammar for datatypes in sygus. Support vts for infinity.

9 years agoMake --fmf-fun and --macros-quant work in incremental mode. Add regressions.
ajreynol [Fri, 31 Jul 2015 23:31:07 +0000 (01:31 +0200)]
Make --fmf-fun and --macros-quant work in incremental mode. Add regressions.

9 years agoSygus support for inductive datatypes.
ajreynol [Fri, 31 Jul 2015 08:32:34 +0000 (10:32 +0200)]
Sygus support for inductive datatypes.

9 years agoImplement virtual term substitution for non-nested quantifiers. Fix soundness bug...
ajreynol [Thu, 30 Jul 2015 15:18:10 +0000 (17:18 +0200)]
Implement virtual term substitution for non-nested quantifiers.  Fix soundness bug in strings related to explaining length terms.

9 years agoDisable bug590.smt2
Tianyi Liang [Tue, 28 Jul 2015 02:10:33 +0000 (21:10 -0500)]
Disable bug590.smt2

9 years agominor change to the last fix
Tianyi Liang [Tue, 28 Jul 2015 01:56:46 +0000 (20:56 -0500)]
minor change to the last fix

9 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Tianyi Liang [Tue, 28 Jul 2015 01:19:35 +0000 (20:19 -0500)]
Merge branch 'master' of https://github.com/CVC4/CVC4

9 years agoHotfix for substr function.
Tianyi Liang [Tue, 28 Jul 2015 01:16:41 +0000 (20:16 -0500)]
Hotfix for substr function.

9 years agoAdd option --sygus-inv-templ for synthesizing strengthening/weakening of pre/post...
ajreynol [Sat, 25 Jul 2015 14:40:54 +0000 (16:40 +0200)]
Add option --sygus-inv-templ for synthesizing strengthening/weakening of pre/post conditions.  Dump synth by default in sygus, update regressions.  Set better defaults for induction. Fix bug in related to IFF and EQUAL in sygus grammar.

9 years agoFix for BOOST_SED_CPP for gcc-5.
Tim King [Thu, 16 Jul 2015 18:49:51 +0000 (20:49 +0200)]
Fix for BOOST_SED_CPP for gcc-5.

9 years agoSquashed merge of SygusComp 2015 branch.
ajreynol [Mon, 20 Jul 2015 17:46:21 +0000 (19:46 +0200)]
Squashed merge of SygusComp 2015 branch.

9 years agoAdd option --full-saturate-quant-rd. Fix option --register-quant-body-terms.
ajreynol [Sun, 12 Jul 2015 11:29:59 +0000 (13:29 +0200)]
Add option --full-saturate-quant-rd.  Fix option --register-quant-body-terms.

9 years agofix bug 650
Kshitij Bansal [Wed, 8 Jul 2015 13:49:48 +0000 (09:49 -0400)]
fix bug 650

9 years agoAdd options --partial-triggers, --elim-taut-quant, improve robustness of --purify...
ajreynol [Sun, 5 Jul 2015 17:56:42 +0000 (19:56 +0200)]
Add options --partial-triggers, --elim-taut-quant, improve robustness of --purify-triggers. Enable --quant-alpha-equiv by default. Fix fairness issue when combining cbqi+E-matching.  Avoid unecessary delta lemmas.  Update casc scripts.

9 years agoOn-demand upper bound lemmas for deltas in quantified LRA (for casc). Force no macros...
ajreynol [Thu, 2 Jul 2015 14:54:10 +0000 (16:54 +0200)]
On-demand upper bound lemmas for deltas in quantified LRA (for casc). Force no macros-quant in incremental. Update casc TFN script.

9 years agoAdd options --qcf-all-conflict, --ite-dtt-split-quant, refactor --ite-lift-quant...
ajreynol [Wed, 1 Jul 2015 16:42:43 +0000 (18:42 +0200)]
Add options --qcf-all-conflict, --ite-dtt-split-quant, refactor --ite-lift-quant. Minor bug fixes for internalReps, alpha equivalence.  Update casc 25 FOF script.

9 years agofix sets-translate
Kshitij Bansal [Tue, 30 Jun 2015 05:47:10 +0000 (01:47 -0400)]
fix sets-translate

9 years agofix smt2 parameterized sort printing
Kshitij Bansal [Tue, 30 Jun 2015 04:16:47 +0000 (00:16 -0400)]
fix smt2 parameterized sort printing

9 years agoModule to infer alpha equivalence of quantified formulas. Minor clean up of options.
ajreynol [Mon, 29 Jun 2015 11:30:44 +0000 (13:30 +0200)]
Module to infer alpha equivalence of quantified formulas.  Minor clean up of options.

9 years agoRefactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by default...
ajreynol [Sat, 27 Jun 2015 07:30:06 +0000 (09:30 +0200)]
Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by default on pure quantified arithmetic. Fix bug in sort inference related to mixed real/int, add regression.

9 years agoDo not assert fail for fmf empty domains. Fixes bug 644.
ajreynol [Thu, 25 Jun 2015 12:06:06 +0000 (14:06 +0200)]
Do not assert fail for fmf empty domains. Fixes bug 644.

9 years agoAdd --user-pat=interleave. Remove unused lte inst strategy.
ajreynol [Mon, 22 Jun 2015 13:27:44 +0000 (15:27 +0200)]
Add --user-pat=interleave. Remove unused lte inst strategy.

9 years agoAvoid completion for large finite types. Fix bug for --fmf-fun.
ajreynol [Tue, 16 Jun 2015 16:06:27 +0000 (18:06 +0200)]
Avoid completion for large finite types.  Fix bug for --fmf-fun.

9 years agoMake array basis term a skolem (avoids crashing in fmf).
ajreynol [Mon, 15 Jun 2015 08:59:23 +0000 (10:59 +0200)]
Make array basis term a skolem (avoids crashing in fmf).

9 years agoChanging options for QF_AUFNIA to avoid bug
Clark Barrett [Mon, 15 Jun 2015 03:38:41 +0000 (20:38 -0700)]
Changing options for QF_AUFNIA to avoid bug

9 years agoFixing an assertion Constraint::assertionFringe(...) to allow hasTrichotomyProof().
Tim King [Sun, 14 Jun 2015 22:28:10 +0000 (00:28 +0200)]
Fixing an assertion Constraint::assertionFringe(...) to allow hasTrichotomyProof().

9 years agoHanding the case in replay where a cut is directly in conflict with an existing bound.
Tim King [Sun, 14 Jun 2015 21:37:59 +0000 (23:37 +0200)]
Handing the case in replay where a cut is directly in conflict with an existing bound.

9 years agoFixes for shared term normalization in replay for constraint construction.
Tim King [Sun, 14 Jun 2015 13:03:15 +0000 (15:03 +0200)]
Fixes for shared term normalization in replay for constraint construction.

9 years agoTurning off aggressive arith ite simplifications during incremental solving.
Tim King [Sat, 13 Jun 2015 22:51:19 +0000 (00:51 +0200)]
Turning off aggressive arith ite simplifications during incremental solving.

9 years agoRobust check to avoid store all instantiations. Fix prior commit for sort inference.
ajreynol [Sat, 13 Jun 2015 21:45:11 +0000 (23:45 +0200)]
Robust check to avoid store all instantiations. Fix prior commit for sort inference.

9 years agoChanging the run script for master for the application track.
Tim King [Sat, 13 Jun 2015 21:30:24 +0000 (23:30 +0200)]
Changing the run script for master for the application track.

9 years agoRestricting TheoryArith to computeRelevantTerms.
Tim King [Sat, 13 Jun 2015 21:14:46 +0000 (23:14 +0200)]
Restricting TheoryArith to computeRelevantTerms.

9 years agoDisable sort inference for SMT COMP
ajreynol [Sat, 13 Jun 2015 21:05:26 +0000 (23:05 +0200)]
Disable sort inference for SMT COMP

9 years agoFixed bug in iteSimp
Clark Barrett [Sat, 13 Jun 2015 20:23:07 +0000 (13:23 -0700)]
Fixed bug in iteSimp

9 years agoFix for assertion failure:
Clark Barrett [Sat, 13 Jun 2015 17:21:40 +0000 (10:21 -0700)]
Fix for assertion failure:
smt_engine.cpp:1992: Rewriter::rewrite(d_assertions[i]) == d_assertions[i]
when --ite-simp and --repeat-simp are on

9 years agoFix for sort inference involving mixed Int/Real equalities.
ajreynol [Sat, 13 Jun 2015 16:36:31 +0000 (18:36 +0200)]
Fix for sort inference involving mixed Int/Real equalities.

9 years agoA return value for an ApproxGLPK::loadVB() failure case was incorrect.
Tim King [Sat, 13 Jun 2015 14:25:23 +0000 (16:25 +0200)]
A return value for an ApproxGLPK::loadVB() failure case was incorrect.

9 years agoAvoid instantiating with array constants.
ajreynol [Sat, 13 Jun 2015 14:06:49 +0000 (16:06 +0200)]
Avoid instantiating with array constants.

9 years agoEnsure mkRep instantiation strategies do not violate types.
ajreynol [Sat, 13 Jun 2015 08:00:27 +0000 (10:00 +0200)]
Ensure mkRep instantiation strategies do not violate types.

9 years agosync options of default-assertions run script with default
Kshitij Bansal [Fri, 12 Jun 2015 21:21:38 +0000 (17:21 -0400)]
sync options of default-assertions run script with default

9 years agoFix crash in non-linear cbqi.
ajreynol [Fri, 12 Jun 2015 20:15:18 +0000 (22:15 +0200)]
Fix crash in non-linear cbqi.

9 years agoIn TheoryArithPrivate::vectorToIntHoleConflict, adding check for whether or not negBa...
Tim King [Fri, 12 Jun 2015 15:11:29 +0000 (17:11 +0200)]
In TheoryArithPrivate::vectorToIntHoleConflict, adding check for whether or not negBack is already in conflict. This is needed as it can be called multiple times on the same constraint.

9 years agoMake sygus an output language. Parse declare-fun in sygus. Minor improvements to...
ajreynol [Fri, 12 Jun 2015 14:32:32 +0000 (16:32 +0200)]
Make sygus an output language.  Parse declare-fun in sygus.  Minor improvements to robustness of sygus parsing.

9 years agoAccelerate sygus solution reconstruction for constants and id functions. Minor chang...
ajreynol [Fri, 12 Jun 2015 12:15:14 +0000 (14:15 +0200)]
Accelerate sygus solution reconstruction for constants and id functions.  Minor changes to sygus type registration.  Print sygus let solutions assuming fixed variable names.

9 years agoremove runscripts from master meant for experimental submission
Kshitij Bansal [Thu, 11 Jun 2015 18:39:34 +0000 (14:39 -0400)]
remove runscripts from master meant for experimental submission

9 years agoAvoid naming conflicts in sygus, refactor. Add missing regression. Detect Start...
ajreynol [Thu, 11 Jun 2015 16:13:37 +0000 (18:13 +0200)]
Avoid naming conflicts in sygus, refactor. Add missing regression.  Detect Start grammar. Add regression.

9 years agoHandle duplicate operators in sygus grammars. Parse sygus quoted literals. Add regre...
ajreynol [Thu, 11 Jun 2015 14:05:55 +0000 (16:05 +0200)]
Handle duplicate operators in sygus grammars.  Parse sygus quoted literals. Add regression.

9 years agoUpdate experimental scripts. Support top-level non-terminals in sygus grammars....
ajreynol [Thu, 11 Jun 2015 13:03:52 +0000 (15:03 +0200)]
Update experimental scripts.  Support top-level non-terminals in sygus grammars.  Allow -N in sygus terms.  Minor bug fix in datatypes_sygus. Add regression.

9 years agoBug fix parsing constant constructor sygus.
ajreynol [Wed, 10 Jun 2015 14:43:03 +0000 (16:43 +0200)]
Bug fix parsing constant constructor sygus.

9 years agoSupport for printing solutions involving LetGTerm sygus. Bug fix define-fun within...
ajreynol [Wed, 10 Jun 2015 13:35:07 +0000 (15:35 +0200)]
Support for printing solutions involving LetGTerm sygus. Bug fix define-fun within LetGTerm sygus.  Bug fix sygus argument generalization.  Add regressions.

9 years agoParse support for sygus LetGTerm.
ajreynol [Wed, 10 Jun 2015 09:26:51 +0000 (11:26 +0200)]
Parse support for sygus LetGTerm.

9 years agobump thread stack size to 1 GB
Kshitij Bansal [Tue, 9 Jun 2015 20:25:02 +0000 (16:25 -0400)]
bump thread stack size to 1 GB

9 years agoBug fix instantiations for fmf-bound-int. Disable nested pre-skolemization for non...
ajreynol [Tue, 9 Jun 2015 09:45:14 +0000 (11:45 +0200)]
Bug fix instantiations for fmf-bound-int.  Disable nested pre-skolemization for non-UF logics.  Update SMT COMP scripts accordingly.

9 years agomake comment precise
Kshitij Bansal [Tue, 9 Jun 2015 00:54:08 +0000 (20:54 -0400)]
make comment precise

9 years agomove delete beyond ifdef CVC4_COMPETITION_MODE
Kshitij Bansal [Tue, 9 Jun 2015 00:19:57 +0000 (20:19 -0400)]
move delete beyond ifdef CVC4_COMPETITION_MODE

9 years agopcvc4 with assertions
Kshitij Bansal [Fri, 5 Jun 2015 21:16:58 +0000 (17:16 -0400)]
pcvc4 with assertions

9 years agoupdate run script for assertions/scrambled run
Kshitij Bansal [Fri, 5 Jun 2015 21:15:42 +0000 (17:15 -0400)]
update run script for assertions/scrambled run

9 years agoassertions runscript (for testing) derived from current stable (default) script
Kshitij Bansal [Fri, 5 Jun 2015 21:00:00 +0000 (17:00 -0400)]
assertions runscript (for testing) derived from current stable (default) script

9 years agofor experimental, use incremental instead of teardown for all logics for testing...
Kshitij Bansal [Fri, 5 Jun 2015 20:57:05 +0000 (16:57 -0400)]
for experimental, use incremental instead of teardown for all logics for testing purposes

9 years agomove decision to use teardown or not to logics
Kshitij Bansal [Fri, 5 Jun 2015 20:55:46 +0000 (16:55 -0400)]
move decision to use teardown or not to logics

9 years agoFix for last commit.
ajreynol [Thu, 4 Jun 2015 18:32:46 +0000 (20:32 +0200)]
Fix for last commit.

9 years agorpl -- "--cbqi" "--cbqi --no-cbqi-sat" run-script-smtcomp2015{,-application}
Kshitij Bansal [Thu, 4 Jun 2015 17:24:42 +0000 (13:24 -0400)]
rpl -- "--cbqi" "--cbqi --no-cbqi-sat" run-script-smtcomp2015{,-application}

9 years agosync exerimental scripts with regular ones
Kshitij Bansal [Thu, 4 Jun 2015 17:18:12 +0000 (13:18 -0400)]
sync exerimental scripts with regular ones

9 years agoMinor changes to smt comp script for quantified arith. Add option --cbqi-sat whether...
ajreynol [Thu, 4 Jun 2015 06:14:30 +0000 (08:14 +0200)]
Minor changes to smt comp script for quantified arith.  Add option --cbqi-sat whether to disable sat for quantified arith.

9 years agoexperimental run scripts
Kshitij Bansal [Wed, 3 Jun 2015 22:16:00 +0000 (18:16 -0400)]
experimental run scripts

9 years agorunscript thread stack 256
Kshitij Bansal [Wed, 3 Jun 2015 20:58:39 +0000 (16:58 -0400)]
runscript thread stack 256

9 years agoRefactoring of sygus parsing, properly parse Constant/Variable constructors.
ajreynol [Wed, 3 Jun 2015 11:16:44 +0000 (13:16 +0200)]
Refactoring of sygus parsing, properly parse Constant/Variable constructors.

9 years agoapplication smtcomp
Kshitij Bansal [Tue, 2 Jun 2015 20:40:36 +0000 (16:40 -0400)]
application smtcomp

9 years agoFlatten sygus grammars during parsing. Remove duplicate operators from grammars.
ajreynol [Tue, 2 Jun 2015 17:17:53 +0000 (19:17 +0200)]
Flatten sygus grammars during parsing. Remove duplicate operators from grammars.

9 years agoAdd casc 25 tfn script. Change tff script to output instantiations. Work towards...
ajreynol [Tue, 2 Jun 2015 11:43:51 +0000 (13:43 +0200)]
Add casc 25 tfn script.  Change tff script to output instantiations. Work towards parsing non-flattened sygus grammars.

9 years agoWhen proof enabled, disable uf sym break. Add regression.
ajreynol [Mon, 1 Jun 2015 20:44:40 +0000 (22:44 +0200)]
When proof enabled, disable uf sym break. Add regression.

9 years agoDo not enforce dt fairness when single invocation sygus.
ajreynol [Fri, 29 May 2015 09:47:28 +0000 (11:47 +0200)]
Do not enforce dt fairness when single invocation sygus.

9 years agochanged resource step options to unsigned
lianah [Fri, 29 May 2015 14:18:36 +0000 (10:18 -0400)]
changed resource step options to unsigned

9 years agoadded options for controlling resource step-count for various solving stages
Liana Hadarean [Thu, 28 May 2015 14:03:10 +0000 (15:03 +0100)]
added options for controlling resource step-count for various solving stages

9 years agoMerge pull request #75 from Dunedune/master
lianah [Wed, 27 May 2015 18:25:04 +0000 (19:25 +0100)]
Merge pull request #75 from Dunedune/master

Added missing LogicException to throws in method lemma.

9 years agoAdd missing regression
ajreynol [Mon, 25 May 2015 08:35:00 +0000 (10:35 +0200)]
Add missing regression

9 years agoBug fix for CNF proofs (and/or case 1), thanks to Alain Mebsout for bug report.
ajreynol [Mon, 25 May 2015 08:34:26 +0000 (10:34 +0200)]
Bug fix for CNF proofs (and/or case 1), thanks to Alain Mebsout for bug report.

9 years agoAdded throw LogicException to method lemma.
Jordy Ruiz [Fri, 22 May 2015 08:36:23 +0000 (10:36 +0200)]
Added throw LogicException to method lemma.

9 years agoFixes related to cbqi + E-matching.
ajreynol [Fri, 15 May 2015 17:47:32 +0000 (19:47 +0200)]
Fixes related to cbqi + E-matching.

9 years agoAvoid ensureLiteral on unpreprocessed formulas in cbqi.
ajreynol [Fri, 15 May 2015 07:09:51 +0000 (09:09 +0200)]
Avoid ensureLiteral on unpreprocessed formulas in cbqi.

9 years agoRefactor interface for incompleteness in quantifiers engine, cbqi. Minor fix for...
ajreynol [Wed, 13 May 2015 08:13:16 +0000 (10:13 +0200)]
Refactor interface for incompleteness in quantifiers engine, cbqi. Minor fix for sygus.

9 years agoAdded Finn Haedicke as a contributor.
Clark Barrett [Tue, 12 May 2015 20:56:00 +0000 (13:56 -0700)]
Added Finn Haedicke as a contributor.

9 years agoMerge pull request #74 from finnhaedicke/namespace_minisat
barrettcw [Tue, 12 May 2015 20:53:34 +0000 (13:53 -0700)]
Merge pull request #74 from finnhaedicke/namespace_minisat

moved Minisat namespace into CVC4

9 years agoAllow sygus with no syntactic restrictions for LIA. Add regressions.
ajreynol [Mon, 11 May 2015 18:06:21 +0000 (20:06 +0200)]
Allow sygus with no syntactic restrictions for LIA.  Add regressions.

9 years agoAdd missing regression.
ajreynol [Mon, 11 May 2015 09:53:07 +0000 (11:53 +0200)]
Add missing regression.

9 years agoSupport for arbitrary constants/variables in Sygus grammars.
ajreynol [Mon, 11 May 2015 09:41:48 +0000 (11:41 +0200)]
Support for arbitrary constants/variables in Sygus grammars.

9 years agoMinor improvements to infrastructure. Minor changes to default options. Add tff scrip...
ajreynol [Sun, 10 May 2015 17:44:58 +0000 (19:44 +0200)]
Minor improvements to infrastructure. Minor changes to default options. Add tff script. Minor additions to sygus.

9 years agoAdd casc25 fnt script.
ajreynol [Fri, 8 May 2015 11:03:41 +0000 (13:03 +0200)]
Add casc25 fnt script.

9 years agoMinor fix for corner cases of fmf-fun, fix for --dt-rewrite-error-sel. Add competitio...
ajreynol [Sat, 2 May 2015 08:13:18 +0000 (10:13 +0200)]
Minor fix for corner cases of fmf-fun, fix for --dt-rewrite-error-sel. Add competition scripts (in progress).