From ec98568a0b55eed432004a80960e21ced60116f7 Mon Sep 17 00:00:00 2001 From: "P. Oscar Boykin" Date: Sat, 21 Feb 2026 20:20:02 -1000 Subject: [PATCH 1/6] Add minimal core subproject and move foundational utilities --- build.sbt | 19 ++++++++++++++++--- .../scala/ap/basetypes/HeapCollector.scala | 0 .../main/scala/ap/basetypes/IdealInt.scala | 0 .../main/scala/ap/basetypes/IdealRat.scala | 0 .../main/scala/ap/basetypes/LeftistHeap.scala | 0 .../main/scala/ap/basetypes/MultiSet.scala | 0 .../main/scala/ap/basetypes/SetTrie.scala | 0 .../src}/main/scala/ap/basetypes/Tree.scala | 0 .../main/scala/ap/basetypes/UnionFind.scala | 0 .../src}/main/scala/ap/util/CmdlParser.scala | 0 .../main/scala/ap/util/Combinatorics.scala | 0 .../src}/main/scala/ap/util/CountIt.scala | 0 .../src}/main/scala/ap/util/Debug.scala | 0 .../src}/main/scala/ap/util/Dijkstra.scala | 0 .../main/scala/ap/util/FastImmutableMap.scala | 0 .../src}/main/scala/ap/util/FilterIt.scala | 0 .../src}/main/scala/ap/util/LRUCache.scala | 0 .../scala/ap/util/LazyIndexedSeqConcat.scala | 0 .../scala/ap/util/LazyIndexedSeqSlice.scala | 0 .../main/scala/ap/util/LazyMappedMap.scala | 0 .../main/scala/ap/util/LazyMappedSet.scala | 0 .../src}/main/scala/ap/util/Logic.scala | 0 .../src}/main/scala/ap/util/POGraph.scala | 0 .../main/scala/ap/util/PeekIterator.scala | 0 .../src}/main/scala/ap/util/PlainRange.scala | 0 .../ap/util/PriorityQueueWithIterators.scala | 0 .../scala/ap/util/RuntimeStatistics.scala | 0 .../src}/main/scala/ap/util/Seqs.scala | 0 .../src}/main/scala/ap/util/Tarjan.scala | 0 .../src}/main/scala/ap/util/Timeout.scala | 0 .../src}/main/scala/ap/util/UnionMap.scala | 0 .../src}/main/scala/ap/util/UnionSet.scala | 0 32 files changed, 16 insertions(+), 3 deletions(-) rename {src => core/src}/main/scala/ap/basetypes/HeapCollector.scala (100%) rename {src => core/src}/main/scala/ap/basetypes/IdealInt.scala (100%) rename {src => core/src}/main/scala/ap/basetypes/IdealRat.scala (100%) rename {src => core/src}/main/scala/ap/basetypes/LeftistHeap.scala (100%) rename {src => core/src}/main/scala/ap/basetypes/MultiSet.scala (100%) rename {src => core/src}/main/scala/ap/basetypes/SetTrie.scala (100%) rename {src => core/src}/main/scala/ap/basetypes/Tree.scala (100%) rename {src => core/src}/main/scala/ap/basetypes/UnionFind.scala (100%) rename {src => core/src}/main/scala/ap/util/CmdlParser.scala (100%) rename {src => core/src}/main/scala/ap/util/Combinatorics.scala (100%) rename {src => core/src}/main/scala/ap/util/CountIt.scala (100%) rename {src => core/src}/main/scala/ap/util/Debug.scala (100%) rename {src => core/src}/main/scala/ap/util/Dijkstra.scala (100%) rename {src => core/src}/main/scala/ap/util/FastImmutableMap.scala (100%) rename {src => core/src}/main/scala/ap/util/FilterIt.scala (100%) rename {src => core/src}/main/scala/ap/util/LRUCache.scala (100%) rename {src => core/src}/main/scala/ap/util/LazyIndexedSeqConcat.scala (100%) rename {src => core/src}/main/scala/ap/util/LazyIndexedSeqSlice.scala (100%) rename {src => core/src}/main/scala/ap/util/LazyMappedMap.scala (100%) rename {src => core/src}/main/scala/ap/util/LazyMappedSet.scala (100%) rename {src => core/src}/main/scala/ap/util/Logic.scala (100%) rename {src => core/src}/main/scala/ap/util/POGraph.scala (100%) rename {src => core/src}/main/scala/ap/util/PeekIterator.scala (100%) rename {src => core/src}/main/scala/ap/util/PlainRange.scala (100%) rename {src => core/src}/main/scala/ap/util/PriorityQueueWithIterators.scala (100%) rename {src => core/src}/main/scala/ap/util/RuntimeStatistics.scala (100%) rename {src => core/src}/main/scala/ap/util/Seqs.scala (100%) rename {src => core/src}/main/scala/ap/util/Tarjan.scala (100%) rename {src => core/src}/main/scala/ap/util/Timeout.scala (100%) rename {src => core/src}/main/scala/ap/util/UnionMap.scala (100%) rename {src => core/src}/main/scala/ap/util/UnionSet.scala (100%) diff --git a/build.sbt b/build.sbt index 91eb58569..9b8182b93 100644 --- a/build.sbt +++ b/build.sbt @@ -90,12 +90,26 @@ lazy val smtParser = (project in file("smt-parser")). ). disablePlugins(AssemblyPlugin) +lazy val core = (project in file("core")). + settings(commonSettings: _*). + settings( + name := "Princess-core", + Compile / scalacOptions ++= + List("-feature", + "-language:implicitConversions,postfixOps,reflectiveCalls"), + scalacOptions += (scalaVersion map { sv => sv match { + case "2.11.12" => "-optimise" + case "2.12.20" => "-opt:_" + }}).value + ). + disablePlugins(AssemblyPlugin) + // Actual project lazy val root = (project in file(".")). enablePlugins(NativeImagePlugin). - aggregate(parser, smtParser). - dependsOn(parser, smtParser). + aggregate(core, parser, smtParser). + dependsOn(core, parser, smtParser). settings(commonSettings: _*). // settings( @@ -129,4 +143,3 @@ lazy val root = (project in file(".")). nativeImageAgentMerge := true ) - diff --git a/src/main/scala/ap/basetypes/HeapCollector.scala b/core/src/main/scala/ap/basetypes/HeapCollector.scala similarity index 100% rename from src/main/scala/ap/basetypes/HeapCollector.scala rename to core/src/main/scala/ap/basetypes/HeapCollector.scala diff --git a/src/main/scala/ap/basetypes/IdealInt.scala b/core/src/main/scala/ap/basetypes/IdealInt.scala similarity index 100% rename from src/main/scala/ap/basetypes/IdealInt.scala rename to core/src/main/scala/ap/basetypes/IdealInt.scala diff --git a/src/main/scala/ap/basetypes/IdealRat.scala b/core/src/main/scala/ap/basetypes/IdealRat.scala similarity index 100% rename from src/main/scala/ap/basetypes/IdealRat.scala rename to core/src/main/scala/ap/basetypes/IdealRat.scala diff --git a/src/main/scala/ap/basetypes/LeftistHeap.scala b/core/src/main/scala/ap/basetypes/LeftistHeap.scala similarity index 100% rename from src/main/scala/ap/basetypes/LeftistHeap.scala rename to core/src/main/scala/ap/basetypes/LeftistHeap.scala diff --git a/src/main/scala/ap/basetypes/MultiSet.scala b/core/src/main/scala/ap/basetypes/MultiSet.scala similarity index 100% rename from src/main/scala/ap/basetypes/MultiSet.scala rename to core/src/main/scala/ap/basetypes/MultiSet.scala diff --git a/src/main/scala/ap/basetypes/SetTrie.scala b/core/src/main/scala/ap/basetypes/SetTrie.scala similarity index 100% rename from src/main/scala/ap/basetypes/SetTrie.scala rename to core/src/main/scala/ap/basetypes/SetTrie.scala diff --git a/src/main/scala/ap/basetypes/Tree.scala b/core/src/main/scala/ap/basetypes/Tree.scala similarity index 100% rename from src/main/scala/ap/basetypes/Tree.scala rename to core/src/main/scala/ap/basetypes/Tree.scala diff --git a/src/main/scala/ap/basetypes/UnionFind.scala b/core/src/main/scala/ap/basetypes/UnionFind.scala similarity index 100% rename from src/main/scala/ap/basetypes/UnionFind.scala rename to core/src/main/scala/ap/basetypes/UnionFind.scala diff --git a/src/main/scala/ap/util/CmdlParser.scala b/core/src/main/scala/ap/util/CmdlParser.scala similarity index 100% rename from src/main/scala/ap/util/CmdlParser.scala rename to core/src/main/scala/ap/util/CmdlParser.scala diff --git a/src/main/scala/ap/util/Combinatorics.scala b/core/src/main/scala/ap/util/Combinatorics.scala similarity index 100% rename from src/main/scala/ap/util/Combinatorics.scala rename to core/src/main/scala/ap/util/Combinatorics.scala diff --git a/src/main/scala/ap/util/CountIt.scala b/core/src/main/scala/ap/util/CountIt.scala similarity index 100% rename from src/main/scala/ap/util/CountIt.scala rename to core/src/main/scala/ap/util/CountIt.scala diff --git a/src/main/scala/ap/util/Debug.scala b/core/src/main/scala/ap/util/Debug.scala similarity index 100% rename from src/main/scala/ap/util/Debug.scala rename to core/src/main/scala/ap/util/Debug.scala diff --git a/src/main/scala/ap/util/Dijkstra.scala b/core/src/main/scala/ap/util/Dijkstra.scala similarity index 100% rename from src/main/scala/ap/util/Dijkstra.scala rename to core/src/main/scala/ap/util/Dijkstra.scala diff --git a/src/main/scala/ap/util/FastImmutableMap.scala b/core/src/main/scala/ap/util/FastImmutableMap.scala similarity index 100% rename from src/main/scala/ap/util/FastImmutableMap.scala rename to core/src/main/scala/ap/util/FastImmutableMap.scala diff --git a/src/main/scala/ap/util/FilterIt.scala b/core/src/main/scala/ap/util/FilterIt.scala similarity index 100% rename from src/main/scala/ap/util/FilterIt.scala rename to core/src/main/scala/ap/util/FilterIt.scala diff --git a/src/main/scala/ap/util/LRUCache.scala b/core/src/main/scala/ap/util/LRUCache.scala similarity index 100% rename from src/main/scala/ap/util/LRUCache.scala rename to core/src/main/scala/ap/util/LRUCache.scala diff --git a/src/main/scala/ap/util/LazyIndexedSeqConcat.scala b/core/src/main/scala/ap/util/LazyIndexedSeqConcat.scala similarity index 100% rename from src/main/scala/ap/util/LazyIndexedSeqConcat.scala rename to core/src/main/scala/ap/util/LazyIndexedSeqConcat.scala diff --git a/src/main/scala/ap/util/LazyIndexedSeqSlice.scala b/core/src/main/scala/ap/util/LazyIndexedSeqSlice.scala similarity index 100% rename from src/main/scala/ap/util/LazyIndexedSeqSlice.scala rename to core/src/main/scala/ap/util/LazyIndexedSeqSlice.scala diff --git a/src/main/scala/ap/util/LazyMappedMap.scala b/core/src/main/scala/ap/util/LazyMappedMap.scala similarity index 100% rename from src/main/scala/ap/util/LazyMappedMap.scala rename to core/src/main/scala/ap/util/LazyMappedMap.scala diff --git a/src/main/scala/ap/util/LazyMappedSet.scala b/core/src/main/scala/ap/util/LazyMappedSet.scala similarity index 100% rename from src/main/scala/ap/util/LazyMappedSet.scala rename to core/src/main/scala/ap/util/LazyMappedSet.scala diff --git a/src/main/scala/ap/util/Logic.scala b/core/src/main/scala/ap/util/Logic.scala similarity index 100% rename from src/main/scala/ap/util/Logic.scala rename to core/src/main/scala/ap/util/Logic.scala diff --git a/src/main/scala/ap/util/POGraph.scala b/core/src/main/scala/ap/util/POGraph.scala similarity index 100% rename from src/main/scala/ap/util/POGraph.scala rename to core/src/main/scala/ap/util/POGraph.scala diff --git a/src/main/scala/ap/util/PeekIterator.scala b/core/src/main/scala/ap/util/PeekIterator.scala similarity index 100% rename from src/main/scala/ap/util/PeekIterator.scala rename to core/src/main/scala/ap/util/PeekIterator.scala diff --git a/src/main/scala/ap/util/PlainRange.scala b/core/src/main/scala/ap/util/PlainRange.scala similarity index 100% rename from src/main/scala/ap/util/PlainRange.scala rename to core/src/main/scala/ap/util/PlainRange.scala diff --git a/src/main/scala/ap/util/PriorityQueueWithIterators.scala b/core/src/main/scala/ap/util/PriorityQueueWithIterators.scala similarity index 100% rename from src/main/scala/ap/util/PriorityQueueWithIterators.scala rename to core/src/main/scala/ap/util/PriorityQueueWithIterators.scala diff --git a/src/main/scala/ap/util/RuntimeStatistics.scala b/core/src/main/scala/ap/util/RuntimeStatistics.scala similarity index 100% rename from src/main/scala/ap/util/RuntimeStatistics.scala rename to core/src/main/scala/ap/util/RuntimeStatistics.scala diff --git a/src/main/scala/ap/util/Seqs.scala b/core/src/main/scala/ap/util/Seqs.scala similarity index 100% rename from src/main/scala/ap/util/Seqs.scala rename to core/src/main/scala/ap/util/Seqs.scala diff --git a/src/main/scala/ap/util/Tarjan.scala b/core/src/main/scala/ap/util/Tarjan.scala similarity index 100% rename from src/main/scala/ap/util/Tarjan.scala rename to core/src/main/scala/ap/util/Tarjan.scala diff --git a/src/main/scala/ap/util/Timeout.scala b/core/src/main/scala/ap/util/Timeout.scala similarity index 100% rename from src/main/scala/ap/util/Timeout.scala rename to core/src/main/scala/ap/util/Timeout.scala diff --git a/src/main/scala/ap/util/UnionMap.scala b/core/src/main/scala/ap/util/UnionMap.scala similarity index 100% rename from src/main/scala/ap/util/UnionMap.scala rename to core/src/main/scala/ap/util/UnionMap.scala diff --git a/src/main/scala/ap/util/UnionSet.scala b/core/src/main/scala/ap/util/UnionSet.scala similarity index 100% rename from src/main/scala/ap/util/UnionSet.scala rename to core/src/main/scala/ap/util/UnionSet.scala From ef013dd503512265f039a6858d25d5346b500ada Mon Sep 17 00:00:00 2001 From: "P. Oscar Boykin" Date: Sat, 21 Feb 2026 21:18:40 -1000 Subject: [PATCH 2/6] Checkpoint: minimal core split with theorem checks --- build.sbt | 2 + .../src}/main/scala/ap/PresburgerTools.scala | 0 {src => core/src}/main/scala/ap/Prover.scala | 0 .../src}/main/scala/ap/Signature.scala | 0 .../src}/main/scala/ap/algebra/Group.scala | 0 .../src}/main/scala/ap/algebra/Integers.scala | 0 .../src}/main/scala/ap/algebra/Ring.scala | 0 .../src}/main/scala/ap/algebra/package.scala | 0 .../src}/main/scala/ap/api/PartialModel.scala | 0 .../scala/ap/core/ImplicationChecker.scala | 23 + .../scala/ap/interpolants/BenchUtils.scala | 0 .../interpolants/InterpolantSimplifier.scala | 0 .../interpolants/InterpolationContext.scala | 0 .../scala/ap/interpolants/Interpolator.scala | 0 .../ap/interpolants/InterpolatorQE.scala | 0 .../ap/interpolants/PartialInterpolant.scala | 0 .../ap/interpolants/ProofSimplifier.scala | 0 .../src}/main/scala/ap/parameters/Param.scala | 0 .../main/scala/ap/parameters/Settings.scala | 0 .../scala/ap/parser/BooleanCompactifier.scala | 0 .../scala/ap/parser/CSIsatLineariser.scala | 0 .../main/scala/ap/parser/Environment.scala | 0 .../main/scala/ap/parser/EquivExpander.scala | 0 .../main/scala/ap/parser/EquivInliner.scala | 0 .../main/scala/ap/parser/ExMaxiscoper.scala | 0 .../scala/ap/parser/FunctionEncoder.scala | 0 .../ap/parser/FunctionPreprocessing.scala | 0 .../main/scala/ap/parser/IExpression.scala | 0 .../src}/main/scala/ap/parser/IFormula.scala | 0 .../src}/main/scala/ap/parser/ITerm.scala | 0 .../ap/parser/ImplicationCompressor.scala | 0 .../scala/ap/parser/InputAbsy2Internal.scala | 0 .../scala/ap/parser/InputAbsyVisitor.scala | 0 .../scala/ap/parser/Internal2InputAbsy.scala | 0 .../src}/main/scala/ap/parser/KBO.scala | 0 .../scala/ap/parser/Parser2InputAbsy.scala | 0 .../main/scala/ap/parser/PartExtractor.scala | 0 .../scala/ap/parser/PartialEvaluator.scala | 0 .../main/scala/ap/parser/Postprocessing.scala | 0 .../main/scala/ap/parser/Preprocessing.scala | 0 .../src}/main/scala/ap/parser/Rewriter.scala | 0 .../main/scala/ap/parser/SMTLineariser.scala | 27 +- .../scala/ap/parser/SMTParseableTheory.scala | 8 +- .../src/main/scala/ap/parser/SMTSupport.scala | 21 + .../src}/main/scala/ap/parser/SMTTypes.scala | 17 +- .../scala/ap/parser/SimpleClausifier.scala | 0 .../scala/ap/parser/SimpleMiniscoper.scala | 0 .../main/scala/ap/parser/Simplifier.scala | 0 .../main/scala/ap/parser/TPTPLineariser.scala | 0 .../scala/ap/parser/TriggerGenerator.scala | 0 .../main/scala/ap/proof/BindingContext.scala | 0 .../main/scala/ap/proof/ConstantFreedom.scala | 0 .../scala/ap/proof/ConstraintSimplifier.scala | 13 +- .../scala/ap/proof/ExhaustiveProver.scala | 0 .../scala/ap/proof/ModelSearchProver.scala | 50 +-- .../scala/ap/proof/QuantifierElimProver.scala | 0 .../src}/main/scala/ap/proof/Vocabulary.scala | 0 .../certificates/BinaryCertificate.scala | 0 .../BranchInferenceCollection.scala | 0 .../ap/proof/certificates/CertFormula.scala | 0 .../ap/proof/certificates/Certificate.scala | 0 .../certificates/CertificateOneChild.scala | 0 .../proof/certificates/CloseCertificate.scala | 0 .../DagCertificateConverter.scala | 0 .../ap/proof/certificates/DotLineariser.scala | 0 .../ap/proof/certificates/LemmaBase.scala | 0 .../proof/certificates/OmegaCertificate.scala | 0 .../proof/certificates/PropCertificate.scala | 0 .../certificates/SplitEqCertificate.scala | 0 .../certificates/StrengthenCertificate.scala | 0 .../scala/ap/proof/goal/AddFactsTask.scala | 0 .../scala/ap/proof/goal/AliasAnalyser.scala | 0 .../ap/proof/goal/AllQuantifierTask.scala | 0 .../scala/ap/proof/goal/BetaFormulaTask.scala | 0 .../ap/proof/goal/BlockedFormulaTask.scala | 0 .../ap/proof/goal/BoundStrengthenTask.scala | 0 .../ap/proof/goal/CompoundFormulas.scala | 0 .../ap/proof/goal/DivisibilityTask.scala | 0 .../main/scala/ap/proof/goal/EagerTask.scala | 0 .../ap/proof/goal/EagerTaskManager.scala | 0 .../ap/proof/goal/EliminateFactsTask.scala | 0 .../ap/proof/goal/ExQuantifierTask.scala | 0 .../proof/goal/FactsNormalisationTask.scala | 0 .../scala/ap/proof/goal/FormulaTask.scala | 0 .../src}/main/scala/ap/proof/goal/Goal.scala | 0 .../main/scala/ap/proof/goal/MatchTasks.scala | 0 .../ap/proof/goal/NegLitClauseTask.scala | 0 .../main/scala/ap/proof/goal/OmegaTask.scala | 0 .../scala/ap/proof/goal/PrioritisedTask.scala | 0 .../scala/ap/proof/goal/QuantifierTask.scala | 0 .../scala/ap/proof/goal/SymbolWeigths.scala | 0 .../src}/main/scala/ap/proof/goal/Task.scala | 0 .../scala/ap/proof/goal/TaskAggregator.scala | 0 .../scala/ap/proof/goal/TaskManager.scala | 0 .../goal/UpdateConstantFreedomTask.scala | 0 .../scala/ap/proof/goal/UpdateTasksTask.scala | 0 .../ap/proof/goal/WrappedFormulaTask.scala | 0 .../scala/ap/proof/theoryPlugins/Plugin.scala | 0 .../main/scala/ap/proof/tree/AndTree.scala | 0 .../tree/IteratingProofTreeFactory.scala | 0 .../main/scala/ap/proof/tree/ProofTree.scala | 0 .../ap/proof/tree/ProofTreeFactory.scala | 0 .../ap/proof/tree/ProofTreeOneChild.scala | 0 .../scala/ap/proof/tree/QuantifiedTree.scala | 0 .../ap/proof/tree/RandomDataSource.scala | 0 .../proof/tree/SimpleProofTreeFactory.scala | 0 .../scala/ap/proof/tree/StrengthenTree.scala | 0 .../scala/ap/proof/tree/TestProofTree.scala | 0 .../main/scala/ap/proof/tree/WeakenTree.scala | 0 .../main/scala/ap/terfor/AliasStatus.scala | 0 .../scala/ap/terfor/ComputationLogger.scala | 0 .../main/scala/ap/terfor/ConstantTerm.scala | 0 .../src}/main/scala/ap/terfor/Formula.scala | 0 .../src}/main/scala/ap/terfor/OneTerm.scala | 0 .../src}/main/scala/ap/terfor/Sorted.scala | 0 .../scala/ap/terfor/SortedWithOrder.scala | 0 .../src}/main/scala/ap/terfor/TerFor.scala | 0 .../scala/ap/terfor/TerForConvenience.scala | 0 .../src}/main/scala/ap/terfor/Term.scala | 0 .../src}/main/scala/ap/terfor/TermOrder.scala | 0 .../main/scala/ap/terfor/VariableTerm.scala | 0 .../scala/ap/terfor/arithconj/ArithConj.scala | 0 .../ap/terfor/arithconj/ModelFinder.scala | 0 .../ap/terfor/arithconj/ReduceWithAC.scala | 0 .../conjunctions/ConjunctEliminator.scala | 0 .../ap/terfor/conjunctions/Conjunction.scala | 0 .../conjunctions/IterativeClauseMatcher.scala | 0 .../terfor/conjunctions/LazyConjunction.scala | 0 .../conjunctions/NegatedConjunctions.scala | 0 .../ap/terfor/conjunctions/Quantifier.scala | 0 .../conjunctions/ReduceWithConjunction.scala | 0 .../terfor/conjunctions/ReducerPlugin.scala | 0 .../conjunctions/SubsumptionRemover.scala | 0 .../ap/terfor/equations/ColumnSolver.scala | 0 .../ap/terfor/equations/EquationConj.scala | 0 .../ap/terfor/equations/EquationSet.scala | 0 .../ap/terfor/equations/NegEquationConj.scala | 0 .../ap/terfor/equations/ReduceWithEqs.scala | 0 .../terfor/equations/ReduceWithNegEqs.scala | 0 .../terfor/inequalities/FMInfsComputer.scala | 0 .../ap/terfor/inequalities/InEqConj.scala | 0 .../ap/terfor/inequalities/IntervalProp.scala | 0 .../terfor/inequalities/ReduceWithInEqs.scala | 0 .../terfor/linearcombination/LCBlender.scala | 0 .../linearcombination/LinearCombination.scala | 0 .../linearcombination/ScalingIterator.scala | 0 .../main/scala/ap/terfor/preds/Atom.scala | 0 .../main/scala/ap/terfor/preds/PredConj.scala | 0 .../scala/ap/terfor/preds/Predicate.scala | 0 .../ap/terfor/preds/ReduceWithPredLits.scala | 0 .../terfor/substitutions/ComposeSubsts.scala | 0 .../terfor/substitutions/ConstantSubst.scala | 0 .../terfor/substitutions/IdentitySubst.scala | 0 .../substitutions/PseudoConstantSubst.scala | 0 .../substitutions/PseudoDivSubstitution.scala | 0 .../substitutions/SimpleSubstitution.scala | 0 .../terfor/substitutions/Substitution.scala | 0 .../substitutions/VariableShiftSubst.scala | 0 .../terfor/substitutions/VariableSubst.scala | 0 .../src}/main/scala/ap/theories/ADT.scala | 3 +- .../ap/theories/BitShiftMultiplication.scala | 0 .../src}/main/scala/ap/theories/DivZero.scala | 0 .../ap/theories/FunctionalConsistency.scala | 0 .../scala/ap/theories/Incompleteness.scala | 0 .../main/scala/ap/theories/MulTheory.scala | 0 .../ap/theories/SaturationProcedure.scala | 0 .../src}/main/scala/ap/theories/Theory.scala | 0 .../scala/ap/theories/TheoryBuilder.scala | 0 .../scala/ap/theories/TheoryCollector.scala | 0 .../scala/ap/theories/TheoryRegistry.scala | 0 .../scala/ap/theories/ValueEnumerator.scala | 0 .../scala/ap/theories/arrays/CombArray.scala | 0 .../scala/ap/theories/arrays/ExtArray.scala | 0 .../ap/theories/arrays/MinMaxArray.scala | 0 .../scala/ap/theories/arrays/SetTheory.scala | 0 .../ap/theories/arrays/SimpleArray.scala | 0 .../bitvectors/ExtractArithEncoder.scala | 0 .../theories/bitvectors/ModCastSplitter.scala | 0 .../ap/theories/bitvectors/ModPlugin.scala | 0 .../bitvectors/ModPostprocessor.scala | 0 .../theories/bitvectors/ModPreprocessor.scala | 0 .../ap/theories/bitvectors/ModReducer.scala | 0 .../bitvectors/ModuloArithmetic.scala | 0 .../scala/ap/theories/bitvectors/Ring.scala | 0 .../bitvectors/ShiftCastSplitter.scala | 0 .../scala/ap/theories/heaps/ArrayHeap.scala | 0 .../main/scala/ap/theories/heaps/Heap.scala | 0 .../scala/ap/theories/heaps/NativeHeap.scala | 0 .../scala/ap/theories/nia/Buchberger.scala | 0 .../main/scala/ap/theories/nia/Gaussian.scala | 163 +++++++ .../theories/nia/GroebnerMultiplication.scala | 0 .../main/scala/ap/theories/nia/Interval.scala | 0 .../ap/theories/nia/IntervalPropagator.scala | 0 .../scala/ap/theories/nia/Polynomial.scala | 0 .../main/scala/ap/theories/nia/Splitter.scala | 0 .../src}/main/scala/ap/theories/package.scala | 0 .../ap/theories/rationals/Fractions.scala | 0 .../ap/theories/rationals/Rationals.scala | 0 .../theories/sequences/ArraySeqTheory.scala | 0 .../sequences/ArraySeqTheoryBuilder.scala | 0 .../ap/theories/sequences/SeqTheory.scala | 0 .../theories/sequences/SeqTheoryBuilder.scala | 0 .../strings/AbstractStringTheory.scala | 0 .../ap/theories/strings/SeqStringTheory.scala | 0 .../strings/SeqStringTheoryBuilder.scala | 0 .../ap/theories/strings/StringTheory.scala | 0 .../strings/StringTheoryBuilder.scala | 0 .../src}/main/scala/ap/types/Sort.scala | 0 .../main/scala/ap/types/SortedSymbols.scala | 0 .../src}/main/scala/ap/types/TypeTheory.scala | 0 .../scala/ap/types/UninterpretedSort.scala | 0 .../src}/main/scala/ap/util/OpCounters.scala | 0 .../src}/main/scala/ap/util/Timer.scala | 0 .../ap/core/ImplicationCheckerTest.scala | 46 ++ docs/scala-js-migration-plan.md | 407 ++++++++++++++++++ .../scala/ap/parser/SMTParser2InputAbsy.scala | 12 +- src/main/scala/ap/theories/nia/Gaussian.scala | 5 +- 217 files changed, 718 insertions(+), 79 deletions(-) rename {src => core/src}/main/scala/ap/PresburgerTools.scala (100%) rename {src => core/src}/main/scala/ap/Prover.scala (100%) rename {src => core/src}/main/scala/ap/Signature.scala (100%) rename {src => core/src}/main/scala/ap/algebra/Group.scala (100%) rename {src => core/src}/main/scala/ap/algebra/Integers.scala (100%) rename {src => core/src}/main/scala/ap/algebra/Ring.scala (100%) rename {src => core/src}/main/scala/ap/algebra/package.scala (100%) rename {src => core/src}/main/scala/ap/api/PartialModel.scala (100%) create mode 100644 core/src/main/scala/ap/core/ImplicationChecker.scala rename {src => core/src}/main/scala/ap/interpolants/BenchUtils.scala (100%) rename {src => core/src}/main/scala/ap/interpolants/InterpolantSimplifier.scala (100%) rename {src => core/src}/main/scala/ap/interpolants/InterpolationContext.scala (100%) rename {src => core/src}/main/scala/ap/interpolants/Interpolator.scala (100%) rename {src => core/src}/main/scala/ap/interpolants/InterpolatorQE.scala (100%) rename {src => core/src}/main/scala/ap/interpolants/PartialInterpolant.scala (100%) rename {src => core/src}/main/scala/ap/interpolants/ProofSimplifier.scala (100%) rename {src => core/src}/main/scala/ap/parameters/Param.scala (100%) rename {src => core/src}/main/scala/ap/parameters/Settings.scala (100%) rename {src => core/src}/main/scala/ap/parser/BooleanCompactifier.scala (100%) rename {src => core/src}/main/scala/ap/parser/CSIsatLineariser.scala (100%) rename {src => core/src}/main/scala/ap/parser/Environment.scala (100%) rename {src => core/src}/main/scala/ap/parser/EquivExpander.scala (100%) rename {src => core/src}/main/scala/ap/parser/EquivInliner.scala (100%) rename {src => core/src}/main/scala/ap/parser/ExMaxiscoper.scala (100%) rename {src => core/src}/main/scala/ap/parser/FunctionEncoder.scala (100%) rename {src => core/src}/main/scala/ap/parser/FunctionPreprocessing.scala (100%) rename {src => core/src}/main/scala/ap/parser/IExpression.scala (100%) rename {src => core/src}/main/scala/ap/parser/IFormula.scala (100%) rename {src => core/src}/main/scala/ap/parser/ITerm.scala (100%) rename {src => core/src}/main/scala/ap/parser/ImplicationCompressor.scala (100%) rename {src => core/src}/main/scala/ap/parser/InputAbsy2Internal.scala (100%) rename {src => core/src}/main/scala/ap/parser/InputAbsyVisitor.scala (100%) rename {src => core/src}/main/scala/ap/parser/Internal2InputAbsy.scala (100%) rename {src => core/src}/main/scala/ap/parser/KBO.scala (100%) rename {src => core/src}/main/scala/ap/parser/Parser2InputAbsy.scala (100%) rename {src => core/src}/main/scala/ap/parser/PartExtractor.scala (100%) rename {src => core/src}/main/scala/ap/parser/PartialEvaluator.scala (100%) rename {src => core/src}/main/scala/ap/parser/Postprocessing.scala (100%) rename {src => core/src}/main/scala/ap/parser/Preprocessing.scala (100%) rename {src => core/src}/main/scala/ap/parser/Rewriter.scala (100%) rename {src => core/src}/main/scala/ap/parser/SMTLineariser.scala (98%) rename {src => core/src}/main/scala/ap/parser/SMTParseableTheory.scala (95%) create mode 100644 core/src/main/scala/ap/parser/SMTSupport.scala rename {src => core/src}/main/scala/ap/parser/SMTTypes.scala (96%) rename {src => core/src}/main/scala/ap/parser/SimpleClausifier.scala (100%) rename {src => core/src}/main/scala/ap/parser/SimpleMiniscoper.scala (100%) rename {src => core/src}/main/scala/ap/parser/Simplifier.scala (100%) rename {src => core/src}/main/scala/ap/parser/TPTPLineariser.scala (100%) rename {src => core/src}/main/scala/ap/parser/TriggerGenerator.scala (100%) rename {src => core/src}/main/scala/ap/proof/BindingContext.scala (100%) rename {src => core/src}/main/scala/ap/proof/ConstantFreedom.scala (100%) rename {src => core/src}/main/scala/ap/proof/ConstraintSimplifier.scala (95%) rename {src => core/src}/main/scala/ap/proof/ExhaustiveProver.scala (100%) rename {src => core/src}/main/scala/ap/proof/ModelSearchProver.scala (97%) rename {src => core/src}/main/scala/ap/proof/QuantifierElimProver.scala (100%) rename {src => core/src}/main/scala/ap/proof/Vocabulary.scala (100%) rename {src => core/src}/main/scala/ap/proof/certificates/BinaryCertificate.scala (100%) rename {src => core/src}/main/scala/ap/proof/certificates/BranchInferenceCollection.scala (100%) rename {src => core/src}/main/scala/ap/proof/certificates/CertFormula.scala (100%) rename {src => core/src}/main/scala/ap/proof/certificates/Certificate.scala (100%) rename {src => core/src}/main/scala/ap/proof/certificates/CertificateOneChild.scala (100%) rename {src => core/src}/main/scala/ap/proof/certificates/CloseCertificate.scala (100%) rename {src => core/src}/main/scala/ap/proof/certificates/DagCertificateConverter.scala (100%) rename {src => core/src}/main/scala/ap/proof/certificates/DotLineariser.scala (100%) rename {src => core/src}/main/scala/ap/proof/certificates/LemmaBase.scala (100%) rename {src => core/src}/main/scala/ap/proof/certificates/OmegaCertificate.scala (100%) rename {src => core/src}/main/scala/ap/proof/certificates/PropCertificate.scala (100%) rename {src => core/src}/main/scala/ap/proof/certificates/SplitEqCertificate.scala (100%) rename {src => core/src}/main/scala/ap/proof/certificates/StrengthenCertificate.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/AddFactsTask.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/AliasAnalyser.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/AllQuantifierTask.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/BetaFormulaTask.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/BlockedFormulaTask.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/BoundStrengthenTask.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/CompoundFormulas.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/DivisibilityTask.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/EagerTask.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/EagerTaskManager.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/EliminateFactsTask.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/ExQuantifierTask.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/FactsNormalisationTask.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/FormulaTask.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/Goal.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/MatchTasks.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/NegLitClauseTask.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/OmegaTask.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/PrioritisedTask.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/QuantifierTask.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/SymbolWeigths.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/Task.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/TaskAggregator.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/TaskManager.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/UpdateConstantFreedomTask.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/UpdateTasksTask.scala (100%) rename {src => core/src}/main/scala/ap/proof/goal/WrappedFormulaTask.scala (100%) rename {src => core/src}/main/scala/ap/proof/theoryPlugins/Plugin.scala (100%) rename {src => core/src}/main/scala/ap/proof/tree/AndTree.scala (100%) rename {src => core/src}/main/scala/ap/proof/tree/IteratingProofTreeFactory.scala (100%) rename {src => core/src}/main/scala/ap/proof/tree/ProofTree.scala (100%) rename {src => core/src}/main/scala/ap/proof/tree/ProofTreeFactory.scala (100%) rename {src => core/src}/main/scala/ap/proof/tree/ProofTreeOneChild.scala (100%) rename {src => core/src}/main/scala/ap/proof/tree/QuantifiedTree.scala (100%) rename {src => core/src}/main/scala/ap/proof/tree/RandomDataSource.scala (100%) rename {src => core/src}/main/scala/ap/proof/tree/SimpleProofTreeFactory.scala (100%) rename {src => core/src}/main/scala/ap/proof/tree/StrengthenTree.scala (100%) rename {src => core/src}/main/scala/ap/proof/tree/TestProofTree.scala (100%) rename {src => core/src}/main/scala/ap/proof/tree/WeakenTree.scala (100%) rename {src => core/src}/main/scala/ap/terfor/AliasStatus.scala (100%) rename {src => core/src}/main/scala/ap/terfor/ComputationLogger.scala (100%) rename {src => core/src}/main/scala/ap/terfor/ConstantTerm.scala (100%) rename {src => core/src}/main/scala/ap/terfor/Formula.scala (100%) rename {src => core/src}/main/scala/ap/terfor/OneTerm.scala (100%) rename {src => core/src}/main/scala/ap/terfor/Sorted.scala (100%) rename {src => core/src}/main/scala/ap/terfor/SortedWithOrder.scala (100%) rename {src => core/src}/main/scala/ap/terfor/TerFor.scala (100%) rename {src => core/src}/main/scala/ap/terfor/TerForConvenience.scala (100%) rename {src => core/src}/main/scala/ap/terfor/Term.scala (100%) rename {src => core/src}/main/scala/ap/terfor/TermOrder.scala (100%) rename {src => core/src}/main/scala/ap/terfor/VariableTerm.scala (100%) rename {src => core/src}/main/scala/ap/terfor/arithconj/ArithConj.scala (100%) rename {src => core/src}/main/scala/ap/terfor/arithconj/ModelFinder.scala (100%) rename {src => core/src}/main/scala/ap/terfor/arithconj/ReduceWithAC.scala (100%) rename {src => core/src}/main/scala/ap/terfor/conjunctions/ConjunctEliminator.scala (100%) rename {src => core/src}/main/scala/ap/terfor/conjunctions/Conjunction.scala (100%) rename {src => core/src}/main/scala/ap/terfor/conjunctions/IterativeClauseMatcher.scala (100%) rename {src => core/src}/main/scala/ap/terfor/conjunctions/LazyConjunction.scala (100%) rename {src => core/src}/main/scala/ap/terfor/conjunctions/NegatedConjunctions.scala (100%) rename {src => core/src}/main/scala/ap/terfor/conjunctions/Quantifier.scala (100%) rename {src => core/src}/main/scala/ap/terfor/conjunctions/ReduceWithConjunction.scala (100%) rename {src => core/src}/main/scala/ap/terfor/conjunctions/ReducerPlugin.scala (100%) rename {src => core/src}/main/scala/ap/terfor/conjunctions/SubsumptionRemover.scala (100%) rename {src => core/src}/main/scala/ap/terfor/equations/ColumnSolver.scala (100%) rename {src => core/src}/main/scala/ap/terfor/equations/EquationConj.scala (100%) rename {src => core/src}/main/scala/ap/terfor/equations/EquationSet.scala (100%) rename {src => core/src}/main/scala/ap/terfor/equations/NegEquationConj.scala (100%) rename {src => core/src}/main/scala/ap/terfor/equations/ReduceWithEqs.scala (100%) rename {src => core/src}/main/scala/ap/terfor/equations/ReduceWithNegEqs.scala (100%) rename {src => core/src}/main/scala/ap/terfor/inequalities/FMInfsComputer.scala (100%) rename {src => core/src}/main/scala/ap/terfor/inequalities/InEqConj.scala (100%) rename {src => core/src}/main/scala/ap/terfor/inequalities/IntervalProp.scala (100%) rename {src => core/src}/main/scala/ap/terfor/inequalities/ReduceWithInEqs.scala (100%) rename {src => core/src}/main/scala/ap/terfor/linearcombination/LCBlender.scala (100%) rename {src => core/src}/main/scala/ap/terfor/linearcombination/LinearCombination.scala (100%) rename {src => core/src}/main/scala/ap/terfor/linearcombination/ScalingIterator.scala (100%) rename {src => core/src}/main/scala/ap/terfor/preds/Atom.scala (100%) rename {src => core/src}/main/scala/ap/terfor/preds/PredConj.scala (100%) rename {src => core/src}/main/scala/ap/terfor/preds/Predicate.scala (100%) rename {src => core/src}/main/scala/ap/terfor/preds/ReduceWithPredLits.scala (100%) rename {src => core/src}/main/scala/ap/terfor/substitutions/ComposeSubsts.scala (100%) rename {src => core/src}/main/scala/ap/terfor/substitutions/ConstantSubst.scala (100%) rename {src => core/src}/main/scala/ap/terfor/substitutions/IdentitySubst.scala (100%) rename {src => core/src}/main/scala/ap/terfor/substitutions/PseudoConstantSubst.scala (100%) rename {src => core/src}/main/scala/ap/terfor/substitutions/PseudoDivSubstitution.scala (100%) rename {src => core/src}/main/scala/ap/terfor/substitutions/SimpleSubstitution.scala (100%) rename {src => core/src}/main/scala/ap/terfor/substitutions/Substitution.scala (100%) rename {src => core/src}/main/scala/ap/terfor/substitutions/VariableShiftSubst.scala (100%) rename {src => core/src}/main/scala/ap/terfor/substitutions/VariableSubst.scala (100%) rename {src => core/src}/main/scala/ap/theories/ADT.scala (99%) rename {src => core/src}/main/scala/ap/theories/BitShiftMultiplication.scala (100%) rename {src => core/src}/main/scala/ap/theories/DivZero.scala (100%) rename {src => core/src}/main/scala/ap/theories/FunctionalConsistency.scala (100%) rename {src => core/src}/main/scala/ap/theories/Incompleteness.scala (100%) rename {src => core/src}/main/scala/ap/theories/MulTheory.scala (100%) rename {src => core/src}/main/scala/ap/theories/SaturationProcedure.scala (100%) rename {src => core/src}/main/scala/ap/theories/Theory.scala (100%) rename {src => core/src}/main/scala/ap/theories/TheoryBuilder.scala (100%) rename {src => core/src}/main/scala/ap/theories/TheoryCollector.scala (100%) rename {src => core/src}/main/scala/ap/theories/TheoryRegistry.scala (100%) rename {src => core/src}/main/scala/ap/theories/ValueEnumerator.scala (100%) rename {src => core/src}/main/scala/ap/theories/arrays/CombArray.scala (100%) rename {src => core/src}/main/scala/ap/theories/arrays/ExtArray.scala (100%) rename {src => core/src}/main/scala/ap/theories/arrays/MinMaxArray.scala (100%) rename {src => core/src}/main/scala/ap/theories/arrays/SetTheory.scala (100%) rename {src => core/src}/main/scala/ap/theories/arrays/SimpleArray.scala (100%) rename {src => core/src}/main/scala/ap/theories/bitvectors/ExtractArithEncoder.scala (100%) rename {src => core/src}/main/scala/ap/theories/bitvectors/ModCastSplitter.scala (100%) rename {src => core/src}/main/scala/ap/theories/bitvectors/ModPlugin.scala (100%) rename {src => core/src}/main/scala/ap/theories/bitvectors/ModPostprocessor.scala (100%) rename {src => core/src}/main/scala/ap/theories/bitvectors/ModPreprocessor.scala (100%) rename {src => core/src}/main/scala/ap/theories/bitvectors/ModReducer.scala (100%) rename {src => core/src}/main/scala/ap/theories/bitvectors/ModuloArithmetic.scala (100%) rename {src => core/src}/main/scala/ap/theories/bitvectors/Ring.scala (100%) rename {src => core/src}/main/scala/ap/theories/bitvectors/ShiftCastSplitter.scala (100%) rename {src => core/src}/main/scala/ap/theories/heaps/ArrayHeap.scala (100%) rename {src => core/src}/main/scala/ap/theories/heaps/Heap.scala (100%) rename {src => core/src}/main/scala/ap/theories/heaps/NativeHeap.scala (100%) rename {src => core/src}/main/scala/ap/theories/nia/Buchberger.scala (100%) create mode 100644 core/src/main/scala/ap/theories/nia/Gaussian.scala rename {src => core/src}/main/scala/ap/theories/nia/GroebnerMultiplication.scala (100%) rename {src => core/src}/main/scala/ap/theories/nia/Interval.scala (100%) rename {src => core/src}/main/scala/ap/theories/nia/IntervalPropagator.scala (100%) rename {src => core/src}/main/scala/ap/theories/nia/Polynomial.scala (100%) rename {src => core/src}/main/scala/ap/theories/nia/Splitter.scala (100%) rename {src => core/src}/main/scala/ap/theories/package.scala (100%) rename {src => core/src}/main/scala/ap/theories/rationals/Fractions.scala (100%) rename {src => core/src}/main/scala/ap/theories/rationals/Rationals.scala (100%) rename {src => core/src}/main/scala/ap/theories/sequences/ArraySeqTheory.scala (100%) rename {src => core/src}/main/scala/ap/theories/sequences/ArraySeqTheoryBuilder.scala (100%) rename {src => core/src}/main/scala/ap/theories/sequences/SeqTheory.scala (100%) rename {src => core/src}/main/scala/ap/theories/sequences/SeqTheoryBuilder.scala (100%) rename {src => core/src}/main/scala/ap/theories/strings/AbstractStringTheory.scala (100%) rename {src => core/src}/main/scala/ap/theories/strings/SeqStringTheory.scala (100%) rename {src => core/src}/main/scala/ap/theories/strings/SeqStringTheoryBuilder.scala (100%) rename {src => core/src}/main/scala/ap/theories/strings/StringTheory.scala (100%) rename {src => core/src}/main/scala/ap/theories/strings/StringTheoryBuilder.scala (100%) rename {src => core/src}/main/scala/ap/types/Sort.scala (100%) rename {src => core/src}/main/scala/ap/types/SortedSymbols.scala (100%) rename {src => core/src}/main/scala/ap/types/TypeTheory.scala (100%) rename {src => core/src}/main/scala/ap/types/UninterpretedSort.scala (100%) rename {src => core/src}/main/scala/ap/util/OpCounters.scala (100%) rename {src => core/src}/main/scala/ap/util/Timer.scala (100%) create mode 100644 core/src/test/scala/ap/core/ImplicationCheckerTest.scala create mode 100644 docs/scala-js-migration-plan.md diff --git a/build.sbt b/build.sbt index 9b8182b93..6af27a839 100644 --- a/build.sbt +++ b/build.sbt @@ -94,6 +94,8 @@ lazy val core = (project in file("core")). settings(commonSettings: _*). settings( name := "Princess-core", + libraryDependencies += + "org.scalacheck" %% "scalacheck" % "1.15.2" % Test, Compile / scalacOptions ++= List("-feature", "-language:implicitConversions,postfixOps,reflectiveCalls"), diff --git a/src/main/scala/ap/PresburgerTools.scala b/core/src/main/scala/ap/PresburgerTools.scala similarity index 100% rename from src/main/scala/ap/PresburgerTools.scala rename to core/src/main/scala/ap/PresburgerTools.scala diff --git a/src/main/scala/ap/Prover.scala b/core/src/main/scala/ap/Prover.scala similarity index 100% rename from src/main/scala/ap/Prover.scala rename to core/src/main/scala/ap/Prover.scala diff --git a/src/main/scala/ap/Signature.scala b/core/src/main/scala/ap/Signature.scala similarity index 100% rename from src/main/scala/ap/Signature.scala rename to core/src/main/scala/ap/Signature.scala diff --git a/src/main/scala/ap/algebra/Group.scala b/core/src/main/scala/ap/algebra/Group.scala similarity index 100% rename from src/main/scala/ap/algebra/Group.scala rename to core/src/main/scala/ap/algebra/Group.scala diff --git a/src/main/scala/ap/algebra/Integers.scala b/core/src/main/scala/ap/algebra/Integers.scala similarity index 100% rename from src/main/scala/ap/algebra/Integers.scala rename to core/src/main/scala/ap/algebra/Integers.scala diff --git a/src/main/scala/ap/algebra/Ring.scala b/core/src/main/scala/ap/algebra/Ring.scala similarity index 100% rename from src/main/scala/ap/algebra/Ring.scala rename to core/src/main/scala/ap/algebra/Ring.scala diff --git a/src/main/scala/ap/algebra/package.scala b/core/src/main/scala/ap/algebra/package.scala similarity index 100% rename from src/main/scala/ap/algebra/package.scala rename to core/src/main/scala/ap/algebra/package.scala diff --git a/src/main/scala/ap/api/PartialModel.scala b/core/src/main/scala/ap/api/PartialModel.scala similarity index 100% rename from src/main/scala/ap/api/PartialModel.scala rename to core/src/main/scala/ap/api/PartialModel.scala diff --git a/core/src/main/scala/ap/core/ImplicationChecker.scala b/core/src/main/scala/ap/core/ImplicationChecker.scala new file mode 100644 index 000000000..3c1679f6c --- /dev/null +++ b/core/src/main/scala/ap/core/ImplicationChecker.scala @@ -0,0 +1,23 @@ +package ap.core + +import ap.PresburgerTools +import ap.parser.{IFormula, IExpression, SymbolCollector, InputAbsy2Internal, IBoolLit} +import ap.terfor.TermOrder +import ap.terfor.conjunctions.Conjunction + +object ImplicationChecker { + + import IExpression._ + + def implies(assumptions : Seq[IFormula], conclusion : IFormula) : Boolean = { + val premise = assumptions.foldLeft[IFormula](IBoolLit(true))(_ & _) + isValid(premise ==> conclusion) + } + + def isValid(formula : IFormula) : Boolean = { + val order = + TermOrder.EMPTY.extend(SymbolCollector.constantsSorted(formula)) + val internal = InputAbsy2Internal(formula, order) + PresburgerTools.isValid(Conjunction.conj(internal, order)) + } +} diff --git a/src/main/scala/ap/interpolants/BenchUtils.scala b/core/src/main/scala/ap/interpolants/BenchUtils.scala similarity index 100% rename from src/main/scala/ap/interpolants/BenchUtils.scala rename to core/src/main/scala/ap/interpolants/BenchUtils.scala diff --git a/src/main/scala/ap/interpolants/InterpolantSimplifier.scala b/core/src/main/scala/ap/interpolants/InterpolantSimplifier.scala similarity index 100% rename from src/main/scala/ap/interpolants/InterpolantSimplifier.scala rename to core/src/main/scala/ap/interpolants/InterpolantSimplifier.scala diff --git a/src/main/scala/ap/interpolants/InterpolationContext.scala b/core/src/main/scala/ap/interpolants/InterpolationContext.scala similarity index 100% rename from src/main/scala/ap/interpolants/InterpolationContext.scala rename to core/src/main/scala/ap/interpolants/InterpolationContext.scala diff --git a/src/main/scala/ap/interpolants/Interpolator.scala b/core/src/main/scala/ap/interpolants/Interpolator.scala similarity index 100% rename from src/main/scala/ap/interpolants/Interpolator.scala rename to core/src/main/scala/ap/interpolants/Interpolator.scala diff --git a/src/main/scala/ap/interpolants/InterpolatorQE.scala b/core/src/main/scala/ap/interpolants/InterpolatorQE.scala similarity index 100% rename from src/main/scala/ap/interpolants/InterpolatorQE.scala rename to core/src/main/scala/ap/interpolants/InterpolatorQE.scala diff --git a/src/main/scala/ap/interpolants/PartialInterpolant.scala b/core/src/main/scala/ap/interpolants/PartialInterpolant.scala similarity index 100% rename from src/main/scala/ap/interpolants/PartialInterpolant.scala rename to core/src/main/scala/ap/interpolants/PartialInterpolant.scala diff --git a/src/main/scala/ap/interpolants/ProofSimplifier.scala b/core/src/main/scala/ap/interpolants/ProofSimplifier.scala similarity index 100% rename from src/main/scala/ap/interpolants/ProofSimplifier.scala rename to core/src/main/scala/ap/interpolants/ProofSimplifier.scala diff --git a/src/main/scala/ap/parameters/Param.scala b/core/src/main/scala/ap/parameters/Param.scala similarity index 100% rename from src/main/scala/ap/parameters/Param.scala rename to core/src/main/scala/ap/parameters/Param.scala diff --git a/src/main/scala/ap/parameters/Settings.scala b/core/src/main/scala/ap/parameters/Settings.scala similarity index 100% rename from src/main/scala/ap/parameters/Settings.scala rename to core/src/main/scala/ap/parameters/Settings.scala diff --git a/src/main/scala/ap/parser/BooleanCompactifier.scala b/core/src/main/scala/ap/parser/BooleanCompactifier.scala similarity index 100% rename from src/main/scala/ap/parser/BooleanCompactifier.scala rename to core/src/main/scala/ap/parser/BooleanCompactifier.scala diff --git a/src/main/scala/ap/parser/CSIsatLineariser.scala b/core/src/main/scala/ap/parser/CSIsatLineariser.scala similarity index 100% rename from src/main/scala/ap/parser/CSIsatLineariser.scala rename to core/src/main/scala/ap/parser/CSIsatLineariser.scala diff --git a/src/main/scala/ap/parser/Environment.scala b/core/src/main/scala/ap/parser/Environment.scala similarity index 100% rename from src/main/scala/ap/parser/Environment.scala rename to core/src/main/scala/ap/parser/Environment.scala diff --git a/src/main/scala/ap/parser/EquivExpander.scala b/core/src/main/scala/ap/parser/EquivExpander.scala similarity index 100% rename from src/main/scala/ap/parser/EquivExpander.scala rename to core/src/main/scala/ap/parser/EquivExpander.scala diff --git a/src/main/scala/ap/parser/EquivInliner.scala b/core/src/main/scala/ap/parser/EquivInliner.scala similarity index 100% rename from src/main/scala/ap/parser/EquivInliner.scala rename to core/src/main/scala/ap/parser/EquivInliner.scala diff --git a/src/main/scala/ap/parser/ExMaxiscoper.scala b/core/src/main/scala/ap/parser/ExMaxiscoper.scala similarity index 100% rename from src/main/scala/ap/parser/ExMaxiscoper.scala rename to core/src/main/scala/ap/parser/ExMaxiscoper.scala diff --git a/src/main/scala/ap/parser/FunctionEncoder.scala b/core/src/main/scala/ap/parser/FunctionEncoder.scala similarity index 100% rename from src/main/scala/ap/parser/FunctionEncoder.scala rename to core/src/main/scala/ap/parser/FunctionEncoder.scala diff --git a/src/main/scala/ap/parser/FunctionPreprocessing.scala b/core/src/main/scala/ap/parser/FunctionPreprocessing.scala similarity index 100% rename from src/main/scala/ap/parser/FunctionPreprocessing.scala rename to core/src/main/scala/ap/parser/FunctionPreprocessing.scala diff --git a/src/main/scala/ap/parser/IExpression.scala b/core/src/main/scala/ap/parser/IExpression.scala similarity index 100% rename from src/main/scala/ap/parser/IExpression.scala rename to core/src/main/scala/ap/parser/IExpression.scala diff --git a/src/main/scala/ap/parser/IFormula.scala b/core/src/main/scala/ap/parser/IFormula.scala similarity index 100% rename from src/main/scala/ap/parser/IFormula.scala rename to core/src/main/scala/ap/parser/IFormula.scala diff --git a/src/main/scala/ap/parser/ITerm.scala b/core/src/main/scala/ap/parser/ITerm.scala similarity index 100% rename from src/main/scala/ap/parser/ITerm.scala rename to core/src/main/scala/ap/parser/ITerm.scala diff --git a/src/main/scala/ap/parser/ImplicationCompressor.scala b/core/src/main/scala/ap/parser/ImplicationCompressor.scala similarity index 100% rename from src/main/scala/ap/parser/ImplicationCompressor.scala rename to core/src/main/scala/ap/parser/ImplicationCompressor.scala diff --git a/src/main/scala/ap/parser/InputAbsy2Internal.scala b/core/src/main/scala/ap/parser/InputAbsy2Internal.scala similarity index 100% rename from src/main/scala/ap/parser/InputAbsy2Internal.scala rename to core/src/main/scala/ap/parser/InputAbsy2Internal.scala diff --git a/src/main/scala/ap/parser/InputAbsyVisitor.scala b/core/src/main/scala/ap/parser/InputAbsyVisitor.scala similarity index 100% rename from src/main/scala/ap/parser/InputAbsyVisitor.scala rename to core/src/main/scala/ap/parser/InputAbsyVisitor.scala diff --git a/src/main/scala/ap/parser/Internal2InputAbsy.scala b/core/src/main/scala/ap/parser/Internal2InputAbsy.scala similarity index 100% rename from src/main/scala/ap/parser/Internal2InputAbsy.scala rename to core/src/main/scala/ap/parser/Internal2InputAbsy.scala diff --git a/src/main/scala/ap/parser/KBO.scala b/core/src/main/scala/ap/parser/KBO.scala similarity index 100% rename from src/main/scala/ap/parser/KBO.scala rename to core/src/main/scala/ap/parser/KBO.scala diff --git a/src/main/scala/ap/parser/Parser2InputAbsy.scala b/core/src/main/scala/ap/parser/Parser2InputAbsy.scala similarity index 100% rename from src/main/scala/ap/parser/Parser2InputAbsy.scala rename to core/src/main/scala/ap/parser/Parser2InputAbsy.scala diff --git a/src/main/scala/ap/parser/PartExtractor.scala b/core/src/main/scala/ap/parser/PartExtractor.scala similarity index 100% rename from src/main/scala/ap/parser/PartExtractor.scala rename to core/src/main/scala/ap/parser/PartExtractor.scala diff --git a/src/main/scala/ap/parser/PartialEvaluator.scala b/core/src/main/scala/ap/parser/PartialEvaluator.scala similarity index 100% rename from src/main/scala/ap/parser/PartialEvaluator.scala rename to core/src/main/scala/ap/parser/PartialEvaluator.scala diff --git a/src/main/scala/ap/parser/Postprocessing.scala b/core/src/main/scala/ap/parser/Postprocessing.scala similarity index 100% rename from src/main/scala/ap/parser/Postprocessing.scala rename to core/src/main/scala/ap/parser/Postprocessing.scala diff --git a/src/main/scala/ap/parser/Preprocessing.scala b/core/src/main/scala/ap/parser/Preprocessing.scala similarity index 100% rename from src/main/scala/ap/parser/Preprocessing.scala rename to core/src/main/scala/ap/parser/Preprocessing.scala diff --git a/src/main/scala/ap/parser/Rewriter.scala b/core/src/main/scala/ap/parser/Rewriter.scala similarity index 100% rename from src/main/scala/ap/parser/Rewriter.scala rename to core/src/main/scala/ap/parser/Rewriter.scala diff --git a/src/main/scala/ap/parser/SMTLineariser.scala b/core/src/main/scala/ap/parser/SMTLineariser.scala similarity index 98% rename from src/main/scala/ap/parser/SMTLineariser.scala rename to core/src/main/scala/ap/parser/SMTLineariser.scala index b15f4a1d0..defd893fa 100644 --- a/src/main/scala/ap/parser/SMTLineariser.scala +++ b/core/src/main/scala/ap/parser/SMTLineariser.scala @@ -61,7 +61,7 @@ import java.io.PrintStream object SMTLineariser { import SMTTypes._ - import SMTParser2InputAbsy.SMTFunctionType + import SMTSupport.SMTFunctionType private val AC = Debug.AC_PARSER @@ -631,9 +631,9 @@ object SMTLineariser { constantType : ConstantTerm => Option[SMTTypes.SMTType], functionType : - IFunction => Option[SMTParser2InputAbsy.SMTFunctionType], + IFunction => Option[SMTSupport.SMTFunctionType], predType : - Predicate => Option[SMTParser2InputAbsy.SMTFunctionType], + Predicate => Option[SMTSupport.SMTFunctionType], prettyBitvectors : Boolean = true) : Unit = formula match { case IBoolLit(value) => print(value) @@ -671,11 +671,21 @@ object SMTLineariser { case t : ITerm => asString(t) } + private def captureString(comp : => Unit) : String = { + val out = new java.io.ByteArrayOutputStream + val ps = new java.io.PrintStream(out) + Console.withOut(ps) { + comp + } + ps.flush() + out.toString("UTF-8") + } + def asString(formula : IFormula) : String = - ap.DialogUtil.asString { apply(formula) } + captureString { apply(formula) } def asString(t : ITerm) : String = - ap.DialogUtil.asString { apply(t) } + captureString { apply(t) } ////////////////////////////////////////////////////////////////////////////// @@ -946,9 +956,9 @@ class SMTLineariser(benchmarkName : String, constantType : ConstantTerm => Option[SMTTypes.SMTType], functionType : - IFunction => Option[SMTParser2InputAbsy.SMTFunctionType], + IFunction => Option[SMTSupport.SMTFunctionType], predType : - Predicate => Option[SMTParser2InputAbsy.SMTFunctionType], + Predicate => Option[SMTSupport.SMTFunctionType], prettyBitvectors : Boolean = true) { import SMTTypes._ @@ -1065,7 +1075,7 @@ class SMTLineariser(benchmarkName : String, ////////////////////////////////////////////////////////////////////////////// - import SMTParser2InputAbsy.SMTFunctionType + import SMTSupport.SMTFunctionType private def getTermType(t : ITerm) (implicit variableType : Int => Option[SMTType]) @@ -1484,4 +1494,3 @@ class SMTLineariser(benchmarkName : String, } } - diff --git a/src/main/scala/ap/parser/SMTParseableTheory.scala b/core/src/main/scala/ap/parser/SMTParseableTheory.scala similarity index 95% rename from src/main/scala/ap/parser/SMTParseableTheory.scala rename to core/src/main/scala/ap/parser/SMTParseableTheory.scala index b268eaa21..31d8c8027 100644 --- a/src/main/scala/ap/parser/SMTParseableTheory.scala +++ b/core/src/main/scala/ap/parser/SMTParseableTheory.scala @@ -34,7 +34,6 @@ package ap.parser import ap.theories.Theory -import ap.parser.smtlib.Absyn.{Sort => SSort, SymbolRef} import ap.types.Sort /** @@ -89,10 +88,13 @@ trait SMTParseableTheory { import SMTTypes.SMTType + type SMTSortAST = Any + type SMTSymbolRefAST = Any + /** * Translate a sort AST. */ - def translateSMTSortAST(s : SSort) : Option[SMTType] = None + def translateSMTSortAST(s : SMTSortAST) : Option[SMTType] = None /** * Translate the application of a function or predicate. The @@ -100,7 +102,7 @@ trait SMTParseableTheory { * argument. */ def translateSMTOperatorAST( - sym : SymbolRef, + sym : SMTSymbolRefAST, arguments : Seq[(Int) => (IExpression, SMTType)], polarity : Int) : Option[(IExpression, SMTType)] = None diff --git a/core/src/main/scala/ap/parser/SMTSupport.scala b/core/src/main/scala/ap/parser/SMTSupport.scala new file mode 100644 index 000000000..ba3519be4 --- /dev/null +++ b/core/src/main/scala/ap/parser/SMTSupport.scala @@ -0,0 +1,21 @@ +/** + * Shared SMT helper types that are independent from concrete frontends. + */ +package ap.parser + +object SMTSupport { + + import IExpression.{Sort => TSort} + import SMTTypes._ + + def toNormalBool(s : TSort) : TSort = s match { + case TSort.MultipleValueBool => TSort.Bool + case other => other + } + + case class SMTFunctionType(arguments : List[SMTType], + result : SMTType) + + val SMTBoolVariableType : SMTFunctionType = + SMTFunctionType(List(), SMTBool) +} diff --git a/src/main/scala/ap/parser/SMTTypes.scala b/core/src/main/scala/ap/parser/SMTTypes.scala similarity index 96% rename from src/main/scala/ap/parser/SMTTypes.scala rename to core/src/main/scala/ap/parser/SMTTypes.scala index c315997fe..17dc2d3c0 100644 --- a/src/main/scala/ap/parser/SMTTypes.scala +++ b/core/src/main/scala/ap/parser/SMTTypes.scala @@ -34,7 +34,6 @@ package ap.parser; import ap.basetypes.IdealInt -import ap.DialogUtil import ap.types.Sort import ap.theories.{ADT, ModuloArithmetic, TheoryRegistry} import ap.theories.sequences.SeqTheory @@ -53,7 +52,17 @@ object SMTTypes { private val AC = Debug.AC_PARSER - import SMTParser2InputAbsy.toNormalBool + import SMTSupport.toNormalBool + + private def asString(comp : => Unit) : String = { + val out = new java.io.ByteArrayOutputStream + val ps = new java.io.PrintStream(out) + Console.withOut(ps) { + comp + } + ps.flush() + out.toString("UTF-8") + } abstract class SMTType { def toSort : Sort @@ -80,7 +89,7 @@ object SMTTypes { val theory = ExtArray(arguments map { t => toNormalBool(t.toSort) }, toNormalBool(result.toSort)) def toSort = theory.sort - def toSMTLIBString = DialogUtil asString { + def toSMTLIBString = asString { print("(Array") for (s <- arguments) { print(" ") @@ -190,7 +199,7 @@ object SMTTypes { elementType : SMTType) extends SMTType { def toSort = theory.sort override def toString = theory.toString - def toSMTLIBString = DialogUtil asString { + def toSMTLIBString = asString { print("(Seq ") print(elementType.toSMTLIBString) print(")") diff --git a/src/main/scala/ap/parser/SimpleClausifier.scala b/core/src/main/scala/ap/parser/SimpleClausifier.scala similarity index 100% rename from src/main/scala/ap/parser/SimpleClausifier.scala rename to core/src/main/scala/ap/parser/SimpleClausifier.scala diff --git a/src/main/scala/ap/parser/SimpleMiniscoper.scala b/core/src/main/scala/ap/parser/SimpleMiniscoper.scala similarity index 100% rename from src/main/scala/ap/parser/SimpleMiniscoper.scala rename to core/src/main/scala/ap/parser/SimpleMiniscoper.scala diff --git a/src/main/scala/ap/parser/Simplifier.scala b/core/src/main/scala/ap/parser/Simplifier.scala similarity index 100% rename from src/main/scala/ap/parser/Simplifier.scala rename to core/src/main/scala/ap/parser/Simplifier.scala diff --git a/src/main/scala/ap/parser/TPTPLineariser.scala b/core/src/main/scala/ap/parser/TPTPLineariser.scala similarity index 100% rename from src/main/scala/ap/parser/TPTPLineariser.scala rename to core/src/main/scala/ap/parser/TPTPLineariser.scala diff --git a/src/main/scala/ap/parser/TriggerGenerator.scala b/core/src/main/scala/ap/parser/TriggerGenerator.scala similarity index 100% rename from src/main/scala/ap/parser/TriggerGenerator.scala rename to core/src/main/scala/ap/parser/TriggerGenerator.scala diff --git a/src/main/scala/ap/proof/BindingContext.scala b/core/src/main/scala/ap/proof/BindingContext.scala similarity index 100% rename from src/main/scala/ap/proof/BindingContext.scala rename to core/src/main/scala/ap/proof/BindingContext.scala diff --git a/src/main/scala/ap/proof/ConstantFreedom.scala b/core/src/main/scala/ap/proof/ConstantFreedom.scala similarity index 100% rename from src/main/scala/ap/proof/ConstantFreedom.scala rename to core/src/main/scala/ap/proof/ConstantFreedom.scala diff --git a/src/main/scala/ap/proof/ConstraintSimplifier.scala b/core/src/main/scala/ap/proof/ConstraintSimplifier.scala similarity index 95% rename from src/main/scala/ap/proof/ConstraintSimplifier.scala rename to core/src/main/scala/ap/proof/ConstraintSimplifier.scala index a4abf37c2..def0af454 100644 --- a/src/main/scala/ap/proof/ConstraintSimplifier.scala +++ b/core/src/main/scala/ap/proof/ConstraintSimplifier.scala @@ -93,6 +93,11 @@ abstract class ConstraintSimplifier { class SimpleSimplifier(lemmas : Boolean, ground2DNF : Boolean, output : Boolean) extends ConstraintSimplifier { + + private val NullStream = + new java.io.PrintStream(new java.io.OutputStream { + def write(b : Int) : Unit = () + }) private lazy val posProver = new ExhaustiveProver(false, @@ -155,10 +160,10 @@ class SimpleSimplifier(lemmas : Boolean, ground2DNF : Boolean, output : Boolean) private def simplify(f : Conjunction, order : TermOrder) : Conjunction = Timeout.unfinishedValue(None) { println("Simplify: " + f + " (positive)") - val res = if (lemmas) Console.withOut(ap.CmdlMain.NullStream) { + val res = if (lemmas) Console.withOut(NullStream) { QuantifierElimProver(f, false, order) } else { - val tree = Console.withOut(ap.CmdlMain.NullStream) { posProver(f, order) } + val tree = Console.withOut(NullStream) { posProver(f, order) } TestProofTree.assertNormalisedTree(tree) tree.closingConstraint } @@ -169,10 +174,10 @@ class SimpleSimplifier(lemmas : Boolean, ground2DNF : Boolean, output : Boolean) private def negSimplify(f : Conjunction, order : TermOrder) : Conjunction = Timeout.unfinishedValue(None) { println("Simplify: " + f + " (negative)") - val res = if (lemmas) Console.withOut(ap.CmdlMain.NullStream) { + val res = if (lemmas) Console.withOut(NullStream) { QuantifierElimProver(f.negate, ground2DNF, order).negate } else { - val tree = Console.withOut(ap.CmdlMain.NullStream) { negProver(f.negate, order) } + val tree = Console.withOut(NullStream) { negProver(f.negate, order) } TestProofTree.assertNormalisedTree(tree) tree.closingConstraint.negate } diff --git a/src/main/scala/ap/proof/ExhaustiveProver.scala b/core/src/main/scala/ap/proof/ExhaustiveProver.scala similarity index 100% rename from src/main/scala/ap/proof/ExhaustiveProver.scala rename to core/src/main/scala/ap/proof/ExhaustiveProver.scala diff --git a/src/main/scala/ap/proof/ModelSearchProver.scala b/core/src/main/scala/ap/proof/ModelSearchProver.scala similarity index 97% rename from src/main/scala/ap/proof/ModelSearchProver.scala rename to core/src/main/scala/ap/proof/ModelSearchProver.scala index ee8ce49bc..0c12cc15a 100644 --- a/src/main/scala/ap/proof/ModelSearchProver.scala +++ b/core/src/main/scala/ap/proof/ModelSearchProver.scala @@ -326,53 +326,9 @@ class ModelSearchProver(defaultSettings : GoalSettings) { ////////////////////////////////////////////////////////////////////////////// private def verifyCertificate(cert : Certificate, - disjuncts : Seq[Conjunction]) : Boolean = { - - // verify assumptions - (cert.assumedFormulas subsetOf - (for (d <- disjuncts.iterator) yield CertFormula(d.negate)).toSet) && - // - // verify theory axioms - (true || SimpleAPI.withProver { p => - import p._ - - def traverse(c : Certificate) : Boolean = - (c match { - case BranchInferenceCertificate(inferences, _, order) => - inferences forall { - case TheoryAxiomInference(axiom, GroebnerMultiplication) => - scope { - Console.err.println("Verifying: " + axiom) - addTheory(GroebnerMultiplication) - addConclusion(axiom.toConj) - - try { - withTimeout(3000) { - ??? match { - case SimpleAPI.ProverStatus.Valid => - true - case _ => - Console.err.println("FAILED") - true - } - } - } catch { - case SimpleAPI.TimeoutException => - Console.err.println("T/O") - true - } - } - case _ => - true - } - case _ => - true - }) && - (c.subCertificates forall (traverse _)) - - traverse(cert) - }) - } + disjuncts : Seq[Conjunction]) : Boolean = + cert.assumedFormulas subsetOf + (for (d <- disjuncts.iterator) yield CertFormula(d.negate)).toSet ////////////////////////////////////////////////////////////////////////////// diff --git a/src/main/scala/ap/proof/QuantifierElimProver.scala b/core/src/main/scala/ap/proof/QuantifierElimProver.scala similarity index 100% rename from src/main/scala/ap/proof/QuantifierElimProver.scala rename to core/src/main/scala/ap/proof/QuantifierElimProver.scala diff --git a/src/main/scala/ap/proof/Vocabulary.scala b/core/src/main/scala/ap/proof/Vocabulary.scala similarity index 100% rename from src/main/scala/ap/proof/Vocabulary.scala rename to core/src/main/scala/ap/proof/Vocabulary.scala diff --git a/src/main/scala/ap/proof/certificates/BinaryCertificate.scala b/core/src/main/scala/ap/proof/certificates/BinaryCertificate.scala similarity index 100% rename from src/main/scala/ap/proof/certificates/BinaryCertificate.scala rename to core/src/main/scala/ap/proof/certificates/BinaryCertificate.scala diff --git a/src/main/scala/ap/proof/certificates/BranchInferenceCollection.scala b/core/src/main/scala/ap/proof/certificates/BranchInferenceCollection.scala similarity index 100% rename from src/main/scala/ap/proof/certificates/BranchInferenceCollection.scala rename to core/src/main/scala/ap/proof/certificates/BranchInferenceCollection.scala diff --git a/src/main/scala/ap/proof/certificates/CertFormula.scala b/core/src/main/scala/ap/proof/certificates/CertFormula.scala similarity index 100% rename from src/main/scala/ap/proof/certificates/CertFormula.scala rename to core/src/main/scala/ap/proof/certificates/CertFormula.scala diff --git a/src/main/scala/ap/proof/certificates/Certificate.scala b/core/src/main/scala/ap/proof/certificates/Certificate.scala similarity index 100% rename from src/main/scala/ap/proof/certificates/Certificate.scala rename to core/src/main/scala/ap/proof/certificates/Certificate.scala diff --git a/src/main/scala/ap/proof/certificates/CertificateOneChild.scala b/core/src/main/scala/ap/proof/certificates/CertificateOneChild.scala similarity index 100% rename from src/main/scala/ap/proof/certificates/CertificateOneChild.scala rename to core/src/main/scala/ap/proof/certificates/CertificateOneChild.scala diff --git a/src/main/scala/ap/proof/certificates/CloseCertificate.scala b/core/src/main/scala/ap/proof/certificates/CloseCertificate.scala similarity index 100% rename from src/main/scala/ap/proof/certificates/CloseCertificate.scala rename to core/src/main/scala/ap/proof/certificates/CloseCertificate.scala diff --git a/src/main/scala/ap/proof/certificates/DagCertificateConverter.scala b/core/src/main/scala/ap/proof/certificates/DagCertificateConverter.scala similarity index 100% rename from src/main/scala/ap/proof/certificates/DagCertificateConverter.scala rename to core/src/main/scala/ap/proof/certificates/DagCertificateConverter.scala diff --git a/src/main/scala/ap/proof/certificates/DotLineariser.scala b/core/src/main/scala/ap/proof/certificates/DotLineariser.scala similarity index 100% rename from src/main/scala/ap/proof/certificates/DotLineariser.scala rename to core/src/main/scala/ap/proof/certificates/DotLineariser.scala diff --git a/src/main/scala/ap/proof/certificates/LemmaBase.scala b/core/src/main/scala/ap/proof/certificates/LemmaBase.scala similarity index 100% rename from src/main/scala/ap/proof/certificates/LemmaBase.scala rename to core/src/main/scala/ap/proof/certificates/LemmaBase.scala diff --git a/src/main/scala/ap/proof/certificates/OmegaCertificate.scala b/core/src/main/scala/ap/proof/certificates/OmegaCertificate.scala similarity index 100% rename from src/main/scala/ap/proof/certificates/OmegaCertificate.scala rename to core/src/main/scala/ap/proof/certificates/OmegaCertificate.scala diff --git a/src/main/scala/ap/proof/certificates/PropCertificate.scala b/core/src/main/scala/ap/proof/certificates/PropCertificate.scala similarity index 100% rename from src/main/scala/ap/proof/certificates/PropCertificate.scala rename to core/src/main/scala/ap/proof/certificates/PropCertificate.scala diff --git a/src/main/scala/ap/proof/certificates/SplitEqCertificate.scala b/core/src/main/scala/ap/proof/certificates/SplitEqCertificate.scala similarity index 100% rename from src/main/scala/ap/proof/certificates/SplitEqCertificate.scala rename to core/src/main/scala/ap/proof/certificates/SplitEqCertificate.scala diff --git a/src/main/scala/ap/proof/certificates/StrengthenCertificate.scala b/core/src/main/scala/ap/proof/certificates/StrengthenCertificate.scala similarity index 100% rename from src/main/scala/ap/proof/certificates/StrengthenCertificate.scala rename to core/src/main/scala/ap/proof/certificates/StrengthenCertificate.scala diff --git a/src/main/scala/ap/proof/goal/AddFactsTask.scala b/core/src/main/scala/ap/proof/goal/AddFactsTask.scala similarity index 100% rename from src/main/scala/ap/proof/goal/AddFactsTask.scala rename to core/src/main/scala/ap/proof/goal/AddFactsTask.scala diff --git a/src/main/scala/ap/proof/goal/AliasAnalyser.scala b/core/src/main/scala/ap/proof/goal/AliasAnalyser.scala similarity index 100% rename from src/main/scala/ap/proof/goal/AliasAnalyser.scala rename to core/src/main/scala/ap/proof/goal/AliasAnalyser.scala diff --git a/src/main/scala/ap/proof/goal/AllQuantifierTask.scala b/core/src/main/scala/ap/proof/goal/AllQuantifierTask.scala similarity index 100% rename from src/main/scala/ap/proof/goal/AllQuantifierTask.scala rename to core/src/main/scala/ap/proof/goal/AllQuantifierTask.scala diff --git a/src/main/scala/ap/proof/goal/BetaFormulaTask.scala b/core/src/main/scala/ap/proof/goal/BetaFormulaTask.scala similarity index 100% rename from src/main/scala/ap/proof/goal/BetaFormulaTask.scala rename to core/src/main/scala/ap/proof/goal/BetaFormulaTask.scala diff --git a/src/main/scala/ap/proof/goal/BlockedFormulaTask.scala b/core/src/main/scala/ap/proof/goal/BlockedFormulaTask.scala similarity index 100% rename from src/main/scala/ap/proof/goal/BlockedFormulaTask.scala rename to core/src/main/scala/ap/proof/goal/BlockedFormulaTask.scala diff --git a/src/main/scala/ap/proof/goal/BoundStrengthenTask.scala b/core/src/main/scala/ap/proof/goal/BoundStrengthenTask.scala similarity index 100% rename from src/main/scala/ap/proof/goal/BoundStrengthenTask.scala rename to core/src/main/scala/ap/proof/goal/BoundStrengthenTask.scala diff --git a/src/main/scala/ap/proof/goal/CompoundFormulas.scala b/core/src/main/scala/ap/proof/goal/CompoundFormulas.scala similarity index 100% rename from src/main/scala/ap/proof/goal/CompoundFormulas.scala rename to core/src/main/scala/ap/proof/goal/CompoundFormulas.scala diff --git a/src/main/scala/ap/proof/goal/DivisibilityTask.scala b/core/src/main/scala/ap/proof/goal/DivisibilityTask.scala similarity index 100% rename from src/main/scala/ap/proof/goal/DivisibilityTask.scala rename to core/src/main/scala/ap/proof/goal/DivisibilityTask.scala diff --git a/src/main/scala/ap/proof/goal/EagerTask.scala b/core/src/main/scala/ap/proof/goal/EagerTask.scala similarity index 100% rename from src/main/scala/ap/proof/goal/EagerTask.scala rename to core/src/main/scala/ap/proof/goal/EagerTask.scala diff --git a/src/main/scala/ap/proof/goal/EagerTaskManager.scala b/core/src/main/scala/ap/proof/goal/EagerTaskManager.scala similarity index 100% rename from src/main/scala/ap/proof/goal/EagerTaskManager.scala rename to core/src/main/scala/ap/proof/goal/EagerTaskManager.scala diff --git a/src/main/scala/ap/proof/goal/EliminateFactsTask.scala b/core/src/main/scala/ap/proof/goal/EliminateFactsTask.scala similarity index 100% rename from src/main/scala/ap/proof/goal/EliminateFactsTask.scala rename to core/src/main/scala/ap/proof/goal/EliminateFactsTask.scala diff --git a/src/main/scala/ap/proof/goal/ExQuantifierTask.scala b/core/src/main/scala/ap/proof/goal/ExQuantifierTask.scala similarity index 100% rename from src/main/scala/ap/proof/goal/ExQuantifierTask.scala rename to core/src/main/scala/ap/proof/goal/ExQuantifierTask.scala diff --git a/src/main/scala/ap/proof/goal/FactsNormalisationTask.scala b/core/src/main/scala/ap/proof/goal/FactsNormalisationTask.scala similarity index 100% rename from src/main/scala/ap/proof/goal/FactsNormalisationTask.scala rename to core/src/main/scala/ap/proof/goal/FactsNormalisationTask.scala diff --git a/src/main/scala/ap/proof/goal/FormulaTask.scala b/core/src/main/scala/ap/proof/goal/FormulaTask.scala similarity index 100% rename from src/main/scala/ap/proof/goal/FormulaTask.scala rename to core/src/main/scala/ap/proof/goal/FormulaTask.scala diff --git a/src/main/scala/ap/proof/goal/Goal.scala b/core/src/main/scala/ap/proof/goal/Goal.scala similarity index 100% rename from src/main/scala/ap/proof/goal/Goal.scala rename to core/src/main/scala/ap/proof/goal/Goal.scala diff --git a/src/main/scala/ap/proof/goal/MatchTasks.scala b/core/src/main/scala/ap/proof/goal/MatchTasks.scala similarity index 100% rename from src/main/scala/ap/proof/goal/MatchTasks.scala rename to core/src/main/scala/ap/proof/goal/MatchTasks.scala diff --git a/src/main/scala/ap/proof/goal/NegLitClauseTask.scala b/core/src/main/scala/ap/proof/goal/NegLitClauseTask.scala similarity index 100% rename from src/main/scala/ap/proof/goal/NegLitClauseTask.scala rename to core/src/main/scala/ap/proof/goal/NegLitClauseTask.scala diff --git a/src/main/scala/ap/proof/goal/OmegaTask.scala b/core/src/main/scala/ap/proof/goal/OmegaTask.scala similarity index 100% rename from src/main/scala/ap/proof/goal/OmegaTask.scala rename to core/src/main/scala/ap/proof/goal/OmegaTask.scala diff --git a/src/main/scala/ap/proof/goal/PrioritisedTask.scala b/core/src/main/scala/ap/proof/goal/PrioritisedTask.scala similarity index 100% rename from src/main/scala/ap/proof/goal/PrioritisedTask.scala rename to core/src/main/scala/ap/proof/goal/PrioritisedTask.scala diff --git a/src/main/scala/ap/proof/goal/QuantifierTask.scala b/core/src/main/scala/ap/proof/goal/QuantifierTask.scala similarity index 100% rename from src/main/scala/ap/proof/goal/QuantifierTask.scala rename to core/src/main/scala/ap/proof/goal/QuantifierTask.scala diff --git a/src/main/scala/ap/proof/goal/SymbolWeigths.scala b/core/src/main/scala/ap/proof/goal/SymbolWeigths.scala similarity index 100% rename from src/main/scala/ap/proof/goal/SymbolWeigths.scala rename to core/src/main/scala/ap/proof/goal/SymbolWeigths.scala diff --git a/src/main/scala/ap/proof/goal/Task.scala b/core/src/main/scala/ap/proof/goal/Task.scala similarity index 100% rename from src/main/scala/ap/proof/goal/Task.scala rename to core/src/main/scala/ap/proof/goal/Task.scala diff --git a/src/main/scala/ap/proof/goal/TaskAggregator.scala b/core/src/main/scala/ap/proof/goal/TaskAggregator.scala similarity index 100% rename from src/main/scala/ap/proof/goal/TaskAggregator.scala rename to core/src/main/scala/ap/proof/goal/TaskAggregator.scala diff --git a/src/main/scala/ap/proof/goal/TaskManager.scala b/core/src/main/scala/ap/proof/goal/TaskManager.scala similarity index 100% rename from src/main/scala/ap/proof/goal/TaskManager.scala rename to core/src/main/scala/ap/proof/goal/TaskManager.scala diff --git a/src/main/scala/ap/proof/goal/UpdateConstantFreedomTask.scala b/core/src/main/scala/ap/proof/goal/UpdateConstantFreedomTask.scala similarity index 100% rename from src/main/scala/ap/proof/goal/UpdateConstantFreedomTask.scala rename to core/src/main/scala/ap/proof/goal/UpdateConstantFreedomTask.scala diff --git a/src/main/scala/ap/proof/goal/UpdateTasksTask.scala b/core/src/main/scala/ap/proof/goal/UpdateTasksTask.scala similarity index 100% rename from src/main/scala/ap/proof/goal/UpdateTasksTask.scala rename to core/src/main/scala/ap/proof/goal/UpdateTasksTask.scala diff --git a/src/main/scala/ap/proof/goal/WrappedFormulaTask.scala b/core/src/main/scala/ap/proof/goal/WrappedFormulaTask.scala similarity index 100% rename from src/main/scala/ap/proof/goal/WrappedFormulaTask.scala rename to core/src/main/scala/ap/proof/goal/WrappedFormulaTask.scala diff --git a/src/main/scala/ap/proof/theoryPlugins/Plugin.scala b/core/src/main/scala/ap/proof/theoryPlugins/Plugin.scala similarity index 100% rename from src/main/scala/ap/proof/theoryPlugins/Plugin.scala rename to core/src/main/scala/ap/proof/theoryPlugins/Plugin.scala diff --git a/src/main/scala/ap/proof/tree/AndTree.scala b/core/src/main/scala/ap/proof/tree/AndTree.scala similarity index 100% rename from src/main/scala/ap/proof/tree/AndTree.scala rename to core/src/main/scala/ap/proof/tree/AndTree.scala diff --git a/src/main/scala/ap/proof/tree/IteratingProofTreeFactory.scala b/core/src/main/scala/ap/proof/tree/IteratingProofTreeFactory.scala similarity index 100% rename from src/main/scala/ap/proof/tree/IteratingProofTreeFactory.scala rename to core/src/main/scala/ap/proof/tree/IteratingProofTreeFactory.scala diff --git a/src/main/scala/ap/proof/tree/ProofTree.scala b/core/src/main/scala/ap/proof/tree/ProofTree.scala similarity index 100% rename from src/main/scala/ap/proof/tree/ProofTree.scala rename to core/src/main/scala/ap/proof/tree/ProofTree.scala diff --git a/src/main/scala/ap/proof/tree/ProofTreeFactory.scala b/core/src/main/scala/ap/proof/tree/ProofTreeFactory.scala similarity index 100% rename from src/main/scala/ap/proof/tree/ProofTreeFactory.scala rename to core/src/main/scala/ap/proof/tree/ProofTreeFactory.scala diff --git a/src/main/scala/ap/proof/tree/ProofTreeOneChild.scala b/core/src/main/scala/ap/proof/tree/ProofTreeOneChild.scala similarity index 100% rename from src/main/scala/ap/proof/tree/ProofTreeOneChild.scala rename to core/src/main/scala/ap/proof/tree/ProofTreeOneChild.scala diff --git a/src/main/scala/ap/proof/tree/QuantifiedTree.scala b/core/src/main/scala/ap/proof/tree/QuantifiedTree.scala similarity index 100% rename from src/main/scala/ap/proof/tree/QuantifiedTree.scala rename to core/src/main/scala/ap/proof/tree/QuantifiedTree.scala diff --git a/src/main/scala/ap/proof/tree/RandomDataSource.scala b/core/src/main/scala/ap/proof/tree/RandomDataSource.scala similarity index 100% rename from src/main/scala/ap/proof/tree/RandomDataSource.scala rename to core/src/main/scala/ap/proof/tree/RandomDataSource.scala diff --git a/src/main/scala/ap/proof/tree/SimpleProofTreeFactory.scala b/core/src/main/scala/ap/proof/tree/SimpleProofTreeFactory.scala similarity index 100% rename from src/main/scala/ap/proof/tree/SimpleProofTreeFactory.scala rename to core/src/main/scala/ap/proof/tree/SimpleProofTreeFactory.scala diff --git a/src/main/scala/ap/proof/tree/StrengthenTree.scala b/core/src/main/scala/ap/proof/tree/StrengthenTree.scala similarity index 100% rename from src/main/scala/ap/proof/tree/StrengthenTree.scala rename to core/src/main/scala/ap/proof/tree/StrengthenTree.scala diff --git a/src/main/scala/ap/proof/tree/TestProofTree.scala b/core/src/main/scala/ap/proof/tree/TestProofTree.scala similarity index 100% rename from src/main/scala/ap/proof/tree/TestProofTree.scala rename to core/src/main/scala/ap/proof/tree/TestProofTree.scala diff --git a/src/main/scala/ap/proof/tree/WeakenTree.scala b/core/src/main/scala/ap/proof/tree/WeakenTree.scala similarity index 100% rename from src/main/scala/ap/proof/tree/WeakenTree.scala rename to core/src/main/scala/ap/proof/tree/WeakenTree.scala diff --git a/src/main/scala/ap/terfor/AliasStatus.scala b/core/src/main/scala/ap/terfor/AliasStatus.scala similarity index 100% rename from src/main/scala/ap/terfor/AliasStatus.scala rename to core/src/main/scala/ap/terfor/AliasStatus.scala diff --git a/src/main/scala/ap/terfor/ComputationLogger.scala b/core/src/main/scala/ap/terfor/ComputationLogger.scala similarity index 100% rename from src/main/scala/ap/terfor/ComputationLogger.scala rename to core/src/main/scala/ap/terfor/ComputationLogger.scala diff --git a/src/main/scala/ap/terfor/ConstantTerm.scala b/core/src/main/scala/ap/terfor/ConstantTerm.scala similarity index 100% rename from src/main/scala/ap/terfor/ConstantTerm.scala rename to core/src/main/scala/ap/terfor/ConstantTerm.scala diff --git a/src/main/scala/ap/terfor/Formula.scala b/core/src/main/scala/ap/terfor/Formula.scala similarity index 100% rename from src/main/scala/ap/terfor/Formula.scala rename to core/src/main/scala/ap/terfor/Formula.scala diff --git a/src/main/scala/ap/terfor/OneTerm.scala b/core/src/main/scala/ap/terfor/OneTerm.scala similarity index 100% rename from src/main/scala/ap/terfor/OneTerm.scala rename to core/src/main/scala/ap/terfor/OneTerm.scala diff --git a/src/main/scala/ap/terfor/Sorted.scala b/core/src/main/scala/ap/terfor/Sorted.scala similarity index 100% rename from src/main/scala/ap/terfor/Sorted.scala rename to core/src/main/scala/ap/terfor/Sorted.scala diff --git a/src/main/scala/ap/terfor/SortedWithOrder.scala b/core/src/main/scala/ap/terfor/SortedWithOrder.scala similarity index 100% rename from src/main/scala/ap/terfor/SortedWithOrder.scala rename to core/src/main/scala/ap/terfor/SortedWithOrder.scala diff --git a/src/main/scala/ap/terfor/TerFor.scala b/core/src/main/scala/ap/terfor/TerFor.scala similarity index 100% rename from src/main/scala/ap/terfor/TerFor.scala rename to core/src/main/scala/ap/terfor/TerFor.scala diff --git a/src/main/scala/ap/terfor/TerForConvenience.scala b/core/src/main/scala/ap/terfor/TerForConvenience.scala similarity index 100% rename from src/main/scala/ap/terfor/TerForConvenience.scala rename to core/src/main/scala/ap/terfor/TerForConvenience.scala diff --git a/src/main/scala/ap/terfor/Term.scala b/core/src/main/scala/ap/terfor/Term.scala similarity index 100% rename from src/main/scala/ap/terfor/Term.scala rename to core/src/main/scala/ap/terfor/Term.scala diff --git a/src/main/scala/ap/terfor/TermOrder.scala b/core/src/main/scala/ap/terfor/TermOrder.scala similarity index 100% rename from src/main/scala/ap/terfor/TermOrder.scala rename to core/src/main/scala/ap/terfor/TermOrder.scala diff --git a/src/main/scala/ap/terfor/VariableTerm.scala b/core/src/main/scala/ap/terfor/VariableTerm.scala similarity index 100% rename from src/main/scala/ap/terfor/VariableTerm.scala rename to core/src/main/scala/ap/terfor/VariableTerm.scala diff --git a/src/main/scala/ap/terfor/arithconj/ArithConj.scala b/core/src/main/scala/ap/terfor/arithconj/ArithConj.scala similarity index 100% rename from src/main/scala/ap/terfor/arithconj/ArithConj.scala rename to core/src/main/scala/ap/terfor/arithconj/ArithConj.scala diff --git a/src/main/scala/ap/terfor/arithconj/ModelFinder.scala b/core/src/main/scala/ap/terfor/arithconj/ModelFinder.scala similarity index 100% rename from src/main/scala/ap/terfor/arithconj/ModelFinder.scala rename to core/src/main/scala/ap/terfor/arithconj/ModelFinder.scala diff --git a/src/main/scala/ap/terfor/arithconj/ReduceWithAC.scala b/core/src/main/scala/ap/terfor/arithconj/ReduceWithAC.scala similarity index 100% rename from src/main/scala/ap/terfor/arithconj/ReduceWithAC.scala rename to core/src/main/scala/ap/terfor/arithconj/ReduceWithAC.scala diff --git a/src/main/scala/ap/terfor/conjunctions/ConjunctEliminator.scala b/core/src/main/scala/ap/terfor/conjunctions/ConjunctEliminator.scala similarity index 100% rename from src/main/scala/ap/terfor/conjunctions/ConjunctEliminator.scala rename to core/src/main/scala/ap/terfor/conjunctions/ConjunctEliminator.scala diff --git a/src/main/scala/ap/terfor/conjunctions/Conjunction.scala b/core/src/main/scala/ap/terfor/conjunctions/Conjunction.scala similarity index 100% rename from src/main/scala/ap/terfor/conjunctions/Conjunction.scala rename to core/src/main/scala/ap/terfor/conjunctions/Conjunction.scala diff --git a/src/main/scala/ap/terfor/conjunctions/IterativeClauseMatcher.scala b/core/src/main/scala/ap/terfor/conjunctions/IterativeClauseMatcher.scala similarity index 100% rename from src/main/scala/ap/terfor/conjunctions/IterativeClauseMatcher.scala rename to core/src/main/scala/ap/terfor/conjunctions/IterativeClauseMatcher.scala diff --git a/src/main/scala/ap/terfor/conjunctions/LazyConjunction.scala b/core/src/main/scala/ap/terfor/conjunctions/LazyConjunction.scala similarity index 100% rename from src/main/scala/ap/terfor/conjunctions/LazyConjunction.scala rename to core/src/main/scala/ap/terfor/conjunctions/LazyConjunction.scala diff --git a/src/main/scala/ap/terfor/conjunctions/NegatedConjunctions.scala b/core/src/main/scala/ap/terfor/conjunctions/NegatedConjunctions.scala similarity index 100% rename from src/main/scala/ap/terfor/conjunctions/NegatedConjunctions.scala rename to core/src/main/scala/ap/terfor/conjunctions/NegatedConjunctions.scala diff --git a/src/main/scala/ap/terfor/conjunctions/Quantifier.scala b/core/src/main/scala/ap/terfor/conjunctions/Quantifier.scala similarity index 100% rename from src/main/scala/ap/terfor/conjunctions/Quantifier.scala rename to core/src/main/scala/ap/terfor/conjunctions/Quantifier.scala diff --git a/src/main/scala/ap/terfor/conjunctions/ReduceWithConjunction.scala b/core/src/main/scala/ap/terfor/conjunctions/ReduceWithConjunction.scala similarity index 100% rename from src/main/scala/ap/terfor/conjunctions/ReduceWithConjunction.scala rename to core/src/main/scala/ap/terfor/conjunctions/ReduceWithConjunction.scala diff --git a/src/main/scala/ap/terfor/conjunctions/ReducerPlugin.scala b/core/src/main/scala/ap/terfor/conjunctions/ReducerPlugin.scala similarity index 100% rename from src/main/scala/ap/terfor/conjunctions/ReducerPlugin.scala rename to core/src/main/scala/ap/terfor/conjunctions/ReducerPlugin.scala diff --git a/src/main/scala/ap/terfor/conjunctions/SubsumptionRemover.scala b/core/src/main/scala/ap/terfor/conjunctions/SubsumptionRemover.scala similarity index 100% rename from src/main/scala/ap/terfor/conjunctions/SubsumptionRemover.scala rename to core/src/main/scala/ap/terfor/conjunctions/SubsumptionRemover.scala diff --git a/src/main/scala/ap/terfor/equations/ColumnSolver.scala b/core/src/main/scala/ap/terfor/equations/ColumnSolver.scala similarity index 100% rename from src/main/scala/ap/terfor/equations/ColumnSolver.scala rename to core/src/main/scala/ap/terfor/equations/ColumnSolver.scala diff --git a/src/main/scala/ap/terfor/equations/EquationConj.scala b/core/src/main/scala/ap/terfor/equations/EquationConj.scala similarity index 100% rename from src/main/scala/ap/terfor/equations/EquationConj.scala rename to core/src/main/scala/ap/terfor/equations/EquationConj.scala diff --git a/src/main/scala/ap/terfor/equations/EquationSet.scala b/core/src/main/scala/ap/terfor/equations/EquationSet.scala similarity index 100% rename from src/main/scala/ap/terfor/equations/EquationSet.scala rename to core/src/main/scala/ap/terfor/equations/EquationSet.scala diff --git a/src/main/scala/ap/terfor/equations/NegEquationConj.scala b/core/src/main/scala/ap/terfor/equations/NegEquationConj.scala similarity index 100% rename from src/main/scala/ap/terfor/equations/NegEquationConj.scala rename to core/src/main/scala/ap/terfor/equations/NegEquationConj.scala diff --git a/src/main/scala/ap/terfor/equations/ReduceWithEqs.scala b/core/src/main/scala/ap/terfor/equations/ReduceWithEqs.scala similarity index 100% rename from src/main/scala/ap/terfor/equations/ReduceWithEqs.scala rename to core/src/main/scala/ap/terfor/equations/ReduceWithEqs.scala diff --git a/src/main/scala/ap/terfor/equations/ReduceWithNegEqs.scala b/core/src/main/scala/ap/terfor/equations/ReduceWithNegEqs.scala similarity index 100% rename from src/main/scala/ap/terfor/equations/ReduceWithNegEqs.scala rename to core/src/main/scala/ap/terfor/equations/ReduceWithNegEqs.scala diff --git a/src/main/scala/ap/terfor/inequalities/FMInfsComputer.scala b/core/src/main/scala/ap/terfor/inequalities/FMInfsComputer.scala similarity index 100% rename from src/main/scala/ap/terfor/inequalities/FMInfsComputer.scala rename to core/src/main/scala/ap/terfor/inequalities/FMInfsComputer.scala diff --git a/src/main/scala/ap/terfor/inequalities/InEqConj.scala b/core/src/main/scala/ap/terfor/inequalities/InEqConj.scala similarity index 100% rename from src/main/scala/ap/terfor/inequalities/InEqConj.scala rename to core/src/main/scala/ap/terfor/inequalities/InEqConj.scala diff --git a/src/main/scala/ap/terfor/inequalities/IntervalProp.scala b/core/src/main/scala/ap/terfor/inequalities/IntervalProp.scala similarity index 100% rename from src/main/scala/ap/terfor/inequalities/IntervalProp.scala rename to core/src/main/scala/ap/terfor/inequalities/IntervalProp.scala diff --git a/src/main/scala/ap/terfor/inequalities/ReduceWithInEqs.scala b/core/src/main/scala/ap/terfor/inequalities/ReduceWithInEqs.scala similarity index 100% rename from src/main/scala/ap/terfor/inequalities/ReduceWithInEqs.scala rename to core/src/main/scala/ap/terfor/inequalities/ReduceWithInEqs.scala diff --git a/src/main/scala/ap/terfor/linearcombination/LCBlender.scala b/core/src/main/scala/ap/terfor/linearcombination/LCBlender.scala similarity index 100% rename from src/main/scala/ap/terfor/linearcombination/LCBlender.scala rename to core/src/main/scala/ap/terfor/linearcombination/LCBlender.scala diff --git a/src/main/scala/ap/terfor/linearcombination/LinearCombination.scala b/core/src/main/scala/ap/terfor/linearcombination/LinearCombination.scala similarity index 100% rename from src/main/scala/ap/terfor/linearcombination/LinearCombination.scala rename to core/src/main/scala/ap/terfor/linearcombination/LinearCombination.scala diff --git a/src/main/scala/ap/terfor/linearcombination/ScalingIterator.scala b/core/src/main/scala/ap/terfor/linearcombination/ScalingIterator.scala similarity index 100% rename from src/main/scala/ap/terfor/linearcombination/ScalingIterator.scala rename to core/src/main/scala/ap/terfor/linearcombination/ScalingIterator.scala diff --git a/src/main/scala/ap/terfor/preds/Atom.scala b/core/src/main/scala/ap/terfor/preds/Atom.scala similarity index 100% rename from src/main/scala/ap/terfor/preds/Atom.scala rename to core/src/main/scala/ap/terfor/preds/Atom.scala diff --git a/src/main/scala/ap/terfor/preds/PredConj.scala b/core/src/main/scala/ap/terfor/preds/PredConj.scala similarity index 100% rename from src/main/scala/ap/terfor/preds/PredConj.scala rename to core/src/main/scala/ap/terfor/preds/PredConj.scala diff --git a/src/main/scala/ap/terfor/preds/Predicate.scala b/core/src/main/scala/ap/terfor/preds/Predicate.scala similarity index 100% rename from src/main/scala/ap/terfor/preds/Predicate.scala rename to core/src/main/scala/ap/terfor/preds/Predicate.scala diff --git a/src/main/scala/ap/terfor/preds/ReduceWithPredLits.scala b/core/src/main/scala/ap/terfor/preds/ReduceWithPredLits.scala similarity index 100% rename from src/main/scala/ap/terfor/preds/ReduceWithPredLits.scala rename to core/src/main/scala/ap/terfor/preds/ReduceWithPredLits.scala diff --git a/src/main/scala/ap/terfor/substitutions/ComposeSubsts.scala b/core/src/main/scala/ap/terfor/substitutions/ComposeSubsts.scala similarity index 100% rename from src/main/scala/ap/terfor/substitutions/ComposeSubsts.scala rename to core/src/main/scala/ap/terfor/substitutions/ComposeSubsts.scala diff --git a/src/main/scala/ap/terfor/substitutions/ConstantSubst.scala b/core/src/main/scala/ap/terfor/substitutions/ConstantSubst.scala similarity index 100% rename from src/main/scala/ap/terfor/substitutions/ConstantSubst.scala rename to core/src/main/scala/ap/terfor/substitutions/ConstantSubst.scala diff --git a/src/main/scala/ap/terfor/substitutions/IdentitySubst.scala b/core/src/main/scala/ap/terfor/substitutions/IdentitySubst.scala similarity index 100% rename from src/main/scala/ap/terfor/substitutions/IdentitySubst.scala rename to core/src/main/scala/ap/terfor/substitutions/IdentitySubst.scala diff --git a/src/main/scala/ap/terfor/substitutions/PseudoConstantSubst.scala b/core/src/main/scala/ap/terfor/substitutions/PseudoConstantSubst.scala similarity index 100% rename from src/main/scala/ap/terfor/substitutions/PseudoConstantSubst.scala rename to core/src/main/scala/ap/terfor/substitutions/PseudoConstantSubst.scala diff --git a/src/main/scala/ap/terfor/substitutions/PseudoDivSubstitution.scala b/core/src/main/scala/ap/terfor/substitutions/PseudoDivSubstitution.scala similarity index 100% rename from src/main/scala/ap/terfor/substitutions/PseudoDivSubstitution.scala rename to core/src/main/scala/ap/terfor/substitutions/PseudoDivSubstitution.scala diff --git a/src/main/scala/ap/terfor/substitutions/SimpleSubstitution.scala b/core/src/main/scala/ap/terfor/substitutions/SimpleSubstitution.scala similarity index 100% rename from src/main/scala/ap/terfor/substitutions/SimpleSubstitution.scala rename to core/src/main/scala/ap/terfor/substitutions/SimpleSubstitution.scala diff --git a/src/main/scala/ap/terfor/substitutions/Substitution.scala b/core/src/main/scala/ap/terfor/substitutions/Substitution.scala similarity index 100% rename from src/main/scala/ap/terfor/substitutions/Substitution.scala rename to core/src/main/scala/ap/terfor/substitutions/Substitution.scala diff --git a/src/main/scala/ap/terfor/substitutions/VariableShiftSubst.scala b/core/src/main/scala/ap/terfor/substitutions/VariableShiftSubst.scala similarity index 100% rename from src/main/scala/ap/terfor/substitutions/VariableShiftSubst.scala rename to core/src/main/scala/ap/terfor/substitutions/VariableShiftSubst.scala diff --git a/src/main/scala/ap/terfor/substitutions/VariableSubst.scala b/core/src/main/scala/ap/terfor/substitutions/VariableSubst.scala similarity index 100% rename from src/main/scala/ap/terfor/substitutions/VariableSubst.scala rename to core/src/main/scala/ap/terfor/substitutions/VariableSubst.scala diff --git a/src/main/scala/ap/theories/ADT.scala b/core/src/main/scala/ap/theories/ADT.scala similarity index 99% rename from src/main/scala/ap/theories/ADT.scala rename to core/src/main/scala/ap/theories/ADT.scala index 6ffe15709..5fb30ef80 100644 --- a/src/main/scala/ap/theories/ADT.scala +++ b/core/src/main/scala/ap/theories/ADT.scala @@ -42,8 +42,7 @@ import ap.terfor.conjunctions.{Conjunction, ReduceWithConjunction, import ap.terfor.{TermOrder, TerForConvenience, Formula, OneTerm, Term} import ap.terfor.preds.Atom import ap.terfor.substitutions.{VariableShiftSubst, VariableSubst} -import ap.{SimpleAPI, PresburgerTools} -import SimpleAPI.ProverStatus +import ap.PresburgerTools import ap.types.{Sort, ProxySort, MonoSortedIFunction, SortedPredicate, SortedConstantTerm, MonoSortedPredicate} import ap.proof.theoryPlugins.Plugin diff --git a/src/main/scala/ap/theories/BitShiftMultiplication.scala b/core/src/main/scala/ap/theories/BitShiftMultiplication.scala similarity index 100% rename from src/main/scala/ap/theories/BitShiftMultiplication.scala rename to core/src/main/scala/ap/theories/BitShiftMultiplication.scala diff --git a/src/main/scala/ap/theories/DivZero.scala b/core/src/main/scala/ap/theories/DivZero.scala similarity index 100% rename from src/main/scala/ap/theories/DivZero.scala rename to core/src/main/scala/ap/theories/DivZero.scala diff --git a/src/main/scala/ap/theories/FunctionalConsistency.scala b/core/src/main/scala/ap/theories/FunctionalConsistency.scala similarity index 100% rename from src/main/scala/ap/theories/FunctionalConsistency.scala rename to core/src/main/scala/ap/theories/FunctionalConsistency.scala diff --git a/src/main/scala/ap/theories/Incompleteness.scala b/core/src/main/scala/ap/theories/Incompleteness.scala similarity index 100% rename from src/main/scala/ap/theories/Incompleteness.scala rename to core/src/main/scala/ap/theories/Incompleteness.scala diff --git a/src/main/scala/ap/theories/MulTheory.scala b/core/src/main/scala/ap/theories/MulTheory.scala similarity index 100% rename from src/main/scala/ap/theories/MulTheory.scala rename to core/src/main/scala/ap/theories/MulTheory.scala diff --git a/src/main/scala/ap/theories/SaturationProcedure.scala b/core/src/main/scala/ap/theories/SaturationProcedure.scala similarity index 100% rename from src/main/scala/ap/theories/SaturationProcedure.scala rename to core/src/main/scala/ap/theories/SaturationProcedure.scala diff --git a/src/main/scala/ap/theories/Theory.scala b/core/src/main/scala/ap/theories/Theory.scala similarity index 100% rename from src/main/scala/ap/theories/Theory.scala rename to core/src/main/scala/ap/theories/Theory.scala diff --git a/src/main/scala/ap/theories/TheoryBuilder.scala b/core/src/main/scala/ap/theories/TheoryBuilder.scala similarity index 100% rename from src/main/scala/ap/theories/TheoryBuilder.scala rename to core/src/main/scala/ap/theories/TheoryBuilder.scala diff --git a/src/main/scala/ap/theories/TheoryCollector.scala b/core/src/main/scala/ap/theories/TheoryCollector.scala similarity index 100% rename from src/main/scala/ap/theories/TheoryCollector.scala rename to core/src/main/scala/ap/theories/TheoryCollector.scala diff --git a/src/main/scala/ap/theories/TheoryRegistry.scala b/core/src/main/scala/ap/theories/TheoryRegistry.scala similarity index 100% rename from src/main/scala/ap/theories/TheoryRegistry.scala rename to core/src/main/scala/ap/theories/TheoryRegistry.scala diff --git a/src/main/scala/ap/theories/ValueEnumerator.scala b/core/src/main/scala/ap/theories/ValueEnumerator.scala similarity index 100% rename from src/main/scala/ap/theories/ValueEnumerator.scala rename to core/src/main/scala/ap/theories/ValueEnumerator.scala diff --git a/src/main/scala/ap/theories/arrays/CombArray.scala b/core/src/main/scala/ap/theories/arrays/CombArray.scala similarity index 100% rename from src/main/scala/ap/theories/arrays/CombArray.scala rename to core/src/main/scala/ap/theories/arrays/CombArray.scala diff --git a/src/main/scala/ap/theories/arrays/ExtArray.scala b/core/src/main/scala/ap/theories/arrays/ExtArray.scala similarity index 100% rename from src/main/scala/ap/theories/arrays/ExtArray.scala rename to core/src/main/scala/ap/theories/arrays/ExtArray.scala diff --git a/src/main/scala/ap/theories/arrays/MinMaxArray.scala b/core/src/main/scala/ap/theories/arrays/MinMaxArray.scala similarity index 100% rename from src/main/scala/ap/theories/arrays/MinMaxArray.scala rename to core/src/main/scala/ap/theories/arrays/MinMaxArray.scala diff --git a/src/main/scala/ap/theories/arrays/SetTheory.scala b/core/src/main/scala/ap/theories/arrays/SetTheory.scala similarity index 100% rename from src/main/scala/ap/theories/arrays/SetTheory.scala rename to core/src/main/scala/ap/theories/arrays/SetTheory.scala diff --git a/src/main/scala/ap/theories/arrays/SimpleArray.scala b/core/src/main/scala/ap/theories/arrays/SimpleArray.scala similarity index 100% rename from src/main/scala/ap/theories/arrays/SimpleArray.scala rename to core/src/main/scala/ap/theories/arrays/SimpleArray.scala diff --git a/src/main/scala/ap/theories/bitvectors/ExtractArithEncoder.scala b/core/src/main/scala/ap/theories/bitvectors/ExtractArithEncoder.scala similarity index 100% rename from src/main/scala/ap/theories/bitvectors/ExtractArithEncoder.scala rename to core/src/main/scala/ap/theories/bitvectors/ExtractArithEncoder.scala diff --git a/src/main/scala/ap/theories/bitvectors/ModCastSplitter.scala b/core/src/main/scala/ap/theories/bitvectors/ModCastSplitter.scala similarity index 100% rename from src/main/scala/ap/theories/bitvectors/ModCastSplitter.scala rename to core/src/main/scala/ap/theories/bitvectors/ModCastSplitter.scala diff --git a/src/main/scala/ap/theories/bitvectors/ModPlugin.scala b/core/src/main/scala/ap/theories/bitvectors/ModPlugin.scala similarity index 100% rename from src/main/scala/ap/theories/bitvectors/ModPlugin.scala rename to core/src/main/scala/ap/theories/bitvectors/ModPlugin.scala diff --git a/src/main/scala/ap/theories/bitvectors/ModPostprocessor.scala b/core/src/main/scala/ap/theories/bitvectors/ModPostprocessor.scala similarity index 100% rename from src/main/scala/ap/theories/bitvectors/ModPostprocessor.scala rename to core/src/main/scala/ap/theories/bitvectors/ModPostprocessor.scala diff --git a/src/main/scala/ap/theories/bitvectors/ModPreprocessor.scala b/core/src/main/scala/ap/theories/bitvectors/ModPreprocessor.scala similarity index 100% rename from src/main/scala/ap/theories/bitvectors/ModPreprocessor.scala rename to core/src/main/scala/ap/theories/bitvectors/ModPreprocessor.scala diff --git a/src/main/scala/ap/theories/bitvectors/ModReducer.scala b/core/src/main/scala/ap/theories/bitvectors/ModReducer.scala similarity index 100% rename from src/main/scala/ap/theories/bitvectors/ModReducer.scala rename to core/src/main/scala/ap/theories/bitvectors/ModReducer.scala diff --git a/src/main/scala/ap/theories/bitvectors/ModuloArithmetic.scala b/core/src/main/scala/ap/theories/bitvectors/ModuloArithmetic.scala similarity index 100% rename from src/main/scala/ap/theories/bitvectors/ModuloArithmetic.scala rename to core/src/main/scala/ap/theories/bitvectors/ModuloArithmetic.scala diff --git a/src/main/scala/ap/theories/bitvectors/Ring.scala b/core/src/main/scala/ap/theories/bitvectors/Ring.scala similarity index 100% rename from src/main/scala/ap/theories/bitvectors/Ring.scala rename to core/src/main/scala/ap/theories/bitvectors/Ring.scala diff --git a/src/main/scala/ap/theories/bitvectors/ShiftCastSplitter.scala b/core/src/main/scala/ap/theories/bitvectors/ShiftCastSplitter.scala similarity index 100% rename from src/main/scala/ap/theories/bitvectors/ShiftCastSplitter.scala rename to core/src/main/scala/ap/theories/bitvectors/ShiftCastSplitter.scala diff --git a/src/main/scala/ap/theories/heaps/ArrayHeap.scala b/core/src/main/scala/ap/theories/heaps/ArrayHeap.scala similarity index 100% rename from src/main/scala/ap/theories/heaps/ArrayHeap.scala rename to core/src/main/scala/ap/theories/heaps/ArrayHeap.scala diff --git a/src/main/scala/ap/theories/heaps/Heap.scala b/core/src/main/scala/ap/theories/heaps/Heap.scala similarity index 100% rename from src/main/scala/ap/theories/heaps/Heap.scala rename to core/src/main/scala/ap/theories/heaps/Heap.scala diff --git a/src/main/scala/ap/theories/heaps/NativeHeap.scala b/core/src/main/scala/ap/theories/heaps/NativeHeap.scala similarity index 100% rename from src/main/scala/ap/theories/heaps/NativeHeap.scala rename to core/src/main/scala/ap/theories/heaps/NativeHeap.scala diff --git a/src/main/scala/ap/theories/nia/Buchberger.scala b/core/src/main/scala/ap/theories/nia/Buchberger.scala similarity index 100% rename from src/main/scala/ap/theories/nia/Buchberger.scala rename to core/src/main/scala/ap/theories/nia/Buchberger.scala diff --git a/core/src/main/scala/ap/theories/nia/Gaussian.scala b/core/src/main/scala/ap/theories/nia/Gaussian.scala new file mode 100644 index 000000000..b808a4aa3 --- /dev/null +++ b/core/src/main/scala/ap/theories/nia/Gaussian.scala @@ -0,0 +1,163 @@ +/** + * This file is part of Princess, a theorem prover for Presburger + * arithmetic with uninterpreted predicates. + * + * + * Copyright (C) 2014-2019 Philipp Ruemmer + * 2014 Peter Backeman + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * * Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * * Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * * Neither the name of the authors nor the names of their + * contributors may be used to endorse or promote products derived from + * this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +package ap.theories.nia + +import ap.basetypes.{IdealInt, IdealRat} +import ap.util.LRUCache + +import scala.collection.immutable.BitSet + + +object Gaussian { + private val cache = new LRUCache[Vector[Vector[IdealInt]], + List[(Array[IdealInt], BitSet)]](3) + + def apply(array : Vector[Vector[IdealInt]]) = + cache(array) { (new Gaussian(array)).getRows } +} + + +// Assuming rectangular matrix +class Gaussian private (array : Vector[Vector[IdealInt]]) { + val rows = array.length + val cols = array(0).length + + override def toString : String = + (for (a <- array) yield a.mkString(" ")).mkString("\n") + + /** + * Reduced linear rows with the originating row labels. + */ + val getRows : List[(Array[IdealInt], BitSet)] = { + val matrix = Array.tabulate(rows) { r => + Array.tabulate(cols) { c => IdealRat(array(r)(c)) } + } + val rowComb = Array.tabulate(rows) { r => + Array.tabulate(rows) { c => + if (r == c) IdealRat.ONE else IdealRat.ZERO + } + } + + var pivotRow = 0 + var col = 0 + + while (pivotRow < rows && col < cols) { + var pivot = pivotRow + while (pivot < rows && matrix(pivot)(col).isZero) + pivot += 1 + + if (pivot < rows) { + if (pivot != pivotRow) { + val tmp = matrix(pivotRow); matrix(pivotRow) = matrix(pivot); matrix(pivot) = tmp + val ctmp = rowComb(pivotRow); rowComb(pivotRow) = rowComb(pivot); rowComb(pivot) = ctmp + } + + val pivotValue = matrix(pivotRow)(col) + var c = col + while (c < cols) { + matrix(pivotRow)(c) = matrix(pivotRow)(c) / pivotValue + c += 1 + } + var l = 0 + while (l < rows) { + rowComb(pivotRow)(l) = rowComb(pivotRow)(l) / pivotValue + l += 1 + } + + var r = 0 + while (r < rows) { + if (r != pivotRow) { + val factor = matrix(r)(col) + if (!factor.isZero) { + c = col + while (c < cols) { + matrix(r)(c) = matrix(r)(c) - (factor * matrix(pivotRow)(c)) + c += 1 + } + l = 0 + while (l < rows) { + rowComb(r)(l) = rowComb(r)(l) - (factor * rowComb(pivotRow)(l)) + l += 1 + } + } + } + r += 1 + } + + pivotRow += 1 + } + + col += 1 + } + + (for { + r <- 0 until rows + row = normaliseRow(matrix(r)) + if row.exists(x => !x.isZero) + label = BitSet() ++ + (for (i <- 0 until rows; + if !rowComb(r)(i).isZero) + yield i) + } yield (row, label)).toList + } + + private def normaliseRow(row : Array[IdealRat]) : Array[IdealInt] = { + if (row.forall(_.isZero)) + return Array.fill(cols)(IdealInt.ZERO) + + val lcmDenom = + IdealInt.lcm(for (x <- row.iterator; if !x.isZero) yield x.denom) + + val intRow = + Array.tabulate(cols) { i => + val x = row(i) + if (x.isZero) IdealInt.ZERO else x.num * (lcmDenom / x.denom) + } + + val gcdAbs = + IdealInt.gcd(for (x <- intRow.iterator; if !x.isZero) yield x.abs) + + if (!gcdAbs.isZero && !gcdAbs.isOne) + for (i <- 0 until cols) + intRow(i) = intRow(i) / gcdAbs + + val firstNZ = intRow.find(x => !x.isZero) + if (firstNZ.exists(_.signum < 0)) + for (i <- 0 until cols) + intRow(i) = -intRow(i) + + intRow + } +} diff --git a/src/main/scala/ap/theories/nia/GroebnerMultiplication.scala b/core/src/main/scala/ap/theories/nia/GroebnerMultiplication.scala similarity index 100% rename from src/main/scala/ap/theories/nia/GroebnerMultiplication.scala rename to core/src/main/scala/ap/theories/nia/GroebnerMultiplication.scala diff --git a/src/main/scala/ap/theories/nia/Interval.scala b/core/src/main/scala/ap/theories/nia/Interval.scala similarity index 100% rename from src/main/scala/ap/theories/nia/Interval.scala rename to core/src/main/scala/ap/theories/nia/Interval.scala diff --git a/src/main/scala/ap/theories/nia/IntervalPropagator.scala b/core/src/main/scala/ap/theories/nia/IntervalPropagator.scala similarity index 100% rename from src/main/scala/ap/theories/nia/IntervalPropagator.scala rename to core/src/main/scala/ap/theories/nia/IntervalPropagator.scala diff --git a/src/main/scala/ap/theories/nia/Polynomial.scala b/core/src/main/scala/ap/theories/nia/Polynomial.scala similarity index 100% rename from src/main/scala/ap/theories/nia/Polynomial.scala rename to core/src/main/scala/ap/theories/nia/Polynomial.scala diff --git a/src/main/scala/ap/theories/nia/Splitter.scala b/core/src/main/scala/ap/theories/nia/Splitter.scala similarity index 100% rename from src/main/scala/ap/theories/nia/Splitter.scala rename to core/src/main/scala/ap/theories/nia/Splitter.scala diff --git a/src/main/scala/ap/theories/package.scala b/core/src/main/scala/ap/theories/package.scala similarity index 100% rename from src/main/scala/ap/theories/package.scala rename to core/src/main/scala/ap/theories/package.scala diff --git a/src/main/scala/ap/theories/rationals/Fractions.scala b/core/src/main/scala/ap/theories/rationals/Fractions.scala similarity index 100% rename from src/main/scala/ap/theories/rationals/Fractions.scala rename to core/src/main/scala/ap/theories/rationals/Fractions.scala diff --git a/src/main/scala/ap/theories/rationals/Rationals.scala b/core/src/main/scala/ap/theories/rationals/Rationals.scala similarity index 100% rename from src/main/scala/ap/theories/rationals/Rationals.scala rename to core/src/main/scala/ap/theories/rationals/Rationals.scala diff --git a/src/main/scala/ap/theories/sequences/ArraySeqTheory.scala b/core/src/main/scala/ap/theories/sequences/ArraySeqTheory.scala similarity index 100% rename from src/main/scala/ap/theories/sequences/ArraySeqTheory.scala rename to core/src/main/scala/ap/theories/sequences/ArraySeqTheory.scala diff --git a/src/main/scala/ap/theories/sequences/ArraySeqTheoryBuilder.scala b/core/src/main/scala/ap/theories/sequences/ArraySeqTheoryBuilder.scala similarity index 100% rename from src/main/scala/ap/theories/sequences/ArraySeqTheoryBuilder.scala rename to core/src/main/scala/ap/theories/sequences/ArraySeqTheoryBuilder.scala diff --git a/src/main/scala/ap/theories/sequences/SeqTheory.scala b/core/src/main/scala/ap/theories/sequences/SeqTheory.scala similarity index 100% rename from src/main/scala/ap/theories/sequences/SeqTheory.scala rename to core/src/main/scala/ap/theories/sequences/SeqTheory.scala diff --git a/src/main/scala/ap/theories/sequences/SeqTheoryBuilder.scala b/core/src/main/scala/ap/theories/sequences/SeqTheoryBuilder.scala similarity index 100% rename from src/main/scala/ap/theories/sequences/SeqTheoryBuilder.scala rename to core/src/main/scala/ap/theories/sequences/SeqTheoryBuilder.scala diff --git a/src/main/scala/ap/theories/strings/AbstractStringTheory.scala b/core/src/main/scala/ap/theories/strings/AbstractStringTheory.scala similarity index 100% rename from src/main/scala/ap/theories/strings/AbstractStringTheory.scala rename to core/src/main/scala/ap/theories/strings/AbstractStringTheory.scala diff --git a/src/main/scala/ap/theories/strings/SeqStringTheory.scala b/core/src/main/scala/ap/theories/strings/SeqStringTheory.scala similarity index 100% rename from src/main/scala/ap/theories/strings/SeqStringTheory.scala rename to core/src/main/scala/ap/theories/strings/SeqStringTheory.scala diff --git a/src/main/scala/ap/theories/strings/SeqStringTheoryBuilder.scala b/core/src/main/scala/ap/theories/strings/SeqStringTheoryBuilder.scala similarity index 100% rename from src/main/scala/ap/theories/strings/SeqStringTheoryBuilder.scala rename to core/src/main/scala/ap/theories/strings/SeqStringTheoryBuilder.scala diff --git a/src/main/scala/ap/theories/strings/StringTheory.scala b/core/src/main/scala/ap/theories/strings/StringTheory.scala similarity index 100% rename from src/main/scala/ap/theories/strings/StringTheory.scala rename to core/src/main/scala/ap/theories/strings/StringTheory.scala diff --git a/src/main/scala/ap/theories/strings/StringTheoryBuilder.scala b/core/src/main/scala/ap/theories/strings/StringTheoryBuilder.scala similarity index 100% rename from src/main/scala/ap/theories/strings/StringTheoryBuilder.scala rename to core/src/main/scala/ap/theories/strings/StringTheoryBuilder.scala diff --git a/src/main/scala/ap/types/Sort.scala b/core/src/main/scala/ap/types/Sort.scala similarity index 100% rename from src/main/scala/ap/types/Sort.scala rename to core/src/main/scala/ap/types/Sort.scala diff --git a/src/main/scala/ap/types/SortedSymbols.scala b/core/src/main/scala/ap/types/SortedSymbols.scala similarity index 100% rename from src/main/scala/ap/types/SortedSymbols.scala rename to core/src/main/scala/ap/types/SortedSymbols.scala diff --git a/src/main/scala/ap/types/TypeTheory.scala b/core/src/main/scala/ap/types/TypeTheory.scala similarity index 100% rename from src/main/scala/ap/types/TypeTheory.scala rename to core/src/main/scala/ap/types/TypeTheory.scala diff --git a/src/main/scala/ap/types/UninterpretedSort.scala b/core/src/main/scala/ap/types/UninterpretedSort.scala similarity index 100% rename from src/main/scala/ap/types/UninterpretedSort.scala rename to core/src/main/scala/ap/types/UninterpretedSort.scala diff --git a/src/main/scala/ap/util/OpCounters.scala b/core/src/main/scala/ap/util/OpCounters.scala similarity index 100% rename from src/main/scala/ap/util/OpCounters.scala rename to core/src/main/scala/ap/util/OpCounters.scala diff --git a/src/main/scala/ap/util/Timer.scala b/core/src/main/scala/ap/util/Timer.scala similarity index 100% rename from src/main/scala/ap/util/Timer.scala rename to core/src/main/scala/ap/util/Timer.scala diff --git a/core/src/test/scala/ap/core/ImplicationCheckerTest.scala b/core/src/test/scala/ap/core/ImplicationCheckerTest.scala new file mode 100644 index 000000000..80d364bfb --- /dev/null +++ b/core/src/test/scala/ap/core/ImplicationCheckerTest.scala @@ -0,0 +1,46 @@ +package ap.core + +import ap.parser.IExpression._ +import ap.terfor.ConstantTerm + +import org.scalacheck.Properties + +class ImplicationCheckerTest extends Properties("ImplicationChecker") { + + private def c(name : String) = new ConstantTerm(name) + + property("decrease-is-strict") = { + val n = c("n") + ImplicationChecker.implies( + Seq(i(n) > 0), + i(n) - 1 < i(n) + ) + } + + property("decrease-keeps-nonnegative") = { + val current = c("current") + val next = c("next") + ImplicationChecker.implies( + Seq(i(current) > 0, + i(next) === i(current) - 1), + i(next) >= 0 + ) + } + + property("invalid-implication-is-rejected") = { + val n = c("n") + !ImplicationChecker.implies( + Seq(i(n) >= 0), + i(n) - 1 >= 0 + ) + } + + property("strict-upper-bound-step") = { + val iVar = c("i") + val hi = c("hi") + ImplicationChecker.implies( + Seq(i(iVar) < i(hi)), + i(iVar) + 1 <= i(hi) + ) + } +} diff --git a/docs/scala-js-migration-plan.md b/docs/scala-js-migration-plan.md new file mode 100644 index 000000000..444019036 --- /dev/null +++ b/docs/scala-js-migration-plan.md @@ -0,0 +1,407 @@ +# Scala.js Migration Plan for Princess + +Date: 2026-02-22 + +## Goal and scope + +This document lists **blocking issues** to run Princess on Scala.js, evaluates moving parsing to a pure-Scala parser (cats-parse), and proposes a phased work schedule. + +Assumptions used for this plan: + +- Primary target is a Scala.js library build (browser and/or Node), not a JVM CLI binary. +- Required minimum feature set for first usable Scala.js release: + - parse SMT-LIB from strings/readers, + - run core solving APIs, + - expose results without JVM threads/queues. +- JVM-only entry points (CLI, Swing UI, daemon server, portfolio multi-threading) can remain JVM modules. + +## Executive summary + +The largest blockers are: + +1. Parser stack depends on generated Java/CUP/JFlex parsers and JVM jars. +2. Core API execution model depends on JVM threads and blocking queues. +3. Build is not set up as a Scala.js cross-project and uses JVM-only dependency wiring. +4. Core code has coupling to `CmdlMain` (CLI object), which drags JVM-only code into library paths. + +A realistic path is: + +- split into `core` (cross JVM/JS) and `jvm-app` modules, +- replace SMT-LIB and Princess parsers with cats-parse (or equivalent pure Scala parser), +- replace `Thread`/`LinkedBlockingQueue`/`ConcurrentHashMap` usage in shared code with Scala.js-safe primitives, +- keep CLI/server/GUI/portfolio parallel execution in JVM-only module. + +## Blocking issues + +### B1. Build architecture is JVM-only + +**Evidence** + +- `build.sbt:73-90` wires `parser` and `smt-parser` subprojects around prebuilt JVM jars. +- `build.sbt:95-99` makes root depend on those parser subprojects. +- `build.sbt:112-116` adds JVM `java-cup-runtime` and JVM dependency style (`%%`) for parser-combinators. +- `project/assembly.sbt:1-2` has assembly/native-image setup, but no Scala.js plugin/cross-project setup. + +**Why this blocks Scala.js** + +Scala.js cannot consume JVM bytecode parser jars (`parser.jar`, `smt-parser.jar`) as source-level JS-compatible code. + +**Required action** + +- Introduce cross-project layout (`coreJVM/coreJS`). +- Remove parser-jar dependency from shared module. +- Add Scala.js plugin and JS-specific dependency coordinates (`%%%` where needed). + +--- + +### B2. SMT-LIB parser is generated Java (BNFC + CUP + JFlex) + +**Evidence** + +- `smt-parser/Makefile:18-36` generates Java lexer/parser with BNFC/CUP/JFlex. +- `src/main/scala/ap/parser/SMTParser2InputAbsy.scala:57-58` imports generated `ap.parser.smtlib` AST/parser classes. +- `src/main/scala/ap/parser/SMTParser2InputAbsy.scala:229-230` instantiates generated `Yylex` and `parser`. +- `src/main/scala/ap/parser/SMTParsingUtils.scala:37-38` imports generated classes; `:47-48` uses generated parser. +- `src/main/scala/ap/parser/SMTParseableTheory.scala:37` and `:95-106` expose generated AST types in extension interfaces. + +**Why this blocks Scala.js** + +Generated parser/AST classes are Java bytecode and JVM runtime dependent. + +**Required action** + +- Replace with pure Scala parser implementation (cats-parse recommended). +- Define Scala AST model and remove/bridge `smtlib.Absyn.*` from shared interfaces. + +--- + +### B3. Princess `.pri` parser is generated Java (BNFC + CUP + JFlex) + +**Evidence** + +- `parser/Makefile:34-50` generates Java lexer/parser and classes. +- `src/main/scala/ap/parser/ApParser2InputAbsy.scala:46-47` imports generated `ap.parser.ap_input.*` classes. +- `src/main/scala/ap/parser/ApParser2InputAbsy.scala:87-88` uses generated `Yylex` and `parser`. + +**Why this blocks Scala.js** + +Same root issue as SMT-LIB parser: JVM generated parser stack. + +**Required action** + +- Port `.pri` grammar to pure Scala parser (cats-parse). +- Keep translator logic but retarget it to pure Scala AST. + +--- + +### B4. Core solving API uses JVM threading + blocking queues + +**Evidence** + +- `src/main/scala/ap/api/SimpleAPI.scala:58` imports `LinkedBlockingQueue` and `TimeUnit`. +- `src/main/scala/ap/api/SimpleAPI.scala:4462-4475` creates blocking queues and a dedicated `Thread`. +- `src/main/scala/ap/api/SimpleAPI.scala:2144-2147` calls blocking/polling queue methods. +- `src/main/scala/ap/api/ProofThread.scala:44` imports `LinkedBlockingQueue`; `:104` uses `.take`. + +**Why this blocks Scala.js** + +Scala.js has no JVM threads or blocking queue semantics. + +**Required action** + +- Replace proof-thread command loop with Scala.js-safe async model (Future/Promise/event loop), or a synchronous single-thread mode with explicit async wrapper. + +--- + +### B5. Additional JVM concurrency primitives in shared/near-shared code + +**Evidence** + +- `src/main/scala/ap/util/OpCounters.scala:40-41` uses `ConcurrentHashMap` and `LongAdder`. +- `src/main/scala/ap/util/Timer.scala:39` imports `java.lang.Thread` and checks thread identity at `:87-88`. +- `src/main/scala/ap/ParallelFileProver.scala:44,47,492` uses `SyncVar`, blocking queues, and threads. +- `src/main/scala/ap/ServerMain.scala:39,95` uses `Semaphore` and threads. +- `src/main/scala/ap/interpolants/WolverineInterface.scala:39,111,148` uses `Executors` and `Await.result`. + +**Why this blocks Scala.js** + +These APIs are JVM-only or rely on blocking semantics not available in Scala.js. + +**Required action** + +- In shared code: replace with Scala collections + `Future`/`Promise` primitives. +- Move server/portfolio/daemon behavior to JVM-only modules. + +--- + +### B6. Core code is coupled to CLI object (`CmdlMain`) + +**Evidence** + +- `src/main/scala/ap/api/SimpleAPI.scala:66` references `CmdlMain.version`. +- `src/main/scala/ap/api/SimpleAPI.scala:2425` calls `CmdlMain.doPrintTextCertificate`. +- `src/main/scala/ap/parser/SMTParser2InputAbsy.scala:1591,1597` uses `CmdlMain.printGreeting/version`. +- `src/main/scala/ap/proof/ConstraintSimplifier.scala:158,161` uses `CmdlMain.NullStream`. +- `src/main/scala/ap/theories/nia/Gaussian.scala:73` uses `CmdlMain.NullStream`. + +**Why this blocks Scala.js** + +`CmdlMain` is CLI-centric and includes JVM file/process style logic. This coupling prevents clean `core` extraction. + +**Required action** + +- Extract shared constants/utilities (`version`, null output stream, certificate formatting facade) into platform-neutral modules. +- Keep CLI wiring in JVM module. + +--- + +### B7. File/network/UI features are JVM-specific and must be isolated + +**Evidence** + +- `src/main/scala/ap/CmdlMain.scala:267,288,379,1039` uses `FileOutputStream`/`FileReader`. +- `src/main/scala/ap/JavaWrapper.scala:82-86` uses `java.io.File`/`FileReader`. +- `src/main/scala/ap/parser/TPTPTParser.scala:1384-1387` resolves includes via env var + `FileReader`. +- `src/main/scala/ap/ServerMain.scala:41,64` uses `java.net.ServerSocket`. +- `src/main/scala/ap/DialogMain.scala:44-46` uses Swing/AWT. + +**Why this blocks Scala.js** + +No JVM filesystem/socket/Swing in Scala.js runtime. + +**Required action** + +- Put these features in JVM-only modules. +- For JS, expose string/reader-based APIs and optional host callbacks for include/file resolution. + +--- + +### B8. Scala version baseline needs simplification for Scala.js work + +**Evidence** + +- `build.sbt:56-57` cross-builds `2.11.12` and `2.12.20`. + +**Why this blocks or slows migration** + +Practical Scala.js migration + modern parser libraries is significantly easier if shared code targets one modern Scala line (at least 2.12, usually 2.13+). + +**Required action** + +- Drop 2.11 in shared module migration branch. +- Stabilize on one Scala line for cross-platform core during migration. + +## Parser migration evaluation (cats-parse) + +## Current parser landscape + +- SMT-LIB: Java-generated parser + Java-generated AST + large Scala translator (`SMTParser2InputAbsy.scala`, ~4.4k LOC). +- Princess `.pri`: Java-generated parser + AST + large translator (`ApParser2InputAbsy.scala`, ~1.3k LOC). +- TPTP: already pure Scala parser combinators (`TPTPTParser.scala`), but with JVM file-include behavior. + +## Why cats-parse is a good fit + +- Pure Scala, Scala.js compatible. +- Fine-grained control over lexical and syntactic layers. +- Deterministic behavior and explicit error reporting. +- Avoids generated Java artifacts and Java collection bridging. + +## Major migration design choices + +### Choice 1: AST compatibility vs direct translation + +- **AST compatibility approach (recommended first)**: + - create pure Scala ASTs matching current translator expectations, + - keep most semantic translation logic in place, + - reduces churn and regression risk. +- **Direct translation approach**: + - parse directly into `IExpression`/internal forms, + - less intermediate AST code long-term, + - much higher short-term risk and rewrite cost. + +### Choice 2: TPTP parser now vs later + +- Keep existing TPTP parser-combinators initially and only isolate file include (`include(...)`) behind callback. +- Optional later migration of TPTP to cats-parse for uniformity/performance. + +## Estimated effort for parser migration + +- SMT-LIB parser + incremental command stream parity: **3-4 weeks**. +- `.pri` parser parity: **2-3 weeks**. +- TPTP parser port to cats-parse (optional): **1-2 weeks**. + +## Concurrency migration evaluation (Scala.js-safe primitives) + +## Current model + +- `SimpleAPI` offloads solving to a dedicated JVM thread and communicates through blocking queues. +- External API offers polling/blocking status retrieval. + +## Scala.js-safe replacement options + +### Option A: Synchronous core + async facade (recommended) + +- Core solver runs synchronously in same thread. +- JS facade exposes `Future`-based API for host integration. +- In browser, run solver in a Web Worker for responsiveness. + +Pros: + +- Minimal invasive changes to solver internals. +- Clear separation between solver determinism and host scheduling. + +Cons: + +- Some `SimpleAPI` status semantics (`Running`, blocking `getStatus(true)`) need adaptation/deprecation in JS profile. + +### Option B: Fully async command loop in shared code + +- Reimplement command processing as Promise/Future mailbox. + +Pros: + +- Closer to current command architecture. + +Cons: + +- More complexity without true parallelism in Scala.js. + +## Concrete replacements + +- `Thread` + `LinkedBlockingQueue` -> `Future`/`Promise` + immutable/mutable queue in event loop. +- `poll(timeout, TimeUnit)` -> deadline-aware Future composition (no blocking). +- `ConcurrentHashMap`/`LongAdder` -> plain mutable map counters in JS/shared path. +- `Await.result` -> non-blocking Future chains. + +## Proposed target architecture + +- `princess-core` (cross JVM/JS): + - solver core, + - parser frontends (pure Scala), + - shared utilities, + - cross-platform API surface. +- `princess-jvm-app` (JVM only): + - `CmdlMain`, `ServerMain`, `DialogMain`, `ParallelFileProver`, `JavaWrapper`, warmup/daemon features. +- `princess-js` (JS only wrappers): + - JS-friendly entrypoints, + - worker integration helpers, + - optional include/file resolver callbacks. + +## Detailed work plan and schedule + +Schedule below assumes **2 engineers full-time** and aims for a first JS release in ~10 weeks. + +### Phase 0 (Week 1): migration scaffolding and decisions + +Deliverables: + +- Define target runtime matrix (browser, Node, or both). +- Create module split (`core` cross-project + JVM app module). +- Add Scala.js build plumbing and first empty JS compile target. + +Exit criteria: + +- `coreJS` compiles with a minimal placeholder API. +- JVM app still builds unchanged. + +### Phase 1 (Weeks 2-3): decouple core from JVM app objects + +Tasks: + +- Remove direct references from core to `CmdlMain` (`SimpleAPI`, parser get-info path, simplifier, gaussian). +- Introduce shared constants/util abstractions. +- Move clearly JVM-only files to JVM module (CLI/server/gui/portfolio wrappers). + +Exit criteria: + +- Shared module has no references to JVM entrypoint classes. +- No `java.net`, Swing/AWT, or daemon/server code in shared sources. + +### Phase 2 (Weeks 3-6): parser migration to pure Scala + +Tasks: + +- Implement SMT-LIB lexer/parser in cats-parse. +- Preserve incremental SMT command processing behavior currently in `processIncrementally`. +- Implement `.pri` parser in cats-parse. +- Bridge/replace `SMTParseableTheory` AST interfaces. + +Test plan: + +- Reuse `testcases/smtlib-parser` and `testcases/adt` parser-heavy suites. +- Add parser roundtrip/error-location checks. + +Exit criteria: + +- No dependency on `parser.jar`, `smt-parser.jar`, `java-cup-runtime` in shared module. +- Parser regression suites pass at agreed threshold (>= 99% identical outputs, known deltas documented). + +### Phase 3 (Weeks 6-8): concurrency and API execution model + +Tasks: + +- Replace `SimpleAPI` proof-thread queue model with JS-safe model (recommended Option A). +- Remove blocking queue operations in shared API. +- Refactor `OpCounters` and `Timer` implementations for cross-platform compatibility. + +Test plan: + +- API behavioral tests for `checkSat` / status transitions / model extraction. +- Timeout and cancellation contract tests in JVM and JS profiles. + +Exit criteria: + +- Shared module has no `java.util.concurrent.*` usage. +- JS build exposes non-blocking API with documented semantics. + +### Phase 4 (Weeks 8-9): platform adapters and feature gating + +Tasks: + +- JVM module keeps CLI/server/portfolio behavior. +- JS module adds browser/Node adapters (input from strings; optional include resolver for TPTP). +- Explicitly gate unsupported features in JS (server daemon, Swing UI, multi-thread portfolio). + +Exit criteria: + +- Feature matrix document completed. +- JS runtime behavior for unsupported features is explicit (compile-time exclusion or clear runtime error). + +### Phase 5 (Weeks 9-10): stabilization and release prep + +Tasks: + +- Performance baseline against representative SMT-LIB workloads. +- Memory and responsiveness checks for browser worker integration. +- Documentation and migration notes for API users. + +Exit criteria: + +- Green CI for JVM + JS core builds. +- Release candidate with known-issues list. + +## Risk register and mitigations + +1. Parser parity regressions (highest risk). + - Mitigation: preserve translator behavior; run full parser corpus on each milestone. +2. API semantic drift from blocking to async model. + - Mitigation: define JS-specific status contract early and keep compatibility wrappers on JVM. +3. Hidden core/JVM coupling. + - Mitigation: enforce module boundaries in build; fail CI on forbidden package imports. +4. Browser responsiveness for heavy proofs. + - Mitigation: worker-based execution from first JS beta. + +## Acceptance criteria for “Scala.js-ready” + +- Shared core compiles/runs on Scala.js without JVM parser jars and without Java concurrency APIs. +- SMT-LIB parsing and solving works from string input in JS runtime. +- Core test subset passes in both JVM and JS pipelines. +- JVM-specific tools remain available through dedicated JVM module. + +## Immediate next actions (first 2 weeks) + +1. Create `core` cross-project and move solver/parser/shared files there. +2. Remove direct `CmdlMain` dependencies from shared code. +3. Prototype cats-parse SMT-LIB command parser for `(set-logic ...)`, `(assert ...)`, `(check-sat)`, `(exit)` plus error reporting. +4. Decide and document JS API contract (`Future`-first vs status polling emulation). + diff --git a/src/main/scala/ap/parser/SMTParser2InputAbsy.scala b/src/main/scala/ap/parser/SMTParser2InputAbsy.scala index 03eb37a90..b87a7148d 100644 --- a/src/main/scala/ap/parser/SMTParser2InputAbsy.scala +++ b/src/main/scala/ap/parser/SMTParser2InputAbsy.scala @@ -69,15 +69,13 @@ object SMTParser2InputAbsy { import IExpression.{Sort => TSort} import SMTTypes._ - protected[parser] def toNormalBool(s : TSort) : TSort = s match { - case TSort.MultipleValueBool => TSort.Bool - case s => s - } + type SMTFunctionType = SMTSupport.SMTFunctionType + val SMTFunctionType = SMTSupport.SMTFunctionType - case class SMTFunctionType(arguments : List[SMTType], - result : SMTType) + protected[parser] def toNormalBool(s : TSort) : TSort = + SMTSupport.toNormalBool(s) - val SMTBoolVariableType = SMTFunctionType(List(), SMTBool) + val SMTBoolVariableType : SMTFunctionType = SMTSupport.SMTBoolVariableType sealed abstract class VariableType case class BoundVariable(varType : SMTType) extends VariableType diff --git a/src/main/scala/ap/theories/nia/Gaussian.scala b/src/main/scala/ap/theories/nia/Gaussian.scala index 727926952..2b57d4853 100644 --- a/src/main/scala/ap/theories/nia/Gaussian.scala +++ b/src/main/scala/ap/theories/nia/Gaussian.scala @@ -36,10 +36,9 @@ package ap.theories.nia import ap.basetypes.IdealInt import ap.terfor.linearcombination.LinearCombination -import ap.terfor.{TerForConvenience, TermOrder, ConstantTerm} -import ap.terfor.preds.Atom -import ap.terfor.equations.EquationConj +import ap.terfor.ConstantTerm import ap.terfor.TerForConvenience._ +import ap.terfor.equations.EquationConj import ap.SimpleAPI import ap.parser._ import ap.util.{Debug, LRUCache} From 3a1baa01c7730eda4f0177309e2a4d74eb645eae Mon Sep 17 00:00:00 2001 From: "P. Oscar Boykin" Date: Sat, 21 Feb 2026 21:24:51 -1000 Subject: [PATCH 3/6] Checkpoint: move core-compatible tests into core module --- .../scala/ap/basetypes/TestIdealInt.scala | 0 .../scala/ap/basetypes/TestLeftistHeap.scala | 0 .../test/scala/ap/basetypes/TestSetTrie.scala | 0 .../test/scala/ap/parser/SimplePrint.scala | 0 .../ap/parser/TestInputAbsyVisitor.scala | 0 .../test/scala/ap/parser/TestSimplifier.scala | 0 .../scala/ap/proof/TestEquationSystems.scala | 0 .../scala/ap/proof/TestRandomProving.scala | 0 .../scala/ap/terfor/TestGenConjunctions.scala | 0 .../scala/ap/terfor/TestPropConnectives.scala | 0 .../test/scala/ap/terfor/TestTermOrder.scala | 0 .../ap/terfor/equations/TestEquationSet.scala | 0 .../inequalities/TestInequalities.scala | 0 .../TestLinearCombination.scala | 0 .../ap/terfor/substitutions/TestSubst.scala | 0 .../scala/ap/theories/DivModEncoding.scala | 0 core/src/test/scala/ap/util/Prop.scala | 82 +++++++++++++++++++ 17 files changed, 82 insertions(+) rename {src => core/src}/test/scala/ap/basetypes/TestIdealInt.scala (100%) rename {src => core/src}/test/scala/ap/basetypes/TestLeftistHeap.scala (100%) rename {src => core/src}/test/scala/ap/basetypes/TestSetTrie.scala (100%) rename {src => core/src}/test/scala/ap/parser/SimplePrint.scala (100%) rename {src => core/src}/test/scala/ap/parser/TestInputAbsyVisitor.scala (100%) rename {src => core/src}/test/scala/ap/parser/TestSimplifier.scala (100%) rename {src => core/src}/test/scala/ap/proof/TestEquationSystems.scala (100%) rename {src => core/src}/test/scala/ap/proof/TestRandomProving.scala (100%) rename {src => core/src}/test/scala/ap/terfor/TestGenConjunctions.scala (100%) rename {src => core/src}/test/scala/ap/terfor/TestPropConnectives.scala (100%) rename {src => core/src}/test/scala/ap/terfor/TestTermOrder.scala (100%) rename {src => core/src}/test/scala/ap/terfor/equations/TestEquationSet.scala (100%) rename {src => core/src}/test/scala/ap/terfor/inequalities/TestInequalities.scala (100%) rename {src => core/src}/test/scala/ap/terfor/linearcombination/TestLinearCombination.scala (100%) rename {src => core/src}/test/scala/ap/terfor/substitutions/TestSubst.scala (100%) rename {src => core/src}/test/scala/ap/theories/DivModEncoding.scala (100%) create mode 100644 core/src/test/scala/ap/util/Prop.scala diff --git a/src/test/scala/ap/basetypes/TestIdealInt.scala b/core/src/test/scala/ap/basetypes/TestIdealInt.scala similarity index 100% rename from src/test/scala/ap/basetypes/TestIdealInt.scala rename to core/src/test/scala/ap/basetypes/TestIdealInt.scala diff --git a/src/test/scala/ap/basetypes/TestLeftistHeap.scala b/core/src/test/scala/ap/basetypes/TestLeftistHeap.scala similarity index 100% rename from src/test/scala/ap/basetypes/TestLeftistHeap.scala rename to core/src/test/scala/ap/basetypes/TestLeftistHeap.scala diff --git a/src/test/scala/ap/basetypes/TestSetTrie.scala b/core/src/test/scala/ap/basetypes/TestSetTrie.scala similarity index 100% rename from src/test/scala/ap/basetypes/TestSetTrie.scala rename to core/src/test/scala/ap/basetypes/TestSetTrie.scala diff --git a/src/test/scala/ap/parser/SimplePrint.scala b/core/src/test/scala/ap/parser/SimplePrint.scala similarity index 100% rename from src/test/scala/ap/parser/SimplePrint.scala rename to core/src/test/scala/ap/parser/SimplePrint.scala diff --git a/src/test/scala/ap/parser/TestInputAbsyVisitor.scala b/core/src/test/scala/ap/parser/TestInputAbsyVisitor.scala similarity index 100% rename from src/test/scala/ap/parser/TestInputAbsyVisitor.scala rename to core/src/test/scala/ap/parser/TestInputAbsyVisitor.scala diff --git a/src/test/scala/ap/parser/TestSimplifier.scala b/core/src/test/scala/ap/parser/TestSimplifier.scala similarity index 100% rename from src/test/scala/ap/parser/TestSimplifier.scala rename to core/src/test/scala/ap/parser/TestSimplifier.scala diff --git a/src/test/scala/ap/proof/TestEquationSystems.scala b/core/src/test/scala/ap/proof/TestEquationSystems.scala similarity index 100% rename from src/test/scala/ap/proof/TestEquationSystems.scala rename to core/src/test/scala/ap/proof/TestEquationSystems.scala diff --git a/src/test/scala/ap/proof/TestRandomProving.scala b/core/src/test/scala/ap/proof/TestRandomProving.scala similarity index 100% rename from src/test/scala/ap/proof/TestRandomProving.scala rename to core/src/test/scala/ap/proof/TestRandomProving.scala diff --git a/src/test/scala/ap/terfor/TestGenConjunctions.scala b/core/src/test/scala/ap/terfor/TestGenConjunctions.scala similarity index 100% rename from src/test/scala/ap/terfor/TestGenConjunctions.scala rename to core/src/test/scala/ap/terfor/TestGenConjunctions.scala diff --git a/src/test/scala/ap/terfor/TestPropConnectives.scala b/core/src/test/scala/ap/terfor/TestPropConnectives.scala similarity index 100% rename from src/test/scala/ap/terfor/TestPropConnectives.scala rename to core/src/test/scala/ap/terfor/TestPropConnectives.scala diff --git a/src/test/scala/ap/terfor/TestTermOrder.scala b/core/src/test/scala/ap/terfor/TestTermOrder.scala similarity index 100% rename from src/test/scala/ap/terfor/TestTermOrder.scala rename to core/src/test/scala/ap/terfor/TestTermOrder.scala diff --git a/src/test/scala/ap/terfor/equations/TestEquationSet.scala b/core/src/test/scala/ap/terfor/equations/TestEquationSet.scala similarity index 100% rename from src/test/scala/ap/terfor/equations/TestEquationSet.scala rename to core/src/test/scala/ap/terfor/equations/TestEquationSet.scala diff --git a/src/test/scala/ap/terfor/inequalities/TestInequalities.scala b/core/src/test/scala/ap/terfor/inequalities/TestInequalities.scala similarity index 100% rename from src/test/scala/ap/terfor/inequalities/TestInequalities.scala rename to core/src/test/scala/ap/terfor/inequalities/TestInequalities.scala diff --git a/src/test/scala/ap/terfor/linearcombination/TestLinearCombination.scala b/core/src/test/scala/ap/terfor/linearcombination/TestLinearCombination.scala similarity index 100% rename from src/test/scala/ap/terfor/linearcombination/TestLinearCombination.scala rename to core/src/test/scala/ap/terfor/linearcombination/TestLinearCombination.scala diff --git a/src/test/scala/ap/terfor/substitutions/TestSubst.scala b/core/src/test/scala/ap/terfor/substitutions/TestSubst.scala similarity index 100% rename from src/test/scala/ap/terfor/substitutions/TestSubst.scala rename to core/src/test/scala/ap/terfor/substitutions/TestSubst.scala diff --git a/src/test/scala/ap/theories/DivModEncoding.scala b/core/src/test/scala/ap/theories/DivModEncoding.scala similarity index 100% rename from src/test/scala/ap/theories/DivModEncoding.scala rename to core/src/test/scala/ap/theories/DivModEncoding.scala diff --git a/core/src/test/scala/ap/util/Prop.scala b/core/src/test/scala/ap/util/Prop.scala new file mode 100644 index 000000000..6570e881a --- /dev/null +++ b/core/src/test/scala/ap/util/Prop.scala @@ -0,0 +1,82 @@ +/** + * This file is part of Princess, a theorem prover for Presburger + * arithmetic with uninterpreted predicates. + * + * + * Copyright (C) 2024 Philipp Ruemmer + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * * Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * * Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * * Neither the name of the authors nor the names of their + * contributors may be used to endorse or promote products derived from + * this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE + * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE + * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER + * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, + * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE + * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +package ap.util + +import java.io.{ByteArrayOutputStream, PrintStream} + +import org.scalacheck.Properties + +object Prop { + + def assertEquals(a : Any, b : Any) : Unit = + assert(a == b) + + def assertEquals(msg : String, a : Any, b : Any) : Unit = + assert(a == b, msg) + + def assertTrue(b : Boolean) : Unit = + assert(b) + + def assertTrue(msg : String, b : Boolean) : Unit = + assert(b, msg) + +} + +trait ExtraAssertions extends Properties { + + def checkOutput(expected : String)(comp : => Unit) : Boolean = { + val output = { + val baos = new ByteArrayOutputStream + val ps = new PrintStream(baos) + Console.withOut(ps)(comp) + ps.flush() + baos.toString + } + + if (output == expected) { + true + } else if (expected == "") { + println(output) + false + } else { + for (((exp, seen), line) <- + (expected.linesIterator zip output.linesIterator).zipWithIndex) { + if (exp != seen) + Console.err.println(f"${name}:${line}: ${seen}") + } + false + } + } + +} From 724fc2da266b154a926590ea78389e20201eba8c Mon Sep 17 00:00:00 2001 From: "P. Oscar Boykin" Date: Sat, 21 Feb 2026 21:31:28 -1000 Subject: [PATCH 4/6] Remove design doc from tracked changes --- docs/scala-js-migration-plan.md | 407 -------------------------------- 1 file changed, 407 deletions(-) delete mode 100644 docs/scala-js-migration-plan.md diff --git a/docs/scala-js-migration-plan.md b/docs/scala-js-migration-plan.md deleted file mode 100644 index 444019036..000000000 --- a/docs/scala-js-migration-plan.md +++ /dev/null @@ -1,407 +0,0 @@ -# Scala.js Migration Plan for Princess - -Date: 2026-02-22 - -## Goal and scope - -This document lists **blocking issues** to run Princess on Scala.js, evaluates moving parsing to a pure-Scala parser (cats-parse), and proposes a phased work schedule. - -Assumptions used for this plan: - -- Primary target is a Scala.js library build (browser and/or Node), not a JVM CLI binary. -- Required minimum feature set for first usable Scala.js release: - - parse SMT-LIB from strings/readers, - - run core solving APIs, - - expose results without JVM threads/queues. -- JVM-only entry points (CLI, Swing UI, daemon server, portfolio multi-threading) can remain JVM modules. - -## Executive summary - -The largest blockers are: - -1. Parser stack depends on generated Java/CUP/JFlex parsers and JVM jars. -2. Core API execution model depends on JVM threads and blocking queues. -3. Build is not set up as a Scala.js cross-project and uses JVM-only dependency wiring. -4. Core code has coupling to `CmdlMain` (CLI object), which drags JVM-only code into library paths. - -A realistic path is: - -- split into `core` (cross JVM/JS) and `jvm-app` modules, -- replace SMT-LIB and Princess parsers with cats-parse (or equivalent pure Scala parser), -- replace `Thread`/`LinkedBlockingQueue`/`ConcurrentHashMap` usage in shared code with Scala.js-safe primitives, -- keep CLI/server/GUI/portfolio parallel execution in JVM-only module. - -## Blocking issues - -### B1. Build architecture is JVM-only - -**Evidence** - -- `build.sbt:73-90` wires `parser` and `smt-parser` subprojects around prebuilt JVM jars. -- `build.sbt:95-99` makes root depend on those parser subprojects. -- `build.sbt:112-116` adds JVM `java-cup-runtime` and JVM dependency style (`%%`) for parser-combinators. -- `project/assembly.sbt:1-2` has assembly/native-image setup, but no Scala.js plugin/cross-project setup. - -**Why this blocks Scala.js** - -Scala.js cannot consume JVM bytecode parser jars (`parser.jar`, `smt-parser.jar`) as source-level JS-compatible code. - -**Required action** - -- Introduce cross-project layout (`coreJVM/coreJS`). -- Remove parser-jar dependency from shared module. -- Add Scala.js plugin and JS-specific dependency coordinates (`%%%` where needed). - ---- - -### B2. SMT-LIB parser is generated Java (BNFC + CUP + JFlex) - -**Evidence** - -- `smt-parser/Makefile:18-36` generates Java lexer/parser with BNFC/CUP/JFlex. -- `src/main/scala/ap/parser/SMTParser2InputAbsy.scala:57-58` imports generated `ap.parser.smtlib` AST/parser classes. -- `src/main/scala/ap/parser/SMTParser2InputAbsy.scala:229-230` instantiates generated `Yylex` and `parser`. -- `src/main/scala/ap/parser/SMTParsingUtils.scala:37-38` imports generated classes; `:47-48` uses generated parser. -- `src/main/scala/ap/parser/SMTParseableTheory.scala:37` and `:95-106` expose generated AST types in extension interfaces. - -**Why this blocks Scala.js** - -Generated parser/AST classes are Java bytecode and JVM runtime dependent. - -**Required action** - -- Replace with pure Scala parser implementation (cats-parse recommended). -- Define Scala AST model and remove/bridge `smtlib.Absyn.*` from shared interfaces. - ---- - -### B3. Princess `.pri` parser is generated Java (BNFC + CUP + JFlex) - -**Evidence** - -- `parser/Makefile:34-50` generates Java lexer/parser and classes. -- `src/main/scala/ap/parser/ApParser2InputAbsy.scala:46-47` imports generated `ap.parser.ap_input.*` classes. -- `src/main/scala/ap/parser/ApParser2InputAbsy.scala:87-88` uses generated `Yylex` and `parser`. - -**Why this blocks Scala.js** - -Same root issue as SMT-LIB parser: JVM generated parser stack. - -**Required action** - -- Port `.pri` grammar to pure Scala parser (cats-parse). -- Keep translator logic but retarget it to pure Scala AST. - ---- - -### B4. Core solving API uses JVM threading + blocking queues - -**Evidence** - -- `src/main/scala/ap/api/SimpleAPI.scala:58` imports `LinkedBlockingQueue` and `TimeUnit`. -- `src/main/scala/ap/api/SimpleAPI.scala:4462-4475` creates blocking queues and a dedicated `Thread`. -- `src/main/scala/ap/api/SimpleAPI.scala:2144-2147` calls blocking/polling queue methods. -- `src/main/scala/ap/api/ProofThread.scala:44` imports `LinkedBlockingQueue`; `:104` uses `.take`. - -**Why this blocks Scala.js** - -Scala.js has no JVM threads or blocking queue semantics. - -**Required action** - -- Replace proof-thread command loop with Scala.js-safe async model (Future/Promise/event loop), or a synchronous single-thread mode with explicit async wrapper. - ---- - -### B5. Additional JVM concurrency primitives in shared/near-shared code - -**Evidence** - -- `src/main/scala/ap/util/OpCounters.scala:40-41` uses `ConcurrentHashMap` and `LongAdder`. -- `src/main/scala/ap/util/Timer.scala:39` imports `java.lang.Thread` and checks thread identity at `:87-88`. -- `src/main/scala/ap/ParallelFileProver.scala:44,47,492` uses `SyncVar`, blocking queues, and threads. -- `src/main/scala/ap/ServerMain.scala:39,95` uses `Semaphore` and threads. -- `src/main/scala/ap/interpolants/WolverineInterface.scala:39,111,148` uses `Executors` and `Await.result`. - -**Why this blocks Scala.js** - -These APIs are JVM-only or rely on blocking semantics not available in Scala.js. - -**Required action** - -- In shared code: replace with Scala collections + `Future`/`Promise` primitives. -- Move server/portfolio/daemon behavior to JVM-only modules. - ---- - -### B6. Core code is coupled to CLI object (`CmdlMain`) - -**Evidence** - -- `src/main/scala/ap/api/SimpleAPI.scala:66` references `CmdlMain.version`. -- `src/main/scala/ap/api/SimpleAPI.scala:2425` calls `CmdlMain.doPrintTextCertificate`. -- `src/main/scala/ap/parser/SMTParser2InputAbsy.scala:1591,1597` uses `CmdlMain.printGreeting/version`. -- `src/main/scala/ap/proof/ConstraintSimplifier.scala:158,161` uses `CmdlMain.NullStream`. -- `src/main/scala/ap/theories/nia/Gaussian.scala:73` uses `CmdlMain.NullStream`. - -**Why this blocks Scala.js** - -`CmdlMain` is CLI-centric and includes JVM file/process style logic. This coupling prevents clean `core` extraction. - -**Required action** - -- Extract shared constants/utilities (`version`, null output stream, certificate formatting facade) into platform-neutral modules. -- Keep CLI wiring in JVM module. - ---- - -### B7. File/network/UI features are JVM-specific and must be isolated - -**Evidence** - -- `src/main/scala/ap/CmdlMain.scala:267,288,379,1039` uses `FileOutputStream`/`FileReader`. -- `src/main/scala/ap/JavaWrapper.scala:82-86` uses `java.io.File`/`FileReader`. -- `src/main/scala/ap/parser/TPTPTParser.scala:1384-1387` resolves includes via env var + `FileReader`. -- `src/main/scala/ap/ServerMain.scala:41,64` uses `java.net.ServerSocket`. -- `src/main/scala/ap/DialogMain.scala:44-46` uses Swing/AWT. - -**Why this blocks Scala.js** - -No JVM filesystem/socket/Swing in Scala.js runtime. - -**Required action** - -- Put these features in JVM-only modules. -- For JS, expose string/reader-based APIs and optional host callbacks for include/file resolution. - ---- - -### B8. Scala version baseline needs simplification for Scala.js work - -**Evidence** - -- `build.sbt:56-57` cross-builds `2.11.12` and `2.12.20`. - -**Why this blocks or slows migration** - -Practical Scala.js migration + modern parser libraries is significantly easier if shared code targets one modern Scala line (at least 2.12, usually 2.13+). - -**Required action** - -- Drop 2.11 in shared module migration branch. -- Stabilize on one Scala line for cross-platform core during migration. - -## Parser migration evaluation (cats-parse) - -## Current parser landscape - -- SMT-LIB: Java-generated parser + Java-generated AST + large Scala translator (`SMTParser2InputAbsy.scala`, ~4.4k LOC). -- Princess `.pri`: Java-generated parser + AST + large translator (`ApParser2InputAbsy.scala`, ~1.3k LOC). -- TPTP: already pure Scala parser combinators (`TPTPTParser.scala`), but with JVM file-include behavior. - -## Why cats-parse is a good fit - -- Pure Scala, Scala.js compatible. -- Fine-grained control over lexical and syntactic layers. -- Deterministic behavior and explicit error reporting. -- Avoids generated Java artifacts and Java collection bridging. - -## Major migration design choices - -### Choice 1: AST compatibility vs direct translation - -- **AST compatibility approach (recommended first)**: - - create pure Scala ASTs matching current translator expectations, - - keep most semantic translation logic in place, - - reduces churn and regression risk. -- **Direct translation approach**: - - parse directly into `IExpression`/internal forms, - - less intermediate AST code long-term, - - much higher short-term risk and rewrite cost. - -### Choice 2: TPTP parser now vs later - -- Keep existing TPTP parser-combinators initially and only isolate file include (`include(...)`) behind callback. -- Optional later migration of TPTP to cats-parse for uniformity/performance. - -## Estimated effort for parser migration - -- SMT-LIB parser + incremental command stream parity: **3-4 weeks**. -- `.pri` parser parity: **2-3 weeks**. -- TPTP parser port to cats-parse (optional): **1-2 weeks**. - -## Concurrency migration evaluation (Scala.js-safe primitives) - -## Current model - -- `SimpleAPI` offloads solving to a dedicated JVM thread and communicates through blocking queues. -- External API offers polling/blocking status retrieval. - -## Scala.js-safe replacement options - -### Option A: Synchronous core + async facade (recommended) - -- Core solver runs synchronously in same thread. -- JS facade exposes `Future`-based API for host integration. -- In browser, run solver in a Web Worker for responsiveness. - -Pros: - -- Minimal invasive changes to solver internals. -- Clear separation between solver determinism and host scheduling. - -Cons: - -- Some `SimpleAPI` status semantics (`Running`, blocking `getStatus(true)`) need adaptation/deprecation in JS profile. - -### Option B: Fully async command loop in shared code - -- Reimplement command processing as Promise/Future mailbox. - -Pros: - -- Closer to current command architecture. - -Cons: - -- More complexity without true parallelism in Scala.js. - -## Concrete replacements - -- `Thread` + `LinkedBlockingQueue` -> `Future`/`Promise` + immutable/mutable queue in event loop. -- `poll(timeout, TimeUnit)` -> deadline-aware Future composition (no blocking). -- `ConcurrentHashMap`/`LongAdder` -> plain mutable map counters in JS/shared path. -- `Await.result` -> non-blocking Future chains. - -## Proposed target architecture - -- `princess-core` (cross JVM/JS): - - solver core, - - parser frontends (pure Scala), - - shared utilities, - - cross-platform API surface. -- `princess-jvm-app` (JVM only): - - `CmdlMain`, `ServerMain`, `DialogMain`, `ParallelFileProver`, `JavaWrapper`, warmup/daemon features. -- `princess-js` (JS only wrappers): - - JS-friendly entrypoints, - - worker integration helpers, - - optional include/file resolver callbacks. - -## Detailed work plan and schedule - -Schedule below assumes **2 engineers full-time** and aims for a first JS release in ~10 weeks. - -### Phase 0 (Week 1): migration scaffolding and decisions - -Deliverables: - -- Define target runtime matrix (browser, Node, or both). -- Create module split (`core` cross-project + JVM app module). -- Add Scala.js build plumbing and first empty JS compile target. - -Exit criteria: - -- `coreJS` compiles with a minimal placeholder API. -- JVM app still builds unchanged. - -### Phase 1 (Weeks 2-3): decouple core from JVM app objects - -Tasks: - -- Remove direct references from core to `CmdlMain` (`SimpleAPI`, parser get-info path, simplifier, gaussian). -- Introduce shared constants/util abstractions. -- Move clearly JVM-only files to JVM module (CLI/server/gui/portfolio wrappers). - -Exit criteria: - -- Shared module has no references to JVM entrypoint classes. -- No `java.net`, Swing/AWT, or daemon/server code in shared sources. - -### Phase 2 (Weeks 3-6): parser migration to pure Scala - -Tasks: - -- Implement SMT-LIB lexer/parser in cats-parse. -- Preserve incremental SMT command processing behavior currently in `processIncrementally`. -- Implement `.pri` parser in cats-parse. -- Bridge/replace `SMTParseableTheory` AST interfaces. - -Test plan: - -- Reuse `testcases/smtlib-parser` and `testcases/adt` parser-heavy suites. -- Add parser roundtrip/error-location checks. - -Exit criteria: - -- No dependency on `parser.jar`, `smt-parser.jar`, `java-cup-runtime` in shared module. -- Parser regression suites pass at agreed threshold (>= 99% identical outputs, known deltas documented). - -### Phase 3 (Weeks 6-8): concurrency and API execution model - -Tasks: - -- Replace `SimpleAPI` proof-thread queue model with JS-safe model (recommended Option A). -- Remove blocking queue operations in shared API. -- Refactor `OpCounters` and `Timer` implementations for cross-platform compatibility. - -Test plan: - -- API behavioral tests for `checkSat` / status transitions / model extraction. -- Timeout and cancellation contract tests in JVM and JS profiles. - -Exit criteria: - -- Shared module has no `java.util.concurrent.*` usage. -- JS build exposes non-blocking API with documented semantics. - -### Phase 4 (Weeks 8-9): platform adapters and feature gating - -Tasks: - -- JVM module keeps CLI/server/portfolio behavior. -- JS module adds browser/Node adapters (input from strings; optional include resolver for TPTP). -- Explicitly gate unsupported features in JS (server daemon, Swing UI, multi-thread portfolio). - -Exit criteria: - -- Feature matrix document completed. -- JS runtime behavior for unsupported features is explicit (compile-time exclusion or clear runtime error). - -### Phase 5 (Weeks 9-10): stabilization and release prep - -Tasks: - -- Performance baseline against representative SMT-LIB workloads. -- Memory and responsiveness checks for browser worker integration. -- Documentation and migration notes for API users. - -Exit criteria: - -- Green CI for JVM + JS core builds. -- Release candidate with known-issues list. - -## Risk register and mitigations - -1. Parser parity regressions (highest risk). - - Mitigation: preserve translator behavior; run full parser corpus on each milestone. -2. API semantic drift from blocking to async model. - - Mitigation: define JS-specific status contract early and keep compatibility wrappers on JVM. -3. Hidden core/JVM coupling. - - Mitigation: enforce module boundaries in build; fail CI on forbidden package imports. -4. Browser responsiveness for heavy proofs. - - Mitigation: worker-based execution from first JS beta. - -## Acceptance criteria for “Scala.js-ready” - -- Shared core compiles/runs on Scala.js without JVM parser jars and without Java concurrency APIs. -- SMT-LIB parsing and solving works from string input in JS runtime. -- Core test subset passes in both JVM and JS pipelines. -- JVM-specific tools remain available through dedicated JVM module. - -## Immediate next actions (first 2 weeks) - -1. Create `core` cross-project and move solver/parser/shared files there. -2. Remove direct `CmdlMain` dependencies from shared code. -3. Prototype cats-parse SMT-LIB command parser for `(set-logic ...)`, `(assert ...)`, `(check-sat)`, `(exit)` plus error reporting. -4. Decide and document JS API contract (`Future`-first vs status polling emulation). - From 246d7a9137227368c978745f23e84ddad13120e8 Mon Sep 17 00:00:00 2001 From: "P. Oscar Boykin" Date: Sat, 21 Feb 2026 21:54:23 -1000 Subject: [PATCH 5/6] Make core utils Scala.js-safe (remove Thread/CHM usage) --- core/src/main/scala/ap/util/OpCounters.scala | 19 ++++++------------- core/src/main/scala/ap/util/Timer.scala | 14 -------------- 2 files changed, 6 insertions(+), 27 deletions(-) diff --git a/core/src/main/scala/ap/util/OpCounters.scala b/core/src/main/scala/ap/util/OpCounters.scala index 0677ba57c..e230bf938 100644 --- a/core/src/main/scala/ap/util/OpCounters.scala +++ b/core/src/main/scala/ap/util/OpCounters.scala @@ -35,10 +35,6 @@ package ap.util import scala.util.DynamicVariable import scala.collection.mutable.{HashMap => MHashMap} -import scala.collection.JavaConverters._ - -import java.util.concurrent.ConcurrentHashMap -import java.util.concurrent.atomic.LongAdder /** * Object to implement different kinds of performance counters. Such @@ -98,25 +94,22 @@ object OpCounters { class CounterState { - private val counters = new ConcurrentHashMap[Counter, LongAdder] + private val counters = new MHashMap[Counter, Long] { + override def default(c : Counter) : Long = 0L + } private val startTime = System.currentTimeMillis - private val createAdder = - new java.util.function.Function[Counter, LongAdder] { - def apply(c : Counter) : LongAdder = new LongAdder - } - def inc(c : Counter) : Unit = - counters.computeIfAbsent(c, createAdder).increment() + counters += (c -> (counters(c) + 1L)) def apply(c : Counter) : Long = c match { case Milliseconds => System.currentTimeMillis - startTime - case c => counters.computeIfAbsent(c, createAdder).sum() + case c => counters(c) } def counterIterator : Iterator[Counter] = - Iterator(Milliseconds) ++ counters.keys.asScala + Iterator.single(Milliseconds) ++ counters.keysIterator } diff --git a/core/src/main/scala/ap/util/Timer.scala b/core/src/main/scala/ap/util/Timer.scala index 76dfb0e1c..289240a74 100644 --- a/core/src/main/scala/ap/util/Timer.scala +++ b/core/src/main/scala/ap/util/Timer.scala @@ -36,8 +36,6 @@ package ap.util; import scala.collection.mutable.{ArrayStack => Stack, HashMap, ArrayBuilder} import scala.util.Sorting -import java.lang.Thread - /** * Object for measuring the time needed by the various tasks, methods, etc. * The object, in particular, supports nested operations that call each other @@ -70,7 +68,6 @@ object Timer { startTime = now } - private var lastThread : Thread = null private var timerDisabled = false def measure[A](op : String)(comp : => A) : A = @@ -82,16 +79,6 @@ object Timer { comp } else { - - if (lastThread == null) { - lastThread = Thread.currentThread - } else if (!(lastThread eq Thread.currentThread)) { - Console.err.println( - "Warning: disabling ap.util.Timer due to multi-threading") - timerDisabled = true - return measure(op)(comp) - } - addTime callCounters += (op -> (callCounters(op) + 1)) runningOps push op @@ -111,7 +98,6 @@ object Timer { accumulatedTimes.clear callCounters.clear runningOps.clear - lastThread = null timerDisabled = false } From f5a41b4edd1063a1bb5a5368d0f1828bda8124f5 Mon Sep 17 00:00:00 2001 From: "P. Oscar Boykin" Date: Sat, 21 Feb 2026 22:09:28 -1000 Subject: [PATCH 6/6] Revert "Make core utils Scala.js-safe (remove Thread/CHM usage)" This reverts commit 246d7a9137227368c978745f23e84ddad13120e8. --- core/src/main/scala/ap/util/OpCounters.scala | 19 +++++++++++++------ core/src/main/scala/ap/util/Timer.scala | 14 ++++++++++++++ 2 files changed, 27 insertions(+), 6 deletions(-) diff --git a/core/src/main/scala/ap/util/OpCounters.scala b/core/src/main/scala/ap/util/OpCounters.scala index e230bf938..0677ba57c 100644 --- a/core/src/main/scala/ap/util/OpCounters.scala +++ b/core/src/main/scala/ap/util/OpCounters.scala @@ -35,6 +35,10 @@ package ap.util import scala.util.DynamicVariable import scala.collection.mutable.{HashMap => MHashMap} +import scala.collection.JavaConverters._ + +import java.util.concurrent.ConcurrentHashMap +import java.util.concurrent.atomic.LongAdder /** * Object to implement different kinds of performance counters. Such @@ -94,22 +98,25 @@ object OpCounters { class CounterState { - private val counters = new MHashMap[Counter, Long] { - override def default(c : Counter) : Long = 0L - } + private val counters = new ConcurrentHashMap[Counter, LongAdder] private val startTime = System.currentTimeMillis + private val createAdder = + new java.util.function.Function[Counter, LongAdder] { + def apply(c : Counter) : LongAdder = new LongAdder + } + def inc(c : Counter) : Unit = - counters += (c -> (counters(c) + 1L)) + counters.computeIfAbsent(c, createAdder).increment() def apply(c : Counter) : Long = c match { case Milliseconds => System.currentTimeMillis - startTime - case c => counters(c) + case c => counters.computeIfAbsent(c, createAdder).sum() } def counterIterator : Iterator[Counter] = - Iterator.single(Milliseconds) ++ counters.keysIterator + Iterator(Milliseconds) ++ counters.keys.asScala } diff --git a/core/src/main/scala/ap/util/Timer.scala b/core/src/main/scala/ap/util/Timer.scala index 289240a74..76dfb0e1c 100644 --- a/core/src/main/scala/ap/util/Timer.scala +++ b/core/src/main/scala/ap/util/Timer.scala @@ -36,6 +36,8 @@ package ap.util; import scala.collection.mutable.{ArrayStack => Stack, HashMap, ArrayBuilder} import scala.util.Sorting +import java.lang.Thread + /** * Object for measuring the time needed by the various tasks, methods, etc. * The object, in particular, supports nested operations that call each other @@ -68,6 +70,7 @@ object Timer { startTime = now } + private var lastThread : Thread = null private var timerDisabled = false def measure[A](op : String)(comp : => A) : A = @@ -79,6 +82,16 @@ object Timer { comp } else { + + if (lastThread == null) { + lastThread = Thread.currentThread + } else if (!(lastThread eq Thread.currentThread)) { + Console.err.println( + "Warning: disabling ap.util.Timer due to multi-threading") + timerDisabled = true + return measure(op)(comp) + } + addTime callCounters += (op -> (callCounters(op) + 1)) runningOps push op @@ -98,6 +111,7 @@ object Timer { accumulatedTimes.clear callCounters.clear runningOps.clear + lastThread = null timerDisabled = false }