From 2bd8e21f16bdb738017e648c2c286f90309c6efa Mon Sep 17 00:00:00 2001 From: Christoph Zengler Date: Thu, 30 Jul 2020 00:17:32 +0200 Subject: [PATCH] Formatting fixes and added license headers --- src/main/java/org/logicng/LogicNGVersion.java | 28 +++++++ .../datastructures/ubtrees/UBNode.java | 28 +++++++ .../datastructures/ubtrees/UBTree.java | 28 +++++++ .../explanations/smus/SmusComputation.java | 28 +++++++ .../formulas/FormulaFactoryConfig.java | 28 +++++++ .../org/logicng/formulas/PBConstraint.java | 4 +- .../functions/FormulaDepthFunction.java | 28 +++++++ .../MinimumPrimeImplicantFunction.java | 28 +++++++ .../generators/ConstraintGraphGenerator.java | 28 +++++++ .../generators/HypergraphGenerator.java | 28 +++++++ .../logicng/handlers/ComputationHandler.java | 28 +++++++ .../handlers/DnnfCompilationHandler.java | 32 ++++++++ .../java/org/logicng/handlers/Handler.java | 28 +++++++ .../org/logicng/handlers/TimeoutHandler.java | 28 +++++++ .../TimeoutModelEnumerationHandler.java | 28 +++++++ .../logicng/io/parsers/ParserWithFormula.java | 28 +++++++ .../bdds/functions/BDDCNFFunction.java | 28 +++++++ .../bdds/functions/BDDFunction.java | 29 ++++++- .../BDDModelEnumerationFunction.java | 28 +++++++ .../bdds/functions/LngBDDFunction.java | 28 +++++++ .../bdds/jbuddy/BDDConstruction.java | 30 ++++++- .../bdds/jbuddy/BDDKernel.java | 2 +- .../bdds/jbuddy/BDDOperations.java | 29 ++++++- .../bdds/jbuddy/BDDReordering.java | 28 +++++++ .../bdds/jbuddy/BDDReorderingMethod.java | 28 +++++++ .../bdds/jbuddy/BDDTree.java | 28 +++++++ .../dnnf/DNNFFactory.java | 49 ----------- .../{DNNFCompiler.java => DnnfCompiler.java} | 36 +++++++- .../dnnf/DnnfFactory.java | 77 +++++++++++++++++ ...olver.java => DnnfMiniSatStyleSolver.java} | 32 +++++++- ...{DNNFSATSolver.java => DnnfSatSolver.java} | 30 ++++++- .../dnnf/datastructures/DNNF.java | 54 ------------ .../dnnf/datastructures/Dnnf.java | 82 +++++++++++++++++++ .../dnnf/datastructures/dtree/DTree.java | 32 +++++++- .../datastructures/dtree/DTreeGenerator.java | 28 +++++++ .../dnnf/datastructures/dtree/DTreeLeaf.java | 34 +++++++- .../dnnf/datastructures/dtree/DTreeNode.java | 34 +++++++- .../dtree/EliminatingOrderDTreeGenerator.java | 28 +++++++ .../dtree/MinFillDTreeGenerator.java | 28 +++++++ .../dnnf/functions/DNNFFunction.java | 23 ------ .../dnnf/functions/DnnfFunction.java | 51 ++++++++++++ ...ction.java => DnnfModelCountFunction.java} | 36 +++++++- .../logicng/modelcounting/ModelCounter.java | 40 +++++++-- src/main/java/org/logicng/np/SetCover.java | 28 +++++++ .../org/logicng/predicates/AIGPredicate.java | 4 +- .../org/logicng/predicates/CNFPredicate.java | 4 +- .../predicates/ContainsPBCPredicate.java | 28 +++++++ .../org/logicng/predicates/DNFPredicate.java | 4 +- .../EvaluatesToConstantPredicate.java | 28 +++++++ .../org/logicng/predicates/NNFPredicate.java | 4 +- .../satisfiability/SATPredicate.java | 4 +- .../primecomputation/NaivePrimeReduction.java | 28 +++++++ .../primecomputation/PrimeCompiler.java | 28 +++++++ .../logicng/primecomputation/PrimeResult.java | 28 +++++++ .../logicng/pseudobooleans/PBEncoding.java | 28 +++++++ .../solvers/functions/BackboneFunction.java | 28 +++++++ .../functions/FormulaOnSolverFunction.java | 28 +++++++ .../functions/ModelEnumerationFunction.java | 28 +++++++ .../functions/OptimizationFunction.java | 28 +++++++ .../solvers/functions/SolverFunction.java | 28 +++++++ .../solvers/functions/UnsatCoreFunction.java | 28 +++++++ .../functions/UpZeroLiteralsFunction.java | 28 +++++++ .../logicng/transformations/Anonymizer.java | 28 +++++++ .../transformations/LiteralSubstitution.java | 28 +++++++ .../PureExpansionTransformation.java | 4 +- .../logicng/transformations/Subsumption.java | 28 +++++++ .../transformations/cnf/CNFFactorization.java | 10 +-- .../cnf/PlaistedGreenbaumTransformation.java | 6 +- .../qmc/QuineMcCluskeyAlgorithm.java | 1 + .../simplification/AdvancedSimplifier.java | 28 +++++++ .../simplification/BackboneSimplifier.java | 1 + .../org/logicng/util/CollectionHelper.java | 28 +++++++ .../org/logicng/util/FormulaCornerCases.java | 28 +++++++ .../java/org/logicng/util/FormulaHelper.java | 28 +++++++ .../org/logicng/util/FormulaRandomizer.java | 28 +++++++ .../logicng/util/FormulaRandomizerConfig.java | 28 +++++++ src/test/java/org/logicng/LogicNGTest.java | 28 +++++++ .../java/org/logicng/LogicNGVersionTest.java | 28 +++++++ src/test/java/org/logicng/LongRunningTag.java | 28 +++++++ src/test/java/org/logicng/RandomTag.java | 28 +++++++ .../org/logicng/TestWithExampleFormulas.java | 28 +++++++ .../cardinalityconstraints/CCALKTest.java | 6 +- .../cardinalityconstraints/CCAMKTest.java | 6 +- .../cardinalityconstraints/CCAMOTest.java | 18 ++-- .../cardinalityconstraints/CCEXKTest.java | 4 +- .../cardinalityconstraints/CCEXOTest.java | 24 +++--- .../CCIncrementalFormulaTest.java | 4 +- .../CCIncrementalSolverTest.java | 4 +- .../CCPerformanceTest.java | 4 +- .../logicng/collections/LNGVectorTest.java | 6 +- .../datastructures/ubtrees/UBNodeTest.java | 28 +++++++ .../datastructures/ubtrees/UBTreeTest.java | 28 +++++++ .../logicng/explanations/UNSATCoreTest.java | 28 +++++++ .../smus/SmusComputationTest.java | 28 +++++++ .../java/org/logicng/formulas/CacheTest.java | 4 +- .../formulas/ExtendedFormulaFactoryTest.java | 11 ++- .../java/org/logicng/formulas/FTypeTest.java | 32 +++++++- ...aFactoryWithoutContradictionCheckTest.java | 28 +++++++ .../logicng/formulas/FormulaMergeTest.java | 28 +++++++ .../java/org/logicng/formulas/NNFTest.java | 1 + .../functions/FormulaDepthFunctionTest.java | 28 +++++++ .../functions/MinimumPrimeImplicantTest.java | 28 +++++++ .../ConstraintGraphGeneratorTest.java | 28 +++++++ .../handlers/NumberOfNodesBDDHandlerTest.java | 28 +++++++ .../logicng/io/readers/DimacsReaderTest.java | 28 +++++++ .../bdds/BDDLowLevelTest.java | 28 +++++++ .../bdds/BDDReorderingTest.java | 28 +++++++ .../bdds/jbuddy/BDDPrimeTest.java | 30 ++++++- .../bdds/jbuddy/BDDVerification.java | 28 +++++++ .../dnnf/DnnfCompilerTest.java | 50 ++++++++--- .../datastructures/dtree/DTreeNodeTest.java | 28 +++++++ .../modelcounting/ModelCounterTest.java | 28 +++++++ .../java/org/logicng/np/SetCoverTest.java | 28 +++++++ .../EvaluatesToConstantPredicateTest.java | 28 +++++++ .../primecomputation/PrimeCompilerTest.java | 28 +++++++ .../PrimeImplicantReductionTest.java | 28 +++++++ .../PrimeImplicateReductionTest.java | 28 +++++++ .../primecomputation/PrimeResultTest.java | 28 +++++++ .../propositions/ExtendedPropositionTest.java | 4 +- .../logicng/pseudobooleans/PBEncoderTest.java | 4 +- .../logicng/pseudobooleans/PBSolvingTest.java | 4 +- .../java/org/logicng/solvers/ModelTest.java | 28 +++++++ .../functions/BackboneFunctionTest.java | 28 +++++++ .../functions/OptimizationFunctionTest.java | 28 +++++++ .../functions/UnsatCoreFunctionTest.java | 30 ++++++- .../logicng/solvers/sat/GlucoseSyrupTest.java | 28 +++++++ .../transformations/AnonymizerTest.java | 28 +++++++ .../LiteralSubstitutionTest.java | 28 +++++++ .../transformations/cnf/CNFEncoderTest.java | 6 +- .../cnf/CNFSubsumptionTest.java | 6 +- .../cnf/CnfMethodComparisonTest.java | 28 +++++++ ...stedGreenbaumTransformationSolverTest.java | 28 +++++++ .../qmc/QuineMcCluskeyTest.java | 14 ++-- .../transformations/qmc/TermTableTest.java | 28 +++++++ .../logicng/transformations/qmc/TermTest.java | 38 +++++++-- .../simplification/SimplifierTest.java | 28 +++++++ .../logicng/util/CollectionHelperTest.java | 36 +++++++- .../logicng/util/FormulaRandomizerTest.java | 28 +++++++ 138 files changed, 3209 insertions(+), 267 deletions(-) delete mode 100644 src/main/java/org/logicng/knowledgecompilation/dnnf/DNNFFactory.java rename src/main/java/org/logicng/knowledgecompilation/dnnf/{DNNFCompiler.java => DnnfCompiler.java} (83%) create mode 100644 src/main/java/org/logicng/knowledgecompilation/dnnf/DnnfFactory.java rename src/main/java/org/logicng/knowledgecompilation/dnnf/{DNNFMiniSatStyleSolver.java => DnnfMiniSatStyleSolver.java} (77%) rename src/main/java/org/logicng/knowledgecompilation/dnnf/{DNNFSATSolver.java => DnnfSatSolver.java} (56%) delete mode 100644 src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/DNNF.java create mode 100644 src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/Dnnf.java delete mode 100644 src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DNNFFunction.java create mode 100644 src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DnnfFunction.java rename src/main/java/org/logicng/knowledgecompilation/dnnf/functions/{DNNFModelCountFunction.java => DnnfModelCountFunction.java} (55%) diff --git a/src/main/java/org/logicng/LogicNGVersion.java b/src/main/java/org/logicng/LogicNGVersion.java index 14f643ab..4128f797 100644 --- a/src/main/java/org/logicng/LogicNGVersion.java +++ b/src/main/java/org/logicng/LogicNGVersion.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng; /** diff --git a/src/main/java/org/logicng/datastructures/ubtrees/UBNode.java b/src/main/java/org/logicng/datastructures/ubtrees/UBNode.java index a92d37bf..167dd1c2 100644 --- a/src/main/java/org/logicng/datastructures/ubtrees/UBNode.java +++ b/src/main/java/org/logicng/datastructures/ubtrees/UBNode.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.datastructures.ubtrees; import java.util.Objects; diff --git a/src/main/java/org/logicng/datastructures/ubtrees/UBTree.java b/src/main/java/org/logicng/datastructures/ubtrees/UBTree.java index aa0b494c..11e2d8a9 100644 --- a/src/main/java/org/logicng/datastructures/ubtrees/UBTree.java +++ b/src/main/java/org/logicng/datastructures/ubtrees/UBTree.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.datastructures.ubtrees; import java.util.ArrayList; diff --git a/src/main/java/org/logicng/explanations/smus/SmusComputation.java b/src/main/java/org/logicng/explanations/smus/SmusComputation.java index 6990a32c..8b2c80c4 100644 --- a/src/main/java/org/logicng/explanations/smus/SmusComputation.java +++ b/src/main/java/org/logicng/explanations/smus/SmusComputation.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.explanations.smus; import org.logicng.datastructures.Assignment; diff --git a/src/main/java/org/logicng/formulas/FormulaFactoryConfig.java b/src/main/java/org/logicng/formulas/FormulaFactoryConfig.java index 57dddca7..bfe4992b 100644 --- a/src/main/java/org/logicng/formulas/FormulaFactoryConfig.java +++ b/src/main/java/org/logicng/formulas/FormulaFactoryConfig.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.formulas; import org.logicng.configurations.Configuration; diff --git a/src/main/java/org/logicng/formulas/PBConstraint.java b/src/main/java/org/logicng/formulas/PBConstraint.java index e3a8d050..aaaac453 100644 --- a/src/main/java/org/logicng/formulas/PBConstraint.java +++ b/src/main/java/org/logicng/formulas/PBConstraint.java @@ -28,6 +28,8 @@ package org.logicng.formulas; +import static org.logicng.formulas.cache.TransformationCacheEntry.NNF; + import org.logicng.collections.LNGIntVector; import org.logicng.collections.LNGVector; import org.logicng.datastructures.Assignment; @@ -48,8 +50,6 @@ import java.util.TreeMap; import java.util.stream.Stream; -import static org.logicng.formulas.cache.TransformationCacheEntry.NNF; - /** * A pseudo-Boolean constraint of the form {@code c_1 * l_1 + ... + c_n * l_n R k} where {@code R} is one of * {@code =, >, >=, <, <=}. diff --git a/src/main/java/org/logicng/functions/FormulaDepthFunction.java b/src/main/java/org/logicng/functions/FormulaDepthFunction.java index f81683ea..3a6bd56e 100644 --- a/src/main/java/org/logicng/functions/FormulaDepthFunction.java +++ b/src/main/java/org/logicng/functions/FormulaDepthFunction.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.functions; import static org.logicng.formulas.cache.FunctionCacheEntry.DEPTH; diff --git a/src/main/java/org/logicng/functions/MinimumPrimeImplicantFunction.java b/src/main/java/org/logicng/functions/MinimumPrimeImplicantFunction.java index 7d4fc482..2994caf6 100644 --- a/src/main/java/org/logicng/functions/MinimumPrimeImplicantFunction.java +++ b/src/main/java/org/logicng/functions/MinimumPrimeImplicantFunction.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.functions; import org.logicng.datastructures.Assignment; diff --git a/src/main/java/org/logicng/graphs/generators/ConstraintGraphGenerator.java b/src/main/java/org/logicng/graphs/generators/ConstraintGraphGenerator.java index 3914875e..c1eb7ffb 100644 --- a/src/main/java/org/logicng/graphs/generators/ConstraintGraphGenerator.java +++ b/src/main/java/org/logicng/graphs/generators/ConstraintGraphGenerator.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.graphs.generators; import org.logicng.formulas.Formula; diff --git a/src/main/java/org/logicng/graphs/generators/HypergraphGenerator.java b/src/main/java/org/logicng/graphs/generators/HypergraphGenerator.java index 3edf244d..0849e0e5 100644 --- a/src/main/java/org/logicng/graphs/generators/HypergraphGenerator.java +++ b/src/main/java/org/logicng/graphs/generators/HypergraphGenerator.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.graphs.generators; import org.logicng.formulas.FType; diff --git a/src/main/java/org/logicng/handlers/ComputationHandler.java b/src/main/java/org/logicng/handlers/ComputationHandler.java index db24d441..4f72f598 100644 --- a/src/main/java/org/logicng/handlers/ComputationHandler.java +++ b/src/main/java/org/logicng/handlers/ComputationHandler.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.handlers; /** diff --git a/src/main/java/org/logicng/handlers/DnnfCompilationHandler.java b/src/main/java/org/logicng/handlers/DnnfCompilationHandler.java index 09232c11..a5ef159e 100644 --- a/src/main/java/org/logicng/handlers/DnnfCompilationHandler.java +++ b/src/main/java/org/logicng/handlers/DnnfCompilationHandler.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.handlers; /** @@ -7,6 +35,10 @@ */ public interface DnnfCompilationHandler extends Handler { + /** + * This method is called when an shannon expansion was performed. + * @return true when the computation should be continued, false if it should be aborted with a {@link java.util.concurrent.TimeoutException} + */ boolean shannonExpansion(); /** diff --git a/src/main/java/org/logicng/handlers/Handler.java b/src/main/java/org/logicng/handlers/Handler.java index 102936da..67992e85 100644 --- a/src/main/java/org/logicng/handlers/Handler.java +++ b/src/main/java/org/logicng/handlers/Handler.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.handlers; /** diff --git a/src/main/java/org/logicng/handlers/TimeoutHandler.java b/src/main/java/org/logicng/handlers/TimeoutHandler.java index 9a62dd52..cbea95fa 100644 --- a/src/main/java/org/logicng/handlers/TimeoutHandler.java +++ b/src/main/java/org/logicng/handlers/TimeoutHandler.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.handlers; /** diff --git a/src/main/java/org/logicng/handlers/TimeoutModelEnumerationHandler.java b/src/main/java/org/logicng/handlers/TimeoutModelEnumerationHandler.java index 266295bb..368e1755 100644 --- a/src/main/java/org/logicng/handlers/TimeoutModelEnumerationHandler.java +++ b/src/main/java/org/logicng/handlers/TimeoutModelEnumerationHandler.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.handlers; import org.logicng.datastructures.Assignment; diff --git a/src/main/java/org/logicng/io/parsers/ParserWithFormula.java b/src/main/java/org/logicng/io/parsers/ParserWithFormula.java index 3e1cebe8..d6da7db8 100644 --- a/src/main/java/org/logicng/io/parsers/ParserWithFormula.java +++ b/src/main/java/org/logicng/io/parsers/ParserWithFormula.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.io.parsers; import org.antlr.v4.runtime.Parser; diff --git a/src/main/java/org/logicng/knowledgecompilation/bdds/functions/BDDCNFFunction.java b/src/main/java/org/logicng/knowledgecompilation/bdds/functions/BDDCNFFunction.java index 985136a4..c378b817 100644 --- a/src/main/java/org/logicng/knowledgecompilation/bdds/functions/BDDCNFFunction.java +++ b/src/main/java/org/logicng/knowledgecompilation/bdds/functions/BDDCNFFunction.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.knowledgecompilation.bdds.functions; import org.logicng.formulas.Formula; diff --git a/src/main/java/org/logicng/knowledgecompilation/bdds/functions/BDDFunction.java b/src/main/java/org/logicng/knowledgecompilation/bdds/functions/BDDFunction.java index fef7186a..6799cbf7 100644 --- a/src/main/java/org/logicng/knowledgecompilation/bdds/functions/BDDFunction.java +++ b/src/main/java/org/logicng/knowledgecompilation/bdds/functions/BDDFunction.java @@ -1,5 +1,32 @@ -package org.logicng.knowledgecompilation.bdds.functions; +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// +package org.logicng.knowledgecompilation.bdds.functions; import org.logicng.knowledgecompilation.bdds.BDD; diff --git a/src/main/java/org/logicng/knowledgecompilation/bdds/functions/BDDModelEnumerationFunction.java b/src/main/java/org/logicng/knowledgecompilation/bdds/functions/BDDModelEnumerationFunction.java index 042bf409..356778d0 100644 --- a/src/main/java/org/logicng/knowledgecompilation/bdds/functions/BDDModelEnumerationFunction.java +++ b/src/main/java/org/logicng/knowledgecompilation/bdds/functions/BDDModelEnumerationFunction.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.knowledgecompilation.bdds.functions; import org.logicng.datastructures.Assignment; diff --git a/src/main/java/org/logicng/knowledgecompilation/bdds/functions/LngBDDFunction.java b/src/main/java/org/logicng/knowledgecompilation/bdds/functions/LngBDDFunction.java index 0cf49d04..d7ecff36 100644 --- a/src/main/java/org/logicng/knowledgecompilation/bdds/functions/LngBDDFunction.java +++ b/src/main/java/org/logicng/knowledgecompilation/bdds/functions/LngBDDFunction.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.knowledgecompilation.bdds.functions; import org.logicng.formulas.Variable; diff --git a/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDConstruction.java b/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDConstruction.java index af7cfd49..48a1fa69 100644 --- a/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDConstruction.java +++ b/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDConstruction.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.knowledgecompilation.bdds.jbuddy; import static org.logicng.knowledgecompilation.bdds.jbuddy.BDDKernel.CACHEID_FORALL; @@ -122,7 +150,6 @@ public int equivalence(final int l, final int r) { return this.k.apply(l, r, BDDKernel.Operand.EQUIV); } - /** * Returns the negation of a BDD. * @param r the BDD @@ -153,7 +180,6 @@ protected int notRec(final int r) throws BDDKernel.BddReorderRequest { return res; } - /** * Restricts the variables in the BDD {@code r} to constants true or false. The restriction is submitted in the BDD * {@code var}. diff --git a/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDKernel.java b/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDKernel.java index 8f7319a6..ad9429d7 100644 --- a/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDKernel.java +++ b/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDKernel.java @@ -752,7 +752,7 @@ protected void varResize() { this.quantvarset = new int[this.varnum]; this.quantvarsetID = 0; } - + /** * Returns the statistics for this BDD Kernel. * @return the statistics diff --git a/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDOperations.java b/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDOperations.java index 76be07e5..af23dd14 100644 --- a/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDOperations.java +++ b/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDOperations.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.knowledgecompilation.bdds.jbuddy; import static org.logicng.knowledgecompilation.bdds.jbuddy.BDDKernel.CACHEID_PATHCOU_ONE; @@ -407,7 +435,6 @@ protected void varProfileRec(final int r, final int[] varprofile) { varProfileRec(this.k.high(r), varprofile); } - /** * Returns all nodes for a given root node in their internal representation. The internal representation is stored * in an array: {@code [node number, variable, low, high]} diff --git a/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDReordering.java b/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDReordering.java index 4ae79f9e..081606bd 100644 --- a/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDReordering.java +++ b/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDReordering.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.knowledgecompilation.bdds.jbuddy; import static org.logicng.knowledgecompilation.bdds.jbuddy.BDDKernel.MARKHIDE; diff --git a/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDReorderingMethod.java b/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDReorderingMethod.java index 679f0092..8e835c43 100644 --- a/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDReorderingMethod.java +++ b/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDReorderingMethod.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.knowledgecompilation.bdds.jbuddy; /** diff --git a/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDTree.java b/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDTree.java index 3a5bab70..901ddaa7 100644 --- a/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDTree.java +++ b/src/main/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDTree.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.knowledgecompilation.bdds.jbuddy; /** diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/DNNFFactory.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/DNNFFactory.java deleted file mode 100644 index 9f3d6228..00000000 --- a/src/main/java/org/logicng/knowledgecompilation/dnnf/DNNFFactory.java +++ /dev/null @@ -1,49 +0,0 @@ -package org.logicng.knowledgecompilation.dnnf; - -import org.logicng.formulas.Formula; -import org.logicng.formulas.Variable; -import org.logicng.knowledgecompilation.dnnf.datastructures.DNNF; -import org.logicng.knowledgecompilation.dnnf.datastructures.dtree.MinFillDTreeGenerator; -import org.logicng.transformations.cnf.CNFSubsumption; -import org.logicng.transformations.simplification.BackboneSimplifier; - -import java.util.SortedSet; -import java.util.TreeSet; - -/** - * A DNNF factory that can be used to compute DNNFs from formulas. - * @version 2.0.0 - * @since 2.0.0 - */ -public class DNNFFactory { - - protected final BackboneSimplifier backboneSimplifier; - protected final CNFSubsumption subsumption; - - /** - * Constructs a new DNNF factory instance. - */ - public DNNFFactory() { - this.backboneSimplifier = new BackboneSimplifier(); - this.subsumption = new CNFSubsumption(); - } - - /** - * Compiles the given formula to a DNNF instance. - * @param formula the formula - * @return the compiled DNNF - */ - public DNNF compile(final Formula formula) { - final SortedSet originalVariables = new TreeSet<>(formula.variables()); - final Formula cnf = formula.cnf(); - originalVariables.addAll(cnf.variables()); - final Formula simplifedFormula = simplifyFormula(cnf); - final DNNFCompiler compiler = new DNNFCompiler(simplifedFormula); - final Formula dnnf = compiler.compile(new MinFillDTreeGenerator()); - return new DNNF(originalVariables, dnnf); - } - - protected Formula simplifyFormula(final Formula formula) { - return formula.transform(this.backboneSimplifier).transform(this.subsumption); - } -} diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/DNNFCompiler.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/DnnfCompiler.java similarity index 83% rename from src/main/java/org/logicng/knowledgecompilation/dnnf/DNNFCompiler.java rename to src/main/java/org/logicng/knowledgecompilation/dnnf/DnnfCompiler.java index 607e0951..05d34532 100644 --- a/src/main/java/org/logicng/knowledgecompilation/dnnf/DNNFCompiler.java +++ b/src/main/java/org/logicng/knowledgecompilation/dnnf/DnnfCompiler.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.knowledgecompilation.dnnf; import org.logicng.formulas.Formula; @@ -27,14 +55,14 @@ * @version 2.0.0 * @since 2.0.0 */ -public class DNNFCompiler { +public class DnnfCompiler { protected final FormulaFactory f; protected final Formula cnf; protected final Formula unitClauses; protected final Formula nonUnitClauses; - protected final DNNFSATSolver solver; + protected final DnnfSatSolver solver; protected final int numberOfVariables; @@ -50,13 +78,13 @@ public class DNNFCompiler { * Constructs a new DNNF compiler for the given formula. * @param formula the formula to compile */ - public DNNFCompiler(final Formula formula) { + public DnnfCompiler(final Formula formula) { this.f = formula.factory(); this.cnf = formula; final Pair pair = initializeClauses(); this.unitClauses = this.f.and(pair.first()); this.nonUnitClauses = this.f.and(pair.second()); - this.solver = new DNNFMiniSatStyleSolver(this.f, this.cnf.variables().size()); + this.solver = new DnnfMiniSatStyleSolver(this.f, this.cnf.variables().size()); this.solver.add(this.cnf); this.numberOfVariables = this.cnf.variables().size(); this.cache = new HashMap<>(); diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/DnnfFactory.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/DnnfFactory.java new file mode 100644 index 00000000..b8b4baa5 --- /dev/null +++ b/src/main/java/org/logicng/knowledgecompilation/dnnf/DnnfFactory.java @@ -0,0 +1,77 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + +package org.logicng.knowledgecompilation.dnnf; + +import org.logicng.formulas.Formula; +import org.logicng.formulas.Variable; +import org.logicng.knowledgecompilation.dnnf.datastructures.Dnnf; +import org.logicng.knowledgecompilation.dnnf.datastructures.dtree.MinFillDTreeGenerator; +import org.logicng.transformations.cnf.CNFSubsumption; +import org.logicng.transformations.simplification.BackboneSimplifier; + +import java.util.SortedSet; +import java.util.TreeSet; + +/** + * A DNNF factory that can be used to compute DNNFs from formulas. + * @version 2.0.0 + * @since 2.0.0 + */ +public class DnnfFactory { + + protected final BackboneSimplifier backboneSimplifier; + protected final CNFSubsumption subsumption; + + /** + * Constructs a new DNNF factory instance. + */ + public DnnfFactory() { + this.backboneSimplifier = new BackboneSimplifier(); + this.subsumption = new CNFSubsumption(); + } + + /** + * Compiles the given formula to a DNNF instance. + * @param formula the formula + * @return the compiled DNNF + */ + public Dnnf compile(final Formula formula) { + final SortedSet originalVariables = new TreeSet<>(formula.variables()); + final Formula cnf = formula.cnf(); + originalVariables.addAll(cnf.variables()); + final Formula simplifedFormula = simplifyFormula(cnf); + final DnnfCompiler compiler = new DnnfCompiler(simplifedFormula); + final Formula dnnf = compiler.compile(new MinFillDTreeGenerator()); + return new Dnnf(originalVariables, dnnf); + } + + protected Formula simplifyFormula(final Formula formula) { + return formula.transform(this.backboneSimplifier).transform(this.subsumption); + } +} diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/DNNFMiniSatStyleSolver.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/DnnfMiniSatStyleSolver.java similarity index 77% rename from src/main/java/org/logicng/knowledgecompilation/dnnf/DNNFMiniSatStyleSolver.java rename to src/main/java/org/logicng/knowledgecompilation/dnnf/DnnfMiniSatStyleSolver.java index d3780d98..1068c750 100644 --- a/src/main/java/org/logicng/knowledgecompilation/dnnf/DNNFMiniSatStyleSolver.java +++ b/src/main/java/org/logicng/knowledgecompilation/dnnf/DnnfMiniSatStyleSolver.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.knowledgecompilation.dnnf; import org.logicng.collections.LNGIntVector; @@ -21,7 +49,7 @@ * @version 2.0.0 * @since 2.0.0 */ -public class DNNFMiniSatStyleSolver extends MiniSat2Solver implements DNNFSATSolver { +public class DnnfMiniSatStyleSolver extends MiniSat2Solver implements DnnfSatSolver { protected boolean newlyImpliedDirty = false; protected int assertionLevel = -1; @@ -35,7 +63,7 @@ public class DNNFMiniSatStyleSolver extends MiniSat2Solver implements DNNFSATSol * @param f the formula factory * @param numberOfVariables the number of variables */ - public DNNFMiniSatStyleSolver(final FormulaFactory f, final int numberOfVariables) { + public DnnfMiniSatStyleSolver(final FormulaFactory f, final int numberOfVariables) { this.f = f; this.assignment = new Tristate[2 * numberOfVariables]; Arrays.fill(this.assignment, Tristate.UNDEF); diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/DNNFSATSolver.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/DnnfSatSolver.java similarity index 56% rename from src/main/java/org/logicng/knowledgecompilation/dnnf/DNNFSATSolver.java rename to src/main/java/org/logicng/knowledgecompilation/dnnf/DnnfSatSolver.java index 79e1bbdf..b642f725 100644 --- a/src/main/java/org/logicng/knowledgecompilation/dnnf/DNNFSATSolver.java +++ b/src/main/java/org/logicng/knowledgecompilation/dnnf/DnnfSatSolver.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.knowledgecompilation.dnnf; import org.logicng.datastructures.Tristate; @@ -11,7 +39,7 @@ * @version 2.0.0 * @since 2.0.0 */ -public interface DNNFSATSolver { +public interface DnnfSatSolver { /** * Adds a formula to the solver. The formula is first converted to CNF. diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/DNNF.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/DNNF.java deleted file mode 100644 index a869b1d1..00000000 --- a/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/DNNF.java +++ /dev/null @@ -1,54 +0,0 @@ -package org.logicng.knowledgecompilation.dnnf.datastructures; - -import org.logicng.formulas.Formula; -import org.logicng.formulas.Variable; -import org.logicng.knowledgecompilation.dnnf.functions.DNNFFunction; - -import java.util.SortedSet; - -/** - * A DNNF - Decomposable Negation Normal Form. - * @version 2.0.0 - * @since 2.0.0 - */ -public final class DNNF { - - private final SortedSet originalVariables; - private final Formula formula; - - /** - * Constructs a new DNNF. - * @param originalVariables the set of original variables - * @param dnnf the formula of the DNNF - */ - public DNNF(final SortedSet originalVariables, final Formula dnnf) { - this.originalVariables = originalVariables; - this.formula = dnnf; - } - - /** - * Executes a given DNNF function on this DNNF. - * @param function the function - * @param the result type - * @return the result of the function application - */ - public RESULT execute(final DNNFFunction function) { - return function.apply(this.originalVariables, this.formula); - } - - /** - * Returns the formula of the DNNF. - * @return the formula - */ - public Formula formula() { - return this.formula; - } - - /** - * Returns the original variables of the formula - * @return the original variables - */ - public SortedSet getOriginalVariables() { - return this.originalVariables; - } -} diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/Dnnf.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/Dnnf.java new file mode 100644 index 00000000..4a2dea46 --- /dev/null +++ b/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/Dnnf.java @@ -0,0 +1,82 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + +package org.logicng.knowledgecompilation.dnnf.datastructures; + +import org.logicng.formulas.Formula; +import org.logicng.formulas.Variable; +import org.logicng.knowledgecompilation.dnnf.functions.DnnfFunction; + +import java.util.SortedSet; + +/** + * A DNNF - Decomposable Negation Normal Form. + * @version 2.0.0 + * @since 2.0.0 + */ +public final class Dnnf { + + private final SortedSet originalVariables; + private final Formula formula; + + /** + * Constructs a new DNNF. + * @param originalVariables the set of original variables + * @param dnnf the formula of the DNNF + */ + public Dnnf(final SortedSet originalVariables, final Formula dnnf) { + this.originalVariables = originalVariables; + this.formula = dnnf; + } + + /** + * Executes a given DNNF function on this DNNF. + * @param function the function + * @param the result type + * @return the result of the function application + */ + public RESULT execute(final DnnfFunction function) { + return function.apply(this.originalVariables, this.formula); + } + + /** + * Returns the formula of the DNNF. + * @return the formula + */ + public Formula formula() { + return this.formula; + } + + /** + * Returns the original variables of the formula + * @return the original variables + */ + public SortedSet getOriginalVariables() { + return this.originalVariables; + } +} diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTree.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTree.java index 82b2ac03..ff844623 100644 --- a/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTree.java +++ b/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTree.java @@ -1,7 +1,35 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.knowledgecompilation.dnnf.datastructures.dtree; import org.logicng.formulas.Variable; -import org.logicng.knowledgecompilation.dnnf.DNNFSATSolver; +import org.logicng.knowledgecompilation.dnnf.DnnfSatSolver; import java.util.BitSet; import java.util.List; @@ -23,7 +51,7 @@ public abstract class DTree { * Initializes the DTree. * @param solver a specializes DNNF SAT solver */ - public abstract void initialize(final DNNFSATSolver solver); + public abstract void initialize(final DnnfSatSolver solver); /** * Returns the size of the DTree. diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTreeGenerator.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTreeGenerator.java index 6c5083f8..daf45eb5 100644 --- a/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTreeGenerator.java +++ b/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTreeGenerator.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.knowledgecompilation.dnnf.datastructures.dtree; import org.logicng.formulas.Formula; diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTreeLeaf.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTreeLeaf.java index 2dea236e..3bd0b679 100644 --- a/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTreeLeaf.java +++ b/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTreeLeaf.java @@ -1,10 +1,38 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.knowledgecompilation.dnnf.datastructures.dtree; import org.logicng.datastructures.Tristate; import org.logicng.formulas.Formula; import org.logicng.formulas.Literal; import org.logicng.formulas.Variable; -import org.logicng.knowledgecompilation.dnnf.DNNFSATSolver; +import org.logicng.knowledgecompilation.dnnf.DnnfSatSolver; import org.logicng.solvers.sat.MiniSatStyleSolver; import java.util.ArrayList; @@ -28,7 +56,7 @@ public class DTreeLeaf extends DTree { protected final BitSet separatorBitSet = new BitSet(); - protected DNNFSATSolver solver; + protected DnnfSatSolver solver; protected final int[] staticClauseIds; /** @@ -46,7 +74,7 @@ public DTreeLeaf(final int id, final Formula clause) { } @Override - public void initialize(final DNNFSATSolver solver) { + public void initialize(final DnnfSatSolver solver) { this.solver = solver; final SortedSet lits = this.clause.literals(); final int size = lits.size(); diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTreeNode.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTreeNode.java index 730d3df8..3ed95a0a 100644 --- a/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTreeNode.java +++ b/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTreeNode.java @@ -1,9 +1,37 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.knowledgecompilation.dnnf.datastructures.dtree; import org.logicng.collections.LNGIntVector; import org.logicng.datastructures.Tristate; import org.logicng.formulas.Variable; -import org.logicng.knowledgecompilation.dnnf.DNNFSATSolver; +import org.logicng.knowledgecompilation.dnnf.DnnfSatSolver; import org.logicng.solvers.sat.MiniSatStyleSolver; import java.util.BitSet; @@ -22,7 +50,7 @@ public class DTreeNode extends DTree { protected final DTree right; protected final int size; - protected DNNFSATSolver solver; + protected DnnfSatSolver solver; protected final SortedSet staticVariableSet; protected final BitSet staticSeparatorBitSet; @@ -89,7 +117,7 @@ public DTree right() { } @Override - public void initialize(final DNNFSATSolver solver) { + public void initialize(final DnnfSatSolver solver) { this.solver = solver; this.left.initialize(solver); this.right.initialize(solver); diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/EliminatingOrderDTreeGenerator.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/EliminatingOrderDTreeGenerator.java index 0552193b..70dbee8c 100644 --- a/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/EliminatingOrderDTreeGenerator.java +++ b/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/EliminatingOrderDTreeGenerator.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.knowledgecompilation.dnnf.datastructures.dtree; import org.logicng.formulas.FType; diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/MinFillDTreeGenerator.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/MinFillDTreeGenerator.java index 76d71d9b..30c17399 100644 --- a/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/MinFillDTreeGenerator.java +++ b/src/main/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/MinFillDTreeGenerator.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.knowledgecompilation.dnnf.datastructures.dtree; import org.logicng.collections.LNGIntVector; diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DNNFFunction.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DNNFFunction.java deleted file mode 100644 index d0599a04..00000000 --- a/src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DNNFFunction.java +++ /dev/null @@ -1,23 +0,0 @@ -package org.logicng.knowledgecompilation.dnnf.functions; - -import org.logicng.formulas.Formula; -import org.logicng.formulas.Variable; - -import java.util.SortedSet; - -/** - * A function which can be applied on a DNNF. - * @param the result type of the function - * @version 2.0.0 - * @since 2.0.0 - */ -public interface DNNFFunction { - - /** - * Applies this function to a given DNNF - * @param originalVariables the original variables of the DNNF - * @param formula the formula of the DNNF - * @return the result of the function application - */ - RESULT apply(final SortedSet originalVariables, final Formula formula); -} diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DnnfFunction.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DnnfFunction.java new file mode 100644 index 00000000..ebc26d9b --- /dev/null +++ b/src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DnnfFunction.java @@ -0,0 +1,51 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + +package org.logicng.knowledgecompilation.dnnf.functions; + +import org.logicng.formulas.Formula; +import org.logicng.formulas.Variable; + +import java.util.SortedSet; + +/** + * A function which can be applied on a DNNF. + * @param the result type of the function + * @version 2.0.0 + * @since 2.0.0 + */ +public interface DnnfFunction { + + /** + * Applies this function to a given DNNF + * @param originalVariables the original variables of the DNNF + * @param formula the formula of the DNNF + * @return the result of the function application + */ + RESULT apply(final SortedSet originalVariables, final Formula formula); +} diff --git a/src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DNNFModelCountFunction.java b/src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DnnfModelCountFunction.java similarity index 55% rename from src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DNNFModelCountFunction.java rename to src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DnnfModelCountFunction.java index 54a9b978..bb8b3cec 100644 --- a/src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DNNFModelCountFunction.java +++ b/src/main/java/org/logicng/knowledgecompilation/dnnf/functions/DnnfModelCountFunction.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.knowledgecompilation.dnnf.functions; import org.logicng.formulas.Formula; @@ -15,11 +43,11 @@ * @version 2.0.0 * @since 2.0.0 */ -public final class DNNFModelCountFunction implements DNNFFunction { +public final class DnnfModelCountFunction implements DnnfFunction { - private static final DNNFModelCountFunction INSTANCE = new DNNFModelCountFunction(); + private static final DnnfModelCountFunction INSTANCE = new DnnfModelCountFunction(); - private DNNFModelCountFunction() { + private DnnfModelCountFunction() { // intentionally left empty } @@ -27,7 +55,7 @@ private DNNFModelCountFunction() { * Returns the singleton instance of this function. * @return an instance of this function */ - public static DNNFModelCountFunction get() { + public static DnnfModelCountFunction get() { return INSTANCE; } diff --git a/src/main/java/org/logicng/modelcounting/ModelCounter.java b/src/main/java/org/logicng/modelcounting/ModelCounter.java index e983814b..0fed5eae 100644 --- a/src/main/java/org/logicng/modelcounting/ModelCounter.java +++ b/src/main/java/org/logicng/modelcounting/ModelCounter.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.modelcounting; import org.logicng.datastructures.Assignment; @@ -10,9 +38,9 @@ import org.logicng.graphs.datastructures.Graph; import org.logicng.graphs.datastructures.Node; import org.logicng.graphs.generators.ConstraintGraphGenerator; -import org.logicng.knowledgecompilation.dnnf.DNNFFactory; -import org.logicng.knowledgecompilation.dnnf.datastructures.DNNF; -import org.logicng.knowledgecompilation.dnnf.functions.DNNFModelCountFunction; +import org.logicng.knowledgecompilation.dnnf.DnnfFactory; +import org.logicng.knowledgecompilation.dnnf.datastructures.Dnnf; +import org.logicng.knowledgecompilation.dnnf.functions.DnnfModelCountFunction; import org.logicng.transformations.PureExpansionTransformation; import org.logicng.transformations.cnf.CNFConfig; import org.logicng.transformations.cnf.CNFEncoder; @@ -98,11 +126,11 @@ private static BigInteger count(final Collection formulas, final Formul final Graph constraintGraph = ConstraintGraphGenerator.generateFromFormulas(formulas); final Set>> ccs = ConnectedComponentsComputation.compute(constraintGraph); final List> components = ConnectedComponentsComputation.splitFormulasByComponent(formulas, ccs); - final DNNFFactory factory = new DNNFFactory(); + final DnnfFactory factory = new DnnfFactory(); BigInteger count = BigInteger.ONE; for (final List component : components) { - final DNNF dnnf = factory.compile(f.and(component)); - count = count.multiply(dnnf.execute(DNNFModelCountFunction.get())); + final Dnnf dnnf = factory.compile(f.and(component)); + count = count.multiply(dnnf.execute(DnnfModelCountFunction.get())); } return count; } diff --git a/src/main/java/org/logicng/np/SetCover.java b/src/main/java/org/logicng/np/SetCover.java index b18c64b7..cf54a1e1 100644 --- a/src/main/java/org/logicng/np/SetCover.java +++ b/src/main/java/org/logicng/np/SetCover.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.np; import org.logicng.formulas.FormulaFactory; diff --git a/src/main/java/org/logicng/predicates/AIGPredicate.java b/src/main/java/org/logicng/predicates/AIGPredicate.java index 92ae42bc..33444b2d 100644 --- a/src/main/java/org/logicng/predicates/AIGPredicate.java +++ b/src/main/java/org/logicng/predicates/AIGPredicate.java @@ -28,13 +28,13 @@ package org.logicng.predicates; +import static org.logicng.formulas.cache.PredicateCacheEntry.IS_AIG; + import org.logicng.datastructures.Tristate; import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaPredicate; import org.logicng.formulas.Not; -import static org.logicng.formulas.cache.PredicateCacheEntry.IS_AIG; - /** * And-inverter-graph (AIG) predicate. Returns {@code true} if the given formula is an AIG, {@code false} otherwise. * @version 1.0 diff --git a/src/main/java/org/logicng/predicates/CNFPredicate.java b/src/main/java/org/logicng/predicates/CNFPredicate.java index 501e4939..31a4e558 100644 --- a/src/main/java/org/logicng/predicates/CNFPredicate.java +++ b/src/main/java/org/logicng/predicates/CNFPredicate.java @@ -28,12 +28,12 @@ package org.logicng.predicates; +import static org.logicng.formulas.cache.PredicateCacheEntry.IS_CNF; + import org.logicng.datastructures.Tristate; import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaPredicate; -import static org.logicng.formulas.cache.PredicateCacheEntry.IS_CNF; - /** * CNF predicate. Indicates whether a formula is in CNF or not. * @version 1.0 diff --git a/src/main/java/org/logicng/predicates/ContainsPBCPredicate.java b/src/main/java/org/logicng/predicates/ContainsPBCPredicate.java index a1ffb2f2..10a035a0 100644 --- a/src/main/java/org/logicng/predicates/ContainsPBCPredicate.java +++ b/src/main/java/org/logicng/predicates/ContainsPBCPredicate.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.predicates; import org.logicng.formulas.BinaryOperator; diff --git a/src/main/java/org/logicng/predicates/DNFPredicate.java b/src/main/java/org/logicng/predicates/DNFPredicate.java index ec85ec8a..87954671 100644 --- a/src/main/java/org/logicng/predicates/DNFPredicate.java +++ b/src/main/java/org/logicng/predicates/DNFPredicate.java @@ -28,13 +28,13 @@ package org.logicng.predicates; +import static org.logicng.formulas.cache.PredicateCacheEntry.IS_DNF; + import org.logicng.datastructures.Tristate; import org.logicng.formulas.FType; import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaPredicate; -import static org.logicng.formulas.cache.PredicateCacheEntry.IS_DNF; - /** * DNF predicate. Indicates whether a formula is in DNF or not. * @version 1.0 diff --git a/src/main/java/org/logicng/predicates/EvaluatesToConstantPredicate.java b/src/main/java/org/logicng/predicates/EvaluatesToConstantPredicate.java index bc8424e1..d39d863d 100644 --- a/src/main/java/org/logicng/predicates/EvaluatesToConstantPredicate.java +++ b/src/main/java/org/logicng/predicates/EvaluatesToConstantPredicate.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.predicates; import org.logicng.datastructures.Assignment; diff --git a/src/main/java/org/logicng/predicates/NNFPredicate.java b/src/main/java/org/logicng/predicates/NNFPredicate.java index 5f56eb0f..54182e0a 100644 --- a/src/main/java/org/logicng/predicates/NNFPredicate.java +++ b/src/main/java/org/logicng/predicates/NNFPredicate.java @@ -28,12 +28,12 @@ package org.logicng.predicates; +import static org.logicng.formulas.cache.PredicateCacheEntry.IS_NNF; + import org.logicng.datastructures.Tristate; import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaPredicate; -import static org.logicng.formulas.cache.PredicateCacheEntry.IS_NNF; - /** * NNF predicate. Indicates whether a formula is in NNF or not. * @version 1.5.1 diff --git a/src/main/java/org/logicng/predicates/satisfiability/SATPredicate.java b/src/main/java/org/logicng/predicates/satisfiability/SATPredicate.java index f328c00b..3e0c72cc 100644 --- a/src/main/java/org/logicng/predicates/satisfiability/SATPredicate.java +++ b/src/main/java/org/logicng/predicates/satisfiability/SATPredicate.java @@ -28,6 +28,8 @@ package org.logicng.predicates.satisfiability; +import static org.logicng.formulas.cache.PredicateCacheEntry.IS_SAT; + import org.logicng.datastructures.Tristate; import org.logicng.formulas.FType; import org.logicng.formulas.Formula; @@ -36,8 +38,6 @@ import org.logicng.solvers.MiniSat; import org.logicng.solvers.SATSolver; -import static org.logicng.formulas.cache.PredicateCacheEntry.IS_SAT; - /** * A SAT solver based SAT predicate. Indicates whether a formula is satisfiable or not. * @version 1.5.1 diff --git a/src/main/java/org/logicng/primecomputation/NaivePrimeReduction.java b/src/main/java/org/logicng/primecomputation/NaivePrimeReduction.java index 7167829c..484db403 100644 --- a/src/main/java/org/logicng/primecomputation/NaivePrimeReduction.java +++ b/src/main/java/org/logicng/primecomputation/NaivePrimeReduction.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.primecomputation; import org.logicng.datastructures.Tristate; diff --git a/src/main/java/org/logicng/primecomputation/PrimeCompiler.java b/src/main/java/org/logicng/primecomputation/PrimeCompiler.java index 9520d6b6..98475dcd 100644 --- a/src/main/java/org/logicng/primecomputation/PrimeCompiler.java +++ b/src/main/java/org/logicng/primecomputation/PrimeCompiler.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.primecomputation; import org.logicng.datastructures.Assignment; diff --git a/src/main/java/org/logicng/primecomputation/PrimeResult.java b/src/main/java/org/logicng/primecomputation/PrimeResult.java index 8ae0059c..e95fc36c 100644 --- a/src/main/java/org/logicng/primecomputation/PrimeResult.java +++ b/src/main/java/org/logicng/primecomputation/PrimeResult.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.primecomputation; import org.logicng.formulas.Literal; diff --git a/src/main/java/org/logicng/pseudobooleans/PBEncoding.java b/src/main/java/org/logicng/pseudobooleans/PBEncoding.java index 2eddf9fb..5b8c3ede 100644 --- a/src/main/java/org/logicng/pseudobooleans/PBEncoding.java +++ b/src/main/java/org/logicng/pseudobooleans/PBEncoding.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.pseudobooleans; import org.logicng.collections.LNGIntVector; diff --git a/src/main/java/org/logicng/solvers/functions/BackboneFunction.java b/src/main/java/org/logicng/solvers/functions/BackboneFunction.java index 19811fdd..80ba25cb 100644 --- a/src/main/java/org/logicng/solvers/functions/BackboneFunction.java +++ b/src/main/java/org/logicng/solvers/functions/BackboneFunction.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.solvers.functions; import org.logicng.backbones.Backbone; diff --git a/src/main/java/org/logicng/solvers/functions/FormulaOnSolverFunction.java b/src/main/java/org/logicng/solvers/functions/FormulaOnSolverFunction.java index 08464f17..d4cd2c9a 100644 --- a/src/main/java/org/logicng/solvers/functions/FormulaOnSolverFunction.java +++ b/src/main/java/org/logicng/solvers/functions/FormulaOnSolverFunction.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.solvers.functions; import static org.logicng.datastructures.Tristate.TRUE; diff --git a/src/main/java/org/logicng/solvers/functions/ModelEnumerationFunction.java b/src/main/java/org/logicng/solvers/functions/ModelEnumerationFunction.java index d8dfa925..7a6d7836 100644 --- a/src/main/java/org/logicng/solvers/functions/ModelEnumerationFunction.java +++ b/src/main/java/org/logicng/solvers/functions/ModelEnumerationFunction.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.solvers.functions; import static org.logicng.datastructures.Tristate.TRUE; diff --git a/src/main/java/org/logicng/solvers/functions/OptimizationFunction.java b/src/main/java/org/logicng/solvers/functions/OptimizationFunction.java index eede7800..32de0496 100644 --- a/src/main/java/org/logicng/solvers/functions/OptimizationFunction.java +++ b/src/main/java/org/logicng/solvers/functions/OptimizationFunction.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.solvers.functions; import org.logicng.cardinalityconstraints.CCIncrementalData; diff --git a/src/main/java/org/logicng/solvers/functions/SolverFunction.java b/src/main/java/org/logicng/solvers/functions/SolverFunction.java index d621bd9e..831f705e 100644 --- a/src/main/java/org/logicng/solvers/functions/SolverFunction.java +++ b/src/main/java/org/logicng/solvers/functions/SolverFunction.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.solvers.functions; import org.logicng.datastructures.Tristate; diff --git a/src/main/java/org/logicng/solvers/functions/UnsatCoreFunction.java b/src/main/java/org/logicng/solvers/functions/UnsatCoreFunction.java index d4ebfe1b..cc42e393 100644 --- a/src/main/java/org/logicng/solvers/functions/UnsatCoreFunction.java +++ b/src/main/java/org/logicng/solvers/functions/UnsatCoreFunction.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.solvers.functions; import static org.logicng.datastructures.Tristate.TRUE; diff --git a/src/main/java/org/logicng/solvers/functions/UpZeroLiteralsFunction.java b/src/main/java/org/logicng/solvers/functions/UpZeroLiteralsFunction.java index 77c4c793..28ac7d78 100644 --- a/src/main/java/org/logicng/solvers/functions/UpZeroLiteralsFunction.java +++ b/src/main/java/org/logicng/solvers/functions/UpZeroLiteralsFunction.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.solvers.functions; import static org.logicng.datastructures.Tristate.FALSE; diff --git a/src/main/java/org/logicng/transformations/Anonymizer.java b/src/main/java/org/logicng/transformations/Anonymizer.java index 36389d8d..5c9869fd 100644 --- a/src/main/java/org/logicng/transformations/Anonymizer.java +++ b/src/main/java/org/logicng/transformations/Anonymizer.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.transformations; import static org.logicng.formulas.cache.TransformationCacheEntry.ANONYMIZATION; diff --git a/src/main/java/org/logicng/transformations/LiteralSubstitution.java b/src/main/java/org/logicng/transformations/LiteralSubstitution.java index 38d59e48..b42372b0 100644 --- a/src/main/java/org/logicng/transformations/LiteralSubstitution.java +++ b/src/main/java/org/logicng/transformations/LiteralSubstitution.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.transformations; import org.logicng.formulas.BinaryOperator; diff --git a/src/main/java/org/logicng/transformations/PureExpansionTransformation.java b/src/main/java/org/logicng/transformations/PureExpansionTransformation.java index efe09a82..2aab4485 100644 --- a/src/main/java/org/logicng/transformations/PureExpansionTransformation.java +++ b/src/main/java/org/logicng/transformations/PureExpansionTransformation.java @@ -28,6 +28,8 @@ package org.logicng.transformations; +import static org.logicng.util.FormulaHelper.literalsAsVariables; + import org.logicng.cardinalityconstraints.CCAMOPure; import org.logicng.datastructures.EncodingResult; import org.logicng.formulas.BinaryOperator; @@ -42,8 +44,6 @@ import java.util.ArrayList; import java.util.List; -import static org.logicng.util.FormulaHelper.literalsAsVariables; - /** * Transformation of a formula to a formula with expanded at-most-one and exactly-one cardinality constraints. * Each subformula of the formula that is a pseudo-Boolean constraint of type AMO or EXO gets replaced by a pure encoding such that diff --git a/src/main/java/org/logicng/transformations/Subsumption.java b/src/main/java/org/logicng/transformations/Subsumption.java index 82867aaa..f7fb6896 100644 --- a/src/main/java/org/logicng/transformations/Subsumption.java +++ b/src/main/java/org/logicng/transformations/Subsumption.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.transformations; import org.logicng.datastructures.ubtrees.UBTree; diff --git a/src/main/java/org/logicng/transformations/cnf/CNFFactorization.java b/src/main/java/org/logicng/transformations/cnf/CNFFactorization.java index 7154161d..e7faad8a 100644 --- a/src/main/java/org/logicng/transformations/cnf/CNFFactorization.java +++ b/src/main/java/org/logicng/transformations/cnf/CNFFactorization.java @@ -28,6 +28,10 @@ package org.logicng.transformations.cnf; +import static org.logicng.formulas.FType.AND; +import static org.logicng.formulas.FType.LITERAL; +import static org.logicng.formulas.cache.TransformationCacheEntry.FACTORIZED_CNF; + import org.logicng.formulas.Formula; import org.logicng.formulas.FormulaFactory; import org.logicng.formulas.FormulaTransformation; @@ -36,10 +40,6 @@ import java.util.Iterator; import java.util.LinkedHashSet; -import static org.logicng.formulas.FType.AND; -import static org.logicng.formulas.FType.LITERAL; -import static org.logicng.formulas.cache.TransformationCacheEntry.FACTORIZED_CNF; - /** * Transformation of a formula in CNF by factorization. * @version 1.1 @@ -75,7 +75,7 @@ public Formula apply(final Formula formula, final boolean cache) { this.proceed = true; return applyRec(formula, cache); } - + private Formula applyRec(final Formula formula, final boolean cache) { if (!this.proceed) { return null; diff --git a/src/main/java/org/logicng/transformations/cnf/PlaistedGreenbaumTransformation.java b/src/main/java/org/logicng/transformations/cnf/PlaistedGreenbaumTransformation.java index 796472d3..21cb1977 100644 --- a/src/main/java/org/logicng/transformations/cnf/PlaistedGreenbaumTransformation.java +++ b/src/main/java/org/logicng/transformations/cnf/PlaistedGreenbaumTransformation.java @@ -28,6 +28,9 @@ package org.logicng.transformations.cnf; +import static org.logicng.formulas.cache.TransformationCacheEntry.PLAISTED_GREENBAUM_POS; +import static org.logicng.formulas.cache.TransformationCacheEntry.PLAISTED_GREENBAUM_VARIABLE; + import org.logicng.datastructures.Assignment; import org.logicng.formulas.FType; import org.logicng.formulas.Formula; @@ -39,9 +42,6 @@ import java.util.ArrayList; import java.util.List; -import static org.logicng.formulas.cache.TransformationCacheEntry.PLAISTED_GREENBAUM_POS; -import static org.logicng.formulas.cache.TransformationCacheEntry.PLAISTED_GREENBAUM_VARIABLE; - /** * Transformation of a formula into CNF due to Plaisted & Greenbaum. Results in this implementation will always be * cached. diff --git a/src/main/java/org/logicng/transformations/qmc/QuineMcCluskeyAlgorithm.java b/src/main/java/org/logicng/transformations/qmc/QuineMcCluskeyAlgorithm.java index 507c8902..2e5d69f5 100644 --- a/src/main/java/org/logicng/transformations/qmc/QuineMcCluskeyAlgorithm.java +++ b/src/main/java/org/logicng/transformations/qmc/QuineMcCluskeyAlgorithm.java @@ -25,6 +25,7 @@ // permissions and limitations under the License. // // // /////////////////////////////////////////////////////////////////////////// + package org.logicng.transformations.qmc; import org.logicng.cardinalityconstraints.CCIncrementalData; diff --git a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java index 1c59a088..ba3e46d3 100644 --- a/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java +++ b/src/main/java/org/logicng/transformations/simplification/AdvancedSimplifier.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.transformations.simplification; import org.logicng.backbones.Backbone; diff --git a/src/main/java/org/logicng/transformations/simplification/BackboneSimplifier.java b/src/main/java/org/logicng/transformations/simplification/BackboneSimplifier.java index 9a5bb84f..244d1d59 100644 --- a/src/main/java/org/logicng/transformations/simplification/BackboneSimplifier.java +++ b/src/main/java/org/logicng/transformations/simplification/BackboneSimplifier.java @@ -25,6 +25,7 @@ // permissions and limitations under the License. // // // /////////////////////////////////////////////////////////////////////////// + package org.logicng.transformations.simplification; import org.logicng.backbones.Backbone; diff --git a/src/main/java/org/logicng/util/CollectionHelper.java b/src/main/java/org/logicng/util/CollectionHelper.java index 3339a2e8..0ef1fb6a 100644 --- a/src/main/java/org/logicng/util/CollectionHelper.java +++ b/src/main/java/org/logicng/util/CollectionHelper.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.util; import java.util.Collection; diff --git a/src/main/java/org/logicng/util/FormulaCornerCases.java b/src/main/java/org/logicng/util/FormulaCornerCases.java index dbb33351..6dd45ed4 100644 --- a/src/main/java/org/logicng/util/FormulaCornerCases.java +++ b/src/main/java/org/logicng/util/FormulaCornerCases.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.util; import org.logicng.formulas.CType; diff --git a/src/main/java/org/logicng/util/FormulaHelper.java b/src/main/java/org/logicng/util/FormulaHelper.java index 27ca8080..e2ee0da6 100644 --- a/src/main/java/org/logicng/util/FormulaHelper.java +++ b/src/main/java/org/logicng/util/FormulaHelper.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.util; import org.logicng.formulas.And; diff --git a/src/main/java/org/logicng/util/FormulaRandomizer.java b/src/main/java/org/logicng/util/FormulaRandomizer.java index ee857b6a..2a41c41f 100644 --- a/src/main/java/org/logicng/util/FormulaRandomizer.java +++ b/src/main/java/org/logicng/util/FormulaRandomizer.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.util; import org.logicng.formulas.CType; diff --git a/src/main/java/org/logicng/util/FormulaRandomizerConfig.java b/src/main/java/org/logicng/util/FormulaRandomizerConfig.java index a38e6416..38ef885c 100644 --- a/src/main/java/org/logicng/util/FormulaRandomizerConfig.java +++ b/src/main/java/org/logicng/util/FormulaRandomizerConfig.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.util; import org.logicng.configurations.Configuration; diff --git a/src/test/java/org/logicng/LogicNGTest.java b/src/test/java/org/logicng/LogicNGTest.java index 8383f765..81ab56f0 100644 --- a/src/test/java/org/logicng/LogicNGTest.java +++ b/src/test/java/org/logicng/LogicNGTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/LogicNGVersionTest.java b/src/test/java/org/logicng/LogicNGVersionTest.java index 86916d88..1aaf821c 100644 --- a/src/test/java/org/logicng/LogicNGVersionTest.java +++ b/src/test/java/org/logicng/LogicNGVersionTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/LongRunningTag.java b/src/test/java/org/logicng/LongRunningTag.java index c355252a..de7d903b 100644 --- a/src/test/java/org/logicng/LongRunningTag.java +++ b/src/test/java/org/logicng/LongRunningTag.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng; import org.junit.jupiter.api.Tag; diff --git a/src/test/java/org/logicng/RandomTag.java b/src/test/java/org/logicng/RandomTag.java index 17ad03d4..8b9285b8 100644 --- a/src/test/java/org/logicng/RandomTag.java +++ b/src/test/java/org/logicng/RandomTag.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng; import org.junit.jupiter.api.Tag; diff --git a/src/test/java/org/logicng/TestWithExampleFormulas.java b/src/test/java/org/logicng/TestWithExampleFormulas.java index 849730ac..b6c1fe5f 100644 --- a/src/test/java/org/logicng/TestWithExampleFormulas.java +++ b/src/test/java/org/logicng/TestWithExampleFormulas.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng; import org.logicng.formulas.CType; diff --git a/src/test/java/org/logicng/cardinalityconstraints/CCALKTest.java b/src/test/java/org/logicng/cardinalityconstraints/CCALKTest.java index ecdc1096..f732087c 100644 --- a/src/test/java/org/logicng/cardinalityconstraints/CCALKTest.java +++ b/src/test/java/org/logicng/cardinalityconstraints/CCALKTest.java @@ -28,6 +28,9 @@ package org.logicng.cardinalityconstraints; +import static org.assertj.core.api.Assertions.assertThat; +import static org.assertj.core.api.Assertions.assertThatThrownBy; + import org.junit.jupiter.api.Test; import org.logicng.LogicNGTest; import org.logicng.formulas.CType; @@ -41,9 +44,6 @@ import java.util.Arrays; -import static org.assertj.core.api.Assertions.assertThat; -import static org.assertj.core.api.Assertions.assertThatThrownBy; - /** * Unit tests for the at-least-k configs. * @version 2.0.0 diff --git a/src/test/java/org/logicng/cardinalityconstraints/CCAMKTest.java b/src/test/java/org/logicng/cardinalityconstraints/CCAMKTest.java index 8b5d77e2..984dba52 100644 --- a/src/test/java/org/logicng/cardinalityconstraints/CCAMKTest.java +++ b/src/test/java/org/logicng/cardinalityconstraints/CCAMKTest.java @@ -28,6 +28,9 @@ package org.logicng.cardinalityconstraints; +import static org.assertj.core.api.Assertions.assertThat; +import static org.assertj.core.api.Assertions.assertThatThrownBy; + import org.junit.jupiter.api.Test; import org.logicng.LogicNGTest; import org.logicng.LongRunningTag; @@ -38,9 +41,6 @@ import org.logicng.solvers.MiniSat; import org.logicng.solvers.SATSolver; -import static org.assertj.core.api.Assertions.assertThat; -import static org.assertj.core.api.Assertions.assertThatThrownBy; - /** * Unit tests for the at-most-k encoders. * @version 2.0.0 diff --git a/src/test/java/org/logicng/cardinalityconstraints/CCAMOTest.java b/src/test/java/org/logicng/cardinalityconstraints/CCAMOTest.java index b795e1b5..6e9cd9ba 100644 --- a/src/test/java/org/logicng/cardinalityconstraints/CCAMOTest.java +++ b/src/test/java/org/logicng/cardinalityconstraints/CCAMOTest.java @@ -28,15 +28,6 @@ package org.logicng.cardinalityconstraints; -import org.junit.jupiter.api.Test; -import org.logicng.LogicNGTest; -import org.logicng.formulas.CardinalityConstraint; -import org.logicng.formulas.Formula; -import org.logicng.formulas.FormulaFactory; -import org.logicng.formulas.Variable; -import org.logicng.solvers.MiniSat; -import org.logicng.solvers.SATSolver; - import static org.assertj.core.api.Assertions.assertThat; import static org.logicng.cardinalityconstraints.CCConfig.AMO_ENCODER.BEST; import static org.logicng.cardinalityconstraints.CCConfig.AMO_ENCODER.BIMANDER; @@ -50,6 +41,15 @@ import static org.logicng.cardinalityconstraints.CCConfig.BIMANDER_GROUP_SIZE.HALF; import static org.logicng.cardinalityconstraints.CCConfig.BIMANDER_GROUP_SIZE.SQRT; +import org.junit.jupiter.api.Test; +import org.logicng.LogicNGTest; +import org.logicng.formulas.CardinalityConstraint; +import org.logicng.formulas.Formula; +import org.logicng.formulas.FormulaFactory; +import org.logicng.formulas.Variable; +import org.logicng.solvers.MiniSat; +import org.logicng.solvers.SATSolver; + /** * Unit tests for the at-most-one configs. * @version 2.0.0 diff --git a/src/test/java/org/logicng/cardinalityconstraints/CCEXKTest.java b/src/test/java/org/logicng/cardinalityconstraints/CCEXKTest.java index 13813ec3..29dffbcb 100644 --- a/src/test/java/org/logicng/cardinalityconstraints/CCEXKTest.java +++ b/src/test/java/org/logicng/cardinalityconstraints/CCEXKTest.java @@ -28,6 +28,8 @@ package org.logicng.cardinalityconstraints; +import static org.assertj.core.api.Assertions.assertThat; + import org.junit.jupiter.api.Test; import org.logicng.LogicNGTest; import org.logicng.datastructures.EncodingResult; @@ -37,8 +39,6 @@ import org.logicng.solvers.MiniSat; import org.logicng.solvers.SATSolver; -import static org.assertj.core.api.Assertions.assertThat; - /** * Unit tests for the exactly-k encoders. * @version 2.0.0 diff --git a/src/test/java/org/logicng/cardinalityconstraints/CCEXOTest.java b/src/test/java/org/logicng/cardinalityconstraints/CCEXOTest.java index b7c5ba3f..a4cb5c70 100644 --- a/src/test/java/org/logicng/cardinalityconstraints/CCEXOTest.java +++ b/src/test/java/org/logicng/cardinalityconstraints/CCEXOTest.java @@ -28,18 +28,6 @@ package org.logicng.cardinalityconstraints; -import org.junit.jupiter.api.Test; -import org.logicng.LogicNGTest; -import org.logicng.formulas.CardinalityConstraint; -import org.logicng.formulas.Formula; -import org.logicng.formulas.FormulaFactory; -import org.logicng.formulas.Variable; -import org.logicng.solvers.MiniSat; -import org.logicng.solvers.SATSolver; - -import java.util.stream.Collectors; -import java.util.stream.IntStream; - import static org.assertj.core.api.Assertions.assertThat; import static org.logicng.cardinalityconstraints.CCConfig.AMO_ENCODER.BEST; import static org.logicng.cardinalityconstraints.CCConfig.AMO_ENCODER.BIMANDER; @@ -53,6 +41,18 @@ import static org.logicng.cardinalityconstraints.CCConfig.BIMANDER_GROUP_SIZE.HALF; import static org.logicng.cardinalityconstraints.CCConfig.BIMANDER_GROUP_SIZE.SQRT; +import org.junit.jupiter.api.Test; +import org.logicng.LogicNGTest; +import org.logicng.formulas.CardinalityConstraint; +import org.logicng.formulas.Formula; +import org.logicng.formulas.FormulaFactory; +import org.logicng.formulas.Variable; +import org.logicng.solvers.MiniSat; +import org.logicng.solvers.SATSolver; + +import java.util.stream.Collectors; +import java.util.stream.IntStream; + /** * Unit tests for the exactly-one encoders. * @version 2.0.0 diff --git a/src/test/java/org/logicng/cardinalityconstraints/CCIncrementalFormulaTest.java b/src/test/java/org/logicng/cardinalityconstraints/CCIncrementalFormulaTest.java index 81ca6800..ceaa9e77 100644 --- a/src/test/java/org/logicng/cardinalityconstraints/CCIncrementalFormulaTest.java +++ b/src/test/java/org/logicng/cardinalityconstraints/CCIncrementalFormulaTest.java @@ -28,6 +28,8 @@ package org.logicng.cardinalityconstraints; +import static org.assertj.core.api.Assertions.assertThat; + import org.junit.jupiter.api.Test; import org.logicng.LogicNGTest; import org.logicng.LongRunningTag; @@ -45,8 +47,6 @@ import java.util.List; -import static org.assertj.core.api.Assertions.assertThat; - /** * Tests for incremental cardinality constraints generated as formulas and {@link CCIncrementalData}. * @version 2.0.0 diff --git a/src/test/java/org/logicng/cardinalityconstraints/CCIncrementalSolverTest.java b/src/test/java/org/logicng/cardinalityconstraints/CCIncrementalSolverTest.java index 7a6b5e72..0e005185 100644 --- a/src/test/java/org/logicng/cardinalityconstraints/CCIncrementalSolverTest.java +++ b/src/test/java/org/logicng/cardinalityconstraints/CCIncrementalSolverTest.java @@ -28,6 +28,8 @@ package org.logicng.cardinalityconstraints; +import static org.assertj.core.api.Assertions.assertThat; + import org.junit.jupiter.api.Test; import org.logicng.LogicNGTest; import org.logicng.LongRunningTag; @@ -41,8 +43,6 @@ import org.logicng.solvers.SolverState; import org.logicng.solvers.sat.MiniSatConfig; -import static org.assertj.core.api.Assertions.assertThat; - /** * Tests for incremental cardinality constraints generated on the solver and {@link CCIncrementalData}. * @version 2.0.0 diff --git a/src/test/java/org/logicng/cardinalityconstraints/CCPerformanceTest.java b/src/test/java/org/logicng/cardinalityconstraints/CCPerformanceTest.java index 35531c01..3138c8e4 100644 --- a/src/test/java/org/logicng/cardinalityconstraints/CCPerformanceTest.java +++ b/src/test/java/org/logicng/cardinalityconstraints/CCPerformanceTest.java @@ -28,6 +28,8 @@ package org.logicng.cardinalityconstraints; +import static org.assertj.core.api.Assertions.assertThat; + import org.junit.jupiter.api.Test; import org.logicng.LogicNGTest; import org.logicng.LongRunningTag; @@ -39,8 +41,6 @@ import org.logicng.solvers.MiniSat; import org.logicng.solvers.SATSolver; -import static org.assertj.core.api.Assertions.assertThat; - /** * Performance tests for cardinality constraints. * @version 2.0.0 diff --git a/src/test/java/org/logicng/collections/LNGVectorTest.java b/src/test/java/org/logicng/collections/LNGVectorTest.java index ae868318..10be930a 100644 --- a/src/test/java/org/logicng/collections/LNGVectorTest.java +++ b/src/test/java/org/logicng/collections/LNGVectorTest.java @@ -28,6 +28,9 @@ package org.logicng.collections; +import static org.assertj.core.api.Assertions.assertThat; +import static org.assertj.core.api.Assertions.assertThatThrownBy; + import org.junit.jupiter.api.Test; import java.util.ArrayList; @@ -36,9 +39,6 @@ import java.util.List; import java.util.NoSuchElementException; -import static org.assertj.core.api.Assertions.assertThat; -import static org.assertj.core.api.Assertions.assertThatThrownBy; - /** * Unit tests for {@link LNGVector}. * @version 2.0.0 diff --git a/src/test/java/org/logicng/datastructures/ubtrees/UBNodeTest.java b/src/test/java/org/logicng/datastructures/ubtrees/UBNodeTest.java index ce8b6845..555dfce8 100644 --- a/src/test/java/org/logicng/datastructures/ubtrees/UBNodeTest.java +++ b/src/test/java/org/logicng/datastructures/ubtrees/UBNodeTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.datastructures.ubtrees; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/datastructures/ubtrees/UBTreeTest.java b/src/test/java/org/logicng/datastructures/ubtrees/UBTreeTest.java index 9a500100..3bb02d6e 100644 --- a/src/test/java/org/logicng/datastructures/ubtrees/UBTreeTest.java +++ b/src/test/java/org/logicng/datastructures/ubtrees/UBTreeTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.datastructures.ubtrees; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/explanations/UNSATCoreTest.java b/src/test/java/org/logicng/explanations/UNSATCoreTest.java index 2a3cf7d8..f870a42f 100644 --- a/src/test/java/org/logicng/explanations/UNSATCoreTest.java +++ b/src/test/java/org/logicng/explanations/UNSATCoreTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.explanations; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java b/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java index baad1277..ec1b6ad2 100644 --- a/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java +++ b/src/test/java/org/logicng/explanations/smus/SmusComputationTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.explanations.smus; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/formulas/CacheTest.java b/src/test/java/org/logicng/formulas/CacheTest.java index 8ad0e5fe..d42bd00b 100644 --- a/src/test/java/org/logicng/formulas/CacheTest.java +++ b/src/test/java/org/logicng/formulas/CacheTest.java @@ -28,6 +28,8 @@ package org.logicng.formulas; +import static org.assertj.core.api.Assertions.assertThat; + import org.junit.jupiter.api.Test; import org.logicng.formulas.cache.FunctionCacheEntry; import org.logicng.formulas.cache.PredicateCacheEntry; @@ -36,8 +38,6 @@ import java.util.Arrays; import java.util.List; -import static org.assertj.core.api.Assertions.assertThat; - /** * Unit tests for the package formulas.cache. * @version 2.0.0 diff --git a/src/test/java/org/logicng/formulas/ExtendedFormulaFactoryTest.java b/src/test/java/org/logicng/formulas/ExtendedFormulaFactoryTest.java index c63fa1b5..1da106cb 100644 --- a/src/test/java/org/logicng/formulas/ExtendedFormulaFactoryTest.java +++ b/src/test/java/org/logicng/formulas/ExtendedFormulaFactoryTest.java @@ -28,6 +28,10 @@ package org.logicng.formulas; +import static org.assertj.core.api.Assertions.assertThat; +import static org.assertj.core.api.Assertions.assertThatThrownBy; +import static org.assertj.core.data.MapEntry.entry; + import org.assertj.core.api.SoftAssertions; import org.junit.jupiter.api.Test; import org.logicng.LongRunningTag; @@ -39,7 +43,6 @@ import org.logicng.transformations.cnf.CNFFactorization; import org.logicng.transformations.cnf.PlaistedGreenbaumTransformation; import org.logicng.transformations.dnf.DNFFactorization; -import sun.awt.image.ImageWatched; import java.util.ArrayList; import java.util.HashSet; @@ -48,10 +51,6 @@ import java.util.List; import java.util.TreeMap; -import static org.assertj.core.api.Assertions.assertThat; -import static org.assertj.core.api.Assertions.assertThatThrownBy; -import static org.assertj.core.data.MapEntry.entry; - /** * Unit tests for the class {@link ExtendedFormulaFactory}. * @version 2.0.0 @@ -63,7 +62,7 @@ public class ExtendedFormulaFactoryTest { public void testShrinkMapWithWrongArguments() { assertThatThrownBy(() -> ExtendedFormulaFactory.shrinkMap(new TreeMap<>(), 4)) .isInstanceOf(IllegalStateException.class) - .hasMessage("Cannot shrink a map which is not of type LinkedHashMap"); + .hasMessage("Cannot shrink a map which is not of type LinkedHashMap"); assertThatThrownBy(() -> ExtendedFormulaFactory.shrinkMap(new LinkedHashMap<>(), 4)) .isInstanceOf(IllegalStateException.class) .hasMessage("Cannot shrink a map of size 0 to new size 4"); diff --git a/src/test/java/org/logicng/formulas/FTypeTest.java b/src/test/java/org/logicng/formulas/FTypeTest.java index 5aece022..439d9a40 100644 --- a/src/test/java/org/logicng/formulas/FTypeTest.java +++ b/src/test/java/org/logicng/formulas/FTypeTest.java @@ -1,10 +1,38 @@ -package org.logicng.formulas; +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// -import org.junit.jupiter.api.Test; +package org.logicng.formulas; import static org.assertj.core.api.Assertions.assertThat; import static org.junit.jupiter.api.Assertions.assertThrows; +import org.junit.jupiter.api.Test; + /** * Unit tests for formula types. * @version 2.0.0 diff --git a/src/test/java/org/logicng/formulas/FormulaFactoryWithoutContradictionCheckTest.java b/src/test/java/org/logicng/formulas/FormulaFactoryWithoutContradictionCheckTest.java index 34ae8fba..a3798ca4 100644 --- a/src/test/java/org/logicng/formulas/FormulaFactoryWithoutContradictionCheckTest.java +++ b/src/test/java/org/logicng/formulas/FormulaFactoryWithoutContradictionCheckTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.formulas; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/formulas/FormulaMergeTest.java b/src/test/java/org/logicng/formulas/FormulaMergeTest.java index 64e088da..983ab1bb 100644 --- a/src/test/java/org/logicng/formulas/FormulaMergeTest.java +++ b/src/test/java/org/logicng/formulas/FormulaMergeTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.formulas; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/formulas/NNFTest.java b/src/test/java/org/logicng/formulas/NNFTest.java index b50b5221..c86a7af9 100644 --- a/src/test/java/org/logicng/formulas/NNFTest.java +++ b/src/test/java/org/logicng/formulas/NNFTest.java @@ -25,6 +25,7 @@ // permissions and limitations under the License. // // // /////////////////////////////////////////////////////////////////////////// + package org.logicng.formulas; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/functions/FormulaDepthFunctionTest.java b/src/test/java/org/logicng/functions/FormulaDepthFunctionTest.java index abc742f9..791e3b42 100644 --- a/src/test/java/org/logicng/functions/FormulaDepthFunctionTest.java +++ b/src/test/java/org/logicng/functions/FormulaDepthFunctionTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.functions; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/functions/MinimumPrimeImplicantTest.java b/src/test/java/org/logicng/functions/MinimumPrimeImplicantTest.java index 6194e9c9..b507671d 100644 --- a/src/test/java/org/logicng/functions/MinimumPrimeImplicantTest.java +++ b/src/test/java/org/logicng/functions/MinimumPrimeImplicantTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.functions; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/graphs/generators/ConstraintGraphGeneratorTest.java b/src/test/java/org/logicng/graphs/generators/ConstraintGraphGeneratorTest.java index 5f492bcd..b247386b 100644 --- a/src/test/java/org/logicng/graphs/generators/ConstraintGraphGeneratorTest.java +++ b/src/test/java/org/logicng/graphs/generators/ConstraintGraphGeneratorTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.graphs.generators; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/handlers/NumberOfNodesBDDHandlerTest.java b/src/test/java/org/logicng/handlers/NumberOfNodesBDDHandlerTest.java index 7174b2fb..0b6a4b50 100644 --- a/src/test/java/org/logicng/handlers/NumberOfNodesBDDHandlerTest.java +++ b/src/test/java/org/logicng/handlers/NumberOfNodesBDDHandlerTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.handlers; import static org.assertj.core.api.Assertions.assertThatThrownBy; diff --git a/src/test/java/org/logicng/io/readers/DimacsReaderTest.java b/src/test/java/org/logicng/io/readers/DimacsReaderTest.java index 711dacea..aed47526 100644 --- a/src/test/java/org/logicng/io/readers/DimacsReaderTest.java +++ b/src/test/java/org/logicng/io/readers/DimacsReaderTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.io.readers; import static org.assertj.core.api.AssertionsForClassTypes.assertThatThrownBy; diff --git a/src/test/java/org/logicng/knowledgecompilation/bdds/BDDLowLevelTest.java b/src/test/java/org/logicng/knowledgecompilation/bdds/BDDLowLevelTest.java index 51ed5a0c..4240d0a1 100644 --- a/src/test/java/org/logicng/knowledgecompilation/bdds/BDDLowLevelTest.java +++ b/src/test/java/org/logicng/knowledgecompilation/bdds/BDDLowLevelTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.knowledgecompilation.bdds; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/knowledgecompilation/bdds/BDDReorderingTest.java b/src/test/java/org/logicng/knowledgecompilation/bdds/BDDReorderingTest.java index ea3ebc08..2da86efa 100644 --- a/src/test/java/org/logicng/knowledgecompilation/bdds/BDDReorderingTest.java +++ b/src/test/java/org/logicng/knowledgecompilation/bdds/BDDReorderingTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.knowledgecompilation.bdds; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDPrimeTest.java b/src/test/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDPrimeTest.java index 3779ff05..08ae44d7 100644 --- a/src/test/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDPrimeTest.java +++ b/src/test/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDPrimeTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.knowledgecompilation.bdds.jbuddy; import static org.assertj.core.api.AssertionsForInterfaceTypes.assertThat; @@ -12,4 +40,4 @@ public void testNumberOfBits() { assertThat(BDDPrime.numberOfBits(1)).isEqualTo(1); } -} \ No newline at end of file +} diff --git a/src/test/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDVerification.java b/src/test/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDVerification.java index 41f05701..adb58934 100644 --- a/src/test/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDVerification.java +++ b/src/test/java/org/logicng/knowledgecompilation/bdds/jbuddy/BDDVerification.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.knowledgecompilation.bdds.jbuddy; public class BDDVerification { diff --git a/src/test/java/org/logicng/knowledgecompilation/dnnf/DnnfCompilerTest.java b/src/test/java/org/logicng/knowledgecompilation/dnnf/DnnfCompilerTest.java index 6f1d234a..d539e8da 100644 --- a/src/test/java/org/logicng/knowledgecompilation/dnnf/DnnfCompilerTest.java +++ b/src/test/java/org/logicng/knowledgecompilation/dnnf/DnnfCompilerTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.knowledgecompilation.dnnf; import static org.assertj.core.api.Assertions.assertThat; @@ -23,8 +51,8 @@ import org.logicng.knowledgecompilation.bdds.BDDFactory; import org.logicng.knowledgecompilation.bdds.jbuddy.BDDKernel; import org.logicng.knowledgecompilation.bdds.orderings.ForceOrdering; -import org.logicng.knowledgecompilation.dnnf.datastructures.DNNF; -import org.logicng.knowledgecompilation.dnnf.functions.DNNFModelCountFunction; +import org.logicng.knowledgecompilation.dnnf.datastructures.Dnnf; +import org.logicng.knowledgecompilation.dnnf.functions.DnnfModelCountFunction; import org.logicng.predicates.satisfiability.TautologyPredicate; import org.logicng.transformations.cnf.CNFFactorization; @@ -35,7 +63,7 @@ import java.util.Set; /** - * Unit Tests for the class {@link DNNFCompiler}. + * Unit Tests for the class {@link DnnfCompiler}. * @version 2.0.0 * @since 2.0.0 */ @@ -82,7 +110,7 @@ public void testLargeFormulas() throws IOException { @Test public void testDnnfProperties() throws ParserException { - final DNNF dnnf = new DNNFFactory().compile(this.parser.parse("a | ((b & ~c) | (c & (~d | ~a & b)) & e)")); + final Dnnf dnnf = new DnnfFactory().compile(this.parser.parse("a | ((b & ~c) | (c & (~d | ~a & b)) & e)")); assertThat(dnnf.getOriginalVariables()).extracting(Variable::name).containsExactlyInAnyOrder("a", "b", "c", "d", "e"); } @@ -99,9 +127,9 @@ public void testLargeFormula() throws IOException, ParserException { final FormulaFactory f = new FormulaFactory(); f.putConfiguration(CCConfig.builder().amoEncoding(CCConfig.AMO_ENCODER.PURE).build()); final Formula parsed = FormulaReader.readPseudoBooleanFormula("src/test/resources/formulas/formula1.txt", f); - final DNNFFactory dnnfFactory = new DNNFFactory(); - DNNF dnnf = dnnfFactory.compile(parsed); - final BigInteger dnnfCount = dnnf.execute(DNNFModelCountFunction.get()); + final DnnfFactory dnnfFactory = new DnnfFactory(); + Dnnf dnnf = dnnfFactory.compile(parsed); + final BigInteger dnnfCount = dnnf.execute(DnnfModelCountFunction.get()); final List formulas = new ArrayList<>(); final List originalFormulas = new ArrayList<>(); for (final Formula formula : parsed) { @@ -118,15 +146,15 @@ public void testLargeFormula() throws IOException, ParserException { BigInteger multipliedCount = BigInteger.ONE; for (final List component : split) { dnnf = dnnfFactory.compile(f.and(component)); - multipliedCount = multipliedCount.multiply(dnnf.execute(DNNFModelCountFunction.get())); + multipliedCount = multipliedCount.multiply(dnnf.execute(DnnfModelCountFunction.get())); } assertThat(dnnfCount).isEqualTo(multipliedCount); } private void testFormula(final Formula formula, final boolean withEquivalence) { - final DNNFFactory dnnfFactory = new DNNFFactory(); - final DNNF dnnf = dnnfFactory.compile(formula); - final BigInteger dnnfCount = dnnf.execute(DNNFModelCountFunction.get()); + final DnnfFactory dnnfFactory = new DnnfFactory(); + final Dnnf dnnf = dnnfFactory.compile(formula); + final BigInteger dnnfCount = dnnf.execute(DnnfModelCountFunction.get()); if (withEquivalence) { final Formula equivalence = formula.factory().equivalence(formula, dnnf.formula()); assertThat(equivalence.holds(new TautologyPredicate(formula.factory()))).isTrue(); diff --git a/src/test/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTreeNodeTest.java b/src/test/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTreeNodeTest.java index bed49746..48029cc5 100644 --- a/src/test/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTreeNodeTest.java +++ b/src/test/java/org/logicng/knowledgecompilation/dnnf/datastructures/dtree/DTreeNodeTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.knowledgecompilation.dnnf.datastructures.dtree; import static org.assertj.core.api.AssertionsForInterfaceTypes.assertThat; diff --git a/src/test/java/org/logicng/modelcounting/ModelCounterTest.java b/src/test/java/org/logicng/modelcounting/ModelCounterTest.java index 665097d6..62178611 100644 --- a/src/test/java/org/logicng/modelcounting/ModelCounterTest.java +++ b/src/test/java/org/logicng/modelcounting/ModelCounterTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.modelcounting; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/np/SetCoverTest.java b/src/test/java/org/logicng/np/SetCoverTest.java index ac8d857f..c593ae1e 100644 --- a/src/test/java/org/logicng/np/SetCoverTest.java +++ b/src/test/java/org/logicng/np/SetCoverTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.np; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/predicates/EvaluatesToConstantPredicateTest.java b/src/test/java/org/logicng/predicates/EvaluatesToConstantPredicateTest.java index aac93f44..d68d738f 100644 --- a/src/test/java/org/logicng/predicates/EvaluatesToConstantPredicateTest.java +++ b/src/test/java/org/logicng/predicates/EvaluatesToConstantPredicateTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.predicates; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/primecomputation/PrimeCompilerTest.java b/src/test/java/org/logicng/primecomputation/PrimeCompilerTest.java index c36e928c..0b6252fc 100644 --- a/src/test/java/org/logicng/primecomputation/PrimeCompilerTest.java +++ b/src/test/java/org/logicng/primecomputation/PrimeCompilerTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.primecomputation; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/primecomputation/PrimeImplicantReductionTest.java b/src/test/java/org/logicng/primecomputation/PrimeImplicantReductionTest.java index e13c2485..beada488 100644 --- a/src/test/java/org/logicng/primecomputation/PrimeImplicantReductionTest.java +++ b/src/test/java/org/logicng/primecomputation/PrimeImplicantReductionTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.primecomputation; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/primecomputation/PrimeImplicateReductionTest.java b/src/test/java/org/logicng/primecomputation/PrimeImplicateReductionTest.java index 591939c5..8bcfadf4 100644 --- a/src/test/java/org/logicng/primecomputation/PrimeImplicateReductionTest.java +++ b/src/test/java/org/logicng/primecomputation/PrimeImplicateReductionTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.primecomputation; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/primecomputation/PrimeResultTest.java b/src/test/java/org/logicng/primecomputation/PrimeResultTest.java index fd7839ed..3697e7a1 100644 --- a/src/test/java/org/logicng/primecomputation/PrimeResultTest.java +++ b/src/test/java/org/logicng/primecomputation/PrimeResultTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.primecomputation; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/propositions/ExtendedPropositionTest.java b/src/test/java/org/logicng/propositions/ExtendedPropositionTest.java index 10481108..a8df5f7e 100644 --- a/src/test/java/org/logicng/propositions/ExtendedPropositionTest.java +++ b/src/test/java/org/logicng/propositions/ExtendedPropositionTest.java @@ -28,6 +28,8 @@ package org.logicng.propositions; +import static org.assertj.core.api.Assertions.assertThat; + import org.junit.jupiter.api.Test; import org.logicng.formulas.FormulaFactory; import org.logicng.io.parsers.ParserException; @@ -35,8 +37,6 @@ import java.util.Objects; -import static org.assertj.core.api.Assertions.assertThat; - /** * Unit tests for {@link ExtendedProposition}. * @version 2.0.0 diff --git a/src/test/java/org/logicng/pseudobooleans/PBEncoderTest.java b/src/test/java/org/logicng/pseudobooleans/PBEncoderTest.java index 17345244..d6ca75d8 100644 --- a/src/test/java/org/logicng/pseudobooleans/PBEncoderTest.java +++ b/src/test/java/org/logicng/pseudobooleans/PBEncoderTest.java @@ -27,6 +27,8 @@ /////////////////////////////////////////////////////////////////////////// package org.logicng.pseudobooleans; +import static org.assertj.core.api.Assertions.assertThat; + import org.junit.jupiter.api.Test; import org.logicng.LogicNGTest; import org.logicng.cardinalityconstraints.CCConfig; @@ -45,8 +47,6 @@ import java.util.Arrays; import java.util.List; -import static org.assertj.core.api.Assertions.assertThat; - /** * Unit tests for {@link PBEncoder}. * @version 2.0.0 diff --git a/src/test/java/org/logicng/pseudobooleans/PBSolvingTest.java b/src/test/java/org/logicng/pseudobooleans/PBSolvingTest.java index 55dfa1ec..69662b36 100644 --- a/src/test/java/org/logicng/pseudobooleans/PBSolvingTest.java +++ b/src/test/java/org/logicng/pseudobooleans/PBSolvingTest.java @@ -28,6 +28,8 @@ package org.logicng.pseudobooleans; +import static org.assertj.core.api.Assertions.assertThat; + import org.junit.jupiter.api.Test; import org.logicng.LogicNGTest; import org.logicng.datastructures.Assignment; @@ -41,8 +43,6 @@ import java.util.List; -import static org.assertj.core.api.Assertions.assertThat; - /** * Test the solving (via encoding) of pseudo-Boolean constraints. * @version 2.0.0 diff --git a/src/test/java/org/logicng/solvers/ModelTest.java b/src/test/java/org/logicng/solvers/ModelTest.java index 834a4ec2..b3b4099d 100644 --- a/src/test/java/org/logicng/solvers/ModelTest.java +++ b/src/test/java/org/logicng/solvers/ModelTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.solvers; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/solvers/functions/BackboneFunctionTest.java b/src/test/java/org/logicng/solvers/functions/BackboneFunctionTest.java index ee27f4ac..c0c0901e 100644 --- a/src/test/java/org/logicng/solvers/functions/BackboneFunctionTest.java +++ b/src/test/java/org/logicng/solvers/functions/BackboneFunctionTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.solvers.functions; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/solvers/functions/OptimizationFunctionTest.java b/src/test/java/org/logicng/solvers/functions/OptimizationFunctionTest.java index c96e0595..c2e37efc 100644 --- a/src/test/java/org/logicng/solvers/functions/OptimizationFunctionTest.java +++ b/src/test/java/org/logicng/solvers/functions/OptimizationFunctionTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.solvers.functions; import static java.util.stream.Collectors.toCollection; diff --git a/src/test/java/org/logicng/solvers/functions/UnsatCoreFunctionTest.java b/src/test/java/org/logicng/solvers/functions/UnsatCoreFunctionTest.java index 721557ab..a7cb24de 100644 --- a/src/test/java/org/logicng/solvers/functions/UnsatCoreFunctionTest.java +++ b/src/test/java/org/logicng/solvers/functions/UnsatCoreFunctionTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.solvers.functions; import static org.assertj.core.api.AssertionsForClassTypes.assertThatThrownBy; @@ -48,4 +76,4 @@ public void testExceptionalBehavior() { }).isInstanceOf(IllegalStateException.class) .hasMessage("Cannot compute an unsat core for a computation with assumptions."); } -} \ No newline at end of file +} diff --git a/src/test/java/org/logicng/solvers/sat/GlucoseSyrupTest.java b/src/test/java/org/logicng/solvers/sat/GlucoseSyrupTest.java index 7dfc1566..abf904cf 100644 --- a/src/test/java/org/logicng/solvers/sat/GlucoseSyrupTest.java +++ b/src/test/java/org/logicng/solvers/sat/GlucoseSyrupTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.solvers.sat; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/transformations/AnonymizerTest.java b/src/test/java/org/logicng/transformations/AnonymizerTest.java index 308927b1..c4108dd1 100644 --- a/src/test/java/org/logicng/transformations/AnonymizerTest.java +++ b/src/test/java/org/logicng/transformations/AnonymizerTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.transformations; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/transformations/LiteralSubstitutionTest.java b/src/test/java/org/logicng/transformations/LiteralSubstitutionTest.java index d16221bb..5955541d 100644 --- a/src/test/java/org/logicng/transformations/LiteralSubstitutionTest.java +++ b/src/test/java/org/logicng/transformations/LiteralSubstitutionTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.transformations; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/transformations/cnf/CNFEncoderTest.java b/src/test/java/org/logicng/transformations/cnf/CNFEncoderTest.java index 886b5ac1..55f3fcbb 100644 --- a/src/test/java/org/logicng/transformations/cnf/CNFEncoderTest.java +++ b/src/test/java/org/logicng/transformations/cnf/CNFEncoderTest.java @@ -28,6 +28,9 @@ package org.logicng.transformations.cnf; +import static org.assertj.core.api.Assertions.assertThat; +import static org.assertj.core.api.Assertions.assertThatThrownBy; + import org.junit.jupiter.api.Test; import org.logicng.datastructures.Assignment; import org.logicng.formulas.Formula; @@ -42,9 +45,6 @@ import java.util.List; import java.util.SortedSet; -import static org.assertj.core.api.Assertions.assertThat; -import static org.assertj.core.api.Assertions.assertThatThrownBy; - /** * Unit tests for the class {@link CNFEncoder}. * @version 2.0.0 diff --git a/src/test/java/org/logicng/transformations/cnf/CNFSubsumptionTest.java b/src/test/java/org/logicng/transformations/cnf/CNFSubsumptionTest.java index a3813f34..addff6d1 100644 --- a/src/test/java/org/logicng/transformations/cnf/CNFSubsumptionTest.java +++ b/src/test/java/org/logicng/transformations/cnf/CNFSubsumptionTest.java @@ -28,6 +28,9 @@ package org.logicng.transformations.cnf; +import static org.assertj.core.api.Assertions.assertThat; +import static org.assertj.core.api.Assertions.assertThatThrownBy; + import org.junit.jupiter.api.Test; import org.logicng.LongRunningTag; import org.logicng.formulas.Formula; @@ -39,9 +42,6 @@ import java.io.IOException; -import static org.assertj.core.api.Assertions.assertThat; -import static org.assertj.core.api.Assertions.assertThatThrownBy; - /** * Unit tests for {@link CNFSubsumption}. * @version 2.0.0 diff --git a/src/test/java/org/logicng/transformations/cnf/CnfMethodComparisonTest.java b/src/test/java/org/logicng/transformations/cnf/CnfMethodComparisonTest.java index 8f7c0539..ab89c241 100644 --- a/src/test/java/org/logicng/transformations/cnf/CnfMethodComparisonTest.java +++ b/src/test/java/org/logicng/transformations/cnf/CnfMethodComparisonTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.transformations.cnf; import static org.assertj.core.api.AssertionsForClassTypes.assertThat; diff --git a/src/test/java/org/logicng/transformations/cnf/PlaistedGreenbaumTransformationSolverTest.java b/src/test/java/org/logicng/transformations/cnf/PlaistedGreenbaumTransformationSolverTest.java index 8709112b..afcc1678 100644 --- a/src/test/java/org/logicng/transformations/cnf/PlaistedGreenbaumTransformationSolverTest.java +++ b/src/test/java/org/logicng/transformations/cnf/PlaistedGreenbaumTransformationSolverTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.transformations.cnf; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/transformations/qmc/QuineMcCluskeyTest.java b/src/test/java/org/logicng/transformations/qmc/QuineMcCluskeyTest.java index 2bc408ac..42c10969 100644 --- a/src/test/java/org/logicng/transformations/qmc/QuineMcCluskeyTest.java +++ b/src/test/java/org/logicng/transformations/qmc/QuineMcCluskeyTest.java @@ -28,6 +28,13 @@ package org.logicng.transformations.qmc; +import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.transformations.qmc.QuineMcCluskeyAlgorithm.chooseSatBased; +import static org.logicng.transformations.qmc.QuineMcCluskeyAlgorithm.combineInTermClasses; +import static org.logicng.transformations.qmc.QuineMcCluskeyAlgorithm.computePrimeImplicants; +import static org.logicng.transformations.qmc.QuineMcCluskeyAlgorithm.convertToTerm; +import static org.logicng.transformations.qmc.QuineMcCluskeyAlgorithm.generateInitialTermClasses; + import org.junit.jupiter.api.Test; import org.logicng.datastructures.Assignment; import org.logicng.datastructures.Tristate; @@ -53,13 +60,6 @@ import java.util.List; import java.util.SortedMap; -import static org.assertj.core.api.Assertions.assertThat; -import static org.logicng.transformations.qmc.QuineMcCluskeyAlgorithm.chooseSatBased; -import static org.logicng.transformations.qmc.QuineMcCluskeyAlgorithm.combineInTermClasses; -import static org.logicng.transformations.qmc.QuineMcCluskeyAlgorithm.computePrimeImplicants; -import static org.logicng.transformations.qmc.QuineMcCluskeyAlgorithm.convertToTerm; -import static org.logicng.transformations.qmc.QuineMcCluskeyAlgorithm.generateInitialTermClasses; - /** * Unit tests for {@link QuineMcCluskeyAlgorithm}. * @version 2.0.0 diff --git a/src/test/java/org/logicng/transformations/qmc/TermTableTest.java b/src/test/java/org/logicng/transformations/qmc/TermTableTest.java index 6ca6ac70..26623391 100644 --- a/src/test/java/org/logicng/transformations/qmc/TermTableTest.java +++ b/src/test/java/org/logicng/transformations/qmc/TermTableTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.transformations.qmc; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/transformations/qmc/TermTest.java b/src/test/java/org/logicng/transformations/qmc/TermTest.java index 5f14845d..f944e0f1 100644 --- a/src/test/java/org/logicng/transformations/qmc/TermTest.java +++ b/src/test/java/org/logicng/transformations/qmc/TermTest.java @@ -1,5 +1,38 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.transformations.qmc; +import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.datastructures.Tristate.FALSE; +import static org.logicng.datastructures.Tristate.TRUE; +import static org.logicng.datastructures.Tristate.UNDEF; + import org.junit.jupiter.api.Test; import org.logicng.datastructures.Tristate; import org.logicng.formulas.Formula; @@ -12,11 +45,6 @@ import java.util.Collections; import java.util.List; -import static org.assertj.core.api.Assertions.assertThat; -import static org.logicng.datastructures.Tristate.FALSE; -import static org.logicng.datastructures.Tristate.TRUE; -import static org.logicng.datastructures.Tristate.UNDEF; - /** * Unit tests for {@link Term}. * @version 2.0.0 diff --git a/src/test/java/org/logicng/transformations/simplification/SimplifierTest.java b/src/test/java/org/logicng/transformations/simplification/SimplifierTest.java index 710d28a4..184f7536 100644 --- a/src/test/java/org/logicng/transformations/simplification/SimplifierTest.java +++ b/src/test/java/org/logicng/transformations/simplification/SimplifierTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.transformations.simplification; import static org.assertj.core.api.Assertions.assertThat; diff --git a/src/test/java/org/logicng/util/CollectionHelperTest.java b/src/test/java/org/logicng/util/CollectionHelperTest.java index 849150a8..f98d0d22 100644 --- a/src/test/java/org/logicng/util/CollectionHelperTest.java +++ b/src/test/java/org/logicng/util/CollectionHelperTest.java @@ -1,5 +1,37 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.util; +import static org.assertj.core.api.Assertions.assertThat; +import static org.logicng.util.CollectionHelper.nullOrEmpty; +import static org.logicng.util.CollectionHelper.nullSafe; + import org.junit.jupiter.api.Test; import java.util.ArrayList; @@ -9,10 +41,6 @@ import java.util.SortedSet; import java.util.TreeSet; -import static org.assertj.core.api.Assertions.assertThat; -import static org.logicng.util.CollectionHelper.nullOrEmpty; -import static org.logicng.util.CollectionHelper.nullSafe; - /** * Unit tests for {@link CollectionHelper} * @version 2.0.0 diff --git a/src/test/java/org/logicng/util/FormulaRandomizerTest.java b/src/test/java/org/logicng/util/FormulaRandomizerTest.java index c6cd50fd..d9eb4faf 100644 --- a/src/test/java/org/logicng/util/FormulaRandomizerTest.java +++ b/src/test/java/org/logicng/util/FormulaRandomizerTest.java @@ -1,3 +1,31 @@ +/////////////////////////////////////////////////////////////////////////// +// __ _ _ ________ // +// / / ____ ____ _(_)____/ | / / ____/ // +// / / / __ \/ __ `/ / ___/ |/ / / __ // +// / /___/ /_/ / /_/ / / /__/ /| / /_/ / // +// /_____/\____/\__, /_/\___/_/ |_/\____/ // +// /____/ // +// // +// The Next Generation Logic Library // +// // +/////////////////////////////////////////////////////////////////////////// +// // +// Copyright 2015-20xx Christoph Zengler // +// // +// Licensed under the Apache License, Version 2.0 (the "License"); // +// you may not use this file except in compliance with the License. // +// You may obtain a copy of the License at // +// // +// http://www.apache.org/licenses/LICENSE-2.0 // +// // +// Unless required by applicable law or agreed to in writing, software // +// distributed under the License is distributed on an "AS IS" BASIS, // +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or // +// implied. See the License for the specific language governing // +// permissions and limitations under the License. // +// // +/////////////////////////////////////////////////////////////////////////// + package org.logicng.util; import static org.assertj.core.api.Assertions.assertThat;