Skip to content

[WIP] Quality of life improvements and cleanup #4

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
amandasystems wants to merge 4 commits into
base: scala-2.13
Choose a base branch
from
Open

[WIP] Quality of life improvements and cleanup #4

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
2322146
Quality of life improvements and cleanup
amandasystems Feb 16, 2023
5f220e8
Drop deprecated use of `SyncVar`.
amandasystems Feb 16, 2023
d80cb31
Nicer and probably more correct version
amandasystems Feb 20, 2023
4756c83
Move overloaded methods next to each other, add comment
amandasystems Feb 20, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/ap/ParallelFileProver.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -404,7 +404,7 @@ object ParallelFileProver {
var startTime : Long = 0

def localStoppingCond : Boolean = actorStopped || {
subProverCommands.poll(0, TimeUnit.SECONDS) match {
subProverCommands.poll() match {
case null => // nothing
case SubProverStop => actorStopped = true
case SubProverResume(u) => runUntil = u
Expand Down
12 changes: 6 additions & 6 deletions src/ap/api/ProofThread.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,14 +33,14 @@

package ap.api

import ap.proof.{ModelSearchProver, ExhaustiveProver}
import ap.proof.{ExhaustiveProver, ModelSearchProver}
import ap.terfor.conjunctions.Conjunction
import ap.proof.certificates.{Certificate, LemmaBase}
import ap.terfor.TermOrder
import ap.parameters.{GoalSettings, Param}
import ap.util.{Debug, Timeout}

import scala.concurrent.SyncVar
import java.util.concurrent.LinkedBlockingQueue

object ProofThreadRunnable {

Expand Down Expand Up @@ -78,10 +78,10 @@ object ProofThreadRunnable {
}

class ProofThreadRunnable(
proverCmd : SyncVar[ProofThreadRunnable.ProverCommand],
proverRes : SyncVar[ProofThreadRunnable.ProverResult],
enableAssert : Boolean,
logging : Set[Param.LOG_FLAG]) extends Runnable {
proverCmd : LinkedBlockingQueue[ProofThreadRunnable.ProverCommand],
proverRes : LinkedBlockingQueue[ProofThreadRunnable.ProverResult],
enableAssert : Boolean,
logging : Set[Param.LOG_FLAG]) extends Runnable {
import ProofThreadRunnable._

private var stopProofTaskVar = false
Expand Down
109 changes: 43 additions & 66 deletions src/ap/api/SimpleAPI.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,38 +35,27 @@ package ap.api

import ap._
import ap.basetypes.{IdealInt, Tree}
import ap.interpolants.{InterpolationContext, Interpolator, ProofSimplifier}
import ap.parameters._
import ap.parser.IExpression.Sort
import ap.parser._
import ap.parameters.{PreprocessingSettings, GoalSettings, ParserSettings,
ReducerSettings, Param}
import ap.terfor.{TermOrder, Formula}
import ap.terfor.TerForConvenience
import ap.proof.{ModelSearchProver, ExhaustiveProver}
import ap.proof.goal.{SymbolWeights, FormulaTask}
import ap.proof.certificates.{Certificate, LemmaBase, CertFormula}
import ap.proof.certificates.{CertFormula, Certificate}
import ap.proof.goal.SymbolWeights
import ap.proof.theoryPlugins.{Plugin, PluginSequence}
import ap.proof.tree.{NonRandomDataSource, SeededRandomDataSource}
import ap.interpolants.{ProofSimplifier, InterpolationContext, Interpolator}
import ap.proof.{ExhaustiveProver, ModelSearchProver}
import ap.terfor.conjunctions._
import ap.terfor.equations.ReduceWithEqs
import ap.terfor.preds.{Atom, PredConj, ReduceWithPredLits}
import ap.terfor.preds.{Atom, ReduceWithPredLits}
import ap.terfor.substitutions.ConstantSubst
import ap.terfor.conjunctions.{Conjunction, ReduceWithConjunction,
IterativeClauseMatcher, Quantifier,
LazyConjunction, SeqReducerPluginFactory}
import ap.theories.{Theory, TheoryCollector, TheoryRegistry,
SimpleArray, MulTheory, Incompleteness, ADT}
import ap.proof.theoryPlugins.{Plugin, PluginSequence}
import ap.types.{SortedConstantTerm, SortedIFunction,
MonoSortedIFunction, MonoSortedPredicate,
SortedPredicate, TypeTheory}
import ap.util.{Debug, Timeout, Seqs}

import IExpression.Sort
import Signature.PredicateMatchConfig

import scala.collection.mutable.{HashMap => MHashMap, HashSet => MHashSet,
ArrayStack, LinkedHashMap, ArrayBuffer}
import scala.concurrent.SyncVar
import ap.terfor.{Formula, TerForConvenience, TermOrder}
import ap.theories._
import ap.types._
import ap.util.{Debug, Seqs, Timeout}

import java.io.File
import java.util.concurrent.{LinkedBlockingQueue, TimeUnit}
import scala.collection.mutable.{ArrayBuffer, LinkedHashMap, HashMap => MHashMap, HashSet => MHashSet}

object SimpleAPI {

Expand Down Expand Up @@ -267,7 +256,7 @@ object SimpleAPI {
val Init, AtPartialModel, AtFullModel = Value
}

private val badStringChar = """[^a-zA-Z_0-9']""".r
private val badStringChar = """[^a-zA-Z_\d']""".r

private def sanitiseHelp(s : String) : String =
badStringChar.replaceAllIn(s, (m : scala.util.matching.Regex.Match) =>
Expand Down Expand Up @@ -320,8 +309,8 @@ class SimpleAPI private (enableAssert : Boolean,
randomSeed : Option[Int],
logging : Set[Param.LOG_FLAG] = Set()) {

import SimpleAPI._
import ProofThreadRunnable._
import SimpleAPI._

private val apiStack = new APIStack

Expand Down Expand Up @@ -359,7 +348,7 @@ class SimpleAPI private (enableAssert : Boolean,
}

private def doDumpSMT(comp : => Unit) =
if (dumpSMT != None) Console.withOut(dumpSMTStream) {
if (dumpSMT.isDefined) Console.withOut(dumpSMTStream) {
comp
}

Expand All @@ -373,7 +362,7 @@ class SimpleAPI private (enableAssert : Boolean,
}

private def doDumpScala(comp : => Unit) =
if (dumpScala != None) Console.withOut(dumpScalaStream) {
if (dumpScala.isDefined) Console.withOut(dumpScalaStream) {
comp
}

Expand Down Expand Up @@ -402,14 +391,7 @@ class SimpleAPI private (enableAssert : Boolean,
// make sure that no prover command is queued at the moment;
// repeatedly calling <code>shutDown</code> would otherwise
// hang

try {
if (proverCmd.isSet)
proverCmd take 0
} catch {
case _ : NoSuchElementException => // nothing
}

proverCmd.clear()
proverCmd put ShutdownCommand
}

Expand Down Expand Up @@ -625,7 +607,6 @@ class SimpleAPI private (enableAssert : Boolean,
private def createConstantRaw(rawName : String,
scalaCmd : String,
sort : Sort) : IExpression.ConstantTerm = {
import IExpression._

restartProofThread
resetModel
Expand Down Expand Up @@ -692,7 +673,6 @@ class SimpleAPI private (enableAssert : Boolean,
scalaCmd : String,
sort : Sort)
: IndexedSeq[IExpression.ConstantTerm] = {
import IExpression._
val cs = (for (i <- nums)
yield {
val c = sort newConstant (prefix + i)
Expand Down Expand Up @@ -1360,7 +1340,6 @@ class SimpleAPI private (enableAssert : Boolean,
* cannot be used within triggers.
*/
def createRelation(rawName : String, argSorts : Seq[Sort]) = {
import IExpression._

val name = sanitise(rawName)
val r = MonoSortedPredicate(name, argSorts)
Expand Down Expand Up @@ -1937,7 +1916,7 @@ class SimpleAPI private (enableAssert : Boolean,
getStatusHelp(false) match {
case ProverStatus.Unknown => {
//-BEGIN-ASSERTION-/////////////////////////////////////////////////////
Debug.assertInt(SimpleAPI.AC, !proverRes.isSet)
Debug.assertInt(SimpleAPI.AC, proverRes.isEmpty)
//-END-ASSERTION-///////////////////////////////////////////////////////

flushTodo
Expand All @@ -1952,7 +1931,7 @@ class SimpleAPI private (enableAssert : Boolean,

if (constructProofs)
// Restart, but keep lemmas that have been derived previously
proverCmd put CheckSatCommand(currentProver, true, true)
proverCmd put CheckSatCommand(currentProver, needLemmaBase = true, reuseLemmaBase = true)
else
// We can just add new formulas to the running proof thread,
// without a complete restart
Expand Down Expand Up @@ -1984,7 +1963,7 @@ class SimpleAPI private (enableAssert : Boolean,
// use a ModelCheckProver
lastStatus = ProverStatus.Running
proverCmd put CheckSatCommand(currentProver, constructProofs,
false)
reuseLemmaBase = false)
}

}
Expand Down Expand Up @@ -2046,7 +2025,7 @@ class SimpleAPI private (enableAssert : Boolean,
checkTimeout

//-BEGIN-ASSERTION-/////////////////////////////////////////////////////////
Debug.assertInt(SimpleAPI.AC, !proverRes.isSet)
Debug.assertInt(SimpleAPI.AC, proverRes.isEmpty)
//-END-ASSERTION-///////////////////////////////////////////////////////////

lastStatus = ProverStatus.Running
Expand Down Expand Up @@ -2082,12 +2061,22 @@ class SimpleAPI private (enableAssert : Boolean,
getStatusWithDeadline(block)
}

private def getStatusHelp(block : Boolean) : ProverStatus.Value = {
if (lastStatus == ProverStatus.Running && (block || proverRes.isSet))
evalProverResult(proverRes.take)
@inline
private def getOrUpdateLastStatus(pollExpr: => ProverResult): ProverStatus.Value = {
if (lastStatus == ProverStatus.Running) {
Option(pollExpr).foreach(evalProverResult)
}
lastStatus
}


private def getStatusHelp(block : Boolean) : ProverStatus.Value =
getOrUpdateLastStatus(if (block) proverRes.take() else proverRes.poll())

private def getStatusHelp(timeout : Long) : ProverStatus.Value =
getOrUpdateLastStatus(proverRes.poll(timeout, TimeUnit.MILLISECONDS))
// Experiments (and convention) seems to suggest that polling for zero
// or less time means "finish immediately".

/**
* Query result of the last <code>checkSat</code> or <code>nextModel</code>
* call. Will block until a result is available, or until <code>timeout</code>
Expand All @@ -2099,17 +2088,6 @@ class SimpleAPI private (enableAssert : Boolean,
}
getStatusHelp(timeout)
}

private def getStatusHelp(timeout : Long) : ProverStatus.Value = {
if (lastStatus == ProverStatus.Running &&
// behaviour of SyncVar for timeout 0 is unclear
(if (timeout <= 0)
proverRes.isSet
else
(proverRes get timeout).isDefined))
evalProverResult(proverRes.take)
lastStatus
}

private def evalProverResult(pr : ProverResult) : Unit = pr match {
case UnsatResult => {
Expand Down Expand Up @@ -2308,8 +2286,8 @@ class SimpleAPI private (enableAssert : Boolean,
* <code>ProverStatus.Unsat</code> or <code>ProverStates.Valid</code>,
* produce a certificate in textual/readable format.
*/
def certificateAsString(partNames : Map[Int, PartName],
format : Param.InputFormat.Value) : String = {
def certificateAsString(partNames : Map[Int, PartName] = Map(),
format : Param.InputFormat.Value = Param.InputFormat.Auto) : String = {
doDumpSMT {
println("(get-proof)")
}
Expand Down Expand Up @@ -2993,7 +2971,7 @@ class SimpleAPI private (enableAssert : Boolean,
ensurePartialModel
while (proofThreadStatus != ProofThreadStatus.AtFullModel) {
//-BEGIN-ASSERTION-///////////////////////////////////////////////////////
Debug.assertInt(SimpleAPI.AC, !proverRes.isSet)
Debug.assertInt(SimpleAPI.AC, proverRes.isEmpty)
//-END-ASSERTION-/////////////////////////////////////////////////////////

// let's get a complete model
Expand Down Expand Up @@ -3415,7 +3393,6 @@ class SimpleAPI private (enableAssert : Boolean,
*/
private def reduceTerm(t : ITerm)
: (Conjunction, IExpression.ConstantTerm, TermOrder) = {
import TerForConvenience._
val existential = setupTermEval

val c = new IExpression.ConstantTerm ("c")
Expand Down Expand Up @@ -4339,8 +4316,8 @@ class SimpleAPI private (enableAssert : Boolean,
//
// Prover thread, for the hard work

private val proverRes = new SyncVar[ProverResult]
private val proverCmd = new SyncVar[ProverCommand]
private val proverRes = new LinkedBlockingQueue[ProverResult](1)
private val proverCmd = new LinkedBlockingQueue[ProverCommand](1)

private var proofThreadStatus : ProofThreadStatus.Value = _

Expand Down